Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Chain of read+writes could be improved by analyzing array/map indices #454

Open
msooseth opened this issue Feb 20, 2024 · 0 comments
Open
Labels
enhancement New feature or request

Comments

@msooseth
Copy link
Collaborator

As documented in:

-- 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.

                            (SLoad
                              slot:
                                (Keccak
                                  (WriteWord
                                    idx:
                                      0
                                    val:
                                      (Add
                                        1
                                        (Var "arg2")
                                      )
                                  )
                                  (ConcreteBuf
                                    Length: 64 (0x40) bytes
                                    0000:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                    0010:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                    0020:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                    0030:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 01   ................
                                  )
                                )
                              storage:
                                (SStore
                                  slot:
                                    (Keccak
                                      (WriteWord
                                        idx:
                                          0
                                        val:
                                          (Add
                                            (Var "arg2")
                                            (Var "arg1")
                                          )
                                      )
                                      (ConcreteBuf
                                        Length: 64 (0x40) bytes
                                        0000:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                        0010:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                        0020:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                        0030:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 01   ................
                                      )
                                    )
                                  val:
                                    55
                                )
                                (SStore
                                  slot:
                                    (Keccak
                                      (WriteWord
                                        idx:
                                          0
                                        val:
                                          (Add
                                            1
                                            (Var "arg2")
                                          )
                                      )
                                      (ConcreteBuf
                                        Length: 64 (0x40) bytes
                                        0000:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                        0010:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                        0020:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                        0030:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 01   ................
                                      )
                                    )
                                  val:
                                    (Add
                                      1
                                      (Var "arg1")
                                    )
                                )
                                (SStore
                                  slot:
                                    (Keccak
                                      (WriteWord
                                        idx:
                                          0
                                        val:
                                          (Add
                                            1
                                            (Var "arg2")
                                          )
                                      )
                                      (ConcreteBuf
                                        Length: 64 (0x40) bytes
                                        0000:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                        0010:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                        0020:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                        0030:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 01   ................
                                      )
                                    )
                                  val:
                                    (Add
                                      1
                                      (Var "arg1")
                                    )
                                )
                                (SStore
                                  slot:
                                    (Keccak
                                      (WriteWord
                                        idx:
                                          0
                                        val:
                                          (Var "arg2")
                                      )
                                      (ConcreteBuf
                                        Length: 64 (0x40) bytes
                                        0000:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                        0010:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                        0020:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                        0030:   00 00 00 00  00 00 00 00  00 00 00 00  00 00 00 00   ................
                                      )
                                    )
                                  val:
                                    (Var "arg1")
                                )
                                (AbstractStore (SymAddr "entrypoint") Nothing)
                            )
@msooseth msooseth added the enhancement New feature or request label Feb 20, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request
Projects
None yet
Development

No branches or pull requests

1 participant