diff --git a/source/air/src/bisect.rs b/source/air/src/bisect.rs index cbbef5ef47..fb35417d93 100644 --- a/source/air/src/bisect.rs +++ b/source/air/src/bisect.rs @@ -218,6 +218,12 @@ impl Answer { } } + /// The solver cancelled the check at a wall-clock cap + /// (`Prober::set_probe_timeout`), so the probe says nothing. + pub fn timed_out(&self) -> bool { + matches!(self, Answer::Unknown(reason) if reason == "timeout") + } + /// The classes a `Changed` search tells apart: the result, and for /// `unknown` whether the solver ran out of budget or gave up. pub fn class(&self) -> &'static str { @@ -309,6 +315,8 @@ pub struct Prober<'c> { context: &'c mut Context, units: Vec, checks: usize, + /// Wall-clock cap per probe, in milliseconds (see `set_probe_timeout`). + probe_timeout_ms: Option, /// The switch that turns every goal into `false` (ablation only). vacuity: Option, /// The scope was opened with `Context::push`, so the AIR logs saw it too. @@ -355,7 +363,14 @@ impl Context { match assert_switchable(self, &query, facts, None) { Ok(mut units) => { units.sort_by_key(|u| u.sort_key()); - Ok(Prober { context: self, units, checks: 0, vacuity: None, air_scope: false }) + Ok(Prober { + context: self, + units, + checks: 0, + probe_timeout_ms: None, + vacuity: None, + air_scope: false, + }) } Err(err) => { self.pop_name_scope(); @@ -394,6 +409,7 @@ impl Context { context: self, units, checks: 0, + probe_timeout_ms: None, vacuity: Some(vacuity), air_scope: true, }) @@ -537,6 +553,13 @@ impl<'c> Prober<'c> { } /// Ask the solver about the query with `disabled[i]` switching off + /// Cancel any probe that runs longer than `ms` milliseconds of wall-clock + /// time: it answers `unknown` with reason `timeout` (`Answer::timed_out`), + /// which the searches take as not valid. `None` lifts the cap. + pub fn set_probe_timeout(&mut self, ms: Option) { + self.probe_timeout_ms = ms; + } + /// `units()[i]`, under the query's resource budget. An `Err` carries /// solver output this could not read. pub fn probe(&mut self, disabled: &[bool]) -> Result { @@ -585,6 +608,7 @@ impl<'c> Prober<'c> { let var = ident_var(switch); literals.push(if vacuous { var } else { mk_not(&var) }); } + let probe_timeout_ms = self.probe_timeout_ms; let context = &mut *self.context; let detailed = detailed && matches!(context.solver, SmtSolver::Cvc5); match context.solver { @@ -597,6 +621,9 @@ impl<'c> Prober<'c> { context.smt_log.log_set_option("reproducible-resource-limit", &budget.to_string()); } } + if probe_timeout_ms.is_some() { + context.set_check_timeout(probe_timeout_ms); + } context.smt_log.log_check_sat_assuming(&literals); if detailed { // in the same batch, right after the answer it describes @@ -614,6 +641,9 @@ impl<'c> Prober<'c> { } SmtSolver::Cvc5 => context.smt_log.log_set_option("reproducible-resource-limit", "0"), } + if probe_timeout_ms.is_some() { + context.set_check_timeout(None); + } let mut answer = None; let mut detail = ProbeDetail::default(); for line in output { diff --git a/source/air/src/context.rs b/source/air/src/context.rs index c18b6904be..3829f8a4d0 100644 --- a/source/air/src/context.rs +++ b/source/air/src/context.rs @@ -1113,6 +1113,20 @@ impl Context { crate::smt_verify::cvc5_query_budget(self) } + /// Bound each following `check-sat`'s wall-clock time to `ms` + /// milliseconds (cvc5's `tlimit-per`, z3's `timeout`): a check that + /// reaches it is cancelled by the solver and answers `unknown` with + /// reason `timeout`. `None` lifts the bound. The option goes to the + /// solver with the next commands sent, and stays until set again. + pub fn set_check_timeout(&mut self, ms: Option) { + let ms = ms.unwrap_or(0).to_string(); + let option = match self.solver { + SmtSolver::Z3 => "timeout", + SmtSolver::Cvc5 => "tlimit-per", + }; + self.smt_log.log_set_option(option, &ms); + } + /// Ask the solver for the instantiation graph of its last `check-sat` and /// return its reply lines (cvc5 with `set_inst_graph` only). Read-only: /// call it after a query's answer and before anything that checks again. diff --git a/source/rust_verify/src/resident.rs b/source/rust_verify/src/resident.rs index 84e6231bd7..04e9282ecd 100644 --- a/source/rust_verify/src/resident.rs +++ b/source/rust_verify/src/resident.rs @@ -235,6 +235,17 @@ enum Request { /// candidates. Lets a caller search past a witness the absence /// check disowned. exclude: Option>, + /// Resource limit for each probe, in `#[verifier::rlimit]` units, + /// above 0 and at most `MAX_RUNG_RLIMIT`. Default: the query's own. + /// A diagnostic budget for the probes alone: the absence check, an + /// ordinary check of the witness, keeps the query's own limit, as + /// does every other request. + rlimit: Option, + /// Wall-clock cap per probe, in milliseconds. A probe that reaches + /// it is cancelled by the solver (it answers `unknown`, reason + /// `timeout`, and the search takes it as not valid), is listed in + /// `skipped_probes`, and the reply is marked `partial`. + probe_timeout_ms: Option, }, Egraph { session: String, @@ -1374,6 +1385,13 @@ struct AblateReport { probes: Vec, elapsed_ms: u128, restore_ms: u128, + /// Some probe was cancelled at the request's `probe_timeout_ms`, so the + /// witness is what the other probes established: possibly not minimal, + /// and confirmed only as far as `skipped_probes` allows. + partial: bool, + /// The probes cancelled at the wall-clock cap, by what they asked. + #[serde(skip_serializing_if = "Vec::is_empty")] + skipped_probes: Vec, } struct AblateRequest { @@ -1381,6 +1399,10 @@ struct AblateRequest { budget: usize, hypotheses: bool, exclude: Vec, + /// The probes' own resource limit; `None` keeps the query's. + rlimit: Option, + /// Wall-clock cap per probe. + probe_timeout_ms: Option, } /// A goal the vacuity probes name. @@ -1421,6 +1443,8 @@ fn scan_vacuity( goals: &[usize], removed: &[usize], checks: &mut usize, + skipped: &mut Vec, + label: &str, ) -> Result { use air::bisect::Answer; let count = prober.units().len(); @@ -1434,6 +1458,9 @@ fn scan_vacuity( if goals.is_empty() { let answer = prober.probe_vacuity(&mask(removed))?; *checks += 1; + if answer.timed_out() { + skipped.push(format!("{label} vacuity probe")); + } return Ok(VacuityScan { answer, goal: None, unchecked: 0 }); } let mut unknown = None; @@ -1448,6 +1475,9 @@ fn scan_vacuity( off.extend(goals.iter().copied().filter(|&g| g != goal)); let answer = prober.probe_vacuity(&mask(&off))?; *checks += 1; + if answer.timed_out() { + skipped.push(format!("{label} vacuity probe of goal {goal}")); + } if answer == Answer::Valid { return Ok(VacuityScan { answer, goal: Some(goal), unchecked: 0 }); } @@ -1476,14 +1506,21 @@ fn ablate( query: &RetainedQuery, symbols: Option<&crate::provenance::Symbols>, request: AblateRequest, + set_rlimit: &impl Fn(&mut Context, f32), ) -> io::Result { use air::bisect::{Answer, Mode, ProbeDetail, Status, Target, UnitKind}; let group_of = |axiom: &air::ast::Axiom| -> Option { symbols.and_then(|symbols| symbols.axiom_group(axiom)).map(str::to_owned) }; + // The probes' budget: their own rlimit when the request gives one, and + // a wall-clock cap each. The absence check below runs at the query's. + set_rlimit(air, request.rlimit.unwrap_or(query.rlimit)); let mut prober = air .ablate_query(prefix, &mut |axiom| group_of(axiom), &query.query) .map_err(|error| io::Error::other(error.to_string()))?; + prober.set_probe_timeout(request.probe_timeout_ms); + // Probes the solver cancelled at the cap, by what they asked. + let mut skipped: Vec = Vec::new(); let units = prober.units().to_vec(); let count = units.len(); let no_candidate = |&&i: &&usize| { @@ -1514,6 +1551,9 @@ fn ablate( }; let mut details: HashMap, ProbeDetail> = HashMap::new(); let (before, detail) = prober.probe_detailed(&mask(&[])).map_err(io::Error::other)?; + if before.timed_out() { + skipped.push("probe with nothing removed".to_owned()); + } details.insert(Vec::new(), detail); let mode = match request.mode { AblateMode::Auto if before == Answer::Valid => AblateMode::LoadBearing, @@ -1561,7 +1601,11 @@ fn ablate( Some(before), &mut |disabled| -> Result { let (answer, detail) = prober.probe_detailed(disabled)?; - details.insert(switched_off(disabled), detail); + let removed = switched_off(disabled); + if answer.timed_out() { + skipped.push(format!("search probe with {removed:?} removed")); + } + details.insert(removed, detail); Ok(answer) }, ) @@ -1578,13 +1622,15 @@ fn ablate( let goals: Vec = (0..count).filter(|&i| units[i].kind == UnitKind::Goal).rev().collect(); let mut extra_checks = 0; let vacuity_before = - scan_vacuity(&mut prober, &goals, &[], &mut extra_checks).map_err(io::Error::other)?; + scan_vacuity(&mut prober, &goals, &[], &mut extra_checks, &mut skipped, "before") + .map_err(io::Error::other)?; let mut vacuity_witness = None; let mut participated = Vec::new(); let mut participation_unchecked = 0; if let Some(removed) = &witness_removed { - let scan = scan_vacuity(&mut prober, &goals, removed, &mut extra_checks) - .map_err(io::Error::other)?; + let scan = + scan_vacuity(&mut prober, &goals, removed, &mut extra_checks, &mut skipped, "witness") + .map_err(io::Error::other)?; // A removal leaves its members out of the contradiction by // definition; only kept members can take part in it. Each is tried // at the goal the scan found contradictory. @@ -1601,6 +1647,9 @@ fn ablate( without.push(member); let answer = prober.probe_vacuity(&mask(&without)).map_err(io::Error::other)?; extra_checks += 1; + if answer.timed_out() { + skipped.push(format!("participation probe of unit {member}")); + } if answer != Answer::Valid { participated.push(member); } @@ -1622,18 +1671,35 @@ fn ablate( Some(removed) => { let answer = prober.probe_vacuity(&mask(&removed)).map_err(io::Error::other)?; extra_checks += 1; + if answer.timed_out() { + skipped.push("every-goal vacuity probe".to_owned()); + } Some(answer) } None => None, }; drop(prober); + // The absence check is an ordinary check of the witness: the query's + // own rlimit, which every later request expects to find, under the + // same wall-clock cap. + set_rlimit(air, query.rlimit); let absence_check = match &witness_removed { Some(removed) => { let probed_valid = outcome.after == Some(Answer::Valid); - let check = - absence_check(air, prefix, query, &group_of, &units, removed, probed_valid)?; + air.set_check_timeout(request.probe_timeout_ms); + let checked = + absence_check(air, prefix, query, &group_of, &units, removed, probed_valid); + if request.probe_timeout_ms.is_some() { + air.set_check_timeout(None); + } + let check = checked?; extra_checks += 1; + if check.result == QueryResult::ResourceLimit + && request.probe_timeout_ms.is_some_and(|ms| check.elapsed_ms >= ms as u128) + { + skipped.push("absence check".to_owned()); + } Some(check) } None => None, @@ -1789,6 +1855,8 @@ fn ablate( .collect(), elapsed_ms: 0, restore_ms: 0, + partial: !skipped.is_empty(), + skipped_probes: skipped, }) } @@ -5153,6 +5221,8 @@ impl Server { budget_checks, hypotheses, exclude, + rlimit, + probe_timeout_ms, .. } => { let Some(bucket) = self.buckets.get(bucket_id.0) else { @@ -5171,6 +5241,20 @@ impl Server { )?; continue; } + if rlimit.is_some_and(|r| !(r.is_finite() && r > 0.0 && r <= MAX_RUNG_RLIMIT)) { + send( + &mut output, + &Response::Error { message: "rlimit must be above 0 and at most 1000" }, + )?; + continue; + } + if probe_timeout_ms == Some(0) { + send( + &mut output, + &Response::Error { message: "probe_timeout_ms must be positive" }, + )?; + continue; + } let mut state = match bucket.state.lock() { Ok(state) => state, Err(_) => { @@ -5192,16 +5276,39 @@ impl Server { let restore_ms = restore_start.elapsed().as_millis(); let query = &journal.queries[local]; let prefix = journal.prefix_decls(query.prefix); - set_rlimit(air, query.rlimit); + // A probe budget too small for one cvc5 unit converts to + // 0, which cvc5 takes as no limit, as the ladder refuses. + if let Some(probe_rlimit) = rlimit { + set_rlimit(air, probe_rlimit); + let empty = air.cvc5_query_budget() == 0; + set_rlimit(air, query.rlimit); + if empty { + send( + &mut output, + &Response::Error { + message: "rlimit is below one cvc5 resource unit", + }, + )?; + continue; + } + } let request = AblateRequest { mode, budget, hypotheses: hypotheses.unwrap_or(true), exclude: exclude.unwrap_or_default(), + rlimit, + probe_timeout_ms, }; let start = Instant::now(); - let report = match ablate(air, &prefix, query, bucket.symbols.as_ref(), request) - { + let report = match ablate( + air, + &prefix, + query, + bucket.symbols.as_ref(), + request, + &set_rlimit, + ) { Ok(mut report) => { report.elapsed_ms = start.elapsed().as_millis(); report.restore_ms = restore_ms; diff --git a/source/rust_verify_test/tests/resident.rs b/source/rust_verify_test/tests/resident.rs index c42664f14e..6891a76223 100644 --- a/source/rust_verify_test/tests/resident.rs +++ b/source/rust_verify_test/tests/resident.rs @@ -821,6 +821,77 @@ fn resident_ablation_finds_witnesses_and_leaves_the_session_unchanged() { } } +/// Ablation probes take a budget of their own: an `rlimit` for the probes +/// alone, which the absence check and every later request do not see, and a +/// wall-clock cap per probe past which the solver cancels the probe, which +/// is then listed as skipped and marks the reply partial. +#[test] +fn resident_ablation_probes_take_their_own_budget() { + let mut worker = Worker::start(ABLATE_SOURCE, &["--rlimit", "2"]); + let ready = worker.receive(); + let session = ready["session"].clone(); + let request = |name: &str, extra: Value| -> Value { + let mut request = json!({ + "command": "ablate", "session": session, "bucket": 0, "query": query_id(&ready, name), + }); + request.as_object_mut().unwrap().extend(extra.as_object().unwrap().clone()); + request + }; + // Both fields are taken; a generous cap skips nothing. + let reply = worker.send(request( + "::quad_is_four", + json!({"mode": "load_bearing", "rlimit": 4.0, "probe_timeout_ms": 600_000}), + )); + assert_eq!(reply["event"], "ablated", "{reply}"); + assert_eq!(reply["result"], "load_bearing_set", "{reply}"); + assert_eq!(reply["partial"], false, "{reply}"); + assert!(reply.get("skipped_probes").is_none(), "{}", reply); + // A bad budget is refused without ending the session. + for extra in [ + json!({"rlimit": 0}), + json!({"rlimit": 5000}), + json!({"rlimit": 1e-9}), + json!({"probe_timeout_ms": 0}), + ] { + let refused = worker.send(request("::quad_is_four", extra.clone())); + assert_eq!(refused["event"], "error", "{extra}: {refused}"); + } + // A cap of one millisecond: whatever the solver manages in that time, + // every probe it cancelled is listed, and the reply says it is partial + // exactly when some probe was. + let reply = worker.send(request( + "::buried", + json!({"mode": "minimal_removal", "budget_checks": 2, "probe_timeout_ms": 1}), + )); + assert_eq!(reply["event"], "ablated", "{reply}"); + let skipped = reply["skipped_probes"].as_array().map_or(0, Vec::len); + assert_eq!(reply["partial"], skipped > 0, "{reply}"); + if skipped > 0 { + assert!(reply.to_string().contains("timeout"), "{}", reply); + } + // The session answers as before: the probes' rlimit did not stick. + let check = worker.send(json!({"command": "check", "session": session, "bucket": 0, + "query": query_id(&ready, "::quad_is_four")})); + assert_eq!(check["result"], "valid", "{check}"); + assert_eq!(worker.send(json!({"command": "close", "session": session}))["event"], "closed"); + worker.finish(false); + // The solvers saw exactly two budgets: the session's, and twice it for + // the probes that asked for rlimit 4. + let budgets = resource_budgets(&smt_logs(worker.dir.path())); + assert_eq!(budgets.len(), 2, "{budgets:?}"); + let (low, high) = (*budgets.iter().next().unwrap(), *budgets.iter().last().unwrap()); + assert_eq!(high, low * 2, "{budgets:?}"); + for log in smt_logs(worker.dir.path()) { + assert_eq!(log.matches("(push").count(), log.matches("(pop").count()); + // The cap is lifted after every probe it bounded. + assert_eq!( + log.matches("(set-option :tlimit-per 1)").count() + + log.matches("(set-option :tlimit-per 600000)").count(), + log.matches("(set-option :tlimit-per 0)").count() + ); + } +} + const TWIN_SOURCE: &str = r#" use vstd::prelude::*; verus! {