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 recursion structure of the abstract syntax
(similarly to the c$::printer).
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.
Subtopics
- Simpadd0-exprs/decls/stmts
- Transform expressions, declarations, statements,
and related entities.
- Simpadd0-filepath
- Transform a file path.
- 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-fundef
- Transform a function definition.
- Simpadd0-extdecl
- Transform an external declaration.
- Simpadd0-transunit
- Transform a translation unit.
- 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.
