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,
into just the variable E.
- Each file path <file>.<ext> in *old*
is turned into <file>.simpadd0.<ext>,
if the path has a dot, and where <ext> had no dots;
if the path is <file> without dots,
it is turned into <file>.simpadd.
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.
