Rectangle regression test for cargo kani (rust-lang#909)

New regression test that shows unit testing, property-based testing and Kani

Author: nchong-at-aws

tests/cargo-kani/rectangle-example/Cargo.toml

@@ -0,0 +1,9 @@
+[package]
+name = "rectangle-example"
+version = "0.1.0"
+edition = "2018"
+
+[dependencies]
+
+[dev-dependencies]
+proptest = "1.0.0"

tests/cargo-kani/rectangle-example/README.md

@@ -0,0 +1,51 @@
+Using an implementation of a `Rectangle` we use unit tests, property-based testing and Kani
+
+## Reproducing results locally
+
+### Dependencies
+
+  - Rust edition 2018
+  - [Kani](https://model-checking.github.io/kani/getting-started.html)
+
+If you have problems installing Kani then please file an [issue](https://github.com/model-checking/kani/issues/new/choose).
+
+###  Unit testing and proptest
+
+Use `cargo test` to run the unit test and property-based test.
+
+```bash
+$ cargo test
+# --snip--
+running 2 tests
+test rectangle::tests::stretched_rectangle_can_hold_original ... ok
+test rectangle::proptests::stretched_rectangle_can_hold_original ... ok
+```
+
+### Using Kani
+
+Use `cargo kani` to verify the first proof harness `stretched_rectangle_can_hold_original`. As we explain in the post, verification failure is expected.
+
+```bash
+$ cargo kani --function stretched_rectangle_can_hold_original --output-format terse
+# --snip--
+VERIFICATION:- FAILED
+```
+
+In order to view a trace (a step-by-step execution of the program) use the `--visualize` flag:
+
+```bash
+$ cargo kani --function stretched_rectangle_can_hold_original --output-format terse --visualize
+# --snip--
+VERIFICATION:- FAILED
+# and generates a html report in target/report/html/index.html
+```
+
+And open the report in a browser.
+
+After fixing the problem we can re-run Kani (on the proof harness `stretched_rectangle_can_hold_original_fixed`). This time we expect verification success:
+
+```bash
+$ cargo kani --function stretched_rectangle_can_hold_original_fixed --output-format terse
+# --snip--
+VERIFICATION:- SUCCESSFUL
+```

tests/cargo-kani/rectangle-example/src/lib.rs

@@ -0,0 +1,4 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+pub mod rectangle;

tests/cargo-kani/rectangle-example/src/rectangle.rs

@@ -0,0 +1,108 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// ANCHOR: rectangle_definition
+#[derive(Debug, Copy, Clone)]
+struct Rectangle {
+    width: u64,
+    height: u64,
+}
+
+impl Rectangle {
+    fn can_hold(&self, other: &Rectangle) -> bool {
+        self.width > other.width && self.height > other.height
+    }
+}
+// ANCHOR_END: rectangle_definition
+
+impl Rectangle {
+    // ANCHOR: stretch_definition
+    fn stretch(&self, factor: u64) -> Option<Self> {
+        let w = self.width.checked_mul(factor)?;
+        let h = self.height.checked_mul(factor)?;
+        Some(Rectangle { width: w, height: h })
+    }
+    // ANCHOR_END: stretch_definition
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    // ANCHOR: stretch_unit_test
+    #[test]
+    fn stretched_rectangle_can_hold_original() {
+        let original = Rectangle { width: 8, height: 7 };
+        let factor = 2;
+        let larger = original.stretch(factor);
+        assert!(larger.unwrap().can_hold(&original));
+    }
+    // ANCHOR_END: stretch_unit_test
+}
+
+#[cfg(test)]
+mod proptests {
+    use super::*;
+    use proptest::num::u64;
+    use proptest::prelude::*;
+
+    proptest! {
+        // ANCHOR: stretch_proptest
+        #[test]
+        fn stretched_rectangle_can_hold_original(width in u64::ANY,
+            height in u64::ANY,
+            factor in u64::ANY) {
+            let original = Rectangle {
+                width: width,
+                height: height,
+            };
+            if let Some(larger) = original.stretch(factor) {
+                assert!(larger.can_hold(&original));
+            }
+        }
+        // ANCHOR_END: stretch_proptest
+    }
+}
+
+#[cfg(kani)]
+mod verification {
+    use super::*;
+
+    // ANCHOR: stretch_kani
+    #[kani::proof]
+    pub fn stretched_rectangle_can_hold_original() {
+        let original = Rectangle { width: kani::any(), height: kani::any() };
+        let factor = kani::any();
+        if let Some(larger) = original.stretch(factor) {
+            assert!(larger.can_hold(&original));
+        }
+    }
+    // ANCHOR_END: stretch_kani
+
+    // ANCHOR: stretch_kani_fixed
+    #[kani::proof]
+    pub fn stretched_rectangle_can_hold_original_fixed() {
+        let original = Rectangle { width: kani::any(), height: kani::any() };
+        let factor: u8 = kani::any(); //< would like to make u64
+        kani::assume(0 != original.width);
+        kani::assume(0 != original.height);
+        kani::assume(1 < factor);
+        if let Some(larger) = original.stretch(factor as u64) {
+            assert!(larger.can_hold(&original));
+        }
+    }
+    // ANCHOR_END: stretch_kani_fixed
+
+    // Currently causes Kani timeout
+    #[kani::proof]
+    pub fn stretched_rectangle_can_hold_original_fixed_u64() {
+        let original = Rectangle { width: kani::any(), height: kani::any() };
+        let factor = kani::any();
+        kani::assume(0 != original.width);
+        kani::assume(0 != original.height);
+        kani::assume(1 < factor);
+        if let Some(larger) = original.stretch(factor) {
+            assert!(larger.can_hold(&original));
+        }
+    }
+}

tests/cargo-kani/rectangle-example/stretched_rectangle_can_hold_original.expected

@@ -0,0 +1 @@
+VERIFICATION:- FAILED

tests/cargo-kani/rectangle-example/stretched_rectangle_can_hold_original_fixed.expected

@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL