From ed4566f94a971be8f2da5b67e309e285ecda21ad Mon Sep 17 00:00:00 2001 From: Travis Hance Date: Mon, 28 Oct 2024 11:01:45 -0400 Subject: [PATCH 01/14] Consolidate code for classifying 'external' items (#1315) --- source/builtin_macros/src/syntax.rs | 5 +- source/rust_verify/src/attributes.rs | 95 ++-- source/rust_verify/src/context.rs | 13 +- source/rust_verify/src/external.rs | 494 ++++++++++++++++++ source/rust_verify/src/lib.rs | 1 + source/rust_verify/src/lifetime.rs | 5 +- source/rust_verify/src/lifetime_generate.rs | 61 +-- source/rust_verify/src/rust_to_vir.rs | 345 ++++-------- source/rust_verify/src/rust_to_vir_base.rs | 1 - source/rust_verify/src/rust_to_vir_func.rs | 17 - source/rust_verify/src/rust_to_vir_impl.rs | 10 +- source/rust_verify/src/rust_to_vir_trait.rs | 6 +- source/rust_verify/src/verifier.rs | 2 +- .../tests/external_fn_specification.rs | 17 +- source/rust_verify_test/tests/std.rs | 2 +- source/rust_verify_test/tests/traits.rs | 2 +- 16 files changed, 727 insertions(+), 349 deletions(-) create mode 100644 source/rust_verify/src/external.rs diff --git a/source/builtin_macros/src/syntax.rs b/source/builtin_macros/src/syntax.rs index 6fb71e7f7c..dbf96012ef 100644 --- a/source/builtin_macros/src/syntax.rs +++ b/source/builtin_macros/src/syntax.rs @@ -1278,7 +1278,9 @@ impl Visitor { let block = Block { brace_token: token::Brace { span: into_spans(span) }, stmts }; *item = Item::Verbatim(quote_spanned! { span => - #[verus::internal(item_broadcast_use)] const _: () = #block; + #[verus::internal(verus_macro)] + #[verus::internal(item_broadcast_use)] + const _: () = #block; }); } } @@ -1473,6 +1475,7 @@ impl Visitor { let block = Block { brace_token: token::Brace { span: into_spans(span) }, stmts }; let mut item_fn: ItemFn = parse_quote_spanned! { span => #[verus::internal(reveal_group)] + #[verus::internal(verus_macro)] #[verus::internal(proof)] #vis fn #ident() #block }; diff --git a/source/rust_verify/src/attributes.rs b/source/rust_verify/src/attributes.rs index ac6e91d8e4..07356fecb2 100644 --- a/source/rust_verify/src/attributes.rs +++ b/source/rust_verify/src/attributes.rs @@ -843,12 +843,27 @@ pub(crate) fn get_publish( } } +// Only those relevant to classifying an item as external / not external +// (external_body is relevant because it means anything on the inside of the item should +// be external) +#[derive(Debug)] +pub(crate) struct ExternalAttrs { + pub(crate) external: bool, + pub(crate) external_body: bool, + pub(crate) external_fn_specification: bool, + pub(crate) external_type_specification: bool, + pub(crate) external_trait_specification: bool, + pub(crate) sets_mode: bool, + pub(crate) verify: bool, + pub(crate) verus_macro: bool, + pub(crate) any_other_verus_specific_attribute: bool, + pub(crate) internal_get_field_many_variants: bool, +} + #[derive(Debug)] pub(crate) struct VerifierAttrs { pub(crate) verus_macro: bool, pub(crate) external_body: bool, - pub(crate) external: bool, - pub(crate) verify: bool, pub(crate) opaque: bool, pub(crate) publish: Option, pub(crate) opaque_outside_module: bool, @@ -896,20 +911,6 @@ pub(crate) struct VerifierAttrs { pub(crate) type_invariant_fn: bool, } -impl VerifierAttrs { - pub(crate) fn is_external(&self, cmd_line_args: &crate::config::Args) -> bool { - self.external - || !(cmd_line_args.no_external_by_default - || self.verus_macro - || self.external_body - || self.external_fn_specification - || self.external_type_specification - || self.external_trait_specification.is_some() - || self.verify - || self.sets_mode) - } -} - // Check for the `get_field_many_variants` attribute // Skips additional checks that are meant to be applied only during the 'main' processing // of an item. @@ -946,16 +947,52 @@ pub(crate) fn is_sealed( Ok(false) } +/// Get the attributes needed to determine if the item is external. +pub(crate) fn get_external_attrs( + attrs: &[Attribute], + diagnostics: Option<&mut Vec>, +) -> Result { + let mut es = ExternalAttrs { + external_body: false, + external_fn_specification: false, + external_type_specification: false, + external_trait_specification: false, + external: false, + verify: false, + sets_mode: false, + verus_macro: false, + any_other_verus_specific_attribute: false, + internal_get_field_many_variants: false, + }; + + for attr in parse_attrs(attrs, diagnostics)? { + match attr { + Attr::ExternalBody => es.external_body = true, + Attr::ExternalFnSpecification => es.external_fn_specification = true, + Attr::ExternalTypeSpecification => es.external_type_specification = true, + Attr::ExternalTraitSpecification(_) => es.external_trait_specification = true, + Attr::External => es.external = true, + Attr::Verify => es.verify = true, + Attr::Mode(_) => es.sets_mode = true, + Attr::VerusMacro => es.verus_macro = true, + Attr::InternalGetFieldManyVariants => es.internal_get_field_many_variants = true, + Attr::UnsupportedRustcAttr(..) => {} + _ => { + es.any_other_verus_specific_attribute = true; + } + } + } + + return Ok(es); +} + pub(crate) fn get_verifier_attrs( attrs: &[Attribute], diagnostics: Option<&mut Vec>, - cmd_line_args: Option<&crate::config::Args>, ) -> Result { let mut vs = VerifierAttrs { verus_macro: false, external_body: false, - external: false, - verify: false, opaque: false, publish: None, opaque_outside_module: false, @@ -1006,8 +1043,6 @@ pub(crate) fn get_verifier_attrs( match attr { Attr::VerusMacro => vs.verus_macro = true, Attr::ExternalBody => vs.external_body = true, - Attr::External => vs.external = true, - Attr::Verify => vs.verify = true, Attr::ExternalFnSpecification => vs.external_fn_specification = true, Attr::ExternalTypeSpecification => vs.external_type_specification = true, Attr::ExternalTraitSpecification(assoc) => { @@ -1072,24 +1107,8 @@ pub(crate) fn get_verifier_attrs( _ => {} } } - if attrs.len() > 0 { - let span = attrs[0].span; - let mismatches = vec![ - ("inside verus macro", "`verify`", vs.verus_macro, vs.verify), - ("`external`", "`verify`", vs.external, vs.verify), - ("`external_body`", "`verify`", vs.external_body, vs.verify), - ("`external_body`", "`external`", vs.external_body, vs.external), - ]; - for (msg1, msg2, flag1, flag2) in mismatches { - if flag1 && flag2 { - return err_span(span, format!("item cannot be both {msg1} and {msg2}",)); - } - } - } if let Some((rustc_attr, span)) = unsupported_rustc_attr { - if cmd_line_args.is_none() || !vs.is_external(cmd_line_args.unwrap()) { - return err_span(span, format!("The attribute `{rustc_attr:}` is not supported")); - } + return err_span(span, format!("The attribute `{rustc_attr:}` is not supported")); } Ok(vs) } diff --git a/source/rust_verify/src/context.rs b/source/rust_verify/src/context.rs index 864e205153..19d18322eb 100644 --- a/source/rust_verify/src/context.rs +++ b/source/rust_verify/src/context.rs @@ -55,10 +55,13 @@ impl<'tcx> ContextX<'tcx> { &self, attrs: &[Attribute], ) -> Result { - crate::attributes::get_verifier_attrs( - attrs, - Some(&mut *self.diagnostics.borrow_mut()), - Some(&self.cmd_line_args), - ) + crate::attributes::get_verifier_attrs(attrs, Some(&mut *self.diagnostics.borrow_mut())) + } + + pub(crate) fn get_external_attrs( + &self, + attrs: &[Attribute], + ) -> Result { + crate::attributes::get_external_attrs(attrs, Some(&mut *self.diagnostics.borrow_mut())) } } diff --git a/source/rust_verify/src/external.rs b/source/rust_verify/src/external.rs new file mode 100644 index 0000000000..95ccb5d911 --- /dev/null +++ b/source/rust_verify/src/external.rs @@ -0,0 +1,494 @@ +/*! +This function traverses the entire crate and categorizes every +Item, ImplItem, TraitItem, and ForeignItem as either 'verus-aware' or 'external'. + +This roughly goes as follows: + + * By default, things are external (though this can be configured) + + * If something is marked with a Verus attribute (such as `verify`) then it gets marked VerusAware + + * If something is marked external, then it's ignored. Also *all nested items* + inside it are ignored. + +Here are some odd cases to watch out for: + + * If an item is marked external_body, it automatically gets marked VerusAware. + That way you don't have to mark the item as 'verify' too (since that'd be confusing). + Similarly for a few other attributes, (see the `opts_in_to_verus` function). + + * However, if an item is marked external_body, then while the item itself + is marked VerusAware, all its *nested* items are ignored. + (This is important for the rare case where a function has nested items, for example.) + + * If an item (e.g., a module) is marked 'external', then EVERYTHING inside it is ignored, + this can't be overriden from inside, not even if a nested item is marked 'verify'. + This situation results in a warning. + + * For trait decls and trait impls, we disallow #[verifier::external] on individual + TraitItems or ImplItems. + +To implement this traversal, we use some rustc visitor machinery to do the recursive +traversal, while keeping track of the current state (Default, Verify, or External). +(The difference between Default and External is that if a module is in the Default state, +then it's nested items can be marked VerusAware, but if it's External, this this is not the case.) +*/ + +use crate::attributes::ExternalAttrs; +use crate::context::Context; +use crate::rust_to_vir_base::{def_id_to_vir_path, def_id_to_vir_path_option}; +use crate::rustc_hir::intravisit::*; +use rustc_hir::{ + ForeignItem, ForeignItemId, HirId, ImplItem, ImplItemId, ImplItemKind, Item, ItemId, ItemKind, + OwnerId, TraitItem, TraitItemId, TraitItemKind, +}; +use rustc_span::Span; +use std::collections::HashMap; +use vir::ast::{Path, VirErr, VirErrAs}; + +/// Main exported type of this module. +/// Contains all item-things and their categorizations +pub struct CrateItems { + /// Vector of all crate items + pub items: Vec, + /// Same information, indexed by OwnerId + pub map: HashMap, +} + +/// Categorizes a single item-thing as VerusAware of External. +#[derive(Debug)] +pub struct CrateItem { + pub id: GeneralItemId, + pub verif: VerifOrExternal, +} + +#[derive(Debug, Clone)] +pub enum VerifOrExternal { + /// Path is the *module path* containing this item + VerusAware { module_path: Path }, + /// Path/String to refer to this item for diagnostics + /// Path is an Option because there are some items we can't compute a Path for + External { path: Option, path_string: String }, +} + +/// Abstracts over the different the different ItemX things in rust + +#[derive(Clone, Copy, Debug)] +pub enum GeneralItem<'a> { + Item(&'a Item<'a>), + ForeignItem(&'a ForeignItem<'a>), + ImplItem(&'a ImplItem<'a>), + TraitItem(&'a TraitItem<'a>), +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum GeneralItemId { + ItemId(ItemId), + ForeignItemId(ForeignItemId), + ImplItemId(ImplItemId), + TraitItemId(TraitItemId), +} + +impl CrateItems { + pub fn is_item_external(&self, item_id: ItemId) -> bool { + matches!(self.map.get(&item_id.owner_id), Some(VerifOrExternal::External { .. })) + } + + pub fn is_impl_item_external(&self, impl_item_id: ImplItemId) -> bool { + matches!(self.map.get(&impl_item_id.owner_id), Some(VerifOrExternal::External { .. })) + } + + pub fn is_trait_item_external(&self, trait_item_id: TraitItemId) -> bool { + matches!(self.map.get(&trait_item_id.owner_id), Some(VerifOrExternal::External { .. })) + } +} + +/// Collect all items (Items, ForeignItems, and ImplItems), classified as either +/// 'External' or 'VerusAware'. +/// +/// We should try to never 'error' for anything not marked verification-ready. +/// +/// Notes: +/// +/// 1. Items can be nested. Verus doesn't really support these now but we need to +/// be careful about them in external/external_body functions. Don't error +/// if there's a nested item inside an external_body function. +/// +/// 2. Impls can be either 'normal impls' or 'trait impls'. For normal impls, +/// individual items can be treated as external individually. +/// Trait impls need to be "whole" so we forbid external_body on individual +/// ImplItems in a trait_impl. + +pub(crate) fn get_crate_items<'tcx>(ctxt: &Context<'tcx>) -> Result { + let default_state = if ctxt.cmd_line_args.no_external_by_default { + VerifState::Verify + } else { + VerifState::Default + }; + + let root_module = ctxt.tcx.hir().root_module(); + let root_module_path = crate::rust_to_vir::get_root_module_path(ctxt); + + let mut visitor = VisitMod { + items: vec![], + ctxt: ctxt, + state: default_state, + module_path: root_module_path, + errors: vec![], + is_impl_trait: false, + }; + let owner = ctxt.tcx.hir().owner(rustc_hir::CRATE_OWNER_ID); + visitor.visit_mod(root_module, owner.span(), rustc_hir::CRATE_HIR_ID); + + if visitor.errors.len() > 0 { + return Err(visitor.errors[0].clone()); + } + + let mut map = HashMap::::new(); + for crate_item in visitor.items.iter() { + let owner_id = match crate_item.id { + GeneralItemId::ItemId(id) => id.owner_id, + GeneralItemId::ImplItemId(id) => id.owner_id, + GeneralItemId::ForeignItemId(id) => id.owner_id, + GeneralItemId::TraitItemId(id) => id.owner_id, + }; + let old = map.insert(owner_id, crate_item.verif.clone()); + assert!(old.is_none()); + } + + Ok(CrateItems { items: visitor.items, map }) +} + +#[derive(PartialEq, Eq, Clone, Copy, Debug)] +enum VerifState { + /// This is what the root module is unless it's overridden. Nothing has been + /// marked either 'external' or 'verify' + Default, + /// We're in a context that has been marked 'verify' + Verify, + /// We're in a context that has been marked 'external' + /// (This is a terminal state - we can never get out of it.) + External, +} + +struct VisitMod<'a, 'tcx> { + items: Vec, + ctxt: &'a Context<'tcx>, + errors: Vec, + + state: VerifState, + module_path: Path, + is_impl_trait: bool, +} + +impl<'a, 'tcx> rustc_hir::intravisit::Visitor<'tcx> for VisitMod<'a, 'tcx> { + // Configure the visitor for nested visits + type Map = rustc_middle::hir::map::Map<'tcx>; + type NestedFilter = rustc_middle::hir::nested_filter::All; + + fn nested_visit_map(&mut self) -> Self::Map { + self.ctxt.tcx.hir() + } + + fn visit_item(&mut self, item: &'tcx Item<'tcx>) { + self.visit_general(GeneralItem::Item(item), item.hir_id(), item.span); + } + + fn visit_foreign_item(&mut self, item: &'tcx ForeignItem<'tcx>) { + self.visit_general(GeneralItem::ForeignItem(item), item.hir_id(), item.span); + } + + fn visit_impl_item(&mut self, item: &'tcx ImplItem<'tcx>) { + self.visit_general(GeneralItem::ImplItem(item), item.hir_id(), item.span); + } + + fn visit_trait_item(&mut self, item: &'tcx TraitItem<'tcx>) { + self.visit_general(GeneralItem::TraitItem(item), item.hir_id(), item.span); + } +} + +fn opts_in_to_verus(eattrs: &ExternalAttrs) -> bool { + eattrs.verify + || eattrs.verus_macro + || eattrs.external_body + || eattrs.external_fn_specification + || eattrs.external_type_specification + || eattrs.external_trait_specification + || eattrs.sets_mode +} + +impl<'a, 'tcx> VisitMod<'a, 'tcx> { + fn visit_general(&mut self, general_item: GeneralItem<'tcx>, hir_id: HirId, span: Span) { + let attrs = self.ctxt.tcx.hir().attrs(hir_id); + let eattrs = match self.ctxt.get_external_attrs(attrs) { + Ok(eattrs) => eattrs, + Err(err) => { + self.errors.push(err); + return; + } + }; + + let owner_id = hir_id.expect_owner(); + let def_id = owner_id.to_def_id(); + + emit_errors_warnings_for_ignored_attrs( + self.ctxt, + self.state, + &eattrs, + &mut *self.ctxt.diagnostics.borrow_mut(), + &mut self.errors, + span, + ); + + // Compute the VerifState of this particular item based on its context + // and its attributes. + + let state_for_this_item = match self.state { + VerifState::Default => { + if eattrs.external { + VerifState::External + } else if opts_in_to_verus(&eattrs) { + VerifState::Verify + } else { + VerifState::Default + } + } + VerifState::Verify => { + if eattrs.external { + VerifState::External + } else { + VerifState::Verify + } + } + VerifState::External => VerifState::External, + }; + + // Error if any item of a trait or trait impl is ignored. + + if matches!(general_item, GeneralItem::ImplItem(_)) + && self.is_impl_trait + && self.state == VerifState::Verify + && state_for_this_item == VerifState::External + { + self.errors.push(crate::util::err_span_bare( + span, + "An individual item of a trait impl cannot be marked external. Perhaps you meant to mark the entire trait impl external, or you meant to mark this item as `external_body`?", + )); + return; + } + if matches!(general_item, GeneralItem::TraitItem(_)) + && self.state == VerifState::Verify + && state_for_this_item == VerifState::External + { + self.errors.push(crate::util::err_span_bare( + span, + "An individual item of a trait cannot be marked external. Perhaps you meant to mark the entire trait external?", + )); + return; + } + + // Append this item to the items + + let verif = if state_for_this_item == VerifState::Verify { + VerifOrExternal::VerusAware { module_path: self.module_path.clone() } + } else { + let path_opt = + def_id_to_vir_path_option(self.ctxt.tcx, Some(&self.ctxt.verus_items), def_id); + let path_string = match &path_opt { + Some(path) => vir::ast_util::path_as_friendly_rust_name(&path), + None => format!("{:?}", def_id), + }; + VerifOrExternal::External { path: path_opt, path_string } + }; + + self.items.push(CrateItem { id: general_item.id(), verif }); + + // Compute the context for any _nested_ items + + let state_inside = if eattrs.external_body { + if !general_item.may_have_external_body() { + self.errors.push(crate::util::err_span_bare( + span, + "#[verifier::external_body] doesn't make sense for this item type -- it is only applicable to functions and datatype declarations", + )); + return; + } + VerifState::External + } else { + state_for_this_item + }; + + // Recurse. If entering a module or an impl, update the relevant + // recursion state. + + let saved_state = self.state; + let saved_mod = self.module_path.clone(); + let saved_is_impl_trait = self.is_impl_trait; + + self.state = state_inside; + + match general_item { + GeneralItem::Item(item) => match item.kind { + ItemKind::Mod(_module) => { + self.module_path = + def_id_to_vir_path(self.ctxt.tcx, &self.ctxt.verus_items, def_id); + } + ItemKind::Impl(impll) => { + self.is_impl_trait = impll.of_trait.is_some(); + } + _ => {} + }, + _ => {} + } + + match general_item { + GeneralItem::Item(i) => rustc_hir::intravisit::walk_item(self, i), + GeneralItem::ForeignItem(i) => rustc_hir::intravisit::walk_foreign_item(self, i), + GeneralItem::ImplItem(i) => rustc_hir::intravisit::walk_impl_item(self, i), + GeneralItem::TraitItem(i) => rustc_hir::intravisit::walk_trait_item(self, i), + } + + self.state = saved_state; + self.module_path = saved_mod; + self.is_impl_trait = saved_is_impl_trait; + } +} + +/// Emit warnings and errors from nonsense combinations. +fn emit_errors_warnings_for_ignored_attrs<'tcx>( + ctxt: &Context<'tcx>, + state: VerifState, + eattrs: &ExternalAttrs, + diagnostics: &mut Vec, + errors: &mut Vec, + span: rustc_span::Span, +) { + if ctxt.cmd_line_args.vstd == crate::config::Vstd::IsCore { + // This gives a lot of warnings from the embedding of the 'builtin' crate so ignore it + return; + } + + if eattrs.internal_get_field_many_variants { + // The macro sometimes outputs this attribute together with 'external' for the purpose + // of some diagnostics. We thus want to ignore it. + return; + } + + // If an item is external, of if it's in a module that is marked external, then + // it will be ignored. Therefore, if there's any other verus-relevant attribute, + // it's probably a mistake. + // + // It's a hard-error for external_{fn,type,trait}_specification and a warning for + // everything else. This inconsistency is mostly for continuity with the legacy behavior, + // not necessarily for a good reason, so we might revisit it later. + if eattrs.external || state == VerifState::External { + if eattrs.external_body { + diagnostics.push(VirErrAs::Warning(crate::util::err_span_bare( + span, + format!("#[verifier::external_body] has no effect because item is already marked external"), + ))); + } else if eattrs.verify { + diagnostics.push(VirErrAs::Warning(crate::util::err_span_bare( + span, + format!( + "#[verifier::verify] has no effect because item is already marked external" + ), + ))); + } else if eattrs.external_fn_specification { + diagnostics.push(VirErrAs::Warning(crate::util::err_span_bare( + span, + format!("#[verifier::external_fn_specification] has no effect because item is already marked external"), + ))); + if eattrs.external { + errors.push(crate::util::err_span_bare( + span, + format!("a function cannot be marked both `external_fn_specification` and `external`"), + )); + } + } else if eattrs.external_type_specification { + diagnostics.push(VirErrAs::Warning(crate::util::err_span_bare( + span, + format!("#[verifier::external_type_specification] has no effect because item is already marked external"), + ))); + if eattrs.external { + errors.push(crate::util::err_span_bare( + span, + format!( + "a type cannot be marked both `external_type_specification` and `external`" + ), + )); + } + } else if eattrs.external_trait_specification { + diagnostics.push(VirErrAs::Warning(crate::util::err_span_bare( + span, + format!("#[verifier::external_trait_specification] has no effect because item is already marked external"), + ))); + if eattrs.external { + errors.push(crate::util::err_span_bare( + span, + format!("a trait cannot be marked both `external_trait_specification` and `external`"), + )); + } + } else if eattrs.sets_mode { + diagnostics.push(VirErrAs::Warning(crate::util::err_span_bare( + span, + format!( + "verifier mode attribute has no effect because item is already marked external" + ), + ))); + //} else if eattrs.verus_macro { + //diagnostics.push(VirErrAs::Warning(crate::util::err_span_bare( + // span, + // format!("The verus macro has no effect because item is already marked external"), + //))); + } else if eattrs.any_other_verus_specific_attribute { + diagnostics.push(VirErrAs::Warning(crate::util::err_span_bare( + span, + format!( + "verus-related attribute has no effect because item is already marked external" + ), + ))); + } + } + + if state == VerifState::Default && !opts_in_to_verus(&eattrs) { + if eattrs.any_other_verus_specific_attribute { + diagnostics.push(VirErrAs::Warning(crate::util::err_span_bare( + span, + format!("verus-related attribute has no effect because Verus is already ignoring this item. You may need to mark it as `#[verifier::verify]`."), + ))); + } + } +} + +impl<'a> GeneralItem<'a> { + fn id(self) -> GeneralItemId { + match self { + GeneralItem::Item(i) => GeneralItemId::ItemId(i.item_id()), + GeneralItem::ForeignItem(i) => GeneralItemId::ForeignItemId(i.foreign_item_id()), + GeneralItem::ImplItem(i) => GeneralItemId::ImplItemId(i.impl_item_id()), + GeneralItem::TraitItem(i) => GeneralItemId::TraitItemId(i.trait_item_id()), + } + } + + fn may_have_external_body(self) -> bool { + match self { + GeneralItem::Item(i) => match i.kind { + ItemKind::Fn(..) => true, + ItemKind::Struct(..) => true, + ItemKind::Enum(..) => true, + ItemKind::Union(..) => true, + _ => false, + }, + GeneralItem::ForeignItem(_) => false, + GeneralItem::ImplItem(i) => match i.kind { + ImplItemKind::Fn(..) => true, + _ => false, + }, + GeneralItem::TraitItem(i) => match i.kind { + TraitItemKind::Fn(..) => true, + _ => false, + }, + } + } +} diff --git a/source/rust_verify/src/lib.rs b/source/rust_verify/src/lib.rs index 0cac1ff9a7..d7cbda3065 100644 --- a/source/rust_verify/src/lib.rs +++ b/source/rust_verify/src/lib.rs @@ -43,6 +43,7 @@ pub mod driver; pub mod erase; mod expand_errors_driver; pub mod externs; +pub mod external; pub mod file_loader; mod fn_call_to_vir; mod hir_hide_reveal_rewrite; diff --git a/source/rust_verify/src/lifetime.rs b/source/rust_verify/src/lifetime.rs index ae6edab676..11c26d96cc 100644 --- a/source/rust_verify/src/lifetime.rs +++ b/source/rust_verify/src/lifetime.rs @@ -112,6 +112,7 @@ and then sending the error messages and spans to the rustc diagnostics for the o // In functions executed through the lifetime rustc driver, use `ldbg!` for debug output. use crate::erase::ErasureHints; +use crate::external::CrateItems; use crate::lifetime_emit::*; use crate::lifetime_generate::*; use crate::spans::SpanContext; @@ -271,7 +272,7 @@ fn emit_check_tracked_lifetimes<'tcx>( krate: &'tcx Crate<'tcx>, emit_state: &mut EmitState, erasure_hints: &ErasureHints, - item_to_module_map: &crate::rust_to_vir::ItemToModuleMap, + item_to_module_map: &CrateItems, vir_crate: &vir::ast::Krate, ) -> State { let mut gen_state = crate::lifetime_generate::gen_check_tracked_lifetimes( @@ -374,7 +375,7 @@ pub(crate) fn check_tracked_lifetimes<'tcx>( verus_items: std::sync::Arc, spans: &SpanContext, erasure_hints: &ErasureHints, - item_to_module_map: &crate::rust_to_vir::ItemToModuleMap, + item_to_module_map: &CrateItems, vir_crate: &vir::ast::Krate, lifetime_log_file: Option, ) -> Result, VirErr> { diff --git a/source/rust_verify/src/lifetime_generate.rs b/source/rust_verify/src/lifetime_generate.rs index 93d8f32e84..cdf66bb0db 100644 --- a/source/rust_verify/src/lifetime_generate.rs +++ b/source/rust_verify/src/lifetime_generate.rs @@ -1,5 +1,6 @@ use crate::attributes::{get_ghost_block_opt, get_mode, get_verifier_attrs, GhostBlockAttr}; use crate::erase::{ErasureHints, ResolvedCall}; +use crate::external::CrateItems; use crate::rust_to_vir_base::{def_id_to_vir_path, mid_ty_const_to_vir, remove_host_arg}; use crate::rust_to_vir_expr::{get_adt_res_struct_enum, get_adt_res_struct_enum_union}; use crate::verus_items::{BuiltinTypeItem, RustItem, VerusItem, VerusItems}; @@ -45,7 +46,7 @@ impl TypX { } struct Context<'tcx> { - cmd_line_args: crate::config::Args, + _cmd_line_args: crate::config::Args, tcx: TyCtxt<'tcx>, verus_items: Arc, types_opt: Option<&'tcx TypeckResults<'tcx>>, @@ -2438,8 +2439,7 @@ fn erase_trait_item<'tcx>( let id = owner_id.to_def_id(); let attrs = ctxt.tcx.hir().attrs(trait_item.hir_id()); - let vattrs = get_verifier_attrs(attrs, None, Some(&ctxt.cmd_line_args)) - .expect("get_verifier_attrs"); + let vattrs = get_verifier_attrs(attrs, None).expect("get_verifier_attrs"); erase_fn( krate, @@ -2466,6 +2466,7 @@ fn erase_impl<'tcx>( state: &mut State, impl_id: DefId, impll: &Impl<'tcx>, + crate_items: &CrateItems, ) { for impl_item_ref in impll.items { match impl_item_ref.kind { @@ -2474,9 +2475,8 @@ fn erase_impl<'tcx>( let ImplItem { ident, owner_id, kind, .. } = impl_item; let id = owner_id.to_def_id(); let attrs = ctxt.tcx.hir().attrs(impl_item.hir_id()); - let vattrs = get_verifier_attrs(attrs, None, Some(&ctxt.cmd_line_args)) - .expect("get_verifier_attrs"); - if vattrs.is_external(&ctxt.cmd_line_args) { + let vattrs = get_verifier_attrs(attrs, None).expect("get_verifier_attrs"); + if crate_items.is_impl_item_external(impl_item_ref.id) { continue; } if vattrs.reveal_group { @@ -2613,8 +2613,7 @@ fn erase_mir_datatype<'tcx>(ctxt: &Context<'tcx>, state: &mut State, id: DefId) } else { ctxt.tcx.item_attrs(id) }; - let vattrs = - get_verifier_attrs(attrs, None, Some(&ctxt.cmd_line_args)).expect("get_verifier_attrs"); + let vattrs = get_verifier_attrs(attrs, None).expect("get_verifier_attrs"); if vattrs.external_type_specification { return; } @@ -2683,10 +2682,10 @@ pub(crate) fn gen_check_tracked_lifetimes<'tcx>( verus_items: Arc, krate: &'tcx Crate<'tcx>, erasure_hints: &ErasureHints, - item_to_module_map: &crate::rust_to_vir::ItemToModuleMap, + crate_items: &CrateItems, ) -> State { let mut ctxt = Context { - cmd_line_args, + _cmd_line_args: cmd_line_args, tcx, verus_items, types_opt: None, @@ -2777,7 +2776,7 @@ pub(crate) fn gen_check_tracked_lifetimes<'tcx>( if let MaybeOwner::Owner(owner) = owner { match owner.node() { OwnerNode::Item(item) => { - if matches!(item_to_module_map.get(&item.item_id()), Some(None)) { + if crate_items.is_item_external(item.item_id()) { // item is external continue; } @@ -2794,10 +2793,7 @@ pub(crate) fn gen_check_tracked_lifetimes<'tcx>( _bounds, _trait_items, ) => { - let attrs = tcx.hir().attrs(item.hir_id()); - let vattrs = get_verifier_attrs(attrs, None, Some(&ctxt.cmd_line_args)) - .expect("get_verifier_attrs"); - if vattrs.is_external(&ctxt.cmd_line_args) { + if crate_items.is_item_external(item.item_id()) { continue; } // We only need traits with associated type declarations. @@ -2817,14 +2813,13 @@ pub(crate) fn gen_check_tracked_lifetimes<'tcx>( if let MaybeOwner::Owner(owner) = owner { match owner.node() { OwnerNode::Item(item) => { - if matches!(item_to_module_map.get(&item.item_id()), Some(None)) { + if crate_items.is_item_external(item.item_id()) { // item is external continue; } let attrs = tcx.hir().attrs(item.hir_id()); - let vattrs = get_verifier_attrs(attrs, None, Some(&ctxt.cmd_line_args)) - .expect("get_verifier_attrs"); - if vattrs.external || vattrs.internal_reveal_fn || vattrs.internal_const_body { + let vattrs = get_verifier_attrs(attrs, None).expect("get_verifier_attrs"); + if vattrs.internal_reveal_fn || vattrs.internal_const_body { continue; } let id = item.owner_id.to_def_id(); @@ -2837,28 +2832,16 @@ pub(crate) fn gen_check_tracked_lifetimes<'tcx>( ItemKind::TyAlias(..) => {} ItemKind::GlobalAsm(..) => {} ItemKind::Struct(_s, _generics) => { - if vattrs.is_external(&ctxt.cmd_line_args) { - continue; - } state.reach_datatype(&ctxt, id); } ItemKind::Enum(_e, _generics) => { - if vattrs.is_external(&ctxt.cmd_line_args) { - continue; - } state.reach_datatype(&ctxt, id); } ItemKind::Union(_e, _generics) => { - if vattrs.is_external(&ctxt.cmd_line_args) { - continue; - } state.reach_datatype(&ctxt, id); } ItemKind::Const(_ty, _, body_id) | ItemKind::Static(_ty, _, body_id) => { - if vattrs.size_of_global - || vattrs.item_broadcast_use - || vattrs.is_external(&ctxt.cmd_line_args) - { + if vattrs.size_of_global || vattrs.item_broadcast_use { continue; } erase_const_or_static( @@ -2873,9 +2856,6 @@ pub(crate) fn gen_check_tracked_lifetimes<'tcx>( ); } ItemKind::Fn(sig, _generics, body_id) => { - if vattrs.is_external(&ctxt.cmd_line_args) { - continue; - } if vattrs.reveal_group { continue; } @@ -2918,9 +2898,6 @@ pub(crate) fn gen_check_tracked_lifetimes<'tcx>( _bounds, trait_items, ) => { - if vattrs.is_external(&ctxt.cmd_line_args) { - continue; - } let ex_trait_id_for = crate::rust_to_vir_trait::external_trait_specification_of( tcx, @@ -2944,10 +2921,7 @@ pub(crate) fn gen_check_tracked_lifetimes<'tcx>( ); } ItemKind::Impl(impll) => { - if vattrs.is_external(&ctxt.cmd_line_args) { - continue; - } - erase_impl(krate, &mut ctxt, &mut state, id, impll); + erase_impl(krate, &mut ctxt, &mut state, id, impll, crate_items); } ItemKind::OpaqueTy(OpaqueTy { generics: _, @@ -2959,9 +2933,6 @@ pub(crate) fn gen_check_tracked_lifetimes<'tcx>( continue; } _ => { - if vattrs.is_external(&ctxt.cmd_line_args) { - continue; - } dbg!(item); panic!("unexpected item"); } diff --git a/source/rust_verify/src/rust_to_vir.rs b/source/rust_verify/src/rust_to_vir.rs index 2f9314beea..369d0550b4 100644 --- a/source/rust_verify/src/rust_to_vir.rs +++ b/source/rust_verify/src/rust_to_vir.rs @@ -7,6 +7,7 @@ For soundness's sake, be as defensive as possible: */ use crate::context::Context; +use crate::external::{CrateItems, GeneralItemId, VerifOrExternal}; use crate::reveal_hide::handle_reveal_hide; use crate::rust_to_vir_adts::{check_item_enum, check_item_struct, check_item_union}; use crate::rust_to_vir_base::{def_id_to_vir_path, mid_ty_to_vir, mk_visibility}; @@ -16,6 +17,7 @@ use crate::rust_to_vir_impl::ExternalInfo; use crate::util::err_span; use crate::verus_items::{self, VerusItem}; use crate::{unsupported_err, unsupported_err_unless}; +use std::collections::HashSet; use rustc_ast::IsAuto; use rustc_hir::{ @@ -31,25 +33,12 @@ use vir::ast::{FunX, FunctionKind, Krate, KrateX, Path, VirErr}; fn check_item<'tcx>( ctxt: &Context<'tcx>, vir: &mut KrateX, - mpath: Option<&Option>, + module_path: &Path, id: &ItemId, item: &'tcx Item<'tcx>, external_info: &mut ExternalInfo, + crate_items: &CrateItems, ) -> Result<(), VirErr> { - // delay computation of module_path because some external or builtin items don't have a valid Path - let module_path = || { - if let Some(Some(path)) = mpath { - path.clone() - } else { - let owned_by = ctxt.krate.owners[item.hir_id().owner.def_id] - .as_owner() - .as_ref() - .expect("owner of item") - .node(); - def_id_to_vir_path(ctxt.tcx, &ctxt.verus_items, owned_by.def_id().to_def_id()) - } - }; - let attrs = ctxt.tcx.hir().attrs(item.hir_id()); let vattrs = ctxt.get_verifier_attrs(attrs)?; if vattrs.internal_reveal_fn { @@ -74,19 +63,6 @@ fn check_item<'tcx>( ); } } - if vattrs.is_external(&ctxt.cmd_line_args) - && crate::rust_to_vir_base::def_id_to_vir_path_option( - ctxt.tcx, - Some(&ctxt.verus_items), - item.owner_id.to_def_id(), - ) - .is_none() - { - // If the path of an external item would cause a panic in def_id_to_vir_path, - // ignore it completely to avoid a panic (potentially leading to less informative - // error messages to users if they try to access the external item directly from Verus code) - return Ok(()); - } let visibility = || mk_visibility(ctxt, item.owner_id.to_def_id()); @@ -159,13 +135,10 @@ fn check_item<'tcx>( }) .collect::, _>>()?; - let Some(Some(mpath)) = mpath else { - unsupported_err!(item.span, "unsupported broadcast use here", item); - }; let module = vir .modules .iter_mut() - .find(|m| &m.x.path == mpath) + .find(|m| &m.x.path == module_path) .expect("cannot find current module"); let reveals = &mut Arc::make_mut(module).x.reveals; if reveals.is_some() { @@ -188,14 +161,6 @@ fn check_item<'tcx>( return Ok(()); } - if vattrs.is_external(&ctxt.cmd_line_args) { - let mut erasure_info = ctxt.erasure_info.borrow_mut(); - let path = def_id_to_vir_path(ctxt.tcx, &ctxt.verus_items, item.owner_id.to_def_id()); - let name = Arc::new(FunX { path: path.clone() }); - erasure_info.external_functions.push(name); - return Ok(()); - } - let mid_ty = ctxt.tcx.type_of(def_id).skip_binder(); let vir_ty = mid_ty_to_vir(ctxt.tcx, &ctxt.verus_items, def_id, item.span, &mid_ty, false)?; @@ -205,7 +170,7 @@ fn check_item<'tcx>( item.span, item.owner_id.to_def_id(), visibility(), - &module_path(), + module_path, ctxt.tcx.hir().attrs(item.hir_id()), &vir_ty, body_id, @@ -222,7 +187,7 @@ fn check_item<'tcx>( item.owner_id.to_def_id(), FunctionKind::Static, visibility(), - &module_path(), + module_path, ctxt.tcx.hir().attrs(item.hir_id()), sig, None, @@ -247,28 +212,13 @@ fn check_item<'tcx>( // rustc_middle; in fact, we still rely on attributes which we can only // get from the HIR data. - if vattrs.is_external(&ctxt.cmd_line_args) { - if vattrs.external_type_specification { - return err_span( - item.span, - "a type cannot be marked both `external_type_specification` and `external`", - ); - } - - let def_id = id.owner_id.to_def_id(); - let path = def_id_to_vir_path(ctxt.tcx, &ctxt.verus_items, def_id); - vir.external_types.push(path); - - return Ok(()); - } - let tyof = ctxt.tcx.type_of(item.owner_id.to_def_id()).skip_binder(); let adt_def = tyof.ty_adt_def().expect("adt_def"); check_item_struct( ctxt, vir, - &module_path(), + module_path, item.span, id, visibility(), @@ -280,14 +230,6 @@ fn check_item<'tcx>( )?; } ItemKind::Enum(enum_def, generics) => { - if vattrs.is_external(&ctxt.cmd_line_args) { - let def_id = id.owner_id.to_def_id(); - let path = def_id_to_vir_path(ctxt.tcx, &ctxt.verus_items, def_id); - vir.external_types.push(path); - - return Ok(()); - } - let tyof = ctxt.tcx.type_of(item.owner_id.to_def_id()).skip_binder(); let adt_def = tyof.ty_adt_def().expect("adt_def"); @@ -295,7 +237,7 @@ fn check_item<'tcx>( check_item_enum( ctxt, vir, - &module_path(), + module_path, item.span, id, visibility(), @@ -306,21 +248,13 @@ fn check_item<'tcx>( )?; } ItemKind::Union(variant_data, generics) => { - if vattrs.is_external(&ctxt.cmd_line_args) { - let def_id = id.owner_id.to_def_id(); - let path = def_id_to_vir_path(ctxt.tcx, &ctxt.verus_items, def_id); - vir.external_types.push(path); - - return Ok(()); - } - let tyof = ctxt.tcx.type_of(item.owner_id.to_def_id()).skip_binder(); let adt_def = tyof.ty_adt_def().expect("adt_def"); check_item_union( ctxt, vir, - &module_path(), + module_path, item.span, id, visibility(), @@ -331,25 +265,16 @@ fn check_item<'tcx>( )?; } ItemKind::Impl(impll) => { - if vattrs.is_external(&ctxt.cmd_line_args) { - return Ok(()); - } crate::rust_to_vir_impl::translate_impl( ctxt, vir, item, impll, - module_path(), + module_path.clone(), external_info, + crate_items, )?; } - ItemKind::Static(..) - if ctxt - .get_verifier_attrs(ctxt.tcx.hir().attrs(item.hir_id()))? - .is_external(&ctxt.cmd_line_args) => - { - return Ok(()); - } ItemKind::Const(_ty, generics, body_id) => { unsupported_err_unless!( generics.params.len() == 0 && generics.predicates.len() == 0, @@ -362,22 +287,10 @@ fn check_item<'tcx>( handle_const_or_static(body_id)?; } ItemKind::Static(_ty, Mutability::Mut, _body_id) => { - if vattrs.is_external(&ctxt.cmd_line_args) { - return Ok(()); - } unsupported_err!(item.span, "static mut"); } ItemKind::Macro(_, _) => {} ItemKind::Trait(IsAuto::No, Safety::Safe, trait_generics, _bounds, trait_items) => { - if vattrs.is_external(&ctxt.cmd_line_args) { - if vattrs.external_trait_specification.is_some() { - return err_span( - item.span, - "a trait cannot be marked both `external_trait_specification` and `external`", - ); - } - return Ok(()); - } let trait_def_id = item.owner_id.to_def_id(); crate::rust_to_vir_trait::translate_trait( ctxt, @@ -385,11 +298,12 @@ fn check_item<'tcx>( item.span, trait_def_id, visibility(), - &module_path(), + module_path, trait_generics, trait_items, &vattrs, external_info, + crate_items, )?; } ItemKind::TyAlias(_ty, _generics) => { @@ -411,9 +325,6 @@ fn check_item<'tcx>( return Ok(()); } _ => { - if vattrs.is_external(&ctxt.cmd_line_args) { - return Ok(()); - } unsupported_err!(item.span, "unsupported item", item); } } @@ -441,44 +352,20 @@ fn check_foreign_item<'tcx>( )?; } _ => { - if ctxt - .get_verifier_attrs(ctxt.tcx.hir().attrs(item.hir_id()))? - .is_external(&ctxt.cmd_line_args) - { - return Ok(()); - } else { - unsupported_err!(item.span, "unsupported foreign item", item); - } + unsupported_err!(item.span, "unsupported foreign item", item); } } Ok(()) } -struct VisitMod<'tcx> { - _tcx: rustc_middle::ty::TyCtxt<'tcx>, - ids: Vec, -} - -impl<'tcx> rustc_hir::intravisit::Visitor<'tcx> for VisitMod<'tcx> { - type Map = rustc_middle::hir::map::Map<'tcx>; - type NestedFilter = rustc_middle::hir::nested_filter::All; - - fn nested_visit_map(&mut self) -> Self::Map { - self._tcx.hir() - } - - fn visit_item(&mut self, item: &'tcx Item<'tcx>) { - self.ids.push(item.item_id()); - rustc_hir::intravisit::walk_item(self, item); - } +pub(crate) fn get_root_module_path<'tcx>(ctxt: &Context<'tcx>) -> Path { + def_id_to_vir_path(ctxt.tcx, &ctxt.verus_items, rustc_hir::CRATE_OWNER_ID.to_def_id()) } -pub type ItemToModuleMap = HashMap>; - -pub fn crate_to_vir<'tcx>( +pub fn crate_to_vir<'a, 'tcx>( ctxt: &mut Context<'tcx>, imported: &Vec, -) -> Result<(Krate, ItemToModuleMap), VirErr> { +) -> Result<(Krate, CrateItems), VirErr> { let mut vir: KrateX = KrateX { functions: Vec::new(), reveal_groups: Vec::new(), @@ -507,64 +394,7 @@ pub fn crate_to_vir<'tcx>( .trait_id_set .insert(tcx.get_diagnostic_item(rustc_span::sym::Send).expect("send")); - // Map each item to the module that contains it, or None if the module is external - let mut item_to_module: HashMap> = HashMap::new(); - for (owner_id, owner_opt) in ctxt.krate.owners.iter_enumerated() { - if let MaybeOwner::Owner(owner) = owner_opt { - match owner.node() { - OwnerNode::Item(item @ Item { kind: ItemKind::Mod(mod_), owner_id, .. }) => { - let attrs = ctxt.tcx.hir().attrs(item.hir_id()); - let vattrs = ctxt.get_verifier_attrs(attrs)?; - if vattrs.external { - // Recursively mark every item in the module external, - // even in nested modules - use crate::rustc_hir::intravisit::Visitor; - let mut visitor = VisitMod { _tcx: ctxt.tcx, ids: Vec::new() }; - visitor.visit_item(item); - item_to_module.extend(visitor.ids.iter().map(move |ii| (*ii, None))) - } else { - // Shallowly visit just the top-level items (don't visit nested modules) - let path = - def_id_to_vir_path(ctxt.tcx, &ctxt.verus_items, owner_id.to_def_id()); - vir.modules.push(ctxt.spanned_new( - item.span, - vir::ast::ModuleX { path: path.clone(), reveals: None }, - )); - let path = Some(path); - item_to_module - .extend(mod_.item_ids.iter().map(move |ii| (*ii, path.clone()))) - }; - } - OwnerNode::Item(item @ Item { kind: _, owner_id: _, .. }) => { - // If we have something like: - // #[verifier::external_body] - // fn test() { - // fn nested_item() { ... } - // } - // Then we need to make sure nested_item() gets marked external. - let attrs = ctxt.tcx.hir().attrs(item.hir_id()); - let vattrs = ctxt.get_verifier_attrs(attrs)?; - if vattrs.external || vattrs.external_body { - use crate::rustc_hir::intravisit::Visitor; - let mut visitor = VisitMod { _tcx: ctxt.tcx, ids: Vec::new() }; - visitor.visit_item(item); - item_to_module.extend(visitor.ids.iter().skip(1).map(move |ii| (*ii, None))) - } - } - OwnerNode::Crate(mod_) => { - let path = - def_id_to_vir_path(ctxt.tcx, &ctxt.verus_items, owner_id.to_def_id()); - vir.modules.push(ctxt.spanned_new( - mod_.spans.inner_span, - vir::ast::ModuleX { path: path.clone(), reveals: None }, - )); - item_to_module - .extend(mod_.item_ids.iter().map(move |ii| (*ii, Some(path.clone())))) - } - _ => (), - } - } - } + let crate_items = crate::external::get_crate_items(ctxt)?; let mut typs_sizes_set: HashMap = HashMap::new(); for (_, owner_opt) in ctxt.krate.owners.iter_enumerated() { @@ -581,64 +411,119 @@ pub fn crate_to_vir<'tcx>( } } } + { let ctxt = Arc::make_mut(ctxt); let arch_word_bits = ctxt.arch_word_bits.unwrap_or(vir::ast::ArchWordBits::Either32Or64); ctxt.arch_word_bits = Some(arch_word_bits); vir.arch.word_bits = arch_word_bits; } - for owner in ctxt.krate.owners.iter() { - if let MaybeOwner::Owner(owner) = owner { + + // Find all modules that contain at least 1 item of interest + let mut used_modules = HashSet::::new(); + for crate_item in crate_items.items.iter() { + match &crate_item.verif { + VerifOrExternal::VerusAware { module_path } => { + used_modules.insert(module_path.clone()); + } + _ => {} + } + } + // Insert those modules into vir.modules + let root_module_path = get_root_module_path(ctxt); + if used_modules.contains(&root_module_path) { + let owner = ctxt.tcx.hir().owner(rustc_hir::CRATE_OWNER_ID); + vir.modules.push(ctxt.spanned_new( + owner.span(), + vir::ast::ModuleX { path: root_module_path.clone(), reveals: None }, + )); + } + for (_owner_id, owner_opt) in ctxt.krate.owners.iter_enumerated() { + if let MaybeOwner::Owner(owner) = owner_opt { match owner.node() { - OwnerNode::Item(item) => { - // If the item does not belong to a module, use the def_id of its owner as the - // module path - let mpath = item_to_module.get(&item.item_id()); - if let Some(None) = mpath { - // whole module is external, so skip the item - continue; + OwnerNode::Item(item @ Item { kind: ItemKind::Mod(_module), owner_id, .. }) => { + let path = + def_id_to_vir_path(ctxt.tcx, &ctxt.verus_items, owner_id.to_def_id()); + if used_modules.contains(&path) { + vir.modules.push(ctxt.spanned_new( + item.span, + vir::ast::ModuleX { path: path.clone(), reveals: None }, + )); } - check_item(ctxt, &mut vir, mpath, &item.item_id(), item, &mut external_info)? } - OwnerNode::ForeignItem(foreign_item) => check_foreign_item( - ctxt, - &mut vir, - &foreign_item.foreign_item_id(), - foreign_item, - )?, - OwnerNode::TraitItem(_trait_item) => { - // handled by ItemKind::Trait + _ => {} + } + } + } + + for crate_item in crate_items.items.iter() { + match &crate_item.verif { + VerifOrExternal::VerusAware { module_path } => { + match crate_item.id { + GeneralItemId::ItemId(item_id) => { + let item = ctxt.tcx.hir().item(item_id); + check_item( + ctxt, + &mut vir, + &module_path, + &item_id, + item, + &mut external_info, + &crate_items, + )?; + } + GeneralItemId::ForeignItemId(foreign_item_id) => { + let foreign_item = ctxt.tcx.hir().foreign_item(foreign_item_id); + check_foreign_item(ctxt, &mut vir, &foreign_item_id, foreign_item)?; + } + GeneralItemId::ImplItemId(_impl_item_id) => { + // Processed as part of the impl (which is an Item) + } + GeneralItemId::TraitItemId(_trait_item_id) => { + // Processed as part of the impl (which is an Item) + } } - OwnerNode::ImplItem(impl_item) => match impl_item.kind { - ImplItemKind::Fn(_, _) => { - let impl_item_ident = impl_item.ident.as_str(); - if impl_item_ident == "assert_receiver_is_total_eq" - || impl_item_ident == "eq" - || impl_item_ident == "ne" - || impl_item_ident == "assert_receiver_is_structural" - { - // TODO: check whether these implement the correct trait + } + VerifOrExternal::External { path: Some(my_path), path_string: _ } => { + // If possible, track this item in the VIR Krate for diagnostic purposes + let (is_fn, is_datatype) = match crate_item.id { + GeneralItemId::ItemId(item_id) => { + let i = ctxt.tcx.hir().item(item_id); + match i.kind { + ItemKind::Fn(..) | ItemKind::Const(..) => (true, false), + ItemKind::Struct(..) | ItemKind::Enum(..) | ItemKind::Union(..) => { + (false, true) + } + _ => (false, false), } } - ImplItemKind::Type(_ty) => { - // checked by the type system + GeneralItemId::ForeignItemId(foreign_item_id) => { + let i = ctxt.tcx.hir().foreign_item(foreign_item_id); + match i.kind { + ForeignItemKind::Fn(..) => (true, false), + _ => (false, false), + } } - _ => { - let attrs = ctxt.tcx.hir().attrs(impl_item.hir_id()); - let vattrs = ctxt.get_verifier_attrs(attrs)?; - if !vattrs.is_external(&ctxt.cmd_line_args) { - unsupported_err!(impl_item.span, "unsupported_impl_item", impl_item); + GeneralItemId::ImplItemId(impl_item_id) => { + let i = ctxt.tcx.hir().impl_item(impl_item_id); + match i.kind { + ImplItemKind::Fn(..) => (true, false), + _ => (false, false), } } - }, - OwnerNode::Crate(_mod_) => (), - OwnerNode::Synthetic => (), + GeneralItemId::TraitItemId(_trait_item_id) => (false, false), + }; + if is_fn { + vir.external_fns.push(Arc::new(FunX { path: my_path.clone() })); + } + if is_datatype { + vir.external_types.push(my_path.clone()); + } } + VerifOrExternal::External { path: None, path_string: _ } => {} } } - let erasure_info = ctxt.erasure_info.borrow(); - vir.external_fns = erasure_info.external_functions.clone(); vir.path_as_rust_names = vir::ast_util::get_path_as_rust_names_for_krate(&ctxt.vstd_crate_name); crate::rust_to_vir_impl::collect_external_trait_impls( @@ -650,5 +535,5 @@ pub fn crate_to_vir<'tcx>( crate::rust_to_vir_adts::setup_type_invariants(&mut vir)?; - Ok((Arc::new(vir), item_to_module)) + Ok((Arc::new(vir), crate_items)) } diff --git a/source/rust_verify/src/rust_to_vir_base.rs b/source/rust_verify/src/rust_to_vir_base.rs index b90e5d12c0..118d9a0a3f 100644 --- a/source/rust_verify/src/rust_to_vir_base.rs +++ b/source/rust_verify/src/rust_to_vir_base.rs @@ -1658,7 +1658,6 @@ fn check_generics_bounds_main<'tcx>( let vattrs = get_verifier_attrs( tcx.hir().attrs(hir_param.hir_id), if let Some(diagnostics) = &mut diagnostics { Some(diagnostics) } else { None }, - None, )?; if vattrs.reject_recursive_types || vattrs.reject_recursive_types_in_ground_variants diff --git a/source/rust_verify/src/rust_to_vir_func.rs b/source/rust_verify/src/rust_to_vir_func.rs index ec41f13259..bcadf77a33 100644 --- a/source/rust_verify/src/rust_to_vir_func.rs +++ b/source/rust_verify/src/rust_to_vir_func.rs @@ -205,12 +205,6 @@ pub(crate) fn handle_external_fn<'tcx>( ); } - if vattrs.external { - return err_span( - sig.span, - format!("an `assume_specification` declaration cannot be marked `external`"), - ); - } if vattrs.external_body { return err_span( sig.span, @@ -639,12 +633,6 @@ pub(crate) fn check_item_fn<'tcx>( let name = Arc::new(FunX { path: path.clone() }); - if vattrs.is_external(&ctxt.cmd_line_args) { - let mut erasure_info = ctxt.erasure_info.borrow_mut(); - erasure_info.external_functions.push(name); - return Ok(None); - } - let self_typ_params = if let Some((cg, impl_def_id)) = self_generics { Some(check_generics_bounds_no_polarity( ctxt.tcx, @@ -1822,11 +1810,6 @@ pub(crate) fn check_foreign_item_fn<'tcx>( if vattrs.external_fn_specification { return err_span(span, "assume_specification not supported here"); } - if vattrs.is_external(&ctxt.cmd_line_args) { - let mut erasure_info = ctxt.erasure_info.borrow_mut(); - erasure_info.external_functions.push(name); - return Ok(()); - } let mode = get_mode(Mode::Exec, attrs); diff --git a/source/rust_verify/src/rust_to_vir_impl.rs b/source/rust_verify/src/rust_to_vir_impl.rs index 0d859e0afc..d03c196af9 100644 --- a/source/rust_verify/src/rust_to_vir_impl.rs +++ b/source/rust_verify/src/rust_to_vir_impl.rs @@ -1,4 +1,5 @@ use crate::context::Context; +use crate::external::CrateItems; use crate::rust_to_vir_base::{ def_id_to_vir_path, def_id_to_vir_path_option, mid_ty_const_to_vir, mid_ty_to_vir, mk_visibility, remove_host_arg, typ_path_and_ident_to_vir_path, @@ -218,6 +219,7 @@ pub(crate) fn translate_impl<'tcx>( impll: &rustc_hir::Impl<'tcx>, module_path: Path, external_info: &mut ExternalInfo, + crate_items: &CrateItems, ) -> Result<(), VirErr> { let impl_def_id = item.owner_id.to_def_id(); let impl_path = def_id_to_vir_path(ctxt.tcx, &ctxt.verus_items, impl_def_id); @@ -340,14 +342,16 @@ pub(crate) fn translate_impl<'tcx>( for impl_item_ref in impll.items { let impl_item = ctxt.tcx.hir().impl_item(impl_item_ref.id); let fn_attrs = ctxt.tcx.hir().attrs(impl_item.hir_id()); - if trait_path_typ_args.is_some() { - let vattrs = ctxt.get_verifier_attrs(fn_attrs)?; - if vattrs.external { + + if crate_items.is_impl_item_external(impl_item_ref.id) { + if trait_path_typ_args.is_some() { + // sanity check - this should be redundant with prior check in external.rs return err_span( item.span, "an item in a trait impl cannot be marked external - you can either use external_body, or mark the entire trait impl as external", ); } + continue; } match impl_item_ref.kind { diff --git a/source/rust_verify/src/rust_to_vir_trait.rs b/source/rust_verify/src/rust_to_vir_trait.rs index fb4561efb1..307b033e8e 100644 --- a/source/rust_verify/src/rust_to_vir_trait.rs +++ b/source/rust_verify/src/rust_to_vir_trait.rs @@ -1,5 +1,6 @@ use crate::attributes::VerifierAttrs; use crate::context::Context; +use crate::external::CrateItems; use crate::rust_to_vir_base::{ check_generics_bounds_with_polarity, def_id_to_vir_path, process_predicate_bounds, }; @@ -78,6 +79,7 @@ pub(crate) fn translate_trait<'tcx>( trait_items: &'tcx [TraitItemRef], trait_vattrs: &VerifierAttrs, external_info: &mut ExternalInfo, + crate_items: &CrateItems, ) -> Result<(), VirErr> { let tcx = ctxt.tcx; let orig_trait_path = def_id_to_vir_path(tcx, &ctxt.verus_items, trait_def_id); @@ -202,9 +204,7 @@ pub(crate) fn translate_trait<'tcx>( Some(&mut *ctxt.diagnostics.borrow_mut()), )?; - let attrs = tcx.hir().attrs(trait_item.hir_id()); - let vattrs = ctxt.get_verifier_attrs(attrs)?; - if vattrs.external { + if crate_items.is_trait_item_external(trait_item_ref.id) { return err_span( *span, "a trait item cannot be marked 'external' - perhaps you meant to mark the entire trait external?", diff --git a/source/rust_verify/src/verifier.rs b/source/rust_verify/src/verifier.rs index 8c02c760ec..2d0d0067d6 100644 --- a/source/rust_verify/src/verifier.rs +++ b/source/rust_verify/src/verifier.rs @@ -296,7 +296,7 @@ pub struct Verifier { crate_names: Option>, air_no_span: Option, current_crate_modules: Option>, - item_to_module_map: Option>, + item_to_module_map: Option>, buckets: HashMap, // proof debugging purposes diff --git a/source/rust_verify_test/tests/external_fn_specification.rs b/source/rust_verify_test/tests/external_fn_specification.rs index 44cba556c3..86aaad6868 100644 --- a/source/rust_verify_test/tests/external_fn_specification.rs +++ b/source/rust_verify_test/tests/external_fn_specification.rs @@ -1275,7 +1275,7 @@ test_verify_one_file! { impl Tr for X { fn foo(&self) { } } - } => Err(err) => assert_vir_error_msg(err, "X::foo` is not supported") // TODO could have clearer error msg + } => Err(err) => assert_vir_error_msg(err, "cannot call function marked `external`; try marking it `external_body` instead, or add a Verus specification via `external_fn_specification`") } test_verify_one_file! { @@ -1355,3 +1355,18 @@ test_verify_one_file! { } } => Err(err) => assert_vir_error_msg(err, "assume_specification for a provided trait method") } + +test_verify_one_file! { + #[test] module_external code! { + #[verifier::external] + mod moo { + #[verifier::verify] + fn stuff() { + builtin::assert_(false); + } + } + } => Ok(err) => { + assert!(err.warnings.len() == 2); + assert!(err.warnings[0].message.contains("#[verifier::verify] has no effect because item is already marked external")); + } +} diff --git a/source/rust_verify_test/tests/std.rs b/source/rust_verify_test/tests/std.rs index b294964770..73007a3705 100644 --- a/source/rust_verify_test/tests/std.rs +++ b/source/rust_verify_test/tests/std.rs @@ -57,7 +57,7 @@ test_verify_one_file! { fn foo(x: &X) { let y = x.clone(); } - } => Err(err) => assert_vir_error_msg(err, "`crate::X::clone` is not supported") + } => Err(err) => assert_vir_error_msg(err, "cannot call function marked `external`") } test_verify_one_file! { diff --git a/source/rust_verify_test/tests/traits.rs b/source/rust_verify_test/tests/traits.rs index 3a45d015b4..b6a8591d51 100644 --- a/source/rust_verify_test/tests/traits.rs +++ b/source/rust_verify_test/tests/traits.rs @@ -2845,7 +2845,7 @@ test_verify_one_file! { let x = 1 / 0; } } - } => Err(err) => assert_vir_error_msg(err, "an item in a trait impl cannot be marked external") + } => Err(err) => assert_vir_error_msg(err, "An individual item of a trait impl cannot be marked external") } test_verify_one_file! { From 00435a1f7122abb1d07d53f50dc246a25777ea22 Mon Sep 17 00:00:00 2001 From: Travis Hance Date: Tue, 29 Oct 2024 09:58:21 -0400 Subject: [PATCH 02/14] bugfix: Incorrect warning when using global size_of usize, fixes #1321 --- source/rust_verify/src/attributes.rs | 3 +++ source/rust_verify/src/external.rs | 1 + 2 files changed, 4 insertions(+) diff --git a/source/rust_verify/src/attributes.rs b/source/rust_verify/src/attributes.rs index 07356fecb2..7b43f5b9df 100644 --- a/source/rust_verify/src/attributes.rs +++ b/source/rust_verify/src/attributes.rs @@ -856,6 +856,7 @@ pub(crate) struct ExternalAttrs { pub(crate) sets_mode: bool, pub(crate) verify: bool, pub(crate) verus_macro: bool, + pub(crate) size_of_global: bool, pub(crate) any_other_verus_specific_attribute: bool, pub(crate) internal_get_field_many_variants: bool, } @@ -961,6 +962,7 @@ pub(crate) fn get_external_attrs( verify: false, sets_mode: false, verus_macro: false, + size_of_global: false, any_other_verus_specific_attribute: false, internal_get_field_many_variants: false, }; @@ -975,6 +977,7 @@ pub(crate) fn get_external_attrs( Attr::Verify => es.verify = true, Attr::Mode(_) => es.sets_mode = true, Attr::VerusMacro => es.verus_macro = true, + Attr::SizeOfGlobal => es.size_of_global = true, Attr::InternalGetFieldManyVariants => es.internal_get_field_many_variants = true, Attr::UnsupportedRustcAttr(..) => {} _ => { diff --git a/source/rust_verify/src/external.rs b/source/rust_verify/src/external.rs index 95ccb5d911..5b404432c5 100644 --- a/source/rust_verify/src/external.rs +++ b/source/rust_verify/src/external.rs @@ -215,6 +215,7 @@ fn opts_in_to_verus(eattrs: &ExternalAttrs) -> bool { || eattrs.external_type_specification || eattrs.external_trait_specification || eattrs.sets_mode + || eattrs.size_of_global } impl<'a, 'tcx> VisitMod<'a, 'tcx> { From f891a11c2cc8d0d2b126f86aba9a764b39620500 Mon Sep 17 00:00:00 2001 From: Travis Hance Date: Tue, 29 Oct 2024 10:28:09 -0400 Subject: [PATCH 03/14] bugfix: don't warn about 'trusted' attribute; fixes #1324 --- source/rust_verify/src/attributes.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/source/rust_verify/src/attributes.rs b/source/rust_verify/src/attributes.rs index 7b43f5b9df..c4962d6710 100644 --- a/source/rust_verify/src/attributes.rs +++ b/source/rust_verify/src/attributes.rs @@ -979,6 +979,7 @@ pub(crate) fn get_external_attrs( Attr::VerusMacro => es.verus_macro = true, Attr::SizeOfGlobal => es.size_of_global = true, Attr::InternalGetFieldManyVariants => es.internal_get_field_many_variants = true, + Attr::Trusted => {} Attr::UnsupportedRustcAttr(..) => {} _ => { es.any_other_verus_specific_attribute = true; From d52007c190e8fa457ef73f8647be6cf5c78f7091 Mon Sep 17 00:00:00 2001 From: Andrea Lattuada Date: Tue, 29 Oct 2024 13:46:59 +0100 Subject: [PATCH 04/14] allow `#[verifier(external_body)]` again on consts * add failing test for #1322 --- source/rust_verify/src/external.rs | 1 + source/rust_verify_test/tests/consts.rs | 15 +++++++++++++++ 2 files changed, 16 insertions(+) diff --git a/source/rust_verify/src/external.rs b/source/rust_verify/src/external.rs index 5b404432c5..8502c4806d 100644 --- a/source/rust_verify/src/external.rs +++ b/source/rust_verify/src/external.rs @@ -479,6 +479,7 @@ impl<'a> GeneralItem<'a> { ItemKind::Struct(..) => true, ItemKind::Enum(..) => true, ItemKind::Union(..) => true, + ItemKind::Const(..) => true, _ => false, }, GeneralItem::ForeignItem(_) => false, diff --git a/source/rust_verify_test/tests/consts.rs b/source/rust_verify_test/tests/consts.rs index 92647199c0..64479e3885 100644 --- a/source/rust_verify_test/tests/consts.rs +++ b/source/rust_verify_test/tests/consts.rs @@ -413,3 +413,18 @@ test_verify_one_file! { const A: usize = unimplemented!(); } => Err(err) => assert_rust_error_msg(err, "evaluation of constant value failed") } + +test_verify_one_file! { + #[test] allow_external_body_const_regression_1322_1 verus_code! { + #[verifier(external_body)] + const A: usize = unimplemented!(); + } => Ok(()) +} + +test_verify_one_file! { + // TODO un-ignore once fixed + #[ignore] #[test] allow_external_body_const_regression_1322_2 verus_code! { + #[verifier(external_body)] + const A: usize ensures 32 <= A <= 52 { unimplemented!() } + } => Ok(()) +} From 9bfb2f93958f473f744355edc60c79d48553f6c9 Mon Sep 17 00:00:00 2001 From: Travis Hance Date: Wed, 11 Dec 2024 20:38:26 -0500 Subject: [PATCH 05/14] rebase issues --- source/rust_verify/src/external.rs | 4 ++-- source/rust_verify/src/rust_to_vir.rs | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/source/rust_verify/src/external.rs b/source/rust_verify/src/external.rs index 8502c4806d..1e6b4d5b86 100644 --- a/source/rust_verify/src/external.rs +++ b/source/rust_verify/src/external.rs @@ -137,8 +137,8 @@ pub(crate) fn get_crate_items<'tcx>(ctxt: &Context<'tcx>) -> Result 0 { return Err(visitor.errors[0].clone()); diff --git a/source/rust_verify/src/rust_to_vir.rs b/source/rust_verify/src/rust_to_vir.rs index 369d0550b4..67e5e6cf1c 100644 --- a/source/rust_verify/src/rust_to_vir.rs +++ b/source/rust_verify/src/rust_to_vir.rs @@ -432,9 +432,9 @@ pub fn crate_to_vir<'a, 'tcx>( // Insert those modules into vir.modules let root_module_path = get_root_module_path(ctxt); if used_modules.contains(&root_module_path) { - let owner = ctxt.tcx.hir().owner(rustc_hir::CRATE_OWNER_ID); + let owner = ctxt.tcx.hir_owner_node(rustc_hir::CRATE_OWNER_ID); vir.modules.push(ctxt.spanned_new( - owner.span(), + *owner.span(), vir::ast::ModuleX { path: root_module_path.clone(), reveals: None }, )); } From 8dd5ce8abeaa7b472dfb97940e2a1157754ffd06 Mon Sep 17 00:00:00 2001 From: Travis Hance Date: Thu, 19 Dec 2024 20:35:19 -0500 Subject: [PATCH 06/14] work on opts_in_by_automatic_derive --- source/rust_verify/src/external.rs | 53 +++++++++++++++++++++++++++++- 1 file changed, 52 insertions(+), 1 deletion(-) diff --git a/source/rust_verify/src/external.rs b/source/rust_verify/src/external.rs index 1e6b4d5b86..5a418da316 100644 --- a/source/rust_verify/src/external.rs +++ b/source/rust_verify/src/external.rs @@ -221,6 +221,7 @@ fn opts_in_to_verus(eattrs: &ExternalAttrs) -> bool { impl<'a, 'tcx> VisitMod<'a, 'tcx> { fn visit_general(&mut self, general_item: GeneralItem<'tcx>, hir_id: HirId, span: Span) { let attrs = self.ctxt.tcx.hir().attrs(hir_id); + let eattrs = match self.ctxt.get_external_attrs(attrs) { Ok(eattrs) => eattrs, Err(err) => { @@ -248,7 +249,8 @@ impl<'a, 'tcx> VisitMod<'a, 'tcx> { VerifState::Default => { if eattrs.external { VerifState::External - } else if opts_in_to_verus(&eattrs) { + } else if opts_in_to_verus(&eattrs) + || opts_in_by_automatic_derive(&self.ctxt, &general_item, &attrs) { VerifState::Verify } else { VerifState::Default @@ -494,3 +496,52 @@ impl<'a> GeneralItem<'a> { } } } + +fn opts_in_by_automatic_derive<'tcx>( + ctxt: &Context<'tcx>, + general_item: &GeneralItem<'tcx>, + attrs: &[rustc_ast::Attribute], +) -> bool { + if is_automatically_derived(attrs) { + match general_item { + GeneralItem::Item(item) => match &item.kind { + ItemKind::Impl(impll) => { + let def_id = match impll.self_ty.kind { + rustc_hir::TyKind::Path(rustc_hir::QPath::Resolved(None, path)) => path.res.def_id(), + _ => { return false; } + }; + if let Some(local_def_id) = def_id.as_local() { + let hir_id = ctxt.tcx.local_def_id_to_hir_id(local_def_id); + let attrs = ctxt.tcx.hir().attrs(hir_id); + let eattrs = match ctxt.get_external_attrs(attrs) { + Ok(eattrs) => eattrs, + Err(_) => { return false; } + }; + opts_in_to_verus(&eattrs) + } else { + false + } + } + _ => false, + } + _ => false, + } + } else { + false + } +} + +fn is_automatically_derived(attrs: &[rustc_ast::Attribute]) -> bool { + for attr in attrs.iter() { + match &attr.kind { + rustc_ast::AttrKind::Normal(item) => match &item.item.path.segments[..] { + [segment] => if segment.ident.as_str() == "automatically_derived" { + return true; + } + _ => { } + } + _ => { } + } + } + false +} From 9f6503e665e338fb8fdf11164a012220a11214d5 Mon Sep 17 00:00:00 2001 From: Travis Hance Date: Sat, 11 Jan 2025 18:56:02 -0500 Subject: [PATCH 07/14] undo that --- source/rust_verify/src/external.rs | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/source/rust_verify/src/external.rs b/source/rust_verify/src/external.rs index 5a418da316..5b70f77590 100644 --- a/source/rust_verify/src/external.rs +++ b/source/rust_verify/src/external.rs @@ -249,8 +249,8 @@ impl<'a, 'tcx> VisitMod<'a, 'tcx> { VerifState::Default => { if eattrs.external { VerifState::External - } else if opts_in_to_verus(&eattrs) - || opts_in_by_automatic_derive(&self.ctxt, &general_item, &attrs) { + } else if opts_in_to_verus(&eattrs) { + //|| opts_in_by_automatic_derive(&self.ctxt, &general_item, &attrs) { VerifState::Verify } else { VerifState::Default @@ -497,6 +497,7 @@ impl<'a> GeneralItem<'a> { } } +/* fn opts_in_by_automatic_derive<'tcx>( ctxt: &Context<'tcx>, general_item: &GeneralItem<'tcx>, @@ -545,3 +546,4 @@ fn is_automatically_derived(attrs: &[rustc_ast::Attribute]) -> bool { } false } +*/ From 27519fbf9bde7b66dce84a14540c406863740dcc Mon Sep 17 00:00:00 2001 From: Travis Hance Date: Sat, 11 Jan 2025 19:32:31 -0500 Subject: [PATCH 08/14] fixes --- source/rust_verify/src/external.rs | 2 +- source/rust_verify/src/lib.rs | 2 +- source/rust_verify/src/lifetime_generate.rs | 8 ++++++-- source/rust_verify_test/tests/consts.rs | 11 ++++++++--- .../tests/external_fn_specification.rs | 2 +- source/rust_verify_test/tests/fndef_types.rs | 2 +- source/rust_verify_test/tests/std.rs | 2 +- 7 files changed, 19 insertions(+), 10 deletions(-) diff --git a/source/rust_verify/src/external.rs b/source/rust_verify/src/external.rs index 5b70f77590..a4d594e210 100644 --- a/source/rust_verify/src/external.rs +++ b/source/rust_verify/src/external.rs @@ -250,7 +250,7 @@ impl<'a, 'tcx> VisitMod<'a, 'tcx> { if eattrs.external { VerifState::External } else if opts_in_to_verus(&eattrs) { - //|| opts_in_by_automatic_derive(&self.ctxt, &general_item, &attrs) { + //|| opts_in_by_automatic_derive(&self.ctxt, &general_item, &attrs) { VerifState::Verify } else { VerifState::Default diff --git a/source/rust_verify/src/lib.rs b/source/rust_verify/src/lib.rs index d7cbda3065..3e3a99e163 100644 --- a/source/rust_verify/src/lib.rs +++ b/source/rust_verify/src/lib.rs @@ -42,8 +42,8 @@ pub mod def; pub mod driver; pub mod erase; mod expand_errors_driver; -pub mod externs; pub mod external; +pub mod externs; pub mod file_loader; mod fn_call_to_vir; mod hir_hide_reveal_rewrite; diff --git a/source/rust_verify/src/lifetime_generate.rs b/source/rust_verify/src/lifetime_generate.rs index cdf66bb0db..e53597cf95 100644 --- a/source/rust_verify/src/lifetime_generate.rs +++ b/source/rust_verify/src/lifetime_generate.rs @@ -2776,7 +2776,9 @@ pub(crate) fn gen_check_tracked_lifetimes<'tcx>( if let MaybeOwner::Owner(owner) = owner { match owner.node() { OwnerNode::Item(item) => { - if crate_items.is_item_external(item.item_id()) { + if !matches!(&item.kind, ItemKind::Impl(_)) + && crate_items.is_item_external(item.item_id()) + { // item is external continue; } @@ -2813,7 +2815,9 @@ pub(crate) fn gen_check_tracked_lifetimes<'tcx>( if let MaybeOwner::Owner(owner) = owner { match owner.node() { OwnerNode::Item(item) => { - if crate_items.is_item_external(item.item_id()) { + if !matches!(&item.kind, ItemKind::Impl(_)) + && crate_items.is_item_external(item.item_id()) + { // item is external continue; } diff --git a/source/rust_verify_test/tests/consts.rs b/source/rust_verify_test/tests/consts.rs index 64479e3885..36eea7ae58 100644 --- a/source/rust_verify_test/tests/consts.rs +++ b/source/rust_verify_test/tests/consts.rs @@ -416,15 +416,20 @@ test_verify_one_file! { test_verify_one_file! { #[test] allow_external_body_const_regression_1322_1 verus_code! { + #[verifier::external] + const fn stuff() -> usize { 0 } + #[verifier(external_body)] - const A: usize = unimplemented!(); + const A: usize = stuff(); } => Ok(()) } test_verify_one_file! { - // TODO un-ignore once fixed #[ignore] #[test] allow_external_body_const_regression_1322_2 verus_code! { + #[verifier::external] + const fn stuff() -> usize { 0 } + #[verifier(external_body)] - const A: usize ensures 32 <= A <= 52 { unimplemented!() } + const A: usize ensures 32 <= A <= 52 { stuff() } } => Ok(()) } diff --git a/source/rust_verify_test/tests/external_fn_specification.rs b/source/rust_verify_test/tests/external_fn_specification.rs index 86aaad6868..eb3cae4ec1 100644 --- a/source/rust_verify_test/tests/external_fn_specification.rs +++ b/source/rust_verify_test/tests/external_fn_specification.rs @@ -1275,7 +1275,7 @@ test_verify_one_file! { impl Tr for X { fn foo(&self) { } } - } => Err(err) => assert_vir_error_msg(err, "cannot call function marked `external`; try marking it `external_body` instead, or add a Verus specification via `external_fn_specification`") + } => Err(err) => assert_vir_error_msg(err, "cannot use function `crate::X::foo` which is ignored") } test_verify_one_file! { diff --git a/source/rust_verify_test/tests/fndef_types.rs b/source/rust_verify_test/tests/fndef_types.rs index 58af028b07..bae791f907 100644 --- a/source/rust_verify_test/tests/fndef_types.rs +++ b/source/rust_verify_test/tests/fndef_types.rs @@ -1702,7 +1702,7 @@ test_verify_one_file! { forall |a: Self, b: Self| call_ensures(Clone::clone, (&a,), b) ==> a == b, { assume(false); } } - } => Err(err) => assert_vir_error_msg(err, "Foo::clone` is not supported") + } => Err(err) => assert_vir_error_msg(err, "cannot use function `test_crate::Foo::clone` which is ignored") } test_verify_one_file! { diff --git a/source/rust_verify_test/tests/std.rs b/source/rust_verify_test/tests/std.rs index 73007a3705..c88390e890 100644 --- a/source/rust_verify_test/tests/std.rs +++ b/source/rust_verify_test/tests/std.rs @@ -57,7 +57,7 @@ test_verify_one_file! { fn foo(x: &X) { let y = x.clone(); } - } => Err(err) => assert_vir_error_msg(err, "cannot call function marked `external`") + } => Err(err) => assert_vir_error_msg(err, "cannot use function `crate::X::clone` which is ignored") } test_verify_one_file! { From 4f701b507f1201d900e5b0f1bcc9f7135857f78e Mon Sep 17 00:00:00 2001 From: Travis Hance Date: Sat, 11 Jan 2025 19:43:20 -0500 Subject: [PATCH 09/14] fix --- source/vstd/state_machine_internal.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/source/vstd/state_machine_internal.rs b/source/vstd/state_machine_internal.rs index a70155b079..8a6a5699ba 100644 --- a/source/vstd/state_machine_internal.rs +++ b/source/vstd/state_machine_internal.rs @@ -13,6 +13,7 @@ pub struct SyncSendIfSyncSend { _sync_send: super::prelude::SyncSendIfSyncSend, } +#[cfg_attr(verus_keep_ghost, verifier::verus_macro)] impl Clone for SyncSendIfSyncSend { #[cfg_attr(verus_keep_ghost, verifier::external_body)] fn clone(&self) -> Self { From 18e23fc12b638d49d7c5a4cc6fab0c23d3caf6ee Mon Sep 17 00:00:00 2001 From: Travis Hance Date: Sat, 11 Jan 2025 20:18:44 -0500 Subject: [PATCH 10/14] add is_item_explicitly_external for legacy behavior --- source/rust_verify/src/external.rs | 20 ++++++++++++++++++-- source/rust_verify/src/lifetime_generate.rs | 12 +++++++++++- source/rust_verify/src/rust_to_vir.rs | 4 ++-- 3 files changed, 31 insertions(+), 5 deletions(-) diff --git a/source/rust_verify/src/external.rs b/source/rust_verify/src/external.rs index a4d594e210..e8e3c227a8 100644 --- a/source/rust_verify/src/external.rs +++ b/source/rust_verify/src/external.rs @@ -68,7 +68,7 @@ pub enum VerifOrExternal { VerusAware { module_path: Path }, /// Path/String to refer to this item for diagnostics /// Path is an Option because there are some items we can't compute a Path for - External { path: Option, path_string: String }, + External { path: Option, path_string: String, explicit: bool }, } /// Abstracts over the different the different ItemX things in rust @@ -94,6 +94,18 @@ impl CrateItems { matches!(self.map.get(&item_id.owner_id), Some(VerifOrExternal::External { .. })) } + // TODO we should not be taking into consideration whether an item is + // "explicitly" external vs "implicitly" external. Rather, we should be treating these + // the same for consistency. + // Presently, we make this distinction in lifetime_generate, when determining whether + // to emit a trait impl. + pub(crate) fn is_item_explicitly_external(&self, item_id: ItemId) -> bool { + matches!( + self.map.get(&item_id.owner_id), + Some(VerifOrExternal::External { explicit: true, .. }) + ) + } + pub fn is_impl_item_external(&self, impl_item_id: ImplItemId) -> bool { matches!(self.map.get(&impl_item_id.owner_id), Some(VerifOrExternal::External { .. })) } @@ -301,7 +313,11 @@ impl<'a, 'tcx> VisitMod<'a, 'tcx> { Some(path) => vir::ast_util::path_as_friendly_rust_name(&path), None => format!("{:?}", def_id), }; - VerifOrExternal::External { path: path_opt, path_string } + VerifOrExternal::External { + path: path_opt, + path_string, + explicit: state_for_this_item == VerifState::External, + } }; self.items.push(CrateItem { id: general_item.id(), verif }); diff --git a/source/rust_verify/src/lifetime_generate.rs b/source/rust_verify/src/lifetime_generate.rs index e53597cf95..0a458bcc49 100644 --- a/source/rust_verify/src/lifetime_generate.rs +++ b/source/rust_verify/src/lifetime_generate.rs @@ -2503,7 +2503,7 @@ fn erase_impl<'tcx>( AssocItemKind::Type => { // handled in erase_trait } - _ => panic!("unexpected impl"), + _ => panic!("unexpected impl {:?}", impl_item_ref), } } } @@ -2776,6 +2776,11 @@ pub(crate) fn gen_check_tracked_lifetimes<'tcx>( if let MaybeOwner::Owner(owner) = owner { match owner.node() { OwnerNode::Item(item) => { + if matches!(&item.kind, ItemKind::Impl(_)) + && crate_items.is_item_explicitly_external(item.item_id()) + { + continue; + } if !matches!(&item.kind, ItemKind::Impl(_)) && crate_items.is_item_external(item.item_id()) { @@ -2815,6 +2820,11 @@ pub(crate) fn gen_check_tracked_lifetimes<'tcx>( if let MaybeOwner::Owner(owner) = owner { match owner.node() { OwnerNode::Item(item) => { + if matches!(&item.kind, ItemKind::Impl(_)) + && crate_items.is_item_explicitly_external(item.item_id()) + { + continue; + } if !matches!(&item.kind, ItemKind::Impl(_)) && crate_items.is_item_external(item.item_id()) { diff --git a/source/rust_verify/src/rust_to_vir.rs b/source/rust_verify/src/rust_to_vir.rs index 67e5e6cf1c..ba16e29cff 100644 --- a/source/rust_verify/src/rust_to_vir.rs +++ b/source/rust_verify/src/rust_to_vir.rs @@ -484,7 +484,7 @@ pub fn crate_to_vir<'a, 'tcx>( } } } - VerifOrExternal::External { path: Some(my_path), path_string: _ } => { + VerifOrExternal::External { path: Some(my_path), path_string: _, explicit: _ } => { // If possible, track this item in the VIR Krate for diagnostic purposes let (is_fn, is_datatype) = match crate_item.id { GeneralItemId::ItemId(item_id) => { @@ -520,7 +520,7 @@ pub fn crate_to_vir<'a, 'tcx>( vir.external_types.push(my_path.clone()); } } - VerifOrExternal::External { path: None, path_string: _ } => {} + VerifOrExternal::External { path: None, path_string: _, explicit: _ } => {} } } From 8d483ca53f7785335712da64c60d9c0eb8e03394 Mon Sep 17 00:00:00 2001 From: Travis Hance Date: Wed, 29 Jan 2025 15:02:07 +0100 Subject: [PATCH 11/14] rebase fixes --- source/rust_verify/src/external.rs | 6 +++--- source/rust_verify/src/rust_to_vir.rs | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/source/rust_verify/src/external.rs b/source/rust_verify/src/external.rs index e8e3c227a8..b9efb3ebb4 100644 --- a/source/rust_verify/src/external.rs +++ b/source/rust_verify/src/external.rs @@ -150,7 +150,7 @@ pub(crate) fn get_crate_items<'tcx>(ctxt: &Context<'tcx>) -> Result 0 { return Err(visitor.errors[0].clone()); @@ -416,12 +416,12 @@ fn emit_errors_warnings_for_ignored_attrs<'tcx>( } else if eattrs.external_fn_specification { diagnostics.push(VirErrAs::Warning(crate::util::err_span_bare( span, - format!("#[verifier::external_fn_specification] has no effect because item is already marked external"), + format!("an `assume_specification` declaration cannot be marked `external`"), ))); if eattrs.external { errors.push(crate::util::err_span_bare( span, - format!("a function cannot be marked both `external_fn_specification` and `external`"), + format!("an `assume_specification` declaration cannot be marked `external`"), )); } } else if eattrs.external_type_specification { diff --git a/source/rust_verify/src/rust_to_vir.rs b/source/rust_verify/src/rust_to_vir.rs index ba16e29cff..429cb5903d 100644 --- a/source/rust_verify/src/rust_to_vir.rs +++ b/source/rust_verify/src/rust_to_vir.rs @@ -434,7 +434,7 @@ pub fn crate_to_vir<'a, 'tcx>( if used_modules.contains(&root_module_path) { let owner = ctxt.tcx.hir_owner_node(rustc_hir::CRATE_OWNER_ID); vir.modules.push(ctxt.spanned_new( - *owner.span(), + owner.span(), vir::ast::ModuleX { path: root_module_path.clone(), reveals: None }, )); } From 08cf7d56bb6ecff14b7124d478d651e59b5eefff Mon Sep 17 00:00:00 2001 From: Travis Hance Date: Wed, 29 Jan 2025 15:36:09 +0100 Subject: [PATCH 12/14] fix --- source/rust_verify/src/lifetime_generate.rs | 23 +++++++++------------ 1 file changed, 10 insertions(+), 13 deletions(-) diff --git a/source/rust_verify/src/lifetime_generate.rs b/source/rust_verify/src/lifetime_generate.rs index 0a458bcc49..29d046caf0 100644 --- a/source/rust_verify/src/lifetime_generate.rs +++ b/source/rust_verify/src/lifetime_generate.rs @@ -2613,28 +2613,25 @@ fn erase_mir_datatype<'tcx>(ctxt: &Context<'tcx>, state: &mut State, id: DefId) } else { ctxt.tcx.item_attrs(id) }; - let vattrs = get_verifier_attrs(attrs, None).expect("get_verifier_attrs"); - if vattrs.external_type_specification { - return; - } let rust_item = verus_items::get_rust_item(ctxt.tcx, id); - - if let Some(RustItem::Box) = rust_item { - return; - } - let path = def_id_to_vir_path(ctxt.tcx, &ctxt.verus_items, id); - if let Some( - RustItem::Rc + if let Some(RustItem::Box + | RustItem::Rc | RustItem::Arc | RustItem::AllocGlobal | RustItem::ManuallyDrop | RustItem::PhantomData, - ) = rust_item - { + ) = rust_item { + return; + } + + let vattrs = get_verifier_attrs(attrs, None).expect("get_verifier_attrs"); + if vattrs.external_type_specification { return; } + let path = def_id_to_vir_path(ctxt.tcx, &ctxt.verus_items, id); + // Check if the struct is 'external_body' // (Recall that the 'external_body' label may have been applied by a proxy type, // so we can't check the vattrs of the datatype definition directly. From d2cd72d04f6d4e78cab09035cad876b9e09ba9e6 Mon Sep 17 00:00:00 2001 From: Travis Hance Date: Wed, 29 Jan 2025 15:43:01 +0100 Subject: [PATCH 13/14] fmt --- source/rust_verify/src/lifetime_generate.rs | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/source/rust_verify/src/lifetime_generate.rs b/source/rust_verify/src/lifetime_generate.rs index 29d046caf0..0fe97f9f14 100644 --- a/source/rust_verify/src/lifetime_generate.rs +++ b/source/rust_verify/src/lifetime_generate.rs @@ -2615,13 +2615,15 @@ fn erase_mir_datatype<'tcx>(ctxt: &Context<'tcx>, state: &mut State, id: DefId) }; let rust_item = verus_items::get_rust_item(ctxt.tcx, id); - if let Some(RustItem::Box + if let Some( + RustItem::Box | RustItem::Rc | RustItem::Arc | RustItem::AllocGlobal | RustItem::ManuallyDrop | RustItem::PhantomData, - ) = rust_item { + ) = rust_item + { return; } From 24f75e46ba0dfcd3052572d1d4b5b83042c24b67 Mon Sep 17 00:00:00 2001 From: Travis Hance Date: Mon, 10 Feb 2025 15:22:33 +0100 Subject: [PATCH 14/14] try to fix the external trait impls again --- source/rust_verify/src/external.rs | 12 ------------ source/rust_verify/src/lifetime_generate.rs | 14 +------------- 2 files changed, 1 insertion(+), 25 deletions(-) diff --git a/source/rust_verify/src/external.rs b/source/rust_verify/src/external.rs index b9efb3ebb4..48dd33c571 100644 --- a/source/rust_verify/src/external.rs +++ b/source/rust_verify/src/external.rs @@ -94,18 +94,6 @@ impl CrateItems { matches!(self.map.get(&item_id.owner_id), Some(VerifOrExternal::External { .. })) } - // TODO we should not be taking into consideration whether an item is - // "explicitly" external vs "implicitly" external. Rather, we should be treating these - // the same for consistency. - // Presently, we make this distinction in lifetime_generate, when determining whether - // to emit a trait impl. - pub(crate) fn is_item_explicitly_external(&self, item_id: ItemId) -> bool { - matches!( - self.map.get(&item_id.owner_id), - Some(VerifOrExternal::External { explicit: true, .. }) - ) - } - pub fn is_impl_item_external(&self, impl_item_id: ImplItemId) -> bool { matches!(self.map.get(&impl_item_id.owner_id), Some(VerifOrExternal::External { .. })) } diff --git a/source/rust_verify/src/lifetime_generate.rs b/source/rust_verify/src/lifetime_generate.rs index 0fe97f9f14..7c8804d531 100644 --- a/source/rust_verify/src/lifetime_generate.rs +++ b/source/rust_verify/src/lifetime_generate.rs @@ -2775,11 +2775,6 @@ pub(crate) fn gen_check_tracked_lifetimes<'tcx>( if let MaybeOwner::Owner(owner) = owner { match owner.node() { OwnerNode::Item(item) => { - if matches!(&item.kind, ItemKind::Impl(_)) - && crate_items.is_item_explicitly_external(item.item_id()) - { - continue; - } if !matches!(&item.kind, ItemKind::Impl(_)) && crate_items.is_item_external(item.item_id()) { @@ -2819,14 +2814,7 @@ pub(crate) fn gen_check_tracked_lifetimes<'tcx>( if let MaybeOwner::Owner(owner) = owner { match owner.node() { OwnerNode::Item(item) => { - if matches!(&item.kind, ItemKind::Impl(_)) - && crate_items.is_item_explicitly_external(item.item_id()) - { - continue; - } - if !matches!(&item.kind, ItemKind::Impl(_)) - && crate_items.is_item_external(item.item_id()) - { + if crate_items.is_item_external(item.item_id()) { // item is external continue; }