feat: introduce other failure modes (#237)

.github/workflows/test-external.yml

@@ -67,5 +67,5 @@ jobs:
         run: python -m pip install -e ./halmos
 
       - name: Test external repo
-        run: ${{ matrix.cmd }} -v -st --error-unknown --solver-timeout-assertion 0 --solver-threads 2
+        run: ${{ matrix.cmd }} -v -st --solver-timeout-assertion 0 --solver-threads 2
         working-directory: ${{ matrix.dir }}

.github/workflows/test-ffi.yml

@@ -38,4 +38,4 @@ jobs:
         run: python -m pip install -e .
 
       - name: Run pytest
-        run: pytest -v tests/test_halmos.py -k ${{ matrix.testname }} --halmos-options="--ffi -v -st --error-unknown --solver-timeout-assertion 0"
+        run: pytest -v tests/test_halmos.py -k ${{ matrix.testname }} --halmos-options="--ffi -v -st --solver-timeout-assertion 0"

.github/workflows/test-long.yml

@@ -42,4 +42,4 @@ jobs:
         run: python -m pip install -e .
 
       - name: Run pytest
-        run: pytest -x -v tests/test_halmos.py -k ${{ matrix.testname }} --halmos-options="-v -st --error-unknown --solver-timeout-assertion 0 --solver-threads 2" -s --log-cli-level=
+        run: pytest -x -v tests/test_halmos.py -k ${{ matrix.testname }} --halmos-options="-v -st --solver-timeout-assertion 0 --solver-threads 2" -s --log-cli-level=

.github/workflows/test.yml

@@ -40,4 +40,4 @@ jobs:
         run: python -m pip install -e .
 
       - name: Run pytest
-        run: pytest -v -k "not long and not ffi" --ignore=tests/lib --halmos-options="-v -st --error-unknown ${{ matrix.parallel }} --storage-layout ${{ matrix.storage-layout }} --solver-timeout-assertion 0"
+        run: pytest -v -k "not long and not ffi" --ignore=tests/lib --halmos-options="-v -st ${{ matrix.parallel }} --storage-layout ${{ matrix.storage-layout }} --solver-timeout-assertion 0"

src/halmos/__main__.py

@@ -13,6 +13,8 @@
 from argparse import Namespace
 from dataclasses import dataclass, asdict
 from importlib import metadata
+from enum import Enum
+from collections import Counter
 
 from concurrent.futures import ProcessPoolExecutor, ThreadPoolExecutor
 
@@ -541,14 +543,23 @@ class ModelWithContext:
 @dataclass(frozen=True)
 class TestResult:
     name: str  # test function name
-    exitcode: int  # 0: passed, 1: failed, 2: setup failed, ...
+    exitcode: int
     num_models: int = None
     models: List[ModelWithContext] = None
     num_paths: Tuple[int, int, int] = None  # number of paths: [total, success, blocked]
     time: Tuple[int, int, int] = None  # time: [total, paths, models]
     num_bounded_loops: int = None  # number of incomplete loops
 
 
+class Exitcode(Enum):
+    PASS = 0
+    COUNTEREXAMPLE = 1
+    TIMEOUT = 2
+    STUCK = 3
+    REVERT_ALL = 4
+    EXCEPTION = 5
+
+
 def is_global_fail_set(context: CallContext) -> bool:
     hevm_fail = isinstance(context.output.error, FailCheatcode)
     return hevm_fail or any(is_global_fail_set(x) for x in context.subcalls())
@@ -743,18 +754,33 @@ def future_callback(future_model):
     else:
         thread_pool.shutdown(wait=True)
 
-    no_counterexample = all(m.model is None for m in models)
-    passed = no_counterexample and normal > 0 and len(stuck) == 0
-    if args.error_unknown:
-        passed = passed and all(m.result == unsat for m in models)
-    passfail = color_good("[PASS]") if passed else color_warn("[FAIL]")
+    counter = Counter(str(m.result) for m in models)
+    if counter["sat"] > 0:
+        passfail = color_warn("[FAIL]")
+        exitcode = Exitcode.COUNTEREXAMPLE.value
+    elif counter["unknown"] > 0:
+        passfail = color_warn("[TIMEOUT]")
+        exitcode = Exitcode.TIMEOUT.value
+    elif len(stuck) > 0:
+        passfail = color_warn("[ERROR]")
+        exitcode = Exitcode.STUCK.value
+    elif normal == 0:
+        passfail = color_warn("[ERROR]")
+        exitcode = Exitcode.REVERT_ALL.value
+        warn(
+            REVERT_ALL,
+            f"{funsig}: all paths have been reverted; the setup state or inputs may have been too restrictive.",
+        )
+    else:
+        passfail = color_good("[PASS]")
+        exitcode = Exitcode.PASS.value
 
     timer.stop()
     time_info = timer.report(include_subtimers=args.statistics)
 
     # print result
     print(
-        f"{passfail} {funsig} (paths: {normal}/{len(result_exs)}, {time_info}, bounds: [{', '.join(dyn_param_size)}])"
+        f"{passfail} {funsig} (paths: {len(result_exs)}, {time_info}, bounds: [{', '.join(dyn_param_size)}])"
     )
 
     for idx, ex, err in stuck:
@@ -791,7 +817,6 @@ def future_callback(future_model):
             json.dump(steps, json_file)
 
     # return test result
-    exitcode = 0 if passed else 1
     if args.minimal_json_output:
         return TestResult(funsig, exitcode, len(counterexamples))
     else:
@@ -844,11 +869,11 @@ def setup_and_run_single(fn_args: SetupAndRunSingleArgs) -> List[TestResult]:
             fn_args.args,
         )
     except Exception as err:
-        print(f"{yellow('[SKIP]')} {fn_args.fun_info.sig}")
+        print(f"{color_warn('[ERROR]')} {fn_args.fun_info.sig}")
         error(f"{type(err).__name__}: {err}")
         if args.debug:
             traceback.print_exc()
-        return [TestResult(fn_args.fun_info.sig, 2)]
+        return [TestResult(fn_args.fun_info.sig, Exitcode.EXCEPTION.value)]
 
     return [test_result]
 
@@ -960,11 +985,11 @@ def run_sequential(run_args: RunArgs) -> List[TestResult]:
             )
             test_result = run(setup_ex, run_args.abi, fun_info, extended_args)
         except Exception as err:
-            print(f"{color_warn('[SKIP]')} {funsig}")
+            print(f"{color_warn('[ERROR]')} {funsig}")
             print(color_warn(f"{type(err).__name__}: {err}"))
             if args.debug:
                 traceback.print_exc()
-            test_results.append(TestResult(funsig, 2))
+            test_results.append(TestResult(funsig, Exitcode.EXCEPTION.value))
             continue
 
         test_results.append(test_result)

src/halmos/parser.py

@@ -145,11 +145,6 @@ def mk_arg_parser() -> argparse.ArgumentParser:
         action="store_true",
         help="print full counterexample model",
     )
-    group_debug.add_argument(
-        "--error-unknown",
-        action="store_true",
-        help="turn unknown counterexample warnings to errors",
-    )
     group_debug.add_argument(
         "--early-exit",
         action="store_true",

src/halmos/warnings.py

@@ -23,6 +23,7 @@ def url(self) -> str:
 INTERNAL_ERROR = ErrorCode("internal-error")
 UNSUPPORTED_OPCODE = ErrorCode("unsupported-opcode")
 LIBRARY_PLACEHOLDER = ErrorCode("library-placeholder")
+REVERT_ALL = ErrorCode("revert-all")
 
 LOOP_BOUND = ErrorCode("loop-bound")
 UNINTERPRETED_UNKNOWN_CALLS = ErrorCode("uninterpreted-unknown-calls")

tests/expected/all.json

@@ -408,7 +408,7 @@
             },
             {
                 "name": "check_call0_halmos_exception()",
-                "exitcode": 1,
+                "exitcode": 3,
                 "num_models": 0,
                 "models": null,
                 "num_paths": null,
@@ -435,7 +435,7 @@
             },
             {
                 "name": "check_call1_halmos_exception(uint256)",
-                "exitcode": 1,
+                "exitcode": 3,
                 "num_models": 0,
                 "models": null,
                 "num_paths": null,
@@ -462,7 +462,7 @@
             },
             {
                 "name": "check_create_halmos_exception()",
-                "exitcode": 1,
+                "exitcode": 3,
                 "num_models": 0,
                 "models": null,
                 "num_paths": null,
@@ -693,7 +693,7 @@
             },
             {
                 "name": "check_create2_collision_basic(uint256,uint256,bytes32)",
-                "exitcode": 1,
+                "exitcode": 4,
                 "num_models": 0,
                 "models": null,
                 "num_paths": null,
@@ -827,7 +827,7 @@
         "test/HalmosCheatCode.t.sol:HalmosCheatCodeTest": [
             {
                 "name": "check_FailUnknownCheatcode()",
-                "exitcode": 1,
+                "exitcode": 3,
                 "num_models": 0,
                 "models": null,
                 "num_paths": null,
@@ -1755,7 +1755,7 @@
             },
             {
                 "name": "check_unknown_not_allowed(address)",
-                "exitcode": 1,
+                "exitcode": 3,
                 "num_models": 0,
                 "models": null,
                 "num_paths": null,
@@ -1800,7 +1800,7 @@
             },
             {
                 "name": "check_unknown_send_fail(address)",
-                "exitcode": 1,
+                "exitcode": 4,
                 "num_models": 0,
                 "models": null,
                 "num_paths": null,
@@ -1820,7 +1820,7 @@
         "test/UnsupportedOpcode.t.sol:X": [
             {
                 "name": "check_unsupported_opcode()",
-                "exitcode": 1,
+                "exitcode": 3,
                 "num_models": 0,
                 "models": null,
                 "num_paths": null,
@@ -1831,7 +1831,7 @@
         "test/UnsupportedOpcode.t.sol:Y": [
             {
                 "name": "check_unsupported_opcode()",
-                "exitcode": 1,
+                "exitcode": 3,
                 "num_models": 0,
                 "models": null,
                 "num_paths": null,
@@ -1842,7 +1842,7 @@
         "test/UnsupportedOpcode.t.sol:Z": [
             {
                 "name": "check_unsupported_opcode()",
-                "exitcode": 1,
+                "exitcode": 3,
                 "num_models": 0,
                 "models": null,
                 "num_paths": null,

tests/expected/ffi.json

@@ -4,7 +4,7 @@
         "test/Ffi.t.sol:FfiTest": [
             {
                 "name": "check_Failure()",
-                "exitcode": 2,
+                "exitcode": 5,
                 "num_models": null,
                 "models": null,
                 "num_paths": null,

tests/expected/simple.json

@@ -82,7 +82,7 @@
         "test/Vault.t.sol:VaultTest": [
             {
                 "name": "check_deposit(uint256)",
-                "exitcode": 1,
+                "exitcode": 2,
                 "num_models": 0,
                 "models": null,
                 "num_paths": null,

tests/expected/solver.json

@@ -13,7 +13,7 @@
             },
             {
                 "name": "check_deposit(uint256,uint256,uint256)",
-                "exitcode": 1,
+                "exitcode": 2,
                 "num_models": 0,
                 "models": null,
                 "num_paths": null,