From 1556374a0095d3cb40277debc2804c186a6007f4 Mon Sep 17 00:00:00 2001 From: karmacoma Date: Wed, 20 Mar 2024 10:24:30 -0700 Subject: [PATCH 1/7] feat: support for signing and verifying signatures (#257) --- src/halmos/cheatcodes.py | 100 +++++++++ src/halmos/sevm.py | 39 +++- src/halmos/utils.py | 26 ++- tests/expected/all.json | 216 +++++++++++++++++++ tests/regression/test/Signature.t.sol | 299 ++++++++++++++++++++++++++ 5 files changed, 669 insertions(+), 11 deletions(-) diff --git a/src/halmos/cheatcodes.py b/src/halmos/cheatcodes.py index 9a49e0ea..2e430786 100644 --- a/src/halmos/cheatcodes.py +++ b/src/halmos/cheatcodes.py @@ -12,6 +12,19 @@ from .utils import * +# f_vmaddr(key) -> address +f_vmaddr = Function("f_vmaddr", BitVecSort256, BitVecSort160) + +# f_sign_v(key, digest) -> v +f_sign_v = Function("f_sign_v", BitVecSort256, BitVecSort256, BitVecSort8) + +# f_sign_r(key, digest) -> r +f_sign_r = Function("f_sign_r", BitVecSort256, BitVecSort256, BitVecSort256) + +# f_sign_s(key, digest) -> s +f_sign_s = Function("f_sign_s", BitVecSort256, BitVecSort256, BitVecSort256) + + def name_of(x: str) -> str: return re.sub(r"\s+", "_", x) @@ -192,6 +205,25 @@ def create_bool(ex, arg): return uint256(create_generic(ex, 1, name, "bool")) +def apply_vmaddr(ex, private_key: Any): + # check if this private key has an existing address associated with it + known_keys = ex.known_keys + addr = known_keys.get(private_key, None) + if addr is None: + # if not, create a new address + addr = f_vmaddr(private_key) + + # mark the addresses as distinct + for other_key, other_addr in known_keys.items(): + distinct = Implies(private_key != other_key, addr != other_addr) + ex.path.append(distinct) + + # associate the new address with the private key + known_keys[private_key] = addr + + return addr + + class halmos_cheat_code: # address constant SVM_ADDRESS = # address(bytes20(uint160(uint256(keccak256('svm cheat code'))))); @@ -287,6 +319,15 @@ class hevm_cheat_code: # bytes4(keccak256("ffi(string[])")) ffi_sig: int = 0x89160467 + # addr(uint256) + addr_sig: int = 0xFFA18649 + + # 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") @@ -448,6 +489,65 @@ def handle(sevm, ex, arg: BitVec) -> BitVec: return stringified_bytes_to_bytes(out_str) + elif funsig == hevm_cheat_code.addr_sig: + private_key = extract_bytes(arg, 4, 32) + + # TODO: handle concrete private key (return directly the corresponding address) + # TODO: check (or assume?) private_key is valid + # - less than curve order + # - not zero + # TODO: add constraints that the generated addresses are reasonable + # - not zero + # - not the address of a known contract + + addr = apply_vmaddr(ex, private_key) + return uint256(addr) + + elif funsig == hevm_cheat_code.sign_sig: + key = extract_bytes(arg, 4, 32) + 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 + (v, r, s) = known_sigs.get((key, digest), (None, None, None)) + if (v, r, s) == (None, None, None): + # if not, create a new signature + v, r, s = (f(key, digest) for f in (f_sign_v, f_sign_r, f_sign_s)) + + # associate the new signature with the private key and digest + known_sigs[(key, digest)] = (v, r, s) + + # explicitly model malleability + recover = f_ecrecover(digest, v, r, s) + recover_malleable = f_ecrecover(digest, v ^ 1, r, secp256k1n - s) + + addr = apply_vmaddr(ex, key) + ex.path.append(recover == addr) + ex.path.append(recover_malleable == addr) + + # mark signatures as distinct if key or digest are distinct + # NOTE: the condition `And(r != _r, s != _s)` is stronger than `Or(v != _v, r != _r, s != _s)` which is sound + # TODO: we need to figure out whether this stronger condition is necessary and whether it could lead to unsound results in practical cases + for (_key, _digest), (_v, _r, _s) in known_sigs.items(): + distinct = Implies( + Or(key != _key, digest != _digest), + Or(v != _v, r != _r, s != _s), + ) + ex.path.append(distinct) + + 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)}" diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py index 3b23dc85..37950d1f 100644 --- a/src/halmos/sevm.py +++ b/src/halmos/sevm.py @@ -32,7 +32,6 @@ INTERNAL_ERROR, ) - Steps = Dict[int, Dict[str, Any]] # execution tree EMPTY_BYTES = b"" @@ -41,6 +40,7 @@ # TODO: make this configurable MAX_MEMORY_SIZE = 2**20 + # symbolic states # calldataload(index) f_calldataload = Function("calldataload", BitVecSort256, BitVecSort256) @@ -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) @@ -768,6 +764,8 @@ class Exec: # an execution path storages: Dict[Any, Any] # storage updates balances: Dict[Any, Any] # balance updates calls: List[Any] # external calls + known_keys: Dict[Any, Any] # maps address to private key + known_sigs: Dict[Any, Any] # maps (private_key, digest) to (v, r, s) def __init__(self, **kwargs) -> None: self.code = kwargs["code"] @@ -796,6 +794,8 @@ def __init__(self, **kwargs) -> None: self.storages = kwargs["storages"] self.balances = kwargs["balances"] self.calls = kwargs["calls"] + self.known_keys = kwargs["known_keys"] if "known_keys" in kwargs else {} + self.known_sigs = kwargs["known_sigs"] if "known_sigs" in kwargs else {} assert_address(self.context.message.target) assert_address(self.context.message.caller) @@ -1769,6 +1769,8 @@ def callback(new_ex, stack, step_id): storages=ex.storages, balances=ex.balances, calls=ex.calls, + known_keys=ex.known_keys, + known_sigs=ex.known_sigs, ) stack.append((sub_ex, step_id)) @@ -1826,25 +1828,38 @@ def call_unknown() -> None: # ecrecover if eq(to, con_addr(1)): - ex.path.append(exit_code_var != con(0)) + # TODO: explicitly return empty data in case of an error + # TODO: validate input and fork on error? + # - v in [27, 28] + # - r, s in [1, secp256k1n) + + # call never fails, errors result in empty returndata + ex.path.append(exit_code_var != 0) + + digest = extract_bytes(arg, 0, 32) + v = uint8(extract_bytes(arg, 32, 32)) + r = extract_bytes(arg, 64, 32) + s = extract_bytes(arg, 96, 32) + + ret = uint256(f_ecrecover(digest, v, r, s)) # identity - if eq(to, con_addr(4)): + elif eq(to, con_addr(4)): ex.path.append(exit_code_var != con(0)) ret = arg # halmos cheat code - if eq(to, halmos_cheat_code.address): + elif eq(to, halmos_cheat_code.address): ex.path.append(exit_code_var != con(0)) ret = halmos_cheat_code.handle(ex, arg) # vm cheat code - if eq(to, hevm_cheat_code.address): + elif eq(to, hevm_cheat_code.address): ex.path.append(exit_code_var != con(0)) ret = hevm_cheat_code.handle(self, ex, arg) # console - if eq(to, console.address): + elif eq(to, console.address): ex.path.append(exit_code_var != con(0)) console.handle(ex, arg) @@ -2058,6 +2073,8 @@ def callback(new_ex, stack, step_id): storages=ex.storages, balances=ex.balances, calls=ex.calls, + known_keys=ex.known_keys, + known_sigs=ex.known_sigs, ) stack.append((sub_ex, step_id)) @@ -2180,6 +2197,8 @@ def create_branch(self, ex: Exec, cond: BitVecRef, target: int) -> Exec: storages=ex.storages.copy(), balances=ex.balances.copy(), calls=ex.calls.copy(), + known_keys=ex.known_keys, # pass by reference, not need to copy + known_sigs=ex.known_sigs, # pass by reference, not need to copy ) return new_ex diff --git a/src/halmos/utils.py b/src/halmos/utils.py index f892ea77..2ff0a317 100644 --- a/src/halmos/utils.py +++ b/src/halmos/utils.py @@ -9,6 +9,10 @@ from .exceptions import NotConcreteError, HalmosException +# order of the secp256k1 curve +secp256k1n = ( + 115792089237316195423570985008687907852837564279074904382605163141518161494337 +) Word = Any # z3 expression (including constants) Byte = Any # z3 expression (including constants) @@ -55,6 +59,12 @@ def __getitem__(self, size: int) -> BitVecSort: BitVecSort512 = BitVecSorts[512] +# ecrecover(digest, v, r, s) +f_ecrecover = Function( + "ecrecover", BitVecSort256, BitVecSort8, BitVecSort256, BitVecSort256, BitVecSort160 +) + + def concat(args): if len(args) > 1: return Concat(args) @@ -92,6 +102,16 @@ def uint160(x: BitVecRef) -> BitVecRef: return simplify(ZeroExt(160 - bitsize, x)) +def uint8(x: BitVecRef) -> BitVecRef: + bitsize = x.size() + if bitsize == 8: + return x + if bitsize > 8: + return simplify(Extract(7, 0, x)) + else: + return simplify(ZeroExt(8 - bitsize, x)) + + def con(n: int, size_bits=256) -> Word: return BitVecVal(n, BitVecSorts[size_bits]) @@ -121,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) @@ -155,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: diff --git a/tests/expected/all.json b/tests/expected/all.json index 828cbd8d..cbba7ea4 100644 --- a/tests/expected/all.json +++ b/tests/expected/all.json @@ -1468,6 +1468,60 @@ "time": null, "num_bounded_loops": null }, + { + "name": "check_ecrecover_distinctKeysSameDigestCorrectRecovery(uint256,uint256,bytes32)", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_ecrecover_distinctKeysSameDigestDistinctAddrs(uint256,uint256,bytes32)", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_ecrecover_explicitMalleability(uint256,bytes32)", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_ecrecover_sameKeyDistinctDigestsCorrectRecovery(uint256,bytes32,bytes32)", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_ecrecover_sameKeyDistinctDigestsUniqueRecovery(uint256,bytes32,bytes32)", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_ecrecover_solveForMalleability(uint256,bytes32)", + "exitcode": 1, + "num_models": 3, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, { "name": "check_isValidERC1271SignatureNow(bytes32,bytes)", "exitcode": 0, @@ -1486,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, @@ -1494,6 +1602,114 @@ "num_paths": null, "time": null, "num_bounded_loops": null + }, + { + "name": "check_vmaddr_canFindKeyForAddr_concrete(uint256)", + "exitcode": 1, + "num_models": 1, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_vmaddr_canFindKeyForAddr_mixed(uint256)", + "exitcode": 1, + "num_models": 1, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_vmaddr_canFindKeyForAddr_symbolic(uint256,uint256)", + "exitcode": 1, + "num_models": 1, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_vmaddr_consistent(uint256)", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_vmaddr_noCollision_concrete(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_vmaddr_noCollision_symbolic(uint256,uint256)", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_vmsign_canFindKeyForGivenSig(uint256,uint256,bytes32)", + "exitcode": 1, + "num_models": 1, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_vmsign_consistent(uint256,bytes32)", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_vmsign_ecrecover_e2e_recoveredCanNotMatchOtherAddr(uint256,bytes32,address)", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_vmsign_ecrecover_e2e_recoveredMatches(uint256,bytes32)", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_vmsign_noDigestCollision(uint256,bytes32,bytes32)", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_vmsign_noKeyCollision(uint256,uint256,bytes32)", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null } ], "test/SmolWETH.t.sol:SmolWETHTest": [ diff --git a/tests/regression/test/Signature.t.sol b/tests/regression/test/Signature.t.sol index bc9c9ea6..600f64ae 100644 --- a/tests/regression/test/Signature.t.sol +++ b/tests/regression/test/Signature.t.sol @@ -3,10 +3,13 @@ pragma solidity >=0.8.0 <0.9.0; import {SymTest} from "halmos-cheatcodes/SymTest.sol"; import {Test} from "forge-std/Test.sol"; +import {console2} from "forge-std/console2.sol"; import {SignatureChecker} from "openzeppelin/utils/cryptography/SignatureChecker.sol"; import {ECDSA} from "openzeppelin/utils/cryptography/ECDSA.sol"; +uint256 constant secp256k1n = 115792089237316195423570985008687907852837564279074904382605163141518161494337; + contract SymAccount is SymTest { fallback(bytes calldata) external payable returns (bytes memory) { uint mode = svm.createUint256("mode"); @@ -23,6 +26,8 @@ contract SymAccount is SymTest { } contract SignatureTest is SymTest, Test { + uint256 constant private ECRECOVER_PRECOMPILE = 1; + function check_isValidSignatureNow(bytes32 hash, bytes memory signature) public { address signer = address(new SymAccount()); if (!SignatureChecker.isValidSignatureNow(signer, hash, signature)) revert(); @@ -51,4 +56,298 @@ contract SignatureTest is SymTest, Test { if (signer == address(0)) revert(); assert(true); } + + function check_vmaddr_consistent(uint256 privateKey) public { + address addr1 = vm.addr(privateKey); + address addr2 = vm.addr(privateKey); + + assertEq(addr1, addr2); + } + + function check_vmaddr_noCollision_symbolic( + uint256 privateKey1, + uint256 privateKey2 + ) public { + vm.assume(privateKey1 != privateKey2); + + address addr1 = vm.addr(privateKey1); + address addr2 = vm.addr(privateKey2); + + assertNotEq(addr1, addr2); + } + + function check_vmaddr_noCollision_concrete( + uint256 privateKey1, + uint256 privateKey2 + ) public { + assertNotEq(vm.addr(42), vm.addr(43)); + } + + /// FIXME: this returns a counterexample, but it shouldn't + // function check_vmaddr_concreteKey() public { + // address addr = vm.addr(0x42); + // assertEq(addr, 0x6f4c950442e1Af093BcfF730381E63Ae9171b87a); + // } + + /// FIXME: this returns a counterexample, but it shouldn't + // function check_vmaddr_saneAddressConstraints(uint256 privateKey) public { + // address addr = vm.addr(privateKey); + // assertNotEq(addr, address(0)); + // assertNotEq(addr, address(this)); + // } + + /// we expect a counterexample for this test + /// the addresses match if the private keys are equal + function check_vmaddr_canFindKeyForAddr_symbolic( + uint256 privateKey1, + uint256 privateKey2 + ) public { + address addr1 = vm.addr(privateKey1); + address addr2 = vm.addr(privateKey2); + + assertNotEq(addr1, addr2); + } + + /// we expect a counterexample for this test + /// the addresses match if the private keys are equal + function check_vmaddr_canFindKeyForAddr_mixed( + uint256 privateKey + ) public { + address addr1 = vm.addr(0x42); + address addr2 = vm.addr(privateKey); + + assertNotEq(addr1, addr2); + } + + /// we expect a counterexample (the key for a given address which is ofc nonsense) + /// that's because we only add constraints about the relations between + /// different vm.addr() calls, but not about specific addresses + function check_vmaddr_canFindKeyForAddr_concrete(uint256 privateKey) public { + address addr = vm.addr(privateKey); + assertNotEq(addr, address(0x42)); + } + + function check_vmsign_consistent( + uint256 privateKey, + bytes32 digest + ) public { + (uint8 v1, bytes32 r1, bytes32 s1) = vm.sign(privateKey, digest); + (uint8 v2, bytes32 r2, bytes32 s2) = vm.sign(privateKey, digest); + + assertEq(v1, v2); + assertEq(r1, r2); + assertEq(s1, s2); + } + + function check_vmsign_noDigestCollision( + uint256 privateKey, + bytes32 digest1, + bytes32 digest2 + ) public { + vm.assume(digest1 != digest2); + + (uint8 v1, bytes32 r1, bytes32 s1) = vm.sign(privateKey, digest1); + (uint8 v2, bytes32 r2, bytes32 s2) = vm.sign(privateKey, digest2); + + bytes memory sig1 = abi.encodePacked(v1, r1, s1); + bytes memory sig2 = abi.encodePacked(v2, r2, s2); + assertNotEq(keccak256(sig1), keccak256(sig2)); + } + + function check_vmsign_noKeyCollision( + uint256 privateKey1, + uint256 privateKey2, + bytes32 digest + ) public { + vm.assume(privateKey1 != privateKey2); + + (uint8 v1, bytes32 r1, bytes32 s1) = vm.sign(privateKey1, digest); + (uint8 v2, bytes32 r2, bytes32 s2) = vm.sign(privateKey2, digest); + + assert(v1 != v2 || r1 != r2 || s1 != s2); + } + + /// we expect a counterexample for this test + /// the signatures match if the private keys are equal + function check_vmsign_canFindKeyForGivenSig( + uint256 privateKey1, + uint256 privateKey2, + bytes32 digest + ) public { + (uint8 v1, bytes32 r1, bytes32 s1) = vm.sign(privateKey1, digest); + (uint8 v2, bytes32 r2, bytes32 s2) = vm.sign(privateKey2, digest); + + assertNotEq(r1, r2); + } + + function check_vmsign_ecrecover_e2e_recoveredMatches( + uint256 privateKey, + bytes32 digest + ) public { + address originalAddr = vm.addr(privateKey); + (uint8 v, bytes32 r, bytes32 s) = vm.sign(privateKey, digest); + address recoveredAddr = ecrecover(digest, v, r, s); + assertEq(originalAddr, recoveredAddr); + } + + function check_vmsign_ecrecover_e2e_recoveredCanNotMatchOtherAddr( + uint256 privateKey, + bytes32 digest, + address otherAddr + ) public { + address originalAddr = vm.addr(privateKey); + vm.assume(originalAddr != otherAddr); + + (uint8 v, bytes32 r, bytes32 s) = vm.sign(privateKey, digest); + address recoveredAddr = ecrecover(digest, v, r, s); + assertNotEq(otherAddr, recoveredAddr); + } + + /// we expect a counterexample for this test + function check_ecrecover_solveForMalleability( + uint256 privateKey, + bytes32 digest + ) public { + (uint8 v, bytes32 r, bytes32 s) = vm.sign(privateKey, digest); + + // create another symbolic signature + uint8 otherV = uint8(svm.createUint256("otherV")); + bytes32 otherR = svm.createBytes32("otherR"); + bytes32 otherS = svm.createBytes32("otherS"); + + vm.assume(v != otherV || r != otherR || s != otherS); + + assertNotEq(ecrecover(digest, v, r, s), ecrecover(digest, otherV, otherR, otherS)); + } + + function check_ecrecover_explicitMalleability( + uint256 privateKey, + bytes32 digest + ) public { + (uint8 v, bytes32 r, bytes32 s) = vm.sign(privateKey, digest); + + assertEq( + ecrecover(digest, v, r, s), + ecrecover(digest, v ^ 1, r, bytes32(secp256k1n - uint256(s))) + ); + } + + function check_ecrecover_sameKeyDistinctDigestsUniqueRecovery( + uint256 privateKey, + bytes32 digest1, + bytes32 digest2 + ) public { + vm.assume(digest1 != digest2); + + (uint8 v1, bytes32 r1, bytes32 s1) = vm.sign(privateKey, digest1); + (uint8 v2, bytes32 r2, bytes32 s2) = vm.sign(privateKey, digest2); + + assertEq(ecrecover(digest1, v1, r1, s1), ecrecover(digest2, v2, r2, s2)); + } + + function check_ecrecover_sameKeyDistinctDigestsCorrectRecovery( + uint256 privateKey, + bytes32 digest1, + bytes32 digest2 + ) public { + vm.assume(digest1 != digest2); + + address originalAddr = vm.addr(privateKey); + + (uint8 v1, bytes32 r1, bytes32 s1) = vm.sign(privateKey, digest1); + (uint8 v2, bytes32 r2, bytes32 s2) = vm.sign(privateKey, digest2); + + address addr1 = ecrecover(digest1, v1, r1, s1); + assertEq(addr1, originalAddr); + + address addr2 = ecrecover(digest2, v2, r2, s2); + assertEq(addr2, originalAddr); + } + + function check_ecrecover_distinctKeysSameDigestDistinctAddrs( + uint256 privateKey1, + uint256 privateKey2, + bytes32 digest + ) public { + vm.assume(privateKey1 != privateKey2); + + (uint8 v1, bytes32 r1, bytes32 s1) = vm.sign(privateKey1, digest); + (uint8 v2, bytes32 r2, bytes32 s2) = vm.sign(privateKey2, digest); + + address addr1 = ecrecover(digest, v1, r1, s1); + address addr2 = ecrecover(digest, v2, r2, s2); + + assertNotEq(addr1, addr2); + } + + function check_ecrecover_distinctKeysSameDigestCorrectRecovery( + uint256 privateKey1, + uint256 privateKey2, + bytes32 digest + ) public { + vm.assume(privateKey1 != privateKey2); + + (uint8 v1, bytes32 r1, bytes32 s1) = vm.sign(privateKey1, digest); + (uint8 v2, bytes32 r2, bytes32 s2) = vm.sign(privateKey2, digest); + + 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); + } } From 8053b5872cd7230a53cc92eae86fce698c82e23d Mon Sep 17 00:00:00 2001 From: Cosmin Radoi Date: Wed, 20 Mar 2024 10:25:25 -0700 Subject: [PATCH 2/7] docs: small fixes for `getting-started.md` (#258) --- docs/getting-started.md | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/docs/getting-started.md b/docs/getting-started.md index 865305d8..c3ca1534 100644 --- a/docs/getting-started.md +++ b/docs/getting-started.md @@ -58,8 +58,10 @@ contract MyToken is ERC20 { Then you can write a `setUp()` function that creates a new token contract with a _symbolic_ initial supply, as follows: ```solidity import {SymTest} from "halmos-cheatcodes/SymTest.sol"; +import {Test} from "forge-std/Test.sol"; +import {MyToken} from "../src/MyToken.sol"; -contract MyTokenTest is SymTest { +contract MyTokenTest is SymTest, Test { MyToken token; function setUp() public { @@ -104,7 +106,7 @@ Below is an example symbolic test for the token transfer function: function check_transfer(address sender, address receiver, uint256 amount) public { // specify input conditions vm.assume(receiver != address(0)); - vm.assume(token.balance(sender) >= amount); + vm.assume(token.balanceOf(sender) >= amount); // record the current balance of sender and receiver uint256 balanceOfSender = token.balanceOf(sender); @@ -179,7 +181,7 @@ Recall that symbolic tests take into account all possible input combinations. Ho In our example, the conditions for the valid sender and receiver addresses are specified as follows: ```solidity vm.assume(receiver != address(0)); -vm.assume(token.balance(sender) >= amount); +vm.assume(token.balanceOf(sender) >= amount); ``` Like fuzz tests, any input combinations that don't satisfy the `assume()` conditions are disregarded. This means that, after executing the above `assume()` statements, only the input combinations in which the receiver is non-zero and the sender has sufficient balance are considered. Other input combinations that violate these conditions are ignored. From 30c6bb741d2e6d50136f389eed0b9ac748e9bc58 Mon Sep 17 00:00:00 2001 From: karmacoma Date: Tue, 26 Mar 2024 10:11:40 -0700 Subject: [PATCH 3/7] feat: constrain (r, s, v) signature values (#259) --- examples/simple/src/BadElections.sol | 38 +++++++++++++++ examples/simple/test/BadElections.t.sol | 60 +++++++++++++++++++++++ src/halmos/cheatcodes.py | 10 ++++ src/halmos/utils.py | 7 ++- tests/expected/all.json | 27 +++++++++++ tests/regression/test/Signature.t.sol | 64 +++++++++++++++++++++++++ 6 files changed, 205 insertions(+), 1 deletion(-) create mode 100644 examples/simple/src/BadElections.sol create mode 100644 examples/simple/test/BadElections.t.sol diff --git a/examples/simple/src/BadElections.sol b/examples/simple/src/BadElections.sol new file mode 100644 index 00000000..24ffd798 --- /dev/null +++ b/examples/simple/src/BadElections.sol @@ -0,0 +1,38 @@ +// SPDX-License-Identifier: AGPL-3.0 +pragma solidity >=0.8.0 <0.9.0; + +import {ECDSA} from "openzeppelin/utils/cryptography/ECDSA.sol"; + +/// DO NOT USE, this demonstrates signature malleability problems +contract BadElections { + event Voted(uint256 proposalId, bool support, address voter); + + mapping (bytes32 => bool) hasVoted; + + // maps proposalId to vote count + mapping (uint256 => uint256) public votesFor; + mapping (uint256 => uint256) public votesAgainst; + + // vote on a proposal by signature, anyone can cast a vote on behalf of someone else + function vote(uint256 proposalId, bool support, address voter, bytes calldata signature) public { + bytes32 sigHash = keccak256(signature); + require(!hasVoted[sigHash], "already voted"); + + bytes32 badSigDigest = keccak256(abi.encode(proposalId, support, voter)); + address recovered = ECDSA.recover(badSigDigest, signature); + require(recovered == voter, "invalid signature"); + require(recovered != address(0), "invalid signature"); + + // prevent replay + hasVoted[sigHash] = true; + + // record vote + if (support) { + votesFor[proposalId]++; + } else { + votesAgainst[proposalId]++; + } + + emit Voted(proposalId, support, voter); + } +} diff --git a/examples/simple/test/BadElections.t.sol b/examples/simple/test/BadElections.t.sol new file mode 100644 index 00000000..5c5ed196 --- /dev/null +++ b/examples/simple/test/BadElections.t.sol @@ -0,0 +1,60 @@ +// SPDX-License-Identifier: AGPL-3.0 +pragma solidity >=0.8.0 <0.9.0; + +import "forge-std/Test.sol"; + +import {SymTest} from "halmos-cheatcodes/SymTest.sol"; + +import {BadElections} from "src/BadElections.sol"; + +contract BadElectionsTest is SymTest, Test { + BadElections elections; + + function setUp() public { + elections = new BadElections(); + } + + /// The output will look something like this: + /// + /// Running 1 tests for test/BadElections.t.sol:BadElectionsTest + /// Counterexample: + /// halmos_fakeSig_bytes_01 = 0x00000000000000000000000000000000000000000000000000000000000000003fffffffffffffffffffffffffffffff5d576e7357a4501ddfe92f46681b20a100 (65 bytes) + /// p_proposalId_uint256 = 0x0000000000000000000000000000000000000000000000000000000000000000 (0) + /// [FAIL] check_canNotVoteTwice(uint256) (paths: 7, time: 0.63s, bounds: []) + /// + /// the counterexample values are not meaningful, but examining the trace shows + /// that halmos found a signature s.t. the voter can vote twice on the same proposal, + /// and the final vote count is 2 + function check_canNotVoteTwice(uint256 proposalId) public { + // setup + bool support = true; + (address voter, uint256 privateKey) = makeAddrAndKey("voter"); + + bytes32 sigDigest = keccak256(abi.encode(proposalId, support, voter)); + (uint8 v, bytes32 r, bytes32 s) = vm.sign(privateKey, sigDigest); + bytes memory signature = abi.encodePacked(r, s, v); + + // we start with no vote + assertEq(elections.votesFor(proposalId), 0); + + // when we cast the vote + elections.vote(proposalId, support, voter, signature); + + // then the vote count increases + assertEq(elections.votesFor(proposalId), 1); + + // when we vote again with the same signature, it reverts + try elections.vote(proposalId, support, voter, signature) { + assert(false); + } catch { + // expected + } + + // when the same voter votes with a different signature + elections.vote(proposalId, support, voter, svm.createBytes(65, "fakeSig")); + + // then the vote count remains unchanged + // @note spoiler alert: it does not + assertEq(elections.votesFor(proposalId), 1); + } +} diff --git a/src/halmos/cheatcodes.py b/src/halmos/cheatcodes.py index 2e430786..8d31f314 100644 --- a/src/halmos/cheatcodes.py +++ b/src/halmos/cheatcodes.py @@ -521,6 +521,16 @@ def handle(sevm, ex, arg: BitVec) -> BitVec: # associate the new signature with the private key and digest known_sigs[(key, digest)] = (v, r, s) + # constrain values to their expected ranges + in_range = And( + Or(v == 27, v == 28), + ULT(0, r), + ULT(r, secp256k1n), + ULT(0, s), + ULT(s, secp256k1n), + ) + ex.path.append(in_range) + # explicitly model malleability recover = f_ecrecover(digest, v, r, s) recover_malleable = f_ecrecover(digest, v ^ 1, r, secp256k1n - s) diff --git a/src/halmos/utils.py b/src/halmos/utils.py index 2ff0a317..55687568 100644 --- a/src/halmos/utils.py +++ b/src/halmos/utils.py @@ -182,8 +182,13 @@ def extract_string_argument(calldata: BitVecRef, arg_idx: int): 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: +def extract_bytes( + data: Optional[BitVecRef], byte_offset: int, size_bytes: int +) -> BitVecRef: """Extract bytes from calldata. Zero-pad if out of bounds.""" + if data is None: + return BitVecVal(0, size_bytes * 8) + n = data.size() if n % 8 != 0: raise ValueError(n) diff --git a/tests/expected/all.json b/tests/expected/all.json index cbba7ea4..c6e2f66f 100644 --- a/tests/expected/all.json +++ b/tests/expected/all.json @@ -1486,6 +1486,15 @@ "time": null, "num_bounded_loops": null }, + { + "name": "check_ecrecover_eip2098CompactSignatures(uint256,bytes32)", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, { "name": "check_ecrecover_explicitMalleability(uint256,bytes32)", "exitcode": 0, @@ -1710,6 +1719,24 @@ "num_paths": null, "time": null, "num_bounded_loops": null + }, + { + "name": "check_vmsign_tryRecover(uint256,bytes32)", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_vmsign_valuesInExpectedRange(uint256,bytes32)", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null } ], "test/SmolWETH.t.sol:SmolWETHTest": [ diff --git a/tests/regression/test/Signature.t.sol b/tests/regression/test/Signature.t.sol index 600f64ae..ef09c414 100644 --- a/tests/regression/test/Signature.t.sol +++ b/tests/regression/test/Signature.t.sol @@ -127,6 +127,19 @@ contract SignatureTest is SymTest, Test { assertNotEq(addr, address(0x42)); } + function check_vmsign_valuesInExpectedRange( + uint256 privateKey, + bytes32 digest + ) public { + (uint8 v, bytes32 r, bytes32 s) = vm.sign(privateKey, digest); + + assert(v == 27 || v == 28); + assertGt(uint256(r), 0); + assertLt(uint256(r), secp256k1n); + assertGt(uint256(s), 0); + assertLt(uint256(s), secp256k1n); + } + function check_vmsign_consistent( uint256 privateKey, bytes32 digest @@ -180,6 +193,17 @@ contract SignatureTest is SymTest, Test { assertNotEq(r1, r2); } + /// FIXME: this should pass, but it doesn't because we always return 32 bytes + // function check_ecrecover_invalidCallReturnsNothing() public { + // uint256 returnDataSize; + // assembly { + // let succ := call(gas(), ECRECOVER_PRECOMPILE, 0, 0, 0, 0, 0) + // returnDataSize := returndatasize() + // } + + // assertEq(returnDataSize, 0); + // } + function check_vmsign_ecrecover_e2e_recoveredMatches( uint256 privateKey, bytes32 digest @@ -220,6 +244,27 @@ contract SignatureTest is SymTest, Test { assertNotEq(ecrecover(digest, v, r, s), ecrecover(digest, otherV, otherR, otherS)); } + function check_vmsign_tryRecover( + uint256 privateKey, + bytes32 digest + ) public { + (uint8 v, bytes32 r, bytes32 s) = vm.sign(privateKey, digest); + bytes memory sig = abi.encodePacked(r, s, v); + address originalAddr = vm.addr(privateKey); + + // we don't want ecrecover to return address(0), it would indicate an error + vm.assume(originalAddr != address(0)); + + (address recovered, ECDSA.RecoverError error, ) = ECDSA.tryRecover(digest, sig); + if (error == ECDSA.RecoverError.InvalidSignatureS) { + // tryRecover rejects s values in the high half order + assertGt(uint256(s), secp256k1n / 2); + } else { + assertEq(uint256(error), uint256(ECDSA.RecoverError.NoError)); + assertEq(recovered, originalAddr); + } + } + function check_ecrecover_explicitMalleability( uint256 privateKey, bytes32 digest @@ -294,6 +339,25 @@ contract SignatureTest is SymTest, Test { assertEq(ecrecover(digest, v2, r2, s2), vm.addr(privateKey2)); } + function check_ecrecover_eip2098CompactSignatures( + uint256 privateKey, + bytes32 digest + ) public { + address addr = vm.addr(privateKey); + (uint8 v, bytes32 r, bytes32 s) = vm.sign(privateKey, digest); + + // assume s is in the lower half order + vm.assume(uint256(s) < secp256k1n / 2); + + // convert to compact format + uint8 yParity = v - 27; + bytes32 vs = bytes32(((uint256(yParity) << 255) | uint256(s))); + + // check that the compact signature can be verified + address recovered = ECDSA.recover(digest, r, vs); + assertEq(recovered, addr); + } + function check_makeAddrAndKey_consistent_symbolic() public { string memory keyName = svm.createString(32, "keyName"); (address addr, uint256 key) = makeAddrAndKey(keyName); From 4f536c7d53a171882b01ae99925448a7cefdf395 Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Tue, 26 Mar 2024 14:57:57 -0700 Subject: [PATCH 4/7] test: add expected output for new test (#263) --- tests/expected/simple.json | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/tests/expected/simple.json b/tests/expected/simple.json index e1e2e1d7..673d8ce0 100644 --- a/tests/expected/simple.json +++ b/tests/expected/simple.json @@ -1,6 +1,17 @@ { "exitcode": 1, "test_results": { + "test/BadElections.t.sol:BadElectionsTest": [ + { + "name": "check_canNotVoteTwice(uint256)", + "exitcode": 1, + "num_models": 1, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + } + ], "test/Fork.t.sol:CounterForkTest": [ { "name": "check_invariant(address)", From c2d192651e7973fdcab22baf210821d3d342d0e7 Mon Sep 17 00:00:00 2001 From: karmacoma Date: Tue, 26 Mar 2024 20:39:58 -0700 Subject: [PATCH 5/7] fix: vm.etch(addr, "") used to raise an exception (#264) --- src/halmos/cheatcodes.py | 9 +++++---- tests/expected/all.json | 9 +++++++++ tests/regression/test/Foundry.t.sol | 5 +++++ 3 files changed, 19 insertions(+), 4 deletions(-) diff --git a/src/halmos/cheatcodes.py b/src/halmos/cheatcodes.py index 8d31f314..235dd9b3 100644 --- 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 index c6e2f66f..dd4fe9a3 100644 --- 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 index 556d4d3d..3cb08f44 100644 --- 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 { From f868681585a10b8b2b7c80e3669d9d50a9389552 Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Thu, 28 Mar 2024 17:20:40 -0700 Subject: [PATCH 6/7] docs: update README.md (#268) --- README.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 6a24aaf2..11190b1c 100644 --- a/README.md +++ b/README.md @@ -41,7 +41,9 @@ Refer to the [getting started guide](docs/getting-started.md) and the [examples] ## Contributing -Refer to the [contributing guidelines](CONTRIBUTING.md). +Refer to the [contributing guidelines](CONTRIBUTING.md), and explore the list of issues labeled ["good first issue" or "help wanted."][issues] + +[issues]: ## Disclaimer From 3e160f54ce141cce81dbd6bd51ce10d452f1a6c8 Mon Sep 17 00:00:00 2001 From: karmacoma Date: Tue, 9 Apr 2024 17:38:44 -0700 Subject: [PATCH 7/7] feat: --solver-command lets user replace z3 invocations This removes: - `--solver-subprocess` - `--solver-subprocess-command` - `--solver-fresh` (was unused AFAICT) This adds: - `--solver-command` with no default (meaning we run z3 in-process) - some prints about where SMT files are generated - auto-dumping of SMT files when invoking an external solver - a very crude way to determine if the external solver generated a valid model (instead of assuming it is valid, so that we still benefit from refinement) Before: ```sh $ halmos --root examples/simple --contract VaultTest --function check_mint -vvv --statistics [...] [FAIL] check_mint(uint256) (paths: 8, time: 282.15s (paths: 0.45s, models: 281.70s), bounds: []) ``` After: ```sh $ halmos --root examples/simple --contract VaultTest --function check_mint -vvv --statistics --solver-command="bitwuzla -m" [...] [FAIL] check_mint(uint256) (paths: 8, time: 19.69s (paths: 0.46s, models: 19.22s), bounds: []) ``` --- src/halmos/__main__.py | 99 ++++++++++++++++++++++-------------------- src/halmos/parser.py | 15 +------ 2 files changed, 55 insertions(+), 59 deletions(-) diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py index ed5b3155..45c8331f 100644 --- a/src/halmos/__main__.py +++ b/src/halmos/__main__.py @@ -1017,25 +1017,52 @@ def copy_model(model: Model) -> Dict: def solve( query: str, args: Namespace, dump_filename: Optional[str] = None ) -> Tuple[CheckSatResult, Model]: - if dump_filename: + if args.dump_smt_queries or args.solver_command: + if not dump_filename: + dump_filename = f"/tmp/{uuid.uuid4().hex}.smt2" + with open(dump_filename, "w") as f: + print(f"Writing SMT query to {dump_filename}") f.write("(set-logic QF_AUFBV)\n") f.write(query) f.write("(get-model)\n") - solver = mk_solver(args, ctx=Context(), assertion=True) - solver.from_string(query) - result = solver.check() - model = copy_model(solver.model()) if result == sat else None - return result, model + if args.solver_command: + if args.verbose >= 1: + print(f" Checking with external solver process") + print(f" {args.solver_command} {dump_filename} >{dump_filename}.out") + + cmd = args.solver_command.split() + [dump_filename] + res_str = subprocess.run(cmd, capture_output=True, text=True).stdout.strip() + res_str_head = res_str.split("\n", 1)[0] + + with open(f"{dump_filename}.out", "w") as f: + f.write(res_str) + + if args.verbose >= 1: + print(f" {res_str_head}") + + if res_str_head == "unsat": + return unsat, None + elif res_str_head == "sat": + return sat, f"{dump_filename}.out" + else: + return unknown, None + + else: + solver = mk_solver(args, ctx=Context(), assertion=True) + solver.from_string(query) + result = solver.check() + model = copy_model(solver.model()) if result == sat else None + return result, model def gen_model_from_sexpr(fn_args: GenModelArgs) -> ModelWithContext: args, idx, sexpr = fn_args.args, fn_args.idx, fn_args.sexpr - dump_dirname = fn_args.dump_dirname if args.dump_smt_queries else None - dump_filename = f"{dump_dirname}/{idx+1}.smt2" if dump_dirname else None - if dump_dirname: + dump_dirname = fn_args.dump_dirname + dump_filename = f"{dump_dirname}/{idx+1}.smt2" + if args.dump_smt_queries or args.solver_command: if not os.path.isdir(dump_dirname): os.makedirs(dump_dirname) print(f"Generating SMT queries in {dump_dirname}") @@ -1049,39 +1076,8 @@ def gen_model_from_sexpr(fn_args: GenModelArgs) -> ModelWithContext: if args.verbose >= 1: print(f" Checking again with refinement") - res, model = solve( - refine(sexpr), - args, - dump_filename.replace(".smt2", ".refined.smt2") if dump_filename else None, - ) - - if args.solver_subprocess and is_unknown(res, model): - fname = f"/tmp/{uuid.uuid4().hex}.smt2" - - if args.verbose >= 1: - print(f" Checking again in an external process") - print(f" {args.solver_subprocess_command} {fname} >{fname}.out") - - query = refine(sexpr) - with open(fname, "w") as f: - f.write("(set-logic QF_AUFBV)\n") - f.write(query) - - cmd = args.solver_subprocess_command.split() + [fname] - res_str = subprocess.run(cmd, capture_output=True, text=True).stdout.strip() - res_str_head = res_str.split("\n", 1)[0] - - with open(f"{fname}.out", "w") as f: - f.write(res_str) - - if args.verbose >= 1: - print(f" {res_str_head}") - - if res_str_head == "unsat": - res = unsat - elif res_str_head == "sat": - res = sat - model = f"{fname}.out" + refined_filename = dump_filename.replace(".smt2", ".refined.smt2") + res, model = solve(refine(sexpr), args, refined_filename) return package_result(model, idx, res, args) @@ -1140,10 +1136,21 @@ def package_result( def is_model_valid(model: AnyModel) -> bool: # TODO: evaluate the path condition against the given model after excluding evm_* symbols, # since the evm_* symbols may still appear in valid models. - for decl in model: - if str(decl).startswith("evm_"): - return False - return True + + # model is a filename, containing solver output + if isinstance(model, str): + with open(model, "r") as f: + for line in f: + if "evm_" in line: + return False + return True + + # z3 model object + else: + for decl in model: + if str(decl).startswith("evm_"): + return False + return True def to_str_model(model: Model, print_full_model: bool) -> StrModel: diff --git a/src/halmos/parser.py b/src/halmos/parser.py index db23075b..faff9f97 100644 --- a/src/halmos/parser.py +++ b/src/halmos/parser.py @@ -214,20 +214,9 @@ def mk_arg_parser() -> argparse.ArgumentParser: help="set memory limit (in megabytes) for the solver; 0 means no limit (default: %(default)s)", ) group_solver.add_argument( - "--solver-fresh", - action="store_true", - help="run an extra solver with a fresh state for unknown", - ) - group_solver.add_argument( - "--solver-subprocess", - action="store_true", - help="run an extra solver in subprocess for unknown", - ) - group_solver.add_argument( - "--solver-subprocess-command", + "--solver-command", metavar="COMMAND", - default="z3 -model", - help="use the given command for the subprocess solver (requires --solver-subprocess) (default: '%(default)s')", + help="use the given command when invoking the solver, e.g. `z3 -model`", ) group_solver.add_argument( "--solver-parallel",