bring back timeouts, clean children after timeout

src/halmos/__main__.py

@@ -50,7 +50,7 @@
     warn_code,
 )
 from .mapper import BuildOut, DeployAddressMapper, Mapper
-from .processes import PopenExecutor, PopenFuture
+from .processes import PopenExecutor, PopenFuture, TimeoutExpired
 from .sevm import (
     EMPTY_BALANCE,
     EVM,
@@ -177,7 +177,7 @@ class FunctionContext:
     solver_executor: PopenExecutor = field(default_factory=PopenExecutor)
 
     # list of solver outputs for this function
-    _solver_outputs: list["SolverOutput"] = field(default_factory=list)
+    solver_outputs: list["SolverOutput"] = field(default_factory=list)
 
     # list of valid counterexamples for this function
     valid_counterexamples: list[PotentialModel] = field(default_factory=list)
@@ -204,10 +204,6 @@ def __post_init__(self):
         )
         object.__setattr__(self, "thread_pool", thread_pool)
 
-    @property
-    def solver_outputs(self):
-        return self._solver_outputs
-
 
 @dataclass(frozen=True)
 class PathContext:
@@ -679,15 +675,12 @@ def run_test(ctx: FunctionContext) -> TestResult:
 
             def log_future_result(future: Future):
                 if e := future.exception():
-                    error(f"encountered exception during assertion solving: {e}")
+                    error(f"encountered exception during assertion solving: {e!r}")
 
             solve_future = ctx.thread_pool.submit(solve_end_to_end, path_ctx)
             solve_future.add_done_callback(log_future_result)
             submitted_futures.append(solve_future)
 
-            # XXX handle refinement
-            # XXX handle timeout
-
         elif ex.context.is_stuck():
             stuck.append((path_id, ex, ex.context.get_stuck_reason()))
             if args.print_blocked_states:
@@ -731,10 +724,6 @@ def log_future_result(future: Future):
         rich.get_console().clear_live()
         with Status("") as status:
             while True:
-                # XXX should not be necessary, in case of early we expect all futures to be interrupted
-                # if args.early_exit and ctx.valid_counterexamples:
-                #     break
-
                 done = sum(fm.done() for fm in submitted_futures)
                 total = potential
                 if done == total:
@@ -752,12 +741,6 @@ def log_future_result(future: Future):
     # print test result
     #
 
-    for model in ctx.valid_counterexamples:
-        print(red(f"Counterexample: {model}"))
-
-        if args.early_exit:
-            break
-
     counter = Counter(str(m.result) for m in ctx.solver_outputs)
     if counter["sat"] > 0:
         passfail = red("[FAIL]")
@@ -978,24 +961,21 @@ def solve_low_level(path_ctx: PathContext) -> SolverOutput:
         print("  Checking with external solver process")
         print(f"    {args.solver_command} {smt2_filename} > {smt2_filename}.out")
 
-    # XXX fix timeout
-
     # solver_timeout_assertion == 0 means no timeout,
     # which translates to timeout_seconds=None for subprocess.run
-    # timeout_seconds = None
-    # if timeout_millis := args.solver_timeout_assertion:
-    #     timeout_seconds = timeout_millis / 1000
+    timeout_seconds = t / 1000 if (t := args.solver_timeout_assertion) else None
 
     cmd = args.solver_command.split() + [smt2_filename]
-    future = PopenFuture(cmd, metadata={"path_ctx": path_ctx})
-
-    # XXX avoiding callbacks now
-    # future.add_done_callback(solver_callback)
+    future = PopenFuture(cmd, timeout=timeout_seconds)
 
+    # starts the subprocess asynchronously
     fun_ctx.solver_executor.submit(future)
 
     # block until the external solver returns, times out, is interrupted, fails, etc.
-    stdout, stderr, returncode = future.result()
+    try:
+        stdout, stderr, returncode = future.result()
+    except TimeoutExpired:
+        return SolverOutput(result=unknown, path_id=path_ctx.path_id)
 
     # save solver stdout to file
     with open(f"{smt2_filename}.out", "w") as f:
@@ -1066,6 +1046,9 @@ def solve_end_to_end(ctx: PathContext) -> None:
         # we want to stop processing remaining models/timeouts/errors, etc.
         return
 
+    # keep track of the solver outputs, so that we can display PASS/FAIL/TIMEOUT/ERROR later
+    fun_ctx.solver_outputs.append(solver_output)
+
     if result == unsat:
         if solver_output.unsat_core:
             fun_ctx.unsat_cores.append(solver_output.unsat_core)
@@ -1077,14 +1060,14 @@ def solve_end_to_end(ctx: PathContext) -> None:
         return
 
     if model.is_valid:
-        # we don't print the model here because this may be called from multiple threads
+        print(red(f"Counterexample: {model}"))
+
         fun_ctx.valid_counterexamples.append(model)
 
         # we have a valid counterexample, so we are eligible for early exit
         if args.early_exit:
             fun_ctx.solver_executor.shutdown(wait=False)
     else:
-        # XXX avoid printing here
         warn_str = f"Counterexample (potentially invalid): {model}"
         warn_code(COUNTEREXAMPLE_INVALID, warn_str)
         fun_ctx.invalid_counterexamples.append(model)

src/halmos/processes.py

@@ -3,32 +3,32 @@
 import subprocess
 import threading
 import time
-from subprocess import PIPE, Popen
+from subprocess import PIPE, Popen, TimeoutExpired
 
 import psutil
 
 
 class PopenFuture(concurrent.futures.Future):
     cmd: list[str]
+    timeout: float | None  # in seconds, None means no timeout
     process: subprocess.Popen | None
     stdout: str | None
     stderr: str | None
     returncode: int | None
     start_time: float | None
     end_time: float | None
-    metadata: dict | None
     _exception: Exception | None
 
-    def __init__(self, cmd: list[str], metadata: dict | None = None):
+    def __init__(self, cmd: list[str], timeout: float | None = None):
         super().__init__()
         self.cmd = cmd
+        self.timeout = timeout
         self.process = None
         self.stdout = None
         self.stderr = None
         self.returncode = None
         self.start_time = None
         self.end_time = None
-        self.metadata = metadata
         self._exception = None
 
     def start(self):
@@ -40,9 +40,14 @@ def run():
                 self.process = Popen(self.cmd, stdout=PIPE, stderr=PIPE, text=True)
 
                 # blocks until the process terminates
-                self.stdout, self.stderr = self.process.communicate()
+                self.stdout, self.stderr = self.process.communicate(
+                    timeout=self.timeout
+                )
                 self.end_time = time.time()
                 self.returncode = self.process.returncode
+            except TimeoutExpired as e:
+                self._exception = e
+                self.cancel()
             except Exception as e:
                 self._exception = e
             finally:
@@ -58,30 +63,32 @@ def run():
 
     def cancel(self):
         """Attempts to terminate and then kill the process and its children."""
-        if self.is_running():
-            self.process.terminate()
+        if not self.is_running():
+            return
 
-            # use psutil to kill the entire process tree (including children)
-            try:
-                parent_process = psutil.Process(self.process.pid)
-                processes = parent_process.children(recursive=True)
-                processes.append(parent_process)
+        self.process.terminate()
+
+        # use psutil to kill the entire process tree (including children)
+        try:
+            parent_process = psutil.Process(self.process.pid)
+            processes = parent_process.children(recursive=True)
+            processes.append(parent_process)
 
-                # ask politely to terminate first
-                for process in processes:
-                    process.terminate()
+            # ask politely to terminate first
+            for process in processes:
+                process.terminate()
 
-                # give them some time to terminate
-                time.sleep(0.1)
+            # give them some time to terminate
+            time.sleep(0.5)
 
-                # after grace period, force kill
-                for process in processes:
-                    if process.is_running():
-                        process.kill()
+            # after grace period, force kill
+            for process in processes:
+                if process.is_running():
+                    process.kill()
 
-            except psutil.NoSuchProcess:
-                # process already terminated, nothing to do
-                pass
+        except psutil.NoSuchProcess:
+            # process already terminated, nothing to do
+            pass
 
     def exception(self) -> Exception | None:
         """Returns any exception raised during the process."""