kani-cov: A coverage tool for Kani

Cargo.lock

@@ -977,9 +977,9 @@ dependencies = [
 
 [[package]]
 name = "serde_json"
-version = "1.0.114"
+version = "1.0.115"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c5f09b1bd632ef549eaa9f60a1f8de742bdbc698e6cee2095fc84dde5f549ae0"
+checksum = "12dc5c46daa8e9fdf4f5e71b6cf9a53f2487da0e86e55808e2d35539666497dd"
 dependencies = [
  "itoa",
  "ryu",
@@ -1317,6 +1317,17 @@ version = "0.9.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "49874b5167b65d7193b8aba1567f5c7d93d001cafc34600cee003eda787e483f"
 
+[[package]]
+name = "visualize_coverage"
+version = "0.1.0"
+dependencies = [
+ "anyhow",
+ "console",
+ "serde",
+ "serde_derive",
+ "serde_json",
+]
+
 [[package]]
 name = "wait-timeout"
 version = "0.2.0"

Cargo.toml

@@ -41,6 +41,7 @@ members = [
   "tools/bookrunner",
   "tools/compiletest",
   "tools/build-kani",
+  "tools/kanicov",
   "kani-driver",
   "kani-compiler",
   "kani_metadata",

tools/kanicov/Cargo.toml

@@ -0,0 +1,13 @@
+[package]
+name = "visualize_coverage"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+anyhow = "1.0.81"
+console = "0.15.8"
+serde = "1.0.197"
+serde_derive = "1.0.197"
+serde_json = "1.0.115"

tools/kanicov/src/coverage.rs

@@ -0,0 +1,124 @@
+use anyhow::Result;
+use console::style;
+use serde_derive::{Deserialize, Serialize};
+use std::fmt::{self, Write};
+use std::{collections::BTreeMap, fmt::Display};
+
+#[derive(Copy, Clone, Debug, Serialize, Deserialize, PartialEq, Eq)]
+#[serde(rename_all = "UPPERCASE")]
+pub enum CheckStatus {
+    Failure,
+    Covered,   // for `code_coverage` properties only
+    Satisfied, // for `cover` properties only
+    Success,
+    Undetermined,
+    Unreachable,
+    Uncovered,     // for `code_coverage` properties only
+    Unsatisfiable, // for `cover` properties only
+}
+
+#[derive(Clone, Debug, Serialize, Deserialize)]
+pub struct CoverageResults {
+    pub data: BTreeMap<String, Vec<CoverageCheck>>,
+}
+
+impl CoverageResults {
+    pub fn new(data: BTreeMap<String, Vec<CoverageCheck>>) -> Self {
+        Self { data }
+    }
+}
+pub fn fmt_coverage_results(coverage_results: &CoverageResults) -> Result<String> {
+    let mut fmt_string = String::new();
+    for (file, checks) in coverage_results.data.iter() {
+        let mut checks_by_function: BTreeMap<String, Vec<CoverageCheck>> = BTreeMap::new();
+
+        // // Group checks by function
+        for check in checks {
+            // Insert the check into the vector corresponding to its function
+            checks_by_function
+                .entry(check.function.clone())
+                .or_insert_with(Vec::new)
+                .push(check.clone());
+        }
+
+        for (function, checks) in checks_by_function {
+            writeln!(fmt_string, "{file} ({function})")?;
+            let mut sorted_checks: Vec<CoverageCheck> = checks.to_vec();
+            sorted_checks.sort_by(|a, b| a.region.start.cmp(&b.region.start));
+            for check in sorted_checks.iter() {
+                writeln!(fmt_string, " * {} {}", check.region, check.status)?;
+            }
+            writeln!(fmt_string, "")?;
+        }
+    }
+    Ok(fmt_string)
+}
+
+#[derive(Debug, Clone, Serialize, Deserialize)]
+pub struct CoverageCheck {
+    pub function: String,
+    term: CoverageTerm,
+    pub region: CoverageRegion,
+    status: CheckStatus,
+}
+
+impl CoverageCheck {
+    pub fn new(
+        function: String,
+        term: CoverageTerm,
+        region: CoverageRegion,
+        status: CheckStatus,
+    ) -> Self {
+        Self { function, term, region, status }
+    }
+
+    pub fn is_covered(&self) -> bool {
+        self.status == CheckStatus::Covered
+    }
+}
+
+#[derive(Debug, Clone, Eq, PartialEq, PartialOrd, Ord, Serialize, Deserialize)]
+pub struct CoverageRegion {
+    pub file: String,
+    pub start: (u32, u32),
+    pub end: (u32, u32),
+}
+
+impl Display for CoverageRegion {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        write!(f, "{}:{} - {}:{}", self.start.0, self.start.1, self.end.0, self.end.1)
+    }
+}
+
+impl CoverageRegion {
+    pub fn from_str(str: String) -> Self {
+        let str_splits: Vec<&str> = str.split([':', '-']).map(|s| s.trim()).collect();
+        assert_eq!(str_splits.len(), 5, "{str:?}");
+        let file = str_splits[0].to_string();
+        let start = (str_splits[1].parse().unwrap(), str_splits[2].parse().unwrap());
+        let end = (str_splits[3].parse().unwrap(), str_splits[4].parse().unwrap());
+        Self { file, start, end }
+    }
+}
+
+#[derive(Debug, Clone, Serialize, Deserialize)]
+pub enum CoverageTerm {
+    Counter(u32),
+    Expression(u32),
+}
+
+impl std::fmt::Display for CheckStatus {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        let check_str = match self {
+            CheckStatus::Satisfied => style("SATISFIED").green(),
+            CheckStatus::Success => style("SUCCESS").green(),
+            CheckStatus::Covered => style("COVERED").green(),
+            CheckStatus::Uncovered => style("UNCOVERED").red(),
+            CheckStatus::Failure => style("FAILURE").red(),
+            CheckStatus::Unreachable => style("UNREACHABLE").yellow(),
+            CheckStatus::Undetermined => style("UNDETERMINED").yellow(),
+            CheckStatus::Unsatisfiable => style("UNSATISFIABLE").yellow(),
+        };
+        write!(f, "{check_str}")
+    }
+}

tools/kanicov/src/main.rs

@@ -0,0 +1,113 @@
+mod coverage;
+use std::fs::File;
+use std::io::Read;
+use std::io::{BufRead, BufReader};
+use std::path::PathBuf;
+
+use crate::coverage::CoverageResults;
+use anyhow::{Context, Result};
+use coverage::CoverageCheck;
+
+fn main() -> Result<()> {
+    let args = std::env::args().collect::<Vec<_>>();
+
+    let file_path = args.get(1).context("kanicov file not specified")?;
+    let mut file = File::open(file_path)?;
+    let mut contents = String::new();
+    file.read_to_string(&mut contents)?;
+    let path_to_root = cargo_root_dir(file_path.into());
+    let cov_results: CoverageResults = serde_json::from_str(&contents)?;
+    let visual_results = visualize_coverage_results(&cov_results, path_to_root.unwrap())
+        .expect("error: couldn't format coverage results");
+    println!("{visual_results}");
+    Ok(())
+}
+
+fn visualize_coverage_results(cov_results: &CoverageResults, root_path: PathBuf) -> Result<String> {
+    let mut formatted_output = String::new();
+    let cov_data = &cov_results.data;
+
+    for file in cov_data.keys() {
+        let file_path = root_path.join(file);
+        let file_handle = File::open(file_path)?;
+        let reader = BufReader::new(file_handle);
+
+        let checks = cov_data.get(file).unwrap().to_vec();
+        let mut must_highlight = false;
+
+        for (idx, line) in reader.lines().enumerate() {
+            let line = format!("{}\n", line.unwrap());
+
+            let cur_idx = idx + 1;
+            let line_checks: Vec<&CoverageCheck> = checks
+                .iter()
+                .filter(|c| {
+                    c.is_covered()
+                        && (cur_idx == c.region.start.0 as usize
+                            || cur_idx == c.region.end.0 as usize)
+                })
+                .collect();
+            let new_line = if line_checks.is_empty() {
+                if must_highlight {
+                    insert_escapes(&line, vec![(0, true), (line.len() - 1, false)])
+                } else {
+                    line
+                }
+            } else {
+                let mut markers = vec![];
+                if must_highlight {
+                    markers.push((0, true))
+                };
+
+                for check in line_checks {
+                    let start_line = check.region.start.0 as usize;
+                    let start_column = (check.region.start.1 - 1u32) as usize;
+                    let end_line = check.region.end.0 as usize;
+                    let end_column = (check.region.end.1 - 1u32) as usize;
+                    if start_line == cur_idx {
+                        markers.push((start_column, true))
+                    }
+                    if end_line == cur_idx {
+                        markers.push((end_column, false))
+                    }
+                }
+
+                if markers.last().unwrap().1 {
+                    must_highlight = true;
+                    markers.push((line.len() - 1, false))
+                } else {
+                    must_highlight = false;
+                }
+                println!("{:?}", markers);
+                insert_escapes(&line, markers)
+            };
+            formatted_output.push_str(&new_line);
+        }
+    }
+    Ok(formatted_output)
+}
+
+fn cargo_root_dir(filepath: PathBuf) -> Option<PathBuf> {
+    let mut cargo_root_path = filepath.clone();
+    while !cargo_root_path.join("Cargo.toml").exists() {
+        let pop_result = cargo_root_path.pop();
+        if !pop_result {
+            return None;
+        }
+    }
+    Some(cargo_root_path)
+}
+
+fn insert_escapes(str: &String, markers: Vec<(usize, bool)>) -> String {
+    let mut new_str = str.clone();
+    let mut offset = 0;
+
+    let sym_markers = markers.iter().map(|(i, b)| (i, if *b { "\x1b[42m" } else { "\x1b[0m" }));
+    // let sym_markers = markers.iter().map(|(i, b)| (i, if *b { "```" } else { "'''" }));
+    for (i, b) in sym_markers {
+        println!("{}", i + offset);
+        new_str.insert_str(i + offset, b);
+        offset = offset + b.bytes().len();
+    }
+    new_str
+}