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.