		Search-engine friendly clone of the ACL2 documentation.

Atc-tutorial

Atc-tutorial-events

ATC tutorial: ACL2 events generated by ATC.

(This page may be skipped at first reading.)

As briefly mentioned in atc-tutorial-int-programs, ATC generates some events, besides the C file. This page describes these events in more detail.

These events are generated only if the :proofs option is t, which is the default, i.e. if proofs are generated. The events all pertain to the proofs. When :proofs is nil, ATC only generates the C file.

These events are generated in an encapsulate, from which they are exported. The encapsulate also includes some locally generated events that support the exported events. The option :print :all can be used to see all the events, including the local ones.

Program Constant

ATC generates a named constant whose value is the AST of the generated C program. More precisely, it is the AST of the generated C file, which is a value of the fixtype file in the abstract syntax of C. More precisely, it is the content of the generated file on disk: the AST is pretty-printed to the .c file. Currently ATC generates C programs that consist of single translation units in single C files.

The :const-name option directly controls the name of this constant.

The reason for generating this constant is so that it can be used in the generated theorems described next, making the theorems more readable.

Static Correctness Theorem

ATC generates a theorem asserting that the generated C program is statically correct, according to the formal static semantics of C.

More precisely, ATC generates a theorem of the form

(defthm <constant>-well-formed
  (equal (check-file <constant>) :wellformed))

This asserts that when check-fileset is applied to the named constant described above (i.e. the abstract syntax of the generated C program), the result is the value :wellformed. That is, the AST satisfies all the requirements of the static semantics of C: the code can be compiled by a C compiler, which is a prerequisite for executing it.

Since the program AST is a constant and check-fileset is executable, the theorem is proved easily by execution.

The name of the theorem is obtained by appending -well-formed after the name of the constant for the generated program. Currently ATC provides no option to control directly the name of this theorem; it can be controlled only indirectly, via the :const-name option for the constant name (see above).

Dynamic Correctness Theorems

ATC generates theorems asserting that the generated C program is dynamically correct, according to the C dynamic semantics.

More precisely, for each target function fn (see atc-tutorial-multiple-functions for details on how multiple ACL2 functions are translated to corresponding C functions), ATC generates a theorem of the form

(defthm <constant>-<fn>-correct
  (implies (and <guard-of-fn>
                (compustatep compst)
                (integerp limit)
                (>= limit <number>))
           (equal (exec-fun (ident "<fn>")
                            (list <x1> ... <xn>)
                            compst
                            (init-fun-env (preprocess <constant>))
                            limit)
                  (<fn> <x1> ... <xn>))))

This asserts that, under the guard of fn, running the C function corresponding to fn yields the same result as fn. Here, <x1>, ..., <xn> are the formal parameters of fn.

The variable compst represents the C computation state, described in the C dynamic semantics: the theorem applies to execution in every possible computation state.

The term (init-fun-env (preprocess <constant>)) constructs the C function environment of the generated translation unit.

The variable limit and the <number> that provides a lower bound are motivated by the fact that the big-step execution functions take a limit value, as explained in the C dynamic semantics. The number is calculated by ATC as sufficient to execute the function. The theorem asserts that, for any limit value at or above that limit, execution terminates and yields the same result as fn.

We remark that the form of the theorem above is accurate when none of the function's arguments are pointers. When they are, the theorem has a slightly more general form, which will be described in upcoming tutorial pages.

Note that, since fn does not return error values, the theorem implies that the execution of the C code never results in an error, including unsafe operations. This is because the dynamic semantics is defensive, i.e. it checks the validity of every operation before performing it, returning an error if the operation is invalid.

The guard satisfaction hypothesis is critical. Without it, the C code may return some error, e.g. if the result of an int addition does not fit in an int. Also see the discussion in atc-tutorial-int-representation about the guards of the ACL2 functions that represent C operations.

The dynamic semantics of C is formalized in terms of a deep embedding of C in ACL2: C ASTs are explicitly modeled in ACL2, and (static and dynamic) semantics is defined on the ASTs. In contrast, the ACL2 representation of C programs, e.g. as described in atc-tutorial-int-representation, is like a shallow embedding of C in ACL2. Thus, the correctness theorem above provides a bridge between shallow and deep embedding. The two embeddings are in close correspondence by design, but the proofs are still not trivial, because the two embeddings are actually quite different in nature and details.

The correctness theorem above is proved by expanding fn (for the shallow embedding) and symbolically executing its C counterpart (for the deep embedding). The two converge to the same (non-error) result.

These correctness proofs for functions are modular with respect to the function call graph: theorems about the correctness of callees are used to prove theorems about the correctness of callers. This is achieved via locally generated theorems that are more general than the exported ones (the latter are not compositional). Future versions of ATC may export these theorems from the encapsulate.

See atc-implementation for details on the generated theorems and their proofs.

Code Generation after the Events

The actual code is generated (i.e. written into the file) after the events above have been successfully processed by ACL2. Thus, if one of the theorems above fails for some reason, no code is generated. The rationale is that, unless the code can be proved correct, it should not be generated. Of course, this is easily defated by setting :proofs to nil. Nonetheless, when :proofs is t, it seems appropriate to generate the code after the proofs.

This deferral is achieved by having ATC not generate the code directly, but by having ATC generate an event that generates the code. Thus, ATC generates this and the events above, putting the latter before the former, and submits the events, in that order. The effect is as desired.

Previous: ACL2 representation and generation of multiple C functions

Next: ACL2 representation of C local variables