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

Storage struct assignment with mappings #39

Closed hajduakos closed 4 years ago

hajduakos commented 5 years ago

Currently we translate storage structures to SMT datatypes. Assignments between them are simply translated to assignments between the datatypes, which will make a deep copy. However, in Solidity there is an exception: mappings are not copied.

pragma solidity >=0.5.0;

contract StructsMaps {

  struct A {
    mapping(address=>int) m;
  }

  A a1;
  A a2;

  function() external payable {
    a1.m[address(this)] = 2;
    a1 = a2; // Mapping should not be overwritten
    assert(a1.m[address(this)] == 2);
  }
}

Output:

$ solc-verify.py StructsMaps.sol
StructsMaps::[fallback]: ERROR
 - StructsMaps.sol:15:5: Assertion might not hold.
StructsMaps::[implicit_constructor]: OK
Errors were found by the verifier.

(The assert should hold.)

dddejan commented 5 years ago

This looks very annoying.

hajduakos commented 4 years ago

Will be disallowed in 0.7, see https://github.com/ethereum/solidity/issues/7739