		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-iconst

Validate an integer constant.

Signature
(valid-iconst iconst ienv) → (mv erp new-iconst type)
Arguments: iconst — Guard (iconstp iconst).; ienv — Guard (ienvp ienv).
Returns: new-iconst — Type (iconstp new-iconst).; type — Type (typep type).

An integer constant is valid iff it has a type according to the table in [C17:6.4.4.1/5]. We formalize that table here, and we return the type of the constant. If the constant is too large, it does not have a type, and it is invalid.

Definitions and Theorems

Function: valid-iconst

(defun valid-iconst (iconst ienv)
 (declare (xargs :guard (and (iconstp iconst) (ienvp ienv))))
 (let ((__function__ 'valid-iconst))
  (declare (ignorable __function__))
  (b*
   (((reterr) (irr-iconst) (irr-type))
    ((iconst iconst) iconst)
    (value (valid-dec/oct/hex-const iconst.core))
    ((erp type)
     (b* (((reterr) (irr-type)))
      (cond
       ((not iconst.suffix?)
        (if (dec/oct/hex-const-case iconst.core :dec)
            (cond ((sint-rangep value ienv)
                   (retok (type-sint)))
                  ((slong-rangep value ienv)
                   (retok (type-slong)))
                  ((sllong-rangep value ienv)
                   (retok (type-sllong)))
                  (t (reterr (msg "The constant ~x0 is too large."
                                  (iconst-fix iconst)))))
          (cond ((sint-rangep value ienv)
                 (retok (type-sint)))
                ((uint-rangep value ienv)
                 (retok (type-uint)))
                ((slong-rangep value ienv)
                 (retok (type-slong)))
                ((ulong-rangep value ienv)
                 (retok (type-ulong)))
                ((sllong-rangep value ienv)
                 (retok (type-sllong)))
                ((ullong-rangep value ienv)
                 (retok (type-ullong)))
                (t (reterr (msg "The constant ~x0 is too large."
                                (iconst-fix iconst)))))))
       ((isuffix-case iconst.suffix? :u)
        (cond ((uint-rangep value ienv)
               (retok (type-uint)))
              ((ulong-rangep value ienv)
               (retok (type-ulong)))
              ((ullong-rangep value ienv)
               (retok (type-ullong)))
              (t (reterr (msg "The constant ~x0 is too large."
                              (iconst-fix iconst))))))
       ((isuffix-case iconst.suffix? :l)
        (cond
         ((member-eq
               (lsuffix-kind (isuffix-l->length iconst.suffix?))
               '(:locase-l :upcase-l))
          (if (dec/oct/hex-const-case iconst.core :dec)
              (cond ((slong-rangep value ienv)
                     (retok (type-slong)))
                    ((sllong-rangep value ienv)
                     (retok (type-sllong)))
                    (t (reterr (msg "The constant ~x0 is too large."
                                    (iconst-fix iconst)))))
            (cond ((slong-rangep value ienv)
                   (retok (type-slong)))
                  ((ulong-rangep value ienv)
                   (retok (type-ulong)))
                  ((sllong-rangep value ienv)
                   (retok (type-sllong)))
                  ((ullong-rangep value ienv)
                   (retok (type-ullong)))
                  (t (reterr (msg "The constant ~x0 is too large."
                                  (iconst-fix iconst)))))))
         ((member-eq
               (lsuffix-kind (isuffix-l->length iconst.suffix?))
               '(:locase-ll :upcase-ll))
          (if (dec/oct/hex-const-case iconst.core :dec)
              (cond ((sllong-rangep value ienv)
                     (retok (type-sllong)))
                    (t (reterr (msg "The constant ~x0 is too large."
                                    (iconst-fix iconst)))))
            (cond ((sllong-rangep value ienv)
                   (retok (type-sllong)))
                  ((ullong-rangep value ienv)
                   (retok (type-ullong)))
                  (t (reterr (msg "The constant ~x0 is too large."
                                  (iconst-fix iconst)))))))
         (t (prog2$ (impossible) (reterr t)))))
       ((or
         (and
             (isuffix-case iconst.suffix? :ul)
             (member-eq
                  (lsuffix-kind (isuffix-ul->length iconst.suffix?))
                  '(:locase-l :upcase-l)))
         (and
             (isuffix-case iconst.suffix? :lu)
             (member-eq
                  (lsuffix-kind (isuffix-lu->length iconst.suffix?))
                  '(:locase-l :upcase-l))))
        (cond ((ulong-rangep value ienv)
               (retok (type-ulong)))
              ((ullong-rangep value ienv)
               (retok (type-ullong)))
              (t (reterr (msg "The constant ~x0 is too large."
                              (iconst-fix iconst))))))
       ((or
         (and
             (isuffix-case iconst.suffix? :ul)
             (member-eq
                  (lsuffix-kind (isuffix-ul->length iconst.suffix?))
                  '(:locase-ll :upcase-ll)))
         (and
             (isuffix-case iconst.suffix? :lu)
             (member-eq
                  (lsuffix-kind (isuffix-lu->length iconst.suffix?))
                  '(:locase-ll :upcase-ll))))
        (cond ((ullong-rangep value ienv)
               (retok (type-ullong)))
              (t (reterr (msg "The constant ~x0 is too large."
                              (iconst-fix iconst))))))
       (t (prog2$ (impossible) (reterr t))))))
    (info (make-iconst-info :type type
                            :value value))
    (new-iconst (change-iconst iconst :info info)))
   (retok new-iconst type))))

Theorem: iconstp-of-valid-iconst.new-iconst

(defthm iconstp-of-valid-iconst.new-iconst
  (b* (((mv acl2::?erp ?new-iconst ?type)
        (valid-iconst iconst ienv)))
    (iconstp new-iconst))
  :rule-classes :rewrite)

Theorem: typep-of-valid-iconst.type

(defthm typep-of-valid-iconst.type
  (b* (((mv acl2::?erp ?new-iconst ?type)
        (valid-iconst iconst ienv)))
    (typep type))
  :rule-classes :rewrite)

Theorem: valid-iconst-of-iconst-fix-iconst

(defthm valid-iconst-of-iconst-fix-iconst
  (equal (valid-iconst (iconst-fix iconst) ienv)
         (valid-iconst iconst ienv)))

Theorem: valid-iconst-iconst-equiv-congruence-on-iconst

(defthm valid-iconst-iconst-equiv-congruence-on-iconst
  (implies (iconst-equiv iconst iconst-equiv)
           (equal (valid-iconst iconst ienv)
                  (valid-iconst iconst-equiv ienv)))
  :rule-classes :congruence)

Theorem: valid-iconst-of-ienv-fix-ienv

(defthm valid-iconst-of-ienv-fix-ienv
  (equal (valid-iconst iconst (ienv-fix ienv))
         (valid-iconst iconst ienv)))

Theorem: valid-iconst-ienv-equiv-congruence-on-ienv

(defthm valid-iconst-ienv-equiv-congruence-on-ienv
  (implies (ienv-equiv ienv ienv-equiv)
           (equal (valid-iconst iconst ienv)
                  (valid-iconst iconst ienv-equiv)))
  :rule-classes :congruence)