From 85026e8f36fd62dbd55b9910cb8a208b29c7d7a1 Mon Sep 17 00:00:00 2001 From: Ziqiao Zhou Date: Thu, 6 Feb 2025 17:43:23 -0800 Subject: [PATCH 1/4] Support loop spec in verus_spec --- dependencies/syn/src/lib.rs | 9 +-- dependencies/syn/src/verus.rs | 27 +++++++ source/builtin_macros/src/attr_rewrite.rs | 34 +++++++-- source/builtin_macros/src/syntax.rs | 85 +++++++++++++++++++++++ 4 files changed, 144 insertions(+), 11 deletions(-) diff --git a/dependencies/syn/src/lib.rs b/dependencies/syn/src/lib.rs index b40004bfe6..14653425eb 100644 --- a/dependencies/syn/src/lib.rs +++ b/dependencies/syn/src/lib.rs @@ -556,10 +556,11 @@ pub use crate::verus::{ BroadcastUse, Closed, DataMode, Decreases, Ensures, ExprGetField, ExprHas, ExprIs, ExprMatches, FnMode, Global, GlobalInner, GlobalLayout, GlobalSizeOf, Invariant, InvariantEnsures, InvariantExceptBreak, InvariantNameSet, InvariantNameSetAny, InvariantNameSetList, - InvariantNameSetNone, ItemBroadcastGroup, MatchesOpExpr, MatchesOpToken, Mode, ModeExec, - ModeGhost, ModeProof, ModeSpec, ModeSpecChecked, ModeTracked, Open, OpenRestricted, Prover, - Publish, Recommends, Requires, Returns, RevealHide, SignatureDecreases, SignatureInvariants, - SignatureSpec, SignatureSpecAttr, SignatureUnwind, Specification, TypeFnSpec, View, + InvariantNameSetNone, ItemBroadcastGroup, LoopSpec, MatchesOpExpr, MatchesOpToken, Mode, + ModeExec, ModeGhost, ModeProof, ModeSpec, ModeSpecChecked, ModeTracked, Open, OpenRestricted, + Prover, Publish, Recommends, Requires, Returns, RevealHide, SignatureDecreases, + SignatureInvariants, SignatureSpec, SignatureSpecAttr, SignatureUnwind, Specification, + TypeFnSpec, View, }; #[rustfmt::skip] // https://github.com/rust-lang/rustfmt/issues/6176 diff --git a/dependencies/syn/src/verus.rs b/dependencies/syn/src/verus.rs index c31ec239c9..6d62b820ef 100644 --- a/dependencies/syn/src/verus.rs +++ b/dependencies/syn/src/verus.rs @@ -2048,3 +2048,30 @@ pub(crate) fn parse_fn_spec(input: ParseStream) -> Result { Ok(fn_spec) } + +ast_struct! { + pub struct LoopSpec { + pub invariants: Option, + pub invariant_except_breaks: Option, + pub invariant_ensures: Option, + pub ensures: Option, + pub decreases: Option, + } +} + +impl parse::Parse for LoopSpec { + fn parse(input: ParseStream) -> Result { + let invariants: Option = input.parse()?; + let invariant_except_breaks: Option = input.parse()?; + let invariant_ensures: Option = input.parse()?; + let ensures: Option = input.parse()?; + let decreases: Option = input.parse()?; + Ok(LoopSpec { + invariants, + invariant_except_breaks, + invariant_ensures, + ensures, + decreases, + }) + } +} diff --git a/source/builtin_macros/src/attr_rewrite.rs b/source/builtin_macros/src/attr_rewrite.rs index 7b37407c0f..4c74a51c91 100644 --- a/source/builtin_macros/src/attr_rewrite.rs +++ b/source/builtin_macros/src/attr_rewrite.rs @@ -207,19 +207,23 @@ pub fn rewrite_verus_spec( ); } }; - let spec_attr = - syn_verus::parse_macro_input!(outer_attr_tokens as syn_verus::SignatureSpecAttr); + match f { AnyFnOrLoop::Fn(mut fun) => { + let spec_attr = + syn_verus::parse_macro_input!(outer_attr_tokens as syn_verus::SignatureSpecAttr); // Note: trait default methods appear in this case, // since they look syntactically like non-trait functions let spec_stmts = syntax::sig_specs_attr(erase, spec_attr, &fun.sig); let new_stmts = spec_stmts.into_iter().map(|s| parse2(quote! { #s }).unwrap()); let _ = fun.block_mut().unwrap().stmts.splice(0..0, new_stmts); fun.attrs.push(mk_verus_attr_syn(fun.span(), quote! { verus_macro })); + proc_macro::TokenStream::from(fun.to_token_stream()) } AnyFnOrLoop::TraitMethod(mut method) => { + let spec_attr = + syn_verus::parse_macro_input!(outer_attr_tokens as syn_verus::SignatureSpecAttr); // Note: default trait methods appear in the AnyFnOrLoop::Fn case, not here let spec_stmts = syntax::sig_specs_attr(erase, spec_attr, &method.sig); let new_stmts = spec_stmts.into_iter().map(|s| parse2(quote! { #s }).unwrap()); @@ -232,11 +236,27 @@ pub fn rewrite_verus_spec( method.to_tokens(&mut new_stream); proc_macro::TokenStream::from(new_stream) } - _ => { - let span = spec_attr.span(); - proc_macro::TokenStream::from( - quote_spanned!(span => compile_error!("'verus_spec' is not allowed here");), - ) + AnyFnOrLoop::ForLoop(forloop) => { + let spec_attr = syn_verus::parse_macro_input!(outer_attr_tokens as syn_verus::LoopSpec); + syntax::for_loop_spec_attr(erase, spec_attr, forloop).to_token_stream().into() + } + AnyFnOrLoop::Loop(mut l) => { + let spec_attr = syn_verus::parse_macro_input!(outer_attr_tokens as syn_verus::LoopSpec); + let spec_stmts = syntax::while_loop_spec_attr(erase, spec_attr); + let new_stmts = spec_stmts.into_iter().map(|s| parse2(quote! { #s }).unwrap()); + if erase.keep() { + l.body.stmts.splice(0..0, new_stmts); + } + l.to_token_stream().into() + } + AnyFnOrLoop::While(mut l) => { + let spec_attr = syn_verus::parse_macro_input!(outer_attr_tokens as syn_verus::LoopSpec); + let spec_stmts = syntax::while_loop_spec_attr(erase, spec_attr); + let new_stmts = spec_stmts.into_iter().map(|s| parse2(quote! { #s }).unwrap()); + if erase.keep() { + l.body.stmts.splice(0..0, new_stmts); + } + l.to_token_stream().into() } } } diff --git a/source/builtin_macros/src/syntax.rs b/source/builtin_macros/src/syntax.rs index dbf96012ef..066e8deaf9 100644 --- a/source/builtin_macros/src/syntax.rs +++ b/source/builtin_macros/src/syntax.rs @@ -20,6 +20,7 @@ use syn_verus::visit_mut::{ }; use syn_verus::BroadcastUse; use syn_verus::ExprBlock; +use syn_verus::ExprForLoop; use syn_verus::{ braced, bracketed, parenthesized, parse_macro_input, AssumeSpecification, Attribute, BareFnArg, BinOp, Block, DataMode, Decreases, Ensures, Expr, ExprBinary, ExprCall, ExprLit, ExprLoop, @@ -239,6 +240,26 @@ impl Visitor { } } + fn visit_loop_spec(&mut self, spec: &mut syn_verus::LoopSpec) { + let mut visit_spec = |exprs: &mut syn_verus::Specification| { + for expr in exprs.exprs.iter_mut() { + self.visit_expr_mut(expr); + } + }; + if let Some(exprs) = spec.invariants.as_mut() { + visit_spec(&mut exprs.exprs); + } + if let Some(exprs) = spec.invariant_except_breaks.as_mut() { + visit_spec(&mut exprs.exprs); + } + if let Some(exprs) = spec.invariant_ensures.as_mut() { + visit_spec(&mut exprs.exprs); + } + if let Some(exprs) = spec.decreases.as_mut() { + visit_spec(&mut exprs.exprs); + } + } + fn take_sig_specs( &mut self, spec: &mut SignatureSpec, @@ -3981,6 +4002,70 @@ pub(crate) fn sig_specs_attr( visitor.take_sig_specs(&mut spec, ret_pat, sig.constness.is_some(), sig_span) } +pub(crate) fn while_loop_spec_attr( + erase_ghost: EraseGhost, + spec_attr: syn_verus::LoopSpec, +) -> Vec { + let mut visitor = Visitor { + erase_ghost, + use_spec_traits: true, + inside_ghost: 1, + inside_type: 0, + inside_external_code: 0, + inside_const: false, + inside_arith: InsideArith::None, + assign_to: false, + rustdoc: env_rustdoc(), + }; + let mut spec_attr = spec_attr; + visitor.visit_loop_spec(&mut spec_attr); + let syn_verus::LoopSpec { + invariants, + invariant_except_breaks, + invariant_ensures, + ensures, + decreases, + .. + } = spec_attr; + let mut stmt = vec![]; + visitor.add_loop_specs( + &mut stmt, + invariant_except_breaks, + invariants, + invariant_ensures, + ensures, + decreases, + ); + stmt +} + +pub(crate) fn for_loop_spec_attr( + erase_ghost: EraseGhost, + spec_attr: syn_verus::LoopSpec, + forloop: syn::ExprForLoop, +) -> syn_verus::Expr { + let mut visitor = Visitor { + erase_ghost, + use_spec_traits: true, + inside_ghost: 1, + inside_type: 0, + inside_external_code: 0, + inside_const: false, + inside_arith: InsideArith::None, + assign_to: false, + rustdoc: env_rustdoc(), + }; + let mut spec_attr = spec_attr; + visitor.visit_loop_spec(&mut spec_attr); + let syn_verus::LoopSpec { invariants, decreases, .. } = spec_attr; + let mut forloop: ExprForLoop = + syn_verus::parse2(forloop.to_token_stream().into()).expect("ExprForLoop"); + + forloop.invariant = invariants; + forloop.decreases = decreases; + visitor.desugar_for_loop(forloop) +} + // Unfortunately, the macro_rules tt tokenizer breaks tokens like &&& and ==> into smaller tokens. // Try to put the original tokens back together here. #[cfg(verus_keep_ghost)] From 269142d8610cc524f55f529dfb127b16ebc56b76 Mon Sep 17 00:00:00 2001 From: Ziqiao Zhou Date: Mon, 17 Feb 2025 17:23:36 -0800 Subject: [PATCH 2/4] Remove unused attributes --- source/builtin_macros/src/attr_rewrite.rs | 150 +--------------------- source/builtin_macros/src/lib.rs | 66 ---------- 2 files changed, 2 insertions(+), 214 deletions(-) diff --git a/source/builtin_macros/src/attr_rewrite.rs b/source/builtin_macros/src/attr_rewrite.rs index 4c74a51c91..151cdf4d1e 100644 --- a/source/builtin_macros/src/attr_rewrite.rs +++ b/source/builtin_macros/src/attr_rewrite.rs @@ -30,10 +30,9 @@ /// /// Example: /// - Refer to `example/syntax_attr.rs`. -use core::convert::TryFrom; use proc_macro2::TokenStream; use quote::{quote, quote_spanned, ToTokens}; -use syn::{parse2, spanned::Spanned, Ident, Item}; +use syn::{parse2, spanned::Spanned, Item}; use crate::{ attr_block_trait::{AnyAttrBlock, AnyFnOrLoop}, @@ -42,122 +41,6 @@ use crate::{ EraseGhost, }; -#[derive(Debug)] -pub enum SpecAttributeKind { - Requires, - Ensures, - Decreases, - Invariant, - InvariantExceptBreak, -} - -struct SpecAttributeApply { - pub on_function: bool, - pub on_loop: bool, -} - -type SpecAttrWithArgs = (SpecAttributeKind, TokenStream); - -impl SpecAttributeKind { - fn applies_to(&self) -> SpecAttributeApply { - let (on_function, on_loop) = match self { - SpecAttributeKind::Requires => (true, false), - SpecAttributeKind::Ensures => (true, true), - SpecAttributeKind::Decreases => (true, true), - SpecAttributeKind::Invariant => (false, true), - SpecAttributeKind::InvariantExceptBreak => (false, true), - }; - SpecAttributeApply { on_function, on_loop } - } - - fn applies_to_function(&self) -> bool { - self.applies_to().on_function - } - - fn applies_to_loop(&self) -> bool { - self.applies_to().on_loop - } -} - -impl TryFrom for SpecAttributeKind { - type Error = String; - - fn try_from(name: String) -> Result { - match name.as_str() { - "requires" => Ok(SpecAttributeKind::Requires), - "ensures" => Ok(SpecAttributeKind::Ensures), - "decreases" => Ok(SpecAttributeKind::Decreases), - "invariant" => Ok(SpecAttributeKind::Invariant), - _ => Err(name), - } - } -} - -// Add brackets for requires, invariant. -// Add brackets for ensures if it could not be parsed as a syn_verus::Expr. -fn insert_brackets(attr_type: &SpecAttributeKind, tokens: TokenStream) -> TokenStream { - // Parse the TokenStream into a Syn Expression - match attr_type { - SpecAttributeKind::Ensures => { - // if the tokens are not valid verus expr, it might need a bracket. - syn_verus::parse2::(tokens.clone()) - .map_or(quote! {[#tokens]}, |e| quote! {#e}) - } - SpecAttributeKind::Decreases => tokens, - _ => { - quote! {[#tokens]} - } - } -} - -fn expand_verus_attribute( - erase: EraseGhost, - verus_attrs: Vec, - any_with_attr_block: &mut dyn AnyAttrBlock, - function_or_loop: bool, -) { - if !erase.keep() { - return; - } - // rewrite based on different spec attributes - for (attr_kind, attr_tokens) in verus_attrs { - if function_or_loop { - assert!(attr_kind.applies_to_function()); - } - if !function_or_loop { - assert!(attr_kind.applies_to_loop()); - } - match attr_kind { - SpecAttributeKind::Invariant => { - insert_spec_call(any_with_attr_block, "invariant", attr_tokens) - } - SpecAttributeKind::Decreases => { - insert_spec_call(any_with_attr_block, "decreases", attr_tokens) - } - SpecAttributeKind::Ensures => { - insert_spec_call(any_with_attr_block, "ensures", attr_tokens) - } - SpecAttributeKind::Requires => { - insert_spec_call(any_with_attr_block, "requires", attr_tokens) - } - SpecAttributeKind::InvariantExceptBreak => { - insert_spec_call(any_with_attr_block, "invariant_except_break", attr_tokens) - } - } - } -} - -fn insert_spec_call(any_fn: &mut dyn AnyAttrBlock, call: &str, verus_expr: TokenStream) { - let fname = Ident::new(call, verus_expr.span()); - let tokens: TokenStream = - syntax::rewrite_expr(EraseGhost::Keep, true, verus_expr.into()).into(); - any_fn.block_mut().unwrap().stmts.insert( - 0, - parse2(quote! { #[verus::internal(const_header_wrapper)]||{::builtin::#fname(#tokens);};}) - .unwrap(), - ); -} - pub fn rewrite_verus_attribute( erase: &EraseGhost, attr_args: Vec, @@ -203,7 +86,7 @@ pub fn rewrite_verus_spec( // (In the normal case, this results in a redundant extra error message after // the normal Rust syntax error, but it's a reasonable looking error message.) return proc_macro::TokenStream::from( - quote_spanned!(err.span() => compile_error!("syntax error in function");), + quote_spanned!(err.span() => compile_error!("Misuse of #[verus_spec]");), ); } }; @@ -261,35 +144,6 @@ pub fn rewrite_verus_spec( } } -pub fn rewrite( - erase: EraseGhost, - outer_attr: SpecAttributeKind, - outer_attr_tokens: TokenStream, - input: TokenStream, -) -> Result { - let span = outer_attr_tokens.span(); - let outer_attr_tokens = insert_brackets(&outer_attr, outer_attr_tokens); - let verus_attrs = vec![(outer_attr, outer_attr_tokens)]; - let f = parse2::(input)?; - match f { - AnyFnOrLoop::Loop(mut l) => { - expand_verus_attribute(erase, verus_attrs, &mut l, false); - Ok(quote_spanned! {l.span()=>#l}) - } - AnyFnOrLoop::ForLoop(mut l) => { - expand_verus_attribute(erase, verus_attrs, &mut l, false); - Ok(quote_spanned! {l.span()=>#l}) - } - AnyFnOrLoop::While(mut l) => { - expand_verus_attribute(erase, verus_attrs, &mut l, false); - Ok(quote_spanned! {l.span()=>#l}) - } - AnyFnOrLoop::Fn(_) | AnyFnOrLoop::TraitMethod(_) => Ok( - quote_spanned!(span => compile_error!("'verus_spec' attribute expected on function");), - ), - } -} - pub fn proof_rewrite(erase: EraseGhost, input: TokenStream) -> proc_macro::TokenStream { if erase.keep() { let block: TokenStream = diff --git a/source/builtin_macros/src/lib.rs b/source/builtin_macros/src/lib.rs index 6abb95fc80..aa67d93815 100644 --- a/source/builtin_macros/src/lib.rs +++ b/source/builtin_macros/src/lib.rs @@ -7,7 +7,6 @@ feature(proc_macro_diagnostic) )] -use attr_rewrite::SpecAttributeKind; #[cfg(verus_keep_ghost)] use std::sync::OnceLock; use synstructure::{decl_attribute, decl_derive}; @@ -280,71 +279,6 @@ pub fn verus_spec( } } -// The attribute should work together with verus_verify attribute. -#[proc_macro_attribute] -pub fn ensures( - attr: proc_macro::TokenStream, - input: proc_macro::TokenStream, -) -> proc_macro::TokenStream { - let erase = cfg_erase(); - if erase.keep() { - attr_rewrite::rewrite(erase, SpecAttributeKind::Ensures, attr.into(), input.into()) - .expect("Misuse of #[ensures()].") - .into() - } else { - input - } -} - -// The attribute should work together with verus_verify attribute. -#[proc_macro_attribute] -pub fn decreases( - attr: proc_macro::TokenStream, - input: proc_macro::TokenStream, -) -> proc_macro::TokenStream { - let erase = cfg_erase(); - if erase.keep() { - attr_rewrite::rewrite(erase, SpecAttributeKind::Decreases, attr.into(), input.into()) - .expect("Misuse of #[decreases()].") - .into() - } else { - input - } -} - -// The attribute should work together with verus_verify attribute. -#[proc_macro_attribute] -pub fn invariant( - attr: proc_macro::TokenStream, - input: proc_macro::TokenStream, -) -> proc_macro::TokenStream { - let erase = cfg_erase(); - if erase.keep() { - attr_rewrite::rewrite(erase, SpecAttributeKind::Invariant, attr.into(), input.into()) - .expect("Misuse of #[invariant()]") - .into() - } else { - input - } -} - -// The attribute should work together with verus_verify attribute. -#[proc_macro_attribute] -pub fn invariant_except_break( - attr: proc_macro::TokenStream, - input: proc_macro::TokenStream, -) -> proc_macro::TokenStream { - let erase = cfg_erase(); - if erase.keep() { - let kind = SpecAttributeKind::InvariantExceptBreak; - attr_rewrite::rewrite(erase, kind, attr.into(), input.into()) - .expect("Misuse of #[invariant_except_break()]") - .into() - } else { - input - } -} - #[proc_macro] pub fn proof(input: proc_macro::TokenStream) -> proc_macro::TokenStream { attr_rewrite::proof_rewrite(cfg_erase(), input.into()).into() From 6d6f0148bf6c4de4a45ba6a94293643b80077133 Mon Sep 17 00:00:00 2001 From: Ziqiao Zhou Date: Mon, 17 Feb 2025 17:23:57 -0800 Subject: [PATCH 3/4] update tests --- source/rust_verify_test/tests/syntax_attr.rs | 66 +++++++++++++++----- 1 file changed, 51 insertions(+), 15 deletions(-) diff --git a/source/rust_verify_test/tests/syntax_attr.rs b/source/rust_verify_test/tests/syntax_attr.rs index e5e508e691..c7da5859ac 100644 --- a/source/rust_verify_test/tests/syntax_attr.rs +++ b/source/rust_verify_test/tests/syntax_attr.rs @@ -4,11 +4,14 @@ mod common; use common::*; test_verify_one_file! { - #[test] verus_verify_basic_while code! { - #[verus_verify] + #[test] verus_verify_basic_while code! { + #[verus_spec] fn test1() { let mut i = 0; - #[invariant(i <= 10)] + #[verus_spec( + invariant + i <= 10 + )] while i < 10 { i = i + 1; @@ -20,12 +23,14 @@ test_verify_one_file! { test_verify_one_file! { #[test] verus_verify_basic_loop code! { - #[verus_verify] + #[verus_spec] fn test1() { let mut i = 0; - #[invariant(i <= 10)] - #[invariant_except_break(i <= 9)] - #[ensures(i == 10)] + #[verus_spec( + invariant i <= 10, + invariant_except_break i <= 9, + ensures i == 10 + )] loop { i = i + 1; @@ -38,9 +43,33 @@ test_verify_one_file! { } => Ok(()) } +test_verify_one_file! { + #[test] verus_verify_basic_for_loop_verus_spec code! { + use vstd::prelude::*; + #[verus_spec(v => + ensures + v.len() == n, + forall|i: int| 0 <= i < n ==> v[i] == i + )] + fn test_loop(n: u32) -> Vec + { + let mut v: Vec = Vec::new(); + #[verus_spec( + invariant + v@ =~= Seq::new(i as nat, |k| k as u32), + )] + for i in 0..n + { + v.push(i); + } + v + } + } => Ok(()) +} + test_verify_one_file! { #[test] verus_verify_basic_while_fail1 code! { - #[verus_verify] + #[verus_spec] fn test1() { let mut i = 0; while i < 10 { @@ -56,7 +85,10 @@ test_verify_one_file! { #[verus_verify] fn test1() { let mut i = 0; - #[invariant(i <= 10, false)] + #[verus_spec( + invariant + i <= 10, false + )] while i < 10 { i = i + 1; } @@ -65,11 +97,12 @@ test_verify_one_file! { } test_verify_one_file! { - #[test] verus_verify_bad_loop_spec code! { - #[verus_verify] - #[invariant(true)] + #[test] verus_verify_invariant_on_func code! { + #[verus_spec( + invariant true + )] fn test1() {} - } => Err(err) => assert_any_vir_error_msg(err, "'verus_spec' attribute expected") + } => Err(err) => assert_any_vir_error_msg(err, "unexpected token") } test_verify_one_file! { @@ -100,10 +133,13 @@ test_verify_one_file! { test_verify_one_file! { #[test] test_bad_macro_attributes_in_trait code!{ trait SomeTrait { - #[ensures(true)] + #[verus_spec( + ensures + true + )] type T; } - } => Err(err) => assert_custom_attr_error_msg(err, "Misuse of #[ensures()]") + } => Err(err) => assert_any_vir_error_msg(err, "Misuse of #[verus_spec]") } test_verify_one_file! { From 5c4023aad16a4e44d164939109946b0e19e34aa7 Mon Sep 17 00:00:00 2001 From: Ziqiao Zhou Date: Thu, 27 Feb 2025 00:19:37 -0800 Subject: [PATCH 4/4] Support naming iterator in LoopSpec && Construct syn::ExprForLoop --- dependencies/syn/src/verus.rs | 13 ++++-- source/builtin_macros/src/syntax.rs | 42 ++++++++++++-------- source/rust_verify_test/tests/syntax_attr.rs | 32 +++++++++++++-- 3 files changed, 64 insertions(+), 23 deletions(-) diff --git a/dependencies/syn/src/verus.rs b/dependencies/syn/src/verus.rs index 6d62b820ef..7d1910b1b7 100644 --- a/dependencies/syn/src/verus.rs +++ b/dependencies/syn/src/verus.rs @@ -2051,9 +2051,9 @@ pub(crate) fn parse_fn_spec(input: ParseStream) -> Result { ast_struct! { pub struct LoopSpec { + pub iter_name: Option<(Ident, Token![=>])>, pub invariants: Option, pub invariant_except_breaks: Option, - pub invariant_ensures: Option, pub ensures: Option, pub decreases: Option, } @@ -2061,15 +2061,22 @@ ast_struct! { impl parse::Parse for LoopSpec { fn parse(input: ParseStream) -> Result { + let iter_name = if input.peek2(Token![=>]) { + let pat = input.parse()?; + let token = input.parse()?; + Some((pat, token)) + } else { + None + }; + let invariants: Option = input.parse()?; let invariant_except_breaks: Option = input.parse()?; - let invariant_ensures: Option = input.parse()?; let ensures: Option = input.parse()?; let decreases: Option = input.parse()?; Ok(LoopSpec { + iter_name, invariants, invariant_except_breaks, - invariant_ensures, ensures, decreases, }) diff --git a/source/builtin_macros/src/syntax.rs b/source/builtin_macros/src/syntax.rs index 066e8deaf9..7dfe2fce89 100644 --- a/source/builtin_macros/src/syntax.rs +++ b/source/builtin_macros/src/syntax.rs @@ -252,7 +252,7 @@ impl Visitor { if let Some(exprs) = spec.invariant_except_breaks.as_mut() { visit_spec(&mut exprs.exprs); } - if let Some(exprs) = spec.invariant_ensures.as_mut() { + if let Some(exprs) = spec.ensures.as_mut() { visit_spec(&mut exprs.exprs); } if let Some(exprs) = spec.decreases.as_mut() { @@ -4019,20 +4019,14 @@ pub(crate) fn while_loop_spec_attr( }; let mut spec_attr = spec_attr; visitor.visit_loop_spec(&mut spec_attr); - let syn_verus::LoopSpec { - invariants, - invariant_except_breaks, - invariant_ensures, - ensures, - decreases, - .. - } = spec_attr; + let syn_verus::LoopSpec { invariants, invariant_except_breaks, ensures, decreases, .. } = + spec_attr; let mut stmt = vec![]; visitor.add_loop_specs( &mut stmt, invariant_except_breaks, invariants, - invariant_ensures, + None, ensures, decreases, ); @@ -4057,13 +4051,27 @@ pub(crate) fn for_loop_spec_attr( }; let mut spec_attr = spec_attr; visitor.visit_loop_spec(&mut spec_attr); - let syn_verus::LoopSpec { invariants, decreases, .. } = spec_attr; - let mut forloop: ExprForLoop = - syn_verus::parse2(forloop.to_token_stream().into()).expect("ExprForLoop"); - - forloop.invariant = invariants; - forloop.decreases = decreases; - visitor.desugar_for_loop(forloop) + let syn_verus::LoopSpec { iter_name, invariants: invariant, decreases, .. } = spec_attr; + let syn::ExprForLoop { attrs, label, for_token, pat, in_token, expr, body, .. } = forloop; + let verus_forloop = ExprForLoop { + attrs: attrs.into_iter().map(|a| parse_quote_spanned! {a.span() => #a}).collect(), + label: label.map(|l| syn_verus::Label { + name: syn_verus::Lifetime::new(l.name.ident.to_string().as_str(), l.name.span()), + colon_token: Token![:](l.colon_token.span), + }), + for_token: Token![for](for_token.span), + pat: Box::new(Pat::Verbatim(quote_spanned! {pat.span() => #pat})), + in_token: Token![in](in_token.span), + expr_name: iter_name.map(|(name, token)| Box::new((name, Token![:](token.span())))), + expr: Box::new(Expr::Verbatim(quote_spanned! {expr.span() => #expr})), + invariant, + decreases, + body: Block { + brace_token: Brace(body.brace_token.span), + stmts: vec![Stmt::Expr(Expr::Verbatim(quote_spanned! {body.span() => #body}), None)], + }, + }; + visitor.desugar_for_loop(verus_forloop) } // Unfortunately, the macro_rules tt tokenizer breaks tokens like &&& and ==> into smaller tokens. diff --git a/source/rust_verify_test/tests/syntax_attr.rs b/source/rust_verify_test/tests/syntax_attr.rs index c7da5859ac..56b60959fa 100644 --- a/source/rust_verify_test/tests/syntax_attr.rs +++ b/source/rust_verify_test/tests/syntax_attr.rs @@ -26,19 +26,21 @@ test_verify_one_file! { #[verus_spec] fn test1() { let mut i = 0; + let mut ret = 0; #[verus_spec( invariant i <= 10, invariant_except_break i <= 9, - ensures i == 10 + ensures i == 10, ret == 10 )] loop { i = i + 1; if (i == 10) { + ret = i; break; } } - proof!{assert(i == 10);} + proof!{assert(ret == 10);} } } => Ok(()) } @@ -51,7 +53,7 @@ test_verify_one_file! { v.len() == n, forall|i: int| 0 <= i < n ==> v[i] == i )] - fn test_loop(n: u32) -> Vec + fn test_for_loop(n: u32) -> Vec { let mut v: Vec = Vec::new(); #[verus_spec( @@ -67,6 +69,30 @@ test_verify_one_file! { } => Ok(()) } +test_verify_one_file! { + #[test] verus_verify_for_loop_verus_spec_naming_iter code! { + use vstd::prelude::*; + #[verus_spec(v => + ensures + v.len() == n, + forall|i: int| 0 <= i < n ==> v[i] == 0 + )] + fn test(n: u32) -> Vec + { + let mut v: Vec = Vec::new(); + #[verus_spec(iter => + invariant + v@ =~= Seq::new(iter.cur as nat, |k| 0u32), + )] + for _ in 0..n + { + v.push(0); + } + v + } + } => Ok(()) +} + test_verify_one_file! { #[test] verus_verify_basic_while_fail1 code! { #[verus_spec]