diff --git a/library/kani/src/futures.rs b/library/kani/src/futures.rs index cd3b9ad60597..637f24a80f6a 100644 --- a/library/kani/src/futures.rs +++ b/library/kani/src/futures.rs @@ -182,10 +182,12 @@ impl Future for JoinHandle { #[crate::unstable(feature = "async-lib", issue = 2559, reason = "experimental async support")] pub fn spawn + Sync + 'static>(fut: F) -> JoinHandle { unsafe { - GLOBAL_EXECUTOR - .as_mut() - .expect("`spawn` should only be called within `block_on_with_spawn`") - .spawn(fut) + if let Some(executor) = GLOBAL_EXECUTOR.as_mut() { + executor.spawn(fut) + } else { + // An explicit panic instead of `.expect(...)` has better location information in Kani's output + panic!("`spawn` should only be called within `block_on_with_spawn`") + } } } diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 6cded7052369..858efc6388d0 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -22,7 +22,12 @@ use regular as attr_impl; /// Marks a Kani proof harness /// -/// For async harnesses, this will call [`kani::block_on`] (see its documentation for more information). +/// For async harnesses, this will call [`block_on`] to drive the future to completion (see its documentation for more information). +/// +/// If you want to spawn tasks in an async harness, you have to pass a schedule to the `#[kani::proof]` attribute, +/// e.g. `#[kani::proof(schedule = kani::RoundRobin::default())]`. +/// This will wrap the async function in a call to [`block_on_with_spawn`] (see its documentation for more information). +#[proc_macro_error] #[proc_macro_attribute] pub fn proof(attr: TokenStream, item: TokenStream) -> TokenStream { attr_impl::proof(attr, item) @@ -93,10 +98,13 @@ pub fn derive_arbitrary(item: TokenStream) -> TokenStream { /// This code should only be activated when pre-building Kani's sysroot. #[cfg(kani_sysroot)] mod sysroot { + use proc_macro_error::{abort, abort_call_site}; + use super::*; use { quote::{format_ident, quote}, + syn::parse::{Parse, ParseStream}, syn::{parse_macro_input, ItemFn}, }; @@ -126,7 +134,31 @@ mod sysroot { }; } + struct ProofOptions { + schedule: Option, + } + + impl Parse for ProofOptions { + fn parse(input: ParseStream) -> syn::Result { + if input.is_empty() { + Ok(ProofOptions { schedule: None }) + } else { + let ident = input.parse::()?; + if ident != "schedule" { + abort_call_site!("`{}` is not a valid option for `#[kani::proof]`.", ident; + help = "did you mean `schedule`?"; + note = "for now, `schedule` is the only option for `#[kani::proof]`."; + ); + } + let _ = input.parse::()?; + let schedule = Some(input.parse::()?); + Ok(ProofOptions { schedule }) + } + } + } + pub fn proof(attr: TokenStream, item: TokenStream) -> TokenStream { + let proof_options = parse_macro_input!(attr as ProofOptions); let fn_item = parse_macro_input!(item as ItemFn); let attrs = fn_item.attrs; let vis = fn_item.vis; @@ -138,9 +170,13 @@ mod sysroot { #[kanitool::proof] ); - assert!(attr.is_empty(), "#[kani::proof] does not take any arguments currently"); - if sig.asyncness.is_none() { + if proof_options.schedule.is_some() { + abort_call_site!( + "`#[kani::proof(schedule = ...)]` can only be used with `async` functions."; + help = "did you mean to make this function `async`?"; + ); + } // Adds `#[kanitool::proof]` and other attributes quote!( #kani_attributes @@ -152,32 +188,44 @@ mod sysroot { // For async functions, it translates to a synchronous function that calls `kani::block_on`. // Specifically, it translates // ```ignore - // #[kani::async_proof] + // #[kani::proof] // #[attribute] // pub async fn harness() { ... } // ``` // to // ```ignore - // #[kani::proof] + // #[kanitool::proof] // #[attribute] // pub fn harness() { // async fn harness() { ... } // kani::block_on(harness()) + // // OR + // kani::spawnable_block_on(harness(), schedule) + // // where `schedule` was provided as an argument to `#[kani::proof]`. // } // ``` - assert!( - sig.inputs.is_empty(), - "#[kani::proof] cannot be applied to async functions that take inputs for now" - ); + if !sig.inputs.is_empty() { + abort!( + sig.inputs, + "`#[kani::proof]` cannot be applied to async functions that take arguments for now"; + help = "try removing the arguments"; + ); + } let mut modified_sig = sig.clone(); modified_sig.asyncness = None; let fn_name = &sig.ident; + let schedule = proof_options.schedule; + let block_on_call = if let Some(schedule) = schedule { + quote!(kani::block_on_with_spawn(#fn_name(), #schedule)) + } else { + quote!(kani::block_on(#fn_name())) + }; quote!( #kani_attributes #(#attrs)* #vis #modified_sig { #sig #body - kani::block_on(#fn_name()) + #block_on_call } ) .into() diff --git a/tests/expected/async_proof/expected b/tests/expected/async_proof/expected index d3da9cd06188..25d5a330f464 100644 --- a/tests/expected/async_proof/expected +++ b/tests/expected/async_proof/expected @@ -1,5 +1,3 @@ -error: custom attribute panicked -#[kani::proof] does not take any arguments currently +`foo` is not a valid option for `#[kani::proof]`. -error: custom attribute panicked -#[kani::proof] cannot be applied to async functions that take inputs for now +`#[kani::proof]` cannot be applied to async functions that take arguments for now diff --git a/tests/expected/async_proof/main.rs b/tests/expected/async_proof/main.rs index a050c50dd428..be09cc2e974e 100644 --- a/tests/expected/async_proof/main.rs +++ b/tests/expected/async_proof/main.rs @@ -8,7 +8,7 @@ fn main() {} #[kani::proof(foo)] -async fn test_async_proof_with_arguments() {} +async fn test_async_proof_with_options() {} #[kani::proof] -async fn test_async_proof_on_function_with_inputs(_: ()) {} +async fn test_async_proof_on_function_with_arguments(_: ()) {} diff --git a/tests/kani/AsyncAwait/spawn.rs b/tests/kani/AsyncAwait/spawn.rs index 3bef244ef547..76583f10d615 100644 --- a/tests/kani/AsyncAwait/spawn.rs +++ b/tests/kani/AsyncAwait/spawn.rs @@ -11,9 +11,24 @@ use std::sync::{ Arc, }; +#[kani::proof(schedule = kani::RoundRobin::default())] +#[kani::unwind(4)] +async fn round_robin_schedule() { + let x = Arc::new(AtomicI64::new(0)); // Surprisingly, Arc verified faster than Rc + let x2 = x.clone(); + let x3 = x2.clone(); + let handle = kani::spawn(async move { + x3.fetch_add(1, Ordering::Relaxed); + }); + kani::yield_now().await; + x2.fetch_add(1, Ordering::Relaxed); + handle.await; + assert_eq!(x.load(Ordering::Relaxed), 2); +} + #[kani::proof] #[kani::unwind(4)] -fn round_robin_schedule() { +fn round_robin_schedule_manual() { let x = Arc::new(AtomicI64::new(0)); // Surprisingly, Arc verified faster than Rc let x2 = x.clone(); kani::block_on_with_spawn( diff --git a/tests/ui/arguments-proof/expected b/tests/ui/arguments-proof/expected index e1e9392bd48e..7805c716c2ad 100644 --- a/tests/ui/arguments-proof/expected +++ b/tests/ui/arguments-proof/expected @@ -1 +1,3 @@ - = help: message: #[kani::proof] does not take any arguments +`some` is not a valid option for `#[kani::proof]`. + +the trait bound `NotASchedule: kani::futures::SchedulingStrategy` is not satisfied diff --git a/tests/ui/arguments-proof/main.rs b/tests/ui/arguments-proof/main.rs index 887d51e3b87b..6fefe3d5c27c 100644 --- a/tests/ui/arguments-proof/main.rs +++ b/tests/ui/arguments-proof/main.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --no-unwinding-checks +// kani-flags: --no-unwinding-checks -Z async-lib // This test is to check Kani's error handling for harnesses that have proof attributes // with arguments when the expected declaration takes no arguments. @@ -19,3 +19,12 @@ fn harness() { assert!(counter < 10); } } + +// Test what happens if the schedule option is incorrect: + +struct NotASchedule; + +#[kani::proof(schedule = NotASchedule)] +async fn test() { + assert!(true); +} diff --git a/tests/ui/arguments-proof/missing-unstable-flag/expected b/tests/ui/arguments-proof/missing-unstable-flag/expected new file mode 100644 index 000000000000..8d905c9fc2c9 --- /dev/null +++ b/tests/ui/arguments-proof/missing-unstable-flag/expected @@ -0,0 +1 @@ +error: Use of unstable feature `async-lib`: experimental async support diff --git a/tests/ui/arguments-proof/missing-unstable-flag/main.rs b/tests/ui/arguments-proof/missing-unstable-flag/main.rs new file mode 100644 index 000000000000..b68ed75afe26 --- /dev/null +++ b/tests/ui/arguments-proof/missing-unstable-flag/main.rs @@ -0,0 +1,12 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// compile-flags: --edition 2018 +// kani-flags: --no-unwinding-checks + +// This test is to check that the `schedule` argument requires an unstable flag. + +#[kani::proof(schedule = kani::RoundRobin::default())] +async fn test() { + assert!(true); +}