From a1fa34344df279ee956c26bb7546dc68922b10f1 Mon Sep 17 00:00:00 2001 From: Chris Hawblitzel Date: Fri, 31 Jan 2025 20:26:24 +0100 Subject: [PATCH] Post-merge fixes for prettyplease and syn --- dependencies/prettyplease/src/expr.rs | 3 +- dependencies/prettyplease/src/stmt.rs | 15 ++++- dependencies/syn/src/expr.rs | 3 +- dependencies/syn/src/item.rs | 2 +- source/Cargo.lock | 8 +-- source/builtin_macros/Cargo.toml | 2 +- source/builtin_macros/src/rustdoc.rs | 15 ++--- source/builtin_macros/src/structural.rs | 8 ++- source/builtin_macros/src/syntax.rs | 65 ++++++++++++++------- source/rust_verify_test/tests/regression.rs | 4 +- source/rust_verify_test/tests/triggers.rs | 4 +- 11 files changed, 83 insertions(+), 46 deletions(-) diff --git a/dependencies/prettyplease/src/expr.rs b/dependencies/prettyplease/src/expr.rs index b738d422b..1cc8a98a0 100644 --- a/dependencies/prettyplease/src/expr.rs +++ b/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); diff --git a/dependencies/prettyplease/src/stmt.rs b/dependencies/prettyplease/src/stmt.rs index ed5e72c5a..e08fcec1c 100644 --- a/dependencies/prettyplease/src/stmt.rs +++ b/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"), } } diff --git a/dependencies/syn/src/expr.rs b/dependencies/syn/src/expr.rs index 6e0aee713..65fe66b25 100644 --- a/dependencies/syn/src/expr.rs +++ b/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, }; diff --git a/dependencies/syn/src/item.rs b/dependencies/syn/src/item.rs index a6e7e827d..6c3e87845 100644 --- a/dependencies/syn/src/item.rs +++ b/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 { diff --git a/source/Cargo.lock b/source/Cargo.lock index b1c77353d..d4000291e 100644 --- a/source/Cargo.lock +++ b/source/Cargo.lock @@ -165,7 +165,7 @@ dependencies = [ "quote", "syn 2.0.25", "syn_verus", - "synstructure 0.13.1", + "synstructure 0.13.0", ] [[package]] @@ -1808,13 +1808,13 @@ dependencies = [ [[package]] name = "synstructure" -version = "0.13.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c8af7666ab7b6390ab78131fb5b0fce11d6b7a6951602017c35fa82800708971" +version = "0.13.0" +source = "git+https://github.com/mystor/synstructure.git?rev=1079497eb2bea252433dac53afe41291d8779641#1079497eb2bea252433dac53afe41291d8779641" dependencies = [ "proc-macro2", "quote", "syn 2.0.25", + "unicode-xid", ] [[package]] diff --git a/source/builtin_macros/Cargo.toml b/source/builtin_macros/Cargo.toml index 4e96775d5..3881cd0c1 100644 --- a/source/builtin_macros/Cargo.toml +++ b/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" } diff --git a/source/builtin_macros/src/rustdoc.rs b/source/builtin_macros/src/rustdoc.rs index df2ed17bc..c1729b5c1 100644 --- a/source/builtin_macros/src/rustdoc.rs +++ b/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), } } diff --git a/source/builtin_macros/src/structural.rs b/source/builtin_macros/src/structural.rs index 9097c61b5..7acc1d2fd 100644 --- a/source/builtin_macros/src/structural.rs +++ b/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::(); + + // 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 { diff --git a/source/builtin_macros/src/syntax.rs b/source/builtin_macros/src/syntax.rs index c73318a8f..6fb71e7f7 100644 --- a/source/builtin_macros/src/syntax.rs +++ b/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, } } }; diff --git a/source/rust_verify_test/tests/regression.rs b/source/rust_verify_test/tests/regression.rs index 8c15c1f27..1a195ef3d 100644 --- a/source/rust_verify_test/tests/regression.rs +++ b/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! { diff --git a/source/rust_verify_test/tests/triggers.rs b/source/rust_verify_test/tests/triggers.rs index db4f4ce74..22e80c88e 100644 --- a/source/rust_verify_test/tests/triggers.rs +++ b/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::(i)).values.len() ==> { - let values = #[verifier(trigger)] self.nodes.index(spec_cast_integer::(i)).values; - self.base_v <= #[verifier(trigger)] values.index(spec_cast_integer::(j)) + let values = #[trigger] self.nodes.index(spec_cast_integer::(i)).values; + self.base_v <= #[trigger] values.index(spec_cast_integer::(j)) } } }