fix: vm.etch(addr, "") used to raise an exception (a16z#264)

ApeWorX · Apr 11, 2024 · dcd1658 · dcd1658
1 parent 8063b22
commit dcd1658
Show file tree

Hide file tree

Showing 3 changed files with 19 additions and 4 deletions.
diff --git a/src/halmos/cheatcodes.py b/src/halmos/cheatcodes.py
@@ -448,8 +448,11 @@ def handle(sevm, ex, arg: BitVec) -> BitVec:
             try:
                 code_offset = int_of(extract_bytes(arg, 4 + 32, 32))
                 code_length = int_of(extract_bytes(arg, 4 + code_offset, 32))
-                code_int = int_of(extract_bytes(arg, 4 + code_offset + 32, code_length))
-                code_bytes = code_int.to_bytes(code_length, "big")
+
+                code_bytes = bytes()
+                if code_length != 0:
+                    code_bv = extract_bytes(arg, 4 + code_offset + 32, code_length)
+                    code_bytes = bv_value_to_bytes(code_bv)
                 ex.set_code(who, code_bytes)
             except Exception as e:
                 error_msg = f"vm.etch(address who, bytes code) must have concrete argument `code` but received calldata {arg}"
@@ -508,8 +511,6 @@ def handle(sevm, ex, arg: BitVec) -> BitVec:
             digest = extract_bytes(arg, 4 + 32, 32)
 
             # TODO: handle concrete private key + digest (generate concrete signature)
-            # TODO: do we want to constrain v to {27, 28}?
-            # TODO: do we want to constrain r and s to be less than curve order?
 
             # check for an existing signature
             known_sigs = ex.known_sigs

diff --git a/tests/expected/all.json b/tests/expected/all.json
@@ -802,6 +802,15 @@
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
+            },
+            {
+                "name": "check_etch_emptyBytecode()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
             }
         ],
         "test/Getter.t.sol:GetterTest": [

diff --git a/tests/regression/test/Foundry.t.sol b/tests/regression/test/Foundry.t.sol
@@ -66,7 +66,12 @@ contract FoundryTest is Test {
         assertEq(uint256(uint8(retval[0])), 0xAA);
     }
 
+    function check_etch_emptyBytecode() public {
+        vm.etch(address(0x42), hex"");
+        (bool success, ) = address(0x42).call("");
 
+        assertTrue(success);
+    }
 
     /// @notice etching to a symbolic address is not supported
     // function check_etch_SymbolicAddr(address who) public {