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

• Parser

Parse-asm-name-specifier

Parse an assembler name specifier.

Signature

(parse-asm-name-specifier uscores first-span parstate) 
  → 
(mv erp asmspec span new-parstate)

Arguments

uscores — Guard (keyword-uscores-p uscores).

first-span — Guard (spanp first-span).

parstate — Guard (parstatep parstate).

Returns

asmspec — Type (asm-name-specp asmspec).

span — Type (spanp span).

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

This is used only if GCC extensions are supported.

This is called after parsing the initial asm or __asm__. We pass to this function a flag distinguishing the two keywords (i.e. whether it has underscores or not), as well as the span of that keyword. We parse the rest of the assembler name specifier, and return its abstract syntax representation. We ensure that there is at least one string literal; see grammar rule for asm-name-specifier, which uses 1*.

Definitions and Theorems

Function: parse-asm-name-specifier

(defun parse-asm-name-specifier (uscores first-span parstate)
  (declare (xargs :stobjs (parstate)))
  (declare (xargs :guard (and (keyword-uscores-p uscores)
                              (spanp first-span)
                              (parstatep parstate))))
  (let ((__function__ 'parse-asm-name-specifier))
    (declare (ignorable __function__))
    (b* (((reterr)
          (irr-asm-name-spec)
          (irr-span)
          parstate)
         ((erp & parstate)
          (read-punctuator "(" parstate))
         ((erp token span parstate)
          (read-token parstate))
         ((unless (and token (token-case token :string)))
          (reterr-msg :where (position-to-msg (span->start span))
                      :expected "a string literal"
                      :found (token-to-msg token)))
         (parstate (unread-token parstate))
         ((erp strings & parstate)
          (parse-*-stringlit parstate))
         ((erp last-span parstate)
          (read-punctuator ")" parstate)))
      (retok (make-asm-name-spec :strings strings
                                 :uscores uscores)
             (span-join first-span last-span)
             parstate))))

Theorem: asm-name-specp-of-parse-asm-name-specifier.asmspec

(defthm asm-name-specp-of-parse-asm-name-specifier.asmspec
  (b* (((mv acl2::?erp ?asmspec ?span ?new-parstate)
        (parse-asm-name-specifier uscores first-span parstate)))
    (asm-name-specp asmspec))
  :rule-classes :rewrite)

Theorem: spanp-of-parse-asm-name-specifier.span

(defthm spanp-of-parse-asm-name-specifier.span
  (b* (((mv acl2::?erp ?asmspec ?span ?new-parstate)
        (parse-asm-name-specifier uscores first-span parstate)))
    (spanp span))
  :rule-classes :rewrite)

Theorem: parstatep-of-parse-asm-name-specifier.new-parstate

(defthm parstatep-of-parse-asm-name-specifier.new-parstate
 (implies
      (parstatep parstate)
      (b* (((mv acl2::?erp ?asmspec ?span ?new-parstate)
            (parse-asm-name-specifier uscores first-span parstate)))
        (parstatep new-parstate)))
 :rule-classes :rewrite)

Theorem: parsize-of-parse-asm-name-specifier-uncond

(defthm parsize-of-parse-asm-name-specifier-uncond
  (b* (((mv acl2::?erp ?asmspec ?span ?new-parstate)
        (parse-asm-name-specifier uscores first-span parstate)))
    (<= (parsize new-parstate)
        (parsize parstate)))
  :rule-classes :linear)

Theorem: parsize-of-parse-asm-name-specifier-cond

(defthm parsize-of-parse-asm-name-specifier-cond
  (b* (((mv acl2::?erp ?asmspec ?span ?new-parstate)
        (parse-asm-name-specifier uscores first-span parstate)))
    (implies (not erp)
             (<= (parsize new-parstate)
                 (1- (parsize parstate)))))
  :rule-classes :linear)