Support for static storage arrays

[QGarchery]

Describe the bug
When trying to use a custom getter of an array of integers in storage, halmos fails with:
ValueError: invalid literal for int() with base 10: 'p_i_uint256'

To Reproduce
Run halmos on the following contract:

contract GetterTest {
    uint256[3] v;

    function getV(uint256 i) public view returns (uint256) {
        if (i >= 3) return 0;
        return v[i];
    }

    function testGetter(uint256 i) public view {
        assert(i >= 3 || getV(i) == v[i]);
    }
}

Environment:

• OS: linux
• Python version: 3.11.13
• Halmos and other dependency versions: halmos 0.0.8

[karmacoma-eth]

On the main branch, we get the following error instead

halmos --root tests --contract GetterTest --function testGetter --symbolic-storage

Running 1 tests for test/GetterTest.t.sol:GetterTest
[FAIL] testGetter(uint256) (paths: 1/3, time: 0.02s, bounds: [])
Not supported: SLOAD symbolic storage base slot: p_i_uint256
Symbolic test result: 0 passed; 1 failed; time: 0.03s

I think this is related to how static arrays are laid out (flattened to slots 0-2) vs dynamic arrays, and indeed the test passes if you define make v dynamic (uint256[] v;):

halmos --contract GetterTest --function testGetter --symbolic-storage                                                                                                                                                     

Running 1 tests for test/GetterTest.t.sol:GetterTest
[PASS] testGetter(uint256) (paths: 2/4, time: 0.04s, bounds: [])
Symbolic test result: 1 passed; 0 failed; time: 0.04s

I think this works as expected -- wdyt @daejunpark ?

[daejunpark]

@QGarchery Apologies for delayed response! I have been trying to find a good way to support this, but no luck so far (other than major design change for storage encoding scheme).

In the current design, each mapping or dynamic array is encoded as a logically separate object (smt-array). To do that, when given a storage slot (usually a hash expression), we need to determine which logical object it belongs to. For that, we use their base slot (i.e., 0, 1, 2, ... assigned to each storage variables in the order they appear in source code), as the slots belong to the same logical object share the same base slot. To identify the base slot, we decode the hash expression. For example, the slot for map[key] is hash(key, slot(map)) and the slot for arr[idx] is hash(slot(arr)) + idx, where we keep hash as uninterpreted, thus can extract the base slot slot(map) or slot(arr) by analyzing their expression structure. However, for static arrays, the slot for staticArr[idx] is just slot(staticArr) + idx, without involving any hash function, so it is more involved to extract the base slot for static arrays.

We might be able to come up with a scheme that works for simple cases, but I'm not sure how robust it would be. I think we may need to re-design the storage encoding scheme, to better handle this case as well as other known limitations.

[QGarchery]

Thanks for the detailed reponse @daejunpark ! I'll try to rephrase it to make sure I understood it well, please tell me if I'm missing something.

In Halmos, when you see a storage access, you try to map it to an object that was already encoded in SMT. You first look at the key to deduce the base slot, and from the base slot you can get the corresponding object. There are 2 patterns of keys that are recognized currently: hash(key, slot(map)) and hash(slot(arr)) + idx, corresponding to mappings and dynamic arrays respectively. Keeping hash uninterpreted:

• if the key is of the form hash(k, s) then you know that the corresponding object is a mapping at base slot s
• if the key is of the form hash(s) + i then you know that the corresponding object is a dynamic array at base slot s

The following potential solutions come to mind (I have no idea how applicable they are):

1. add the pattern slot(staticArr) + idx, and for any key of the form s + i where s is not of the form hash(x), map it to a static array with base slot s. This would only work if we know that solidity will always compile a key of a static arrays as an addition where the first term is the base slot and the second term is the offset, always in the same order. I'm assuming that it's not the case ?
2. precompute the initial storage layout, encode the corresponding objects along with the range of slots that they contain. Compute the size N of the initial storage as the end of the range of the last object and add the axiom that hash returns a integer greater than N. Given an integer i < N, the corresponding object would be the one with the range that contains i. Theoretically adding the axiom is not sound, but the tool could check that N is not too big and raise an error if it's not the case, and for most cases that should be enough (I'm not entirely sure about that, it would have to be verified more thoroughly).
3. identify the objects by their variables in the solidity sources instead of their base slots. Is it what you mean when you say it requires a re-design of the encoding scheme ?

[daejunpark]

@QGarchery yes, your understanding is correct, and thank you for the suggestions!

indeed, i've already considered (1) and (2), and i would probably try some combinations of them.

a challenge for (1) would be how to distinguish slot(staticArr) from normal constants. there are many expressions of the form s + i where s is constant and i is a symbol. also, the generated bytecode sometimes freely swaps the order for addition. so we need to consider the form i + s as well.

while such forms of expressions may not appear as arguments for the sload and sstore opcode in most cases, i've seen some smart contracts using their own custom storage layout (e.g., solady library) for gas optimization. in that case, the forms s + i or i + s may not refer to static array access, and (1) could interpret them incorrectly, leading to weird issues.

so, i think we also need to utilize the storage layout information, like you mentioned in (2), to avoid mis-interpretation. however, the storage layout information is not yet available within halmos, and we need to improve the frontend compilation pipeline to get that information. there are also other issues in the current frontend, so we will have to work on that anyway.

regarding (3), it might be doable by using the source mapping information. again, that needs the frontend work. also i'm not sure how precise the source mapping will be. if there are multiple storage variable accesses in the given source mapping range, it would be hard to make it robust.

again, thank you for reporting this issue and providing well-thought-out suggestions! please feel free to reach out if you have any other ideas!

[daejunpark]

This should be fixed by #192 which is part of the v0.1.5 release. Please add --custom-storage-layout option to enable the new feature that addresses this issue, and let us know if you have any further issues!

[daejunpark]

FYI, the option name is changed to: --storage-layout=generic, by #194 of the v0.1.6 release.