Add more tests and fix typo in kani_core

library/kani_core/src/arbitrary.rs

@@ -34,7 +34,7 @@ macro_rules! generate_arbitrary {
                         unsafe { crate::kani::any_raw_internal::<Self>() }
                     }
                     fn any_array<const MAX_ARRAY_LENGTH: usize>() -> [Self; MAX_ARRAY_LENGTH] {
-                        unsafe { crate::kani::any_raw_array::<Self; MAX_ARRAY_LENGTH>() }
+                        unsafe { crate::kani::any_raw_array::<Self, MAX_ARRAY_LENGTH>() }
                     }
                 }
             };

tests/script-based-pre/playback_expected/config.yml

@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: playback.sh
+expected: expected

tests/script-based-pre/playback_expected/expected

@@ -0,0 +1,8 @@
+[TEST] Generate test for playback_contract.rs...
+Verification failed for - check_modify_slice
+Result for playback_contract.rs: test result: FAILED. 1 passed; 1 failed
+
+[TEST] Generate test for playback_stubs.rs...
+Verification failed for - check_lt_0
+Verification failed for - check_bad_stub
+Result for playback_stubs.rs: test result: FAILED. 1 passed; 1 failed

tests/script-based-pre/playback_expected/playback.sh

@@ -0,0 +1,39 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+# This will run Kani verification in every `src/*.rs` file followed by playback command.
+# Expected output is generated from individual expected files.
+set -o nounset
+
+run() {
+  input_rs=${1:?"Missing input file"}
+
+  echo "[TEST] Generate test for $input_rs..."
+  kani ${input_rs} \
+    -Z concrete-playback --concrete-playback=inplace \
+    -Z function-contracts -Z stubbing --output-format terse
+
+  # Note that today one of the tests will succeed since the contract pre-conditions are not inserted by Kani.
+  # Hopefully this will change with https://github.com/model-checking/kani/issues/3326
+  echo "[TEST] Run test for $input_rs..."
+  summary=$(kani playback -Z concrete-playback ${input_rs} -- kani_concrete_playback | grep "test result")
+  echo "Result for $input_rs: $summary"
+}
+
+ROOT_DIR=$(git rev-parse --show-toplevel)
+MODIFIED_DIR=modified
+rm -rf $MODIFIED_DIR
+mkdir $MODIFIED_DIR
+
+for rs in src/*.rs
+do
+  [[ -e "${rs}" ]] || exit 1
+  echo "Running ${rs}"
+  cp "$rs" $MODIFIED_DIR
+  pushd $MODIFIED_DIR
+  run $(basename $rs)
+  popd
+done
+
+  # Cleanup
+rm -rf $MODIFIED_DIR

tests/script-based-pre/playback_expected/src/playback_stubs.rs

@@ -0,0 +1,34 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Check that Kani playback works with stubs.
+#![allow(dead_code)]
+
+fn is_zero(val: u8) -> bool {
+    val == 0
+}
+
+fn not_zero(val: u8) -> bool {
+    val != 0
+}
+
+/// Add a harness that will fail due to incorrect stub but the test will succeed.
+#[kani::proof]
+#[kani::stub(is_zero, not_zero)]
+fn check_bad_stub() {
+    assert!(is_zero(kani::any()))
+}
+
+fn lt_zero(val: i8) -> bool {
+    val < 0
+}
+
+fn lt_ten(val: i8) -> bool {
+    val < 10
+}
+
+/// Add a harness that will fail in an equivalent way.
+#[kani::proof]
+#[kani::stub(lt_zero, lt_ten)]
+fn check_lt_0() {
+    assert!(lt_zero(kani::any()))
+}