Atc-let-designations
Designations of let and mv-let representations
for ATC.
ACL2's let is used to represent different things in C:
- A local variable declaration with an initializer.
- An assignment of an expression to a local variable.
- An assignment to an integer by pointer.
- An assignment to an element of an array.
- An assignment to an integer member of a structure.
- An assignment to an element of an array member of a structure.
- A transformation of a variable via statements.
The third, fourth, fifth, and sixth cases are recognized
by the presence of certain write functions,
according to the patterns described in the user documentation.
The other three cases could be recognized
by looking at the conditions that must hold in each cases,
but in order to ease ATC's task,
and also to encourage the user to explicate their intentions,
we use declar and assign
to indicate the declaration and assignment cases,
as explained in the user documentation.
Thus, the seventh case is what remains
when the others do not apply.
In all four cases above,
the term to which the variable is bound must be single-valued.
For multi-valued terms, we follow a similar approach for mv-let,
which is used to represent three different things in C:
- A local variable declaration with an initializer
that side-effects some variable(s)
in addition to returning the value to initialize the variable with.
- An assignment of an expression to a local variable
where the expression side-effects some variable(s)
in addition to returning the value to assign to the variable.
- A transformation of two or more variables via statements.
These cases mirror the first, second, and last cases
described above for let.
For these mv-let cases,
we use a similiar approach to the let cases,
i.e. we explicitly use indicators for declarations and assignments.
But the functions declar and assign
cannot be applied to multi-valued terms.
Thus, we introduce macros declar<n> and assign<n>,
for <n> equal to 1, 2, 3, etc.
(we stop at some point, but it is easy to add more if needed).
Note that <n> indicates the number of side-effected variables,
in addition to the declared or assigned variable;
it does not indicate the number of variables bound by mv-let,
which are always <n> + 1.
These must be macros, and cannot be functions,
because function may be only applied to single-valued terms,
while macros do not have that restriction;
and we need to have different macros for different values of <n>.
These representations are described in the user documentation.
Since ATC works on translated terms,
it does not directly see the macros declar<n> and assign<n>.
But it recognizes their presence as the term patterns they expand to.
See the ATC developer documentation for details.
We remark that an external (APT) transformation
could automatically add the needed wrappers
based on the conditions under which a let or mv-let occurs.
Thus, our approach does not forgo automation,
but rather modularizes the problem into simpler pieces.
Subtopics
- Declar
- Wrapper to indicate a C local variable declaration in a let.
- Assign
- Wrapper to indicate a C local variable assignment in a let.
- Declar9
- Wrapper to indicate a C local variable declaration
in an mv-let that side-effects 9 additional variables.
- Declar8
- Wrapper to indicate a C local variable declaration
in an mv-let that side-effects 8 additional variables.
- Declar7
- Wrapper to indicate a C local variable declaration
in an mv-let that side-effects 7 additional variables.
- Declar6
- Wrapper to indicate a C local variable declaration
in an mv-let that side-effects 6 additional variables.
- Declar5
- Wrapper to indicate a C local variable declaration
in an mv-let that side-effects 5 additional variables.
- Declar4
- Wrapper to indicate a C local variable declaration
in an mv-let that side-effects 4 additional variables.
- Declar3
- Wrapper to indicate a C local variable declaration
in an mv-let that side-effects 3 additional variables.
- Declar2
- Wrapper to indicate a C local variable declaration
in an mv-let that side-effects 2 additional variables.
- Assign9
- Wrapper to indicate a C local variable assignment
in an mv-let that side-effects 9 additional variables.
- Assign8
- Wrapper to indicate a C local variable assignment
in an mv-let that side-effects 8 additional variables.
- Assign7
- Wrapper to indicate a C local variable assignment
in an mv-let that side-effects 7 additional variables.
- Assign6
- Wrapper to indicate a C local variable assignment
in an mv-let that side-effects 6 additional variables.
- Assign5
- Wrapper to indicate a C local variable assignment
in an mv-let that side-effects 5 additional variables.
- Assign4
- Wrapper to indicate a C local variable assignment
in an mv-let that side-effects 4 additional variables.
- Assign3
- Wrapper to indicate a C local variable assignment
in an mv-let that side-effects 3 additional variables.
- Assign2
- Wrapper to indicate a C local variable assignment
in an mv-let that side-effects 2 additional variables.
- Declar1
- Wrapper to indicate a C local variable declaration
in an mv-let that side-effects 1 additional variable.
- Assign1
- Wrapper to indicate a C local variable assignment
in an mv-let that side-effects 1 additional variable.
