		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-iconst

Validate an integer constant.

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

An integer constant is valid iff it has a type according to the table in [C: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-type))
       ((iconst iconst) iconst)
       (value (valid-dec/oct/hex-const iconst.core)))
   (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)))))))

Theorem: typep-of-valid-iconst.type

(defthm typep-of-valid-iconst.type
  (b* (((mv acl2::?erp ?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)