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] =
Currently, this is not handled properly and can cause a loss of soudness on the analysis when using this option.
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.,
IfX == 5 is_sat()thenStorage[5] =Currently, this is not handled properly and can cause a loss of soudness on the analysis when using this option.