search

SRI-CSL / solidity

This is solc-verify, a modular verifier for Solidity.
https://github.com/SRI-CSL/solidity/blob/boogie/SOLC-VERIFY-README.md
GNU General Public License v3.0
50 stars 14 forks source link

Further dereferencing local storage pointer #133

Closed hajduakos closed 4 years ago

hajduakos commented 4 years ago

Currently, the base identifier of an expression to be used as a local storage pointer has to refer to a state variable. Therefore, the following does not work:

contract LocalStorageRepack {
    struct S { int x; T t; }
    struct T { int z; }

    S s1; S s2;

    function() external payable {
        s1.x = 1;
        s1.t.z = 11;
        s2.x = 2;
        s2.t.z = 22;

        S storage sptr = s1;
        T storage tptr = sptr.t;

        assert(tptr.z == 11);
    }
}
dddejan commented 4 years ago

See #134 for another corner case when you work this out.

hajduakos commented 4 years ago

Works for this simple case (as of 48fb6b3), when the type of the base pointer (S) only appears as a state variable without being inside an array or another struct. Will go for these cases now and only close the issue if those work out as well.

hajduakos commented 4 years ago

Implemented in 4d29c29f8c3121ed2d93ccafb6c12d875cc4b3bd, opening a PR