Post-merge fixes for prettyplease and syn

dependencies/prettyplease/src/expr.rs

@@ -340,7 +340,8 @@ impl Printer {
         );
         let left_needs_group = match binop_prec {
             Precedence::Assign => left_prec <= Precedence::Range,
-            Precedence::Compare => left_prec <= binop_prec,
+            // verus supports chained comparisons:
+            // Precedence::Compare => left_prec <= binop_prec,
             _ => left_prec < binop_prec,
         };
         let right_fixup = fixup.rightmost_subexpression_fixup(false, false, binop_prec);

dependencies/prettyplease/src/stmt.rs

@@ -85,8 +85,7 @@ pub fn add_semi(expr: &Expr) -> bool {
         Expr::Assign(_) | Expr::Break(_) | Expr::Continue(_) | Expr::Return(_) | Expr::Yield(_) => {
             true
         }
-        Expr::Binary(expr) =>
-        {
+        Expr::Binary(expr) => {
             match expr.op {
                 #![cfg_attr(all(test, exhaustive), deny(non_exhaustive_omitted_patterns))]
                 BinOp::AddAssign(_)
@@ -117,6 +116,18 @@ pub fn add_semi(expr: &Expr) -> bool {
                 | BinOp::Ne(_)
                 | BinOp::Ge(_)
                 | BinOp::Gt(_) => false,
+
+                // verus
+                BinOp::Equiv(_)
+                | BinOp::Imply(_)
+                | BinOp::Exply(_)
+                | BinOp::BigEq(_)
+                | BinOp::BigNe(_)
+                | BinOp::ExtEq(_)
+                | BinOp::ExtNe(_)
+                | BinOp::ExtDeepEq(_)
+                | BinOp::ExtDeepNe(_) => false,
+
                 _ => unimplemented!("unknown BinOp"),
             }
         }

dependencies/syn/src/expr.rs

@@ -3611,7 +3611,8 @@ pub(crate) mod printing {
         );
         let left_needs_group = match binop_prec {
             Precedence::Assign => left_prec <= Precedence::Range,
-            Precedence::Compare => left_prec <= binop_prec,
+            // verus supports chained comparisons:
+            // Precedence::Compare => left_prec <= binop_prec,
             _ => left_prec < binop_prec,
         };
 

dependencies/syn/src/item.rs

@@ -1133,7 +1133,7 @@ pub(crate) mod parsing {
                     None,
                     Some(input.parse()?),
                 ),
-                (None, Some(_)) => (None, Some(input.parse()?), None),
+                (None, Some(_)) => (Some((None, None)), Some(input.parse()?), None),
                 _ => return Err(lookahead.error()),
             };
             match value {

source/builtin_macros/Cargo.toml

@@ -9,7 +9,7 @@ proc-macro = true
 [dependencies]
 proc-macro2 = "1.0.39"
 quote = "1.0"
-synstructure = "0.13"
+synstructure = { git = "https://github.com/mystor/synstructure.git", rev = "1079497eb2bea252433dac53afe41291d8779641" }
 syn = { version = "2.0", features = ["full", "visit", "visit-mut", "extra-traits"] }
 syn_verus = { path="../../dependencies/syn", features = ["full", "visit", "visit-mut", "extra-traits"] }
 prettyplease_verus = { path="../../dependencies/prettyplease" }

source/builtin_macros/src/rustdoc.rs

@@ -29,7 +29,6 @@
 // some data explaining the function mode, param modes, and return mode.
 
 use proc_macro2::Span;
-use proc_macro2::TokenTree;
 use std::iter::FromIterator;
 use syn_verus::punctuated::Punctuated;
 use syn_verus::spanned::Spanned;
@@ -317,20 +316,16 @@ fn doc_attr_from_string(doc_str: &str, span: Span) -> Attribute {
             arguments: PathArguments::None,
         }]),
     };
-    let list = syn_verus::MetaList {
+    let lit = syn_verus::Lit::Str(syn_verus::LitStr::new(doc_str, span));
+    let name_value = syn_verus::MetaNameValue {
         path,
-        delimiter: syn_verus::MacroDelimiter::Paren(token::Paren {
-            span: crate::syntax::into_spans(span),
-        }),
-        tokens: proc_macro2::TokenStream::from_iter(vec![
-            TokenTree::Punct(proc_macro2::Punct::new('=', proc_macro2::Spacing::Alone)),
-            TokenTree::Literal(proc_macro2::Literal::string(doc_str)),
-        ]),
+        eq_token: token::Eq { spans: [span] },
+        value: Expr::Lit(syn_verus::ExprLit { attrs: vec![], lit }),
     };
     Attribute {
         pound_token: token::Pound { spans: [span] },
         style: AttrStyle::Outer,
         bracket_token: token::Bracket { span: crate::syntax::into_spans(span) },
-        meta: syn_verus::Meta::List(list),
+        meta: syn_verus::Meta::NameValue(name_value),
     }
 }

source/builtin_macros/src/structural.rs

@@ -1,6 +1,6 @@
 use syn_verus::spanned::Spanned;
 
-pub fn derive_structural(s: synstructure::Structure) -> proc_macro2::TokenStream {
+pub fn derive_structural(mut s: synstructure::Structure) -> proc_macro2::TokenStream {
     let assert_receiver_is_structural_body = s
         .variants()
         .iter()
@@ -12,6 +12,12 @@ pub fn derive_structural(s: synstructure::Structure) -> proc_macro2::TokenStream
             }
         })
         .collect::<proc_macro2::TokenStream>();
+
+    // TODO: this feature has disappeared in the latest version of synstructure
+    // (this is why we still use a specific commit of synstructure)
+    // see 'path.segments.iter().find(|s| s.starts_with("_DERIVE_builtin_Structural_FOR_")).is_some()' in rust_to_vir
+    s.underscore_const(false);
+
     s.gen_impl(quote_spanned_builtin! { builtin, s.ast().span() =>
         #[automatically_derived]
         gen impl #builtin::Structural for @Self {

source/builtin_macros/src/syntax.rs

@@ -3214,22 +3214,23 @@ impl VisitMut for Visitor {
                             };
                             let mut path_segments = path_verifier(span);
                             path_segments.push(second_segment.clone());
-                            let list = syn_verus::MetaList {
-                                path: Path { leading_colon: None, segments: path_segments },
-                                delimiter: syn_verus::MacroDelimiter::Paren(token::Paren {
-                                    span: into_spans(span),
-                                }),
-                                tokens: if let Some(nested) = nested {
-                                    quote! { #nested }
-                                } else {
-                                    quote! {}
-                                },
+                            let path = Path { leading_colon: None, segments: path_segments };
+                            let meta = if let Some(nested) = nested {
+                                syn_verus::Meta::List(syn_verus::MetaList {
+                                    path,
+                                    delimiter: syn_verus::MacroDelimiter::Paren(token::Paren {
+                                        span: into_spans(span),
+                                    }),
+                                    tokens: quote! { #nested },
+                                })
+                            } else {
+                                syn_verus::Meta::Path(path)
                             };
                             *attr = Attribute {
                                 pound_token: token::Pound { spans: [span] },
                                 style: syn_verus::AttrStyle::Outer,
                                 bracket_token: token::Bracket { span: into_spans(span) },
-                                meta: syn_verus::Meta::List(list),
+                                meta,
                             };
                         }
                         _ => {
@@ -3640,6 +3641,7 @@ enum MacroElement {
     Comma(Token![,]),
     Semi(Token![;]),
     FatArrow(Token![=>]),
+    Colon(Token![:]),
     Expr(Expr),
 }
 
@@ -3648,6 +3650,7 @@ enum MacroElementExplicitExpr {
     Comma(Token![,]),
     Semi(Token![;]),
     FatArrow(Token![=>]),
+    Colon(Token![:]),
     ExplicitExpr(Token![@], Token![@], Expr),
     TT(TokenTree),
 }
@@ -3693,6 +3696,8 @@ impl Parse for MacroElement {
             Ok(MacroElement::Semi(input.parse()?))
         } else if input.peek(Token![=>]) {
             Ok(MacroElement::FatArrow(input.parse()?))
+        } else if input.peek(Token![:]) {
+            Ok(MacroElement::Colon(input.parse()?))
         } else {
             Ok(MacroElement::Expr(input.parse()?))
         }
@@ -3707,6 +3712,8 @@ impl Parse for MacroElementExplicitExpr {
             Ok(MacroElementExplicitExpr::Semi(input.parse()?))
         } else if input.peek(Token![=>]) {
             Ok(MacroElementExplicitExpr::FatArrow(input.parse()?))
+        } else if input.peek(Token![:]) {
+            Ok(MacroElementExplicitExpr::Colon(input.parse()?))
         } else if input.peek(Token![@]) && input.peek2(Token![@]) {
             let at1 = input.parse()?;
             let at2 = input.parse()?;
@@ -3791,6 +3798,7 @@ impl ToTokens for MacroElement {
             MacroElement::Comma(e) => e.to_tokens(tokens),
             MacroElement::Semi(e) => e.to_tokens(tokens),
             MacroElement::FatArrow(e) => e.to_tokens(tokens),
+            MacroElement::Colon(e) => e.to_tokens(tokens),
             MacroElement::Expr(e) => e.to_tokens(tokens),
         }
     }
@@ -3802,6 +3810,7 @@ impl ToTokens for MacroElementExplicitExpr {
             MacroElementExplicitExpr::Comma(e) => e.to_tokens(tokens),
             MacroElementExplicitExpr::Semi(e) => e.to_tokens(tokens),
             MacroElementExplicitExpr::FatArrow(e) => e.to_tokens(tokens),
+            MacroElementExplicitExpr::Colon(e) => e.to_tokens(tokens),
             MacroElementExplicitExpr::ExplicitExpr(_at1, _at2, e) => e.to_tokens(tokens),
             MacroElementExplicitExpr::TT(e) => e.to_tokens(tokens),
         }
@@ -4206,16 +4215,23 @@ macro_rules! declare_mk_rust_attr {
                 ident: $s::Ident::new(name, span),
                 arguments: $s::PathArguments::None,
             });
-            let list = $s::MetaList {
-                path: $s::Path { leading_colon: None, segments: path_segments },
-                delimiter: $s::MacroDelimiter::Paren($s::token::Paren { span: into_spans(span) }),
-                tokens: quote! { #tokens },
+            let path = $s::Path { leading_colon: None, segments: path_segments };
+            let meta = if tokens.is_empty() {
+                $s::Meta::Path(path)
+            } else {
+                $s::Meta::List($s::MetaList {
+                    path,
+                    delimiter: $s::MacroDelimiter::Paren($s::token::Paren {
+                        span: into_spans(span),
+                    }),
+                    tokens: quote! { #tokens },
+                })
             };
             $s::Attribute {
                 pound_token: $s::token::Pound { spans: [span] },
                 style: $s::AttrStyle::Outer,
                 bracket_token: $s::token::Bracket { span: into_spans(span) },
-                meta: $s::Meta::List(list),
+                meta,
             }
         }
     };
@@ -4236,16 +4252,23 @@ macro_rules! declare_mk_verus_attr {
                 ident: $s::Ident::new("internal", span),
                 arguments: $s::PathArguments::None,
             });
-            let list = $s::MetaList {
-                path: $s::Path { leading_colon: None, segments: path_segments },
-                delimiter: $s::MacroDelimiter::Paren($s::token::Paren { span: into_spans(span) }),
-                tokens: quote! { #tokens },
+            let path = $s::Path { leading_colon: None, segments: path_segments };
+            let meta = if tokens.is_empty() {
+                $s::Meta::Path(path)
+            } else {
+                $s::Meta::List($s::MetaList {
+                    path,
+                    delimiter: $s::MacroDelimiter::Paren($s::token::Paren {
+                        span: into_spans(span),
+                    }),
+                    tokens: quote! { #tokens },
+                })
             };
             $s::Attribute {
                 pound_token: $s::token::Pound { spans: [span] },
                 style: $s::AttrStyle::Outer,
                 bracket_token: $s::token::Bracket { span: into_spans(span) },
-                meta: $s::Meta::List(list),
+                meta,
             }
         }
     };

source/rust_verify_test/tests/regression.rs

@@ -535,7 +535,7 @@ test_verify_one_file! {
         pub struct Y {
             y: int
         }
-    } => Err(err) => assert_vir_error_msg(err, "expected one of")
+    } => Err(err) => assert_vir_error_msg(err, "unexpected token, expected `]`")
 }
 
 test_verify_one_file! {
@@ -552,7 +552,7 @@ test_verify_one_file! {
         #[verifier(external),verifier(external_body)]
         proof fn bar() {
         }
-    } => Err(err) => assert_vir_error_msg(err, "expected `]`, found `,`")
+    } => Err(err) => assert_vir_error_msg(err, "unexpected token, expected `]`")
 }
 
 test_verify_one_file! {

source/rust_verify_test/tests/triggers.rs

@@ -18,8 +18,8 @@ test_verify_one_file! {
                 forall|i: nat, j: nat|
                     i < self.nodes.len() && j < self.nodes.index(spec_cast_integer::<nat, int>(i)).values.len() ==>
                     {
-                        let values = #[verifier(trigger)] self.nodes.index(spec_cast_integer::<nat, int>(i)).values;
-                        self.base_v <= #[verifier(trigger)] values.index(spec_cast_integer::<nat, int>(j))
+                        let values = #[trigger] self.nodes.index(spec_cast_integer::<nat, int>(i)).values;
+                        self.base_v <= #[trigger] values.index(spec_cast_integer::<nat, int>(j))
                     }
             }
         }