kani-cov: A coverage tool for Kani

Cargo.lock

@@ -769,6 +769,20 @@ dependencies = [
  "tracing-tree 0.4.0",
 ]
 
+[[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.56.0"
@@ -1811,6 +1825,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.5",
+ "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 = "typed-arena"
 version = "2.0.2"

Cargo.toml

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

scripts/kani-regression.sh

@@ -70,6 +70,9 @@ echo "--- Compiletest configuration"
 cargo run -p compiletest --quiet -- --suite kani --mode cargo-kani --dry-run --verbose
 echo "-----------------------------"
 
+# Build `kani-cov`
+cargo build -p kani-cov
+
 # Extract testing suite information and run compiletest
 for testp in "${TESTS[@]}"; do
   testl=($testp)

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|    1| fn main() {\
+  10|    1|     for i in 0..4 {\
+  11|     |         if i == 1 {\
+  12|     |             // This comes first and it should be reachable.\
+  13|    1|             process::abort();\
+  14|    1|         }\
+  15|    1|         if i == 2 {\
+  16|     |             // This should never happen.\
+  17|    0|             ```process::exit(1)''';\
+  18|    1|         } \
+  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|    1| fn foo() {\
+   6|    1|     let x: i32 = kani::any();\
+   7|    1|     if x > 5 {\
+   8|     |         // fails\
+   9|    1|         assert!(x < 4);\
+  10|    1|         if x < 3 ```{'''\
+  11|    0| ```            // unreachable'''\
+  12|    0| ```            assert!(x == 2);'''\
+  13|    0| ```        }'''``` '''\
+  14|    1|     } else {\
+  15|    1|         // passes\
+  16|    1|         assert!(x <= 5);\
+  17|    1|     }\
+  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|    1| fn main() {\
+   6|    1|     let x: i32 = kani::any();\
+   7|    1|     let y = if x > 10 { 15 } else { 33 };\
+   8|    0|     if y > 50 ```{'''\
+   9|    0| ```        assert_eq!(y, 55);'''\
+  10|    1| ```    }'''\
+  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|    1| fn main() {\
+   6|    1|     let x: u32 = kani::any();\
+   7|    1|     if x > 0 {\
+   8|    1|         let y = x / 2;\
+   9|    1|         // y is strictly less than x\
+  10|    1|         if y == x ```{'''\
+  11|    0| ```            assert_ne!(y, 1);'''\
+  12|    1| ```        }'''\
+  13|    1|     }\
+  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|    1| fn find_positive(nums: &[i32]) -> Option<i32> {\
+   5|    1|     for &num in nums {\
+   6|     |         if num > 0 {\
+   7|    1|             return Some(num);\
+   8|    1|         } \
+   9|     |     }\
+  10|     |     // `None` is unreachable because there is at least one positive number.\
+  11|    0|     ```None'''\
+  12|     | }\
+  13|     | \
+  14|     | #[kani::proof]\
+  15|    1| fn main() {\
+  16|    1|     let numbers = [-3, -1, 0, 2, 4];\
+  17|    1|     let result = find_positive(&numbers);\
+  18|    1|     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|    1| fn compare(x: u16, y: u16) -> u16 {\
+   5|    1|     // The case where `x < y` isn't possible so its region is `UNCOVERED`\
+   6|    1|     if x >= y { 1 } else { ```0''' }\
+   7|     | }\
+   8|     | \
+   9|     | #[kani::proof]\
+  10|    1| fn main() {\
+  11|    1|     let x: u16 = kani::any();\
+  12|    1|     let y: u16 = kani::any();\
+  13|    1|     if x >= y {\
+  14|    1|         compare(x, y);\
+  15|    1|     } \
+  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|    1| fn contradiction() {\
+   5|    1|     let x: u8 = kani::any();\
+   6|    1|     let mut y: u8 = 0;\
+   7|    1|     if x > 5 {\
+   8|    1|         if x < 2 ```{'''\
+   9|    0| ```            y = x;'''\
+  10|    1| ```        }'''\
+  11|    1|     } else {\
+  12|    1|         assert!(x < 10);\
+  13|    1|     }\
+  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|    1| fn main() {\
+  11|    1|     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|    1| fn div(x: u16, y: u16) -> u16 {\
+   5|    1|     if y != 0 { x / y } else { ```0''' }\
+   6|     | }\
+   7|     | \
+   8|     | #[kani::proof]\
+   9|    1| fn main() {\
+  10|    1|     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|    1| fn find_index(nums: &[i32], target: i32) -> Option<usize> {\
+   5|    1|     for (index, &num) in nums.iter().enumerate() {\
+   6|     |         if num == target {\
+   7|    1|             return Some(index);\
+   8|    1|         } \
+   9|     |     }\
+  10|    0|     ```None'''\
+  11|     | }\
+  12|     | \
+  13|     | #[kani::proof]\
+  14|    1| fn main() {\
+  15|    1|     let numbers = [10, 20, 30, 40, 50];\
+  16|    1|     let target = 30;\
+  17|    1|     let result = find_index(&numbers, target);\
+  18|    1|     assert_eq!(result, Some(2));\
+  19|     | }\

tests/coverage/if-statement-multi/expected

@@ -1,11 +1,26 @@
-Source-based code coverage results:
-
-test.rs (main)\
- * 21:1 - 26:2 COVERED
-
-test.rs (test_cov)\
- * 16:1 - 17:15 COVERED\
- * 17:19 - 17:28 UNCOVERED\
- * 17:31 - 17:35 COVERED\
- * 17:45 - 17:50 UNCOVERED\
- * 18:1 - 18:2 COVERED
+   1|     | // Copyright Kani Contributors\
+   2|     | // SPDX-License-Identifier: Apache-2.0 OR MIT\
+   3|     | // kani-flags: --coverage -Zsource-coverage\
+   4|     | \
+   5|     | //! Checks that we are covering all regions except\
+   6|     | //!  * the `val == 42` condition\
+   7|     | //!  * the `false` branch\
+   8|     | //!\
+   9|     | //! No coverage information is shown for `_other_function` because it's sliced\
+  10|     | //! off: <https://github.com/model-checking/kani/issues/3445>\
+  11|     | \
+  12|    0| ```fn _other_function() {'''\
+  13|    0| ```    println!("Hello, world!");'''\
+  14|    0| ```}'''\
+  15|     | \
+  16|    1| fn test_cov(val: u32) -> bool {\
+  17|    1|     if val < 3 || ```val == 42''' { true } else { ```false''' }\
+  18|     | }\
+  19|     | \
+  20|     | #[cfg_attr(kani, kani::proof)]\
+  21|    1| fn main() {\
+  22|    1|     let test1 = test_cov(1);\
+  23|    1|     let test2 = test_cov(2);\
+  24|    1|     assert!(test1);\
+  25|    1|     assert!(test2);\
+  26|     | }\