From acec7a5d89e8ecf32e30857d9afdc3b6932efe1b Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Mon, 18 Nov 2024 23:20:05 -0500 Subject: [PATCH 1/6] use CommonArgs instead of VerificationArgs --- kani-driver/src/args/list_args.rs | 16 +++++++--------- kani-driver/src/list/collect_metadata.rs | 15 ++++++++++----- kani-driver/src/main.rs | 8 +++++--- 3 files changed, 22 insertions(+), 17 deletions(-) diff --git a/kani-driver/src/args/list_args.rs b/kani-driver/src/args/list_args.rs index 7129bd0a85c4..ac94748323d0 100644 --- a/kani-driver/src/args/list_args.rs +++ b/kani-driver/src/args/list_args.rs @@ -4,17 +4,15 @@ use std::path::PathBuf; -use crate::args::ValidateArgs; +use crate::args::{CommonArgs, ValidateArgs}; use clap::{Error, Parser, ValueEnum, error::ErrorKind}; use kani_metadata::UnstableFeature; -use super::VerificationArgs; - /// List information relevant to verification #[derive(Debug, Parser)] pub struct CargoListArgs { #[command(flatten)] - pub verify_opts: VerificationArgs, + pub common_args: CommonArgs, /// Output format #[clap(long, default_value = "pretty")] @@ -32,7 +30,7 @@ pub struct StandaloneListArgs { pub crate_name: Option, #[command(flatten)] - pub verify_opts: VerificationArgs, + pub common_args: CommonArgs, /// Output format #[clap(long, default_value = "pretty")] @@ -56,8 +54,8 @@ pub enum Format { impl ValidateArgs for CargoListArgs { fn validate(&self) -> Result<(), Error> { - self.verify_opts.validate()?; - if !self.verify_opts.common_args.unstable_features.contains(UnstableFeature::List) { + self.common_args.validate()?; + if !self.common_args.unstable_features.contains(UnstableFeature::List) { return Err(Error::raw( ErrorKind::MissingRequiredArgument, "The `list` subcommand is unstable and requires -Z list", @@ -70,8 +68,8 @@ impl ValidateArgs for CargoListArgs { impl ValidateArgs for StandaloneListArgs { fn validate(&self) -> Result<(), Error> { - self.verify_opts.validate()?; - if !self.verify_opts.common_args.unstable_features.contains(UnstableFeature::List) { + self.common_args.validate()?; + if !self.common_args.unstable_features.contains(UnstableFeature::List) { return Err(Error::raw( ErrorKind::MissingRequiredArgument, "The `list` subcommand is unstable and requires -Z list", diff --git a/kani-driver/src/list/collect_metadata.rs b/kani-driver/src/list/collect_metadata.rs index 99da0477314d..04c3689a2ae0 100644 --- a/kani-driver/src/list/collect_metadata.rs +++ b/kani-driver/src/list/collect_metadata.rs @@ -6,7 +6,10 @@ use std::collections::{BTreeMap, BTreeSet}; use crate::{ InvocationType, - args::list_args::{CargoListArgs, Format, StandaloneListArgs}, + args::{ + VerificationArgs, + list_args::{CargoListArgs, Format, StandaloneListArgs}, + }, list::Totals, list::output::{json, pretty}, project::{Project, cargo_project, standalone_project, std_project}, @@ -75,8 +78,9 @@ fn process_metadata(metadata: Vec, format: Format) -> Result<()> { } } -pub fn list_cargo(args: CargoListArgs) -> Result<()> { - let session = KaniSession::new(args.verify_opts)?; +pub fn list_cargo(args: CargoListArgs, mut verify_opts: VerificationArgs) -> Result<()> { + verify_opts.common_args = args.common_args; + let session = KaniSession::new(verify_opts)?; if !session.args.common_args.quiet { print_kani_version(InvocationType::CargoKani(vec![])); } @@ -85,8 +89,9 @@ pub fn list_cargo(args: CargoListArgs) -> Result<()> { process_metadata(project.metadata, args.format) } -pub fn list_standalone(args: StandaloneListArgs) -> Result<()> { - let session = KaniSession::new(args.verify_opts)?; +pub fn list_standalone(args: StandaloneListArgs, mut verify_opts: VerificationArgs) -> Result<()> { + verify_opts.common_args = args.common_args; + let session = KaniSession::new(verify_opts)?; if !session.args.common_args.quiet { print_kani_version(InvocationType::Standalone); } diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index b0fa22334da0..07405a30a307 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -68,8 +68,8 @@ fn cargokani_main(input_args: Vec) -> Result<()> { let args = args::CargoKaniArgs::parse_from(&input_args); check_is_valid(&args); - if let Some(CargoKaniSubcommand::List(args)) = args.command { - return list_cargo(*args); + if let Some(CargoKaniSubcommand::List(list_args)) = args.command { + return list_cargo(*list_args, args.verify_opts); } let session = session::KaniSession::new(args.verify_opts)?; @@ -104,7 +104,9 @@ fn standalone_main() -> Result<()> { let (session, project) = match args.command { Some(StandaloneSubcommand::Playback(args)) => return playback_standalone(*args), - Some(StandaloneSubcommand::List(args)) => return list_standalone(*args), + Some(StandaloneSubcommand::List(list_args)) => { + return list_standalone(*list_args, args.verify_opts); + } Some(StandaloneSubcommand::VerifyStd(args)) => { let session = KaniSession::new(args.verify_opts)?; if !session.args.common_args.quiet { From fbab96931904f1991aea26145a799413924b96ac Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 19 Nov 2024 00:44:01 -0500 Subject: [PATCH 2/6] change pretty tables to markdown --- Cargo.lock | 10 +++ kani-driver/Cargo.toml | 1 + kani-driver/src/args/list_args.rs | 10 +-- kani-driver/src/list/collect_metadata.rs | 4 +- kani-driver/src/list/output.rs | 96 +++++------------------- 5 files changed, 38 insertions(+), 83 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 66c5a40522e0..9bed46ed62fd 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -826,6 +826,7 @@ dependencies = [ "strum_macros", "tempfile", "time", + "to_markdown_table", "tokio", "toml", "tracing", @@ -1753,6 +1754,15 @@ dependencies = [ "time-core", ] +[[package]] +name = "to_markdown_table" +version = "0.1.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8450ade61b78735ed7811cc14639462723d87a6cd748a41e7bfde554ac5033dd" +dependencies = [ + "thiserror", +] + [[package]] name = "tokio" version = "1.41.1" diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index 844b844b8ef4..1025b4b201e2 100644 --- a/kani-driver/Cargo.toml +++ b/kani-driver/Cargo.toml @@ -17,6 +17,7 @@ cargo_metadata = "0.18.0" anyhow = "1" console = "0.15.1" once_cell = "1.19.0" +to_markdown_table = "0.1.0" serde = { version = "1", features = ["derive"] } serde_json = { version = "1", features = ["preserve_order"] } clap = { version = "4.4.11", features = ["derive"] } diff --git a/kani-driver/src/args/list_args.rs b/kani-driver/src/args/list_args.rs index ac94748323d0..744fd17d3b68 100644 --- a/kani-driver/src/args/list_args.rs +++ b/kani-driver/src/args/list_args.rs @@ -15,7 +15,7 @@ pub struct CargoListArgs { pub common_args: CommonArgs, /// Output format - #[clap(long, default_value = "pretty")] + #[clap(long, default_value = "markdown")] pub format: Format, } @@ -33,7 +33,7 @@ pub struct StandaloneListArgs { pub common_args: CommonArgs, /// Output format - #[clap(long, default_value = "pretty")] + #[clap(long, default_value = "markdown")] pub format: Format, /// Pass this flag to run the `list` command on the standard library. @@ -46,9 +46,9 @@ pub struct StandaloneListArgs { #[derive(Copy, Clone, Debug, PartialEq, Eq, ValueEnum, strum_macros::Display)] #[strum(serialize_all = "kebab-case")] pub enum Format { - /// Print diagnostic messages in a user friendly format. - Pretty, - /// Print diagnostic messages in JSON format. + /// Print output in Markdown format. + Markdown, + /// Print output in JSON format. Json, } diff --git a/kani-driver/src/list/collect_metadata.rs b/kani-driver/src/list/collect_metadata.rs index 04c3689a2ae0..e9db880a146f 100644 --- a/kani-driver/src/list/collect_metadata.rs +++ b/kani-driver/src/list/collect_metadata.rs @@ -11,7 +11,7 @@ use crate::{ list_args::{CargoListArgs, Format, StandaloneListArgs}, }, list::Totals, - list::output::{json, pretty}, + list::output::{json, markdown}, project::{Project, cargo_project, standalone_project, std_project}, session::KaniSession, version::print_kani_version, @@ -73,7 +73,7 @@ fn process_metadata(metadata: Vec, format: Format) -> Result<()> { }; match format { - Format::Pretty => pretty(standard_harnesses, contracted_functions, totals), + Format::Markdown => markdown(standard_harnesses, contracted_functions, totals), Format::Json => json(standard_harnesses, contract_harnesses, contracted_functions, totals), } } diff --git a/kani-driver/src/list/output.rs b/kani-driver/src/list/output.rs index 79a5fcf6fe5e..e2307e502898 100644 --- a/kani-driver/src/list/output.rs +++ b/kani-driver/src/list/output.rs @@ -3,7 +3,6 @@ //! This module handles outputting the result for the list subcommand use std::{ - cmp::max, collections::{BTreeMap, BTreeSet}, fs::File, io::BufWriter, @@ -14,6 +13,7 @@ use anyhow::Result; use colour::print_ln_bold; use kani_metadata::ContractedFunction; use serde_json::json; +use to_markdown_table::{MarkdownTable, MarkdownTableError}; // Represents the version of our JSON file format. // Increment this version (according to semantic versioning rules) whenever the JSON output format changes. @@ -24,96 +24,40 @@ const JSON_FILENAME: &str = "kani-list.json"; fn construct_contracts_table( contracted_functions: BTreeSet, totals: Totals, -) -> Vec { +) -> Result { const NO_HARNESSES_MSG: &str = "NONE"; - - // Since the harnesses will be separated by newlines, the column length is equal to the length of the longest harness - fn column_len(harnesses: &[String]) -> usize { - harnesses.iter().map(|s| s.len()).max().unwrap_or(NO_HARNESSES_MSG.len()) - } - - // Contracts table headers const FUNCTION_HEADER: &str = "Function"; 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 harnesses_total = totals.contract_harnesses.to_string(); - - let mut table_rows: Vec = vec![]; - let mut max_function_fmt_width = max(FUNCTION_HEADER.len(), functions_total.len()); - let mut max_contract_harnesses_fmt_width = - max(CONTRACT_HARNESSES_HEADER.len(), harnesses_total.len()); - let mut data_rows: Vec<(String, Vec)> = vec![]; + let mut table_rows: Vec> = vec![]; for cf in contracted_functions { - max_function_fmt_width = max(max_function_fmt_width, cf.function.len()); - max_contract_harnesses_fmt_width = - max(max_contract_harnesses_fmt_width, column_len(&cf.harnesses)); - - data_rows.push((cf.function, cf.harnesses)); - } - - let function_sep = "-".repeat(max_function_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} | {contract_harnesses_sep} |"); - table_rows.push(sep_row.clone()); - - let function_space = " ".repeat(max_function_fmt_width - FUNCTION_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} | {CONTRACT_HARNESSES_HEADER}{contract_harnesses_space} |" - ); - table_rows.push(header_row); - table_rows.push(sep_row.clone()); - - for (function, harnesses) in data_rows { - let function_space = " ".repeat(max_function_fmt_width - function.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} | {first_harness}{contract_harnesses_space} |" - ); + let first_harness = cf.harnesses.first().map_or(NO_HARNESSES_MSG, |v| v).to_string(); + let first_row = vec![String::new(), cf.function.clone(), first_harness]; table_rows.push(first_row); - for subsequent_harness in harnesses.iter().skip(1) { - let function_space = " ".repeat(max_function_fmt_width); - let contract_harnesses_space = - " ".repeat(max_contract_harnesses_fmt_width - subsequent_harness.len()); - let row = format!( - "| {totals_space} | {function_space} | {subsequent_harness}{contract_harnesses_space} |" - ); + for subsequent_harness in cf.harnesses.iter().skip(1) { + let row = vec![String::new(), cf.function.clone(), subsequent_harness.to_string()]; table_rows.push(row); } - - table_rows.push(sep_row.clone()) } - let total_function_space = " ".repeat(max_function_fmt_width - functions_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} | {harnesses_total}{total_harnesses_space} |" - ); - + let totals_row = vec![ + TOTALS_HEADER.to_string(), + totals.contracted_functions.to_string(), + totals.contract_harnesses.to_string(), + ]; table_rows.push(totals_row); - table_rows.push(sep_row.clone()); - table_rows + let table = + MarkdownTable::new(Some(vec!["", FUNCTION_HEADER, CONTRACT_HARNESSES_HEADER]), table_rows)?; + + Ok(table) } -/// Output results as a table printed to the terminal. -pub fn pretty( +// /// Output results as a table printed to the terminal. +pub fn markdown( standard_harnesses: BTreeMap>, contracted_functions: BTreeSet, totals: Totals, @@ -128,8 +72,8 @@ pub fn pretty( if contracted_functions.is_empty() { println!("{NO_CONTRACTS_MSG}"); } else { - let table_rows = construct_contracts_table(contracted_functions, totals); - println!("{}", table_rows.join("\n")); + let table = construct_contracts_table(contracted_functions, totals)?; + println!("{}", table); }; print_ln_bold!("\n{HARNESSES_SECTION}"); From 0ffbd4ce336e0641043ac1fb9cbbed997d36b3de Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 19 Nov 2024 00:44:17 -0500 Subject: [PATCH 3/6] write JSON filepath --- kani-driver/src/list/output.rs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/kani-driver/src/list/output.rs b/kani-driver/src/list/output.rs index e2307e502898..47f7601292f1 100644 --- a/kani-driver/src/list/output.rs +++ b/kani-driver/src/list/output.rs @@ -120,5 +120,7 @@ pub fn json( serde_json::to_writer_pretty(writer, &json_obj)?; + println!("Wrote list results to {}", std::fs::canonicalize(JSON_FILENAME)?.display()); + Ok(()) } From a8afa4d5f81629d4133ccb03e5ea73f7e8fa6a1a Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 19 Nov 2024 11:35:16 -0500 Subject: [PATCH 4/6] pretty table and markdown table --- kani-driver/src/args/list_args.rs | 6 +- kani-driver/src/args/mod.rs | 4 +- kani-driver/src/list/collect_metadata.rs | 13 ++-- kani-driver/src/list/output.rs | 93 ++++++++++++++++-------- 4 files changed, 77 insertions(+), 39 deletions(-) diff --git a/kani-driver/src/args/list_args.rs b/kani-driver/src/args/list_args.rs index 744fd17d3b68..89970abe0b6b 100644 --- a/kani-driver/src/args/list_args.rs +++ b/kani-driver/src/args/list_args.rs @@ -15,7 +15,7 @@ pub struct CargoListArgs { pub common_args: CommonArgs, /// Output format - #[clap(long, default_value = "markdown")] + #[clap(long, default_value = "pretty")] pub format: Format, } @@ -33,7 +33,7 @@ pub struct StandaloneListArgs { pub common_args: CommonArgs, /// Output format - #[clap(long, default_value = "markdown")] + #[clap(long, default_value = "pretty")] pub format: Format, /// Pass this flag to run the `list` command on the standard library. @@ -46,6 +46,8 @@ pub struct StandaloneListArgs { #[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. Markdown, /// Print output in JSON format. diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 2be3ff58f2fc..66ff247ddc82 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -143,7 +143,7 @@ pub enum StandaloneSubcommand { Playback(Box), /// Verify the rust standard library. VerifyStd(Box), - /// Execute the list subcommand + /// List contracts and harnesses. List(Box), } @@ -171,7 +171,7 @@ pub enum CargoKaniSubcommand { /// Execute concrete playback testcases of a local package. Playback(Box), - /// List metadata relevant to verification, e.g., harnesses. + /// List contracts and harnesses. List(Box), } diff --git a/kani-driver/src/list/collect_metadata.rs b/kani-driver/src/list/collect_metadata.rs index e9db880a146f..50ee19f069c0 100644 --- a/kani-driver/src/list/collect_metadata.rs +++ b/kani-driver/src/list/collect_metadata.rs @@ -11,7 +11,7 @@ use crate::{ list_args::{CargoListArgs, Format, StandaloneListArgs}, }, list::Totals, - list::output::{json, markdown}, + list::output::output_list_results, project::{Project, cargo_project, standalone_project, std_project}, session::KaniSession, version::print_kani_version, @@ -72,10 +72,13 @@ fn process_metadata(metadata: Vec, format: Format) -> Result<()> { contracted_functions: contracted_functions.len(), }; - match format { - Format::Markdown => markdown(standard_harnesses, contracted_functions, totals), - Format::Json => json(standard_harnesses, contract_harnesses, contracted_functions, totals), - } + output_list_results( + standard_harnesses, + contract_harnesses, + contracted_functions, + totals, + format, + ) } pub fn list_cargo(args: CargoListArgs, mut verify_opts: VerificationArgs) -> Result<()> { diff --git a/kani-driver/src/list/output.rs b/kani-driver/src/list/output.rs index 47f7601292f1..0f8842e10852 100644 --- a/kani-driver/src/list/output.rs +++ b/kani-driver/src/list/output.rs @@ -4,43 +4,48 @@ use std::{ collections::{BTreeMap, BTreeSet}, + fmt::Display, fs::File, io::BufWriter, }; -use crate::{list::Totals, version::KANI_VERSION}; +use crate::{args::list_args::Format, list::Totals, 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, MarkdownTableError}; +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"; -/// Construct the table of contracts information. +/// 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, totals: Totals, -) -> Result { +) -> (Vec, Vec>) { const NO_HARNESSES_MSG: &str = "NONE"; const FUNCTION_HEADER: &str = "Function"; const CONTRACT_HARNESSES_HEADER: &str = "Contract Harnesses (#[kani::proof_for_contract])"; const TOTALS_HEADER: &str = "Total"; - let mut table_rows: Vec> = vec![]; + let header = + vec![String::new(), FUNCTION_HEADER.to_string(), CONTRACT_HARNESSES_HEADER.to_string()]; - for cf in contracted_functions { - let first_harness = cf.harnesses.first().map_or(NO_HARNESSES_MSG, |v| v).to_string(); - let first_row = vec![String::new(), cf.function.clone(), first_harness]; - table_rows.push(first_row); + let mut rows: Vec> = vec![]; - for subsequent_harness in cf.harnesses.iter().skip(1) { - let row = vec![String::new(), cf.function.clone(), subsequent_harness.to_string()]; - table_rows.push(row); + for cf in contracted_functions { + let mut row = vec![String::new(), cf.function]; + if cf.harnesses.is_empty() { + row.push(NO_HARNESSES_MSG.to_string()); + } else { + row.push(cf.harnesses.join(", ")); } + rows.push(row); } let totals_row = vec![ @@ -48,20 +53,16 @@ fn construct_contracts_table( totals.contracted_functions.to_string(), totals.contract_harnesses.to_string(), ]; - table_rows.push(totals_row); - - let table = - MarkdownTable::new(Some(vec!["", FUNCTION_HEADER, CONTRACT_HARNESSES_HEADER]), table_rows)?; + rows.push(totals_row); - Ok(table) + (header, rows) } -// /// Output results as a table printed to the terminal. -pub fn markdown( +/// Print results to the terminal. +fn print_results( + table: Option, standard_harnesses: BTreeMap>, - contracted_functions: BTreeSet, - 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."; @@ -69,12 +70,11 @@ pub fn markdown( print_ln_bold!("\n{CONTRACTS_SECTION}"); - if contracted_functions.is_empty() { - println!("{NO_CONTRACTS_MSG}"); + if let Some(table) = table { + println!("{table}"); } else { - let table = construct_contracts_table(contracted_functions, totals)?; - println!("{}", table); - }; + println!("{NO_CONTRACTS_MSG}"); + } print_ln_bold!("\n{HARNESSES_SECTION}"); if standard_harnesses.is_empty() { @@ -91,12 +91,10 @@ pub fn markdown( } println!(); - - Ok(()) } /// Output results as a JSON file. -pub fn json( +fn json( standard_harnesses: BTreeMap>, contract_harnesses: BTreeMap>, contracted_functions: BTreeSet, @@ -124,3 +122,38 @@ pub fn json( Ok(()) } + +/// Output the results of the list subcommand. +pub fn output_list_results( + standard_harnesses: BTreeMap>, + contract_harnesses: BTreeMap>, + contracted_functions: BTreeSet, + 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), + } +} From fa5627b5a042e072effdb2aab7fc93a4663f26e6 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 19 Nov 2024 20:42:07 -0500 Subject: [PATCH 5/6] write markdown to a file; don't print if quiet --- kani-driver/src/args/list_args.rs | 6 +- kani-driver/src/list/collect_metadata.rs | 42 ++--- kani-driver/src/list/mod.rs | 20 ++- kani-driver/src/list/output.rs | 187 ++++++++++++----------- 4 files changed, 132 insertions(+), 123 deletions(-) diff --git a/kani-driver/src/args/list_args.rs b/kani-driver/src/args/list_args.rs index 89970abe0b6b..ebd97d01f2fb 100644 --- a/kani-driver/src/args/list_args.rs +++ b/kani-driver/src/args/list_args.rs @@ -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, } diff --git a/kani-driver/src/list/collect_metadata.rs b/kani-driver/src/list/collect_metadata.rs index 50ee19f069c0..a7901e997ab1 100644 --- a/kani-driver/src/list/collect_metadata.rs +++ b/kani-driver/src/list/collect_metadata.rs @@ -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, @@ -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, format: Format) -> Result<()> { +fn process_metadata(metadata: Vec) -> 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. @@ -29,14 +29,14 @@ fn process_metadata(metadata: Vec, format: Format) -> Result<()> { let mut contracted_functions: BTreeSet = 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); @@ -48,7 +48,7 @@ fn process_metadata(metadata: Vec, 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); @@ -66,36 +66,34 @@ fn process_metadata(metadata: Vec, 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); } @@ -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) } diff --git a/kani-driver/src/list/mod.rs b/kani-driver/src/list/mod.rs index 0987a0e9c927..982c71d0120f 100644 --- a/kani-driver/src/list/mod.rs +++ b/kani-driver/src/list/mod.rs @@ -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>, + // Total number of #[kani::proof] harnesses + standard_harnesses_count: usize, + // Files mapped to their #[kani::proof_for_contract] harnesses + contract_harnesses: BTreeMap>, + // Total number of #[kani:proof_for_contract] harnesses + contract_harnesses_count: usize, + // Set of all functions under contract + contracted_functions: BTreeSet, } diff --git a/kani-driver/src/list/output.rs b/kani-driver/src/list/output.rs index 0f8842e10852..47b32bd6ed5e 100644 --- a/kani-driver/src/list/output.rs +++ b/kani-driver/src/list/output.rs @@ -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, - totals: Totals, -) -> (Vec, Vec>) { +fn construct_contracts_table(list_metadata: &ListMetadata) -> (Vec, Vec>) { const NO_HARNESSES_MSG: &str = "NONE"; const FUNCTION_HEADER: &str = "Function"; const CONTRACT_HARNESSES_HEADER: &str = "Contract Harnesses (#[kani::proof_for_contract])"; @@ -38,8 +106,8 @@ fn construct_contracts_table( let mut rows: Vec> = 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 { @@ -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( - table: Option, - standard_harnesses: BTreeMap>, -) { +/// Format results as a String +fn format_results(table: Option, 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 = 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>, - contract_harnesses: BTreeMap>, - contracted_functions: BTreeSet, - 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>, - contract_harnesses: BTreeMap>, - contracted_functions: BTreeSet, - 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") } From 04daf2c1d54d7c16a877c1bc52b9b23dc670ca00 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 19 Nov 2024 22:00:00 -0500 Subject: [PATCH 6/6] add markdown tests; test that filepath gets printed --- tests/script-based-pre/cargo_list/list.sh | 10 --- .../Cargo.toml | 0 .../config.yml | 0 .../list.expected | 0 .../script-based-pre/cargo_list_json/list.sh | 22 ++++++ .../src/lib.rs | 0 .../src/standard_harnesses.rs | 0 .../script-based-pre/cargo_list_md/.gitignore | 1 + .../script-based-pre/cargo_list_md/Cargo.toml | 10 +++ .../{kani_list => cargo_list_md}/config.yml | 0 .../cargo_list_md/list.expected | 14 ++++ tests/script-based-pre/cargo_list_md/list.sh | 22 ++++++ .../script-based-pre/cargo_list_md/src/lib.rs | 68 ++++++++++++++++++ .../cargo_list_md/src/standard_harnesses.rs | 15 ++++ tests/script-based-pre/kani_list/list.sh | 10 --- .../kani_list_json/config.yml | 4 ++ .../list.expected | 0 tests/script-based-pre/kani_list_json/list.sh | 22 ++++++ .../{kani_list => kani_list_json}/src/lib.rs | 0 .../script-based-pre/kani_list_md/.gitignore | 1 + .../script-based-pre/kani_list_md/config.yml | 4 ++ .../kani_list_md/list.expected | 14 ++++ tests/script-based-pre/kani_list_md/list.sh | 22 ++++++ .../script-based-pre/kani_list_md/src/lib.rs | 71 +++++++++++++++++++ 24 files changed, 290 insertions(+), 20 deletions(-) delete mode 100755 tests/script-based-pre/cargo_list/list.sh rename tests/script-based-pre/{cargo_list => cargo_list_json}/Cargo.toml (100%) rename tests/script-based-pre/{cargo_list => cargo_list_json}/config.yml (100%) rename tests/script-based-pre/{cargo_list => cargo_list_json}/list.expected (100%) create mode 100755 tests/script-based-pre/cargo_list_json/list.sh rename tests/script-based-pre/{cargo_list => cargo_list_json}/src/lib.rs (100%) rename tests/script-based-pre/{cargo_list => cargo_list_json}/src/standard_harnesses.rs (100%) create mode 100644 tests/script-based-pre/cargo_list_md/.gitignore create mode 100644 tests/script-based-pre/cargo_list_md/Cargo.toml rename tests/script-based-pre/{kani_list => cargo_list_md}/config.yml (100%) create mode 100644 tests/script-based-pre/cargo_list_md/list.expected create mode 100755 tests/script-based-pre/cargo_list_md/list.sh create mode 100644 tests/script-based-pre/cargo_list_md/src/lib.rs create mode 100644 tests/script-based-pre/cargo_list_md/src/standard_harnesses.rs delete mode 100755 tests/script-based-pre/kani_list/list.sh create mode 100644 tests/script-based-pre/kani_list_json/config.yml rename tests/script-based-pre/{kani_list => kani_list_json}/list.expected (100%) create mode 100755 tests/script-based-pre/kani_list_json/list.sh rename tests/script-based-pre/{kani_list => kani_list_json}/src/lib.rs (100%) create mode 100644 tests/script-based-pre/kani_list_md/.gitignore create mode 100644 tests/script-based-pre/kani_list_md/config.yml create mode 100644 tests/script-based-pre/kani_list_md/list.expected create mode 100755 tests/script-based-pre/kani_list_md/list.sh create mode 100644 tests/script-based-pre/kani_list_md/src/lib.rs diff --git a/tests/script-based-pre/cargo_list/list.sh b/tests/script-based-pre/cargo_list/list.sh deleted file mode 100755 index 6b1ab80b0f5f..000000000000 --- a/tests/script-based-pre/cargo_list/list.sh +++ /dev/null @@ -1,10 +0,0 @@ -#!/usr/bin/env bash -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -# Check that the JSON file produced by `cargo kani list` is correct. -# Note that the list.expected file omits the value for "kani-version" -# to avoid having to update the test every time we bump versions. - -cargo kani list -Z list -Z function-contracts --format json -cat "kani-list.json" diff --git a/tests/script-based-pre/cargo_list/Cargo.toml b/tests/script-based-pre/cargo_list_json/Cargo.toml similarity index 100% rename from tests/script-based-pre/cargo_list/Cargo.toml rename to tests/script-based-pre/cargo_list_json/Cargo.toml diff --git a/tests/script-based-pre/cargo_list/config.yml b/tests/script-based-pre/cargo_list_json/config.yml similarity index 100% rename from tests/script-based-pre/cargo_list/config.yml rename to tests/script-based-pre/cargo_list_json/config.yml diff --git a/tests/script-based-pre/cargo_list/list.expected b/tests/script-based-pre/cargo_list_json/list.expected similarity index 100% rename from tests/script-based-pre/cargo_list/list.expected rename to tests/script-based-pre/cargo_list_json/list.expected diff --git a/tests/script-based-pre/cargo_list_json/list.sh b/tests/script-based-pre/cargo_list_json/list.sh new file mode 100755 index 000000000000..a9865f5e6b5d --- /dev/null +++ b/tests/script-based-pre/cargo_list_json/list.sh @@ -0,0 +1,22 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +# Check that the json file produced by `kani list` is correct. +# Note that the list.expected file omits the value for "kani-version" +# to avoid having to update the test every time we bump versions. + +output=$(kani list -Z list -Z function-contracts src/lib.rs --format json) + +# Check that Kani prints the absolute path to kani-list.json +absolute_path="$(cd "$(dirname "kani-list.json")" && pwd -P && cd - > /dev/null)/$(basename "kani-list.json")" +expected_last_line="Wrote list results to $absolute_path" +last_line=$(echo "$output" | tail -n 1) + +if [ "$last_line" = "$expected_last_line" ]; then + cat kani-list.json + exit 0 +else + echo "Test failed: Absolute path to kani-list.json is missing from printed output" + exit 1 +fi diff --git a/tests/script-based-pre/cargo_list/src/lib.rs b/tests/script-based-pre/cargo_list_json/src/lib.rs similarity index 100% rename from tests/script-based-pre/cargo_list/src/lib.rs rename to tests/script-based-pre/cargo_list_json/src/lib.rs diff --git a/tests/script-based-pre/cargo_list/src/standard_harnesses.rs b/tests/script-based-pre/cargo_list_json/src/standard_harnesses.rs similarity index 100% rename from tests/script-based-pre/cargo_list/src/standard_harnesses.rs rename to tests/script-based-pre/cargo_list_json/src/standard_harnesses.rs diff --git a/tests/script-based-pre/cargo_list_md/.gitignore b/tests/script-based-pre/cargo_list_md/.gitignore new file mode 100644 index 000000000000..882848e2fba9 --- /dev/null +++ b/tests/script-based-pre/cargo_list_md/.gitignore @@ -0,0 +1 @@ +kani-list.md diff --git a/tests/script-based-pre/cargo_list_md/Cargo.toml b/tests/script-based-pre/cargo_list_md/Cargo.toml new file mode 100644 index 000000000000..2f213d2fccd7 --- /dev/null +++ b/tests/script-based-pre/cargo_list_md/Cargo.toml @@ -0,0 +1,10 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "cargo_list" +version = "0.1.0" +edition = "2021" + +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } diff --git a/tests/script-based-pre/kani_list/config.yml b/tests/script-based-pre/cargo_list_md/config.yml similarity index 100% rename from tests/script-based-pre/kani_list/config.yml rename to tests/script-based-pre/cargo_list_md/config.yml diff --git a/tests/script-based-pre/cargo_list_md/list.expected b/tests/script-based-pre/cargo_list_md/list.expected new file mode 100644 index 000000000000..9e913345e664 --- /dev/null +++ b/tests/script-based-pre/cargo_list_md/list.expected @@ -0,0 +1,14 @@ + +Contracts: +| | Function | Contract Harnesses (#[kani::proof_for_contract]) | +| ----- | ----------------------------- | -------------------------------------------------------------- | +| | example::implementation::bar | example::verify::check_bar | +| | example::implementation::foo | example::verify::check_foo_u32, example::verify::check_foo_u64 | +| | example::implementation::func | example::verify::check_func | +| | example::prep::parse | NONE | +| Total | 4 | 4 | + + +Standard Harnesses (#[kani::proof]): +1. standard_harnesses::example::verify::check_modify +2. standard_harnesses::example::verify::check_new \ No newline at end of file diff --git a/tests/script-based-pre/cargo_list_md/list.sh b/tests/script-based-pre/cargo_list_md/list.sh new file mode 100755 index 000000000000..e35c4835c42e --- /dev/null +++ b/tests/script-based-pre/cargo_list_md/list.sh @@ -0,0 +1,22 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +# Check that the MD file produced by `kani list` is correct. +# Note that the list.expected file omits the value for "kani-version" +# to avoid having to update the test every time we bump versions. + +output=$(kani list -Z list -Z function-contracts src/lib.rs --format markdown) + +# Check that Kani prints the absolute path to kani-list.md +absolute_path="$(cd "$(dirname "kani-list.md")" && pwd -P && cd - > /dev/null)/$(basename "kani-list.md")" +expected_last_line="Wrote list results to $absolute_path" +last_line=$(echo "$output" | tail -n 1) + +if [ "$last_line" = "$expected_last_line" ]; then + cat kani-list.md + exit 0 +else + echo "Test failed: Absolute path to kani-list.md is missing from printed output" + exit 1 +fi diff --git a/tests/script-based-pre/cargo_list_md/src/lib.rs b/tests/script-based-pre/cargo_list_md/src/lib.rs new file mode 100644 index 000000000000..e7382a9124a3 --- /dev/null +++ b/tests/script-based-pre/cargo_list_md/src/lib.rs @@ -0,0 +1,68 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +//! This test replicates the module structure from the running example in the list RFC. +//! It ensures that the list command works across modules, and with modifies clauses, history expressions, and generic functions. + +mod standard_harnesses; + +#[cfg(kani)] +mod example { + mod prep { + #[kani::requires(s.len() < 10)] + fn parse(s: &str) -> u32 { + s.parse().unwrap() + } + } + + pub mod implementation { + #[kani::requires(*x < 4)] + #[kani::requires(*x > 2)] + #[kani::ensures(|_| old(*x - 1) == *x)] + #[kani::ensures(|_| *x == 4)] + #[kani::modifies(x)] + pub fn bar(x: &mut u32) { + *x += 1; + } + + #[kani::requires(*x < 100)] + #[kani::modifies(x)] + pub fn func(x: &mut i32) { + *x *= 1; + } + + #[kani::requires(true)] + #[kani::ensures(|_| old(*x) == *x)] + pub fn foo(x: &mut T) -> T { + *x + } + } + + mod verify { + use crate::example::implementation; + + #[kani::proof_for_contract(implementation::bar)] + fn check_bar() { + let mut x = 7; + implementation::bar(&mut x); + } + + #[kani::proof_for_contract(implementation::foo)] + fn check_foo_u32() { + let mut x: u32 = 7; + implementation::foo(&mut x); + } + + #[kani::proof_for_contract(implementation::foo)] + fn check_foo_u64() { + let mut x: u64 = 7; + implementation::foo(&mut x); + } + + #[kani::proof_for_contract(implementation::func)] + fn check_func() { + let mut x = 7; + implementation::func(&mut x); + } + } +} diff --git a/tests/script-based-pre/cargo_list_md/src/standard_harnesses.rs b/tests/script-based-pre/cargo_list_md/src/standard_harnesses.rs new file mode 100644 index 000000000000..5df490461d0c --- /dev/null +++ b/tests/script-based-pre/cargo_list_md/src/standard_harnesses.rs @@ -0,0 +1,15 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +//! Test that the cargo list command can find Kani attributes across multiple files. + +#[cfg(kani)] +mod example { + mod verify { + #[kani::proof] + fn check_modify() {} + + #[kani::proof] + fn check_new() {} + } +} diff --git a/tests/script-based-pre/kani_list/list.sh b/tests/script-based-pre/kani_list/list.sh deleted file mode 100755 index e7bb6f081044..000000000000 --- a/tests/script-based-pre/kani_list/list.sh +++ /dev/null @@ -1,10 +0,0 @@ -#!/usr/bin/env bash -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -# Check that the JSON file produced by `kani list` is correct. -# Note that the list.expected file omits the value for "kani-version" -# to avoid having to update the test every time we bump versions. - -kani list -Z list -Z function-contracts src/lib.rs --format json -cat "kani-list.json" diff --git a/tests/script-based-pre/kani_list_json/config.yml b/tests/script-based-pre/kani_list_json/config.yml new file mode 100644 index 000000000000..4eac6f79588c --- /dev/null +++ b/tests/script-based-pre/kani_list_json/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: list.sh +expected: list.expected diff --git a/tests/script-based-pre/kani_list/list.expected b/tests/script-based-pre/kani_list_json/list.expected similarity index 100% rename from tests/script-based-pre/kani_list/list.expected rename to tests/script-based-pre/kani_list_json/list.expected diff --git a/tests/script-based-pre/kani_list_json/list.sh b/tests/script-based-pre/kani_list_json/list.sh new file mode 100755 index 000000000000..a70938ffcea9 --- /dev/null +++ b/tests/script-based-pre/kani_list_json/list.sh @@ -0,0 +1,22 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +# Check that the JSON file produced by `kani list` is correct. +# Note that the list.expected file omits the value for "kani-version" +# to avoid having to update the test every time we bump versions. + +output=$(kani list -Z list -Z function-contracts src/lib.rs --format json) + +# Check that Kani prints the absolute path to kani-list.json +absolute_path="$(cd "$(dirname "kani-list.json")" && pwd -P && cd - > /dev/null)/$(basename "kani-list.json")" +expected_last_line="Wrote list results to $absolute_path" +last_line=$(echo "$output" | tail -n 1) + +if [ "$last_line" = "$expected_last_line" ]; then + cat kani-list.json + exit 0 +else + echo "Test failed: Absolute path to kani-list.json is missing from printed output" + exit 1 +fi diff --git a/tests/script-based-pre/kani_list/src/lib.rs b/tests/script-based-pre/kani_list_json/src/lib.rs similarity index 100% rename from tests/script-based-pre/kani_list/src/lib.rs rename to tests/script-based-pre/kani_list_json/src/lib.rs diff --git a/tests/script-based-pre/kani_list_md/.gitignore b/tests/script-based-pre/kani_list_md/.gitignore new file mode 100644 index 000000000000..882848e2fba9 --- /dev/null +++ b/tests/script-based-pre/kani_list_md/.gitignore @@ -0,0 +1 @@ +kani-list.md diff --git a/tests/script-based-pre/kani_list_md/config.yml b/tests/script-based-pre/kani_list_md/config.yml new file mode 100644 index 000000000000..4eac6f79588c --- /dev/null +++ b/tests/script-based-pre/kani_list_md/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: list.sh +expected: list.expected diff --git a/tests/script-based-pre/kani_list_md/list.expected b/tests/script-based-pre/kani_list_md/list.expected new file mode 100644 index 000000000000..eb4ca335d678 --- /dev/null +++ b/tests/script-based-pre/kani_list_md/list.expected @@ -0,0 +1,14 @@ + +Contracts: +| | Function | Contract Harnesses (#[kani::proof_for_contract]) | +| ----- | ----------------------------- | -------------------------------------------------------------- | +| | example::implementation::bar | example::verify::check_bar | +| | example::implementation::foo | example::verify::check_foo_u32, example::verify::check_foo_u64 | +| | example::implementation::func | example::verify::check_func | +| | example::prep::parse | NONE | +| Total | 4 | 4 | + + +Standard Harnesses (#[kani::proof]): +1. example::verify::check_modify +2. example::verify::check_new \ No newline at end of file diff --git a/tests/script-based-pre/kani_list_md/list.sh b/tests/script-based-pre/kani_list_md/list.sh new file mode 100755 index 000000000000..e35c4835c42e --- /dev/null +++ b/tests/script-based-pre/kani_list_md/list.sh @@ -0,0 +1,22 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +# Check that the MD file produced by `kani list` is correct. +# Note that the list.expected file omits the value for "kani-version" +# to avoid having to update the test every time we bump versions. + +output=$(kani list -Z list -Z function-contracts src/lib.rs --format markdown) + +# Check that Kani prints the absolute path to kani-list.md +absolute_path="$(cd "$(dirname "kani-list.md")" && pwd -P && cd - > /dev/null)/$(basename "kani-list.md")" +expected_last_line="Wrote list results to $absolute_path" +last_line=$(echo "$output" | tail -n 1) + +if [ "$last_line" = "$expected_last_line" ]; then + cat kani-list.md + exit 0 +else + echo "Test failed: Absolute path to kani-list.md is missing from printed output" + exit 1 +fi diff --git a/tests/script-based-pre/kani_list_md/src/lib.rs b/tests/script-based-pre/kani_list_md/src/lib.rs new file mode 100644 index 000000000000..69dbba5a9e0f --- /dev/null +++ b/tests/script-based-pre/kani_list_md/src/lib.rs @@ -0,0 +1,71 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +//! This test replicates the module structure from the running example in the list RFC. +//! It ensures that the list command across modules, and with modifies clauses, history expressions, and generic functions. + +mod example { + mod prep { + #[kani::requires(s.len() < 10)] + fn parse(s: &str) -> u32 { + s.parse().unwrap() + } + } + + pub mod implementation { + #[kani::requires(*x < 4)] + #[kani::requires(*x > 2)] + #[kani::ensures(|_| old(*x - 1) == *x)] + #[kani::ensures(|_| *x == 4)] + #[kani::modifies(x)] + pub fn bar(x: &mut u32) { + *x += 1; + } + + #[kani::requires(true)] + #[kani::ensures(|_| old(*x) == *x)] + pub fn foo(x: &mut T) -> T { + *x + } + + #[kani::requires(*x < 100)] + #[kani::modifies(x)] + pub fn func(x: &mut i32) { + *x *= 1; + } + } + + mod verify { + use crate::example::implementation; + + #[kani::proof_for_contract(implementation::bar)] + fn check_bar() { + let mut x = 7; + implementation::bar(&mut x); + } + + #[kani::proof_for_contract(implementation::foo)] + fn check_foo_u32() { + let mut x: u32 = 7; + implementation::foo(&mut x); + } + + #[kani::proof_for_contract(implementation::foo)] + fn check_foo_u64() { + let mut x: u64 = 7; + implementation::foo(&mut x); + } + + #[kani::proof_for_contract(implementation::func)] + fn check_func() { + let mut x = 7; + implementation::func(&mut x); + } + + #[kani::proof] + fn check_modify() {} + + #[kani::proof] + fn check_new() {} + } +}