add symbolic revert test

a16z · Aug 21, 2024 · afd5c11 · afd5c11
1 parent af3df48
commit afd5c11
Show file tree

Hide file tree

Showing 2 changed files with 21 additions and 0 deletions.
diff --git a/tests/expected/all.json b/tests/expected/all.json
@@ -77,6 +77,15 @@
                 "num_paths": null,
                 "time": null,
                 "num_bounded_loops": null
+            },
+            {
+                "name": "check_symbolic_revert(uint256)",
+                "exitcode": 0,
+                "num_models": 0,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
             }
         ],
         "test/Block.t.sol:BlockCheatCodeTest": [

diff --git a/tests/regression/test/AssertTest.t.sol b/tests/regression/test/AssertTest.t.sol
@@ -27,4 +27,16 @@ contract AssertTest is Test {
     function check_fail_propagated() public {
         address(c).call(abi.encodeWithSelector(C.bar.selector, bytes(""))); // fail
     }
+
+    function check_symbolic_revert(uint256 x) public {
+        // reverts with Concat(0x4e487b71, p_x_uint256())
+        // halmos only considers reverts with explicit revert codes so we expect a PASS here
+        // this is really to make sure we handle symbolic reverts gracefully
+        if (x > 0) {
+            bytes memory data = abi.encodeWithSignature("Panic(uint256)", x);
+            assembly {
+                revert(add(data, 0x20), mload(data))
+            }
+        }
+    }
 }