From c487f2a1facc54d42f95cf8fa73fc35d9a22bab9 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Wed, 3 Apr 2024 21:41:29 +0000 Subject: [PATCH 01/36] `kanicov`: A tool to visualize coverage in Kani --- Cargo.lock | 15 +++- Cargo.toml | 1 + tools/kanicov/Cargo.toml | 13 ++++ tools/kanicov/src/coverage.rs | 124 ++++++++++++++++++++++++++++++++++ tools/kanicov/src/main.rs | 113 +++++++++++++++++++++++++++++++ 5 files changed, 264 insertions(+), 2 deletions(-) create mode 100644 tools/kanicov/Cargo.toml create mode 100644 tools/kanicov/src/coverage.rs create mode 100644 tools/kanicov/src/main.rs diff --git a/Cargo.lock b/Cargo.lock index aa3c4e089392..5bb80a896589 100644 --- a/Cargo.lock +++ b/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" diff --git a/Cargo.toml b/Cargo.toml index 8d397f2b0bd4..8dc310b51eb9 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -41,6 +41,7 @@ members = [ "tools/bookrunner", "tools/compiletest", "tools/build-kani", + "tools/kanicov", "kani-driver", "kani-compiler", "kani_metadata", diff --git a/tools/kanicov/Cargo.toml b/tools/kanicov/Cargo.toml new file mode 100644 index 000000000000..e852c8d13a1b --- /dev/null +++ b/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" diff --git a/tools/kanicov/src/coverage.rs b/tools/kanicov/src/coverage.rs new file mode 100644 index 000000000000..90032c677243 --- /dev/null +++ b/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>, +} + +impl CoverageResults { + pub fn new(data: BTreeMap>) -> Self { + Self { data } + } +} +pub fn fmt_coverage_results(coverage_results: &CoverageResults) -> Result { + let mut fmt_string = String::new(); + for (file, checks) in coverage_results.data.iter() { + let mut checks_by_function: BTreeMap> = 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 = 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}") + } +} diff --git a/tools/kanicov/src/main.rs b/tools/kanicov/src/main.rs new file mode 100644 index 000000000000..48881381b54a --- /dev/null +++ b/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::>(); + + 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 { + 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 { + 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 +} From eddb3631b07b086f8e877b403b5ce146127e9198 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 9 Apr 2024 15:21:37 +0000 Subject: [PATCH 02/36] Rename and more --- Cargo.lock | 43 +++++++++++++++------ Cargo.toml | 2 +- tools/{kanicov => kani-cov}/Cargo.toml | 3 +- tools/{kanicov => kani-cov}/src/coverage.rs | 0 tools/{kanicov => kani-cov}/src/main.rs | 11 ++++++ 5 files changed, 46 insertions(+), 13 deletions(-) rename tools/{kanicov => kani-cov}/Cargo.toml (88%) rename tools/{kanicov => kani-cov}/src/coverage.rs (100%) rename tools/{kanicov => kani-cov}/src/main.rs (96%) diff --git a/Cargo.lock b/Cargo.lock index 5bb80a896589..e7d34b5e0b93 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -87,6 +87,17 @@ version = "1.0.81" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0952808a6c2afd1aa8947271f3a60f1a6763c7b912d210184c5149b5cf147247" +[[package]] +name = "atty" +version = "0.2.14" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d9b39be18770d11421cdb1b9947a45dd3f37e93092cbf377614828a319d5fee8" +dependencies = [ + "hermit-abi", + "libc", + "winapi", +] + [[package]] name = "autocfg" version = "1.1.0" @@ -398,6 +409,15 @@ version = "0.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "2304e00983f87ffb38b55b444b5e3b60a884b5d30c0fca7d82fe33449bbe55ea" +[[package]] +name = "hermit-abi" +version = "0.1.19" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "62b467343b94ba476dcb2500d242dadbb39557df889310ac77c5d99100aaac33" +dependencies = [ + "libc", +] + [[package]] name = "home" version = "0.5.9" @@ -460,6 +480,18 @@ dependencies = [ "tracing-subscriber", ] +[[package]] +name = "kani-cov" +version = "0.1.0" +dependencies = [ + "anyhow", + "atty", + "console", + "serde", + "serde_derive", + "serde_json", +] + [[package]] name = "kani-driver" version = "0.48.0" @@ -1317,17 +1349,6 @@ 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" diff --git a/Cargo.toml b/Cargo.toml index 8dc310b51eb9..5f426553dbe8 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -41,7 +41,7 @@ members = [ "tools/bookrunner", "tools/compiletest", "tools/build-kani", - "tools/kanicov", + "tools/kani-cov", "kani-driver", "kani-compiler", "kani_metadata", diff --git a/tools/kanicov/Cargo.toml b/tools/kani-cov/Cargo.toml similarity index 88% rename from tools/kanicov/Cargo.toml rename to tools/kani-cov/Cargo.toml index e852c8d13a1b..53dcfce0ef6c 100644 --- a/tools/kanicov/Cargo.toml +++ b/tools/kani-cov/Cargo.toml @@ -1,5 +1,5 @@ [package] -name = "visualize_coverage" +name = "kani-cov" version = "0.1.0" edition = "2021" @@ -7,6 +7,7 @@ edition = "2021" [dependencies] anyhow = "1.0.81" +atty = "0.2.14" console = "0.15.8" serde = "1.0.197" serde_derive = "1.0.197" diff --git a/tools/kanicov/src/coverage.rs b/tools/kani-cov/src/coverage.rs similarity index 100% rename from tools/kanicov/src/coverage.rs rename to tools/kani-cov/src/coverage.rs diff --git a/tools/kanicov/src/main.rs b/tools/kani-cov/src/main.rs similarity index 96% rename from tools/kanicov/src/main.rs rename to tools/kani-cov/src/main.rs index 48881381b54a..00ef061f8c0a 100644 --- a/tools/kanicov/src/main.rs +++ b/tools/kani-cov/src/main.rs @@ -4,10 +4,13 @@ use std::io::Read; use std::io::{BufRead, BufReader}; use std::path::PathBuf; +use atty::Stream; + use crate::coverage::CoverageResults; use anyhow::{Context, Result}; use coverage::CoverageCheck; + fn main() -> Result<()> { let args = std::env::args().collect::>(); @@ -111,3 +114,11 @@ fn insert_escapes(str: &String, markers: Vec<(usize, bool)>) -> String { } new_str } + +fn open_marker() -> String { + if atty::is(Stream::Stdout) { + "\x1b[42m".to_string() + } else { + "```".to_string() + } +} From 13c26fdaf2d9f213de6d8510df699d01553bdaa2 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 22 Aug 2024 12:59:13 +0000 Subject: [PATCH 03/36] Scaffold for `kani-cov` --- Cargo.lock | 5 ++-- tools/kani-cov/Cargo.toml | 1 + tools/kani-cov/src/args.rs | 51 ++++++++++++++++++++++++++++++++++ tools/kani-cov/src/coverage.rs | 3 ++ tools/kani-cov/src/main.rs | 38 +++++++++++++++++-------- tools/kani-cov/src/merge.rs | 14 ++++++++++ tools/kani-cov/src/report.rs | 8 ++++++ tools/kani-cov/src/summary.rs | 6 ++++ 8 files changed, 113 insertions(+), 13 deletions(-) create mode 100644 tools/kani-cov/src/args.rs create mode 100644 tools/kani-cov/src/merge.rs create mode 100644 tools/kani-cov/src/report.rs create mode 100644 tools/kani-cov/src/summary.rs diff --git a/Cargo.lock b/Cargo.lock index f5bc44bf71f0..7642eec4d09d 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -157,9 +157,9 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" [[package]] name = "clap" -version = "4.5.15" +version = "4.5.16" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "11d8838454fda655dafd3accb2b6e2bea645b9e4078abe84a22ceb947235c5cc" +checksum = "ed6719fffa43d0d87e5fd8caeab59be1554fb028cd30edc88fc4369b17971019" dependencies = [ "clap_builder", "clap_derive", @@ -485,6 +485,7 @@ version = "0.1.0" dependencies = [ "anyhow", "atty", + "clap", "console", "serde", "serde_derive", diff --git a/tools/kani-cov/Cargo.toml b/tools/kani-cov/Cargo.toml index 53dcfce0ef6c..192b69db4884 100644 --- a/tools/kani-cov/Cargo.toml +++ b/tools/kani-cov/Cargo.toml @@ -8,6 +8,7 @@ edition = "2021" [dependencies] anyhow = "1.0.81" atty = "0.2.14" +clap = { version = "4.4.11", features = ["derive"] } console = "0.15.8" serde = "1.0.197" serde_derive = "1.0.197" diff --git a/tools/kani-cov/src/args.rs b/tools/kani-cov/src/args.rs new file mode 100644 index 000000000000..d1e851fe5650 --- /dev/null +++ b/tools/kani-cov/src/args.rs @@ -0,0 +1,51 @@ + +use std::path::PathBuf; + +use anyhow::{bail, Result}; +use clap::{arg, command}; + +use crate::{merge, summary, report}; + +#[derive(Debug, clap::Subcommand)] +pub enum Subcommand { + Merge(MergeArgs), + // Summary(SummaryArgs), + // Report(ReportArgs), +} + +#[derive(Debug, clap::Parser)] +#[command( + version, + name = "kani-cov", + about = "Process coverage information from Kani", + args_override_self = true, + subcommand_negates_reqs = true, + subcommand_precedence_over_arg = true, + args_conflicts_with_subcommands = true +)] +pub struct Args { + #[command(subcommand)] + pub command: Option, +} + +#[derive(Debug, clap::Args)] +pub struct MergeArgs { + #[arg(long)] + output: Option, + #[arg(required = true)] + files: Vec, +} + +pub fn validate_args(args: &Args) -> Result<()> { + if args.command.is_none() { + bail!("subcommand needs to be specified") + } + + match args.command.as_ref().unwrap() { + Subcommand::Merge(merge_args) => merge::validate_merge_args(&merge_args)?, + // Subcommand::Summary => summary::validate_summary_args(args)?, + // Subcommand::Report => report::validate_report_args(args)?, + }; + + Ok(()) +} diff --git a/tools/kani-cov/src/coverage.rs b/tools/kani-cov/src/coverage.rs index 90032c677243..2c8cc9fda13d 100644 --- a/tools/kani-cov/src/coverage.rs +++ b/tools/kani-cov/src/coverage.rs @@ -1,3 +1,6 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + use anyhow::Result; use console::style; use serde_derive::{Deserialize, Serialize}; diff --git a/tools/kani-cov/src/main.rs b/tools/kani-cov/src/main.rs index 00ef061f8c0a..e751d6be5bc0 100644 --- a/tools/kani-cov/src/main.rs +++ b/tools/kani-cov/src/main.rs @@ -1,4 +1,11 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + mod coverage; +mod args; +mod merge; +mod summary; +mod report; use std::fs::File; use std::io::Read; use std::io::{BufRead, BufReader}; @@ -7,22 +14,31 @@ use std::path::PathBuf; use atty::Stream; use crate::coverage::CoverageResults; +use args::{Args, validate_args, Subcommand}; +use clap::Parser; use anyhow::{Context, Result}; use coverage::CoverageCheck; fn main() -> Result<()> { - let args = std::env::args().collect::>(); - - 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}"); + let args = args::Args::parse(); + + validate_args(&args)?; + + match args.command.unwrap() { + Subcommand::Merge(merge_args) => merge::merge_main(&merge_args)?, + // Subcommand::Summary => summary::summary_main()?, + // Subcommand::Report => report::report_main()?, + }; + // 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(()) } diff --git a/tools/kani-cov/src/merge.rs b/tools/kani-cov/src/merge.rs new file mode 100644 index 000000000000..35648fc8affe --- /dev/null +++ b/tools/kani-cov/src/merge.rs @@ -0,0 +1,14 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +use anyhow::Result; + +use crate::args::MergeArgs; + +pub fn merge_main(args: &MergeArgs) -> Result<()> { + Ok(()) +} + +pub fn validate_merge_args(args: &MergeArgs) -> Result<()> { + Ok(()) +} diff --git a/tools/kani-cov/src/report.rs b/tools/kani-cov/src/report.rs new file mode 100644 index 000000000000..c8e6196b948d --- /dev/null +++ b/tools/kani-cov/src/report.rs @@ -0,0 +1,8 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +use anyhow::Result; + +pub fn report_main() -> Result<()> { + Ok(()) +} diff --git a/tools/kani-cov/src/summary.rs b/tools/kani-cov/src/summary.rs new file mode 100644 index 000000000000..7ba1e21dd219 --- /dev/null +++ b/tools/kani-cov/src/summary.rs @@ -0,0 +1,6 @@ + +use anyhow::Result; + +pub fn summary_main() -> Result<()> { + Ok(()) +} From bee8f2da5367bcd494f84408b7bdd4161f93cacc Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 22 Aug 2024 21:51:17 +0000 Subject: [PATCH 04/36] Parse and combine raw results --- tools/kani-cov/src/args.rs | 4 +-- tools/kani-cov/src/coverage.rs | 18 ++++++++++- tools/kani-cov/src/merge.rs | 55 +++++++++++++++++++++++++++++++++- 3 files changed, 73 insertions(+), 4 deletions(-) diff --git a/tools/kani-cov/src/args.rs b/tools/kani-cov/src/args.rs index d1e851fe5650..f7213b008067 100644 --- a/tools/kani-cov/src/args.rs +++ b/tools/kani-cov/src/args.rs @@ -31,9 +31,9 @@ pub struct Args { #[derive(Debug, clap::Args)] pub struct MergeArgs { #[arg(long)] - output: Option, + pub output: Option, #[arg(required = true)] - files: Vec, + pub files: Vec, } pub fn validate_args(args: &Args) -> Result<()> { diff --git a/tools/kani-cov/src/coverage.rs b/tools/kani-cov/src/coverage.rs index 2c8cc9fda13d..b53070c1af8e 100644 --- a/tools/kani-cov/src/coverage.rs +++ b/tools/kani-cov/src/coverage.rs @@ -30,6 +30,12 @@ impl CoverageResults { Self { data } } } + +#[derive(Clone, Debug, Serialize, Deserialize)] +pub struct CombinedCoverageResults { + pub data: BTreeMap>, +} + pub fn fmt_coverage_results(coverage_results: &CoverageResults) -> Result { let mut fmt_string = String::new(); for (file, checks) in coverage_results.data.iter() { @@ -62,7 +68,17 @@ pub struct CoverageCheck { pub function: String, term: CoverageTerm, pub region: CoverageRegion, - status: CheckStatus, + pub status: CheckStatus, +} + +#[derive(Debug, Clone, Serialize, Deserialize)] +pub struct CovResult { + pub function: String, + // term: CoverageTerm, + pub region: CoverageRegion, + // status: CheckStatus, + pub times_covered: u32, + pub total_times: u32, } impl CoverageCheck { diff --git a/tools/kani-cov/src/merge.rs b/tools/kani-cov/src/merge.rs index 35648fc8affe..06cd529ad2be 100644 --- a/tools/kani-cov/src/merge.rs +++ b/tools/kani-cov/src/merge.rs @@ -1,14 +1,67 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +use std::{collections::BTreeMap, fs::File, io::BufReader, os::linux::raw, path::PathBuf}; + use anyhow::Result; -use crate::args::MergeArgs; +use crate::{args::MergeArgs, coverage::{CheckStatus, CombinedCoverageResults, CovResult, CoverageCheck, CoverageResults}}; pub fn merge_main(args: &MergeArgs) -> Result<()> { + let raw_results = parse_raw_results(&args.files)?; + let combined_results = combine_raw_results(&raw_results); + // save_combined_results(combined_results, args.output)?; Ok(()) } pub fn validate_merge_args(args: &MergeArgs) -> Result<()> { Ok(()) } + +fn parse_raw_results(paths: &Vec) -> Result> { + let mut raw_results = Vec::with_capacity(paths.len()); + for path in paths { + let filename = path.to_string_lossy(); + let file = File::open(path).expect(&format!("could not open file {filename}")); + let reader = BufReader::new(file); + + let result = serde_json::from_reader(reader).expect(&format!("could not deserialize file {filename}")); + raw_results.push(result); + } + Ok(raw_results) +} + +fn combine_raw_results(results: &Vec) -> CombinedCoverageResults { + let all_function_names = function_names_from_results(results); + println!("{:?}", all_function_names); + let mut new_data = BTreeMap::new(); + for fun_name in all_function_names { + let mut this_fun_checks: Vec<&CoverageCheck> = Vec::new(); + + for result in results { + if result.data.contains_key(&fun_name) { + this_fun_checks.extend(result.data.get(&fun_name).unwrap()) + } + } + + let mut new_results = Vec::new(); + while !this_fun_checks.is_empty() { + let this_region_check = this_fun_checks[0]; + // should do this with a partition... + let mut same_region_checks: Vec<&CoverageCheck> = this_fun_checks.iter().cloned().filter(|check| check.region == this_region_check.region).collect(); + this_fun_checks.retain(|check| check.region != this_region_check.region); + same_region_checks.push(this_region_check); + let total_times = same_region_checks.len().try_into().unwrap(); + let times_covered = same_region_checks.iter().filter(|check| check.status == CheckStatus::Covered).count().try_into().unwrap(); + let new_result = CovResult { function: fun_name.clone(), region: this_region_check.region.clone() , times_covered, total_times }; + new_results.push(new_result); + } + + new_data.insert(fun_name, new_results); + } + CombinedCoverageResults { data: new_data } +} + +fn function_names_from_results(results: &Vec) -> Vec { + results.iter().map(|result| result.data.keys().cloned().collect()).collect() +} From 0aa25b99080cdbab3b3a23b862f23d05c5d0511d Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Wed, 28 Aug 2024 20:39:00 +0000 Subject: [PATCH 05/36] Add missing copyright notices --- tools/kani-cov/Cargo.toml | 3 +++ tools/kani-cov/src/args.rs | 2 ++ tools/kani-cov/src/summary.rs | 2 ++ 3 files changed, 7 insertions(+) diff --git a/tools/kani-cov/Cargo.toml b/tools/kani-cov/Cargo.toml index 192b69db4884..89f6a7c15d5d 100644 --- a/tools/kani-cov/Cargo.toml +++ b/tools/kani-cov/Cargo.toml @@ -1,3 +1,6 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + [package] name = "kani-cov" version = "0.1.0" diff --git a/tools/kani-cov/src/args.rs b/tools/kani-cov/src/args.rs index f7213b008067..16aade953c82 100644 --- a/tools/kani-cov/src/args.rs +++ b/tools/kani-cov/src/args.rs @@ -1,3 +1,5 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT use std::path::PathBuf; diff --git a/tools/kani-cov/src/summary.rs b/tools/kani-cov/src/summary.rs index 7ba1e21dd219..e23e7281b163 100644 --- a/tools/kani-cov/src/summary.rs +++ b/tools/kani-cov/src/summary.rs @@ -1,3 +1,5 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT use anyhow::Result; From debeef408bf54a70964a4ab10f37a0d48f998baf Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 29 Aug 2024 14:52:55 +0000 Subject: [PATCH 06/36] Remove `atty` dependency --- Cargo.lock | 21 --------------------- tools/kani-cov/Cargo.toml | 1 - tools/kani-cov/src/main.rs | 7 +++---- 3 files changed, 3 insertions(+), 26 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 912cfe7d40ca..a5540b08a5eb 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -79,17 +79,6 @@ version = "1.0.86" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b3d1d046238990b9cf5bcde22a3fb3584ee5cf65fb2765f454ed428c7a0063da" -[[package]] -name = "atty" -version = "0.2.14" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d9b39be18770d11421cdb1b9947a45dd3f37e93092cbf377614828a319d5fee8" -dependencies = [ - "hermit-abi", - "libc", - "winapi", -] - [[package]] name = "autocfg" version = "1.3.0" @@ -428,15 +417,6 @@ version = "0.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "2304e00983f87ffb38b55b444b5e3b60a884b5d30c0fca7d82fe33449bbe55ea" -[[package]] -name = "hermit-abi" -version = "0.1.19" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "62b467343b94ba476dcb2500d242dadbb39557df889310ac77c5d99100aaac33" -dependencies = [ - "libc", -] - [[package]] name = "home" version = "0.5.9" @@ -512,7 +492,6 @@ name = "kani-cov" version = "0.1.0" dependencies = [ "anyhow", - "atty", "clap", "console", "serde", diff --git a/tools/kani-cov/Cargo.toml b/tools/kani-cov/Cargo.toml index 89f6a7c15d5d..1e721ad96e7c 100644 --- a/tools/kani-cov/Cargo.toml +++ b/tools/kani-cov/Cargo.toml @@ -10,7 +10,6 @@ edition = "2021" [dependencies] anyhow = "1.0.81" -atty = "0.2.14" clap = { version = "4.4.11", features = ["derive"] } console = "0.15.8" serde = "1.0.197" diff --git a/tools/kani-cov/src/main.rs b/tools/kani-cov/src/main.rs index e751d6be5bc0..ee68c137a0a5 100644 --- a/tools/kani-cov/src/main.rs +++ b/tools/kani-cov/src/main.rs @@ -7,12 +7,10 @@ mod merge; mod summary; mod report; use std::fs::File; -use std::io::Read; +use std::io::{IsTerminal, Read}; use std::io::{BufRead, BufReader}; use std::path::PathBuf; -use atty::Stream; - use crate::coverage::CoverageResults; use args::{Args, validate_args, Subcommand}; use clap::Parser; @@ -132,7 +130,8 @@ fn insert_escapes(str: &String, markers: Vec<(usize, bool)>) -> String { } fn open_marker() -> String { - if atty::is(Stream::Stdout) { + let support_color = std::io::stdout().is_terminal(); + if support_color { "\x1b[42m".to_string() } else { "```".to_string() From 9e9575afb6897f09d002dafd90f09635645d5fb5 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 29 Aug 2024 14:54:28 +0000 Subject: [PATCH 07/36] Add license to Cargo.toml --- tools/kani-cov/Cargo.toml | 1 + 1 file changed, 1 insertion(+) diff --git a/tools/kani-cov/Cargo.toml b/tools/kani-cov/Cargo.toml index 1e721ad96e7c..699fe8b101e8 100644 --- a/tools/kani-cov/Cargo.toml +++ b/tools/kani-cov/Cargo.toml @@ -5,6 +5,7 @@ name = "kani-cov" version = "0.1.0" edition = "2021" +license = "MIT OR Apache-2.0" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html From dd53e384099389e77ed10999e7178a084f97f029 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 29 Aug 2024 19:26:04 +0000 Subject: [PATCH 08/36] Move unused code to report --- tools/kani-cov/src/coverage.rs | 52 +++++++------- tools/kani-cov/src/main.rs | 121 ++------------------------------- tools/kani-cov/src/report.rs | 101 +++++++++++++++++++++++++++ 3 files changed, 131 insertions(+), 143 deletions(-) diff --git a/tools/kani-cov/src/coverage.rs b/tools/kani-cov/src/coverage.rs index b53070c1af8e..181f21663e5e 100644 --- a/tools/kani-cov/src/coverage.rs +++ b/tools/kani-cov/src/coverage.rs @@ -36,32 +36,32 @@ pub struct CombinedCoverageResults { pub data: BTreeMap>, } -pub fn fmt_coverage_results(coverage_results: &CoverageResults) -> Result { - let mut fmt_string = String::new(); - for (file, checks) in coverage_results.data.iter() { - let mut checks_by_function: BTreeMap> = 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 = 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) -} +// pub fn fmt_coverage_results(coverage_results: &CoverageResults) -> Result { +// let mut fmt_string = String::new(); +// for (file, checks) in coverage_results.data.iter() { +// let mut checks_by_function: BTreeMap> = 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 = 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 { diff --git a/tools/kani-cov/src/main.rs b/tools/kani-cov/src/main.rs index ee68c137a0a5..d7e9ff295aef 100644 --- a/tools/kani-cov/src/main.rs +++ b/tools/kani-cov/src/main.rs @@ -6,17 +6,10 @@ mod args; mod merge; mod summary; mod report; -use std::fs::File; -use std::io::{IsTerminal, Read}; -use std::io::{BufRead, BufReader}; -use std::path::PathBuf; -use crate::coverage::CoverageResults; -use args::{Args, validate_args, Subcommand}; +use args::{validate_args, Subcommand}; use clap::Parser; -use anyhow::{Context, Result}; -use coverage::CoverageCheck; - +use anyhow::Result; fn main() -> Result<()> { let args = args::Args::parse(); @@ -25,115 +18,9 @@ fn main() -> Result<()> { match args.command.unwrap() { Subcommand::Merge(merge_args) => merge::merge_main(&merge_args)?, - // Subcommand::Summary => summary::summary_main()?, + Subcommand::Summary(summary_args) => summary::summary_main(&summary_args)?, // Subcommand::Report => report::report_main()?, }; - // 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 { - 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 { - 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 -} - -fn open_marker() -> String { - let support_color = std::io::stdout().is_terminal(); - if support_color { - "\x1b[42m".to_string() - } else { - "```".to_string() - } + Ok(()) } diff --git a/tools/kani-cov/src/report.rs b/tools/kani-cov/src/report.rs index c8e6196b948d..11932f614349 100644 --- a/tools/kani-cov/src/report.rs +++ b/tools/kani-cov/src/report.rs @@ -2,7 +2,108 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use anyhow::Result; +// use coverage::CoverageCheck; +// use crate::coverage::CoverageResults; +// use args::Args; pub fn report_main() -> Result<()> { Ok(()) } + +// fn visualize_coverage_results(cov_results: &CoverageResults, root_path: PathBuf) -> Result { +// 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 { +// 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 +// } + +// fn open_marker() -> String { +// let support_color = std::io::stdout().is_terminal(); +// if support_color { +// "\x1b[42m".to_string() +// } else { +// "```".to_string() +// } +// } From ad632f32f89b79fc4b0b84454f374e25f20b0fa2 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 29 Aug 2024 19:26:30 +0000 Subject: [PATCH 09/36] Save combined results through merge --- tools/kani-cov/src/merge.rs | 18 ++++++++++++++---- 1 file changed, 14 insertions(+), 4 deletions(-) diff --git a/tools/kani-cov/src/merge.rs b/tools/kani-cov/src/merge.rs index 06cd529ad2be..5ca406776bc0 100644 --- a/tools/kani-cov/src/merge.rs +++ b/tools/kani-cov/src/merge.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -use std::{collections::BTreeMap, fs::File, io::BufReader, os::linux::raw, path::PathBuf}; +use std::{collections::BTreeMap, fs::File, io::{BufReader, BufWriter}, os::linux::raw, path::PathBuf}; use anyhow::Result; @@ -10,11 +10,11 @@ use crate::{args::MergeArgs, coverage::{CheckStatus, CombinedCoverageResults, Co pub fn merge_main(args: &MergeArgs) -> Result<()> { let raw_results = parse_raw_results(&args.files)?; let combined_results = combine_raw_results(&raw_results); - // save_combined_results(combined_results, args.output)?; + save_combined_results(&combined_results, &args.output)?; Ok(()) } -pub fn validate_merge_args(args: &MergeArgs) -> Result<()> { +pub fn validate_merge_args(_args: &MergeArgs) -> Result<()> { Ok(()) } @@ -33,7 +33,7 @@ fn parse_raw_results(paths: &Vec) -> Result> { fn combine_raw_results(results: &Vec) -> CombinedCoverageResults { let all_function_names = function_names_from_results(results); - println!("{:?}", all_function_names); + let mut new_data = BTreeMap::new(); for fun_name in all_function_names { let mut this_fun_checks: Vec<&CoverageCheck> = Vec::new(); @@ -62,6 +62,16 @@ fn combine_raw_results(results: &Vec) -> CombinedCoverageResult CombinedCoverageResults { data: new_data } } +fn save_combined_results(results: &CombinedCoverageResults, output: &Option) -> Result<()> { + let output_path = if let Some(out) = output { out } else { &PathBuf::from("default_kanicov.json") }; + let file = File::create(output_path)?; + let writer = BufWriter::new(file); + + serde_json::to_writer(writer, results)?; + + Ok(()) +} + fn function_names_from_results(results: &Vec) -> Vec { results.iter().map(|result| result.data.keys().cloned().collect()).collect() } From a659c1a0dd7b4e0a661ee24e817929e325fbf431 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 29 Aug 2024 19:26:47 +0000 Subject: [PATCH 10/36] Start summary command --- tools/kani-cov/src/args.rs | 12 ++++++++++-- tools/kani-cov/src/summary.rs | 8 +++++++- 2 files changed, 17 insertions(+), 3 deletions(-) diff --git a/tools/kani-cov/src/args.rs b/tools/kani-cov/src/args.rs index 16aade953c82..2621063349f7 100644 --- a/tools/kani-cov/src/args.rs +++ b/tools/kani-cov/src/args.rs @@ -11,7 +11,7 @@ use crate::{merge, summary, report}; #[derive(Debug, clap::Subcommand)] pub enum Subcommand { Merge(MergeArgs), - // Summary(SummaryArgs), + Summary(SummaryArgs), // Report(ReportArgs), } @@ -38,6 +38,14 @@ pub struct MergeArgs { pub files: Vec, } +#[derive(Debug, clap::Args)] +pub struct SummaryArgs { + #[arg(required = true)] + pub profile: Vec, + #[arg(required = true)] + pub output: Option, +} + pub fn validate_args(args: &Args) -> Result<()> { if args.command.is_none() { bail!("subcommand needs to be specified") @@ -45,7 +53,7 @@ pub fn validate_args(args: &Args) -> Result<()> { match args.command.as_ref().unwrap() { Subcommand::Merge(merge_args) => merge::validate_merge_args(&merge_args)?, - // Subcommand::Summary => summary::validate_summary_args(args)?, + Subcommand::Summary(summary_args) => summary::validate_summary_args(&summary_args)?, // Subcommand::Report => report::validate_report_args(args)?, }; diff --git a/tools/kani-cov/src/summary.rs b/tools/kani-cov/src/summary.rs index e23e7281b163..60afabfecb5a 100644 --- a/tools/kani-cov/src/summary.rs +++ b/tools/kani-cov/src/summary.rs @@ -3,6 +3,12 @@ use anyhow::Result; -pub fn summary_main() -> Result<()> { +use crate::args::SummaryArgs; + +pub fn summary_main(_args: &SummaryArgs) -> Result<()> { + Ok(()) +} + +pub fn validate_summary_args(_args: &SummaryArgs) -> Result<()> { Ok(()) } From 76351fd002c96240aae8d40bf6c321c8fa0251f5 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 29 Aug 2024 19:30:40 +0000 Subject: [PATCH 11/36] Some format fixes --- tools/kani-cov/src/args.rs | 2 +- tools/kani-cov/src/main.rs | 6 ++--- tools/kani-cov/src/merge.rs | 44 ++++++++++++++++++++++++++++++------- 3 files changed, 40 insertions(+), 12 deletions(-) diff --git a/tools/kani-cov/src/args.rs b/tools/kani-cov/src/args.rs index 2621063349f7..8df4a120a11d 100644 --- a/tools/kani-cov/src/args.rs +++ b/tools/kani-cov/src/args.rs @@ -6,7 +6,7 @@ use std::path::PathBuf; use anyhow::{bail, Result}; use clap::{arg, command}; -use crate::{merge, summary, report}; +use crate::{merge, report, summary}; #[derive(Debug, clap::Subcommand)] pub enum Subcommand { diff --git a/tools/kani-cov/src/main.rs b/tools/kani-cov/src/main.rs index d7e9ff295aef..25b32f14a2cf 100644 --- a/tools/kani-cov/src/main.rs +++ b/tools/kani-cov/src/main.rs @@ -1,15 +1,15 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -mod coverage; mod args; +mod coverage; mod merge; -mod summary; mod report; +mod summary; +use anyhow::Result; use args::{validate_args, Subcommand}; use clap::Parser; -use anyhow::Result; fn main() -> Result<()> { let args = args::Args::parse(); diff --git a/tools/kani-cov/src/merge.rs b/tools/kani-cov/src/merge.rs index 5ca406776bc0..f9eab5ffba4c 100644 --- a/tools/kani-cov/src/merge.rs +++ b/tools/kani-cov/src/merge.rs @@ -1,11 +1,20 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -use std::{collections::BTreeMap, fs::File, io::{BufReader, BufWriter}, os::linux::raw, path::PathBuf}; +use std::{ + collections::BTreeMap, + fs::File, + io::{BufReader, BufWriter}, + os::linux::raw, + path::PathBuf, +}; use anyhow::Result; -use crate::{args::MergeArgs, coverage::{CheckStatus, CombinedCoverageResults, CovResult, CoverageCheck, CoverageResults}}; +use crate::{ + args::MergeArgs, + coverage::{CheckStatus, CombinedCoverageResults, CovResult, CoverageCheck, CoverageResults}, +}; pub fn merge_main(args: &MergeArgs) -> Result<()> { let raw_results = parse_raw_results(&args.files)?; @@ -25,7 +34,8 @@ fn parse_raw_results(paths: &Vec) -> Result> { let file = File::open(path).expect(&format!("could not open file {filename}")); let reader = BufReader::new(file); - let result = serde_json::from_reader(reader).expect(&format!("could not deserialize file {filename}")); + let result = serde_json::from_reader(reader) + .expect(&format!("could not deserialize file {filename}")); raw_results.push(result); } Ok(raw_results) @@ -48,12 +58,26 @@ fn combine_raw_results(results: &Vec) -> CombinedCoverageResult while !this_fun_checks.is_empty() { let this_region_check = this_fun_checks[0]; // should do this with a partition... - let mut same_region_checks: Vec<&CoverageCheck> = this_fun_checks.iter().cloned().filter(|check| check.region == this_region_check.region).collect(); + let mut same_region_checks: Vec<&CoverageCheck> = this_fun_checks + .iter() + .cloned() + .filter(|check| check.region == this_region_check.region) + .collect(); this_fun_checks.retain(|check| check.region != this_region_check.region); same_region_checks.push(this_region_check); let total_times = same_region_checks.len().try_into().unwrap(); - let times_covered = same_region_checks.iter().filter(|check| check.status == CheckStatus::Covered).count().try_into().unwrap(); - let new_result = CovResult { function: fun_name.clone(), region: this_region_check.region.clone() , times_covered, total_times }; + let times_covered = same_region_checks + .iter() + .filter(|check| check.status == CheckStatus::Covered) + .count() + .try_into() + .unwrap(); + let new_result = CovResult { + function: fun_name.clone(), + region: this_region_check.region.clone(), + times_covered, + total_times, + }; new_results.push(new_result); } @@ -62,8 +86,12 @@ fn combine_raw_results(results: &Vec) -> CombinedCoverageResult CombinedCoverageResults { data: new_data } } -fn save_combined_results(results: &CombinedCoverageResults, output: &Option) -> Result<()> { - let output_path = if let Some(out) = output { out } else { &PathBuf::from("default_kanicov.json") }; +fn save_combined_results( + results: &CombinedCoverageResults, + output: &Option, +) -> Result<()> { + let output_path = + if let Some(out) = output { out } else { &PathBuf::from("default_kanicov.json") }; let file = File::create(output_path)?; let writer = BufWriter::new(file); From 304cfd22462e6e84ae9c78eaed811374d1d69636 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 29 Aug 2024 19:38:53 +0000 Subject: [PATCH 12/36] Fixes for `clippy` --- tools/kani-cov/src/args.rs | 12 +++++-- tools/kani-cov/src/coverage.rs | 59 +++++++++++++++++----------------- tools/kani-cov/src/main.rs | 2 +- tools/kani-cov/src/merge.rs | 3 +- tools/kani-cov/src/report.rs | 8 ++++- 5 files changed, 47 insertions(+), 37 deletions(-) diff --git a/tools/kani-cov/src/args.rs b/tools/kani-cov/src/args.rs index 8df4a120a11d..54749260043a 100644 --- a/tools/kani-cov/src/args.rs +++ b/tools/kani-cov/src/args.rs @@ -12,7 +12,7 @@ use crate::{merge, report, summary}; pub enum Subcommand { Merge(MergeArgs), Summary(SummaryArgs), - // Report(ReportArgs), + Report(ReportArgs), } #[derive(Debug, clap::Parser)] @@ -43,7 +43,13 @@ pub struct SummaryArgs { #[arg(required = true)] pub profile: Vec, #[arg(required = true)] - pub output: Option, + pub mapfile: Option, +} + +#[derive(Debug, clap::Args)] +pub struct ReportArgs { + #[arg(required = true)] + pub profile: Vec, } pub fn validate_args(args: &Args) -> Result<()> { @@ -54,7 +60,7 @@ pub fn validate_args(args: &Args) -> Result<()> { match args.command.as_ref().unwrap() { Subcommand::Merge(merge_args) => merge::validate_merge_args(&merge_args)?, Subcommand::Summary(summary_args) => summary::validate_summary_args(&summary_args)?, - // Subcommand::Report => report::validate_report_args(args)?, + Subcommand::Report(report_args) => report::validate_report_args(&report_args)?, }; Ok(()) diff --git a/tools/kani-cov/src/coverage.rs b/tools/kani-cov/src/coverage.rs index 181f21663e5e..b189c0c513cc 100644 --- a/tools/kani-cov/src/coverage.rs +++ b/tools/kani-cov/src/coverage.rs @@ -1,10 +1,9 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -use anyhow::Result; use console::style; use serde_derive::{Deserialize, Serialize}; -use std::fmt::{self, Write}; +use std::fmt; use std::{collections::BTreeMap, fmt::Display}; #[derive(Copy, Clone, Debug, Serialize, Deserialize, PartialEq, Eq)] @@ -25,11 +24,11 @@ pub struct CoverageResults { pub data: BTreeMap>, } -impl CoverageResults { - pub fn new(data: BTreeMap>) -> Self { - Self { data } - } -} +// impl CoverageResults { +// pub fn new(data: BTreeMap>) -> Self { +// Self { data } +// } +// } #[derive(Clone, Debug, Serialize, Deserialize)] pub struct CombinedCoverageResults { @@ -81,20 +80,20 @@ pub struct CovResult { pub total_times: u32, } -impl CoverageCheck { - pub fn new( - function: String, - term: CoverageTerm, - region: CoverageRegion, - status: CheckStatus, - ) -> Self { - Self { function, term, region, status } - } +// 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 - } -} +// pub fn is_covered(&self) -> bool { +// self.status == CheckStatus::Covered +// } +// } #[derive(Debug, Clone, Eq, PartialEq, PartialOrd, Ord, Serialize, Deserialize)] pub struct CoverageRegion { @@ -109,16 +108,16 @@ impl Display for CoverageRegion { } } -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 } - } -} +// 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 { diff --git a/tools/kani-cov/src/main.rs b/tools/kani-cov/src/main.rs index 25b32f14a2cf..1606637328f5 100644 --- a/tools/kani-cov/src/main.rs +++ b/tools/kani-cov/src/main.rs @@ -19,7 +19,7 @@ fn main() -> Result<()> { match args.command.unwrap() { Subcommand::Merge(merge_args) => merge::merge_main(&merge_args)?, Subcommand::Summary(summary_args) => summary::summary_main(&summary_args)?, - // Subcommand::Report => report::report_main()?, + Subcommand::Report(report_args) => report::report_main(&report_args)?, }; Ok(()) diff --git a/tools/kani-cov/src/merge.rs b/tools/kani-cov/src/merge.rs index f9eab5ffba4c..e583c408c2f7 100644 --- a/tools/kani-cov/src/merge.rs +++ b/tools/kani-cov/src/merge.rs @@ -5,7 +5,6 @@ use std::{ collections::BTreeMap, fs::File, io::{BufReader, BufWriter}, - os::linux::raw, path::PathBuf, }; @@ -100,6 +99,6 @@ fn save_combined_results( Ok(()) } -fn function_names_from_results(results: &Vec) -> Vec { +fn function_names_from_results(results: &[CoverageResults]) -> Vec { results.iter().map(|result| result.data.keys().cloned().collect()).collect() } diff --git a/tools/kani-cov/src/report.rs b/tools/kani-cov/src/report.rs index 11932f614349..c2252c0a202d 100644 --- a/tools/kani-cov/src/report.rs +++ b/tools/kani-cov/src/report.rs @@ -2,11 +2,17 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use anyhow::Result; + +use crate::args::ReportArgs; // use coverage::CoverageCheck; // use crate::coverage::CoverageResults; // use args::Args; -pub fn report_main() -> Result<()> { +pub fn report_main(_args: &ReportArgs) -> Result<()> { + Ok(()) +} + +pub fn validate_report_args(_args: &ReportArgs) -> Result<()> { Ok(()) } From c69f4653f1fcdf26f625825a735299a30def2c7b Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 29 Aug 2024 20:02:13 +0000 Subject: [PATCH 13/36] Add description to Cargo.toml --- tools/kani-cov/Cargo.toml | 1 + tools/kani-cov/src/args.rs | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/tools/kani-cov/Cargo.toml b/tools/kani-cov/Cargo.toml index 699fe8b101e8..a6efd26fdfb9 100644 --- a/tools/kani-cov/Cargo.toml +++ b/tools/kani-cov/Cargo.toml @@ -6,6 +6,7 @@ name = "kani-cov" version = "0.1.0" edition = "2021" license = "MIT OR Apache-2.0" +description = "A tool to process coverage information from Kani" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html diff --git a/tools/kani-cov/src/args.rs b/tools/kani-cov/src/args.rs index 54749260043a..6de629ebff79 100644 --- a/tools/kani-cov/src/args.rs +++ b/tools/kani-cov/src/args.rs @@ -19,7 +19,7 @@ pub enum Subcommand { #[command( version, name = "kani-cov", - about = "Process coverage information from Kani", + about = "A tool to process coverage information from Kani", args_override_self = true, subcommand_negates_reqs = true, subcommand_precedence_over_arg = true, From d0bb4787531abfe885e70bf0b778900702751089 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 30 Aug 2024 18:40:52 +0000 Subject: [PATCH 14/36] Parse function info with tree-sitter --- Cargo.lock | 45 ++++++++++++++++++++ tools/kani-cov/Cargo.toml | 2 + tools/kani-cov/src/args.rs | 10 +++-- tools/kani-cov/src/summary.rs | 80 ++++++++++++++++++++++++++++++++++- 4 files changed, 131 insertions(+), 6 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index a5540b08a5eb..7ebe030070a1 100644 --- a/Cargo.lock +++ b/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" @@ -497,6 +506,8 @@ dependencies = [ "serde", "serde_derive", "serde_json", + "tree-sitter", + "tree-sitter-rust", ] [[package]] @@ -1100,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" @@ -1365,6 +1382,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.12" diff --git a/tools/kani-cov/Cargo.toml b/tools/kani-cov/Cargo.toml index a6efd26fdfb9..4b9f14cc3ca9 100644 --- a/tools/kani-cov/Cargo.toml +++ b/tools/kani-cov/Cargo.toml @@ -17,3 +17,5 @@ console = "0.15.8" serde = "1.0.197" serde_derive = "1.0.197" serde_json = "1.0.115" +tree-sitter = "0.23.0" +tree-sitter-rust = "0.21.2" diff --git a/tools/kani-cov/src/args.rs b/tools/kani-cov/src/args.rs index 6de629ebff79..15ddd0247617 100644 --- a/tools/kani-cov/src/args.rs +++ b/tools/kani-cov/src/args.rs @@ -41,15 +41,17 @@ pub struct MergeArgs { #[derive(Debug, clap::Args)] pub struct SummaryArgs { #[arg(required = true)] - pub profile: Vec, - #[arg(required = true)] - pub mapfile: Option, + pub mapfile: PathBuf, + #[arg(long, required = true)] + pub profile: PathBuf, } #[derive(Debug, clap::Args)] pub struct ReportArgs { #[arg(required = true)] - pub profile: Vec, + pub mapfile: PathBuf, + #[arg(long, required = true)] + pub profile: PathBuf, } pub fn validate_args(args: &Args) -> Result<()> { diff --git a/tools/kani-cov/src/summary.rs b/tools/kani-cov/src/summary.rs index 60afabfecb5a..bce7acc01c36 100644 --- a/tools/kani-cov/src/summary.rs +++ b/tools/kani-cov/src/summary.rs @@ -1,14 +1,90 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +use std::{ + fs::{self, File}, + io::BufReader, + path::PathBuf, +}; + use anyhow::Result; +use tree_sitter::{Node, Parser}; + +use crate::{args::SummaryArgs, coverage::CombinedCoverageResults}; + +pub fn summary_main(args: &SummaryArgs) -> Result<()> { + let mapfile = File::open(&args.mapfile)?; + let reader = BufReader::new(mapfile); + + let covfile = File::open(&args.profile)?; + let covreader = BufReader::new(covfile); + let cov_results: CombinedCoverageResults = + serde_json::from_reader(covreader).expect("could not load coverage results"); + + println!("{cov_results:?}"); -use crate::args::SummaryArgs; + let source_files: Vec = + serde_json::from_reader(reader).expect("could not parse coverage metadata"); + + let mut function_info: Vec = Vec::new(); + + for file in source_files { + let new_info = function_info_from_file(&file); + function_info.extend(new_info); + } -pub fn summary_main(_args: &SummaryArgs) -> Result<()> { Ok(()) } pub fn validate_summary_args(_args: &SummaryArgs) -> Result<()> { Ok(()) } + +#[derive(Debug)] +struct FunctionCoverageInfo { + name: String, + start: (usize, usize), + end: (usize, usize), + num_lines: usize, +} + +fn function_info_from_file(filepath: &PathBuf) -> Vec { + let source_code = fs::read_to_string(filepath).expect("could not read source file"); + let mut parser = Parser::new(); + parser.set_language(&tree_sitter_rust::language()).expect("Error loading Rust grammar"); + + let tree = parser.parse(&source_code, None).expect("Failed to parse file"); + + let mut cursor = tree.walk(); + let first_child_exists = cursor.goto_first_child(); + + if !first_child_exists { + return vec![]; + } + + let mut function_info: Vec = Vec::new(); + + if cursor.node().kind() == "function_item" { + function_info.push(function_info_from_node(cursor.node(), source_code.as_bytes())) + }; + + while cursor.goto_next_sibling() { + if cursor.node().kind() == "function_item" { + function_info.push(function_info_from_node(cursor.node(), source_code.as_bytes())) + } + } + + function_info +} + +fn function_info_from_node<'a>(node: Node, source: &'a [u8]) -> FunctionCoverageInfo { + let name = node + .child_by_field_name("name") + .and_then(|name| name.utf8_text(source).ok()) + .expect("couldn't get function name") + .to_string(); + let start = (node.start_position().row, node.start_position().column); + let end = (node.end_position().row, node.end_position().column); + let num_lines = end.0 - start.0 + 1; + FunctionCoverageInfo { name, start, end, num_lines } +} From 5512d28f251b050ed40bd0c53025bd62638250ae Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Sat, 31 Aug 2024 12:06:56 +0000 Subject: [PATCH 15/36] Use file-function pairs to combine results --- tools/kani-cov/src/merge.rs | 39 +++++++++++++++++++++++++++---------- 1 file changed, 29 insertions(+), 10 deletions(-) diff --git a/tools/kani-cov/src/merge.rs b/tools/kani-cov/src/merge.rs index e583c408c2f7..b2f5a85fa3ce 100644 --- a/tools/kani-cov/src/merge.rs +++ b/tools/kani-cov/src/merge.rs @@ -3,8 +3,8 @@ use std::{ collections::BTreeMap, - fs::File, - io::{BufReader, BufWriter}, + fs::{File, OpenOptions}, + io::{BufReader, BufWriter, Write}, path::PathBuf, }; @@ -41,19 +41,20 @@ fn parse_raw_results(paths: &Vec) -> Result> { } fn combine_raw_results(results: &Vec) -> CombinedCoverageResults { - let all_function_names = function_names_from_results(results); + let all_file_function_names = function_names_from_results(results); let mut new_data = BTreeMap::new(); - for fun_name in all_function_names { + for (file_name, fun_name) in all_file_function_names { let mut this_fun_checks: Vec<&CoverageCheck> = Vec::new(); for result in results { - if result.data.contains_key(&fun_name) { - this_fun_checks.extend(result.data.get(&fun_name).unwrap()) + if result.data.contains_key(&file_name) { + this_fun_checks.extend(result.data.get(&file_name).unwrap().iter().filter(|check| check.function == fun_name)) } } let mut new_results = Vec::new(); + while !this_fun_checks.is_empty() { let this_region_check = this_fun_checks[0]; // should do this with a partition... @@ -65,12 +66,14 @@ fn combine_raw_results(results: &Vec) -> CombinedCoverageResult this_fun_checks.retain(|check| check.region != this_region_check.region); same_region_checks.push(this_region_check); let total_times = same_region_checks.len().try_into().unwrap(); + let times_covered = same_region_checks .iter() .filter(|check| check.status == CheckStatus::Covered) .count() .try_into() .unwrap(); + let new_result = CovResult { function: fun_name.clone(), region: this_region_check.region.clone(), @@ -80,7 +83,8 @@ fn combine_raw_results(results: &Vec) -> CombinedCoverageResult new_results.push(new_result); } - new_data.insert(fun_name, new_results); + let pair_string = format!("{file_name}+{fun_name}"); + new_data.insert(pair_string, new_results); } CombinedCoverageResults { data: new_data } } @@ -91,7 +95,8 @@ fn save_combined_results( ) -> Result<()> { let output_path = if let Some(out) = output { out } else { &PathBuf::from("default_kanicov.json") }; - let file = File::create(output_path)?; + + let file = OpenOptions::new().write(true).create(true).open(output_path)?; let writer = BufWriter::new(file); serde_json::to_writer(writer, results)?; @@ -99,6 +104,20 @@ fn save_combined_results( Ok(()) } -fn function_names_from_results(results: &[CoverageResults]) -> Vec { - results.iter().map(|result| result.data.keys().cloned().collect()).collect() +fn function_names_from_results(results: &[CoverageResults]) -> Vec<(String, String)> { + let mut file_function_pairs = vec![]; + for result in results { + let files = result.data.keys().cloned(); + for file in files { + let checks = result.data.get(&file).unwrap(); + for check in checks { + let function = check.function.clone(); + let file_function = (file.clone(), function); + if !file_function_pairs.contains(&file_function) { + file_function_pairs.push(file_function); + } + } + } + } + file_function_pairs } From 0e1dcc0e23c7df79cc43aff685cb55144f2db947 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Sat, 31 Aug 2024 13:39:01 +0000 Subject: [PATCH 16/36] Change combined results again --- tools/kani-cov/src/coverage.rs | 2 +- tools/kani-cov/src/merge.rs | 13 ++++++++++--- tools/kani-cov/src/summary.rs | 15 +++++++++++++++ 3 files changed, 26 insertions(+), 4 deletions(-) diff --git a/tools/kani-cov/src/coverage.rs b/tools/kani-cov/src/coverage.rs index b189c0c513cc..d1f9df318e0d 100644 --- a/tools/kani-cov/src/coverage.rs +++ b/tools/kani-cov/src/coverage.rs @@ -32,7 +32,7 @@ pub struct CoverageResults { #[derive(Clone, Debug, Serialize, Deserialize)] pub struct CombinedCoverageResults { - pub data: BTreeMap>, + pub data: BTreeMap)>>, } // pub fn fmt_coverage_results(coverage_results: &CoverageResults) -> Result { diff --git a/tools/kani-cov/src/merge.rs b/tools/kani-cov/src/merge.rs index b2f5a85fa3ce..0063431a13d1 100644 --- a/tools/kani-cov/src/merge.rs +++ b/tools/kani-cov/src/merge.rs @@ -43,7 +43,8 @@ fn parse_raw_results(paths: &Vec) -> Result> { fn combine_raw_results(results: &Vec) -> CombinedCoverageResults { let all_file_function_names = function_names_from_results(results); - let mut new_data = BTreeMap::new(); + let mut new_data: BTreeMap)>> = BTreeMap::new(); + for (file_name, fun_name) in all_file_function_names { let mut this_fun_checks: Vec<&CoverageCheck> = Vec::new(); @@ -83,8 +84,14 @@ fn combine_raw_results(results: &Vec) -> CombinedCoverageResult new_results.push(new_result); } - let pair_string = format!("{file_name}+{fun_name}"); - new_data.insert(pair_string, new_results); + // let pair_string = format!("{file_name}+{fun_name}"); + let filename_copy = file_name.clone(); + if new_data.contains_key(&file_name) { + new_data.get_mut(&filename_copy).unwrap().push((fun_name, new_results)); + } else { + new_data.insert(file_name.clone(), vec![(fun_name, new_results)]); + } + // new_data.insert(file_name, (fun_name, new_results)); } CombinedCoverageResults { data: new_data } } diff --git a/tools/kani-cov/src/summary.rs b/tools/kani-cov/src/summary.rs index bce7acc01c36..0d4b10c83445 100644 --- a/tools/kani-cov/src/summary.rs +++ b/tools/kani-cov/src/summary.rs @@ -33,6 +33,10 @@ pub fn summary_main(args: &SummaryArgs) -> Result<()> { function_info.extend(new_info); } + for info in function_info { + calculate_coverage_info(&info, &cov_results); + } + Ok(()) } @@ -40,6 +44,12 @@ pub fn validate_summary_args(_args: &SummaryArgs) -> Result<()> { Ok(()) } +fn calculate_coverage_info(info: &FunctionCoverageInfo, results: &CombinedCoverageResults) { + // `info` does not include file so how do we match? + // use function just for now... + let this_info_key = results.data.keys().find(|key| key.split_once('+').unwrap_or_default().1 == info.name).unwrap(); + let this_info_results = results.data.get(this_info_key); +} #[derive(Debug)] struct FunctionCoverageInfo { name: String, @@ -48,6 +58,11 @@ struct FunctionCoverageInfo { num_lines: usize, } +// struct SummaryInfo { +// covered_functions: u32, +// total_functions: u32, +// } + fn function_info_from_file(filepath: &PathBuf) -> Vec { let source_code = fs::read_to_string(filepath).expect("could not read source file"); let mut parser = Parser::new(); From fabdf4421e46a79c5b00a9760461a1ea65f57635 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 13 Sep 2024 15:37:04 +0000 Subject: [PATCH 17/36] Produce markdown table with `summary` --- tools/kani-cov/src/args.rs | 7 + tools/kani-cov/src/summary.rs | 289 +++++++++++++++++++++++++++++++--- 2 files changed, 273 insertions(+), 23 deletions(-) diff --git a/tools/kani-cov/src/args.rs b/tools/kani-cov/src/args.rs index 15ddd0247617..11602036144b 100644 --- a/tools/kani-cov/src/args.rs +++ b/tools/kani-cov/src/args.rs @@ -44,6 +44,13 @@ pub struct SummaryArgs { pub mapfile: PathBuf, #[arg(long, required = true)] pub profile: PathBuf, + #[arg(long, short, value_parser = clap::value_parser!(SummaryFormat), default_value = "markdown")] + pub format: SummaryFormat, +} + +#[derive(Clone, Debug, PartialEq, Eq, clap::ValueEnum)] +pub enum SummaryFormat { + Markdown, } #[derive(Debug, clap::Args)] diff --git a/tools/kani-cov/src/summary.rs b/tools/kani-cov/src/summary.rs index 0d4b10c83445..18d3350174c1 100644 --- a/tools/kani-cov/src/summary.rs +++ b/tools/kani-cov/src/summary.rs @@ -2,15 +2,13 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use std::{ - fs::{self, File}, - io::BufReader, - path::PathBuf, + cmp::max, fs::{self, File}, io::BufReader, path::PathBuf }; use anyhow::Result; use tree_sitter::{Node, Parser}; -use crate::{args::SummaryArgs, coverage::CombinedCoverageResults}; +use crate::{args::{SummaryArgs, SummaryFormat}, coverage::{CombinedCoverageResults, CovResult, CoverageRegion}}; pub fn summary_main(args: &SummaryArgs) -> Result<()> { let mapfile = File::open(&args.mapfile)?; @@ -18,52 +16,297 @@ pub fn summary_main(args: &SummaryArgs) -> Result<()> { let covfile = File::open(&args.profile)?; let covreader = BufReader::new(covfile); - let cov_results: CombinedCoverageResults = + let results: CombinedCoverageResults = serde_json::from_reader(covreader).expect("could not load coverage results"); - println!("{cov_results:?}"); - let source_files: Vec = serde_json::from_reader(reader).expect("could not parse coverage metadata"); - let mut function_info: Vec = Vec::new(); + let mut all_cov_info: Vec = Vec::new(); for file in source_files { - let new_info = function_info_from_file(&file); - function_info.extend(new_info); + let fun_info = function_info_from_file(&file); + let mut file_cov_info = Vec::new(); + for info in fun_info { + let cov_results = function_coverage_results(&info, &file, &results); + let function_coverage = function_coverage_info(&cov_results); + let line_coverage = line_coverage_info(&info, &cov_results); + let region_coverage = region_coverage_info(&cov_results); + let cur_function_coverage_results = FunctionCoverageResults { is_covered: function_coverage, total_lines: line_coverage.1, covered_lines: line_coverage.0, covered_regions: region_coverage.0, total_regions: region_coverage.1 }; + file_cov_info.push(cur_function_coverage_results); + } + let aggr_cov_info = aggregate_cov_info(&file, &file_cov_info); + all_cov_info.push(aggr_cov_info); } + print_coverage_info(&all_cov_info, &args.format); + + Ok(()) +} + +fn aggregate_cov_info(file: &PathBuf, file_cov_info: &Vec) -> FileCoverageInfo { + let total_functions = file_cov_info.len().try_into().unwrap(); + let covered_functions = file_cov_info.iter().filter(|f| f.is_covered).count().try_into().unwrap(); + let fun_cov_info = FunCovInfo { covered: covered_functions, total: total_functions }; + + let covered_lines = file_cov_info.iter().map(|c| c.covered_lines).sum(); + let total_lines = file_cov_info.iter().map(|c| c.total_lines).sum(); + let lines_cov_info = LineCovInfo { covered: covered_lines, total: total_lines }; + + let covered_regions = file_cov_info.iter().map(|c| c.covered_regions).sum(); + let total_regions = file_cov_info.iter().map(|c| c.total_regions).sum(); + let region_cov_info = RegionCovInfo { covered: covered_regions, total: total_regions }; - for info in function_info { - calculate_coverage_info(&info, &cov_results); + FileCoverageInfo { + filename: file.to_string_lossy().to_string(), + function: fun_cov_info, + line: lines_cov_info, + region: region_cov_info, } +} - Ok(()) +fn function_coverage_info(cov_results: &Option<(String, Vec)>) -> bool { + if let Some(res) = cov_results { + res.1.iter().any(|c| c.times_covered > 0) + } else { + false + } +} + +struct FunctionCoverageResults { + is_covered: bool, + covered_lines: u32, + total_lines: u32, + covered_regions: u32, + total_regions: u32, } pub fn validate_summary_args(_args: &SummaryArgs) -> Result<()> { Ok(()) } -fn calculate_coverage_info(info: &FunctionCoverageInfo, results: &CombinedCoverageResults) { +fn function_coverage_results(info: &FunctionInfo, file: &PathBuf, results: &CombinedCoverageResults) -> Option<(String, Vec)> { // `info` does not include file so how do we match? // use function just for now... - let this_info_key = results.data.keys().find(|key| key.split_once('+').unwrap_or_default().1 == info.name).unwrap(); - let this_info_results = results.data.get(this_info_key); + let filename = file.clone().into_os_string().into_string().unwrap(); + let right_filename = results.data.keys().find(|p| filename.ends_with(*p)).unwrap(); + // TODO: The filenames in kaniraw files should be absolute, just like in metadata + // Otherwise the key for `results` just fails... + let file_results = results.data.get(right_filename).unwrap(); + let function = info.name.clone(); + let fun_results = file_results.iter().find(|(f, _)| *f == function); + fun_results.cloned() +} + +// fn calculate_coverage_info(info: &FunctionInfo, file: &PathBuf, results: &CombinedCoverageResults) -> CovInfo { +// let cov_info = calculate_cov_info(info, fun_results); +// let lines_total = cov_info.iter().filter(|c|c.is_some()).count(); +// let lines_covered = cov_info.iter().filter(|c|c.is_some() && c.as_ref().unwrap().0 > 0).count(); + +// CovInfo { filename: function, function: FunCovInfo { covered: 0, total: 0 }, line: LineCovInfo { covered: lines_covered.try_into().unwrap(), total: lines_total.try_into().unwrap() }, region: RegionCovInfo { covered: 0, total: 0 }} +// // println!("{filename} {lines_covered}/{lines_total}"); +// // println!("{fun_results:?}"); +// } + +struct FileCoverageInfo { + filename: String, + function: FunCovInfo, + line: LineCovInfo, + region: RegionCovInfo, +} + +struct FunCovInfo { + covered: u32, + total: u32, +} + +struct LineCovInfo { + covered: u32, + total: u32, +} + +struct RegionCovInfo { + covered: u32, + total: u32, +} + + +// enum LineCoverStatus { +// Full, +// Partial, +// None, +// } + +fn line_coverage_info(info: &FunctionInfo, fun_results: &Option<(String, Vec)>) -> (u32, u32) { + let start_line: u32 = info.start.0.try_into().unwrap(); + let end_line: u32 = info.end.0.try_into().unwrap(); + // `line_status` represents all the lines between `start_line` and + // `end_line`. For each line, we will have either: + // - `None`, meaning there were no results associated with this line (this + // may happen with lines that only contain a closing `}`, for example). + // - `Some(max, other)`, where `max` represents the maximum number of times + // the line was covered by any coverage result, and `other` specifies the + // coverage results that don't amount to the maximum. + let mut line_status: Vec)>> = Vec::with_capacity((end_line - start_line + 1).try_into().unwrap()); + + if let Some(res) = fun_results { + let mut cur_results = res.1.clone(); + // was this sorted already? looks like it was not + // println!("BEFORE: {cur_results:?}"); + cur_results.sort_by(|a,b| b.region.start.0.cmp(&a.region.start.0)); + // println!("AFTER: {cur_results:?}"); + + fn line_contained_in_region(line: u32, region: &CoverageRegion) -> bool { + region.start.0 <= line && region.end.0 >= line + } + + + for line in start_line..end_line { + let line_results: Vec = cur_results.iter().filter(|c| line_contained_in_region(line, &c.region)).cloned().collect(); + if line_results.is_empty() { + line_status.push(None); + } else { + let max_covered = line_results.iter().max_by_key(|obj| obj.times_covered).map(|obj| obj.times_covered).unwrap_or(0); + let other_covered: Vec = line_results.iter().filter(|obj| obj.times_covered != max_covered).cloned().collect(); + line_status.push(Some((max_covered, other_covered))); + } + } + + // println!("{} : {:?}", res.0, line_status); + + // sanity check + // let info_start = (info.start.0.try_into().unwrap(),info.start.1.try_into().unwrap()); + // assert_eq!(cur_span.region.start, info_start); + } + let total_lines = line_status.iter().filter(|s| s.is_some()).count().try_into().unwrap(); + let covered_lines = line_status.iter().filter(|s| s.is_some() && s.as_ref().unwrap().0 > 0).count().try_into().unwrap(); + (covered_lines, total_lines) +} + +fn region_coverage_info(fun_results: &Option<(String, Vec)>) -> (u32, u32) { + if let Some(res) = fun_results { + let total_regions = res.1.len().try_into().unwrap(); + let covered_regions = res.1.iter().filter(|c| c.times_covered > 0).count().try_into().unwrap(); + (covered_regions, total_regions) + } else { (0, 0) } } + #[derive(Debug)] -struct FunctionCoverageInfo { +struct FunctionInfo { name: String, start: (usize, usize), end: (usize, usize), num_lines: usize, } +#[derive(Debug)] +struct NewFunctionInfo { + // name: String, + // start: (usize, usize), + // end: (usize, usize), + // function_covered: bool, + // lines_covered: usize, + // lines_total: usize, + // regions_covered: Option, + // regions_total: Option, +} + // struct SummaryInfo { // covered_functions: u32, // total_functions: u32, // } -fn function_info_from_file(filepath: &PathBuf) -> Vec { +fn print_coverage_info(info: &Vec, format: &SummaryFormat) { + match format { + SummaryFormat::Markdown => print_coverage_markdown_info(info), + } +} + +fn print_coverage_markdown_info(info: &Vec) { + + fn safe_div(num: u32, denom: u32) -> Option { + if denom == 0 { None } + else { Some(num as f32/denom as f32) } + } + + const HEADERS_ROWS: usize = 3; + const FILENAME_HEADER: &str = "Filename"; + const FUNCTION_HEADER: &str = "Function (%)"; + const LINE_HEADER: &str = "Line (%)"; + const REGION_HEADER: &str = "Region (%)"; + + let mut table_rows: Vec = Vec::with_capacity(HEADERS_ROWS + info.len() + 1); + let mut max_filename_fmt_width = FILENAME_HEADER.len(); + let mut max_function_fmt_width = FUNCTION_HEADER.len(); + let mut max_line_fmt_width = LINE_HEADER.len(); + let mut max_region_fmt_width = REGION_HEADER.len(); + + let mut data_rows: Vec<(String, String, String, String)> = Vec::with_capacity(info.len()); + + for cov_info in info { + let filename = cov_info.filename.to_string(); + let function_covered = cov_info.function.covered; + let function_total = cov_info.function.total; + let function_rate = safe_div(function_covered, function_total); + let function_rate_fmt = if let Some(rate) = function_rate { + format!("{:.2}", (rate * 100_f32)) + } else { + "N/A".to_string() + }; + let function_fmt = format!("{function_covered}/{function_total} ({function_rate_fmt})"); + + let line_covered = cov_info.line.covered; + let line_total = cov_info.line.total; + let line_rate = safe_div(line_covered, line_total); + let line_rate_fmt = if let Some(rate) = line_rate { + format!("{:.2}", (rate * 100_f32)) + } else { + "N/A".to_string() + }; + let line_fmt = format!("{line_covered}/{line_total} ({line_rate_fmt})"); + + let region_covered = cov_info.region.covered; + let region_total = cov_info.region.total; + let region_rate = safe_div(region_covered, region_total); + let region_rate_fmt = if let Some(rate) = region_rate { + format!("{:.2}", (rate * 100_f32)) + } else { + "N/A".to_string() + }; + let region_fmt = format!("{region_covered}/{region_total} ({region_rate_fmt})"); + + max_filename_fmt_width = max(max_filename_fmt_width, filename.len()); + max_function_fmt_width = max(max_function_fmt_width, function_fmt.len()); + max_line_fmt_width = max(max_line_fmt_width, line_fmt.len()); + max_region_fmt_width = max(max_region_fmt_width, region_fmt.len()); + + data_rows.push((filename, function_fmt, line_fmt, region_fmt)); + } + + let filename_sep: String = std::iter::repeat('-').take(max_filename_fmt_width).collect(); + let filename_space: String = std::iter::repeat(' ').take(max_filename_fmt_width - FILENAME_HEADER.len()).collect::(); + let function_sep: String = std::iter::repeat('-').take(max_function_fmt_width).collect(); + let function_space: String = std::iter::repeat(' ').take(max_function_fmt_width - FUNCTION_HEADER.len()).collect::(); + let line_sep: String = std::iter::repeat('-').take(max_line_fmt_width).collect(); + let line_space: String = std::iter::repeat(' ').take(max_line_fmt_width - LINE_HEADER.len()).collect::(); + let region_sep: String = std::iter::repeat('-').take(max_region_fmt_width).collect(); + let region_space: String = std::iter::repeat(' ').take(max_region_fmt_width - REGION_HEADER.len()).collect::(); + + let sep_row = format!("| {filename_sep} | {function_sep} | {line_sep} | {region_sep} |"); + table_rows.push(format!("| {FILENAME_HEADER}{filename_space} | {FUNCTION_HEADER}{function_space} | {LINE_HEADER}{line_space} | {REGION_HEADER}{region_space} |")); + table_rows.push(sep_row); + for (filename, function_fmt, line_fmt, region_fmt) in data_rows { + let filename_space: String = std::iter::repeat(' ').take(max_filename_fmt_width - filename.len()).collect::(); + let function_space: String = std::iter::repeat(' ').take(max_function_fmt_width - function_fmt.len()).collect::(); + let line_space: String = std::iter::repeat(' ').take(max_line_fmt_width - line_fmt.len()).collect::(); + let region_space: String = std::iter::repeat(' ').take(max_region_fmt_width - region_fmt.len()).collect::(); + let cur_row = format!("| {filename}{filename_space} | {function_fmt}{function_space} | {line_fmt}{line_space} | {region_fmt}{region_space} |"); + table_rows.push(cur_row); + } + + println!("{}", table_rows.join("\n")); +} + +fn function_info_from_file(filepath: &PathBuf) -> Vec { let source_code = fs::read_to_string(filepath).expect("could not read source file"); let mut parser = Parser::new(); parser.set_language(&tree_sitter_rust::language()).expect("Error loading Rust grammar"); @@ -77,7 +320,7 @@ fn function_info_from_file(filepath: &PathBuf) -> Vec { return vec![]; } - let mut function_info: Vec = Vec::new(); + let mut function_info: Vec = Vec::new(); if cursor.node().kind() == "function_item" { function_info.push(function_info_from_node(cursor.node(), source_code.as_bytes())) @@ -92,14 +335,14 @@ fn function_info_from_file(filepath: &PathBuf) -> Vec { function_info } -fn function_info_from_node<'a>(node: Node, source: &'a [u8]) -> FunctionCoverageInfo { +fn function_info_from_node<'a>(node: Node, source: &'a [u8]) -> FunctionInfo { let name = node .child_by_field_name("name") .and_then(|name| name.utf8_text(source).ok()) .expect("couldn't get function name") .to_string(); - let start = (node.start_position().row, node.start_position().column); - let end = (node.end_position().row, node.end_position().column); + let start = (node.start_position().row + 1, node.start_position().column + 1); + let end = (node.end_position().row + 1, node.end_position().column + 1); let num_lines = end.0 - start.0 + 1; - FunctionCoverageInfo { name, start, end, num_lines } + FunctionInfo { name, start, end, num_lines } } From 855d0a6a5699236225a8568adc964e487b964334 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 13 Sep 2024 21:31:05 +0000 Subject: [PATCH 18/36] Sketch Json format for summary --- tools/kani-cov/src/args.rs | 1 + tools/kani-cov/src/summary.rs | 1 + 2 files changed, 2 insertions(+) diff --git a/tools/kani-cov/src/args.rs b/tools/kani-cov/src/args.rs index 11602036144b..f8e57138e7f6 100644 --- a/tools/kani-cov/src/args.rs +++ b/tools/kani-cov/src/args.rs @@ -51,6 +51,7 @@ pub struct SummaryArgs { #[derive(Clone, Debug, PartialEq, Eq, clap::ValueEnum)] pub enum SummaryFormat { Markdown, + // Json, } #[derive(Debug, clap::Args)] diff --git a/tools/kani-cov/src/summary.rs b/tools/kani-cov/src/summary.rs index 18d3350174c1..07516f0a6afa 100644 --- a/tools/kani-cov/src/summary.rs +++ b/tools/kani-cov/src/summary.rs @@ -218,6 +218,7 @@ struct NewFunctionInfo { fn print_coverage_info(info: &Vec, format: &SummaryFormat) { match format { SummaryFormat::Markdown => print_coverage_markdown_info(info), + // SummaryFormat::Json => print_coverage_json_info(info), } } From 0df18b92f6cfcabaa318f2215e1061993c34379a Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 13 Sep 2024 22:30:15 +0000 Subject: [PATCH 19/36] Refator some code so it's shared with `report` --- tools/kani-cov/src/coverage.rs | 106 +++++++++++++++++++------ tools/kani-cov/src/report.rs | 29 ++++++- tools/kani-cov/src/summary.rs | 136 ++------------------------------- 3 files changed, 116 insertions(+), 155 deletions(-) diff --git a/tools/kani-cov/src/coverage.rs b/tools/kani-cov/src/coverage.rs index d1f9df318e0d..d47d4904d5b1 100644 --- a/tools/kani-cov/src/coverage.rs +++ b/tools/kani-cov/src/coverage.rs @@ -3,8 +3,10 @@ use console::style; use serde_derive::{Deserialize, Serialize}; -use std::fmt; +use std::{fmt, fs}; +use std::path::PathBuf; use std::{collections::BTreeMap, fmt::Display}; +use tree_sitter::{Node, Parser}; #[derive(Copy, Clone, Debug, Serialize, Deserialize, PartialEq, Eq)] #[serde(rename_all = "UPPERCASE")] @@ -24,12 +26,6 @@ pub struct CoverageResults { pub data: BTreeMap>, } -// impl CoverageResults { -// pub fn new(data: BTreeMap>) -> Self { -// Self { data } -// } -// } - #[derive(Clone, Debug, Serialize, Deserialize)] pub struct CombinedCoverageResults { pub data: BTreeMap)>>, @@ -80,21 +76,6 @@ pub struct CovResult { pub total_times: u32, } -// 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, @@ -140,3 +121,84 @@ impl std::fmt::Display for CheckStatus { write!(f, "{check_str}") } } + +pub struct FileCoverageInfo { + pub filename: String, + pub function: CoverageMetric, + pub line: CoverageMetric, + pub region: CoverageMetric, +} + +pub struct CoverageMetric { + pub covered: u32, + pub total: u32, + // rate: Option +} + +impl CoverageMetric { + pub fn new(covered: u32, total: u32) -> Self { + CoverageMetric { covered, total } + } +} + +pub fn function_info_from_file(filepath: &PathBuf) -> Vec { + let source_code = fs::read_to_string(filepath).expect("could not read source file"); + let mut parser = Parser::new(); + parser.set_language(&tree_sitter_rust::language()).expect("Error loading Rust grammar"); + + let tree = parser.parse(&source_code, None).expect("Failed to parse file"); + + let mut cursor = tree.walk(); + let first_child_exists = cursor.goto_first_child(); + + if !first_child_exists { + return vec![]; + } + + let mut function_info: Vec = Vec::new(); + + if cursor.node().kind() == "function_item" { + function_info.push(function_info_from_node(cursor.node(), source_code.as_bytes())) + }; + + while cursor.goto_next_sibling() { + if cursor.node().kind() == "function_item" { + function_info.push(function_info_from_node(cursor.node(), source_code.as_bytes())) + } + } + + function_info +} + +fn function_info_from_node<'a>(node: Node, source: &'a [u8]) -> FunctionInfo { + let name = node + .child_by_field_name("name") + .and_then(|name| name.utf8_text(source).ok()) + .expect("couldn't get function name") + .to_string(); + let start = (node.start_position().row + 1, node.start_position().column + 1); + let end = (node.end_position().row + 1, node.end_position().column + 1); + let num_lines = end.0 - start.0 + 1; + FunctionInfo { name, start, end, num_lines } +} + +#[derive(Debug)] +pub struct FunctionInfo { + pub name: String, + pub start: (usize, usize), + pub end: (usize, usize), + pub num_lines: usize, +} + +pub fn function_coverage_results(info: &FunctionInfo, file: &PathBuf, results: &CombinedCoverageResults) -> Option<(String, Vec)> { + // `info` does not include file so how do we match? + // use function just for now... + let filename = file.clone().into_os_string().into_string().unwrap(); + let right_filename = results.data.keys().find(|p| filename.ends_with(*p)).unwrap(); + // TODO: The filenames in kaniraw files should be absolute, just like in metadata + // Otherwise the key for `results` just fails... + let file_results = results.data.get(right_filename).unwrap(); + let function = info.name.clone(); + let fun_results = file_results.iter().find(|(f, _)| *f == function); + fun_results.cloned() +} diff --git a/tools/kani-cov/src/report.rs b/tools/kani-cov/src/report.rs index c2252c0a202d..830a43f97285 100644 --- a/tools/kani-cov/src/report.rs +++ b/tools/kani-cov/src/report.rs @@ -1,14 +1,37 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +use std::{fs::File, io::BufReader, path::PathBuf}; + use anyhow::Result; -use crate::args::ReportArgs; -// use coverage::CoverageCheck; +use crate::{args::ReportArgs, coverage::CombinedCoverageResults}; +use crate::coverage::{function_coverage_results, function_info_from_file, FileCoverageInfo}; // use crate::coverage::CoverageResults; // use args::Args; -pub fn report_main(_args: &ReportArgs) -> Result<()> { +pub fn report_main(args: &ReportArgs) -> Result<()> { + let mapfile = File::open(&args.mapfile)?; + let reader = BufReader::new(mapfile); + + let covfile = File::open(&args.profile)?; + let covreader = BufReader::new(covfile); + let results: CombinedCoverageResults = + serde_json::from_reader(covreader).expect("could not load coverage results"); + + let source_files: Vec = + serde_json::from_reader(reader).expect("could not parse coverage metadata"); + + let mut all_cov_info: Vec = Vec::new(); + + for file in source_files { + let fun_info = function_info_from_file(&file); + // let mut file_cov_info = Vec::new(); + for info in fun_info { + let cov_results = function_coverage_results(&info, &file, &results); + } + } + Ok(()) } diff --git a/tools/kani-cov/src/summary.rs b/tools/kani-cov/src/summary.rs index 07516f0a6afa..04a921f53be5 100644 --- a/tools/kani-cov/src/summary.rs +++ b/tools/kani-cov/src/summary.rs @@ -2,13 +2,12 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use std::{ - cmp::max, fs::{self, File}, io::BufReader, path::PathBuf + cmp::max, fs::File, io::BufReader, path::PathBuf }; use anyhow::Result; -use tree_sitter::{Node, Parser}; -use crate::{args::{SummaryArgs, SummaryFormat}, coverage::{CombinedCoverageResults, CovResult, CoverageRegion}}; +use crate::{args::{SummaryArgs, SummaryFormat}, coverage::{function_coverage_results, function_info_from_file, CombinedCoverageResults, CovResult, CoverageMetric, CoverageRegion, FileCoverageInfo, FunctionInfo}}; pub fn summary_main(args: &SummaryArgs) -> Result<()> { let mapfile = File::open(&args.mapfile)?; @@ -46,15 +45,15 @@ pub fn summary_main(args: &SummaryArgs) -> Result<()> { fn aggregate_cov_info(file: &PathBuf, file_cov_info: &Vec) -> FileCoverageInfo { let total_functions = file_cov_info.len().try_into().unwrap(); let covered_functions = file_cov_info.iter().filter(|f| f.is_covered).count().try_into().unwrap(); - let fun_cov_info = FunCovInfo { covered: covered_functions, total: total_functions }; + let fun_cov_info = CoverageMetric::new(covered_functions, total_functions); let covered_lines = file_cov_info.iter().map(|c| c.covered_lines).sum(); let total_lines = file_cov_info.iter().map(|c| c.total_lines).sum(); - let lines_cov_info = LineCovInfo { covered: covered_lines, total: total_lines }; + let lines_cov_info = CoverageMetric::new(covered_lines, total_lines); let covered_regions = file_cov_info.iter().map(|c| c.covered_regions).sum(); let total_regions = file_cov_info.iter().map(|c| c.total_regions).sum(); - let region_cov_info = RegionCovInfo { covered: covered_regions, total: total_regions }; + let region_cov_info = CoverageMetric::new(covered_regions, total_regions); FileCoverageInfo { filename: file.to_string_lossy().to_string(), @@ -84,58 +83,6 @@ pub fn validate_summary_args(_args: &SummaryArgs) -> Result<()> { Ok(()) } -fn function_coverage_results(info: &FunctionInfo, file: &PathBuf, results: &CombinedCoverageResults) -> Option<(String, Vec)> { - // `info` does not include file so how do we match? - // use function just for now... - let filename = file.clone().into_os_string().into_string().unwrap(); - let right_filename = results.data.keys().find(|p| filename.ends_with(*p)).unwrap(); - // TODO: The filenames in kaniraw files should be absolute, just like in metadata - // Otherwise the key for `results` just fails... - let file_results = results.data.get(right_filename).unwrap(); - let function = info.name.clone(); - let fun_results = file_results.iter().find(|(f, _)| *f == function); - fun_results.cloned() -} - -// fn calculate_coverage_info(info: &FunctionInfo, file: &PathBuf, results: &CombinedCoverageResults) -> CovInfo { -// let cov_info = calculate_cov_info(info, fun_results); -// let lines_total = cov_info.iter().filter(|c|c.is_some()).count(); -// let lines_covered = cov_info.iter().filter(|c|c.is_some() && c.as_ref().unwrap().0 > 0).count(); - -// CovInfo { filename: function, function: FunCovInfo { covered: 0, total: 0 }, line: LineCovInfo { covered: lines_covered.try_into().unwrap(), total: lines_total.try_into().unwrap() }, region: RegionCovInfo { covered: 0, total: 0 }} -// // println!("{filename} {lines_covered}/{lines_total}"); -// // println!("{fun_results:?}"); -// } - -struct FileCoverageInfo { - filename: String, - function: FunCovInfo, - line: LineCovInfo, - region: RegionCovInfo, -} - -struct FunCovInfo { - covered: u32, - total: u32, -} - -struct LineCovInfo { - covered: u32, - total: u32, -} - -struct RegionCovInfo { - covered: u32, - total: u32, -} - - -// enum LineCoverStatus { -// Full, -// Partial, -// None, -// } - fn line_coverage_info(info: &FunctionInfo, fun_results: &Option<(String, Vec)>) -> (u32, u32) { let start_line: u32 = info.start.0.try_into().unwrap(); let end_line: u32 = info.end.0.try_into().unwrap(); @@ -170,13 +117,8 @@ fn line_coverage_info(info: &FunctionInfo, fun_results: &Option<(String, Vec 0).count().try_into().unwrap(); (covered_lines, total_lines) @@ -190,31 +132,6 @@ fn region_coverage_info(fun_results: &Option<(String, Vec, - // regions_total: Option, -} - -// struct SummaryInfo { -// covered_functions: u32, -// total_functions: u32, -// } - fn print_coverage_info(info: &Vec, format: &SummaryFormat) { match format { SummaryFormat::Markdown => print_coverage_markdown_info(info), @@ -306,44 +223,3 @@ fn print_coverage_markdown_info(info: &Vec) { println!("{}", table_rows.join("\n")); } - -fn function_info_from_file(filepath: &PathBuf) -> Vec { - let source_code = fs::read_to_string(filepath).expect("could not read source file"); - let mut parser = Parser::new(); - parser.set_language(&tree_sitter_rust::language()).expect("Error loading Rust grammar"); - - let tree = parser.parse(&source_code, None).expect("Failed to parse file"); - - let mut cursor = tree.walk(); - let first_child_exists = cursor.goto_first_child(); - - if !first_child_exists { - return vec![]; - } - - let mut function_info: Vec = Vec::new(); - - if cursor.node().kind() == "function_item" { - function_info.push(function_info_from_node(cursor.node(), source_code.as_bytes())) - }; - - while cursor.goto_next_sibling() { - if cursor.node().kind() == "function_item" { - function_info.push(function_info_from_node(cursor.node(), source_code.as_bytes())) - } - } - - function_info -} - -fn function_info_from_node<'a>(node: Node, source: &'a [u8]) -> FunctionInfo { - let name = node - .child_by_field_name("name") - .and_then(|name| name.utf8_text(source).ok()) - .expect("couldn't get function name") - .to_string(); - let start = (node.start_position().row + 1, node.start_position().column + 1); - let end = (node.end_position().row + 1, node.end_position().column + 1); - let num_lines = end.0 - start.0 + 1; - FunctionInfo { name, start, end, num_lines } -} From 50bb5530bb0309dbc9d36c9c385b04bf843c913c Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 16 Sep 2024 22:23:01 +0000 Subject: [PATCH 20/36] Init. version for terminal reports --- tools/kani-cov/src/coverage.rs | 8 +- tools/kani-cov/src/merge.rs | 9 ++- tools/kani-cov/src/report.rs | 86 +++++++++++++++++--- tools/kani-cov/src/summary.rs | 140 +++++++++++++++++++++++---------- 4 files changed, 188 insertions(+), 55 deletions(-) diff --git a/tools/kani-cov/src/coverage.rs b/tools/kani-cov/src/coverage.rs index d47d4904d5b1..2bc800ba80ad 100644 --- a/tools/kani-cov/src/coverage.rs +++ b/tools/kani-cov/src/coverage.rs @@ -3,9 +3,9 @@ use console::style; use serde_derive::{Deserialize, Serialize}; -use std::{fmt, fs}; use std::path::PathBuf; use std::{collections::BTreeMap, fmt::Display}; +use std::{fmt, fs}; use tree_sitter::{Node, Parser}; #[derive(Copy, Clone, Debug, Serialize, Deserialize, PartialEq, Eq)] @@ -190,7 +190,11 @@ pub struct FunctionInfo { pub num_lines: usize, } -pub fn function_coverage_results(info: &FunctionInfo, file: &PathBuf, results: &CombinedCoverageResults) -> Option<(String, Vec)> { +pub fn function_coverage_results( + info: &FunctionInfo, + file: &PathBuf, + results: &CombinedCoverageResults, +) -> Option<(String, Vec)> { // `info` does not include file so how do we match? // use function just for now... let filename = file.clone().into_os_string().into_string().unwrap(); diff --git a/tools/kani-cov/src/merge.rs b/tools/kani-cov/src/merge.rs index 0063431a13d1..87863a314aa0 100644 --- a/tools/kani-cov/src/merge.rs +++ b/tools/kani-cov/src/merge.rs @@ -50,7 +50,14 @@ fn combine_raw_results(results: &Vec) -> CombinedCoverageResult for result in results { if result.data.contains_key(&file_name) { - this_fun_checks.extend(result.data.get(&file_name).unwrap().iter().filter(|check| check.function == fun_name)) + this_fun_checks.extend( + result + .data + .get(&file_name) + .unwrap() + .iter() + .filter(|check| check.function == fun_name), + ) } } diff --git a/tools/kani-cov/src/report.rs b/tools/kani-cov/src/report.rs index 830a43f97285..ecbcbe8d2f2a 100644 --- a/tools/kani-cov/src/report.rs +++ b/tools/kani-cov/src/report.rs @@ -1,12 +1,16 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +use std::io::{BufRead, IsTerminal}; use std::{fs::File, io::BufReader, path::PathBuf}; use anyhow::Result; +use crate::coverage::{ + function_coverage_results, function_info_from_file, CovResult, FileCoverageInfo, FunctionInfo, +}; +use crate::summary::{line_coverage_info, line_coverage_results}; use crate::{args::ReportArgs, coverage::CombinedCoverageResults}; -use crate::coverage::{function_coverage_results, function_info_from_file, FileCoverageInfo}; // use crate::coverage::CoverageResults; // use args::Args; @@ -22,14 +26,21 @@ pub fn report_main(args: &ReportArgs) -> Result<()> { let source_files: Vec = serde_json::from_reader(reader).expect("could not parse coverage metadata"); - let mut all_cov_info: Vec = Vec::new(); - for file in source_files { let fun_info = function_info_from_file(&file); - // let mut file_cov_info = Vec::new(); + let mut file_cov_info = Vec::new(); for info in fun_info { let cov_results = function_coverage_results(&info, &file, &results); + let line_coverage = line_coverage_results(&info, &cov_results); + let line_coverage_matched: Vec<(usize, Option<(u32, Vec)>)> = + (info.start.0..=info.end.0).zip(line_coverage.clone()).collect(); + // println!("REG: {line_coverage:?}"); + // println!("MATCHED: {line_coverage_matched:?}"); + // let new_res = line_coverage_matched.into_iter().filter(|(num, data)| data.is_some()).collect(); + file_cov_info.push(line_coverage_matched); } + // let file_coverage_results = match_line_coverage_file(file_cov_info); + print_coverage_results(file, file_cov_info)?; } Ok(()) @@ -39,6 +50,57 @@ pub fn validate_report_args(_args: &ReportArgs) -> Result<()> { Ok(()) } +pub fn print_coverage_results( + filepath: PathBuf, + results: Vec)>)>>, +) -> Result<()> { + let flattened_results: Vec<(usize, Option<(u32, Vec)>)> = + results.into_iter().flatten().collect(); + println!("{}", filepath.to_string_lossy().to_string()); + + let file = File::open(filepath)?; + let reader = BufReader::new(file); + + println!("{flattened_results:?}"); + for (i, line) in reader.lines().enumerate() { + let idx = i + 1; + let line = line?; + let cur_line_result = flattened_results.iter().find(|(num, _)| *num == idx); + let max = if let Some((num, data)) = cur_line_result { + if data.is_some() { + format!("{:4}", data.clone().unwrap().0) + } else { + format!("{:4}", " ".to_string()) + } + } else { + format!("{:4}", " ".to_string()) + }; + let line_fmt = if max == " 0" { format!("{}{line}{}", "\x1b[42m", "\x1b[0m") } else {line}; + println!("{idx:4}| {max}| {line_fmt}"); + let differing_results: Vec = + if let Some((num, data)) = cur_line_result { if data.is_some() {data.clone().unwrap().1} else {vec![]} } else { vec![] }; + let zero_differing_results: Vec<&CovResult> = + differing_results.iter().filter(|x| x.times_covered == 0).collect(); + let mut str = std::iter::repeat(' ').take(11_usize).collect::(); + let mut cur_shift = 0; + let mut print_differing = false; + for res in zero_differing_results { + let start: usize = res.region.start.1.try_into().unwrap(); + let spaces_next = std::iter::repeat(' ').take(start - cur_shift).collect::(); + str.push_str(&format!("{spaces_next}^0")); + cur_shift += start + 2; + print_differing = true; + // res.region.start + } + if print_differing { + println!("{str}"); + } + } + + Ok(()) +} +// fn match_line_coverage_file(line_cov_info: Vec<(FunctionInfo, Vec)>) -> ?? { +// } // fn visualize_coverage_results(cov_results: &CoverageResults, root_path: PathBuf) -> Result { // let mut formatted_output = String::new(); // let cov_data = &cov_results.data; @@ -128,11 +190,11 @@ pub fn validate_report_args(_args: &ReportArgs) -> Result<()> { // new_str // } -// fn open_marker() -> String { -// let support_color = std::io::stdout().is_terminal(); -// if support_color { -// "\x1b[42m".to_string() -// } else { -// "```".to_string() -// } -// } +fn red() -> String { + let support_color = std::io::stdout().is_terminal(); + if support_color { + "\x1b[42m".to_string() + } else { + "```".to_string() + } +} diff --git a/tools/kani-cov/src/summary.rs b/tools/kani-cov/src/summary.rs index 04a921f53be5..ea0c1c33c894 100644 --- a/tools/kani-cov/src/summary.rs +++ b/tools/kani-cov/src/summary.rs @@ -1,13 +1,17 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -use std::{ - cmp::max, fs::File, io::BufReader, path::PathBuf -}; +use std::{cmp::max, fs::File, io::BufReader, path::PathBuf}; use anyhow::Result; -use crate::{args::{SummaryArgs, SummaryFormat}, coverage::{function_coverage_results, function_info_from_file, CombinedCoverageResults, CovResult, CoverageMetric, CoverageRegion, FileCoverageInfo, FunctionInfo}}; +use crate::{ + args::{SummaryArgs, SummaryFormat}, + coverage::{ + function_coverage_results, function_info_from_file, CombinedCoverageResults, CovResult, + CoverageMetric, CoverageRegion, FileCoverageInfo, FunctionInfo, + }, +}; pub fn summary_main(args: &SummaryArgs) -> Result<()> { let mapfile = File::open(&args.mapfile)?; @@ -31,7 +35,13 @@ pub fn summary_main(args: &SummaryArgs) -> Result<()> { let function_coverage = function_coverage_info(&cov_results); let line_coverage = line_coverage_info(&info, &cov_results); let region_coverage = region_coverage_info(&cov_results); - let cur_function_coverage_results = FunctionCoverageResults { is_covered: function_coverage, total_lines: line_coverage.1, covered_lines: line_coverage.0, covered_regions: region_coverage.0, total_regions: region_coverage.1 }; + let cur_function_coverage_results = FunctionCoverageResults { + is_covered: function_coverage, + total_lines: line_coverage.1, + covered_lines: line_coverage.0, + covered_regions: region_coverage.0, + total_regions: region_coverage.1, + }; file_cov_info.push(cur_function_coverage_results); } let aggr_cov_info = aggregate_cov_info(&file, &file_cov_info); @@ -42,15 +52,19 @@ pub fn summary_main(args: &SummaryArgs) -> Result<()> { Ok(()) } -fn aggregate_cov_info(file: &PathBuf, file_cov_info: &Vec) -> FileCoverageInfo { +fn aggregate_cov_info( + file: &PathBuf, + file_cov_info: &Vec, +) -> FileCoverageInfo { let total_functions = file_cov_info.len().try_into().unwrap(); - let covered_functions = file_cov_info.iter().filter(|f| f.is_covered).count().try_into().unwrap(); + let covered_functions = + file_cov_info.iter().filter(|f| f.is_covered).count().try_into().unwrap(); let fun_cov_info = CoverageMetric::new(covered_functions, total_functions); - + let covered_lines = file_cov_info.iter().map(|c| c.covered_lines).sum(); let total_lines = file_cov_info.iter().map(|c| c.total_lines).sum(); let lines_cov_info = CoverageMetric::new(covered_lines, total_lines); - + let covered_regions = file_cov_info.iter().map(|c| c.covered_regions).sum(); let total_regions = file_cov_info.iter().map(|c| c.total_regions).sum(); let region_cov_info = CoverageMetric::new(covered_regions, total_regions); @@ -64,11 +78,7 @@ fn aggregate_cov_info(file: &PathBuf, file_cov_info: &Vec)>) -> bool { - if let Some(res) = cov_results { - res.1.iter().any(|c| c.times_covered > 0) - } else { - false - } + if let Some(res) = cov_results { res.1.iter().any(|c| c.times_covered > 0) } else { false } } struct FunctionCoverageResults { @@ -83,7 +93,10 @@ pub fn validate_summary_args(_args: &SummaryArgs) -> Result<()> { Ok(()) } -fn line_coverage_info(info: &FunctionInfo, fun_results: &Option<(String, Vec)>) -> (u32, u32) { +pub fn line_coverage_results( + info: &FunctionInfo, + fun_results: &Option<(String, Vec)>, +) -> Vec)>> { let start_line: u32 = info.start.0.try_into().unwrap(); let end_line: u32 = info.end.0.try_into().unwrap(); // `line_status` represents all the lines between `start_line` and @@ -93,43 +106,77 @@ fn line_coverage_info(info: &FunctionInfo, fun_results: &Option<(String, Vec)>> = Vec::with_capacity((end_line - start_line + 1).try_into().unwrap()); + let mut line_status: Vec)>> = + Vec::with_capacity((end_line - start_line + 1).try_into().unwrap()); if let Some(res) = fun_results { - let mut cur_results = res.1.clone(); + let mut cur_results = res.1.clone(); // was this sorted already? looks like it was not // println!("BEFORE: {cur_results:?}"); - cur_results.sort_by(|a,b| b.region.start.0.cmp(&a.region.start.0)); + cur_results.sort_by(|a, b| b.region.start.0.cmp(&a.region.start.0)); // println!("AFTER: {cur_results:?}"); fn line_contained_in_region(line: u32, region: &CoverageRegion) -> bool { region.start.0 <= line && region.end.0 >= line } - for line in start_line..end_line { - let line_results: Vec = cur_results.iter().filter(|c| line_contained_in_region(line, &c.region)).cloned().collect(); + let line_results: Vec = cur_results + .iter() + .filter(|c| line_contained_in_region(line, &c.region)) + .cloned() + .collect(); if line_results.is_empty() { line_status.push(None); } else { - let max_covered = line_results.iter().max_by_key(|obj| obj.times_covered).map(|obj| obj.times_covered).unwrap_or(0); - let other_covered: Vec = line_results.iter().filter(|obj| obj.times_covered != max_covered).cloned().collect(); + let max_covered = line_results + .iter() + .max_by_key(|obj| obj.times_covered) + .map(|obj| obj.times_covered) + .unwrap_or(0); + let other_covered: Vec = line_results + .iter() + .filter(|obj| obj.times_covered != max_covered) + .cloned() + .collect(); line_status.push(Some((max_covered, other_covered))); } } + } else { + line_status = std::iter::repeat(Some((0, vec![]))) + .take((end_line - start_line + 1).try_into().unwrap()) + .collect(); } + println!("{line_status:?}"); + line_status +} +pub fn line_coverage_info( + info: &FunctionInfo, + fun_results: &Option<(String, Vec)>, +) -> (u32, u32) { + let line_status = line_coverage_results(info, fun_results); let total_lines = line_status.iter().filter(|s| s.is_some()).count().try_into().unwrap(); - let covered_lines = line_status.iter().filter(|s| s.is_some() && s.as_ref().unwrap().0 > 0).count().try_into().unwrap(); + let covered_lines = line_status + .iter() + .filter(|s| s.is_some() && s.as_ref().unwrap().0 > 0) + .count() + .try_into() + .unwrap(); (covered_lines, total_lines) } -fn region_coverage_info(fun_results: &Option<(String, Vec)>) -> (u32, u32) { +fn region_coverage_info( + fun_results: &Option<(String, Vec)>, +) -> (u32, u32) { if let Some(res) = fun_results { let total_regions = res.1.len().try_into().unwrap(); - let covered_regions = res.1.iter().filter(|c| c.times_covered > 0).count().try_into().unwrap(); + let covered_regions = + res.1.iter().filter(|c| c.times_covered > 0).count().try_into().unwrap(); (covered_regions, total_regions) - } else { (0, 0) } + } else { + (0, 0) + } } fn print_coverage_info(info: &Vec, format: &SummaryFormat) { @@ -140,10 +187,8 @@ fn print_coverage_info(info: &Vec, format: &SummaryFormat) { } fn print_coverage_markdown_info(info: &Vec) { - fn safe_div(num: u32, denom: u32) -> Option { - if denom == 0 { None } - else { Some(num as f32/denom as f32) } + if denom == 0 { None } else { Some(num as f32 / denom as f32) } } const HEADERS_ROWS: usize = 3; @@ -157,7 +202,7 @@ fn print_coverage_markdown_info(info: &Vec) { let mut max_function_fmt_width = FUNCTION_HEADER.len(); let mut max_line_fmt_width = LINE_HEADER.len(); let mut max_region_fmt_width = REGION_HEADER.len(); - + let mut data_rows: Vec<(String, String, String, String)> = Vec::with_capacity(info.len()); for cov_info in info { @@ -191,7 +236,7 @@ fn print_coverage_markdown_info(info: &Vec) { "N/A".to_string() }; let region_fmt = format!("{region_covered}/{region_total} ({region_rate_fmt})"); - + max_filename_fmt_width = max(max_filename_fmt_width, filename.len()); max_function_fmt_width = max(max_function_fmt_width, function_fmt.len()); max_line_fmt_width = max(max_line_fmt_width, line_fmt.len()); @@ -201,23 +246,38 @@ fn print_coverage_markdown_info(info: &Vec) { } let filename_sep: String = std::iter::repeat('-').take(max_filename_fmt_width).collect(); - let filename_space: String = std::iter::repeat(' ').take(max_filename_fmt_width - FILENAME_HEADER.len()).collect::(); + let filename_space: String = std::iter::repeat(' ') + .take(max_filename_fmt_width - FILENAME_HEADER.len()) + .collect::(); let function_sep: String = std::iter::repeat('-').take(max_function_fmt_width).collect(); - let function_space: String = std::iter::repeat(' ').take(max_function_fmt_width - FUNCTION_HEADER.len()).collect::(); + let function_space: String = std::iter::repeat(' ') + .take(max_function_fmt_width - FUNCTION_HEADER.len()) + .collect::(); let line_sep: String = std::iter::repeat('-').take(max_line_fmt_width).collect(); - let line_space: String = std::iter::repeat(' ').take(max_line_fmt_width - LINE_HEADER.len()).collect::(); + let line_space: String = + std::iter::repeat(' ').take(max_line_fmt_width - LINE_HEADER.len()).collect::(); let region_sep: String = std::iter::repeat('-').take(max_region_fmt_width).collect(); - let region_space: String = std::iter::repeat(' ').take(max_region_fmt_width - REGION_HEADER.len()).collect::(); + let region_space: String = + std::iter::repeat(' ').take(max_region_fmt_width - REGION_HEADER.len()).collect::(); let sep_row = format!("| {filename_sep} | {function_sep} | {line_sep} | {region_sep} |"); table_rows.push(format!("| {FILENAME_HEADER}{filename_space} | {FUNCTION_HEADER}{function_space} | {LINE_HEADER}{line_space} | {REGION_HEADER}{region_space} |")); table_rows.push(sep_row); for (filename, function_fmt, line_fmt, region_fmt) in data_rows { - let filename_space: String = std::iter::repeat(' ').take(max_filename_fmt_width - filename.len()).collect::(); - let function_space: String = std::iter::repeat(' ').take(max_function_fmt_width - function_fmt.len()).collect::(); - let line_space: String = std::iter::repeat(' ').take(max_line_fmt_width - line_fmt.len()).collect::(); - let region_space: String = std::iter::repeat(' ').take(max_region_fmt_width - region_fmt.len()).collect::(); - let cur_row = format!("| {filename}{filename_space} | {function_fmt}{function_space} | {line_fmt}{line_space} | {region_fmt}{region_space} |"); + let filename_space: String = std::iter::repeat(' ') + .take(max_filename_fmt_width - filename.len()) + .collect::(); + let function_space: String = std::iter::repeat(' ') + .take(max_function_fmt_width - function_fmt.len()) + .collect::(); + let line_space: String = + std::iter::repeat(' ').take(max_line_fmt_width - line_fmt.len()).collect::(); + let region_space: String = std::iter::repeat(' ') + .take(max_region_fmt_width - region_fmt.len()) + .collect::(); + let cur_row = format!( + "| {filename}{filename_space} | {function_fmt}{function_space} | {line_fmt}{line_space} | {region_fmt}{region_space} |" + ); table_rows.push(cur_row); } From 5b4d717b5aa2cb9519fcb2a734acb1d64e1bd117 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 17 Sep 2024 20:20:01 +0000 Subject: [PATCH 21/36] Simplify processing for markers --- tools/kani-cov/src/coverage.rs | 6 +++ tools/kani-cov/src/report.rs | 98 ++++++++++++++++++---------------- tools/kani-cov/src/summary.rs | 16 +++--- 3 files changed, 65 insertions(+), 55 deletions(-) diff --git a/tools/kani-cov/src/coverage.rs b/tools/kani-cov/src/coverage.rs index 2bc800ba80ad..2face345f768 100644 --- a/tools/kani-cov/src/coverage.rs +++ b/tools/kani-cov/src/coverage.rs @@ -206,3 +206,9 @@ pub fn function_coverage_results( let fun_results = file_results.iter().find(|(f, _)| *f == function); fun_results.cloned() } + +#[derive(Debug, Clone)] +pub enum MarkerInfo { + FullLine, + Markers(Vec<(u32, u32, u32)>), +} diff --git a/tools/kani-cov/src/report.rs b/tools/kani-cov/src/report.rs index ecbcbe8d2f2a..daff72d2a083 100644 --- a/tools/kani-cov/src/report.rs +++ b/tools/kani-cov/src/report.rs @@ -8,6 +8,7 @@ use anyhow::Result; use crate::coverage::{ function_coverage_results, function_info_from_file, CovResult, FileCoverageInfo, FunctionInfo, + MarkerInfo, }; use crate::summary::{line_coverage_info, line_coverage_results}; use crate::{args::ReportArgs, coverage::CombinedCoverageResults}; @@ -32,14 +33,13 @@ pub fn report_main(args: &ReportArgs) -> Result<()> { for info in fun_info { let cov_results = function_coverage_results(&info, &file, &results); let line_coverage = line_coverage_results(&info, &cov_results); - let line_coverage_matched: Vec<(usize, Option<(u32, Vec)>)> = + let line_coverage_matched: Vec<(usize, Option<(u32, MarkerInfo)>)> = (info.start.0..=info.end.0).zip(line_coverage.clone()).collect(); // println!("REG: {line_coverage:?}"); // println!("MATCHED: {line_coverage_matched:?}"); // let new_res = line_coverage_matched.into_iter().filter(|(num, data)| data.is_some()).collect(); file_cov_info.push(line_coverage_matched); } - // let file_coverage_results = match_line_coverage_file(file_cov_info); print_coverage_results(file, file_cov_info)?; } @@ -52,9 +52,9 @@ pub fn validate_report_args(_args: &ReportArgs) -> Result<()> { pub fn print_coverage_results( filepath: PathBuf, - results: Vec)>)>>, + results: Vec)>>, ) -> Result<()> { - let flattened_results: Vec<(usize, Option<(u32, Vec)>)> = + let flattened_results: Vec<(usize, Option<(u32, MarkerInfo)>)> = results.into_iter().flatten().collect(); println!("{}", filepath.to_string_lossy().to_string()); @@ -66,35 +66,46 @@ pub fn print_coverage_results( let idx = i + 1; let line = line?; let cur_line_result = flattened_results.iter().find(|(num, _)| *num == idx); - let max = if let Some((num, data)) = cur_line_result { - if data.is_some() { - format!("{:4}", data.clone().unwrap().0) + + let (max_times, line_fmt) = if let Some((_, span_data)) = cur_line_result { + if let Some((max, marker_info)) = span_data { + match marker_info { + MarkerInfo::FullLine => { + (Some(max), insert_escapes(&line, vec![(0, true), (line.len(), false)])) + } + MarkerInfo::Markers(markers) => + // Note: I'm not sure why we need to offset the columns by -1 + { + ( + Some(max), + insert_escapes( + &line, + markers + .iter() + .filter(|m| m.2 == 0) + .map(|m| { + vec![ + ((m.0 - 1) as usize, true), + ((m.1 - 1) as usize, false), + ] + }) + .flatten() + .collect(), + ), + ) + } + } } else { - format!("{:4}", " ".to_string()) + (None, line) } } else { - format!("{:4}", " ".to_string()) + (None, line) }; - let line_fmt = if max == " 0" { format!("{}{line}{}", "\x1b[42m", "\x1b[0m") } else {line}; - println!("{idx:4}| {max}| {line_fmt}"); - let differing_results: Vec = - if let Some((num, data)) = cur_line_result { if data.is_some() {data.clone().unwrap().1} else {vec![]} } else { vec![] }; - let zero_differing_results: Vec<&CovResult> = - differing_results.iter().filter(|x| x.times_covered == 0).collect(); - let mut str = std::iter::repeat(' ').take(11_usize).collect::(); - let mut cur_shift = 0; - let mut print_differing = false; - for res in zero_differing_results { - let start: usize = res.region.start.1.try_into().unwrap(); - let spaces_next = std::iter::repeat(' ').take(start - cur_shift).collect::(); - str.push_str(&format!("{spaces_next}^0")); - cur_shift += start + 2; - print_differing = true; - // res.region.start - } - if print_differing { - println!("{str}"); - } + + let max_fmt = + if let Some(num) = max_times { format!("{num:4}") } else { format!("{:4}", " ") }; + + println!("{idx:4}| {max_fmt}| {line_fmt}"); } Ok(()) @@ -176,25 +187,20 @@ pub fn print_coverage_results( // 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 -// } +fn insert_escapes(str: &String, markers: Vec<(usize, bool)>) -> String { + let mut new_str = str.clone(); + let mut offset = 0; -fn red() -> String { let support_color = std::io::stdout().is_terminal(); - if support_color { - "\x1b[42m".to_string() + let sym_markers: Vec<(&usize, &str)> = if support_color { + markers.iter().map(|(i, b)| (i, if *b { "\x1b[41m" } else { "\x1b[0m" })).collect() } else { - "```".to_string() + markers.iter().map(|(i, b)| (i, if *b { "```" } else { "'''" })).collect() + }; + for (i, b) in sym_markers { + // println!("{}", i + offset); + new_str.insert_str(i + offset, b); + offset = offset + b.bytes().len(); } + new_str } diff --git a/tools/kani-cov/src/summary.rs b/tools/kani-cov/src/summary.rs index ea0c1c33c894..862e361cfdd5 100644 --- a/tools/kani-cov/src/summary.rs +++ b/tools/kani-cov/src/summary.rs @@ -9,7 +9,7 @@ use crate::{ args::{SummaryArgs, SummaryFormat}, coverage::{ function_coverage_results, function_info_from_file, CombinedCoverageResults, CovResult, - CoverageMetric, CoverageRegion, FileCoverageInfo, FunctionInfo, + CoverageMetric, CoverageRegion, FileCoverageInfo, FunctionInfo, MarkerInfo, }, }; @@ -96,7 +96,7 @@ pub fn validate_summary_args(_args: &SummaryArgs) -> Result<()> { pub fn line_coverage_results( info: &FunctionInfo, fun_results: &Option<(String, Vec)>, -) -> Vec)>> { +) -> Vec> { let start_line: u32 = info.start.0.try_into().unwrap(); let end_line: u32 = info.end.0.try_into().unwrap(); // `line_status` represents all the lines between `start_line` and @@ -106,7 +106,7 @@ pub fn line_coverage_results( // - `Some(max, other)`, where `max` represents the maximum number of times // the line was covered by any coverage result, and `other` specifies the // coverage results that don't amount to the maximum. - let mut line_status: Vec)>> = + let mut line_status: Vec> = Vec::with_capacity((end_line - start_line + 1).try_into().unwrap()); if let Some(res) = fun_results { @@ -134,20 +134,18 @@ pub fn line_coverage_results( .max_by_key(|obj| obj.times_covered) .map(|obj| obj.times_covered) .unwrap_or(0); - let other_covered: Vec = line_results + let markers: Vec<(u32, u32, u32)> = line_results .iter() - .filter(|obj| obj.times_covered != max_covered) - .cloned() + .map(|obj| (obj.region.start.1, obj.region.end.1, obj.times_covered)) .collect(); - line_status.push(Some((max_covered, other_covered))); + line_status.push(Some((max_covered, MarkerInfo::Markers(markers)))); } } } else { - line_status = std::iter::repeat(Some((0, vec![]))) + line_status = std::iter::repeat(Some((0, MarkerInfo::FullLine))) .take((end_line - start_line + 1).try_into().unwrap()) .collect(); } - println!("{line_status:?}"); line_status } From e1d0160479f00446e6e9ff65777a5d17e216d709 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 17 Sep 2024 20:20:23 +0000 Subject: [PATCH 22/36] Remove some formatting code that's not needed anymore --- tools/kani-cov/src/report.rs | 76 ------------------------------------ 1 file changed, 76 deletions(-) diff --git a/tools/kani-cov/src/report.rs b/tools/kani-cov/src/report.rs index daff72d2a083..e350d1cf4d11 100644 --- a/tools/kani-cov/src/report.rs +++ b/tools/kani-cov/src/report.rs @@ -110,82 +110,6 @@ pub fn print_coverage_results( Ok(()) } -// fn match_line_coverage_file(line_cov_info: Vec<(FunctionInfo, Vec)>) -> ?? { -// } -// fn visualize_coverage_results(cov_results: &CoverageResults, root_path: PathBuf) -> Result { -// 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 { -// 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(); From 6d47c0bdd4f628e57728332955fb26dd2608e742 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 17 Sep 2024 20:22:04 +0000 Subject: [PATCH 23/36] Remove leftover debugging info --- tools/kani-cov/src/report.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/tools/kani-cov/src/report.rs b/tools/kani-cov/src/report.rs index e350d1cf4d11..9f95fc080c12 100644 --- a/tools/kani-cov/src/report.rs +++ b/tools/kani-cov/src/report.rs @@ -61,7 +61,6 @@ pub fn print_coverage_results( let file = File::open(filepath)?; let reader = BufReader::new(file); - println!("{flattened_results:?}"); for (i, line) in reader.lines().enumerate() { let idx = i + 1; let line = line?; From ae48e21c4c69da6b6b68569dd4f938869fec3a65 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 19 Sep 2024 16:15:29 +0000 Subject: [PATCH 24/36] Complete terminal highlight algorithm --- tools/kani-cov/src/coverage.rs | 2 +- tools/kani-cov/src/report.rs | 129 +++++++++++++++++++++++++++------ tools/kani-cov/src/summary.rs | 6 +- 3 files changed, 109 insertions(+), 28 deletions(-) diff --git a/tools/kani-cov/src/coverage.rs b/tools/kani-cov/src/coverage.rs index 2face345f768..78238cdee208 100644 --- a/tools/kani-cov/src/coverage.rs +++ b/tools/kani-cov/src/coverage.rs @@ -210,5 +210,5 @@ pub fn function_coverage_results( #[derive(Debug, Clone)] pub enum MarkerInfo { FullLine, - Markers(Vec<(u32, u32, u32)>), + Markers(Vec), } diff --git a/tools/kani-cov/src/report.rs b/tools/kani-cov/src/report.rs index 9f95fc080c12..16c960bd223e 100644 --- a/tools/kani-cov/src/report.rs +++ b/tools/kani-cov/src/report.rs @@ -35,9 +35,6 @@ pub fn report_main(args: &ReportArgs) -> Result<()> { let line_coverage = line_coverage_results(&info, &cov_results); let line_coverage_matched: Vec<(usize, Option<(u32, MarkerInfo)>)> = (info.start.0..=info.end.0).zip(line_coverage.clone()).collect(); - // println!("REG: {line_coverage:?}"); - // println!("MATCHED: {line_coverage_matched:?}"); - // let new_res = line_coverage_matched.into_iter().filter(|(num, data)| data.is_some()).collect(); file_cov_info.push(line_coverage_matched); } print_coverage_results(file, file_cov_info)?; @@ -61,9 +58,54 @@ pub fn print_coverage_results( let file = File::open(filepath)?; let reader = BufReader::new(file); + let mut must_highlight = false; + for (i, line) in reader.lines().enumerate() { let idx = i + 1; let line = line?; + + // 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) + // }; let cur_line_result = flattened_results.iter().find(|(num, _)| *num == idx); let (max_times, line_fmt) = if let Some((_, span_data)) = cur_line_result { @@ -72,33 +114,75 @@ pub fn print_coverage_results( MarkerInfo::FullLine => { (Some(max), insert_escapes(&line, vec![(0, true), (line.len(), false)])) } - MarkerInfo::Markers(markers) => + MarkerInfo::Markers(results) => // Note: I'm not sure why we need to offset the columns by -1 { + // Filter out cases where the span is a single unit AND it ends after the line + let results: Vec<&CovResult> = results.into_iter().filter(|m| if m.region.start.0 as usize == idx && m.region.end.0 as usize == idx { (m.region.end.1 - m.region.start.1 != 1) && (m.region.end.1 as usize) < line.len() } else {true }).collect(); + let mut complete_escapes: Vec<(usize, bool)> = results + .iter() + .filter(|m| m.times_covered == 0 && m.region.start.0 as usize == idx && m.region.end.0 as usize == idx) + .map(|m| { + vec![ + ((m.region.start.1 - 1) as usize, true), + ((m.region.end.1 - 1) as usize, false), + ] + }) + .flatten() + .collect(); + // println!("COMPLETE: {complete_escapes:?}"); + let mut starting_escapes: Vec<(usize, bool)> = results + .iter() + .filter(|m| m.times_covered == 0 && m.region.start.0 as usize == idx && m.region.end.0 as usize != idx) + .map(|m| { + vec![ + ((m.region.start.1 - 1) as usize, true), + ] + }) + .flatten() + .collect(); + // println!("{starting_escapes:?}"); + let mut ending_escapes: Vec<(usize, bool)> = results + .iter() + .filter(|m| m.times_covered == 0 && m.region.start.0 as usize != idx && m.region.end.0 as usize == idx) + .map(|m| { + vec![ + ((m.region.end.1 - 1) as usize, false), + ] + }) + .flatten() + .collect(); + + // println!("{starting_escapes:?}"); + // println!("{ending_escapes:?}"); + if must_highlight && ending_escapes.len() > 0 { + ending_escapes.push((0_usize, true)); + must_highlight = false; + } + if starting_escapes.len() > 0 { + starting_escapes.push((line.len(), false)); + must_highlight = true; + } + + ending_escapes.extend(complete_escapes); + ending_escapes.extend(starting_escapes); + + if must_highlight && ending_escapes.is_empty() { + ending_escapes.push((0, true)); + ending_escapes.push((line.len(), false)); + } + ( Some(max), - insert_escapes( - &line, - markers - .iter() - .filter(|m| m.2 == 0) - .map(|m| { - vec![ - ((m.0 - 1) as usize, true), - ((m.1 - 1) as usize, false), - ] - }) - .flatten() - .collect(), - ), + insert_escapes(&line, ending_escapes) ) } } } else { - (None, line) + (None, if !must_highlight { line } else {insert_escapes(&line, vec![(0, true), (line.len(), false)])}) } } else { - (None, line) + (None, if !must_highlight { line } else {insert_escapes(&line, vec![(0, true), (line.len(), false)])}) }; let max_fmt = @@ -115,13 +199,14 @@ fn insert_escapes(str: &String, markers: Vec<(usize, bool)>) -> String { let mut offset = 0; let support_color = std::io::stdout().is_terminal(); - let sym_markers: Vec<(&usize, &str)> = if support_color { + let mut sym_markers: Vec<(&usize, &str)> = if support_color { markers.iter().map(|(i, b)| (i, if *b { "\x1b[41m" } else { "\x1b[0m" })).collect() } else { markers.iter().map(|(i, b)| (i, if *b { "```" } else { "'''" })).collect() }; + // Sorting + sym_markers.sort(); for (i, b) in sym_markers { - // println!("{}", i + offset); new_str.insert_str(i + offset, b); offset = offset + b.bytes().len(); } diff --git a/tools/kani-cov/src/summary.rs b/tools/kani-cov/src/summary.rs index 862e361cfdd5..23f260073af8 100644 --- a/tools/kani-cov/src/summary.rs +++ b/tools/kani-cov/src/summary.rs @@ -134,11 +134,7 @@ pub fn line_coverage_results( .max_by_key(|obj| obj.times_covered) .map(|obj| obj.times_covered) .unwrap_or(0); - let markers: Vec<(u32, u32, u32)> = line_results - .iter() - .map(|obj| (obj.region.start.1, obj.region.end.1, obj.times_covered)) - .collect(); - line_status.push(Some((max_covered, MarkerInfo::Markers(markers)))); + line_status.push(Some((max_covered, MarkerInfo::Markers(line_results)))); } } } else { From 8c79bafa4c33b87b30dda8b30cd1dacb7081ef34 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 19 Sep 2024 17:38:31 +0000 Subject: [PATCH 25/36] Change `coverage` mode to get `kani-cov` reports --- tools/compiletest/src/runtest.rs | 63 +++++++++++++++++++++++++++++++- 1 file changed, 61 insertions(+), 2 deletions(-) diff --git a/tools/compiletest/src/runtest.rs b/tools/compiletest/src/runtest.rs index c8387c691296..f5b9bc826fb5 100644 --- a/tools/compiletest/src/runtest.rs +++ b/tools/compiletest/src/runtest.rs @@ -412,10 +412,69 @@ impl<'test> TestCx<'test> { /// Runs Kani in coverage mode on the test file specified by `self.testpaths.file`. fn run_expected_coverage_test(&self) { let proc_res = self.run_kani_with_coverage(); + let cov_results_path = self.extract_cov_results_path(&proc_res); + let (kanimap, kaniraws, kanicov) = self.find_cov_files(&cov_results_path); + let kanicov_proc = self.run_kanicov_report(&kanimap, &kaniraws, &kanicov); let expected_path = self.testpaths.file.parent().unwrap().join("expected"); - self.verify_output(&proc_res, &expected_path); + self.verify_output(&kanicov_proc, &expected_path); + } + + fn run_kanicov_report(&self, kanimap: &PathBuf, kaniraws: &Vec, kanicov: &PathBuf) -> ProcRes { + let mut kanicov_merge = Command::new("kani-cov"); + kanicov_merge.arg("merge"); + kanicov_merge.args(kaniraws); + kanicov_merge.arg("--output"); + kanicov_merge.arg(kanicov); + let merge_cmd = self.compose_and_run(kanicov_merge); + + if !merge_cmd.status.success() { + self.fatal_proc_rec( + "test failed: could not run `kani-cov merge` command", + &merge_cmd, + ); + } + + let mut kanicov_report = Command::new("kani-cov"); + kanicov_report.arg("report").arg(kanimap).arg("--profile").arg(kanicov); + let report_cmd = self.compose_and_run(kanicov_report); + + if !report_cmd.status.success() { + self.fatal_proc_rec( + "test failed: could not run `kani-cov report` command", + &report_cmd, + ); + } + report_cmd } + fn find_cov_files(&self, folder_path: &PathBuf) -> (PathBuf, Vec, PathBuf) { + let folder_name = folder_path.file_name().unwrap(); + let kanimap = folder_path.join(format!("{}_kanimap.json", folder_name.to_string_lossy())); + + let kanicov = folder_path.join(format!("{}_kanicov.json", folder_name.to_string_lossy())); + + let kaniraw_glob = format!("{}/*_kaniraw.json", folder_path.display()); + // self.error(&format!("kaniraw_glob: {kaniraw_glob}")); + let kaniraws: Vec = glob::glob(&kaniraw_glob) + .expect("Failed to read glob pattern") + .filter_map(|entry| entry.ok()) + .collect(); + + (kanimap, kaniraws, kanicov) + } + + fn extract_cov_results_path(&self, proc_res: &ProcRes) -> PathBuf { + let output_lines = proc_res.stdout.split('\n').collect::>(); + let coverage_info = output_lines.iter().find(|l| l.contains("Coverage results saved to")); + if coverage_info.is_none() { + self.fatal_proc_rec( + &format!( + "failed to find the path to the coverage results!"), + proc_res); + } + let coverage_path = coverage_info.unwrap().split(' ').last().unwrap(); + PathBuf::from(coverage_path) + } /// Runs Kani with stub implementations of various data structures. /// Currently, it only runs tests for the Vec module with the (Kani)Vec /// abstraction. At a later stage, it should be possible to add command-line @@ -511,7 +570,7 @@ impl<'test> TestCx<'test> { pub struct ProcRes { status: ExitStatus, - stdout: String, + pub stdout: String, stderr: String, cmdline: String, } From 39f5ac295e126ebb5165ec8ee05e43be97c0ed5a Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 19 Sep 2024 17:49:12 +0000 Subject: [PATCH 26/36] Bless expected files --- tests/coverage/abort/expected | 35 +++++--- tests/coverage/assert/expected | 28 +++++-- tests/coverage/assert_eq/expected | 20 +++-- tests/coverage/assert_ne/expected | 24 ++++-- tests/coverage/break/expected | 33 +++++--- tests/coverage/compare/expected | 28 ++++--- tests/coverage/contradiction/expected | 24 ++++-- tests/coverage/debug-assert/expected | 26 +++--- tests/coverage/div-zero/expected | 21 +++-- tests/coverage/early-return/expected | 32 +++++--- tests/coverage/if-statement-multi/expected | 38 ++++++--- tests/coverage/if-statement/expected | 35 ++++---- .../assert_uncovered_end/expected | 24 ++++-- .../known_issues/assume_assert/expected | 20 ++++- .../known_issues/out-of-bounds/expected | 23 ++++-- tests/coverage/known_issues/variant/expected | 47 +++++++---- tests/coverage/multiple-harnesses/expected | 82 ++++++++++--------- tests/coverage/overflow-failure/expected | 25 ++++-- .../coverage/overflow-full-coverage/expected | 27 ++++-- tests/coverage/while-loop-break/expected | 37 ++++++--- 20 files changed, 399 insertions(+), 230 deletions(-) diff --git a/tests/coverage/abort/expected b/tests/coverage/abort/expected index 91142ebf94fc..0570f1e3f710 100644 --- a/tests/coverage/abort/expected +++ b/tests/coverage/abort/expected @@ -1,13 +1,22 @@ -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 +/home/ubuntu/kani/tests/coverage/abort/main.rs + 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| | } diff --git a/tests/coverage/assert/expected b/tests/coverage/assert/expected index 46bb664cf6f5..e066d470cd9b 100644 --- a/tests/coverage/assert/expected +++ b/tests/coverage/assert/expected @@ -1,9 +1,19 @@ -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 +/home/ubuntu/kani/tests/coverage/assert/test.rs + 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| | } diff --git a/tests/coverage/assert_eq/expected b/tests/coverage/assert_eq/expected index c2eee7adf803..7d5a91d46771 100644 --- a/tests/coverage/assert_eq/expected +++ b/tests/coverage/assert_eq/expected @@ -1,8 +1,12 @@ -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 +/home/ubuntu/kani/tests/coverage/assert_eq/test.rs + 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| | } diff --git a/tests/coverage/assert_ne/expected b/tests/coverage/assert_ne/expected index c9b727da0f82..d29a77afeb5f 100644 --- a/tests/coverage/assert_ne/expected +++ b/tests/coverage/assert_ne/expected @@ -1,9 +1,15 @@ -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 +/home/ubuntu/kani/tests/coverage/assert_ne/test.rs + 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| | } diff --git a/tests/coverage/break/expected b/tests/coverage/break/expected index 739735cdf1a2..aca305b0f411 100644 --- a/tests/coverage/break/expected +++ b/tests/coverage/break/expected @@ -1,13 +1,20 @@ -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 +/home/ubuntu/kani/tests/coverage/break/main.rs + 1| | // Copyright Kani Contributors + 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT + 3| | + 4| 2| fn find_positive(nums: &[i32]) -> Option { + 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| | } diff --git a/tests/coverage/compare/expected b/tests/coverage/compare/expected index 153dbfa37d80..fc776f1cd4ea 100644 --- a/tests/coverage/compare/expected +++ b/tests/coverage/compare/expected @@ -1,11 +1,17 @@ -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 +/home/ubuntu/kani/tests/coverage/compare/main.rs + 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| | } diff --git a/tests/coverage/contradiction/expected b/tests/coverage/contradiction/expected index db3676d7da15..5acc7f5c7d4d 100644 --- a/tests/coverage/contradiction/expected +++ b/tests/coverage/contradiction/expected @@ -1,9 +1,15 @@ -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 +/home/ubuntu/kani/tests/coverage/contradiction/main.rs + 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| | } diff --git a/tests/coverage/debug-assert/expected b/tests/coverage/debug-assert/expected index fbe57690d347..7ce531204090 100644 --- a/tests/coverage/debug-assert/expected +++ b/tests/coverage/debug-assert/expected @@ -1,10 +1,16 @@ -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 +/home/ubuntu/kani/tests/coverage/debug-assert/main.rs + 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| | } diff --git a/tests/coverage/div-zero/expected b/tests/coverage/div-zero/expected index f351005f4f22..a5a7f94c83fd 100644 --- a/tests/coverage/div-zero/expected +++ b/tests/coverage/div-zero/expected @@ -1,9 +1,12 @@ -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 +/home/ubuntu/kani/tests/coverage/div-zero/test.rs + 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| | } diff --git a/tests/coverage/early-return/expected b/tests/coverage/early-return/expected index 53cde3abeaf8..9cb66a254204 100644 --- a/tests/coverage/early-return/expected +++ b/tests/coverage/early-return/expected @@ -1,12 +1,20 @@ -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 +/home/ubuntu/kani/tests/coverage/early-return/main.rs + 1| | // Copyright Kani Contributors + 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT + 3| | + 4| 2| fn find_index(nums: &[i32], target: i32) -> Option { + 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| | } diff --git a/tests/coverage/if-statement-multi/expected b/tests/coverage/if-statement-multi/expected index 4e8382d10a6f..ee486c9b8975 100644 --- a/tests/coverage/if-statement-multi/expected +++ b/tests/coverage/if-statement-multi/expected @@ -1,11 +1,27 @@ -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 +/home/ubuntu/kani/tests/coverage/if-statement-multi/test.rs + 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: + 11| | + 12| 0| ```fn _other_function() {''' + 13| 0| ``` println!("Hello, world!");''' + 14| 0| ```}''' + 15| | + 16| 2| fn test_cov(val: u32) -> bool { + 17| 2| if val < 3 || ```val == 42''' { true } else { ```false''' } + 18| | } + 19| | + 20| | #[cfg_attr(kani, kani::proof)] + 21| 2| fn main() { + 22| 2| let test1 = test_cov(1); + 23| 2| let test2 = test_cov(2); + 24| 2| assert!(test1); + 25| 2| assert!(test2); + 26| | } diff --git a/tests/coverage/if-statement/expected b/tests/coverage/if-statement/expected index b85b95de9c84..fd1dd049975d 100644 --- a/tests/coverage/if-statement/expected +++ b/tests/coverage/if-statement/expected @@ -1,14 +1,21 @@ -Source-based code coverage results: - -main.rs (check_number)\ - * 4:1 - 5:15 COVERED\ - * 7:12 - 7:24 COVERED\ - * 7:27 - 7:46 UNCOVERED\ - * 7:56 - 7:74 COVERED\ - * 8:15 - 8:22 UNCOVERED\ - * 9:9 - 9:19 UNCOVERED\ - * 11:9 - 11:15 UNCOVERED\ - * 13:1 - 13:2 COVERED - -main.rs (main)\ - * 16:1 - 20:2 COVERED +/home/ubuntu/kani/tests/coverage/if-statement/main.rs + 1| | // Copyright Kani Contributors + 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT + 3| | + 4| 2| fn check_number(num: i32) -> &'static str { + 5| 2| if num > 0 { + 6| | // The next line is partially covered + 7| 2| if num % 2 == 0 { ```"Positive and Even"''' } else { "Positive and Odd" } + 8| 0| } else if ```num < 0''' { + 9| 0| "Negative" + 10| | } else { + 11| 0| "Zero" + 12| | } + 13| | } + 14| | + 15| | #[kani::proof] + 16| 2| fn main() { + 17| 2| let number = 7; + 18| 2| let result = check_number(number); + 19| 2| assert_eq!(result, "Positive and Odd"); + 20| | } diff --git a/tests/coverage/known_issues/assert_uncovered_end/expected b/tests/coverage/known_issues/assert_uncovered_end/expected index ceba065ce424..58d4ed5475a7 100644 --- a/tests/coverage/known_issues/assert_uncovered_end/expected +++ b/tests/coverage/known_issues/assert_uncovered_end/expected @@ -1,9 +1,15 @@ -Source-based code coverage results: - -test.rs (check_assert)\ - * 9:1 - 10:34 COVERED\ - * 11:14 - 13:6 COVERED\ - * 13:6 - 13:7 UNCOVERED - -test.rs (check_assert::{closure#0})\ - * 10:40 - 10:49 COVERED +/home/ubuntu/kani/tests/coverage/known_issues/assert_uncovered_end/test.rs + 1| | // Copyright Kani Contributors + 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT + 3| | + 4| | //! Checks that `check_assert` is fully covered. At present, the coverage for + 5| | //! this test reports an uncovered single-column region at the end of the `if` + 6| | //! statement: + 7| | + 8| | #[kani::proof] + 9| 2| fn check_assert() { + 10| 2| let x: u32 = kani::any_where(|val| *val == 5); + 11| 2| if x > 3 { + 12| 2| assert!(x > 4); + 13| 2| } + 14| | } diff --git a/tests/coverage/known_issues/assume_assert/expected b/tests/coverage/known_issues/assume_assert/expected index 55f3235d7d24..90d75e5c3026 100644 --- a/tests/coverage/known_issues/assume_assert/expected +++ b/tests/coverage/known_issues/assume_assert/expected @@ -1,4 +1,16 @@ -Source-based code coverage results: - -main.rs (check_assume_assert)\ - * 11:1 - 15:2 COVERED +/home/ubuntu/kani/tests/coverage/known_issues/assume_assert/main.rs + 1| | // Copyright Kani Contributors + 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT + 3| | + 4| | //! This test should check that the region after `kani::assume(false)` is + 5| | //! `UNCOVERED`. However, due to a technical limitation in `rustc`'s coverage + 6| | //! instrumentation, only one `COVERED` region is reported for the whole + 7| | //! function. More details in + 8| | //! . + 9| | + 10| | #[kani::proof] + 11| 2| fn check_assume_assert() { + 12| 2| let a: u8 = kani::any(); + 13| 2| kani::assume(false); + 14| 2| assert!(a < 5); + 15| | } diff --git a/tests/coverage/known_issues/out-of-bounds/expected b/tests/coverage/known_issues/out-of-bounds/expected index 8ab9e2e15627..d3ee28dff909 100644 --- a/tests/coverage/known_issues/out-of-bounds/expected +++ b/tests/coverage/known_issues/out-of-bounds/expected @@ -1,7 +1,16 @@ -Source-based code coverage results: - -test.rs (get)\ - * 8:1 - 10:2 COVERED - -test.rs (main)\ - * 13:1 - 15:2 COVERED +/home/ubuntu/kani/tests/coverage/known_issues/out-of-bounds/test.rs + 1| | // Copyright Kani Contributors + 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT + 3| | + 4| | //! This test should check that the return in `get` is `UNCOVERED`. However, the + 5| | //! coverage results currently report that the whole function is `COVERED`, + 6| | //! likely due to + 7| | + 8| 2| fn get(s: &[i16], index: usize) -> i16 { + 9| 2| s[index] + 10| | } + 11| | + 12| | #[kani::proof] + 13| 2| fn main() { + 14| 2| get(&[7, -83, 19], 15); + 15| | } diff --git a/tests/coverage/known_issues/variant/expected b/tests/coverage/known_issues/variant/expected index 13383ed3bab0..37e7a9b61d15 100644 --- a/tests/coverage/known_issues/variant/expected +++ b/tests/coverage/known_issues/variant/expected @@ -1,14 +1,33 @@ -Source-based code coverage results: - -main.rs (main)\ - * 29:1 - 32:2 COVERED - -main.rs (print_direction)\ - * 16:1 - 16:36 COVERED\ - * 18:11 - 18:14 UNCOVERED\ - * 19:26 - 19:47 UNCOVERED\ - * 20:28 - 20:51 UNCOVERED\ - * 21:28 - 21:51 COVERED\ - * 22:34 - 22:63 UNCOVERED\ - * 24:14 - 24:45 UNCOVERED\ - * 26:1 - 26:2 COVERED +/home/ubuntu/kani/tests/coverage/known_issues/variant/main.rs + 1| | // Copyright Kani Contributors + 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT + 3| | + 4| | //! Checks coverage results in an example with a `match` statement matching on + 5| | //! all enum variants. Currently, it does not yield the expected results because + 6| | //! it reports the `dir` in the match statement as `UNCOVERED`: + 7| | //! + 8| | + 9| | enum Direction { + 10| | Up, + 11| | Down, + 12| | Left, + 13| | Right, + 14| | } + 15| | + 16| 2| fn print_direction(dir: Direction) { + 17| | // For some reason, `dir`'s span is reported as `UNCOVERED` too + 18| 0| match ```dir''' { + 19| 0| Direction::Up => println!("Going up!"), + 20| 0| Direction::Down => println!("Going down!"), + 21| 2| Direction::Left => println!("Going left!"), + 22| 0| Direction::Right if 1 == 1 => println!("Going right!"), + 23| | // This part is unreachable since we cover all variants in the match. + 24| 0| _ => println!("Not going anywhere!"), + 25| | } + 26| | } + 27| | + 28| | #[kani::proof] + 29| 2| fn main() { + 30| 2| let direction = Direction::Left; + 31| 2| print_direction(direction); + 32| | } diff --git a/tests/coverage/multiple-harnesses/expected b/tests/coverage/multiple-harnesses/expected index b5362147fed1..58176fc4dca3 100644 --- a/tests/coverage/multiple-harnesses/expected +++ b/tests/coverage/multiple-harnesses/expected @@ -1,37 +1,45 @@ -Source-based code coverage results: - -main.rs (estimate_size)\ - * 4:1 - 7:15 COVERED\ - * 8:12 - 8:19 COVERED\ - * 9:20 - 9:21 COVERED\ - * 11:20 - 11:21 COVERED\ - * 13:15 - 13:23 COVERED\ - * 14:12 - 14:20 COVERED\ - * 15:20 - 15:21 COVERED\ - * 17:20 - 17:21 COVERED\ - * 20:12 - 20:20 COVERED\ - * 21:20 - 21:21 COVERED\ - * 23:20 - 23:21 COVERED\ - * 26:1 - 26:2 COVERED - -main.rs (fully_covered)\ - * 39:1 - 44:2 COVERED - -Source-based code coverage results: - -main.rs (estimate_size)\ - * 4:1 - 7:15 COVERED\ - * 8:12 - 8:19 COVERED\ - * 9:20 - 9:21 COVERED\ - * 11:20 - 11:21 COVERED\ - * 13:15 - 13:23 COVERED\ - * 14:12 - 14:20 COVERED\ - * 15:20 - 15:21 COVERED\ - * 17:20 - 17:21 COVERED\ - * 20:12 - 20:20 COVERED\ - * 21:20 - 21:21 COVERED\ - * 23:20 - 23:21 UNCOVERED\ - * 26:1 - 26:2 COVERED - -main.rs (mostly_covered)\ - * 30:1 - 35:2 COVERED +/home/ubuntu/kani/tests/coverage/multiple-harnesses/main.rs + 1| | // Copyright Kani Contributors + 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT + 3| | + 4| 3| fn estimate_size(x: u32) -> u32 { + 5| 3| assert!(x < 4096); + 6| 3| + 7| 3| if x < 256 { + 8| 3| if x < 128 { + 9| 3| return 1; + 10| | } else { + 11| 3| return 3; + 12| | } + 13| 3| } else if x < 1024 { + 14| 3| if x > 1022 { + 15| 3| return 4; + 16| | } else { + 17| 3| return 5; + 18| | } + 19| | } else { + 20| 3| if x < 2048 { + 21| 3| return 7; + 22| | } else { + 23| 2| return 9; + 24| | } + 25| | } + 26| | } + 27| | + 28| | #[cfg(kani)] + 29| | #[kani::proof] + 30| 2| fn mostly_covered() { + 31| 2| let x: u32 = kani::any(); + 32| 2| kani::assume(x < 2048); + 33| 2| let y = estimate_size(x); + 34| 2| assert!(y < 10); + 35| | } + 36| | + 37| | #[cfg(kani)] + 38| | #[kani::proof] + 39| 2| fn fully_covered() { + 40| 2| let x: u32 = kani::any(); + 41| 2| kani::assume(x < 4096); + 42| 2| let y = estimate_size(x); + 43| 2| assert!(y < 10); + 44| | } diff --git a/tests/coverage/overflow-failure/expected b/tests/coverage/overflow-failure/expected index db4f29d51336..cc07742f3070 100644 --- a/tests/coverage/overflow-failure/expected +++ b/tests/coverage/overflow-failure/expected @@ -1,9 +1,16 @@ -Source-based code coverage results: - -test.rs (cond_reduce)\ - * 7:1 - 8:18 COVERED\ - * 8:21 - 8:27 COVERED\ - * 8:37 - 8:38 UNCOVERED - -test.rs (main)\ - * 12:1 - 15:2 COVERED +/home/ubuntu/kani/tests/coverage/overflow-failure/test.rs + 1| | // Copyright Kani Contributors + 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT + 3| | + 4| | //! Checks that Kani reports the correct coverage results in the case of an + 5| | //! arithmetic overflow failure (caused by the second call to `cond_reduce`). + 6| | + 7| 2| fn cond_reduce(thresh: u32, x: u32) -> u32 { + 8| 2| if x > thresh { x - 50 } else { x } + 9| | } + 10| | + 11| | #[kani::proof] + 12| 2| fn main() { + 13| 2| cond_reduce(60, 70); + 14| 2| cond_reduce(40, 42); + 15| | } diff --git a/tests/coverage/overflow-full-coverage/expected b/tests/coverage/overflow-full-coverage/expected index 4d17761505eb..7f666b5571f7 100644 --- a/tests/coverage/overflow-full-coverage/expected +++ b/tests/coverage/overflow-full-coverage/expected @@ -1,9 +1,18 @@ -Source-based code coverage results: - -test.rs (main)\ - * 12:1 - 17:2 COVERED - -test.rs (reduce)\ - * 7:1 - 8:16 COVERED\ - * 8:19 - 8:27 COVERED\ - * 8:37 - 8:38 COVERED +/home/ubuntu/kani/tests/coverage/overflow-full-coverage/test.rs + 1| | // Copyright Kani Contributors + 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT + 3| | + 4| | //! Checks that Kani reports all regions as `COVERED` as expected in this case + 5| | //! where arithmetic overflow failures are prevented. + 6| | + 7| 2| fn reduce(x: u32) -> u32 { + 8| 2| if x > 1000 { x - 1000 } else { x } + 9| | } + 10| | + 11| | #[kani::proof] + 12| 2| fn main() { + 13| 2| reduce(7); + 14| 2| reduce(33); + 15| 2| reduce(728); + 16| 2| reduce(1079); + 17| | } diff --git a/tests/coverage/while-loop-break/expected b/tests/coverage/while-loop-break/expected index 34afef9ee12c..574875ac558b 100644 --- a/tests/coverage/while-loop-break/expected +++ b/tests/coverage/while-loop-break/expected @@ -1,13 +1,24 @@ -Source-based code coverage results: - -main.rs (find_first_negative)\ - * 7:1 - 8:22 COVERED\ - * 9:11 - 9:29 COVERED\ - * 10:12 - 10:27 COVERED\ - * 11:20 - 11:37 COVERED\ - * 12:10 - 13:19 COVERED\ - * 15:5 - 15:9 UNCOVERED\ - * 16:1 - 16:2 COVERED - -main.rs (main)\ - * 19:1 - 23:2 COVERED +/home/ubuntu/kani/tests/coverage/while-loop-break/main.rs + 1| | // Copyright Kani Contributors + 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT + 3| | + 4| | //! Checks coverage results in an example with a `while` loop that returns before + 5| | //! running the last iteration. + 6| | + 7| 2| fn find_first_negative(nums: &[i32]) -> Option { + 8| 2| let mut index = 0; + 9| 2| while index < nums.len() { + 10| 2| if nums[index] < 0 { + 11| 2| return Some(nums[index]); + 12| 2| } + 13| 2| index += 1; + 14| | } + 15| 0| None + 16| | } + 17| | + 18| | #[kani::proof] + 19| 2| fn main() { + 20| 2| let numbers = [1, 2, -3, 4, -5]; + 21| 2| let result = find_first_negative(&numbers); + 22| 2| assert_eq!(result, Some(-3)); + 23| | } From 778816a437656ec090e5fdc3b100c5b4f1d06e99 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 19 Sep 2024 17:54:51 +0000 Subject: [PATCH 27/36] Complete blessing for `coverage` tests --- tests/coverage/abort/expected | 43 +++++---- tests/coverage/assert/expected | 37 ++++---- tests/coverage/assert_eq/expected | 23 +++-- tests/coverage/assert_ne/expected | 29 +++--- tests/coverage/break/expected | 39 ++++---- tests/coverage/compare/expected | 33 ++++--- tests/coverage/contradiction/expected | 29 +++--- tests/coverage/debug-assert/expected | 31 ++++--- tests/coverage/div-zero/expected | 23 +++-- tests/coverage/early-return/expected | 39 ++++---- tests/coverage/if-statement-multi/expected | 53 ++++++----- tests/coverage/if-statement/expected | 41 +++++---- tests/coverage/multiple-harnesses/expected | 89 +++++++++---------- tests/coverage/overflow-failure/expected | 31 ++++--- .../coverage/overflow-full-coverage/expected | 35 ++++---- tests/coverage/while-loop-break/expected | 47 +++++----- 16 files changed, 303 insertions(+), 319 deletions(-) diff --git a/tests/coverage/abort/expected b/tests/coverage/abort/expected index 0570f1e3f710..a5df4acee287 100644 --- a/tests/coverage/abort/expected +++ b/tests/coverage/abort/expected @@ -1,22 +1,21 @@ -/home/ubuntu/kani/tests/coverage/abort/main.rs - 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| | } + 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| | }\ diff --git a/tests/coverage/assert/expected b/tests/coverage/assert/expected index e066d470cd9b..8825a53c0d07 100644 --- a/tests/coverage/assert/expected +++ b/tests/coverage/assert/expected @@ -1,19 +1,18 @@ -/home/ubuntu/kani/tests/coverage/assert/test.rs - 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| | } + 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| | }\ diff --git a/tests/coverage/assert_eq/expected b/tests/coverage/assert_eq/expected index 7d5a91d46771..851d079661ec 100644 --- a/tests/coverage/assert_eq/expected +++ b/tests/coverage/assert_eq/expected @@ -1,12 +1,11 @@ -/home/ubuntu/kani/tests/coverage/assert_eq/test.rs - 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| | } + 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| | }\ diff --git a/tests/coverage/assert_ne/expected b/tests/coverage/assert_ne/expected index d29a77afeb5f..ede0547016c4 100644 --- a/tests/coverage/assert_ne/expected +++ b/tests/coverage/assert_ne/expected @@ -1,15 +1,14 @@ -/home/ubuntu/kani/tests/coverage/assert_ne/test.rs - 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| | } + 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| | }\ diff --git a/tests/coverage/break/expected b/tests/coverage/break/expected index aca305b0f411..fbf1ddf75436 100644 --- a/tests/coverage/break/expected +++ b/tests/coverage/break/expected @@ -1,20 +1,19 @@ -/home/ubuntu/kani/tests/coverage/break/main.rs - 1| | // Copyright Kani Contributors - 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT - 3| | - 4| 2| fn find_positive(nums: &[i32]) -> Option { - 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| | } + 1| | // Copyright Kani Contributors\ + 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT\ + 3| | \ + 4| 2| fn find_positive(nums: &[i32]) -> Option {\ + 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| | }\ diff --git a/tests/coverage/compare/expected b/tests/coverage/compare/expected index fc776f1cd4ea..bca5c3d98559 100644 --- a/tests/coverage/compare/expected +++ b/tests/coverage/compare/expected @@ -1,17 +1,16 @@ -/home/ubuntu/kani/tests/coverage/compare/main.rs - 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| | } + 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| | }\ diff --git a/tests/coverage/contradiction/expected b/tests/coverage/contradiction/expected index 5acc7f5c7d4d..ae214727543f 100644 --- a/tests/coverage/contradiction/expected +++ b/tests/coverage/contradiction/expected @@ -1,15 +1,14 @@ -/home/ubuntu/kani/tests/coverage/contradiction/main.rs - 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| | } + 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| | }\ diff --git a/tests/coverage/debug-assert/expected b/tests/coverage/debug-assert/expected index 7ce531204090..b1b8bd6c7c95 100644 --- a/tests/coverage/debug-assert/expected +++ b/tests/coverage/debug-assert/expected @@ -1,16 +1,15 @@ -/home/ubuntu/kani/tests/coverage/debug-assert/main.rs - 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| | } + 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| | }\ diff --git a/tests/coverage/div-zero/expected b/tests/coverage/div-zero/expected index a5a7f94c83fd..9074e6f36d26 100644 --- a/tests/coverage/div-zero/expected +++ b/tests/coverage/div-zero/expected @@ -1,12 +1,11 @@ -/home/ubuntu/kani/tests/coverage/div-zero/test.rs - 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| | } + 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| | }\ diff --git a/tests/coverage/early-return/expected b/tests/coverage/early-return/expected index 9cb66a254204..7203570b106a 100644 --- a/tests/coverage/early-return/expected +++ b/tests/coverage/early-return/expected @@ -1,20 +1,19 @@ -/home/ubuntu/kani/tests/coverage/early-return/main.rs - 1| | // Copyright Kani Contributors - 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT - 3| | - 4| 2| fn find_index(nums: &[i32], target: i32) -> Option { - 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| | } + 1| | // Copyright Kani Contributors\ + 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT\ + 3| | \ + 4| 2| fn find_index(nums: &[i32], target: i32) -> Option {\ + 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| | }\ diff --git a/tests/coverage/if-statement-multi/expected b/tests/coverage/if-statement-multi/expected index ee486c9b8975..35dbc31b2423 100644 --- a/tests/coverage/if-statement-multi/expected +++ b/tests/coverage/if-statement-multi/expected @@ -1,27 +1,26 @@ -/home/ubuntu/kani/tests/coverage/if-statement-multi/test.rs - 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: - 11| | - 12| 0| ```fn _other_function() {''' - 13| 0| ``` println!("Hello, world!");''' - 14| 0| ```}''' - 15| | - 16| 2| fn test_cov(val: u32) -> bool { - 17| 2| if val < 3 || ```val == 42''' { true } else { ```false''' } - 18| | } - 19| | - 20| | #[cfg_attr(kani, kani::proof)] - 21| 2| fn main() { - 22| 2| let test1 = test_cov(1); - 23| 2| let test2 = test_cov(2); - 24| 2| assert!(test1); - 25| 2| assert!(test2); - 26| | } + 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: \ + 11| | \ + 12| 0| ```fn _other_function() {'''\ + 13| 0| ``` println!("Hello, world!");'''\ + 14| 0| ```}'''\ + 15| | \ + 16| 2| fn test_cov(val: u32) -> bool {\ + 17| 2| if val < 3 || ```val == 42''' { true } else { ```false''' }\ + 18| | }\ + 19| | \ + 20| | #[cfg_attr(kani, kani::proof)]\ + 21| 2| fn main() {\ + 22| 2| let test1 = test_cov(1);\ + 23| 2| let test2 = test_cov(2);\ + 24| 2| assert!(test1);\ + 25| 2| assert!(test2);\ + 26| | }\ diff --git a/tests/coverage/if-statement/expected b/tests/coverage/if-statement/expected index fd1dd049975d..ba8de00e08fb 100644 --- a/tests/coverage/if-statement/expected +++ b/tests/coverage/if-statement/expected @@ -1,21 +1,20 @@ -/home/ubuntu/kani/tests/coverage/if-statement/main.rs - 1| | // Copyright Kani Contributors - 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT - 3| | - 4| 2| fn check_number(num: i32) -> &'static str { - 5| 2| if num > 0 { - 6| | // The next line is partially covered - 7| 2| if num % 2 == 0 { ```"Positive and Even"''' } else { "Positive and Odd" } - 8| 0| } else if ```num < 0''' { - 9| 0| "Negative" - 10| | } else { - 11| 0| "Zero" - 12| | } - 13| | } - 14| | - 15| | #[kani::proof] - 16| 2| fn main() { - 17| 2| let number = 7; - 18| 2| let result = check_number(number); - 19| 2| assert_eq!(result, "Positive and Odd"); - 20| | } + 1| | // Copyright Kani Contributors\ + 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT\ + 3| | \ + 4| 2| fn check_number(num: i32) -> &'static str {\ + 5| 2| if num > 0 {\ + 6| | // The next line is partially covered\ + 7| 2| if num % 2 == 0 { ```"Positive and Even"''' } else { "Positive and Odd" }\ + 8| 0| } else if ```num < 0''' {\ + 9| 0| "Negative"\ + 10| | } else {\ + 11| 0| "Zero"\ + 12| | }\ + 13| | }\ + 14| | \ + 15| | #[kani::proof]\ + 16| 2| fn main() {\ + 17| 2| let number = 7;\ + 18| 2| let result = check_number(number);\ + 19| 2| assert_eq!(result, "Positive and Odd");\ + 20| | }\ diff --git a/tests/coverage/multiple-harnesses/expected b/tests/coverage/multiple-harnesses/expected index 58176fc4dca3..432ba426ddd5 100644 --- a/tests/coverage/multiple-harnesses/expected +++ b/tests/coverage/multiple-harnesses/expected @@ -1,45 +1,44 @@ -/home/ubuntu/kani/tests/coverage/multiple-harnesses/main.rs - 1| | // Copyright Kani Contributors - 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT - 3| | - 4| 3| fn estimate_size(x: u32) -> u32 { - 5| 3| assert!(x < 4096); - 6| 3| - 7| 3| if x < 256 { - 8| 3| if x < 128 { - 9| 3| return 1; - 10| | } else { - 11| 3| return 3; - 12| | } - 13| 3| } else if x < 1024 { - 14| 3| if x > 1022 { - 15| 3| return 4; - 16| | } else { - 17| 3| return 5; - 18| | } - 19| | } else { - 20| 3| if x < 2048 { - 21| 3| return 7; - 22| | } else { - 23| 2| return 9; - 24| | } - 25| | } - 26| | } - 27| | - 28| | #[cfg(kani)] - 29| | #[kani::proof] - 30| 2| fn mostly_covered() { - 31| 2| let x: u32 = kani::any(); - 32| 2| kani::assume(x < 2048); - 33| 2| let y = estimate_size(x); - 34| 2| assert!(y < 10); - 35| | } - 36| | - 37| | #[cfg(kani)] - 38| | #[kani::proof] - 39| 2| fn fully_covered() { - 40| 2| let x: u32 = kani::any(); - 41| 2| kani::assume(x < 4096); - 42| 2| let y = estimate_size(x); - 43| 2| assert!(y < 10); - 44| | } + 1| | // Copyright Kani Contributors\ + 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT\ + 3| | \ + 4| 3| fn estimate_size(x: u32) -> u32 {\ + 5| 3| assert!(x < 4096);\ + 6| 3| \ + 7| 3| if x < 256 {\ + 8| 3| if x < 128 {\ + 9| 3| return 1;\ + 10| | } else {\ + 11| 3| return 3;\ + 12| | }\ + 13| 3| } else if x < 1024 {\ + 14| 3| if x > 1022 {\ + 15| 3| return 4;\ + 16| | } else {\ + 17| 3| return 5;\ + 18| | }\ + 19| | } else {\ + 20| 3| if x < 2048 {\ + 21| 3| return 7;\ + 22| | } else {\ + 23| 2| return 9;\ + 24| | }\ + 25| | }\ + 26| | }\ + 27| | \ + 28| | #[cfg(kani)]\ + 29| | #[kani::proof]\ + 30| 2| fn mostly_covered() {\ + 31| 2| let x: u32 = kani::any();\ + 32| 2| kani::assume(x < 2048);\ + 33| 2| let y = estimate_size(x);\ + 34| 2| assert!(y < 10);\ + 35| | }\ + 36| | \ + 37| | #[cfg(kani)]\ + 38| | #[kani::proof]\ + 39| 2| fn fully_covered() {\ + 40| 2| let x: u32 = kani::any();\ + 41| 2| kani::assume(x < 4096);\ + 42| 2| let y = estimate_size(x);\ + 43| 2| assert!(y < 10);\ + 44| | }\ diff --git a/tests/coverage/overflow-failure/expected b/tests/coverage/overflow-failure/expected index cc07742f3070..e717f072a897 100644 --- a/tests/coverage/overflow-failure/expected +++ b/tests/coverage/overflow-failure/expected @@ -1,16 +1,15 @@ -/home/ubuntu/kani/tests/coverage/overflow-failure/test.rs - 1| | // Copyright Kani Contributors - 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT - 3| | - 4| | //! Checks that Kani reports the correct coverage results in the case of an - 5| | //! arithmetic overflow failure (caused by the second call to `cond_reduce`). - 6| | - 7| 2| fn cond_reduce(thresh: u32, x: u32) -> u32 { - 8| 2| if x > thresh { x - 50 } else { x } - 9| | } - 10| | - 11| | #[kani::proof] - 12| 2| fn main() { - 13| 2| cond_reduce(60, 70); - 14| 2| cond_reduce(40, 42); - 15| | } + 1| | // Copyright Kani Contributors\ + 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT\ + 3| | \ + 4| | //! Checks that Kani reports the correct coverage results in the case of an\ + 5| | //! arithmetic overflow failure (caused by the second call to `cond_reduce`).\ + 6| | \ + 7| 2| fn cond_reduce(thresh: u32, x: u32) -> u32 {\ + 8| 2| if x > thresh { x - 50 } else { x }\ + 9| | }\ + 10| | \ + 11| | #[kani::proof]\ + 12| 2| fn main() {\ + 13| 2| cond_reduce(60, 70);\ + 14| 2| cond_reduce(40, 42);\ + 15| | }\ diff --git a/tests/coverage/overflow-full-coverage/expected b/tests/coverage/overflow-full-coverage/expected index 7f666b5571f7..e25b5740eacd 100644 --- a/tests/coverage/overflow-full-coverage/expected +++ b/tests/coverage/overflow-full-coverage/expected @@ -1,18 +1,17 @@ -/home/ubuntu/kani/tests/coverage/overflow-full-coverage/test.rs - 1| | // Copyright Kani Contributors - 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT - 3| | - 4| | //! Checks that Kani reports all regions as `COVERED` as expected in this case - 5| | //! where arithmetic overflow failures are prevented. - 6| | - 7| 2| fn reduce(x: u32) -> u32 { - 8| 2| if x > 1000 { x - 1000 } else { x } - 9| | } - 10| | - 11| | #[kani::proof] - 12| 2| fn main() { - 13| 2| reduce(7); - 14| 2| reduce(33); - 15| 2| reduce(728); - 16| 2| reduce(1079); - 17| | } + 1| | // Copyright Kani Contributors\ + 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT\ + 3| | \ + 4| | //! Checks that Kani reports all regions as `COVERED` as expected in this case\ + 5| | //! where arithmetic overflow failures are prevented.\ + 6| | \ + 7| 2| fn reduce(x: u32) -> u32 {\ + 8| 2| if x > 1000 { x - 1000 } else { x }\ + 9| | }\ + 10| | \ + 11| | #[kani::proof]\ + 12| 2| fn main() {\ + 13| 2| reduce(7);\ + 14| 2| reduce(33);\ + 15| 2| reduce(728);\ + 16| 2| reduce(1079);\ + 17| | }\ diff --git a/tests/coverage/while-loop-break/expected b/tests/coverage/while-loop-break/expected index 574875ac558b..d6bf62ff23d0 100644 --- a/tests/coverage/while-loop-break/expected +++ b/tests/coverage/while-loop-break/expected @@ -1,24 +1,23 @@ -/home/ubuntu/kani/tests/coverage/while-loop-break/main.rs - 1| | // Copyright Kani Contributors - 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT - 3| | - 4| | //! Checks coverage results in an example with a `while` loop that returns before - 5| | //! running the last iteration. - 6| | - 7| 2| fn find_first_negative(nums: &[i32]) -> Option { - 8| 2| let mut index = 0; - 9| 2| while index < nums.len() { - 10| 2| if nums[index] < 0 { - 11| 2| return Some(nums[index]); - 12| 2| } - 13| 2| index += 1; - 14| | } - 15| 0| None - 16| | } - 17| | - 18| | #[kani::proof] - 19| 2| fn main() { - 20| 2| let numbers = [1, 2, -3, 4, -5]; - 21| 2| let result = find_first_negative(&numbers); - 22| 2| assert_eq!(result, Some(-3)); - 23| | } + 1| | // Copyright Kani Contributors\ + 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT\ + 3| | \ + 4| | //! Checks coverage results in an example with a `while` loop that returns before\ + 5| | //! running the last iteration.\ + 6| | \ + 7| 2| fn find_first_negative(nums: &[i32]) -> Option {\ + 8| 2| let mut index = 0;\ + 9| 2| while index < nums.len() {\ + 10| 2| if nums[index] < 0 {\ + 11| 2| return Some(nums[index]);\ + 12| 2| }\ + 13| 2| index += 1;\ + 14| | }\ + 15| 0| None\ + 16| | }\ + 17| | \ + 18| | #[kani::proof]\ + 19| 2| fn main() {\ + 20| 2| let numbers = [1, 2, -3, 4, -5];\ + 21| 2| let result = find_first_negative(&numbers);\ + 22| 2| assert_eq!(result, Some(-3));\ + 23| | }\ From 06b97f0f9f660f400f8c9e9bababcea46c492d3f Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 20 Sep 2024 15:08:43 +0000 Subject: [PATCH 28/36] Reformat --- tools/compiletest/src/runtest.rs | 30 ++--- tools/kani-cov/src/report.rs | 183 ++++++++++++++++++------------- 2 files changed, 121 insertions(+), 92 deletions(-) diff --git a/tools/compiletest/src/runtest.rs b/tools/compiletest/src/runtest.rs index f5b9bc826fb5..ed06ca5e60ed 100644 --- a/tools/compiletest/src/runtest.rs +++ b/tools/compiletest/src/runtest.rs @@ -419,7 +419,12 @@ impl<'test> TestCx<'test> { self.verify_output(&kanicov_proc, &expected_path); } - fn run_kanicov_report(&self, kanimap: &PathBuf, kaniraws: &Vec, kanicov: &PathBuf) -> ProcRes { + fn run_kanicov_report( + &self, + kanimap: &PathBuf, + kaniraws: &Vec, + kanicov: &PathBuf, + ) -> ProcRes { let mut kanicov_merge = Command::new("kani-cov"); kanicov_merge.arg("merge"); kanicov_merge.args(kaniraws); @@ -428,16 +433,13 @@ impl<'test> TestCx<'test> { let merge_cmd = self.compose_and_run(kanicov_merge); if !merge_cmd.status.success() { - self.fatal_proc_rec( - "test failed: could not run `kani-cov merge` command", - &merge_cmd, - ); + self.fatal_proc_rec("test failed: could not run `kani-cov merge` command", &merge_cmd); } let mut kanicov_report = Command::new("kani-cov"); kanicov_report.arg("report").arg(kanimap).arg("--profile").arg(kanicov); let report_cmd = self.compose_and_run(kanicov_report); - + if !report_cmd.status.success() { self.fatal_proc_rec( "test failed: could not run `kani-cov report` command", @@ -456,25 +458,25 @@ impl<'test> TestCx<'test> { let kaniraw_glob = format!("{}/*_kaniraw.json", folder_path.display()); // self.error(&format!("kaniraw_glob: {kaniraw_glob}")); let kaniraws: Vec = glob::glob(&kaniraw_glob) - .expect("Failed to read glob pattern") - .filter_map(|entry| entry.ok()) - .collect(); + .expect("Failed to read glob pattern") + .filter_map(|entry| entry.ok()) + .collect(); (kanimap, kaniraws, kanicov) } - fn extract_cov_results_path(&self, proc_res: &ProcRes) -> PathBuf { + fn extract_cov_results_path(&self, proc_res: &ProcRes) -> PathBuf { let output_lines = proc_res.stdout.split('\n').collect::>(); let coverage_info = output_lines.iter().find(|l| l.contains("Coverage results saved to")); if coverage_info.is_none() { self.fatal_proc_rec( - &format!( - "failed to find the path to the coverage results!"), - proc_res); + &format!("failed to find the path to the coverage results!"), + proc_res, + ); } let coverage_path = coverage_info.unwrap().split(' ').last().unwrap(); PathBuf::from(coverage_path) - } + } /// Runs Kani with stub implementations of various data structures. /// Currently, it only runs tests for the Vec module with the (Kani)Vec /// abstraction. At a later stage, it should be possible to add command-line diff --git a/tools/kani-cov/src/report.rs b/tools/kani-cov/src/report.rs index 16c960bd223e..ea1b2284727e 100644 --- a/tools/kani-cov/src/report.rs +++ b/tools/kani-cov/src/report.rs @@ -64,48 +64,48 @@ pub fn print_coverage_results( let idx = i + 1; let line = line?; - // 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) - // }; + // 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) + // }; let cur_line_result = flattened_results.iter().find(|(num, _)| *num == idx); let (max_times, line_fmt) = if let Some((_, span_data)) = cur_line_result { @@ -118,40 +118,56 @@ pub fn print_coverage_results( // Note: I'm not sure why we need to offset the columns by -1 { // Filter out cases where the span is a single unit AND it ends after the line - let results: Vec<&CovResult> = results.into_iter().filter(|m| if m.region.start.0 as usize == idx && m.region.end.0 as usize == idx { (m.region.end.1 - m.region.start.1 != 1) && (m.region.end.1 as usize) < line.len() } else {true }).collect(); + let results: Vec<&CovResult> = results + .into_iter() + .filter(|m| { + if m.region.start.0 as usize == idx + && m.region.end.0 as usize == idx + { + (m.region.end.1 - m.region.start.1 != 1) + && (m.region.end.1 as usize) < line.len() + } else { + true + } + }) + .collect(); let mut complete_escapes: Vec<(usize, bool)> = results - .iter() - .filter(|m| m.times_covered == 0 && m.region.start.0 as usize == idx && m.region.end.0 as usize == idx) - .map(|m| { - vec![ - ((m.region.start.1 - 1) as usize, true), - ((m.region.end.1 - 1) as usize, false), - ] - }) - .flatten() - .collect(); + .iter() + .filter(|m| { + m.times_covered == 0 + && m.region.start.0 as usize == idx + && m.region.end.0 as usize == idx + }) + .map(|m| { + vec![ + ((m.region.start.1 - 1) as usize, true), + ((m.region.end.1 - 1) as usize, false), + ] + }) + .flatten() + .collect(); // println!("COMPLETE: {complete_escapes:?}"); let mut starting_escapes: Vec<(usize, bool)> = results - .iter() - .filter(|m| m.times_covered == 0 && m.region.start.0 as usize == idx && m.region.end.0 as usize != idx) - .map(|m| { - vec![ - ((m.region.start.1 - 1) as usize, true), - ] - }) - .flatten() - .collect(); + .iter() + .filter(|m| { + m.times_covered == 0 + && m.region.start.0 as usize == idx + && m.region.end.0 as usize != idx + }) + .map(|m| vec![((m.region.start.1 - 1) as usize, true)]) + .flatten() + .collect(); // println!("{starting_escapes:?}"); let mut ending_escapes: Vec<(usize, bool)> = results - .iter() - .filter(|m| m.times_covered == 0 && m.region.start.0 as usize != idx && m.region.end.0 as usize == idx) - .map(|m| { - vec![ - ((m.region.end.1 - 1) as usize, false), - ] - }) - .flatten() - .collect(); + .iter() + .filter(|m| { + m.times_covered == 0 + && m.region.start.0 as usize != idx + && m.region.end.0 as usize == idx + }) + .map(|m| vec![((m.region.end.1 - 1) as usize, false)]) + .flatten() + .collect(); // println!("{starting_escapes:?}"); // println!("{ending_escapes:?}"); @@ -166,23 +182,34 @@ pub fn print_coverage_results( ending_escapes.extend(complete_escapes); ending_escapes.extend(starting_escapes); - + if must_highlight && ending_escapes.is_empty() { ending_escapes.push((0, true)); ending_escapes.push((line.len(), false)); } - ( - Some(max), - insert_escapes(&line, ending_escapes) - ) + (Some(max), insert_escapes(&line, ending_escapes)) } } } else { - (None, if !must_highlight { line } else {insert_escapes(&line, vec![(0, true), (line.len(), false)])}) + ( + None, + if !must_highlight { + line + } else { + insert_escapes(&line, vec![(0, true), (line.len(), false)]) + }, + ) } } else { - (None, if !must_highlight { line } else {insert_escapes(&line, vec![(0, true), (line.len(), false)])}) + ( + None, + if !must_highlight { + line + } else { + insert_escapes(&line, vec![(0, true), (line.len(), false)]) + }, + ) }; let max_fmt = From 781ba583fe81ff374252369081194d11a88dff8e Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 20 Sep 2024 15:12:03 +0000 Subject: [PATCH 29/36] Clippy fixes --- tools/compiletest/src/runtest.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tools/compiletest/src/runtest.rs b/tools/compiletest/src/runtest.rs index ed06ca5e60ed..ac7cfca77ae5 100644 --- a/tools/compiletest/src/runtest.rs +++ b/tools/compiletest/src/runtest.rs @@ -449,7 +449,7 @@ impl<'test> TestCx<'test> { report_cmd } - fn find_cov_files(&self, folder_path: &PathBuf) -> (PathBuf, Vec, PathBuf) { + fn find_cov_files(&self, folder_path: &Path) -> (PathBuf, Vec, PathBuf) { let folder_name = folder_path.file_name().unwrap(); let kanimap = folder_path.join(format!("{}_kanimap.json", folder_name.to_string_lossy())); @@ -470,7 +470,7 @@ impl<'test> TestCx<'test> { let coverage_info = output_lines.iter().find(|l| l.contains("Coverage results saved to")); if coverage_info.is_none() { self.fatal_proc_rec( - &format!("failed to find the path to the coverage results!"), + "failed to find the path to the coverage results", proc_res, ); } From 7d7ef6c2efbfee57ba4d8f0d2a80b27d075f55d3 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 20 Sep 2024 15:28:37 +0000 Subject: [PATCH 30/36] Clean up: unused imports and commented out code --- tools/compiletest/src/runtest.rs | 5 +--- tools/kani-cov/src/coverage.rs | 31 +------------------- tools/kani-cov/src/merge.rs | 4 +-- tools/kani-cov/src/report.rs | 49 ++------------------------------ 4 files changed, 5 insertions(+), 84 deletions(-) diff --git a/tools/compiletest/src/runtest.rs b/tools/compiletest/src/runtest.rs index ac7cfca77ae5..2d4e3caa0d2f 100644 --- a/tools/compiletest/src/runtest.rs +++ b/tools/compiletest/src/runtest.rs @@ -469,10 +469,7 @@ impl<'test> TestCx<'test> { let output_lines = proc_res.stdout.split('\n').collect::>(); let coverage_info = output_lines.iter().find(|l| l.contains("Coverage results saved to")); if coverage_info.is_none() { - self.fatal_proc_rec( - "failed to find the path to the coverage results", - proc_res, - ); + self.fatal_proc_rec("failed to find the path to the coverage results", proc_res); } let coverage_path = coverage_info.unwrap().split(' ').last().unwrap(); PathBuf::from(coverage_path) diff --git a/tools/kani-cov/src/coverage.rs b/tools/kani-cov/src/coverage.rs index 78238cdee208..b4a35d331481 100644 --- a/tools/kani-cov/src/coverage.rs +++ b/tools/kani-cov/src/coverage.rs @@ -31,33 +31,6 @@ pub struct CombinedCoverageResults { pub data: BTreeMap)>>, } -// pub fn fmt_coverage_results(coverage_results: &CoverageResults) -> Result { -// let mut fmt_string = String::new(); -// for (file, checks) in coverage_results.data.iter() { -// let mut checks_by_function: BTreeMap> = 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 = 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, @@ -178,8 +151,7 @@ fn function_info_from_node<'a>(node: Node, source: &'a [u8]) -> FunctionInfo { .to_string(); let start = (node.start_position().row + 1, node.start_position().column + 1); let end = (node.end_position().row + 1, node.end_position().column + 1); - let num_lines = end.0 - start.0 + 1; - FunctionInfo { name, start, end, num_lines } + FunctionInfo { name, start, end } } #[derive(Debug)] @@ -187,7 +159,6 @@ pub struct FunctionInfo { pub name: String, pub start: (usize, usize), pub end: (usize, usize), - pub num_lines: usize, } pub fn function_coverage_results( diff --git a/tools/kani-cov/src/merge.rs b/tools/kani-cov/src/merge.rs index 87863a314aa0..0d9fd74c3b43 100644 --- a/tools/kani-cov/src/merge.rs +++ b/tools/kani-cov/src/merge.rs @@ -4,7 +4,7 @@ use std::{ collections::BTreeMap, fs::{File, OpenOptions}, - io::{BufReader, BufWriter, Write}, + io::{BufReader, BufWriter}, path::PathBuf, }; @@ -91,14 +91,12 @@ fn combine_raw_results(results: &Vec) -> CombinedCoverageResult new_results.push(new_result); } - // let pair_string = format!("{file_name}+{fun_name}"); let filename_copy = file_name.clone(); if new_data.contains_key(&file_name) { new_data.get_mut(&filename_copy).unwrap().push((fun_name, new_results)); } else { new_data.insert(file_name.clone(), vec![(fun_name, new_results)]); } - // new_data.insert(file_name, (fun_name, new_results)); } CombinedCoverageResults { data: new_data } } diff --git a/tools/kani-cov/src/report.rs b/tools/kani-cov/src/report.rs index ea1b2284727e..5534540d2234 100644 --- a/tools/kani-cov/src/report.rs +++ b/tools/kani-cov/src/report.rs @@ -6,11 +6,8 @@ use std::{fs::File, io::BufReader, path::PathBuf}; use anyhow::Result; -use crate::coverage::{ - function_coverage_results, function_info_from_file, CovResult, FileCoverageInfo, FunctionInfo, - MarkerInfo, -}; -use crate::summary::{line_coverage_info, line_coverage_results}; +use crate::coverage::{function_coverage_results, function_info_from_file, CovResult, MarkerInfo}; +use crate::summary::line_coverage_results; use crate::{args::ReportArgs, coverage::CombinedCoverageResults}; // use crate::coverage::CoverageResults; // use args::Args; @@ -64,48 +61,6 @@ pub fn print_coverage_results( let idx = i + 1; let line = line?; - // 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) - // }; let cur_line_result = flattened_results.iter().find(|(num, _)| *num == idx); let (max_times, line_fmt) = if let Some((_, span_data)) = cur_line_result { From 5cd068703a09b2be970ce6d4cd866b16f397f1dd Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 20 Sep 2024 18:44:44 +0000 Subject: [PATCH 31/36] Report format --- tools/kani-cov/src/args.rs | 8 ++++++++ tools/kani-cov/src/report.rs | 2 -- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/tools/kani-cov/src/args.rs b/tools/kani-cov/src/args.rs index f8e57138e7f6..1d136ecefa77 100644 --- a/tools/kani-cov/src/args.rs +++ b/tools/kani-cov/src/args.rs @@ -60,6 +60,14 @@ pub struct ReportArgs { pub mapfile: PathBuf, #[arg(long, required = true)] pub profile: PathBuf, + #[arg(long, short, value_parser = clap::value_parser!(ReportFormat), default_value = "terminal")] + pub format: ReportFormat, +} + +#[derive(Clone, Debug, PartialEq, Eq, clap::ValueEnum)] +pub enum ReportFormat { + Terminal, + Escapes, } pub fn validate_args(args: &Args) -> Result<()> { diff --git a/tools/kani-cov/src/report.rs b/tools/kani-cov/src/report.rs index 5534540d2234..c690e07526cf 100644 --- a/tools/kani-cov/src/report.rs +++ b/tools/kani-cov/src/report.rs @@ -9,8 +9,6 @@ use anyhow::Result; use crate::coverage::{function_coverage_results, function_info_from_file, CovResult, MarkerInfo}; use crate::summary::line_coverage_results; use crate::{args::ReportArgs, coverage::CombinedCoverageResults}; -// use crate::coverage::CoverageResults; -// use args::Args; pub fn report_main(args: &ReportArgs) -> Result<()> { let mapfile = File::open(&args.mapfile)?; From 4694294d421b80ea0b09a73ff0adfd395d733e3f Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 20 Sep 2024 19:25:52 +0000 Subject: [PATCH 32/36] Introduce format for reports --- tools/kani-cov/src/args.rs | 1 + tools/kani-cov/src/report.rs | 53 ++++++++++++++++++++++++++---------- 2 files changed, 39 insertions(+), 15 deletions(-) diff --git a/tools/kani-cov/src/args.rs b/tools/kani-cov/src/args.rs index 1d136ecefa77..632d5fa8c9e8 100644 --- a/tools/kani-cov/src/args.rs +++ b/tools/kani-cov/src/args.rs @@ -25,6 +25,7 @@ pub enum Subcommand { subcommand_precedence_over_arg = true, args_conflicts_with_subcommands = true )] + pub struct Args { #[command(subcommand)] pub command: Option, diff --git a/tools/kani-cov/src/report.rs b/tools/kani-cov/src/report.rs index c690e07526cf..cfd7ee9bf405 100644 --- a/tools/kani-cov/src/report.rs +++ b/tools/kani-cov/src/report.rs @@ -6,6 +6,7 @@ use std::{fs::File, io::BufReader, path::PathBuf}; use anyhow::Result; +use crate::args::ReportFormat; use crate::coverage::{function_coverage_results, function_info_from_file, CovResult, MarkerInfo}; use crate::summary::line_coverage_results; use crate::{args::ReportArgs, coverage::CombinedCoverageResults}; @@ -22,6 +23,8 @@ pub fn report_main(args: &ReportArgs) -> Result<()> { let source_files: Vec = serde_json::from_reader(reader).expect("could not parse coverage metadata"); + let checked_format = check_format(&args.format); + for file in source_files { let fun_info = function_info_from_file(&file); let mut file_cov_info = Vec::new(); @@ -32,17 +35,35 @@ pub fn report_main(args: &ReportArgs) -> Result<()> { (info.start.0..=info.end.0).zip(line_coverage.clone()).collect(); file_cov_info.push(line_coverage_matched); } - print_coverage_results(file, file_cov_info)?; + print_coverage_results(&checked_format, file, file_cov_info)?; } Ok(()) } +// Validate arguments to the `report` subcommand in addition to clap's +// validation. pub fn validate_report_args(_args: &ReportArgs) -> Result<()> { + // No validation is done at the moment Ok(()) } +fn check_format(format: &ReportFormat) -> ReportFormat { + let is_terminal = std::io::stdout().is_terminal(); + match format { + ReportFormat::Terminal => { + if is_terminal { + ReportFormat::Terminal + } else { + ReportFormat::Escapes + } + } + ReportFormat::Escapes => ReportFormat::Escapes, + } +} + pub fn print_coverage_results( + format: &ReportFormat, filepath: PathBuf, results: Vec)>>, ) -> Result<()> { @@ -64,9 +85,10 @@ pub fn print_coverage_results( let (max_times, line_fmt) = if let Some((_, span_data)) = cur_line_result { if let Some((max, marker_info)) = span_data { match marker_info { - MarkerInfo::FullLine => { - (Some(max), insert_escapes(&line, vec![(0, true), (line.len(), false)])) - } + MarkerInfo::FullLine => ( + Some(max), + insert_escapes(&line, vec![(0, true), (line.len(), false)], format), + ), MarkerInfo::Markers(results) => // Note: I'm not sure why we need to offset the columns by -1 { @@ -84,7 +106,7 @@ pub fn print_coverage_results( } }) .collect(); - let mut complete_escapes: Vec<(usize, bool)> = results + let complete_escapes: Vec<(usize, bool)> = results .iter() .filter(|m| { m.times_covered == 0 @@ -141,7 +163,7 @@ pub fn print_coverage_results( ending_escapes.push((line.len(), false)); } - (Some(max), insert_escapes(&line, ending_escapes)) + (Some(max), insert_escapes(&line, ending_escapes, format)) } } } else { @@ -150,7 +172,7 @@ pub fn print_coverage_results( if !must_highlight { line } else { - insert_escapes(&line, vec![(0, true), (line.len(), false)]) + insert_escapes(&line, vec![(0, true), (line.len(), false)], format) }, ) } @@ -160,7 +182,7 @@ pub fn print_coverage_results( if !must_highlight { line } else { - insert_escapes(&line, vec![(0, true), (line.len(), false)]) + insert_escapes(&line, vec![(0, true), (line.len(), false)], format) }, ) }; @@ -174,17 +196,18 @@ pub fn print_coverage_results( Ok(()) } -fn insert_escapes(str: &String, markers: Vec<(usize, bool)>) -> String { +fn insert_escapes(str: &String, markers: Vec<(usize, bool)>, format: &ReportFormat) -> String { let mut new_str = str.clone(); let mut offset = 0; - let support_color = std::io::stdout().is_terminal(); - let mut sym_markers: Vec<(&usize, &str)> = if support_color { - markers.iter().map(|(i, b)| (i, if *b { "\x1b[41m" } else { "\x1b[0m" })).collect() - } else { - markers.iter().map(|(i, b)| (i, if *b { "```" } else { "'''" })).collect() + let (open_escape, close_escape) = match format { + ReportFormat::Terminal => ("\x1b[41m", "\x1b[0m"), + ReportFormat::Escapes => ("```", "'''"), }; - // Sorting + + let mut sym_markers: Vec<(&usize, &str)> = + markers.iter().map(|(i, b)| (i, if *b { open_escape } else { close_escape })).collect(); + sym_markers.sort(); for (i, b) in sym_markers { new_str.insert_str(i + offset, b); From 21f2bd8548b1eaf8823328fba80299569bd3630a Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 20 Sep 2024 20:02:50 +0000 Subject: [PATCH 33/36] Add documentation for several functions --- tools/kani-cov/src/merge.rs | 3 +++ tools/kani-cov/src/summary.rs | 47 ++++++++++++++++++++++++----------- 2 files changed, 36 insertions(+), 14 deletions(-) diff --git a/tools/kani-cov/src/merge.rs b/tools/kani-cov/src/merge.rs index 0d9fd74c3b43..76415e8457b5 100644 --- a/tools/kani-cov/src/merge.rs +++ b/tools/kani-cov/src/merge.rs @@ -22,7 +22,10 @@ pub fn merge_main(args: &MergeArgs) -> Result<()> { Ok(()) } +// Validate arguments to the `merge` subcommand in addition to clap's +// validation. pub fn validate_merge_args(_args: &MergeArgs) -> Result<()> { + // No validation is done at the moment Ok(()) } diff --git a/tools/kani-cov/src/summary.rs b/tools/kani-cov/src/summary.rs index 23f260073af8..8623e550c550 100644 --- a/tools/kani-cov/src/summary.rs +++ b/tools/kani-cov/src/summary.rs @@ -89,50 +89,65 @@ struct FunctionCoverageResults { total_regions: u32, } +// Validate arguments to the `summary` subcommand in addition to clap's +// validation. pub fn validate_summary_args(_args: &SummaryArgs) -> Result<()> { + // No validation is done at the moment Ok(()) } +/// Computes coverage results from a line-based perspective. +/// +/// Basically, for each line we produce an `>` result +/// where: +/// * `None` means there were no coverage results associated with this line. +/// This may happen in lines that only contain a closing `}`, for example. +/// * `Some(max, markers)` means there were coverage results associated with +/// the line or we deduced no results were possible based on function +/// information (i.e., the function was not reachable during verification). +/// Here, `max` represents the maximum number of times the line was covered by +/// any coverage result, and `markers` represents marker information which is +/// relevant to the line (including coverage results). +/// +/// As a result, we essentially precompute here most of the information required +/// for the generation of coverage reports. pub fn line_coverage_results( info: &FunctionInfo, fun_results: &Option<(String, Vec)>, ) -> Vec> { let start_line: u32 = info.start.0.try_into().unwrap(); let end_line: u32 = info.end.0.try_into().unwrap(); - // `line_status` represents all the lines between `start_line` and - // `end_line`. For each line, we will have either: - // - `None`, meaning there were no results associated with this line (this - // may happen with lines that only contain a closing `}`, for example). - // - `Some(max, other)`, where `max` represents the maximum number of times - // the line was covered by any coverage result, and `other` specifies the - // coverage results that don't amount to the maximum. + let mut line_status: Vec> = Vec::with_capacity((end_line - start_line + 1).try_into().unwrap()); if let Some(res) = fun_results { let mut cur_results = res.1.clone(); - // was this sorted already? looks like it was not - // println!("BEFORE: {cur_results:?}"); + // Sort the results by row cur_results.sort_by(|a, b| b.region.start.0.cmp(&a.region.start.0)); - // println!("AFTER: {cur_results:?}"); - fn line_contained_in_region(line: u32, region: &CoverageRegion) -> bool { + /// Checks if a line is relevant to a region. + /// Here, we define "relevant" as the line appearing after/at the start + /// of a region and before/at the end of a region. + fn line_relevant_to_region(line: u32, region: &CoverageRegion) -> bool { region.start.0 <= line && region.end.0 >= line } for line in start_line..end_line { + // Filter results which are relevant to the current line let line_results: Vec = cur_results .iter() - .filter(|c| line_contained_in_region(line, &c.region)) + .filter(|c| line_relevant_to_region(line, &c.region)) .cloned() .collect(); + if line_results.is_empty() { line_status.push(None); } else { let max_covered = line_results .iter() - .max_by_key(|obj| obj.times_covered) - .map(|obj| obj.times_covered) + .max_by_key(|res| res.times_covered) + .map(|res| res.times_covered) .unwrap_or(0); line_status.push(Some((max_covered, MarkerInfo::Markers(line_results)))); } @@ -145,6 +160,8 @@ pub fn line_coverage_results( line_status } +/// Compute the number of covered lines and number of total lines given the +/// coverage results for a given function. pub fn line_coverage_info( info: &FunctionInfo, fun_results: &Option<(String, Vec)>, @@ -160,6 +177,8 @@ pub fn line_coverage_info( (covered_lines, total_lines) } +/// Compute the number of covered regions and number of total regions given the +/// coverage results for a given function. fn region_coverage_info( fun_results: &Option<(String, Vec)>, ) -> (u32, u32) { From 923e6061844cef994d0c5efc567f95dee746ca2f Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 20 Sep 2024 20:47:07 +0000 Subject: [PATCH 34/36] Most clippy fixes --- tools/kani-cov/src/coverage.rs | 21 ++++------- tools/kani-cov/src/merge.rs | 2 +- tools/kani-cov/src/report.rs | 16 ++++----- tools/kani-cov/src/summary.rs | 64 ++++++++++++++++------------------ 4 files changed, 44 insertions(+), 59 deletions(-) diff --git a/tools/kani-cov/src/coverage.rs b/tools/kani-cov/src/coverage.rs index b4a35d331481..1efd0129f7db 100644 --- a/tools/kani-cov/src/coverage.rs +++ b/tools/kani-cov/src/coverage.rs @@ -3,11 +3,13 @@ use console::style; use serde_derive::{Deserialize, Serialize}; -use std::path::PathBuf; +use std::path::{Path, PathBuf}; use std::{collections::BTreeMap, fmt::Display}; use std::{fmt, fs}; use tree_sitter::{Node, Parser}; +pub type LineResults = Vec>; + #[derive(Copy, Clone, Debug, Serialize, Deserialize, PartialEq, Eq)] #[serde(rename_all = "UPPERCASE")] pub enum CheckStatus { @@ -62,17 +64,6 @@ impl Display for CoverageRegion { } } -// 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), @@ -143,7 +134,7 @@ pub fn function_info_from_file(filepath: &PathBuf) -> Vec { function_info } -fn function_info_from_node<'a>(node: Node, source: &'a [u8]) -> FunctionInfo { +fn function_info_from_node(node: Node, source: &[u8]) -> FunctionInfo { let name = node .child_by_field_name("name") .and_then(|name| name.utf8_text(source).ok()) @@ -163,12 +154,12 @@ pub struct FunctionInfo { pub fn function_coverage_results( info: &FunctionInfo, - file: &PathBuf, + file: &Path, results: &CombinedCoverageResults, ) -> Option<(String, Vec)> { // `info` does not include file so how do we match? // use function just for now... - let filename = file.clone().into_os_string().into_string().unwrap(); + let filename = file.to_path_buf().into_os_string().into_string().unwrap(); let right_filename = results.data.keys().find(|p| filename.ends_with(*p)).unwrap(); // TODO: The filenames in kaniraw files should be absolute, just like in metadata // Otherwise the key for `results` just fails... diff --git a/tools/kani-cov/src/merge.rs b/tools/kani-cov/src/merge.rs index 76415e8457b5..48d542b4824e 100644 --- a/tools/kani-cov/src/merge.rs +++ b/tools/kani-cov/src/merge.rs @@ -111,7 +111,7 @@ fn save_combined_results( let output_path = if let Some(out) = output { out } else { &PathBuf::from("default_kanicov.json") }; - let file = OpenOptions::new().write(true).create(true).open(output_path)?; + let file = OpenOptions::new().write(true).create(true).truncate(true).open(output_path)?; let writer = BufWriter::new(file); serde_json::to_writer(writer, results)?; diff --git a/tools/kani-cov/src/report.rs b/tools/kani-cov/src/report.rs index cfd7ee9bf405..dd30c05bc9ac 100644 --- a/tools/kani-cov/src/report.rs +++ b/tools/kani-cov/src/report.rs @@ -69,7 +69,7 @@ pub fn print_coverage_results( ) -> Result<()> { let flattened_results: Vec<(usize, Option<(u32, MarkerInfo)>)> = results.into_iter().flatten().collect(); - println!("{}", filepath.to_string_lossy().to_string()); + println!("{}", filepath.to_string_lossy()); let file = File::open(filepath)?; let reader = BufReader::new(file); @@ -94,7 +94,7 @@ pub fn print_coverage_results( { // Filter out cases where the span is a single unit AND it ends after the line let results: Vec<&CovResult> = results - .into_iter() + .iter() .filter(|m| { if m.region.start.0 as usize == idx && m.region.end.0 as usize == idx @@ -113,13 +113,12 @@ pub fn print_coverage_results( && m.region.start.0 as usize == idx && m.region.end.0 as usize == idx }) - .map(|m| { + .flat_map(|m| { vec![ ((m.region.start.1 - 1) as usize, true), ((m.region.end.1 - 1) as usize, false), ] }) - .flatten() .collect(); // println!("COMPLETE: {complete_escapes:?}"); let mut starting_escapes: Vec<(usize, bool)> = results @@ -129,8 +128,7 @@ pub fn print_coverage_results( && m.region.start.0 as usize == idx && m.region.end.0 as usize != idx }) - .map(|m| vec![((m.region.start.1 - 1) as usize, true)]) - .flatten() + .flat_map(|m| vec![((m.region.start.1 - 1) as usize, true)]) .collect(); // println!("{starting_escapes:?}"); let mut ending_escapes: Vec<(usize, bool)> = results @@ -146,11 +144,11 @@ pub fn print_coverage_results( // println!("{starting_escapes:?}"); // println!("{ending_escapes:?}"); - if must_highlight && ending_escapes.len() > 0 { + if must_highlight && !ending_escapes.is_empty() { ending_escapes.push((0_usize, true)); must_highlight = false; } - if starting_escapes.len() > 0 { + if !starting_escapes.is_empty() { starting_escapes.push((line.len(), false)); must_highlight = true; } @@ -211,7 +209,7 @@ fn insert_escapes(str: &String, markers: Vec<(usize, bool)>, format: &ReportForm sym_markers.sort(); for (i, b) in sym_markers { new_str.insert_str(i + offset, b); - offset = offset + b.bytes().len(); + offset += b.bytes().len(); } new_str } diff --git a/tools/kani-cov/src/summary.rs b/tools/kani-cov/src/summary.rs index 8623e550c550..344936a7c212 100644 --- a/tools/kani-cov/src/summary.rs +++ b/tools/kani-cov/src/summary.rs @@ -9,7 +9,7 @@ use crate::{ args::{SummaryArgs, SummaryFormat}, coverage::{ function_coverage_results, function_info_from_file, CombinedCoverageResults, CovResult, - CoverageMetric, CoverageRegion, FileCoverageInfo, FunctionInfo, MarkerInfo, + CoverageMetric, CoverageRegion, FileCoverageInfo, FunctionInfo, LineResults, MarkerInfo, }, }; @@ -101,20 +101,20 @@ pub fn validate_summary_args(_args: &SummaryArgs) -> Result<()> { /// Basically, for each line we produce an `>` result /// where: /// * `None` means there were no coverage results associated with this line. -/// This may happen in lines that only contain a closing `}`, for example. +/// This may happen in lines that only contain a closing `}`, for example. /// * `Some(max, markers)` means there were coverage results associated with -/// the line or we deduced no results were possible based on function -/// information (i.e., the function was not reachable during verification). -/// Here, `max` represents the maximum number of times the line was covered by -/// any coverage result, and `markers` represents marker information which is -/// relevant to the line (including coverage results). +/// the line or we deduced no results were possible based on function +/// information (i.e., the function was not reachable during verification). +/// Here, `max` represents the maximum number of times the line was covered by +/// any coverage result, and `markers` represents marker information which is +/// relevant to the line (including coverage results). /// /// As a result, we essentially precompute here most of the information required /// for the generation of coverage reports. pub fn line_coverage_results( info: &FunctionInfo, fun_results: &Option<(String, Vec)>, -) -> Vec> { +) -> LineResults { let start_line: u32 = info.start.0.try_into().unwrap(); let end_line: u32 = info.end.0.try_into().unwrap(); @@ -192,6 +192,7 @@ fn region_coverage_info( } } +/// Output coverage information for a set of files fn print_coverage_info(info: &Vec, format: &SummaryFormat) { match format { SummaryFormat::Markdown => print_coverage_markdown_info(info), @@ -199,6 +200,7 @@ fn print_coverage_info(info: &Vec, format: &SummaryFormat) { } } +/// Output coverage information for a set of files in the markdown format fn print_coverage_markdown_info(info: &Vec) { fn safe_div(num: u32, denom: u32) -> Option { if denom == 0 { None } else { Some(num as f32 / denom as f32) } @@ -258,36 +260,30 @@ fn print_coverage_markdown_info(info: &Vec) { data_rows.push((filename, function_fmt, line_fmt, region_fmt)); } - let filename_sep: String = std::iter::repeat('-').take(max_filename_fmt_width).collect(); - let filename_space: String = std::iter::repeat(' ') - .take(max_filename_fmt_width - FILENAME_HEADER.len()) - .collect::(); - let function_sep: String = std::iter::repeat('-').take(max_function_fmt_width).collect(); - let function_space: String = std::iter::repeat(' ') - .take(max_function_fmt_width - FUNCTION_HEADER.len()) - .collect::(); - let line_sep: String = std::iter::repeat('-').take(max_line_fmt_width).collect(); - let line_space: String = - std::iter::repeat(' ').take(max_line_fmt_width - LINE_HEADER.len()).collect::(); - let region_sep: String = std::iter::repeat('-').take(max_region_fmt_width).collect(); - let region_space: String = - std::iter::repeat(' ').take(max_region_fmt_width - REGION_HEADER.len()).collect::(); + let filename_space = " ".repeat(max_filename_fmt_width - FILENAME_HEADER.len()); + let function_space = " ".repeat(max_function_fmt_width - FUNCTION_HEADER.len()); + let line_space = " ".repeat(max_line_fmt_width - LINE_HEADER.len()); + let region_space = " ".repeat(max_region_fmt_width - REGION_HEADER.len()); + + let header_row = format!( + "| {FILENAME_HEADER}{filename_space} | {FUNCTION_HEADER}{function_space} | {LINE_HEADER}{line_space} | {REGION_HEADER}{region_space} |" + ); + table_rows.push(header_row); + + let filename_sep = "-".repeat(max_filename_fmt_width); + let function_sep = "-".repeat(max_function_fmt_width); + let line_sep = "-".repeat(max_line_fmt_width); + let region_sep = "-".repeat(max_region_fmt_width); let sep_row = format!("| {filename_sep} | {function_sep} | {line_sep} | {region_sep} |"); - table_rows.push(format!("| {FILENAME_HEADER}{filename_space} | {FUNCTION_HEADER}{function_space} | {LINE_HEADER}{line_space} | {REGION_HEADER}{region_space} |")); table_rows.push(sep_row); + for (filename, function_fmt, line_fmt, region_fmt) in data_rows { - let filename_space: String = std::iter::repeat(' ') - .take(max_filename_fmt_width - filename.len()) - .collect::(); - let function_space: String = std::iter::repeat(' ') - .take(max_function_fmt_width - function_fmt.len()) - .collect::(); - let line_space: String = - std::iter::repeat(' ').take(max_line_fmt_width - line_fmt.len()).collect::(); - let region_space: String = std::iter::repeat(' ') - .take(max_region_fmt_width - region_fmt.len()) - .collect::(); + let filename_space = " ".repeat(max_filename_fmt_width - filename.len()); + let function_space = " ".repeat(max_function_fmt_width - function_fmt.len()); + let line_space = " ".repeat(max_line_fmt_width - line_fmt.len()); + let region_space = " ".repeat(max_region_fmt_width - region_fmt.len()); + let cur_row = format!( "| {filename}{filename_space} | {function_fmt}{function_space} | {line_fmt}{line_space} | {region_fmt}{region_space} |" ); From 812231e4ac3b9c689de8e0e1cb26cfd044b2e046 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 20 Sep 2024 21:31:48 +0000 Subject: [PATCH 35/36] More documentation --- tools/kani-cov/src/coverage.rs | 2 +- tools/kani-cov/src/merge.rs | 4 +-- tools/kani-cov/src/report.rs | 58 +++++++++++++++++++++------------- tools/kani-cov/src/summary.rs | 22 +++++++------ 4 files changed, 51 insertions(+), 35 deletions(-) diff --git a/tools/kani-cov/src/coverage.rs b/tools/kani-cov/src/coverage.rs index 1efd0129f7db..86716aebdc1e 100644 --- a/tools/kani-cov/src/coverage.rs +++ b/tools/kani-cov/src/coverage.rs @@ -8,7 +8,7 @@ use std::{collections::BTreeMap, fmt::Display}; use std::{fmt, fs}; use tree_sitter::{Node, Parser}; -pub type LineResults = Vec>; +pub type LineResults = Vec<(usize, Option<(u32, MarkerInfo)>)>; #[derive(Copy, Clone, Debug, Serialize, Deserialize, PartialEq, Eq)] #[serde(rename_all = "UPPERCASE")] diff --git a/tools/kani-cov/src/merge.rs b/tools/kani-cov/src/merge.rs index 48d542b4824e..98310d7b6c14 100644 --- a/tools/kani-cov/src/merge.rs +++ b/tools/kani-cov/src/merge.rs @@ -22,8 +22,8 @@ pub fn merge_main(args: &MergeArgs) -> Result<()> { Ok(()) } -// Validate arguments to the `merge` subcommand in addition to clap's -// validation. +/// Validate arguments to the `merge` subcommand in addition to clap's +/// validation. pub fn validate_merge_args(_args: &MergeArgs) -> Result<()> { // No validation is done at the moment Ok(()) diff --git a/tools/kani-cov/src/report.rs b/tools/kani-cov/src/report.rs index dd30c05bc9ac..514c3a991890 100644 --- a/tools/kani-cov/src/report.rs +++ b/tools/kani-cov/src/report.rs @@ -7,7 +7,9 @@ use std::{fs::File, io::BufReader, path::PathBuf}; use anyhow::Result; use crate::args::ReportFormat; -use crate::coverage::{function_coverage_results, function_info_from_file, CovResult, MarkerInfo}; +use crate::coverage::{ + function_coverage_results, function_info_from_file, CovResult, LineResults, MarkerInfo, +}; use crate::summary::line_coverage_results; use crate::{args::ReportArgs, coverage::CombinedCoverageResults}; @@ -41,13 +43,19 @@ pub fn report_main(args: &ReportArgs) -> Result<()> { Ok(()) } -// Validate arguments to the `report` subcommand in addition to clap's -// validation. +/// Validate arguments to the `report` subcommand in addition to clap's +/// validation. pub fn validate_report_args(_args: &ReportArgs) -> Result<()> { // No validation is done at the moment Ok(()) } +/// Checks the `format` argument for the `report` subcommand and selects to +/// another format if the one we are checking is not possible for any reason. +/// +/// For example, if the `Terminal` format is specified but we are not writing to +/// a terminal, it will auto-select the `Escapes` format to avoid character +/// issues. fn check_format(format: &ReportFormat) -> ReportFormat { let is_terminal = std::io::stdout().is_terminal(); match format { @@ -65,7 +73,7 @@ fn check_format(format: &ReportFormat) -> ReportFormat { pub fn print_coverage_results( format: &ReportFormat, filepath: PathBuf, - results: Vec)>>, + results: Vec, ) -> Result<()> { let flattened_results: Vec<(usize, Option<(u32, MarkerInfo)>)> = results.into_iter().flatten().collect(); @@ -89,10 +97,9 @@ pub fn print_coverage_results( Some(max), insert_escapes(&line, vec![(0, true), (line.len(), false)], format), ), - MarkerInfo::Markers(results) => - // Note: I'm not sure why we need to offset the columns by -1 - { + MarkerInfo::Markers(results) => { // Filter out cases where the span is a single unit AND it ends after the line + // TODO: Create issue and link let results: Vec<&CovResult> = results .iter() .filter(|m| { @@ -120,7 +127,7 @@ pub fn print_coverage_results( ] }) .collect(); - // println!("COMPLETE: {complete_escapes:?}"); + let mut starting_escapes: Vec<(usize, bool)> = results .iter() .filter(|m| { @@ -130,7 +137,7 @@ pub fn print_coverage_results( }) .flat_map(|m| vec![((m.region.start.1 - 1) as usize, true)]) .collect(); - // println!("{starting_escapes:?}"); + let mut ending_escapes: Vec<(usize, bool)> = results .iter() .filter(|m| { @@ -138,12 +145,9 @@ pub fn print_coverage_results( && m.region.start.0 as usize != idx && m.region.end.0 as usize == idx }) - .map(|m| vec![((m.region.end.1 - 1) as usize, false)]) - .flatten() + .flat_map(|m| vec![((m.region.end.1 - 1) as usize, false)]) .collect(); - // println!("{starting_escapes:?}"); - // println!("{ending_escapes:?}"); if must_highlight && !ending_escapes.is_empty() { ending_escapes.push((0_usize, true)); must_highlight = false; @@ -194,22 +198,32 @@ pub fn print_coverage_results( Ok(()) } -fn insert_escapes(str: &String, markers: Vec<(usize, bool)>, format: &ReportFormat) -> String { - let mut new_str = str.clone(); - let mut offset = 0; - +/// Inserts opening/closing escape strings into `str` given a set of `markers`. +/// Each marker is a tuple `(offset, type)` where: +/// * `offset` represents the offset in which the marker must be inserted, and +/// * `type` represents whether it is an opening (`true`) or closing (`false`) +/// escape. +/// The specific escape to be used are determined by the report format. +fn insert_escapes(str: &str, markers: Vec<(usize, bool)>, format: &ReportFormat) -> String { + // Determine the escape strings based on the format let (open_escape, close_escape) = match format { ReportFormat::Terminal => ("\x1b[41m", "\x1b[0m"), ReportFormat::Escapes => ("```", "'''"), }; - let mut sym_markers: Vec<(&usize, &str)> = + let mut escape_markers: Vec<(&usize, &str)> = markers.iter().map(|(i, b)| (i, if *b { open_escape } else { close_escape })).collect(); + escape_markers.sort(); + + let mut escaped_str = str.to_owned(); + let mut offset = 0; - sym_markers.sort(); - for (i, b) in sym_markers { - new_str.insert_str(i + offset, b); + // Iteratively insert the escape strings into the original string + for (i, b) in escape_markers { + escaped_str.insert_str(i + offset, b); + // `offset` keeps track of the bytes we've already inserted so the original + // index is shifted by the appropriate amount in subsequent insertions. offset += b.bytes().len(); } - new_str + escaped_str } diff --git a/tools/kani-cov/src/summary.rs b/tools/kani-cov/src/summary.rs index 344936a7c212..6da9d561a591 100644 --- a/tools/kani-cov/src/summary.rs +++ b/tools/kani-cov/src/summary.rs @@ -1,7 +1,12 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -use std::{cmp::max, fs::File, io::BufReader, path::PathBuf}; +use std::{ + cmp::max, + fs::File, + io::BufReader, + path::{Path, PathBuf}, +}; use anyhow::Result; @@ -9,7 +14,7 @@ use crate::{ args::{SummaryArgs, SummaryFormat}, coverage::{ function_coverage_results, function_info_from_file, CombinedCoverageResults, CovResult, - CoverageMetric, CoverageRegion, FileCoverageInfo, FunctionInfo, LineResults, MarkerInfo, + CoverageMetric, CoverageRegion, FileCoverageInfo, FunctionInfo, MarkerInfo, }, }; @@ -52,10 +57,7 @@ pub fn summary_main(args: &SummaryArgs) -> Result<()> { Ok(()) } -fn aggregate_cov_info( - file: &PathBuf, - file_cov_info: &Vec, -) -> FileCoverageInfo { +fn aggregate_cov_info(file: &Path, file_cov_info: &[FunctionCoverageResults]) -> FileCoverageInfo { let total_functions = file_cov_info.len().try_into().unwrap(); let covered_functions = file_cov_info.iter().filter(|f| f.is_covered).count().try_into().unwrap(); @@ -89,8 +91,8 @@ struct FunctionCoverageResults { total_regions: u32, } -// Validate arguments to the `summary` subcommand in addition to clap's -// validation. +/// Validate arguments to the `summary` subcommand in addition to clap's +/// validation. pub fn validate_summary_args(_args: &SummaryArgs) -> Result<()> { // No validation is done at the moment Ok(()) @@ -113,8 +115,8 @@ pub fn validate_summary_args(_args: &SummaryArgs) -> Result<()> { /// for the generation of coverage reports. pub fn line_coverage_results( info: &FunctionInfo, - fun_results: &Option<(String, Vec)>, -) -> LineResults { + fun_results: &Option<(String, Vec)>, +) -> Vec> { let start_line: u32 = info.start.0.try_into().unwrap(); let end_line: u32 = info.end.0.try_into().unwrap(); From 745a55f34c338ddc64f05c413361a4f47a86b11c Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 20 Sep 2024 21:51:47 +0000 Subject: [PATCH 36/36] Documentation for main methods --- tools/kani-cov/src/report.rs | 7 +++++++ tools/kani-cov/src/summary.rs | 6 ++++++ 2 files changed, 13 insertions(+) diff --git a/tools/kani-cov/src/report.rs b/tools/kani-cov/src/report.rs index 514c3a991890..5cbdb36695f9 100644 --- a/tools/kani-cov/src/report.rs +++ b/tools/kani-cov/src/report.rs @@ -13,6 +13,12 @@ use crate::coverage::{ use crate::summary::line_coverage_results; use crate::{args::ReportArgs, coverage::CombinedCoverageResults}; +/// Executes the `report` subcommand. +/// +/// First, it loads the coverage metadata and results from the files passed as +/// arguments. Then, for each file referenced in the metadata, it computes its +/// associated coverage information on a per-function basis, producing a +/// human-readable report for each one of the files. pub fn report_main(args: &ReportArgs) -> Result<()> { let mapfile = File::open(&args.mapfile)?; let reader = BufReader::new(mapfile); @@ -203,6 +209,7 @@ pub fn print_coverage_results( /// * `offset` represents the offset in which the marker must be inserted, and /// * `type` represents whether it is an opening (`true`) or closing (`false`) /// escape. +/// /// The specific escape to be used are determined by the report format. fn insert_escapes(str: &str, markers: Vec<(usize, bool)>, format: &ReportFormat) -> String { // Determine the escape strings based on the format diff --git a/tools/kani-cov/src/summary.rs b/tools/kani-cov/src/summary.rs index 6da9d561a591..f2d73140c81c 100644 --- a/tools/kani-cov/src/summary.rs +++ b/tools/kani-cov/src/summary.rs @@ -18,6 +18,12 @@ use crate::{ }, }; +/// Executes the `summary` subcommand. +/// +/// First, it loads the coverage metadata and results from the files passed as +/// arguments. Then, for each file referenced in the metadata, it computes its +/// associated coverage information on a per-function basis, producing coverage +/// metrics for each one of the files. pub fn summary_main(args: &SummaryArgs) -> Result<()> { let mapfile = File::open(&args.mapfile)?; let reader = BufReader::new(mapfile);