• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • 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
        • Soft
        • C
          • Syntax-for-tools
            • Disambiguator
              • Dimb-exprs/decls/stmts
              • Dimb-make/adjust-expr-binary
              • Dimb-transunit
              • Dimb-params-to-names
              • Dimb-cast/call-to-call
              • Dimb-make/adjust-expr-cast
              • Dimb-fundef
              • Dimb-make/adjust-expr-unary
              • Dimb-expr
                • Dimb-dirdeclor
                • Dimb-amb-declor/absdeclor
                • Dimb-cast/call-to-cast
                • Dimb-cast/addsub-to-cast
                • Dimb-cast/addsub-to-addsub
                • Dimb-transunit-ensemble
                • Dimb-add-ident
                • Dimb-kind
                • Dimb-declor
                • Dimb-amb-expr/tyname
                • Dimb-cast/mul-to-cast
                • Dimb-cast/and-to-cast
                • Dimb-cast/mul-to-mul
                • Dimb-cast/and-to-and
                • Dimb-kind-option
                • Dimb-type-spec
                • Dimb-extdecl-list
                • Dimb-extdecl
                • Dimb-lookup-ident
                • Dimb-param-declor
                • Dimb-decl-spec
                • Dimb-add-idents-objfun
                • Dimb-param-declon
                • Dimb-add-ident-objfun
                • Dimb-table
                • Dimb-amb-decl/stmt
                • Dimb-pop-scope
                • Dimb-push-scope
                • Dimb-initdeclor
                • Dimb-declor-option
                • Dimb-enumspec
                • Dimb-decl
                • Dimb-stmt
                • Dimb-scope
                • Dimb-structdeclor
                • Dimb-initdeclor-list
                • Dimb-decl-spec-list
                • Dimb-absdeclor
                • Dimb-init-table
                • Dimb-dirabsdeclor
                • Dimb-align-spec
                • Dimb-strunispec
                • Irr-dimb-table
                • Irr-dimb-kind
                • Dimb-spec/qual-list
                • Dimb-spec/qual
                • Dimb-param-declon-list
                • Dimb-label
                • Dimb-enumer-list
                • Dimb-enumer
                • Dimb-dirabsdeclor-option
                • Dimb-block-item
                • Dimb-structdeclor-list
                • Dimb-structdecl-list
                • Dimb-statassert
                • Dimb-desiniter-list
                • Dimb-desiniter
                • Dimb-decl-list
                • Dimb-const-expr-option
                • Dimb-absdeclor-option
                • Dimb-structdecl
                • Dimb-member-designor
                • Dimb-initer-option
                • Dimb-initer
                • Dimb-genassoc-list
                • Dimb-genassoc
                • Dimb-expr-option
                • Dimb-expr-list
                • Dimb-designor-list
                • Dimb-designor
                • Dimb-const-expr
                • Dimb-block-item-list
                • Dimb-tyname
              • Abstract-syntax
              • Parser
              • Validator
              • Printer
              • Formalized-subset
              • Mapping-to-language-definition
              • Input-files
              • Defpred
              • Output-files
              • Abstract-syntax-operations
              • Validation-information
              • Implementation-environments
              • Concrete-syntax
              • Unambiguity
              • Ascii-identifiers
              • 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
    • Disambiguator
    • Dimb-exprs/decls/stmts

    Dimb-expr

    Disambiguate an expression.

    Signature
    (dimb-expr expr table) → (mv erp new-expr new-table)
    Arguments
    expr — Guard (exprp expr).
    table — Guard (dimb-tablep table).
    Returns
    new-expr — Type (exprp new-expr).
    new-table — Type (dimb-tablep new-table).

    If an expression is an identifier, we look it up in the table to see whether it should be re-classified as an enumeration constant.

    A constant or string literal is left unchanged; there is nothing to disambiguate. If the constant is an enumeration constant, we could check that the identifier is in the table and has the kind of enumeration constant. However, the parser never generates enumeration constants, so there is no need to do that.

    We recursively disambiguate sub-expressions, and other sub-entities (e.g. generic associations, type names), following the recursive structure of the types.

    We call a separate function to disambiguate an ambiguous sizeof expression. Depending on whether the result is an expression or a type name, we re-classify the expression into an unambiguous one.

    An ambiguous cast or call is described in detail in expr: refer to that documentation to understand how it is disambiguated here; recall that it has the form (X) IncDec (E)Pr. We call a separate function to disambiguate the initial expression or type name, X. Based on the result, we re-classify the expression as a cast or call, using separate ACL2 functions.

    The other kinds of ambiguous cast or binary expressions are described in detail in expr: refer to that documentation to understand how it is disambiguated here; recall that is has the form (X) IncDec O E, where O is an ambiguous unary or binary operator. We call a separate function to disambiguate the initial expression or type name, X. Based on the result, we re-classify the expression as a cast or a binary one, using separate ACL2 functions.

    For cast and binary expressions, after disambiguating their sub-constructs, we use dimb-make/adjust-expr-cast and dimb-make/adjust-expr-binary for the reasons explained in the documentation of those functions. These two kinds of expressions are the only ones needing this treatment, because the only change in priorities that may be caused by disambiguation is for cast and binary expressions.