Fix concrete playback for array and add test

kani-driver/src/concrete_playback/test_generator.rs

@@ -6,6 +6,7 @@
 
 use crate::args::ConcretePlaybackMode;
 use crate::call_cbmc::VerificationResult;
+use crate::cbmc_output_parser::Property;
 use crate::session::KaniSession;
 use anyhow::{Context, Result};
 use concrete_vals_extractor::{extract_harness_values, ConcreteVal};
@@ -32,7 +33,7 @@ impl KaniSession {
  };
 
  if let Ok(result_items) = &verification_result.results {
- let harness_values: Vec<Vec<ConcreteVal>> = extract_harness_values(result_items);
+ let harness_values = extract_harness_values(result_items);
 
  if harness_values.is_empty() {
  println!(
@@ -43,9 +44,9 @@ impl KaniSession {
  } else {
  let mut unit_tests: Vec<UnitTest> = harness_values
  .iter()
- .map(|concrete_vals| {
+ .map(|(prop, concrete_vals)| {
  let pretty_name = harness.get_harness_name_unqualified();
- format_unit_test(&pretty_name, &concrete_vals, gen_test_doc(harness))
+ format_unit_test(&pretty_name, &concrete_vals, gen_test_doc(harness, *prop))
  })
  .collect();
  unit_tests.dedup_by(|a, b| a.name == b.name);
@@ -168,6 +169,9 @@ impl KaniSession {
  writeln!(temp_file, "{line}")?;
  if curr_line_num == proof_harness_end_line {
  for unit_test in unit_tests.iter() {
+ // Write an empty line before the unit test.
+ writeln!(temp_file, "")?;
+
  for unit_test_line in unit_test.code.iter() {
  curr_line_num += 1;
  writeln!(temp_file, "{unit_test_line}")?;
@@ -176,7 +180,7 @@ impl KaniSession {
  }
  }
 
- // Renames are usually automic, so we won't corrupt the user's source file during a
+ // Renames are usually atomic, so we won't corrupt the user's source file during a
  // crash; but first flush all updates to disk, which persist wouldn't take care of.
  temp_file.as_file().sync_all()?;
  temp_file.persist(source_path).expect("Could not rename file");
@@ -231,28 +235,34 @@ impl KaniSession {
  }
 }
 
-fn gen_test_doc(harness: &HarnessMetadata) -> String {
+fn gen_test_doc(harness: &HarnessMetadata, property: &Property) -> String {
  let mut doc_str = match &harness.attributes.kind {
  HarnessKind::Proof => {
  format!("/// Test generated for harness `{}` \n", harness.pretty_name)
  }
  HarnessKind::ProofForContract { target_fn } => {
  format!(
- "/// Test generated for harness `{}` that check contract for `{target_fn}`\n",
+ "/// Test generated for harness `{}` that checks contract for `{target_fn}`\n",
  harness.pretty_name
  )
  }
  HarnessKind::Test => {
  unreachable!("Concrete playback for tests is not supported")
  }
  };
+ doc_str.push_str("///\n");
+ doc_str.push_str(&format!(
+ "/// Check for `{}`: \"{}\"\n",
+ property.property_class(),
+ property.description
+ ));
  if !harness.attributes.stubs.is_empty() {
  doc_str.push_str("///\n");
  doc_str.push_str(
  "/// # Warning\n\
  ///\n\
- /// Concrete playback tests combined with stubs is highly experimental, and\n\
- /// subject to change.\n\
+ /// Concrete playback tests combined with stubs or contracts is highly \n\
+ /// experimental, and subject to change.\n\
  ///\n\
  /// The original harness has stubs which are not applied to this test.\n\
  /// This may cause a mismatch of non-deterministic values if the stub\n\
@@ -362,7 +372,7 @@ mod concrete_vals_extractor {
  /// Extract a set of concrete values that trigger one assertion
  /// failure. Each element of the outer vector corresponds to
  /// inputs triggering one assertion failure or cover statement.
- pub fn extract_harness_values(result_items: &[Property]) -> Vec<Vec<ConcreteVal>> {
+ pub fn extract_harness_values(result_items: &[Property]) -> Vec<(&Property, Vec<ConcreteVal>)> {
  result_items
  .iter()
  .filter(|prop| {
@@ -378,7 +388,7 @@ mod concrete_vals_extractor {
  let concrete_vals: Vec<ConcreteVal> =
  trace.iter().filter_map(&extract_from_trace_item).collect();
 
- concrete_vals
+ (property, concrete_vals)
  })
  .collect()
  }
@@ -397,7 +407,7 @@ mod concrete_vals_extractor {
  {
  if trace_item.step_type == "assignment"
  && lhs.starts_with("goto_symex$$return_value")
- && func.starts_with("kani::any_raw_internal")
+ && func.starts_with("kani::any_raw_")
  {
  let declared_width = width_u64 as usize;
  let actual_width = bit_concrete_val.len();
@@ -647,7 +657,7 @@ mod tests {
  }),
  }]),
  }];
- let concrete_vals = extract_harness_values(&processed_items).pop().unwrap();
+ let (_, concrete_vals) = extract_harness_values(&processed_items).pop().unwrap();
  let concrete_val = &concrete_vals[0];
 
  assert_eq!(concrete_val.byte_arr, vec![1, 3]);

library/kani/src/arbitrary.rs

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

library/kani/src/lib.rs

@@ -250,20 +250,31 @@ pub fn any_where<T: Arbitrary, F: FnOnce(&T) -> bool>(f: F) -> T {
 #[inline(never)]
 #[cfg(not(feature = "concrete_playback"))]
 pub(crate) unsafe fn any_raw_internal<T: Copy>() -> T {
- any_raw_inner::<T>()
+ any_raw::<T>()
 }
 
+/// This is the same as [any_raw_internal] for verification flow, but not for concrete playback.
 #[inline(never)]
+#[cfg(not(feature = "concrete_playback"))]
+pub(crate) unsafe fn any_raw_array<T: Copy, const N: usize>() -> [T; N] {
+ any_raw::<[T; N]>()
+}
+
 #[cfg(feature = "concrete_playback")]
-pub(crate) unsafe fn any_raw_internal<T: Copy>() -> T {
- concrete_playback::any_raw_internal::<T>()
+use concrete_playback::any_raw_internal;
+
+/// Iterate over `any_raw_internal` since CBMC produces assignment per element.
+#[inline(never)]
+#[cfg(feature = "concrete_playback")]
+pub(crate) unsafe fn any_raw_array<T: Copy, const N: usize>() -> [T; N] {
+ [(); N].map(|_| any_raw_internal::<T>())
 }
 
 /// This low-level function returns nondet bytes of size T.
 #[rustc_diagnostic_item = "KaniAnyRaw"]
 #[inline(never)]
 #[allow(dead_code)]
-fn any_raw_inner<T: Copy>() -> T {
+fn any_raw<T: Copy>() -> T {
  kani_intrinsic()
 }
 

library/kani_macros/src/sysroot/contracts/mod.rs

@@ -336,7 +336,7 @@
 use proc_macro::TokenStream;
 use proc_macro2::{Ident, TokenStream as TokenStream2};
 use quote::{quote, ToTokens};
-use syn::{parse_macro_input, Expr, ExprClosure, ItemFn};
+use syn::{parse_macro_input, parse_quote, Expr, ExprClosure, ItemFn};
 
 mod bootstrap;
 mod check;
@@ -387,15 +387,12 @@ passthrough!(stub_verified, false);
 
 pub fn proof_for_contract(attr: TokenStream, item: TokenStream) -> TokenStream {
  let args = proc_macro2::TokenStream::from(attr);
- let ItemFn { attrs, vis, sig, block } = parse_macro_input!(item as ItemFn);
+ let mut fn_item = parse_macro_input!(item as ItemFn);
+ fn_item.block.stmts.insert(0, parse_quote!(kani::internal::init_contracts();));
  quote!(
  #[allow(dead_code)]
  #[kanitool::proof_for_contract = stringify!(#args)]
- #(#attrs)*
- #vis #sig {
- kani::internal::init_contracts();
- #block
- }
+ #fn_item
  )
  .into()
 }

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

@@ -0,0 +1,19 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Check that Kani correctly adds tests to when the harness is a proof for contract.
+extern crate kani;
+
+#[kani::requires(idx < slice.len())]
+#[kani::modifies(slice)]
+#[kani::ensures(| _ | slice[idx] == new_val)]
+fn modify_slice(slice: &mut [u32], idx: usize, new_val: u32) {
+ // Inject bug by incrementing index first.
+ let new_idx = idx + 1;
+ *slice.get_mut(new_idx).expect("Expected valid index, but contract is wrong") = new_val;
+}
+
+#[kani::proof_for_contract(modify_slice)]
+fn check_modify_slice() {
+ let mut data: [u32; 4] = kani::any();
+ modify_slice(&mut data, kani::any(), kani::any())
+}

tests/script-based-pre/playback_contracts/playback_with_contracts.expected

@@ -0,0 +1,15 @@
+[TEST] Generate test...
+Checking harness check_modify_slice...
+
+Failed Checks: | _ | slice[idx] == new_val
+Failed Checks:\
+in std::option::expect_failed
+
+VERIFICATION:- FAILED
+
+[TEST] Run test...
+
+running 2 tests
+
+Expected valid index, but contract is wrong
+test result: FAILED. 1 passed; 1 failed;

tests/script-based-pre/playback_contracts/playback_with_contracts.sh

@@ -0,0 +1,20 @@
+#!/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 nounset
+
+RS_FILE="modified.rs"
+cp original.rs ${RS_FILE}
+
+echo "[TEST] Generate test..."
+kani ${RS_FILE} -Z concrete-playback --concrete-playback=inplace -Z function-contracts --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..."
+kani playback -Z concrete-playback ${RS_FILE} -- kani_concrete_playback
+
+# Cleanup
+rm ${RS_FILE}
+rm kani_concrete_playback