Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370use crate::{erase::ResolvedCall, verus_items::VerusItems};use air::messages::MessageLevel;use rustc_hir::Attribute;use rustc_hir::HirId;use rustc_hir::def_id::LocalDefId;use rustc_middle::ty::{TyCtxt, TypeckResults};use rustc_mir_build_verus::verus::BodyErasure;use rustc_span::SpanData;use rustc_span::def_id::DefId;use std::cell::RefCell;use std::collections::HashMap;use std::ops::DerefMut;use std::rc::Rc;use std::sync::Arc;use std::sync::atomic::AtomicU64;use std::sync::mpsc::Sender;use vir::ast::{CrateId, Mode, Path, Pattern, VirErr};use vir::messages::{AstId, ToAny, WarningAllow};
#[derive(Clone)]pub struct ErasureInfo { /// Connect every PlaceX::Local, ExprX::Var, and ExprX::VarAt node to its /// HirId (an ExprKind::Path node that resolves to Local). /// /// Use None if there is no corresponding source node, e.g., from synthetically produced /// expressions. pub(crate) local_hir_vir_ids: Vec<(Option<HirId>, AstId)>, /// Connect every VIR Pattern binder onto its HirId (a PatKind::Binder) pub(crate) binder_hir_vir_ids: Vec<(Option<HirId>, AstId)>, /// Connect every non-tuple VIR Ctor onto its HirId (either a ExprKind::Struct, or a /// const-style constructor or call-style constructor). pub(crate) ctor_hir_vir_ids: Vec<(Option<HirId>, AstId)>, /// Details of each call in the first run's HIR. /// The last bool is "in ghost block?". /// (This is false for "boundary" calls like Ghost/Tracked /// though that shouldn't matter right now). pub(crate) resolved_calls: Vec<(HirId, SpanData, ResolvedCall, bool)>, /// Details of some patterns in first run's HIR pub(crate) resolved_pats: Vec<(SpanData, Pattern)>, /// Modes specified directly during rust_to_vir pub(crate) direct_var_modes: Vec<(HirId, Mode)>, pub(crate) bodies: Vec<(LocalDefId, BodyErasure)>, pub(crate) shadow_check: Vec<HirId>, /// Extra nodes to erase, use this when a VIR tree gets dropped without getting to /// mode-checking. pub(crate) extra_erase_ast_ids: Vec<vir::messages::Span>, pub(crate) local_invariant_bodies: Vec<rustc_mir_build_verus::verus::LocalInvariantBody>,}
type ErasureInfoRef = std::rc::Rc<std::cell::RefCell<ErasureInfo>>;
pub type Context<'tcx> = Rc<ContextX<'tcx>>;pub struct ContextX<'tcx> { pub(crate) cmd_line_args: crate::config::Args, pub(crate) tcx: TyCtxt<'tcx>, pub(crate) spans: crate::spans::SpanContext, pub(crate) verus_items: Arc<VerusItems>, pub(crate) diagnostics: Rc<PendingDiagnostics>, pub(crate) no_vstd: bool, pub(crate) arch_word_bits: Option<vir::ast::ArchWordBits>, pub(crate) crate_name: CrateId, pub(crate) name_def_id_map: Rc<RefCell<HashMap<Path, DefId>>>, pub(crate) next_read_kind_id: AtomicU64,}
/// Warnings and notes collected while translating HIR to VIR, waiting to be reported./// Dropping it with diagnostics still pending means a flush was forgotten.pub(crate) struct PendingDiagnostics(RefCell<Vec<vir::ast::VirErrAs>>);
impl PendingDiagnostics { fn flush(&self, reporter: &dyn air::messages::Diagnostics) { for diag in self.0.borrow_mut().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) } } } }}
impl std::ops::Deref for PendingDiagnostics { type Target = RefCell<Vec<vir::ast::VirErrAs>>;
fn deref(&self) -> &Self::Target { &self.0 }}
impl Drop for PendingDiagnostics { fn drop(&mut self) { debug_assert!( std::thread::panicking() || self.0.get_mut().is_empty(), "diagnostics were never reported; use flush_diagnostics or flush_diagnostics_on_drop" ); }}
pub(crate) struct FlushDiagnosticsOnDrop<'r> { diagnostics: Rc<PendingDiagnostics>, reporter: &'r dyn air::messages::Diagnostics,}
impl Drop for FlushDiagnosticsOnDrop<'_> { fn drop(&mut self) { // Reporting while unwinding could panic again and abort if !std::thread::panicking() { self.diagnostics.flush(self.reporter); } }}
/// The context in which a given header node might be interpretted#[derive(Clone, Copy, PartialEq, Eq)]pub enum HeaderSetting { /// Fn signature headers (requires, ensures, unwind, mask, decreases) /// Including closures Fn, /// Loops (invariants, ensures, etc.) Loop(HirId), /// Requires or ensures on an assert-by, assert-by-nonlinear, assert-by-forall etc. Assert,}
#[derive(Clone)]pub(crate) struct BodyCtxt<'tcx> { pub(crate) ctxt: Context<'tcx>, pub(crate) types: &'tcx TypeckResults<'tcx>, pub(crate) fun_id: DefId, pub(crate) external_trait_from_to: Option<Arc<(Path, Path, Option<Path>)>>, pub(crate) mode: Mode, pub(crate) external_body: bool, pub(crate) in_ghost: bool, pub(crate) atomically: Option<Arc<AtomicallyCtxt>>, pub(crate) migrate_postcondition_vars: Option<std::collections::HashSet<vir::ast::VarIdent>>, /// Context to interpret a header if we encounter one /// (this is used to determine when it's correct to set `in_fn_sig`). pub(crate) header_setting: HeaderSetting, /// Are we in the signature of a function or closure? pub(crate) in_fn_sig: bool, /// Are we in a postcondition of a function or closure? (implies in_fn_sig) pub(crate) in_postcondition: bool, /// Are we inside an "old" node? (new-mut-ref only) pub(crate) in_old: bool, /// Are we inside an "after_borrow" or "has_resolved" node? (new-mut-ref only) pub(crate) in_explicit_prophecy_node: bool, /// params for the enclosing function and all enclosing non-spec-closures pub(crate) params: Rc<Vec<Vec<vir::ast::VarIdent>>>, /// Assume specification defines a new opaque type for each opaque type in the external function. /// We use this map to resolve them later. pub(crate) external_opaque_type_map: Option<HashMap<Path, Path>>, /// Mapping for HirId found in an HIR Destination to the corresponding VIR Label. pub(crate) label_map: Rc<RefCell<(HashMap<HirId, vir::ast::Label>, usize)>>, pub(crate) erasure_info: ErasureInfoRef,}
pub(crate) struct AtomicallyCtxt { pub(crate) update_binder: HirId, pub(crate) call_spans: Sender<vir::messages::Span>,}
impl<'tcx> ContextX<'tcx> { pub(crate) fn new( cmd_line_args: crate::config::Args, tcx: TyCtxt<'tcx>, spans: crate::spans::SpanContext, verus_items: Arc<VerusItems>, no_vstd: bool, crate_name: CrateId, ) -> Self { ContextX { cmd_line_args, tcx, spans, verus_items, diagnostics: Rc::new(PendingDiagnostics(RefCell::new(Vec::new()))), no_vstd, arch_word_bits: None, crate_name, name_def_id_map: Rc::new(RefCell::new(HashMap::new())), next_read_kind_id: AtomicU64::new(0), } }
pub(crate) fn flush_diagnostics(&self, reporter: &dyn air::messages::Diagnostics) { self.diagnostics.flush(reporter); }
/// Returns a guard that reports the pending diagnostics when it is dropped, /// so they are reported on every exit path, including early returns pub(crate) fn flush_diagnostics_on_drop<'r>( &self, reporter: &'r dyn air::messages::Diagnostics, ) -> FlushDiagnosticsOnDrop<'r> { FlushDiagnosticsOnDrop { diagnostics: self.diagnostics.clone(), reporter } }
pub(crate) fn get_verus_item(&self, def_id: DefId) -> Option<&crate::verus_items::VerusItem> { self.verus_items.id_to_name.get(&def_id) }
pub(crate) fn get_verifier_attrs( &self, attrs: &[Attribute], ) -> Result<crate::attributes::VerifierAttrs, VirErr> { crate::attributes::get_verifier_attrs(attrs, Some(&mut *self.diagnostics.borrow_mut())) }
pub(crate) fn get_verifier_attrs_no_check( &self, attrs: &[Attribute], ) -> Result<crate::attributes::VerifierAttrs, VirErr> { crate::attributes::get_verifier_attrs_no_check( attrs, Some(&mut *self.diagnostics.borrow_mut()), ) }
pub(crate) fn get_external_attrs( &self, attrs: &[Attribute], ) -> Result<crate::attributes::ExternalAttrs, VirErr> { crate::attributes::get_external_attrs(attrs, Some(&mut *self.diagnostics.borrow_mut())) }
pub(crate) fn path_def_id_ref( &self, ) -> Option<impl DerefMut<Target = HashMap<Path, DefId>> + use<'_>> { self.name_def_id_map.try_borrow_mut().ok() }
pub(crate) fn def_id_to_vir_path(&self, def_id: DefId) -> Path { crate::rust_to_vir_base::def_id_to_vir_path( self.tcx, &self.verus_items, def_id, self.path_def_id_ref(), ) }
pub(crate) fn mid_ty_to_vir( &self, param_env_src: DefId, span: rustc_span::Span, ty: &rustc_middle::ty::Ty<'tcx>, assume_specification_opaque_type_map: Option<&HashMap<Path, Path>>, ) -> Result<vir::ast::Typ, VirErr> { crate::rust_to_vir_base::mid_ty_to_vir( self.tcx, &self.verus_items, self.path_def_id_ref(), param_env_src, span, ty, assume_specification_opaque_type_map, ) }
pub(crate) fn unique_read_kind_id(&self) -> u64 { self.next_read_kind_id.fetch_add(1, std::sync::atomic::Ordering::SeqCst) }}
impl<'tcx> BodyCtxt<'tcx> { pub(crate) fn is_copy(&self, ty: rustc_middle::ty::Ty<'tcx>) -> bool { let typing_env = rustc_middle::ty::TypingEnv::new( self.ctxt.tcx.param_env(self.fun_id), rustc_middle::ty::TypingMode::non_body_analysis(), ); self.ctxt.tcx.type_is_copy_modulo_regions(typing_env, ty) }
pub(crate) fn mid_ty_to_vir( &self, span: rustc_span::Span, ty: &rustc_middle::ty::Ty<'tcx>, ) -> Result<vir::ast::Typ, VirErr> { self.ctxt.mid_ty_to_vir(self.fun_id, span, ty, self.external_opaque_type_map.as_ref()) } pub(crate) fn is_param_migrated(&self, ident: &vir::ast::VarIdent) -> bool { let Some(vars) = &self.migrate_postcondition_vars else { return false; }; vars.contains(ident) }
pub(crate) fn is_param_for_fn_or_non_spec_closure(&self, ident: &vir::ast::VarIdent) -> bool { self.params.iter().any(|params| params.iter().any(|param| param == ident)) }
pub(crate) fn is_param_for_innermost_fn_or_non_spec_closure( &self, ident: &vir::ast::VarIdent, ) -> bool { self.params.last().unwrap().iter().any(|param| param == ident) }
pub(crate) fn set_header_setting(&self, s: HeaderSetting) -> BodyCtxt<'tcx> { BodyCtxt { header_setting: s, ..self.clone() } }
pub(crate) fn warning_maybe<S: Into<String>>( &self, span: rustc_span::Span, allow: &WarningAllow, note: impl FnOnce() -> S, emit: impl FnOnce(vir::messages::Message) -> (), ) { crate::attributes::warning_maybe(self.ctxt.tcx, self.fun_id, span, allow, note, emit); }
pub(crate) fn fresh_label( &self, hir_id: HirId, label: &Option<rustc_ast::ast::Label>, ) -> vir::ast::Label { let (map, next_id) = &mut *self.label_map.borrow_mut(); let label = vir::ast::Label { id: *next_id, name: label.map(|l| l.ident.to_string()) }; *next_id += 1; let found = map.insert(hir_id, label.clone()); assert!(found.is_none()); label }
pub(crate) fn label_from_dest( &self, span: rustc_span::Span, dest: &rustc_hir::Destination, ) -> Result<vir::ast::Label, VirErr> { match dest.target_id { Ok(hir_id) => { let (map, _next_id) = &*self.label_map.borrow(); match map.get(&hir_id) { None => crate::internal_err!(span, "unable to find loop label destination"), Some(label) => Ok(label.clone()), } } Err(_err) => { // This should have already been reported by rustc crate::internal_err!(span, "unresolved loop label"); } } }
pub(crate) fn push_body_erasure(&self, local_def_id: LocalDefId, c: BodyErasure) { let mut r = self.erasure_info.borrow_mut(); r.bodies.push((local_def_id, c)); }}
impl ErasureInfo { pub fn new() -> Self { ErasureInfo { local_hir_vir_ids: vec![], binder_hir_vir_ids: vec![], ctor_hir_vir_ids: vec![], resolved_calls: vec![], resolved_pats: vec![], direct_var_modes: vec![], bodies: vec![], shadow_check: vec![], extra_erase_ast_ids: vec![], local_invariant_bodies: vec![], } }}