• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Soft
      • Bv
      • Imp-language
      • C
        • Syntax-for-tools
        • Atc
        • Language
          • Abstract-syntax
          • Integer-ranges
          • Dynamic-semantics
            • Exec
            • Exec-arrsub
            • Exec-expr-pure
            • Exec-expr-asg
            • Init-value-to-value
            • Exec-memberp
            • Exec-address
            • Apconvert-expr-value
            • Exec-member
            • Exec-unary
            • Init-scope
            • Exec-fun
            • Eval-iconst
            • Exec-block-item
            • Exec-binary-strict-pure
            • Exec-expr-pure-list
            • Eval-binary-strict-pure
            • Exec-expr-call-or-pure
            • Exec-block-item-list
            • Exec-stmt-while
            • Exec-indir
            • Exec-stmt
            • Exec-ident
            • Eval-cast
            • Exec-cast
            • Eval-unary
            • Exec-const
            • Exec-initer
            • Exec-expr-call-or-asg
            • Eval-const
            • Exec-expr-call
          • Static-semantics
          • Grammar
          • Integer-formats
          • Types
          • Portable-ascii-identifiers
          • Values
          • Integer-operations
          • Computation-states
          • Object-designators
          • Implementation-environments
          • Operations
          • Errors
          • Tag-environments
          • Function-environments
          • Character-sets
          • Flexible-array-member-removal
          • Arithmetic-operations
          • Pointer-operations
          • Bytes
          • Keywords
          • Real-operations
          • Array-operations
          • Scalar-operations
          • Structure-operations
        • Representation
        • Transformation-tools
        • Pack
      • Event-macros
      • Java
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Number-theory
      • Cryptography
      • Lists-light
      • Builtins
      • Axe
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Dynamic-semantics

Eval-iconst

Evaluate an integer constant.

Signature

(eval-iconst ic) → val

Arguments

ic — Guard (iconstp ic).

Returns

val — Type (value-resultp val).

This is according to [C:6.4.4.1/5]: based on the suffixes and the base, we find the first type that suffices to represent the value, in the lists indicated in the table, and we return the value of the found type. If the value is too large, we return an error.

This is the dynamic counterpart of check-iconst.

Definitions and Theorems

Function: eval-iconst

(defun eval-iconst (ic)
 (declare (xargs :guard (iconstp ic)))
 (let ((__function__ 'eval-iconst))
  (declare (ignorable __function__))
  (b* (((iconst ic) ic)
       (error (error (list :iconst-out-of-range (iconst-fix ic)))))
    (if ic.unsignedp
        (iconst-length-case ic.length
                            :none (cond ((uint-integerp ic.value)
                                         (value-uint ic.value))
                                        ((ulong-integerp ic.value)
                                         (value-ulong ic.value))
                                        ((ullong-integerp ic.value)
                                         (value-ullong ic.value))
                                        (t error))
                            :long (cond ((ulong-integerp ic.value)
                                         (value-ulong ic.value))
                                        ((ullong-integerp ic.value)
                                         (value-ullong ic.value))
                                        (t error))
                            :llong (cond ((ullong-integerp ic.value)
                                          (value-ullong ic.value))
                                         (t error)))
      (iconst-length-case ic.length :none
                          (if (iconst-base-case ic.base :dec)
                              (cond ((sint-integerp ic.value)
                                     (value-sint ic.value))
                                    ((slong-integerp ic.value)
                                     (value-slong ic.value))
                                    ((sllong-integerp ic.value)
                                     (value-sllong ic.value))
                                    (t error))
                            (cond ((sint-integerp ic.value)
                                   (value-sint ic.value))
                                  ((uint-integerp ic.value)
                                   (value-uint ic.value))
                                  ((slong-integerp ic.value)
                                   (value-slong ic.value))
                                  ((ulong-integerp ic.value)
                                   (value-ulong ic.value))
                                  ((sllong-integerp ic.value)
                                   (value-sllong ic.value))
                                  ((ullong-integerp ic.value)
                                   (value-ullong ic.value))
                                  (t error)))
                          :long
                          (if (iconst-base-case ic.base :dec)
                              (cond ((slong-integerp ic.value)
                                     (value-slong ic.value))
                                    ((sllong-integerp ic.value)
                                     (value-sllong ic.value))
                                    (t error))
                            (cond ((slong-integerp ic.value)
                                   (value-slong ic.value))
                                  ((ulong-integerp ic.value)
                                   (value-ulong ic.value))
                                  ((sllong-integerp ic.value)
                                   (value-sllong ic.value))
                                  ((ullong-integerp ic.value)
                                   (value-ullong ic.value))
                                  (t error)))
                          :llong
                          (if (iconst-base-case ic.base :dec)
                              (cond ((sllong-integerp ic.value)
                                     (value-sllong ic.value))
                                    (t error))
                            (cond ((sllong-integerp ic.value)
                                   (value-sllong ic.value))
                                  ((ullong-integerp ic.value)
                                   (value-ullong ic.value))
                                  (t error))))))))

Theorem: value-resultp-of-eval-iconst

(defthm value-resultp-of-eval-iconst
  (b* ((val (eval-iconst ic)))
    (value-resultp val))
  :rule-classes :rewrite)

Theorem: eval-iconst-of-iconst-fix-ic

(defthm eval-iconst-of-iconst-fix-ic
  (equal (eval-iconst (iconst-fix ic))
         (eval-iconst ic)))

Theorem: eval-iconst-iconst-equiv-congruence-on-ic

(defthm eval-iconst-iconst-equiv-congruence-on-ic
  (implies (iconst-equiv ic ic-equiv)
           (equal (eval-iconst ic)
                  (eval-iconst ic-equiv)))
  :rule-classes :congruence)