Skip to content

Commit

Permalink
Merge remote-tracking branch 'upstream/main' into vecdeque-specs
Browse files Browse the repository at this point in the history
  • Loading branch information
@jaylorch
jaylorch committed Feb 28, 2025
2 parents b5a92c9 + 3ec86db commit 32c15dc
Show file tree
Hide file tree
Showing 36 changed files with 1,997 additions and 510 deletions.
9 changes: 5 additions & 4 deletions dependencies/syn/src/lib.rs
View file
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
34 changes: 34 additions & 0 deletions dependencies/syn/src/verus.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2048,3 +2048,37 @@ pub(crate) fn parse_fn_spec(input: ParseStream) -> Result<TypeFnSpec> {

Ok(fn_spec)
}

ast_struct! {
pub struct LoopSpec {
pub iter_name: Option<(Ident, Token![=>])>,
pub invariants: Option<Invariant>,
pub invariant_except_breaks: Option<InvariantExceptBreak>,
pub ensures: Option<Ensures>,
pub decreases: Option<Decreases>,
}
}

impl parse::Parse for LoopSpec {
fn parse(input: ParseStream) -> Result<Self> {
let iter_name = if input.peek2(Token![=>]) {
let pat = input.parse()?;
let token = input.parse()?;
Some((pat, token))
} else {
None
};

let invariants: Option<Invariant> = input.parse()?;
let invariant_except_breaks: Option<InvariantExceptBreak> = input.parse()?;
let ensures: Option<Ensures> = input.parse()?;
let decreases: Option<Decreases> = input.parse()?;
Ok(LoopSpec {
iter_name,
invariants,
invariant_except_breaks,
ensures,
decreases,
})
}
}
6 changes: 6 additions & 0 deletions source/builtin/src/lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -370,6 +370,12 @@ pub struct Tracked<A> {
phantom: PhantomData<A>,
}

impl<A> core::fmt::Debug for Tracked<A> {
fn fmt(&self, _: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
Ok(())
}
}

impl<A> Ghost<A> {
#[cfg(verus_keep_ghost)]
#[rustc_diagnostic_item = "verus::builtin::Ghost::view"]
Expand Down
176 changes: 25 additions & 151 deletions source/builtin_macros/src/attr_rewrite.rs
View file
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
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

0 comments on commit 32c15dc

Please sign in to comment.