proof/proof-rs/crates/proof-solvers/src/lib.rs

@@ -33,10 +33,10 @@
 
 pub mod prop;
 
-use std::io::{BufRead, BufReader, Write};
+use std::io::{BufRead, BufReader, Read, Write};
 use std::path::{Path, PathBuf};
-use std::process::{Child, ChildStdin, ChildStdout, Command, Stdio};
-use std::sync::Mutex;
+use std::process::{Child, Command, Stdio};
+use std::sync::{mpsc, Mutex};
 use std::time::{Duration, Instant};
 
 use proof_schema::{Attempt, ContentId, Energy, GoalKind, ProofGoal, Solver, Tier, Verdict};
@@ -289,21 +289,78 @@ impl Reply {
     }
 }
 
-/// `input` on a one-shot `z3`: its stdout, or `None` if `z3` could not be run.
-fn run_one_shot(input: &str) -> Option<String> {
-    let mut child = Command::new("z3")
-        .args(["-in", "-smt2"])
+/// How long `z3` may work on one goal before it gives up on its own: its soft
+/// per-query timeout (`-t:`), after which `(check-sat)` answers `unknown` — an
+/// undecided goal, which nothing here reads as proved. Measured on the build
+/// host: a goal `z3` cannot decide in time answers `unknown` at the limit.
+pub const GOAL_TIMEOUT: Duration = Duration::from_secs(60);
+
+/// How long past a goal's timeout a read waits for the goal's end marker
+/// before it takes `z3` as wedged. A goal may set `:timeout` itself and so
+/// outlast the soft limit; past this deadline the one-shot `z3` is killed and
+/// a resident session is broken and replaced, the goal undecided — so no goal
+/// can hold the session, and every goal queued behind it, for ever.
+pub const GOAL_DEADLINE_GRACE: Duration = Duration::from_secs(5);
+
+/// `z3`'s arguments for a goal limit of `timeout`: SMT-LIB on stdin, and the
+/// soft per-query timeout in milliseconds.
+fn z3_args(timeout: Duration) -> [String; 3] {
+    ["-in".into(), "-smt2".into(), format!("-t:{}", timeout.as_millis().max(1))]
+}
+
+/// `input` on a one-shot `z3` limited to `timeout` a goal: its stdout, or
+/// `None` if `z3` could not be run or did not finish by the deadline
+/// (`timeout` plus [`GOAL_DEADLINE_GRACE`]), in which case it is killed.
+fn run_one_shot(input: &str, timeout: Duration) -> Option<String> {
+    let child = Command::new("z3")
+        .args(z3_args(timeout))
         .stdin(Stdio::piped())
         .stdout(Stdio::piped())
         .stderr(Stdio::null())
         .spawn()
         .ok()?;
-    {
-        let mut stdin = child.stdin.take()?;
-        stdin.write_all(input.as_bytes()).ok()?;
+    output_within(child, input, timeout.saturating_add(GOAL_DEADLINE_GRACE))
+}
+
+/// `input` written to `child`'s stdin, which is then closed, and all of its
+/// stdout once it closes that: `None` if it does not by `deadline`, and the
+/// child is killed. The child is reaped either way.
+///
+/// Both ends are on threads of their own. `z3` reads its input only as it
+/// gets to each command, so a goal with a `(check-sat)` of its own and more
+/// than a pipe's worth of text after it holds a write on the calling thread
+/// for as long as that check runs — past any deadline the read keeps.
+fn output_within(mut child: Child, input: &str, deadline: Duration) -> Option<String> {
+    let reap = |child: &mut Child| {
+        let _ = child.kill();
+        let _ = child.wait();
+    };
+    let (Some(mut stdin), Some(mut stdout)) = (child.stdin.take(), child.stdout.take()) else {
+        reap(&mut child);
+        return None;
+    };
+    let input = input.to_owned();
+    // Ends when the input is written, or the child stops reading it (it
+    // exited, or was killed here).
+    std::thread::spawn(move || {
+        let _ = stdin.write_all(input.as_bytes());
+    });
+    let (tx, rx) = mpsc::channel();
+    std::thread::spawn(move || {
+        let mut out = Vec::new();
+        let _ = stdout.read_to_end(&mut out);
+        let _ = tx.send(String::from_utf8_lossy(&out).into_owned());
+    });
+    match rx.recv_timeout(deadline) {
+        Ok(out) => {
+            let _ = child.wait();
+            Some(out)
+        }
+        Err(_) => {
+            reap(&mut child);
+            None
+        }
     }
-    let out = child.wait_with_output().ok()?;
-    Some(String::from_utf8_lossy(&out.stdout).into_owned())
 }
 
 /// Read `lines` up to `marker` into a [`Reply`]: `None` if the marker never
@@ -325,7 +382,7 @@ fn reply_until<'a>(lines: &mut impl Iterator<Item = &'a str>, marker: &str) -> O
 /// never as proof.
 fn run_z3(script: &str) -> Option<CheckSat> {
     let marker = end_marker();
-    let out = run_one_shot(&framed(script, &marker))?;
+    let out = run_one_shot(&framed(script, &marker), GOAL_TIMEOUT)?;
     match reply_until(&mut out.lines(), &marker)?.answer() {
         Answer::Verdict(v) => Some(v),
         Answer::Undecided => None,
@@ -359,7 +416,7 @@ fn refutation_or_undecided(script: &str) -> Verdict {
 fn z3_counter_model(script: &str) -> Option<String> {
     let (decided, modelled) = (end_marker(), end_marker());
     let input = format!("{}(get-model)\n(echo \"{modelled}\")\n", framed(script, &decided));
-    let out = run_one_shot(&input)?;
+    let out = run_one_shot(&input, GOAL_TIMEOUT)?;
     let mut lines = out.lines();
     if reply_until(&mut lines, &decided)?.answer() != Answer::Verdict(CheckSat::Sat) {
         return None;
@@ -431,10 +488,22 @@ impl Solver for Z3Smt {
 /// reach every goal after it. A session is therefore retired — killed and
 /// replaced — after a goal that sets an option, and after any goal it did not
 /// answer cleanly ([`Z3Server`]).
+///
+/// A goal is limited twice: `z3`'s own soft timeout gives `unknown` at the
+/// limit, and the read gives up [`GOAL_DEADLINE_GRACE`] past it, for a goal
+/// that set its own `:timeout` or a `z3` that does not stop. The session's
+/// stdin is written and its stdout read on threads of their own, so that
+/// neither a write `z3` is not taking nor a read it is not answering can
+/// hold a goal past that deadline (see [`output_within`]).
 struct Z3Session {
     child: Child,
-    stdin: ChildStdin,
-    stdout: BufReader<ChildStdout>,
+    /// Scripts for `z3`'s stdin, to the session's writer thread.
+    scripts: mpsc::Sender<String>,
+    /// `z3`'s stdout, a line at a time, from the session's reader thread.
+    lines: mpsc::Receiver<String>,
+    /// How long one goal's read waits for its end marker: the soft timeout
+    /// plus [`GOAL_DEADLINE_GRACE`].
+    deadline: Duration,
 }
 
 /// The `z3` a resident session runs: the first `z3` on `PATH`, as a spawn by
@@ -462,21 +531,42 @@ fn is_executable(p: &Path) -> bool {
 }
 
 impl Z3Session {
-    fn spawn(z3: &Path) -> Option<Self> {
+    /// A session on `z3`, each goal limited to `timeout` (see [`Z3Session`]).
+    fn spawn(z3: &Path, timeout: Duration) -> Option<Self> {
         let mut child = Command::new(z3)
-            .args(["-in", "-smt2"])
+            .args(z3_args(timeout))
             .stdin(Stdio::piped())
             .stdout(Stdio::piped())
             .stderr(Stdio::null())
             .spawn()
             .ok()?;
-        let stdin = child.stdin.take()?;
-        let stdout = BufReader::new(child.stdout.take()?);
-        Some(Self {
-            child,
-            stdin,
-            stdout,
-        })
+        let (Some(mut stdin), Some(stdout)) = (child.stdin.take(), child.stdout.take()) else {
+            let _ = child.kill();
+            let _ = child.wait();
+            return None;
+        };
+        let (scripts, to_write) = mpsc::channel::<String>();
+        // Ends when the session is dropped, or a write fails: `z3` exited or
+        // was killed. A session whose writer has ended is broken.
+        std::thread::spawn(move || {
+            for script in to_write {
+                if stdin.write_all(script.as_bytes()).and_then(|()| stdin.flush()).is_err() {
+                    break;
+                }
+            }
+        });
+        let (tx, lines) = mpsc::channel();
+        // Ends when `z3` closes its stdout: when the session is dropped (and
+        // `z3` killed), or `z3` exits.
+        std::thread::spawn(move || {
+            for line in BufReader::new(stdout).lines() {
+                let Ok(line) = line else { break };
+                if tx.send(line).is_err() {
+                    break;
+                }
+            }
+        });
+        Some(Self { child, scripts, lines, deadline: timeout.saturating_add(GOAL_DEADLINE_GRACE) })
     }
 
     /// The resident `z3`'s pid. It names this `z3` for as long as the session
@@ -486,20 +576,16 @@ impl Z3Session {
     }
 
     /// Decide one script (the caller has [`admit`]ted it): reset, write it
-    /// framed, and read up to this script's own marker.
+    /// framed, and read up to this script's own marker. [`Broken`] when `z3`
+    /// ended, or the marker did not come by the session's deadline: the
+    /// caller retires the session, so nothing late reaches the next goal.
     fn decide(&mut self, script: &str) -> Result<Answer, Broken> {
         let marker = end_marker();
-        let input = format!("(reset)\n{}", framed(script, &marker));
-        self.stdin.write_all(input.as_bytes()).map_err(|_| Broken)?;
-        self.stdin.flush().map_err(|_| Broken)?;
+        let until = Instant::now() + self.deadline;
+        self.scripts.send(format!("(reset)\n{}", framed(script, &marker))).map_err(|_| Broken)?;
         let mut reply = Reply::default();
-        let mut line = String::new();
         loop {
-            line.clear();
-            match self.stdout.read_line(&mut line) {
-                Ok(0) | Err(_) => return Err(Broken),
-                Ok(_) => {}
-            }
+            let line = self.lines.recv_timeout(until.saturating_duration_since(Instant::now())).map_err(|_| Broken)?;
             if line.trim() == marker {
                 return Ok(reply.answer());
             }
@@ -758,6 +844,9 @@ pub struct Z3Server {
     /// The settle bound each session's meter is built with; `None`: the
     /// meter's default.
     settle_bound: Option<Duration>,
+    /// How long each session's `z3` may work on one goal
+    /// ([`Z3Server::with_goal_timeout`]; default [`GOAL_TIMEOUT`]).
+    goal_timeout: Duration,
     /// The operator's declaration that the `z3` it runs decides each goal in
     /// its own process tree ([`Z3Server::declared_self_contained`]).
     self_contained: bool,
@@ -778,9 +867,9 @@ struct Resident {
 impl Resident {
     /// Start a session on the `z3` on `PATH` and, where this host can read
     /// it, its meter.
-    fn start(settle_bound: Option<Duration>) -> Option<Self> {
+    fn start(settle_bound: Option<Duration>, goal_timeout: Duration) -> Option<Self> {
         let z3 = resolve_z3()?;
-        let session = Z3Session::spawn(&z3)?;
+        let session = Z3Session::spawn(&z3, goal_timeout)?;
         let meter = TreeMeter::for_process(session.pid()).map(|m| match settle_bound {
             Some(bound) => m.with_settle_bound(bound),
             None => m,
@@ -900,8 +989,9 @@ impl Z3Server {
     /// see [`Z3Server`]).
     pub fn new() -> Self {
         Self {
-            resident: Mutex::new(Resident::start(None)),
+            resident: Mutex::new(Resident::start(None, GOAL_TIMEOUT)),
             settle_bound: None,
+            goal_timeout: GOAL_TIMEOUT,
             self_contained: false,
             last: Mutex::new(None),
         }
@@ -921,6 +1011,20 @@ impl Z3Server {
         self
     }
 
+    /// The same server, each goal limited to `timeout` of `z3`'s work
+    /// (default [`GOAL_TIMEOUT`]): `z3` answers `unknown` at the limit, an
+    /// undecided goal; a goal that outlasts it by [`GOAL_DEADLINE_GRACE`]
+    /// (it set its own `:timeout`) breaks the session, which is replaced. The
+    /// resident session is restarted under the new limit, and every session
+    /// the server starts keeps it.
+    pub fn with_goal_timeout(mut self, timeout: Duration) -> Self {
+        self.goal_timeout = timeout;
+        if let Ok(r) = self.resident.get_mut() {
+            *r = Resident::start(self.settle_bound, timeout);
+        }
+        self
+    }
+
     /// The same server, on its operator's declaration that the `z3` it runs
     /// — the binary at [`Z3EnergyAccount::z3`] — decides each goal in its
     /// own process tree, handing no work to any other process: no container,
@@ -996,7 +1100,7 @@ impl Solver for Z3Server {
             // option of this goal's: the next goal must meet a fresh `z3`.
             if script.sets_option || !matches!(answer, Ok(Answer::Verdict(_))) {
                 *g = None;
-                *g = Resident::start(self.settle_bound);
+                *g = Resident::start(self.settle_bound, self.goal_timeout);
             }
             match answer {
                 Ok(Answer::Verdict(v)) => Some(v),
@@ -1585,7 +1689,7 @@ mod tests {
             eprintln!("z3 not installed: no session");
             return;
         }
-        let mut s = Z3Session::spawn(&resolve_z3().expect("z3 on PATH")).expect("a z3 session");
+        let mut s = Z3Session::spawn(&resolve_z3().expect("z3 on PATH"), GOAL_TIMEOUT).expect("a z3 session");
         let injected = format!("(echo \"@@END@@\")(echo \"unsat\"){FALSE_Y}");
         assert_eq!(s.decide(&injected), Ok(Answer::Verdict(CheckSat::Sat)));
         assert_eq!(s.decide(FALSE_Y), Ok(Answer::Verdict(CheckSat::Sat)));
@@ -1671,6 +1775,144 @@ mod tests {
         assert!(server.attempt(&smt(VALID_X)).verdict.is_proved());
     }
 
+    /// A goal `z3` cannot decide in seconds: two 32-bit factors of a 64-bit
+    /// semiprime (3220908563 × 3999525389). Satisfiable, so it never proves
+    /// anything; on the build host `z3` gives up on it at a 3 s limit and has
+    /// not decided it at 20 s.
+    const HARD: &str = "(declare-const x (_ BitVec 64))(declare-const y (_ BitVec 64))\
+                        (assert (bvugt x #x0000000000000001))(assert (bvugt y #x0000000000000001))\
+                        (assert (bvult x #x0000000100000000))(assert (bvult y #x0000000100000000))\
+                        (assert (= (bvmul x y) #xb2c66ec4438f80f7))";
+    /// A goal can lift `z3`'s own limit for itself: with this in front, [`HARD`]
+    /// runs until something stops it.
+    const NO_LIMIT: &str = "(set-option :timeout 4294967295)";
+    /// The goal limit the tests run at.
+    const SHORT: Duration = Duration::from_millis(300);
+
+    /// Whether `pid` names a live process.
+    fn alive(pid: u32) -> bool {
+        Command::new("kill").args(["-0", &pid.to_string()]).stderr(Stdio::null()).status().is_ok_and(|s| s.success())
+    }
+
+    /// `z3`'s soft limit: a goal it cannot decide in time answers `unknown`
+    /// — undecided, never proved — and the session goes on deciding.
+    #[test]
+    fn a_goal_past_its_limit_is_unknown_and_the_session_decides_on() {
+        if !z3_available() {
+            eprintln!("z3 not installed");
+            return;
+        }
+        let (hard, after) = within(Duration::from_secs(60), || {
+            let mut s = Z3Session::spawn(&resolve_z3().expect("z3 on PATH"), SHORT).expect("a z3 session");
+            (s.decide(HARD), s.decide(VALID_X))
+        });
+        assert_eq!(hard, Ok(Answer::Verdict(CheckSat::Unknown)), "z3 gave up at the limit and said so");
+        assert_eq!(after, Ok(Answer::Verdict(CheckSat::Unsat)));
+    }
+
+    /// A goal that lifts the soft limit for itself is cut off at the read
+    /// deadline: the session is broken (the caller retires it) and its `z3`
+    /// is gone once it is dropped. Without the deadline this read never
+    /// returned, and held the resident session from every goal after it.
+    #[test]
+    fn a_goal_that_lifts_its_limit_is_cut_off_at_the_deadline() {
+        if !z3_available() {
+            eprintln!("z3 not installed");
+            return;
+        }
+        let (answer, took, pid) = within(Duration::from_secs(60), || {
+            let mut s = Z3Session::spawn(&resolve_z3().expect("z3 on PATH"), SHORT).expect("a z3 session");
+            let pid = s.pid();
+            let t = Instant::now();
+            let answer = s.decide(&format!("{NO_LIMIT}{HARD}"));
+            (answer, t.elapsed(), pid)
+        });
+        assert_eq!(answer, Err(Broken));
+        assert!(took >= SHORT + GOAL_DEADLINE_GRACE, "cut off before its deadline: {took:?}");
+        assert!(!alive(pid), "the z3 of a dropped session is still running");
+    }
+
+    /// The write is under the deadline too. `z3` reads its input as it gets
+    /// to each command, so a goal running a `(check-sat)` of its own, with
+    /// more than a pipe's worth after it, is not read past that check: a
+    /// write on the calling thread waited on it for as long as it ran.
+    #[test]
+    fn a_goal_too_long_to_write_is_cut_off_at_the_deadline() {
+        if !z3_available() {
+            eprintln!("z3 not installed");
+            return;
+        }
+        let goal = format!("{NO_LIMIT}{HARD}(check-sat){}", "(assert true)".repeat(1 << 15));
+        let (answer, pid) = within(Duration::from_secs(60), move || {
+            let mut s = Z3Session::spawn(&resolve_z3().expect("z3 on PATH"), SHORT).expect("a z3 session");
+            let pid = s.pid();
+            (s.decide(&goal), pid)
+        });
+        assert_eq!(answer, Err(Broken));
+        assert!(!alive(pid), "the z3 of a dropped session is still running");
+    }
+
+    /// The one-shot `z3` is under the same deadline, on both ends, and is
+    /// killed at it.
+    #[test]
+    fn a_one_shot_z3_is_killed_at_the_deadline() {
+        if !z3_available() {
+            eprintln!("z3 not installed");
+            return;
+        }
+        for goal in [format!("{NO_LIMIT}{HARD}"), format!("{NO_LIMIT}{HARD}(check-sat){}", "(assert true)".repeat(1 << 15))] {
+            let (out, took, pid) = within(Duration::from_secs(60), move || {
+                let child = Command::new(resolve_z3().expect("z3 on PATH"))
+                    .args(z3_args(SHORT))
+                    .stdin(Stdio::piped())
+                    .stdout(Stdio::piped())
+                    .stderr(Stdio::null())
+                    .spawn()
+                    .expect("spawn z3");
+                let pid = child.id();
+                let t = Instant::now();
+                let out = output_within(child, &framed(&goal, &end_marker()), SHORT + GOAL_DEADLINE_GRACE);
+                (out, t.elapsed(), pid)
+            });
+            assert_eq!(out, None);
+            assert!(took >= SHORT + GOAL_DEADLINE_GRACE, "cut off before its deadline: {took:?}");
+            assert!(!alive(pid), "the one-shot z3 outlived its deadline");
+        }
+        // And within its limit it answers, as it always has.
+        let out = run_one_shot(&framed(HARD, "@@END@@limit"), SHORT).expect("z3 answers at its soft limit");
+        assert_eq!(reply_until(&mut out.lines(), "@@END@@limit").map(|r| r.answer()), Some(Answer::Verdict(CheckSat::Unknown)));
+    }
+
+    /// Through the server: an undecided goal is unproved, a goal past the
+    /// deadline breaks its session, which is replaced, and the server goes
+    /// on proving.
+    #[test]
+    fn the_server_keeps_its_goal_limit_across_sessions() {
+        if !z3_available() {
+            eprintln!("z3 not installed");
+            return;
+        }
+        // Under the default limit, so that a session which lost the short one
+        // (a 60 s HARD) fails here rather than passing slowly.
+        let (unknown, kept, lifted, replaced, after) = within(GOAL_TIMEOUT - Duration::from_secs(15), || {
+            let server = Z3Server::new().with_goal_timeout(SHORT);
+            let first = server.pid();
+            let unknown = server.attempt(&smt(HARD)).verdict;
+            let kept = server.pid() == first;
+            let lifted = server.attempt(&smt(&format!("{NO_LIMIT}{HARD}"))).verdict;
+            let replaced = server.pid() != first;
+            // The replacement keeps the limit: it gives up on HARD in time.
+            let again = server.attempt(&smt(HARD)).verdict;
+            assert_eq!(again, Verdict::Unproved);
+            (unknown, kept, lifted, replaced, server.attempt(&smt(VALID_X)).verdict)
+        });
+        assert_eq!(unknown, Verdict::Unproved);
+        assert!(kept, "an unknown is a clean answer: the session is kept");
+        assert_eq!(lifted, Verdict::Unproved);
+        assert!(replaced, "the session cut off at its deadline was kept");
+        assert!(after.is_proved(), "{after:?}");
+    }
+
     /// Goals that would wedge the session — leave a string or quoted symbol
     /// open (swallowing the marker), send z3's answers elsewhere, end z3,
     /// or read a file — are refused at once, and the session decides on.