Add coverage test suite

scripts/kani-regression.sh

@@ -38,6 +38,7 @@ cargo test -p kani_metadata
 # Declare testing suite information (suite and mode)
 TESTS=(
     "script-based-pre exec"
+    "coverage coverage-based"
     "kani kani"
     "expected expected"
     "ui expected"

tests/coverage/reachable/assert-false/expected

@@ -0,0 +1,2 @@
+22, SATISFIED
+27, SATISFIED

tests/coverage/reachable/assert-false/main.rs

@@ -0,0 +1,36 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Check the location of the assert statement when using assert!(false);
+// This currently requires the old format since the new format doesn't include
+// line numbers https://github.com/model-checking/kani/issues/918
+// Also disable reachability checks because they add annotations to each
+// assert's description which would be visible with the old output format
+
+fn any_bool() -> bool {
+    kani::any()
+}
+
+#[kani::proof]
+fn main() {
+    if any_bool() {
+        assert!(false);
+    }
+
+    if any_bool() {
+        let s = "Fail with custom runtime message";
+        kani::cover!();
+        assert!(false, "{}", s);
+    }
+
+    if any_bool() {
+        kani::cover!();
+        assert!(false, "Fail with custom static message");
+    }
+}
+
+#[inline(always)]
+#[track_caller]
+fn check_caller(b: bool) {
+    assert!(b);
+}

tests/coverage/reachable/assert/reachable_fail/expected

@@ -0,0 +1 @@
+8, SATISFIED

tests/coverage/reachable/assert/reachable_fail/test.rs

@@ -0,0 +1,11 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#[kani::proof]
+fn main() {
+    let x = 5;
+    if kani::any() {
+        kani::cover!();
+        assert!(x != 5);
+    }
+}

tests/coverage/reachable/assert/reachable_pass/expected

@@ -0,0 +1 @@
+8, SATISFIED

tests/coverage/reachable/assert/reachable_pass/test.rs

@@ -0,0 +1,11 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#[kani::proof]
+fn main() {
+    let x = 5;
+    if x > 3 {
+        kani::cover!();
+        assert!(x > 4);
+    }
+}

tests/coverage/reachable/bounds/reachable_fail/expected

@@ -0,0 +1 @@
+10, SATISFIED

tests/coverage/reachable/bounds/reachable_fail/test.rs

@@ -0,0 +1,17 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This test checks that kani injects a reachability check for
+// index-out-of-bounds checks and that it reports ones that are unreachable.
+// The check in this test is reachable and doesn't hold, so should be reported
+// as FAILURE
+
+fn get(s: &[i16], index: usize) -> i16 {
+    kani::cover!();
+    s[index]
+}
+
+#[kani::proof]
+fn main() {
+    get(&[7, -83, 19], 15);
+}

tests/coverage/reachable/bounds/reachable_pass/expected

@@ -0,0 +1 @@
+10, SATISFIED

tests/coverage/reachable/bounds/reachable_pass/test.rs

@@ -0,0 +1,20 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This test checks that kani injects a reachability check for
+// index-out-of-bounds checks and that it reports ones that are unreachable.
+// The check in this test is reachable, so should be reported as SUCCESS
+
+fn get(s: &[i16], index: usize) -> i16 {
+    if index < s.len() {
+        kani::cover!();
+        s[index]
+    } else {
+        -1
+    }
+}
+
+#[kani::proof]
+fn main() {
+    get(&[7, -83, 19], 2);
+}

tests/coverage/reachable/debug-assert-eq/reachable_fail/expected

@@ -0,0 +1 @@
+11, SATISFIED

tests/coverage/reachable/debug-assert-eq/reachable_fail/test.rs

@@ -0,0 +1,19 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This test checks that kani injects a reachability check for debug_assert_eq
+// macro and that it reports ones that are unreachable.
+// The check in this test is reachable and does not hold, so should be reported
+// as FAILURE
+
+fn check(x: i32) {
+    if x > 5 {
+        kani::cover!();
+        debug_assert_eq!(x, 10);
+    }
+}
+
+#[kani::proof]
+fn main() {
+    check(7);
+}

tests/coverage/reachable/debug-assert-eq/reachable_pass/expected

@@ -0,0 +1 @@
+10, SATISFIED

tests/coverage/reachable/debug-assert-eq/reachable_pass/test.rs

@@ -0,0 +1,18 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This test checks that kani injects a reachability check for debug_assert_eq
+// macro and that it reports ones that are unreachable.
+// The check in this test is reachable, so should be reported as SUCCESS
+
+fn check(x: i32) {
+    if x > 5 {
+        kani::cover!();
+        debug_assert_eq!(x, 10);
+    }
+}
+
+#[kani::proof]
+fn main() {
+    check(10);
+}

tests/coverage/reachable/debug-assert-ne/reachable_fail/expected

@@ -0,0 +1 @@
+11, SATISFIED

tests/coverage/reachable/debug-assert-ne/reachable_fail/test.rs

@@ -0,0 +1,19 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This test checks that kani injects a reachability check for debug_assert_ne
+// macro and that it reports ones that are unreachable.
+// The check in this test is reachable and does not hold, so should be reported
+// as FAILURE
+
+fn check(x: i32) {
+    if x > 5 {
+        kani::cover!();
+        debug_assert_ne!(x, 17);
+    }
+}
+
+#[kani::proof]
+fn main() {
+    check(17);
+}

tests/coverage/reachable/debug-assert-ne/reachable_pass/expected

@@ -0,0 +1 @@
+10, SATISFIED

tests/coverage/reachable/debug-assert-ne/reachable_pass/test.rs

@@ -0,0 +1,18 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This test checks that kani injects a reachability check for debug_assert_ne
+// macro and that it reports ones that are unreachable.
+// The check in this test is reachable, so should be reported as SUCCESS
+
+fn check(x: i32) {
+    if x > 5 {
+        kani::cover!();
+        debug_assert_ne!(x, 17);
+    }
+}
+
+#[kani::proof]
+fn main() {
+    check(10);
+}

tests/coverage/reachable/div-zero/reachable_fail/expected

@@ -0,0 +1 @@
+10, SATISFIED

tests/coverage/reachable/div-zero/reachable_fail/test.rs

@@ -0,0 +1,17 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This test checks that kani injects a reachability check for
+// divide-by-zero checks and that it reports ones that are unreachable.
+// The check in this test is reachable and doesn't hold, so should be reported
+// as FAILURE
+
+fn div(x: u16, y: u16) -> u16 {
+    kani::cover!();
+    x / y
+}
+
+#[kani::proof]
+fn main() {
+    div(678, 0);
+}

tests/coverage/reachable/div-zero/reachable_pass/expected

@@ -0,0 +1 @@
+10, SATISFIED

tests/coverage/reachable/div-zero/reachable_pass/test.rs

@@ -0,0 +1,20 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This test checks that kani injects a reachability check for
+// divide-by-zero checks and that it reports ones that are unreachable.
+// The check in this test is reachable, so should be reported as SUCCESS
+
+fn div(x: u16, y: u16) -> u16 {
+    if y != 0 {
+        kani::cover!();
+        x / y
+    } else {
+        0
+    }
+}
+
+#[kani::proof]
+fn main() {
+    div(11, 3);
+}

tests/coverage/reachable/overflow-neg/reachable_fail/expected

@@ -0,0 +1 @@
+10, SATISFIED

tests/coverage/reachable/overflow-neg/reachable_fail/test.rs

@@ -0,0 +1,17 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This test checks that kani injects a reachability check for negation
+// overflow checks and that it reports ones that are unreachable
+// The negation overflow check in this test is reachable and doesn't hold, so
+// should be reported as FAILURE
+
+fn negate(x: i32) -> i32 {
+    kani::cover!();
+    -x
+}
+
+#[kani::proof]
+fn main() {
+    negate(std::i32::MIN);
+}

tests/coverage/reachable/overflow-neg/reachable_pass/expected

@@ -0,0 +1 @@
+11, SATISFIED

tests/coverage/reachable/overflow-neg/reachable_pass/test.rs

@@ -0,0 +1,21 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This test checks that kani injects a reachability check for negation
+// overflow checks and that it reports ones that are unreachable
+// The negation overflow check in this test is reachable, so should be
+// reported as SUCCESS
+
+fn negate(x: i32) -> i32 {
+    if x != std::i32::MIN {
+        kani::cover!();
+        -x
+    } else {
+        std::i32::MAX
+    }
+}
+
+#[kani::proof]
+fn main() {
+    negate(7532);
+}

tests/coverage/reachable/overflow/reachable_fail/expected

@@ -0,0 +1 @@
+11, SATISFIED

tests/coverage/reachable/overflow/reachable_fail/test.rs

@@ -0,0 +1,22 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This test checks that kani injects a reachability check for arithmetic
+// overflow checks and that it reports ones that are unreachable.
+// The arithmetic overflow check in this test is reachable but does not hold, so
+// should be reported as FAILURE
+
+fn cond_reduce(thresh: u32, x: u32) -> u32 {
+    if x > thresh {
+        kani::cover!();
+        x - 50
+    } else {
+        x
+    }
+}
+
+#[kani::proof]
+fn main() {
+    cond_reduce(60, 70);
+    cond_reduce(40, 42);
+}

tests/coverage/reachable/overflow/reachable_pass/expected

@@ -0,0 +1 @@
+11, SATISFIED

tests/coverage/reachable/overflow/reachable_pass/test.rs

@@ -0,0 +1,24 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This test checks that kani injects a reachability check for arithmetic
+// overflow checks and that it reports ones that are unreachable.
+// The arithmetic overflow check in this test is reachable, so should be
+// reported as SUCCESS
+
+fn reduce(x: u32) -> u32 {
+    if x > 1000 {
+        kani::cover!();
+        x - 1000
+    } else {
+        x
+    }
+}
+
+#[kani::proof]
+fn main() {
+    reduce(7);
+    reduce(33);
+    reduce(728);
+    reduce(1079);
+}

tests/coverage/reachable/rem-zero/reachable_fail/expected

@@ -0,0 +1 @@
+10, SATISFIED

tests/coverage/reachable/rem-zero/reachable_fail/test.rs

@@ -0,0 +1,17 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This test checks that kani injects a reachability check for
+// remainder-by-zero checks and that it reports ones that are unreachable.
+// The check in this test is reachable and doesn't hold, so should be reported
+// as FAILURE
+
+fn rem(x: u16, y: u16) -> u16 {
+    kani::cover!();
+    x % y
+}
+
+#[kani::proof]
+fn main() {
+    rem(678, 0);
+}

tests/coverage/reachable/rem-zero/reachable_pass/expected

@@ -0,0 +1 @@
+10, SATISFIED

tests/coverage/reachable/rem-zero/reachable_pass/test.rs

@@ -0,0 +1,20 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This test checks that kani injects a reachability check for
+// remainder-by-zero checks and that it reports ones that are unreachable.
+// The check in this test is reachable, so should be reported as SUCCESS
+
+fn rem(x: u16, y: u16) -> u16 {
+    if y != 0 {
+        kani::cover!();
+        x % y
+    } else {
+        0
+    }
+}
+
+#[kani::proof]
+fn main() {
+    rem(11, 3);
+}

tests/coverage/unreachable/abort/expected

@@ -0,0 +1,3 @@
+22, UNREACHABLE
+12, SATISFIED
+17, UNREACHABLE