diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py index 5ab29f80..69acb475 100644 --- a/src/halmos/sevm.py +++ b/src/halmos/sevm.py @@ -1261,6 +1261,11 @@ def call( caller = ex.prank.lookup(ex.this, to) + orig_code = ex.code.copy() + orig_storage = deepcopy(ex.storage) + orig_balance = deepcopy(ex.balance) + orig_log = deepcopy(ex.log) + if not (is_bv_value(fund) and fund.as_long() == 0): ex.balance_update( caller, self.arith(ex, EVM.SUB, ex.balance_of(caller), fund) @@ -1347,6 +1352,12 @@ def call_known() -> None: else: new_ex.st.push(con(0)) + # revert network states + new_ex.code = orig_code + new_ex.storage = orig_storage + new_ex.balance = orig_balance + new_ex.log = orig_log + # add to worklist even if it reverted during the external call new_ex.next_pc() stack.append((new_ex, step_id)) diff --git a/tests/expected/all.json b/tests/expected/all.json index 4257d77b..02cd1f4c 100644 --- a/tests/expected/all.json +++ b/tests/expected/all.json @@ -793,8 +793,8 @@ "test/Revert.t.sol:CTest": [ { "name": "check_Revert1(uint256)", - "exitcode": 1, - "num_models": 1, + "exitcode": 0, + "num_models": 0, "num_paths": null, "time": null, "num_bounded_loops": null @@ -806,6 +806,22 @@ "num_paths": null, "time": null, "num_bounded_loops": null + }, + { + "name": "check_RevertBalance(bool,uint256)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null + }, + { + "name": "check_RevertCode(address)", + "exitcode": 0, + "num_models": 0, + "num_paths": null, + "time": null, + "num_bounded_loops": null } ], "test/Send.t.sol:SendTest": [ diff --git a/tests/test/Revert.t.sol b/tests/test/Revert.t.sol index ed82b2f8..f72f3e1a 100644 --- a/tests/test/Revert.t.sol +++ b/tests/test/Revert.t.sol @@ -3,6 +3,10 @@ pragma solidity >=0.8.0 <0.9.0; // from https://github.com/a16z/halmos/issues/109 +import "forge-std/Test.sol"; + +contract A { } + contract C { uint256 public num; @@ -15,9 +19,18 @@ contract C { revert("blah"); num = x; } + + function deposit(bool paused) public payable { + if (paused) revert("paused"); + } + + function create() public { + A a = new A(); + revert(string(abi.encode(a))); + } } -contract CTest { +contract CTest is Test { C c; function setUp() public { @@ -28,7 +41,7 @@ contract CTest { require(x != 0); (bool result, ) = address(c).call(abi.encodeWithSignature("set1(uint256)", x)); assert(!result); - assert(c.num() != x); // fail // TODO: fix reverting semantics + assert(c.num() != x); } function check_Revert2(uint256 x) public { @@ -37,4 +50,36 @@ contract CTest { assert(!result); assert(c.num() != x); } + + function check_RevertBalance(bool paused, uint256 amount) public { + vm.deal(address(this), amount); + vm.deal(address(c), 0); + + (bool result,) = address(c).call{value: amount}(abi.encodeWithSignature("deposit(bool)", paused)); + + if (result) { + assert(!paused); + assert(address(this).balance == 0); + assert(address(c).balance == amount); + } else { + assert(paused); + assert(address(this).balance == amount); + assert(address(c).balance == 0); + } + } + + function codesize(address x) internal view returns (uint256 size) { + assembly { size := extcodesize(x) } + } + + function check_RevertCode(address x) public { + uint256 oldSize = codesize(x); + try c.create() { + } catch Error(string memory s) { + address a = abi.decode(bytes(s), (address)); + uint256 size = codesize(a); + vm.assume(a == x); + assert(size == oldSize); + } + } }