diff --git a/library/kani/Cargo.toml b/library/kani/Cargo.toml index f0ba79c3c02e..05797c2b79a2 100644 --- a/library/kani/Cargo.toml +++ b/library/kani/Cargo.toml @@ -12,4 +12,4 @@ publish = false kani_macros = { path = "../kani_macros" } [features] -concrete_playback = [] +concrete_playback = ["kani_macros/concrete_playback"] diff --git a/library/kani_macros/Cargo.toml b/library/kani_macros/Cargo.toml index 4dbbd5edd244..5ebeddd665c2 100644 --- a/library/kani_macros/Cargo.toml +++ b/library/kani_macros/Cargo.toml @@ -16,3 +16,6 @@ proc-macro2 = "1.0" proc-macro-error = "1.0.4" quote = "1.0.20" syn = { version = "1.0.98", features = ["full"] } + +[features] +concrete_playback = [] diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 27a811a7bd3a..c0108d06c530 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -19,7 +19,7 @@ use { syn::{parse_macro_input, ItemFn}, }; -#[cfg(not(kani))] +#[cfg(any(not(kani), feature = "concrete_playback"))] #[proc_macro_attribute] pub fn proof(_attr: TokenStream, item: TokenStream) -> TokenStream { // Leave the code intact, so it can be easily be edited in an IDE, @@ -38,7 +38,7 @@ pub fn proof(_attr: TokenStream, item: TokenStream) -> TokenStream { /// Marks a Kani proof harness /// /// For async harnesses, this will call [`kani::block_on`] (see its documentation for more information). -#[cfg(kani)] +#[cfg(all(kani, not(feature = "concrete_playback")))] #[proc_macro_attribute] pub fn proof(attr: TokenStream, item: TokenStream) -> TokenStream { let fn_item = parse_macro_input!(item as ItemFn); @@ -98,14 +98,14 @@ pub fn proof(attr: TokenStream, item: TokenStream) -> TokenStream { } } -#[cfg(not(kani))] +#[cfg(any(not(kani), feature = "concrete_playback"))] #[proc_macro_attribute] pub fn should_panic(_attr: TokenStream, item: TokenStream) -> TokenStream { // No-op in non-kani mode item } -#[cfg(kani)] +#[cfg(all(kani, not(feature = "concrete_playback")))] #[proc_macro_attribute] pub fn should_panic(attr: TokenStream, item: TokenStream) -> TokenStream { assert!(attr.is_empty(), "`#[kani::should_panic]` does not take any arguments currently"); @@ -117,7 +117,7 @@ pub fn should_panic(attr: TokenStream, item: TokenStream) -> TokenStream { result } -#[cfg(not(kani))] +#[cfg(any(not(kani), feature = "concrete_playback"))] #[proc_macro_attribute] pub fn unwind(_attr: TokenStream, item: TokenStream) -> TokenStream { // When the config is not kani, we should leave the function alone @@ -127,7 +127,7 @@ pub fn unwind(_attr: TokenStream, item: TokenStream) -> TokenStream { /// Set Loop unwind limit for proof harnesses /// The attribute '#[kani::unwind(arg)]' can only be called alongside '#[kani::proof]'. /// arg - Takes in a integer value (u32) that represents the unwind value for the harness. -#[cfg(kani)] +#[cfg(all(kani, not(feature = "concrete_playback")))] #[proc_macro_attribute] pub fn unwind(attr: TokenStream, item: TokenStream) -> TokenStream { let mut result = TokenStream::new(); @@ -140,7 +140,7 @@ pub fn unwind(attr: TokenStream, item: TokenStream) -> TokenStream { result } -#[cfg(not(kani))] +#[cfg(any(not(kani), feature = "concrete_playback"))] #[proc_macro_attribute] pub fn stub(_attr: TokenStream, item: TokenStream) -> TokenStream { // When the config is not kani, we should leave the function alone @@ -154,7 +154,7 @@ pub fn stub(_attr: TokenStream, item: TokenStream) -> TokenStream { /// # Arguments /// * `original` - The function or method to replace, specified as a path. /// * `replacement` - The function or method to use as a replacement, specified as a path. -#[cfg(kani)] +#[cfg(all(kani, not(feature = "concrete_playback")))] #[proc_macro_attribute] pub fn stub(attr: TokenStream, item: TokenStream) -> TokenStream { let mut result = TokenStream::new(); @@ -167,7 +167,7 @@ pub fn stub(attr: TokenStream, item: TokenStream) -> TokenStream { result } -#[cfg(not(kani))] +#[cfg(any(not(kani), feature = "concrete_playback"))] #[proc_macro_attribute] pub fn solver(_attr: TokenStream, item: TokenStream) -> TokenStream { // No-op in non-kani mode @@ -178,7 +178,7 @@ pub fn solver(_attr: TokenStream, item: TokenStream) -> TokenStream { /// The attribute `#[kani::solver(arg)]` can only be used alongside `#[kani::proof]`` /// /// arg - name of solver, e.g. kissat -#[cfg(kani)] +#[cfg(all(kani, not(feature = "concrete_playback")))] #[proc_macro_attribute] pub fn solver(attr: TokenStream, item: TokenStream) -> TokenStream { let mut result = TokenStream::new(); diff --git a/tests/script-based-pre/playback_with_cfg_kani/config.yml b/tests/script-based-pre/playback_with_cfg_kani/config.yml new file mode 100644 index 000000000000..a487f834d1e7 --- /dev/null +++ b/tests/script-based-pre/playback_with_cfg_kani/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: playback_with_cfg_kani.sh +expected: playback_with_cfg_kani.expected diff --git a/tests/script-based-pre/playback_with_cfg_kani/playback_with_cfg_kani.expected b/tests/script-based-pre/playback_with_cfg_kani/playback_with_cfg_kani.expected new file mode 100644 index 000000000000..042d881412c2 --- /dev/null +++ b/tests/script-based-pre/playback_with_cfg_kani/playback_with_cfg_kani.expected @@ -0,0 +1,4 @@ +failures: + harnesses::kani_concrete_playback_harness_15598097466099501582 + +test result: FAILED. 0 passed; 1 failed; 0 ignored; 0 measured; 0 filtered out; diff --git a/tests/script-based-pre/playback_with_cfg_kani/playback_with_cfg_kani.sh b/tests/script-based-pre/playback_with_cfg_kani/playback_with_cfg_kani.sh new file mode 100755 index 000000000000..fd2eeec37e38 --- /dev/null +++ b/tests/script-based-pre/playback_with_cfg_kani/playback_with_cfg_kani.sh @@ -0,0 +1,34 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +set +e + +OUT_DIR=sample_crate/target + +echo +echo "Starting output file check..." +echo + + +# Check if cargo is installed +if ! command -v cargo &> /dev/null; then + echo "cargo command not found. Please install Rust and Cargo." + exit 1 +fi + +echo "Running cargo test on the unit test ..." +echo + +cd sample_crate/ + +output=$(grep 'channel = ' ../../../../rust-toolchain.toml | cut -d '"' -f 2) +echo "$output" + +# Run cargo test on the unit test +RUSTFLAGS="--cfg=kani" cargo +${output} test 2>/dev/null + +cd .. + +# Try to leave a clean output folder at the end +rm -rf ${OUT_DIR} diff --git a/tests/script-based-pre/playback_with_cfg_kani/sample_crate/Cargo.toml b/tests/script-based-pre/playback_with_cfg_kani/sample_crate/Cargo.toml new file mode 100644 index 000000000000..053feb5be3b3 --- /dev/null +++ b/tests/script-based-pre/playback_with_cfg_kani/sample_crate/Cargo.toml @@ -0,0 +1,13 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +[package] +name = "sample_crate" +version = "0.1.0" +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] + +[dev-dependencies] +kani = { path = "../../../../library/kani", features = ["concrete_playback"] } diff --git a/tests/script-based-pre/playback_with_cfg_kani/sample_crate/src/main.rs b/tests/script-based-pre/playback_with_cfg_kani/sample_crate/src/main.rs new file mode 100644 index 000000000000..7d3dd90a9aac --- /dev/null +++ b/tests/script-based-pre/playback_with_cfg_kani/sample_crate/src/main.rs @@ -0,0 +1,33 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// This test checks that running the unit test generated using the concrete playback feature +// with `RUSTFLAGS="--cfg=kani" cargo +nightly test doesn't cause a compilation error. +// There is an existing UI test to generate the unit test itself (in kani/tests/ui/concrete-playback/result). + +fn main() {} + +#[cfg(kani)] +mod harnesses { + #[kani::proof] + fn harness() { + let result_1: Result = kani::any(); + let result_2: Result = kani::any(); + assert!(!(result_1 == Ok(101) && result_2 == Err(102))); + } + + #[test] + fn kani_concrete_playback_harness_15598097466099501582() { + let concrete_vals: Vec> = vec![ + // 1 + vec![1], + // 101 + vec![101], + // 0 + vec![0], + // 102 + vec![102], + ]; + kani::concrete_playback_run(concrete_vals, harness); + } +}