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

Jump to bottom

allow #![trigger f(x)] on ensures (of broadcast_forall) functions #713

Merged
merged 1 commit into from
Jul 28, 2023
Merged

allow #![trigger f(x)] on ensures (of broadcast_forall) functions #713

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
1 change: 1 addition & 0 deletions dependencies/syn/src/gen/clone.rs
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

1 change: 1 addition & 0 deletions dependencies/syn/src/gen/debug.rs
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion dependencies/syn/src/gen/eq.rs
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

1 change: 1 addition & 0 deletions dependencies/syn/src/gen/fold.rs
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

1 change: 1 addition & 0 deletions dependencies/syn/src/gen/hash.rs
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

3 changes: 3 additions & 0 deletions dependencies/syn/src/gen/visit.rs
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

3 changes: 3 additions & 0 deletions dependencies/syn/src/gen/visit_mut.rs
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

7 changes: 6 additions & 1 deletion dependencies/syn/src/verus.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -120,6 +120,7 @@ ast_struct! {

ast_struct! {
pub struct Ensures {
pub attrs: Vec<Attribute>,
pub token: Token![ensures],
pub exprs: Specification,
}
Expand Down Expand Up @@ -428,8 +429,12 @@ pub mod parsing {
#[cfg_attr(doc_cfg, doc(cfg(feature = "parsing")))]
impl Parse for Ensures {
fn parse(input: ParseStream) -> Result<Self> {
let mut attrs = Vec::new();
let token = input.parse()?;
attr::parsing::parse_inner(input, &mut attrs)?;
Ok(Ensures {
token: input.parse()?,
attrs,
token,
exprs: input.parse()?,
})
}
Expand Down
5 changes: 5 additions & 0 deletions dependencies/syn/syn.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -846,6 +846,11 @@
"any": []
},
"fields": {
"attrs": {
"vec": {
"syn": "Attribute"
}
},
"token": {
"token": "Ensures"
},
Expand Down
3 changes: 3 additions & 0 deletions dependencies/syn/tests/debug/gen.rs
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

214 changes: 135 additions & 79 deletions source/builtin_macros/src/syntax.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -315,23 +315,63 @@ impl Visitor {
));
}
}
if let Some(Ensures { token, mut exprs }) = ensures {
if let Some(Ensures { attrs, token, mut exprs }) = ensures {
if exprs.exprs.len() > 0 {
for expr in exprs.exprs.iter_mut() {
self.visit_expr_mut(expr);
}
if let Some((p, ty)) = ret_pat {
stmts.push(Stmt::Semi(
Expr::Verbatim(
quote_spanned!(token.span => ::builtin::ensures(|#p: #ty| [#exprs])),
),
Semi { spans: [token.span] },
));
} else {
stmts.push(Stmt::Semi(
Expr::Verbatim(quote_spanned!(token.span => ::builtin::ensures([#exprs]))),
Semi { spans: [token.span] },
));
let cont = match self.extract_quant_triggers(attrs, token.span) {
Ok(
found @ (ExtractQuantTriggersFound::Auto
| ExtractQuantTriggersFound::Triggers(..)),
) => {
if exprs.exprs.len() == 0 {
let err =
"when using #![trigger f(x)], at least one ensures is required";
let expr =
Expr::Verbatim(quote_spanned!(token.span => compile_error!(#err)));
stmts.push(Stmt::Semi(expr, Semi { spans: [token.span] }));
false
} else {
let e = take_expr(&mut exprs.exprs[0]);
match found {
ExtractQuantTriggersFound::Auto => {
exprs.exprs[0] = Expr::Verbatim(
quote_spanned!(exprs.exprs[0].span() => #[verus::internal(auto_trigger)] (#e)),
);
}
ExtractQuantTriggersFound::Triggers(tuple) => {
exprs.exprs[0] = Expr::Verbatim(
quote_spanned!(exprs.exprs[0].span() => ::builtin::with_triggers(#tuple, #e)),
);
}
ExtractQuantTriggersFound::None => unreachable!(),
}
true
}
}
Ok(ExtractQuantTriggersFound::None) => true,
Err(err_expr) => {
exprs.exprs[0] = err_expr;
false
}
};
if cont {
if let Some((p, ty)) = ret_pat {
stmts.push(Stmt::Semi(
Expr::Verbatim(
quote_spanned!(token.span => ::builtin::ensures(|#p: #ty| [#exprs])),
),
Semi { spans: [token.span] },
));
} else {
stmts.push(Stmt::Semi(
Expr::Verbatim(
quote_spanned!(token.span => ::builtin::ensures([#exprs])),
),
Semi { spans: [token.span] },
));
}
}
}
}
Expand Down Expand Up @@ -956,7 +996,7 @@ impl Visitor {
_ => panic!("expected closure for quantifier"),
};

match extract_quant_triggers(inner_attrs, span) {
match self.extract_quant_triggers(inner_attrs, span) {
Ok(ExtractQuantTriggersFound::Auto) => match &mut *arg {
Expr::Closure(closure) => {
let body = take_expr(&mut closure.body);
Expand Down Expand Up @@ -1028,8 +1068,12 @@ impl Visitor {
stmts.push(stmt_with_semi!(token.span => ::builtin::invariant_ensures([#exprs])));
}
}
if let Some(Ensures { token, mut exprs }) = ensures {
if exprs.exprs.len() > 0 {
if let Some(Ensures { token, mut exprs, attrs }) = ensures {
if attrs.len() > 0 {
let err = "outer attributes only allowed on function's ensures";
let expr = Expr::Verbatim(quote_spanned!(token.span => compile_error!(#err)));
stmts.push(Stmt::Semi(expr, Semi { spans: [token.span] }));
} else if exprs.exprs.len() > 0 {
for expr in exprs.exprs.iter_mut() {
self.visit_expr_mut(expr);
}
Expand All @@ -1049,66 +1093,70 @@ impl Visitor {
}
self.inside_ghost -= 1;
}
}

enum ExtractQuantTriggersFound {
Auto,
Triggers(ExprTuple),
None,
}
fn extract_quant_triggers(
&mut self,
inner_attrs: Vec<Attribute>,
span: Span,
) -> Result<ExtractQuantTriggersFound, Expr> {
let mut triggers: Vec<Expr> = Vec::new();
for attr in inner_attrs {
let trigger: syn_verus::Result<syn_verus::Specification> =
syn_verus::parse2(attr.tokens.clone());
let path_segments_str =
attr.path.segments.iter().map(|x| x.ident.to_string()).collect::<Vec<_>>();
let ident_str = match &path_segments_str[..] {
[attr_name] => Some(attr_name),
_ => None,
};
match (trigger, ident_str) {
(Ok(trigger), Some(id)) if id == &"auto" && trigger.exprs.len() == 0 => {
return Ok(ExtractQuantTriggersFound::Auto);
}
(Ok(trigger), Some(id)) if id == &"trigger" => {
let mut exprs = trigger.exprs;
for expr in exprs.iter_mut() {
self.visit_expr_mut(expr);
}
let tuple = ExprTuple { attrs: vec![], paren_token: Paren(span), elems: exprs };
triggers.push(Expr::Tuple(tuple));
}
(Err(err), _) => {
let span = attr.span();
let err = err.to_string();

fn extract_quant_triggers(
inner_attrs: Vec<Attribute>,
span: Span,
) -> Result<ExtractQuantTriggersFound, Expr> {
let mut triggers: Vec<Expr> = Vec::new();
for attr in inner_attrs {
let trigger: syn_verus::Result<syn_verus::Specification> =
syn_verus::parse2(attr.tokens.clone());
let path_segments_str =
attr.path.segments.iter().map(|x| x.ident.to_string()).collect::<Vec<_>>();
let ident_str = match &path_segments_str[..] {
[attr_name] => Some(attr_name),
_ => None,
};
match (trigger, ident_str) {
(Ok(trigger), Some(id)) if id == &"auto" && trigger.exprs.len() == 0 => {
return Ok(ExtractQuantTriggersFound::Auto);
}
(Ok(trigger), Some(id)) if id == &"trigger" => {
let tuple =
ExprTuple { attrs: vec![], paren_token: Paren(span), elems: trigger.exprs };
triggers.push(Expr::Tuple(tuple));
return Err(Expr::Verbatim(quote_spanned!(span => compile_error!(#err))));
}
_ => {
let span = attr.span();
return Err(Expr::Verbatim(
quote_spanned!(span => compile_error!("expected trigger")),
));
}
}
(Err(err), _) => {
let span = attr.span();
let err = err.to_string();
}

return Err(Expr::Verbatim(quote_spanned!(span => compile_error!(#err))));
}
_ => {
let span = attr.span();
return Err(Expr::Verbatim(
quote_spanned!(span => compile_error!("expected trigger")),
));
Ok(if triggers.len() > 0 {
let mut elems = Punctuated::new();
for elem in triggers {
elems.push(elem);
elems.push_punct(Token![,](span));
}
}
ExtractQuantTriggersFound::Triggers(ExprTuple {
attrs: vec![],
paren_token: Paren(span),
elems,
})
} else {
ExtractQuantTriggersFound::None
})
}
}

Ok(if triggers.len() > 0 {
let mut elems = Punctuated::new();
for elem in triggers {
elems.push(elem);
elems.push_punct(Token![,](span));
}
ExtractQuantTriggersFound::Triggers(ExprTuple {
attrs: vec![],
paren_token: Paren(span),
elems,
})
} else {
ExtractQuantTriggersFound::None
})
enum ExtractQuantTriggersFound {
Auto,
Triggers(ExprTuple),
None,
}

impl VisitMut for Visitor {
Expand Down Expand Up @@ -1661,7 +1709,7 @@ impl VisitMut for Visitor {
Expr::AssertForall(assert) => {
let span = assert.assert_token.span;
let mut arg = assert.expr;
match extract_quant_triggers(assert.attrs, span) {
match self.extract_quant_triggers(assert.attrs, span) {
Ok(ExtractQuantTriggersFound::Auto) => {
arg = Box::new(Expr::Verbatim(
quote_spanned!(arg.span() => #[verus::internal(auto_trigger)] #arg),
Expand Down Expand Up @@ -1731,16 +1779,24 @@ impl VisitMut for Visitor {
stmts.push(stmt_with_semi!(
token.span => ::builtin::requires([#exprs])));
}
if let Some(Ensures { token, mut exprs }) = ensures {
for expr in exprs.exprs.iter_mut() {
self.visit_expr_mut(expr);
}
if let Some((p, ty)) = ret_pat {
stmts.push(stmt_with_semi!(
token.span => ::builtin::ensures(|#p: #ty| [#exprs])));
if let Some(Ensures { token, mut exprs, attrs }) = ensures {
if attrs.len() > 0 {
let err = "outer attributes only allowed on function's ensures";
let expr = Expr::Verbatim(
quote_spanned!(token.span => compile_error!(#err)),
);
stmts.push(Stmt::Semi(expr, Semi { spans: [token.span] }));
} else {
stmts.push(stmt_with_semi!(
token.span => ::builtin::ensures([#exprs])));
for expr in exprs.exprs.iter_mut() {
self.visit_expr_mut(expr);
}
if let Some((p, ty)) = ret_pat {
stmts.push(stmt_with_semi!(
token.span => ::builtin::ensures(|#p: #ty| [#exprs])));
} else {
stmts.push(stmt_with_semi!(
token.span => ::builtin::ensures([#exprs])));
}
}
}
self.inside_ghost -= 1;
Expand Down
Loading
Loading