		Search-engine friendly clone of the ACL2 documentation.

Term-checkers-common

Atc-check-iconst

Check if a term represents an integer constant.

Signature
(atc-check-iconst term) → (mv erp yes/no fn type const)
Arguments: term — Guard (pseudo-termp term).
Returns: yes/no — Type (booleanp yes/no).; fn — Type (symbolp fn).; type — Type (typep type).; const — Type (iconstp const).

If the term is a call of a function <type>-<base>-const on a quoted integer constant, we return the ACL2 function symbol, the C type of the term, and the C integer constant represented by the call.

In certain circumstances, we return an error in erp, namely when the term cannot represent any other C construct.

Definitions and Theorems

Function: atc-check-iconst

(defun atc-check-iconst (term)
 (declare (xargs :guard (pseudo-termp term)))
 (let ((__function__ 'atc-check-iconst))
  (declare (ignorable __function__))
  (b*
   (((reterr)
     nil nil (irr-type)
     (irr-iconst))
    ((acl2::fun (no))
     (retok nil nil (irr-type) (irr-iconst)))
    ((mv okp fn args)
     (fty-check-fn-call term))
    ((unless okp) (no))
    ((mv okp type base const)
     (atc-check-symbol-3part fn))
    ((unless (and okp
                  (member-eq type
                             '(sint uint slong ulong sllong ullong))
                  (member-eq base '(dec oct hex))
                  (eq const 'const)))
     (no))
    ((unless (equal (symbol-package-name fn) "C"))
     (reterr
      (msg
       "Invalid function ~x0 encountered: ~
                      it has the form of an integer constant function, ~
                      but it is not in the \"C\" package."
       fn)))
    ((unless (list-lenp 1 args))
     (reterr (raise "Internal error: ~x0 not applied to 1 argument."
                    term)))
    (arg (first args))
    ((unless (pseudo-term-case arg :quote))
     (reterr
      (msg
       "The function ~x0 must be applied to a quoted constant, ~
                      but it is applied to ~x1 instead."
       fn arg)))
    (val (pseudo-term-quote->val arg))
    ((unless (natp val))
     (reterr
      (msg
       "The function ~x0 ~
                      must be applied to a quoted natural number, ~
                      but it is applied to ~x1 instead. ~
                      Since this is required by the guard of ~x0, ~
                      this call is unreachable under the guard."
       fn val)))
    (inrangep (case type
                (sint (sint-integerp val))
                (uint (uint-integerp val))
                (slong (slong-integerp val))
                (ulong (ulong-integerp val))
                (sllong (sllong-integerp val))
                (ullong (ullong-integerp val))
                (t (impossible))))
    ((unless inrangep)
     (reterr
      (msg
       "The function ~x0
                      must be applied to a quoted natural number ~
                      representable in the C type corresponding to ~x1, ~
                      but it is applied to ~x2 instead.
                      This is indicative of provably dead code, ~
                      given that the code is guard-verified."
       fn type val)))
    (base (case base
            (dec (iconst-base-dec))
            (oct (iconst-base-oct))
            (hex (iconst-base-hex))
            (t (impossible))))
    ((mv const type)
     (case type
       (sint (mv (make-iconst :value val
                              :base base
                              :unsignedp nil
                              :length (iconst-length-none))
                 (type-sint)))
       (uint (mv (make-iconst :value val
                              :base base
                              :unsignedp t
                              :length (iconst-length-none))
                 (type-uint)))
       (slong (mv (make-iconst :value val
                               :base base
                               :unsignedp nil
                               :length (iconst-length-long))
                  (type-slong)))
       (ulong (mv (make-iconst :value val
                               :base base
                               :unsignedp t
                               :length (iconst-length-long))
                  (type-ulong)))
       (sllong (mv (make-iconst :value val
                                :base base
                                :unsignedp nil
                                :length (iconst-length-llong))
                   (type-sllong)))
       (ullong (mv (make-iconst :value val
                                :base base
                                :unsignedp t
                                :length (iconst-length-llong))
                   (type-ullong)))
       (t (mv (impossible) (impossible))))))
   (retok t fn type const))))

Theorem: booleanp-of-atc-check-iconst.yes/no

(defthm booleanp-of-atc-check-iconst.yes/no
  (b* (((mv acl2::?erp ?yes/no ?fn ?type ?const)
        (atc-check-iconst term)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: symbolp-of-atc-check-iconst.fn

(defthm symbolp-of-atc-check-iconst.fn
  (b* (((mv acl2::?erp ?yes/no ?fn ?type ?const)
        (atc-check-iconst term)))
    (symbolp fn))
  :rule-classes :rewrite)

Theorem: typep-of-atc-check-iconst.type

(defthm typep-of-atc-check-iconst.type
  (b* (((mv acl2::?erp ?yes/no ?fn ?type ?const)
        (atc-check-iconst term)))
    (typep type))
  :rule-classes :rewrite)

Theorem: iconstp-of-atc-check-iconst.const

(defthm iconstp-of-atc-check-iconst.const
  (b* (((mv acl2::?erp ?yes/no ?fn ?type ?const)
        (atc-check-iconst term)))
    (iconstp const))
  :rule-classes :rewrite)

Theorem: type-integerp-of-atc-check-iconst-type

(defthm type-integerp-of-atc-check-iconst-type
  (b* (((mv acl2::?erp ?yes/no ?fn ?type ?const)
        (atc-check-iconst term)))
    (implies yes/no (type-integerp type))))

Theorem: type-nonchar-integerp-of-atc-check-iconst-type

(defthm type-nonchar-integerp-of-atc-check-iconst-type
  (b* (((mv acl2::?erp ?yes/no ?fn ?type ?const)
        (atc-check-iconst term)))
    (implies yes/no (type-nonchar-integerp type))))