From 3bc4f0c76f8a64e62241daf61e81de18b66f0cd2 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Wed, 31 Jul 2024 11:50:08 -0700
Subject: [PATCH 1/2] 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   | 45 +++++-----
 .../src/kani_middle/codegen_units.rs          |  2 +-
 kani-compiler/src/kani_middle/metadata.rs     |  4 +-
 kani-driver/src/args/mod.rs                   | 13 +--
 .../src/concrete_playback/test_generator.rs   | 85 +++++++++++++++----
 kani-driver/src/metadata.rs                   | 16 ++--
 kani_metadata/src/harness.rs                  | 32 ++++++-
 library/kani/src/arbitrary.rs                 |  2 +-
 library/kani/src/concrete_playback.rs         |  5 ++
 library/kani/src/lib.rs                       | 16 ++--
 library/kani_core/src/arbitrary.rs            |  2 +-
 library/kani_core/src/lib.rs                  | 16 ++--
 .../kani_macros/src/sysroot/contracts/mod.rs  | 11 +--
 .../playback_expected/config.yml              |  4 +
 .../playback_expected/expected                |  8 ++
 .../playback_expected/playback.sh             | 42 +++++++++
 .../src/playback_contract.rs                  | 19 +++++
 .../playback_expected/src/playback_stubs.rs   | 34 ++++++++
 .../verify_std_cmd/verify_std.sh              |  2 +-
 19 files changed, 279 insertions(+), 79 deletions(-)
 create mode 100644 tests/script-based-pre/playback_expected/config.yml
 create mode 100644 tests/script-based-pre/playback_expected/expected
 create mode 100755 tests/script-based-pre/playback_expected/playback.sh
 create mode 100644 tests/script-based-pre/playback_expected/src/playback_contract.rs
 create mode 100644 tests/script-based-pre/playback_expected/src/playback_stubs.rs

diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs
index 9eb6d3d6ee4e..8c729bbdec9f 100644
--- a/kani-compiler/src/kani_middle/attributes.rs
+++ b/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();
diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs
index 260b363a868a..b4ea06c8d5db 100644
--- a/kani-compiler/src/kani_middle/codegen_units.rs
+++ b/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,
diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs
index c00f38be4cb0..2f0f22d49e1c 100644
--- a/kani-compiler/src/kani_middle/metadata.rs
+++ b/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(),
diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs
index 158f1c001b5b..2d7593e8050a 100644
--- a/kani-driver/src/args/mod.rs
+++ b/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]
diff --git a/kani-driver/src/concrete_playback/test_generator.rs b/kani-driver/src/concrete_playback/test_generator.rs
index dbd2fb9e03d2..5faa6299a5d3 100644
--- a/kani-driver/src/concrete_playback/test_generator.rs
+++ b/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]);
diff --git a/kani-driver/src/metadata.rs b/kani-driver/src/metadata.rs
index cd916358d92e..3f9cd8f2bf84 100644
--- a/kani-driver/src/metadata.rs
+++ b/kani-driver/src/metadata.rs
@@ -200,7 +200,7 @@ fn find_proof_harnesses<'a>(
 #[cfg(test)]
 pub mod tests {
     use super::*;
-    use kani_metadata::HarnessAttributes;
+    use kani_metadata::{HarnessAttributes, HarnessKind};
     use std::path::PathBuf;
 
     pub fn mock_proof_harness(
@@ -209,6 +209,8 @@ pub mod tests {
         krate: Option<&str>,
         model_file: Option<PathBuf>,
     ) -> HarnessMetadata {
+        let mut attributes = HarnessAttributes::new(HarnessKind::Proof);
+        attributes.unwind_value = unwind_value;
         HarnessMetadata {
             pretty_name: name.into(),
             mangled_name: name.into(),
@@ -216,7 +218,7 @@ pub mod tests {
             original_file: "<unknown>".into(),
             original_start_line: 0,
             original_end_line: 0,
-            attributes: HarnessAttributes { unwind_value, proof: true, ..Default::default() },
+            attributes,
             goto_file: model_file,
             contract: Default::default(),
         }
@@ -236,7 +238,7 @@ pub mod tests {
             find_proof_harnesses(
                 &BTreeSet::from([&"check_three".to_string()]),
                 &ref_harnesses,
-                false
+                false,
             )
             .len(),
             1
@@ -245,7 +247,7 @@ pub mod tests {
             find_proof_harnesses(
                 &BTreeSet::from([&"check_two".to_string()]),
                 &ref_harnesses,
-                false
+                false,
             )
             .first()
             .unwrap()
@@ -256,7 +258,7 @@ pub mod tests {
             find_proof_harnesses(
                 &BTreeSet::from([&"check_one".to_string()]),
                 &ref_harnesses,
-                false
+                false,
             )
             .first()
             .unwrap()
@@ -280,7 +282,7 @@ pub mod tests {
             find_proof_harnesses(
                 &BTreeSet::from([&"check_three".to_string()]),
                 &ref_harnesses,
-                true
+                true,
             )
             .is_empty()
         );
@@ -299,7 +301,7 @@ pub mod tests {
             find_proof_harnesses(
                 &BTreeSet::from([&"module::not_check_three".to_string()]),
                 &ref_harnesses,
-                true
+                true,
             )
             .first()
             .unwrap()
diff --git a/kani_metadata/src/harness.rs b/kani_metadata/src/harness.rs
index 3dd6c82ebd39..41eb4eb20919 100644
--- a/kani_metadata/src/harness.rs
+++ b/kani_metadata/src/harness.rs
@@ -38,10 +38,10 @@ pub struct HarnessMetadata {
 }
 
 /// The attributes added by the user to control how a harness is executed.
-#[derive(Debug, Clone, Serialize, Deserialize, Default, PartialEq)]
+#[derive(Debug, Clone, Serialize, Deserialize, PartialEq)]
 pub struct HarnessAttributes {
     /// Whether the harness has been annotated with proof.
-    pub proof: bool,
+    pub kind: HarnessKind,
     /// Whether the harness is expected to panic or not.
     pub should_panic: bool,
     /// Optional data to store solver.
@@ -52,6 +52,34 @@ pub struct HarnessAttributes {
     pub stubs: Vec<Stub>,
 }
 
+#[derive(Clone, Eq, PartialEq, Debug, Serialize, Deserialize)]
+pub enum HarnessKind {
+    /// Function was annotated with `#[kani::proof]`.
+    Proof,
+    /// Function was annotated with `#[kani::proof_for_contract(target_fn)]`.
+    ProofForContract { target_fn: String },
+    /// This is a test harness annotated with `#[test]`.
+    Test,
+}
+
+impl HarnessAttributes {
+    /// Create a new harness of the provided kind.
+    pub fn new(kind: HarnessKind) -> HarnessAttributes {
+        HarnessAttributes {
+            kind,
+            should_panic: false,
+            solver: None,
+            unwind_value: None,
+            stubs: vec![],
+        }
+    }
+
+    /// Return whether this is a proof harness.
+    pub fn is_proof_harness(&self) -> bool {
+        matches!(self.kind, HarnessKind::Proof | HarnessKind::ProofForContract { .. })
+    }
+}
+
 /// The stubbing type.
 #[derive(Debug, Clone, Serialize, Deserialize, PartialEq)]
 pub struct Stub {
diff --git a/library/kani/src/arbitrary.rs b/library/kani/src/arbitrary.rs
index ef6e2ef23dd4..83b113d64927 100644
--- a/library/kani/src/arbitrary.rs
+++ b/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>() }
             }
         }
     };
diff --git a/library/kani/src/concrete_playback.rs b/library/kani/src/concrete_playback.rs
index aa6cd7e4018d..0de51862b7d8 100644
--- a/library/kani/src/concrete_playback.rs
+++ b/library/kani/src/concrete_playback.rs
@@ -40,6 +40,11 @@ pub fn concrete_playback_run<F: Fn()>(mut local_concrete_vals: Vec<Vec<u8>>, pro
     });
 }
 
+/// Iterate over `any_raw_internal` since CBMC produces assignment per element.
+pub(crate) unsafe fn any_raw_array<T: Copy, const N: usize>() -> [T; N] {
+    [(); N].map(|_| crate::any_raw_internal::<T>())
+}
+
 /// 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.
diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs
index 3cf46bd7af07..046c6e7a0667 100644
--- a/library/kani/src/lib.rs
+++ b/library/kani/src/lib.rs
@@ -249,21 +249,25 @@ pub fn any_where<T: Arbitrary, F: FnOnce(&T) -> bool>(f: F) -> T {
 /// Note that SIZE_T must be equal the size of type T in bytes.
 #[inline(never)]
 #[cfg(not(feature = "concrete_playback"))]
-pub(crate) unsafe fn any_raw_internal<T: Copy>() -> T {
-    any_raw_inner::<T>()
+unsafe fn any_raw_internal<T: Copy>() -> T {
+    any_raw::<T>()
 }
 
+/// This is the same as [any_raw_internal] for verification flow, but not for concrete playback.
 #[inline(never)]
-#[cfg(feature = "concrete_playback")]
-pub(crate) unsafe fn any_raw_internal<T: Copy>() -> T {
-    concrete_playback::any_raw_internal::<T>()
+#[cfg(not(feature = "concrete_playback"))]
+unsafe fn any_raw_array<T: Copy, const N: usize>() -> [T; N] {
+    any_raw::<[T; N]>()
 }
 
+#[cfg(feature = "concrete_playback")]
+use concrete_playback::{any_raw_array, any_raw_internal};
+
 /// 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()
 }
 
diff --git a/library/kani_core/src/arbitrary.rs b/library/kani_core/src/arbitrary.rs
index 7cfb649b11a0..8c6cfd335104 100644
--- a/library/kani_core/src/arbitrary.rs
+++ b/library/kani_core/src/arbitrary.rs
@@ -34,7 +34,7 @@ macro_rules! generate_arbitrary {
                         unsafe { crate::kani::any_raw_internal::<Self>() }
                     }
                     fn any_array<const MAX_ARRAY_LENGTH: usize>() -> [Self; MAX_ARRAY_LENGTH] {
-                        unsafe { crate::kani::any_raw_internal::<[Self; MAX_ARRAY_LENGTH]>() }
+                        unsafe { crate::kani::any_raw_array::<Self, MAX_ARRAY_LENGTH>() }
                     }
                 }
             };
diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs
index 016c805e8f8e..9baba1abe886 100644
--- a/library/kani_core/src/lib.rs
+++ b/library/kani_core/src/lib.rs
@@ -248,21 +248,25 @@ macro_rules! kani_intrinsics {
         /// Note that SIZE_T must be equal the size of type T in bytes.
         #[inline(never)]
         #[cfg(not(feature = "concrete_playback"))]
-        pub(crate) unsafe fn any_raw_internal<T: Copy>() -> T {
-            any_raw_inner::<T>()
+        unsafe fn any_raw_internal<T: Copy>() -> T {
+            any_raw::<T>()
         }
 
+        /// This is the same as [any_raw_internal] for verification flow, but not for concrete playback.
         #[inline(never)]
-        #[cfg(feature = "concrete_playback")]
-        pub(crate) unsafe fn any_raw_internal<T: Copy>() -> T {
-            concrete_playback::any_raw_internal::<T>()
+        #[cfg(not(feature = "concrete_playback"))]
+        unsafe fn any_raw_array<T: Copy, const N: usize>() -> [T; N] {
+            any_raw::<[T; N]>()
         }
 
+        #[cfg(feature = "concrete_playback")]
+        use concrete_playback::{any_raw_array, any_raw_internal};
+
         /// This low-level function returns nondet bytes of size T.
         #[rustc_diagnostic_item = "KaniAnyRaw"]
         #[inline(never)]
         #[allow(dead_code)]
-        pub fn any_raw_inner<T: Copy>() -> T {
+        fn any_raw<T: Copy>() -> T {
             kani_intrinsic()
         }
 
diff --git a/library/kani_macros/src/sysroot/contracts/mod.rs b/library/kani_macros/src/sysroot/contracts/mod.rs
index defcd9dae1b4..12a1215de2c7 100644
--- a/library/kani_macros/src/sysroot/contracts/mod.rs
+++ b/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()
 }
diff --git a/tests/script-based-pre/playback_expected/config.yml b/tests/script-based-pre/playback_expected/config.yml
new file mode 100644
index 000000000000..d15b5d277ed6
--- /dev/null
+++ b/tests/script-based-pre/playback_expected/config.yml
@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: playback.sh
+expected: expected
diff --git a/tests/script-based-pre/playback_expected/expected b/tests/script-based-pre/playback_expected/expected
new file mode 100644
index 000000000000..bedb39581b7f
--- /dev/null
+++ b/tests/script-based-pre/playback_expected/expected
@@ -0,0 +1,8 @@
+[TEST] Generate test for playback_contract.rs...
+Verification failed for - check_modify_slice
+Result for playback_contract.rs: test result: FAILED. 1 passed; 1 failed
+
+[TEST] Generate test for playback_stubs.rs...
+Verification failed for - check_lt_0
+Verification failed for - check_bad_stub
+Result for playback_stubs.rs: test result: FAILED. 1 passed; 1 failed
diff --git a/tests/script-based-pre/playback_expected/playback.sh b/tests/script-based-pre/playback_expected/playback.sh
new file mode 100755
index 000000000000..3b358db257a2
--- /dev/null
+++ b/tests/script-based-pre/playback_expected/playback.sh
@@ -0,0 +1,42 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+# This will run Kani verification in every `src/*.rs` file followed by playback command.
+# Expected output is generated from individual expected files.
+set -o nounset
+
+run() {
+  local input_rs=${1:?"Missing input file"}
+
+  echo "[TEST] Generate test for ${input_rs}..."
+  kani "${input_rs}" \
+    -Z concrete-playback --concrete-playback=inplace \
+    -Z function-contracts -Z stubbing --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 for ${input_rs}..."
+  summary=$(kani playback -Z concrete-playback "${input_rs}" -- kani_concrete_playback | grep "test result")
+  echo "Result for ${input_rs}: ${summary}"
+}
+
+ROOT_DIR=$(git rev-parse --show-toplevel)
+MODIFIED_DIR=modified
+rm -rf "${MODIFIED_DIR}"
+mkdir "${MODIFIED_DIR}"
+
+for rs in src/*.rs; do
+  if [[ -e "${rs}" ]]; then
+    echo "Running ${rs}"
+    cp "${rs}" "${MODIFIED_DIR}"
+    pushd "${MODIFIED_DIR}" > /dev/null
+    run "$(basename "${rs}")"
+    popd > /dev/null
+  else
+    echo "No .rs files found in src directory"
+    exit 1
+  fi
+done
+
+  # Cleanup
+rm -rf "${MODIFIED_DIR}"
\ No newline at end of file
diff --git a/tests/script-based-pre/playback_expected/src/playback_contract.rs b/tests/script-based-pre/playback_expected/src/playback_contract.rs
new file mode 100644
index 000000000000..8271e9a3d03f
--- /dev/null
+++ b/tests/script-based-pre/playback_expected/src/playback_contract.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())
+}
diff --git a/tests/script-based-pre/playback_expected/src/playback_stubs.rs b/tests/script-based-pre/playback_expected/src/playback_stubs.rs
new file mode 100644
index 000000000000..ce5107949f04
--- /dev/null
+++ b/tests/script-based-pre/playback_expected/src/playback_stubs.rs
@@ -0,0 +1,34 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Check that Kani playback works with stubs.
+#![allow(dead_code)]
+
+fn is_zero(val: u8) -> bool {
+    val == 0
+}
+
+fn not_zero(val: u8) -> bool {
+    val != 0
+}
+
+/// Add a harness that will fail due to incorrect stub but the test will succeed.
+#[kani::proof]
+#[kani::stub(is_zero, not_zero)]
+fn check_bad_stub() {
+    assert!(is_zero(kani::any()))
+}
+
+fn lt_zero(val: i8) -> bool {
+    val < 0
+}
+
+fn lt_ten(val: i8) -> bool {
+    val < 10
+}
+
+/// Add a harness that will fail in an equivalent way.
+#[kani::proof]
+#[kani::stub(lt_zero, lt_ten)]
+fn check_lt_0() {
+    assert!(lt_zero(kani::any()))
+}
diff --git a/tests/script-based-pre/verify_std_cmd/verify_std.sh b/tests/script-based-pre/verify_std_cmd/verify_std.sh
index 91454c4b65e7..3a24bf15241e 100755
--- a/tests/script-based-pre/verify_std_cmd/verify_std.sh
+++ b/tests/script-based-pre/verify_std_cmd/verify_std.sh
@@ -29,7 +29,7 @@ mod verify {
     use core::kani;
     #[kani::proof]
     fn check_non_zero() {
-        let orig: u32 = kani::any_raw_inner();
+        let orig: u32 = kani::any();
         if let Some(val) = core::num::NonZeroU32::new(orig) {
             assert!(orig == val.into());
         } else {

From 695e6f76832bafd379a9fea2e6434032cebb6166 Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Wed, 31 Jul 2024 16:15:45 -0400
Subject: [PATCH 2/2] Tutorial Sections 2.1 and 2.2 Updates (#3387)

Update the tutorial, namely:

- Update the [bounds checking and pointers
example](https://model-checking.github.io/kani/tutorial-kinds-of-failure.html#bounds-checking-and-pointers).
`cargo test` catches the UB in the current example, so this PR modifies
the code slightly so that `cargo test` still misses the UB, as desired.
- Rather than including larger sections on experimental features
throughout the tutorial, create a separate experimental features section
and include (briefer) references to them in the tutorial.
- The old text recommended debugging by generating a trace with
`--visualize`, with a briefer mention of `--concrete-playback`. Since
`--visualize` is deprecated, revise the debugging exercises to recommend
`--concrete-playback` instead.

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

---------

Co-authored-by: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com>
---
 docs/src/SUMMARY.md                           |  7 +-
 docs/src/reference/attributes.md              |  2 +-
 .../experimental/concrete-playback.md}        | 19 ++---
 docs/src/reference/experimental/coverage.md   | 32 ++++++++
 .../experimental/experimental-features.md     |  5 ++
 .../reference/{ => experimental}/stubbing.md  |  2 +-
 docs/src/tutorial-first-steps.md              | 60 ++-------------
 docs/src/tutorial-kinds-of-failure.md         | 74 ++++++-------------
 docs/src/tutorial-real-code.md                |  2 +-
 .../kinds-of-failure/src/bounds_check.rs      |  2 +-
 docs/src/usage.md                             |  2 +-
 docs/src/verification-results.md              |  2 +-
 12 files changed, 81 insertions(+), 128 deletions(-)
 rename docs/src/{debugging-verification-failures.md => reference/experimental/concrete-playback.md} (87%)
 create mode 100644 docs/src/reference/experimental/coverage.md
 create mode 100644 docs/src/reference/experimental/experimental-features.md
 rename docs/src/reference/{ => experimental}/stubbing.md (99%)

diff --git a/docs/src/SUMMARY.md b/docs/src/SUMMARY.md
index ff7914c1a07a..784ec075d183 100644
--- a/docs/src/SUMMARY.md
+++ b/docs/src/SUMMARY.md
@@ -12,12 +12,13 @@
   - [Failures that Kani can spot](./tutorial-kinds-of-failure.md)
   - [Loop unwinding](./tutorial-loop-unwinding.md)
   - [Nondeterministic variables](./tutorial-nondeterministic-variables.md)
-  - [Debugging verification failures](./debugging-verification-failures.md)
 
 - [Reference](./reference.md)
   - [Attributes](./reference/attributes.md)
-  - [Stubbing](./reference/stubbing.md)
-
+  - [Experimental features](./reference/experimental/experimental-features.md)
+    - [Coverage](./reference/experimental/coverage.md)
+    - [Stubbing](./reference/experimental/stubbing.md)
+    - [Concrete Playback](./reference/experimental/concrete-playback.md)
 - [Application](./application.md)
   - [Comparison with other tools](./tool-comparison.md)
   - [Where to start on real code](./tutorial-real-code.md)
diff --git a/docs/src/reference/attributes.md b/docs/src/reference/attributes.md
index bd8b80cbbdaa..4556077911fc 100644
--- a/docs/src/reference/attributes.md
+++ b/docs/src/reference/attributes.md
@@ -60,7 +60,7 @@ For example, the class in `Check 1: my_harness.assertion.1` is `assertion`, so t
 
 > **NOTE**: The `#[kani::should_panic]` is only recommended for writing
 > harnesses which complement existing harnesses that don't use the same
-> attribute. In order words, it's only recommended to write *negative harnesses*
+> attribute. In other words, it's only recommended to write *negative harnesses*
 > after having written *positive* harnesses that successfully verify interesting
 > properties about the function under verification.
 
diff --git a/docs/src/debugging-verification-failures.md b/docs/src/reference/experimental/concrete-playback.md
similarity index 87%
rename from docs/src/debugging-verification-failures.md
rename to docs/src/reference/experimental/concrete-playback.md
index c5dae6e74308..237f5673caf0 100644
--- a/docs/src/debugging-verification-failures.md
+++ b/docs/src/reference/experimental/concrete-playback.md
@@ -1,20 +1,13 @@
-# Debugging verification failures
+# Concrete Playback
 
-When the result of a certain check comes back as a `FAILURE`,
-Kani offers different options to help debug:
-* `--concrete-playback`. This _experimental_ feature generates a Rust unit test case that plays back a failing
-proof harness using a concrete counterexample.
-* `--visualize`. This feature generates an HTML text-based trace that
-enumerates the execution steps leading to the check failure.
-
-## Concrete playback
+When the result of a certain check comes back as a `FAILURE`, Kani offers the `concrete-playback` option to help debug. This feature generates a Rust unit test case that plays back a failing proof harness using a concrete counterexample.
 
 When concrete playback is enabled, Kani will generate unit tests for assertions that failed during verification,
 as well as cover statements that are reachable.
 
 These tests can then be executed using Kani's playback subcommand.
 
-### Usage
+## Usage
 
 In order to enable this feature, run Kani with the `-Z concrete-playback --concrete-playback=[print|inplace]` flag.
 After getting a verification failure, Kani will generate a Rust unit test case that plays back a failing
@@ -46,7 +39,7 @@ The output will have a line in the beginning like
 
 You can further debug the binary with tools like `rust-gdb` or `lldb`.
 
-### Example
+## Example
 
 Running `kani -Z concrete-playback --concrete-playback=print` on the following source file:
 ```rust
@@ -75,7 +68,7 @@ Here, `133` and `35207` are the concrete values that, when substituted for `a` a
 cause an assertion failure.
 `vec![135, 137]` is the byte array representation of `35207`.
 
-### Request for comments
+## Request for comments
 
 This feature is experimental and is therefore subject to change.
 If you have ideas for improving the user experience of this feature,
@@ -83,7 +76,7 @@ please add them to [this GitHub issue](https://github.com/model-checking/kani/is
 We are tracking the existing feature requests in
 [this GitHub milestone](https://github.com/model-checking/kani/milestone/10).
 
-### Limitations 
+## Limitations 
 
 * This feature does not generate unit tests for failing non-panic checks (e.g., UB checks).
 This is because checks would not trigger runtime errors during concrete playback.
diff --git a/docs/src/reference/experimental/coverage.md b/docs/src/reference/experimental/coverage.md
new file mode 100644
index 000000000000..fb73d5f7c05b
--- /dev/null
+++ b/docs/src/reference/experimental/coverage.md
@@ -0,0 +1,32 @@
+## Coverage
+
+Recall our `estimate_size` example from [First steps](../../tutorial-first-steps.md),
+where we wrote a proof harness constraining the range of inputs to integers less than 4096:
+
+```rust
+{{#include ../../tutorial/first-steps-v2/src/lib.rs:kani}}
+```
+
+We must wonder if we've really fully tested our function.
+What if we revise the function, but forget to update the assumption in our proof harness to cover the new range of inputs?
+
+Fortunately, Kani is able to report a coverage metric for each proof harness.
+In the `first-steps-v2` directory, try running:
+
+```
+cargo kani --coverage -Z line-coverage --harness verify_success
+```
+
+which verifies the harness, then prints coverage information for each line.
+In this case, we see that each line of `estimate_size` is followed by `FULL`, indicating that our proof harness provides full coverage.
+
+Try changing the assumption in the proof harness to `x < 2048`.
+Now the harness won't be testing all possible cases.
+Rerun the command.
+You'll see this line:
+
+```
+src/lib.rs, 24, NONE
+```
+
+which indicates that the proof no longer covers line 24, which addresses the case where `x >= 2048`.
diff --git a/docs/src/reference/experimental/experimental-features.md b/docs/src/reference/experimental/experimental-features.md
new file mode 100644
index 000000000000..bd9fb6cd8572
--- /dev/null
+++ b/docs/src/reference/experimental/experimental-features.md
@@ -0,0 +1,5 @@
+# Experimental Features
+
+We elaborate on some of the more commonly used experimental features in Kani.
+This is not an exhaustive list; to see all of Kani's experimental features, run `cargo kani --help`.
+To use an experimental feature, invoke Kani with the `--unstable` or `-Z` flag followed by the name of the feature.
\ No newline at end of file
diff --git a/docs/src/reference/stubbing.md b/docs/src/reference/experimental/stubbing.md
similarity index 99%
rename from docs/src/reference/stubbing.md
rename to docs/src/reference/experimental/stubbing.md
index b4eeb4fe6b98..0ffbba5f0b0b 100644
--- a/docs/src/reference/stubbing.md
+++ b/docs/src/reference/experimental/stubbing.md
@@ -113,7 +113,7 @@ In the following, we describe all the limitations of the stubbing feature.
 The usage of stubbing is limited to the verification of a single harness.
 Therefore, users are **required to pass the `--harness` option** when using the stubbing feature.
 
-In addition, this feature **isn't compatible with [concrete playback](../debugging-verification-failures.md#concrete-playback)**.
+In addition, this feature **isn't compatible with [concrete playback](./concrete-playback.md)**.
 
 ### Support
 
diff --git a/docs/src/tutorial-first-steps.md b/docs/src/tutorial-first-steps.md
index 57e70edb96dd..bbfd236c6b58 100644
--- a/docs/src/tutorial-first-steps.md
+++ b/docs/src/tutorial-first-steps.md
@@ -53,40 +53,11 @@ Kani has immediately found a failure.
 Notably, we haven't had to write explicit assertions in our proof harness: by default, Kani will find a host of erroneous conditions which include a reachable call to `panic` or a failing `assert`.
 If Kani had run successfully on this harness, this amounts to a mathematical proof that there is no input that could cause a panic in `estimate_size`.
 
-### Getting a trace
+> By default, Kani only reports failures, not how the failure happened.
+> In this example, it would be nice to get a concrete example of a value of `x` that triggers the failure.
+> Kani offers an (experimental) [concrete playback](reference/experimental/concrete-playback.md) feature that serves this purpose.
+> As an exercise, try applying concrete playback to this example and see what Kani outputs.
 
-By default, Kani only reports failures, not how the failure happened.
-In this running example, it seems obvious what we're interested in (the value of `x` that caused the failure) because we just have one unknown input at the start (similar to the property test), but that's kind of a special case.
-In general, understanding how a failure happened requires exploring a full (potentially large) _execution trace_.
-
-An execution trace is a record of exactly how a failure can occur.
-Nondeterminism (like a call to `kani::any()`, which could return any value) can appear in the middle of its execution.
-A trace is a record of exactly how execution proceeded, including concrete choices (like `1023`) for all of these nondeterministic values.
-
-To get a trace for a failing check in Kani, run:
-
-```
-cargo kani --visualize --enable-unstable
-```
-
-This command runs Kani and generates an HTML report that includes a trace.
-Open the report with your preferred browser.
-Under the "Errors" heading, click on the "trace" link to find the trace for this failure.
-
-From this trace report, we can filter through it to find relevant lines.
-A good rule of thumb is to search for either `kani::any()` or assignments to variables you're interested in.
-At present time, an unfortunate amount of generated code is present in the trace.
-This code isn't a part of the Rust code you wrote, but is an internal implementation detail of how Kani runs proof harnesses.
-Still, searching for `kani::any()` quickly finds us these lines:
-
-```
-let x: u32 = kani::any();
-x = 1023u
-```
-
-Here we're seeing the line of code and the value assigned in this particular trace.
-Like property testing, this is just one **example** of a failure.
-To proceed, we recommend fixing the code to avoid this particular issue and then re-running Kani to see if you find more issues.
 
 ### Exercise: Try other failures
 
@@ -193,25 +164,6 @@ Here's a revised example of the proof harness, one that now succeeds:
 {{#include tutorial/first-steps-v2/src/lib.rs:kani}}
 ```
 
-But now we must wonder if we've really fully tested our function.
-What if we revise the function, but forget to update the assumption in our proof harness to cover the new range of inputs?
-
-Fortunately, Kani is able to report a coverage metric for each proof harness.
-Try running:
-
-```
-cargo kani --visualize --harness verify_success
-```
-
-The beginning of the report includes coverage information.
-Clicking through to the file will show fully-covered lines in green.
-Lines not covered by our proof harness will show in red.
-
-Try changing the assumption in the proof harness to `x < 2048`.
-Now the harness won't be testing all possible cases.
-Rerun `cargo kani --visualize`.
-Look at the report: you'll see we no longer have 100% coverage of the function.
-
 ## Summary
 
 In this section:
@@ -219,6 +171,4 @@ In this section:
 1. We saw Kani find panics, assertion failures, and even some other failures like unsafe dereferencing of null pointers.
 2. We saw Kani find failures that testing could not easily find.
 3. We saw how to write a proof harness and use `kani::any()`.
-4. We saw how to get a failing **trace** using `kani --visualize`
-5. We saw how proof harnesses are used to set up preconditions with `kani::assume()`.
-6. We saw how to obtain **coverage** metrics and use them to ensure our proofs are covering as much as they should be.
+4. We saw how proof harnesses are used to set up preconditions with `kani::assume()`.
diff --git a/docs/src/tutorial-kinds-of-failure.md b/docs/src/tutorial-kinds-of-failure.md
index 29236b95db0c..00f9408ca709 100644
--- a/docs/src/tutorial-kinds-of-failure.md
+++ b/docs/src/tutorial-kinds-of-failure.md
@@ -25,7 +25,7 @@ This property test will immediately find a failing case, thanks to Rust's built-
 But what if we change this function to use unsafe Rust?
 
 ```rust
-return unsafe { *a.get_unchecked(i % a.len() + 1) };
+return unsafe { *a.as_ptr().add(i % a.len() + 1) };
 ```
 
 Now the error becomes invisible to this test:
@@ -55,7 +55,7 @@ cargo kani --harness bound_check
 We still see a failure from Kani, even without Rust's runtime bounds checking.
 
 > Also, notice there were many checks in the verification output.
-> (At time of writing, 351.)
+> (At time of writing, 345.)
 > This is a result of using the standard library `Vec` implementation, which means our harness actually used quite a bit of code, short as it looks.
 > Kani is inserting a lot more checks than appear as asserts in our code, so the output can be large.
 
@@ -63,7 +63,7 @@ We get the following summary at the end:
 
 ```
 SUMMARY: 
- ** 1 of 351 failed
+ ** 1 of 345 failed (8 unreachable)
 Failed Checks: dereference failure: pointer outside object bounds
  File: "./src/bounds_check.rs", line 11, in bounds_check::get_wrapped
 
@@ -79,71 +79,44 @@ Consider trying a few more small exercises with this example:
 1. Exercise: Switch back to the normal/safe indexing operation and re-try Kani.
 How does Kani's output change, compared to the unsafe operation?
 (Try predicting the answer, then seeing if you got it right.)
-2. Exercise: [Remember how to get a trace from Kani?](./tutorial-first-steps.md#getting-a-trace) Find out what inputs it failed on.
+2. Exercise: Try Kani's experimental [concrete playback](reference/experimental/concrete-playback.md) feature on this example.
 3. Exercise: Fix the error, run Kani, and see a successful verification.
 4. Exercise: Try switching back to the unsafe code (now with the error fixed) and re-run Kani. Does it still verify successfully?
 
 <details>
 <summary>Click to see explanation for exercise 1</summary>
 
-Having switched back to the safe indexing operation, Kani reports two failures:
+Having switched back to the safe indexing operation, Kani reports a bounds check failure:
 
 ```
-SUMMARY: 
- ** 2 of 350 failed
+SUMMARY:
+ ** 1 of 343 failed (8 unreachable)
 Failed Checks: index out of bounds: the length is less than or equal to the given index
- File: "./src/bounds_check.rs", line 11, in bounds_check::get_wrapped
-Failed Checks: dereference failure: pointer outside object bounds
- File: "./src/bounds_check.rs", line 11, in bounds_check::get_wrapped
+ File: "src/bounds_check.rs", line 11, in bounds_check::get_wrapped
 
 VERIFICATION:- FAILED
 ```
 
-The first is Rust's runtime bounds checking for the safe indexing operation.
-The second is Kani's check to ensure the pointer operation is actually safe.
-This pattern (two checks for similar issues in safe Rust code) is common to see, and we'll see it again in the next section.
-
-> **NOTE**: While Kani will always be checking for both properties, [in the future the output here may change](https://github.com/model-checking/kani/issues/1349).
-> You might have noticed that the bad pointer dereference can't happen, since the bounds check would panic first.
-> In the future, Kani's output may report only the bounds checking failure in this example.
-
 </details>
 
 <details>
 <summary>Click to see explanation for exercise 2</summary>
 
-Having run `cargo kani --harness bound_check --visualize` and clicked on one of the failures to see a trace, there are three things to immediately notice:
-
-1. This trace is huge. Because the standard library `Vec` is involved, there's a lot going on.
-2. The top of the trace file contains some "trace navigation tips" that might be helpful in navigating the trace.
-3. There's a lot of generated code and it's really hard to just read the trace itself.
-
-To navigate this trace to find the information you need, we again recommend searching for things you expect to be somewhere in the trace:
-
-1. Search the page for `kani::any` or `<variable_of_interest> =` such as `size =` or `let size`.
-We can use this to find out what example values lead to a problem.
-In this case, where we just have a couple of `kani::any` values in our proof harness, we can learn a lot just by seeing what these are.
-In this trace we find (and the values you get may be different):
-
-```
-Step 36: Function bound_check, File src/bounds_check.rs, Line 37
-let size: usize = kani::any();
-size = 2464ul
-
-Step 39: Function bound_check, File src/bounds_check.rs, Line 39
-let index: usize = kani::any();
-index = 2463ul
+`cargo kani -Z concrete-playback --concrete-playback=inplace --harness bound_check` produces the following test:
+```
+rust
+#[test]
+fn kani_concrete_playback_bound_check_4752536404478138800() {
+    let concrete_vals: Vec<Vec<u8>> = vec![
+        // 1ul
+        vec![1, 0, 0, 0, 0, 0, 0, 0],
+        // 18446744073709551615ul
+        vec![255, 255, 255, 255, 255, 255, 255, 255],
+    ];
+    kani::concrete_playback_run(concrete_vals, bound_check);
+}
 ```
-
-You may see different values here, as it depends on the solver's behavior.
-
-2. Try searching for `failure:`. This will be near the end of the page.
-You can now search upwards from a failure to see what values certain variables had.
-Sometimes it can be helpful to change the source code to add intermediate variables, so their value is visible in the trace.
-For instance, you might want to compute the index before indexing into the array.
-That way you'd see in the trace exactly what value is being used.
-
-These two techniques should help you find both the nondeterministic inputs, and the values that were involved in the failing assertion.
+which indicates that substituting the concrete values `size = 1` and `index = 2^64` in our proof harness will produce the out of bounds access.
 
 </details>
 
@@ -247,6 +220,5 @@ In this section:
 
 1. We saw Kani spot out-of-bounds accesses.
 2. We saw Kani spot actually-unsafe dereferencing of a raw pointer to invalid memory.
-3. We got more experience reading the traces that Kani generates, to debug a failing proof harness.
 3. We saw Kani spot a division by zero error and an overflowing addition.
-5. As an exercise, we tried proving an assertion (finding the midpoint) that was not completely trivial.
+4. As an exercise, we tried proving an assertion (finding the midpoint) that was not completely trivial.
diff --git a/docs/src/tutorial-real-code.md b/docs/src/tutorial-real-code.md
index c4bad5a2d82e..3dd216cd6258 100644
--- a/docs/src/tutorial-real-code.md
+++ b/docs/src/tutorial-real-code.md
@@ -74,7 +74,7 @@ A first proof will likely start in the following form:
 Running Kani on this simple starting point will help figure out:
 
 1. What unexpected constraints might be needed on your inputs (using `kani::assume`) to avoid "expected" failures.
-2. Whether you're over-constrained. Check the coverage report using `--visualize`. Ideally you'd see 100% coverage, and if not, it's usually because you've assumed too much (thus over-constraining the inputs).
+2. Whether you're over-constrained. Check the coverage report using `--coverage -Z line-coverage`. Ideally you'd see 100% coverage, and if not, it's usually because you've assumed too much (thus over-constraining the inputs).
 3. Whether Kani will support all the Rust features involved.
 4. Whether you've started with a tractable problem.
 (Remember to try setting `#[kani::unwind(1)]` to force early termination and work up from there.)
diff --git a/docs/src/tutorial/kinds-of-failure/src/bounds_check.rs b/docs/src/tutorial/kinds-of-failure/src/bounds_check.rs
index 9204d8f0f17e..c4a30982c95d 100644
--- a/docs/src/tutorial/kinds-of-failure/src/bounds_check.rs
+++ b/docs/src/tutorial/kinds-of-failure/src/bounds_check.rs
@@ -13,7 +13,7 @@ fn get_wrapped(i: usize, a: &[u32]) -> u32 {
 // ANCHOR_END: code
 
 // Alternative unsafe return for the above function:
-// return unsafe { *a.get_unchecked(i % a.len() + 1) };
+// return unsafe { *a.as_ptr().add(i % a.len() + 1) };
 
 #[cfg(test)]
 mod tests {
diff --git a/docs/src/usage.md b/docs/src/usage.md
index 459916c87222..aaa5d3fa234c 100644
--- a/docs/src/usage.md
+++ b/docs/src/usage.md
@@ -26,7 +26,7 @@ Common to both `kani` and `cargo kani` are many command-line flags:
  * `--concrete-playback=[print|inplace]`: _Experimental_, `--enable-unstable` feature that generates a Rust unit test case
  that plays back a failing proof harness using a concrete counterexample.
  If used with `print`, Kani will only print the unit test to stdout.
- If used with `inplace`, Kani will automatically add the unit test to the user's source code, next to the proof harness. For more detailed instructions, see the [debugging verification failures](./debugging-verification-failures.md) section.
+ If used with `inplace`, Kani will automatically add the unit test to the user's source code, next to the proof harness. For more detailed instructions, see the [concrete playback](./experimental/concrete-playback.md) section.
 
  * `--visualize`: _Experimental_, `--enable-unstable` feature that generates an HTML report providing traces (i.e., counterexamples) for each failure found by Kani.
 
diff --git a/docs/src/verification-results.md b/docs/src/verification-results.md
index a8187163d41b..100c9ed554be 100644
--- a/docs/src/verification-results.md
+++ b/docs/src/verification-results.md
@@ -38,7 +38,7 @@ Check 4: success_example.assertion.4
 ```
 
 2. `FAILURE`: This indicates that the check failed (i.e., the property doesn't
-hold). In this case, please see the [debugging verification failures](./debugging-verification-failures.md)
+hold). In this case, please see the [concrete playback](./experimental/concrete-playback.md)
 section for more help.
 
 Example: