Skip to content

Commit

Permalink
remove cli-table dependency; print manually
Browse files Browse the repository at this point in the history
  • Loading branch information
@carolynzech
carolynzech committed Oct 1, 2024
1 parent 0854cb3 commit 7faeb2a
Show file tree
Hide file tree
Showing 4 changed files with 145 additions and 111 deletions.
62 changes: 9 additions & 53 deletions Cargo.lock
View file
Original file line number Diff line number Diff line change
Expand Up @@ -176,7 +176,7 @@ dependencies = [
"heck",
"proc-macro2",
"quote",
"syn 2.0.79",
"syn",
]

[[package]]
Expand All @@ -185,29 +185,6 @@ version = "0.7.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "1462739cb27611015575c0c11df5df7601141071f07518d56fcc1be504cbec97"

[[package]]
name = "cli-table"
version = "0.4.9"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "b53f9241f288a7b12c56565f04aaeaeeab6b8923d42d99255d4ca428b4d97f89"
dependencies = [
"cli-table-derive",
"csv",
"termcolor",
"unicode-width",
]

[[package]]
name = "cli-table-derive"
version = "0.4.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "3e83a93253aaae7c74eb7428ce4faa6e219ba94886908048888701819f82fb94"
dependencies = [
"proc-macro2",
"quote",
"syn 1.0.109",
]

[[package]]
name = "colorchoice"
version = "1.0.2"
Expand Down Expand Up @@ -515,7 +492,7 @@ dependencies = [
"shell-words",
"strum",
"strum_macros",
"syn 2.0.79",
"syn",
"tracing",
"tracing-subscriber",
"tracing-tree",
Expand All @@ -528,7 +505,6 @@ dependencies = [
"anyhow",
"cargo_metadata",
"clap",
"cli-table",
"colour",
"comfy-table",
"console",
Expand Down Expand Up @@ -575,7 +551,7 @@ dependencies = [
"proc-macro-error2",
"proc-macro2",
"quote",
"syn 2.0.79",
"syn",
]

[[package]]
Expand Down Expand Up @@ -862,7 +838,7 @@ dependencies = [
"proc-macro-error-attr2",
"proc-macro2",
"quote",
"syn 2.0.79",
"syn",
]

[[package]]
Expand Down Expand Up @@ -1070,7 +1046,7 @@ checksum = "243902eda00fad750862fc144cea25caca5e20d615af0a81bee94ca738f1df1f"
dependencies = [
"proc-macro2",
"quote",
"syn 2.0.79",
"syn",
]

[[package]]
Expand Down Expand Up @@ -1178,18 +1154,7 @@ dependencies = [
"proc-macro2",
"quote",
"rustversion",
"syn 2.0.79",
]

[[package]]
name = "syn"
version = "1.0.109"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237"
dependencies = [
"proc-macro2",
"quote",
"unicode-ident",
"syn",
]

[[package]]
Expand All @@ -1216,15 +1181,6 @@ dependencies = [
"windows-sys 0.59.0",
]

[[package]]
name = "termcolor"
version = "1.4.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "06794f8f6c5c898b3275aebefa6b8a1cb24cd2c6c79397ab15774837a0bc5755"
dependencies = [
"winapi-util",
]

[[package]]
name = "thiserror"
version = "1.0.64"
Expand All @@ -1242,7 +1198,7 @@ checksum = "08904e7672f5eb876eaaf87e0ce17857500934f4981c4a0ab2b4aa98baac7fc3"
dependencies = [
"proc-macro2",
"quote",
"syn 2.0.79",
"syn",
]

[[package]]
Expand Down Expand Up @@ -1339,7 +1295,7 @@ checksum = "34704c8d6ebcbc939824180af020566b01a7c01f80641264eba0999f6c2b6be7"
dependencies = [
"proc-macro2",
"quote",
"syn 2.0.79",
"syn",
]

[[package]]
Expand Down Expand Up @@ -1626,5 +1582,5 @@ checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e"
dependencies = [
"proc-macro2",
"quote",
"syn 2.0.79",
"syn",
]
1 change: 0 additions & 1 deletion kani-driver/Cargo.toml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,6 @@ once_cell = "1.19.0"
serde = { version = "1", features = ["derive"] }
serde_json = { version = "1", features = ["preserve_order"] }
clap = { version = "4.4.11", features = ["derive"] }
cli-table = "0.4.9"
colour = "2.1.0"
glob = "0.3"
toml = "0.8"
Expand Down
158 changes: 120 additions & 38 deletions kani-driver/src/list/output.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,14 +3,14 @@
// This module handles outputting the result for the list subcommand

use std::{
cmp::max,
collections::{BTreeMap, BTreeSet},
fs::File,
io::BufWriter,
};

use crate::{list::Totals, version::KANI_VERSION};
use anyhow::Result;
use cli_table::{Cell, CellStruct, Style, Table, print_stdout};
use colour::print_ln_bold;
use kani_metadata::ContractedFunction;
use serde_json::json;
Expand All @@ -20,54 +20,135 @@ use serde_json::json;
const FILE_VERSION: &str = "0.1";
const JSON_FILENAME: &str = "kani-list.json";

pub fn pretty(
standard_harnesses: BTreeMap<String, BTreeSet<String>>,
/// Construct the table of contracts information.
fn construct_contracts_table(
contracted_functions: BTreeSet<ContractedFunction>,
totals: Totals,
) -> Result<()> {
fn format_contract_harnesses(harnesses: &mut [String]) -> String {
harnesses.sort();
let joined = harnesses.join("\n");
if joined.is_empty() { "NONE".to_string() } else { joined }
) -> Vec<String> {
const NO_HARNESSES_MSG: &str = "NONE";

// Since the harnesses will be separated by newlines, the harness length is equal to the length of the longest harness
fn harnesses_len(harnesses: &[String]) -> usize {
harnesses.iter().map(|s| s.len()).max().unwrap_or(NO_HARNESSES_MSG.len())
}

print_ln_bold!("\nContracts:");
println!(
"Each function in the table below either has contracts or is the target of a contract harness (#[kani::proof_for_contract])."
// Contracts table headers
const FUNCTION_HEADER: &str = "Function";
const CONTRACTS_COUNT_HEADER: &str = "# of Contracts";
const CONTRACT_HARNESSES_HEADER: &str = "Contract Harnesses (#[kani::proof_for_contract])";

// Contracts table totals row
const TOTALS_HEADER: &str = "Total";
let functions_total = totals.contracted_functions.to_string();
let contracts_total = totals.contracts.to_string();
let harnesses_total = totals.contract_harnesses.to_string();

let mut table_rows: Vec<String> = vec![];
let mut max_function_fmt_width = max(FUNCTION_HEADER.len(), functions_total.len());
let mut max_contracts_count_fmt_width =
max(CONTRACTS_COUNT_HEADER.len(), contracts_total.len());
let mut max_contract_harnesses_fmt_width =
max(CONTRACT_HARNESSES_HEADER.len(), harnesses_total.len());

let mut data_rows: Vec<(String, String, Vec<String>)> = vec![];

for cf in contracted_functions {
max_function_fmt_width = max(max_function_fmt_width, cf.function.len());
max_contracts_count_fmt_width = max(max_contracts_count_fmt_width, cf.total_contracts);
max_contract_harnesses_fmt_width =
max(max_contract_harnesses_fmt_width, harnesses_len(&cf.harnesses));

data_rows.push((cf.function, cf.total_contracts.to_string(), cf.harnesses));
}

let function_sep = "-".repeat(max_function_fmt_width);
let contracts_count_sep = "-".repeat(max_contracts_count_fmt_width);
let contract_harnesses_sep = "-".repeat(max_contract_harnesses_fmt_width);
let totals_sep = "-".repeat(TOTALS_HEADER.len());

let sep_row = format!(
"| {totals_sep} | {function_sep} | {contracts_count_sep} | {contract_harnesses_sep} |"
);
table_rows.push(sep_row.clone());

if contracted_functions.is_empty() {
println!("No contracts or contract harnesses found.")
} else {
let mut contracts_table: Vec<Vec<CellStruct>> = vec![];

for mut cf in contracted_functions {
contracts_table.push(vec![
"".cell(),
cf.function.cell(),
cf.total_contracts.cell(),
format_contract_harnesses(&mut cf.harnesses).cell(),
]);
let function_space = " ".repeat(max_function_fmt_width - FUNCTION_HEADER.len());
let contracts_count_space =
" ".repeat(max_contracts_count_fmt_width - CONTRACTS_COUNT_HEADER.len());
let contract_harnesses_space =
" ".repeat(max_contract_harnesses_fmt_width - CONTRACT_HARNESSES_HEADER.len());
let totals_space = " ".repeat(TOTALS_HEADER.len());

let header_row = format!(
"| {totals_space} | {FUNCTION_HEADER}{function_space} | {CONTRACTS_COUNT_HEADER}{contracts_count_space} | {CONTRACT_HARNESSES_HEADER}{contract_harnesses_space} |"
);
table_rows.push(header_row);
table_rows.push(sep_row.clone());

for (function, total_contracts, harnesses) in data_rows {
let function_space = " ".repeat(max_function_fmt_width - function.len());
let contracts_count_space =
" ".repeat(max_contracts_count_fmt_width - total_contracts.len());
let first_harness = harnesses.first().map_or(NO_HARNESSES_MSG, |v| v);
let contract_harnesses_space =
" ".repeat(max_contract_harnesses_fmt_width - first_harness.len());

let first_row = format!(
"| {totals_space} | {function}{function_space} | {total_contracts}{contracts_count_space} | {first_harness}{contract_harnesses_space} |"
);
table_rows.push(first_row);

for subsequent_harness in harnesses.iter().skip(1) {
let function_space = " ".repeat(max_function_fmt_width);
let contracts_count_space = " ".repeat(max_contracts_count_fmt_width);
let contract_harnesses_space =
" ".repeat(max_contract_harnesses_fmt_width - subsequent_harness.len());
let row = format!(
"| {totals_space} | {function_space} | {contracts_count_space} | {subsequent_harness}{contract_harnesses_space} |"
);
table_rows.push(row);
}

contracts_table.push(vec![
"Total".cell().bold(true),
totals.contracted_functions.cell(),
totals.contracts.cell(),
totals.contract_harnesses.cell(),
]);

print_stdout(contracts_table.table().title(vec![
"".cell(),
"Function".cell().bold(true),
"# of Contracts".cell().bold(true),
"Contract Harnesses".cell().bold(true),
]))?;
table_rows.push(sep_row.clone())
}

print_ln_bold!("\nStandard Harnesses (#[kani::proof]):");
let total_function_space = " ".repeat(max_function_fmt_width - functions_total.len());
let total_contracts_space = " ".repeat(max_contracts_count_fmt_width - contracts_total.len());
let total_harnesses_space =
" ".repeat(max_contract_harnesses_fmt_width - harnesses_total.len());

let totals_row = format!(
"| {TOTALS_HEADER} | {functions_total}{total_function_space} | {contracts_total}{total_contracts_space} | {harnesses_total}{total_harnesses_space} |"
);

table_rows.push(totals_row);
table_rows.push(sep_row.clone());

table_rows
}

/// Output results as a table printed to the terminal.
pub fn pretty(
standard_harnesses: BTreeMap<String, BTreeSet<String>>,
contracted_functions: BTreeSet<ContractedFunction>,
totals: Totals,
) -> Result<()> {
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}");

if contracted_functions.is_empty() {
println!("{NO_CONTRACTS_MSG}");
} else {
let table_rows = construct_contracts_table(contracted_functions, totals);
println!("{}", table_rows.join("\n"));
};

print_ln_bold!("\n{HARNESSES_SECTION}");
if standard_harnesses.is_empty() {
println!("No standard harnesses found.");
println!("{NO_HARNESSES_MSG}");
}

let mut std_harness_index = 0;
Expand All @@ -84,6 +165,7 @@ pub fn pretty(
Ok(())
}

/// Output results as a JSON file.
pub fn json(
standard_harnesses: BTreeMap<String, BTreeSet<String>>,
contract_harnesses: BTreeMap<String, BTreeSet<String>>,
Expand Down
35 changes: 16 additions & 19 deletions rfc/src/rfcs/0013-list.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,25 +39,22 @@ For example:
Kani Rust Verifier 0.54.0 (standalone)
Contracts:
Each function in the table below either has contracts
or is the target of a contract harness (#[kani::proof_for_contract]).
|-------|-------------------------|----------------|-------------------------------------|
| | Function | # of Contracts | Contract Harnesses |
|-------|-------------------------|----------------|-------------------------------------|
| | example::impl::bar | 4 | example::verify::check_bar |
|-------|-------------------------|----------------|-------------------------------------|
| | example::impl::baz | 0 | example::verify::check_baz |
|-------|-------------------------|----------------|-------------------------------------|
| | example::impl::foo | 2 | example::verify::check_foo_u32 |
| | | | example::verify::check_foo_u64 |
|-------|-------------------------|----------------|-------------------------------------|
| | example::impl::func | 1 | example::verify::check_func |
|-------|-------------------------|----------------|-------------------------------------|
| | example::prep::parse | 1 | NONE |
|-------|-------------------------|----------------|-------------------------------------|
| Total | 5 | 8 | 5 |
|-------|-------------------------|----------------|-------------------------------------|
|-------|-------------------------|----------------|--------------------------------------------------|
| | Function | # of Contracts | Contract Harnesses (#[kani::proof_for_contract]) |
|-------|-------------------------|----------------|--------------------------------------------------|
| | example::impl::bar | 4 | example::verify::check_bar |
|-------|-------------------------|----------------|--------------------------------------------------|
| | example::impl::baz | 0 | example::verify::check_baz |
|-------|-------------------------|----------------|--------------------------------------------------|
| | example::impl::foo | 2 | example::verify::check_foo_u32 |
| | | | example::verify::check_foo_u64 |
|-------|-------------------------|----------------|--------------------------------------------------|
| | example::impl::func | 1 | example::verify::check_func |
|-------|-------------------------|----------------|--------------------------------------------------|
| | example::prep::parse | 1 | NONE |
|-------|-------------------------|----------------|--------------------------------------------------|
| Total | 5 | 8 | 5 |
|-------|-------------------------|----------------|--------------------------------------------------|
Standard Harnesses (#[kani::proof]):
1. example::verify::check_modify
Expand Down

0 comments on commit 7faeb2a

Please sign in to comment.