Transformation-tools
C2C: transformation tools for C.
We provide tools to transform C code (C-to-C transformations)
according to various purposes and criteria.
The transformations are invoked as event macros,
which generally have the form
(<xform> :const-old ...
:const-new ...
...)where <xform> is the name of the transformation,
:const-old specifies (the name of a constant containing)
the ``old'' code to apply the transformation to,
const-new specifies (the name of a constant in which to put)
the ``new'' code resulting from the transformation,
and the remaining ... indicate additional keyword inputs
that certain transformations may accept.
See the user documentation of individual transformations for details.
Typically, the C code to be transformed is ingested
via the c$::input-files event macro,
which produces a named constant suitable for
the :const-old input of transformations.
Then the user invokes one or more transformations,
and eventually the final C code is written out
via the c$::output-files event macro,
which takes the named constant specified in
the :const-new input of the last invoked transformation.
The transformations operate on the abstract syntax
defined in c$::syntax-for-tools,
specifically on code ensembles.
The transformations are implemented as
collections of ACL2 functions that operate on the ASTs,
following their recursive structure.
For a growing subset of transformations and C constructs,
we also generate correctness theorems.
The theorems are specific to the code being transformed,
according to a verifying compiler approach.
The theorems are generated in a bottom-up fashion,
until constructs are encountered
for which proof generation is not supported,
at which point proof generation stops
with just the theorems generated so far.
In some cases, proof generation can proceed
all the way up to function definitions,
which currently provide the top-level theorems.
The generated theorems have names obtained by
combining the aforementioned const-new input
with an increasing numeric index,
which is threaded through the transformation functions.
The generated theorem events are accumulated into a list
that is threaded through the transformation functions;
the list is accumulated in reverse order,
so that each new generated event is consed,
but the list is reversed to the right order
in the top-level generated event that is submitted to ACL2.
A growing amount of functionality is factored into
general utilities usable in different transformations.
In particular, proof-generation includes utilities
to generate theorems for various classes of constructs,
and input-processing includes utilities
to process inputs of transformations.
Subtopics
- Simpadd0
- A transformation to simplify E + 0 to E.
- Proof-generation
- Proof generation utilities.
- Split-gso
- A C-to-C transformation to split a global struct object.
- Wrap-fn
- A C-to-C transformation to introduce a function wrapper.
- Constant-propagation
- A C-to-C transformation to propagate constants.
- Specialize
- A C-to-C transformation to specialize a function.
- Split-fn
- A C-to-C transformation to split a function in two.
- Split-fn-when
- A C-to-C transformation to split functions according to some trigger
pattern.
- Split-all-gso
- A transformation to split all global struct objects.
- Copy-fn
- A C-to-C transformation to copy a function.
- Variables-in-computation-states
- Notions and theorems about variables in the computation states.
- Rename
- A C-to-C transformation to rename identifiers.
- Utilities
- Utilities for C transformations.
- Proof-generation-theorems
- Theorems supporting proof generation.
- Input-processing
- Utilities to process inputs of C-to-C transformations.
