Validate a translation unit.
(valid-transunit tunit gcc ienv) → (mv erp 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.
Function:
(defun valid-transunit (tunit gcc ienv) (declare (xargs :guard (and (transunitp tunit) (booleanp gcc) (ienvp ienv)))) (declare (xargs :guard (transunit-unambp tunit))) (let ((__function__ 'valid-transunit)) (declare (ignorable __function__)) (b* (((reterr) (irr-transunit)) (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-ord-file-scope (ident "__atomic_signal_fence") finfo table) ) (table (valid-add-ord-file-scope (ident "__builtin_add_overflow") finfo table) ) (table (valid-add-ord-file-scope (ident "__builtin_bswap16") finfo table) ) (table (valid-add-ord-file-scope (ident "__builtin_bswap32") finfo table) ) (table (valid-add-ord-file-scope (ident "__builtin_bswap64") finfo table) ) (table (valid-add-ord-file-scope (ident "__builtin_choose_expr") finfo table) ) (table (valid-add-ord-file-scope (ident "__builtin_clz") finfo table) ) (table (valid-add-ord-file-scope (ident "__builtin_clzl") finfo table) ) (table (valid-add-ord-file-scope (ident "__builtin_clzll") finfo table) ) (table (valid-add-ord-file-scope (ident "__builtin_constant_p") finfo table) ) (table (valid-add-ord-file-scope (ident "__builtin_ctzl") finfo table) ) (table (valid-add-ord-file-scope (ident "__builtin_dynamic_object_size") finfo table) ) (table (valid-add-ord-file-scope (ident "__builtin_expect") finfo table) ) (table (valid-add-ord-file-scope (ident "__builtin_memchr") finfo table) ) (table (valid-add-ord-file-scope (ident "__builtin_memcmp") finfo table) ) (table (valid-add-ord-file-scope (ident "__builtin_memcpy") finfo table) ) (table (valid-add-ord-file-scope (ident "__builtin_memset") finfo table) ) (table (valid-add-ord-file-scope (ident "__builtin_mul_overflow") finfo table) ) (table (valid-add-ord-file-scope (ident "__builtin_object_size") finfo table) ) (table (valid-add-ord-file-scope (ident "__builtin_return_address") finfo table) ) (table (valid-add-ord-file-scope (ident "__builtin_strcpy") finfo table) ) (table (valid-add-ord-file-scope (ident "__builtin_strlen") finfo table) ) (table (valid-add-ord-file-scope (ident "__builtin_strncat") finfo table) ) (table (valid-add-ord-file-scope (ident "__builtin_strncpy") finfo table) ) (table (valid-add-ord-file-scope (ident "__builtin_sub_overflow") finfo table) ) (table (valid-add-ord-file-scope (ident "__builtin_unreachable") finfo table) ) (table (valid-add-ord-file-scope (ident "__builtin_va_end") finfo table) ) (table (valid-add-ord-file-scope (ident "__builtin_va_start") finfo table) ) (table (valid-add-ord-file-scope (ident "__eax") oinfo table) ) (table (valid-add-ord-file-scope (ident "__ebx") oinfo table) ) (table (valid-add-ord-file-scope (ident "__ecx") oinfo table) ) (table (valid-add-ord-file-scope (ident "__edx") oinfo table) ) (table (valid-add-ord-file-scope (ident "__esi") oinfo table) ) (table (valid-add-ord-file-scope (ident "__edi") oinfo table) ) (table (valid-add-ord-file-scope (ident "__ebp") oinfo table) ) (table (valid-add-ord-file-scope (ident "__esp") oinfo table) ) (table (valid-add-ord-file-scope (ident "__sync_add_and_fetch") finfo table) ) (table (valid-add-ord-file-scope (ident "__sync_and_and_fetch") finfo table) ) (table (valid-add-ord-file-scope (ident "__sync_bool_compare_and_swap") finfo table) ) (table (valid-add-ord-file-scope (ident "__sync_fetch_and_add") finfo table) ) (table (valid-add-ord-file-scope (ident "__sync_fetch_and_and") finfo table) ) (table (valid-add-ord-file-scope (ident "__sync_fetch_and_nand") finfo table) ) (table (valid-add-ord-file-scope (ident "__sync_fetch_and_or") finfo table) ) (table (valid-add-ord-file-scope (ident "__sync_fetch_and_sub") finfo table) ) (table (valid-add-ord-file-scope (ident "__sync_fetch_and_xor") finfo table) ) (table (valid-add-ord-file-scope (ident "__sync_lock_release") finfo table) ) (table (valid-add-ord-file-scope (ident "__sync_lock_test_and_set") finfo table) ) (table (valid-add-ord-file-scope (ident "__sync_nand_and_fetch") finfo table) ) (table (valid-add-ord-file-scope (ident "__sync_or_and_fetch") finfo table) ) (table (valid-add-ord-file-scope (ident "__sync_sub_and_fetch") finfo table) ) (table (valid-add-ord-file-scope (ident "__sync_synchronize") finfo table) ) (table (valid-add-ord-file-scope (ident "__sync_val_compare_and_swap") finfo table) ) (table (valid-add-ord-file-scope (ident "__sync_xor_and_fetch") finfo 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:
(defthm transunitp-of-valid-transunit.new-tunit (b* (((mv acl2::?erp ?new-tunit) (valid-transunit tunit gcc ienv))) (transunitp new-tunit)) :rule-classes :rewrite)
Theorem:
(defthm transunit-unambp-of-valid-transunit (implies (transunit-unambp tunit) (b* (((mv acl2::?erp ?new-tunit) (valid-transunit tunit gcc ienv))) (implies (not erp) (transunit-unambp new-tunit)))))
Theorem:
(defthm valid-transunit-of-transunit-fix-tunit (equal (valid-transunit (transunit-fix tunit) gcc ienv) (valid-transunit tunit gcc ienv)))
Theorem:
(defthm valid-transunit-transunit-equiv-congruence-on-tunit (implies (transunit-equiv tunit tunit-equiv) (equal (valid-transunit tunit gcc ienv) (valid-transunit tunit-equiv gcc ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-transunit-of-bool-fix-gcc (equal (valid-transunit tunit (bool-fix gcc) ienv) (valid-transunit tunit gcc ienv)))
Theorem:
(defthm valid-transunit-iff-congruence-on-gcc (implies (iff gcc gcc-equiv) (equal (valid-transunit tunit gcc ienv) (valid-transunit tunit gcc-equiv ienv))) :rule-classes :congruence)
Theorem:
(defthm valid-transunit-of-ienv-fix-ienv (equal (valid-transunit tunit gcc (ienv-fix ienv)) (valid-transunit tunit gcc ienv)))
Theorem:
(defthm valid-transunit-ienv-equiv-congruence-on-ienv (implies (ienv-equiv ienv ienv-equiv) (equal (valid-transunit tunit gcc ienv) (valid-transunit tunit gcc ienv-equiv))) :rule-classes :congruence)