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() {} + } +}