Simpadd0
A simple transformation to simplify E + 0 to E.
Introduction
This is a very simple proof-of-concept transformation,
which replaces expressions of the form E + 0 with E,
when E is a variable of type int.
The transformation also generates proofs of equivalence
between old (original) and new (transformed) constructs,
for a subset of the constructs.
In particular, the transformation generates equivalence proofs
for C functions of a certain form, detailed below.
General Form
(simpadd0 const-old
const-new
)Inputs
const-old
Specifies the code to the transformed.
This must be a symbol that names an existing ACL2 constant
that contains a validated translation unit ensemble,
i.e. a value of type transunit-ensemble
resulting from validation, and in particular containing validation information. This constant could result from c$::input-files,
or from some other transformation.
In the rest of this documentation page,
we refer to this constant as *old*.
const-new
Specifies the name of the constant for the transformed code.
This must be a symbol that is valid name for a new ACL2 constant.
In the rest of this documentation page,
we refer to this constant as *new*.
Generated Events
*new*
The named constant containing the result of the transformation.
This is a translation unit ensemble that is
the same as the one in *old*, except that
every occurrence of an expression of the form E + 0,
where E is a variable of type int
and 0 is the octal constant for zero
without other leading zeros and without suffixes,
is turned into just the variable E.
The file paths that are the keys of translation unit map
are unchanged by the transformation.
Equivalence theorems.
One theorem is generated for every function definition in *old*
that has all int parameters and
whose body consists of a single return statement
with an expression consisting of
int constants,
function parameters,
the unary operators that do not involve pointers
(i.e. +, -, ~, !),
and the binary operators that are pure and strict
(i.e. *, /, %, +, -, <<, >>,
<, >, <=, >=, ==, !=,
&, ^, |).
Note that the transformed function definition in *new*
satisfies the same restrictions.
These theorems are proved by proving a sequence of theorems,
in a bottom-up fashion, for the sub-constructs of the functions.
Theorems for sub-constructs in the supported subset of C
are also generated for functions that are not in the subset.
The generated theorems are designed to always prove.
It is a bug in the transformation
if a generated theorem fails to prove.
The generated theorems have names of the form *new*-thm-<i>,
where <i> are increasing positive integers.
Subtopics
- Simpadd0-implementation
- Implementation of simpadd0.
- Simpadd0-expr-option
- Transform an optional expression.
- Simpadd0-structdeclor-list
- Transform a list of structure declarators.
- Simpadd0-structdecl-list
- Transform a list of structure declarations.
- Simpadd0-spec/qual-list
- Transform a list of type specifiers and qualifiers.
- Simpadd0-paramdecl-list
- Transform a list of parameter declarations.
- Simpadd0-initdeclor-list
- Transform a list of initializer declarators.
- Simpadd0-dirabsdeclor-option
- Transform an optional direct abstract declarator.
- Simpadd0-dirabsdeclor
- Transform a direct abstract declarator.
- Simpadd0-desiniter-list
- Transform a list of initializers with optional designations.
- Simpadd0-absdeclor-option
- Transform an optional abstract declarator.
- 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
- Transform a type specifier or qualifier.
- Simpadd0-paramdeclor
- Transform a parameter declarator.
- 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-expr
- Transform an expression.
- Simpadd0-enumspec
- Transform an enumeration specifier.
- Simpadd0-enumer-list
- Transform a list of enumerators.
- Simpadd0-dirdeclor
- Transform a direct declarator.
- Simpadd0-desiniter
- Transform an initializer with optional designations.
- Simpadd0-designor-list
- Transform a list of designators.
- Simpadd0-designor
- Transform a designator.
- 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-decl-list
- Transform a list of declarations.
- Simpadd0-const-expr-option
- Transform an optional constant expression.
- Simpadd0-const-expr
- Transform a constant expression.
- Simpadd0-block-item-list
- Transform a list of block items.
- Simpadd0-align-spec
- Transform an alignment specifier.
- 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-list
- Transform a list of expressions.
- Simpadd0-enumer
- Transform an enumerator.
- Simpadd0-declor
- Transform a declarator.
- Simpadd0-decl
- Transform a declaration.
- Simpadd0-block-item
- Transform a block item.
