diff --git a/source/air/src/air_observer.rs b/source/air/src/air_observer.rs new file mode 100644 index 0000000000..59857e3efc --- /dev/null +++ b/source/air/src/air_observer.rs @@ -0,0 +1,59 @@ +//! AIR-level verification pipeline observer. +//! +//! Defines `AirObserver` — the interface for observing the AIR-level +//! verification pipeline: query lowering, WP version creation, and lambda / +//! choose / axiom declarations. +//! +//! This trait is independent: it does **not** require any other observer +//! trait. Query *results* are observed separately via `QueryResultObserver` +//! (`query_result_observer.rs`), and VIR→AIR lowering via `VirObserver` +//! (`vir/src/vir_observer.rs`). A consumer implements only the traits it needs. + +use crate::ast::{Decl, Expr, Ident, Query, Snapshots}; +use std::any::Any; + +/// Origin of a WP versioned constant created during `lower_query`. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum VersionOrigin { + /// From a `StmtX::Havoc` — unconstrained new version (loop entry). + Havoc, + /// From a `StmtX::Assign` — constrained new version (= rhs). + Assign, +} + +/// Observer for the AIR-level verification pipeline. +/// +/// All methods have default no-op implementations except `as_any` +/// and `as_any_mut` which must be implemented (trivially: `self`). +pub trait AirObserver: Any + Send { + /// A verification query has been lowered (variables → versioned constants). + fn on_query_lowered(&mut self, _query: &Query, _snapshots: &Snapshots, _local_vars: &[Decl]) {} + + /// Called from `lower_query` at the moment a new WP version is created. + /// + /// The Nth call for base variable `x` corresponds to the Nth VIR-level + /// `on_havoc` or `on_assign` callback for `x`. Branch and break merges + /// create no versions: a merge takes the highest version a branch reached, + /// which that branch already created. + /// + /// See `VersionCorrelator` in `vir/src/vir_observer.rs` for a shared helper + /// that correlates these callbacks with VIR-level data. + fn on_wp_version_created(&mut self, _versioned: &Ident, _kind: VersionOrigin) {} + + /// A lambda definition was declared (%%lambda%%N). + fn on_lambda_decl(&mut self, _name: &Ident, _params: &[Ident], _body: &Expr) {} + + /// A choose binder name was declared (%%choose%%N). + fn on_choose_decl(&mut self, _name: &Ident, _binder_name: &Ident) {} + + /// An axiom declaration was processed (for accumulating function definitions). + fn on_axiom_decl(&mut self, _expr: &Expr) {} + + fn as_any(&self) -> &dyn Any; + fn as_any_mut(&mut self) -> &mut dyn Any; +} + +/// A shared handle to an `AirObserver`. `Arc>` rather than +/// `Rc>` because an `air::Context` holding one must stay `Send`: +/// resident sessions keep contexts in a `Mutex` served from other threads. +pub type AirObserverHandle = std::sync::Arc>; diff --git a/source/air/src/ast.rs b/source/air/src/ast.rs index c2325c9b0c..8d99352dba 100644 --- a/source/air/src/ast.rs +++ b/source/air/src/ast.rs @@ -9,8 +9,8 @@ pub type TypeError = String; pub type Ident = Arc; -pub(crate) type Snapshot = IndexMap; -pub(crate) type Snapshots = HashMap; +pub type Snapshot = IndexMap; +pub type Snapshots = HashMap; pub type Typ = Arc; pub type Typs = Arc>; diff --git a/source/air/src/bisect.rs b/source/air/src/bisect.rs index fb35417d93..06bce638f6 100644 --- a/source/air/src/bisect.rs +++ b/source/air/src/bisect.rs @@ -337,7 +337,7 @@ pub struct ProbeDetail { /// its switch (declared among the query's locals). fn prepare(context: &mut Context, query: &Query) -> Result<(Query, Vec), TypeError> { let query = crate::typecheck::check_query(context, query)?; - let (query, _, _, _) = crate::var_to_const::lower_query(&query, false); + let (query, _, _, _) = crate::var_to_const::lower_query(&query, false, None); let mut facts = Vec::new(); let assertion = mark_facts(&query.assertion, &mut facts); let mut local = (*query.local).clone(); diff --git a/source/air/src/block_to_assert.rs b/source/air/src/block_to_assert.rs index d6f4b89f06..da39c25919 100644 --- a/source/air/src/block_to_assert.rs +++ b/source/air/src/block_to_assert.rs @@ -77,7 +77,12 @@ fn stmt_to_expr(label_n: &mut u64, locals: &mut Vec, stmt: &Stmt, pred: Ex } } -pub(crate) fn lower_query( +/// Lower a block-structured query to assert form. +/// +/// Re-exported as `air::lower_query` so a consumer that reconstructs the verification +/// condition can apply the same lowering the solver sees. `AirObserver::on_query_lowered` +/// fires before this step. +pub fn lower_query( message_interface: &dyn crate::messages::MessageInterface, query: &Query, ) -> Query { diff --git a/source/air/src/closure.rs b/source/air/src/closure.rs index b4a3673e07..b1838273b8 100644 --- a/source/air/src/closure.rs +++ b/source/air/src/closure.rs @@ -314,6 +314,10 @@ fn simplify_lambda( let closure_fun = Arc::new(name); ctxt.lambda_count += 1; let _ = ctxt.lambda_map.insert(closure, closure_fun.clone()); + if let Some(obs) = &ctxt.air_observer { + let params: Vec = binders.iter().map(|b| b.name.clone()).collect(); + obs.lock().unwrap().on_lambda_decl(&closure_fun, ¶ms, &e1); + } // f(holes): (Fun (t_params) t_body) let decl = Arc::new(DeclX::Fun(closure_fun.clone(), holes.clone(), typ.clone())); @@ -418,6 +422,14 @@ fn simplify_choose( let closure_fun = Arc::new(name); ctxt.choose_count += 1; let _ = ctxt.choose_map.insert(closure, closure_fun.clone()); + if let Some(obs) = &ctxt.air_observer { + let binder_name = binders + .iter() + .next() + .map(|b| b.name.clone()) + .unwrap_or_else(|| Arc::new("_".to_string())); + obs.lock().unwrap().on_choose_decl(&closure_fun, &binder_name); + } // f(holes): typ_body let decl = Arc::new(DeclX::Fun(closure_fun.clone(), holes.clone(), typ_body.clone())); diff --git a/source/air/src/context.rs b/source/air/src/context.rs index dd5fbef16b..a9b3c59cfa 100644 --- a/source/air/src/context.rs +++ b/source/air/src/context.rs @@ -541,6 +541,9 @@ pub struct Context { name_counters: Vec, pub(crate) typing: Typing, pub(crate) debug: bool, + pub(crate) air_observer: Option, + pub(crate) query_result_observer: + Option, pub(crate) ignore_unexpected_smt: bool, pub(crate) rlimit: u32, pub(crate) air_initial_log: Emitter, @@ -687,6 +690,8 @@ impl Context { solver: solver.clone(), }, debug: false, + air_observer: None, + query_result_observer: None, ignore_unexpected_smt: false, rlimit: 0, air_initial_log: Emitter::new( @@ -806,6 +811,24 @@ impl Context { self.get_smt_process().send_commands(smt_data) } + /// Register observers for AIR passes and for solver results. Either may be `None`; + /// with none registered every observer hook is a no-op. + pub fn set_observers( + &mut self, + air_observer: Option, + query_result_observer: Option, + ) { + self.air_observer = air_observer; + self.query_result_observer = query_result_observer; + } + + /// The query-result observer `set_observers` registered, if any. + pub fn query_result_observer( + &self, + ) -> Option<&crate::query_result_observer::QueryResultObserverHandle> { + self.query_result_observer.as_ref() + } + pub fn set_air_initial_log(&mut self, writer: Box) { self.air_initial_log.set_log(Some(writer)); } @@ -1555,11 +1578,22 @@ impl Context { return ValidityResult::TypeError(err); } }; - let (query, snapshots, local_vars, variable_versions) = crate::var_to_const::lower_query( - &query, - self.provenance || self.egraph_request.is_some() || self.speculation.is_some(), - ); + let (query, snapshots, local_vars, variable_versions) = { + // Scope the borrow so it is released before `on_query_lowered` below + // (both use the same shared observer handle — no reentrant borrow). + let mut guard = self.air_observer.as_ref().map(|o| o.lock().unwrap()); + let obs_ref = + guard.as_mut().map(|g| &mut **g as &mut dyn crate::air_observer::AirObserver); + crate::var_to_const::lower_query( + &query, + self.provenance || self.egraph_request.is_some() || self.speculation.is_some(), + obs_ref, + ) + }; self.variable_versions = variable_versions; + if let Some(o) = &self.air_observer { + o.lock().unwrap().on_query_lowered(&query, &snapshots, &local_vars); + } self.air_middle_log.log_query(&query); let query = crate::block_to_assert::lower_query(message_interface, &query); self.air_final_log.log_query(&query); @@ -1630,6 +1664,40 @@ impl Context { smt_output[0].clone() } + /// Evaluate an AIR expression against the current solver model as a boolean. + /// Returns `Some(true)` / `Some(false)` if the solver returns a boolean, + /// `None` if the expression is non-boolean or evaluation fails. + pub fn evaluate_bool(&mut self, expr: &crate::ast::Expr) -> Option { + let printer = + crate::printer::Printer::new(self.message_interface.clone(), true, self.solver.clone()); + let node = printer.expr_to_node(expr); + // A compound value (a quantified formula, a datatype constructor) + // may span several lines; it is never a boolean, so it reads as None. + match self.solver { + SmtSolver::Z3 => { + self.smt_log.log_eval(node); + let smt_data = self.smt_log.take_pipe_data(); + match self.get_smt_process().send_commands(smt_data).as_slice() { + [line] if line == "true" => Some(true), + [line] if line == "false" => Some(false), + _ => None, + } + } + // cvc5 has no `eval`: it takes the command for an unknown one + // and the reader loses its place in the solver's output. + // `get-value` answers `((expr value))` on one line. + SmtSolver::Cvc5 => { + self.smt_log.log_get_value(node); + let smt_data = self.smt_log.take_pipe_data(); + match self.get_smt_process().send_commands(smt_data).as_slice() { + [line] if line.ends_with(" true))") => Some(true), + [line] if line.ends_with(" false))") => Some(false), + _ => None, + } + } + } + } + pub fn command( &mut self, message_interface: &dyn crate::messages::MessageInterface, diff --git a/source/air/src/emitter.rs b/source/air/src/emitter.rs index 7156b399d5..9c5bf3f170 100644 --- a/source/air/src/emitter.rs +++ b/source/air/src/emitter.rs @@ -273,4 +273,12 @@ impl Emitter { self.log_node(&nodes!(eval { expr })); } } + + /// `(get-value (expr))`: the standard spelling of `eval`, which cvc5 + /// answers and z3's `eval` extension does not require. + pub fn log_get_value(&mut self, expr: Node) { + if !self.is_none() { + self.log_node(&nodes!(get-value { Node::List(vec![expr]) })); + } + } } diff --git a/source/air/src/lib.rs b/source/air/src/lib.rs index 81acd8d1b0..a57e595ff3 100644 --- a/source/air/src/lib.rs +++ b/source/air/src/lib.rs @@ -1,3 +1,4 @@ +pub mod air_observer; pub mod ast; pub mod ast_util; pub mod bisect; @@ -10,6 +11,7 @@ pub mod messages; pub mod model; pub mod parser; pub mod profiler; +pub mod query_result_observer; pub mod remove_asserts; pub mod scope_map; pub mod smt_process; @@ -21,6 +23,7 @@ pub mod printer; pub mod scaffold; mod block_to_assert; +pub use block_to_assert::lower_query; mod closure; pub mod def; mod smt_verify; @@ -29,7 +32,7 @@ mod typecheck; mod util; mod var_to_const; pub use var_to_const::GoalScope; -mod visitor; +pub mod visitor; #[cfg(feature = "singular")] pub mod singular_manager; diff --git a/source/air/src/query_result_observer.rs b/source/air/src/query_result_observer.rs new file mode 100644 index 0000000000..a14fc207fd --- /dev/null +++ b/source/air/src/query_result_observer.rs @@ -0,0 +1,70 @@ +//! Query-result observer. +//! +//! Defines `QueryResultObserver` — the interface for observing the outcome of +//! each verification query (`Invalid` / `Valid` / `Timeout`), including live +//! model evaluation on `Invalid`. +//! +//! This trait is independent: it does **not** require `AirObserver` or +//! `VirObserver`. A consumer that only cares about verification outcomes +//! implements this trait alone. +//! +//! **`Invalid` is an interactive, live-window callback** — the one deliberate +//! exception to "observers are passive." Alongside the counterexample model +//! (`model_defs`), it hands the observer `eval_bool_expr`, a closure that +//! evaluates a boolean AIR expression against the *live* solver model. The model is +//! only valid for the duration of the callback: the core discovers the failing +//! assertion, invokes the observer, and only then disables the assertion label +//! (which invalidates the model); see `smt_check_assertion` in `smt_verify.rs`. + +use crate::ast::{Expr, Ident}; +use crate::messages::ArcDynMessage as Message; +use crate::model::ModelDef; +use std::any::Any; +use std::collections::HashMap; + +/// Verification result passed to the observer after each query. +pub enum CheckValidResult<'a> { + Invalid { + /// The parsed counterexample model (concrete symbol assignments). + /// Built by the core for its own error reporting; exposed here for free. + model_defs: &'a HashMap, + /// Evaluate a boolean AIR expression against the live solver model. + /// Returns `Some(bool)` for a boolean result, `None` for a non-boolean + /// expression or one the model cannot evaluate. Valid only during this + /// callback (the model is torn down afterward). + eval_bool_expr: &'a mut dyn FnMut(&Expr) -> Option, + assert_id: &'a Option, + error: &'a Message, + }, + /// The query was discharged (unsat). Carries the ids of every assertion the query + /// checked, so a consumer can attribute the success to specific obligations. There is no + /// model: nothing to evaluate against. + Valid { + assert_ids: &'a [Option], + /// What the solver used to discharge the query (currently the unsat core as the set + /// of named axioms), when usage reporting is enabled (`-V axiom-usage-info`); + /// `UsageInfo::None` otherwise. Computed by the core for its own reporting and exposed + /// here for free. The type is the core's own, so richer usage data can be added there + /// without changing this interface. + usage_info: &'a crate::context::UsageInfo, + }, + Timeout { + assert_id: &'a Option, + }, +} + +/// Observer for verification query results. +/// +/// The single callback fires once per query after the solver returns. All +/// methods except `as_any`/`as_any_mut` have default no-op implementations. +pub trait QueryResultObserver: Any + Send { + /// A verification query completed with a result. + fn on_check_valid_result(&mut self, _result: &mut CheckValidResult) {} + + fn as_any(&self) -> &dyn Any; + fn as_any_mut(&mut self) -> &mut dyn Any; +} + +/// A shared handle to a `QueryResultObserver`; `Arc>` for the reason +/// given at `AirObserverHandle`. +pub type QueryResultObserverHandle = std::sync::Arc>; diff --git a/source/air/src/smt_verify.rs b/source/air/src/smt_verify.rs index aa36f01eaf..2549e25fb6 100644 --- a/source/air/src/smt_verify.rs +++ b/source/air/src/smt_verify.rs @@ -112,6 +112,9 @@ pub(crate) fn smt_add_decl<'ctx>(context: &mut Context, decl: &Decl) { let mut infos: Vec = Vec::new(); let mut axiom_infos: Vec = Vec::new(); let labeled_expr = label_asserts(context, &mut infos, &mut axiom_infos, &expr); + if let Some(obs) = &context.air_observer { + obs.lock().unwrap().on_axiom_decl(&labeled_expr); + } for info in axiom_infos { crate::typecheck::add_decl(context, &info.decl, true).unwrap(); context @@ -637,6 +640,14 @@ pub(crate) fn smt_check_assertion<'ctx>( match reason.expect("expected :reason-unknown") { SmtReasonUnknown::Canceled | SmtReasonUnknown::Unknown => { context.state = ContextState::Canceled; + // Notify observer of timeout/cancellation + if let Some(obs) = &context.query_result_observer { + obs.lock().unwrap().on_check_valid_result( + &mut crate::query_result_observer::CheckValidResult::Timeout { + assert_id: &None, + }, + ); + } ResultDetermination::Determined(ValidityResult::Canceled) } SmtReasonUnknown::Incomplete => ResultDetermination::Undetermined(false), @@ -655,24 +666,22 @@ pub(crate) fn smt_check_assertion<'ctx>( let smt_data = context.smt_log.take_pipe_data(); let smt_output = context.get_smt_process().send_commands(smt_data); - let mut smt_output = smt_output.into_iter(); - let unsat_core_str = - smt_output.next().expect("expected one line in the unsat core output"); - assert!(smt_output.next().is_none()); - - let fun_names: Vec = unsat_core_str - .strip_prefix('(') - .expect("invalid unsat core") - .strip_suffix(')') - .expect("invalid unsat core") - .split_terminator(' ') - .map(|x| Arc::new(x.to_owned())) - .collect(); - crate::context::UsageInfo::UsedAxioms(fun_names) + crate::context::UsageInfo::UsedAxioms(parse_unsat_core(&smt_output)) } else { crate::context::UsageInfo::None }; + if let Some(obs) = &context.query_result_observer { + let assert_ids: Vec> = + infos.iter().map(|info| info.assert_id.clone()).collect(); + obs.lock().unwrap().on_check_valid_result( + &mut crate::query_result_observer::CheckValidResult::Valid { + assert_ids: &assert_ids, + usage_info: &usage_info, + }, + ); + } + ValidityResult::Valid(usage_info) } ResultDetermination::Undetermined(false) => { @@ -1912,17 +1921,21 @@ fn smt_get_model( for def in model.iter() { model_defs.insert(def.name.clone(), def.clone()); } - for info in infos.iter_mut() { + // The `QueryResultObserver::Invalid` callback exposes a live model evaluator + // (`eval_bool_expr`), so the solver model must stay valid across the callback. + // Disabling the failing assertion's label invalidates the model, so that step is + // deferred: first discover the failing assertion, then notify the observer while + // the model is live, and only then disable the label for subsequent check-sats. + // The disable step runs whether or not an observer is registered. + // + // Discover the failing assertion without disabling the label. + let mut discovered_info_index: Option = None; + for (i, info) in infos.iter().enumerate() { if let Some(def) = model_defs.get(&info.label) { if *def.body == "true" { discovered_error = Some(info.clone()); discovered_assert_id = Some(info.assert_id.clone()); - - // Disable this label in subsequent check-sat calls to get additional errors - info.disabled = true; - let disable_label = mk_not(&ident_var(&info.label)); - context.smt_log.log_assert(&None, &None, &disable_label); - + discovered_info_index = Some(i); break; } } @@ -1956,6 +1969,31 @@ fn smt_get_model( let error = discovered_error.error; let e = context.message_interface.append_labels(&error, &discovered_additional_info); + + // Notify the observer while the solver model is still valid. + // eval_expr calls context.evaluate_bool() which sends (eval ...) to the solver. + // This only works before the label is disabled (which invalidates the model). + // Clone the shared handle so `context` stays free for the eval_bool_expr closure. + let obs = context.query_result_observer.clone(); + if let Some(obs) = &obs { + let assert_id = discovered_assert_id.clone().unwrap(); + obs.lock().unwrap().on_check_valid_result( + &mut crate::query_result_observer::CheckValidResult::Invalid { + model_defs: &model_defs, + eval_bool_expr: &mut |expr| context.evaluate_bool(expr), + assert_id: &assert_id, + error: &e, + }, + ); + } + + // Disable the label for subsequent check-sat calls (this invalidates the model). + if let Some(idx) = discovered_info_index { + infos[idx].disabled = true; + let disable_label = mk_not(&ident_var(&infos[idx].label)); + context.smt_log.log_assert(&None, &None, &disable_label); + } + context.state = ContextState::FoundInvalid(infos, Some(air_model.clone())); ValidityResult::Invalid(Some(air_model), Some(e), discovered_assert_id.unwrap()) } @@ -2060,6 +2098,53 @@ pub(crate) fn smt_check_query<'ctx>( result } +/// The names in a `(get-unsat-core)` reply. z3 prints the core on one line; +/// cvc5 puts one name per line. Names may be `|quoted|`. +pub(crate) fn parse_unsat_core(lines: &[String]) -> Vec { + let text = lines.join(" "); + let body = text + .trim() + .strip_prefix('(') + .and_then(|t| t.strip_suffix(')')) + .unwrap_or_else(|| panic!("invalid unsat core: {:?}", lines)); + let mut names = Vec::new(); + let mut rest = body.trim_start(); + while !rest.is_empty() { + let (name, tail) = match rest.strip_prefix('|') { + Some(quoted) => { + let end = + quoted.find('|').unwrap_or_else(|| panic!("invalid unsat core: {:?}", lines)); + ("ed[..end], "ed[end + 1..]) + } + None => { + let end = rest.find(char::is_whitespace).unwrap_or(rest.len()); + (&rest[..end], &rest[end..]) + } + }; + names.push(Arc::new(name.to_owned())); + rest = tail.trim_start(); + } + names +} + +#[cfg(test)] +mod unsat_core_tests { + use super::parse_unsat_core; + + fn names(lines: &[&str]) -> Vec { + let lines: Vec = lines.iter().map(|l| l.to_string()).collect(); + parse_unsat_core(&lines).iter().map(|n| n.to_string()).collect() + } + + #[test] + fn unsat_core_parses_one_line_and_one_name_per_line() { + assert_eq!(names(&["(a b)"]), ["a", "b"]); + assert_eq!(names(&["()"]), Vec::::new()); + assert_eq!(names(&["(", "a", "|b c|", ")"]), ["a", "b c"]); + assert_eq!(names(&["(a", "b)"]), ["a", "b"]); + } +} + #[cfg(test)] mod strategy_rung_tests { use super::parse_strategy_rung; diff --git a/source/air/src/var_to_const.rs b/source/air/src/var_to_const.rs index 7a5a6f18b8..f244c635bc 100644 --- a/source/air/src/var_to_const.rs +++ b/source/air/src/var_to_const.rs @@ -119,7 +119,7 @@ fn update_breaks_to_versions( } } -struct LowerStmtState { +struct LowerStmtState<'a> { decls: Vec, break_versions: HashMap>>, version_decls: HashSet, @@ -129,6 +129,7 @@ struct LowerStmtState { /// When kept, each assert reached, with the versions and snapshots in /// force there. goal_scopes: Option, GoalScope)>>, + observer: Option<&'a mut dyn crate::air_observer::AirObserver>, } /// The variable versions and snapshots in force at one assert of a query: @@ -145,7 +146,7 @@ impl GoalScope { /// occurrence; without a `goal`, or when no assert has it, the query's /// last assert; before any statement when it has none. pub fn of(query: &Query, goal: Option<&AssertId>) -> Self { - let (_, _, _, _, entry, scopes) = lower_query_with(query, false, true); + let (_, _, _, _, entry, scopes) = lower_query_with(query, false, true, None); let scopes = scopes.unwrap_or_default(); let wanted = goal.and_then(|goal| { scopes.iter().find(|(id, _)| id.as_ref().is_some_and(|id| **id == **goal)) @@ -168,8 +169,29 @@ impl GoalScope { } } +impl LowerStmtState<'_> { + /// Version `n` of `x` came into being as `versioned`: recorded for the + /// context's own readers when asked (`record_versions`), and announced to + /// the observer. The declared version 0 of each variable is recorded + /// where it is declared, before any statement. + fn notify_version_created( + &mut self, + x: &Ident, + n: u32, + versioned: &Ident, + kind: crate::air_observer::VersionOrigin, + ) { + if self.record_versions { + self.variable_versions.insert(versioned.to_string(), (x.to_string(), n)); + } + if let Some(obs) = &mut self.observer { + obs.on_wp_version_created(versioned, kind); + } + } +} + fn lower_stmt( - state: &mut LowerStmtState, + state: &mut LowerStmtState<'_>, versions: &mut IndexMap, snapshots: &mut Snapshots, types: &HashMap, @@ -188,18 +210,23 @@ fn lower_stmt( stmt } StmtX::Havoc(x) | StmtX::Assign(x, _) => { + let is_havoc = matches!(&*stmt, StmtX::Havoc(_)); let n = find_version(&versions, x); let typ = types[x].clone(); versions.insert(x.clone(), n + 1); - if state.record_versions { - state.variable_versions.insert(rename_var(x, n + 1), (x.to_string(), n + 1)); - } + let base = x; let x = Arc::new(rename_var(x, n + 1)); if !state.version_decls.contains(&x) { let decl = Arc::new(DeclX::Const(x.clone(), typ)); state.decls.push(decl); state.version_decls.insert(x.clone()); } + let kind = if is_havoc { + crate::air_observer::VersionOrigin::Havoc + } else { + crate::air_observer::VersionOrigin::Assign + }; + state.notify_version_created(base, n + 1, &x, kind); match &*stmt { StmtX::Assign(_, e) => { let expr1 = Arc::new(ExprX::Var(x)); @@ -275,9 +302,10 @@ fn lower_stmt( pub(crate) fn lower_query( query: &Query, record_versions: bool, + observer: Option<&mut dyn crate::air_observer::AirObserver>, ) -> (Query, Snapshots, Vec, crate::context::VariableVersions) { let (query, snapshots, local_vars, versions, _, _) = - lower_query_with(query, record_versions, false); + lower_query_with(query, record_versions, false, observer); (query, snapshots, local_vars, versions) } @@ -287,6 +315,7 @@ fn lower_query_with( query: &Query, record_versions: bool, record_goal_scopes: bool, + observer: Option<&mut dyn crate::air_observer::AirObserver>, ) -> ( Query, Snapshots, @@ -339,6 +368,7 @@ fn lower_query_with( variable_versions, record_versions, goal_scopes: record_goal_scopes.then(Vec::new), + observer, }; let entry = GoalScope { versions: versions.clone(), snapshots: snapshots.clone() }; let assertion = lower_stmt(&mut state, &mut versions, &mut snapshots, &types, assertion); @@ -370,14 +400,14 @@ mod tests { }) }; let (_, _, _, versions) = - lower_query(&query(vec![Arc::new(StmtX::Havoc(name.clone()))]), true); + lower_query(&query(vec![Arc::new(StmtX::Havoc(name.clone()))]), true, None); assert_eq!(versions.get("balance@0"), Some(&("balance@".into(), 0))); assert_eq!(versions.get("balance@1"), Some(&("balance@".into(), 1))); - let (_, _, _, versions) = lower_query(&query(vec![]), true); + let (_, _, _, versions) = lower_query(&query(vec![]), true, None); assert_eq!(versions.len(), 1); assert!(!versions.contains_key("balance@1")); let (_, _, _, versions) = - lower_query(&query(vec![Arc::new(StmtX::Havoc(name.clone()))]), false); + lower_query(&query(vec![Arc::new(StmtX::Havoc(name.clone()))]), false, None); assert!(versions.is_empty()); } @@ -419,4 +449,58 @@ mod tests { assert_eq!(read(None), ("y@1".to_string(), "y@1".to_string())); assert_eq!(read(Some(Arc::new(vec![7]))), ("y@1".to_string(), "y@1".to_string())); } + + /// A merge takes the highest version a branch reached, so every version + /// the lowered query declares was announced where a branch created it. + #[test] + fn merges_announce_no_versions_of_their_own() { + struct Announced(Vec<(String, crate::air_observer::VersionOrigin)>); + impl crate::air_observer::AirObserver for Announced { + fn on_wp_version_created( + &mut self, + versioned: &Ident, + kind: crate::air_observer::VersionOrigin, + ) { + self.0.push((versioned.to_string(), kind)); + } + fn as_any(&self) -> &dyn std::any::Any { + self + } + fn as_any_mut(&mut self) -> &mut dyn std::any::Any { + self + } + } + let x = Arc::new("x@".to_string()); + let havoc = || Arc::new(StmtX::Havoc(x.clone())); + let block = |ss: Vec| Arc::new(StmtX::Block(Arc::new(ss))); + let label = Arc::new("l".to_string()); + // a switch whose branches reach x@1 and x@2, then a breakable whose + // break leaves at x@3 and whose fallthrough reaches x@4 + let query = Arc::new(QueryX { + local: Arc::new(vec![Arc::new(DeclX::Var(x.clone(), Arc::new(crate::ast::TypX::Int)))]), + assertion: block(vec![ + Arc::new(StmtX::Switch(Arc::new(vec![ + block(vec![havoc()]), + block(vec![havoc(), havoc()]), + ]))), + Arc::new(StmtX::Breakable( + label.clone(), + block(vec![havoc(), Arc::new(StmtX::Break(label.clone())), havoc()]), + )), + ]), + }); + let mut announced = Announced(Vec::new()); + let (_, _, decls, _) = lower_query(&query, false, Some(&mut announced)); + let declared: Vec = decls + .iter() + .filter_map(|d| match &**d { + DeclX::Const(c, _) if **c != "x@0" => Some(c.to_string()), + _ => None, + }) + .collect(); + let names: Vec = announced.0.iter().map(|(n, _)| n.clone()).collect(); + assert_eq!(names, ["x@1", "x@1", "x@2", "x@3", "x@4"]); + assert!(declared.iter().all(|d| names.contains(d)), "{:?} vs {:?}", declared, names); + assert!(announced.0.iter().all(|(_, k)| *k == crate::air_observer::VersionOrigin::Havoc)); + } } diff --git a/source/air/src/visitor.rs b/source/air/src/visitor.rs index cba86c0043..f99f016694 100644 --- a/source/air/src/visitor.rs +++ b/source/air/src/visitor.rs @@ -1,7 +1,8 @@ use crate::ast::{BindX, Binder, BinderX, Expr, ExprX, Stmt, StmtX, Trigger}; use std::sync::Arc; -pub(crate) fn map_expr_visitor Expr>(expr: &Expr, f: &mut F) -> Expr { +/// Rebuild `expr` bottom-up, applying `f` to each node after its children. +pub fn map_expr_visitor Expr>(expr: &Expr, f: &mut F) -> Expr { match &**expr { ExprX::Const(_) => f(expr), ExprX::Var(_) => f(expr), diff --git a/source/rust_verify/src/config.rs b/source/rust_verify/src/config.rs index 9cc3c60854..66d4c5c61a 100644 --- a/source/rust_verify/src/config.rs +++ b/source/rust_verify/src/config.rs @@ -151,6 +151,7 @@ pub struct ArgsX { pub reach: Option, /// Serve retained AIR queries over stdin/stdout after compilation. pub resident: bool, + pub observers: Vec, } impl ArgsX { @@ -209,6 +210,7 @@ impl ArgsX { inst_pressure: Default::default(), reach: Default::default(), resident: false, + observers: Default::default(), } } } @@ -464,6 +466,7 @@ pub fn parse_args_with_imports( const EXTENDED_INST_PRESSURE: &str = "inst-pressure"; const EXTENDED_DIFFICULTY: &str = "difficulty"; const EXTENDED_TLA_EXPORT: &str = "tla-export"; + const EXTENDED_OBSERVERS: &str = "observers"; const EXTENDED_KEYS: &[(&str, &str)] = &[ ( EXTENDED_INST_PRESSURE, @@ -519,6 +522,10 @@ pub fn parse_args_with_imports( EXTENDED_NO_BV_SIMPLIFY, "internal option to disable simplification of bit-vector assertions before sending to the SMT solver", ), + ( + EXTENDED_OBSERVERS, + "Comma-separated observers: coverage and/or proof-state (reported in func-details under --output-json/--report-json)", + ), ]; let default_num_threads: usize = std::thread::available_parallelism() @@ -970,8 +977,19 @@ pub fn parse_args_with_imports( }, inst_pressure: extended.contains_key(EXTENDED_INST_PRESSURE), resident: matches.opt_present(OPT_RESIDENT), + observers: extended + .get(EXTENDED_OBSERVERS) + .and_then(|v| v.as_ref()) + .map(|s| s.split(',').map(|s| s.trim().to_string()).collect::>()) + .unwrap_or_default(), }; + if extended.contains_key(EXTENDED_OBSERVERS) { + if let Err(msg) = crate::observers::check_names(&args.observers) { + error(format!("-V {EXTENDED_OBSERVERS}: {msg}")); + } + } + if args.nl_frontier && !matches!(args.solver, SmtSolver::Cvc5) { error( "-V nl-frontier requires cvc5 (it is unavailable for vstd and internal test mode)" diff --git a/source/rust_verify/src/lib.rs b/source/rust_verify/src/lib.rs index c4d58cb467..b1dd58458d 100644 --- a/source/rust_verify/src/lib.rs +++ b/source/rust_verify/src/lib.rs @@ -52,6 +52,7 @@ pub mod file_loader; mod fn_call_to_vir; mod hir_hide_reveal_rewrite; mod import_export; +pub mod observers; pub mod profiler; mod provenance; mod reach; @@ -73,6 +74,7 @@ mod scaffold; #[cfg(feature = "singular")] pub mod singular; mod spans; +pub mod test_observer; pub mod trait_check; mod trait_check_ast; mod trait_check_emit; diff --git a/source/rust_verify/src/observers.rs b/source/rust_verify/src/observers.rs new file mode 100644 index 0000000000..b010775ba3 --- /dev/null +++ b/source/rust_verify/src/observers.rs @@ -0,0 +1,1114 @@ +//! Observers the verifier ships, as opposed to the test observers. +//! +//! One object, [`ObligationObserver`], serves two `-V observers=` names: +//! +//! - `coverage`: for every query, each obligation it asserted (an `assert`, +//! a postcondition, a loop invariant, a precondition of a call...) and what +//! became of it: `proved`, `failed`, `unknown` (the solver gave up on the +//! query) or `unchecked` (the query stopped before reaching it). As in +//! Verus's own checking, an obligation after a failed one is proved +//! assuming the failed one held: after a failing `assert(x > 5 && x < 3)`, +//! `assert(x == 2)` is `proved`. With +//! `-V axiom-usage-info` a proved query also names the axioms in its unsat +//! core. This is the obligation-level counterpart of `verus-reach`, which +//! says which functions are used; this says which of a function's +//! obligations were actually discharged. +//! - `proof-state`: at each failing obligation, while the solver's +//! counterexample is still live, which conjuncts of the failing assertion +//! are false in it and what the counterexample gives each variable the +//! assertion reads. +//! +//! Both need the query's assertions, which `AirObserver::on_query_lowered` +//! hands over after variables became versioned constants, and the answer, +//! which `QueryResultObserver` hands over. Neither knows which function a +//! query belongs to; the verifier does, so it drains the observer after each +//! query ([`ObligationObserver::take_query`]) and files the records under the +//! function, the way it files the other per-query solver reports. Terms stay +//! AIR text until the end of the crate, when [`resolve`] renders them as +//! source with the names the encoders recorded. + +use air::ast::{AssertId, BinaryOp, BindX, Expr, ExprX, Ident, MultiOp, Query, Stmt, StmtX}; +use air::query_result_observer::CheckValidResult; +use serde::Serialize; +use std::any::Any; +use std::collections::{BTreeSet, HashMap}; +use std::sync::Arc; + +/// The observer names this module serves. +pub const COVERAGE: &str = "coverage"; +pub const PROOF_STATE: &str = "proof-state"; + +/// The observers the test suites register, one at a time. +pub const TEST_OBSERVERS: &[&str] = &["test", "air-only", "query-result-only", "vir-only"]; + +/// Whether `-V observers=` names a valid set: `coverage` and `proof-state` +/// in any combination, or a single test observer. +pub fn check_names(names: &[String]) -> Result<(), String> { + let known = |n: &str| n == COVERAGE || n == PROOF_STATE || TEST_OBSERVERS.contains(&n); + if names.is_empty() { + return Err(format!("expected a list of observers ({COVERAGE}, {PROOF_STATE})")); + } + if let Some(bad) = names.iter().find(|n| !known(n)) { + return Err(format!("unknown observer `{bad}`; expected {COVERAGE} and/or {PROOF_STATE}")); + } + let tests = names.iter().filter(|n| TEST_OBSERVERS.contains(&n.as_str())).count(); + if tests > 0 && names.len() > 1 { + return Err(format!("a test observer cannot be combined with others: {}", names.join(","))); + } + Ok(()) +} + +/// A failing assertion's conjuncts are listed up to this many; the rest are +/// counted in `conjuncts_omitted`. +const MAX_CONJUNCTS: usize = 32; +/// At most this many conjuncts are evaluated in the counterexample (one +/// solver round trip each), so that false ones beyond the first +/// `MAX_CONJUNCTS` can still be listed first; the rest are omitted. +const MAX_EVALUATIONS: usize = 4 * MAX_CONJUNCTS; +/// Likewise the variables whose counterexample values are reported. +const MAX_VALUES: usize = 64; +/// How deeply temporaries and preconditions are expanded into their +/// definitions. +const MAX_TEMP_DEPTH: usize = 8; + +#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize)] +#[serde(rename_all = "snake_case")] +pub enum Status { + /// Proved assuming every earlier obligation of the query held, failed + /// ones included. + Proved, + Failed, + /// The solver gave up (resource limit or cancellation) before deciding it. + Unknown, + /// The query stopped before the solver decided it: an earlier failure + /// ended the query (`--multiple-errors 0`), or the error budget ran out. + Unchecked, +} + +/// One assertion of a lowered query. +struct Assertion { + id: Option, + message: String, + span: Option, + /// The asserted formula, over versioned constants. + expr: Expr, + status: Option, +} + +/// The query being checked: its assertions, and the answers so far. +struct Pending { + assertions: Vec, + /// Each Verus temporary (`tmp%1`) the query defines exactly once, by + /// `assume (= tmp%1 e)`, with its definition. `assert(a && b)` asserts + /// such a temporary, so its conjuncts are those of the definition. + temps: HashMap, + used_axioms: Option>, + failing: Vec, +} + +/// One obligation, before its terms are rendered as source. +#[derive(Clone, Debug, Serialize)] +pub struct Obligation { + #[serde(skip_serializing_if = "Option::is_none")] + pub assert_id: Option, + /// What Verus reports when it fails: "postcondition not satisfied", ... + pub message: String, + #[serde(skip_serializing_if = "Option::is_none")] + pub span: Option, + pub status: Status, +} + +/// A conjunct of a failing assertion, and its value in the counterexample: +/// null when the solver could not evaluate it (a quantifier, say). +#[derive(Clone, Debug, Serialize)] +pub struct Conjunct { + pub term: String, + pub value: Option, + /// A temporary or a callee's precondition (`req%f(args)`) whose + /// definition was not available, so it could not be split further. + #[serde(skip_serializing_if = "std::ops::Not::not")] + pub unexpanded: bool, +} + +/// A variable the failing assertion reads, and its counterexample value. +#[derive(Clone, Debug, Serialize)] +pub struct Value { + /// The versioned AIR constant (`x@2`): which assignment of `x` it is. + pub symbol: String, + /// The variable as the source names it, when the encoders recorded it. + #[serde(skip_serializing_if = "Option::is_none")] + pub name: Option, + pub value: String, +} + +#[derive(Clone, Debug)] +pub struct RawFailingAssert { + assert_id: Option, + message: String, + span: Option, + /// (term, value, unexpanded) + conjuncts: Vec<(String, Option, bool)>, + conjuncts_omitted: usize, + values: Vec<(String, String)>, + values_omitted: usize, +} + +/// What the observer saw of one query, before rendering. +pub struct RawQuery { + obligations: Vec, + used_axioms: Option>, + failing: Vec, +} + +/// Coverage of one query, as `func-details` publishes it under `obligations`. +#[derive(Clone, Debug, Serialize)] +pub struct QueryObligations { + pub desc: String, + pub span: String, + /// `body`, `recommends`, `expanded`, ... as the other per-query records. + pub kind: &'static str, + pub obligations: Vec, + /// Under `-V axiom-usage-info`, when the query was proved: the axioms in + /// its unsat core, rendered as source where the encoders named them. + #[serde(skip_serializing_if = "Option::is_none")] + pub used_axioms: Option>, +} + +/// The counterexample at one failing obligation, as `func-details` publishes +/// it under `failing_asserts`. +#[derive(Clone, Debug, Serialize)] +pub struct FailingAssert { + pub desc: String, + pub kind: &'static str, + #[serde(skip_serializing_if = "Option::is_none")] + pub assert_id: Option, + pub message: String, + #[serde(skip_serializing_if = "Option::is_none")] + pub span: Option, + /// False conjuncts first, then undecided, then true ones. + pub conjuncts: Vec, + #[serde(skip_serializing_if = "is_zero")] + pub conjuncts_omitted: usize, + pub values: Vec, + #[serde(skip_serializing_if = "is_zero")] + pub values_omitted: usize, +} + +fn is_zero(n: &usize) -> bool { + *n == 0 +} + +/// A query's records, filed under its function until the end of the crate. +pub struct FiledQuery { + pub desc: String, + pub span: String, + pub kind: &'static str, + pub raw: RawQuery, +} + +pub struct ObligationObserver { + coverage: bool, + proof_state: bool, + pending: Option, + /// Under proof-state: each precondition function the context declared + /// (`req%f`), with its parameters and definition, from the axiom + /// `forall params. req%f(params) == body`. A failing call's + /// precondition splits into the conjuncts of its body. + requires: HashMap, Expr)>, +} + +impl ObligationObserver { + /// `None` unless `names` asks for this observer and nothing else. + pub fn from_names(names: &[String]) -> Option { + let coverage = names.iter().any(|n| n == COVERAGE); + let proof_state = names.iter().any(|n| n == PROOF_STATE); + let others = names.iter().any(|n| n != COVERAGE && n != PROOF_STATE); + ((coverage || proof_state) && !others).then(|| ObligationObserver { + coverage, + proof_state, + pending: None, + requires: HashMap::new(), + }) + } + + /// Close the query just checked and hand over what was seen of it. + /// + /// `failed` are the ids of the failures that reached the verifier + /// without the `Invalid` callback (no model: bit-vector and nonlinear + /// checks, which carry no id at all). Such an answer has no error span, + /// and ids are not unique (a function's postconditions share one; loop + /// invariants and bit-vector asserts have none), so a failure is placed + /// only when its id names exactly one undecided assertion; otherwise + /// which one failed is unknown, and they stay undecided. + /// `truncated` says the verifier stopped checking obligations after the + /// first failure (the `--multiple-errors` budget ran out), so a later + /// `Valid` does not speak for them. + pub fn take_query( + &mut self, + failed: &[Option], + timed_out: bool, + truncated: bool, + ) -> Option { + let mut pending = self.pending.take()?; + for id in failed { + let mut undecided = + pending.assertions.iter_mut().filter(|a| a.status.is_none() && &a.id == id); + if let (Some(a), None) = (undecided.next(), undecided.next()) { + a.status = Some(Status::Failed); + } + } + if truncated { + // AIR's `only_check_earlier` disables every label after the + // first failed one (in label order), so a later `Valid` speaks + // only for the assertions before it. + if let Some(first) = + pending.assertions.iter().position(|a| a.status == Some(Status::Failed)) + { + for a in pending.assertions[first + 1..].iter_mut() { + if a.status == Some(Status::Proved) { + a.status = Some(Status::Unchecked); + } + } + } + } + let rest = if timed_out { Status::Unknown } else { Status::Unchecked }; + let obligations = if self.coverage { + pending + .assertions + .into_iter() + .map(|a| Obligation { + assert_id: a.id.as_ref().map(air::def::assert_id_to_symbol), + message: a.message, + span: a.span, + status: a.status.unwrap_or(rest), + }) + .collect() + } else { + Vec::new() + }; + Some(RawQuery { obligations, used_axioms: pending.used_axioms, failing: pending.failing }) + } +} + +/// The message and primary span of an assertion's error. +fn describe(message: &air::messages::ArcDynMessage) -> (String, Option) { + match message.downcast_ref::() { + Some(m) => (m.note.clone(), m.spans.first().map(|s| s.as_string.clone())), + None => (String::new(), None), + } +} + +fn collect_assertions(stmt: &Stmt, out: &mut Vec) { + match &**stmt { + StmtX::Assert(id, message, _, expr) => { + let (message, span) = describe(message); + out.push(Assertion { id: id.clone(), message, span, expr: expr.clone(), status: None }); + } + StmtX::DeadEnd(s) | StmtX::Breakable(_, s) => collect_assertions(s, out), + StmtX::Block(ss) | StmtX::Switch(ss) => { + for s in ss.iter() { + collect_assertions(s, out); + } + } + StmtX::Assume(_) + | StmtX::Havoc(_) + | StmtX::Assign(..) + | StmtX::Snapshot(_) + | StmtX::Break(_) => {} + } +} + +/// The temporaries `stmt` defines exactly once, with their definitions. +fn temp_definitions(stmt: &Stmt) -> HashMap { + fn walk(stmt: &Stmt, defs: &mut HashMap>) { + match &**stmt { + StmtX::Assume(e) => { + if let ExprX::Binary(air::ast::BinaryOp::Eq, lhs, rhs) = &**e { + if let ExprX::Var(x) = &**lhs { + if x.starts_with(vir::def::PREFIX_TEMP_VAR) { + defs.entry(x.to_string()).or_default().push(rhs.clone()); + } + } + } + } + StmtX::DeadEnd(s) | StmtX::Breakable(_, s) => walk(s, defs), + StmtX::Block(ss) | StmtX::Switch(ss) => { + for s in ss.iter() { + walk(s, defs); + } + } + StmtX::Assert(..) + | StmtX::Havoc(_) + | StmtX::Assign(..) + | StmtX::Snapshot(_) + | StmtX::Break(_) => {} + } + } + let mut defs = HashMap::new(); + walk(stmt, &mut defs); + defs.into_iter() + .filter_map(|(x, mut es)| (es.len() == 1).then(|| (x, es.pop().unwrap()))) + .collect() +} + +/// A precondition function's definition, if `axiom` is the one Verus +/// declares for it: `forall params. req%f(params) == body` (or, with no +/// parameters, `req%f == body`). +fn requires_definition(axiom: &Expr) -> Option<(String, Vec, Expr)> { + let (params, eq): (Vec, &Expr) = match &**axiom { + ExprX::Bind(bind, body) => match &**bind { + BindX::Quant(air::ast::Quant::Forall, bs, _, _) => { + (bs.iter().map(|b| b.name.clone()).collect(), body) + } + _ => return None, + }, + _ => (Vec::new(), axiom), + }; + let ExprX::Binary(BinaryOp::Eq, lhs, body) = &**eq else { return None }; + let (f, args) = match &**lhs { + ExprX::Apply(f, args) => (f, args.iter().collect::>()), + ExprX::Var(f) => (f, Vec::new()), + _ => return None, + }; + let is_param = |(a, p): (&&Expr, &Ident)| matches!(&***a, ExprX::Var(x) if x == p); + (f.starts_with(vir::def::PREFIX_REQUIRES) + && args.len() == params.len() + && args.iter().zip(params.iter()).all(is_param)) + .then(|| (f.to_string(), params, body.clone())) +} + +/// `body` with each parameter replaced by its argument; `None` when a +/// binder inside `body` shadows a parameter. +fn instantiate(params: &[Ident], args: &[Expr], body: &Expr) -> Option { + let mut shadowed = false; + air::visitor::map_expr_visitor(body, &mut |e| { + if let ExprX::Bind(bind, _) = &**e { + let names: Vec<&Ident> = match &**bind { + BindX::Let(bs) => bs.iter().map(|b| &b.name).collect(), + BindX::Quant(_, bs, _, _) + | BindX::Lambda(bs, _, _) + | BindX::Choose(bs, _, _, _) => bs.iter().map(|b| &b.name).collect(), + }; + shadowed |= names.iter().any(|n| params.contains(n)); + } + e.clone() + }); + if shadowed { + return None; + } + Some(air::visitor::map_expr_visitor(body, &mut |e| match &**e { + ExprX::Var(x) => match params.iter().position(|p| p == x) { + Some(i) => args[i].clone(), + None => e.clone(), + }, + _ => e.clone(), + })) +} + +/// What a failing assertion's conjuncts may be read through. +struct Definitions<'a> { + temps: &'a HashMap, + requires: &'a HashMap, Expr)>, +} + +/// The formula's top-level conjuncts, flattening nested conjunctions, +/// reading a temporary as its definition and a callee's precondition as +/// its body at the call's arguments. Each comes with whether it is a +/// temporary or precondition that could not be read that way. +fn conjuncts(expr: &Expr, defs: &Definitions, depth: usize, out: &mut Vec<(Expr, bool)>) { + let deeper = depth < MAX_TEMP_DEPTH; + match &**expr { + ExprX::Multi(MultiOp::And, es) => { + for e in es.iter() { + conjuncts(e, defs, depth, out); + } + } + // a precondition's `axiom_location`, once labelled: + // `%%global_location_label%%N => e` + ExprX::Binary(BinaryOp::Implies, label, e) if matches!(&**label, ExprX::Var(l) if l.starts_with(air::def::GLOBAL_PREFIX_LABEL)) => { + conjuncts(e, defs, depth, out) + } + ExprX::LabeledAxiom(_, _, e) => conjuncts(e, defs, depth, out), + ExprX::Var(x) if deeper && defs.temps.contains_key(&**x) => { + conjuncts(&defs.temps[&**x], defs, depth + 1, out) + } + ExprX::Var(x) if x.starts_with(vir::def::PREFIX_TEMP_VAR) => out.push((expr.clone(), true)), + ExprX::Apply(f, args) if f.starts_with(vir::def::PREFIX_REQUIRES) => { + let body = defs + .requires + .get(&**f) + .filter(|_| deeper) + .and_then(|(params, body)| instantiate(params, args, body)); + match body { + Some(body) => conjuncts(&body, defs, depth + 1, out), + None => out.push((expr.clone(), true)), + } + } + _ => out.push((expr.clone(), false)), + } +} + +/// The constants the formula reads, outside binders' own variables. +fn free_constants(expr: &Expr, bound: &mut Vec, out: &mut BTreeSet) { + match &**expr { + ExprX::Const(_) => {} + ExprX::Var(x) => { + if !bound.iter().any(|b| b == &**x) { + out.insert(x.to_string()); + } + } + ExprX::Old(_, x) => { + out.insert(x.to_string()); + } + ExprX::Apply(_, es) | ExprX::Multi(_, es) | ExprX::Array(es) => { + for e in es.iter() { + free_constants(e, bound, out); + } + } + ExprX::ApplyFun(_, f, es) => { + free_constants(f, bound, out); + for e in es.iter() { + free_constants(e, bound, out); + } + } + ExprX::Unary(_, e) | ExprX::LabeledAxiom(_, _, e) | ExprX::LabeledAssertion(_, _, _, e) => { + free_constants(e, bound, out) + } + ExprX::Binary(_, a, b) => { + free_constants(a, bound, out); + free_constants(b, bound, out); + } + ExprX::IfElse(a, b, c) => { + free_constants(a, bound, out); + free_constants(b, bound, out); + free_constants(c, bound, out); + } + ExprX::Bind(bind, e) => { + let names: Vec = match &**bind { + air::ast::BindX::Let(bs) => { + for b in bs.iter() { + free_constants(&b.a, bound, out); + } + bs.iter().map(|b| b.name.to_string()).collect() + } + air::ast::BindX::Quant(_, bs, _, _) | air::ast::BindX::Lambda(bs, _, _) => { + bs.iter().map(|b| b.name.to_string()).collect() + } + air::ast::BindX::Choose(bs, _, _, cond) => { + let names: Vec = bs.iter().map(|b| b.name.to_string()).collect(); + let depth = bound.len(); + bound.extend(names.iter().cloned()); + free_constants(cond, bound, out); + bound.truncate(depth); + names + } + }; + let depth = bound.len(); + bound.extend(names); + free_constants(e, bound, out); + bound.truncate(depth); + } + } +} + +/// Sorts of the encoding's own constants (type ids like `INT`, the `$` +/// decoration, fuel), whose counterexample values say nothing about the +/// program. +fn is_encoding_sort(typ: &air::ast::Typ) -> bool { + use vir::def::{DECORATION, FUEL_ID, FUEL_TYPE, TYPE}; + matches!(&**typ, air::ast::TypX::Named(n) + if [TYPE, DECORATION, FUEL_TYPE, FUEL_ID].contains(&n.as_str())) +} + +/// `expr` without its binders' triggers and qids: the printer spells them +/// as SMT's `(! body :pattern ...)`, which reads as a negation once +/// rendered as source. +fn strip_attributes(expr: &Expr) -> Expr { + air::visitor::map_expr_visitor(expr, &mut |e| match &**e { + ExprX::Bind(bind, body) => { + let bare = match &**bind { + BindX::Quant(q, bs, trigs, qid) if !trigs.is_empty() || qid.is_some() => { + BindX::Quant(*q, bs.clone(), Arc::new(vec![]), None) + } + BindX::Lambda(bs, trigs, qid) if !trigs.is_empty() || qid.is_some() => { + BindX::Lambda(bs.clone(), Arc::new(vec![]), None) + } + BindX::Choose(bs, trigs, qid, cond) if !trigs.is_empty() || qid.is_some() => { + BindX::Choose(bs.clone(), Arc::new(vec![]), None, cond.clone()) + } + _ => return e.clone(), + }; + Arc::new(ExprX::Bind(Arc::new(bare), body.clone())) + } + _ => e.clone(), + }) +} + +fn term_text(expr: &Expr) -> String { + let expr = &strip_attributes(expr); + let printer = air::printer::Printer::new( + Arc::new(air::messages::AirMessageInterface {}), + true, + air::context::SmtSolver::Cvc5, + ); + air::printer::NodeWriter::new() + .node_to_string_indent(&String::new(), &printer.expr_to_node(expr)) +} + +impl air::air_observer::AirObserver for ObligationObserver { + fn on_axiom_decl(&mut self, expr: &Expr) { + if self.proof_state { + if let Some((f, params, body)) = requires_definition(expr) { + self.requires.insert(f, (params, body)); + } + } + } + + fn on_query_lowered( + &mut self, + query: &Query, + _snapshots: &air::ast::Snapshots, + _local_vars: &[air::ast::Decl], + ) { + let mut assertions = Vec::new(); + collect_assertions(&query.assertion, &mut assertions); + let temps = + if self.proof_state { temp_definitions(&query.assertion) } else { HashMap::new() }; + self.pending = Some(Pending { assertions, temps, used_axioms: None, failing: Vec::new() }); + } + + fn as_any(&self) -> &dyn Any { + self + } + fn as_any_mut(&mut self) -> &mut dyn Any { + self + } +} + +impl air::query_result_observer::QueryResultObserver for ObligationObserver { + fn on_check_valid_result(&mut self, result: &mut CheckValidResult) { + let proof_state = self.proof_state; + let Some(pending) = &mut self.pending else { return }; + match result { + CheckValidResult::Valid { usage_info, .. } => { + for a in pending.assertions.iter_mut() { + if a.status.is_none() { + a.status = Some(Status::Proved); + } + } + if let air::context::UsageInfo::UsedAxioms(axioms) = usage_info { + pending.used_axioms = Some(axioms.iter().map(|a| a.to_string()).collect()); + } + } + CheckValidResult::Timeout { .. } => { + for a in pending.assertions.iter_mut() { + if a.status.is_none() { + a.status = Some(Status::Unknown); + } + } + } + CheckValidResult::Invalid { model_defs, eval_bool_expr, assert_id, error } => { + // The undecided assertion the solver's label named. Ids are + // not unique (loop invariants have none, a function's + // postconditions share one), so the error's primary span + // decides between assertions with the same id. + let (_, error_span) = describe(error); + // Without a span match, the failure is placed only when its + // id picks out exactly one undecided assertion, as in + // `take_query`. + let undecided = |a: &Assertion| a.status.is_none() && &a.id == *assert_id; + let sole_undecided = || { + let mut candidates = + pending.assertions.iter().enumerate().filter(|(_, a)| undecided(a)); + match (candidates.next(), candidates.next()) { + (Some((i, _)), None) => Some(i), + _ => None, + } + }; + let Some(index) = pending + .assertions + .iter() + .position(|a| undecided(a) && error_span.is_some() && a.span == error_span) + .or_else(sole_undecided) + else { + return; + }; + let a = &mut pending.assertions[index]; + a.status = Some(Status::Failed); + if !proof_state { + return; + } + let mut parts = Vec::new(); + let defs = Definitions { temps: &pending.temps, requires: &self.requires }; + conjuncts(&a.expr, &defs, 0, &mut parts); + // each evaluation is a solver round trip; past the cap the + // conjuncts are counted as omitted, not evaluated + let mut evaluated: Vec<(String, Option, bool)> = parts + .iter() + .take(MAX_EVALUATIONS) + .map(|(c, unexpanded)| (term_text(c), eval_bool_expr(c), *unexpanded)) + .collect(); + // false first: those are why the assertion failed + evaluated.sort_by_key(|(_, v, _)| match v { + Some(false) => 0, + None => 1, + Some(true) => 2, + }); + let conjuncts_omitted = parts.len().saturating_sub(MAX_CONJUNCTS); + evaluated.truncate(MAX_CONJUNCTS); + // what the conjuncts read, so an expanded temporary shows + // the variables of its definition + let mut symbols = BTreeSet::new(); + for (part, _) in parts.iter() { + free_constants(part, &mut Vec::new(), &mut symbols); + } + let mut values: Vec<(String, String)> = symbols + .into_iter() + .filter_map(|s| { + let def = model_defs.get(&Arc::new(s.clone()))?; + (def.params.is_empty() && !is_encoding_sort(&def.ret)) + .then(|| (s, def.body.to_string())) + }) + .collect(); + let values_omitted = values.len().saturating_sub(MAX_VALUES); + values.truncate(MAX_VALUES); + pending.failing.push(RawFailingAssert { + assert_id: a.id.as_ref().map(air::def::assert_id_to_symbol), + message: a.message.clone(), + span: a.span.clone(), + conjuncts: evaluated, + conjuncts_omitted, + values, + values_omitted, + }); + } + } + } + + fn as_any(&self) -> &dyn Any { + self + } + fn as_any_mut(&mut self) -> &mut dyn Any { + self + } +} + +/// The source spelling of a versioned constant's variable: `x@2` reads as +/// `x`, when the encoders recorded `x@`. +fn variable_name(names: &vir::air_names::SourceNames, symbol: &str) -> Option { + let base = match symbol.rfind('@') { + Some(at) => &symbol[..=at], + None => symbol, + }; + let rendered = vir::air_names::render_term(names, base); + (rendered != base).then_some(rendered) +} + +/// A term with each versioned constant (`i@1`) read as its variable (`i@`), +/// which the encoders recorded: the source has no versions. +fn render_unversioned(names: &vir::air_names::SourceNames, term: &str) -> String { + let mut out = String::with_capacity(term.len()); + let mut chars = term.chars().peekable(); + while let Some(c) = chars.next() { + out.push(c); + if c == '@' { + while chars.peek().is_some_and(|d| d.is_ascii_digit()) { + chars.next(); + } + } + } + vir::air_names::render_term(names, &out) +} + +/// Render one function's filed queries as source. +pub fn resolve( + names: &vir::air_names::SourceNames, + queries: Vec, +) -> (Vec, Vec) { + let mut obligations = Vec::new(); + let mut failing = Vec::new(); + for q in queries { + let FiledQuery { desc, span, kind, raw } = q; + if !raw.obligations.is_empty() { + obligations.push(QueryObligations { + desc: desc.clone(), + span, + kind, + obligations: raw.obligations, + used_axioms: raw.used_axioms.map(|axioms| { + axioms.iter().map(|a| vir::air_names::render_term(names, a)).collect() + }), + }); + } + for f in raw.failing { + failing.push(FailingAssert { + desc: desc.clone(), + kind, + assert_id: f.assert_id, + message: f.message, + span: f.span, + conjuncts: f + .conjuncts + .into_iter() + .map(|(term, value, unexpanded)| Conjunct { + term: render_unversioned(names, &term), + value, + unexpanded, + }) + .collect(), + conjuncts_omitted: f.conjuncts_omitted, + values: f + .values + .into_iter() + .map(|(symbol, value)| Value { + name: variable_name(names, &symbol), + value: vir::air_names::render_term(names, &value), + symbol, + }) + .collect(), + values_omitted: f.values_omitted, + }); + } + } + (obligations, failing) +} + +#[cfg(test)] +mod tests { + use super::*; + use air::ast::{BinaryOp, Constant, TypX}; + + fn var(x: &str) -> Expr { + Arc::new(ExprX::Var(Arc::new(x.to_string()))) + } + + #[test] + fn names_select_the_observer_alone() { + let names = |ns: &[&str]| ns.iter().map(|n| n.to_string()).collect::>(); + assert!(ObligationObserver::from_names(&names(&["coverage"])).is_some()); + let both = ObligationObserver::from_names(&names(&["coverage", "proof-state"])).unwrap(); + assert!(both.coverage && both.proof_state); + assert!(ObligationObserver::from_names(&names(&["coverage", "test"])).is_none()); + assert!(ObligationObserver::from_names(&names(&["test"])).is_none()); + } + + #[test] + fn observer_names_are_checked() { + let names = |ns: &[&str]| ns.iter().map(|n| n.to_string()).collect::>(); + assert!(check_names(&names(&["coverage", "proof-state"])).is_ok()); + assert!(check_names(&names(&["test"])).is_ok()); + assert!( + check_names(&names(&["covrage"])).unwrap_err().contains("unknown observer `covrage`") + ); + assert!(check_names(&names(&["coverage", ""])).is_err()); + assert!(check_names(&names(&["test", "coverage"])).is_err()); + assert!(check_names(&names(&["test", "vir-only"])).is_err()); + assert!(check_names(&[]).is_err()); + } + + #[test] + fn versions_are_dropped_before_rendering() { + let names = vir::air_names::SourceNames::new(); + assert_eq!(render_unversioned(&names, "(<= i@12 n@)"), "(i@ <= n@)"); + } + + #[test] + fn conjuncts_flatten_nested_ands() { + let and = |es: Vec| Arc::new(ExprX::Multi(MultiOp::And, Arc::new(es))); + let e = and(vec![var("a"), and(vec![var("b"), var("c")])]); + let (temps, requires) = (HashMap::new(), HashMap::new()); + let mut out = Vec::new(); + conjuncts(&e, &Definitions { temps: &temps, requires: &requires }, 0, &mut out); + assert_eq!(out.len(), 3); + } + + /// `assert(a && b)` asserts a temporary; its conjuncts are its + /// definition's. A temporary defined on two branches is left alone. + #[test] + fn temporaries_read_as_their_definitions() { + let and = |es: Vec| Arc::new(ExprX::Multi(MultiOp::And, Arc::new(es))); + let def = |x: &str, e: Expr| { + Arc::new(StmtX::Assume(Arc::new(ExprX::Binary(BinaryOp::Eq, var(x), e)))) + }; + let block = |ss: Vec| Arc::new(StmtX::Block(Arc::new(ss))); + let body = block(vec![ + def("tmp%1", and(vec![var("a@0"), var("tmp%2")])), + def("tmp%2", and(vec![var("b@1"), var("c!")])), + Arc::new(StmtX::Switch(Arc::new(vec![def("tmp%3", var("d")), def("tmp%3", var("e"))]))), + ]); + let temps = temp_definitions(&body); + assert!(temps.contains_key("tmp%1") && !temps.contains_key("tmp%3")); + let requires = HashMap::new(); + let defs = Definitions { temps: &temps, requires: &requires }; + let split = |e: Expr| { + let mut out = Vec::new(); + conjuncts(&e, &defs, 0, &mut out); + out.iter().map(|(c, unexpanded)| (term_text(c), *unexpanded)).collect::>() + }; + let s = |t: &str, u: bool| (t.to_string(), u); + assert_eq!(split(var("tmp%1")), [s("a@0", false), s("b@1", false), s("c!", false)]); + assert_eq!(split(var("tmp%3")), [s("tmp%3", true)]); + } + + /// A failing call's precondition `req%f(args)` splits into the + /// conjuncts of `f`'s requires at those arguments, read through the + /// labels Verus puts on each requires clause. + #[test] + fn preconditions_read_as_their_definitions() { + let int = Arc::new(TypX::Int); + let binder = + |x: &str| Arc::new(air::ast::BinderX { name: Arc::new(x.to_string()), a: int.clone() }); + let app = + |f: &str, es: Vec| Arc::new(ExprX::Apply(Arc::new(f.to_string()), Arc::new(es))); + let bin = |op, a, b| Arc::new(ExprX::Binary(op, a, b)); + let labelled = |n: &str, e| { + bin(BinaryOp::Implies, var(&format!("{}{}", air::def::GLOBAL_PREFIX_LABEL, n)), e) + }; + let body = Arc::new(ExprX::Multi( + MultiOp::And, + Arc::new(vec![ + labelled("0", bin(BinaryOp::Gt, var("y!"), var("five"))), + labelled("1", bin(BinaryOp::Lt, var("y!"), var("z!"))), + ]), + )); + let axiom = Arc::new(ExprX::Bind( + Arc::new(BindX::Quant( + air::ast::Quant::Forall, + Arc::new(vec![binder("y!"), binder("z!")]), + Arc::new(vec![]), + None, + )), + bin(BinaryOp::Eq, app("req%m!g.", vec![var("y!"), var("z!")]), body), + )); + let mut o = ObligationObserver::from_names(&["proof-state".to_string()]).unwrap(); + air::air_observer::AirObserver::on_axiom_decl(&mut o, &axiom); + assert!(o.requires.contains_key("req%m!g.")); + let temps = HashMap::new(); + let defs = Definitions { temps: &temps, requires: &o.requires }; + let mut out = Vec::new(); + conjuncts(&app("req%m!g.", vec![var("a@1"), var("seven")]), &defs, 0, &mut out); + let terms: Vec<(String, bool)> = out.iter().map(|(c, u)| (term_text(c), *u)).collect(); + assert_eq!( + terms, + [("(> a@1 five)".to_string(), false), ("(< a@1 seven)".to_string(), false)] + ); + // a callee whose requires the context never declared stays whole + let mut out = Vec::new(); + conjuncts(&app("req%m!h.", vec![var("a@1")]), &defs, 0, &mut out); + assert_eq!(out.len(), 1); + assert!(out[0].1); + } + + /// A failing assertion with many conjuncts costs at most + /// `MAX_EVALUATIONS` solver round trips; the rest are counted omitted. + #[test] + fn evaluations_are_capped() { + use air::messages::MessageInterface; + let n = MAX_EVALUATIONS + 10; + let expr = Arc::new(ExprX::Multi( + MultiOp::And, + Arc::new((0..n).map(|i| var(&format!("c{i}"))).collect()), + )); + let mut o = ObligationObserver::from_names(&["proof-state".to_string()]).unwrap(); + o.pending = Some(Pending { + assertions: vec![Assertion { + id: None, + message: String::new(), + span: None, + expr, + status: None, + }], + temps: HashMap::new(), + used_axioms: None, + failing: Vec::new(), + }); + let mut calls = 0; + let mut eval = |_: &Expr| { + calls += 1; + Some(false) + }; + let error = air::messages::AirMessageInterface {} + .bare(air::messages::MessageLevel::Error, "assertion failed"); + air::query_result_observer::QueryResultObserver::on_check_valid_result( + &mut o, + &mut CheckValidResult::Invalid { + model_defs: &HashMap::new(), + eval_bool_expr: &mut eval, + assert_id: &None, + error: &error, + }, + ); + assert_eq!(calls, MAX_EVALUATIONS); + let f = &o.pending.as_ref().unwrap().failing[0]; + assert_eq!(f.conjuncts.len(), MAX_CONJUNCTS); + assert_eq!(f.conjuncts_omitted, n - MAX_CONJUNCTS); + } + + /// A quantifier's triggers and qid are left out of its source text: + /// SMT's `(! body :pattern ...)` would render as a negation. + #[test] + fn quantifier_attributes_are_not_rendered() { + let binder = + Arc::new(air::ast::BinderX { name: Arc::new("i".to_string()), a: Arc::new(TypX::Int) }); + let body = Arc::new(ExprX::Binary(BinaryOp::Le, var("i"), var("n@1"))); + let bind = Arc::new(BindX::Quant( + air::ast::Quant::Forall, + Arc::new(vec![binder]), + Arc::new(vec![Arc::new(vec![var("i")])]), + Some(Arc::new("user_q_1".to_string())), + )); + let text = term_text(&Arc::new(ExprX::Bind(bind, body))); + assert!(!text.contains('!') && !text.contains(":pattern"), "{text}"); + assert!(!text.contains(":qid"), "{text}"); + let names = vir::air_names::SourceNames::new(); + assert!(!render_unversioned(&names, &text).contains('!')); + } + + /// A failure whose span matches no assertion is placed only when its + /// id picks out exactly one undecided assertion. + #[test] + fn an_unmatched_failure_is_placed_only_when_unambiguous() { + use air::messages::MessageInterface; + let invariant = || Assertion { + id: None, + message: String::new(), + span: Some("elsewhere".to_string()), + expr: var("x"), + status: None, + }; + let mut o = ObligationObserver::from_names(&["coverage".to_string()]).unwrap(); + let fail = |o: &mut ObligationObserver| { + let error = air::messages::AirMessageInterface {} + .bare(air::messages::MessageLevel::Error, "invariant not satisfied"); + air::query_result_observer::QueryResultObserver::on_check_valid_result( + o, + &mut CheckValidResult::Invalid { + model_defs: &HashMap::new(), + eval_bool_expr: &mut |_: &Expr| None, + assert_id: &None, + error: &error, + }, + ); + }; + let pending = |assertions| Pending { + assertions, + temps: HashMap::new(), + used_axioms: None, + failing: Vec::new(), + }; + o.pending = Some(pending(vec![invariant(), invariant()])); + fail(&mut o); + let statuses = |o: &ObligationObserver| { + o.pending.as_ref().unwrap().assertions.iter().map(|a| a.status).collect::>() + }; + assert_eq!(statuses(&o), vec![None, None]); + o.pending = Some(pending(vec![invariant()])); + fail(&mut o); + assert_eq!(statuses(&o), vec![Some(Status::Failed)]); + } + + #[test] + fn free_constants_skip_bound_variables() { + let binder = + Arc::new(air::ast::BinderX { name: Arc::new("i".to_string()), a: Arc::new(TypX::Int) }); + let body = Arc::new(ExprX::Binary(BinaryOp::Le, var("i"), var("n@1"))); + let bind = Arc::new(air::ast::BindX::Quant( + air::ast::Quant::Forall, + Arc::new(vec![binder]), + Arc::new(vec![]), + None, + )); + let e = Arc::new(ExprX::Multi( + MultiOp::And, + Arc::new(vec![ + Arc::new(ExprX::Bind(bind, body)), + var("x@0"), + Arc::new(ExprX::Const(Constant::Bool(true))), + ]), + )); + let mut out = BTreeSet::new(); + free_constants(&e, &mut Vec::new(), &mut out); + assert_eq!(out.into_iter().collect::>(), vec!["n@1", "x@0"]); + } + + #[test] + fn take_query_fills_statuses() { + let mut o = ObligationObserver { + coverage: true, + proof_state: false, + pending: None, + requires: HashMap::new(), + }; + let id = |n: u64| Some(Arc::new(vec![n])); + let assertion = |n: u64, status| Assertion { + id: id(n), + message: String::new(), + span: None, + expr: var("x"), + status, + }; + let pending = |o: &mut ObligationObserver| { + o.pending = Some(Pending { + temps: HashMap::new(), + assertions: vec![ + assertion(0, Some(Status::Proved)), + assertion(1, Some(Status::Failed)), + assertion(2, Some(Status::Proved)), + assertion(3, None), + ], + used_axioms: None, + failing: Vec::new(), + }) + }; + pending(&mut o); + let statuses = |q: RawQuery| q.obligations.iter().map(|o| o.status).collect::>(); + use Status::*; + // the error budget ran out after #1: a later Valid does not speak for #2 + let q = o.take_query(&[], false, true).unwrap(); + assert_eq!(statuses(q), vec![Proved, Failed, Unchecked, Unchecked]); + // two failures before the budget ran out: the last round disabled + // everything after the first, #1, so #2 was never proved either + o.pending = Some(Pending { + temps: HashMap::new(), + assertions: vec![ + assertion(0, Some(Status::Proved)), + assertion(1, Some(Status::Failed)), + assertion(2, Some(Status::Proved)), + assertion(3, Some(Status::Failed)), + assertion(4, Some(Status::Proved)), + ], + used_axioms: None, + failing: Vec::new(), + }); + let q = o.take_query(&[], false, true).unwrap(); + assert_eq!(statuses(q), vec![Proved, Failed, Unchecked, Failed, Unchecked]); + // #3 failed without an Invalid callback (no model) + pending(&mut o); + let q = o.take_query(&[id(3)], false, false).unwrap(); + assert_eq!(statuses(q), vec![Proved, Failed, Proved, Failed]); + // the solver gave up + pending(&mut o); + let q = o.take_query(&[], true, false).unwrap(); + assert_eq!(statuses(q), vec![Proved, Failed, Proved, Unknown]); + // two undecided postconditions share the id that failed without a + // model: which one failed is not known + o.pending = Some(Pending { + temps: HashMap::new(), + assertions: vec![assertion(5, None), assertion(5, None), assertion(6, None)], + used_axioms: None, + failing: Vec::new(), + }); + let q = o.take_query(&[id(5), id(6)], false, false).unwrap(); + assert_eq!(statuses(q), vec![Unchecked, Unchecked, Failed]); + // a bit-vector assert has no id, and fails without a model + o.pending = Some(Pending { + temps: HashMap::new(), + assertions: vec![Assertion { id: None, ..assertion(0, None) }], + used_axioms: None, + failing: Vec::new(), + }); + let q = o.take_query(&[None], false, false).unwrap(); + assert_eq!(statuses(q), vec![Failed]); + assert!(o.take_query(&[], false, false).is_none()); + } +} diff --git a/source/rust_verify/src/resident.rs b/source/rust_verify/src/resident.rs index 16a0b5379f..111f6b0032 100644 --- a/source/rust_verify/src/resident.rs +++ b/source/rust_verify/src/resident.rs @@ -532,7 +532,10 @@ pub(crate) struct SolverState { } impl SolverState { - pub(crate) fn new(air: Context, journal: QueryJournal) -> Self { + pub(crate) fn new(mut air: Context, journal: QueryJournal) -> Self { + // `-V observers=` records are drained per query by the verifier's + // own query loop; a session's queries would feed them to no one. + air.set_observers(None, None); Self { air, journal } } } @@ -6512,6 +6515,20 @@ mod tests { assert_eq!(names, COMMANDS.iter().copied().collect::>(), "{error}"); } + /// A context a session keeps runs its queries with no `-V observers=` + /// attached: nothing would drain what they record. + #[test] + fn retained_contexts_carry_no_observers() { + let observer = Arc::new(std::sync::Mutex::new( + crate::observers::ObligationObserver::from_names(&["proof-state".to_string()]).unwrap(), + )); + let mut air = Context::new(Arc::new(VirMessageInterface {}), SmtSolver::Cvc5); + air.set_observers(Some(observer.clone()), Some(observer)); + assert!(air.query_result_observer().is_some()); + let state = SolverState::new(air, QueryJournal::new()); + assert!(state.air.query_result_observer().is_none()); + } + #[test] fn kept_graphs_drop_the_least_recently_used_past_the_budget() { let graph = |n: usize| { diff --git a/source/rust_verify/src/test_observer.rs b/source/rust_verify/src/test_observer.rs new file mode 100644 index 0000000000..91db283466 --- /dev/null +++ b/source/rust_verify/src/test_observer.rs @@ -0,0 +1,600 @@ +//! Built-in test observer activated by `-V observers=test`. +//! Records callback data and emits JSON for test assertions. + +use std::any::Any; +use vir::ast_util::LowerUniqueVar; + +/// Counts `Breakable` / `Break` statements in a query assertion (present when loops are +/// lowered without isolation). +fn count_break_stmts(stmt: &air::ast::Stmt) -> (usize, usize) { + use air::ast::StmtX; + match &**stmt { + StmtX::Breakable(_, body) => { + let (b, k) = count_break_stmts(body); + (b + 1, k) + } + StmtX::Break(_) => (0, 1), + StmtX::DeadEnd(body) => count_break_stmts(body), + StmtX::Block(stmts) | StmtX::Switch(stmts) => stmts.iter().fold((0, 0), |(b, k), s| { + let (b2, k2) = count_break_stmts(s); + (b + b2, k + k2) + }), + _ => (0, 0), + } +} + +pub struct TestObserver { + pub krate_function_names: Vec, + pub krate_datatype_names: Vec, + pub havocs: Vec, + pub assigns: Vec, + pub branch_merges: usize, + pub variable_defs: Vec, + pub for_loop_vars: Vec<(String, String)>, + pub reveal_strings: Vec, + pub quantifier_binders: Vec, + pub assert_id_kinds: Vec, + pub function_lowered_count: usize, + pub query_lowered_count: usize, + pub query_snapshot_counts: Vec, + pub version_correlations: Vec<(String, u32, String)>, + pub correlator: vir::vir_observer::VersionCorrelator, + pub lambda_decls: Vec, + pub choose_decls: Vec, + pub check_valid_invalid_count: usize, + pub check_valid_valid_count: usize, + pub check_valid_timeout: usize, + pub check_valid_invalid_model_size: Vec, + pub eval_expr_results: Vec>, + pub binder_decls: Vec, + /// Count of `StmtX::Breakable` in lowered queries (loop encodings without isolation). + /// Per discharged (Valid) query: how many labeled assertion ids it reported. + pub valid_assert_id_counts: Vec, + /// Per discharged query: number of named axioms in the unsat core, or None when usage + /// reporting is not enabled. + pub valid_used_axiom_counts: Vec>, + pub breakable_count: usize, + /// Count of `StmtX::Break` in lowered queries. + pub break_count: usize, + pub pre_body_binders: Vec, + pub post_body_binders: Vec, + pub body_lowering_started: bool, + /// Ordered trace of every callback in fire order — enables sequencing + /// assertions (L1–L5) that per-callback aggregates cannot express. + pub events: Vec, + /// Count of `on_axiom_decl` (high-frequency; counted, not traced). + pub axiom_decls: usize, +} + +impl TestObserver { + pub fn new() -> Self { + TestObserver { + krate_function_names: vec![], + krate_datatype_names: vec![], + havocs: vec![], + assigns: vec![], + branch_merges: 0, + variable_defs: vec![], + for_loop_vars: vec![], + reveal_strings: vec![], + quantifier_binders: vec![], + assert_id_kinds: vec![], + function_lowered_count: 0, + query_lowered_count: 0, + query_snapshot_counts: vec![], + version_correlations: vec![], + correlator: vir::vir_observer::VersionCorrelator::new(), + lambda_decls: vec![], + choose_decls: vec![], + check_valid_invalid_count: 0, + check_valid_valid_count: 0, + check_valid_timeout: 0, + check_valid_invalid_model_size: vec![], + eval_expr_results: vec![], + binder_decls: vec![], + valid_assert_id_counts: vec![], + valid_used_axiom_counts: vec![], + breakable_count: 0, + break_count: 0, + pre_body_binders: vec![], + post_body_binders: vec![], + body_lowering_started: false, + events: vec![], + axiom_decls: 0, + } + } + + fn json_strings(v: &[String]) -> String { + let items: Vec = v.iter().map(|s| format!("\"{}\"", s)).collect(); + format!("[{}]", items.join(",")) + } + fn json_usizes(v: &[usize]) -> String { + let items: Vec = v.iter().map(|n| n.to_string()).collect(); + format!("[{}]", items.join(",")) + } + fn json_opt_bools(v: &[Option]) -> String { + let items: Vec = v + .iter() + .map(|b| match b { + Some(true) => "true".to_string(), + Some(false) => "false".to_string(), + None => "null".to_string(), + }) + .collect(); + format!("[{}]", items.join(",")) + } + fn json_opt_usizes(v: &[Option]) -> String { + let items: Vec = v + .iter() + .map(|n| match n { + Some(n) => n.to_string(), + None => "null".to_string(), + }) + .collect(); + format!("[{}]", items.join(",")) + } + fn json_version_correlations(v: &[(String, u32, String)]) -> String { + let items: Vec = v + .iter() + .map(|(name, line, kind)| format!("[\"{}\",{},\"{}\"]", name, line, kind)) + .collect(); + format!("[{}]", items.join(",")) + } + fn json_string_pairs(v: &[(String, String)]) -> String { + let items: Vec = v.iter().map(|(a, b)| format!("[\"{}\",\"{}\"]", a, b)).collect(); + format!("[{}]", items.join(",")) + } + + pub fn summary_json(&self) -> String { + format!( + concat!( + "OBSERVER:{{", + "\"krate_function_names\":{},\"krate_datatype_names\":{},", + "\"havocs\":{},\"assigns\":{},", + "\"branch_merges\":{},", + "\"variable_defs\":{},\"for_loop_vars\":{},", + "\"reveal_strings\":{},", + "\"quantifier_binders\":{},", + "\"assert_id_kinds\":{},", + "\"function_lowered\":{},\"query_lowered\":{},", + "\"query_snapshot_counts\":{},", + "\"version_correlations\":{},", + "\"lambda_decls\":{},\"choose_decls\":{},", + "\"check_valid_invalid\":{},\"check_valid_valid\":{},", + "\"check_valid_timeout\":{},", + "\"check_valid_invalid_model_size\":{},", + "\"eval_expr_results\":{},", + "\"binder_decls\":{},", + "\"pre_body_binders\":{},", + "\"post_body_binders\":{},", + "\"events\":{},", + "\"axiom_decls\":{},", + "\"breakable_count\":{},\"break_count\":{},", + "\"valid_assert_id_counts\":{},", + "\"valid_used_axiom_counts\":{}", + "}}" + ), + Self::json_strings(&self.krate_function_names), + Self::json_strings(&self.krate_datatype_names), + Self::json_strings(&self.havocs), + Self::json_strings(&self.assigns), + self.branch_merges, + Self::json_strings(&self.variable_defs), + Self::json_string_pairs(&self.for_loop_vars), + Self::json_strings(&self.reveal_strings), + Self::json_strings(&self.quantifier_binders), + Self::json_strings(&self.assert_id_kinds), + self.function_lowered_count, + self.query_lowered_count, + Self::json_usizes(&self.query_snapshot_counts), + Self::json_version_correlations(&self.version_correlations), + Self::json_strings(&self.lambda_decls), + Self::json_strings(&self.choose_decls), + self.check_valid_invalid_count, + self.check_valid_valid_count, + self.check_valid_timeout, + Self::json_usizes(&self.check_valid_invalid_model_size), + Self::json_opt_bools(&self.eval_expr_results), + Self::json_strings(&self.binder_decls), + Self::json_strings(&self.pre_body_binders), + Self::json_strings(&self.post_body_binders), + Self::json_strings(&self.events), + self.axiom_decls, + self.breakable_count, + self.break_count, + Self::json_usizes(&self.valid_assert_id_counts), + Self::json_opt_usizes(&self.valid_used_axiom_counts), + ) + } +} + +fn fun_name(f: &vir::ast::Function) -> String { + f.x.name.path.segments.last().map(|s| s.to_string()).unwrap_or_default() +} +fn dt_name(d: &vir::ast::Datatype) -> String { + match &d.x.name { + vir::ast::Dt::Path(p) => p.segments.last().map(|s| s.to_string()).unwrap_or_default(), + vir::ast::Dt::Tuple(n) => format!("tuple{}", n), + } +} + +impl air::air_observer::AirObserver for TestObserver { + fn on_query_lowered( + &mut self, + query: &air::ast::Query, + snapshots: &air::ast::Snapshots, + _: &[air::ast::Decl], + ) { + self.query_lowered_count += 1; + self.query_snapshot_counts.push(snapshots.len()); + let (breakables, breaks) = count_break_stmts(&query.assertion); + self.breakable_count += breakables; + self.break_count += breaks; + self.events.push("query_lowered".to_string()); + } + fn on_wp_version_created( + &mut self, + versioned: &air::ast::Ident, + kind: air::air_observer::VersionOrigin, + ) { + self.events.push(format!("wp_version:{:?}", kind)); + if let Some(stm) = self.correlator.resolve(versioned, kind) { + if let Some(line) = vir::vir_observer::line_from_span(&stm.span) { + let kind_str = format!("{:?}", kind); + self.version_correlations.push((versioned.to_string(), line, kind_str)); + } + } + } + fn on_lambda_decl( + &mut self, + name: &air::ast::Ident, + _: &[air::ast::Ident], + _: &air::ast::Expr, + ) { + self.lambda_decls.push(name.to_string()); + self.events.push(format!("lambda_decl:{}", name)); + } + fn on_choose_decl(&mut self, name: &air::ast::Ident, _: &air::ast::Ident) { + self.choose_decls.push(name.to_string()); + self.events.push(format!("choose_decl:{}", name)); + } + fn on_axiom_decl(&mut self, _expr: &air::ast::Expr) { + self.axiom_decls += 1; + } + fn as_any(&self) -> &dyn Any { + self + } + fn as_any_mut(&mut self) -> &mut dyn Any { + self + } +} + +impl air::query_result_observer::QueryResultObserver for TestObserver { + fn on_check_valid_result(&mut self, result: &mut air::query_result_observer::CheckValidResult) { + match result { + air::query_result_observer::CheckValidResult::Invalid { + model_defs, + eval_bool_expr, + .. + } => { + self.events.push("check_valid:Invalid".to_string()); + self.check_valid_invalid_count += 1; + self.check_valid_invalid_model_size.push(model_defs.len()); + // Pin the evaluator's three-way contract: a true boolean, a false boolean, + // and a non-boolean (unevaluable) expression. + let true_expr = + std::sync::Arc::new(air::ast::ExprX::Const(air::ast::Constant::Bool(true))); + self.eval_expr_results.push(eval_bool_expr(&true_expr)); + let false_expr = + std::sync::Arc::new(air::ast::ExprX::Const(air::ast::Constant::Bool(false))); + self.eval_expr_results.push(eval_bool_expr(&false_expr)); + let non_bool = std::sync::Arc::new(air::ast::ExprX::Const( + air::ast::Constant::Nat(std::sync::Arc::new("42".to_string())), + )); + self.eval_expr_results.push(eval_bool_expr(&non_bool)); + } + air::query_result_observer::CheckValidResult::Valid { assert_ids, usage_info } => { + self.events.push("check_valid:Valid".to_string()); + self.check_valid_valid_count += 1; + // A discharged query names the obligations it checked (ids may be None for + // assertions the lowering left unlabeled). + self.valid_assert_id_counts.push(assert_ids.iter().filter(|a| a.is_some()).count()); + // Usage data is opt-in: the count of used axioms when reporting is on, else None. + self.valid_used_axiom_counts.push(match usage_info { + air::context::UsageInfo::UsedAxioms(names) => Some(names.len()), + air::context::UsageInfo::None => None, + }); + } + air::query_result_observer::CheckValidResult::Timeout { .. } => { + self.events.push("check_valid:Timeout".to_string()); + self.check_valid_timeout += 1; + } + } + } + fn as_any(&self) -> &dyn Any { + self + } + fn as_any_mut(&mut self) -> &mut dyn Any { + self + } +} + +impl vir::vir_observer::VirObserver for TestObserver { + fn on_krate( + &mut self, + krate: &vir::ast::Krate, + _name_ctxt: &vir::def::NameCtxt, + _current_crate: &vir::ast::CrateId, + ) { + self.krate_function_names = krate.functions.iter().map(fun_name).collect(); + self.krate_datatype_names = krate.datatypes.iter().map(dt_name).collect(); + self.events.push("krate".to_string()); + } + fn on_havoc(&mut self, stm: &vir::sst::Stm, var: &vir::ast::VarIdent) { + let base = vir::def::suffix_local_unique_id(var); + self.havocs.push(base.to_string()); + self.events.push(format!("havoc:{}", base)); + self.correlator.record_havoc_or_assign(&base, stm); + } + fn on_assign(&mut self, stm: &vir::sst::Stm, var: &vir::ast::VarIdent) { + let base = vir::def::suffix_local_unique_id(var); + self.assigns.push(base.to_string()); + self.events.push(format!("assign:{}", base)); + self.correlator.record_havoc_or_assign(&base, stm); + } + fn on_branch_merge(&mut self, _stm: &vir::sst::Stm) { + self.branch_merges += 1; + self.events.push("branch_merge".to_string()); + } + fn on_variable_def(&mut self, _stm: &vir::sst::Stm, var: &vir::ast::VarIdent) { + self.variable_defs.push(vir::def::suffix_local_unique_id(var).to_string()); + self.events.push(format!("variable_def:{}", vir::def::suffix_local_unique_id(var))); + } + fn on_for_loop(&mut self, _stm: &vir::sst::Stm) { + self.for_loop_vars.push(("for_loop".to_string(), "detected".to_string())); + self.events.push("for_loop".to_string()); + } + fn on_reveal_string(&mut self, lit: &std::sync::Arc) { + self.reveal_strings.push((**lit).clone()); + self.events.push("reveal".to_string()); + } + fn on_quantifier_binder( + &mut self, + binder: &vir::ast::VarBinder, + _exp: &vir::sst::Exp, + ) { + let name = binder.name.lower().to_string(); + self.quantifier_binders.push(name.clone()); + self.events.push(format!("quant_binder:{}", name)); + if self.body_lowering_started { + self.post_body_binders.push(name); + } else { + self.pre_body_binders.push(name); + } + } + fn on_body_lowering_start(&mut self) { + self.body_lowering_started = true; + self.events.push("body_start".to_string()); + } + fn make_assert_id( + &mut self, + kind: &vir::vir_observer::AssertIdKind, + _index: usize, + parent: &Option, + ) -> Option { + self.assert_id_kinds.push(format!("{:?}", kind)); + self.events.push(format!("assert_id:{:?}", kind)); + parent.clone() + } + fn on_quantifier_binder_decl(&mut self, var: &vir::ast::VarIdent) { + self.binder_decls.push(vir::def::suffix_local_unique_id(var).to_string()); + self.events.push(format!("binder_decl:{}", vir::def::suffix_local_unique_id(var))); + } + fn on_function_lowered(&mut self) { + self.function_lowered_count += 1; + self.body_lowering_started = false; + self.events.push("function_lowered".to_string()); + } + fn as_any(&self) -> &dyn Any { + self + } + fn as_any_mut(&mut self) -> &mut dyn Any { + self + } +} + +// --------------------------------------------------------------------------- +// Dedicated single-trait observers. +// +// Each implements exactly ONE observer trait. They serve double duty: +// (1) focused functional coverage of that trait's callbacks (payloads + +// within-trait order), on inputs designed to elicit them; and +// (2) a compile-time + runtime proof of decoupling — a single-trait `impl` +// compiles and binds without requiring the other traits, and the +// unrelated registry slots stay `None`. +// --------------------------------------------------------------------------- + +/// Implements only `AirObserver`. +pub struct AirOnlyObserver { + pub events: Vec, + pub lambda_decls: Vec, + pub choose_decls: Vec, + pub query_lowered: usize, + pub axiom_decls: usize, +} +impl AirOnlyObserver { + pub fn new() -> Self { + AirOnlyObserver { + events: vec![], + lambda_decls: vec![], + choose_decls: vec![], + query_lowered: 0, + axiom_decls: 0, + } + } + pub fn summary_json(&self) -> String { + format!( + "AIROBS:{{\"events\":{},\"lambda_decls\":{},\"choose_decls\":{},\"query_lowered\":{},\"axiom_decls\":{}}}", + TestObserver::json_strings(&self.events), + TestObserver::json_strings(&self.lambda_decls), + TestObserver::json_strings(&self.choose_decls), + self.query_lowered, + self.axiom_decls, + ) + } +} +impl air::air_observer::AirObserver for AirOnlyObserver { + fn on_query_lowered( + &mut self, + _: &air::ast::Query, + _: &air::ast::Snapshots, + _: &[air::ast::Decl], + ) { + self.query_lowered += 1; + self.events.push("query_lowered".to_string()); + } + fn on_wp_version_created( + &mut self, + _: &air::ast::Ident, + kind: air::air_observer::VersionOrigin, + ) { + self.events.push(format!("wp_version:{:?}", kind)); + } + fn on_lambda_decl( + &mut self, + name: &air::ast::Ident, + _: &[air::ast::Ident], + _: &air::ast::Expr, + ) { + self.lambda_decls.push(name.to_string()); + self.events.push(format!("lambda_decl:{}", name)); + } + fn on_choose_decl(&mut self, name: &air::ast::Ident, _: &air::ast::Ident) { + self.choose_decls.push(name.to_string()); + self.events.push(format!("choose_decl:{}", name)); + } + fn on_axiom_decl(&mut self, _expr: &air::ast::Expr) { + self.axiom_decls += 1; + } + fn as_any(&self) -> &dyn Any { + self + } + fn as_any_mut(&mut self) -> &mut dyn Any { + self + } +} + +/// Implements only `QueryResultObserver` — receives `Invalid`/`Valid`/`Timeout` +/// and exercises the live `eval_bool_expr` closure on `Invalid`. Proves a +/// results-only consumer couples nothing else. +pub struct QueryResultOnlyObserver { + pub events: Vec, + pub invalid: usize, + pub valid: usize, + pub timeout: usize, + pub eval_expr_results: Vec>, +} +impl QueryResultOnlyObserver { + pub fn new() -> Self { + QueryResultOnlyObserver { + events: vec![], + invalid: 0, + valid: 0, + timeout: 0, + eval_expr_results: vec![], + } + } + pub fn summary_json(&self) -> String { + format!( + "QROBS:{{\"events\":{},\"invalid\":{},\"valid\":{},\"timeout\":{},\"eval_expr_results\":{}}}", + TestObserver::json_strings(&self.events), + self.invalid, + self.valid, + self.timeout, + TestObserver::json_opt_bools(&self.eval_expr_results), + ) + } +} +impl air::query_result_observer::QueryResultObserver for QueryResultOnlyObserver { + fn on_check_valid_result(&mut self, result: &mut air::query_result_observer::CheckValidResult) { + match result { + air::query_result_observer::CheckValidResult::Invalid { eval_bool_expr, .. } => { + self.invalid += 1; + self.events.push("check_valid:Invalid".to_string()); + let true_expr = + std::sync::Arc::new(air::ast::ExprX::Const(air::ast::Constant::Bool(true))); + self.eval_expr_results.push(eval_bool_expr(&true_expr)); + } + air::query_result_observer::CheckValidResult::Valid { .. } => { + self.valid += 1; + self.events.push("check_valid:Valid".to_string()); + } + air::query_result_observer::CheckValidResult::Timeout { .. } => { + self.timeout += 1; + self.events.push("check_valid:Timeout".to_string()); + } + } + } + fn as_any(&self) -> &dyn Any { + self + } + fn as_any_mut(&mut self) -> &mut dyn Any { + self + } +} + +/// Implements only `VirObserver`. +pub struct VirOnlyObserver { + pub events: Vec, + pub function_names: Vec, + pub havocs: Vec, + pub assigns: Vec, + pub function_lowered: usize, +} +impl VirOnlyObserver { + pub fn new() -> Self { + VirOnlyObserver { + events: vec![], + function_names: vec![], + havocs: vec![], + assigns: vec![], + function_lowered: 0, + } + } + pub fn summary_json(&self) -> String { + format!( + "VIROBS:{{\"events\":{},\"function_names\":{},\"havocs\":{},\"assigns\":{},\"function_lowered\":{}}}", + TestObserver::json_strings(&self.events), + TestObserver::json_strings(&self.function_names), + TestObserver::json_strings(&self.havocs), + TestObserver::json_strings(&self.assigns), + self.function_lowered, + ) + } +} +impl vir::vir_observer::VirObserver for VirOnlyObserver { + fn on_krate(&mut self, krate: &vir::ast::Krate, _: &vir::def::NameCtxt, _: &vir::ast::CrateId) { + self.function_names = krate.functions.iter().map(fun_name).collect(); + self.events.push("krate".to_string()); + } + fn on_havoc(&mut self, _stm: &vir::sst::Stm, var: &vir::ast::VarIdent) { + let base = vir::def::suffix_local_unique_id(var); + self.havocs.push(base.to_string()); + self.events.push(format!("havoc:{}", base)); + } + fn on_assign(&mut self, _stm: &vir::sst::Stm, var: &vir::ast::VarIdent) { + let base = vir::def::suffix_local_unique_id(var); + self.assigns.push(base.to_string()); + self.events.push(format!("assign:{}", base)); + } + fn on_function_lowered(&mut self) { + self.function_lowered += 1; + self.events.push("function_lowered".to_string()); + } + fn as_any(&self) -> &dyn Any { + self + } + fn as_any_mut(&mut self) -> &mut dyn Any { + self + } +} diff --git a/source/rust_verify/src/verifier.rs b/source/rust_verify/src/verifier.rs index eddefbd3ba..fe279958f8 100644 --- a/source/rust_verify/src/verifier.rs +++ b/source/rust_verify/src/verifier.rs @@ -29,6 +29,75 @@ use rustc_error_messages::MultiSpan; use rustc_index::bit_set::DenseBitSet; use rustc_middle::ty::TyCtxt; use rustc_span::Span; + +/// Build the observer registry for a given observer name. The concrete type is +/// known here, so each `Arc>` is coerced (unsizing) into an +/// independent per-trait handle. A consumer that implements only a subset of the +/// traits populates only those slots. `TestObserver` implements all three. +fn create_observer(name: &str) -> vir::vir_observer::Observers { + use std::sync::{Arc, Mutex}; + match name { + "test" => { + let o = Arc::new(Mutex::new(crate::test_observer::TestObserver::new())); + let vir: vir::vir_observer::VirObserverHandle = o.clone(); + let air: air::air_observer::AirObserverHandle = o.clone(); + let query_result: air::query_result_observer::QueryResultObserverHandle = o.clone(); + vir::vir_observer::Observers { + vir: Some(vir), + air: Some(air), + query_result: Some(query_result), + } + } + // Dedicated single-trait observers: each populates only its own slot, + // proving a consumer couples nothing it does not implement. + "air-only" => { + let o = Arc::new(Mutex::new(crate::test_observer::AirOnlyObserver::new())); + let air: air::air_observer::AirObserverHandle = o; + vir::vir_observer::Observers { air: Some(air), ..Default::default() } + } + "query-result-only" => { + let o = Arc::new(Mutex::new(crate::test_observer::QueryResultOnlyObserver::new())); + let qr: air::query_result_observer::QueryResultObserverHandle = o; + vir::vir_observer::Observers { query_result: Some(qr), ..Default::default() } + } + "vir-only" => { + let o = Arc::new(Mutex::new(crate::test_observer::VirOnlyObserver::new())); + let vir: vir::vir_observer::VirObserverHandle = o; + vir::vir_observer::Observers { vir: Some(vir), ..Default::default() } + } + // parse_args rejected any other name + _ => unreachable!("unknown observer {name}"), + } +} + +fn create_observer_from_args(names: &[String]) -> vir::vir_observer::Observers { + // `coverage` and `proof-state` are one object, so they may be named together. + if let Some(o) = crate::observers::ObligationObserver::from_names(names) { + let o = Arc::new(std::sync::Mutex::new(o)); + let air: air::air_observer::AirObserverHandle = o.clone(); + let query_result: air::query_result_observer::QueryResultObserverHandle = o; + return vir::vir_observer::Observers { + air: Some(air), + query_result: Some(query_result), + ..Default::default() + }; + } + // parse_args allows a test observer only alone + names.first().map_or_else(Default::default, |n| create_observer(n)) +} + +fn emit_observer_summaries(any: &dyn std::any::Any, reporter: &impl air::messages::Diagnostics) { + if let Some(o) = any.downcast_ref::() { + reporter.report(¬e_bare(&o.summary_json()).to_any()); + } else if let Some(o) = any.downcast_ref::() { + reporter.report(¬e_bare(&o.summary_json()).to_any()); + } else if let Some(o) = any.downcast_ref::() { + reporter.report(¬e_bare(&o.summary_json()).to_any()); + } else if let Some(o) = any.downcast_ref::() { + reporter.report(¬e_bare(&o.summary_json()).to_any()); + } +} + use rustc_span::def_id::LOCAL_CRATE; use rustc_span::source_map::SourceMap; use std::collections::{HashMap, HashSet, VecDeque}; @@ -433,6 +502,9 @@ pub struct Verifier { /// Under `-V inst-pressure`: what cvc5 reported for each query of each /// function, by qid, in check order func_inst_pressure: HashMap>, + /// Under `-V observers=coverage` / `proof-state`: each query's + /// obligations and failing-assert counterexamples, not yet rendered. + func_observations: HashMap>, /// Errors to report after verification has run deferred_errors: Vec, /// Every diagnostic raised while verifying a function's obligations, @@ -504,6 +576,12 @@ pub struct FuncDetails { /// filled under `-V inst-pressure` #[serde(skip_serializing_if = "Vec::is_empty")] pub inst_pressure: Vec, + /// filled under `-V observers=coverage` + #[serde(skip_serializing_if = "Vec::is_empty")] + pub obligations: Vec, + /// filled under `-V observers=proof-state` + #[serde(skip_serializing_if = "Vec::is_empty")] + pub failing_asserts: Vec, } impl Default for FuncDetails { @@ -517,6 +595,8 @@ impl Default for FuncDetails { nl_frontier: Default::default(), matching_loops: Default::default(), inst_pressure: Default::default(), + obligations: Default::default(), + failing_asserts: Default::default(), } } } @@ -531,6 +611,8 @@ impl FuncDetails { self.nl_frontier.extend(other.nl_frontier); self.matching_loops.extend(other.matching_loops); self.inst_pressure.extend(other.inst_pressure); + self.obligations.extend(other.obligations); + self.failing_asserts.extend(other.failing_asserts); } pub fn to_json(&self) -> serde_json::Value { @@ -708,6 +790,7 @@ impl Verifier { func_nl_frontier: HashMap::new(), func_matching_loops: HashMap::new(), func_inst_pressure: HashMap::new(), + func_observations: HashMap::new(), deferred_errors: Vec::new(), raised_diagnostics: Vec::new(), reported_diagnostics: Vec::new(), @@ -770,6 +853,7 @@ impl Verifier { func_nl_frontier: HashMap::new(), func_matching_loops: HashMap::new(), func_inst_pressure: HashMap::new(), + func_observations: HashMap::new(), deferred_errors: Vec::new(), raised_diagnostics: Vec::new(), reported_diagnostics: Vec::new(), @@ -829,6 +913,9 @@ impl Verifier { for (fun, queries) in other.func_inst_pressure { self.func_inst_pressure.entry(fun).or_default().extend(queries); } + for (fun, queries) in other.func_observations { + self.func_observations.entry(fun).or_default().extend(queries); + } self.deferred_errors.extend(other.deferred_errors); } @@ -1143,6 +1230,9 @@ impl Verifier { let mut invalidity = false; let mut timed_out = false; let mut used_axioms = None; + // the ids of this query's failures without a model, which an + // observer's Invalid callback did not see + let mut failed_here: Vec> = Vec::new(); // 0 for the query's first check, then one per multi-error round let mut round = 0usize; loop { @@ -1275,6 +1365,10 @@ impl Verifier { ValidityResult::Invalid(None, error, assert_id_opt) | ValidityResult::Invalid(_, error @ None, assert_id_opt) => { // no model, but the obligation may still be known + // No model, so no observer callback: the observer + // places this failure from its id (none for a + // bit-vector assert) when the query is drained. + failed_here.push(assert_id_opt.clone()); // Borrowed, not moved: the report reads the same id below. if let Some(assert_id) = &assert_id_opt { if prover_choice == vir::def::ProverChoice::DefaultProver { @@ -1305,6 +1399,7 @@ impl Verifier { break; } ValidityResult::Invalid(Some(air_model), Some(error), assert_id_opt) => { + // The observer saw this one through its Invalid callback. // Borrowed, not moved: the report reads the same id below. if let Some(assert_id) = &assert_id_opt { if prover_choice == vir::def::ProverChoice::DefaultProver { @@ -1406,6 +1501,23 @@ impl Verifier { } if is_check_valid && !is_singular { + if let Some(obs) = air_context.query_result_observer() { + let mut obs = obs.lock().unwrap(); + if let Some(o) = + obs.as_any_mut().downcast_mut::() + { + if let Some(raw) = o.take_query(&failed_here, timed_out, only_check_earlier) { + self.func_observations.entry(context.fun.clone()).or_default().push( + crate::observers::FiledQuery { + desc: context.desc.clone(), + span: context.span.as_string.clone(), + kind: query_op.kind(), + raw, + }, + ); + } + } + } air_context.finish_query(); } @@ -1636,6 +1748,17 @@ impl Verifier { } } + /// Render each query's observed obligations and counterexamples as + /// source, per function. + fn resolve_observations(&mut self, names: &vir::air_names::SourceNames) { + for (fun, queries) in std::mem::take(&mut self.func_observations) { + let (obligations, failing) = crate::observers::resolve(names, queries); + let details = self.func_details.entry(fun).or_default(); + details.obligations.extend(obligations); + details.failing_asserts.extend(failing); + } + } + /// Join each query's instantiation pressure to source, per function. fn resolve_inst_pressure(&mut self, symbols: &crate::provenance::Symbols) { for (fun, queries) in std::mem::take(&mut self.func_inst_pressure) { @@ -1885,6 +2008,10 @@ impl Verifier { prover_choice, )?; + // Attach the same shared observer object to the spinoff context via its + // per-trait handles (real trait-object views of one object — no bridge). + air_context.set_observers(ctx.air_observer.clone(), ctx.query_result_observer.clone()); + // Write the span of spun-off query air_context.comment(&span.as_string); air_context.blank_line(); @@ -1962,6 +2089,13 @@ impl Verifier { profile_all_file_name.as_ref(), vir::def::ProverChoice::DefaultProver, )?; + + // Attach the same shared observer object to air::Context via its per-trait + // handles. All views point at one object; the Arc keeps it alive on both + // ctx (VIR callbacks during lowering) and air_context (AIR callbacks + + // query results during verification). + air_context.set_observers(ctx.air_observer.clone(), ctx.query_result_observer.clone()); + if self.args.solver_version_check { air_context.set_expected_solver_version(match self.args.solver { air::context::SmtSolver::Z3 => crate::consts::expected_z3_version().to_string(), @@ -2615,6 +2749,16 @@ impl Verifier { let (time_smt_init, time_smt_run) = air_context.get_time(); let rlimit_count = air_context.get_rlimit_count(); + // Emit observer summaries as diagnostic notes. Only one underlying object + // exists; try each handle (a single-trait observer populates only one). + if let Some(obs_cell) = &ctx.observer { + emit_observer_summaries(obs_cell.lock().unwrap().as_any(), reporter); + } else if let Some(obs_cell) = &ctx.air_observer { + emit_observer_summaries(obs_cell.lock().unwrap().as_any(), reporter); + } else if let Some(obs_cell) = &ctx.query_result_observer { + emit_observer_summaries(obs_cell.lock().unwrap().as_any(), reporter); + } + if let Some(journal) = resident { self.resident_buckets.push(crate::resident::RetainedBucket::new( bucket_id.clone(), @@ -2698,6 +2842,7 @@ impl Verifier { fndef_types, resolved_typs.unwrap(), self.args.debugger, + create_observer_from_args(&self.args.observers), )?; if self.args.log_all || self.args.log_args.log_vir_poly { let mut file = @@ -3283,6 +3428,9 @@ impl Verifier { self.resolve_unknown_reasons(&global_ctx); // Join the diagnostics raised while verifying to their source spans. self.resolve_raised_diagnostics(&reporter); + if !self.func_observations.is_empty() { + self.resolve_observations(&global_ctx.air_source_names.borrow().clone()); + } // Join what cvc5 reported (matching loops, instantiation pressure, // difficulty, provenance, nonlinear frontiers) back to source, per // function. The joins read the same symbols. diff --git a/source/rust_verify_test/tests/common/mod.rs b/source/rust_verify_test/tests/common/mod.rs index c1210d5cea..dd4d54ee41 100644 --- a/source/rust_verify_test/tests/common/mod.rs +++ b/source/rust_verify_test/tests/common/mod.rs @@ -324,6 +324,9 @@ pub fn run_verus( } else if *option == "-V difficulty" { verus_args.push("-V".to_string()); verus_args.push("difficulty".to_string()); + } else if *option == "-V axiom-usage-info" { + verus_args.push("-V".to_string()); + verus_args.push("axiom-usage-info".to_string()); } else if *option == "-V spinoff-all" { verus_args.push("-V".to_string()); verus_args.push("spinoff-all".to_string()); @@ -344,6 +347,14 @@ pub fn run_verus( verus_args.extend(["-V".to_string(), format!("tla-export={module}")]); } else if let Some(dir) = option.strip_prefix("--log-dir ") { verus_args.extend(["--log-dir".to_string(), dir.to_string()]); + } else if option.starts_with("observers=") || option.starts_with("observer=") { + verus_args.push("-V".to_string()); + if option.starts_with("observer=") && !option.starts_with("observers=") { + // Normalize singular to plural form + verus_args.push(format!("observers={}", &option["observer=".len()..])); + } else { + verus_args.push(option.to_string()); + } } else { panic!("option '{}' not recognized by test harness", option); } diff --git a/source/rust_verify_test/tests/obligation_observer.rs b/source/rust_verify_test/tests/obligation_observer.rs new file mode 100644 index 0000000000..bc59494f17 --- /dev/null +++ b/source/rust_verify_test/tests/obligation_observer.rs @@ -0,0 +1,341 @@ +//! `-V observers=coverage` and `-V observers=proof-state`, read back from +//! `--report-json`. These run cvc5 (no internal test mode), which is what +//! `proof-state`'s live model evaluation has to work against. + +#![feature(rustc_private)] +#[macro_use] +mod common; +use common::*; + +use tempfile::TempDir; + +/// Verify `code` with the given observers and return the per-function +/// details of the report. +fn functions_for(code: &str, extra: &[&str]) -> serde_json::Value { + let tempdir = TempDir::new().expect("temp dir"); + let entry_file = tempdir.path().join("test.rs"); + let source = format!("{}\n{}\n{}\n", FEATURE_PRELUDE, USE_PRELUDE, code); + std::fs::write(&entry_file, source).expect("write source file"); + let report_path = tempdir.path().join("report.json"); + let mut args = vec!["--crate-type=lib", "--report-json", report_path.to_str().unwrap()]; + args.extend_from_slice(extra); + args.push(entry_file.to_str().unwrap()); + let output = run_verus_raw(&args, tempdir.path()); + let text = std::fs::read_to_string(&report_path).unwrap_or_else(|err| { + panic!( + "no report at {}: {err}\nstderr:\n{}", + report_path.display(), + String::from_utf8_lossy(&output.stderr) + ) + }); + let report: serde_json::Value = serde_json::from_str(&text).expect("valid json"); + report["functions"].clone() +} + +/// Each obligation of `f`'s queries as (message, status), in query order. +fn statuses(functions: &serde_json::Value, f: &str) -> Vec<(String, String)> { + functions[f]["obligations"] + .as_array() + .unwrap_or_else(|| panic!("no obligations for {}: {:#}", f, functions)) + .iter() + .flat_map(|q| q["obligations"].as_array().unwrap().iter()) + .map(|o| { + (o["message"].as_str().unwrap().to_string(), o["status"].as_str().unwrap().to_string()) + }) + .collect() +} + +const CODE: &str = r#" +verus!{ +fn bump(x: u32, y: u32) -> (r: u32) + requires x < 100, y < 100, + ensures r == x + y + 1, +{ + x + y +} + +fn fine(a: u32) -> (r: u32) + requires a < 10, + ensures r < 20, +{ + let b = a + 1; + assert(b <= 10); + b + 1 +} + +fn loops(n: u32) + requires n < 50, +{ + let mut i = 0; + while i < n + invariant i <= n, i < 40, + decreases n - i, + { + i = i + 1; + } +} + +fn two_bad(a: u32) { + assert(a < 5); + assert(a > 7); +} +} +"#; + +#[test] +fn coverage_says_what_became_of_each_obligation() { + let functions = functions_for(CODE, &["-V", "observers=coverage"]); + let s = |m: &str, st: &str| (m.to_string(), st.to_string()); + assert_eq!( + statuses(&functions, "test::fine"), + vec![ + s("possible arithmetic underflow/overflow", "proved"), + s("assertion failed", "proved"), + s("possible arithmetic underflow/overflow", "proved"), + s("postcondition not satisfied", "proved"), + ] + ); + assert!( + statuses(&functions, "test::bump").contains(&s("postcondition not satisfied", "failed")) + ); + // coverage alone does not collect counterexamples + assert!(functions["test::bump"].get("failing_asserts").is_none()); +} + +/// Loop invariants carry no assertion id: the failure is placed by its span, +/// not on the first id-less invariant. +#[test] +fn an_id_less_failure_lands_on_the_invariant_that_failed() { + let functions = functions_for(CODE, &["-V", "observers=coverage"]); + let loop_query = functions["test::loops"]["obligations"] + .as_array() + .unwrap() + .iter() + .find(|q| q["desc"] == "while loop") + .expect("the loop's query") + .clone(); + let ends: Vec<(String, String)> = loop_query["obligations"] + .as_array() + .unwrap() + .iter() + .filter(|o| o["message"] == "invariant not satisfied at end of loop body") + .map(|o| { + (o["span"].as_str().unwrap().to_string(), o["status"].as_str().unwrap().to_string()) + }) + .collect(); + assert_eq!(ends.len(), 2, "{ends:?}"); + assert_eq!(ends[0].1, "proved", "i <= n holds: {ends:?}"); + assert_eq!(ends[1].1, "failed", "i < 40 fails: {ends:?}"); +} + +/// With `--multiple-errors 0` the query ends at the first failure, so the +/// later assertion is unchecked, not proved. +#[test] +fn a_query_that_stops_early_leaves_obligations_unchecked() { + let functions = functions_for(CODE, &["-V", "observers=coverage", "--multiple-errors", "0"]); + let s = |m: &str, st: &str| (m.to_string(), st.to_string()); + assert_eq!( + statuses(&functions, "test::two_bad"), + vec![s("assertion failed", "failed"), s("assertion failed", "unchecked")] + ); +} + +/// When the `--multiple-errors` budget runs out, the last round disables every +/// assertion after the first failure. Whichever failure the solver finds first, +/// `b + 0 == b` between the two is never proved, so it is unchecked. +#[test] +fn a_truncated_query_leaves_obligations_after_the_first_failure_unchecked() { + let code = r#" +verus!{ +fn tricky(a: u32, b: u32) { + assert(b == b); + assert(a != 123456); + assert(b + 0 == b); + assert(a != 0); +} +} +"#; + let functions = functions_for(code, &["-V", "observers=coverage", "--multiple-errors", "2"]); + let st: Vec = + statuses(&functions, "test::tricky").into_iter().map(|(_, status)| status).collect(); + assert_eq!(st, ["proved", "failed", "unchecked", "failed"]); +} + +/// The counterexample is read while it is live: the false conjunct, in +/// source spelling, and the value the loop counter has there. +#[test] +fn proof_state_reports_the_false_conjunct_and_its_values() { + let functions = functions_for(CODE, &["-V", "observers=proof-state"]); + let failing = functions["test::loops"]["failing_asserts"].as_array().expect("failing_asserts"); + assert_eq!(failing.len(), 1, "{failing:#?}"); + let f = &failing[0]; + assert_eq!(f["message"], "invariant not satisfied at end of loop body"); + assert_eq!(f["conjuncts"][0], serde_json::json!({ "term": "(i < 40)", "value": false })); + let i = f["values"] + .as_array() + .unwrap() + .iter() + .find(|v| v["name"] == "i") + .unwrap_or_else(|| panic!("no value for i: {:#}", f)); + assert_eq!(i["value"], "40"); + // proof-state alone does not collect coverage + assert!(functions["test::loops"].get("obligations").is_none()); + + let bump = &functions["test::bump"]["failing_asserts"][0]; + assert_eq!(bump["conjuncts"][0]["term"], "(r == ((x + y) + 1))"); + assert_eq!(bump["conjuncts"][0]["value"], false); +} + +const MORE: &str = r#" +use vstd::prelude::*; +verus!{ +fn conj(a: u32, b: u32) + requires a > 2, +{ + assert(a > 3 && b < 2); +} + +fn bits(x: u32) { + assert(x & 1 == 0) by (bit_vector); +} + +fn callee(y: u32, z: u32) + requires y > 5 && y < z, z < 100, +{ +} + +fn caller(y: u32) { + callee(y, 7); +} + +fn all_big(v: &Vec) -> (r: u64) + requires v.len() > 0, + ensures forall|i: int| 0 <= i < v.len() ==> v[i] <= r, +{ + v[0] +} + +fn fine(a: u32) -> (r: u32) + requires a < 10, + ensures r == a, +{ + a +} +} +"#; + +/// The failing assertion of `f`, as (term, value) per conjunct, and the +/// symbols it reports values for. +fn failing( + functions: &serde_json::Value, + f: &str, +) -> (Vec<(String, serde_json::Value)>, Vec) { + let failing = functions[f]["failing_asserts"] + .as_array() + .unwrap_or_else(|| panic!("no failing_asserts for {}: {:#}", f, functions[f])); + assert_eq!(failing.len(), 1, "{failing:#?}"); + let conjuncts = failing[0]["conjuncts"] + .as_array() + .unwrap() + .iter() + .map(|c| (c["term"].as_str().unwrap().to_string(), c["value"].clone())) + .collect(); + let symbols = failing[0]["values"] + .as_array() + .unwrap() + .iter() + .map(|v| v["symbol"].as_str().unwrap().to_string()) + .collect(); + (conjuncts, symbols) +} + +/// `assert(a && b)` asserts a Verus temporary; proof-state splits it into +/// the conjuncts of its definition and reports the variables they read. +#[test] +fn proof_state_splits_an_asserted_conjunction() { + let functions = functions_for(MORE, &["-V", "observers=proof-state"]); + let (conjuncts, symbols) = failing(&functions, "test::conj"); + assert_eq!( + conjuncts, + vec![ + ("(a > 3)".to_string(), serde_json::json!(false)), + ("(b < 2)".to_string(), serde_json::json!(true)), + ] + ); + assert_eq!(symbols, vec!["a!", "b!"]); +} + +/// A failing call's precondition splits into the callee's requires +/// clauses at the call's arguments. +#[test] +fn proof_state_splits_a_callee_precondition() { + let functions = functions_for(MORE, &["-V", "observers=proof-state"]); + let (conjuncts, symbols) = failing(&functions, "test::caller"); + let terms: Vec<&str> = conjuncts.iter().map(|(t, _)| t.as_str()).collect(); + assert_eq!(terms, vec!["(y > 5)", "(y < 7)", "(7 < 100)"]); + assert_eq!(conjuncts[0].1, serde_json::json!(false)); + assert_eq!(symbols, vec!["y!"]); +} + +/// Values are the program's: the encoding's type ids and decorations +/// (`INT`, `$`, `TYPE%...`) are left out. +#[test] +fn proof_state_values_leave_out_encoding_constants() { + let functions = functions_for(MORE, &["-V", "observers=proof-state"]); + let (_, symbols) = failing(&functions, "test::all_big"); + assert_eq!(symbols, vec!["r!", "v!"]); +} + +/// A bit-vector assert fails without a model and without an assertion id; +/// coverage still says it failed. +#[test] +fn coverage_marks_a_failing_bit_vector_assert_failed() { + let functions = functions_for(MORE, &["-V", "observers=coverage"]); + let s = |m: &str, st: &str| (m.to_string(), st.to_string()); + assert!( + statuses(&functions, "test::bits") + .contains(&s("bitvector assertion not satisfied", "failed")), + "{:#}", + functions["test::bits"] + ); +} + +/// Under `-V axiom-usage-info` a proved query lists its unsat core; cvc5 +/// prints the core over several lines. +#[test] +fn coverage_lists_used_axioms_under_cvc5() { + let functions = functions_for(MORE, &["-V", "observers=coverage", "-V", "axiom-usage-info"]); + let queries = functions["test::fine"]["obligations"].as_array().expect("obligations"); + let body = queries.iter().find(|q| q["kind"] == "body").expect("the body query"); + assert!(body["used_axioms"].is_array(), "{:#}", body); + let with_axioms = functions + .as_object() + .unwrap() + .values() + .flat_map(|f| f["obligations"].as_array().into_iter().flatten()) + .filter(|q| q["used_axioms"].as_array().is_some_and(|a| !a.is_empty())) + .count(); + assert!(with_axioms > 0, "no proved query named an axiom: {:#}", functions); +} + +/// An observer name Verus does not know is an error, not a run without it. +#[test] +fn unknown_observer_names_are_rejected() { + for (names, expected) in [ + ("covrage", "unknown observer `covrage`"), + ("coverage,", "unknown observer ``"), + ("test,coverage", "cannot be combined"), + ] { + let tempdir = TempDir::new().expect("temp dir"); + let entry_file = tempdir.path().join("test.rs"); + std::fs::write(&entry_file, format!("{}\n{}\n", FEATURE_PRELUDE, USE_PRELUDE)).unwrap(); + let observers = format!("observers={names}"); + let output = run_verus_raw( + &["--crate-type=lib", "-V", &observers, entry_file.to_str().unwrap()], + tempdir.path(), + ); + let stderr = String::from_utf8_lossy(&output.stderr); + assert!(!output.status.success(), "{}: {}", names, stderr); + assert!(stderr.contains(expected), "{}: {}", names, stderr); + } +} diff --git a/source/rust_verify_test/tests/observer.rs b/source/rust_verify_test/tests/observer.rs new file mode 100644 index 0000000000..929b880c44 --- /dev/null +++ b/source/rust_verify_test/tests/observer.rs @@ -0,0 +1,1053 @@ +//! Observer e2e tests with strong oracles. +//! +//! Shared VC-shape seed corpus lives in `vc_shapes` (this branch), so all three layers' +//! suites can drive the same programs. This file adds event-trace oracles over selected seeds. +//! +//! Coverage matrix (+ = positive check, 0 = negative check): +//! +//! ```text +//! | loop | mut | valid | spec | break | for | inv | reveal | bvec | +//! ------------------------------------|------|------|-------|------|-------|------|------|--------|------| +//! on_krate (function names) | + | + | + | + | | | | | | +//! on_krate (datatype names) | + | + | | | | | | | | +//! on_havoc | + | 0 | 0 | 0 | + | + | + | | | +//! on_assign (names) | + | + | 0 | 0 | + | | + | | | +//! on_branch_merge | + | 0 | 0 | 0 | + | 0 | 0 | | | +//! on_variable_def (names) | + | | 0 | 0 | | | | | | +//! on_for_loop_var (ghost, user) | 0 | 0 | 0 | 0 | 0 | + | 0 | | | +//! on_reveal_string | | | | | | | | + | | +//! on_quantifier_binder (names) | 0 | + | 0 | + | 0 | 0 | 0 | | | +//! make_assert_id(Ensures) | + | + | + | + | + | | | | | +//! make_assert_id(LoopInvariant) | + | | | | + | | + | | | +//! make_assert_id(DecreasesCheck) | + | | | | + | | + | | | +//! on_function_lowered | + | + | + | + | + | | + | | | +//! on_query_lowered (count) | + | + | + | + | + | | + | | | +//! on_query_lowered (snapshots) | + | | + | | | | | | | +//! on_lambda_decl (names) | 0 | 0 | 0 | + | 0 | 0 | 0 | | | +//! on_choose_decl (names) | 0 | 0 | 0 | + | 0 | 0 | 0 | | | +//! check_valid_result(Invalid) | + | + | 0 | + | + | | + | + | + | +//! check_valid_result(Valid) | + | | + | | | | | | | +//! check_valid_result(Timeout) | | | | | | | | TODO | | +//! invalid model_defs size | + | + | | + | | | + | | | +//! eval_bool_expr during Invalid | + | | | | | | | | | +//! ``` + +#![feature(rustc_private)] +#[macro_use] +mod common; +use common::*; +mod vc_shapes; + +// ── JSON parsing (mirrors TestObserver data model) ── + +struct D { + krate_function_names: Vec, + krate_datatype_names: Vec, + havocs: Vec, + assigns: Vec, + branch_merges: usize, + variable_defs: Vec, + for_loop_vars: Vec<(String, String)>, + reveal_strings: Vec, + quantifier_binders: Vec, + assert_id_kinds: Vec, + function_lowered: usize, + query_lowered: usize, + query_snapshot_counts: Vec, + version_correlations: Vec<(String, u32, String)>, + lambda_decls: Vec, + choose_decls: Vec, + check_valid_invalid: usize, + check_valid_valid: usize, + check_valid_timeout: usize, + check_valid_invalid_model_size: Vec, + eval_expr_results: Vec>, + binder_decls: Vec, + breakable_count: usize, + break_count: usize, + valid_assert_id_counts: Vec, + valid_used_axiom_counts: Vec>, + pre_body_binders: Vec, + post_body_binders: Vec, + events: Vec, +} + +fn strings(s: &str) -> Vec { + let s = s.trim(); + if s == "[]" { + return vec![]; + } + s[1..s.len() - 1].split(',').map(|i| i.trim().trim_matches('"').to_string()).collect() +} +fn usizes(s: &str) -> Vec { + let s = s.trim(); + if s == "[]" { + return vec![]; + } + s[1..s.len() - 1].split(',').filter_map(|i| i.trim().parse().ok()).collect() +} +fn opt_usizes(s: &str) -> Vec> { + let s = s.trim(); + if s == "[]" { + return vec![]; + } + s[1..s.len() - 1].split(',').map(|i| i.trim().parse::().ok()).collect() +} + +fn opt_bools(s: &str) -> Vec> { + let s = s.trim(); + if s == "[]" { + return vec![]; + } + s[1..s.len() - 1] + .split(',') + .map(|i| match i.trim() { + "true" => Some(true), + "false" => Some(false), + _ => None, + }) + .collect() +} +fn nested_strings(s: &str) -> Vec> { + let s = s.trim(); + if s == "[]" { + return vec![]; + } + let inner = &s[1..s.len() - 1]; + let mut result = vec![]; + let mut depth = 0; + let mut start = 0; + for (i, c) in inner.char_indices() { + match c { + '[' => { + if depth == 0 { + start = i; + } + depth += 1; + } + ']' => { + depth -= 1; + if depth == 0 { + result.push(strings(&inner[start..=i])); + } + } + _ => {} + } + } + result +} +fn parse_version_correlations(s: &str) -> Vec<(String, u32, String)> { + let s = s.trim(); + if s == "[]" { + return vec![]; + } + // Format: [["name",line,"kind"],...] + let mut result = vec![]; + let inner = &s[1..s.len() - 1]; + let mut depth = 0; + let mut start = 0; + for (i, c) in inner.char_indices() { + match c { + '[' => { + if depth == 0 { + start = i; + } + depth += 1; + } + ']' => { + depth -= 1; + if depth == 0 { + let triple = &inner[start + 1..i]; + let parts: Vec<&str> = triple.splitn(3, ',').collect(); + if parts.len() == 3 { + let name = parts[0].trim().trim_matches('"').to_string(); + let line: u32 = parts[1].trim().parse().unwrap_or(0); + let kind = parts[2].trim().trim_matches('"').to_string(); + result.push((name, line, kind)); + } + } + } + _ => {} + } + } + result +} +fn string_pairs(s: &str) -> Vec<(String, String)> { + let nested = nested_strings(s); + nested + .into_iter() + .map(|v| { + assert_eq!(v.len(), 2); + (v[0].clone(), v[1].clone()) + }) + .collect() +} +fn val<'a>(json: &'a str, key: &str) -> &'a str { + let needle = format!("\"{}\":", key); + let start = json.find(&needle).unwrap_or_else(|| panic!("key '{}' not found", key)); + let rest = &json[start + needle.len()..]; + if rest.starts_with("[[") || rest.starts_with("[]") { + // nested array — find matching outer ] + let mut depth = 0; + for (i, c) in rest.char_indices() { + match c { + '[' => depth += 1, + ']' => { + depth -= 1; + if depth == 0 { + return &rest[..=i]; + } + } + _ => {} + } + } + rest + } else if rest.starts_with('[') { + &rest[..rest.find(']').unwrap() + 1] + } else { + let end = rest.find([',', '}']).unwrap_or(rest.len()); + rest[..end].trim() + } +} + +fn parse_note(note_text: &str) -> D { + let json = note_text + .strip_prefix("OBSERVER:") + .or_else(|| { + // Handle OBSERVER_N: prefix for composite + note_text.find(':').and_then(|i| { + if note_text[..i].starts_with("OBSERVER_") { + Some(¬e_text[i + 1..]) + } else { + None + } + }) + }) + .unwrap_or(note_text); + D { + krate_function_names: strings(val(json, "krate_function_names")), + krate_datatype_names: strings(val(json, "krate_datatype_names")), + havocs: strings(val(json, "havocs")), + assigns: strings(val(json, "assigns")), + branch_merges: val(json, "branch_merges").parse().unwrap(), + variable_defs: strings(val(json, "variable_defs")), + for_loop_vars: string_pairs(val(json, "for_loop_vars")), + reveal_strings: strings(val(json, "reveal_strings")), + quantifier_binders: strings(val(json, "quantifier_binders")), + assert_id_kinds: strings(val(json, "assert_id_kinds")), + function_lowered: val(json, "function_lowered").parse().unwrap(), + query_lowered: val(json, "query_lowered").parse().unwrap(), + query_snapshot_counts: usizes(val(json, "query_snapshot_counts")), + version_correlations: parse_version_correlations(val(json, "version_correlations")), + lambda_decls: strings(val(json, "lambda_decls")), + choose_decls: strings(val(json, "choose_decls")), + check_valid_invalid: val(json, "check_valid_invalid").parse().unwrap(), + check_valid_valid: val(json, "check_valid_valid").parse().unwrap(), + check_valid_timeout: val(json, "check_valid_timeout").parse().unwrap(), + check_valid_invalid_model_size: usizes(val(json, "check_valid_invalid_model_size")), + eval_expr_results: opt_bools(val(json, "eval_expr_results")), + binder_decls: strings(val(json, "binder_decls")), + breakable_count: val(json, "breakable_count").parse().unwrap(), + break_count: val(json, "break_count").parse().unwrap(), + valid_assert_id_counts: usizes(val(json, "valid_assert_id_counts")), + valid_used_axiom_counts: opt_usizes(val(json, "valid_used_axiom_counts")), + pre_body_binders: strings(val(json, "pre_body_binders")), + post_body_binders: strings(val(json, "post_body_binders")), + events: strings(val(json, "events")), + } +} + +fn parse(err: &TestErr) -> D { + let note = err + .notes + .iter() + .find_map(|n| { + let t = n.rendered.strip_prefix("note: ").unwrap_or(&n.rendered); + t.strip_prefix("OBSERVER:").map(|_| t.to_string()) + }) + .expect("OBSERVER note not found"); + parse_note(¬e) +} + +fn has(v: &[String], s: &str) -> bool { + v.contains(&s.to_string()) +} +fn count(v: &[String], s: &str) -> usize { + v.iter().filter(|x| *x == s).count() +} + +// Find a diagnostic note beginning with `prefix` (e.g. "AIROBS:", "QROBS:", "VIROBS:"). +fn find_note(err: &TestErr, prefix: &str) -> String { + err.notes + .iter() + .find_map(|n| { + let t = n.rendered.strip_prefix("note: ").unwrap_or(&n.rendered); + if t.starts_with(prefix) { Some(t.to_string()) } else { None } + }) + .unwrap_or_else(|| { + panic!( + "{} note not found; notes: {:?}", + prefix, + err.notes.iter().map(|n| n.rendered.clone()).collect::>() + ) + }) +} +// Assert NO note begins with `prefix` (zero-overhead / decoupling checks). +fn no_note(err: &TestErr, prefix: &str) -> bool { + !err.notes.iter().any(|n| { + let t = n.rendered.strip_prefix("note: ").unwrap_or(&n.rendered); + t.starts_with(prefix) + }) +} +// Index of first event exactly equal to `tag`. +fn idx(events: &[String], tag: &str) -> Option { + events.iter().position(|e| e == tag) +} +// Index of first event starting with `prefix` (for tags carrying a payload). +fn idx_pfx(events: &[String], prefix: &str) -> Option { + events.iter().position(|e| e.starts_with(prefix)) +} + +// ── Tests ── + +test_verify_one_file_with_options! { + #[test] + test_observer_loop ["observers=test"] => verus_code! { + fn test_loop(n: u64) + requires n > 0 + ensures false + { + let mut x: u64 = 0; + let mut i: u64 = 0; + while i < n + invariant i <= n, x >= 0, + decreases n - i + { + x = if i % 2 == 0 { x + 1 } else { x + 2 }; + i = i + 1; + } + } + } => Err(err) => { + let d = parse(&err); + assert!(has(&d.krate_function_names, "test_loop"), "got {:?}", d.krate_function_names); + assert!(has(&d.krate_datatype_names, "tuple0"), "got {:?}", d.krate_datatype_names); + assert!(has(&d.assigns, "x@") && has(&d.assigns, "i@"), "got {:?}", d.assigns); + assert_eq!(d.branch_merges, 2); + assert!(has(&d.variable_defs, "x@") && has(&d.variable_defs, "i@"), "got {:?}", d.variable_defs); + assert!(has(&d.assert_id_kinds, "Ensures"), "got {:?}", d.assert_id_kinds); + assert!(has(&d.assert_id_kinds, "LoopInvariant"), "got {:?}", d.assert_id_kinds); + assert!(has(&d.assert_id_kinds, "DecreasesCheck"), "got {:?}", d.assert_id_kinds); + assert_eq!(d.function_lowered, 2); + assert!(d.query_lowered >= 2); + assert!(!d.query_snapshot_counts.is_empty()); + assert!(d.check_valid_invalid >= 1); + assert!(d.check_valid_valid >= 1); + assert!(d.check_valid_invalid_model_size.iter().all(|&s| s > 0)); + assert!(d.eval_expr_results.contains(&Some(true)), + "eval_bool_expr(true) should return Some(true), got {:?}", d.eval_expr_results); + // Version correlations: loop-modified variables have havoc and assign entries + assert!(!d.version_correlations.is_empty(), + "loop should produce version correlations"); + assert!(d.version_correlations.iter().any(|(_, _, k)| k == "Havoc"), + "should have Havoc correlation from loop entry"); + assert!(d.version_correlations.iter().any(|(_, _, k)| k == "Assign"), + "should have Assign correlation from loop body"); + // x should have correlations with distinct lines + let x_corr: Vec<_> = d.version_correlations.iter() + .filter(|(v, _, _)| v.contains("x")).collect(); + assert!(x_corr.len() >= 2, + "x should have >= 2 correlations, got {}", x_corr.len()); + for (v, line, _) in &d.version_correlations { + assert!(*line > 0, "{} has line 0", v); + } + let x_lines: std::collections::HashSet = + x_corr.iter().map(|(_, l, _)| *l).collect(); + assert!(x_lines.len() >= 2, + "x should have >= 2 distinct lines, got {:?}", x_lines); + // Negatives + assert!(!d.havocs.is_empty(), "loop should produce havocs, got {:?}", d.havocs); + assert!(d.for_loop_vars.is_empty()); + assert!(d.quantifier_binders.is_empty()); + assert!(d.lambda_decls.is_empty()); + assert!(d.choose_decls.is_empty()); + } +} + +test_verify_one_file_with_options! { + #[test] + test_observer_mut_ref ["observers=test"] => verus_code! { + struct Pair { a: u64, b: u64 } + spec fn is_positive(x: int) -> bool { x >= 0 } + fn test_mut(p: &mut Pair, x: &mut u64) + requires old(p).a < 100, *old(x) < 100, + forall|i: int| #[trigger] is_positive(i) ==> i >= 0, + ensures (*final(p)).a == old(p).a + 1, *final(x) == *old(x) + 1, + { + p.a = p.a + 1; + *x = *x + 2; + } + } => Err(err) => { + let d = parse(&err); + assert!(has(&d.krate_datatype_names, "Pair"), "got {:?}", d.krate_datatype_names); + assert!(has(&d.krate_function_names, "test_mut") && has(&d.krate_function_names, "is_positive"), + "got {:?}", d.krate_function_names); + assert!(has(&d.assigns, "p!") && has(&d.assigns, "x!"), "got {:?}", d.assigns); + assert!(has(&d.quantifier_binders, "i$"), "got {:?}", d.quantifier_binders); + assert_eq!(count(&d.assert_id_kinds, "Ensures"), 2, "got {:?}", d.assert_id_kinds); + assert_eq!(d.function_lowered, 2); + assert!(d.query_lowered >= 1); + assert!(d.check_valid_invalid >= 1); + assert!(d.check_valid_invalid_model_size.iter().all(|&s| s > 0)); + // Negatives + assert!(d.havocs.is_empty()); + assert_eq!(d.branch_merges, 0); + assert!(d.for_loop_vars.is_empty()); + assert!(d.lambda_decls.is_empty()); + assert!(d.choose_decls.is_empty()); + } +} + +test_verify_one_file_with_options! { + #[test] + test_observer_valid ["observers=test"] => verus_code! { + fn add_one(x: u64) -> (r: u64) + requires x < 100 + ensures r == x + 1 + { x + 1 } + } => Ok(err) => { + let d = parse(&err); + assert!(has(&d.krate_function_names, "add_one"), "got {:?}", d.krate_function_names); + assert!(has(&d.assert_id_kinds, "Ensures"), "got {:?}", d.assert_id_kinds); + assert!(d.function_lowered >= 1); + assert!(d.query_lowered >= 1); + assert!(!d.query_snapshot_counts.is_empty()); + assert!(d.check_valid_valid >= 1); + assert_eq!(d.check_valid_invalid, 0); + // No loops → no version correlations + assert!(d.version_correlations.is_empty(), + "non-mutating function should have no version correlations, got {:?}", + d.version_correlations); + // Negatives + assert!(d.havocs.is_empty()); + assert_eq!(d.branch_merges, 0); + assert!(d.for_loop_vars.is_empty()); + assert!(d.quantifier_binders.is_empty()); + assert!(d.lambda_decls.is_empty()); + assert!(d.choose_decls.is_empty()); + } +} + +test_verify_one_file_with_options! { + #[test] + test_observer_spec ["observers=test"] => verus_code! { + use vstd::prelude::*; + spec fn has_pos(s: Seq) -> bool { + exists|i: int| 0 <= i < s.len() && s[i] > 0 + } + proof fn test_spec(s: Seq) + requires s.len() > 0, + s.map(|_idx: int, x: int| x + 1).len() > 0, + has_pos(s), + ensures false + {} + } => Err(err) => { + let d = parse(&err); + assert!(has(&d.krate_function_names, "has_pos"), "got {:?}", d.krate_function_names); + assert!(has(&d.krate_function_names, "test_spec"), "got {:?}", d.krate_function_names); + // Lambda from s.map(|...|...) + assert!(!d.lambda_decls.is_empty(), "should have lambda decls, got {:?}", d.lambda_decls); + assert!(d.lambda_decls.iter().any(|n| n.contains("lambda")), "got {:?}", d.lambda_decls); + // Quantifier binder + assert!(!d.quantifier_binders.is_empty(), "got {:?}", d.quantifier_binders); + assert!(has(&d.assert_id_kinds, "Ensures"), "got {:?}", d.assert_id_kinds); + assert!(d.function_lowered >= 1); + assert!(d.query_lowered >= 1); + assert!(d.check_valid_invalid >= 1); + assert!(d.check_valid_invalid_model_size.iter().all(|&s| s > 0)); + // Negatives + assert!(d.havocs.is_empty()); + assert!(d.for_loop_vars.is_empty()); + } +} + +test_verify_one_file_with_options! { + #[test] + test_observer_break ["observers=test"] => verus_code! { + use vstd::prelude::*; + fn find(v: &Vec, target: u64) -> (found: bool) + ensures !found // wrong + { + let mut found = false; + let mut i: usize = 0; + while i < v.len() + invariant + i <= v.len(), + !found, + decreases v.len() - i + { + if v[i] == target { + found = true; + break; + } + i = i + 1; + } + found + } + } => Err(err) => { + let d = parse(&err); + // The if + break structure produces branch merges + assert!(d.branch_merges > 0, "if should trigger branch_merge, got {}", d.branch_merges); + // Assigns + assert!(has(&d.assigns, "found@"), "got {:?}", d.assigns); + assert!(has(&d.assigns, "i@"), "got {:?}", d.assigns); + // Assert ID kinds + assert!(has(&d.assert_id_kinds, "Ensures"), "got {:?}", d.assert_id_kinds); + assert!(has(&d.assert_id_kinds, "LoopInvariant"), "got {:?}", d.assert_id_kinds); + assert!(has(&d.assert_id_kinds, "DecreasesCheck"), "got {:?}", d.assert_id_kinds); + assert!(d.function_lowered >= 1); + assert!(d.query_lowered >= 1); + assert!(d.check_valid_invalid >= 1); + // Negatives + assert!(!d.havocs.is_empty(), "loop should produce havocs, got {:?}", d.havocs); + assert!(d.for_loop_vars.is_empty()); + // quantifier_binders may be non-empty due to vstd internals + assert!(d.choose_decls.is_empty()); + } +} + +test_verify_one_file_with_options! { + #[test] + test_observer_for_loop ["observers=test"] => verus_code! { + use vstd::prelude::*; + fn sum_first(v: &Vec, n: usize) -> (s: u64) + requires n <= v.len(), n < 100, + forall|i: int| 0 <= i < v.len() ==> v[i] < 100, + ensures false + { + let mut s: u64 = 0; + for i in iter: 0..n + invariant + s <= 100 * i, + n < 100, + n <= v.len(), + forall|j: int| 0 <= j < v.len() ==> v[j] < 100, + { + s = s + v[i]; + } + s + } + } => Err(err) => { + let d = parse(&err); + assert!(!d.for_loop_vars.is_empty(), "for-loop should be detected"); + // Negatives + assert!(!d.havocs.is_empty(), "loop should produce havocs, got {:?}", d.havocs); + assert!(d.choose_decls.is_empty()); + } +} + +test_verify_one_file_with_options! { + #[test] + test_observer_loop_invariant ["observers=test"] => verus_code! { + fn bad_loop(n: u64) + requires n > 0 + ensures false + { + let mut i: u64 = 0; + while i < n + invariant i <= n, + decreases n - i + { + i = i + 1; + } + } + } => Err(err) => { + let d = parse(&err); + // Assert ID kinds: LoopInvariant and DecreasesCheck are primary + assert!(count(&d.assert_id_kinds, "LoopInvariant") >= 2, + "should have multiple LoopInvariant, got {:?}", d.assert_id_kinds); + assert!(count(&d.assert_id_kinds, "DecreasesCheck") >= 1, + "got {:?}", d.assert_id_kinds); + assert!(has(&d.assigns, "i@"), "got {:?}", d.assigns); + assert!(d.function_lowered >= 1); + assert!(d.query_lowered >= 1); + assert!(d.check_valid_invalid >= 1); + assert!(d.check_valid_invalid_model_size.iter().all(|&s| s > 0)); + // Negatives + assert!(!d.havocs.is_empty(), "loop should produce havocs, got {:?}", d.havocs); + assert!(d.for_loop_vars.is_empty()); + assert!(d.lambda_decls.is_empty()); + assert!(d.choose_decls.is_empty()); + assert!(d.quantifier_binders.is_empty()); + } +} + +test_verify_one_file_with_options! { + #[test] + test_observer_bitvector ["observers=test"] => verus_code! { + proof fn test_bv(x: u32) by(bit_vector) + ensures x & 0xff == x + { } + } => Err(err) => { + let d = parse(&err); + assert!(d.query_lowered >= 1, + "bitvector query should reach observer, got {} queries", d.query_lowered); + } +} + +test_verify_one_file_with_options! { + #[test] + test_observer_reveal_string ["observers=test"] => verus_code! { + use vstd::prelude::*; + use vstd::string::*; + fn test_reveal() + ensures false + { + let _s = "hello"; + proof { reveal_strlit("hello"); } + } + } => Err(err) => { + let d = parse(&err); + assert!(d.reveal_strings.contains(&"hello".to_string()), + "should record 'hello', got {:?}", d.reveal_strings); + assert!(d.check_valid_invalid >= 1); + } +} + +// TODO: test_observer_timeout — requires --rlimit CLI flag which the test harness +// doesn't currently support. Add rlimit support to common/mod.rs, then test with +// rlimit=1 and assert d.check_valid_timeout > 0. + +test_verify_one_file_with_options! { + #[test] + test_body_boundary ["observers=test"] => verus_code! { + use vstd::prelude::*; + + // requires has forall|x|, body has forall|y| + fn test_body_boundary(v: &Vec) + requires forall|x: int| 0 <= x < v.len() ==> v[x] < 100, + { + assert(forall|y: int| 0 <= y < v.len() ==> v[y] < 200) by { + // intentionally wrong bound to force failure + assume(false); + } + assert(false); // force verification failure + } + } => Err(err) => { + let d = parse(&err); + // x is in requires (pre-body), y is in body (post-body) + assert!(d.pre_body_binders.iter().any(|b| b.starts_with("x")), + "requires binder 'x' should be pre-body, got pre={:?}", d.pre_body_binders); + assert!(d.post_body_binders.iter().any(|b| b.starts_with("y")), + "body binder 'y' should be post-body, got post={:?}", d.post_body_binders); + // y should NOT appear in pre-body (it's only in the body assert) + assert!(!d.pre_body_binders.iter().any(|b| b.starts_with("y")), + "body binder 'y' should NOT be in pre-body, got pre={:?}", d.pre_body_binders); + } +} + +test_verify_one_file_with_options! { + + // ── §3.2 Cross-trait lifecycle sequencing (L1–L5) via the ordered trace ── + #[test] + test_lifecycle_sequencing ["observers=test"] => verus_code! { + fn seq_demo(n: u64) -> (r: u64) + requires n < 100, + ensures r == n, + { + let mut i: u64 = 0; + while i < n + invariant i <= n, + decreases n - i, + { i = i + 1; } + i + } + } => Ok(err) => { + let d = parse(&err); + let e = &d.events; + // L1: on_krate fires exactly once, before everything. + assert_eq!(e.first().map(|s| s.as_str()), Some("krate"), + "L1: krate must be first; events={:?}", e); + assert_eq!(count(e, "krate"), 1, "L1: krate exactly once; events={:?}", e); + // L2: on_body_lowering_start precedes on_function_lowered. + let body = idx(e, "body_start").expect("body_start present"); + let flow = idx(e, "function_lowered").expect("function_lowered present"); + assert!(body < flow, "L2: body_start before function_lowered; events={:?}", e); + // L4: some on_query_lowered precedes a check_valid result. + let q = idx(e, "query_lowered").expect("query_lowered present"); + let cv = idx_pfx(e, "check_valid:").expect("check_valid present"); + assert!(q < cv, "L4: query_lowered before check_valid; events={:?}", e); + } +} + +test_verify_one_file_with_options! { + + // ── §3.1 VirObserver-only: functional coverage + decoupling proof ── + #[test] + test_vir_only_observer ["observers=vir-only"] => verus_code! { + fn vo(a: u64) -> (r: u64) + ensures r == a, + { + let x: u64 = a; + x + } + } => Ok(err) => { + // Decoupling: only VIROBS is emitted — no all-three / air / query-result notes. + assert!(no_note(&err, "OBSERVER:"), "vir-only must not emit all-three note"); + assert!(no_note(&err, "AIROBS:") && no_note(&err, "QROBS:"), + "vir-only must not emit AIR/QR notes"); + let note = find_note(&err, "VIROBS:"); + let json = note.strip_prefix("VIROBS:").unwrap(); + let events = strings(val(json, "events")); + let fns = strings(val(json, "function_names")); + let flowered: usize = val(json, "function_lowered").parse().unwrap(); + assert!(has(&fns, "vo"), "function_names has vo; got {:?}", fns); + assert!(flowered >= 1, "function_lowered >= 1"); + assert_eq!(events.first().map(|s| s.as_str()), Some("krate"), + "krate first; events={:?}", events); + assert!(idx(&events, "function_lowered").is_some(), "events={:?}", events); + } +} + +test_verify_one_file_with_options! { + + // ── §3.1 AirObserver-only: functional coverage + decoupling proof ── + #[test] + test_air_only_observer ["observers=air-only"] => verus_code! { + proof fn ao(x: u64) + requires x < 10, + ensures x < 20, + { } + } => Ok(err) => { + assert!(no_note(&err, "OBSERVER:"), "air-only must not emit all-three note"); + assert!(no_note(&err, "VIROBS:") && no_note(&err, "QROBS:"), + "air-only must not emit VIR/QR notes"); + let note = find_note(&err, "AIROBS:"); + let json = note.strip_prefix("AIROBS:").unwrap(); + let events = strings(val(json, "events")); + let ql: usize = val(json, "query_lowered").parse().unwrap(); + let ax: usize = val(json, "axiom_decls").parse().unwrap(); + assert!(ql >= 1, "query_lowered >= 1; events={:?}", events); + assert!(ax >= 1, "axiom_decls >= 1"); + assert!(idx(&events, "query_lowered").is_some(), "events={:?}", events); + } +} + +test_verify_one_file_with_options! { + + // ── §3.1 QueryResultObserver-only, Invalid: eval_expr liveness + decoupling ── + #[test] + test_query_result_only_invalid ["observers=query-result-only"] => verus_code! { + proof fn bad() + ensures false, + { } + } => Err(err) => { + assert!(no_note(&err, "OBSERVER:"), "qr-only must not emit all-three note"); + assert!(no_note(&err, "AIROBS:") && no_note(&err, "VIROBS:"), + "qr-only must not emit AIR/VIR notes"); + let note = find_note(&err, "QROBS:"); + let json = note.strip_prefix("QROBS:").unwrap(); + let invalid: usize = val(json, "invalid").parse().unwrap(); + let events = strings(val(json, "events")); + let eval = opt_bools(val(json, "eval_expr_results")); + assert!(invalid >= 1, "invalid >= 1"); + assert!(idx(&events, "check_valid:Invalid").is_some(), "events={:?}", events); + assert!(!eval.is_empty(), "eval_expr worked during Invalid; got {:?}", eval); + } +} + +test_verify_one_file_with_options! { + + // ── §3.1/§3.4 QueryResultObserver-only, Valid: no unsat core (capabilities live on AirObserver) ── + // ── §3.1 QueryResultObserver-only, Valid: sees the Valid result + decoupling ── + #[test] + test_query_result_only_valid ["observers=query-result-only"] => verus_code! { + proof fn good(x: u64) + requires x < 10, + ensures x < 20, + { } + } => Ok(err) => { + // Decoupling: only QROBS emitted. + assert!(no_note(&err, "OBSERVER:"), "qr-only must not emit all-three note"); + assert!(no_note(&err, "AIROBS:") && no_note(&err, "VIROBS:"), + "qr-only must not emit AIR/VIR notes"); + let note = find_note(&err, "QROBS:"); + let json = note.strip_prefix("QROBS:").unwrap(); + let valid: usize = val(json, "valid").parse().unwrap(); + let events = strings(val(json, "events")); + assert!(valid >= 1, "valid >= 1"); + assert!(events.iter().any(|e| e == "check_valid:Valid"), + "events should contain check_valid:Valid; got {:?}", events); + } +} + +test_verify_one_file_with_options! { + + // ── §3.5 Zero-overhead: no observer flag => no observer notes at all ── + #[test] + test_no_observer_zero_overhead [] => verus_code! { + proof fn noop(x: u64) + requires x < 10, + ensures x < 20, + { } + } => Ok(err) => { + assert!(no_note(&err, "OBSERVER:"), "no all-three note without flag"); + assert!(no_note(&err, "AIROBS:") && no_note(&err, "QROBS:") && no_note(&err, "VIROBS:"), + "no per-trait notes without flag"); + } +} + +// ---- event-trace oracles over the shared VC-shape corpus ------------------------ + +test_verify_one_file_with_options! { + // covers (VO axis): nested-loops seed drives transitive havoc + all three assert-id kinds. + #[test] + test_observer_seed_nested_loops ["observers=test"] => vc_shapes::seed_nested_loops() + => Err(err) => { + let d = parse(&err); + assert!(has(&d.krate_function_names, "test"), "got {:?}", d.krate_function_names); + // Both loop counters are havoced/assigned; outer + inner invariants + decreases fire. + assert!(has(&d.assigns, "i@") && has(&d.assigns, "j@"), "got {:?}", d.assigns); + assert!(has(&d.assert_id_kinds, "LoopInvariant"), "got {:?}", d.assert_id_kinds); + assert!(has(&d.assert_id_kinds, "DecreasesCheck"), "got {:?}", d.assert_id_kinds); + assert!(d.query_lowered >= 2, "nested loops -> multiple isolated queries"); + } +} + +// ---- Uncovered-callback assertions, result-payload semantics, and neutrality ---- + +test_verify_one_file_with_options! { + // covers (VO axis): on_quantifier_binder_decl — a choose binding declares its binder. + #[test] + test_observer_binder_decl ["observers=test"] => verus_code! { + spec fn p(i: int) -> bool; + proof fn f() { + let w = choose|i: int| p(i); + assert(p(w)); + } + } => Err(err) => { + let d = parse(&err); + assert!(!d.binder_decls.is_empty(), + "choose must declare a quantifier binder; got {:?}", d.binder_decls); + assert!(!d.choose_decls.is_empty(), "got {:?}", d.choose_decls); + } +} + +test_verify_one_file_with_options! { + // covers (VO axis): on_check_valid_result Invalid payload — the live evaluator's + // three-way contract: Some(true) / Some(false) / None per failing query. + #[test] + test_observer_eval_three_way ["observers=test"] => verus_code! { + proof fn f(x: u64) { + assert(x < 5); + } + } => Err(err) => { + let d = parse(&err); + assert!(d.check_valid_invalid >= 1); + // Recorded in triples per Invalid: eval(true), eval(false), eval(non-bool). + assert!(d.eval_expr_results.chunks(3).any(|c| + c == [Some(true), Some(false), None]), + "expected a [Some(true), Some(false), None] triple; got {:?}", d.eval_expr_results); + } +} + +test_verify_one_file_with_options! { + // covers (VO axis over corpus): guarded match — merges and per-arm assigns observed. + #[test] + test_observer_seed_match_guard ["observers=test"] => vc_shapes::seed_match_guard() + => Err(err) => { + let d = parse(&err); + assert!(d.branch_merges >= 1, "a match produces branch merges; got {}", d.branch_merges); + assert!(has(&d.assert_id_kinds, "Ensures"), "got {:?}", d.assert_id_kinds); + } +} + +test_verify_one_file_with_options! { + // covers (VO axis over corpus): early return — ensures obligation still identified. + #[test] + test_observer_seed_early_return ["observers=test"] => vc_shapes::seed_early_return() + => Err(err) => { + let d = parse(&err); + assert!(has(&d.assert_id_kinds, "Ensures"), "got {:?}", d.assert_id_kinds); + assert!(d.query_lowered >= 1); + } +} + +/// Behavior-neutrality differential: for every corpus seed, verification outcomes are +/// identical with and without observers registered (same error count, same primary spans). +#[test] +fn test_observer_neutrality_differential() { + let seeds: Vec<(&str, String)> = vec![ + ("match_nested", vc_shapes::seed_match_nested()), + ("match_in_loop_inv", vc_shapes::seed_match_in_loop_inv()), + ("loop_break", vc_shapes::seed_loop_break()), + ("branch_merge", vc_shapes::seed_branch_merge()), + ("param_mutated_before_loop", vc_shapes::seed_param_mutated_before_loop()), + ("nested_loops", vc_shapes::seed_nested_loops()), + ("for_loop", vc_shapes::seed_for_loop()), + ("match_guard", vc_shapes::seed_match_guard()), + ("bare_loop", vc_shapes::seed_bare_loop()), + ("early_return", vc_shapes::seed_early_return()), + ("continue", vc_shapes::seed_continue()), + ("break_labeled", vc_shapes::seed_break_labeled()), + ("loop_break_noniso", vc_shapes::seed_loop_break_noniso()), + ("nested_loops_noniso", vc_shapes::seed_nested_loops_noniso()), + ("break_labeled_noniso", vc_shapes::seed_break_labeled_noniso()), + ("expand_ensures", vc_shapes::seed_expand_ensures()), + ("truncate_cast", vc_shapes::seed_truncate_cast()), + ]; + for (name, code) in seeds { + let plain = verify_one_file(&format!("neutral_{}_plain", name), code.clone(), &[]); + let observed = verify_one_file(&format!("neutral_{}_obs", name), code, &["observers=test"]); + let (p, o) = match (&plain, &observed) { + (Ok(p), Ok(o)) | (Err(p), Err(o)) | (Ok(p), Err(o)) | (Err(p), Ok(o)) => (p, o), + }; + assert_eq!( + plain.is_err(), + observed.is_err(), + "seed {}: overall outcome differs with observers", + name + ); + assert_eq!( + p.errors.len(), + o.errors.len(), + "seed {}: error count differs with observers", + name + ); + // The corpus programs are small; none should hit the solver resource limit, so the + // result channel must report no Timeout for any of them. + let d = parse(o); + assert_eq!(d.check_valid_timeout, 0, "seed {}: unexpected solver timeout", name); + for (a, b) in p.errors.iter().zip(o.errors.iter()) { + assert_eq!( + a.rendered.lines().next(), + b.rendered.lines().next(), + "seed {}: error text differs with observers", + name + ); + } + } +} + +test_verify_one_file_with_options! { + // covers: S-continue — the loop's invariants (and decreases) are asserted at the + // continue site; the too-strong invariant fails there. + #[test] + test_observer_seed_continue ["observers=test"] => vc_shapes::seed_continue() + => Err(err) => { + let d = parse(&err); + assert!(has(&d.assert_id_kinds, "LoopInvariant"), "got {:?}", d.assert_id_kinds); + // Isolated lowering (the default): loops never appear as Breakable regions. + assert_eq!(d.breakable_count, 0, "got {}", d.breakable_count); + } +} + +test_verify_one_file_with_options! { + // covers: S-break-labeled — `break 'outer` asserts the TARGET loop's invariants at + // the break site; the outer invariant fails there. + #[test] + test_observer_seed_break_labeled ["observers=test"] => vc_shapes::seed_break_labeled() + => Err(err) => { + let d = parse(&err); + assert!(has(&d.assert_id_kinds, "LoopInvariant"), "got {:?}", d.assert_id_kinds); + assert_eq!(d.breakable_count, 0, "got {}", d.breakable_count); + } +} + +test_verify_one_file_with_options! { + // covers: S-loop-noniso — without loop isolation the loop lowers into the enclosing + // query as a labeled Breakable region with Break jumps. + #[test] + test_observer_seed_loop_break_noniso ["observers=test"] => vc_shapes::seed_loop_break_noniso() + => Err(err) => { + let d = parse(&err); + assert!(d.breakable_count >= 1, "non-isolated loop must lower as Breakable; got {}", + d.breakable_count); + assert!(d.break_count >= 1, "got {}", d.break_count); + } +} + +test_verify_one_file_with_options! { + // covers: S-break-labeled-noniso — a labeled break without isolation still lowers the + // loops as Breakable regions with Break jumps (two nested loops -> two of each). + #[test] + test_observer_seed_break_labeled_noniso ["observers=test"] => vc_shapes::seed_break_labeled_noniso() + => Err(err) => { + let d = parse(&err); + assert!(d.breakable_count >= 2, "nested non-isolated loops -> Breakable regions; got {}", + d.breakable_count); + assert!(d.break_count >= 1, "labeled break emits a Break; got {}", d.break_count); + } +} + +test_verify_one_file_with_options! { + // covers: S-nested-noniso — nested loops without isolation: nested Breakable regions + // in a single query. + #[test] + test_observer_seed_nested_loops_noniso ["observers=test"] => vc_shapes::seed_nested_loops_noniso() + => Err(err) => { + let d = parse(&err); + assert!(d.breakable_count >= 2, "two nested Breakable regions; got {}", + d.breakable_count); + assert!(d.break_count >= 2, "got {}", d.break_count); + } +} + +test_verify_one_file_with_options! { + // A discharged (unsat) query is observed with the same shape callbacks as a failing one, + // and its result callback names the obligations it checked: two postconditions and one + // loop invariant here, none of which fail. + #[test] + test_observer_valid_reports_obligations ["observers=test"] => verus_code! { + fn test(n: u64) -> (r: u64) + requires n < 100 + ensures r >= n, r < 200 + { + let mut i: u64 = 0; + while i < n + invariant i <= n + decreases n - i + { + i = i + 1; + } + i + 1 + } + } => Ok(err) => { + let d = parse(&err); + assert!(d.check_valid_valid >= 1, "got {}", d.check_valid_valid); + assert_eq!(d.check_valid_invalid, 0); + // Shape callbacks fire regardless of outcome. + assert!(d.query_lowered >= 1); + assert!(has(&d.assert_id_kinds, "Ensures"), "got {:?}", d.assert_id_kinds); + assert!(has(&d.assert_id_kinds, "LoopInvariant"), "got {:?}", d.assert_id_kinds); + // At least one discharged query reported labeled obligations. + assert!(d.valid_assert_id_counts.iter().any(|&c| c >= 1), + "a Valid result should name its assertion ids; got {:?}", d.valid_assert_id_counts); + // Usage reporting is opt-in: not enabled here, so no core is attached. + assert!(d.valid_used_axiom_counts.iter().all(|c| c.is_none()), + "no usage info without the flag; got {:?}", d.valid_used_axiom_counts); + } +} + +test_verify_one_file_with_options! { + // With usage reporting enabled, a discharged query carries the unsat core: the named + // axioms the solver used. A call to a lemma with a broadcast-style axiom makes the core + // non-empty. + #[test] + test_observer_valid_usage_info ["observers=test", "-V axiom-usage-info"] => verus_code! { + spec fn f(x: int) -> int; + proof fn lemma_f(x: int) + ensures f(x) > 0 + { + admit(); + } + proof fn test(x: int) { + lemma_f(x); + assert(f(x) > 0); + } + } => Ok(err) => { + let d = parse(&err); + assert!(d.check_valid_valid >= 1, "got {}", d.check_valid_valid); + assert!(d.valid_used_axiom_counts.iter().any(|c| c.is_some()), + "usage info should be attached when enabled; got {:?}", d.valid_used_axiom_counts); + } +} diff --git a/source/rust_verify_test/tests/vc_shapes/mod.rs b/source/rust_verify_test/tests/vc_shapes/mod.rs new file mode 100644 index 0000000000..6a92f602b3 --- /dev/null +++ b/source/rust_verify_test/tests/vc_shapes/mod.rs @@ -0,0 +1,381 @@ +//! VC-shape seed corpus, shared by end-to-end suites. +//! +//! Each function returns a small Verus program with a forced verification failure. The +//! `covers:` tags name the shape(s) a seed exercises, using these prefixes: +//! +//! - `S-` statement/control structure (the shapes verification-condition generation composes: +//! branches, matches, loops, breaks, early returns, ...) +//! - `E-` expression grammar (expression forms reachable from source) +//! - `I-` encoding idioms (naming/encoding conventions of the lowering: temporaries, +//! variable versions, old/final values, contract functions, ...) +//! - `X-` interactions (idiom x structure combinations that share per-query state, +//! e.g. temporaries assigned per match arm) +//! +//! Seeds are APPEND-ONLY: once any suite pins an expected-output oracle to a seed, the seed's +//! program text is immutable — behavior changes get a new seed function. This keeps oracles in +//! all consuming suites stable against edits made in any one of them. + +// Not every consumer uses every seed. +#![allow(dead_code)] + +use rust_verify_test_macros::verus_code; + +/// covers: S-match-nested +pub fn seed_match_nested() -> String { + verus_code! { + #[allow(unused)] + enum Outer { A, B } + #[allow(unused)] + enum Inner { X, Y } + + proof fn test(o: Outer, i: Inner, v: int) + requires v > 0 + { + match o { + Outer::A => { + match i { + Inner::X => { + assert(v > 1000); + } + _ => {} + } + } + _ => {} + } + } + } +} + +/// covers: S-match-in-loop, X-switch-in-loop (failing loop invariant, so the match arms are +/// inside the failing query) +pub fn seed_match_in_loop_inv() -> String { + verus_code! { + #[allow(unused)] + enum Op { Add, Nop } + fn test(op: Op, n: u64) + requires n > 0 + { + let mut val: u64 = 0; + let mut i: u64 = 0; + while i < n + invariant i <= n, val == 0 + decreases n - i + { + match op { + Op::Add => { val = val + 1; } + Op::Nop => {} + } + i = i + 1; + } + } + } +} + +/// covers: S-loop-break (bare break inside while) +pub fn seed_loop_break() -> String { + verus_code! { + fn test(n: u64) + requires n > 10 + ensures false + { + let mut i: u64 = 0; + while i < n + invariant i <= n + decreases n - i + { + if i == 5 { + break; + } + i = i + 1; + } + } + } +} + +/// covers: I-versions-merge, S-if-noelse +pub fn seed_branch_merge() -> String { + verus_code! { + proof fn test(cond: bool, v: int) + requires v < 100 + { + let mut x: int = v; + if cond { + x = x + 10; + } + assert(x > v); + } + } +} + +/// covers: X-old-loop, I-versions-mutation (param mutated before the loop) +pub fn seed_param_mutated_before_loop() -> String { + verus_code! { + fn test(n: u64) + requires n > 10 + ensures false + { + let mut x: u64 = n; + x = x + 1; + let mut i: u64 = 0; + while i < x + invariant i <= x + decreases x - i + { + i = i + 1; + } + } + } +} + +/// covers: S-nested-loops, X-versions-nested-loop (inner invariant fails) +pub fn seed_nested_loops() -> String { + verus_code! { + fn test(n: u64) + requires n > 0 + { + let mut i: u64 = 0; + while i < n + invariant i <= n + decreases n - i + { + let mut j: u64 = 0; + while j < i + invariant j <= i, j < 5 + decreases i - j + { + j = j + 1; + } + i = i + 1; + } + } + } +} + +/// covers: S-for (ghost-iterator machinery) +pub fn seed_for_loop() -> String { + verus_code! { + use vstd::prelude::*; + fn test(v: &Vec) -> (sum: u64) + ensures sum == 0 + { + let mut sum: u64 = 0; + for x in v.iter() + invariant sum < 1000000u64, + { + sum = sum + 1u64; + } + sum + } + } +} + +/// covers: S-match-guard (arm with if-guard) +pub fn seed_match_guard() -> String { + verus_code! { + #[allow(unused)] + enum Kind { A, B } + proof fn test(k: Kind, v: int) -> (r: int) + ensures r > 0 + { + match k { + Kind::A if v > 10 => 1, + Kind::A => 0, + Kind::B => 2, + } + } + } +} + +/// covers: S-loop (bare loop with break) +/// (break-with-value is unreachable: Verus rejects "complex break expressions") +pub fn seed_bare_loop() -> String { + verus_code! { + fn test() -> (r: u64) + ensures r > 100 + { + let mut i: u64 = 0; + loop + invariant i <= 10, + decreases 10 - i, + { + if i >= 7 { + break; + } + i = i + 1; + } + i + } + } +} + +/// covers: S-return (early return before an unprovable postcondition) +pub fn seed_early_return() -> String { + verus_code! { + proof fn test(c: bool, v: int) -> (r: int) + ensures r > 10 + { + if c { + return v; + } + 20 + } + } +} + +/// covers: S-continue (loop invariants + decreases asserted at the continue site) +pub fn seed_continue() -> String { + verus_code! { + fn test(n: u64) + requires n > 0 + { + let mut i: u64 = 0; + let mut s: u64 = 0; + while i < n + invariant s >= i, i <= n + decreases n - i + { + i = i + 1; + if i % 2 == 0 { + continue; + } + s = s + 2; + } + } + } +} + +/// covers: S-break-labeled (the labeled target loop's invariants asserted at the break site) +pub fn seed_break_labeled() -> String { + verus_code! { + fn test(n: u64) + requires n > 10 + { + let mut i: u64 = 0; + let mut j: u64 = 0; + 'outer: while i < n + invariant i <= n, j <= 5 + decreases n - i + { + j = 0; + while j < 10 + invariant j <= 10 + decreases 10 - j + { + if j == 8 { + break 'outer; + } + j = j + 1; + } + i = i + 1; + } + } + } +} + +/// covers: S-loop-noniso (same program as seed_loop_break, lowered without loop isolation: +/// the query carries the loop as a labeled `Breakable`/`Break` region with inline +/// assume-false exits instead of a separate loop query) +pub fn seed_loop_break_noniso() -> String { + verus_code! { + #[verifier::loop_isolation(false)] + fn test(n: u64) + requires n > 10 + ensures false + { + let mut i: u64 = 0; + while i < n + invariant i <= n + decreases n - i + { + if i == 5 { + break; + } + i = i + 1; + } + } + } +} + +/// covers: S-nested-noniso (nested loops without isolation: nested Breakable regions in +/// one query) +pub fn seed_nested_loops_noniso() -> String { + verus_code! { + #[verifier::loop_isolation(false)] + fn test(n: u64) + requires n > 0 + { + let mut i: u64 = 0; + while i < n + invariant i <= n + decreases n - i + { + let mut j: u64 = 0; + while j < i + invariant j <= i, j < 5 + decreases i - j + { + j = j + 1; + } + i = i + 1; + } + } + } +} + +/// covers: I-expand (an ensures whose failing spec function expands into conjuncts under +/// --expand-errors, introducing expand% temporaries in the second lowering) +pub fn seed_expand_ensures() -> String { + verus_code! { + spec fn in_range(x: u64) -> bool { + x > 0 && x < 100 + } + fn test() -> (r: u64) + ensures in_range(r) + { + 0 + } + } +} + +/// covers: I-truncate (a truncating cast: the VC clips the value to the target width) +pub fn seed_truncate_cast() -> String { + verus_code! { + #[verifier::truncate] + fn test(x: u64) -> (r: u8) + ensures r as u64 == x + { + x as u8 + } + } +} + +/// covers: S-break-labeled-noniso (labeled `break 'outer` without loop isolation: the +/// break targets the outer Breakable region by label, exercising the labeled-break +/// encoding in a single query) +pub fn seed_break_labeled_noniso() -> String { + verus_code! { + #[verifier::loop_isolation(false)] + fn test(n: u64) + requires n > 10 + ensures false + { + let mut i: u64 = 0; + 'outer: while i < n + invariant i <= n + decreases n - i + { + let mut j: u64 = 0; + while j < 10 + invariant j <= 10 + decreases 10 - j + { + if j == 8 { + break 'outer; + } + j = j + 1; + } + i = i + 1; + } + } + } +} diff --git a/source/vir/src/context.rs b/source/vir/src/context.rs index 6d28e80b2c..e8c3db1cad 100644 --- a/source/vir/src/context.rs +++ b/source/vir/src/context.rs @@ -154,10 +154,43 @@ pub struct Ctx { pub(crate) byte_string_hashes: RefCell>>>, // proof debug purposes pub debug: bool, + /// Observer for the verification pipeline. Three layers of indirection: + /// - `Arc`: shared between VIR `Ctx` (for lowering callbacks) and AIR + /// `Context` (for query/result callbacks) which have independent lifetimes. + /// - `Mutex`: callbacks require `&mut` through shared `Arc` references, and + /// an AIR context retained by a resident session must stay `Send`. + /// - `dyn VirObserver`: type-erased observer, shared with the AIR context's + /// own trait handles via the verifier's observer registry (all views point + /// at one object). + pub observer: Option, + /// AIR-level handles to the same shared observer object, carried here so the + /// verifier can attach them to each `air::Context` it builds (see verifier.rs). + pub air_observer: Option, + pub query_result_observer: Option, pub arch_word_bits: ArchWordBits, } impl Ctx { + /// Call a callback on the observer if one is registered. + pub(crate) fn notify(&self, f: F) { + if let Some(obs) = &self.observer { + f(&mut *obs.lock().unwrap()); + } + } + + /// Ask the observer for an assert ID, or use the default (clone parent). + pub(crate) fn make_assert_id( + &self, + kind: &crate::vir_observer::AssertIdKind, + index: usize, + parent: &Option, + ) -> Option { + self.observer.as_ref().map_or_else( + || parent.clone(), + |obs| obs.lock().unwrap().make_assert_id(kind, index, parent), + ) + } + pub(crate) fn checking_spec_preconditions(&self) -> bool { match self.fun { Some(FunctionCtx { checking_spec_preconditions: true, .. }) => true, @@ -847,6 +880,7 @@ impl Ctx { fndef_types: Vec, resolved_typs: Vec, debug: bool, + observers: crate::vir_observer::Observers, ) -> Result { let name_ctxt = NameCtxt::new(); let mut datatype_is_transparent: HashMap = HashMap::new(); @@ -895,6 +929,19 @@ impl Ctx { opaque_type_map.insert(opaque_type.x.name.clone(), opaque_type.clone()); } + // Register the observer and deliver the krate. The observer receives the + // NameCtxt so it can compute AIR names consistently with lowering — both + // share the same NameCtxt instance, so crate-name interning decisions + // made here are reused during lowering. + let crate::vir_observer::Observers { + vir: observer, + air: air_observer, + query_result: query_result_observer, + } = observers; + if let Some(obs) = &observer { + obs.lock().unwrap().on_krate(&krate, &name_ctxt, &module.x.path.krate); + } + Ok(Ctx { module, datatype_is_transparent, @@ -923,6 +970,9 @@ impl Ctx { string_hashes, byte_string_hashes, debug, + observer, + air_observer, + query_result_observer, arch_word_bits: krate.arch.word_bits, opaque_type_map, }) diff --git a/source/vir/src/def.rs b/source/vir/src/def.rs index 2fd44b0843..f79346affc 100644 --- a/source/vir/src/def.rs +++ b/source/vir/src/def.rs @@ -47,14 +47,14 @@ const SUFFIX_PATH: &str = "."; const PREFIX_ESCAPE: &str = "$~"; const PREFIX_FUEL_ID: &str = "fuel%"; const PREFIX_FUEL_NAT: &str = "fuel_nat%"; -const PREFIX_REQUIRES: &str = "req%"; +pub const PREFIX_REQUIRES: &str = "req%"; const PREFIX_ENSURES: &str = "ens%"; const PREFIX_ENSURES_ASYNC_RET: &str = "VERUS_ASYNC_FUNC_RETURN_VALUE_"; const PREFIX_OPEN_INV: &str = "openinv%"; const PREFIX_NO_UNWIND_WHEN: &str = "no_unwind_when%"; const PREFIX_RECURSIVE: &str = "rec%"; const PREFIX_SIMPLIFY_TEMP_VAR: &str = "tmp%%"; -const PREFIX_TEMP_VAR: &str = "tmp%"; +pub const PREFIX_TEMP_VAR: &str = "tmp%"; pub const PREFIX_EXPAND_ERRORS_TEMP_VAR: &str = "expand%"; const PREFIX_PRE_VAR: &str = "pre%"; /// Datatype box/unbox: `(Poly%D. x)` and `(%Poly%D. p)`. Public because a diff --git a/source/vir/src/lib.rs b/source/vir/src/lib.rs index 21db18dc9c..f0337c1fb5 100644 --- a/source/vir/src/lib.rs +++ b/source/vir/src/lib.rs @@ -81,5 +81,6 @@ mod triggers_auto; mod unicode; pub mod user_defined_type_invariants; pub mod util; +pub mod vir_observer; mod visitor; pub mod well_formed; diff --git a/source/vir/src/sst_to_air.rs b/source/vir/src/sst_to_air.rs index d8f560f3f0..dea3653505 100644 --- a/source/vir/src/sst_to_air.rs +++ b/source/vir/src/sst_to_air.rs @@ -1582,6 +1582,9 @@ pub(crate) fn exp_to_expr(ctx: &Ctx, exp: &Exp, expr_ctxt: &ExprCtxt) -> Result< } BndX::Quant(quant, binders, trigs, _) => { let expr = exp_to_expr(ctx, e, expr_ctxt)?; + for b in binders.iter() { + ctx.notify(|obs| obs.on_quantifier_binder(b, exp)); + } let mut invs: Vec = Vec::new(); for binder in binders.iter() { let typ_inv = typ_invariant( @@ -2130,6 +2133,7 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Result, Vi let var = suffix_local_unique_id(&get_loc_var(dest)); ens_args.push(exp_to_expr(ctx, &dest, expr_ctxt)?); if !*is_init { + ctx.notify(|obs| obs.on_havoc(stm, &get_loc_var(dest))); let havoc = StmtX::Havoc(var); stmts.push(Arc::new(havoc)); } @@ -2270,8 +2274,8 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Result, Vi stmts.append(&mut new_stmts); } } else { - for (span, ens, proof_note) in - state.post_condition_info.ens_exprs.clone().iter() + for (ens_idx, (span, ens, proof_note)) in + state.post_condition_info.ens_exprs.clone().iter().enumerate() { // The base_error should point to the return-statement or // return-expression. Augment with an additional label pointing @@ -2313,7 +2317,12 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Result, Vi } }; - let ens_stmt = StmtX::Assert(assert_id.clone(), error, None, ens.clone()); + let ens_id = ctx.make_assert_id( + &crate::vir_observer::AssertIdKind::Ensures, + ens_idx, + &assert_id, + ); + let ens_stmt = StmtX::Assert(ens_id, error, None, ens.clone()); stmts.push(Arc::new(ens_stmt)); } } @@ -2402,6 +2411,7 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Result, Vi } StmX::Assign { lhs: Dest { dest, is_init: true }, rhs } => { let x = loc_is_var(dest).expect("is_init assign dest must be a variable"); + ctx.notify(|obs| obs.on_variable_def(stm, x)); stm_to_stmts(ctx, state, &assume_var(&stm.span, x, rhs))? } StmX::Assign { lhs: Dest { dest, is_init: false }, rhs } => { @@ -2473,6 +2483,7 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Result, Vi false }; + ctx.notify(|obs| obs.on_assign(stm, &base_var)); let a = Arc::new(StmtX::Assign(suffix_local_unique_id(&base_var), value)); stmts.push(a); if fields.len() > 0 { @@ -2530,7 +2541,7 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Result, Vi } else { error_with_label(&stm.span, "loop invariant not satisfied", "at this continue") }; - for (span, inv, msg, both) in invs.iter() { + for (inv_idx, (span, inv, msg, both)) in invs.iter().enumerate() { let mut error = base_error.secondary_label(span, "failed this invariant"); if let Some(msg) = msg { error = error.secondary_label(span, &**msg); @@ -2541,7 +2552,16 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Result, Vi and use 'ensures' for what is true at the break)"; error = error.secondary_label(span, msg); } - stmts.push(Arc::new(StmtX::Assert(None, error, None, inv.clone()))); + stmts.push(Arc::new(StmtX::Assert( + ctx.make_assert_id( + &crate::vir_observer::AssertIdKind::LoopInvariant, + inv_idx, + &None, + ), + error, + None, + inv.clone(), + ))); } let decrease = &loop_info.decrease; if !is_break && decrease.len() > 0 { @@ -2564,7 +2584,16 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Result, Vi )?; let expr = exp_to_expr(ctx, &dec_exp, expr_ctxt)?; let error = error(&stm.span, crate::def::DEC_FAIL_LOOP_CONTINUE); - let dec_stmt = StmtX::Assert(None, error, None, expr); + let dec_stmt = StmtX::Assert( + ctx.make_assert_id( + &crate::vir_observer::AssertIdKind::DecreasesCheck, + 0, + &None, + ), + error, + None, + expr, + ); stmts.push(Arc::new(dec_stmt)); } } @@ -2610,6 +2639,7 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Result, Vi let lblock = Arc::new(StmtX::Block(Arc::new(lhss))); let rblock = Arc::new(StmtX::Block(Arc::new(rhss))); let mut stmts = vec![Arc::new(StmtX::Switch(Arc::new(vec![lblock, rblock])))]; + ctx.notify(|obs| obs.on_branch_merge(stm)); if ctx.debug { // Add a snapshot for the state after we join the lhs and rhs back together let sid = state.update_current_sid(SUFFIX_SNAP_JOIN); @@ -2674,6 +2704,7 @@ fn stm_to_stmts(ctx: &Ctx, state: &mut State, stm: &Stm) -> Result, Vi stmts } StmX::RevealString(lit) => { + ctx.notify(|obs| obs.on_reveal_string(lit)); let exprs = Arc::new({ vec![string_len_to_air(ctx, lit.clone()), string_indices_to_air(ctx, lit.clone())] }); @@ -2745,6 +2776,9 @@ fn loop_to_stmts( }; let loop_isolation = *loop_isolation; + if *is_for_loop { + ctx.notify(|obs| obs.on_for_loop(stm)); + } let (cond_stm, pos_assume, neg_assume) = if let Some((cond_stm, cond_exp)) = cond { let pos_cond = exp_to_expr(ctx, &cond_exp, expr_ctxt)?; let neg_cond = Arc::new(ExprX::Unary(air::ast::UnaryOp::Not, pos_cond.clone())); @@ -2854,6 +2888,9 @@ fn loop_to_stmts( let mut air_body: Vec = state.static_prelude.clone(); if !loop_isolation { air_body.push(Arc::new(StmtX::Snapshot(snapshot_ident(SNAPSHOT_LOOP)))); + for (var, _) in modified_vars.vars.iter() { + ctx.notify(|obs| obs.on_havoc(stm, var)); + } modified_vars.emit_havocs(ctx, SNAPSHOT_LOOP, &mut air_body); } @@ -2884,6 +2921,9 @@ fn loop_to_stmts( // we need to havoc it, in order to create a difference between // the "current" value and the "pre-state" value. let pre_modified_params_incl = pre_modified_params_incl.as_ref().unwrap(); + for (var, _) in pre_modified_params_incl.vars.iter() { + ctx.notify(|obs| obs.on_havoc(stm, var)); + } pre_modified_params_incl.emit_havocs(ctx, SNAPSHOT_PRE, &mut air_body); } else { // Similar, but this time accounting for isolation boundary @@ -2891,6 +2931,9 @@ fn loop_to_stmts( // Havoc vars between beginning of the function and the start of // the isolation_boundary let pre_modified_params_excl = pre_modified_params_excl.as_ref().unwrap(); + for (var, _) in pre_modified_params_excl.vars.iter() { + ctx.notify(|obs| obs.on_havoc(stm, var)); + } pre_modified_params_excl.emit_havocs(ctx, SNAPSHOT_PRE, &mut air_body); // Execute the code between the isolation boundary and the actual loop start @@ -2898,6 +2941,9 @@ fn loop_to_stmts( // Havoc all vars that might be modified during the loop air_body.push(Arc::new(StmtX::Snapshot(snapshot_ident(SNAPSHOT_BOUNDARY)))); + for (var, _) in modified_vars.vars.iter() { + ctx.notify(|obs| obs.on_havoc(stm, var)); + } modified_vars.emit_havocs(ctx, SNAPSHOT_BOUNDARY, &mut air_body); } } @@ -2950,12 +2996,21 @@ fn loop_to_stmts( } if !ctx.checking_spec_preconditions() { - for (span, inv, msg, _) in invs_entry.iter() { + for (inv_idx, (span, inv, msg, _)) in invs_entry.iter().enumerate() { let mut error = error(span, crate::def::INV_FAIL_LOOP_END); if let Some(msg) = msg { error = error.secondary_label(span, &**msg); } - let inv_stmt = StmtX::Assert(None, error, None, inv.clone()); + let inv_stmt = StmtX::Assert( + ctx.make_assert_id( + &crate::vir_observer::AssertIdKind::LoopInvariant, + inv_idx, + &None, + ), + error, + None, + inv.clone(), + ); air_body.push(Arc::new(inv_stmt)); } if decrease.len() > 0 { @@ -2968,7 +3023,12 @@ fn loop_to_stmts( )?; let expr = exp_to_expr(ctx, &dec_exp, expr_ctxt)?; let error = error(&stm.span, crate::def::DEC_FAIL_LOOP_END); - let dec_stmt = StmtX::Assert(None, error, None, expr); + let dec_stmt = StmtX::Assert( + ctx.make_assert_id(&crate::vir_observer::AssertIdKind::DecreasesCheck, 0, &None), + error, + None, + expr, + ); air_body.push(Arc::new(dec_stmt)); } } @@ -3005,12 +3065,21 @@ fn loop_to_stmts( // At original site of while loop, assert invariant, havoc, assume invariant + neg_cond let mut stmts: Vec = Vec::new(); if !ctx.checking_spec_preconditions() { - for (span, inv, msg, _) in invs_entry.iter() { + for (inv_idx, (span, inv, msg, _)) in invs_entry.iter().enumerate() { let mut error = error(span, crate::def::INV_FAIL_LOOP_FRONT); if let Some(msg) = msg { error = error.secondary_label(span, &**msg); } - let inv_stmt = StmtX::Assert(None, error, None, inv.clone()); + let inv_stmt = StmtX::Assert( + ctx.make_assert_id( + &crate::vir_observer::AssertIdKind::LoopInvariant, + inv_idx, + &None, + ), + error, + None, + inv.clone(), + ); stmts.push(Arc::new(inv_stmt)); } } @@ -3021,6 +3090,9 @@ fn loop_to_stmts( } if loop_isolation { stmts.push(Arc::new(StmtX::Snapshot(snapshot_ident(SNAPSHOT_LOOP)))); + for (var, _) in modified_vars.vars.iter() { + ctx.notify(|obs| obs.on_havoc(stm, var)); + } modified_vars.emit_havocs(ctx, SNAPSHOT_LOOP, &mut stmts); for (_, inv, _, _) in invs_exit.iter() { let inv_stmt = StmtX::Assume(inv.clone()); @@ -3263,6 +3335,10 @@ pub(crate) fn body_stm_to_air( unwind, } = func_check_sst; + // Notify observer that body lowering is starting. + // Binders recorded before this point (requires/ensures) should be discarded. + ctx.notify(|obs| obs.on_body_lowering_start()); + if is_bit_vector_mode { if is_integer_ring { panic!("Error: integer_ring and bit_vector should not be used together"); @@ -3459,6 +3535,17 @@ pub(crate) fn body_stm_to_air( is_integer_ring || is_nonlinear, )); } + // Notify observer of binder-originated local declarations (including Skolemized + // copies): quantifier binders and choose binders alike. + for decl in local_decls.iter() { + if matches!( + decl.kind, + crate::sst::LocalDeclKind::QuantBinder | crate::sst::LocalDeclKind::ChooseBinder + ) { + ctx.notify(|obs| obs.on_quantifier_binder_decl(&decl.ident)); + } + } + ctx.notify(|obs| obs.on_function_lowered()); Ok((state.commands, state.snap_map)) } diff --git a/source/vir/src/vir_observer.rs b/source/vir/src/vir_observer.rs new file mode 100644 index 0000000000..8db3c1dfd4 --- /dev/null +++ b/source/vir/src/vir_observer.rs @@ -0,0 +1,154 @@ +//! VIR-level verification observer. +//! +//! Defines `VirObserver` — callbacks fired during VIR→AIR lowering (havoc, +//! assign, branch merges, loops, quantifier binders, reveals, and +//! function/krate lifecycle). +//! +//! This trait is independent: it does **not** require `AirObserver` or +//! `QueryResultObserver`. A consumer implements only the traits it needs; the +//! verifier wires each implemented trait to its own callbacks (see the observer +//! handle registry in `rust_verify/src/verifier.rs`). + +use crate::ast::{Krate, Typ, VarIdent}; +use crate::sst::{Exp, Stm}; +use air::ast::AssertId; +use std::any::Any; + +// Re-export for convenience (used by `VersionCorrelator::resolve`). +pub use air::air_observer::VersionOrigin; + +/// What kind of assertion is being assigned an ID. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum AssertIdKind { + Ensures, + LoopInvariant, + DecreasesCheck, +} + +/// Observer for the VIR-level verification pipeline. +/// +/// Callbacks fire during VIR→AIR lowering. All methods have default no-op +/// implementations except `as_any`/`as_any_mut` (trivially: `self`). +pub trait VirObserver: Any + Send { + /// Fired once per module in `Ctx::new`. The `NameCtxt` is the same instance + /// used by lowering, so AIR names computed by the observer are consistent + /// with the names lowering will produce. `current_crate` identifies the + /// crate under verification, so observers can strip its prefix from + /// friendly names (e.g. render `double(x)` not `test_crate::double(x)`). + fn on_krate( + &mut self, + _krate: &Krate, + _name_ctxt: &crate::def::NameCtxt, + _current_crate: &crate::ast::CrateId, + ) { + } + fn on_havoc(&mut self, _stm: &Stm, _var: &VarIdent) {} + fn on_assign(&mut self, _stm: &Stm, _var: &VarIdent) {} + fn on_variable_def(&mut self, _stm: &Stm, _var: &VarIdent) {} + fn on_branch_merge(&mut self, _stm: &Stm) {} + fn on_for_loop(&mut self, _stm: &Stm) {} + fn on_quantifier_binder(&mut self, _binder: &crate::ast::VarBinder, _exp: &Exp) {} + fn on_reveal_string(&mut self, _lit: &std::sync::Arc) {} + fn make_assert_id( + &mut self, + _kind: &AssertIdKind, + _index: usize, + parent: &Option, + ) -> Option { + parent.clone() + } + /// A quantifier binder local declaration was processed. + /// Fires for each QuantBinder in local_decls after body lowering, + /// including Skolemized copies (e.g., i$0, i$1). The observer can + /// correlate with the original binder's line via prefix matching + /// on suffix_local_unique_id(var). + /// Fires for choose binders as well as quantifier binders. + fn on_quantifier_binder_decl(&mut self, _var: &VarIdent) {} + /// Called at the start of function body lowering (body_stm_to_air). + /// Binders recorded after this point are body-level binders. + /// Observers should clear any pre-body binder accumulation here. + fn on_body_lowering_start(&mut self) {} + fn on_function_lowered(&mut self) {} + + fn as_any(&self) -> &dyn Any; + fn as_any_mut(&mut self) -> &mut dyn Any; +} + +/// A shared handle to a `VirObserver`; `Arc>` like the AIR handles. +pub type VirObserverHandle = std::sync::Arc>; + +/// Registry of per-trait observer handles: independent trait-object views of +/// (up to) one shared observer object. Each field is `Some` only if the observer +/// implements that trait, so a consumer couples nothing it does not use. All +/// populated fields point at the same underlying `Mutex` (via `Arc` unsizing +/// coercion at the factory), so callbacks mutate one shared object. +#[derive(Clone, Default)] +pub struct Observers { + pub vir: Option, + pub air: Option, + pub query_result: Option, +} + +use std::collections::{HashMap, VecDeque}; +use std::sync::Arc; + +/// Extract line number from a VIR span's string representation ("file:line:col:..."). +pub fn line_from_span(span: &crate::messages::Span) -> Option { + span.as_string.split(':').nth(1)?.trim().parse().ok() +} + +/// Strip the version suffix from a versioned WP constant name. +/// `"x@2"` → `"x@"`, `"foo!@3"` → `"foo!@"` +fn strip_version_suffix(name: &str) -> &str { + if let Some(pos) = name.rfind('@') { &name[..=pos] } else { name } +} + +/// Helper for observers that need to correlate VIR-level +/// `on_havoc`/`on_assign` callbacks with AIR-level WP versioned +/// constants created during `lower_query`. +/// +/// # Ordering invariant +/// +/// For each variable `x`, the Nth `record_havoc_or_assign` call +/// corresponds to the Nth `resolve` call with a `Havoc` or `Assign` +/// origin. This ordering is guaranteed because VIR emits +/// Havoc/Assign statements in the same order that `lower_query` +/// processes them. No AIR pass reorders these statements. +/// +/// Enforced via `debug_assert!` in `resolve`. +pub struct VersionCorrelator { + /// Per-base-variable queue of VIR statements (Havoc/Assign). + queues: HashMap, VecDeque>, +} + +impl VersionCorrelator { + pub fn new() -> Self { + Self { queues: HashMap::new() } + } + + /// Record a VIR-level Havoc or Assign for a variable. + /// `base` is the AIR base name (e.g., `"x@"` from `suffix_local_unique_id`). + pub fn record_havoc_or_assign(&mut self, base: &air::ast::Ident, stm: &Stm) { + self.queues.entry(base.clone()).or_default().push_back(stm.clone()); + } + + /// Resolve an AIR versioned constant to its VIR origin. + /// Returns the VIR `Stm` that caused this version to exist. + pub fn resolve(&mut self, versioned: &air::ast::Ident, _kind: VersionOrigin) -> Option { + let base = strip_version_suffix(versioned); + let base_key = Arc::new(base.to_string()); + let queue = self.queues.get_mut(&base_key)?; + debug_assert!( + !queue.is_empty(), + "VIR/AIR ordering invariant violated for {}: \ + no VIR record available (queue empty)", + versioned + ); + queue.pop_front() + } + + /// Reset between functions. + pub fn reset(&mut self) { + self.queues.clear(); + } +}