perf: early exit for fail()

src/halmos/exceptions.py

@@ -8,18 +8,46 @@
 """
 
 
-class InfeasiblePath(Exception):
+class PathEndingException(Exception):
+    """
+    Base class for any exception that should stop the current path exploration.
+
+    Stopping path exploration means stopping not only the current EVM context but also its parent contexts if any.
+    """
+
     pass
 
 
-class HalmosException(Exception):
+class HalmosException(PathEndingException):
+    """
+    Base class for unexpected internal errors happening during a test run.
+    Inherits from RunEndingException because it should stop further path exploration.
+    """
+
     pass
 
 
 class NotConcreteError(HalmosException):
     pass
 
 
+class InfeasiblePath(PathEndingException):
+    """
+    Raise when the current path condition turns out to be infeasible.
+    """
+
+    pass
+
+
+class FailCheatcode(PathEndingException):
+    """
+    Raised when invoking DSTest's fail() pseudo-cheatcode.
+    Inherits from RunEndingException because it should stop further path exploration.
+    """
+
+    pass
+
+
 class EvmException(Exception):
     """
     Base class for all EVM exceptions.
@@ -136,14 +164,6 @@ class InvalidContractPrefix(ExceptionalHalt):
     pass
 
 
-class FailCheatcode(ExceptionalHalt):
-    """
-    Raised when invoking hevm's vm.fail() cheatcode
-    """
-
-    pass
-
-
 class AddressCollision(ExceptionalHalt):
     """
     Raised when trying to deploy into a non-empty address

src/halmos/sevm.py

@@ -2544,6 +2544,12 @@ def finalize(ex: Exec):
                 yield from finalize(ex)
                 continue
 
+            except FailCheatcode as err:
+                # return data shouldn't be None, as it is considered being stuck
+                ex.halt(data=ByteVec(), error=err)
+                yield ex  # early exit; do not call finalize()
+                continue
+
     def mk_exec(
         self,
         #

tests/expected/all.json

@@ -427,7 +427,7 @@
             {
                 "name": "check_call1_fail(uint256)",
                 "exitcode": 1,
-                "num_models": 2,
+                "num_models": 1,
                 "models": null,
                 "num_paths": null,
                 "time": null,
@@ -766,6 +766,28 @@
                 "num_bounded_loops": null
             }
         ],
+        "test/Foundry.t.sol:DeepFailer": [
+            {
+                "name": "check_fail_cheatcode()",
+                "exitcode": 1,
+                "num_models": 1,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            }
+        ],
+        "test/Foundry.t.sol:EarlyFailTest": [
+            {
+                "name": "check_early_fail_cheatcode(uint256)",
+                "exitcode": 1,
+                "num_models": 1,
+                "models": null,
+                "num_paths": null,
+                "time": null,
+                "num_bounded_loops": null
+            }
+        ],
         "test/Foundry.t.sol:FoundryTest": [
             {
                 "name": "check_assume(uint256)",

tests/regression/test/Foundry.t.sol

@@ -16,11 +16,29 @@ contract DeepFailer is Test {
         }
     }
 
-    function test_fail_cheatcode() public {
+    function check_fail_cheatcode() public {
         DeepFailer(address(this)).do_test(0);
     }
 }
 
+contract EarlyFailTest is Test {
+    function do_fail() external {
+        fail();
+    }
+
+    function check_early_fail_cheatcode(uint x) public {
+        // we want `fail()` to happen in a nested context,
+        // to test that it ends not just the current context but the whole run
+        address(this).call(abi.encodeWithSelector(this.do_fail.selector, ""));
+
+        // this shouldn't be reached due to the early fail() semantics.
+        // if this assertion is executed, two counterexamples will be generated:
+        // - counterexample caused by fail(): x > 0
+        // - counterexample caused by assert(x > 0): x == 0
+        assert(x > 0);
+    }
+}
+
 contract FoundryTest is Test {
     /* TODO: support checkFail prefix
     function checkFail() public {