feat: save timeout queries for offline solving (#552)

Author: daejunpark

src/halmos/__main__.py

@@ -35,6 +35,7 @@
     ZeroExt,
     eq,
     set_option,
+    unknown,
     unsat,
 )
 
@@ -107,6 +108,7 @@
     InvariantTestingContext,
     PathContext,
     SolverOutput,
+    dirname,
     solve_end_to_end,
     solve_low_level,
 )
@@ -126,21 +128,20 @@
     Word,
     address,
     color_error,
+    color_good,
+    color_info,
+    color_warn,
     con,
     con_addr,
     create_solver,
-    cyan,
     extract_bytes,
-    green,
     hexify,
     indent_text,
     int_of,
-    red,
     smt_and,
     smt_or,
     uid,
     unbox_int,
-    yellow,
 )
 
 BAD_FILE_DESCRIPTOR = 9
@@ -646,11 +647,11 @@ def _compute_frontier(ctx: ContractContext, depth: int) -> Iterator[Exec]:
     for idx, pre_ex in enumerate(curr_exs):
         ui.update_status(
             f"{contract_name}: "
-            f"depth: {cyan(depth)} | "
-            f"starting states: {cyan(len(curr_exs))} | "
-            f"unique states: {cyan(len(visited))} | "
-            f"frontier states: {cyan(len(next_exs))} | "
-            f"completed paths: {cyan(idx)} "
+            f"depth: {color_info(depth)} | "
+            f"starting states: {color_info(len(curr_exs))} | "
+            f"unique states: {color_info(len(visited))} | "
+            f"frontier states: {color_info(len(next_exs))} | "
+            f"completed paths: {color_info(idx)} "
         )
 
         for addr in resolve_target_contracts(ctx.inv_ctx, pre_ex):
@@ -908,6 +909,7 @@ def _solve_end_to_end_callback(
             raise
 
         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)
@@ -918,11 +920,17 @@ def _solve_end_to_end_callback(
             return
 
         if result == "err":
+            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
+        if result == unknown:
+            self._save_failed_query(path_id, solver_output, "timeout")
+            return
+
         # model could be an empty dict here, so compare to None explicitly
         if model is None:
             return
@@ -936,14 +944,13 @@ def _solve_end_to_end_callback(
         if description:
             print(description)
 
-        path_id = solver_output.path_id
         if args.verbose >= VERBOSITY_TRACE_COUNTEREXAMPLE:
             pid_str = f" #{path_id}" if args.verbose >= VERBOSITY_TRACE_PATHS else ""
             print(f"Trace{pid_str}:")
             print(ctx.traces[path_id], end="")
 
         if model.is_valid:
-            print(red(f"Counterexample: {model}"))
+            print(color_error(f"Counterexample: {model}"))
             ctx.valid_counterexamples.append(model)
 
             # add the stacks from the temporary flamegraph to the global one
@@ -966,6 +973,33 @@ def _solve_end_to_end_callback(
         if sequence := ctx.call_sequences[path_id]:
             print(f"Sequence:\n{sequence}")
 
+    def _save_failed_query(
+        self, path_id: int, solver_output: SolverOutput, failure_type: str
+    ) -> None:
+        """Save query and call sequence to a separate directory for debugging."""
+        ctx = self.ctx
+        args = ctx.args
+
+        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)
+        except Exception as e:
+            error(f"Could not copy failed query to {failure_type} directory: {e}")
+
+        # save call sequence to a separate file for debugging context
+        if call_sequence := ctx.call_sequences.get(path_id):
+            call_seq_file = f"{debug_query_file}.callseq"
+            try:
+                with open(call_seq_file, "w") as f:
+                    f.write(call_sequence)
+                    if args.verbose >= VERBOSITY_TRACE_COUNTEREXAMPLE:
+                        f.write(f"\nTrace:\n{ctx.traces[path_id]}")
+            except Exception as e:
+                error(f"Could not save call sequence: {e}")
+
 
 def run_test(ctx: FunctionContext) -> TestResult:
     args = ctx.args
@@ -1141,26 +1175,26 @@ def run_test(ctx: FunctionContext) -> TestResult:
 
     counter = Counter(str(m.result) for m in ctx.solver_outputs)
     if counter["sat"] > 0:
-        passfail = red("[FAIL]")
+        passfail = color_error("[FAIL]")
         exitcode = Exitcode.COUNTEREXAMPLE.value
     elif counter["err"] > 0:
-        passfail = red("[ERROR]")
+        passfail = color_error("[ERROR]")
         exitcode = Exitcode.EXCEPTION.value
     elif counter["unknown"] > 0:
-        passfail = yellow("[TIMEOUT]")
+        passfail = color_warn("[TIMEOUT]")
         exitcode = Exitcode.TIMEOUT.value
     elif len(stuck) > 0:
-        passfail = red("[ERROR]")
+        passfail = color_error("[ERROR]")
         exitcode = Exitcode.STUCK.value
     elif normal == 0:
-        passfail = red("[ERROR]")
+        passfail = color_error("[ERROR]")
         exitcode = Exitcode.REVERT_ALL.value
         warn_code(
             REVERT_ALL,
             f"{funsig}: all paths have been reverted; the setup state or inputs may have been too restrictive.",
         )
     else:
-        passfail = green("[PASS]")
+        passfail = color_good("[PASS]")
         exitcode = Exitcode.PASS.value
 
     timer.stop()
@@ -1172,6 +1206,12 @@ def run_test(ctx: FunctionContext) -> TestResult:
         f"bounds: [{', '.join([str(x) for x in dyn_params])}])"
     )
 
+    if exitcode in (Exitcode.TIMEOUT.value, Exitcode.EXCEPTION.value):
+        # print query directory information
+        failure_type = "timeout" if exitcode == Exitcode.TIMEOUT.value else "error"
+        query_dir = f"{dirname(ctx.solving_ctx.dump_dir)}-{failure_type}"
+        print(color_info(f"{failure_type.capitalize()} queries saved in: {query_dir}"))
+
     for path_id, _, err in stuck:
         warn_code(INTERNAL_ERROR, f"Encountered {type(err).__name__}: {err}")
         if args.print_blocked_states:

src/halmos/solve.py

@@ -313,6 +313,9 @@ class SolverOutput:
     # references to Exec objects past the lifetime of the path
     path_id: int
 
+    # input query file path
+    query_file: str
+
     # solver model
     model: PotentialModel | None = None
 
@@ -331,21 +334,27 @@ def from_result(
         first_line = stdout[:newline_idx] if newline_idx != -1 else stdout
 
         args, path_id = path_ctx.args, path_ctx.path_id
+        query_file = str(path_ctx.dump_file)
+
         if args.verbose >= 1:
             debug(f"    {first_line}")
 
         match first_line:
             case "unsat":
                 unsat_core = parse_unsat_core(stdout) if args.cache_solver else None
-                return SolverOutput(unsat, returncode, path_id, unsat_core=unsat_core)
+                return SolverOutput(
+                    unsat, returncode, path_id, query_file, unsat_core=unsat_core
+                )
             case "sat":
                 is_valid = is_model_valid(stdout)
                 model = PotentialModel(model=parse_model_str(stdout), is_valid=is_valid)
-                return SolverOutput(sat, returncode, path_id, model=model)
+                return SolverOutput(sat, returncode, path_id, query_file, model=model)
             case "unknown":
-                return SolverOutput(unknown, returncode, path_id)
+                return SolverOutput(unknown, returncode, path_id, query_file)
             case _:
-                return SolverOutput("err", returncode, path_id, error=stderr)
+                return SolverOutput(
+                    "err", returncode, path_id, query_file, error=stderr
+                )
 
 
 def parse_const_value(value: str) -> int:
@@ -504,7 +513,10 @@ def solve_low_level(path_ctx: PathContext) -> SolverOutput:
         stdout, stderr, returncode = future.result()
     except subprocess.TimeoutExpired:
         return SolverOutput(
-            result=unknown, returncode=EXIT_TIMEDOUT, path_id=path_ctx.path_id
+            result=unknown,
+            returncode=EXIT_TIMEDOUT,
+            path_id=path_ctx.path_id,
+            query_file=smt2_filename,
         )
 
     # save solver stdout to file
@@ -536,7 +548,7 @@ def solve_end_to_end(ctx: PathContext) -> SolverOutput:
     # if the query contains an unsat-core, it is unsat; no need to run the solver
     if check_unsat_cores(query, ctx.solving_ctx.unsat_cores):
         verbose("  Already proven unsat")
-        return SolverOutput(unsat, 0, path_id)
+        return SolverOutput(unsat, 0, path_id, str(ctx.dump_file))
 
     solver_output = solve_low_level(ctx)
     result, model = solver_output.result, solver_output.model