finish sanity check

Author: tjhance

source/rust_verify/src/attributes.rs

@@ -961,6 +961,7 @@ pub(crate) struct ExternalAttrs {
     pub(crate) verify: bool,
     pub(crate) verus_macro: bool,
     pub(crate) size_of_global: bool,
+    pub(crate) item_broadcast_use: bool,
     pub(crate) any_other_verus_specific_attribute: bool,
     pub(crate) internal_get_field_many_variants: bool,
     pub(crate) external_auto_derives: AutoDerivesAttr,
@@ -1079,6 +1080,7 @@ pub(crate) fn get_external_attrs(
         sets_mode: false,
         verus_macro: false,
         size_of_global: false,
+        item_broadcast_use: false,
         any_other_verus_specific_attribute: false,
         internal_get_field_many_variants: false,
         external_auto_derives: AutoDerivesAttr::Regular,
@@ -1096,6 +1098,7 @@ pub(crate) fn get_external_attrs(
             Attr::Mode(_) => es.sets_mode = true,
             Attr::VerusMacro => es.verus_macro = true,
             Attr::SizeOfGlobal => es.size_of_global = true,
+            Attr::ItemBroadcastUse => es.item_broadcast_use = true,
             Attr::InternalGetFieldManyVariants => es.internal_get_field_many_variants = true,
             Attr::Trusted => {}
             Attr::ExternalAutoDerives(None) => {

source/rust_verify/src/erase.rs

@@ -10,10 +10,11 @@ use crate::verus_items::{DummyCaptureItem, VerusItem, VerusItems};
 use rustc_hir::def_id::LocalDefId;
 use rustc_mir_build_verus::verus::{
     BodyErasure, CallErasure, ExpectSpec, ExpectSpecArgs, NodeErase, VarErasure, VerusErasureCtxt,
-    set_verus_erasure_ctxt,
+    set_verus_aware_def_ids, set_verus_erasure_ctxt,
 };
 use rustc_span::Span;
 use std::collections::HashMap;
+use std::collections::HashSet;
 use std::sync::Arc;
 use vir::ast::VirErr;
 
@@ -320,3 +321,27 @@ pub(crate) fn setup_verus_ctxt_for_thir_erasure(
 
     Ok(())
 }
+
+pub(crate) fn setup_verus_aware_ids(crate_items: &crate::external::CrateItems) {
+    // Requirements:
+    //  - If a function requires Verus-erasure, then it MUST be in the set
+    //  - If a function has special properties (e.g., being const), that may cause Rust
+    //    to run mir_borrowck on it before Verus mode-checking, then it MUST NOT be in the set.
+    // For anything else: it doesn't matter.
+    //
+    // Since most consts are marked external, we can just use the VerusAware set for this.
+    // We carve out exceptions for some special directives.
+
+    let mut s = HashSet::<LocalDefId>::new();
+    for item in crate_items.items.iter() {
+        match &item.verif {
+            crate::external::VerifOrExternal::VerusAware { const_directive, .. } => {
+                if !*const_directive {
+                    s.insert(item.id.owner_id().def_id);
+                }
+            }
+            crate::external::VerifOrExternal::External { .. } => {}
+        }
+    }
+    set_verus_aware_def_ids(Arc::new(s));
+}

source/rust_verify/src/external.rs

@@ -70,7 +70,7 @@ pub struct CrateItem {
 #[derive(Debug, Clone)]
 pub enum VerifOrExternal {
     /// Path is the *module path* containing this item
-    VerusAware { module_path: Path },
+    VerusAware { module_path: Path, const_directive: bool },
     /// 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>, path_string: String, explicit: bool },
@@ -324,7 +324,10 @@ impl<'a, 'tcx> VisitMod<'a, 'tcx> {
         // Append this item to the items
 
         let verif = if state_for_this_item == VerifState::Verify {
-            VerifOrExternal::VerusAware { module_path: self.module_path.clone() }
+            VerifOrExternal::VerusAware {
+                module_path: self.module_path.clone(),
+                const_directive: eattrs.size_of_global || eattrs.item_broadcast_use,
+            }
         } else {
             let path_opt =
                 def_id_to_vir_path_option(self.ctxt.tcx, Some(&self.ctxt.verus_items), def_id);
@@ -424,8 +427,10 @@ impl<'a, 'tcx> VisitMod<'a, 'tcx> {
                         "In order to verify any items of this trait impl, the entire impl must be verified. Try wrapping the entire impl in the `verus!` macro.",
                     ));
                 } else {
-                    self.items[this_item_idx].verif =
-                        VerifOrExternal::VerusAware { module_path: self.module_path.clone() }
+                    self.items[this_item_idx].verif = VerifOrExternal::VerusAware {
+                        module_path: self.module_path.clone(),
+                        const_directive: false,
+                    }
                 }
             }
         }

source/rust_verify/src/rust_to_vir.rs

@@ -417,7 +417,7 @@ pub fn crate_to_vir<'a, 'tcx>(
     let mut used_modules = HashSet::<Path>::new();
     for crate_item in crate_items.items.iter() {
         match &crate_item.verif {
-            VerifOrExternal::VerusAware { module_path } => {
+            VerifOrExternal::VerusAware { module_path, const_directive: _ } => {
                 used_modules.insert(module_path.clone());
             }
             _ => {}
@@ -461,7 +461,7 @@ pub fn crate_to_vir<'a, 'tcx>(
 
     for crate_item in crate_items.items.iter() {
         match &crate_item.verif {
-            VerifOrExternal::VerusAware { module_path } => {
+            VerifOrExternal::VerusAware { module_path, const_directive: _ } => {
                 match crate_item.id {
                     GeneralItemId::ItemId(item_id) => {
                         let item = ctxt.tcx.hir_item(item_id);

source/rust_verify/src/verifier.rs

@@ -2627,6 +2627,10 @@ impl Verifier {
         diagnostics: &impl air::messages::Diagnostics,
         crate_name: String,
     ) -> Result<bool, (VirErr, Vec<vir::ast::VirErrAs>)> {
+        if self.args.no_lifetime {
+            rustc_mir_build_verus::verus::set_verus_aware_def_ids(Arc::new(HashSet::new()));
+        }
+
         self.air_no_span = {
             let no_span = tcx
                 .hir_crate(())
@@ -2694,6 +2698,9 @@ impl Verifier {
             |err: VirErr| (err, ctxt_diagnostics.borrow_mut().drain(..).collect());
 
         let crate_items = crate::external::get_crate_items(&ctxt).map_err(map_err_diagnostics)?;
+        if !self.args.no_lifetime {
+            crate::erase::setup_verus_aware_ids(&crate_items);
+        }
 
         let time_hir0 = Instant::now();
 
@@ -2702,11 +2709,6 @@ impl Verifier {
             return Ok(false);
         }
 
-        tcx.ensure_ok().check_private_in_public(());
-        tcx.hir_for_each_module(|module| {
-            tcx.ensure_ok().check_mod_privacy(module);
-        });
-
         let time_hir1 = Instant::now();
         self.time_hir = time_hir1 - time_hir0;
 

source/rustc_mir_build/src/thir/cx/mod.rs

@@ -27,6 +27,9 @@ pub(crate) fn thir_body(
     if let Some(reported) = cx.typeck_results.tainted_by_errors {
         return Err(reported);
     }
+
+    crate::verus::check_this_query_isnt_running_early(owner_def);
+
     let expr = if crate::verus::erase_body(&mut cx, owner_def) {
         crate::verus::erase_tree(&mut cx, body.value)
     } else {

source/rustc_mir_build_additional_files/verus.rs

@@ -115,10 +115,18 @@ static VERUS_AWARE_DEF_IDS: RwLock<Option<Arc<HashSet<LocalDefId>>>> = RwLock::n
 /// Used to communicate the VerusErasureCtxt
 static VERUS_ERASURE_CTXT: RwLock<Option<Arc<VerusErasureCtxt>>> = RwLock::new(None);
 
+pub fn set_verus_aware_def_ids(ids: Arc<HashSet<LocalDefId>>) {
+    let v: &mut Option<Arc<HashSet<LocalDefId>>> = &mut VERUS_AWARE_DEF_IDS.write().unwrap();
+    if v.is_some() {
+        panic!("VERUS_AWARE_DEF_IDS has already been set");
+    }
+    *v = Some(ids);
+}
+
 pub fn set_verus_erasure_ctxt(erasure_ctxt: Arc<VerusErasureCtxt>) {
     let v: &mut Option<Arc<VerusErasureCtxt>> = &mut VERUS_ERASURE_CTXT.write().unwrap();
     if v.is_some() {
-        panic!("VerusErasureCtxt has already been set");
+        panic!("VERUS_ERASURE_CTXT has already been set");
     }
     *v = Some(erasure_ctxt);
 }
@@ -136,9 +144,9 @@ fn get_verus_erasure_ctxt_option() -> Option<Arc<VerusErasureCtxt>> {
     VERUS_ERASURE_CTXT.read().unwrap().clone()
 }
 
-/// Our erasure scheme will fail if this query runs too early, before we initialize the VerusErasureCtxt.
-/// However, there are some items (e.g. consts) where this happens intentionally because consts may be evaluated
-/// during type-checking.
+/// Our erasure scheme will fail if this query runs too early, before we initialize the
+/// VerusErasureCtxt. However, there are some items where this happens
+/// intentionally (e.g., for consts, which may be evaluated during type-checking).
 ///
 /// rust_verify needs to follow the scheme:
 ///
@@ -147,22 +155,23 @@ fn get_verus_erasure_ctxt_option() -> Option<Arc<VerusErasureCtxt>> {
 ///  3. initialize the VERUS_ERASURE_CTXT
 ///  4. Run lifetime checking
 ///
-/// As a result, thir_body is able to sanity check we're in a consistent state. If the VERUS_ERASURE_CTXT
-/// hasn't been initialized yet, we check that the given item is one that doesn't need it.
-fn check_this_query_isnt_running_early(local_def_id: LocalDefId) {
+/// As a result, thir_body is able to sanity check we're in a consistent state.
+/// If the VERUS_ERASURE_CTXT hasn't been initialized yet, we check that the given
+/// item is one that doesn't need it.
+pub(crate) fn check_this_query_isnt_running_early(local_def_id: LocalDefId) {
     if get_verus_erasure_ctxt_option().is_none() {
         match VERUS_AWARE_DEF_IDS.read().unwrap().clone() {
             Some(m) => {
                 if m.contains(&local_def_id) {
                     panic!(
-                        "Internal Verus Error: The thir_body query is running for item {:?} which may require erasure, but the VerusErasureCtxt has not been initialized. Please file a github issue for this error and consider using `--no-lifetime` to work around the issue.",
+                        "Internal Verus Error: The thir_body query is running for item {:?} which may require erasure, but the VerusErasureCtxt has not been initialized. Please file a github issue for this error and consider using `--no-lifetime` as a temperary measure to work around the issue.",
                         local_def_id
                     );
                 }
             }
             None => {
                 panic!(
-                    "Internal Verus Error: The thir_body query is running for item {:?}, but the VerusAwareDefIds map has not been initialized. Please file a github issue for this error and consider using `--no-lifetime` to work around the issue.",
+                    "Internal Verus Error: The thir_body query is running for item {:?}, but the VerusAwareDefIds map has not been initialized. Please file a github issue for this error and consider using `--no-lifetime` as a temporary measure to work around the issue.",
                     local_def_id
                 );
             }
@@ -277,7 +286,7 @@ impl ExpectSpecArgs {
             ExpectSpecArgs::AllNo => ExpectSpec::No,
             ExpectSpecArgs::AllYes => ExpectSpec::Yes,
             ExpectSpecArgs::AllPropagate => ExpectSpec::Propagate,
-            ExpectSpecArgs::PerArg(args) => args[args.len() - 1],
+            ExpectSpecArgs::PerArg(args) => *args.last().unwrap(),
         }
     }
 }