Skip to content

Commit

Permalink
Reformat
Browse files Browse the repository at this point in the history
  • Loading branch information
@adpaco-aws
adpaco-aws committed Sep 20, 2024
1 parent b33fd5c commit 06b97f0
Show file tree
Hide file tree
Showing 2 changed files with 121 additions and 92 deletions.
30 changes: 16 additions & 14 deletions tools/compiletest/src/runtest.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -419,7 +419,12 @@ impl<'test> TestCx<'test> {
self.verify_output(&kanicov_proc, &expected_path);
}

fn run_kanicov_report(&self, kanimap: &PathBuf, kaniraws: &Vec<PathBuf>, kanicov: &PathBuf) -> ProcRes {
fn run_kanicov_report(
&self,
kanimap: &PathBuf,
kaniraws: &Vec<PathBuf>,
kanicov: &PathBuf,
) -> ProcRes {
let mut kanicov_merge = Command::new("kani-cov");
kanicov_merge.arg("merge");
kanicov_merge.args(kaniraws);
Expand All @@ -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",
Expand All @@ -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<PathBuf> = 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::<Vec<&str>>();
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
Expand Down
183 changes: 105 additions & 78 deletions tools/kani-cov/src/report.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand All @@ -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:?}");
Expand All @@ -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 =
Expand Down

0 comments on commit 06b97f0

Please sign in to comment.