Simpadd0
A transformation to simplify x + 0 to x.
This is a very simple proof-of-concept transformation,
which replaces expressions of the form x + 0 with x.
Due to C's arithmetic conversions, it is not immediately clear whether
this transformation always preserves code equivalence,
but for now we are not concerned about this,
as the goal of this proof-of-concept transformation
is just to show a plausible example of C-to-C transformation;
and there are certainly many cases (perhaps all cases) in which
this transformation is indeed equivalence-preserving.
This transformation is implemented as a collection of ACL2 functions
that operate on the abstract syntax,
following the recursive structure of the abstract syntax.
This is a typical pattern for C-to-C transformations,
which we may want to partially automate,
via things like generalized `folds' over the abstract syntax.
We also include a very preliminary proof generateion capability
for this transformation.
This is also just a proof of concept for now.
Subtopics
- Simpadd0-exprs/decls/stmts
- Transform expressions, declarations, statements,
and related entities.
- Simpadd0-gen-proofs-for-transunit-ensemble
- Generate equivalence theorems for all functions in
a translation unit ensemble.
- Simpadd0-filepath
- Transform a file path.
- Simpadd0-gen-proofs-for-transunit
- Generate equivalence theorems
for all the functions in a translation unit.
- Simpadd0-gen-proof-for-fun
- Generate equivalence theorem for a function.
- Simpadd0-transunit-ensemble
- Transform a translation unit ensemble.
- Simpadd0-filepath-transunit-map
- Transform a map from file paths to translation units.
- Simpadd0-extdecl-list
- Transform a list of external declarations.
- Simpadd0-fn
- Event expansion of the transformation.
- Simpadd0-transunit
- Transform a translation unit.
- Simpadd0-fundef
- Transform a function definition.
- Simpadd0-extdecl
- Transform an external declaration.
- Simpadd0-structdeclor-list
- Transform a list of structure declarators.
- Simpadd0-structdecl-list
- Transform a list of structure declarations.
- Simpadd0-initdeclor-list
- Transform a list of initializer declarators.
- Simpadd0-dirabsdeclor-option
- Transform an optional direct abstract declarator.
- Simpadd0-desiniter-list
- Transform a list of initializers with optional designations.
- Simpadd0-strunispec
- Transform a structure or union specifier.
- Simpadd0-structdeclor
- Transform a structure declarator.
- Simpadd0-structdecl
- Transform a structure declaration.
- Simpadd0-statassert
- Transform an static assertion declaration.
- Simpadd0-spec/qual-list
- Transform a list of type specifiers and qualifiers.
- Simpadd0-spec/qual
- Transform a type specifier or qualifier.
- Simpadd0-paramdeclor
- Transform a parameter declarator.
- Simpadd0-paramdecl-list
- Transform a list of parameter declarations.
- Simpadd0-paramdecl
- Transform a parameter declaration.
- Simpadd0-member-designor
- Transform a member designator.
- Simpadd0-initer-option
- Transform an optional initializer.
- Simpadd0-initdeclor
- Transform an initializer declarator.
- Simpadd0-genassoc-list
- Transform a list of generic associations.
- Simpadd0-genassoc
- Transform a generic association.
- Simpadd0-enumspec
- Transform an enumeration specifier.
- Simpadd0-enumer-list
- Transform a list of enumerators.
- Simpadd0-dirdeclor
- Transform a direct declarator.
- Simpadd0-dirabsdeclor
- Transform a direct abstract declarator.
- Simpadd0-desiniter
- Transform an initializer with optional designations.
- Simpadd0-designor-list
- Transform a list of designators.
- Simpadd0-declor-option
- Transform an optional declarator.
- Simpadd0-decl-spec-list
- Transform a list of declaration specifiers.
- Simpadd0-decl-spec
- Transform a declaration specifier.
- Simpadd0-const-expr-option
- Transform an optional constant expression.
- Simpadd0-block-item-list
- Transform a list of block items.
- Simpadd0-align-spec
- Transform an alignment specifier.
- Simpadd0-absdeclor-option
- Transform an optional abstract declarator.
- Simpadd0-absdeclor
- Transform an abstract declarator.
- Simpadd0-type-spec
- Transform a type specifier.
- Simpadd0-tyname
- Transform a type name.
- Simpadd0-stmt
- Transform a statement.
- Simpadd0-label
- Transform a label.
- Simpadd0-initer
- Transform an initializer.
- Simpadd0-expr-option
- Transform an optional expression.
- Simpadd0-expr-list
- Transform a list of expressions.
- Simpadd0-expr
- Transform an expression.
- Simpadd0-enumer
- Transform an enumerator.
- Simpadd0-designor
- Transform a designator.
- Simpadd0-declor
- Transform a declarator.
- Simpadd0-decl-list
- Transform a list of declarations.
- Simpadd0-decl
- Transform a declaration.
- Simpadd0-const-expr
- Transform a constant expression.
- Simpadd0-block-item
- Transform a block item.
- Simpadd0-macro-definition
- Definition of the simpadd0 macro.
