merge main:

docs/src/SUMMARY.md

@@ -22,6 +22,7 @@
     - [Coverage](./reference/experimental/coverage.md)
     - [Stubbing](./reference/experimental/stubbing.md)
     - [Contracts](./reference/experimental/contracts.md)
+    - [Loop Contracts](./reference/experimental/loop-contracts.md)
     - [Concrete Playback](./reference/experimental/concrete-playback.md)
 - [Application](./application.md)
   - [Comparison with other tools](./tool-comparison.md)

kani-driver/src/cbmc_output_parser.rs

@@ -296,12 +296,20 @@ pub struct TraceItem {
 /// Struct that represents a trace value.
 ///
 /// Note: this struct can have a lot of different fields depending on the value type.
-/// The fields included right now are relevant to primitive types.
+/// The fields included right now are relevant to primitive types and arrays.
 #[derive(Clone, Debug, Deserialize)]
 pub struct TraceValue {
     pub binary: Option<String>,
     pub data: Option<TraceData>,
     pub width: Option<u32>,
+    // Invariant: elements is Some iff binary, data, and width are None.
+    pub elements: Option<Vec<TraceArrayValue>>,
+}
+
+/// Struct that represents an element of an array in a trace.
+#[derive(Clone, Debug, Deserialize)]
+pub struct TraceArrayValue {
+    pub value: TraceValue,
 }
 
 /// Enum that represents a trace data item.

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

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

tests/script-based-pre/cargo_playback_array/playback_target.expected

@@ -0,0 +1,9 @@
+Failed Checks: index out of bounds: the length is less than or equal to the given index
+
+VERIFICATION:- FAILED
+
+INFO: Now modifying the source code to include the concrete playback unit test:
+
+running 1 test
+
+index out of bounds: the len is 65 but the index is

tests/script-based-pre/cargo_playback_array/playback_target.sh

@@ -0,0 +1,27 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+set +e
+
+function check_playback {
+  local OUTPUT=output.log
+  cargo kani playback "${@}" >& $OUTPUT
+  # Sort output so we can rely on the order.
+  echo "$(grep "test verify::.* ok" $OUTPUT | sort)"
+  echo
+  echo "======= Raw Output ======="
+  cat $OUTPUT
+  echo "=========================="
+  echo
+  rm $OUTPUT
+}
+
+pushd sample_crate > /dev/null
+cargo clean
+
+cargo kani --concrete-playback inplace -Z concrete-playback
+check_playback -Z concrete-playback
+
+cargo clean
+popd > /dev/null

tests/script-based-pre/cargo_playback_array/sample_crate/Cargo.toml

@@ -0,0 +1,10 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "sample_crate"
+version = "0.1.0"
+edition = "2021"
+doctest = false
+
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }

tests/script-based-pre/cargo_playback_array/sample_crate/src/lib.rs

@@ -0,0 +1,16 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Test that concrete playback generates concrete values for arrays over the length of 64
+//! and that playback can run those tests and find the index out of bounds bug,
+//! c.f. https://github.com/model-checking/kani/issues/3787
+
+#[cfg(kani)]
+mod verify {
+    #[kani::proof]
+    fn index_array_65() {
+        let arr: [u16; 65] = kani::any();
+        let idx: usize = kani::any();
+        arr[idx];
+    }
+}

tests/script-based-pre/playback_already_existing/original.rs

@@ -25,7 +25,7 @@ mod verify {
         }
     }
     #[test]
-    fn kani_concrete_playback_try_nz_u8_17663051139329126359() {
+    fn kani_concrete_playback_try_nz_u8_1592364891838466833() {
         let concrete_vals: Vec<Vec<u8>> = vec![
             // 0
             vec![0],