Mapping key types are memory

[dddejan]

By solidity docs, the only non-primitive types that can be used as keys in a mapping are bytes and strings. In our current model of storage these keys should be represented as SMT arrays which should all work out. But, the solidity compiler marks the non-primitive types of mappings as memory, which leads to errors.

pragma solidity ^0.5.0;

contract MappingKeyIsMemory {

    mapping(bytes=>int) m;

    bytes b1;
    bytes b2;

    function() external payable {
        m[b1] = 2;
        m[b2] = 2;
        assert(m[b1] == m[b2]);
    }
}

Running verifier on this gives

solc-verify.py MappingKeyIsMemory.sol --output .
Error while running verifier, details:
Parsing ./MappingKeyIsMemory.sol.bpl
./MappingKeyIsMemory.sol.bpl(31,38): Error: invalid type for argument 0 in map store: int_arr_type (expected: int_arr_ptr)
./MappingKeyIsMemory.sol.bpl(32,38): Error: invalid type for argument 0 in map store: int_arr_type (expected: int_arr_ptr)
./MappingKeyIsMemory.sol.bpl(33,109): Error: invalid type for argument 0 in map select: int_arr_type (expected: int_arr_ptr)
./MappingKeyIsMemory.sol.bpl(33,138): Error: invalid type for argument 0 in map select: int_arr_type (expected: int_arr_ptr)
4 type checking errors detected in ./MappingKeyIsMemory.sol.bpl

For the compiler it doesn't actually make any difference, because they don't store the keys, they just hash it.

@hajduakos let's discuss this. This is particularly important for the treatment of strings, which give the same error if treated as bytes.

[dddejan]

Relevant code in the compiler at

https://github.com/SRI-CSL/solidity/blob/a1ec1755fdd40a676ef235026890fe1d7be46634/libsolidity/analysis/ReferencesResolver.cpp#L229-L238

[dddejan]

Attempt for fix at branch keys-are-memory, @hajduakos please take a look.

[hajduakos]

05bb5672289914fb70e90e1204d544aa5d48899c looks fine to me. I also used the TypeProvider at other places in the code to convert between memory/storage types.