fix concrete bytes + address collision

src/halmos/sevm.py

@@ -1771,12 +1771,18 @@ def create(
         if op == EVM.CREATE:
             new_addr = ex.new_address()
         else:  # EVM.CREATE2
+            if isinstance(create_hexcode, bytes):
+                create_hexcode = con(
+                    int.from_bytes(create_hexcode, "big"), len(create_hexcode) * 8
+                )
             code_hash = ex.sha3_data(create_hexcode, create_hexcode.size() // 8)
             hash_data = simplify(Concat(con(0xFF, 8), caller, salt, code_hash))
             new_addr = uint160(ex.sha3_data(hash_data, 85))
 
         if new_addr in ex.code:
-            raise ValueError(f"existing address: {new_addr}")
+            ex.error = f"existing address: {hexify(new_addr)}"
+            out.append(ex)
+            return
 
         for addr in ex.code:
             ex.solver.add(new_addr != addr)  # ensure new address is fresh

tests/expected/all.json

@@ -379,6 +379,46 @@
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
+            },
+            {
+                "name": "check_create2_collision(uint256,uint256,bytes32)",
+                "exitcode": 1,
+                "num_models": 0,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_create2_collision_alias(uint256,uint256,bytes32)",
+                "exitcode": 1,
+                "num_models": 1,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_create2_concrete()",
+                "exitcode": 0,
+                "num_models": 0,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_create2_no_collision_1(uint256,uint256,bytes32,bytes32)",
+                "exitcode": 0,
+                "num_models": 0,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_create2_no_collision_2(uint256,uint256,bytes32)",
+                "exitcode": 0,
+                "num_models": 0,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
             }
         ],
         "test/Deal.t.sol:DealTest": [

tests/test/Create2.t.sol

@@ -54,4 +54,54 @@ contract Create2Test is Test {
         assert(C(c2).num1() == y);
         assert(C(c2).num2() == x);
     }
+
+    function check_create2_concrete() public {
+        uint x = 1;
+        uint y = 2;
+        bytes32 salt = bytes32(uint(3));
+
+        C c1 = new C{salt: salt}(x, y);
+
+        bytes32 codeHash = keccak256(abi.encodePacked(type(C).creationCode, abi.encode(x, y)));
+        bytes32 hash = keccak256(abi.encodePacked(bytes1(0xff), address(this), salt, codeHash));
+        address c2 = address(uint160(uint(hash)));
+
+        assert(address(c1) == c2);
+
+        assert(C(c2).num1() == x);
+        assert(C(c2).num2() == y);
+
+        c1.set(y, x);
+
+        assert(C(c2).num1() == y);
+        assert(C(c2).num2() == x);
+    }
+
+    function check_create2_collision(uint x, uint y, bytes32 salt) public {
+        C c1 = new C{salt: salt}(x, y);
+        C c2 = new C{salt: salt}(x, y); // expected to fail
+        assert(c1 == c2); // deadcode
+    }
+
+    function check_create2_no_collision_1(uint x, uint y, bytes32 salt1, bytes32 salt2) public {
+        C c1 = new C{salt: salt1}(x, y);
+        C c2 = new C{salt: salt2}(x, y);
+        assert(c1 != c2);
+    }
+
+    function check_create2_no_collision_2(uint x, uint y, bytes32 salt) public {
+        vm.assume(x != y);
+
+        C c1 = new C{salt: salt}(x, y);
+        C c2 = new C{salt: salt}(y, x);
+        assert(c1 != c2);
+    }
+
+    function check_create2_collision_alias(uint x, uint y, bytes32 salt) public {
+        vm.assume(x == y);
+
+        C c1 = new C{salt: salt}(x, y);
+        C c2 = new C{salt: salt}(y, x);
+        assert(c1 == c2); // currently fail // TODO: support symbolic alias for hash
+    }
 }