Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

New Attribute-based loop specification #1455

Merged
merged 4 commits into from
Feb 27, 2025
+235 −237
Merged

New Attribute-based loop specification #1455

Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
85026e8
Support loop spec in verus_spec
ziqiaozhou Feb 7, 2025
269142d
Remove unused attributes
ziqiaozhou Feb 18, 2025
6d6f014
update tests
ziqiaozhou Feb 18, 2025
5c4023a
Support naming iterator in LoopSpec && Construct syn::ExprForLoop
ziqiaozhou Feb 27, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 5 additions & 4 deletions dependencies/syn/src/lib.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
27 changes: 27 additions & 0 deletions dependencies/syn/src/verus.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2048,3 +2048,30 @@ pub(crate) fn parse_fn_spec(input: ParseStream) -> Result<TypeFnSpec> {

Ok(fn_spec)
}

ast_struct! {
pub struct LoopSpec {
pub invariants: Option<Invariant>,
pub invariant_except_breaks: Option<InvariantExceptBreak>,
pub invariant_ensures: Option<InvariantEnsures>,
pub ensures: Option<Ensures>,
pub decreases: Option<Decreases>,
}
}

impl parse::Parse for LoopSpec {
fn parse(input: ParseStream) -> Result<Self> {
let invariants: Option<Invariant> = input.parse()?;
let invariant_except_breaks: Option<InvariantExceptBreak> = input.parse()?;
let invariant_ensures: Option<InvariantEnsures> = input.parse()?;
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

invariant_ensures is already deprecated in the macro syntax, so I don't think we need to support it in the attribute syntax.

let ensures: Option<Ensures> = input.parse()?;
let decreases: Option<Decreases> = input.parse()?;
Ok(LoopSpec {
invariants,
invariant_except_breaks,
invariant_ensures,
ensures,
decreases,
})
}
}
176 changes: 25 additions & 151 deletions source/builtin_macros/src/attr_rewrite.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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},
Expand All @@ -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<String> for SpecAttributeKind {
type Error = String;

fn try_from(name: String) -> Result<Self, Self::Error> {
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::<syn_verus::Expr>(tokens.clone())
.map_or(quote! {[#tokens]}, |e| quote! {#e})
}
SpecAttributeKind::Decreases => tokens,
_ => {
quote! {[#tokens]}
}
}
}

fn expand_verus_attribute(
erase: EraseGhost,
verus_attrs: Vec<SpecAttrWithArgs>,
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<syn::Ident>,
Expand Down Expand Up @@ -203,23 +86,27 @@ 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]");),
);
}
};
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());
Expand All @@ -232,41 +119,28 @@ 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()
}
}
}

pub fn rewrite(
erase: EraseGhost,
outer_attr: SpecAttributeKind,
outer_attr_tokens: TokenStream,
input: TokenStream,
) -> Result<TokenStream, syn::Error> {
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::<AnyFnOrLoop>(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})
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) => {
expand_verus_attribute(erase, verus_attrs, &mut l, false);
Ok(quote_spanned! {l.span()=>#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::Fn(_) | AnyFnOrLoop::TraitMethod(_) => Ok(
quote_spanned!(span => compile_error!("'verus_spec' attribute expected on function");),
),
}
}

Expand Down
66 changes: 0 additions & 66 deletions source/builtin_macros/src/lib.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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};
Expand Down Expand Up @@ -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()
Expand Down
Loading