Add vstd/contrib and builtin_macros/src/contrib directories (#1813)

* Add vstd/contrib and builtin_macros/src/contrib directories, with contrib/auto_spec example

* Document process for adding contrib macros

* Fix comment

Author: Chris-Hawblitzel

source/builtin_macros/src/contrib/auto_spec.rs

@@ -0,0 +1,82 @@
+use verus_syn::visit_mut::VisitMut;
+use verus_syn::{Block, Expr, ImplItem, Item, parse_quote_spanned, spanned::Spanned};
+
+struct Visitor;
+
+fn is_verus_proof_stmt(stmt: &verus_syn::Stmt) -> bool {
+    // remove proof-related macros (similar to dual_spec macro)
+    use verus_syn::{Expr, ExprUnary, UnOp};
+    match stmt {
+        verus_syn::Stmt::Expr(e, _) => match e {
+            Expr::Assume(..) => true,
+            Expr::Assert(..) => true,
+            Expr::AssertForall(..) => true,
+            Expr::Unary(ExprUnary { op: UnOp::Proof(..), .. }) => true,
+            _ => false,
+        },
+        _ => false,
+    }
+}
+
+impl VisitMut for Visitor {
+    fn visit_expr_mut(&mut self, expr: &mut Expr) {
+        verus_syn::visit_mut::visit_expr_mut(self, expr);
+        use verus_syn::{BinOp, Expr, ExprBinary};
+        let span = expr.span();
+        match expr {
+            Expr::Binary(ExprBinary { op, left, right, .. }) => {
+                match op {
+                    BinOp::Add(_) => {
+                        *expr = parse_quote_spanned_builtin!(builtin, span => #builtin::add(#left, #right));
+                    }
+                    BinOp::Sub(_) => {
+                        *expr = parse_quote_spanned_builtin!(builtin, span => #builtin::sub(#left, #right));
+                    }
+                    BinOp::Mul(_) => {
+                        *expr = parse_quote_spanned_builtin!(builtin, span => #builtin::mul(#left, #right));
+                    }
+                    _ => {}
+                }
+            }
+            _ => {}
+        }
+    }
+
+    fn visit_block_mut(&mut self, block: &mut Block) {
+        block.stmts.retain(|stmt| !is_verus_proof_stmt(stmt));
+        verus_syn::visit_mut::visit_block_mut(self, block);
+    }
+}
+
+fn auto_spec_fn(
+    span: proc_macro2::Span,
+    attrs: &mut Vec<verus_syn::Attribute>,
+    sig: &mut verus_syn::Signature,
+    mut block: Block,
+) {
+    attrs.push(parse_quote_spanned!(span => #[verifier::allow_in_spec]));
+    Visitor.visit_block_mut(&mut block);
+    sig.spec.returns = Some(parse_quote_spanned!(span => returns (#block)));
+}
+
+pub(crate) fn auto_spec_item(
+    item: &mut Item,
+    _args: Option<proc_macro2::TokenStream>,
+    _new_items: &mut Vec<Item>,
+) {
+    if let Item::Fn(f) = item {
+        let span = f.span();
+        auto_spec_fn(span, &mut f.attrs, &mut f.sig, *f.block.clone());
+    }
+}
+
+pub(crate) fn auto_spec_impl_item(
+    item: &mut ImplItem,
+    _args: Option<proc_macro2::TokenStream>,
+    _new_items: &mut Vec<ImplItem>,
+) {
+    if let ImplItem::Fn(f) = item {
+        let span = f.span();
+        auto_spec_fn(span, &mut f.attrs, &mut f.sig, f.block.clone());
+    }
+}

source/builtin_macros/src/contrib/mod.rs

@@ -0,0 +1,136 @@
+pub mod auto_spec;
+
+use proc_macro2::TokenStream;
+use verus_syn::{Attribute, ImplItem, Item, Meta, Path};
+
+fn item_attrs(item: &Item) -> Option<&Vec<Attribute>> {
+    match item {
+        Item::Const(i) => Some(&i.attrs),
+        Item::Enum(i) => Some(&i.attrs),
+        Item::ExternCrate(i) => Some(&i.attrs),
+        Item::Fn(i) => Some(&i.attrs),
+        Item::ForeignMod(i) => Some(&i.attrs),
+        Item::Impl(i) => Some(&i.attrs),
+        Item::Macro(i) => Some(&i.attrs),
+        Item::Mod(i) => Some(&i.attrs),
+        Item::Static(i) => Some(&i.attrs),
+        Item::Struct(i) => Some(&i.attrs),
+        Item::Trait(i) => Some(&i.attrs),
+        Item::TraitAlias(i) => Some(&i.attrs),
+        Item::Type(i) => Some(&i.attrs),
+        Item::Union(i) => Some(&i.attrs),
+        Item::Use(i) => Some(&i.attrs),
+        Item::Global(i) => Some(&i.attrs),
+        Item::BroadcastUse(i) => Some(&i.attrs),
+        Item::BroadcastGroup(i) => Some(&i.attrs),
+        Item::AssumeSpecification(i) => Some(&i.attrs),
+        Item::Verbatim(_) => None,
+        _ => {
+            panic!("Item is non_exhaustive, preventing us from catching this panic statically")
+        }
+    }
+}
+
+fn impl_item_attrs(item: &ImplItem) -> Option<&Vec<Attribute>> {
+    match item {
+        ImplItem::Const(i) => Some(&i.attrs),
+        ImplItem::Fn(i) => Some(&i.attrs),
+        ImplItem::Type(i) => Some(&i.attrs),
+        ImplItem::Macro(i) => Some(&i.attrs),
+        ImplItem::BroadcastGroup(i) => Some(&i.attrs),
+        ImplItem::Verbatim(_) => None,
+        _ => {
+            panic!("ImplItem is non_exhaustive, preventing us from catching this panic statically")
+        }
+    }
+}
+
+fn traverse_path(path: &Path) -> Option<String> {
+    if path.leading_colon.is_some() {
+        return None;
+    }
+    let segments: Vec<String> = path.segments.iter().map(|s| s.ident.to_string()).collect();
+    let segments: Vec<&str> = segments.iter().map(|s| s.as_str()).collect();
+    match &segments[..] {
+        [s] => Some(s.to_string()),
+        ["contrib", s] => Some(s.to_string()),
+        ["vstd", "contrib", s] => Some(s.to_string()),
+        _ => None,
+    }
+}
+
+fn collect_attrs(attrs: Option<&Vec<Attribute>>) -> Vec<(String, Option<TokenStream>)> {
+    let Some(attrs) = attrs else {
+        return vec![];
+    };
+    let mut attr_infos: Vec<(String, Option<TokenStream>)> = Vec::new();
+    for attr in attrs {
+        let Some(name) = traverse_path(attr.path()) else {
+            continue;
+        };
+        let tokens = match &attr.meta {
+            Meta::Path(_) => None,
+            Meta::List(list) => Some(list.tokens.clone()),
+            Meta::NameValue(_) => None,
+        };
+        attr_infos.push((name, tokens));
+    }
+    attr_infos
+}
+
+// It's often more useful to apply a macro to a verus_syn::Item before it's transformed
+// by "verus!" into a verbose syn encoding.
+// For example, we may want to look for "proof { ... }" blocks or change the mode of a Fn,
+// and it's better to do these directly in verus_syn syntax than to try to reverse engineer
+// the syn encoding of these features.
+// Therefore, we give contrib macros a chance to preprocess the verus_syn code here.
+
+// Unfortunately, name resolution hasn't run on item's attributes yet,
+// so we don't have a good way to identify which macro is which.
+// As a hack, we look for any of:
+// - #[vstd::contrib::m(args)]
+// - #[contrib::m(args)]
+// - #[m(args)]
+// where m is on the list of contrib macros and (args) is optional.
+
+pub(crate) fn contrib_preprocess_item(item: &mut Item, new_items: &mut Vec<Item>) {
+    for (name, tokens) in collect_attrs(item_attrs(item)) {
+        match name.as_str() {
+            // Add contrib macros needing preprocessing here:
+            "auto_spec" => auto_spec::auto_spec_item(item, tokens, new_items),
+            _ => {}
+        };
+    }
+}
+
+pub(crate) fn contrib_preprocess_impl_item(item: &mut ImplItem, new_items: &mut Vec<ImplItem>) {
+    for (name, tokens) in collect_attrs(impl_item_attrs(item)) {
+        match name.as_str() {
+            // Add contrib macros needing preprocessing here:
+            "auto_spec" => auto_spec::auto_spec_impl_item(item, tokens, new_items),
+            _ => {}
+        }
+    }
+}
+
+pub(crate) fn contrib_preprocess_items(items: &mut Vec<Item>) {
+    let mut i = 0;
+    while i < items.len() {
+        let mut new_items: Vec<Item> = Vec::new();
+        contrib_preprocess_item(&mut items[i], &mut new_items);
+        // Add new items and preprocess the new items as well:
+        items.extend(new_items);
+        i += 1;
+    }
+}
+
+pub(crate) fn contrib_preprocess_impl_items(items: &mut Vec<ImplItem>) {
+    let mut i = 0;
+    while i < items.len() {
+        let mut new_items: Vec<ImplItem> = Vec::new();
+        contrib_preprocess_impl_item(&mut items[i], &mut new_items);
+        // Add new items and preprocess the new items as well:
+        items.extend(new_items);
+        i += 1;
+    }
+}

source/builtin_macros/src/lib.rs

@@ -16,6 +16,7 @@ mod atomic_ghost;
 mod attr_block_trait;
 mod attr_rewrite;
 mod calc_macro;
+mod contrib;
 mod enum_synthesize;
 mod fndecl;
 mod is_variant;
@@ -377,3 +378,48 @@ pub fn proof_decl(input: proc_macro::TokenStream) -> proc_macro::TokenStream {
 }
 
 /*** End of verus small macro definition for executable items ***/
+
+/*** Start of contrib proc macros
+(unfortunately, proc macros must reside at the root of the crate)
+
+To add a contrib proc macro, complete the following steps:
+- Add a file in builtin_macros/src/contrib/ that contains the bulk of the macro implementation
+  (example: builtin_macros/src/contrib/auto_spec.rs)
+- Declare the file as a submodule of builtin_macros::contrib by adding "pub mod ..." to the top of
+  builtin_macros/src/contrib/mod.rs (example: `pub mod auto_spec;`)
+- Add a short macro declaration below, calling into your file in builtin_macros/src/contrib
+  for any complex work (i.e. the macro declaration below should have a body of at most a few lines)
+- Add a "pub use" to vstd/contrib/mod.rs (example: `pub use verus_builtin_macros::auto_spec;`)
+
+If your macro needs to manipulate function signatures or function bodies,
+it's generally cleaner to write this manipulation on the verus_syn representation of the function
+before it is transformed by `verus!`, rather than trying to manipulate the more complicated output
+of `verus!`.  To work with the verus_syn representation, complete this additional step:
+- In builtin_macros/src/contrib/mod.rs,
+  edit contrib_preprocess_item and/or contrib_preprocess_impl_item to match on your macro name and
+  call into your code that processes the verus_syn item or impl_item.  Example:
+  `"auto_spec" => auto_spec::auto_spec_item(item, tokens, new_items),`.
+  Your code can then edit the item/impl_item in place.
+  It can also optionally emit new items/impl_items by adding them to new_items.
+***/
+
+/// This copies the body of an exec function into a "returns" clause,
+/// so that the exec function will be also usable as a spec function.
+/// For example,
+///   `#[vstd::contrib::auto_spec] fn f(u: u8) -> u8 { u / 2 }`
+/// becomes:
+///   `#[verifier::allow_in_spec] fn f(u: u8) -> u8 returns (u / 2) { u / 2 }`
+/// The macro performs some limited fixups, such as removing proof blocks
+/// and turning +, -, and * into add, sub, mul.
+/// However, only a few such fixups are currently implemented and not all exec bodies
+/// will be usable as return clauses, so this macro will not work on all exec functions.
+#[proc_macro_attribute]
+pub fn auto_spec(
+    _args: proc_macro::TokenStream,
+    input: proc_macro::TokenStream,
+) -> proc_macro::TokenStream {
+    // All the work is done in the preprocesssing; this just double-checks name resolution
+    input
+}
+
+/*** End of contrib macros ***/

source/builtin_macros/src/syntax.rs

@@ -1373,6 +1373,7 @@ impl Visitor {
     }
 
     fn visit_items_prefilter(&mut self, items: &mut Vec<Item>) {
+        crate::contrib::contrib_preprocess_items(items);
         self.visit_items_make_unerased_proxies(items);
         crate::syntax_trait::expand_extension_traits(self.erase_ghost.erase_all(), items);
 
@@ -1847,6 +1848,7 @@ impl Visitor {
     }
 
     fn visit_impl_items_prefilter(&mut self, items: &mut Vec<ImplItem>, for_trait: bool) {
+        crate::contrib::contrib_preprocess_impl_items(items);
         self.visit_impl_items_make_unerased_proxies(items, for_trait);
 
         if self.erase_ghost.erase_all() {

source/rust_verify_test/tests/contrib.rs

@@ -0,0 +1,84 @@
+#![feature(rustc_private)]
+#[macro_use]
+mod common;
+use common::*;
+
+// Adapted from auto_spec tests in syntax_attr.rs
+test_verify_one_file! {
+    #[test] test_auto_spec verus_code! {
+        #[vstd::contrib::auto_spec]
+        pub fn f(x: u32, y: u32) -> u32
+            requires
+                x < 100,
+                y < 100,
+        {
+            proof {
+                assert(true);
+            }
+            x + y
+        }
+
+        #[vstd::contrib::auto_spec]
+        pub fn f2(x: u32) -> u32
+            requires
+                x < 100,
+        {
+            f(x, 1)
+        }
+
+        struct S;
+
+        impl S {
+            #[vstd::contrib::auto_spec]
+            fn foo(&self, x: u32) -> u32 {
+                x / 2
+            }
+        }
+
+        proof fn lemma_f(x: u32, y: u32)
+            requires
+                x < 100,
+            ensures
+                y == 1 ==> f(x, y) == f2(x),
+                f(x, y) == f(y, x),
+                f2(x) == f2(x),
+                f(x, y) == (x + y) as u32,
+                f2(x) == x + 1,
+        {}
+
+        mod inner {
+            use super::*;
+            proof fn lemma_f(x: u32)
+                requires
+                    x < 100,
+                ensures
+                    f2(x) == (x + 1),
+            {}
+        }
+    } => Ok(())
+}
+
+test_verify_one_file_with_options! {
+    #[test] test_auto_spec_missing_use  ["no-auto-import-verus_builtin"] => verus_code! {
+        // fails if we don't say "use vstd::contrib::auto_spec;"
+        #[auto_spec]
+        fn foo(x: u32) -> u32 {
+            x / 2
+        }
+    } => Err(e) => assert_vir_error_msg(e, "cannot find attribute `auto_spec` in this scope")
+}
+
+test_verify_one_file! {
+    #[test] test_auto_spec_unsupported_body verus_code! {
+        use vstd::contrib::auto_spec;
+        #[auto_spec]
+        fn f(x: &mut u32, y: u32) -> u32
+            requires
+                x < 100,
+                y < 100,
+        {
+            *x = *x + y;
+            *x
+        }
+    } => Err(e) => assert_vir_error_msg(e, "The verifier does not yet support the following Rust feature")
+}

source/vstd/contrib/mod.rs

@@ -0,0 +1 @@
+pub use verus_builtin_macros::auto_spec;