Enable concrete playback for contract and stubs (#3389)

This PR enables concrete playback for contract and stubs. Since these
two cases may not actually behave as users expect (it can even have an
internal failure), I am adding documentation to the generated test
calling that out.

As I was testing this issue, I realized that concrete playback didn't
quite work for arrays. So I introduced a new private function
`any_raw_array`, which doesn't change the behavior during verification,
but allow us to special case it in the concrete playback flow.

Resolves #3383 

---------

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

kani-compiler/src/kani_middle/attributes.rs

@@ -4,7 +4,7 @@
 
 use std::collections::BTreeMap;
 
-use kani_metadata::{CbmcSolver, HarnessAttributes, Stub};
+use kani_metadata::{CbmcSolver, HarnessAttributes, HarnessKind, Stub};
 use rustc_ast::{
  attr,
  token::Token,
@@ -310,7 +310,7 @@ impl<'tcx> KaniAttributes<'tcx> {
  /// the session and emit all errors found.
  pub(super) fn check_attributes(&self) {
  // Check that all attributes are correctly used and well formed.
- let is_harness = self.is_harness();
+ let is_harness = self.is_proof_harness();
  for (&kind, attrs) in self.map.iter() {
  let local_error = |msg| self.tcx.dcx().span_err(attrs[0].span, msg);
 
@@ -454,7 +454,7 @@ impl<'tcx> KaniAttributes<'tcx> {
 
  /// Is this item a harness? (either `proof` or `proof_for_contract`
  /// attribute are present)
- fn is_harness(&self) -> bool {
+ fn is_proof_harness(&self) -> bool {
  self.map.contains_key(&KaniAttributeKind::Proof)
  || self.map.contains_key(&KaniAttributeKind::ProofForContract)
  }
@@ -469,13 +469,18 @@ impl<'tcx> KaniAttributes<'tcx> {
  panic!("Expected a local item, but got: {:?}", self.item);
  };
  trace!(?self, "extract_harness_attributes");
- assert!(self.is_harness());
- self.map.iter().fold(HarnessAttributes::default(), |mut harness, (kind, attributes)| {
+ assert!(self.is_proof_harness());
+ let harness_attrs = if let Some(Ok(harness)) = self.proof_for_contract() {
+ HarnessAttributes::new(HarnessKind::ProofForContract { target_fn: harness.to_string() })
+ } else {
+ HarnessAttributes::new(HarnessKind::Proof)
+ };
+ self.map.iter().fold(harness_attrs, |mut harness, (kind, attributes)| {
  match kind {
  KaniAttributeKind::ShouldPanic => harness.should_panic = true,
  KaniAttributeKind::Recursion => {
  self.tcx.dcx().span_err(self.tcx.def_span(self.item), "The attribute `kani::recursion` should only be used in combination with function contracts.");
- },
+ }
  KaniAttributeKind::Solver => {
  harness.solver = parse_solver(self.tcx, attributes[0]);
  }
@@ -485,7 +490,7 @@ impl<'tcx> KaniAttributes<'tcx> {
  KaniAttributeKind::Unwind => {
  harness.unwind_value = parse_unwind(self.tcx, attributes[0])
  }
- KaniAttributeKind::Proof => harness.proof = true,
+ KaniAttributeKind::Proof => { /* no-op */ }
  KaniAttributeKind::ProofForContract => self.handle_proof_for_contract(&mut harness),
  KaniAttributeKind::StubVerified => self.handle_stub_verified(&mut harness),
  KaniAttributeKind::Unstable => {
@@ -498,7 +503,7 @@ impl<'tcx> KaniAttributes<'tcx> {
  | KaniAttributeKind::InnerCheck
  | KaniAttributeKind::ReplacedWith => {
  self.tcx.dcx().span_err(self.tcx.def_span(self.item), format!("Contracts are not supported on harnesses. (Found the kani-internal contract attribute `{}`)", kind.as_ref()));
- },
+ }
  KaniAttributeKind::DisableChecks => {
  // Internal attribute which shouldn't exist here.
  unreachable!()
@@ -552,14 +557,14 @@ impl<'tcx> KaniAttributes<'tcx> {
  self.item_name(),
  ),
  )
- .with_span_note(
- self.tcx.def_span(def_id),
- format!(
- "Try adding a contract to this function or use the unsound `{}` attribute instead.",
- KaniAttributeKind::Stub.as_ref(),
+ .with_span_note(
+ self.tcx.def_span(def_id),
+ format!(
+ "Try adding a contract to this function or use the unsound `{}` attribute instead.",
+ KaniAttributeKind::Stub.as_ref(),
+ ),
  )
- )
- .emit();
+ .emit();
  continue;
  }
  Some(Ok(replacement_name)) => replacement_name,
@@ -689,7 +694,7 @@ fn has_kani_attribute<F: Fn(KaniAttributeKind) -> bool>(
  tcx.get_attrs_unchecked(def_id).iter().filter_map(|a| attr_kind(tcx, a)).any(predicate)
 }
 
-/// Same as [`KaniAttributes::is_harness`] but more efficient because less
+/// Same as [`KaniAttributes::is_proof_harness`] but more efficient because less
 /// attribute parsing is performed.
 pub fn is_proof_harness(tcx: TyCtxt, instance: InstanceStable) -> bool {
  let def_id = rustc_internal::internal(tcx, instance.def.def_id());
@@ -896,7 +901,7 @@ fn parse_stubs(tcx: TyCtxt, harness: DefId, attributes: &[&Attribute]) -> Vec<St
  Err(error_span) => {
  tcx.dcx().span_err(
  error_span,
-  "attribute `kani::stub` takes two path arguments; found argument that is not a path",
+ "attribute `kani::stub` takes two path arguments; found argument that is not a path",
  );
  None
  }
@@ -910,9 +915,9 @@ fn parse_solver(tcx: TyCtxt, attr: &Attribute) -> Option<CbmcSolver> {
  const ATTRIBUTE: &str = "#[kani::solver]";
  let invalid_arg_err = |attr: &Attribute| {
  tcx.dcx().span_err(
-  attr.span,
-  format!("invalid argument for `{ATTRIBUTE}` attribute, expected one of the supported solvers (e.g. `kissat`) or a SAT solver binary (e.g. `bin=\"<SAT_SOLVER_BINARY>\"`)")
-  )
+ attr.span,
+ format!("invalid argument for `{ATTRIBUTE}` attribute, expected one of the supported solvers (e.g. `kissat`) or a SAT solver binary (e.g. `bin=\"<SAT_SOLVER_BINARY>\"`)"),
+ )
  };
 
  let attr_args = attr.meta_item_list().unwrap();

kani-compiler/src/kani_middle/codegen_units.rs

@@ -104,7 +104,7 @@ impl CodegenUnits {
  /// Generate [KaniMetadata] for the target crate.
  fn generate_metadata(&self) -> KaniMetadata {
  let (proof_harnesses, test_harnesses) =
- self.harness_info.values().cloned().partition(|md| md.attributes.proof);
+ self.harness_info.values().cloned().partition(|md| md.attributes.is_proof_harness());
  KaniMetadata {
  crate_name: self.crate_info.name.clone(),
  proof_harnesses,

kani-compiler/src/kani_middle/metadata.rs

@@ -6,7 +6,7 @@
 use std::path::Path;
 
 use crate::kani_middle::attributes::test_harness_name;
-use kani_metadata::{ArtifactType, HarnessAttributes, HarnessMetadata};
+use kani_metadata::{ArtifactType, HarnessAttributes, HarnessKind, HarnessMetadata};
 use rustc_middle::ty::TyCtxt;
 use stable_mir::mir::mono::Instance;
 use stable_mir::CrateDef;
@@ -61,7 +61,7 @@ pub fn gen_test_metadata(
  original_file: loc.filename,
  original_start_line: loc.start_line,
  original_end_line: loc.end_line,
- attributes: HarnessAttributes::default(),
+ attributes: HarnessAttributes::new(HarnessKind::Test),
  // TODO: This no longer needs to be an Option.
  goto_file: Some(model_file),
  contract: Default::default(),

kani-driver/src/args/mod.rs

@@ -559,13 +559,6 @@ impl ValidateArgs for VerificationArgs {
  --output-format=old.",
  ));
  }
- if self.concrete_playback.is_some() && self.is_stubbing_enabled() {
- // Concrete playback currently does not work with contracts or stubbing.
- return Err(Error::raw(
- ErrorKind::ArgumentConflict,
- "Conflicting options: --concrete-playback isn't compatible with stubbing.",
- ));
- }
  if self.concrete_playback.is_some() && self.jobs() != Some(1) {
  // Concrete playback currently embeds a lot of assumptions about the order in which harnesses get called.
  return Err(Error::raw(
@@ -869,13 +862,13 @@ mod tests {
  let res = parse_unstable_disabled("--harness foo -Z stubbing").unwrap();
  assert!(res.verify_opts.is_stubbing_enabled());
 
- // `-Z stubbing` cannot be called with `--concrete-playback`
+ // `-Z stubbing` can now be called with concrete playback.
  let res = parse_unstable_disabled(
  "--harness foo --concrete-playback=print -Z concrete-playback -Z stubbing",
  )
  .unwrap();
- let err = res.validate().unwrap_err();
- assert_eq!(err.kind(), ErrorKind::ArgumentConflict);
+ // Note that `res.validate()` fails because input file does not exist.
+ assert!(matches!(res.verify_opts.validate(), Ok(())));
  }
 
  #[test]

kani-driver/src/concrete_playback/test_generator.rs

@@ -6,10 +6,11 @@
 
 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};
-use kani_metadata::HarnessMetadata;
+use kani_metadata::{HarnessKind, HarnessMetadata};
 use std::collections::hash_map::DefaultHasher;
 use std::ffi::OsString;
 use std::fs::{read_to_string, File};
@@ -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)
+ 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,8 +235,52 @@ impl KaniSession {
  }
 }
 
+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 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(
+ r#"///
+/// # Warning
+///
+/// Concrete playback tests combined with stubs or contracts is highly
+/// experimental, and subject to change.
+///
+/// The original harness has stubs which are not applied to this test.
+/// This may cause a mismatch of non-deterministic values if the stub
+/// creates any non-deterministic value.
+/// The execution path may also differ, which can be used to refine the stub
+/// logic.
+"#,
+ );
+ }
+ doc_str
+}
+
 /// Generate a formatted unit test from a list of concrete values.
-fn format_unit_test(harness_name: &str, concrete_vals: &[ConcreteVal]) -> UnitTest {
+fn format_unit_test(
+ harness_name: &str,
+ concrete_vals: &[ConcreteVal],
+ doc_str: String,
+) -> UnitTest {
  // Hash the concrete values along with the proof harness name.
  let mut hasher = DefaultHasher::new();
  harness_name.hash(&mut hasher);
@@ -241,6 +289,7 @@ fn format_unit_test(harness_name: &str, concrete_vals: &[ConcreteVal]) -> UnitTe
  let func_name = format!("kani_concrete_playback_{harness_name}_{hash}");
 
  let func_before_concrete_vals = [
+ doc_str,
  "#[test]".to_string(),
  format!("fn {func_name}() {{"),
  format!("{:<4}let concrete_vals: Vec<Vec<u8>> = vec![", " "),
@@ -324,7 +373,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| {
@@ -340,7 +389,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()
  }
@@ -359,7 +408,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();
@@ -484,9 +533,10 @@ mod tests {
  /// Since hashes can not be relied on in tests, this compares all parts of a unit test except the hash.
  #[test]
  fn format_unit_test_full_func() {
+ let doc_str = "/// Test documentation";
  let harness_name = "test_proof_harness";
  let concrete_vals = [ConcreteVal { byte_arr: vec![0, 0], interp_val: "0".to_string() }];
- let unit_test = format_unit_test(harness_name, &concrete_vals);
+ let unit_test = format_unit_test(harness_name, &concrete_vals, doc_str.to_string());
  let full_func = unit_test.code;
  let split_unit_test_name = split_unit_test_name(&unit_test.name);
  let expected_after_func_name = vec![
@@ -498,18 +548,23 @@ mod tests {
  "}".to_string(),
  ];
 
- assert_eq!(full_func[0], "#[test]");
+ assert_eq!(full_func[0], doc_str);
+ assert_eq!(full_func[1], "#[test]");
  assert_eq!(
  split_unit_test_name.before_hash,
  format!("kani_concrete_playback_{harness_name}")
  );
- assert_eq!(full_func[1], format!("fn {}() {{", unit_test.name));
- assert_eq!(full_func[2..], expected_after_func_name);
+ assert_eq!(full_func[2], format!("fn {}() {{", unit_test.name));
+ assert_eq!(full_func[3..], expected_after_func_name);
  }
 
  /// Generates a unit test and returns its hash.
  fn extract_hash_from_unit_test(harness_name: &str, concrete_vals: &[ConcreteVal]) -> String {
- let unit_test = format_unit_test(harness_name, concrete_vals);
+ let unit_test = format_unit_test(
+ harness_name,
+ concrete_vals,
+ "/// Harness created for unit test".to_string(),
+ );
  split_unit_test_name(&unit_test.name).hash
  }
 
@@ -603,7 +658,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]);