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

@@ -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)

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.
 

docs/src/debugging-verification-failures.md → 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,15 +68,15 @@ 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,
 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 
+## 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.

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`.

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.

docs/src/reference/stubbing.md → 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
 
@@ -193,32 +164,11 @@ 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:
 
 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()`.

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,15 +55,15 @@ 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.
 
 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.

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.)

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 {

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: