• 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-block-comment

Lex a block comment.

Signature

(lex-block-comment first-pos parstate) 
  → 
(mv erp lexeme span new-parstate)

Arguments

first-pos — Guard (positionp first-pos).

parstate — Guard (parstatep parstate).

Returns

lexeme — Type (lexemep lexeme).

span — Type (spanp span).

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

This is called when we expect a block comment, after we have read the initial /*.

Following the mutually recursive rules of the grammar, we have two mutually recursive loop functions, which scan through the characters until the end of the comment is reached, or until the end of file is reached (in which case it is an error). In case of success, we retutn a comment lexeme, which currently contains no information (but that may change in the future). The span of the comment is calculated from the first position (of the / in /*), passed to this function, and the last position (of the / in the closing */), returned by the loop function.

Definitions and Theorems

Function: lex-rest-of-block-comment

(defun lex-rest-of-block-comment (first-pos parstate)
 (declare (xargs :stobjs (parstate)))
 (declare (xargs :guard (and (positionp first-pos)
                             (parstatep parstate))))
 (let ((__function__ 'lex-rest-of-block-comment))
  (declare (ignorable __function__))
  (b* (((reterr) (irr-position) parstate)
       ((erp char pos parstate)
        (read-char parstate)))
   (cond
    ((not char)
     (reterr-msg
      :where (position-to-msg pos)
      :expected "a character"
      :found (char-to-msg char)
      :extra
      (msg
       "The block comment starting at ~@1 ~
                                    never ends."
       (position-to-msg first-pos))))
    ((= char (char-code #\*))
     (lex-rest-of-block-comment-after-star first-pos parstate))
    (t (lex-rest-of-block-comment first-pos parstate))))))

Function: lex-rest-of-block-comment-after-star

(defun lex-rest-of-block-comment-after-star (first-pos parstate)
 (declare (xargs :stobjs (parstate)))
 (declare (xargs :guard (and (positionp first-pos)
                             (parstatep parstate))))
 (let ((__function__ 'lex-rest-of-block-comment-after-star))
  (declare (ignorable __function__))
  (b* (((reterr) (irr-position) parstate)
       ((erp char pos parstate)
        (read-char parstate)))
   (cond
    ((not char)
     (reterr-msg
      :where (position-to-msg pos)
      :expected "a character"
      :found (char-to-msg char)
      :extra
      (msg
       "The block comment starting at ~@1 ~
                                    never ends."
       (position-to-msg first-pos))))
    ((= char (char-code #\/))
     (retok pos parstate))
    ((= char (char-code #\*))
     (lex-rest-of-block-comment-after-star first-pos parstate))
    (t (lex-rest-of-block-comment first-pos parstate))))))

Theorem: return-type-of-lex-rest-of-block-comment.last-pos

(defthm return-type-of-lex-rest-of-block-comment.last-pos
  (b* (((mv acl2::?erp ?last-pos ?new-parstate)
        (lex-rest-of-block-comment first-pos parstate)))
    (positionp last-pos))
  :rule-classes :rewrite)

Theorem: return-type-of-lex-rest-of-block-comment.new-parstate

(defthm return-type-of-lex-rest-of-block-comment.new-parstate
  (implies (parstatep parstate)
           (b* (((mv acl2::?erp ?last-pos ?new-parstate)
                 (lex-rest-of-block-comment first-pos parstate)))
             (parstatep new-parstate)))
  :rule-classes :rewrite)

Theorem: return-type-of-lex-rest-of-block-comment-after-star.last-pos

(defthm return-type-of-lex-rest-of-block-comment-after-star.last-pos
  (b* (((mv acl2::?erp ?last-pos ?new-parstate)
        (lex-rest-of-block-comment-after-star first-pos parstate)))
    (positionp last-pos))
  :rule-classes :rewrite)

Theorem: return-type-of-lex-rest-of-block-comment-after-star.new-parstate

(defthm
   return-type-of-lex-rest-of-block-comment-after-star.new-parstate
 (implies
   (parstatep parstate)
   (b* (((mv acl2::?erp ?last-pos ?new-parstate)
         (lex-rest-of-block-comment-after-star first-pos parstate)))
     (parstatep new-parstate)))
 :rule-classes :rewrite)

Theorem: parsize-of-lex-rest-of-block-comment-uncond

(defthm parsize-of-lex-rest-of-block-comment-uncond
  (b* (((mv acl2::?erp ?last-pos ?new-parstate)
        (lex-rest-of-block-comment first-pos parstate)))
    (<= (parsize new-parstate)
        (parsize parstate)))
  :rule-classes :linear)

Theorem: parsize-of-lex-resto-of-block-comment-after-star-uncond

(defthm parsize-of-lex-resto-of-block-comment-after-star-uncond
  (b* (((mv acl2::?erp ?last-pos ?new-parstate)
        (lex-rest-of-block-comment-after-star first-pos parstate)))
    (<= (parsize new-parstate)
        (parsize parstate)))
  :rule-classes :linear)

Theorem: parsize-of-lex-rest-of-block-comment-cond

(defthm parsize-of-lex-rest-of-block-comment-cond
  (b* (((mv acl2::?erp ?last-pos ?new-parstate)
        (lex-rest-of-block-comment first-pos parstate)))
    (implies (not erp)
             (<= (parsize new-parstate)
                 (1- (parsize parstate)))))
  :rule-classes :linear)

Theorem: parsize-of-lex-resto-of-block-comment-after-star-cond

(defthm parsize-of-lex-resto-of-block-comment-after-star-cond
  (b* (((mv acl2::?erp ?last-pos ?new-parstate)
        (lex-rest-of-block-comment-after-star first-pos parstate)))
    (implies (not erp)
             (<= (parsize new-parstate)
                 (1- (parsize parstate)))))
  :rule-classes :linear)

Function: lex-block-comment

(defun lex-block-comment (first-pos parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard (and (positionp first-pos)
                              (parstatep parstate))))
  (let ((__function__ 'lex-block-comment))
    (declare (ignorable __function__))
    (b* (((reterr)
          (irr-lexeme)
          (irr-span)
          parstate)
         ((erp last-pos parstate)
          (lex-rest-of-block-comment first-pos parstate)))
      (retok (lexeme-comment)
             (make-span :start first-pos
                        :end last-pos)
             parstate))))

Theorem: lexemep-of-lex-block-comment.lexeme

(defthm lexemep-of-lex-block-comment.lexeme
  (b* (((mv acl2::?erp ?lexeme ?span ?new-parstate)
        (lex-block-comment first-pos parstate)))
    (lexemep lexeme))
  :rule-classes :rewrite)

Theorem: spanp-of-lex-block-comment.span

(defthm spanp-of-lex-block-comment.span
  (b* (((mv acl2::?erp ?lexeme ?span ?new-parstate)
        (lex-block-comment first-pos parstate)))
    (spanp span))
  :rule-classes :rewrite)

Theorem: parstatep-of-lex-block-comment.new-parstate

(defthm parstatep-of-lex-block-comment.new-parstate
  (implies (parstatep parstate)
           (b* (((mv acl2::?erp ?lexeme ?span ?new-parstate)
                 (lex-block-comment first-pos parstate)))
             (parstatep new-parstate)))
  :rule-classes :rewrite)

Theorem: parsize-of-lex-block-comment-uncond

(defthm parsize-of-lex-block-comment-uncond
  (b* (((mv acl2::?erp ?lexeme ?span ?new-parstate)
        (lex-block-comment first-pos parstate)))
    (<= (parsize new-parstate)
        (parsize parstate)))
  :rule-classes :linear)

Theorem: parsize-of-lex-block-comment-cond

(defthm parsize-of-lex-block-comment-cond
  (b* (((mv acl2::?erp ?lexeme ?span ?new-parstate)
        (lex-block-comment first-pos parstate)))
    (implies (not erp)
             (<= (parsize new-parstate)
                 (1- (parsize parstate)))))
  :rule-classes :linear)