		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-transunit

Validate a translation unit.

Signature
(valid-transunit tunit ienv) → (mv erp new-tunit)
Arguments: tunit — Guard (transunitp tunit).; ienv — Guard (ienvp ienv).
Returns: erp — Type (maybe-msgp erp).; new-tunit — Type (transunitp new-tunit).

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 the 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 (tunit ienv)
 (declare (xargs :guard (and (transunitp tunit) (ienvp ienv))))
 (declare (xargs :guard (transunit-unambp tunit)))
 (let ((__function__ 'valid-transunit))
  (declare (ignorable __function__))
  (b*
   (((reterr) (irr-transunit))
    (gcc (ienv->gcc ienv))
    (table (valid-init-table))
    (table
     (if gcc (b* ((finfo (make-valid-ord-info-objfun
                              :type (type-function)
                              :linkage (linkage-external)
                              :defstatus (valid-defstatus-defined)))
                  (oinfo (make-valid-ord-info-objfun
                              :type (type-unknown)
                              :linkage (linkage-external)
                              :defstatus (valid-defstatus-defined)))
                  (table (valid-add-ords-file-scope
                              *gcc-builtin-functions* finfo table)
)
                  (table (valid-add-ords-file-scope
                              *gcc-builtin-vars* oinfo table)
))
               table)
       table)
)
    ((erp new-edecls table)
     (valid-extdecl-list (transunit->decls tunit)
                         table ienv))
    (info (make-transunit-info :table table)))
   (retok (make-transunit :decls new-edecls
                          :info info)))))

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

(defthm maybe-msgp-of-valid-transunit.erp
  (b* (((mv acl2::?erp ?new-tunit)
        (valid-transunit tunit 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)
        (valid-transunit tunit ienv)))
    (transunitp new-tunit))
  :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)
                 (valid-transunit tunit ienv)))
             (implies (not erp)
                      (transunit-unambp new-tunit)))))

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

(defthm valid-transunit-of-transunit-fix-tunit
  (equal (valid-transunit (transunit-fix tunit)
                          ienv)
         (valid-transunit tunit 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 tunit ienv)
                  (valid-transunit tunit-equiv ienv)))
  :rule-classes :congruence)

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

(defthm valid-transunit-of-ienv-fix-ienv
  (equal (valid-transunit tunit (ienv-fix ienv))
         (valid-transunit tunit 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 tunit ienv)
                  (valid-transunit tunit ienv-equiv)))
  :rule-classes :congruence)