Dead-code-eliminator
The DeadCodeEliminator transformation.
This is described in
[Solidity: Internals: The Optimizer: Yul-Based Optimizer Module:
Statement-Scale Simplifications: DeadCodeEliminator].
The description mentions
not only break, continue, and leave,
but also other constructs that are presumably part of the EVM dialect;
since they are not part of our formalization,
we do not handle the latter for now.
We define this transformation assuming that
FunctionHoister and FunctionGrouper have already run:
this means that all the functions are all
immediately contained in the top-level block,
where `immediately' means that
there are no intervening blocks in between,
i.e. the function definitions are not contained in nested blocks.
This condition is formalized in no-function-definitions
(actually, for now only part of those conditions is formalized there,
but we plan to extend that formalization).
We do not represent this condition in the guards,
for greater flexibility and simplicity,
but the correctness theorems for this tranformation
use that condition as hypothesis.
Here is some elaboration on not representing that condition in the guards.
If we used block-nofunp as guard of block-dead,
then we could not use block-dead for the top-level block,
which does not satisfy block-nofunp.
Also, as we need to extend the ...-dead transformations
from syntactic to semantics entities in the proof of dynamic correctness, we would have to extend the -...-nofunp functions
to those semantics entities as well in order to verify the guards.
For these reasons, i.e. flexibility and simplicity respectively,
we do not use ...-nofunp as guards in ...-dead.
Subtopics
- Dead-code-eliminator-execution
- Proof that the DeadCodeEliminator transformation preserves
the execution behavior.
- Statements/blocks/cases/fundefs-dead
- Mutually recursive functions to eliminate dead code in
statements, blocks, cases, and function definitions.
- Fundef-list-dead
- Eliminate dead code in lists of function definitions.
