Implement #[kani::async_proof] attribute (rust-lang#1430)

Author: fzaiser

Cargo.lock

@@ -338,6 +338,10 @@ dependencies = [
 [[package]]
 name = "kani_macros"
 version = "0.7.0"
+dependencies = [
+ "quote",
+ "syn",
+]
 
 [[package]]
 name = "kani_metadata"

library/kani_macros/Cargo.toml

@@ -12,3 +12,5 @@ publish = false
 proc-macro = true
 
 [dependencies]
+quote = "1.0.20"
+syn = { version = "1.0.98", features = ["full"] }

library/kani_macros/src/lib.rs

@@ -10,6 +10,11 @@
 
 // proc_macro::quote is nightly-only, so we'll cobble things together instead
 use proc_macro::TokenStream;
+#[cfg(kani)]
+use {
+    quote::quote,
+    syn::{parse_macro_input, ItemFn},
+};
 
 #[cfg(all(not(kani), not(test)))]
 #[proc_macro_attribute]
@@ -39,7 +44,7 @@ pub fn proof(_attr: TokenStream, item: TokenStream) -> TokenStream {
 pub fn proof(attr: TokenStream, item: TokenStream) -> TokenStream {
     let mut result = TokenStream::new();
 
-    assert!(attr.to_string().is_empty(), "#[kani::proof] does not take any arguments");
+    assert!(attr.is_empty(), "#[kani::proof] does not take any arguments");
     result.extend("#[kanitool::proof]".parse::<TokenStream>().unwrap());
     // no_mangle is a temporary hack to make the function "public" so it gets codegen'd
     result.extend("#[no_mangle]".parse::<TokenStream>().unwrap());
@@ -51,6 +56,58 @@ pub fn proof(attr: TokenStream, item: TokenStream) -> TokenStream {
     // )
 }
 
+#[cfg(not(kani))]
+#[proc_macro_attribute]
+/// Treats #[kani::async_proof] like a normal #[kani::proof] if Kani is not active
+pub fn async_proof(attr: TokenStream, item: TokenStream) -> TokenStream {
+    proof(attr, item)
+}
+
+#[cfg(kani)]
+#[proc_macro_attribute]
+/// Translates #[kani::async_proof] to a #[kani::proof] harness that calls `kani::block_on`, if Kani is active
+///
+/// Specifically, it translates
+/// ```ignore
+/// #[kani::async_proof]
+/// #[attribute]
+/// pub async fn harness() { ... }
+/// ```
+/// to
+/// ```ignore
+/// #[kani::proof]
+/// #[attribute]
+/// pub fn harness() {
+///   async fn harness() { ... }
+///   kani::block_on(harness())
+/// }
+/// ```
+pub fn async_proof(attr: TokenStream, item: TokenStream) -> TokenStream {
+    assert!(attr.is_empty(), "#[kani::async_proof] does not take any arguments for now");
+    let fn_item = parse_macro_input!(item as ItemFn);
+    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");
+    assert!(
+        sig.inputs.is_empty(),
+        "#[kani::async_proof] can only be applied to functions without inputs"
+    );
+    let mut modified_sig = sig.clone();
+    modified_sig.asyncness = None;
+    let body = fn_item.block;
+    let fn_name = &sig.ident;
+    quote!(
+        #[kani::proof]
+        #(#attrs)*
+        #vis #modified_sig {
+            #sig #body
+            kani::block_on(#fn_name())
+        }
+    )
+    .into()
+}
+
 #[cfg(not(kani))]
 #[proc_macro_attribute]
 pub fn unwind(_attr: TokenStream, item: TokenStream) -> TokenStream {

tests/expected/async_proof/expected

@@ -0,0 +1,8 @@
+error: custom attribute panicked
+#[kani::async_proof] does not take any arguments for now
+
+error: custom attribute panicked
+#[kani::async_proof] can only be applied to async functions
+
+error: custom attribute panicked
+#[kani::async_proof] can only be applied to functions without inputs

tests/expected/async_proof/main.rs

@@ -0,0 +1,17 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// compile-flags: --edition 2018
+
+// Tests that the #[kani::async_proof] attribute works correctly
+
+fn main() {}
+
+#[kani::async_proof(foo)]
+async fn test_async_proof_with_arguments() {}
+
+#[kani::async_proof]
+fn test_async_proof_on_sync_function() {}
+
+#[kani::async_proof]
+async fn test_async_proof_on_function_with_inputs(_: ()) {}

tests/kani/AsyncAwait/main.rs

@@ -3,7 +3,7 @@
 //
 // compile-flags: --edition 2018
 
-// Tests that the language constructs `async { .. .}` blocks, `async fn`, and `.await` work correctly.
+// Tests that the language constructs `async { ... }` blocks, `async fn`, and `.await` work correctly.
 
 use std::{
     future::Future,
@@ -13,6 +13,22 @@ use std::{
 
 fn main() {}
 
+#[kani::async_proof]
+#[kani::unwind(2)]
+async fn test_async_proof_harness() {
+    let async_block_result = async { 42 }.await;
+    let async_fn_result = async_fn().await;
+    assert_eq!(async_block_result, async_fn_result);
+}
+
+#[kani::async_proof]
+#[kani::unwind(2)]
+pub async fn test_async_proof_harness_pub() {
+    let async_block_result = async { 42 }.await;
+    let async_fn_result = async_fn().await;
+    assert_eq!(async_block_result, async_fn_result);
+}
+
 #[kani::proof]
 #[kani::unwind(2)]
 fn test_async_await() {