Skip to content

Commit

Permalink
More typenames and use across all of kani-cov
Browse files Browse the repository at this point in the history
  • Loading branch information
adpaco-aws committed Oct 7, 2024
1 parent 421cde4 commit c7606f3
Show file tree
Hide file tree
Showing 4 changed files with 40 additions and 37 deletions.
23 changes: 12 additions & 11 deletions tools/kani-cov/src/coverage.rs
Original file line number Diff line number Diff line change
Expand Up @@ -11,9 +11,10 @@ use std::{collections::HashMap, fmt::Display};
use std::{fmt, fs};
use tree_sitter::{Node, Parser};

type Function = String;
type Filename = String;
type LineNumber = usize;
pub type Function = String;
pub type Filename = String;
pub type LineNumber = usize;
pub type ColumnNumber = usize;

pub type LineResults = Vec<(LineNumber, Option<(usize, MarkerInfo)>)>;

Expand All @@ -40,7 +41,7 @@ pub enum CheckStatus {
/// <https://github.com/model-checking/kani/issues/3541>
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct CoverageCheck {
pub function: String,
pub function: Filename,
term: CoverageTerm,
pub region: CoverageRegion,
pub status: CheckStatus,
Expand Down Expand Up @@ -87,7 +88,7 @@ pub struct CombinedCoverageResults {
/// had the `COVERED` status.
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct CovResult {
pub function: String,
pub function: Filename,
pub region: CoverageRegion,
pub times_covered: usize,
pub total_times: usize,
Expand All @@ -100,9 +101,9 @@ pub struct CovResult {
/// <https://github.com/model-checking/kani/issues/3541>
#[derive(Debug, Clone, Eq, PartialEq, PartialOrd, Ord, Serialize, Deserialize)]
pub struct CoverageRegion {
pub file: String,
pub start: (usize, usize),
pub end: (usize, usize),
pub file: Filename,
pub start: (LineNumber, ColumnNumber),
pub end: (LineNumber, ColumnNumber),
}

impl Display for CoverageRegion {
Expand Down Expand Up @@ -145,8 +146,8 @@ impl CoverageMetric {
#[derive(Debug)]
pub struct FunctionInfo {
pub name: Function,
pub start: (usize, usize),
pub end: (usize, usize),
pub start: (LineNumber, ColumnNumber),
pub end: (LineNumber, ColumnNumber),
}

/// Extract function information from a file using a tree-sitter
Expand Down Expand Up @@ -187,7 +188,7 @@ pub fn function_coverage_results(
info: &FunctionInfo,
file: &Path,
results: &CombinedCoverageResults,
) -> Option<(String, Vec<CovResult>)> {
) -> Option<(Function, Vec<CovResult>)> {
// The filenames in "kaniraw" files are not absolute, so we need to match
// them with the ones we have in the aggregated results (i.e., the filenames
// in the "kanimap" files).
Expand Down
9 changes: 6 additions & 3 deletions tools/kani-cov/src/merge.rs
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,10 @@ use anyhow::Result;

use crate::{
args::MergeArgs,
coverage::{CheckStatus, CombinedCoverageResults, CovResult, CoverageCheck, CoverageResults},
coverage::{
CheckStatus, CombinedCoverageResults, CovResult, CoverageCheck, CoverageResults, Filename,
Function,
},
};

/// Executes the `merge` subcommand.
Expand Down Expand Up @@ -56,7 +59,7 @@ fn parse_raw_results(paths: &Vec<PathBuf>) -> Result<Vec<CoverageResults>> {
fn combine_raw_results(results: &Vec<CoverageResults>) -> CombinedCoverageResults {
let all_file_function_names = function_names_from_results(results);

let mut new_data: HashMap<String, Vec<(String, Vec<CovResult>)>> = HashMap::new();
let mut new_data: HashMap<Filename, Vec<(Function, Vec<CovResult>)>> = HashMap::new();

for (file_name, fun_name) in all_file_function_names {
let mut this_fun_checks: Vec<&CoverageCheck> = Vec::new();
Expand Down Expand Up @@ -129,7 +132,7 @@ fn save_combined_results(
}

/// All function names appearing in raw coverage results
fn function_names_from_results(results: &[CoverageResults]) -> Vec<(String, String)> {
fn function_names_from_results(results: &[CoverageResults]) -> Vec<(Filename, Function)> {
let mut file_function_pairs = HashSet::new();
for result in results {
for (file, checks) in &result.data {
Expand Down
22 changes: 11 additions & 11 deletions tools/kani-cov/src/report.rs
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,8 @@ use anyhow::Result;

use crate::args::ReportFormat;
use crate::coverage::{
CovResult, LineResults, MarkerInfo, function_coverage_results, function_info_from_file,
ColumnNumber, CovResult, LineNumber, LineResults, MarkerInfo, function_coverage_results,
function_info_from_file,
};
use crate::summary::line_coverage_results;
use crate::{args::ReportArgs, coverage::CombinedCoverageResults};
Expand Down Expand Up @@ -41,7 +42,7 @@ 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<(usize, MarkerInfo)>)> =
let line_coverage_matched: LineResults =
(info.start.0..=info.end.0).zip(line_coverage.clone()).collect();
file_cov_info.push(line_coverage_matched);
}
Expand Down Expand Up @@ -113,8 +114,7 @@ pub fn output_coverage_results(
filepath: PathBuf,
results: Vec<LineResults>,
) -> Result<()> {
let flattened_results: Vec<(usize, Option<(usize, MarkerInfo)>)> =
results.into_iter().flatten().collect();
let flattened_results: LineResults = results.into_iter().flatten().collect();
println!("{}", filepath.to_string_lossy());

let file = File::open(filepath)?;
Expand All @@ -135,7 +135,7 @@ pub fn output_coverage_results(
}
MarkerInfo::Markers(results) => {
// Escapes for the regions which start and finish in this line
let complete_escapes: Vec<(usize, bool)> = results
let complete_escapes: Vec<(ColumnNumber, bool)> = results
.iter()
.filter(|m| {
m.times_covered == 0 && m.region.start.0 == idx && m.region.end.0 == idx
Expand All @@ -145,15 +145,15 @@ pub fn output_coverage_results(
})
.collect();
// Escapes for the regions which only start in this line
let mut opening_escapes: Vec<(usize, bool)> = results
let mut opening_escapes: Vec<(ColumnNumber, bool)> = results
.iter()
.filter(|m| {
m.times_covered == 0 && m.region.start.0 == idx && m.region.end.0 != idx
})
.flat_map(|m| vec![((m.region.start.1 - 1), true)])
.collect();
// Escapes for the regions which only finish in this line
let mut closing_escapes: Vec<(usize, bool)> = results
let mut closing_escapes: Vec<(ColumnNumber, bool)> = results
.iter()
.filter(|m| {
m.times_covered == 0 && m.region.start.0 != idx && m.region.end.0 == idx
Expand All @@ -164,7 +164,7 @@ pub fn output_coverage_results(
// Emit an opening escape if there was a closing one and we
// had to continue the highlight
if must_highlight && !closing_escapes.is_empty() {
closing_escapes.push((0_usize, true));
closing_escapes.push((0, true));
must_highlight = false;
}
// Continue the highlight in the next lines if we had an
Expand Down Expand Up @@ -224,7 +224,7 @@ pub fn output_coverage_results(
fn results_with_nonexisting_regions_in_line(
results: &Vec<CovResult>,
line: &String,
idx: usize,
idx: LineNumber,
) -> bool {
let results_with_oob_regions = results.iter().filter(|m| {
m.region.start.0 == idx
Expand All @@ -242,14 +242,14 @@ fn results_with_nonexisting_regions_in_line(
/// 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 {
fn insert_escapes(str: &str, markers: Vec<(ColumnNumber, 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 escape_markers: Vec<(&usize, &str)> =
let mut escape_markers: Vec<(&ColumnNumber, &str)> =
markers.iter().map(|(i, b)| (i, if *b { open_escape } else { close_escape })).collect();
escape_markers.sort();

Expand Down
23 changes: 11 additions & 12 deletions tools/kani-cov/src/summary.rs
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,8 @@ use crate::{
args::{SummaryArgs, SummaryFormat},
coverage::{
CombinedCoverageResults, CovResult, CoverageMetric, CoverageRegion, FileCoverageInfo,
FunctionInfo, MarkerInfo, function_coverage_results, function_info_from_file,
Function, FunctionInfo, LineNumber, MarkerInfo, function_coverage_results,
function_info_from_file,
},
};

Expand Down Expand Up @@ -87,7 +88,7 @@ fn calculate_cov_info(file: &Path, file_cov_info: &[FunctionCoverageResults]) ->
}
}

fn function_coverage_info(cov_results: &Option<(String, Vec<CovResult>)>) -> bool {
fn function_coverage_info(cov_results: &Option<(Function, Vec<CovResult>)>) -> bool {
if let Some(res) = cov_results { res.1.iter().any(|c| c.times_covered > 0) } else { false }
}

Expand All @@ -109,8 +110,8 @@ pub fn validate_summary_args(_args: &SummaryArgs) -> Result<()> {

/// Computes coverage results from a line-based perspective.
///
/// Basically, for each line we produce an `<Option<(u32, MarkerInfo)>>` result
/// where:
/// Basically, for each line we produce an `<Option<(usize, MarkerInfo)>>`
/// 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
Expand All @@ -124,10 +125,10 @@ 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<CovResult>)>,
fun_results: &Option<(Function, Vec<CovResult>)>,
) -> Vec<Option<(usize, MarkerInfo)>> {
let start_line: usize = info.start.0;
let end_line: usize = info.end.0;
let start_line = info.start.0;
let end_line = info.end.0;

let mut line_status: Vec<Option<(usize, MarkerInfo)>> =
Vec::with_capacity(end_line - start_line + 1);
Expand All @@ -140,7 +141,7 @@ pub fn line_coverage_results(
/// 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: usize, region: &CoverageRegion) -> bool {
fn line_relevant_to_region(line: LineNumber, region: &CoverageRegion) -> bool {
region.start.0 <= line && region.end.0 >= line
}

Expand Down Expand Up @@ -175,7 +176,7 @@ pub fn line_coverage_results(
/// coverage results for a given function.
pub fn line_coverage_info(
info: &FunctionInfo,
fun_results: &Option<(String, Vec<crate::coverage::CovResult>)>,
fun_results: &Option<(Function, Vec<CovResult>)>,
) -> (usize, usize) {
let line_status = line_coverage_results(info, fun_results);
let total_lines = line_status.iter().filter(|s| s.is_some()).count();
Expand All @@ -186,9 +187,7 @@ pub fn line_coverage_info(

/// 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<crate::coverage::CovResult>)>,
) -> (usize, usize) {
fn region_coverage_info(fun_results: &Option<(Function, Vec<CovResult>)>) -> (usize, usize) {
if let Some(res) = fun_results {
let total_regions = res.1.len();
let covered_regions = res.1.iter().filter(|c| c.times_covered > 0).count();
Expand Down

0 comments on commit c7606f3

Please sign in to comment.