Migrate docs to new output format (rust-lang#914)

celinval · Mar 10, 2022 · fd0cbb9 · fd0cbb9
1 parent 6cbaa4c
commit fd0cbb9
Show file tree

Hide file tree

Showing 22 changed files with 134 additions and 110 deletions.
diff --git a/docs/src/install-guide.md b/docs/src/install-guide.md
@@ -87,12 +87,12 @@ You should get a result like this one:
 
 ```
 [snipped output]
-** Results:
-test.rs function main
-[main.assertion.1] line 2 assertion failed: 1 == 2: FAILURE
-
-** 1 of 1 failed (2 iterations)
-VERIFICATION FAILED
+RESULTS:
+Check 1: main.assertion.1
+         - Status: FAILURE
+         - Description: "assertion failed: 1 == 2"
+[...]
+VERIFICATION:- FAILED
 ```
 
 Fix the test and you should see `kani` succeed.
diff --git a/docs/src/kani-result-types.md b/docs/src/kani-result-types.md
@@ -1,4 +1,4 @@
-# Kani result types
+# Kani verification results
 
 The result of a check in Kani can be one of the following:
 

diff --git a/docs/src/kani-single-file.md b/docs/src/kani-single-file.md
@@ -24,7 +24,7 @@ This report will shows coverage information, as well as give traces for each fai
 
 **`--function <name>`** Kani defaults to assuming the starting function is called `main`.
 You can change it to a different function with this argument.
-Note that to "find" the function given, it needs to be given the `#[no_mangle]` annotation.
+Note that to "find" the function given, it needs to be given the `#[kani::proof]` annotation.
 
 **`--gen-c`** will generate a C file that roughly corresponds to the input Rust file.
 This can sometimes be helpful when trying to debug a problem with Kani.
@@ -57,4 +57,3 @@ The labels for each loop can be discovered by running with the following CBMC fl
 
 **`--show-loops`** Print the labels of each loop in the program.
 Useful for `--unwindset`.
-
diff --git a/docs/src/tutorial-first-steps.md b/docs/src/tutorial-first-steps.md
@@ -42,12 +42,12 @@ With Kani, however:
 [...]
 Runtime decision procedure: 0.00116886s
 
-** Results:
-./src/lib.rs function estimate_size
-[estimate_size.assertion.1] line 9 Oh no, a failing corner case!: FAILURE
-
-** 1 of 1 failed (2 iterations)
-VERIFICATION FAILED
+RESULTS:
+Check 3: estimate_size.assertion.1
+         - Status: FAILURE
+         - Description: "Oh no, a failing corner case!"
+[...]
+VERIFICATION:- FAILED
 ```
 
 Kani has immediately found a failure.
@@ -106,12 +106,14 @@ Still, it is just a warning, and we can run the code without test failures just
 But Kani still catches the issue:
 
 ```
-** Results:
-./src/lib.rs function estimate_size
-[estimate_size.pointer_dereference.1] line 10 dereference failure: pointer NULL in *var_10: FAILURE
-
-** 1 of 1 failed (2 iterations)
-VERIFICATION FAILED
+[...]
+RESULTS:
+[...]
+Check 2: foo.pointer_dereference.1
+         - Status: FAILURE
+         - Description: "dereference failure: pointer NULL"
+[...]
+VERIFICATION:- FAILED
 ```
 
 **Can you find an example where the Rust compiler will not complain, and Kani will?**
@@ -126,13 +128,17 @@ return 1 << x;
 Overflow (addition, multiplication, etc, and this case, [bitshifting by too much](https://github.com/rust-lang/rust/issues/10183)) is also caught by Kani:
 
 ```
-** Results:
-./src/lib.rs function estimate_size
-[estimate_size.assertion.1] line 10 attempt to shift left by `move _10`, which would overflow: FAILURE
-[estimate_size.undefined-shift.1] line 10 shift distance too large in 1 << var_10: FAILURE
+RESULTS:
+[...]
+Check 3: foo.assertion.1
+         - Status: FAILURE
+         - Description: "attempt to shift left with overflow"
 
-** 2 of 2 failed (2 iterations)
-VERIFICATION FAILED
+Check 4: foo.undefined-shift.1
+         - Status: FAILURE
+         - Description: "shift distance too large"
+[...]
+VERIFICATION:- FAILED
 ```
 
 </details>
@@ -150,12 +156,14 @@ Now we have stated our previously implicit expectation: this function should nev
 But if we attempt to verify this, we get a problem:
 
 ```
-** Results:
-./src/final_form.rs function estimate_size
-[estimate_size.assertion.1] line 3 assertion failed: x < 4096: FAILURE
-
-** 1 of 1 failed (2 iterations)
-VERIFICATION FAILED
+[...]
+RESULTS:
+[...]
+Check 3: final_form::estimate_size.assertion.1
+         - Status: FAILURE
+         - Description: "assertion failed: x < 4096"
+[...]
+VERIFICATION:- FAILED
 ```
 
 We intended this to be a precondition of calling the function, but Kani is treating it like a failure.

diff --git a/docs/src/tutorial-kinds-of-failure.md b/docs/src/tutorial-kinds-of-failure.md
@@ -43,21 +43,35 @@ But we're able to check this unsafe code with Kani:
 ```
 
 ```
-# kani src/bounds_check.rs
+# kani src/bounds_check.rs --function bound_check
 [...]
-** 1 of 468 failed (2 iterations)
-VERIFICATION FAILED
+** 15 of 448 failed
+[...]
+VERIFICATION:- FAILED
 ```
 
-Notice there were a *lot* of verification conditions being checked: in the above output, 468! (It may change for you.)
+Notice there were a *lot* of verification conditions being checked: in the above output, 448! (It may change for you.)
 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.
 Let's narrow that output down a bit:
 
 ```
-# kani src/bounds_check.rs | grep FAIL
-[get_wrapped.pointer_dereference.5] line 10 dereference failure: pointer outside object bounds in *var_5: FAILURE
-VERIFICATION FAILED
+# kani src/bounds_check.rs --function bound_check | grep Failed
+Failed Checks: attempt to compute offset which would overflow
+Failed Checks: attempt to calculate the remainder with a divisor of zero
+Failed Checks: attempt to add with overflow
+Failed Checks: division by zero
+Failed Checks: dereference failure: pointer NULL
+Failed Checks: dereference failure: deallocated dynamic object
+Failed Checks: dereference failure: dead object
+Failed Checks: dereference failure: pointer outside object bounds
+Failed Checks: dereference failure: invalid integer address
+Failed Checks: arithmetic overflow on unsigned to signed type conversion
+Failed Checks: pointer arithmetic: pointer NULL
+Failed Checks: pointer arithmetic: deallocated dynamic object
+Failed Checks: pointer arithmetic: dead object
+Failed Checks: pointer arithmetic: pointer outside object bounds
+Failed Checks: pointer arithmetic: invalid integer address
 ```
 
 Notice that, for Kani, this has gone from a simple bounds-checking problem to a pointer-checking problem.
@@ -75,13 +89,12 @@ Consider trying a few more small exercises with this example:
 <details>
 <summary>Click to see explanation for exercise 1</summary>
 
-Having switched back to the safe indexing operation, Kani reports two failures instead of just one:
+Having switched back to the safe indexing operation, Kani reports two failures:
 
 ```
-# kani src/bounds_check.rs | grep FAIL
-[get_wrapped.assertion.3] line 9 index out of bounds: the length is move _12 but the index is _5: FAILURE
-[get_wrapped.pointer_dereference.5] line 9 dereference failure: pointer outside object bounds in a.data[var_5]: FAILURE
-VERIFICATION FAILED
+# kani src/bounds_check.rs --function bound_check | grep Failed
+Failed Checks: index out of bounds: the length is less than or equal to the given index
+Failed Checks: dereference failure: pointer outside object bounds
 ```
 
 The first is Rust's implicit assertion for the safe indexing operation.
@@ -163,24 +176,18 @@ Kani will find these failures as well.
 Here's the output from Kani:
 
 ```
-# kani src/overflow.rs
+# kani src/overflow.rs --function add_overflow
 [...]
-** Results:
-./src/overflow.rs function simple_addition
-[simple_addition.assertion.1] line 6 attempt to compute `move _3 + move _4`, which would overflow: FAILURE
-[simple_addition.overflow.1] line 6 arithmetic overflow on unsigned + in var_3 + var_4: FAILURE
-
-** 2 of 2 failed (2 iterations)
-VERIFICATION FAILED
+RESULTS:
+Check 1: simple_addition.assertion.1
+         - Status: FAILURE
+         - Description: "attempt to add with overflow"
+[...]
+VERIFICATION:- FAILED
 ```
 
-Notice the two failures: the Rust-inserted overflow check (`simple_addition.assertion.1`) and Kani's explicit overflow check (`simple_addition.overflow.1`).
-
-> **NOTE:** You could attempt to fix this issue by using Rust's alternative mathematical functions with explicit overflow behavior.
+This issue can be fixed using Rust's alternative mathematical functions with explicit overflow behavior.
 For instance, instead of `a + b` write `a.wrapping_add(b)`.
->
-> However, [at the present time](https://github.com/model-checking/kani/issues/480), while this disables the dynamic assertion that Rust inserts, it does not disable the additional Kani overflow check.
-> As a result, this currently still fails in Kani.
 
 ### Exercise: Classic overflow failure
 

diff --git a/docs/src/tutorial-loops-unwinding.md b/docs/src/tutorial-loops-unwinding.md
@@ -39,14 +39,14 @@ Kani will automatically generate verification conditions that help us understand
 Let's start with the "sledge hammer" by dropping all the way down to size 1:
 
 ```
-# kani src/lib.rs --cbmc-args --unwind 1
-[.unwind.0] unwinding assertion loop 0: FAILURE
-VERIFICATION FAILED
+# kani src/lib.rs --unwind 1
+Check 69: .unwind.0
+         - Status: FAILURE
+         - Description: "unwinding assertion loop 0"
+[...]
+VERIFICATION:- FAILED
 ```
 
-> **NOTE:** `--unwind` is a flag to the underlying model checker, CBMC, and so it needs to appear after `--cbmc-args`.
-> This flag `--cbmc-args` "switches modes" in the command line from Kani flags to CBMC flags, so we place all Kani flags and arguments before it.
-
 This output is showing us two things:
 
 1. Kani tells us we haven't unwound enough. This is the failure of the "unwinding assertion."
@@ -58,29 +58,26 @@ Doing an initial `--unwind 1` is generally enough to force termination, but ofte
 We were clearly aiming at a size limit of 10 in our proof harness, so let's try a few things here:
 
 ```
-# kani src/lib.rs --cbmc-args --unwind 10 | grep FAIL
-[.unwind.0] unwinding assertion loop 0: FAILURE
-VERIFICATION FAILED
+# kani src/lib.rs --unwind 10 | grep Failed
+Failed Checks: unwinding assertion loop 0
 ```
 
 A bound of 10 still isn't enough because we generally need to unwind one greater than the number of executed loop iterations:
 
 ```
-# kani src/lib.rs --cbmc-args --unwind 11 | grep FAIL
-[initialize_prefix.unwind.0] line 11 unwinding assertion loop 0: FAILURE
-[initialize_prefix.assertion.2] line 12 index out of bounds: the length is move _20 but the index is _19: FAILURE
-[initialize_prefix.pointer_dereference.5] line 12 dereference failure: pointer outside object bounds in buffer.data[var_19]: FAILURE
-VERIFICATION FAILED
+# kani src/lib.rs --unwind 11 | grep Failed
+Failed Checks: index out of bounds: the length is less than or equal to the given index
+Failed Checks: dereference failure: pointer outside object bounds
+Failed Checks: unwinding assertion loop 0
 ```
 
 We're still not seeing the unwinding assertion failure go away!
 This is because our error is really an off by one problem, we loop one too many times, so let's add one more:
 
 ```
-# kani src/lib.rs --cbmc-args --unwind 12 | grep FAIL
-[initialize_prefix.assertion.2] line 12 index out of bounds: the length is move _20 but the index is _19: FAILURE
-[initialize_prefix.pointer_dereference.5] line 12 dereference failure: pointer outside object bounds in buffer.data[var_19]: FAILURE
-VERIFICATION FAILED
+# kani src/lib.rs --unwind 12 | grep Failed
+Failed Checks: index out of bounds: the length is less than or equal to the given index
+Failed Checks: dereference failure: pointer outside object bounds
 ```
 
 Kani is now sure we've unwound the loop enough to verify our proof harness, and now we're seeing just the bound checking failures from the off by one error.
@@ -104,7 +101,7 @@ For example, we see 0.5s at unwinding 12, and 3s at unwinding 100.
 In situations where you need to optimize solving time better, specific bounds for specific loops can be provided on the command line.
 
 ```
-# kani src/lib.rs --cbmc-args --show-loops
+# kani src/lib.rs --output-format old --cbmc-args --show-loops
 [...]
 Loop _RNvCs6JP7pnlEvdt_3lib17initialize_prefix.0:
   file ./src/lib.rs line 11 column 5 function initialize_prefix
@@ -115,6 +112,11 @@ Loop _RNvMs8_NtNtCswN0xKFrR8r_4core3ops5rangeINtB5_14RangeInclusivejE8is_emptyCs
 Loop gen-repeat<[u8; 10]::16806744624734428132>.0:
 ```
 
+> **NOTE:** `--show-loops` is a flag to the underlying model checker, CBMC, and so it needs to appear after `--cbmc-args`.
+> This flag `--cbmc-args` "switches modes" in the command line from Kani flags to CBMC flags, so we place all Kani flags and arguments before it.
+> Also, the `--output-format old` flag turns off the post-processing of output from CBMC, which is needed here because with `--show-loops`,
+> CBMC is not running the actual verification step.
+
 This command shows us the mangled names of the loops involved.
 Then we can specify the bound for specific loops by name, from the command line:
 

diff --git a/docs/src/tutorial/arbitrary-variables/Cargo.toml b/docs/src/tutorial/arbitrary-variables/Cargo.toml
@@ -11,4 +11,4 @@ vector-map = "1.0.1"
 [workspace]
 
 [workspace.metadata.kani]
-flags = { default-checks = false, unwind = "2", output-format = "old" }
+flags = { default-checks = false, unwind = "2" }
diff --git a/docs/src/tutorial/arbitrary-variables/check_rating.expected b/docs/src/tutorial/arbitrary-variables/check_rating.expected
@@ -1,4 +1,5 @@
-[rating::verification::check_rating.assertion.1] line 38 assertion failed: rating.get() <= 5: SUCCESS
-[rating::verification::check_rating.assertion.2] line 39 assertion failed: Rating::from(rating.get()).is_some(): SUCCESS
-VERIFICATION SUCCESSFUL
-
+SUCCESS\
+assertion failed: rating.get() <= 5
+SUCCESS\
+assertion failed: Rating::from(rating.get()).is_some()
+VERIFICATION:- SUCCESSFUL
diff --git a/docs/src/tutorial/arbitrary-variables/safe_update.expected b/docs/src/tutorial/arbitrary-variables/safe_update.expected
@@ -1,3 +1,5 @@
-[inventory::verification::safe_update.assertion.1] line 38 "NonZeroU32 is internally a u32 but it should never be 0.": SUCCESS
-[inventory::verification::safe_update.assertion.2] line 42 assertion failed: inventory.get(&id).unwrap() == quantity: SUCCESS
-VERIFICATION SUCCESSFUL
+SUCCESS\
+"NonZeroU32 is internally a u32 but it should never be 0."
+SUCCESS\
+assertion failed: inventory.get(&id).unwrap() == quantity
+VERIFICATION:- SUCCESSFUL
diff --git a/docs/src/tutorial/arbitrary-variables/unsafe_update.expected b/docs/src/tutorial/arbitrary-variables/unsafe_update.expected
@@ -1,3 +1,5 @@
-[inventory::verification::unsafe_update.assertion.1] line 61 assertion failed: inventory.get(&id).unwrap() == quantity: SUCCESS
-called `Option::unwrap()` on a `None` value: FAILURE
-VERIFICATION FAILED
+SUCCESS\
+assertion failed: inventory.get(&id).unwrap() == quantity
+FAILURE\
+called `Option::unwrap()` on a `None` value
+VERIFICATION:- FAILED
diff --git a/docs/src/tutorial/kani-first-steps/Cargo.toml b/docs/src/tutorial/kani-first-steps/Cargo.toml
@@ -11,6 +11,3 @@ edition = "2018"
 proptest = "1.0.0"
 
 [workspace]
-
-[workspace.metadata.kani]
-flags = { output-format = "old" }
diff --git a/docs/src/tutorial/kani-first-steps/main.expected b/docs/src/tutorial/kani-first-steps/main.expected
@@ -1 +1,2 @@
-[estimate_size.assertion.1] line 17 Oh no, a failing corner case!: FAILURE
+FAILURE\
+Oh no, a failing corner case!
diff --git a/docs/src/tutorial/kani-first-steps/src/lib.rs b/docs/src/tutorial/kani-first-steps/src/lib.rs
@@ -51,7 +51,7 @@ mod tests {
 
 // ANCHOR: kani
 #[cfg(kani)]
-#[no_mangle]
+#[kani::proof]
 fn main() {
     let x: u32 = kani::any();
     estimate_size(x);

diff --git a/docs/src/tutorial/kani-first-steps/verify_failure.expected b/docs/src/tutorial/kani-first-steps/verify_failure.expected
@@ -1 +1,2 @@
-[final_form::estimate_size.assertion.1] line 6 assertion failed: x < 4096: FAILURE
+FAILURE\
+assertion failed: x < 4096
diff --git a/docs/src/tutorial/kani-first-steps/verify_success.expected b/docs/src/tutorial/kani-first-steps/verify_success.expected
@@ -1,2 +1,4 @@
-[final_form::estimate_size.assertion.1] line 6 assertion failed: x < 4096:
-[final_form::verify_success.assertion.1] line 58 assertion failed: y < 10:
+SUCCESS\
+assertion failed: x < 4096
+SUCCESS\
+assertion failed: y < 10
diff --git a/docs/src/tutorial/kinds-of-failure/Cargo.toml b/docs/src/tutorial/kinds-of-failure/Cargo.toml
@@ -11,6 +11,3 @@ edition = "2018"
 proptest = "1.0.0"
 
 [workspace]
-
-[workspace.metadata.kani]
-flags = { output-format = "old" }
diff --git a/docs/src/tutorial/kinds-of-failure/add_overflow.expected b/docs/src/tutorial/kinds-of-failure/add_overflow.expected
@@ -1 +1,2 @@
-[overflow::simple_addition.assertion.1] line 7 attempt to add with overflow: FAILURE
+FAILURE\
+attempt to add with overflow
diff --git a/docs/src/tutorial/kinds-of-failure/bound_check.expected b/docs/src/tutorial/kinds-of-failure/bound_check.expected
@@ -1,3 +1,5 @@
-line 11 index out of bounds: the length is less than or equal to the given index
-line 11 dereference failure: pointer outside object bounds in a.data[var_5]: FAILURE
-VERIFICATION FAILED
+FAILURE\
+index out of bounds: the length is less than or equal to the given index
+FAILURE\
+dereference failure: pointer outside object bounds
+VERIFICATION:- FAILED
diff --git a/docs/src/tutorial/kinds-of-failure/midpoint_overflow.expected b/docs/src/tutorial/kinds-of-failure/midpoint_overflow.expected
@@ -1,2 +1,3 @@
-[overflow_quicksort::find_midpoint.assertion.1] line 7 attempt to add with overflow: FAILURE
-VERIFICATION FAILED
+FAILURE\
+attempt to add with overflow
+VERIFICATION:- FAILED
diff --git a/docs/src/tutorial/loops-unwinding/Cargo.toml b/docs/src/tutorial/loops-unwinding/Cargo.toml
@@ -10,4 +10,4 @@ edition = "2018"
 [workspace]
 
 [package.metadata.kani]
-flags = { unwind = "11", output-format = "old" }
+flags = { unwind = "11" }