From 738351e3dd435bb498137aa4125ec27ecaceefa9 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 19 Nov 2024 22:56:07 -0500 Subject: [PATCH] List Subcommand Improvements (#3729) Improvements to the list subcommand. - Print the location of the JSON file for `--format=json` (#3633) - Use `CommonArgs` instead of `VerificationArgs` (#3632) - Add a Markdown option. The pretty table is nice for smaller packages, but as we progress with the standard library verification effort, it's too massive to be easily readable. In this case, it's better to print a markdown table and then just read it in a markdown editor. (Once this PR is merged, the [kani list workflow step](https://github.com/model-checking/verify-rust-std/pull/146) will use the markdown option). Resolves #3632, #3633 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- Cargo.lock | 10 + kani-driver/Cargo.toml | 1 + kani-driver/src/args/list_args.rs | 24 +- kani-driver/src/args/mod.rs | 4 +- kani-driver/src/list/collect_metadata.rs | 58 +++-- kani-driver/src/list/mod.rs | 20 +- kani-driver/src/list/output.rs | 242 ++++++++---------- kani-driver/src/main.rs | 8 +- 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 +++++ 32 files changed, 478 insertions(+), 199 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/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 7129bd0a85c4..ebd97d01f2fb 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")] @@ -44,20 +42,22 @@ 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 diagnostic messages in a user friendly format. + /// Print output in human-readable format. Pretty, - /// Print diagnostic messages in JSON format. + /// Write output to a Markdown file. + Markdown, + /// Write output to a JSON file. Json, } 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 +70,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/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 99da0477314d..a7901e997ab1 100644 --- a/kani-driver/src/list/collect_metadata.rs +++ b/kani-driver/src/list/collect_metadata.rs @@ -6,9 +6,12 @@ use std::collections::{BTreeMap, BTreeSet}; use crate::{ InvocationType, - args::list_args::{CargoListArgs, Format, StandaloneListArgs}, - list::Totals, - list::output::{json, pretty}, + args::{ + VerificationArgs, + list_args::{CargoListArgs, StandaloneListArgs}, + }, + list::ListMetadata, + list::output::output_list_results, project::{Project, cargo_project, standalone_project, std_project}, session::KaniSession, version::print_kani_version, @@ -17,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. @@ -26,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); @@ -45,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); @@ -63,31 +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(), - }; - - match format { - Format::Pretty => pretty(standard_harnesses, contracted_functions, totals), - Format::Json => json(standard_harnesses, contract_harnesses, contracted_functions, totals), + ListMetadata { + standard_harnesses, + standard_harnesses_count, + contract_harnesses, + contract_harnesses_count, + contracted_functions, } } -pub fn list_cargo(args: CargoListArgs) -> Result<()> { - let session = KaniSession::new(args.verify_opts)?; - if !session.args.common_args.quiet { +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 !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) -> Result<()> { - let session = KaniSession::new(args.verify_opts)?; - if !session.args.common_args.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 !quiet { print_kani_version(InvocationType::Standalone); } @@ -97,5 +103,7 @@ pub fn list_standalone(args: StandaloneListArgs) -> Result<()> { 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 79a5fcf6fe5e..47b32bd6ed5e 100644 --- a/kani-driver/src/list/output.rs +++ b/kani-driver/src/list/output.rs @@ -3,178 +3,158 @@ //! This module handles outputting the result for the list subcommand use std::{ - cmp::max, - collections::{BTreeMap, BTreeSet}, + fmt::Display, fs::File, - io::BufWriter, + io::{BufWriter, Write}, + path::Path, }; -use crate::{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 kani_metadata::ContractedFunction; +use comfy_table::Table as PrettyTable; 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"; - -/// Construct the table of contracts information. -fn construct_contracts_table( - contracted_functions: BTreeSet, - totals: Totals, -) -> Vec { - 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()) +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), } +} - // 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(); +/// 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); - 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()); + Ok(()) +} - let mut data_rows: Vec<(String, Vec)> = vec![]; +/// 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)?) + }; - 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)); + let output = format_results(table, &list_metadata); - data_rows.push((cf.function, cf.harnesses)); + 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(()) +} - 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} |" - ); - 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} |" - ); - table_rows.push(row); +/// 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(), } + }); - table_rows.push(sep_row.clone()) + serde_json::to_writer_pretty(writer, &json_obj)?; + + if !quiet { + println!("Wrote list results to {}", std::fs::canonicalize(out_path)?.display()); } - 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()); + Ok(()) +} + +/// Construct the rows for the table of contracts information. +/// Returns a tuple of the table header and the rows. +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])"; + const TOTALS_HEADER: &str = "Total"; + + let header = + vec![String::new(), FUNCTION_HEADER.to_string(), CONTRACT_HARNESSES_HEADER.to_string()]; + + let mut rows: Vec> = vec![]; - let totals_row = format!( - "| {TOTALS_HEADER} | {functions_total}{total_function_space} | {harnesses_total}{total_harnesses_space} |" - ); + 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 { + row.push(cf.harnesses.join(", ")); + } + rows.push(row); + } - table_rows.push(totals_row); - table_rows.push(sep_row.clone()); + let totals_row = vec![ + TOTALS_HEADER.to_string(), + list_metadata.contracted_functions.len().to_string(), + list_metadata.contract_harnesses_count.to_string(), + ]; + rows.push(totals_row); - table_rows + (header, rows) } -/// Output results as a table printed to the terminal. -pub fn pretty( - standard_harnesses: BTreeMap>, - contracted_functions: BTreeSet, - totals: Totals, -) -> Result<()> { +/// 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 contracted_functions.is_empty() { - println!("{NO_CONTRACTS_MSG}"); + if let Some(table) = table { + output.push(format!("{table}")); } else { - let table_rows = construct_contracts_table(contracted_functions, totals); - println!("{}", table_rows.join("\n")); - }; + 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!(); - - Ok(()) -} - -/// Output results as a JSON file. -pub 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)?; - - Ok(()) + output.join("\n") } 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 { 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() {} + } +}