Implement #[kani::async_proof] attribute
#1430
Conversation
fzaiser
changed the title
#[kani::async_proof] attribute
| let attrs = fn_item.attrs; | ||
| let vis = fn_item.vis; | ||
| let sig = fn_item.sig; | ||
| assert!(sig.asyncness.is_some(), "#[kani::async_proof] can only be applied to async functions"); |
There was a problem hiding this comment.
Should probably have a test for this
library/kani_macros/src/lib.rs
Outdated
| #[cfg(kani)] | ||
| #[proc_macro_attribute] | ||
| pub fn async_proof(attr: TokenStream, item: TokenStream) -> TokenStream { | ||
| assert!(attr.to_string().is_empty(), "#[kani::async_proof] does not take any arguments"); |
There was a problem hiding this comment.
This is true for now, but will probably not be true in the future if we want to control which executor we use
There was a problem hiding this comment.
Agreed. I'll mention that this may change in the future.
|
|
||
| #[cfg(kani)] | ||
| #[proc_macro_attribute] | ||
| pub fn async_proof(attr: TokenStream, item: TokenStream) -> TokenStream { |
There was a problem hiding this comment.
This macro is more extensive than some of the others, and could probably use a comment.
|
Do we actually need a separate attribute for async? Couldn't the existing |
@camshaft Thanks for the suggestion! I had considered that, but thought it would be better to keep them separate: we expect to extend the attribute later on to allow the user to choose different Kani executors: |
|
Opened #1464 to discuss |
Description of changes:
This adds an attribute
#[kani::async_proof]to make model-checkingasyncfunctions more ergonomic. Before, one had to manually callkani::block_onon anasyncfunction.Call-outs:
This adds the dependencies
synandquotetokani_macros.Testing:
How is this change tested? Added a regression test.
Is this a refactor change? No
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.