use crate::commands::{OpGenerator, OpKind, QueryOp, Style}; use crate::config::{Args, CargoVerusArgs, ShowTriggers}; use crate::context::ContextX; use crate::external::VerifOrExternal; use crate::externs::VerusExterns; use crate::query::{Query, QueryError, set_global_query}; use crate::rust_to_vir_base::mk_crate_id; use crate::spans::{SpanContext, SpanContextX, from_raw_span}; use crate::user_filter::UserFilter; use crate::util::{HashMapAbsorbWith, error}; use crate::verus_items::{VerusItem, VerusItems}; use air::ast::AssertId; use air::ast::{Command, CommandX, Commands}; use air::context::{QueryContext, SmtSolver, ValidityResult}; use air::messages::{ArcDynMessage, Diagnostics as _}; use air::profiler::Profiler; use rustc_errors::{Diag, EmissionGuarantee}; use rustc_hir::OwnerNode; use rustc_interface::interface::Compiler; use rustc_session::config::ErrorOutputType; use std::sync::Mutex; use vir::messages::{ Message, MessageLabel, MessageLevel, MessageX, ToAny, message, note, note_bare, warning, warning_bare, }; use num_format::{Locale, ToFormattedString}; use rustc_error_messages::MultiSpan; use rustc_hir::def::DefKind; use rustc_index::bit_set::DenseBitSet; use rustc_middle::ty::TyCtxt; use rustc_span::Span; use rustc_span::def_id::LOCAL_CRATE; use std::collections::{HashMap, HashSet, VecDeque}; use std::fs::File; use std::io::Write; use std::sync::Arc; use std::time::{Duration, Instant}; use vir::context::{FuncCallGraphLogFiles, GlobalCtx}; use crate::buckets::{Bucket, BucketId}; use crate::expand_errors_driver::ExpandErrorsResult; use std::rc::Rc; use vir::ast::{CrateId, Fun, Krate, VirErr}; use vir::ast_util::{fun_as_friendly_rust_name, is_visible_to}; use vir::def::{CommandContext, CommandsWithContext, CommandsWithContextX}; use vir::prelude::PreludeConfig; const RLIMIT_PER_SECOND_Z3: f32 = 3000000f32; const RLIMIT_PER_SECOND_CVC5: f32 = 333333f32; // ~= 5s #[derive(Clone, Hash, PartialEq, Eq)] pub(crate) struct ProgressBarId(String); trait Diagnostics: air::messages::Diagnostics { fn use_progress_bars(&self) -> bool; fn add_progress_bar(&self, ctx: CommandContext); fn complete_progress_bar(&self, ctx: CommandContext); } pub(crate) struct Reporter<'tcx> { spans: SpanContext, compiler_diagnostics: &'tcx rustc_errors::DiagCtxt, source_map: &'tcx rustc_span::source_map::SourceMap, } impl<'tcx> Reporter<'tcx> { pub(crate) fn new(spans: &SpanContext, compiler: &'tcx Compiler) -> Self { Reporter { spans: spans.clone(), compiler_diagnostics: &compiler.sess.dcx(), source_map: compiler.sess.source_map(), } } pub(crate) fn new_from_tcx(spans: &SpanContext, tcx: TyCtxt<'tcx>) -> Self { Reporter { spans: spans.clone(), compiler_diagnostics: &tcx.sess.dcx(), source_map: tcx.sess.source_map(), } } } /// N.B.: The compiler performs deduplication on diagnostic messages, so reporting an error twice, /// or emitting the same note twice will be surpressed (even if separated in time by other /// errors/notes) impl air::messages::Diagnostics for Reporter<'_> { fn report_as(&self, msg: &ArcDynMessage, level: MessageLevel) { let msg: &MessageX = msg.downcast_ref().expect("unexpected value in Any -> Message conversion"); let mut v: Vec = Vec::new(); for sp in &msg.spans { if let Some(span) = self.spans.from_air_span(&sp, Some(self.source_map)) { v.push(span); } } while let Some(i) = v.iter().position(|a| v.iter().any(|b| a != b && a.contains(*b))) { // Remove i in favor of the more specific spans contained by i v.remove(i); } let mut multispan = MultiSpan::from_spans(v); let mut replacement_error_note: Option = None; for MessageLabel { note, span: sp, is_proof_note, is_custom_err } in &msg.labels { let span = self.spans.from_air_span(&sp, Some(self.source_map)); if *is_custom_err { if replacement_error_note.is_none() { replacement_error_note = Some(note.clone()); } continue; } let note = if *is_proof_note { format!("note: {}", note) } else { note.clone() }; if let Some(span) = span { multispan.push_span_label(span, note); } else { dbg!(¬e, &sp.as_string); } } fn emit_with_diagnostic_details<'a, G: EmissionGuarantee>( mut diag: Diag<'a, G>, multispan: MultiSpan, help: &[String], ) { diag.span = multispan; for help in help { diag.help(help.clone()); } diag.emit(); } match level { MessageLevel::Note => emit_with_diagnostic_details( self.compiler_diagnostics.handle().struct_note(msg.note.clone()), multispan, &msg.help, ), MessageLevel::Warning => emit_with_diagnostic_details( self.compiler_diagnostics.handle().struct_warn(msg.note.clone()), multispan, &msg.help, ), MessageLevel::Error => emit_with_diagnostic_details( self.compiler_diagnostics .handle() .struct_err(replacement_error_note.clone().unwrap_or_else(|| msg.note.clone())), multispan, &msg.help, ), } if let Some(fancy_note) = &msg.fancy_note { // The fancy_note might use terminal colors, which will get escaped if we use // the Rust emitter. Thus, we have to emit this note out-of-band. eprintln!("{:}{:}", console::style("note: ").bright().blue(), fancy_note); } } fn report(&self, msg: &ArcDynMessage) { let vir_msg: &MessageX = msg.downcast_ref().expect("unexpected value in Any -> Message conversion"); self.report_as(msg, vir_msg.level) } fn report_now(&self, msg: &ArcDynMessage) { let vir_msg: &MessageX = msg.downcast_ref().expect("unexpected value in Any -> Message conversion"); self.report_as(msg, vir_msg.level) } fn report_as_now(&self, msg: &ArcDynMessage, msg_as: MessageLevel) { self.report_as(msg, msg_as) } } impl Diagnostics for Reporter<'_> { fn use_progress_bars(&self) -> bool { false } fn add_progress_bar(&self, _: CommandContext) { panic!("progress bars not supported in single-threaded Reporter"); } fn complete_progress_bar(&self, _: CommandContext) { panic!("progress bars not supported in single-threaded Reporter"); } } /// A reporter message that is being collected by the main thread pub(crate) enum ReporterMessage { ReportLongRunning(CommandContext), FinishLongRunning(CommandContext), Message(usize, Message, MessageLevel, bool), Messages(usize, Vec<(Message, MessageLevel)>, bool), WorkerPanicked(Box), Done(usize), } /// A reporter that forwards messages on an mpsc channel pub(crate) struct QueuedReporter { bucket_id: usize, queue: std::sync::mpsc::Sender, } impl QueuedReporter { pub(crate) fn new(bucket_id: usize, queue: std::sync::mpsc::Sender) -> Self { Self { bucket_id, queue } } pub(crate) fn done(&self) { self.queue.send(ReporterMessage::Done(self.bucket_id)).expect("could not send!"); } } impl air::messages::Diagnostics for QueuedReporter { fn report_as(&self, msg: &ArcDynMessage, level: MessageLevel) { let msg: Message = msg.clone().downcast().expect("unexpected value in Any -> Message conversion"); self.queue .send(ReporterMessage::Message(self.bucket_id, msg, level, false)) .expect("could not send the message!"); } fn report_as_multi(&self, msgs: Vec<(ArcDynMessage, MessageLevel)>) { let mut queue_msgs: Vec<(Message, MessageLevel)> = Vec::new(); for (msg, level) in msgs { let msg: Message = msg.clone().downcast().expect("unexpected value in Any -> Message conversion"); queue_msgs.push((msg, level)); } self.queue .send(ReporterMessage::Messages(self.bucket_id, queue_msgs, false)) .expect("could not send the message!"); } fn report_as_now(&self, msg: &ArcDynMessage, level: MessageLevel) { let msg: Message = msg.clone().downcast().expect("unexpected value in Any -> Message conversion"); self.queue .send(ReporterMessage::Message(self.bucket_id, msg, level, true)) .expect("could not send the message!"); } fn report(&self, msg: &ArcDynMessage) { let air_msg: &MessageX = msg.downcast_ref().expect("unexpected value in Any -> Message conversion"); self.report_as(msg, air_msg.level) } fn report_now(&self, msg: &ArcDynMessage) { let air_msg: &MessageX = msg.downcast_ref().expect("unexpected value in Any -> Message conversion"); self.report_as_now(msg, air_msg.level) } } impl Diagnostics for QueuedReporter { fn use_progress_bars(&self) -> bool { true } fn add_progress_bar(&self, pb: CommandContext) { self.queue .send(ReporterMessage::ReportLongRunning(pb)) .expect("could not send the message!"); } fn complete_progress_bar(&self, f: CommandContext) { self.queue .send(ReporterMessage::FinishLongRunning(f)) .expect("could not send the message!"); } } #[derive(Default)] pub struct BucketStats { /// cumulative time in AIR to verify the bucket (this includes SMT solver time) pub time_air: Duration, /// time to initialize the SMT solver pub time_smt_init: Duration, /// cumulative time of all SMT queries pub time_smt_run: Duration, /// total time to verify the bucket pub time_verify: Duration, /// rlimit used to initialize and run the SMT solver pub rlimit_count: Option<(u64, u64)>, } pub struct FunctionSmtStats { pub smt_time: Duration, pub rlimit_count: Option, } pub struct Verifier { /// this is the actual number of threads used for verification. This will be set to the /// minimum of the requested threads and the number of buckets to verify pub num_threads: usize, pub encountered_error: bool, pub encountered_vir_error: bool, pub count_verified: u64, pub count_errors: u64, /// Functions that failed to verify pub func_fails: HashSet, pub args: Args, pub user_filter: Option, pub(crate) verus_items: Option>, /// total real time to verify all activated buckets of the crate, including real time for /// the parallel bucket verification pub time_verify_crate: Duration, /// sequential part of the crate verification before parallel verification pub time_verify_crate_sequential: Duration, /// total sequantial time spent constructing the VIR pub time_vir: Duration, /// the time it took convert the VIR from rust AST pub time_vir_rust_to_vir: Duration, /// time spent in hir when creating the VIR for the crate pub time_hir: Duration, /// time spent importing VIR from other crates pub time_import: Duration, /// execution times for each bucket run in parallel pub bucket_stats: HashMap, /// smt runtimes for each function per bucket pub func_times: HashMap>, /// Details about each function pub func_details: Arc>>, /// Errors to report after verification has run deferred_errors: Arc>>, pub via_cargo_args: Option, // Some(DepTracker) if via_cargo_args.is_some(), None otherwise // In both cases, is set to None when VerifierCallbacksEraseMacro.config finishes with it dep_tracker: Option, import_virs_via_cargo: Option>, export_vir_path_via_cargo: Option, pub(crate) compile: bool, // If we've already created the log directory, this is the path to it: created_log_dir: Arc>>, created_solver_log_dir: Arc>>, vir_crate: Option, crate_id: Option, air_no_span: Option, span_resolver: Option, current_crate_modules: Option>, crate_items: Option>, warning_ctx: Option>, buckets: HashMap, // proof debugging purposes expand_flag: bool, error_format: Option, } #[derive(serde::Serialize, Clone)] pub struct FuncDetails { pub obligation_proof_notes: HashSet, pub failed_proof_notes: HashSet, } impl Default for FuncDetails { fn default() -> Self { Self { obligation_proof_notes: Default::default(), failed_proof_notes: Default::default() } } } impl FuncDetails { fn absorb(&mut self, other: Self) { self.obligation_proof_notes.extend(other.obligation_proof_notes); self.failed_proof_notes.extend(other.failed_proof_notes); } pub fn to_json(&self) -> serde_json::Value { serde_json::to_value(self).unwrap() } } fn report_chosen_triggers( diagnostics: &impl air::messages::Diagnostics, chosen: &vir::context::ChosenTriggers, automatically: bool, ) { let s = if automatically { "automatically chose" } else { "selected" }.to_owned(); diagnostics.report(¬e(&chosen.span, s + " triggers for this expression:").to_any()); for (n, trigger) in chosen.triggers.iter().enumerate() { let note = format!(" trigger {} of {}:", n + 1, chosen.triggers.len()); let msg = note_bare(note); let msg: ArcDynMessage = trigger.iter().fold(msg, |m, (s, _)| { let m: &vir::messages::MessageX = m.downcast_ref().expect("unexpected value in Any -> Message conversion"); m.primary_span(s) }); diagnostics.report(&msg); } } pub(crate) fn io_vir_err(msg: String, err: std::io::Error) -> VirErr { error(format!("{msg}: {err}")) } pub fn module_name(module: &vir::ast::Path) -> String { module.segments.iter().map(|s| s.to_string()).collect::>().join("::") } mod util { pub(crate) struct PanicOnDropVec(Option>); // For https://github.com/verus-lang/verus/issues/1044 : pub(crate) static PANIC_ON_DROP_VEC: std::sync::atomic::AtomicBool = std::sync::atomic::AtomicBool::new(true); impl PanicOnDropVec { pub fn new(v: Vec) -> Self { PanicOnDropVec(Some(v)) } pub fn into_inner(mut self) -> Vec { self.0.take().unwrap() } pub fn as_mut(&mut self) -> &mut Vec { self.0.as_mut().unwrap() } } impl Drop for PanicOnDropVec { fn drop(&mut self) { if self.0.is_some() && PANIC_ON_DROP_VEC.load(std::sync::atomic::Ordering::SeqCst) { panic!("dropped, expected call to `into_inner` instead"); } } } } use util::PanicOnDropVec; struct RunCommandQueriesResult { invalidity: bool, timed_out: bool, not_skipped: bool, used_axioms: Option>, } impl std::ops::Add for RunCommandQueriesResult { type Output = Self; fn add(self, rhs: Self) -> Self::Output { RunCommandQueriesResult { invalidity: self.invalidity || rhs.invalidity, timed_out: self.timed_out || rhs.timed_out, not_skipped: self.not_skipped || rhs.not_skipped, used_axioms: match (self.used_axioms, rhs.used_axioms) { (Some(u), None) => Some(u), (None, Some(u)) => Some(u), (None, None) => None, (Some(_), Some(_)) => panic!("only the primary query should contain used_axioms"), }, } } } struct VerifyBucketOut { time_smt_init: Duration, time_smt_run: Duration, rlimit_count: Option<(u64, u64)>, } pub(crate) enum VerifyErr { Vir(VirErr), Emitted, } impl From for VerifyErr { fn from(err: VirErr) -> Self { VerifyErr::Vir(err) } } /// A titled group of AIR commands. struct CommandBatch { title: String, commands: Commands, } impl CommandBatch { fn new(title: impl Into, commands: Commands) -> Self { CommandBatch { title: title.into(), commands } } } impl Verifier { pub fn new( args: Args, via_cargo_args: Option, via_cargo_compile: bool, dep_tracker: crate::cargo_verus_dep_tracker::DepTracker, ) -> Verifier { let compile = args.compile || via_cargo_compile; Verifier { num_threads: 1, encountered_error: false, encountered_vir_error: false, count_verified: 0, count_errors: 0, func_fails: HashSet::new(), args, user_filter: None, verus_items: None, time_verify_crate: Duration::new(0, 0), time_verify_crate_sequential: Duration::new(0, 0), time_hir: Duration::new(0, 0), time_import: Duration::new(0, 0), time_vir: Duration::new(0, 0), time_vir_rust_to_vir: Duration::new(0, 0), bucket_stats: HashMap::new(), func_times: HashMap::new(), func_details: Arc::new(Mutex::new(HashMap::new())), deferred_errors: Arc::new(Mutex::new(Vec::new())), dep_tracker: if via_cargo_args.is_some() { Some(dep_tracker) } else { None }, via_cargo_args, import_virs_via_cargo: None, export_vir_path_via_cargo: None, compile, created_log_dir: Arc::new(std::sync::Mutex::new(None)), created_solver_log_dir: Arc::new(std::sync::Mutex::new(None)), vir_crate: None, crate_id: None, air_no_span: None, span_resolver: None, current_crate_modules: None, crate_items: None, warning_ctx: None, buckets: HashMap::new(), expand_flag: false, error_format: None, } } pub fn from_self(&self) -> Verifier { // Note: if we needed to share dep_tracker, we could clone it or Arc it assert!(self.dep_tracker.is_none()); Verifier { num_threads: 1, encountered_error: self.encountered_error, encountered_vir_error: false, count_verified: 0, count_errors: 0, func_fails: HashSet::new(), args: self.args.clone(), user_filter: self.user_filter.clone(), verus_items: self.verus_items.clone(), time_verify_crate: Duration::new(0, 0), time_verify_crate_sequential: Duration::new(0, 0), time_hir: Duration::new(0, 0), time_import: Duration::new(0, 0), time_vir: Duration::new(0, 0), time_vir_rust_to_vir: Duration::new(0, 0), bucket_stats: HashMap::new(), func_times: HashMap::new(), func_details: Arc::new(Mutex::new(HashMap::new())), deferred_errors: Arc::new(Mutex::new(Vec::new())), via_cargo_args: self.via_cargo_args.clone(), dep_tracker: None, import_virs_via_cargo: self.import_virs_via_cargo.clone(), export_vir_path_via_cargo: self.export_vir_path_via_cargo.clone(), compile: self.compile, created_log_dir: self.created_log_dir.clone(), created_solver_log_dir: self.created_solver_log_dir.clone(), vir_crate: self.vir_crate.clone(), crate_id: self.crate_id.clone(), air_no_span: self.air_no_span.clone(), span_resolver: self.span_resolver.clone(), current_crate_modules: self.current_crate_modules.clone(), crate_items: self.crate_items.clone(), warning_ctx: self.warning_ctx.clone(), buckets: self.buckets.clone(), expand_flag: self.expand_flag, error_format: self.error_format, } } /// merges two verifiers by summing up times and verified stats from other into self. pub fn merge(&mut self, other: Self) { self.count_verified += other.count_verified; self.count_errors += other.count_errors; self.func_fails.extend(other.func_fails); self.time_vir += other.time_vir; self.time_vir_rust_to_vir += other.time_vir_rust_to_vir; self.bucket_stats.extend(other.bucket_stats); self.func_times.extend(other.func_times); let func_details = { (*other.func_details.lock().unwrap()).clone() }; { self.func_details.lock().unwrap().absorb_with(func_details, |lhs, rhs| lhs.absorb(rhs)); } let deferred_errors = { (*other.deferred_errors.lock().unwrap()).clone() }; { self.deferred_errors.lock().unwrap().extend(deferred_errors); } } fn get_bucket<'a>(&'a self, bucket_id: &BucketId) -> &'a Bucket { self.buckets.get(bucket_id).expect("expected valid BucketId") } fn ensure_solver_log_dir(&mut self) -> Result { Ok({ let mut created_solver_log_dir = self.created_solver_log_dir.lock().expect("failed to lock created_solver_log_dir"); if let Some(dir_path) = &*created_solver_log_dir { dir_path.clone() } else { let dir = std::path::PathBuf::from(crate::config::SOLVER_LOG_DIR.to_string()); delete_dir_if_exists_and_is_dir(&dir)?; std::fs::create_dir_all(&dir).map_err(|err| { io_vir_err(format!("could not create directory {}", dir.display()), err) })?; *created_solver_log_dir = Some(dir.clone()); dir } }) } fn create_log_file( &mut self, bucket_id_opt: Option<&BucketId>, suffix: &str, ) -> Result { let dir_path = { let mut created_log_dir = self.created_log_dir.lock().expect("failed to lock created_log_dir"); if let Some(dir_path) = &*created_log_dir { dir_path.clone() } else { let dir = std::path::PathBuf::from(if let Some(dir) = &self.args.log_dir { dir.clone() } else { crate::config::LOG_DIR.to_string() }); delete_dir_if_exists_and_is_dir(&dir)?; std::fs::create_dir_all(&dir).map_err(|err| { io_vir_err(format!("could not create directory {}", dir.display()), err) })?; *created_log_dir = Some(dir.clone()); dir } }; let log_file_name = self.log_file_name(&dir_path, bucket_id_opt, suffix); match File::create(&log_file_name) { Ok(file) => Ok(file), Err(err) => { Err(io_vir_err(format!("could not open file {}", log_file_name.display()), err)) } } } fn log_file_name( &self, dir_path: &std::path::Path, bucket_id_opt: Option<&BucketId>, suffix: &str, ) -> std::path::PathBuf { let prefix = match bucket_id_opt { None => "crate".to_string(), Some(bucket_id) => bucket_id.to_log_string(), }; std::path::PathBuf::from(&dir_path).join(format!("{prefix}{suffix}")) } /// Use when we expect our call to Z3 to always succeed /// If it doesn't, it's an internal error, not a failure /// to validate user code. fn check_internal_result(result: ValidityResult) { match result { ValidityResult::Valid(air::context::UsageInfo::None) => {} ValidityResult::TypeError(err) => { util::PANIC_ON_DROP_VEC.store(false, std::sync::atomic::Ordering::SeqCst); panic!("internal error: ill-typed AIR code: {}", err) } _ => panic!("internal error: decls should not generate queries ({:?})", result), } } fn print_profile_stats( &self, diagnostics: &impl air::messages::Diagnostics, profiler: Profiler, qid_map: &HashMap, ) { let num_quants = profiler.quant_count(); let total = profiler.total_instantiations(); let max = 10; let msg = format!( "Observed {} total instantiations of user-level quantifiers", total.to_formatted_string(&Locale::en) ); diagnostics.report(¬e_bare(&msg).to_any()); for (index, cost) in profiler.iter().take(max).enumerate() { // Report the quantifier let count = cost.instantiations; let note = format!( "Cost * Instantiations: {} (Instantiated {} times - {}% of the total, cost {}) top {} of {} user-level quantifiers.\n", count * cost.cost, count.to_formatted_string(&Locale::en), 100 * count / total, cost.cost, index + 1, num_quants ); let bnd_info = qid_map .get(&cost.quant) .unwrap_or_else(|| panic!("Failed to find quantifier {}", cost.quant)); let mut msg = note_bare(note); // Summarize the triggers it used let triggers = &bnd_info.user.as_ref().unwrap().trigs; for trigger in triggers.iter() { // HACK: we do not have span info for the verus_builtin crate if !trigger.iter().any(|t| t.span.as_string.contains("verus_builtin")) { msg = trigger.iter().fold(msg, |m, e| m.primary_span(&e.span)); } } msg = msg.secondary_label( &bnd_info.user.as_ref().unwrap().span, "triggers selected for this quantifier".to_string(), ); diagnostics.report(&msg.to_any()); } } /// Check the result of a query that was based on user input. /// Success/failure will (eventually) be communicated back to the user. /// invalidity is true if there was at least one Invalid resulting in an error. /// timed_out is true if there was at least one time out /// not_skipped is true if the performed command was a CheckValid() request /// /// If `level` is None, do not report errors. fn check_result_validity( &mut self, bucket_id: &BucketId, reporter: &impl Diagnostics, diagnostics_to_report: &std::cell::RefCell>>, level: Option, air_context: &mut air::context::Context, command: &Command, context: &CommandContext, prover_choice: vir::def::ProverChoice, default_prover_failed_assert_ids: &mut Vec, ) -> RunCommandQueriesResult { let is_singular = prover_choice == vir::def::ProverChoice::Singular; let message_interface = Arc::new(vir::messages::VirMessageInterface {}); let do_report_long_running = self.args.report_long_running; let report_long_running = || { let report_fn: Box ()> = Box::new( move |elapsed, completed| { if !completed { if let Some(msgs) = diagnostics_to_report.take() { let mut msgs_any: Vec<(ArcDynMessage, MessageLevel)> = Vec::new(); for (error, error_level) in msgs.into_inner().into_iter() { msgs_any.push((error.clone().to_any(), error_level)); } reporter.report_as_multi(msgs_any); } } if do_report_long_running { if !completed { if reporter.use_progress_bars() { reporter.add_progress_bar(context.clone()); } else { let msg = format!( "{} has been running for {} seconds\nreporting errors as they are discovered (they may not be in source order)", context.desc, elapsed.as_secs() ); let msg = note(&context.span, msg); reporter.report_now(&msg.to_any()); } } else { if reporter.use_progress_bars() { reporter.complete_progress_bar(context.clone()); } else { let msg = format!( "{} finished in {} seconds", context.desc, elapsed.as_secs() ); let msg = note(&context.span, msg); reporter.report_now(&msg.to_any()); } } } }, ); (std::time::Duration::from_secs(2), report_fn) }; let is_check_valid = matches!(**command, CommandX::CheckValid(_)); let time0 = Instant::now(); #[cfg(feature = "singular")] let mut result = if !is_singular { air_context.command( &*message_interface, reporter, &command, QueryContext { report_long_running: Some(&mut report_long_running()) }, ) } else { crate::singular::check_singular_valid( air_context, &command, &context.span, QueryContext { report_long_running: Some(&mut report_long_running()) }, reporter, ) }; #[cfg(not(feature = "singular"))] let mut result = air_context.command( &*message_interface, reporter, &command, QueryContext { report_long_running: Some(&mut report_long_running()) }, ); let time1 = Instant::now(); let bucket_time = self.bucket_stats.get_mut(bucket_id).expect("bucket time not found"); bucket_time.time_air += time1 - time0; let mut is_first_check = true; let mut checks_remaining = self.args.multiple_errors; let mut only_check_earlier = false; let mut invalidity = false; let mut timed_out = false; let mut used_axioms = None; loop { match result { ValidityResult::Valid(usage_info) => { if (is_check_valid && is_first_check && level == Some(MessageLevel::Error)) || is_singular { self.count_verified += 1; if let air::context::UsageInfo::UsedAxioms(axioms) = usage_info { assert!(used_axioms.replace(axioms).is_none()); } } break; } ValidityResult::TypeError(err) => { util::PANIC_ON_DROP_VEC.store(false, std::sync::atomic::Ordering::SeqCst); panic!("internal error: generated ill-typed AIR code: {}", err); } ValidityResult::Canceled => { if is_first_check && level == Some(MessageLevel::Error) { self.count_errors += 1; self.func_fails.insert(context.fun.clone()); invalidity = true; } if self.expand_flag { invalidity = true; } let mut msg = format!("{}: resource limit (rlimit) exceeded", context.desc); if !self.args.profile && !self.args.profile_all && !self.args.capture_profiles { msg.push_str("; consider rerunning with `--profile` for more details"); } if let Some(level) = level { reporter.report(&message(level, msg, &context.span).to_any()); } // need to report that we need to rerun from this function (into spinoff) // so that we can run the profiler on an isolated file on the second pass timed_out = true; break; } ValidityResult::Invalid(None, error, _) | ValidityResult::Invalid(_, error @ None, _) => { if is_first_check && level == Some(MessageLevel::Error) { self.count_errors += 1; invalidity = true; } if self.expand_flag { invalidity = true; } if let Some(level) = level { if let Some(error) = error { // singular_invalid case reporter.report_as(&error, level); } else { // bitvector case reporter.report(&message(level, &context.desc, &context.span).to_any()); } } break; } ValidityResult::Invalid(Some(_air_model), Some(error), assert_id_opt) => { if let Some(assert_id) = assert_id_opt { if prover_choice == vir::def::ProverChoice::DefaultProver { default_prover_failed_assert_ids.push(assert_id.clone()); } } if is_first_check && level == Some(MessageLevel::Error) { self.count_errors += 1; self.func_fails.insert(context.fun.clone()); invalidity = true; } if self.expand_flag { invalidity = true; } let error: Message = error.downcast().unwrap(); if let Some(level) = level { if !self.expand_flag { match &mut *diagnostics_to_report.borrow_mut() { Some(collected) => { collected.as_mut().push((error.clone(), level)); } _ => { reporter.report_as(&error.clone().to_any(), level); } } } } // Collect `proof_note` labels related to this failure. let mut proof_notes = HashSet::new(); for label in &error.labels { if label.is_proof_note && !label.is_custom_err { proof_notes.insert(label.note.clone()); } } self.record_func_failed_proof_notes(context.fun.clone(), proof_notes); if level == Some(MessageLevel::Error) { if self.args.expand_errors { assert!(!self.expand_flag); } } if self.args.multiple_errors == 0 { break; } is_first_check = false; if !only_check_earlier { checks_remaining -= 1; if checks_remaining == 0 { only_check_earlier = true; } } let time0 = Instant::now(); result = air_context.check_valid_again( reporter, only_check_earlier, QueryContext { report_long_running: Some(&mut report_long_running()) }, ); let time1 = Instant::now(); let bucket_time = self.bucket_stats.get_mut(bucket_id).expect("bucket time not found"); bucket_time.time_air += time1 - time0; } ValidityResult::UnexpectedOutput(err) => { util::PANIC_ON_DROP_VEC.store(false, std::sync::atomic::Ordering::SeqCst); panic!("unexpected output from solver: {} {}", context.span.as_string, err); } } } if level == Some(MessageLevel::Error) && checks_remaining == 0 { let msg = format!( "{}: not all errors may have been reported; rerun with a higher value for --multiple-errors to find other potential errors in this function", context.desc ); reporter.report(¬e(&context.span, msg).to_any()); } if is_check_valid && !is_singular { air_context.finish_query(); } RunCommandQueriesResult { used_axioms, invalidity, timed_out, not_skipped: matches!(**command, CommandX::CheckValid(_)), } } fn run_command_batch( &mut self, bucket_id: &BucketId, diagnostics: &impl air::messages::Diagnostics, air_context: &mut air::context::Context, batch: &CommandBatch, ) { if batch.commands.len() > 0 { air_context.blank_line(); air_context.comment(&batch.title); } for command in batch.commands.iter() { let time0 = Instant::now(); Self::check_internal_result(air_context.command( &vir::messages::VirMessageInterface {}, diagnostics, &command, Default::default(), )); let time1 = Instant::now(); let bucket_time = self.bucket_stats.get_mut(bucket_id).expect("bucket time not found"); bucket_time.time_air += time1 - time0; } } fn run_command_batches( &mut self, bucket_id: &BucketId, diagnostics: &impl air::messages::Diagnostics, air_context: &mut air::context::Context, batches: &[CommandBatch], ) { for batch in batches { self.run_command_batch(bucket_id, diagnostics, air_context, batch); } } /// Returns the status of running the provided queries /// invalidity: whether the command returned invalid or not /// timed_out: whether the command timed out or not /// not_skipped : whether a nontrivial validity check was performed or not fn run_commands_queries( &mut self, reporter: &impl Diagnostics, level: Option, diagnostics_to_report: &std::cell::RefCell>>, air_context: &mut air::context::Context, commands_with_context: CommandsWithContext, bucket_id: &BucketId, function_name: &Fun, comment: &str, desc_prefix: Option<&str>, default_prover_failed_assert_ids: &mut Vec, ) -> RunCommandQueriesResult { let user_filter = self.user_filter.as_ref().unwrap(); let includes_function = user_filter.includes_function(function_name); if !includes_function { return RunCommandQueriesResult { invalidity: false, timed_out: false, not_skipped: false, used_axioms: None, }; } let mut result = RunCommandQueriesResult { invalidity: false, timed_out: false, not_skipped: false, used_axioms: None, }; let CommandsWithContextX { context, commands, prover_choice, skip_recommends: _ } = &*commands_with_context; let context = context.with_desc_prefix(desc_prefix); if commands.len() > 0 { air_context.blank_line(); air_context.comment(comment); air_context.comment(&context.span.as_string); } for command in commands.iter() { result = result + self.check_result_validity( bucket_id, reporter, diagnostics_to_report, level, air_context, &command, &context, *prover_choice, default_prover_failed_assert_ids, ); } result } fn log_file_name_suffix( ctx: &vir::context::Ctx, is_rerun: bool, query_function_path_counter: Option<(&vir::ast::Path, usize)>, expand_flag: bool, suffix: &str, ) -> String { let rerun_msg = if is_rerun { "_rerun" } else { "" }; let count_msg = query_function_path_counter .map(|(n, ref c)| format!("{}_{:02}", ctx.name_ctxt.path_to_string(n), c)) .unwrap_or("".to_string()); let expand_msg = if expand_flag { "_expand" } else { "" }; format!("{}{}{}{}", rerun_msg, count_msg, expand_msg, suffix,) } fn set_rlimit(air_context: &mut air::context::Context, rlimit: f32) { let per_second = match air_context.get_solver() { air::context::SmtSolver::Z3 => RLIMIT_PER_SECOND_Z3, air::context::SmtSolver::Cvc5 => RLIMIT_PER_SECOND_CVC5, }; air_context.set_rlimit(if rlimit == f32::INFINITY { 0 // both solvers interpret a zero rlimit as infinity } else { (rlimit * per_second).min(u32::MAX as f32) as u32 }); } fn set_default_rlimit(&self, air_context: &mut air::context::Context) { Self::set_rlimit(air_context, self.args.rlimit); } fn new_air_context_with_prelude<'m>( &mut self, ctx: &vir::context::Ctx, message_interface: Arc, diagnostics: &impl air::messages::Diagnostics, bucket_id: &BucketId, query_function_path_counter: Option<(&vir::ast::Path, usize)>, is_rerun: bool, prelude_config: vir::prelude::PreludeConfig, profile_file_name: Option<&std::path::PathBuf>, prover_choice: vir::def::ProverChoice, ) -> Result { let mut air_context = air::context::Context::new_with_encoding( message_interface.clone(), self.args.solver, self.args.smt_encoding, ); air_context.set_ignore_unexpected_smt(self.args.ignore_unexpected_smt); if let Some(profile_file_name) = profile_file_name { air_context.set_profile_with_logfile_name( profile_file_name.to_str().expect("invalid prover log path").to_owned(), ); } if self.args.log_all || self.args.log_args.log_air_initial { let file = self.create_log_file( Some(bucket_id), Self::log_file_name_suffix( ctx, is_rerun, query_function_path_counter, self.expand_flag, crate::config::AIR_INITIAL_FILE_SUFFIX, ) .as_str(), )?; air_context.set_air_initial_log(Box::new(file)); } if self.args.log_all || self.args.log_args.log_air_final { let file = self.create_log_file( Some(bucket_id), Self::log_file_name_suffix( ctx, is_rerun, query_function_path_counter, self.expand_flag, crate::config::AIR_FINAL_FILE_SUFFIX, ) .as_str(), )?; air_context.set_air_final_log(Box::new(file)); } if self.args.log_all || self.args.log_args.log_smt { let file = self.create_log_file( Some(bucket_id), Self::log_file_name_suffix( ctx, is_rerun, query_function_path_counter, self.expand_flag, crate::config::SMT_FILE_SUFFIX, ) .as_str(), )?; air_context.set_smt_log(Box::new(file)); } if self.args.log_all || self.args.log_args.log_smt_transcript { let file = self.create_log_file( Some(bucket_id), Self::log_file_name_suffix( ctx, is_rerun, query_function_path_counter, self.expand_flag, crate::config::SMT_TRANSCRIPT_FILE_SUFFIX, ) .as_str(), )?; air_context.set_smt_transcript_log(Box::new(file)); } // A by(bit_vector) query is self-contained, so it runs prelude-free: it omits the // recommended-options preset, the prelude, and the bucket background. let bitvector = prover_choice == vir::def::ProverChoice::BitVector; if !bitvector { air_context.set_solver_option("air_recommended_options", "true"); } self.set_default_rlimit(&mut air_context); for (option, value) in self.args.smt_options.iter() { air_context.set_solver_option(&option, &value); } if !bitvector { if self.args.axiom_usage_info { air_context.enable_usage_info(); } self.run_command_batch( bucket_id, diagnostics, &mut air_context, &CommandBatch::new("Prelude", ctx.prelude(prelude_config)), ); } air_context.blank_line(); air_context.comment(&("MODULE '".to_string() + &bucket_id.friendly_name() + "'")); Ok(air_context) } /// Per-query SMT tuning options. fn apply_per_query_smt_options( &self, air_context: &mut air::context::Context, prover_choice: vir::def::ProverChoice, ) { match prover_choice { vir::def::ProverChoice::BitVector => { // A prelude-free by(bit_vector) query carries no per-query // options: solver defaults work well. // // TODO: tune Z3/CVC5 options for bit-vector queries } vir::def::ProverChoice::Nonlinear => match self.args.solver { air::context::SmtSolver::Z3 => { air_context.set_solver_option("smt.arith.solver", "6") } // TODO: What cvc5 settings would help here? air::context::SmtSolver::Cvc5 => {} }, vir::def::ProverChoice::DefaultProver | vir::def::ProverChoice::Singular => {} } } fn new_air_context_with_bucket_context<'m>( &mut self, message_interface: Arc, ctx: &vir::context::Ctx, diagnostics: &impl air::messages::Diagnostics, bucket_id: &BucketId, query_function_path_counter: Option<(&vir::ast::Path, usize)>, bucket_context: &[CommandBatch], is_rerun: bool, span: &vir::messages::Span, profile_file_name: Option<&std::path::PathBuf>, spinoff_reason: &str, prover_choice: vir::def::ProverChoice, ) -> Result { let mut air_context = self.new_air_context_with_prelude( ctx, message_interface.clone(), diagnostics, bucket_id, query_function_path_counter, is_rerun, PreludeConfig { arch_word_bits: ctx.arch_word_bits, smt_encoding: self.args.smt_encoding, }, profile_file_name, prover_choice, )?; // Attach the same shared observer objects to the spinoff context 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(); air_context.comment(&format!("query spun off because: {}", spinoff_reason)); // set up bucket context (skipped for a prelude-free bit_vector query) if prover_choice != vir::def::ProverChoice::BitVector { self.run_command_batches(bucket_id, diagnostics, &mut air_context, bucket_context); } Ok(air_context) } // Verify a single bucket fn verify_bucket( &mut self, reporter: &impl Diagnostics, krate: &vir::sst::KrateSst, bucket_id: &BucketId, ctx: &mut vir::context::Ctx, ) -> Result { let message_interface = Arc::new(vir::messages::VirMessageInterface {}); assert!(!(self.args.profile && self.args.profile_all)); assert!(!(self.args.profile && self.args.capture_profiles)); let profile_all_file_name = if self.args.profile_all || self.args.capture_profiles { let solver_log_dir = self.ensure_solver_log_dir()?; let profile_file_name = self.log_file_name( &solver_log_dir, Some(bucket_id), Self::log_file_name_suffix( ctx, false, None, false, crate::config::PROFILE_FILE_SUFFIX, ) .as_str(), ); assert!(!profile_file_name.exists()); Some(profile_file_name) } else { None }; let mut air_context = self.new_air_context_with_prelude( ctx, message_interface.clone(), reporter, bucket_id, None, false, PreludeConfig { arch_word_bits: ctx.arch_word_bits, smt_encoding: self.args.smt_encoding, }, 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 Rc 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 => { cargo_verus_toolchains::external_deps::Z3_VERSION.to_string() } air::context::SmtSolver::Cvc5 => { cargo_verus_toolchains::external_deps::CVC5_VERSION.to_string() } }); } let mut spunoff_time_smt_init = Duration::ZERO; let mut spunoff_time_smt_run = Duration::ZERO; let mut spunoff_rlimit_count: Option<(u64, u64)> = match self.args.solver { SmtSolver::Z3 => Some((0, 0)), SmtSolver::Cvc5 => None, }; let module = &ctx.module_path(); // Bucket context. // // Inserted into the main context, but also stored so the identical // context can be used for spinoff queries. Extended as context ops are // encountered below. let mut bucket_context = vec![ CommandBatch::new("Fuel", ctx.fuel()), CommandBatch::new("Trait-Decls", vir::traits::trait_decls_to_air(ctx, &krate)), CommandBatch::new( "Associated-Type-Decls", vir::assoc_types_to_air::assoc_type_decls_to_air(ctx, &krate.traits), ), CommandBatch::new( "Datatypes", vir::datatype_to_air::datatypes_and_primitives_to_air( ctx, &krate .datatypes .iter() .filter(|d| is_visible_to(&d.x.visibility, module)) .cloned() .collect(), ), ), CommandBatch::new("Trait-Bounds", vir::traits::trait_bound_axioms(ctx, &krate.traits)), CommandBatch::new( "Associated-Type-Impls", vir::assoc_types_to_air::assoc_type_impls_to_air(ctx, &krate.assoc_type_impls), ), CommandBatch::new( "Opaque-Type-Constructors", vir::opaque_type_to_air::opaque_types_to_air(ctx, &krate.opaque_types), ), ]; // Function declarations and their proof notes. let func_to_requires_proof_notes = HashMap::from_iter(krate.functions.iter().map(|function| { ( function.x.name.clone(), vir::sst_util::func_collect_requires_proof_notes(function), ) })); for function in &krate.functions { let obligation_proof_notes = vir::sst_util::func_collect_obligation_proof_notes( function, &func_to_requires_proof_notes, ); self.record_func_obligation_proof_notes( function.x.name.clone(), obligation_proof_notes, ); ctx.fun = vir::ast_to_sst_func::mk_fun_ctx(function, false); let commands = vir::sst_to_air_func::func_name_to_air(ctx, reporter, function)?; let title = "Function-Decl ".to_string() + &fun_as_friendly_rust_name(&function.x.name); bucket_context.push(CommandBatch::new(title, commands)); } ctx.fun = None; // Insert initial bucket context. self.run_command_batches(bucket_id, reporter, &mut air_context, &bucket_context); let bucket = self.get_bucket(bucket_id); let mut opgen = OpGenerator::new(ctx, krate, bucket.clone()); while let Some(mut function_opgen) = opgen.next()? { let diagnostics_to_report: std::cell::RefCell< Option>, > = std::cell::RefCell::new(Some(PanicOnDropVec::new(Vec::new()))); let mut flush_diagnostics_to_report = false; loop { let mut next_op = None; let mut expand_errors_diagnostic = None; if let Some(r) = function_opgen.expand_errors_next(self.error_format) { match r { Ok(op) => { next_op = Some(op); } Err(diagnostic) => { expand_errors_diagnostic = Some(diagnostic); flush_diagnostics_to_report = true; } } } if next_op.is_none() { next_op = function_opgen.next(); } if next_op.is_none() { flush_diagnostics_to_report = true; } if flush_diagnostics_to_report { if let Some(msgs) = diagnostics_to_report.take() { let mut msgs_any: Vec<(ArcDynMessage, MessageLevel)> = Vec::new(); for (error, error_level) in msgs.into_inner().into_iter() { msgs_any.push((error.clone().to_any(), error_level)); } reporter.report_as_multi(msgs_any); } if let Some(diag) = expand_errors_diagnostic { reporter.report(&diag); } } let Some(op) = next_op else { break; }; match &op.kind { OpKind::Context(_context_op, commands) => { let batch = CommandBatch::new(op.to_air_comment(), commands.clone()); self.run_command_batch(bucket_id, reporter, &mut air_context, &batch); bucket_context.push(batch); } OpKind::Query { query_op, commands_with_context_list, profile_rerun, func_check_sst, } => { let level = match query_op { QueryOp::SpecTermination => MessageLevel::Error, QueryOp::Body(Style::Normal) => MessageLevel::Error, QueryOp::Body(Style::RecommendsFollowupFromError) => MessageLevel::Note, QueryOp::Body(Style::RecommendsChecked) => MessageLevel::Warning, QueryOp::Body(Style::Expanded) => MessageLevel::Note, QueryOp::Body(Style::CheckApiSafety) => MessageLevel::Error, }; let function = &op.get_function(); let is_recommend = query_op.is_recommend(); self.expand_flag = query_op.is_expanded(); let mut spinoff_context_counter = 1; let mut any_invalid = false; let mut any_timed_out = false; let mut default_prover_failed_assert_ids = vec![]; let mut func_curr_smt_time = Duration::ZERO; let mut func_curr_smt_rlimit_count = match self.args.solver { air::context::SmtSolver::Z3 => Some(0), air::context::SmtSolver::Cvc5 => None, }; for cmds in commands_with_context_list.iter() { if is_recommend && cmds.skip_recommends { continue; } if cmds.prover_choice == vir::def::ProverChoice::Singular { #[cfg(not(feature = "singular"))] panic!( "Found singular command when Verus is compiled without Singular feature" ); } let mut spinoff_context; let do_spinoff = (cmds.prover_choice == vir::def::ProverChoice::Nonlinear) || (cmds.prover_choice == vir::def::ProverChoice::BitVector) || *profile_rerun || self.args.spinoff_all; let profile_file_name = if *profile_rerun || ((self.args.profile_all || self.args.capture_profiles) && do_spinoff) { let solver_log_dir = self.ensure_solver_log_dir()?; let profile_file_name = self.log_file_name( &solver_log_dir, Some(bucket_id), Self::log_file_name_suffix( function_opgen.ctx(), is_recommend, Some((&(function.x.name).path, spinoff_context_counter)), self.expand_flag, crate::config::PROFILE_FILE_SUFFIX, ) .as_str(), ); assert!(!profile_file_name.exists()); Some(profile_file_name) } else { None }; let mut query_air_context = if do_spinoff { let spinoff_reason = if cmds.prover_choice == vir::def::ProverChoice::Nonlinear { "nonlinear" } else if cmds.prover_choice == vir::def::ProverChoice::BitVector { "bitvector" } else if *profile_rerun { "profile_rerun" } else { "spinoff_all" }; spinoff_context = self.new_air_context_with_bucket_context( message_interface.clone(), function_opgen.ctx(), reporter, bucket_id, Some((&(function.x.name).path, spinoff_context_counter)), &bucket_context, is_recommend, &cmds.context.span, profile_file_name.as_ref(), spinoff_reason, cmds.prover_choice, )?; // for bitvector, only one query, no push/pop if cmds.prover_choice == vir::def::ProverChoice::BitVector { spinoff_context.set_single_check_query(); } // Apply prover-specific SMT tuning. self.apply_per_query_smt_options( &mut spinoff_context, cmds.prover_choice, ); spinoff_context_counter += 1; &mut spinoff_context } else { &mut air_context }; let iter_curr_smt_time = query_air_context.get_time().1; let iter_curr_smt_rlimit_count = query_air_context.get_rlimit_count().map(|x| x.1); if let Some(rlimit) = function.x.attrs.rlimit { if query_air_context.rlimit_is_mutable() { Self::set_rlimit(&mut query_air_context, rlimit); } else { reporter.report( &warning( &cmds.context.span, "`#[verifier::rlimit]` is not supported with your current solver; \ the global `--rlimit` applies instead", ) .to_any(), ); } } let RunCommandQueriesResult { invalidity: command_invalidity, timed_out: command_timed_out, not_skipped: command_not_skipped, used_axioms: command_used_axioms, } = self.run_commands_queries( reporter, (!profile_rerun).then(|| level), &diagnostics_to_report, query_air_context, cmds.clone(), bucket_id, &function.x.name, &op.to_air_comment(), None, &mut default_prover_failed_assert_ids, ); func_curr_smt_time += query_air_context.get_time().1 - iter_curr_smt_time; if let Some(func_curr_smt_rlimit_count) = &mut func_curr_smt_rlimit_count { *func_curr_smt_rlimit_count += query_air_context .get_rlimit_count() .expect("rlimit count in query context") .1 - iter_curr_smt_rlimit_count .expect("rlimit count in query context"); } if do_spinoff { let (time_smt_init, time_smt_run) = query_air_context.get_time(); spunoff_time_smt_init += time_smt_init; spunoff_time_smt_run += time_smt_run; if let Some(spunoff_rlimit_count) = &mut spunoff_rlimit_count { let (init, run) = query_air_context .get_rlimit_count() .expect("rlimit count in query context"); (*spunoff_rlimit_count).0 += init; (*spunoff_rlimit_count).1 += run; } } if function.x.attrs.rlimit.is_some() { self.set_default_rlimit(&mut query_air_context); } any_invalid |= command_invalidity; any_timed_out |= command_timed_out; if let Some(used_axioms) = command_used_axioms { if used_axioms.len() > 0 { let axioms_list = used_axioms .iter() .map(|x| { if x.starts_with(vir::def::AXIOM_NAME_PRELUDE) { return format!(" - (prelude) {}", x); } let funx = &function_opgen.ctx().fun_ident_map[x]; let is_reveal_group = krate .reveal_groups .iter() .find(|g| &g.x.name == funx) .is_some(); format!( " -{} {}", if is_reveal_group { " (group)" } else { "" }, fun_as_friendly_rust_name(&funx,), ) }) .collect::>() .join(",\n"); let msg = format!( "{} used these broadcasted lemmas and broadcast groups:\n{}", op.to_friendly_desc() .unwrap_or("checking this function".to_owned()), axioms_list, ); reporter .report(&vir::messages::note(&function.span, msg).to_any()); } } if let Some(profile_file_name) = profile_file_name { if command_not_skipped && query_air_context.check_valid_used() { assert!(profile_file_name.exists()); let current_profile_description = op.to_friendly_desc().map(|x| x + " ").unwrap_or("".into()) + &fun_as_friendly_rust_name(&function.x.name); match Profiler::parse( message_interface.clone(), &profile_file_name, Some(¤t_profile_description), reporter, ) { Ok(profiler) => { if self.args.capture_profiles { // if capture profiles was passed, silence the report // as we are only interested in the graph/profile data crate::profiler::write_instantiation_graph( &bucket_id, Some(&op), &function_opgen.ctx().func_map, profiler.instantiation_graph(), &function_opgen.ctx().global.qid_map.borrow(), profile_file_name, ); } else { reporter.report( ¬e_bare(format!( "profile statistics for {}", fun_as_friendly_rust_name(&function.x.name) )) .to_any(), ); self.print_profile_stats( reporter, profiler, &function_opgen.ctx().global.qid_map.borrow(), ); } } Err(err) => { reporter.report_now( &warning_bare(format!( "failed parsing profile file for {}: {}", current_profile_description, err )) .to_any(), ); } } } } else { if command_timed_out && self.args.profile { function_opgen.retry_with_profile( query_op.clone(), commands_with_context_list.clone(), function, func_check_sst.clone(), ); flush_diagnostics_to_report = true; } } } // collect the smt run time from this command into the function duration if commands_with_context_list.len() != 0 { let func_time = self.func_times.entry(bucket_id.clone()).or_insert(HashMap::new()); let func_stats = func_time.entry(function.x.name.clone()).or_insert( FunctionSmtStats { smt_time: Duration::ZERO, rlimit_count: matches!(self.args.solver, SmtSolver::Z3) .then(|| 0), }, ); func_stats.smt_time += func_curr_smt_time; if let Some(rlimit_count) = &mut func_stats.rlimit_count { *rlimit_count += func_curr_smt_rlimit_count .expect("current rlimit count should be present"); } } if matches!(query_op, QueryOp::Body(Style::Normal)) { if (any_invalid && !self.args.no_auto_recommends_check && !any_timed_out) || function.x.attrs.check_recommends { function_opgen.retry_with_recommends(&op, any_invalid)?; } if any_invalid && self.args.expand_errors && default_prover_failed_assert_ids.len() > 0 { function_opgen.start_expand_errors_if_possible( &op, default_prover_failed_assert_ids[0].clone(), ); flush_diagnostics_to_report = true; } } if matches!(query_op, QueryOp::Body(Style::Expanded)) { let res = if any_timed_out { ExpandErrorsResult::Timeout } else if any_invalid { ExpandErrorsResult::Fail } else { ExpandErrorsResult::Pass }; function_opgen.report_expand_error_result(res); } if matches!(query_op, QueryOp::SpecTermination) { if (any_invalid && !self.args.no_auto_recommends_check && !any_timed_out) || function.x.attrs.check_recommends { // Do recommends-checking for the body of the function. // This should always happen for spec(checked). // // Note: this is done as a response to the 'termination check' // because a failed termination check will trigger the // spec body check even if spec(checked) is not marked. // TODO the user probably expects us to also do a recommends-retry // or an expand-errors retry of the decreases-by lemma if // it exists. function_opgen.retry_with_recommends(&op, any_invalid)?; } } } } } } // if spinning off all, the regular profile loop inside has already profiled everything if let (Some(profile_all_file_name), false) = (profile_all_file_name, self.args.spinoff_all) { if air_context.check_valid_used() { match Profiler::parse( message_interface.clone(), &profile_all_file_name, Some(&bucket_id.friendly_name()), reporter, ) { Ok(profiler) => { if self.args.capture_profiles { // if capture profiles was passed, silence the report // as we are only interested in the graph/profile data crate::profiler::write_instantiation_graph( &bucket_id, None, &opgen.ctx.func_map, profiler.instantiation_graph(), &opgen.ctx.global.qid_map.borrow(), profile_all_file_name, ); } else { reporter.report( ¬e_bare(format!( "profile statistics for {}", bucket_id.friendly_name() )) .to_any(), ); self.print_profile_stats( reporter, profiler, &opgen.ctx.global.qid_map.borrow(), ); } } Err(err) => { reporter.report_now( &warning_bare(format!( "failed parsing profile file for {}: {}", bucket_id.friendly_name(), err )) .to_any(), ); } } } } ctx.fun = None; 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 { crate::observers::emit_observer_summaries(obs_cell.borrow().as_any(), reporter); } else if let Some(obs_cell) = &ctx.air_observer { crate::observers::emit_observer_summaries(obs_cell.borrow().as_any(), reporter); } else if let Some(obs_cell) = &ctx.query_result_observer { crate::observers::emit_observer_summaries(obs_cell.borrow().as_any(), reporter); } Ok(VerifyBucketOut { time_smt_init: time_smt_init + spunoff_time_smt_init, time_smt_run: time_smt_run + spunoff_time_smt_run, rlimit_count: rlimit_count.map(|rlimit_count| { let spunoff_rlimit_count = spunoff_rlimit_count.expect("spunoff rlimit count should be present"); (rlimit_count.0 + spunoff_rlimit_count.0, rlimit_count.1 + spunoff_rlimit_count.1) }), }) } fn verify_bucket_outer( &mut self, reporter: &impl Diagnostics, krate: &Krate, bucket_id: &BucketId, mut global_ctx: vir::context::GlobalCtx, ) -> Result { let time_verify_start = Instant::now(); self.bucket_stats.insert(bucket_id.clone(), Default::default()); let bucket_name = bucket_id.friendly_name(); let user_filter = self.user_filter.as_ref().unwrap(); if self.args.trace || !user_filter.is_everything() { let functions_msg = if user_filter.is_function_filter() { " (selected functions)" } else { "" }; reporter .report_now(¬e_bare(format!("verifying {bucket_name}{functions_msg}")).to_any()); } let (pruned_krate, prune_info) = vir::prune::prune_krate_for_module_or_krate( &krate, self.crate_id.as_ref().expect("crate_id"), None, Some(bucket_id.module().clone()), bucket_id.function(), true, true, ); let vir::prune::PruneInfo { mono_abstract_datatypes, spec_fn_types, used_builtins, fndef_types, resolved_typs, dyn_traits, } = prune_info; let mono_abstract_datatypes = mono_abstract_datatypes.unwrap(); let module = pruned_krate .modules .iter() .find(|m| &m.x.path == bucket_id.module()) .expect("module in krate") .clone(); let mut ctx = vir::context::Ctx::new( &pruned_krate, global_ctx, module, mono_abstract_datatypes, spec_fn_types, dyn_traits, used_builtins, fndef_types, resolved_typs.unwrap(), vir::vir_observer::Observers { span_resolver: self.span_resolver.clone(), ..crate::observers::create_observer_from_args(self.args.observer.as_deref()) .expect("observer arguments are checked in verify_crate_inner") }, )?; if self.args.log_all || self.args.log_args.log_vir_poly { let mut file = self.create_log_file(Some(&bucket_id), crate::config::VIR_POLY_FILE_SUFFIX)?; vir::printer::write_krate(&mut file, &pruned_krate, &self.args.log_args.vir_log_option); } let krate_sst = vir::ast_to_sst_crate::ast_to_sst_krate( &mut ctx, reporter, &self.get_bucket(bucket_id).funs, &pruned_krate, )?; if self.args.log_all || self.args.log_args.log_vir_sst { let mut file = self.create_log_file(Some(&bucket_id), crate::config::VIR_SST_FILE_SUFFIX)?; vir::printer::write_krate_sst( &mut file, &krate_sst, &self.args.log_args.vir_log_option, ); } if self.args.no_verify { return Ok(ctx.free()); } let krate_sst = vir::poly::poly_krate_for_module(&mut ctx, &krate_sst); let VerifyBucketOut { time_smt_init, time_smt_run, rlimit_count } = self.verify_bucket(reporter, &krate_sst, bucket_id, &mut ctx)?; global_ctx = ctx.free(); let time_verify_end = Instant::now(); let stats_bucket = self.bucket_stats.get_mut(bucket_id).expect("bucket should exist"); stats_bucket.time_smt_init = time_smt_init; stats_bucket.time_smt_run = time_smt_run; stats_bucket.time_verify = time_verify_end - time_verify_start; stats_bucket.rlimit_count = rlimit_count; if self.args.trace { reporter.report_now( ¬e_bare(format!("done with {:}", bucket_id.friendly_name())).to_any(), ); } Ok(global_ctx) } // Verify one or more modules in a crate fn verify_crate_inner( &mut self, compiler: &Compiler, spans: &SpanContext, ) -> Result<(), VerifyErr> { let time_verify_sequential_start = Instant::now(); let reporter = Reporter::new(spans, compiler); crate::observers::create_observer_from_args(self.args.observer.as_deref()) .map_err(|msg| VerifyErr::Vir(vir::messages::error_bare(msg)))?; if self.args.observer.is_some() { self.span_resolver = Some(crate::spans::span_resolver(spans, compiler.sess.source_map())); } let krate = self.vir_crate.clone().expect("vir_crate should be initialized"); let air_no_span = self.air_no_span.clone().expect("air_no_span should be initialized"); #[cfg(debug_assertions)] vir::check_ast_flavor::check_krate(&krate); let call_graph_log = if self.args.log_all || self.args.log_args.log_call_graph { #[rustfmt::skip] // r to work around attributes being experimental on expressions let r = Some(FuncCallGraphLogFiles { all_initial: self.create_log_file(None, crate::config::CALL_GRAPH_FILE_SUFFIX_FULL_INITIAL)?, all_simplified: self.create_log_file(None, crate::config::CALL_GRAPH_FILE_SUFFIX_FULL_SIMPLIFIED)?, nostd_initial: self.create_log_file(None, crate::config::CALL_GRAPH_FILE_SUFFIX_NOSTD_INITIAL)?, nostd_simplified: self.create_log_file(None, crate::config::CALL_GRAPH_FILE_SUFFIX_NOSTD_SIMPLIFIED)?, }); r } else { None }; let mut global_ctx = vir::context::GlobalCtx::new( &krate, self.crate_id.clone().expect("crate_id"), air_no_span.clone(), self.args.rlimit, Arc::new(std::sync::Mutex::new(None)), Arc::new(std::sync::Mutex::new(call_graph_log)), self.warning_ctx.clone().expect("warning_ctx"), self.args.solver, false, self.args.check_api_safety, self.args.axiom_usage_info, self.args.no_bv_simplify, self.args.report_long_running, )?; vir::recursive_types::check_traits(&krate, &global_ctx)?; let krate = vir::ast_simplify::simplify_krate(&mut global_ctx, &krate)?; if self.args.log_all || self.args.log_args.log_vir_simple { let mut file = self.create_log_file(None, crate::config::VIR_SIMPLE_FILE_SUFFIX)?; vir::printer::write_krate(&mut file, &krate, &self.args.log_args.vir_log_option); } #[cfg(debug_assertions)] vir::check_ast_flavor::check_krate_simplified(&krate); // The 'user_filter' handles the filter provided on the command line // (--verify-module, --verify-function, etc.) // Whereas the 'buckets' are the way we group obligations for parallelizing // and context pruning. // Buckets usually fall along module boundaries, but the user can create // more buckets using #[spinoff_prover]. // // For example, suppose module M has functions a, b, c, d. // with a and b both marked spinoff_prover. // Then we would create buckets {a}, {b}, and {c, d}. // // We don't need to create any buckets for stuff that we don't intend // to verify. However, we can't shrink any existing bucket based on the // the user_filter. // For example, suppose the user includes a filter `--verify-function c`. // Then, we can drop the {a} and {b} buckets. // HOWEVER, we still create the entire {c, d} bucket. // We skip the d-related queries when we get to them; however, we still // include d in the bucket because d influences the context. // Our objective is to generate the same queries for c that we'd otherwise // get if we were running verification on the whole module. // If the user wants to reduce the context used for d, then they can use // the spinoff_prover attribute. let user_filter = self.user_filter.as_ref().unwrap(); let modules_to_verify: Vec = { let current_crate_module_ids = self .current_crate_modules .as_ref() .expect("current_crate_module_ids should be initialized"); user_filter.filter_modules(current_crate_module_ids)? }; let buckets = crate::buckets::get_buckets(&krate, &modules_to_verify); let buckets = user_filter.filter_buckets(buckets); let bucket_ids: Vec = buckets.iter().map(|p| p.0.clone()).collect(); self.buckets = buckets.into_iter().collect(); let time_verify_sequential_end = Instant::now(); self.time_verify_crate_sequential = time_verify_sequential_end - time_verify_sequential_start; let source_map = compiler.sess.source_map(); self.num_threads = if self.args.no_verify { // (at most one per bucket: with no buckets, the worker pool's reporter loop below // would wait for a message no worker sends; --no-verify --build-sst on a crate // without verified functions hung) std::cmp::min(1, bucket_ids.len()) } else { std::cmp::min(self.args.num_threads, bucket_ids.len()) }; if self.args.num_threads != 1 && self.num_threads >= 1 { // create the multiple producers, single consumer queue let (sender, receiver) = std::sync::mpsc::channel(); // collect the buckets and create the task queue let mut tasks = VecDeque::with_capacity(bucket_ids.len()); let mut messages: Vec<(bool, Vec<(Message, MessageLevel)>)> = Vec::new(); for (i, bucket_id) in bucket_ids.iter().enumerate() { // give each bucket its own log file let interpreter_log_file = Arc::new(std::sync::Mutex::new( if self.args.log_all || self.args.log_args.log_interpreter { Some(self.create_log_file( Some(bucket_id), crate::config::INTERPRETER_FILE_SUFFIX, )?) } else { None }, )); // give each task a queued reporter to identify the bucket that is sending messages let reporter = QueuedReporter::new(i, sender.clone()); tasks.push_back(( i, bucket_id.clone(), global_ctx.from_self_with_log(interpreter_log_file), reporter, )); messages.push((false, Vec::new())); } // protect the taskq with a mutex let taskq = std::sync::Arc::new(std::sync::Mutex::new(tasks)); // create the worker threads let mut workers = Vec::new(); let mut workers_finished = Vec::new(); for _tid in 0..self.num_threads { // we create a clone of the verifier here to pass each thread its own local // copy as we modify fields in the verifier struct. later, we merge the results let mut thread_verifier = self.from_self(); let thread_taskq = taskq.clone(); let thread_krate = krate.clone(); // is an Arc let worker_sender = sender.clone(); let worker = std::thread::spawn(move || { let r = std::panic::catch_unwind(|| { let mut completed_tasks: Vec> = Vec::new(); loop { let elm = { let mut tq = thread_taskq.lock().unwrap(); let elm = tq.pop_front(); drop(tq); elm }; if let Some((_i, bucket_id, task, reporter)) = elm { let res = thread_verifier.verify_bucket_outer( &reporter, &thread_krate, &bucket_id, task, ); if let Err(e) = &res { reporter.report_now(&e.clone().to_any()); } reporter.done(); // we've verified the bucket, send the done message completed_tasks.push(res.map_err(|_| ())); } else { break; } } (thread_verifier, completed_tasks) }); match r { Ok(x) => x, Err(e) => { worker_sender .send(ReporterMessage::WorkerPanicked(e)) .expect("mpsc open"); panic!("worker thread panicked"); } } }); workers.push(worker); } let multi_progress = indicatif::MultiProgress::with_draw_target( indicatif::ProgressDrawTarget::stderr_with_hz(1), ); let mut multi_progress_header = None; let mut progress_bars = HashMap::new(); // start handling messages, we keep track of the current active bucket for which we // print messages immediately, while buffering other messages from the other buckets let mut active_bucket = None; let mut num_done = 0; let mut local_msgs: VecDeque = VecDeque::new(); let reporter = Reporter::new(spans, compiler); loop { let msg = match local_msgs.pop_front() { Some(msg) => msg, _ => receiver.recv().expect("receiving message failed"), }; match msg { ReporterMessage::Messages(id, mut msgs, now) => { // The multi-message "Messages" gives us a chance to sort the messages // for clearer diagnostics. // We sort by span here, in rustc's thread, so that we can // legally use from_raw_span for the sorting. msgs.sort_by_key(|(m, _)| { m.spans.get(0).and_then(|s| crate::spans::from_raw_span(&s.raw_span)) }); for (msg, level) in msgs { local_msgs.push_back(ReporterMessage::Message(id, msg, level, now)); } } ReporterMessage::Message(id, msg, level, now) => { if now { // if the message should be reported immediately, do so // this is used for printing notices for long running queries multi_progress.suspend(|| reporter.report_as(&msg.to_any(), level)); continue; } if let Some(m) = active_bucket { // if it's the active bucket, print the message if id == m { multi_progress.suspend(|| reporter.report_as(&msg.to_any(), level)); } else { let msgs = messages.get_mut(id).expect("message id out of range"); msgs.1.push((msg, level)); } } else { // no active bucket, print this message and set the bucket as the // active one active_bucket = Some(id); multi_progress.suspend(|| reporter.report_as(&msg.to_any(), level)); } } ReporterMessage::Done(id) => { // the done message is sent by the thread whenever it is done with verifying // a bucket, we mark the bucket as done here. { // record that the bucket is done let msgs = messages.get_mut(id).expect("message id out of range"); msgs.0 = true; } // if it is the active bucket, mark it as done, and reset the active bucket if let Some(m) = active_bucket { if m == id { assert!( messages .get_mut(id) .expect("message id out of range") .1 .is_empty() ); active_bucket = None; } } // try to pick a new active bucket here, the first one that has any messages if active_bucket.is_none() { for (i, msgs) in messages.iter_mut().enumerate() { if msgs.1.is_empty() { continue; } // drain and print all messages of the bucket for (msg, level) in msgs.1.drain(..) { multi_progress .suspend(|| reporter.report_as(&msg.to_any(), level)); } // if the bucket wasn't done, make it active and handle next message if !msgs.0 { active_bucket = Some(i); break; } } } num_done = num_done + 1; } ReporterMessage::ReportLongRunning(context) => { let CommandContext { fun, span, desc } = &context; let span = from_raw_span(&span.raw_span).expect("valid span"); let span_str = source_map.span_to_diagnostic_string(span); let pid = ProgressBarId(span_str.clone()); if progress_bars.contains_key(&pid) { // we already have a primary progress bar, so this query is either for // error localization or recommends checking let (pb, pb_aux) = progress_bars.remove(&pid).unwrap(); match pb_aux { None => { let pb_aux = multi_progress.insert_from_back( 0, indicatif::ProgressBar::new_spinner() .with_elapsed(Duration::from_millis(2000)), ); pb_aux .enable_steady_tick(std::time::Duration::from_millis(120)); let progress_style = indicatif::ProgressStyle::with_template( "{prefix} {elapsed}\n{msg}", ) .expect("invalid progress style"); pb_aux.set_style(progress_style); pb_aux.set_prefix(format!( "{} {} {} {} {}", console::style("•").red(), span_str, console::style("has been").bold(), console::style("running").bold().red(), console::style("for").bold() )); pb_aux.set_message(format!( " ⌝ {} {} {} {}", desc, console::style("for").bold(), fun_as_friendly_rust_name(&fun), console::style("(auxiliary checks)").bold() )); progress_bars.insert(pid, (pb, Some(pb_aux))); } Some(pb_aux) => { let new_pb_aux = multi_progress.insert_after( &pb_aux, indicatif::ProgressBar::new_spinner() .with_elapsed(pb_aux.elapsed()), ); pb_aux.finish_and_clear(); new_pb_aux .enable_steady_tick(std::time::Duration::from_millis(120)); let progress_style = indicatif::ProgressStyle::with_template( "{prefix} {elapsed}\n{msg}", ) .expect("invalid progress style"); new_pb_aux.set_style(progress_style); new_pb_aux.set_prefix(format!( "{} {} {} {} {}", console::style("•").red(), span_str, console::style("has been").bold(), console::style("running").bold().red(), console::style("for").bold() )); new_pb_aux.set_message(format!( " ⌝ {} {} {} {}", desc, console::style("for").bold(), fun_as_friendly_rust_name(&fun), console::style("(auxiliary checks)").bold() )); progress_bars.insert(pid, (pb, Some(new_pb_aux))); } } } else { if let None = multi_progress_header { let header_pb = multi_progress .insert_from_back(0, indicatif::ProgressBar::new_spinner()); let progress_style = indicatif::ProgressStyle::with_template("{msg}") .expect("invalid progress style"); header_pb.set_style(progress_style); header_pb.set_message(format!( "{}", console::style("Some checks are taking longer than 2s (diagnostics for these may be reported out of order)").bold(), )); header_pb.finish(); multi_progress_header = Some(header_pb); } let pb = multi_progress.insert_from_back( 0, indicatif::ProgressBar::new_spinner() .with_elapsed(Duration::from_millis(2000)), ); pb.enable_steady_tick(std::time::Duration::from_millis(120)); let progress_style = indicatif::ProgressStyle::with_template( "{prefix} {elapsed}\n{msg}", ) .expect("invalid progress style"); pb.set_style(progress_style); let CommandContext { fun, span, desc } = &context; let span = from_raw_span(&span.raw_span).expect("valid span"); let span_str = source_map.span_to_diagnostic_string(span); pb.set_prefix(format!( "{} {} {} {} {}", console::style("•").red(), span_str, console::style("has been").bold(), console::style("running").bold().red(), console::style("for").bold() )); pb.set_message(format!( " ⌝ {} {} {}", desc, console::style("for").bold(), fun_as_friendly_rust_name(&fun) )); progress_bars.insert(pid, (pb, None)); } } ReporterMessage::FinishLongRunning(context) => { let CommandContext { fun, span, desc } = &context; let span = from_raw_span(&span.raw_span).expect("valid span"); let span_str = source_map.span_to_diagnostic_string(span); let pid = ProgressBarId(span_str.clone()); let (pb, pb_aux) = progress_bars.get_mut(&pid).unwrap(); if !pb.is_finished() { pb.set_prefix(format!( "{} {} {} {} {}", console::style("•").blue(), span_str, console::style("has").bold(), console::style("finished").bold().blue(), console::style("in").bold() )); pb.finish_with_message(format!( " ⌝ {} {} {}", desc, console::style("for").bold(), fun_as_friendly_rust_name(&fun) )); } else { let pb_aux = pb_aux.as_ref().unwrap(); pb_aux.set_prefix(format!( "{} {} {} {} {}", console::style("•").blue(), span_str, console::style("has").bold(), console::style("finished").bold().blue(), console::style("in").bold() )); pb_aux.finish_with_message(format!( " ⌝ {} {} {} {}", desc, console::style("for").bold(), fun_as_friendly_rust_name(&fun), console::style("(auxiliary checks)").bold() )); } } ReporterMessage::WorkerPanicked(err) => { std::panic::resume_unwind(err); } } if local_msgs.len() > 0 { continue; } let mut workers_running = Vec::with_capacity(workers.len()); for worker in workers.into_iter() { if worker.is_finished() { match worker.join() { Ok(finished) => workers_finished.push(finished), Err(_) => panic!("worker thread panicked"), } } else { workers_running.push(worker); } } workers = workers_running; if num_done == bucket_ids.len() { break; } } // join with all worker threads, they should all have exited by now. // merge the verifier and global contexts for worker in workers { let res = worker.join().unwrap(); workers_finished.push(res); } let mut worker_emitted_error = false; for (verifier, results) in workers_finished { self.merge(verifier); for res in results { match res { Ok(r) => { global_ctx.merge(r); } Err(()) => { worker_emitted_error = true; } } } } if worker_emitted_error { return Err(VerifyErr::Emitted); } // print remaining messages for msgs in messages.drain(..) { for (msg, level) in msgs.1 { reporter.report_as(&msg.to_any(), level); } } } else { global_ctx.set_interpreter_log_file(Arc::new(std::sync::Mutex::new( if self.args.log_all || self.args.log_args.log_interpreter { Some(self.create_log_file(None, crate::config::INTERPRETER_FILE_SUFFIX)?) } else { None }, ))); for bucket_id in &bucket_ids { global_ctx = self.verify_bucket_outer(&reporter, &krate, bucket_id, global_ctx)?; } } if self.args.no_verify { return Ok(()); } if self.args.profile && self.count_errors == 0 { let msg = note_bare( "`--profile` reports prover performance data only when rlimits are exceeded, use `--profile-all` to always report profiler results", ); reporter.report(&msg.to_any()); } // Log/display triggers if self.args.log_all || self.args.log_args.log_triggers { let mut file = self.create_log_file(None, crate::config::TRIGGERS_FILE_SUFFIX)?; let chosen_triggers = global_ctx.get_chosen_triggers(); for triggers in chosen_triggers { writeln!(file, "{:#?}", triggers).expect("error writing to trigger log file"); } } let chosen_triggers = global_ctx.get_chosen_triggers(); let mut low_confidence_triggers = None; for chosen in chosen_triggers { match ( self.args.show_triggers, modules_to_verify.iter().find(|m| &m.x.path == &chosen.module).is_some(), chosen.manual, ) { (ShowTriggers::Selective, true, false) if chosen.low_confidence => { report_chosen_triggers(&reporter, &chosen, true); low_confidence_triggers = Some(chosen.span); } (ShowTriggers::Module, true, false) => { report_chosen_triggers(&reporter, &chosen, true); } (ShowTriggers::AllModules, _, false) => { report_chosen_triggers(&reporter, &chosen, true); } (ShowTriggers::Verbose, true, _) => { report_chosen_triggers(&reporter, &chosen, !chosen.manual); } (ShowTriggers::VerboseAllModules, _, _) => { report_chosen_triggers(&reporter, &chosen, !chosen.manual); } ( ShowTriggers::Selective | ShowTriggers::Module | ShowTriggers::AllModules | ShowTriggers::Silent | ShowTriggers::Verbose, _, _, ) => {} } } if let Some(span) = low_confidence_triggers { let msg = "Verus printed one or more automatically chosen quantifier triggers\n\ because it had low confidence in the chosen triggers.\n\ To suppress these messages, do one of the following:\n \ (1) manually annotate a single desired trigger using `#[trigger]`\n \ (example: `forall|i: int, j: int| f(i) && #[trigger] g(i) && #[trigger] h(j)`),\n \ (2) manually annotate multiple desired triggers using `#![trigger ...]`\n \ (example: `forall|i: int| #![trigger f(i)] #![trigger g(i)] f(i) && g(i)`),\n \ (3) accept the automatically chosen trigger using `#![auto]`\n \ (example: `forall|i: int, j: int| #![auto] f(i) && g(i) && h(j)`)\n \ (4) use the `--triggers-mode silent` command-line option to suppress all printing of triggers.\n\ (Note: triggers are used by the underlying SMT theorem prover to instantiate quantifiers;\n\ the theorem prover instantiates a quantifier whenever some expression matches the\n\ pattern specified by one of the quantifier's triggers.)\ "; reporter.report(¬e(&span, msg).to_any()); } Ok(()) } pub(crate) fn verify_crate<'tcx>( &mut self, compiler: &Compiler, spans: &SpanContext, ) -> Result<(), VerifyErr> { // Verify crate let time_verify_crate_start = Instant::now(); let result = if !self.args.no_verify || self.args.build_sst { self.verify_crate_inner(&compiler, spans) } else { Ok(()) }; let time_verify_crate_end = Instant::now(); self.time_verify_crate = time_verify_crate_end - time_verify_crate_start; result } fn construct_vir_crate<'tcx>( &mut self, tcx: TyCtxt<'tcx>, verus_items: Arc, spans: &SpanContext, other_vir_crates: Vec, diagnostics: &impl air::messages::Diagnostics, ) -> Result, Vec, Option)> { if self.args.no_lifetime { rustc_mir_build_verus::verus::set_verus_aware_def_ids(Arc::new(HashSet::new())); } self.air_no_span = { let crate_owner = tcx.lower_to_hir(rustc_span::def_id::CRATE_DEF_ID); let no_span = { let owner_info = crate_owner.as_owner().expect("OwnerNode::Crate missing"); let OwnerNode::Crate(c) = owner_info.node() else { panic!("OwnerNode::Crate missing"); }; c.spans.inner_span }; Some(vir::messages::Span { raw_span: crate::spans::to_raw_span(no_span), id: 0, data: vec![], as_string: "no location".to_string(), }) }; let mut crate_ids: HashSet = HashSet::new(); for c in tcx.crates(()) { let id = mk_crate_id(tcx, *c); if crate_ids.contains(&id) { // Cannot currently handle multiple `core` or `alloc` or `vstd` crates let err = vir::messages::error( &self.air_no_span.as_ref().unwrap(), format!("cannot handle more than one crate named `{}`", tcx.crate_name(*c)), ); return Err((vec![err], vec![], None)); } crate_ids.insert(id); } if !verus_items.name_to_id.contains_key(&VerusItem::ErasedGhostValue) { let err = crate::util::no_builtin_err(self.air_no_span.as_ref().unwrap()); return Err((vec![err], vec![], None)); } let ctxtx = ContextX::new( self.args.clone(), tcx, spans.clone(), verus_items, self.args.vstd == crate::config::Vstd::NoVstd, self.crate_id.clone().expect("crate_id"), ); let ctxt_diagnostics = ctxtx.diagnostics.clone(); let map_err_diagnostics = |err: VirErr| (vec![err], ctxt_diagnostics.borrow_mut().drain(..).collect(), None); let map_errs_diagnostics = |errs: Vec| (errs, ctxt_diagnostics.borrow_mut().drain(..).collect(), None); let map_query_err = |err: QueryError| { (vec![], ctxt_diagnostics.borrow_mut().drain(..).collect(), Some(err)) }; let map_errors_query_diagnostics = |(es, err)| (es, ctxt_diagnostics.borrow_mut().drain(..).collect(), err); let crate_items = crate::external::get_crate_items(&ctxtx).map_err(map_errs_diagnostics)?; check_no_opaque_types_in_trait(ctxtx.tcx, &crate_items).map_err(map_err_diagnostics)?; let verus_aware_ids = if !self.args.no_lifetime { Some(crate::erase::setup_verus_aware_ids(&crate_items)) } else { None }; let time_hir0 = Instant::now(); let time_hir1 = Instant::now(); self.time_hir = time_hir1 - time_hir0; let time0 = Instant::now(); let pre_crate = crate::rust_to_vir::crate_to_vir(ctxtx, &other_vir_crates, &crate_items) .map_err(map_errors_query_diagnostics)?; if !self.args.no_lifetime { crate::erase::check_verus_aware_ids( tcx, self.air_no_span.as_ref().unwrap(), verus_aware_ids.unwrap(), &pre_crate.def_id_to_fun_name_for_erasure, ) .map_err(map_err_diagnostics)?; } let time1 = Instant::now(); self.current_crate_modules = Some(pre_crate.krate_without_funs.modules.clone()); self.crate_items = Some(Arc::new(crate_items)); let ctxt = pre_crate.ctxt.clone(); ctxt.flush_diagnostics(diagnostics); let query = Rc::new(Query::new( self.args.clone(), Box::new(Reporter::new_from_tcx(spans, tcx)), self.func_details.clone(), self.deferred_errors.clone(), other_vir_crates, pre_crate, self.crate_id.clone().unwrap(), )); set_global_query(query.clone()); rustc_hir_analysis_verus::check_crate(tcx); if tcx.dcx().err_count() != 0 { return Ok(false); } // Export crate if requested. let local_crate = query.get_exportable_crate().map_err(map_query_err)?; let time2 = Instant::now(); let crate_metadata = crate::import_export::CrateMetadata { crate_id: spans.local_crate.as_u64(), original_files: spans.local_files.clone(), }; crate::import_export::export_crate( &self.args, &self.export_vir_path_via_cargo, crate_metadata, local_crate.clone(), ) .map_err(map_err_diagnostics)?; let merged_crate = query.get_merged_crate().map_err(map_query_err)?; self.maybe_log_impl_names(&merged_crate).map_err(map_err_diagnostics)?; self.maybe_log_vir_crate(&merged_crate).map_err(map_err_diagnostics)?; let user_filter = UserFilter::from_args(&self.args, &local_crate).map_err(map_err_diagnostics)?; self.user_filter = Some(user_filter); if self.args.check_api_safety { vir::safe_api::check_safe_api(&merged_crate).map_err(map_err_diagnostics)?; } self.vir_crate = Some(merged_crate.clone()); self.warning_ctx = Some(query.get_updated_warning_ctx().map_err(map_query_err)?); /*if !self.args.no_lifetime { let functions = query.get_all_function_stubs().map_err(map_query_err)?; let datatypes = query.get_datatypes_map().map_err(map_query_err)?; let erasure_modes = query.get_erasure_modes().map_err(map_query_err)?; crate::erase::setup_verus_ctxt_for_thir_erasure( tcx, &self.verus_items.as_ref().unwrap(), &datatypes, &functions, &ctxt.erasure_info.borrow(), &erasure_modes, ) .map_err(map_err_diagnostics)?; }*/ // These can invoke mir_borrowck when opaque types are involved. // Thus, we can only run these after calling `setup_verus_ctxt_for_thir_erasure` tcx.hir_for_each_module(|module| { tcx.ensure_ok().check_private_in_public(module); tcx.ensure_ok().check_mod_privacy(module); }); let time5 = Instant::now(); self.time_vir = time5 - time0; self.time_vir_rust_to_vir = time2 - time1; Ok(true) } pub fn get_function_mode(&self, f: &Fun) -> Option<&vir::ast::Mode> { self.vir_crate.as_ref().and_then(|vir_krate| { vir_krate .functions .iter() .find(|function| function.x.name == *f) .map(|function| &function.x.mode) }) } fn record_func_obligation_proof_notes( &mut self, func: Fun, obligation_proof_notes: HashSet, ) { use std::collections::hash_map::Entry; let mut func_details = self.func_details.lock().unwrap(); match func_details.entry(func) { Entry::Occupied(mut occupied_entry) => { occupied_entry.get_mut().obligation_proof_notes.extend(obligation_proof_notes); } Entry::Vacant(vacant_entry) => { let _ = vacant_entry.insert(FuncDetails { obligation_proof_notes: obligation_proof_notes, ..Default::default() }); } } } fn record_func_failed_proof_notes(&mut self, func: Fun, failed_proof_notes: HashSet) { use std::collections::hash_map::Entry; let mut func_details = self.func_details.lock().unwrap(); match func_details.entry(func) { Entry::Occupied(mut occupied_entry) => { occupied_entry.get_mut().failed_proof_notes.extend(failed_proof_notes); } Entry::Vacant(vacant_entry) => { let _ = vacant_entry.insert(FuncDetails { failed_proof_notes: failed_proof_notes, ..Default::default() }); } } } fn maybe_log_impl_names(&mut self, krate: &Krate) -> Result<(), VirErr> { if self.args.log_all || self.args.log_args.log_impl_names { let mut file = self.create_log_file(None, crate::config::IMPL_NAMES_SUFFIX)?; for imp in &krate.trait_impls { let ts: Vec = imp.x.trait_typ_args.iter().map(vir::ast_util::typ_to_diagnostic_str).collect(); writeln!( &mut file, "{} ### {} ### {} ### {}", vir::ast_util::path_as_friendly_rust_name(&imp.x.impl_path), vir::ast_util::path_as_friendly_rust_name(&imp.x.trait_path), ts.join(", "), imp.span.as_string, ) .map_err(|e| io_vir_err("log_impl_names".to_string(), e))?; } } Ok(()) } fn maybe_log_vir_crate(&mut self, krate: &Krate) -> Result<(), VirErr> { if self.args.log_all || self.args.log_args.log_vir { let mut file = self.create_log_file(None, crate::config::VIR_FILE_SUFFIX)?; vir::printer::write_krate(&mut file, krate, &self.args.log_args.vir_log_option); } Ok(()) } } fn delete_dir_if_exists_and_is_dir(dir: &std::path::PathBuf) -> Result<(), VirErr> { Ok(if dir.exists() { if dir.is_dir() { let entries = std::fs::read_dir(dir).map_err(|err| { io_vir_err(format!("could not read directory {}", dir.display()), err) })?; for entry in entries.flatten() { if entry.path().is_file() { std::fs::remove_file(entry.path()).map_err(|err| { io_vir_err(format!("could not remove file {}", entry.path().display()), err) })?; } } } else { return Err(error(format!("{} exists and is not a directory", dir.display()))); } }) } /// Currently performing an rustc_hir_analysis::check_crate() with trait methods with opaque return types /// will cause the thir_body to run before VerusErasureCtxt is initialized. /// We disallow opaque types in trait for now. fn check_no_opaque_types_in_trait<'tcx>( tcx: TyCtxt<'tcx>, crate_items: &crate::external::CrateItems, ) -> Result<(), VirErr> { for item in crate_items.items.iter() { if matches!(item.verif, VerifOrExternal::External { .. }) { continue; } match item.id { crate::external::GeneralItemId::TraitItemId(trait_item_id) => { match tcx.hir_trait_item(trait_item_id).kind { rustc_hir::TraitItemKind::Fn(sig, _) => { if let rustc_hir::FnRetTy::Return(ty) = sig.decl.output { if matches!(ty.kind, rustc_hir::TyKind::OpaqueDef { .. }) { crate::unsupported_err!( ty.span, "`impl Trait` types in trait definitions" ); } } } _ => {} } } _ => {} } } Ok(()) } // TODO: move the callbacks into a different file, like driver.rs pub(crate) struct VerifierCallbacksEraseMacro { pub(crate) verifier: Verifier, /// start time of the rustc compilation pub(crate) rust_start_time: Instant, /// time when entered the `after_expansion` callback pub(crate) rust_end_time: Option, /// start time of lifetime analysys pub(crate) tc_start_time: Option, /// end time of lifetime analysys pub(crate) tc_end_time: Option, pub(crate) verus_externs: Option, pub(crate) spans: Option, /// import-dep-if-present names that did not match any direct `--extern`; /// resolved against rustc's loaded transitive crates in `after_expansion`. pub(crate) unresolved_import_deps: HashSet, } pub(crate) static BODY_HIR_ID_TO_REVEAL_PATH_RES: std::sync::RwLock< Option< HashMap< rustc_span::def_id::DefId, (Option, crate::hir_hide_reveal_rewrite::ResOrSymbol), >, >, > = std::sync::RwLock::new(None); fn lower_to_hir<'tcx>( tcx: TyCtxt<'tcx>, def_id: rustc_hir::def_id::LocalDefId, ) -> rustc_hir::MaybeOwner<'tcx> { let owner = (rustc_interface::DEFAULT_QUERY_PROVIDERS.queries.lower_to_hir)(tcx, def_id); crate::hir_hide_reveal_rewrite::hir_hide_reveal_rewrite(owner, tcx) } impl rustc_driver::Callbacks for VerifierCallbacksEraseMacro { fn config(&mut self, config: &mut rustc_interface::interface::Config) { if let Some(mut dep_tracker) = self.verifier.dep_tracker.take() { let import_dep_if_present = &self .verifier .via_cargo_args .as_ref() .expect("dep_tracker is present, so via_cargo_args must be Some") .import_dep_if_present; let mut import_deps_if_present: HashSet = import_dep_if_present.iter().cloned().collect(); let success = crate::cargo_verus::handle_externs( &config.opts.externs, &mut import_deps_if_present, &mut dep_tracker, ); match success { Ok(imports) => { self.verifier.import_virs_via_cargo = Some(imports); } Err(err) => { eprintln!("error: {}", err); std::process::exit(1); } } self.unresolved_import_deps = import_deps_if_present; dep_tracker.config_install(config); } if self.verifier.args.no_lifetime { config.override_queries = Some(|_session, providers| { providers.queries.lower_to_hir = lower_to_hir; providers.queries.mir_const_qualif = |_, _| rustc_middle::mir::ConstQualifs::default(); providers.queries.lint_mod = |_, _| {}; providers.queries.check_liveness = |_, _| DenseBitSet::new_empty(0); providers.queries.check_mod_deathness = |_, _| {}; rustc_hir_analysis_verus::provide(&mut providers.queries); providers.queries.mir_borrowck = |tcx, _local_def_id| Ok(tcx.arena.alloc(Default::default())); providers.queries.type_of_opaque = |tcx, def_id| { let ty = (rustc_interface::DEFAULT_QUERY_PROVIDERS.queries.type_of_opaque)( tcx, def_id, ); ty.map_bound(|ty| { crate::rust_to_vir_base::hack_fix_no_lifetime_opaque_ty_issue2541(tcx, ty) }) }; }); } else { config.override_queries = Some(|_session, providers| { providers.queries.lower_to_hir = lower_to_hir; providers.queries.mir_const_qualif = |_, _| rustc_middle::mir::ConstQualifs::default(); providers.queries.lint_mod = |_, _| {}; providers.queries.check_liveness = |_, _| DenseBitSet::new_empty(0); providers.queries.check_mod_deathness = |_, _| {}; rustc_hir_analysis_verus::provide(&mut providers.queries); rustc_mir_build_verus::verus_provide(providers); providers.queries.mir_built = |tcx, def| { // We need to override this to call our verus of build_mir. // mir_built is defined in the crate rustc_mir_transform, which I prefer // not to fork. The actual implementation of mir_built is more complicated // than this, but this seems to be the essential functionality. let body = rustc_mir_build_verus::builder::build_mir_inner_impl(tcx, def); //let pass = rustc_mir_transform::simplify::SimplifyCfg::Initial; //pass.run_pass(tcx, &mut body); tcx.alloc_steal_mir(body) }; }); } } fn after_expansion<'tcx>( &mut self, compiler: &Compiler, tcx: TyCtxt<'tcx>, ) -> rustc_driver::Compilation { self.rust_end_time = Some(Instant::now()); if let Some(_guar) = compiler.sess.dcx().has_errors() { self.verifier.encountered_error = true; return rustc_driver::Compilation::Stop; } self.verifier.error_format = Some(compiler.sess.opts.error_format); if self.verifier.via_cargo_args.is_some() { let crate_meta_path = tcx.output_filenames(()).path(rustc_session::config::OutputType::Metadata); if let rustc_session::config::OutFileName::Real(path) = crate_meta_path { self.verifier.export_vir_path_via_cargo = Some(path.with_extension("vir")); } } let mut import_virs_via_cargo = self.verifier.import_virs_via_cargo.clone().unwrap_or_default(); if !self.unresolved_import_deps.is_empty() { // Resolve transitive .vir imports before `write_dep_info` so each // resolved .vir gets registered in `psess.file_depinfo` and ends // up in the consumer's `.d` file, mirroring `dep_tracker.mark_file` // for direct externs. match crate::cargo_verus::handle_transitive_imports(tcx, &self.unresolved_import_deps) { Ok(extra) => import_virs_via_cargo.extend(extra), Err(err) => { eprintln!("error: {}", err); std::process::exit(1); } } } rustc_interface::passes::write_dep_info(tcx); self.verifier.crate_id = Some(mk_crate_id(tcx, LOCAL_CRATE)); let time_import0 = Instant::now(); let imported = match crate::import_export::import_crates(&self.verifier.args, import_virs_via_cargo) { Ok(imported) => imported, Err(err) => { assert!(err.spans.len() == 0); assert!(err.level == MessageLevel::Error); compiler.sess.dcx().err(err.note.clone()); self.verifier.encountered_vir_error = true; return rustc_driver::Compilation::Stop; } }; let time_import1 = Instant::now(); self.verifier.time_import = time_import1 - time_import0; let verus_items = Arc::new(crate::verus_items::from_diagnostic_items(tcx)); self.verifier.verus_items = Some(verus_items.clone()); let spans = SpanContextX::new( tcx, tcx.stable_crate_id(LOCAL_CRATE), compiler.sess.source_map(), imported.metadatas.into_iter().map(|c| (c.crate_id, c.original_files)).collect(), self.verus_externs.as_ref(), ); { let reporter = Reporter::new(&spans, compiler); if self.verifier.args.trace { reporter.report_now(¬e_bare("preparing crate for verification").to_any()); } if let Err((errs, mut diagnostics, query_err)) = self.verifier.construct_vir_crate( tcx, verus_items.clone(), &spans, imported.vir_crates, &reporter, ) { assert!(errs.len() > 0 || query_err.is_some()); for err in errs.into_iter() { reporter.report_as(&err.to_any(), MessageLevel::Error); } self.verifier.encountered_vir_error = true; for diag in diagnostics.drain(..) { match diag { vir::ast::VirErrAs::Warning(err) => { reporter.report_as(&err.to_any(), MessageLevel::Warning) } vir::ast::VirErrAs::Note(err) => { reporter.report_as(&err.to_any(), MessageLevel::Note) } } } return rustc_driver::Compilation::Stop; } if let Some(_guar) = compiler.sess.dcx().has_errors() { self.verifier.encountered_error = true; return rustc_driver::Compilation::Stop; } self.tc_start_time = Some(Instant::now()); let status = if self.verifier.args.no_trait_conflicts { Ok(vec![]) } else { let log_trait_conflicts = self.verifier.args.log_all || self.verifier.args.log_args.log_trait_conflicts; let tc_log_file = if log_trait_conflicts { let file = self .verifier .create_log_file(None, crate::config::TRAIT_CONFLICT_FILE_SUFFIX); match file { Err(err) => { reporter.report_as(&err.to_any(), MessageLevel::Error); self.verifier.encountered_vir_error = true; return rustc_driver::Compilation::Stop; } Ok(file) => Some(file), } } else { None }; crate::trait_check::check_trait_conflicts( &spans, self.verifier.vir_crate.as_ref().expect("vir_crate should be initialized"), tc_log_file, ) }; self.tc_end_time = Some(Instant::now()); match status { Ok(msgs) => { if msgs.len() > 0 { self.verifier.encountered_vir_error = true; for msg in &msgs { reporter.report(&msg.clone().to_any()); } reporter.report( ¬e_bare("this error was found in Verus's trait-conflict checker") .to_any(), ); return rustc_driver::Compilation::Stop; } } Err(err) => { reporter.report_as(&err.to_any(), MessageLevel::Error); self.verifier.encountered_vir_error = true; return rustc_driver::Compilation::Stop; } } } if let Some(_guar) = compiler.sess.dcx().has_errors() { return rustc_driver::Compilation::Stop; } if !self.verifier.args.no_lifetime { self.run_lifetime_checks_on_verus_aware_items(tcx); } if let Some(_guar) = compiler.sess.dcx().has_errors() { return rustc_driver::Compilation::Stop; } self.spans = Some(spans); self.finish_verus(compiler); rustc_driver::Compilation::Stop } fn after_analysis<'tcx>( &mut self, _compiler: &Compiler, _tcx: TyCtxt<'tcx>, ) -> rustc_driver::Compilation { rustc_driver::Compilation::Stop } } impl VerifierCallbacksEraseMacro { fn run_lifetime_checks_on_verus_aware_items<'tcx>(&mut self, tcx: TyCtxt<'tcx>) { let crate_items = self.verifier.crate_items.as_ref().unwrap().clone(); tcx.par_hir_body_owners(|def_id| { if matches!(tcx.def_kind(def_id), DefKind::OpaqueTy | DefKind::Impl { of_trait: true }) { let _ = rustc_hir_analysis_verus::check::check::check_item_type_inner( tcx, def_id, true, ); } if !tcx.is_typeck_child(def_id.to_def_id()) { let owner_id = rustc_hir::OwnerId { def_id: def_id }; let crate_item = crate_items.map.get(&owner_id); match &crate_item { Some(VerifOrExternal::VerusAware { module_path: _, const_directive: false, external_body: false, external_fn_specification: false, }) => { tcx.ensure_ok().mir_borrowck(def_id); } Some(VerifOrExternal::VerusAware { .. }) | Some(VerifOrExternal::External { .. }) | None => {} } } }); } fn finish_verus(&mut self, compiler: &Compiler) { let spans = self.spans.clone().unwrap(); let reporter = Reporter::new(&spans, compiler); match self.verifier.verify_crate(compiler, &spans) { Ok(()) => {} Err(err) => { if let VerifyErr::Vir(err) = err { reporter.report_as(&err.to_any(), MessageLevel::Error); } self.verifier.encountered_vir_error = true; } } for err in std::mem::take(&mut *self.verifier.deferred_errors.lock().unwrap()) { reporter.report_as(&err.to_any(), MessageLevel::Error); self.verifier.encountered_vir_error = true; } if !self.verifier.args.output_json && !self.verifier.args.no_verify && !self.verifier.encountered_error && !self.verifier.encountered_vir_error { println!( "verification results:: {} verified, {} errors{}", self.verifier.count_verified, self.verifier.count_errors, if !crate::driver::is_verifying_entire_crate(&self.verifier) { " (partial verification with `--verify-*`)" } else { "" } ); } } }