use unerased proxies for associated consts and statics (#1793)

Author: tjhance

source/builtin_macros/src/lib.rs

@@ -25,6 +25,7 @@ mod struct_decl_inv;
 mod structural;
 mod syntax_trait;
 mod topological_sort;
+mod unerased_proxies;
 
 decl_derive!([Structural] => structural::derive_structural);
 

source/builtin_macros/src/syntax.rs

@@ -36,7 +36,6 @@ use syn_verus::{
 };
 
 pub(crate) const VERUS_SPEC: &str = "VERUS_SPEC__";
-const VERUS_UNERASED_PROXY: &str = "VERUS_UNERASED_PROXY__";
 
 fn take_expr(expr: &mut Expr) -> Expr {
     let dummy: Expr = Expr::Verbatim(TokenStream::new());
@@ -69,8 +68,8 @@ enum InsideArith {
     Fixed,
 }
 
-struct Visitor {
-    erase_ghost: EraseGhost,
+pub(crate) struct Visitor {
+    pub(crate) erase_ghost: EraseGhost,
     // TODO: this should always be true
     use_spec_traits: bool,
     // inside_ghost > 0 means we're currently visiting ghost code
@@ -94,7 +93,7 @@ struct Visitor {
     assign_to: bool,
 
     // Add extra verus signature information to the docstring
-    rustdoc: bool,
+    pub(crate) rustdoc: bool,
 }
 
 // For exec "let pat = init" declarations, recursively find Tracked(x), Ghost(x), x in pat
@@ -463,10 +462,6 @@ fn merge_default_ensures(
 }
 
 impl Visitor {
-    fn needs_unerased_proxies(&self) -> bool {
-        self.erase_ghost.keep() && !self.rustdoc
-    }
-
     fn take_ghost<T: Default>(&self, dest: &mut T) -> T {
         take_ghost(self.erase_ghost, dest)
     }
@@ -511,8 +506,7 @@ impl Visitor {
         spec: &mut SignatureSpec,
         ret_pat: Option<(Pat, TType)>,
         final_ret_pat: Option<Pat>, // Some(pat) if different from ret_pat,
-        is_const: bool,
-        span: Span,
+        _span: Span,
     ) -> Vec<Stmt> {
         let requires = self.take_ghost(&mut spec.requires);
         let recommends = self.take_ghost(&mut spec.recommends);
@@ -741,16 +735,7 @@ impl Visitor {
             }
         }
 
-        if is_const {
-            vec![Stmt::Expr(
-                Expr::Verbatim(
-                    quote_spanned!(span => #[verus::internal(const_header_wrapper)] || { #(#spec_stmts)* };),
-                ),
-                None,
-            )]
-        } else {
-            spec_stmts
-        }
+        spec_stmts
     }
 
     fn visit_fn(
@@ -945,8 +930,7 @@ impl Visitor {
         self.inside_ghost += 1; // for requires, ensures, etc.
 
         let sig_span = sig.span().clone();
-        let spec_stmts =
-            self.take_sig_specs(&mut sig.spec, ret_pat, None, sig.constness.is_some(), sig_span);
+        let spec_stmts = self.take_sig_specs(&mut sig.spec, ret_pat, None, sig_span);
         if !self.erase_ghost.erase() {
             stmts.extend(spec_stmts);
         }
@@ -992,36 +976,14 @@ impl Visitor {
                 })));
             }
         } else {
-            let ensures = self.take_ghost(con_ensures);
-            if let Some(Ensures { token, mut exprs, attrs }) = ensures {
-                self.inside_ghost += 1;
-                let mut stmts: Vec<Stmt> = Vec::new();
-                if attrs.len() > 0 {
-                    let err = "outer attributes only allowed on function's ensures";
-                    let expr = Expr::Verbatim(quote_spanned!(token.span => compile_error!(#err)));
-                    stmts.push(Stmt::Expr(expr, Some(Semi { spans: [token.span] })));
-                } else if exprs.exprs.len() > 0 {
-                    for expr in exprs.exprs.iter_mut() {
-                        self.visit_expr_mut(expr);
-                    }
-                    // Use a closure in the ensures to avoid circular const definition.
-                    // Note: we can't use con.ident as the closure pattern,
-                    // because Rust would treat this as a const path pattern.
-                    // So we use a 0-parameter closure.
-                    stmts.push(stmt_with_semi!(builtin, token.span => #[verus::internal(const_header_wrapper)] || { #builtin::ensures(|| [#exprs]); }));
-                }
-                let mut block = std::mem::take(con_block).expect("const-with-ensures block");
-                block.stmts.splice(0..0, stmts);
-                *con_block = Some(block);
-                self.inside_ghost -= 1;
-            }
             if let Some(block) = std::mem::take(con_block) {
                 let expr_block = syn_verus::ExprBlock { attrs: vec![], label: None, block: *block };
                 *con_expr = Some(Box::new(Expr::Block(expr_block)));
                 *con_eq_token = Some(syn_verus::token::Eq { spans: [con_span] });
                 *con_semi_token = Some(Semi { spans: [con_span] });
             }
         }
+        *con_ensures = None;
     }
 
     fn visit_const_or_static(
@@ -1791,161 +1753,9 @@ impl Visitor {
         }
     }
 
-    fn item_needs_unerased_proxy(&self, item: &Item) -> bool {
-        match item {
-            Item::Const(item_const) => !is_external(&item_const.attrs),
-            Item::Fn(item_fn) => item_fn.sig.constness.is_some() && !is_external(&item_fn.attrs),
-            _ => false,
-        }
-    }
-
-    fn item_translate_const_to_0_arg_fn(&self, item: Item) -> Item {
-        match item {
-            Item::Const(item_const) => {
-                let span = item_const.span();
-                let ItemConst {
-                    mut attrs,
-                    vis,
-                    const_token,
-                    ident,
-                    generics,
-                    colon_token,
-                    ty,
-                    eq_token: _,
-                    expr,
-                    semi_token: _,
-                    publish,
-                    mode,
-                    ensures,
-                    block,
-                } = item_const;
-                attrs.push(mk_verus_attr(span, quote! { encoded_const }));
-
-                let publish = match (publish, &mode, &vis) {
-                    (publish, _, Visibility::Inherited) => publish,
-                    (
-                        Publish::Default,
-                        FnMode::Spec(_) | FnMode::SpecChecked(_) | FnMode::Default,
-                        _,
-                    ) => Publish::Open(syn_verus::Open { token: token::Open { span } }),
-                    (publish, _, _) => publish,
-                };
-
-                Item::Fn(ItemFn {
-                    attrs,
-                    vis,
-                    sig: Signature {
-                        spec: SignatureSpec {
-                            prover: None,
-                            requires: None,
-                            recommends: None,
-                            ensures,
-                            default_ensures: None,
-                            returns: None,
-                            decreases: None,
-                            invariants: None,
-                            unwind: None,
-                            with: None,
-                        },
-                        publish,
-                        constness: None,
-                        asyncness: None,
-                        unsafety: None,
-                        abi: None,
-                        broadcast: None,
-                        mode: mode,
-                        fn_token: token::Fn { span: const_token.span },
-                        ident: ident.clone(),
-                        generics,
-                        paren_token: Paren { span: into_spans(colon_token.span) },
-                        inputs: Punctuated::new(),
-                        variadic: None,
-                        output: ReturnType::Type(
-                            token::RArrow { spans: [colon_token.span, colon_token.span] },
-                            None,
-                            None, /*
-                                  Some(Box::new((
-                                      Paren { span: into_spans(colon_token.span) },
-                                      Pat::Verbatim(quote!{ #ident }),
-                                      colon_token,
-                                  ))), */
-                            ty,
-                        ),
-                    },
-                    block: (match block {
-                        Some(block) => block,
-                        _ => {
-                            let expr = expr.unwrap();
-                            Box::new(Block {
-                                brace_token: Brace { span: into_spans(expr.span()) },
-                                stmts: vec![Stmt::Expr(*expr, None)],
-                            })
-                        }
-                    }),
-                    semi_token: None,
-                })
-            }
-            item => item,
-        }
-    }
-
-    fn item_make_proxy(&self, item: Item) -> Item {
-        let mut item = item;
-        item = self.item_translate_const_to_0_arg_fn(item);
-        match &mut item {
-            Item::Fn(item_fn) => {
-                item_fn.sig.ident = Ident::new(
-                    &format!("{}{}", VERUS_UNERASED_PROXY, &item_fn.sig.ident),
-                    item_fn.sig.span(),
-                );
-                item_fn.attrs.push(mk_verus_attr(item_fn.span(), quote! { unerased_proxy }));
-            }
-            _ => unreachable!(),
-        }
-        item
-    }
-
-    fn item_make_external_and_erased(&mut self, item: Item) -> Item {
-        let mut item = item;
-
-        self.erase_ghost = EraseGhost::Erase;
-        self.visit_item_mut(&mut item);
-        self.erase_ghost = EraseGhost::Keep;
-
-        let span = item.span();
-        let attributes = match &mut item {
-            Item::Fn(item_fn) => &mut item_fn.attrs,
-            Item::Const(item_const) => &mut item_const.attrs,
-            _ => unreachable!(),
-        };
-        attributes.push(mk_verifier_attr(span, quote! { external }));
-        attributes.push(mk_verus_attr(span, quote! { uses_unerased_proxy }));
-
-        item
-    }
-
-    fn visit_items_make_unerased_proxies(&mut self, items: &mut Vec<Item>) {
-        if !self.needs_unerased_proxies() {
-            return;
-        }
-
-        let mut new_items = vec![];
-
-        for item in std::mem::take(items).into_iter() {
-            if self.item_needs_unerased_proxy(&item) {
-                let proxy = self.item_make_proxy(item.clone());
-                let erased = self.item_make_external_and_erased(item);
-                new_items.push(proxy);
-                new_items.push(erased);
-            } else {
-                new_items.push(item);
-            }
-        }
-
-        *items = new_items;
-    }
-
     fn visit_impl_items_prefilter(&mut self, items: &mut Vec<ImplItem>, for_trait: bool) {
+        self.visit_impl_items_make_unerased_proxies(items, for_trait);
+
         if self.erase_ghost.erase_all() {
             items.retain(|item| match item {
                 ImplItem::Fn(fun) => match fun.sig.mode {
@@ -4816,13 +4626,7 @@ pub(crate) fn sig_specs_attr(
         rustdoc: env_rustdoc(),
     };
     let sig_span = sig.span().clone();
-    spec_stmts.extend(visitor.take_sig_specs(
-        &mut spec,
-        ret_pat,
-        final_ret_pat,
-        sig.constness.is_some(),
-        sig_span,
-    ));
+    spec_stmts.extend(visitor.take_sig_specs(&mut spec, ret_pat, final_ret_pat, sig_span));
     spec_stmts
 }