From 24a56ea77612a763df2b01a0cbd9011804302ba3 Mon Sep 17 00:00:00 2001
From: Daejun Park <daejunpark@gmail.com>
Date: Mon, 24 Jul 2023 17:58:00 -0700
Subject: [PATCH] fix: revert state (#143)

---
 src/halmos/sevm.py      | 11 +++++++++
 tests/expected/all.json | 20 +++++++++++++++--
 tests/test/Revert.t.sol | 49 +++++++++++++++++++++++++++++++++++++++--
 3 files changed, 76 insertions(+), 4 deletions(-)

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);
+        }
+    }
 }