From 4a137b3cddc975e3e68b1427992f71151800f6bd Mon Sep 17 00:00:00 2001 From: Transaction Science Date: Tue, 13 Oct 2026 03:01:42 -0400 Subject: [PATCH] proof-solvers: a time limit on every z3 goal, and a deadline on its I/O The resident z3 session had no limit. One goal z3 could not decide held the session, and every goal queued behind it, for as long as z3 kept at it. Two guards now close that, in the resident session and the one-shot z3 alike: - z3's own soft limit (`-t:`, GOAL_TIMEOUT = 60 s by default; Z3Server::with_goal_timeout). At the limit `(check-sat)` answers `unknown`, which counts as undecided, and the session decides on. - A deadline GOAL_DEADLINE_GRACE (5 s) past that limit, on both the write and the read. A goal can lift z3's limit for itself with `(set-option :timeout ...)`. Past the deadline the one-shot z3 is killed, and the resident session is broken and replaced. z3 reads its input only as it reaches each command. So a goal with a `(check-sat)` of its own and more than a pipe's worth of text after it blocked the write on the calling thread for as long as that check ran. Both ends of the pipe are now on threads of their own. Checked on Homebrew z3 (build host) and on Ubuntu's 4.8.12 (the CI image's version): unknown at the soft limit, the limit lifted by a goal's :timeout even after (reset), and a 426 KB write that blocks behind the goal's own check. Co-Authored-By: Claude Opus 5.5 --- .../proof-rs/crates/proof-solvers/src/lib.rs | 322 +++++++++++++++--- 1 file changed, 282 insertions(+), 40 deletions(-) diff --git a/proof/proof-rs/crates/proof-solvers/src/lib.rs b/proof/proof-rs/crates/proof-solvers/src/lib.rs index 47e65db52..f30e4ebf7 100644 --- a/proof/proof-rs/crates/proof-solvers/src/lib.rs +++ b/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 { - 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 { + 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 { + 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, marker: &str) -> O /// never as proof. fn run_z3(script: &str) -> Option { 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 { 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, + /// Scripts for `z3`'s stdin, to the session's writer thread. + scripts: mpsc::Sender, + /// `z3`'s stdout, a line at a time, from the session's reader thread. + lines: mpsc::Receiver, + /// 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 { + /// A session on `z3`, each goal limited to `timeout` (see [`Z3Session`]). + fn spawn(z3: &Path, timeout: Duration) -> Option { 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::(); + // 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 { 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, + /// 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) -> Option { + fn start(settle_bound: Option, goal_timeout: Duration) -> Option { 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. -- 2.54.0 (Apple Git-157)