• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Set
      • C
        • Syntax-for-tools
          • Formalized-subset
          • Mapping-to-language-definition
          • Input-files
          • Compilation-database
          • Printer
          • Output-files
          • Abstract-syntax-operations
          • Implementation-environments
          • Abstract-syntax
          • Concrete-syntax
          • Disambiguation
          • Validation
          • Gcc-builtins
          • Preprocessing
          • Parsing
            • Parser
              • Parse-exprs/decls/stmts
              • Parser-states
              • Parse-external-declaration
              • Parse-cast-expression
              • Parse-expression-or-type-name
              • Parse-postfix-expression
              • Lexer
                • Check-full-ppnumber
                • Lex-lexeme
                • Lex-oct-iconst-/-dec-fconst
                • Lex-?-integer-suffix
                • Lex-hex-iconst/fconst
                • Lex-identifier/keyword
                • Lex-dec-iconst/fconst
                • Lex-block-comment
                • Lex-escape-sequence
                • Read-token
                • Lex-*-hexadecimal-digit
                • Lex-?-floating-suffix
                • Lex-*-c-char
                • Lex-*-s-char
                • Lex-prepr-directive
                • Lex-line-comment
                • Lex-*-digit
                • Lex-*-q-char
                • Lex-*-h-char
                • Lex-iconst/fconst
                • Lex-?-exponent-part
                • Lex-character-constant
                • Lexeme
                • Lex-string-literal
                • Lex-dec-fconst
                • Reread-to-token
                • Lex-non-octal-digit
                • Lex-hexadecimal-digit
                • Lex-header-name
                • Lex-binary-exponent-part
                • Lex-exponent-part
                • Lex-?-sign
                • Only-whitespace-backward-through-line
                • Lexeme-option
                • Lex-hex-quad
                • Unread-to-token
                • Read-stringlit
                • Unread-tokens
                • Read-identifier
                • Read-punctuator
                • Read-keyword
                • Unread-token
                • Irr-lexeme
              • Parse-primary-expression
              • Token-unary-expression-start-p
              • Parse-declaration-specifier
              • Parse-declaration-specifiers
              • Parse-unary-expression-or-parenthesized-type-name
              • Parse-asm-name-specifier
              • Parse-specifier/qualifier
              • Parse-expression-rest
              • Token-type-specifier-keyword-p
              • Parse-fileset
              • Parse-*-external-declaration
              • Parse-declarator-or-abstract-declarator
              • Parse-asm-goto-labels
              • Parse-asm-clobbers
              • Parse-translation-unit
              • Parse-*-label-declaration
              • Token-postfix-expression-rest-start-p
              • Parse-?-asm-name-specifier
              • Parse-*-comma-identifier
              • Parse-postfix-expression-rest
              • Parse-expression
              • Make-expr-unary-with-preinc/predec-ops
              • Parse-*-stringlit
              • Parse-statement
              • Token-struct-declaration-start-p
              • Parse-*-attribute-specifier
              • Parse-initializer-list
              • Parse-file
              • Parse-pointer
              • Parse-label-declaration
              • Parse-array/function-declarator
              • Token-type-qualifier-p
              • Parse-*-asm-qualifier
              • Parse-parameter-declaration
              • Parse-attribute-name
              • Parse-argument-expressions
              • Make-expr-cast/add-or-cast/sub-ambig
              • Parse-struct-or-union-specifier
              • Parse-declaration-or-statement
              • Parse-assignment-expression
              • Parse-asm-clobber
              • Token-specifier/qualifier-start-p
              • Token-primary-expression-start-p
              • Token-function-specifier-p
              • Token-expression-start-p
              • Parse-*-increment/decrement
              • Parse-direct-abstract-declarator
              • Parse-compound-statement
              • Token-to-type-specifier-keyword
              • Parse-unary-expression
              • Parse-argument-expressions-rest
              • Parse-generic-associations-rest
              • Parse-conditional-expression
              • Parse-fileset-loop
              • Parse-direct-abstract-declarator-rest
              • Token-designation?-initializer-start-p
              • Token-declaration-specifier-start-p
              • Parse-designator-list
              • 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-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-initializer-start-p
              • Token-direct-abstract-declarator-start-p
              • Token-declarator-start-p
              • Parse-initializer
              • Parse-direct-declarator-rest
              • Token-to-storage-class-specifier
              • Token-to-assignment-operator
              • Token-to-asm-qualifier
              • Token-struct-declarator-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
              • 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
              • Parse-asm-statement
              • Parse-asm-input-operands
              • Token-to-equality-operator
              • Token-to-additive-operator
              • Token-shift-operator-p
              • Parser-messages
              • 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
              • Parse-struct-declarator
              • Parse-shift-expression-rest
              • Parse-member-designor
              • Parse-init-declarator-list
              • Parse-init-declarator
              • Parse-designator
              • Parse-and-expression-rest
              • Parse-alignment-specifier
              • Reader
              • 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
              • Parse-member-designor-rest
              • Parse-declarator
              • Parse-attribute
              • Parse-type-qualifier-or-attribute-specifier
              • Parse-enumerator
              • Parse-asm-output-operand
              • Parse-asm-input-operand
        • Atc
        • Transformation-tools
        • Language
        • Representation
        • Insertion-sort
        • Pack
      • Soft
      • Bv
      • Imp-language
      • Ethereum
      • Event-macros
      • Java
      • Riscv
      • Bitcoin
      • Zcash
      • Yul
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Cryptography
      • Number-theory
      • Axe
      • Lists-light
      • Builtins
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Lexer

Lex-oct-iconst-/-dec-fconst

Signature

(lex-oct-iconst-/-dec-fconst zero-pos parstate) 
  → 
(mv erp const last-pos new-parstate)

Arguments

zero-pos — Guard (positionp zero-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 after the initial 0 has been read, and when it is not immediately followed by x or X. (The caller checks whether the next character is x or X, and if it is not it puts the character back into the parser state.) Thus, it meaans that we are reading either an octal integer constant or a decimal floating constant. Note that there are no octal floating constants, and that decimal integer constants do no start with 0. The position of the already read initial 0 is passed as the input zero-pos to this function.

We read all the digits that follow the initial 0, which could be none, or one, or more. If these are all octal digits in fact (i.e. no 8 or 9, this could be an octal constant. However, it could be also the start of a decimal constant whose initial digits, before the dot or exponent, happen to be all octal digits as well. So we look at the next character first. If there is no next character, and all the digits are octal, then we have an octal constant. If there is no next character, but not all the digits are octal, it is an error, because recall that, as explained in check-full-ppnumber, no all-octal prefix of this sequence could form an octal constant: the subsequent non-all-octal digits are part of the preprocessing number, which means that the octal constant would have extra characters. In order to find the first offending digit and report an informative error message, we unread all the digits and we call lex-non-octal-digit to find the offending digit.

If there is a dot or an e or an E just after the digits, this cannot be an octal constant, because it would mean that the preprocessing number has at least those extra characters. So it must be a decimal constant, if it is anything valid. So we proceed according to the grammar of decimal floating constants.

If there is any other character just after the digits, there are two cases. If all the digits read are octal, we may well have an octal constant, so long as the subsequent characters are not part of the preprocessing number, except for possibly an integer suffix. If not all the digits are octal, then it cannot be an octal constant, but it cannot be a decimal constant either, because in the latter case the digits would have to be followed by a dot or an exponent; so it is an error in that case.

Definitions and Theorems

Function: oct-iconst-leading-zeros

(defun oct-iconst-leading-zeros (octdigs)
  (declare (xargs :guard (oct-digit-char-listp octdigs)))
  (let ((__function__ 'oct-iconst-leading-zeros))
    (declare (ignorable __function__))
    (b* (((when (endp octdigs)) 0)
         (octdig (car octdigs)))
      (if (eql octdig #\0)
          (1+ (oct-iconst-leading-zeros (cdr octdigs)))
        0))))

Theorem: natp-of-oct-iconst-leading-zeros

(defthm natp-of-oct-iconst-leading-zeros
  (b* ((count (oct-iconst-leading-zeros octdigs)))
    (natp count))
  :rule-classes :rewrite)

Function: lex-oct-iconst-/-dec-fconst

(defun lex-oct-iconst-/-dec-fconst (zero-pos parstate)
 (declare (xargs :stobjs (parstate)))
 (declare (xargs :guard (and (positionp zero-pos)
                             (parstatep parstate))))
 (let ((__function__ 'lex-oct-iconst-/-dec-fconst))
  (declare (ignorable __function__))
  (b* (((reterr)
        (irr-const)
        (irr-position)
        parstate)
       ((erp digits digits-last-pos & parstate)
        (lex-*-digit zero-pos parstate))
       ((erp char pos parstate)
        (read-char parstate)))
   (cond
    ((not char)
     (cond
      ((oct-digit-char-listp digits)
       (retok
        (const-int
         (make-iconst
          :core
          (make-dec/oct/hex-const-oct
               :leading-zeros (1+ (oct-iconst-leading-zeros digits))
               :value (str::oct-digit-chars-value digits))
          :suffix? nil
          :info nil))
        (cond (digits digits-last-pos)
              (t (position-fix zero-pos)))
        parstate))
      (t (b* ((parstate (unread-chars (len digits) parstate))
              ((erp nonoctdig pos parstate)
               (lex-non-octal-digit parstate)))
           (reterr-msg :where (position-to-msg pos)
                       :expected "octal digit"
                       :found (char-to-msg nonoctdig))))))
    ((utf8-= char (char-code #\.))
     (b*
      (((erp digits2 digits2-last-pos & parstate)
        (lex-*-digit pos parstate))
       ((erp expo? expo-last/next-pos parstate)
        (lex-?-exponent-part parstate))
       ((erp fsuffix? suffix-last/next-pos parstate)
        (lex-?-floating-suffix parstate))
       ((erp parstate)
        (check-full-ppnumber nil parstate))
       (core
        (cond
         (digits2
          (cond
            (expo?
                 (make-dec-core-fconst-frac
                      :significand
                      (make-dec-frac-const :before (cons #\0 digits)
                                           :after digits2)
                      :expo? expo?))
            (t (make-dec-core-fconst-frac
                    :significand
                    (make-dec-frac-const :before (cons #\0 digits)
                                         :after digits2)
                    :expo? nil))))
         (t
          (cond
            (expo?
                 (make-dec-core-fconst-frac
                      :significand
                      (make-dec-frac-const :before (cons #\0 digits)
                                           :after nil)
                      :expo? expo?))
            (t (make-dec-core-fconst-frac
                    :significand
                    (make-dec-frac-const :before (cons #\0 digits)
                                         :after nil)
                    :expo? nil)))))))
      (retok (const-float (make-fconst-dec :core core
                                           :suffix? fsuffix?))
             (cond (fsuffix? suffix-last/next-pos)
                   (expo? expo-last/next-pos)
                   (digits2 digits2-last-pos)
                   (t pos))
             parstate)))
    ((or (utf8-= char (char-code #\e))
         (utf8-= char (char-code #\E)))
     (b* ((parstate (unread-char parstate))
          ((erp expo expo-last-pos parstate)
           (lex-exponent-part parstate))
          ((erp fsuffix? suffix-last/next-pos parstate)
           (lex-?-floating-suffix parstate))
          ((erp parstate)
           (check-full-ppnumber nil parstate)))
      (retok
       (const-float
        (make-fconst-dec
            :core
            (make-dec-core-fconst-int :significand (cons #\0 digits)
                                      :expo expo)
            :suffix? fsuffix?))
       (cond (fsuffix? suffix-last/next-pos)
             (t expo-last-pos))
       parstate)))
    (t
     (cond
      ((oct-digit-char-listp digits)
       (b* ((parstate (unread-char parstate))
            ((erp isuffix? suffix-last/next-pos parstate)
             (lex-?-integer-suffix parstate))
            ((erp parstate)
             (check-full-ppnumber nil parstate)))
        (retok
         (const-int
          (make-iconst
           :core
           (make-dec/oct/hex-const-oct
               :leading-zeros (1+ (oct-iconst-leading-zeros digits))
               :value (str::oct-digit-chars-value digits))
           :suffix? isuffix?
           :info nil))
         (cond (isuffix? suffix-last/next-pos)
               (digits digits-last-pos)
               (t (position-fix zero-pos)))
         parstate)))
      (t (b* ((parstate (unread-chars (len digits) parstate))
              ((erp nonoctdig pos parstate)
               (lex-non-octal-digit parstate)))
           (reterr-msg :where (position-to-msg pos)
                       :expected "octal digit"
                       :found (char-to-msg nonoctdig))))))))))

Theorem: constp-of-lex-oct-iconst-/-dec-fconst.const

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

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

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

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

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

Theorem: parsize-of-lex-oct-iconst-/-dec-fconst-uncond

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