create solver_output in case of errors too (#570)

Author: 0xkarmacoma

src/halmos/__main__.py

@@ -777,6 +777,16 @@ def run_message(
                 reset(solver)
 
 
+def is_benign_solving_error(e: Exception) -> bool:
+    match e:
+        case ShutdownError():
+            return True
+        case OSError(errno=9):  # BAD_FILE_DESCRIPTOR
+            return True
+        case _:
+            return False
+
+
 @dataclass(frozen=True)
 class CounterexampleHandler:
     """Handles potential assertion violations and generates counterexamples."""
@@ -856,13 +866,35 @@ def handle_assertion_violation(
             partial(
                 self._solve_end_to_end_callback,
                 ex=ex,
+                path_ctx=path_ctx,
                 description=description,
             )
         )
         self.submitted_futures.append(solve_future)
 
+    def _get_solver_output(self, future: Future, path_ctx: PathContext) -> SolverOutput:
+        path_id, query_file = path_ctx.path_id, str(path_ctx.dump_file)
+
+        if self.ctx.solving_ctx.executor.is_shutdown():
+            # if the thread pool is in the process of shutting down,
+            # we want to stop processing remaining models/timeouts/errors, etc.
+            e = "executor has been shutdown"
+            return SolverOutput.from_error(e, path_id=path_id, query_file=query_file)
+
+        if e := future.exception():
+            if not is_benign_solving_error(e):
+                error(f"encountered exception during assertion solving: {e!r}")
+            return SolverOutput.from_error(e, path_id=path_id, query_file=query_file)
+
+        try:
+            return future.result()
+        except Exception as e:
+            if not is_benign_solving_error(e):
+                error(f"encountered exception during assertion solving: {e!r}")
+            return SolverOutput.from_error(e, path_id=path_id, query_file=query_file)
+
     def _solve_end_to_end_callback(
-        self, future: Future, ex: Exec, description: str
+        self, future: Future, ex: Exec, path_ctx: PathContext, description: str
     ) -> None:
         """
         Callback function for handling solver results.
@@ -878,52 +910,19 @@ def _solve_end_to_end_callback(
         ctx = self.ctx
         args = ctx.args
 
-        if ctx.solving_ctx.executor.is_shutdown():
-            # if the thread pool is in the process of shutting down,
-            # we want to stop processing remaining models/timeouts/errors, etc.
-            return
-
-        if e := future.exception():
-            if isinstance(e, ShutdownError):
-                return
-
-            # we close file descriptors forcibly to avoid this issue:
-            # https://github.com/a16z/halmos/pull/527
-            if isinstance(e, OSError) and e.errno == BAD_FILE_DESCRIPTOR:
-                return
-
-            error(f"encountered exception during assertion solving: {e!r}")
-            return
-
-        #
-        # we are done solving, process and triage the result
-        #
-
-        try:
-            solver_output: SolverOutput = future.result()
-        except OSError as e:
-            if e.errno == BAD_FILE_DESCRIPTOR:
-                return
-
-            # re-raise other OSErrors
-            raise
-
+        solver_output: SolverOutput = self._get_solver_output(future, path_ctx)
+        ctx.solver_outputs.append(solver_output)
         result, model = solver_output.result, solver_output.model
         path_id = solver_output.path_id
 
-        # keep track of the solver outputs, so that we can display PASS/FAIL/TIMEOUT/ERROR later
-        ctx.solver_outputs.append(solver_output)
-
         if result == unsat:
             if solver_output.unsat_core:
                 ctx.append_unsat_core(solver_output.unsat_core)
             return
 
         if result == "err":
+            error(f"{solver_output.error=} ({solver_output.returncode=})")
             self._save_failed_query(path_id, solver_output, "error")
-            error(
-                f"solver error: {solver_output.error} (returncode={solver_output.returncode})"
-            )
             return
 
         # handle "unknown" (timeout) result
@@ -980,9 +979,9 @@ def _save_failed_query(
         ctx = self.ctx
         args = ctx.args
 
+        query_file = solver_output.query_file
         debug_dir = f"{dirname(ctx.solving_ctx.dump_dir)}-{failure_type}"
         os.makedirs(debug_dir, exist_ok=True)
-        query_file = solver_output.query_file
         debug_query_file = os.path.join(debug_dir, os.path.basename(query_file))
         try:
             shutil.copy2(query_file, debug_query_file)

src/halmos/solve.py

@@ -356,6 +356,21 @@ def from_result(
                     "err", returncode, path_id, query_file, error=stderr
                 )
 
+    @staticmethod
+    def from_error(
+        error: Exception | str,
+        path_id: int,
+        query_file: str,
+        returncode: int = -1,
+    ) -> "SolverOutput":
+        return SolverOutput(
+            result="err",
+            returncode=returncode,
+            path_id=path_id,
+            query_file=query_file,
+            error=str(error),
+        )
+
 
 def parse_const_value(value: str) -> int:
     match value[:2]:

tests/test_config.py

@@ -356,14 +356,14 @@ def test_solver_resolution_precedence(config):
     # command line overrides
     #########################################################
 
-    cli_config = config.with_overrides(ConfigSource.command_line, solver="cvc5")
-    assert cli_config.solver == "cvc5"
+    cli_config = config.with_overrides(ConfigSource.command_line, solver="z3")
+    assert cli_config.solver == "z3"
 
     # the solver command is inherited from the default config
     assert cli_config.solver_command == config.solver_command
 
     # but the actual command is derived from the solver option (at a higher precedence)
-    assert "cvc5" in " ".join(cli_config.resolved_solver_command)
+    assert "z3" in " ".join(cli_config.resolved_solver_command)
 
     #########################################################
     # contract annotation overrides
@@ -375,7 +375,7 @@ def test_solver_resolution_precedence(config):
     )
     # the solver option is inherited from the command line config
     assert contract_config.value_with_source("solver") == (
-        "cvc5",
+        "z3",
         ConfigSource.command_line,
     )
 
@@ -384,7 +384,7 @@ def test_solver_resolution_precedence(config):
 
     # the resolved solver command is derived from the solver option (command line)
     # because command line has higher precedence than contract annotation
-    assert "cvc5" in " ".join(contract_config.resolved_solver_command)
+    assert "z3" in " ".join(contract_config.resolved_solver_command)
 
 
 def test_command_line_precedence_over_annotations(config):