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
- Transform expressions, declarations, and related artifacts.
- Simpadd0-stmts/blocks
- Transform statements, blocks, and related entities.
- Simpadd0-filepath
- Transform a file path.
- Simpadd0-transunit-ensemble
- Transform a translation unit ensemble.
- Simpadd0-initdeclor-list
- Transform a list of initializer declarators.
- Simpadd0-initdeclor
- Transform an initializer declarator.
- Simpadd0-extdecl-list
- Transform a list of external declarations.
- Simpadd0-filepath-transunit-map
- Transform a map from file paths to translation units.
- Simpadd0-fundef
- Transform a function definition.
- Simpadd0-extdecl
- Transform an external declaration.
- Simpadd0-decl-list
- Transform a list of declarations.
- Simpadd0-transunit
- Transform a translation unit.
- Simpadd0-label
- Transform a label.
- Simpadd0-decl
- Transform a declaration.
- Simpadd0-structdeclor-list
- Transform a list of structure declarators.
- Simpadd0-structdecl-list
- Transform a list of structure declarations.
- 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-initer-option
- Transform an optional initializer.
- 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-declspec-list
- Transform a list of declaration specifiers.
- Simpadd0-declspec
- Transform a declaration specifier.
- Simpadd0-declor-option
- Transform an optional declarator.
- 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-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-const-expr
- Transform a constant expression.
- Simpadd0-block-item
- Transform a block item.
