replace visualize references with concrete playback; fix links

docs/src/SUMMARY.md

@@ -18,7 +18,7 @@
  - [Experimental features](./reference/experimental/experimental-features.md)
  - [Coverage](./reference/experimental/coverage.md)
  - [Stubbing](./reference/experimental/stubbing.md)
- - [Debugging verification failures](./reference/experimental/debugging-verification-failures.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)

docs/src/reference/experimental/concrete-playback.md

@@ -1,11 +1,6 @@
 # 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.
+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.

docs/src/reference/experimental/coverage.md

@@ -1,6 +1,6 @@
 ## Coverage
 
-Recall our `estimate_size` example from [First steps](../tutorial-first-steps.md),
+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

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
 

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
 
@@ -200,5 +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()`.
+4. We saw how proof harnesses are used to set up preconditions with `kani::assume()`.

docs/src/tutorial-kinds-of-failure.md

@@ -79,7 +79,7 @@ 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?
 
@@ -102,40 +102,21 @@ VERIFICATION:- FAILED
 <details>
 <summary>Click to see explanation for exercise 2</summary>
 
-Having run `cargo kani --harness bound_check --visualize --enable-unstable` 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 523: Function bound_check, File src/bounds_check.rs, Line 37
-<- kani::any::<usize>
-Step 524: Function bound_check, File src/bounds_check.rs, Line 37
-size = 1ul (00000000 00000000 00000000 00000000 00000000 00000000 00000000 00000001)
-...
-Step 537: Function bound_check, File src/bounds_check.rs, Line 39
-<- kani::any::<usize>
-Step 538: Function bound_check, File src/bounds_check.rs, Line 39
-index = 18446744073709551615ul (11111111 11111111 11111111 11111111 11111111 11111111 11111111 11111111)
+`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>
 
@@ -239,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.

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.
 

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: