Add documentation of Kani result types (rust-lang#864)

Author: zhassan-aws

docs/README.md

@@ -18,5 +18,5 @@ It also means the necessary `kani-` flag-comments must appear in each file.
 To run just these tests, return to the Kani root directory and run:
 
 ```
-COMPILETEST_FORCE_STAGE0=1 ./x.py test -i --stage 0 kani-docs
+cargo run -p compiletest --quiet -- --suite kani-docs --mode cargo-kani --quiet
 ```

docs/src/SUMMARY.md

@@ -5,6 +5,7 @@
   - [Comparison with other tools](./tool-comparison.md)
   - [Kani on a single file](./kani-single-file.md)
   - [Kani on a package](./cargo-kani.md)
+  - [Kani result types](./kani-result-types.md)
   - [Debugging failures]()
   - [Debugging non-termination]()
   - [Debugging coverage]()

docs/src/getting-started/result-types/Cargo.toml

@@ -0,0 +1,11 @@
+[package]
+name = "result-types"
+version = "0.1.0"
+edition = "2018"
+
+[dependencies]
+
+[workspace]
+
+[package.metadata.kani]
+flags = {output-format = "regular", assertion-reach-checks = true}

docs/src/getting-started/result-types/failure_example.expected

@@ -0,0 +1 @@
+FAILURE

docs/src/getting-started/result-types/src/main.rs

@@ -0,0 +1,48 @@
+#[kani::proof]
+// ANCHOR: success_example
+fn success_example() {
+    let mut sum = 0;
+    for i in 1..4 {
+        sum += i;
+    }
+    assert_eq!(sum, 6);
+}
+// ANCHOR_END: success_example
+
+#[kani::proof]
+// ANCHOR: failure_example
+fn failure_example() {
+    let arr = [1, 2, 3];
+    assert_ne!(arr.len(), 3);
+}
+// ANCHOR_END: failure_example
+
+#[kani::proof]
+// ANCHOR: unreachable_example
+fn unreachable_example() {
+    let x = 5;
+    let y = x + 2;
+    if x > y {
+        assert!(x < 8);
+    }
+}
+// ANCHOR_END: unreachable_example
+
+#[kani::proof]
+// ANCHOR: undetermined_example
+fn undetermined_example() {
+    let mut x = 0;
+    unsupp(&mut x);
+    assert!(x == 0);
+}
+
+#[feature(asm)]
+fn unsupp(x: &mut u8) {
+    unsafe {
+        std::arch::asm!("nop");
+    }
+}
+
+// ANCHOR_END: undetermined_example
+
+fn main() {}

docs/src/getting-started/result-types/success_example.expected

@@ -0,0 +1 @@
+SUCCESS

docs/src/getting-started/result-types/undetermined_example.expected

@@ -0,0 +1 @@
+UNDETERMINED

docs/src/getting-started/result-types/unreachable_example.expected

@@ -0,0 +1 @@
+UNREACHABLE

docs/src/kani-result-types.md

@@ -0,0 +1,80 @@
+# Kani result types
+
+The result of a check in Kani can be one of the following:
+
+1. `SUCCESS`: This indicates that the check passed, i.e., the property holds.
+Note that in some cases, the property may hold _vacuously_. This can occur
+because the property is unreachable, or because the harness is
+_over-constrained_.
+
+Example:
+```rust
+{{#include getting-started/result-types/src/main.rs:success_example}}
+```
+The output from Kani indicates that the assertion holds:
+```
+Check 4: success_example.assertion.4
+         - Status: SUCCESS
+         - Description: "assertion failed: sum == 6"
+```
+
+2. `FAILURE`: This indicates that the check failed, i.e., the property doesn't
+hold. In this case, you can view the failure trace by re-running with the
+`--visualize` option.  This generates a directory that contains the trace
+information. Load the `html/index.html` file from that directory in a browser to
+examine the trace.
+
+Example:
+```rust
+{{#include getting-started/result-types/src/main.rs:failure_example}}
+```
+The assertion doesn't hold as Kani's output indicates:
+```
+Check 2: failure_example.assertion.2
+         - Status: FAILURE
+         - Description: "assertion failed: arr.len() != 3"
+```
+
+3. `UNREACHABLE` (requires `--assertion-reach-checks`): This indicates that the check is unreachable. This occurs when
+there is no possible execution trace that can reach the check's line of code.
+This may be because the function that contains the check is unused, or that the
+harness does not trigger the condition under which the check is invoked. Kani
+currently checks the reachability of the following assertion types:
+    1. Assert macros (e.g. `assert`, `assert_eq`, etc.)
+    2. Arithmetic overflow checks
+    3. Negation overflow checks
+    4. Index out-of-bound checks
+    5. Divide/remainder-by-zero checks
+
+
+Example:
+
+```rust
+{{#include getting-started/result-types/src/main.rs:unreachable_example}}
+```
+
+The output from Kani when run with `--assertion-reach-checks` indicates that
+the assertion is unreachable:
+```
+Check 2: unreachable_example.assertion.2
+         - Status: UNREACHABLE
+         - Description: "assertion failed: x < 8"
+```
+
+4. `UNDETERMINED`: This indicates that Kani was not able to conclude whether the
+property holds or not. This can occur when the Rust program contains a construct
+that is not currently supported by Kani. See
+[Limitations](./limitations.md#limitations) for Kani's current support of the
+Rust language features.
+
+Example:
+```rust
+{{#include getting-started/result-types/src/main.rs:undetermined_example}}
+```
+The output from Kani indicates that the assertion is undetermined due to the
+missing support for inline assembly in Kani:
+```
+Check 2: undetermined_example.assertion.2
+         - Status: UNDETERMINED
+         - Description: "assertion failed: x == 0"
+```