fix: revert state (#143)

a16z · Jul 25, 2023 · 24a56ea · 24a56ea
1 parent a740005
commit 24a56ea
Show file tree

Hide file tree

Showing 3 changed files with 76 additions and 4 deletions.
diff --git 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
@@ -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
@@ -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);
+        }
+    }
 }