|
|
|---|
|
|
|
|---|
Flattening of Leo.
Leo code is flattened by transforming it according to certain criteria. The transformation involves:
The latter could be replaced by function inlining, but for now we want to preserve the functional decomposition of the program and therefore we do function specialization instead.
The flattening transformation starts with known values for
the constant inputs of the
The known values of the constants are propagated where those constants are mentioned in expressions. That is, the names of the constants are replaced with value expressions.
This constant propagation may cause certain (sub)expressions to consists of operators applied to operands that are value expressions. In this case, the constants can be folded, i.e. the operands are evaluated to values, the operator is applied to values, and the result is turned into a value expression. This is constant folding.
Note that constant folding also applies to constant expression that only involve literals and operators (i.e. no named constants), which perhaps the Leo code writer has written that way for clarity. Those are folded by this transformation, as expected and desired.
When we encounter a constant declaration, assuming that the code is type-checked, the initializing expression must be constant. Therefore, constant propagation and folding must cause it to be turned into a value (more precisely, a value expression). Thus, we extend our table of known constant values with a new association, so that this constant can be also propagated.
When a loop is encountered, assuming that the code is type-checked, the starting and ending bounds must be reducible to values, in the same way as the initializing expressions of constant declarations. Thus, we know all the values that the loop counter goes through, and we unroll the loop. This is done by replicating the body block as many times as the values taken by the loop counter, in order. For each replicated block, the table of known constant values is extended with the known value of the loop counter, so that constant propagation and folding can be performed in each replicated block.
When we encounter a call of a function, say
The above transformations, which start on
Functions with constant parameters are eventually eliminated.
Only their specialized versions survive the transformation.
Function without constant parameters survive if they are called,
directly or indirectly, from
Overall, this transformation produces a new program that includes
one or more functions (i.e.
We formalize these flattening transformations as executable ACL2 functions that perform the flattening. These ACL2 functions return error indications when certain unexpected conditions happen, e.g. that the initializing expression of a constant declaration cannot be evaluated to a value. These conditions should be ruled out by type checking: that is, type checking, which also does ``constancy checking'', is meant to ensure that the code can in fact be flattened. We plan to prove formally that this is the case: that is, that the executable transformation functions never returns certain error indications when executed over type-checked code; this proof, which is similar to the one planned for the dynamic semantics, would also provide a major validation of the design of Leo.
More precisely, the flattening ACL2 functions may return two kinds of errors. A static error happens when some condition is violated that should be ruled out by type checking: we plan to prove that static errors never occur when flattening type-checked code, as mentioned above. A dynamic error happens when constant folding results in an erroneous operation, such as integer overflow: these conditions are not ruled out by type checking, and may cause actual errors when flattening type-checked code.