Partial Concrete Storage precision

[degrigis]

Whenever we use the partial concrete storage, an SSTORE to a symbolic slot ID (e.g., X) can potentially overwrite a value previously loaded from the blockchain at a concrete slot id (e.g., id=0x5). This happens when X=5 is satisfiable.

In these cases, we should either:

1- Invalidate the content of Storage[0x5] if X can be concretized to 5 (this is done immediately after we observe the symbolic storage write but might be expensive) 2- Encode extra constraints (ITE?) that handle the case at solving time.

e.g.,

• SLOAD from ID=5 --> w3.get_storage_at(0x5) = 0xdeadbeef --> Storage[5] = 0xdeadbeef
• SSTORE at ID=X --> If X == 5 is_sat() then Storage[5] = <Symbol>

Currently, this is not handled properly and can cause a loss of soudness on the analysis when using this option.