		Search-engine friendly clone of the ACL2 documentation.

Atc-implementation

Atc-event-and-code-generation

Event generation and code generation performed by atc.

We generate C abstract syntax, which we pretty-print to a file and also assign to a named constant.

Given the restrictions on the target functions, the translation is relatively straightforward, by design.

Some events are generated in two slightly different variants: one that is local to the generated encapsulate, and one that is exported from the encapsulate. Proof hints are in the former but not in the latter, thus keeping the ACL2 history ``clean''; some proof hints may refer to events that are generated only locally to the encapsulate.

Some code and event generation functions group some of their inputs and some of their outputs into fty::defprod values, to make the code more readable and more easily extensible, at a performance cost that should be unimportant. These product fixtypes have names ...-gin and ...-gout, where ... is related to the corresponding function name, and where the g in gin and gout conveys the reference to code and event generation functions. Most components follow the naming conventions described in atc-implementation. Other components common to all these types are:

proofs is a flag that is threaded through and that is used to determine and to indicate whether modular proofs are generated or not. We are incrementally developing a new approch to proof generation that generates compositional and more efficient theorems as each ACL2 construct is translated to the corresponding C construct. Not all constructs are currently covered: as soon as a non-covered construct is encountered, we stop generating modular theorems and we set the flag; prior to attempting to generate a modular theorem, the flag is checked, and modular theorem generation is skipped, even if the current construct is covered, but the reason is that previous constructs were not covered, and thus we cannot reliably generate a modular proof for a construct when we don't have modular proofs for the sub-constructs. Eventually we will eliminate this flag, once modular proof generation covers all the constructs.

events is a list of theorem events generated for a construct and its sub-constructs.

Other components are described where the types are defined.

Subtopics

Atc-symbolic-computation-states: Canonical representation of the computation states for the symbolic execution.
Atc-symbolic-execution-rules: Symbolic execution rules for ATC.
Atc-gen-ext-declon-lists: Generate two lists of C external declarations from the targets, including generating C loops from recursive ACL2 functions.
Atc-function-and-loop-generation: Generation of C functions and loops.
Atc-statement-generation: Generation of C statements.
Atc-gen-fileset: Generate a file set from the ATC targets, and accompanying events.
Atc-gen-everything: Generate the file and the events.
Atc-gen-obj-declon: Generate a C external object declaration.
Atc-gen-fileset-event: Event to pretty-print the generated C code to the file system.
Atc-tag-tables: Tables of defstructs, and operations on these tables.
Atc-expression-generation: Generation of C expressions.
Atc-generation-contexts: Logical contexts in which ATC generates C expressions and statements.
Atc-gen-wf-thm: Generate the theorem asserting the static well-formedness of the generated C code (referenced as the named constant).
Term-checkers-atc: Checkers of ACL2 terms that represent C constructs, used by ATC.
Atc-variable-tables: Tables of ACL2 variables, and operations on these tables.
Term-checkers-common: Checkers of ACL2 terms that represent C constructs, common to ATC and defobject.
Atc-gen-init-fun-env-thm: Generate the theorem asserting that applying init-fun-env to the translation unit gives the corresponding function environment.
Atc-gen-appconds: Generate the applicability conditions.
Read-write-variables: Functions to read and write variables.
Atc-gen-thm-assert-events: Generate assertion events to double-check that all the correctness theorems were generated.
Test*: Wrapper for contextual tests.
Atc-gen-prog-const: Generate the named constant for the abstract syntax tree of the generated C code (i.e. C file set).
Atc-gen-expr-bool: Generate a C expression from an ACL2 term that must be an expression term returning a boolean.
Atc-theorem-generation: Facilities for generating theorems in ATC.
Atc-tag-generation: Generation of C tag declarations (currently just structures).
Atc-gen-expr-pure: Generate a C expression from an ACL2 term that must be a pure expression term.
Atc-function-tables: Tables of ACL2 functions, and operations on these tables.
Atc-object-tables: Tables of defobjects, and operations on these tables.