Give a timed-out solver a chance to clean up after itself

Cargo.toml

@@ -30,6 +30,7 @@ thiserror = "2.0.18"
 tracing = "0.1.44"
 tracing-subscriber = { version = "0.3.23", features = ["env-filter"] }
 process_control = "5.2.0"
+nix = { version = "0.31.3", default-features = false, features = ["signal"] }
 
 [dev-dependencies]
 ui_test = "0.30.6"

README.md

@@ -139,7 +139,7 @@ Several environment variables are used by Thrust to configure its behavior:
 
 - `THRUST_SOLVER`: A CHC solver command used to solve CHC constraints generated by Thrust. Default: `z3`
 - `THRUST_SOLVER_ARGS`: Whitespace-separated command-line flags passed to the solver. The default is `fp.spacer.global=true fp.validate=true` when the solver is `z3`.
-- `THRUST_SOLVER_TIMEOUT_SECS`: Timeout for waiting on results from the solver. Default: `30`
+- `THRUST_SOLVER_TIMEOUT_SECS`: Timeout for waiting on results from the solver. A solver that exceeds it is sent `SIGTERM`, and is expected to exit on it so that it can release what it holds. Default: `30`
 - `THRUST_OUTPUT_DIR`: When configured, Thrust outputs intermediate smtlib2 files into this directory.
 - `THRUST_ENUM_EXPANSION_DEPTH_LIMIT`: When Thrust works with enums, it "expands" the structure of the enum value onto its environment. This configuration value sets the limit on the depth of recursion during this expansion to handle enums that are defined recursively. It is our future work to discover a sensible value for this automatically. Default: `2`
 

src/chc/solver.rs

@@ -19,6 +19,20 @@ pub enum CheckSatError {
     Io(#[from] std::io::Error),
 }
 
+/// Asks a solver command that ran over its time limit to shut itself down.
+///
+/// It is asked rather than killed because it may hold resources that outlive the process
+/// and that only it knows how to release, as `tests/thrust-pcsat-wrapper` does with the
+/// Docker container it runs the solver in.
+///
+/// A timed-out process is left unreaped, so the system cannot hand its identifier to an
+/// unrelated process that this would then reach.
+fn terminate(pid: u32) {
+    use nix::sys::signal::{kill, Signal};
+
+    let _ = kill(nix::unistd::Pid::from_raw(pid as i32), Signal::SIGTERM);
+}
+
 /// A configuration for running a command-line CHC solver.
 #[derive(Debug, Clone)]
 pub struct CommandConfig {
@@ -52,13 +66,17 @@ impl CommandConfig {
         use process_control::{ChildExt as _, Control as _};
 
         let start = std::time::Instant::now();
-        tracing::info!(timeout = ?self.timeout, pid = child.id(), "waiting");
-        let mut child = child.controlled_with_output().terminate_for_timeout();
+        let pid = child.id();
+        tracing::info!(timeout = ?self.timeout, pid, "waiting");
+        let mut child = child.controlled_with_output();
         if let Some(timeout) = self.timeout {
             child = child.time_limit(timeout);
         }
         let output = match child.wait()? {
-            None => return Err(CheckSatError::Timeout(self.timeout.unwrap())),
+            None => {
+                terminate(pid);
+                return Err(CheckSatError::Timeout(self.timeout.unwrap()));
+            }
             Some(output) => output,
         };
         let elapsed = std::time::Instant::now() - start;

tests/thrust-pcsat-wrapper

@@ -3,12 +3,25 @@
 COAR_IMAGE=${COAR_IMAGE:-ghcr.io/hiroshi-unno/coar:main}
 
 smt2=$(mktemp -p . --suffix .smt2)
-trap "rm -f $smt2" EXIT
+solver_out=$(mktemp)
+trap 'rm -f "$smt2" "$solver_out"' EXIT
 cp "$1" "$smt2"
-out=$(
-docker run --rm -v "$PWD:/mnt" -w /root/coar "$COAR_IMAGE" \
-    main.exe -c ./config/solver/pcsat_tbq_ar.json -p pcsp "/mnt/$smt2"
-)
+
+container=$(docker create --rm -v "$PWD:/mnt" -w /root/coar "$COAR_IMAGE" \
+    main.exe -c ./config/solver/pcsat_tbq_ar.json -p pcsp "/mnt/$smt2")
+
+# Thrust ends a solver that runs over its timeout with SIGTERM, and Docker keeps the
+# container going once the client attached to it is gone. Passing the signal on to the
+# solver instead would achieve nothing: it runs as the container's PID 1, for which the
+# kernel drops every signal that has no handler.
+trap 'docker rm --force "$container" > /dev/null 2>&1; exit 143' TERM
+
+# Bash defers a trap until the command in the foreground finishes -- which would be the
+# solver the trap above is meant to interrupt. `wait` is the exception.
+docker start --attach "$container" > "$solver_out" &
+wait $!
 exit_code=$?
+
+out=$(< "$solver_out")
 echo "${out%,*}"
 exit "$exit_code"