Merge pull request #894 from verus-lang/reapply-external-by-default

Make non-verus-macro items external by default (#771)
verus-lang · Nov 7, 2023 · 81ac467 · 81ac467
2 parents 03d7e5d + 526c72d
commit 81ac467
Show file tree

Hide file tree

Showing 19 changed files with 191 additions and 17 deletions.
diff --git a/source/builtin_macros/src/is_variant.rs b/source/builtin_macros/src/is_variant.rs
@@ -98,6 +98,7 @@ pub fn attribute_is_variant(
     quote! {
         #ast
 
+        #[verus::internal(verus_macro)]
         #[cfg(verus_keep_ghost)]
         #[automatically_derived]
         impl #impl_generics #struct_name #ty_generics #where_clause {

diff --git a/source/builtin_macros/src/syntax.rs b/source/builtin_macros/src/syntax.rs
@@ -2334,13 +2334,15 @@ impl VisitMut for Visitor {
     }
 
     fn visit_item_enum_mut(&mut self, item: &mut ItemEnum) {
+        item.attrs.push(mk_verus_attr(item.span(), quote! { verus_macro }));
         visit_item_enum_mut(self, item);
         item.attrs.extend(data_mode_attrs(&item.mode));
         item.mode = DataMode::Default;
         self.filter_attrs(&mut item.attrs);
     }
 
     fn visit_item_struct_mut(&mut self, item: &mut ItemStruct) {
+        item.attrs.push(mk_verus_attr(item.span(), quote! { verus_macro }));
         visit_item_struct_mut(self, item);
         item.attrs.extend(data_mode_attrs(&item.mode));
         item.mode = DataMode::Default;
@@ -2420,6 +2422,7 @@ impl VisitMut for Visitor {
     }
 
     fn visit_item_mod_mut(&mut self, item: &mut ItemMod) {
+        item.attrs.push(mk_verus_attr(item.span(), quote! { verus_macro }));
         if let Some((_, items)) = &mut item.content {
             self.visit_items_prefilter(items);
         }
@@ -2428,12 +2431,14 @@ impl VisitMut for Visitor {
     }
 
     fn visit_item_impl_mut(&mut self, imp: &mut ItemImpl) {
+        imp.attrs.push(mk_verus_attr(imp.span(), quote! { verus_macro }));
         self.visit_impl_items_prefilter(&mut imp.items, imp.trait_.is_some());
         self.filter_attrs(&mut imp.attrs);
         syn_verus::visit_mut::visit_item_impl_mut(self, imp);
     }
 
     fn visit_item_trait_mut(&mut self, tr: &mut ItemTrait) {
+        tr.attrs.push(mk_verus_attr(tr.span(), quote! { verus_macro }));
         self.visit_trait_items_prefilter(&mut tr.items);
         self.filter_attrs(&mut tr.attrs);
         syn_verus::visit_mut::visit_item_trait_mut(self, tr);

diff --git a/source/pervasive/atomic.rs b/source/pervasive/atomic.rs
@@ -37,6 +37,7 @@ macro_rules! make_unsigned_integer_atomic {
         } // verus!
 
         atomic_types!($at_ident, $p_ident, $p_data_ident, $rust_ty, $value_ty);
+        #[cfg_attr(verus_keep_ghost, verus::internal(verus_macro))]
         impl $at_ident {
             atomic_common_methods!($at_ident, $p_ident, $p_data_ident, $rust_ty, $value_ty);
             atomic_integer_methods!($at_ident, $p_ident, $rust_ty, $value_ty, $wrap_add, $wrap_sub);
@@ -71,6 +72,7 @@ macro_rules! make_signed_integer_atomic {
         } // verus!
 
         atomic_types!($at_ident, $p_ident, $p_data_ident, $rust_ty, $value_ty);
+        #[cfg_attr(verus_keep_ghost, verus::internal(verus_macro))]
         impl $at_ident {
             atomic_common_methods!($at_ident, $p_ident, $p_data_ident, $rust_ty, $value_ty);
             atomic_integer_methods!($at_ident, $p_ident, $rust_ty, $value_ty, $wrap_add, $wrap_sub);
@@ -82,6 +84,7 @@ macro_rules! make_signed_integer_atomic {
 macro_rules! make_bool_atomic {
     ($at_ident:ident, $p_ident:ident, $p_data_ident:ident, $rust_ty: ty, $value_ty: ty) => {
         atomic_types!($at_ident, $p_ident, $p_data_ident, $rust_ty, $value_ty);
+        #[cfg_attr(verus_keep_ghost, verus::internal(verus_macro))]
         impl $at_ident {
             atomic_common_methods!($at_ident, $p_ident, $p_data_ident, $rust_ty, $value_ty);
             atomic_bool_methods!($at_ident, $p_ident, $rust_ty, $value_ty);

diff --git a/source/pervasive/view.rs b/source/pervasive/view.rs
@@ -52,8 +52,10 @@ impl<A: View> View for alloc::sync::Arc<A> {
 
 macro_rules! declare_identity_view {
     ($t:ty) => {
+        #[cfg_attr(verus_keep_ghost, verifier::verify)]
         impl View for $t {
             type V = $t;
+
             #[cfg(verus_keep_ghost)]
             #[verus::internal(spec)]
             #[verus::internal(open)]
@@ -82,6 +84,7 @@ declare_identity_view!(isize);
 
 macro_rules! declare_tuple_view {
     ([$($n:tt)*], [$($a:ident)*]) => {
+        #[cfg_attr(verus_keep_ghost, verifier::verify)]
         impl<$($a: View, )*> View for ($($a, )*) {
             type V = ($($a::V, )*);
             #[cfg(verus_keep_ghost)]

diff --git a/source/rust_verify/example/state_machines/flat_combine.rs b/source/rust_verify/example/state_machines/flat_combine.rs
@@ -14,6 +14,8 @@ use state_machines_macros::tokenized_state_machine;
 // rather complicated to use, and it wasn't necessary.
 // Now, I expect storage to be a lot easier to use, easier than the alternative.
 
+verus! {
+
 pub struct Request {
     pub rid: int,
     pub req: int,
@@ -36,6 +38,8 @@ pub enum Combiner {
     Responding {elems: Seq<Option<int>>, idx: nat},
 }
 
+} // verus!
+
 tokenized_state_machine!{
     FlatCombiner {
         fields {

diff --git a/source/rust_verify/example/state_machines/petersons_algorithm.rs b/source/rust_verify/example/state_machines/petersons_algorithm.rs
@@ -3,6 +3,7 @@ use builtin_macros::*;
 use state_machines_macros::*;
 use vstd::prelude::*;
 
+#[verifier::verify]
 pub enum ThreadState {
     Idle,
     SetFlag,

diff --git a/source/rust_verify/example/state_machines/rwlock.rs b/source/rust_verify/example/state_machines/rwlock.rs
@@ -9,6 +9,7 @@ use vstd::cell::*;
 use state_machines_macros::tokenized_state_machine;
 
 // TODO make T generic
+#[verifier::verify]
 pub struct T {
     t: u8,
 }

diff --git a/source/rust_verify/src/attributes.rs b/source/rust_verify/src/attributes.rs
@@ -199,6 +199,8 @@ pub(crate) enum Attr {
     ExternalBody,
     // don't parse function; function can't be called directly from verified code
     External,
+    // opposite of External; verify item even if it's declared without VerusMacro
+    Verify,
     // hide body (from all modules) until revealed
     Opaque,
     // publish body?
@@ -329,6 +331,7 @@ pub(crate) fn parse_attrs(
                 AttrTree::Fun(_, arg, None) if arg == "verus_macro" => v.push(Attr::VerusMacro),
                 AttrTree::Fun(_, arg, None) if arg == "external_body" => v.push(Attr::ExternalBody),
                 AttrTree::Fun(_, arg, None) if arg == "external" => v.push(Attr::External),
+                AttrTree::Fun(_, arg, None) if arg == "verify" => v.push(Attr::Verify),
                 AttrTree::Fun(_, arg, None) if arg == "opaque" => v.push(Attr::Opaque),
                 AttrTree::Fun(_, arg, None) if arg == "publish" => {
                     report_deprecated("publish");
@@ -638,6 +641,7 @@ 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<bool>,
     pub(crate) opaque_outside_module: bool,
@@ -664,11 +668,25 @@ pub(crate) struct VerifierAttrs {
     pub(crate) external_fn_specification: bool,
     pub(crate) external_type_specification: bool,
     pub(crate) unwrapped_binding: bool,
+    pub(crate) sets_mode: bool,
     pub(crate) internal_reveal_fn: bool,
     pub(crate) trusted: bool,
     pub(crate) size_of_global: 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.verify
+                || self.sets_mode)
+    }
+}
+
 pub(crate) fn get_verifier_attrs(
     attrs: &[Attribute],
     diagnostics: Option<&mut Vec<VirErrAs>>,
@@ -677,6 +695,7 @@ pub(crate) fn get_verifier_attrs(
         verus_macro: false,
         external_body: false,
         external: false,
+        verify: false,
         opaque: false,
         publish: None,
         opaque_outside_module: false,
@@ -702,6 +721,7 @@ pub(crate) fn get_verifier_attrs(
         external_fn_specification: false,
         external_type_specification: false,
         unwrapped_binding: false,
+        sets_mode: false,
         internal_reveal_fn: false,
         trusted: false,
         size_of_global: false,
@@ -711,6 +731,7 @@ pub(crate) fn get_verifier_attrs(
             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::Opaque => vs.opaque = true,
@@ -746,11 +767,26 @@ pub(crate) fn get_verifier_attrs(
             Attr::Memoize => vs.memoize = true,
             Attr::Truncate => vs.truncate = true,
             Attr::UnwrappedBinding => vs.unwrapped_binding = true,
+            Attr::Mode(_) => vs.sets_mode = true,
             Attr::InternalRevealFn => vs.internal_reveal_fn = true,
             Attr::Trusted => vs.trusted = true,
             Attr::SizeOfGlobal => vs.size_of_global = true,
             _ => {}
         }
     }
+    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}",));
+            }
+        }
+    }
     Ok(vs)
 }
diff --git a/source/rust_verify/src/config.rs b/source/rust_verify/src/config.rs
@@ -53,6 +53,7 @@ pub struct ArgsX {
     pub verify_root: bool,
     pub verify_module: Vec<String>,
     pub verify_function: Option<String>,
+    pub no_external_by_default: bool,
     pub no_verify: bool,
     pub no_lifetime: bool,
     pub no_auto_recommends_check: bool,
@@ -131,6 +132,7 @@ pub fn parse_args_with_imports(
     const OPT_VERIFY_ROOT: &str = "verify-root";
     const OPT_VERIFY_MODULE: &str = "verify-module";
     const OPT_VERIFY_FUNCTION: &str = "verify-function";
+    const OPT_NO_EXTERNAL_BY_DEFAULT: &str = "no-external-by-default";
     const OPT_NO_VERIFY: &str = "no-verify";
     const OPT_NO_LIFETIME: &str = "no-lifetime";
     const OPT_NO_AUTO_RECOMMENDS_CHECK: &str = "no-auto-recommends-check";
@@ -235,6 +237,7 @@ pub fn parse_args_with_imports(
         "Verify just one function within the one module specified by verify-module or verify-root, \nmatches on unique substring (foo) or wildcards at ends of the argument (*foo, foo*, *foo*)",
         "MODULE",
     );
+    opts.optflag("", OPT_NO_EXTERNAL_BY_DEFAULT, "(deprecated) Verify all items, even those declared outside the verus! macro, and even if they aren't marked #[verifier::verify]");
     opts.optflag("", OPT_NO_VERIFY, "Do not run verification");
     opts.optflag("", OPT_NO_LIFETIME, "Do not run lifetime checking on proofs");
     opts.optflag(
@@ -395,6 +398,7 @@ pub fn parse_args_with_imports(
         import: import,
         verify_module: matches.opt_strs(OPT_VERIFY_MODULE),
         verify_function: matches.opt_str(OPT_VERIFY_FUNCTION),
+        no_external_by_default: matches.opt_present(OPT_NO_EXTERNAL_BY_DEFAULT),
         no_verify: matches.opt_present(OPT_NO_VERIFY),
         no_lifetime: matches.opt_present(OPT_NO_LIFETIME),
         no_auto_recommends_check: matches.opt_present(OPT_NO_AUTO_RECOMMENDS_CHECK),

diff --git a/source/rust_verify/src/context.rs b/source/rust_verify/src/context.rs
@@ -22,6 +22,7 @@ type ErasureInfoRef = std::rc::Rc<std::cell::RefCell<ErasureInfo>>;
 pub type Context<'tcx> = Arc<ContextX<'tcx>>;
 #[derive(Clone)]
 pub struct ContextX<'tcx> {
+    pub(crate) cmd_line_args: crate::config::Args,
     pub(crate) tcx: TyCtxt<'tcx>,
     pub(crate) krate: &'tcx Crate<'tcx>,
     pub(crate) erasure_info: ErasureInfoRef,

diff --git a/source/rust_verify/src/lifetime.rs b/source/rust_verify/src/lifetime.rs
@@ -199,13 +199,15 @@ fn index<'a, V, Idx, Output>(v: &'a V, index: Idx) -> &'a Output { panic!() }
 ";
 
 fn emit_check_tracked_lifetimes<'tcx>(
+    cmd_line_args: crate::config::Args,
     tcx: TyCtxt<'tcx>,
     verus_items: std::sync::Arc<VerusItems>,
     krate: &'tcx Crate<'tcx>,
     emit_state: &mut EmitState,
     erasure_hints: &ErasureHints,
 ) -> State {
     let gen_state = crate::lifetime_generate::gen_check_tracked_lifetimes(
+        cmd_line_args,
         tcx,
         verus_items,
         krate,
@@ -295,6 +297,7 @@ pub fn lifetime_rustc_driver(rustc_args: &[String], rust_code: String) {
 }
 
 pub(crate) fn check_tracked_lifetimes<'tcx>(
+    cmd_line_args: crate::config::Args,
     tcx: TyCtxt<'tcx>,
     verus_items: std::sync::Arc<VerusItems>,
     spans: &SpanContext,
@@ -303,8 +306,14 @@ pub(crate) fn check_tracked_lifetimes<'tcx>(
 ) -> Result<Vec<Message>, VirErr> {
     let krate = tcx.hir().krate();
     let mut emit_state = EmitState::new();
-    let gen_state =
-        emit_check_tracked_lifetimes(tcx, verus_items, krate, &mut emit_state, erasure_hints);
+    let gen_state = emit_check_tracked_lifetimes(
+        cmd_line_args,
+        tcx,
+        verus_items,
+        krate,
+        &mut emit_state,
+        erasure_hints,
+    );
     let mut rust_code: String = String::new();
     for line in &emit_state.lines {
         rust_code.push_str(&line.text);

diff --git a/source/rust_verify/src/lifetime_generate.rs b/source/rust_verify/src/lifetime_generate.rs
@@ -41,6 +41,7 @@ impl TypX {
 }
 
 struct Context<'tcx> {
+    cmd_line_args: crate::config::Args,
     tcx: TyCtxt<'tcx>,
     verus_items: Arc<VerusItems>,
     types_opt: Option<&'tcx TypeckResults<'tcx>>,
@@ -1926,7 +1927,7 @@ fn erase_impl<'tcx>(
                 let id = owner_id.to_def_id();
                 let attrs = ctxt.tcx.hir().attrs(impl_item.hir_id());
                 let vattrs = get_verifier_attrs(attrs, None).expect("get_verifier_attrs");
-                if vattrs.external {
+                if vattrs.is_external(&ctxt.cmd_line_args) {
                     continue;
                 }
                 match &kind {
@@ -2172,12 +2173,14 @@ fn erase_mir_datatype<'tcx>(ctxt: &Context<'tcx>, state: &mut State, id: DefId)
 }
 
 pub(crate) fn gen_check_tracked_lifetimes<'tcx>(
+    cmd_line_args: crate::config::Args,
     tcx: TyCtxt<'tcx>,
     verus_items: Arc<VerusItems>,
     krate: &'tcx Crate<'tcx>,
     erasure_hints: &ErasureHints,
 ) -> State {
     let mut ctxt = Context {
+        cmd_line_args,
         tcx,
         verus_items,
         types_opt: None,
@@ -2309,13 +2312,19 @@ 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::Const(_ty, body_id) | ItemKind::Static(_ty, _, body_id) => {
-                            if vattrs.size_of_global {
+                            if vattrs.size_of_global || vattrs.is_external(&ctxt.cmd_line_args) {
                                 continue;
                             }
                             erase_const_or_static(
@@ -2330,6 +2339,9 @@ 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.external_fn_specification {
                                 erase_fn(
                                     krate,
@@ -2369,9 +2381,15 @@ pub(crate) fn gen_check_tracked_lifetimes<'tcx>(
                             _bounds,
                             trait_items,
                         ) => {
+                            if vattrs.is_external(&ctxt.cmd_line_args) {
+                                continue;
+                            }
                             erase_trait_methods(krate, &mut ctxt, &mut state, id, trait_items);
                         }
                         ItemKind::Impl(impll) => {
+                            if vattrs.is_external(&ctxt.cmd_line_args) {
+                                continue;
+                            }
                             erase_impl(krate, &mut ctxt, &mut state, id, impll);
                         }
                         ItemKind::OpaqueTy(OpaqueTy {