		Search-engine friendly clone of the ACL2 documentation.

Disambiguator

Dimb-transunit

Disambiguate a translation unit.

Signature
(dimb-transunit tunit gcc) → (mv erp new-tunit)
Arguments: tunit — Guard (transunitp tunit).; gcc — Guard (booleanp gcc).
Returns: new-tunit — Type (transunitp new-tunit).

We initialize the disambiguation table, we disambiguate all the external declarations in order, and we discard the final disambiguation table.

If the GCC flag is nil (i.e. no GCC extensions), the initial disambiguation table is empty. If the flag is t, for now the only difference is that we initialize the disambiguation table with some GCC built-ins. For now we only add some built-ins that we have observed in some preprocessed files. We should revisit this, adding all the GCC built-ins, with clear and accurate references.

We also add entries for certain built-in variables corresponding to the x86 registers, i.e. __eax etc. We could not find those documented in the GCC manual, but we found them in practical code. Experiments suggest that these variables are somewhat restricted in usage. The normal pattern seems to be something like

unsigned long __eax = __eax;

after which one can use __eax as a regular variable. However, without the declaration above, __eax cannot be used as a regular variable. This is odd, because the validity of the declaration above presupposes that __eax is already in scope. It is not clear why such a declaration is needed in the first place. To add to the strangeness, one can change the above initializer to __eax + 1 (and presumably other similar expressions) and the compiler acceptes it.

However, none of this matters for the disambiguator, which does not need to validate the code, and is only required to return correct results only if the code is indeed valid (even though validity is checked after disambiguation). We add these special variables to the initial disambiguation table, so that declarations such as the one above do not cause an error during disambiguation. The declaration itself is handled by the disambiguator by overriding any preceding entry with the same name (see dimb-add-ident), so after a declaration like the one above __eax is still in the table, with the right kind, and can be used as an expression in scope. However, note that these variables only make sense on an x86 platform: we should refine our GCC flag with a richer description of the C implementation.

Definitions and Theorems

Function: dimb-transunit

(defun dimb-transunit (tunit gcc)
 (declare (xargs :guard (and (transunitp tunit)
                             (booleanp gcc))))
 (let ((__function__ 'dimb-transunit))
   (declare (ignorable __function__))
   (b*
    (((reterr) (irr-transunit))
     (edecls (transunit->decls tunit))
     (table (dimb-init-table))
     (table
          (if gcc (dimb-add-idents-objfun
                       (list (ident "__atomic_signal_fence")
                             (ident "__builtin_add_overflow")
                             (ident "__builtin_bswap16")
                             (ident "__builtin_bswap32")
                             (ident "__builtin_bswap64")
                             (ident "__builtin_choose_expr")
                             (ident "__builtin_clz")
                             (ident "__builtin_clzl")
                             (ident "__builtin_clzll")
                             (ident "__builtin_constant_p")
                             (ident "__builtin_ctzl")
                             (ident "__builtin_dynamic_object_size")
                             (ident "__builtin_expect")
                             (ident "__builtin_memchr")
                             (ident "__builtin_memcmp")
                             (ident "__builtin_memcpy")
                             (ident "__builtin_memset")
                             (ident "__builtin_mul_overflow")
                             (ident "__builtin_object_size")
                             (ident "__builtin_return_address")
                             (ident "__builtin_strcpy")
                             (ident "__builtin_strlen")
                             (ident "__builtin_strncat")
                             (ident "__builtin_strncpy")
                             (ident "__builtin_sub_overflow")
                             (ident "__builtin_unreachable")
                             (ident "__builtin_va_end")
                             (ident "__builtin_va_start")
                             (ident "__eax")
                             (ident "__ebx")
                             (ident "__ecx")
                             (ident "__edx")
                             (ident "__esi")
                             (ident "__edi")
                             (ident "__ebp")
                             (ident "__esp")
                             (ident "__sync_add_and_fetch")
                             (ident "__sync_and_and_fetch")
                             (ident "__sync_bool_compare_and_swap")
                             (ident "__sync_fetch_and_add")
                             (ident "__sync_fetch_and_and")
                             (ident "__sync_fetch_and_nand")
                             (ident "__sync_fetch_and_or")
                             (ident "__sync_fetch_and_sub")
                             (ident "__sync_fetch_and_xor")
                             (ident "__sync_lock_release")
                             (ident "__sync_lock_test_and_set")
                             (ident "__sync_nand_and_fetch")
                             (ident "__sync_or_and_fetch")
                             (ident "__sync_sub_and_fetch")
                             (ident "__sync_synchronize")
                             (ident "__sync_val_compare_and_swap")
                             (ident "__sync_xor_and_fetch"))
                       table)
            table)
)
     ((erp new-edecls &)
      (dimb-extdecl-list edecls table)))
    (retok (make-transunit :decls new-edecls
                           :info nil)))))

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

(defthm transunitp-of-dimb-transunit.new-tunit
  (b* (((mv acl2::?erp ?new-tunit)
        (dimb-transunit tunit gcc)))
    (transunitp new-tunit))
  :rule-classes :rewrite)

Theorem: transunit-unambp-of-dimb-transunit

(defthm transunit-unambp-of-dimb-transunit
  (b* (((mv acl2::?erp ?new-tunit)
        (dimb-transunit tunit gcc)))
    (implies (not erp)
             (transunit-unambp new-tunit))))

Theorem: dimb-transunit-of-transunit-fix-tunit

(defthm dimb-transunit-of-transunit-fix-tunit
  (equal (dimb-transunit (transunit-fix tunit)
                         gcc)
         (dimb-transunit tunit gcc)))

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

(defthm dimb-transunit-transunit-equiv-congruence-on-tunit
  (implies (transunit-equiv tunit tunit-equiv)
           (equal (dimb-transunit tunit gcc)
                  (dimb-transunit tunit-equiv gcc)))
  :rule-classes :congruence)

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

(defthm dimb-transunit-of-bool-fix-gcc
  (equal (dimb-transunit tunit (bool-fix gcc))
         (dimb-transunit tunit gcc)))

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

(defthm dimb-transunit-iff-congruence-on-gcc
  (implies (iff gcc gcc-equiv)
           (equal (dimb-transunit tunit gcc)
                  (dimb-transunit tunit gcc-equiv)))
  :rule-classes :congruence)