fix: vm.etch() leaves storage uninitialized (#363)

.gitignore

@@ -14,7 +14,7 @@ __pycache__/
 
 # Environments
 .env
-.venv
+.venv*
 env/
 venv/
 

src/halmos/cheatcodes.py

@@ -721,6 +721,9 @@ def handle(sevm, ex, arg: ByteVec, stack, step_id) -> ByteVec | None:
             code_bytes = arg[code_loc : code_loc + code_length]
             ex.set_code(who, code_bytes)
 
+            # vm.etch() initializes but does not clear storage
+            ex.storage.setdefault(who, sevm.mk_storagedata())
+
             return ret
 
         # vm.ffi(string[]) returns (bytes)

src/halmos/sevm.py

@@ -2252,6 +2252,7 @@ def create(
 
         # setup new account
         ex.set_code(new_addr, Contract(b""))  # existing code must be empty
+
         # existing storage may not be empty and reset here
         ex.storage[new_addr] = self.mk_storagedata()
 

tests/expected/all.json

@@ -1109,6 +1109,26 @@
                 "num_bounded_loops": null
             }
         ],
+        "test/Foundry.t.sol:TestNotEtchFriendly": [
+            {
+                "name": "check_etch_no_owner(address)",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_etch_then_store()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            }
+        ],
         "test/Getter.t.sol:GetterTest": [
             {
                 "name": "check_Getter(uint256)",

tests/regression/test/Foundry.t.sol

@@ -124,3 +124,47 @@ contract FoundryTest is Test {
     //     assertEq(code, who.code);
     // }
 }
+
+
+contract NotEtchFriendly {
+    address owner;
+
+    constructor() {
+        owner = msg.sender;
+    }
+
+    function beepBoop() public {
+        console2.log("owner is", owner);
+        require(msg.sender == owner, "NotEtchFriendly: only owner can beep boop");
+    }
+}
+
+contract TestNotEtchFriendly is Test {
+    NotEtchFriendly target;
+
+    function setUp() public {
+        /// @dev this is supported in foundry, but not halmos (can't vm.store to uninitialized account)
+        // make address(this) the owner of the yet-to-be-deployed contract
+        // vm.store(address(42), 0, bytes32(uint256(uint160(address(this)))));
+
+        // etch does not run the constructor, so owner is not set by the constructor
+        // additionally, vm.etch does not reset storage (unlike CREATE2)
+        vm.etch(address(42), type(NotEtchFriendly).runtimeCode);
+
+        target = NotEtchFriendly(address(42));
+    }
+
+    function check_etch_no_owner(address sender) external {
+        vm.prank(sender);
+        target.beepBoop();
+
+        assertEq(sender, address(0));
+    }
+
+    function check_etch_then_store() external {
+        // make address(this) the owner of the contract, emulating the constructor that did not run
+        vm.store(address(42), 0, bytes32(uint256(uint160(address(this)))));
+
+        target.beepBoop();
+    }
+}