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

Parse a file set.

Signature

(parse-fileset fileset version keep-going) → (mv erp tunits)

Arguments

fileset — Guard (filesetp fileset).

version — Guard (c::versionp version).

keep-going — Guard (booleanp keep-going).

Returns

tunits — Type (transunit-ensemblep tunits).

We pass an indication of the C version to use, and a flag saying whether to keep parsing other translation units after a parsing failure.

We go through each file of the file set and parse it, obtaining a translation unit for each, which we return in an ensemble of translation units that corresponds to the file set. The file paths are the same for the file set and for the translation unit ensembles (they are the keys of the maps).

Definitions and Theorems

Function: parse-fileset-loop

(defun parse-fileset-loop (filemap version keep-going)
 (declare (xargs :guard (and (filepath-filedata-mapp filemap)
                             (c::versionp version)
                             (booleanp keep-going))))
 (let ((__function__ 'parse-fileset-loop))
  (declare (ignorable __function__))
  (b*
   (((reterr) nil)
    ((when (omap::emptyp filemap))
     (retok nil))
    ((mv filepath filedata)
     (omap::head filemap))
    ((mv erp tunit)
     (parse-file filepath (filedata->unwrap filedata)
                 version))
    ((when erp)
     (if keep-going (prog2$ (cw "~@0~%" erp)
                            (parse-fileset-loop (omap::tail filemap)
                                                version keep-going))
       (reterr erp)))
    ((erp tunitmap)
     (parse-fileset-loop (omap::tail filemap)
                         version keep-going)))
   (retok (omap::update (filepath-fix filepath)
                        tunit tunitmap)))))

Theorem: filepath-transunit-mapp-of-parse-fileset-loop.tunitmap

(defthm filepath-transunit-mapp-of-parse-fileset-loop.tunitmap
  (b* (((mv acl2::?erp ?tunitmap)
        (parse-fileset-loop filemap version keep-going)))
    (filepath-transunit-mapp tunitmap))
  :rule-classes :rewrite)

Theorem: keys-of-parse-fileset-loop

(defthm keys-of-parse-fileset-loop
  (implies (filepath-filedata-mapp filemap)
           (b* (((mv acl2::?erp ?tunitmap)
                 (parse-fileset-loop filemap version keep-going)))
             (implies (and (not keep-going) (not erp))
                      (equal (omap::keys tunitmap)
                             (omap::keys filemap))))))

Function: parse-fileset

(defun parse-fileset (fileset version keep-going)
  (declare (xargs :guard (and (filesetp fileset)
                              (c::versionp version)
                              (booleanp keep-going))))
  (let ((__function__ 'parse-fileset))
    (declare (ignorable __function__))
    (b* (((reterr) (irr-transunit-ensemble))
         (filemap (fileset->unwrap fileset))
         ((erp tunitmap)
          (parse-fileset-loop filemap version keep-going))
         (- (if keep-going (b* ((len-filemap (omap::size filemap))
                                (len-tunitmap (omap::size tunitmap))
                                (diff (- len-filemap len-tunitmap)))
                             (if (= (the integer diff) 0)
                                 nil
                               (cw "Parsed ~x0/~x1 files.~%"
                                   len-tunitmap len-filemap)))
              nil)))
      (retok (transunit-ensemble tunitmap)))))

Theorem: transunit-ensemblep-of-parse-fileset.tunits

(defthm transunit-ensemblep-of-parse-fileset.tunits
  (b* (((mv acl2::?erp ?tunits)
        (parse-fileset fileset version keep-going)))
    (transunit-ensemblep tunits))
  :rule-classes :rewrite)

Theorem: filepaths-of-parse-fileset

(defthm filepaths-of-parse-fileset
  (b* (((mv acl2::?erp ?tunits)
        (parse-fileset fileset version keep-going)))
    (implies (and (not keep-going) (not erp))
             (equal (omap::keys (transunit-ensemble->units tunits))
                    (omap::keys (fileset->unwrap fileset))))))