---
# System prepended metadata

title: Untitled

---

## Redundant Store Eliminator

General idea: reuse the mechanism from RedundantAssignEliminator.

write: area, statement
read: area

area is: memory / storage plus some encoding of the slot / memory area

Definition:
 - two writes / reads are _unrelated_ if their areas are non-overlapping.
 - write statement A _covers_ write statement B if the area of B is part of the area of A


while we traverse:
 - record all write statements and their state (unused, undecided, used)
 - split the state mapping into two unrelated copies on control-flow splits
 - start a new state mapping for each function
 - on read statement: turn all "undecided" write statements into "used" unless they can be proven to be unrelated
 - on write statament: turn all "undecided" write statements into "unused" if they can be proven to be covered by the new write statement

on forward control-flow joins:
 - merge state as follows:
   - consider all pairs of write statements that cannot be proven to be unrelated and keep them both with their max value.
     - unused x undecided -> undecided
     - unused x used -> used
     - undecided x used -> used

on for loops:
 - turn all write statements of memory/storage into "used" if the for loop body touches memory / storage

If control-flow terminates:
 - all undecided mstores are set to unused
 - all undecided sstores are set to used
 - when joining the terminated control-flow with the non-terminate control-flow,
   ignore all statements that only exist in the terminated control-flow

At the end of a function:
 - turn all undecided stores into used.

Delete all stores that are "unused" at the end of the traversal.


A: mstore(0, a)
B: keccak(100, calldatasize())

B does not cover A <=>
 - 0 + 32 <= 100 OR
 - 100 + calldatasize() <= 0


SMT: 

[100, 100 + calldatasize())
0 <= calldatasize() <= 2**32

[0, 32)

-------

Detail about merging control-flow joins:

We are joining the set of write statements X with the set of
write statements Y. They have a common ancestor, i.e.
they might contain identical write statements (pointers are the same),
but with different state. There can also be write statements that
are only in one set. Both can be from terminating or from continuing
control-flow. We also join with a terminating control-flow,
because it can influence whether or not a write operation in a
common ancestor branch can be removed or not.
If all control-flow branches are terminating, we do not have to continue.

We construct a new set of write statements Z.

First, consider all pairs of write statements that are identical in X
and Z (both pointer and state). Remove them from both X and Y
and put them into Z unchanged.

---------

## New version:

while we traverse:
 - record all write statements and their state (unused, undecided, used)
 - split the state mapping into two unrelated copies on control-flow splits
 - start a new state mapping for each function
 - on read+write statement: treat as read plus subsequent write.
 - on read statement: turn all "undecided" write statements from the current state mapping into "used" unless they can be proven to be unrelated
 - on write statament:
   - turn all "undecided" write statements from the current mapping into "unused" if they can be proven to be covered by the new write statement
   - add the write statement to the state mapping with state "undecided"
 - calling user-defined functions that read/write memory or storage have to be considered reading / writing to memory/storage as above

on forward control-flow joins:
 - merge state mappings as follows:
   - use write statements only existing in one branch without change.
   - combine write statements existing in both branches and use the max value:
     - unused x undecided -> undecided
     - unused x used -> used
     - undecided x used -> used

on for loops:
 - turn all write statements of memory/storage into "used" if the for loop body touches memory / storage

If control-flow terminates:
 - all undecided mstores are set to unused
 - all undecided sstores are set to
   - used if the termination is non-reverting
   - unused if the termination is reverting
 - the state mapping is still being used and joined with the
   non-terminating branch according to the same rules above

At the end of a function:
 - turn all undecided stores into used.

Delete all stores that are "unused" at the end of the traversal.

