• 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-isuffix-if-present

Lex an integer suffix, if present.

Signature

(lex-isuffix-if-present parstate) 
  → 
(mv erp isuffix? last/next-pos new-parstate)

Arguments

parstate — Guard (parstatep parstate).

Returns

isuffix? — Type (isuffix-optionp isuffix?).

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

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

If a suffix is found, the last/next-pos output is the position of its last character. Otherwise, it is the first position where the suffix would start.

We read the next character. If there is no next character, there is no integer suffix.

If the next character is l or L, there must be an integer suffix starting with a length indication. We try to read a second l or L if any, to decide on whether the length indication is for long or long long. After that, we read more to see if there is u or U, which provides a sign indication if present. Based on all the cases, we create the appropriate integer suffix. We unread any characters that are not part of the suffix, since they may form the next lexeme (whether that will pass parsing is a separate issue: here we follow the lexical rules for longest lexeme).

If the next character is u or U, there must be an integer suffix starting with a sign indication. We attempt to read an additional length indication, in a manner similar to the previous case, and we return the appropriate integer suffix at the end, unreading any characters that may be part of the next lexeme.

This code turned out to be verbose. We could shorten it by merging the treatment of lowercase l and uppercase L, single or double.

Definitions and Theorems

Function: lex-isuffix-if-present

(defun lex-isuffix-if-present (parstate)
 (declare (xargs :stobjs (parstate)))
 (declare (xargs :guard (parstatep parstate)))
 (let ((__function__ 'lex-isuffix-if-present))
  (declare (ignorable __function__))
  (b* (((reterr) nil (irr-position) parstate)
       ((erp char pos parstate)
        (read-char parstate)))
   (cond
    ((not char) (retok nil pos parstate))
    ((= char (char-code #\l))
     (b* (((erp char2 pos2 parstate)
           (read-char parstate)))
      (cond
       ((not char2)
        (retok (isuffix-l (lsuffix-locase-l))
               pos parstate))
       ((= char2 (char-code #\l))
        (b* (((erp char3 pos3 parstate)
              (read-char parstate)))
         (cond
              ((not char3)
               (retok (isuffix-l (lsuffix-locase-ll))
                      pos2 parstate))
              ((= char3 (char-code #\u))
               (retok (make-isuffix-lu :length (lsuffix-locase-ll)
                                       :unsigned (usuffix-locase-u))
                      pos3 parstate))
              ((= char3 (char-code #\U))
               (retok (make-isuffix-lu :length (lsuffix-locase-ll)
                                       :unsigned (usuffix-upcase-u))
                      pos3 parstate))
              (t (b* ((parstate (unread-char parstate)))
                   (retok (isuffix-l (lsuffix-locase-ll))
                          pos2 parstate))))))
       ((= char2 (char-code #\u))
        (retok (make-isuffix-lu :length (lsuffix-locase-l)
                                :unsigned (usuffix-locase-u))
               pos2 parstate))
       ((= char2 (char-code #\U))
        (retok (make-isuffix-lu :length (lsuffix-locase-l)
                                :unsigned (usuffix-upcase-u))
               pos2 parstate))
       (t (b* ((parstate (unread-char parstate)))
            (retok (isuffix-l (lsuffix-locase-l))
                   pos parstate))))))
    ((= char (char-code #\L))
     (b* (((erp char2 pos2 parstate)
           (read-char parstate)))
      (cond
       ((not char2)
        (retok (isuffix-l (lsuffix-upcase-l))
               pos parstate))
       ((= char2 (char-code #\L))
        (b* (((erp char3 pos3 parstate)
              (read-char parstate)))
         (cond
              ((not char3)
               (retok (isuffix-l (lsuffix-upcase-ll))
                      pos2 parstate))
              ((= char3 (char-code #\u))
               (retok (make-isuffix-lu :length (lsuffix-upcase-ll)
                                       :unsigned (usuffix-locase-u))
                      pos3 parstate))
              ((= char3 (char-code #\U))
               (retok (make-isuffix-lu :length (lsuffix-upcase-ll)
                                       :unsigned (usuffix-upcase-u))
                      pos3 parstate))
              (t (b* ((parstate (unread-char parstate)))
                   (retok (isuffix-l (lsuffix-upcase-ll))
                          pos2 parstate))))))
       ((= char2 (char-code #\u))
        (retok (make-isuffix-lu :length (lsuffix-upcase-l)
                                :unsigned (usuffix-locase-u))
               pos2 parstate))
       ((= char2 (char-code #\U))
        (retok (make-isuffix-lu :length (lsuffix-upcase-l)
                                :unsigned (usuffix-upcase-u))
               pos2 parstate))
       (t (b* ((parstate (unread-char parstate)))
            (retok (isuffix-l (lsuffix-upcase-l))
                   pos parstate))))))
    ((= char (char-code #\u))
     (b* (((erp char2 pos2 parstate)
           (read-char parstate)))
      (cond
       ((not char2)
        (retok (isuffix-u (usuffix-locase-u))
               pos parstate))
       ((= char2 (char-code #\l))
        (b* (((erp char3 pos3 parstate)
              (read-char parstate)))
         (cond
           ((not char3)
            (retok (make-isuffix-ul :unsigned (usuffix-locase-u)
                                    :length (lsuffix-locase-l))
                   pos2 parstate))
           ((= char3 (char-code #\l))
            (retok (make-isuffix-ul :unsigned (usuffix-locase-u)
                                    :length (lsuffix-locase-ll))
                   pos3 parstate))
           (t (b* ((parstate (unread-char parstate)))
                (retok (make-isuffix-ul :unsigned (usuffix-locase-u)
                                        :length (lsuffix-locase-l))
                       pos2 parstate))))))
       ((= char2 (char-code #\L))
        (b* (((erp char3 pos3 parstate)
              (read-char parstate)))
         (cond
           ((not char3)
            (retok (make-isuffix-ul :unsigned (usuffix-locase-u)
                                    :length (lsuffix-upcase-l))
                   pos2 parstate))
           ((= char3 (char-code #\L))
            (retok (make-isuffix-ul :unsigned (usuffix-locase-u)
                                    :length (lsuffix-upcase-ll))
                   pos3 parstate))
           (t (b* ((parstate (unread-char parstate)))
                (retok (make-isuffix-ul :unsigned (usuffix-locase-u)
                                        :length (lsuffix-upcase-l))
                       pos2 parstate))))))
       (t (b* ((parstate (unread-char parstate)))
            (retok (isuffix-u (usuffix-locase-u))
                   pos parstate))))))
    ((= char (char-code #\U))
     (b* (((erp char2 pos2 parstate)
           (read-char parstate)))
      (cond
       ((not char2)
        (retok (isuffix-u (usuffix-upcase-u))
               pos parstate))
       ((= char2 (char-code #\l))
        (b* (((erp char3 pos3 parstate)
              (read-char parstate)))
         (cond
           ((not char3)
            (retok (make-isuffix-ul :unsigned (usuffix-upcase-u)
                                    :length (lsuffix-locase-l))
                   pos2 parstate))
           ((= char3 (char-code #\l))
            (retok (make-isuffix-ul :unsigned (usuffix-upcase-u)
                                    :length (lsuffix-locase-ll))
                   pos3 parstate))
           (t (b* ((parstate (unread-char parstate)))
                (retok (make-isuffix-ul :unsigned (usuffix-upcase-u)
                                        :length (lsuffix-locase-l))
                       pos2 parstate))))))
       ((= char2 (char-code #\L))
        (b* (((erp char3 pos3 parstate)
              (read-char parstate)))
         (cond
           ((not char3)
            (retok (make-isuffix-ul :unsigned (usuffix-upcase-u)
                                    :length (lsuffix-upcase-l))
                   pos2 parstate))
           ((= char3 (char-code #\L))
            (retok (make-isuffix-ul :unsigned (usuffix-upcase-u)
                                    :length (lsuffix-upcase-ll))
                   pos3 parstate))
           (t (b* ((parstate (unread-char parstate)))
                (retok (make-isuffix-ul :unsigned (usuffix-upcase-u)
                                        :length (lsuffix-upcase-l))
                       pos2 parstate))))))
       (t (b* ((parstate (unread-char parstate)))
            (retok (isuffix-u (usuffix-upcase-u))
                   pos parstate))))))
    (t (b* ((parstate (unread-char parstate)))
         (retok nil pos parstate)))))))

Theorem: isuffix-optionp-of-lex-isuffix-if-present.isuffix?

(defthm isuffix-optionp-of-lex-isuffix-if-present.isuffix?
  (b* (((mv acl2::?erp
            ?isuffix? ?last/next-pos ?new-parstate)
        (lex-isuffix-if-present parstate)))
    (isuffix-optionp isuffix?))
  :rule-classes :rewrite)

Theorem: positionp-of-lex-isuffix-if-present.last/next-pos

(defthm positionp-of-lex-isuffix-if-present.last/next-pos
  (b* (((mv acl2::?erp
            ?isuffix? ?last/next-pos ?new-parstate)
        (lex-isuffix-if-present parstate)))
    (positionp last/next-pos))
  :rule-classes :rewrite)

Theorem: parstatep-of-lex-isuffix-if-present.new-parstate

(defthm parstatep-of-lex-isuffix-if-present.new-parstate
  (implies (parstatep parstate)
           (b* (((mv acl2::?erp
                     ?isuffix? ?last/next-pos ?new-parstate)
                 (lex-isuffix-if-present parstate)))
             (parstatep new-parstate)))
  :rule-classes :rewrite)

Theorem: parsize-of-lex-isuffix-if-present-uncond

(defthm parsize-of-lex-isuffix-if-present-uncond
  (b* (((mv acl2::?erp
            ?isuffix? ?last/next-pos ?new-parstate)
        (lex-isuffix-if-present parstate)))
    (<= (parsize new-parstate)
        (parsize parstate)))
  :rule-classes :linear)

Theorem: parsize-of-lex-isuffix-if-present-cond

(defthm parsize-of-lex-isuffix-if-present-cond
  (b* (((mv acl2::?erp
            ?isuffix? ?last/next-pos ?new-parstate)
        (lex-isuffix-if-present parstate)))
    (implies (and (not erp) isuffix?)
             (<= (parsize new-parstate)
                 (1- (parsize parstate)))))
  :rule-classes :linear)