Escape Zero-size types in playback

library/kani/src/concrete_playback.rs

@@ -40,7 +40,9 @@ pub fn concrete_playback_run<F: Fn()>(mut local_concrete_vals: Vec<Vec<u8>>, pro
     });
 }
 
-/// Concrete playback implementation of kani::any_raw_internal.
+/// Concrete playback implementation of
+/// kani::any_raw_internal. Because CBMC does not bother putting in
+/// Zero-Sized Types, those are defaulted to an empty vector.
 ///
 /// # Safety
 ///
@@ -49,7 +51,11 @@ pub(crate) unsafe fn any_raw_internal<T, const SIZE_T: usize>() -> T {
     let mut next_concrete_val: Vec<u8> = Vec::new();
     CONCRETE_VALS.with(|glob_concrete_vals| {
         let mut_ref_glob_concrete_vals = &mut *glob_concrete_vals.borrow_mut();
-        next_concrete_val = mut_ref_glob_concrete_vals.pop().expect("Not enough det vals found");
+        next_concrete_val = if SIZE_T > 0 {
+            mut_ref_glob_concrete_vals.pop().expect("Not enough det vals found")
+        } else {
+            vec![]
+        };
     });
     let next_concrete_val_len = next_concrete_val.len();
     let bytes_t: [u8; SIZE_T] = next_concrete_val.try_into().expect(&format!(

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

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

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

@@ -0,0 +1,9 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! This checks that Kani zero-size playback, 2 of them in a row.
+
+#[kani::proof]
+fn any_is_ok() {
+    let unit: () = kani::any();
+    kani::cover!(unit == ());
+}

tests/script-based-pre/playback_zero_size/playback_zst.expected

@@ -0,0 +1,5 @@
+[TEST] Generate test...
+Checking harness any_is_ok
+
+[TEST] Run test...
+test result: ok. 1 passed; 0 failed;

tests/script-based-pre/playback_zero_size/playback_zst.sh

@@ -0,0 +1,18 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+# Test that concrete playback -Z concrete-playback executes as expected
+set -o pipefail
+set -o nounset
+
+RS_FILE="modified.rs"
+cp original.rs ${RS_FILE}
+
+echo "[TEST] Generate test..."
+kani ${RS_FILE} -Z concrete-playback --concrete-playback=inplace
+
+echo "[TEST] Run test..."
+kani playback -Z concrete-playback ${RS_FILE} -- kani_concrete_playback
+
+# Cleanup
+rm ${RS_FILE}