Multi-dimensional mappings are not zero-initialized

[daejunpark]

Summary

Verisol seems to incorrectly reason about the initialization of multi-dimensional mappings, leading to generating false positives.

Minimal example

In the following example, two contracts MapInitTest1 and MapInitTest2 are similar except the dimension of the mapping involved (i.e., the former uses a single-dimensional mapping, while the latter uses a multi-dimensional mapping). However, Verisol proves the former, but refutes the latter with a counter example, which is a false positive.

pragma solidity >=0.4.24<0.6.0;
    
contract MapInitTest1 {
    mapping (uint256 => uint256) public recoverMap1; 
        
    constructor(uint256 owner, uint256 key)
        public
    {   
        require(owner != 0);
        recoverMap1[key] = owner;
    }   
        
    function test(uint256 key)
        external
    {   
        uint256 owner1 = recoverMap1[key];
        uint256 owner2 = recoverMap1[key + 1];
        require(owner1 != 0);
    
        assert(owner1 != owner2);
    }
}

contract MapInitTest2 {
    mapping (uint256 => mapping (uint256 => uint256)) public recoverMap2;

    constructor(uint256 owner, uint256 key1, uint256 key2)
        public
    {
        require(owner != 0);
        recoverMap2[key1][key2] = owner;
    }

    function test(uint256 key1, uint256 key2)
        external
    {
        uint256 owner1 = recoverMap2[key1][key2];
        uint256 owner2 = recoverMap2[key1][key2 + 1];
        require(owner1 != 0);

        assert(owner1 != owner2);   // <--- false positive corral runs
    }
}

To reproduce, run Verisol with the following commands:

$ dotnet VeriSol.dll MapInitTest.sol MapInitTest1 /tryProof /tryRefutation:8 /printTransactionSequence
    ...
    *** Proof found! Formal Verification successful!

$ dotnet VeriSol.dll MapInitTest.sol MapInitTest2 /tryProof /tryRefutation:8 /printTransactionSequence
    ...
    *** Found a counterexample
    ...

Details

In the generated boogie file, we have the initialization of the single-dimensional mapping recoverMap1, as follows,

var recoverMap1_MapInitTest1: [Ref]Ref;
implementation MapInitTest1_MapInitTest1_NoBaseCtor(...)
{
var __var_1: Ref;
// start of initialization
...
// Make array/mapping vars distinct for recoverMap1
call __var_1 := FreshRefGenerator();
recoverMap1_MapInitTest1[this] := __var_1;
// Initialize Integer mapping recoverMap1
assume (forall  __i__0_0:int ::  ((M_int_int[recoverMap1_MapInitTest1[this]][__i__0_0]) == (0)));
// end of initialization
...
}

but we do NOT have any initialization for the multi-dimensional mapping recoverMap2 as follows:

var recoverMap2_MapInitTest2: [Ref]Ref;
implementation MapInitTest2_MapInitTest2_NoBaseCtor(...)
{
var __var_2: Ref;
// start of initialization
...
// Make array/mapping vars distinct for recoverMap2
call __var_2 := FreshRefGenerator();
recoverMap2_MapInitTest2[this] := __var_2;
// end of initialization
...
}