[Draft] kani-cov: A coverage tool for Kani

Cargo.lock

@@ -139,6 +139,15 @@ dependencies = [
  "thiserror",
 ]
 
+[[package]]
+name = "cc"
+version = "1.1.15"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "57b6a275aa2903740dc87da01c62040406b8812552e97129a63ea8850a17c6e6"
+dependencies = [
+ "shlex",
+]
+
 [[package]]
 name = "cfg-if"
 version = "1.0.0"
@@ -489,6 +498,20 @@ dependencies = [
  "tracing-tree",
 ]
 
+[[package]]
+name = "kani-cov"
+version = "0.1.0"
+dependencies = [
+ "anyhow",
+ "clap",
+ "console",
+ "serde",
+ "serde_derive",
+ "serde_json",
+ "tree-sitter",
+ "tree-sitter-rust",
+]
+
 [[package]]
 name = "kani-driver"
 version = "0.55.0"
@@ -1088,6 +1111,12 @@ version = "1.1.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "24188a676b6ae68c3b2cb3a01be17fbf7240ce009799bb56d5b1409051e78fde"
 
+[[package]]
+name = "shlex"
+version = "1.3.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0fda2ff0d084019ba4d7c6f371c95d8fd75ce3524c3cb8fb653a3023f6323e64"
+
 [[package]]
 name = "smallvec"
 version = "1.13.2"
@@ -1343,6 +1372,34 @@ dependencies = [
  "tracing-subscriber",
 ]
 
+[[package]]
+name = "tree-sitter"
+version = "0.23.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "20f4cd3642c47a85052a887d86704f4eac272969f61b686bdd3f772122aabaff"
+dependencies = [
+ "cc",
+ "regex",
+ "regex-syntax 0.8.4",
+ "tree-sitter-language",
+]
+
+[[package]]
+name = "tree-sitter-language"
+version = "0.1.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2545046bd1473dac6c626659cc2567c6c0ff302fc8b84a56c4243378276f7f57"
+
+[[package]]
+name = "tree-sitter-rust"
+version = "0.21.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "277690f420bf90741dea984f3da038ace46c4fe6047cba57a66822226cde1c93"
+dependencies = [
+ "cc",
+ "tree-sitter",
+]
+
 [[package]]
 name = "unicode-ident"
 version = "1.0.13"

Cargo.toml

@@ -40,6 +40,7 @@ members = [
  "library/std",
  "tools/compiletest",
  "tools/build-kani",
+ "tools/kani-cov",
  "tools/scanner",
  "kani-driver",
  "kani-compiler",

tests/coverage/abort/expected

@@ -1,13 +1,21 @@
-Source-based code coverage results:
-
-main.rs (main)\
- * 9:1 - 9:11 COVERED\
- * 10:9 - 10:10 COVERED\
- * 10:14 - 10:18 COVERED\
- * 13:13 - 13:29 COVERED\
- * 14:10 - 15:18 COVERED\
- * 17:13 - 17:29 UNCOVERED\
- * 18:10 - 18:11 COVERED\
- * 20:5 - 20:12 UNCOVERED\
- * 20:20 - 20:41 UNCOVERED\
- * 21:1 - 21:2 UNCOVERED
+ 1| | // Copyright Kani Contributors\
+ 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+ 3| | \
+ 4| | //! Test that the abort() function is respected and nothing beyond it will execute.\
+ 5| | \
+ 6| | use std::process;\
+ 7| | \
+ 8| | #[kani::proof]\
+ 9| 2| fn main() {\
+ 10| 2| for i in 0..4 {\
+ 11| | if i == 1 {\
+ 12| | // This comes first and it should be reachable.\
+ 13| 2| process::abort();\
+ 14| 2| }\
+ 15| 2| if i == 2 {\
+ 16| | // This should never happen.\
+ 17| 0| process::exit(1);\
+ 18| 2| }\
+ 19| | }\
+ 20| 0| ```assert!'''(false, ```"This is unreachable"''');\
+ 21| | }\

tests/coverage/assert/expected

@@ -1,9 +1,18 @@
-Source-based code coverage results:
-
-test.rs (foo)
- * 5:1 - 7:13 COVERED\
- * 9:9 - 10:17 COVERED\
- * 10:18 - 13:10 UNCOVERED\
- * 13:10 - 13:11 UNCOVERED\
- * 14:12 - 17:6 COVERED\
- * 18:1 - 18:2 COVERED
+ 1| | // Copyright Kani Contributors\
+ 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+ 3| | \
+ 4| | #[kani::proof]\
+ 5| 2| fn foo() {\
+ 6| 2| let x: i32 = kani::any();\
+ 7| 2| if x > 5 {\
+ 8| | // fails\
+ 9| 2| assert!(x < 4);\
+ 10| 2| if x < 3 ```{'''\
+ 11| 0| ``` // unreachable'''\
+ 12| 0| ``` assert!(x == 2);'''\
+ 13| 0| ``` }'''\
+ 14| 2| } else {\
+ 15| 2| // passes\
+ 16| 2| assert!(x <= 5);\
+ 17| 2| }\
+ 18| | }\

tests/coverage/assert_eq/expected

@@ -1,8 +1,11 @@
-Source-based code coverage results:
-
-test.rs (main)\
- * 5:1 - 6:29 COVERED\
- * 7:25 - 7:27 COVERED\
- * 7:37 - 7:39 COVERED\
- * 8:15 - 10:6 UNCOVERED\
- * 10:6 - 10:7 COVERED
+ 1| | // Copyright Kani Contributors\
+ 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+ 3| | \
+ 4| | #[kani::proof]\
+ 5| 2| fn main() {\
+ 6| 2| let x: i32 = kani::any();\
+ 7| 2| let y = if x > 10 { 15 } else { 33 };\
+ 8| 0| if y > 50 ```{'''\
+ 9| 0| ``` assert_eq!(y, 55);'''\
+ 10| 2| ``` }'''\
+ 11| | }\

tests/coverage/assert_ne/expected

@@ -1,9 +1,14 @@
-Source-based code coverage results:
-
-test.rs (main)\
- * 5:1 - 7:13 COVERED\
- * 8:13 - 10:18 COVERED\
- * 10:19 - 12:10 UNCOVERED\
- * 12:10 - 12:11 COVERED\
- * 13:6 - 13:7 COVERED\
- * 14:1 - 14:2 COVERED
+ 1| | // Copyright Kani Contributors\
+ 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+ 3| | \
+ 4| | #[kani::proof]\
+ 5| 2| fn main() {\
+ 6| 2| let x: u32 = kani::any();\
+ 7| 2| if x > 0 {\
+ 8| 2| let y = x / 2;\
+ 9| 2| // y is strictly less than x\
+ 10| 2| if y == x ```{'''\
+ 11| 0| ``` assert_ne!(y, 1);'''\
+ 12| 2| ``` }'''\
+ 13| 2| }\
+ 14| | }\

tests/coverage/break/expected

@@ -1,13 +1,19 @@
-Source-based code coverage results:
-
-main.rs (find_positive)\
- * 4:1 - 4:47 COVERED\
- * 5:10 - 5:13 COVERED\
- * 5:17 - 5:21 COVERED\
- * 7:20 - 7:29 COVERED\
- * 8:10 - 8:11 COVERED\
- * 11:5 - 11:9 UNCOVERED\
- * 12:1 - 12:2 COVERED
-
-main.rs (main)\
- * 15:1 - 19:2 COVERED
+ 1| | // Copyright Kani Contributors\
+ 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+ 3| | \
+ 4| 2| fn find_positive(nums: &[i32]) -> Option<i32> {\
+ 5| 2| for &num in nums {\
+ 6| | if num > 0 {\
+ 7| 2| return Some(num);\
+ 8| 2| }\
+ 9| | }\
+ 10| | // `None` is unreachable because there is at least one positive number.\
+ 11| 0| None\
+ 12| | }\
+ 13| | \
+ 14| | #[kani::proof]\
+ 15| 2| fn main() {\
+ 16| 2| let numbers = [-3, -1, 0, 2, 4];\
+ 17| 2| let result = find_positive(&numbers);\
+ 18| 2| assert_eq!(result, Some(2));\
+ 19| | }\

tests/coverage/compare/expected

@@ -1,11 +1,16 @@
-Source-based code coverage results:
-
-main.rs (compare)\
- * 4:1 - 6:14 COVERED\
- * 6:17 - 6:18 COVERED\
- * 6:28 - 6:29 UNCOVERED
-
-main.rs (main)\
- * 10:1 - 13:14 COVERED\
- * 13:15 - 15:6 COVERED\
- * 15:6 - 15:7 COVERED
+ 1| | // Copyright Kani Contributors\
+ 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+ 3| | \
+ 4| 2| fn compare(x: u16, y: u16) -> u16 {\
+ 5| 2| // The case where `x < y` isn't possible so its region is `UNCOVERED`\
+ 6| 2| if x >= y { 1 } else { 0 }\
+ 7| | }\
+ 8| | \
+ 9| | #[kani::proof]\
+ 10| 2| fn main() {\
+ 11| 2| let x: u16 = kani::any();\
+ 12| 2| let y: u16 = kani::any();\
+ 13| 2| if x >= y {\
+ 14| 2| compare(x, y);\
+ 15| 2| }\
+ 16| | }\

tests/coverage/contradiction/expected

@@ -1,9 +1,14 @@
-Source-based code coverage results:
-
-main.rs (contradiction)\
- * 4:1 - 7:13 COVERED\
- * 8:12 - 8:17 COVERED\
- * 8:18 - 10:10 UNCOVERED\
- * 10:10 - 10:11 COVERED\
- * 11:12 - 13:6 COVERED\
- * 14:1 - 14:2 COVERED
+ 1| | // Copyright Kani Contributors\
+ 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+ 3| | #[kani::proof]\
+ 4| 2| fn contradiction() {\
+ 5| 2| let x: u8 = kani::any();\
+ 6| 2| let mut y: u8 = 0;\
+ 7| 2| if x > 5 {\
+ 8| 2| if x < 2 ```{'''\
+ 9| 0| ``` y = x;'''\
+ 10| 2| ``` }'''\
+ 11| 2| } else {\
+ 12| 2| assert!(x < 10);\
+ 13| 2| }\
+ 14| | }\

tests/coverage/debug-assert/expected

@@ -1,10 +1,15 @@
-Source-based code coverage results:
-
-main.rs (main)\
- * 10:1 - 10:11 COVERED\
- * 11:9 - 11:10 COVERED\
- * 11:14 - 11:18 COVERED\
- * 12:30 - 12:71 UNCOVERED\
- * 13:9 - 13:23 UNCOVERED\
- * 13:25 - 13:53 UNCOVERED\
- * 15:1 - 15:2 UNCOVERED
+ 1| | // Copyright Kani Contributors\
+ 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+ 3| | \
+ 4| | //! This test checks that the regions after the `debug_assert` macro are\
+ 5| | //! `UNCOVERED`. In fact, for this example, the region associated to `"This\
+ 6| | //! should fail and stop the execution"` is also `UNCOVERED` because the macro\
+ 7| | //! calls span two regions each.\
+ 8| | \
+ 9| | #[kani::proof]\
+ 10| 2| fn main() {\
+ 11| 2| for i in 0..4 {\
+ 12| 0| debug_assert!(i > 0, ```"This should fail and stop the execution"''');\
+ 13| 0| ```assert!(i == 0''', ```"This should be unreachable"''');\
+ 14| | }\
+ 15| | }\

tests/coverage/div-zero/expected

@@ -1,9 +1,11 @@
-Source-based code coverage results:
-
-test.rs (div)\
- * 4:1 - 5:14 COVERED\
- * 5:17 - 5:22 COVERED\
- * 5:32 - 5:33 UNCOVERED
-
-test.rs (main)\
- * 9:1 - 11:2 COVERED
+ 1| | // Copyright Kani Contributors\
+ 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+ 3| | \
+ 4| 2| fn div(x: u16, y: u16) -> u16 {\
+ 5| 2| if y != 0 { x / y } else { 0 }\
+ 6| | }\
+ 7| | \
+ 8| | #[kani::proof]\
+ 9| 2| fn main() {\
+ 10| 2| div(11, 3);\
+ 11| | }\

tests/coverage/early-return/expected

@@ -1,12 +1,19 @@
-Source-based code coverage results:
-
-main.rs (find_index)\
- * 4:1 - 4:59 COVERED\
- * 5:10 - 5:21 COVERED\
- * 7:20 - 7:31 COVERED\
- * 8:10 - 8:11 COVERED\
- * 10:5 - 10:9 UNCOVERED\
- * 11:1 - 11:2 COVERED
-
-main.rs (main)\
- * 14:1 - 19:2 COVERED
+ 1| | // Copyright Kani Contributors\
+ 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+ 3| | \
+ 4| 2| fn find_index(nums: &[i32], target: i32) -> Option<usize> {\
+ 5| 2| for (index, &num) in nums.iter().enumerate() {\
+ 6| | if num == target {\
+ 7| 2| return Some(index);\
+ 8| 2| }\
+ 9| | }\
+ 10| 0| None\
+ 11| | }\
+ 12| | \
+ 13| | #[kani::proof]\
+ 14| 2| fn main() {\
+ 15| 2| let numbers = [10, 20, 30, 40, 50];\
+ 16| 2| let target = 30;\
+ 17| 2| let result = find_index(&numbers, target);\
+ 18| 2| assert_eq!(result, Some(2));\
+ 19| | }\