feat: add support for vm.label() and makeAddrAndKey()

src/halmos/cheatcodes.py

@@ -325,6 +325,9 @@ class hevm_cheat_code:
     # sign(uint256,bytes32)
     sign_sig: int = 0xE341EAA4
 
+    # label(address,string)
+    label_sig: int = 0xC657C718
+
     @staticmethod
     def handle(sevm, ex, arg: BitVec) -> BitVec:
         funsig: int = int_of(extract_funsig(arg), "symbolic hevm cheatcode")
@@ -536,6 +539,13 @@ def handle(sevm, ex, arg: BitVec) -> BitVec:
 
             return Concat(uint256(v), r, s)
 
+        elif funsig == hevm_cheat_code.label_sig:
+            addr = extract_bytes(arg, 4, 32)
+            label = extract_string_argument(arg, 1)
+
+            # TODO: no-op for now
+            pass
+
         else:
             # TODO: support other cheat codes
             msg = f"Unsupported cheat code: calldata = {hexify(arg)}"

src/halmos/sevm.py

@@ -153,10 +153,6 @@ def iter_bytes(x: Any, _byte_length: int = -1):
     raise ValueError(x)
 
 
-def is_concrete(x: Any) -> bool:
-    return isinstance(x, int) or isinstance(x, bytes) or is_bv_value(x)
-
-
 def mnemonic(opcode) -> str:
     if is_concrete(opcode):
         opcode = int_of(opcode)

src/halmos/utils.py

@@ -141,6 +141,10 @@ def is_zero(x: Word) -> Word:
     return test(x, False)
 
 
+def is_concrete(x: Any) -> bool:
+    return isinstance(x, int) or isinstance(x, bytes) or is_bv_value(x)
+
+
 def create_solver(logic="QF_AUFBV", ctx=None, timeout=0, max_memory=0):
     # QF_AUFBV: quantifier-free bitvector + array theory: https://smtlib.cs.uiowa.edu/logics.shtml
     solver = SolverFor(logic, ctx=ctx)
@@ -175,7 +179,7 @@ def extract_bytes_argument(calldata: BitVecRef, arg_idx: int) -> bytes:
 def extract_string_argument(calldata: BitVecRef, arg_idx: int):
     """Extracts idx-th argument of string from calldata"""
     string_bytes = extract_bytes_argument(calldata, arg_idx)
-    return string_bytes.decode("utf-8") if string_bytes else ""
+    return string_bytes.decode("utf-8") if is_concrete(string_bytes) else string_bytes
 
 
 def extract_bytes(data: BitVecRef, byte_offset: int, size_bytes: int) -> BitVecRef:

tests/expected/all.json

@@ -1540,6 +1540,60 @@
                 "time": null,
                 "num_bounded_loops": null
             },
+            {
+                "name": "check_makeAddrAndKey_consistent_concrete()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_makeAddrAndKey_consistent_symbolic()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_makeAddrAndKey_noCollision_concrete()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_makeAddrAndKey_noCollision_symbolic()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_makeAddrAndKey_vmsign_ecrecover_e2e_concrete()",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
+            {
+                "name": "check_makeAddrAndKey_vmsign_ecrecover_e2e_symbolic(string,bytes32)",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            },
             {
                 "name": "check_tryRecover(address,bytes32,bytes)",
                 "exitcode": 0,
@@ -2078,4 +2132,4 @@
             }
         ]
     }
-}
+}

tests/regression/test/Signature.t.sol

@@ -86,7 +86,7 @@ contract SignatureTest is SymTest, Test {
     /// FIXME: this returns a counterexample, but it shouldn't
     // function check_vmaddr_concreteKey() public {
     //     address addr = vm.addr(0x42);
-    //     assertEq(0x6f4c950442e1Af093BcfF730381E63Ae9171b87a);
+    //     assertEq(addr, 0x6f4c950442e1Af093BcfF730381E63Ae9171b87a);
     // }
 
     /// FIXME: this returns a counterexample, but it shouldn't
@@ -293,4 +293,61 @@ contract SignatureTest is SymTest, Test {
         assertEq(ecrecover(digest, v1, r1, s1), vm.addr(privateKey1));
         assertEq(ecrecover(digest, v2, r2, s2), vm.addr(privateKey2));
     }
+
+    function check_makeAddrAndKey_consistent_symbolic() public {
+        string memory keyName = svm.createString(32, "keyName");
+        (address addr, uint256 key) = makeAddrAndKey(keyName);
+
+        assertEq(addr, vm.addr(key));
+    }
+
+    function check_makeAddrAndKey_consistent_concrete() public {
+        (address addr, uint256 key) = makeAddrAndKey("someKey");
+
+        assertEq(addr, vm.addr(key));
+    }
+
+    function check_makeAddrAndKey_noCollision_symbolic() public {
+        string memory keyName1 = svm.createString(32, "keyName1");
+        (address addr1, uint256 key1) = makeAddrAndKey(keyName1);
+
+        string memory keyName2 = svm.createString(32, "keyName2");
+        (address addr2, uint256 key2) = makeAddrAndKey(keyName2);
+
+        // assume distinct keys
+        vm.assume(keccak256(abi.encodePacked(keyName1)) != keccak256(abi.encodePacked(keyName2)));
+
+        assertNotEq(key1, key2);
+        assertNotEq(addr1, addr2);
+        assertEq(vm.addr(key1), addr1);
+        assertEq(vm.addr(key2), addr2);
+    }
+
+    function check_makeAddrAndKey_noCollision_concrete() public {
+        (address addr1, uint256 key1) = makeAddrAndKey("someKey");
+        (address addr2, uint256 key2) = makeAddrAndKey("anotherKey");
+
+        assertNotEq(key1, key2);
+        assertNotEq(addr1, addr2);
+        assertEq(vm.addr(key1), addr1);
+        assertEq(vm.addr(key2), addr2);
+    }
+
+    function check_makeAddrAndKey_vmsign_ecrecover_e2e_symbolic(
+        string memory keyName,
+        bytes32 digest
+    ) public {
+        (address addr, uint256 key) = makeAddrAndKey(keyName);
+        (uint8 v, bytes32 r, bytes32 s) = vm.sign(key, digest);
+        address recoveredAddr = ecrecover(digest, v, r, s);
+        assertEq(addr, recoveredAddr);
+    }
+
+    function check_makeAddrAndKey_vmsign_ecrecover_e2e_concrete() public {
+        (address addr, uint256 key) = makeAddrAndKey("someKey");
+        bytes32 digest = keccak256(abi.encodePacked("someData"));
+        (uint8 v, bytes32 r, bytes32 s) = vm.sign(key, digest);
+        address recoveredAddr = ecrecover(digest, v, r, s);
+        assertEq(addr, recoveredAddr);
+    }
 }