Skip to content

Commit

Permalink
write markdown to a file; don't print if quiet
Browse files Browse the repository at this point in the history
  • Loading branch information
@carolynzech
carolynzech committed Nov 20, 2024
1 parent a8afa4d commit fa5627b
Show file tree
Hide file tree
Showing 4 changed files with 132 additions and 123 deletions.
6 changes: 3 additions & 3 deletions kani-driver/src/args/list_args.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,15 +42,15 @@ pub struct StandaloneListArgs {
pub std: bool,
}

/// Message formats available for the subcommand.
/// Output formats available for the subcommand.
#[derive(Copy, Clone, Debug, PartialEq, Eq, ValueEnum, strum_macros::Display)]
#[strum(serialize_all = "kebab-case")]
pub enum Format {
/// Print output in human-readable format.
Pretty,
/// Print output in Markdown format.
/// Write output to a Markdown file.
Markdown,
/// Print output in JSON format.
/// Write output to a JSON file.
Json,
}

Expand Down
42 changes: 21 additions & 21 deletions kani-driver/src/list/collect_metadata.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,9 +8,9 @@ use crate::{
InvocationType,
args::{
VerificationArgs,
list_args::{CargoListArgs, Format, StandaloneListArgs},
list_args::{CargoListArgs, StandaloneListArgs},
},
list::Totals,
list::ListMetadata,
list::output::output_list_results,
project::{Project, cargo_project, standalone_project, std_project},
session::KaniSession,
Expand All @@ -20,7 +20,7 @@ use anyhow::Result;
use kani_metadata::{ContractedFunction, HarnessKind, KaniMetadata};

/// Process the KaniMetadata output from kani-compiler and output the list subcommand results
fn process_metadata(metadata: Vec<KaniMetadata>, format: Format) -> Result<()> {
fn process_metadata(metadata: Vec<KaniMetadata>) -> ListMetadata {
// We use ordered maps and sets so that the output is in lexicographic order (and consistent across invocations).

// Map each file to a vector of its harnesses.
Expand All @@ -29,14 +29,14 @@ fn process_metadata(metadata: Vec<KaniMetadata>, format: Format) -> Result<()> {

let mut contracted_functions: BTreeSet<ContractedFunction> = BTreeSet::new();

let mut total_standard_harnesses = 0;
let mut total_contract_harnesses = 0;
let mut standard_harnesses_count = 0;
let mut contract_harnesses_count = 0;

for kani_meta in metadata {
for harness_meta in kani_meta.proof_harnesses {
match harness_meta.attributes.kind {
HarnessKind::Proof => {
total_standard_harnesses += 1;
standard_harnesses_count += 1;
if let Some(harnesses) = standard_harnesses.get_mut(&harness_meta.original_file)
{
harnesses.insert(harness_meta.pretty_name);
Expand All @@ -48,7 +48,7 @@ fn process_metadata(metadata: Vec<KaniMetadata>, format: Format) -> Result<()> {
}
}
HarnessKind::ProofForContract { .. } => {
total_contract_harnesses += 1;
contract_harnesses_count += 1;
if let Some(harnesses) = contract_harnesses.get_mut(&harness_meta.original_file)
{
harnesses.insert(harness_meta.pretty_name);
Expand All @@ -66,36 +66,34 @@ fn process_metadata(metadata: Vec<KaniMetadata>, format: Format) -> Result<()> {
contracted_functions.extend(kani_meta.contracted_functions.into_iter());
}

let totals = Totals {
standard_harnesses: total_standard_harnesses,
contract_harnesses: total_contract_harnesses,
contracted_functions: contracted_functions.len(),
};

output_list_results(
ListMetadata {
standard_harnesses,
standard_harnesses_count,
contract_harnesses,
contract_harnesses_count,
contracted_functions,
totals,
format,
)
}
}

pub fn list_cargo(args: CargoListArgs, mut verify_opts: VerificationArgs) -> Result<()> {
let quiet = args.common_args.quiet;
verify_opts.common_args = args.common_args;
let session = KaniSession::new(verify_opts)?;
if !session.args.common_args.quiet {
if !quiet {
print_kani_version(InvocationType::CargoKani(vec![]));
}

let project = cargo_project(&session, false)?;
process_metadata(project.metadata, args.format)
let list_metadata = process_metadata(project.metadata);

output_list_results(list_metadata, args.format, quiet)
}

pub fn list_standalone(args: StandaloneListArgs, mut verify_opts: VerificationArgs) -> Result<()> {
let quiet = args.common_args.quiet;
verify_opts.common_args = args.common_args;
let session = KaniSession::new(verify_opts)?;
if !session.args.common_args.quiet {
if !quiet {
print_kani_version(InvocationType::Standalone);
}

Expand All @@ -105,5 +103,7 @@ pub fn list_standalone(args: StandaloneListArgs, mut verify_opts: VerificationAr
standalone_project(&args.input, args.crate_name, &session)?
};

process_metadata(project.metadata, args.format)
let list_metadata = process_metadata(project.metadata);

output_list_results(list_metadata, args.format, quiet)
}
20 changes: 14 additions & 6 deletions kani-driver/src/list/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,13 +2,21 @@
// SPDX-License-Identifier: Apache-2.0 OR MIT
// Implements the list subcommand logic

use kani_metadata::ContractedFunction;
use std::collections::{BTreeMap, BTreeSet};

pub mod collect_metadata;
mod output;

/// Stores the total count of standard harnesses, contract harnesses,
/// and functions under contract across all `KaniMetadata` objects.
struct Totals {
standard_harnesses: usize,
contract_harnesses: usize,
contracted_functions: usize,
struct ListMetadata {
// Files mapped to their #[kani::proof] harnesses
standard_harnesses: BTreeMap<String, BTreeSet<String>>,
// Total number of #[kani::proof] harnesses
standard_harnesses_count: usize,
// Files mapped to their #[kani::proof_for_contract] harnesses
contract_harnesses: BTreeMap<String, BTreeSet<String>>,
// Total number of #[kani:proof_for_contract] harnesses
contract_harnesses_count: usize,
// Set of all functions under contract
contracted_functions: BTreeSet<ContractedFunction>,
}
187 changes: 94 additions & 93 deletions kani-driver/src/list/output.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,31 +3,99 @@
//! This module handles outputting the result for the list subcommand
use std::{
collections::{BTreeMap, BTreeSet},
fmt::Display,
fs::File,
io::BufWriter,
io::{BufWriter, Write},
path::Path,
};

use crate::{args::list_args::Format, list::Totals, version::KANI_VERSION};
use crate::{args::list_args::Format, list::ListMetadata, version::KANI_VERSION};
use anyhow::Result;
use colour::print_ln_bold;
use comfy_table::Table as PrettyTable;
use kani_metadata::ContractedFunction;
use serde_json::json;
use to_markdown_table::MarkdownTable;

// Represents the version of our JSON file format.
// Increment this version (according to semantic versioning rules) whenever the JSON output format changes.
const FILE_VERSION: &str = "0.1";
const JSON_FILENAME: &str = "kani-list.json";
const OUTPUT_FILENAME: &str = "kani-list";

/// Output the results of the list subcommand.
pub fn output_list_results(list_metadata: ListMetadata, format: Format, quiet: bool) -> Result<()> {
match format {
Format::Pretty => pretty(list_metadata),
Format::Markdown => markdown(list_metadata, quiet),
Format::Json => json(list_metadata, quiet),
}
}

/// Print results to the terminal.
fn pretty(list_metadata: ListMetadata) -> Result<()> {
let table = if list_metadata.contracted_functions.is_empty() {
None
} else {
let (header, rows) = construct_contracts_table(&list_metadata);
let mut t = PrettyTable::new();
t.set_header(header).add_rows(rows);
Some(t)
};
let output = format_results(table, &list_metadata);
println!("{}", output);

Ok(())
}

/// Output results to a Markdown file.
fn markdown(list_metadata: ListMetadata, quiet: bool) -> Result<()> {
let table = if list_metadata.contracted_functions.is_empty() {
None
} else {
let (header, rows) = construct_contracts_table(&list_metadata);
Some(MarkdownTable::new(Some(header), rows)?)
};

let output = format_results(table, &list_metadata);

let out_path = Path::new(OUTPUT_FILENAME).with_extension("md");
let mut out_file = File::create(&out_path).unwrap();
out_file.write_all(output.as_bytes()).unwrap();
if !quiet {
println!("Wrote list results to {}", std::fs::canonicalize(&out_path)?.display());
}
Ok(())
}

/// Output results as a JSON file.
fn json(list_metadata: ListMetadata, quiet: bool) -> Result<()> {
let out_path = Path::new(OUTPUT_FILENAME).with_extension("json");
let out_file = File::create(&out_path).unwrap();
let writer = BufWriter::new(out_file);

let json_obj = json!({
"kani-version": KANI_VERSION,
"file-version": FILE_VERSION,
"standard-harnesses": &list_metadata.standard_harnesses,
"contract-harnesses": &list_metadata.contract_harnesses,
"contracts": &list_metadata.contracted_functions,
"totals": {
"standard-harnesses": list_metadata.standard_harnesses_count,
"contract-harnesses": list_metadata.contract_harnesses_count,
"functions-under-contract": list_metadata.contracted_functions.len(),
}
});

serde_json::to_writer_pretty(writer, &json_obj)?;

if !quiet {
println!("Wrote list results to {}", std::fs::canonicalize(out_path)?.display());
}

Ok(())
}

/// Construct the rows for the table of contracts information.
/// Returns a tuple of the table header and the rows.
fn construct_contracts_table(
contracted_functions: BTreeSet<ContractedFunction>,
totals: Totals,
) -> (Vec<String>, Vec<Vec<String>>) {
fn construct_contracts_table(list_metadata: &ListMetadata) -> (Vec<String>, Vec<Vec<String>>) {
const NO_HARNESSES_MSG: &str = "NONE";
const FUNCTION_HEADER: &str = "Function";
const CONTRACT_HARNESSES_HEADER: &str = "Contract Harnesses (#[kani::proof_for_contract])";
Expand All @@ -38,8 +106,8 @@ fn construct_contracts_table(

let mut rows: Vec<Vec<String>> = vec![];

for cf in contracted_functions {
let mut row = vec![String::new(), cf.function];
for cf in &list_metadata.contracted_functions {
let mut row = vec![String::new(), cf.function.clone()];
if cf.harnesses.is_empty() {
row.push(NO_HARNESSES_MSG.to_string());
} else {
Expand All @@ -50,110 +118,43 @@ fn construct_contracts_table(

let totals_row = vec![
TOTALS_HEADER.to_string(),
totals.contracted_functions.to_string(),
totals.contract_harnesses.to_string(),
list_metadata.contracted_functions.len().to_string(),
list_metadata.contract_harnesses_count.to_string(),
];
rows.push(totals_row);

(header, rows)
}

/// Print results to the terminal.
fn print_results<T: Display>(
table: Option<T>,
standard_harnesses: BTreeMap<String, BTreeSet<String>>,
) {
/// Format results as a String
fn format_results<T: Display>(table: Option<T>, list_metadata: &ListMetadata) -> String {
const CONTRACTS_SECTION: &str = "Contracts:";
const HARNESSES_SECTION: &str = "Standard Harnesses (#[kani::proof]):";
const NO_CONTRACTS_MSG: &str = "No contracts or contract harnesses found.";
const NO_HARNESSES_MSG: &str = "No standard harnesses found.";

print_ln_bold!("\n{CONTRACTS_SECTION}");
let mut output: Vec<String> = vec![];
output.push(format!("\n{CONTRACTS_SECTION}"));

if let Some(table) = table {
println!("{table}");
output.push(format!("{table}"));
} else {
println!("{NO_CONTRACTS_MSG}");
output.push(NO_CONTRACTS_MSG.to_string());
}

print_ln_bold!("\n{HARNESSES_SECTION}");
if standard_harnesses.is_empty() {
println!("{NO_HARNESSES_MSG}");
output.push(format!("\n{HARNESSES_SECTION}"));
if list_metadata.standard_harnesses.is_empty() {
output.push(NO_HARNESSES_MSG.to_string());
}

let mut std_harness_index = 0;

for (_, harnesses) in standard_harnesses {
for harnesses in (&list_metadata.standard_harnesses).values() {
for harness in harnesses {
println!("{}. {harness}", std_harness_index + 1);
output.push(format!("{}. {harness}", std_harness_index + 1));
std_harness_index += 1;
}
}

println!();
}

/// Output results as a JSON file.
fn json(
standard_harnesses: BTreeMap<String, BTreeSet<String>>,
contract_harnesses: BTreeMap<String, BTreeSet<String>>,
contracted_functions: BTreeSet<ContractedFunction>,
totals: Totals,
) -> Result<()> {
let out_file = File::create(JSON_FILENAME).unwrap();
let writer = BufWriter::new(out_file);

let json_obj = json!({
"kani-version": KANI_VERSION,
"file-version": FILE_VERSION,
"standard-harnesses": &standard_harnesses,
"contract-harnesses": &contract_harnesses,
"contracts": &contracted_functions,
"totals": {
"standard-harnesses": totals.standard_harnesses,
"contract-harnesses": totals.contract_harnesses,
"functions-under-contract": totals.contracted_functions,
}
});

serde_json::to_writer_pretty(writer, &json_obj)?;

println!("Wrote list results to {}", std::fs::canonicalize(JSON_FILENAME)?.display());

Ok(())
}

/// Output the results of the list subcommand.
pub fn output_list_results(
standard_harnesses: BTreeMap<String, BTreeSet<String>>,
contract_harnesses: BTreeMap<String, BTreeSet<String>>,
contracted_functions: BTreeSet<ContractedFunction>,
totals: Totals,
format: Format,
) -> Result<()> {
match format {
Format::Pretty => {
let table = if totals.contracted_functions == 0 {
None
} else {
let (header, rows) = construct_contracts_table(contracted_functions, totals);
let mut t = PrettyTable::new();
t.set_header(header).add_rows(rows);
Some(t)
};
print_results(table, standard_harnesses);
Ok(())
}
Format::Markdown => {
let table = if totals.contracted_functions == 0 {
None
} else {
let (header, rows) = construct_contracts_table(contracted_functions, totals);
Some(MarkdownTable::new(Some(header), rows)?)
};
print_results(table, standard_harnesses);
Ok(())
}
Format::Json => json(standard_harnesses, contract_harnesses, contracted_functions, totals),
}
output.join("\n")
}

0 comments on commit fa5627b

Please sign in to comment.