Enable Concrete Playback Unit tests to run with --cfg kani (#2353)

Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>

library/kani/Cargo.toml

@@ -12,4 +12,4 @@ publish = false
 kani_macros = { path = "../kani_macros" }
 
 [features]
-concrete_playback = []
+concrete_playback = ["kani_macros/concrete_playback"]

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 = []

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();

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

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;

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}

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"] }

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<u8, u8> = kani::any();
+        let result_2: Result<u8, u8> = kani::any();
+        assert!(!(result_1 == Ok(101) && result_2 == Err(102)));
+    }
+
+    #[test]
+    fn kani_concrete_playback_harness_15598097466099501582() {
+        let concrete_vals: Vec<Vec<u8>> = vec![
+            // 1
+            vec![1],
+            // 101
+            vec![101],
+            // 0
+            vec![0],
+            // 102
+            vec![102],
+        ];
+        kani::concrete_playback_run(concrete_vals, harness);
+    }
+}