Support concrete playback for arrays of length 65 or greater (#3888)

### Problem
When CBMC generates a JSON trace for a nondeterministic array, it will
output a key-value pair `elements: [array]`, where `array` contains
concrete values for each element in the array. If the array is length 64
or shorter, it will _also_ output the elements of the array as separate
values in the trace (so each element is in the trace twice). Prior to
this PR, concrete playback relied on the latter output format to find
elements of an array. However, when the array was length 65 or greater,
those elements wouldn't be values in their own right, so we wouldn't
find any values for the array and just output an empty array.

### Solution
This PR changes our representation of concrete values to handle arrays
explicitly; i.e., to look for the `elements` array and populate the
concrete values of the array from that instead.

### Callouts
For those wondering why the `playback_already_existed` test changed,
it's because we're hashing `ConcreteItem` instead of `ConcreteValue`, so
the hash changes.

Resolves #3787

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: carolynzech

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.

kani-driver/src/concrete_playback/test_generator.rs

@@ -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/config.yml

@@ -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.expected

@@ -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/playback_target.sh

@@ -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/Cargo.toml

@@ -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/cargo_playback_array/sample_crate/src/lib.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],