Simpadd0
A transformation to simplify E + 0 to E.
Introduction
This is a simple proof-of-concept transformation,
which replaces expressions of the form E + 0 with E,
when E is an expression that our current c$::validator
annotates as having type int,
and 0 is the octal constant for zero
without other leading zeros and without suffixes.
The transformation also generates proofs of equivalence
between old (original) and new (transformed) constructs,
for a growing 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 ... ; required, no default
:const-new ... ; required, no default
)Inputs
:const-old — required, no default
Specifies the code to the transformed.
This must be a symbol that names an existing ACL2 constant
that contains avalidated (and thus unambiguous) code ensemble, 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 — required, no default
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 code ensemble that is
the same as the one in *old*, except that,
in the translation unit ensemble,
every occurrence of an expression of the form E + 0,
when E is an expression that our current c$::validator
annotates as having type int,
and 0 is the octal constant for zero
without other leading zeros and without suffixes,
is turned into just the expression 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 integer parameters
(except plain char and except _Bool) and
whose body only contains the following constructs:
- Declarations of integer variables.
- Assignment expression statements.
- The null statement,
compound statements,
return (with or without expression) statements,
conditional (if and if-else statements,
and while loop statements.
- Expressions consisting of
integer constants,
integer variables,
the unary operators that do not involve pointers
(i.e. +, -, ~, !),
the binary operators that are pure
(i.e. *, /, %, +, -, <<, >>,
<, >, <=, >=, ==, !=,
&, ^, |, &&, ||),
the ternary conditional operator ? :,
casts to integer types,
and parentheses.
These are all pure and may be used anywhere.
- Simple (not compound) integer assignment expressions,
only as expression statements.
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-dirdeclor
- Transform a direct declarator.
- Simpadd0-implementation
- Implementation of simpadd0.
- Simpadd0-declor
- Transform a declarator.
- Simpadd0-initdeclor
- Transform an initializer declarator.
- Simpadd0-initdeclor-list
- Transform a list of initializer declarators.
- Simpadd0-decl
- Transform a declaration.
- Simpadd0-comp-stmt
- Transform a compound-statement.
- Simpadd0-param-declor
- Transform a parameter declarator.
- Simpadd0-param-declon-list
- Transform a list of parameter declarations.
- Simpadd0-param-declon
- Transform a parameter declaration.
- Simpadd0-expr-option
- Transform an optional expression.
- Simpadd0-struct-declor-list
- Transform a list of structure declarators.
- Simpadd0-struct-declon-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-struni-spec
- Transform a structure or union specifier.
- Simpadd0-struct-declor
- Transform a structure declarator.
- Simpadd0-struct-declon
- 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-genassoc-list
- Transform a list of generic associations.
- Simpadd0-dirabsdeclor
- Transform a direct abstract declarator.
- Simpadd0-desiniter
- Transform an initializer with optional designations.
- Simpadd0-designor-list
- Transform a list of designators.
- Simpadd0-decl-spec-list
- Transform a list of declaration specifiers.
- Simpadd0-const-expr-option
- Transform an optional constant expression.
- Simpadd0-align-spec
- Transform an alignment specifier.
- Simpadd0-absdeclor-option
- Transform an optional abstract declarator.
- Simpadd0-type-spec
- Transform a type specifier.
- Simpadd0-tyname
- Transform a type name.
- Simpadd0-member-designor
- Transform a member designator.
- Simpadd0-initer-option
- Transform an optional initializer.
- Simpadd0-initer
- Transform an initializer.
- Simpadd0-genassoc
- Transform a generic association.
- Simpadd0-expr-list
- Transform a list of expressions.
- Simpadd0-enumer-list
- Transform a list of enumerators.
- Simpadd0-enumer
- Transform an enumerator.
- Simpadd0-enum-spec
- Transform an enumeration specifier.
- Simpadd0-designor
- Transform a designator.
- Simpadd0-declor-option
- Transform an optional declarator.
- Simpadd0-decl-spec
- Transform a declaration specifier.
- Simpadd0-decl-list
- Transform a list of declarations.
- Simpadd0-const-expr
- Transform a constant expression.
- Simpadd0-block-item-list
- Transform a list of block items.
- Simpadd0-block-item
- Transform a block item.
- Simpadd0-absdeclor
- Transform an abstract declarator.
- Simpadd0-stmt
- Transform a statement.
- Simpadd0-label
- Transform a label.
- Simpadd0-expr
- Transform an expression.
