From e46f43a2a45515a30e898a34d931e0d0e18c7869 Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Tue, 27 Aug 2024 11:40:11 -0700 Subject: [PATCH 1/5] fix failed() cheatcode error --- src/halmos/cheatcodes.py | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/src/halmos/cheatcodes.py b/src/halmos/cheatcodes.py index 333cbc1d..3875ee4a 100644 --- a/src/halmos/cheatcodes.py +++ b/src/halmos/cheatcodes.py @@ -354,6 +354,18 @@ class hevm_cheat_code: ) ) + # abi.encodePacked( + # bytes4(keccak256("load(address,bytes32)")), + # abi.encode(HEVM_ADDRESS, bytes32("failed")) + # ) + failed_payload = ByteVec( + bytes.fromhex( + "667f9d70" + + "0000000000000000000000007109709ecfa91a80626ff3989d68f67f5b1dd12d" + + "6661696c65640000000000000000000000000000000000000000000000000000" + ) + ) + # bytes4(keccak256("assume(bool)")) assume_sig: int = 0x4C63E562 @@ -533,6 +545,9 @@ def handle(sevm, ex, arg: ByteVec, stack, step_id) -> ByteVec | None: # vm.load(address,bytes32) elif funsig == hevm_cheat_code.load_sig: + if arg == hevm_cheat_code.failed_payload: + return ByteVec(con(0)) + load_account = uint160(arg.get_word(4)) load_slot = uint256(arg.get_word(36)) load_account_alias = sevm.resolve_address_alias( From 10f85d980232bb022910040b390e8448bfc1cc53 Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Tue, 27 Aug 2024 11:49:02 -0700 Subject: [PATCH 2/5] add test --- src/halmos/cheatcodes.py | 3 +++ tests/regression/test/Foundry.t.sol | 5 +++++ 2 files changed, 8 insertions(+) diff --git a/src/halmos/cheatcodes.py b/src/halmos/cheatcodes.py index 3875ee4a..da904742 100644 --- a/src/halmos/cheatcodes.py +++ b/src/halmos/cheatcodes.py @@ -545,7 +545,10 @@ def handle(sevm, ex, arg: ByteVec, stack, step_id) -> ByteVec | None: # vm.load(address,bytes32) elif funsig == hevm_cheat_code.load_sig: + # vm.load(HEVM_ADDRESS, "failed") is handled separately if arg == hevm_cheat_code.failed_payload: + # since fail(), which triggers vm.store(HEVM_ADDRESS, "failed", 1), halts immediately, (see vm.store() above) + # the "failed" slot is never assigned, thus vm.load(HEVM_ADDRESS, "failed") always return zero at this point return ByteVec(con(0)) load_account = uint160(arg.get_word(4)) diff --git a/tests/regression/test/Foundry.t.sol b/tests/regression/test/Foundry.t.sol index f6d390f4..bc5d2db5 100644 --- a/tests/regression/test/Foundry.t.sol +++ b/tests/regression/test/Foundry.t.sol @@ -37,6 +37,11 @@ contract EarlyFailTest is Test { // - counterexample caused by assert(x > 0): x == 0 assert(x > 0); } + + function check_failed_cheatcode() public { + // since fail() halts immediately, failed() always return true here + assertFalse(failed()); + } } contract FoundryTest is Test { From 03850b34f2a3ab78ab49e895be4eeac406f9d33c Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Tue, 27 Aug 2024 11:53:22 -0700 Subject: [PATCH 3/5] updated test expected --- tests/expected/all.json | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/tests/expected/all.json b/tests/expected/all.json index ac918d8a..f8d5c64d 100644 --- a/tests/expected/all.json +++ b/tests/expected/all.json @@ -1024,6 +1024,15 @@ "num_paths": null, "time": null, "num_bounded_loops": null + }, + { + "name": "check_failed_cheatcode()", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null } ], "test/Foundry.t.sol:FoundryTest": [ From d1a4380398e4a7a63d329e4eb61c8e5afd621bfd Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Tue, 27 Aug 2024 22:12:00 -0700 Subject: [PATCH 4/5] fix: handle the case where resolve_address_alias returns None --- src/halmos/cheatcodes.py | 32 +++++++++------------ tests/expected/all.json | 27 +++++++++++++++++ tests/regression/test/Foundry.t.sol | 2 +- tests/regression/test/HalmosCheatCode.t.sol | 5 ++++ tests/regression/test/Store.t.sol | 10 +++++++ 5 files changed, 57 insertions(+), 19 deletions(-) diff --git a/src/halmos/cheatcodes.py b/src/halmos/cheatcodes.py index da904742..6ababd0c 100644 --- a/src/halmos/cheatcodes.py +++ b/src/halmos/cheatcodes.py @@ -208,6 +208,11 @@ def symbolic_storage(ex, arg, sevm, stack, step_id): account_alias = sevm.resolve_address_alias( ex, account, stack, step_id, branching=False ) + + if account_alias is None: + error_msg = f"enableSymbolicStorage() is not allowed for a nonexistent account: {hexify(account)}" + raise HalmosException(error_msg) + ex.storage[account_alias].symbolic = True @@ -354,18 +359,6 @@ class hevm_cheat_code: ) ) - # abi.encodePacked( - # bytes4(keccak256("load(address,bytes32)")), - # abi.encode(HEVM_ADDRESS, bytes32("failed")) - # ) - failed_payload = ByteVec( - bytes.fromhex( - "667f9d70" - + "0000000000000000000000007109709ecfa91a80626ff3989d68f67f5b1dd12d" - + "6661696c65640000000000000000000000000000000000000000000000000000" - ) - ) - # bytes4(keccak256("assume(bool)")) assume_sig: int = 0x4C63E562 @@ -540,23 +533,26 @@ def handle(sevm, ex, arg: ByteVec, stack, step_id) -> ByteVec | None: ex, store_account, stack, step_id, branching=False ) + if store_account_alias is None: + error_msg = f"vm.store() is not allowed for a nonexistent account: {hexify(store_account)}" + raise HalmosException(error_msg) + sevm.sstore(ex, store_account_alias, store_slot, store_value) return ret # vm.load(address,bytes32) elif funsig == hevm_cheat_code.load_sig: - # vm.load(HEVM_ADDRESS, "failed") is handled separately - if arg == hevm_cheat_code.failed_payload: - # since fail(), which triggers vm.store(HEVM_ADDRESS, "failed", 1), halts immediately, (see vm.store() above) - # the "failed" slot is never assigned, thus vm.load(HEVM_ADDRESS, "failed") always return zero at this point - return ByteVec(con(0)) - load_account = uint160(arg.get_word(4)) load_slot = uint256(arg.get_word(36)) load_account_alias = sevm.resolve_address_alias( ex, load_account, stack, step_id, branching=False ) + if load_account_alias is None: + # since load_account doesn't exist, its storage is empty. + # note: the storage cannot be symbolic, as the symbolic storage cheatcode fails for nonexistent addresses. + return ByteVec(con(0)) + return ByteVec(sevm.sload(ex, load_account_alias, load_slot)) # vm.fee(uint256) diff --git a/tests/expected/all.json b/tests/expected/all.json index f8d5c64d..a86d30fa 100644 --- a/tests/expected/all.json +++ b/tests/expected/all.json @@ -1246,6 +1246,15 @@ "num_paths": null, "time": null, "num_bounded_loops": null + }, + { + "name": "check_enableSymbolicStorage()", + "exitcode": 3, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null } ], "test/Library.t.sol:LibraryTest": [ @@ -3150,6 +3159,15 @@ } ], "test/Store.t.sol:StoreTest": [ + { + "name": "check_load_nonexistent_account(uint256)", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, { "name": "check_store_Array(uint256,uint256)", "exitcode": 0, @@ -3176,6 +3194,15 @@ "num_paths": null, "time": null, "num_bounded_loops": null + }, + { + "name": "check_store_nonexistent_account()", + "exitcode": 3, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null } ], "test/Struct.t.sol:StructTest": [ diff --git a/tests/regression/test/Foundry.t.sol b/tests/regression/test/Foundry.t.sol index bc5d2db5..a3f6d983 100644 --- a/tests/regression/test/Foundry.t.sol +++ b/tests/regression/test/Foundry.t.sol @@ -39,7 +39,7 @@ contract EarlyFailTest is Test { } function check_failed_cheatcode() public { - // since fail() halts immediately, failed() always return true here + // since fail() halts immediately, failed() always returns true here assertFalse(failed()); } } diff --git a/tests/regression/test/HalmosCheatCode.t.sol b/tests/regression/test/HalmosCheatCode.t.sol index 20473d02..bcb594fb 100644 --- a/tests/regression/test/HalmosCheatCode.t.sol +++ b/tests/regression/test/HalmosCheatCode.t.sol @@ -115,6 +115,11 @@ contract HalmosCheatCodeTest is SymTest, Test { // NOTE: the following reverts due to the failure of the nonzero check for extcodesize(svm) // Dummy(address(svm)).foo(); } + + function check_enableSymbolicStorage() public { + // symbolic storage is not allowed for a nonexistent account + svm.enableSymbolicStorage(address(0xdeadbeef)); // HalmosException + } } interface Dummy { diff --git a/tests/regression/test/Store.t.sol b/tests/regression/test/Store.t.sol index db80ac6b..67c5602b 100644 --- a/tests/regression/test/Store.t.sol +++ b/tests/regression/test/Store.t.sol @@ -47,4 +47,14 @@ contract StoreTest is Test { assert(c.a(key) == value); assert(uint(vm.load(address(c), bytes32(uint(keccak256(abi.encode(2))) + key))) == value); } + + function check_store_nonexistent_account() public { + // vm.store() is not allowed for a nonexistent account + vm.store(address(0xdeadbeef), bytes32(0), bytes32(0)); // HalmosException + } + + function check_load_nonexistent_account(uint slot) public { + // vm.load() from nonexistent accounts returns zero + assertEq(vm.load(address(0xdeadbeef), bytes32(slot)), 0); + } } From 714d39c841905bfd09d412abf3bd94c6fdf25818 Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Tue, 27 Aug 2024 22:27:03 -0700 Subject: [PATCH 5/5] add svm.enableSymbolicStorage tests --- tests/expected/all.json | 20 +++++++++++++++++++- tests/regression/test/HalmosCheatCode.t.sol | 20 +++++++++++++++++++- 2 files changed, 38 insertions(+), 2 deletions(-) diff --git a/tests/expected/all.json b/tests/expected/all.json index a86d30fa..236eef58 100644 --- a/tests/expected/all.json +++ b/tests/expected/all.json @@ -1248,13 +1248,31 @@ "num_bounded_loops": null }, { - "name": "check_enableSymbolicStorage()", + "name": "check_enableSymbolicStorage_fail()", + "exitcode": 1, + "num_models": 1, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_enableSymbolicStorage_nonexistent()", "exitcode": 3, "num_models": 0, "models": null, "num_paths": null, "time": null, "num_bounded_loops": null + }, + { + "name": "check_enableSymbolicStorage_pass(uint256)", + "exitcode": 0, + "num_models": 0, + "models": null, + "num_paths": null, + "time": null, + "num_bounded_loops": null } ], "test/Library.t.sol:LibraryTest": [ diff --git a/tests/regression/test/HalmosCheatCode.t.sol b/tests/regression/test/HalmosCheatCode.t.sol index bcb594fb..1b510c15 100644 --- a/tests/regression/test/HalmosCheatCode.t.sol +++ b/tests/regression/test/HalmosCheatCode.t.sol @@ -116,7 +116,25 @@ contract HalmosCheatCodeTest is SymTest, Test { // Dummy(address(svm)).foo(); } - function check_enableSymbolicStorage() public { + function check_enableSymbolicStorage_pass(uint val) public { + address dummy = address(new Beep()); + // initial value is zero + assertEq(vm.load(dummy, bytes32(0)), 0); + + vm.store(dummy, bytes32(0), bytes32(val)); + svm.enableSymbolicStorage(dummy); + // enableSymbolicStorage updates only uninitialized slots + assertEq(vm.load(dummy, bytes32(0)), bytes32(val)); + } + + function check_enableSymbolicStorage_fail() public { + address dummy = address(new Beep()); + svm.enableSymbolicStorage(dummy); + // storage slots have been initialized with a symbolic value + assertEq(vm.load(dummy, bytes32(0)), 0); // fail + } + + function check_enableSymbolicStorage_nonexistent() public { // symbolic storage is not allowed for a nonexistent account svm.enableSymbolicStorage(address(0xdeadbeef)); // HalmosException }