From 115e66db9c8a8ed2601d17383a6d8f384e3884dc Mon Sep 17 00:00:00 2001
From: karmacoma <karma@coma.lol>
Date: Tue, 17 Sep 2024 15:31:18 -0700
Subject: [PATCH] fix: vm.etch() leaves storage uninitialized (#363)

---
 .gitignore                          |  2 +-
 src/halmos/cheatcodes.py            |  3 ++
 src/halmos/sevm.py                  |  1 +
 tests/expected/all.json             | 20 +++++++++++++
 tests/regression/test/Foundry.t.sol | 44 +++++++++++++++++++++++++++++
 5 files changed, 69 insertions(+), 1 deletion(-)

diff --git a/.gitignore b/.gitignore
index 4397613f..b7579872 100644
--- a/.gitignore
+++ b/.gitignore
@@ -14,7 +14,7 @@ __pycache__/
 
 # Environments
 .env
-.venv
+.venv*
 env/
 venv/
 
diff --git a/src/halmos/cheatcodes.py b/src/halmos/cheatcodes.py
index a6b3afd9..660ed371 100644
--- a/src/halmos/cheatcodes.py
+++ b/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)
diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py
index 6ba9f3e9..28a731c6 100644
--- a/src/halmos/sevm.py
+++ b/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()
 
diff --git a/tests/expected/all.json b/tests/expected/all.json
index 9ef6b057..e624f9d2 100644
--- a/tests/expected/all.json
+++ b/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)",
diff --git a/tests/regression/test/Foundry.t.sol b/tests/regression/test/Foundry.t.sol
index a3f6d983..b61de375 100644
--- a/tests/regression/test/Foundry.t.sol
+++ b/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();
+    }
+}