Add #[verifier::allow(...)] to suppress warnings

source/rust_verify/src/attributes.rs

@@ -296,6 +296,8 @@ pub(crate) enum Attr {
     Memoize,
     // Override default rlimit
     RLimit(f32),
+    // suppress warning
+    Allow(String),
     // Suppress the recommends check for narrowing casts that may truncate
     Truncate,
     // In order to apply a specification to a method externally
@@ -619,6 +621,9 @@ pub(crate) fn parse_attrs(
                     let number = get_rlimit_arg(*span, attrs)?;
                     v.push(Attr::RLimit(number));
                 }
+                AttrTree::Fun(_, arg, Some(box [AttrTree::Fun(_, s, None)])) if arg == "allow" => {
+                    v.push(Attr::Allow(s.clone()))
+                }
                 AttrTree::Fun(_, arg, None) if arg == "truncate" => v.push(Attr::Truncate),
                 AttrTree::Fun(_, arg, None) if arg == "external_fn_specification" => {
                     v.push(Attr::ExternalFnSpecification)
@@ -879,6 +884,60 @@ pub(crate) fn parse_attrs_walk_parents<'tcx>(
     }
 }
 
+fn is_allow_walk_parents<'tcx>(
+    tcx: rustc_middle::ty::TyCtxt<'tcx>,
+    def_id: rustc_span::def_id::DefId,
+    allow: &str,
+) -> bool {
+    for attr in parse_attrs_walk_parents(tcx, def_id) {
+        if let Attr::Allow(s) = attr {
+            if s == allow {
+                return true;
+            }
+        }
+    }
+    false
+}
+
+struct WarningDefId<'tcx>(rustc_middle::ty::TyCtxt<'tcx>, rustc_span::def_id::DefId);
+
+impl<'tcx> vir::messages::CheckAllowForWarning for WarningDefId<'tcx> {
+    fn allowed(&self, s: &str) -> bool {
+        let WarningDefId(tcx, def_id) = *self;
+        is_allow_walk_parents(tcx, def_id, s)
+    }
+}
+
+pub(crate) fn warning_maybe<'tcx, S: Into<String>>(
+    tcx: rustc_middle::ty::TyCtxt<'tcx>,
+    def_id: rustc_span::def_id::DefId,
+    span: Span,
+    allow: &str,
+    note: impl FnOnce() -> S,
+    emit: impl FnOnce(vir::messages::Message) -> (),
+) {
+    vir::messages::warning_maybe(
+        &WarningDefId(tcx, def_id),
+        &crate::spans::err_air_span(span),
+        allow,
+        note,
+        emit,
+    );
+}
+
+pub(crate) fn warning_config_walk_parents<'tcx>(
+    tcx: rustc_middle::ty::TyCtxt<'tcx>,
+    def_id: rustc_span::def_id::DefId,
+) -> vir::context::WarningConfig {
+    let mut allows = Vec::new();
+    for attr in parse_attrs_walk_parents(tcx, def_id) {
+        if let Attr::Allow(s) = attr {
+            allows.push(s.clone());
+        }
+    }
+    vir::context::WarningConfig(allows)
+}
+
 pub(crate) fn get_loop_isolation_walk_parents<'tcx>(
     tcx: rustc_middle::ty::TyCtxt<'tcx>,
     def_id: rustc_span::def_id::DefId,
@@ -1092,6 +1151,7 @@ pub(crate) struct VerifierAttrs {
     pub(crate) allow_complex_invariants: bool,
     pub(crate) memoize: bool,
     pub(crate) rlimit: Option<f32>,
+    pub(crate) allow_list: Vec<String>,
     pub(crate) truncate: bool,
     pub(crate) external_fn_specification: bool,
     pub(crate) external_type_specification: bool,
@@ -1267,6 +1327,7 @@ pub(crate) fn get_verifier_attrs_maybe_check(
         allow_complex_invariants: false,
         memoize: false,
         rlimit: None,
+        allow_list: vec![],
         truncate: false,
         external_fn_specification: false,
         external_type_specification: false,
@@ -1351,6 +1412,7 @@ pub(crate) fn get_verifier_attrs_maybe_check(
             Attr::Memoize => vs.memoize = true,
             Attr::RLimit(rlimit) => vs.rlimit = Some(rlimit),
             Attr::Truncate => vs.truncate = true,
+            Attr::Allow(name) => vs.allow_list.push(name.clone()),
             Attr::UnwrappedBinding => vs.unwrapped_binding = true,
             Attr::Mode(_) => vs.sets_mode = true,
             Attr::InternalRevealFn => vs.internal_reveal_fn = true,

source/rust_verify/src/automatic_derive.rs

@@ -64,6 +64,8 @@ pub fn is_automatically_derived(attrs: &[rustc_hir::Attribute]) -> bool {
 
 pub fn modify_derived_item<'tcx>(
     ctxt: &Context<'tcx>,
+    id: rustc_span::def_id::DefId,
+    inputs: &Vec<rustc_middle::ty::Ty>,
     span: Span,
     hir_id: HirId,
     action: &AutomaticDeriveAction,
@@ -75,7 +77,7 @@ pub fn modify_derived_item<'tcx>(
     match special {
         SpecialTrait::Clone => {
             if &*function.name.path.last_segment() == "clone" {
-                return clone_add_post_condition(ctxt, span, hir_id, function);
+                return clone_add_post_condition(ctxt, id, inputs, span, hir_id, function);
             }
         }
     }
@@ -84,14 +86,30 @@ pub fn modify_derived_item<'tcx>(
 
 fn clone_add_post_condition<'tcx>(
     ctxt: &Context<'tcx>,
+    mut id: rustc_span::def_id::DefId,
+    inputs: &Vec<rustc_middle::ty::Ty>,
     span: Span,
     hir_id: HirId,
     functionx: &mut FunctionX,
 ) -> Result<(), VirErr> {
+    if inputs.len() >= 1 {
+        use rustc_middle::ty::{AdtDef, TyKind};
+        if let TyKind::Ref(_, t, _) = inputs[0].kind() {
+            if let TyKind::Adt(AdtDef(adt_def_data), _) = t.kind() {
+                // It's more convenient to put verifier::allow on the datatype than on the function
+                id = adt_def_data.did;
+            }
+        }
+    }
     let warn = |msg: &str| {
-        ctxt.diagnostics
-            .borrow_mut()
-            .push(VirErrAs::Warning(crate::util::err_span_bare(span, msg.to_string())));
+        crate::attributes::warning_maybe(
+            ctxt.tcx,
+            id,
+            span,
+            "autoderive_clone_without_spec",
+            || msg,
+            |msg| ctxt.diagnostics.borrow_mut().push(VirErrAs::Warning(msg)),
+        );
     };
     let warn_unexpected = || {
         warn(

source/rust_verify/src/context.rs

@@ -47,7 +47,7 @@ pub struct ContextX<'tcx> {
     pub(crate) arch_word_bits: Option<vir::ast::ArchWordBits>,
     pub(crate) crate_name: Ident,
     pub(crate) vstd_crate_name: Ident,
-    pub(crate) name_def_id_map: Rc<RefCell<std::collections::HashMap<Path, DefId>>>,
+    pub(crate) name_def_id_map: Rc<RefCell<HashMap<Path, DefId>>>,
     pub(crate) next_read_kind_id: AtomicU64,
 }
 
@@ -257,4 +257,14 @@ impl<'tcx> BodyCtxt<'tcx> {
     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: &str,
+        note: impl FnOnce() -> S,
+        emit: impl FnOnce(vir::messages::Message) -> (),
+    ) {
+        crate::attributes::warning_maybe(self.ctxt.tcx, self.fun_id, span, allow, note, emit);
+    }
 }

source/rust_verify/src/external.rs

@@ -652,12 +652,14 @@ fn get_attributes_for_automatic_derive<'tcx>(
     span: Span,
 ) -> Option<ExternalAttrs> {
     let warn_unknown = || {
-        ctxt.diagnostics.borrow_mut().push(VirErrAs::Warning(crate::util::err_span_bare(
+        crate::attributes::warning_maybe(
+            ctxt.tcx,
+            general_item.id().owner_id().to_def_id(),
             span,
-            format!(
-                "Verus doesn't known how to handle this automatically derived item; ignoring it"
-            ),
-        )));
+            "unknown_automatic_derive",
+            || "Verus doesn't known how to handle this automatically derived item; ignoring it",
+            |msg| ctxt.diagnostics.borrow_mut().push(VirErrAs::Warning(msg)),
+        );
     };
 
     if !crate::automatic_derive::is_automatically_derived(attrs) {