		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-transunit

Validate a translation unit.

Signature
(valid-transunit tunit gcc ienv) → (mv erp new-tunit table)
Arguments: tunit — Guard (transunitp tunit).; gcc — Guard (booleanp gcc).; ienv — Guard (ienvp ienv).
Returns: 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 return the final validation table. For now we do no make any use of the returned table, but in the future we should use it to validate the externally linked identifiers across different translation units of a translation unit ensemble. In fact, we should probably extend this validation function to trim the returned validation table so it only has entries for identifiers with external linkage.

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 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)
     (irr-valid-table))
    (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)))
   (retok (transunit new-edecls) table))))

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

(defthm transunitp-of-valid-transunit.new-tunit
  (b* (((mv acl2::?erp ?new-tunit acl2::?table)
        (valid-transunit tunit gcc 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 tunit gcc ienv)))
    (valid-tablep table))
  :rule-classes :rewrite)

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

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

Theorem: valid-transunit-of-bool-fix-gcc

(defthm valid-transunit-of-bool-fix-gcc
  (equal (valid-transunit tunit (bool-fix gcc)
                          ienv)
         (valid-transunit tunit gcc ienv)))

Theorem: valid-transunit-iff-congruence-on-gcc

(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: valid-transunit-of-ienv-fix-ienv

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