• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • ACL2
  • Macro-libraries
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Set
      • Soft
      • C
        • Syntax-for-tools
          • Disambiguator
          • Abstract-syntax
          • Parser
            • Parse-exprs/decls/stmts
            • Check-full-ppnumber
            • Read-char
            • Parstate
            • Lex-identifier/keyword
            • Lex-oct-iconst-/-dec-fconst
            • Lex-lexeme
            • Parse-external-declaration
            • Parse-cast-expression
            • Lex-isuffix-if-present
            • Parse-expression-or-type-name
            • Parse-postfix-expression
            • Lex-hex-iconst/fconst
            • Lex-dec-iconst/fconst
            • Lex-block-comment
            • Lex-escape-sequence
            • Read-token
            • Token
            • Lex-*-hexadecimal-digit
            • Lex-*-c-char
            • Lex-*-s-char
            • Parse-specifier/qualifier
            • Lex-*-digit
            • Lex-line-comment
            • Char-to-msg
            • Parse-primary-expression
            • Parse-declaration-specifier
            • Lex-iconst/fconst
            • Parse-external-declaration-list
            • Parse-declaration-specifiers
            • Lex-dec-expo-if-present
            • Init-parstate
            • Reread-to-token
            • Parse-asm-name-specifier
            • Lex-character-constant
            • Parse-expression-rest
            • Parstate$
            • Lex-dec-fconst
            • Token-unary-expression-start-p
            • Parse-declarator-or-abstract-declarator
            • Parse-asm-goto-labels
            • Parse-asm-clobbers
            • Lex-stringlit
            • Lex-non-octal-digit
            • Position
            • Lexeme
            • Lex-fsuffix-if-present
            • Parse-translation-unit
            • Lex-hexadecimal-digit
            • Token-type-specifier-keyword-p
            • Token-postfix-expression-rest-start-p
            • To-parstate$
            • Parse-?-asm-name-specifier
            • Parse-postfix-expression-rest
            • Parse-expression
            • Make-expr-unary-with-preinc/predec-ops
            • Lex-sign-if-present
            • Lex-dec-expo
            • Lex-bin-expo
            • Unread-to-token
            • Parse-*-stringlit
            • Parse-statement
            • Parse-fileset
            • Token-option
            • Lexeme-option
            • Token-struct-declaration-start-p
            • Parse-*-attribute-specifier
            • Parse-initializer-list
            • Parse-file
            • Parse-pointer
            • Parse-array/function-declarator
            • Unread-chars
            • Span
            • Read-stringlit
            • Lex-hex-quad
            • Unread-tokens
            • Token-type-qualifier-p
            • Read-identifier
            • Parse-*-asm-qualifier
            • Unread-char
            • Parse-attribute-name
            • Parse-argument-expressions
            • Make-expr-cast/add-or-cast/sub-ambig
            • Read-punctuator
            • Parse-struct-or-union-specifier
            • Parse-assignment-expression
            • Parse-asm-clobber
            • Token-specifier/qualifier-start-p
            • Token-primary-expression-start-p
            • Token-function-specifier-p
            • Reterr-msg
            • Read-keyword
            • Parse-*-increment/decrement
            • Parse-direct-abstract-declarator
            • Parse-declaration-or-statement
            • Char+position
            • Unread-token
            • Token+span
            • Token-expression-start-p
            • Update-parstate->tokens-unread
            • Update-parstate->chars-unread
            • Token-to-msg
            • Update-parstate->tokens-read
            • Update-parstate->tokens-length
            • Update-parstate->position
            • Update-parstate->chars-read
            • Parse-parameter-declaration
            • Parse-argument-expressions-rest
            • Update-parstate->chars-length
            • Token-to-type-specifier-keyword
            • Update-parstate->bytes
            • Parse-unary-expression
            • Parse-generic-associations-rest
            • Parse-conditional-expression
            • Update-parstate->size
            • Update-parstate->gcc
            • Parsize
            • Parse-direct-abstract-declarator-rest
            • Token-declaration-specifier-start-p
            • Parse-designator-list
            • Token-designation?-initializer-start-p
            • Token-abstract-declarator-start-p
            • Parse-?-asm-output-operands
            • Parse-?-asm-input-operands
            • Parse-struct-declaration
            • Parse-specifier-qualifier-list
            • Parse-parameter-declaration-list
            • Parse-constant-expression
            • Token-type-specifier-start-p
            • Token-type-qualifier-or-attribute-specifier-start-p
            • Parse-static-assert-declaration
            • Parse-fileset-loop
            • Parse-direct-declarator
            • Parse-declaration
            • Parse-attribute-parameters
            • Token-unary-operator-p
            • Token-to-unary-operator
            • Token-to-type-qualifier
            • Token-storage-class-specifier-p
            • Token-punctuatorp
            • Token-direct-abstract-declarator-start-p
            • Token-declarator-start-p
            • Parse-direct-declarator-rest
            • Token-to-storage-class-specifier
            • Token-to-assignment-operator
            • Token-to-asm-qualifier
            • Token-struct-declarator-start-p
            • Token-keywordp
            • Token-initializer-start-p
            • Token-direct-declarator-start-p
            • Token-assignment-operator-p
            • Parse-type-qualifier-and-attribute-specifier-list
            • Parse-enumerator-list
            • Parse-designation?-initializer
            • Parse-compound-literal
            • Parse-block-item
            • Token-type-name-start-p
            • Token-to-function-specifier
            • Token-preinc/predec-operator-p
            • Token-multiplicative-operator-p
            • Token-designator-start-p
            • Token-designation-start-p
            • Parstate->tokens-unread
            • Parstate->chars-unread
            • Parstate->bytes
            • Parse-initializer
            • Parse-generic-association
            • Parse-declaration-list
            • Parse-attribute-specifier
            • Parse-asm-output-operands
            • Token-to-relational-operator
            • Token-to-preinc/predec-operator
            • Token-to-multiplicative-operator
            • Token-relational-operator-p
            • Token-equality-operator-p
            • Token-asm-qualifier-p
            • Token-additive-operator-p
            • Span-join
            • Parstate->tokens-read
            • Parstate->tokens-length
            • Parstate->size
            • Parstate->chars-read
            • Parstate->chars-length
            • Parse-asm-statement
            • Parse-asm-input-operands
            • Update-parstate->token
            • Update-parstate->char
            • Token-to-equality-operator
            • Token-to-additive-operator
            • Token-shift-operator-p
            • To-parstate$-tokens-unread
            • To-parstate$-chars-unread
            • Position-inc-line
            • Position-inc-column
            • Parstate->gcc
            • Parse-type-name
            • Parse-struct-declarator-list
            • Parse-struct-declaration-list
            • Parse-relational-expression-rest
            • Parse-multiplicative-expression-rest
            • Parse-logical-or-expression-rest
            • Parse-logical-and-expression-rest
            • Parse-inclusive-or-expression-rest
            • Parse-exclusive-or-expression-rest
            • Parse-equality-expression-rest
            • Parse-array/function-abstract-declarator
            • Parse-additive-expression-rest
            • Token-to-shift-operator
            • To-parstate$-tokens-read
            • Parse-struct-declarator
            • Parse-shift-expression-rest
            • Parse-member-designor
            • Parse-init-declarator-list
            • Parse-init-declarator
            • Parse-and-expression-rest
            • Parse-alignment-specifier
            • To-parstate$-chars-read
            • Position-to-msg
            • Parstate->token
            • Parstate->char
            • Parse-shift-expression
            • Parse-relational-expression
            • Parse-multiplicative-expression
            • Parse-logical-or-expression
            • Parse-logical-and-expression
            • Parse-inclusive-or-expression
            • Parse-exclusive-or-expression
            • Parse-equality-expression
            • Parse-enum-specifier
            • Parse-block-item-list
            • Parse-attribute-list
            • Parse-and-expression
            • Parse-additive-expression
            • Parse-abstract-declarator
            • Char+position-list
            • Token+span-list
            • Span-to-msg
            • Parstate-fix
            • Parse-member-designor-rest
            • Position-init
            • Parstate->position
            • Parse-designator
            • Parse-declarator
            • Parse-attribute
            • Irr-token
            • Irr-span
            • Irr-position
            • Irr-lexeme
            • Token-list
            • Parse-type-qualifier-or-attribute-specifier
            • Parse-enumerator
            • Parse-asm-output-operand
            • Parse-asm-input-operand
          • Validator
          • Printer
          • Formalized-subset
          • Mapping-to-language-definition
          • Input-files
          • Defpred
          • Output-files
          • Abstract-syntax-operations
          • Validation-information
          • Implementation-environments
          • Concrete-syntax
          • Ascii-identifiers
          • Unambiguity
          • Preprocessing
          • Abstraction-mapping
        • Atc
        • Language
        • Representation
        • Transformation-tools
        • Insertion-sort
        • Pack
      • Bv
      • Imp-language
      • Event-macros
      • Java
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Cryptography
      • Number-theory
      • Lists-light
      • Axe
      • Builtins
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Parser

Lex-hex-iconst/fconst

Lex a hexadecimal integer or floating constant.

Signature

(lex-hex-iconst/fconst hprefix prefix-last-pos parstate) 
  → 
(mv erp const last-pos new-parstate)

Arguments

hprefix — Guard (hprefixp hprefix).

prefix-last-pos — Guard (positionp prefix-last-pos).

parstate — Guard (parstatep parstate).

Returns

const — Type (constp const).

last-pos — Type (positionp last-pos).

new-parstate — Type (parstatep new-parstate), given (parstatep parstate).

This is called when we expect a hexadecimal constant, after reading the hexadecimal prefix 0x or 0X.

First we read zero or more hexadecimal digits. If there are none, we check if the next character is a dot, because we may have a constant like 0x.1 for example. If there is no dot, it is an error. If there is a dot, we read zero or more hexadecimal digits. If there are none, it is an error. If there are some, we read the binary exponent, which must be present (otherwise it is an error); then we read the suffix if present, and we return an appropriate hexadecimal constant.

If instead there are hexadecimal digits after the prefix, we check whether the next character is a dot. If it is, we read zero or more hexadecimal digits, then a binary exponent (which must be present, otherwise it is an error), and finally a suffix if present; we return an appropriate hexadecimal floating constant. If instead there is no dot, we check whether there is the starting p or P of a binary exponent: if there is, it must be a floating constant, so we proceed to read the binary exponent, then a suffix if present; if there is not, it must be an integer constant.

Just before returning the constant, we use check-full-ppnumber, for the reasons explained there.

Definitions and Theorems

Function: lex-hex-iconst/fconst

(defun lex-hex-iconst/fconst (hprefix prefix-last-pos parstate)
 (declare (xargs :stobjs (parstate)))
 (declare (xargs :guard (and (hprefixp hprefix)
                             (positionp prefix-last-pos)
                             (parstatep parstate))))
 (let ((__function__ 'lex-hex-iconst/fconst))
  (declare (ignorable __function__))
  (b* (((reterr)
        (irr-const)
        (irr-position)
        parstate)
       ((erp hexdigs hexdigs-last-pos & parstate)
        (lex-*-hexadecimal-digit prefix-last-pos parstate)))
   (cond
    ((not hexdigs)
     (b* (((erp char pos parstate)
           (read-char parstate)))
      (cond
       ((not char)
        (reterr-msg :where (position-to-msg pos)
                    :expected "a hexadecimal digit or a dot"
                    :found (char-to-msg char)))
       ((= char (char-code #\.))
        (b* (((erp hexdigs2 & hexdigs2-next-pos parstate)
              (lex-*-hexadecimal-digit pos parstate)))
         (cond
          ((not hexdigs2)
           (reterr-msg :where (position-to-msg hexdigs2-next-pos)
                       :expected "a hexadecimal digit or a dot"
                       :found (char-to-msg nil)))
          (t
           (b* (((erp expo expo-last-pos parstate)
                 (lex-bin-expo parstate)))
            (b* (((erp fsuffix? suffix-last/next-pos parstate)
                  (lex-fsuffix-if-present parstate))
                 ((erp parstate)
                  (check-full-ppnumber nil parstate)))
             (retok
              (const-float
               (make-fconst-hex
                :prefix hprefix
                :core
                (make-hex-core-fconst-frac
                  :significand (make-hex-frac-const :before nil
                                                    :after hexdigs2)
                  :expo expo)
                :suffix? fsuffix?))
              (cond (fsuffix? suffix-last/next-pos)
                    (t expo-last-pos))
              parstate)))))))
       (t (reterr-msg :where (position-to-msg pos)
                      :expected "a hexadecimal digit or a dot"
                      :found (char-to-msg char))))))
    (t
     (b* (((erp char pos parstate)
           (read-char parstate)))
      (cond
       ((not char)
        (retok
         (const-int
             (make-iconst
                  :core (make-dec/oct/hex-const-hex :prefix hprefix
                                                    :digits hexdigs)
                  :suffix? nil
                  :info nil))
         hexdigs-last-pos parstate))
       ((= char (char-code #\.))
        (b* (((erp hexdigs2 & & parstate)
              (lex-*-hexadecimal-digit pos parstate)))
         (cond
          ((not hexdigs2)
           (b* (((erp expo expo-last-pos parstate)
                 (lex-bin-expo parstate))
                ((erp fsuffix? suffix-last/next-pos parstate)
                 (lex-fsuffix-if-present parstate))
                ((erp parstate)
                 (check-full-ppnumber nil parstate)))
            (retok
             (const-float
              (make-fconst-hex
               :prefix hprefix
               :core
               (make-hex-core-fconst-frac
                   :significand (make-hex-frac-const :before hexdigs
                                                     :after nil)
                   :expo expo)
               :suffix? fsuffix?))
             (cond (fsuffix? suffix-last/next-pos)
                   (t expo-last-pos))
             parstate)))
          (t
           (b* (((erp expo expo-last-pos parstate)
                 (lex-bin-expo parstate))
                ((erp fsuffix? suffix-last/next-pos parstate)
                 (lex-fsuffix-if-present parstate))
                ((erp parstate)
                 (check-full-ppnumber nil parstate)))
            (retok
             (const-float
              (make-fconst-hex
               :prefix hprefix
               :core
               (make-hex-core-fconst-frac
                  :significand (make-hex-frac-const :before hexdigs
                                                    :after hexdigs2)
                  :expo expo)
               :suffix? fsuffix?))
             (cond (fsuffix? suffix-last/next-pos)
                   (t expo-last-pos))
             parstate))))))
       ((or (= char (char-code #\p))
            (= char (char-code #\P)))
        (b* ((parstate (unread-char parstate))
             ((erp expo expo-last-pos parstate)
              (lex-bin-expo parstate))
             ((erp fsuffix? suffix-last/next-pos parstate)
              (lex-fsuffix-if-present parstate))
             ((erp parstate)
              (check-full-ppnumber nil parstate)))
         (retok
          (const-float
           (make-fconst-hex
                :prefix hprefix
                :core (make-hex-core-fconst-int :significand hexdigs
                                                :expo expo)
                :suffix? fsuffix?))
          (cond (fsuffix? suffix-last/next-pos)
                (t expo-last-pos))
          parstate)))
       (t
        (b* ((parstate (unread-char parstate))
             ((erp isuffix? suffix-last/next-pos parstate)
              (lex-isuffix-if-present parstate))
             ((erp parstate)
              (check-full-ppnumber
                   (and (member (car (last hexdigs)) '(#\e #\E))
                        t)
                   parstate)))
         (retok
          (const-int
             (make-iconst
                  :core (make-dec/oct/hex-const-hex :prefix hprefix
                                                    :digits hexdigs)
                  :suffix? isuffix?
                  :info nil))
          (cond (isuffix? suffix-last/next-pos)
                (t hexdigs-last-pos))
          parstate))))))))))

Theorem: constp-of-lex-hex-iconst/fconst.const

(defthm constp-of-lex-hex-iconst/fconst.const
  (b* (((mv acl2::?erp
            ?const ?last-pos ?new-parstate)
        (lex-hex-iconst/fconst hprefix prefix-last-pos parstate)))
    (constp const))
  :rule-classes :rewrite)

Theorem: positionp-of-lex-hex-iconst/fconst.last-pos

(defthm positionp-of-lex-hex-iconst/fconst.last-pos
  (b* (((mv acl2::?erp
            ?const ?last-pos ?new-parstate)
        (lex-hex-iconst/fconst hprefix prefix-last-pos parstate)))
    (positionp last-pos))
  :rule-classes :rewrite)

Theorem: parstatep-of-lex-hex-iconst/fconst.new-parstate

(defthm parstatep-of-lex-hex-iconst/fconst.new-parstate
 (implies
    (parstatep parstate)
    (b* (((mv acl2::?erp
              ?const ?last-pos ?new-parstate)
          (lex-hex-iconst/fconst hprefix prefix-last-pos parstate)))
      (parstatep new-parstate)))
 :rule-classes :rewrite)

Theorem: parsize-of-lex-hex-iconst/fconst-uncond

(defthm parsize-of-lex-hex-iconst/fconst-uncond
  (b* (((mv acl2::?erp
            ?const ?last-pos ?new-parstate)
        (lex-hex-iconst/fconst hprefix prefix-last-pos parstate)))
    (<= (parsize new-parstate)
        (parsize parstate)))
  :rule-classes :linear)

Theorem: parsize-of-lex-hex-iconst/fconst-cond

(defthm parsize-of-lex-hex-iconst/fconst-cond
  (b* (((mv acl2::?erp
            ?const ?last-pos ?new-parstate)
        (lex-hex-iconst/fconst hprefix prefix-last-pos parstate)))
    (implies (and (not erp) const?)
             (<= (parsize new-parstate)
                 (1- (parsize parstate)))))
  :rule-classes :linear)