Add documentation for cover properties (rust-lang#2057)

Author: zhassan-aws

docs/src/getting-started/verification-results/src/main.rs

@@ -48,4 +48,49 @@ fn unsupp(x: &mut u8) {
 
 // ANCHOR_END: undetermined_example
 
+#[kani::proof]
+// ANCHOR: cover_satisfied_example
+#[kani::unwind(256)]
+fn cover_satisfied_example() {
+    let mut x: u8 = kani::any();
+    let mut y: u8 = kani::any();
+    y /= 2;
+    let mut i = 0;
+    while x != 0 && y != 0 {
+        kani::cover!(i > 2 && x == 24 && y == 72);
+        if x >= y { x -= y; }
+        else { y -= x; }
+        i += 1;
+    }
+}
+// ANCHOR_END: cover_satisfied_example
+
+#[kani::proof]
+// ANCHOR: cover_unsatisfiable_example
+#[kani::unwind(6)]
+fn cover_unsatisfiable_example() {
+    let bytes: [u8; 5] = kani::any();
+    let s = std::str::from_utf8(&bytes);
+    if let Ok(s) = s {
+        kani::cover!(s.chars().count() <= 1);
+    }
+}
+// ANCHOR_END: cover_unsatisfiable_example
+
+#[kani::proof]
+// ANCHOR: cover_unreachable_example
+#[kani::unwind(6)]
+fn cover_unreachable_example() {
+    let r1: std::ops::Range<i32> = kani::any()..kani::any();
+    let r2: std::ops::Range<i32> = kani::any()..kani::any();
+    kani::assume(!r1.is_empty());
+    kani::assume(!r2.is_empty());
+    if r2.start > r1.end {
+        if r2.end < r1.end {
+            kani::cover!(r2.contains(&0));
+        }
+    }
+}
+// ANCHOR_END: cover_unreachable_example
+
 fn main() {}

docs/src/verification-results.md

@@ -94,3 +94,68 @@ Check 2: undetermined_example.assertion.2
          - Status: UNDETERMINED
          - Description: "assertion failed: x == 0"
 ```
+
+## Cover property results
+
+Kani provides a [`kani::cover`](https://model-checking.github.io/kani/crates/doc/kani/macro.cover.html) macro that can be used for checking whether a condition may occur at a certain point in the code.
+
+The result of a cover property can be one of the following:
+
+1. `SATISFIED`: This indicates that Kani found an execution that triggers the specified condition.
+
+The following example uses `kani::cover` to check if it's possible for `x` and `y` to hold the values 24 and 72, respectively, after 3 iterations of the `while` loop, which turns out to be the case.
+```rust
+{{#include getting-started/verification-results/src/main.rs:cover_satisfied_example}}
+```
+Results:
+```
+Check 1: cover_satisfied_example.cover.1
+         - Status: SATISFIED
+         - Description: "cover condition: i > 2 && x == 24 && y == 72"
+         - Location: src/main.rs:60:9 in function cover_satisfied_example
+```
+
+2. `UNSATISFIABLE`: This indicates that Kani _proved_ that the specified condition is impossible.
+
+The following example uses `kani::cover` to check if it's possible to have a UTF-8 encoded string consisting of 5 bytes that correspond to a string with a single character.
+```rust
+{{#include getting-started/verification-results/src/main.rs:cover_unsatisfiable_example}}
+```
+which is not possible as such string will contain at least two characters.
+```
+Check 46: cover_unsatisfiable_example.cover.1
+         - Status: UNSATISFIABLE
+         - Description: "cover condition: s.chars().count() <= 1"
+         - Location: src/main.rs:75:9 in function cover_unsatisfiable_example
+```
+
+3. `UNREACHABLE`: This indicates that the `cover` property itself is unreachable (i.e. it is _vacuously_ unsatisfiable).
+
+In contrast to an `UNREACHABLE` result for assertions, an unreachable (or an unsatisfiable) cover property may indicate an incomplete proof.
+
+Example:
+In this example, a `kani::cover` call is unreachable because if the outer `if` condition holds, then the non-empty range `r2` is strictly larger than the non-empty range `r1`, in which case, the condition in the inner `if` condition is impossible.
+```rust
+{{#include getting-started/verification-results/src/main.rs:cover_unreachable_example}}
+```
+```
+Check 3: cover_unreachable_example.cover.1
+         - Status: UNREACHABLE
+         - Description: "cover condition: r2.contains(&0)"
+         - Location: src/main.rs:90:13 in function cover_unreachable_example
+```
+
+4. `UNDETERMINED`: This is the same as the `UNDETERMINED` result for normal checks (see [check_results]).
+
+## Verification summary
+
+Kani reports a summary at the end of the verification report, which includes the overall results of all checks, the overall results of cover properties (if the package includes cover properties), and the overall verification result, e.g.:
+```
+SUMMARY:
+ ** 0 of 786 failed (41 unreachable)
+
+ ** 0 of 1 cover properties satisfied
+
+
+VERIFICATION:- SUCCESSFUL
+```