docs: add conc playback docs to getting started tutorial (rust-lang#1537)

* docs: add conc playback sub-section to getting started

* refactor: change exe-trace name in Kani flags

* refactor: initial change over to new flags

* refactor: change exe_trace in Kani lib

* more Kani lib name updates

* update feature flag in docs

* bunch more name changes

* change det val to concrete val

* fix wording

* update arg desc

* make output_filename_opt more clean

* more renaming

* more det renaming in kani lib

* address some of Celina's comments

* remove all the rename changes

* some more updates

* change tense from 'user' to 'you'

* make setup section more clear

* update doc structure to debug verif fails

* turn options into bullets

* add enable-unstable

* add example

* add to example

* add mode description to args

* add link to milestone

Author: sanjit-bhat

docs/src/SUMMARY.md

@@ -5,6 +5,7 @@
     - [Building from source](./build-from-source.md)
   - [Using Kani](./usage.md)
   - [Verification results](./verification-results.md)
+  - [Debugging verification failures](./debugging-verification-failures.md)
 
 - [Tutorial](./kani-tutorial.md)
   - [First steps](./tutorial-first-steps.md)

docs/src/debugging-verification-failures.md

@@ -0,0 +1,107 @@
+# Debugging verification failures
+
+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
+
+This section describes the concrete playback feature in more detail.
+
+### Setup
+
+The Kani library needs to be linked as a dev dependency to the crate you're trying to debug.
+This requires adding the following lines to your `Cargo.toml` file,
+which differ depending on what version of the Kani library you would like to use:
+* The latest version:
+```toml
+[dev-dependencies]
+kani = { git = "https://github.com/model-checking/kani", features = ["concrete_playback"] }
+```
+* A specific version of the Kani library (v0.9+) that's already downloaded:
+```toml
+[dev-dependencies]
+kani = { path = "{path_to_kani_root}/library/kani", features = ["concrete_playback"] }
+```
+
+### Usage
+
+In order to enable this feature, run Kani with the `--enable-unstable --concrete-playback=[print|inplace]` flag.
+After getting a verification failure, Kani will generate a Rust unit test case that plays back a failing
+proof harness with a concrete counterexample.
+The concrete playback modes mean the following:
+* `print`: Kani will just print the unit test to stdout.
+You will then need to copy this unit test into the same module as your proof harness.
+* `inplace`: Kani will automatically copy the unit test into your source code.
+Before running this mode, you might find it helpful to have your existing code committed to `git`.
+That way, you can easily remove the unit test with `git revert`.
+Note that Kani will not copy the unit test into your source code if it detects
+that the exact same test already exists. 
+
+After the unit test is in your source code, you can run it with `cargo test`.
+To debug it, there are a couple of options:
+* If you have certain IDEs, there are extensions (e.g., `rust-analyzer` for `VS Code`)
+that support UI elements like a `Run Test | Debug` button next to all unit tests.
+* Otherwise, you can debug the unit test on the command line.
+To do this, you first run `cargo test {unit_test_func_name}`.
+The output from this will have a line in the beginning like `Running unittests {files} ({binary})`.
+You can then debug the binary with tools like `rust-gdb` or `lldb`.
+
+### Example
+
+Running `kani --harness proof_harness --enable-unstable --concrete-playback=print` on the following source file:
+```rust
+#[kani::proof]
+fn proof_harness() {
+    let a: u8 = kani::any();
+    let b: u16 = kani::any();
+    assert!(a / 2 * 2 == a &&
+            b / 2 * 2 == b);
+}
+```
+yields this concrete playback Rust unit test:
+```rust
+#[test]
+fn kani_concrete_playback_proof_harness_16220658101615121791() {
+    let concrete_vals: Vec<Vec<u8>> = vec![
+        // 133
+        vec![133],
+        // 35207
+        vec![135, 137],
+    ];
+    kani::concrete_playback_run(concrete_vals, proof_harness);
+}
+```
+Here, `133` and `35207` are the concrete values that, when substituted for `a` and `b`,
+cause an assertion failure.
+`vec![135, 137]` is the byte array representation of `35207`.
+
+### Common issues
+
+* `error[E0425]: cannot find function x in this scope`:
+this is usually caused by having `#[cfg(kani)]` somewhere in the control flow path of the user's proof harness.
+To fix this, remove `#[cfg(kani)]` from those paths.
+
+### 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,
+please add them to [this GitHub issue](https://github.com/model-checking/kani/issues/1536).
+We are tracking the existing feature requests in
+[this GitHub milestone](https://github.com/model-checking/kani/milestone/10).
+
+### 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.
+Kani generates warning messages for this.
+* This feature does not support generating unit tests for multiple assertion failures within the same harness.
+This limitation might be removed in the future.
+Kani generates warning messages for this.
+* This feature requires that you do not change your code or runtime configurations between when Kani generates the unit test and when you run it.
+For instance, if you linked with library A during unit test generation and library B during unit test play back,
+that might cause unintended errors in the unit test counterexample.
+Kani currently has no way to detect this issue.

docs/src/usage.md

@@ -23,6 +23,11 @@ This works like `cargo test` except that it will analyze all proof harnesses ins
 
 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.
+
  * `--visualize`: Generates an HTML report showing coverage information and providing traces (i.e., counterexamples) for each failure found by Kani.
 
  * `--tests`: Build in "[test mode](https://doc.rust-lang.org/rustc/tests/index.html)", i.e. with `cfg(test)` set and `dev-dependencies` available (when using `cargo kani`).

docs/src/verification-results.md

@@ -38,9 +38,8 @@ Check 4: success_example.assertion.4
 ```
 
 2. `FAILURE`: This indicates that the check failed (i.e., the property doesn't
-hold). In this case, you can examine a trace by re-running with the
-`--visualize` option.  This generates an HTML report with the trace
-information.
+hold). In this case, please see the [debugging verification failures](./debugging-verification-failures.md)
+section for more help.
 
 Example:
 ```rust

kani-driver/src/args.rs

@@ -43,7 +43,9 @@ pub struct KaniArgs {
     /// Generate visualizer report to <target-dir>/report/html/index.html
     #[structopt(long)]
     pub visualize: bool,
-    /// Generate concrete playback unit test and either 1) just print it to stdout or 2) add it in-place to the source code.
+    /// Generate concrete playback unit test.
+    /// If value supplied is 'print', Kani prints the unit test to stdout.
+    /// If value supplied is 'inplace', Kani automatically adds the unit test to your source code.
     /// This option does not work with `--output-format old`.
     #[structopt(
         long,