		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-transunit

Validate a translation unit.

Signature
(valid-transunit filepath tunit externals next-uid ienv) → (mv erp new-tunit table)
Arguments: filepath — Guard (filepathp filepath).; tunit — Guard (transunitp tunit).; externals — Guard (valid-externalsp externals).; next-uid — Guard (uidp next-uid).; ienv — Guard (ienvp ienv).
Returns: erp — Type (maybe-msgp erp).; new-tunit — Type (transunitp new-tunit).; table — Type (valid-tablep table).

If GCC extensions are not enabled, the initial validation table is the one returned by valid-init-table. If GCC extensions are enabled, we add a number of objects and functions that we have encountered in practical code; we should eventually have a comprehensive list here.

Starting with the validation table as just described, we validate all the external declarations in the translation unit. Since these are translation units after preprocesing, all the referenced names must be declared in the translation unit, so it is appropriate to start with the initial validation table.

If validation is successful, we add the final validation table to the information slot of the translation unit, i.e. we annotate the translation unit with its final validation table.

For each GCC function, the associated information consists of an unknown function type, external linkage, and defined status. The latter two seem reasonable, given that these identifiers are visible and have the same meaning in every translation unit, and have their own (built-in) definitions. For each GCC object, the associated information consists of the unknown type, external linkage, and defined status; the rationale for the latter two is the same as for functions.

Definitions and Theorems

Function: valid-transunit

(defun valid-transunit (filepath tunit externals next-uid ienv)
  (declare (xargs :guard (and (filepathp filepath)
                              (transunitp tunit)
                              (valid-externalsp externals)
                              (uidp next-uid)
                              (ienvp ienv))))
  (declare (xargs :guard (transunit-unambp tunit)))
  (b*
   (((reterr)
     (irr-transunit)
     (irr-valid-table))
    (gcc (ienv->gcc ienv))
    (table (valid-init-table filepath externals next-uid)
)
    (table
     (if gcc
      (b*
       ((table
         (valid-add-ord-objfuns-file-scope
              *gcc-builtin-functions*
              (make-type-function :ret (type-unknown)
                                  :params (type-params-unspecified))
              (linkage-external)
              (valid-defstatus-defined)
              table)
)
        (table (valid-add-ord-objfuns-file-scope
                    *gcc-builtin-vars* (type-unknown)
                    (linkage-external)
                    (valid-defstatus-defined)
                    table)
))
       table)
      table)
)
    ((erp new-edecls table)
     (valid-ext-declon-list (transunit->declons tunit)
                            table ienv))
    (info (make-transunit-info :table-end table)))
   (retok (make-transunit :comment (transunit->comment tunit)
                          :declons new-edecls
                          :info info)
          table)))

Theorem: maybe-msgp-of-valid-transunit.erp

(defthm maybe-msgp-of-valid-transunit.erp
  (b* (((mv acl2::?erp ?new-tunit acl2::?table)
        (valid-transunit filepath
                         tunit externals next-uid ienv)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: transunitp-of-valid-transunit.new-tunit

(defthm transunitp-of-valid-transunit.new-tunit
  (b* (((mv acl2::?erp ?new-tunit acl2::?table)
        (valid-transunit filepath
                         tunit externals next-uid ienv)))
    (transunitp new-tunit))
  :rule-classes :rewrite)

Theorem: valid-tablep-of-valid-transunit.table

(defthm valid-tablep-of-valid-transunit.table
  (b* (((mv acl2::?erp ?new-tunit acl2::?table)
        (valid-transunit filepath
                         tunit externals next-uid ienv)))
    (valid-tablep table))
  :rule-classes :rewrite)

Theorem: transunit-unambp-of-valid-transunit

(defthm transunit-unambp-of-valid-transunit
  (implies (transunit-unambp tunit)
           (b* (((mv acl2::?erp ?new-tunit acl2::?table)
                 (valid-transunit filepath
                                  tunit externals next-uid ienv)))
             (implies (not erp)
                      (transunit-unambp new-tunit)))))

Theorem: valid-transunit-of-filepath-fix-filepath

(defthm valid-transunit-of-filepath-fix-filepath
  (equal (valid-transunit (filepath-fix filepath)
                          tunit externals next-uid ienv)
         (valid-transunit filepath
                          tunit externals next-uid ienv)))

Theorem: valid-transunit-filepath-equiv-congruence-on-filepath

(defthm valid-transunit-filepath-equiv-congruence-on-filepath
 (implies
     (filepath-equiv filepath filepath-equiv)
     (equal (valid-transunit filepath tunit externals next-uid ienv)
            (valid-transunit filepath-equiv
                             tunit externals next-uid ienv)))
 :rule-classes :congruence)

Theorem: valid-transunit-of-transunit-fix-tunit

(defthm valid-transunit-of-transunit-fix-tunit
  (equal (valid-transunit filepath (transunit-fix tunit)
                          externals next-uid ienv)
         (valid-transunit filepath
                          tunit externals next-uid ienv)))

Theorem: valid-transunit-transunit-equiv-congruence-on-tunit

(defthm valid-transunit-transunit-equiv-congruence-on-tunit
 (implies
     (transunit-equiv tunit tunit-equiv)
     (equal (valid-transunit filepath tunit externals next-uid ienv)
            (valid-transunit filepath
                             tunit-equiv externals next-uid ienv)))
 :rule-classes :congruence)

Theorem: valid-transunit-of-valid-externals-fix-externals

(defthm valid-transunit-of-valid-externals-fix-externals
  (equal (valid-transunit filepath
                          tunit (valid-externals-fix externals)
                          next-uid ienv)
         (valid-transunit filepath
                          tunit externals next-uid ienv)))

Theorem: valid-transunit-valid-externals-equiv-congruence-on-externals

(defthm
      valid-transunit-valid-externals-equiv-congruence-on-externals
 (implies
     (valid-externals-equiv externals externals-equiv)
     (equal (valid-transunit filepath tunit externals next-uid ienv)
            (valid-transunit filepath
                             tunit externals-equiv next-uid ienv)))
 :rule-classes :congruence)

Theorem: valid-transunit-of-uid-fix-next-uid

(defthm valid-transunit-of-uid-fix-next-uid
  (equal (valid-transunit filepath
                          tunit externals (uid-fix next-uid)
                          ienv)
         (valid-transunit filepath
                          tunit externals next-uid ienv)))

Theorem: valid-transunit-uid-equiv-congruence-on-next-uid

(defthm valid-transunit-uid-equiv-congruence-on-next-uid
 (implies
     (uid-equiv next-uid next-uid-equiv)
     (equal (valid-transunit filepath tunit externals next-uid ienv)
            (valid-transunit filepath
                             tunit externals next-uid-equiv ienv)))
 :rule-classes :congruence)

Theorem: valid-transunit-of-ienv-fix-ienv

(defthm valid-transunit-of-ienv-fix-ienv
  (equal (valid-transunit filepath tunit
                          externals next-uid (ienv-fix ienv))
         (valid-transunit filepath
                          tunit externals next-uid ienv)))

Theorem: valid-transunit-ienv-equiv-congruence-on-ienv

(defthm valid-transunit-ienv-equiv-congruence-on-ienv
 (implies
     (ienv-equiv ienv ienv-equiv)
     (equal (valid-transunit filepath tunit externals next-uid ienv)
            (valid-transunit filepath
                             tunit externals next-uid ienv-equiv)))
 :rule-classes :congruence)