a16z / halmos

A symbolic testing tool for EVM smart contracts
GNU Affero General Public License v3.0
802 stars 65 forks source link

storage is not initialized for etched contracts #362

Closed karmacoma-eth closed 2 weeks ago

karmacoma-eth commented 2 weeks ago

Describe the bug We get an internal KeyError when trying to access storage from a vm.etch'ed contract

Reproduce with:

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.15;

import "forge-std/Test.sol";
import {console2} from "forge-std/console2.sol";

import {SymTest} from "halmos-cheatcodes/SymTest.sol";

contract NotEtchable {
    address owner;

    constructor() {
        owner = msg.sender;
    }

    function beepBoop() public {
        require(msg.sender == owner, "NotEtchable: only owner can beep boop");
        console2.log("beep boop");
    }
}

contract Test95 is Test, SymTest {
    NotEtchable target;

    function setUp() public {
        // etch does not run the constructor, so owner is never set
        vm.etch(address(42), type(NotEtchable).runtimeCode);

        target = NotEtchable(address(42));
    }

    function test_beep_boop() external {
        target.beepBoop();
    }
}
halmos --function test_beep_boop

Executing test_beep_boop
[ERROR] test_beep_boop()
KeyError: 42
Traceback (most recent call last):
  File "/Users/karma/projects/halmos/src/halmos/__main__.py", line 950, in run_sequential
    test_result = run(setup_ex, run_args.abi, fun_info, test_config)
                  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/Users/karma/projects/halmos/src/halmos/__main__.py", line 666, in run
    for idx, ex in enumerate(exs):
  File "/Users/karma/projects/halmos/src/halmos/sevm.py", line 2829, in run
    ex.st.push(self.sload(ex, ex.this(), slot))
               ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/Users/karma/projects/halmos/src/halmos/sevm.py", line 1775, in sload
    return self.storage_model.load(ex, addr, loc)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/Users/karma/projects/halmos/src/halmos/sevm.py", line 1382, in load
    cls.init(ex, addr, loc, size_keys)
  File "/Users/karma/projects/halmos/src/halmos/sevm.py", line 1372, in init
    mapping = ex.storage[addr].mapping
              ~~~~~~~~~~^^^^^^
KeyError: 42
Symbolic test result: 0 passed; 1 failed; time: 0.06s

[time] total: 1.32s (build: 0.71s, load: 0.54s, tests: 0.07s)