-- This does not strip writes that cannot possibly match a read, in case there are
-- some write(s) in between that it cannot statically determine to be removable, because
-- it will early-abort. So (load idx1 (store idx1 (store idx1 (store idx0)))) will not strip
-- the idx0 store, in case things in between cannot be stripped. Potential for improvement. TODO.
-- See simplify-storage-map-todo test for an example where this happens
readStorage :: Expr EWord -> Expr Storage -> Maybe (Expr EWord)
readStorage w st = go (simplify w) st
A good example test where this is obvious:
, test "simplify-storage-map-todo" $ do
Just c <- solcRuntime "MyContract"
[i|
contract MyContract {
mapping (uint => uint) a;
mapping (uint => uint) b;
function fun(uint v, uint i) public {
require(i < 1000);
require(v < 1000);
a[i] = v;
b[i+1] = v+1;
b[i+v] = 55; // note: this can overwrite b[i+1], hence assert below can fail
assert(a[i] == v);
assert(b[i+1] == v+1);
}
}
Which will do things like below, where we read from 0x1, and write to a bunch of 0x1, but ALSO write to 0x0, which could be stripped.
As documented in:
A good example test where this is obvious:
Which will do things like below, where we read from 0x1, and write to a bunch of 0x1, but ALSO write to 0x0, which could be stripped.