[verus_spec] avoid rewrite exec code when external/external_body (verus-lang#2317)

Author: ziqiaozhou

source/builtin_macros/src/attr_rewrite.rs

@@ -43,7 +43,7 @@ use syn::{Expr, Item, ItemConst, parse2, spanned::Spanned};
 use crate::{
     EraseGhost,
     attr_block_trait::{AnyAttrBlock, AnyFnOrLoop},
-    syntax::{self, mk_verifier_attr_syn, mk_verus_attr_syn},
+    syntax::{self, has_external_code_syn, mk_verifier_attr_syn, mk_verus_attr_syn},
     syntax_trait,
     unerased_proxies::VERUS_UNERASED_PROXY,
 };
@@ -159,7 +159,7 @@ pub(crate) fn rewrite_verus_attribute(
                 spec_f.sig.ident = ident.clone();
                 spec_f.attrs = vec![mk_verus_attr_syn(f.span(), quote! { spec })];
                 // remove proof-related macros
-                replace_block(EraseGhost::Erase, spec_f.block_mut().unwrap());
+                replace_block(EraseGhost::Erase, spec_f.block_mut().unwrap(), false);
                 spec_fun = Some(spec_f);
 
                 attributes
@@ -194,6 +194,7 @@ pub(crate) fn rewrite_verus_attribute(
 
 struct ExecReplacer {
     erase: EraseGhost,
+    inside_external_code: bool,
 }
 
 impl VisitMut for ExecReplacer {
@@ -202,7 +203,7 @@ impl VisitMut for ExecReplacer {
     fn visit_macro_mut(&mut self, mac: &mut syn::Macro) {
         syn::visit_mut::visit_macro_mut(self, mac);
         // Only replace in verification mode
-        if !self.erase.keep() {
+        if !self.erase.keep() || self.inside_external_code {
             return;
         }
         if let Some(x) = mac.path.segments.first_mut() {
@@ -291,7 +292,7 @@ impl VisitMut for ExecReplacer {
     fn visit_expr_for_loop_mut(&mut self, for_loop: &mut syn::ExprForLoop) {
         syn::visit_mut::visit_expr_for_loop_mut(self, for_loop);
 
-        if !self.erase.keep() {
+        if !self.erase.keep() || self.inside_external_code {
             return;
         }
 
@@ -370,13 +371,17 @@ fn is_verus_proof_stmt(stmt: &syn::Stmt) -> bool {
 // TODO: when tracked/ghost is supported, we need to clear verus-related
 // attributes for expression so that unverfied `cargo build` does not need to
 // enable unstable feature for macro.
-pub(crate) fn replace_block(erase: EraseGhost, fblock: &mut syn::Block) {
-    let mut replacer = ExecReplacer { erase };
+pub(crate) fn replace_block(
+    erase: EraseGhost,
+    fblock: &mut syn::Block,
+    inside_external_code: bool,
+) {
+    let mut replacer = ExecReplacer { erase, inside_external_code };
     replacer.visit_block_mut(fblock);
 }
 
 pub(crate) fn replace_expr(erase: EraseGhost, expr: &mut syn::Expr) {
-    let mut replacer = ExecReplacer { erase };
+    let mut replacer = ExecReplacer { erase, inside_external_code: false };
     replacer.visit_expr_mut(expr);
 }
 
@@ -637,7 +642,8 @@ pub(crate) fn rewrite_verus_spec_on_fun_or_loop(
             let _ = fun.block_mut().unwrap().stmts.splice(0..0, new_stmts);
 
             // Parse and replace proof_xxx!() inside function and replace panic.
-            replace_block(erase, fun.block_mut().unwrap());
+            let inside_external_code = has_external_code_syn(&fun.attrs);
+            replace_block(erase, fun.block_mut().unwrap(), inside_external_code);
             fun.to_tokens(&mut new_stream);
             proc_macro::TokenStream::from(new_stream)
         }
@@ -974,7 +980,8 @@ fn rewrite_const_ret_proxy(const_fun: &mut syn::ItemFn) -> syn::ItemFn {
     // But just do it to be safe and consistent with verus macro.
     let span = const_fun.sig.constness.unwrap().span();
     let mut proxy_fun = const_fun.clone();
-    replace_block(EraseGhost::Erase, const_fun.block_mut().unwrap());
+    let inside_external_code = has_external_code_syn(&const_fun.attrs);
+    replace_block(EraseGhost::Erase, const_fun.block_mut().unwrap(), inside_external_code);
     const_fun.attrs.push(mk_verifier_attr_syn(span, quote! { external }));
     const_fun.attrs.push(mk_verus_attr_syn(span, quote! { uses_unerased_proxy }));
     const_fun.attrs.push(mk_verus_attr_syn(span, quote! { encoded_const }));

source/builtin_macros/src/syntax.rs

@@ -5267,24 +5267,30 @@ pub(crate) fn proof_macro_explicit_exprs(
     proc_macro::TokenStream::from(new_stream)
 }
 
-pub(crate) fn has_external_code(attrs: &Vec<Attribute>) -> bool {
-    attrs.iter().any(|attr| {
-        // verifier::external
-        attr.path().segments.len() == 2
-            && attr.path().segments[0].ident == "verifier"
-            && (attr.path().segments[1].ident == "external"
-                || attr.path().segments[1].ident == "external_body")
-        // verifier(external)
-        || attr.path().segments.len() == 1
-            && attr.path().segments[0].ident == "verifier"
-            && match &attr.meta {
-                verus_syn::Meta::List(list) => {
-                    matches!(list.tokens.to_string().as_str(), "external" | "external_body")
-                }
-                _ => false,
-            }
-    })
+macro_rules! declare_has_external_code {
+    ($name:ident, $s:ident) => {
+        pub(crate) fn $name(attrs: &Vec<$s::Attribute>) -> bool {
+            attrs.iter().any(|attr| {
+                // verifier::external
+                attr.path().segments.len() == 2
+                    && attr.path().segments[0].ident == "verifier"
+                    && (attr.path().segments[1].ident == "external"
+                        || attr.path().segments[1].ident == "external_body")
+                // verifier(external) or verus_verify(external)
+                || attr.path().segments.len() == 1
+                    && matches!(attr.path().segments[0].ident.to_string().as_str(), "verifier" | "verus_verify")
+                    && match &attr.meta {
+                        $s::Meta::List(list) => {
+                            matches!(list.tokens.to_string().as_str(), "external" | "external_body")
+                        }
+                        _ => false,
+                    }
+            })
+        }
+    };
 }
+declare_has_external_code!(has_external_code, verus_syn);
+declare_has_external_code!(has_external_code_syn, syn);
 
 pub(crate) fn is_encoded_const(attrs: &Vec<Attribute>) -> bool {
     attrs.iter().any(|attr| match &attr.meta {

source/rust_verify_test/tests/syntax_attr.rs

@@ -1296,6 +1296,32 @@ test_verify_one_file! {
     } => Ok(())
 }
 
+test_verify_one_file! {
+    #[test] test_skip_desugar_loop_with_external_body code!{
+        use vstd::prelude::*;
+
+        #[verus_verify]
+        struct A;
+
+        impl Iterator for A {
+            type Item = u32;
+            fn next(&mut self) -> Option<Self::Item> {
+                None
+            }
+        }
+
+        #[verus_verify(external_body)]
+        #[verus_spec(ensures false)]
+        fn test_for_loop()
+        {
+            let a = A;
+            for i in a
+            {
+            }
+        }
+    } => Ok(())
+}
+
 test_verify_one_file! {
     #[test] test_proof_with_struct code!{
         use vstd::prelude::*;