From 04000248aaa2d44d2c990c059542c9245c78eab0 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Wed, 9 Oct 2024 12:27:13 -0400 Subject: [PATCH] List Subcommand (Implementation) (#3523) Implementation of the list subcommand (and updates to the RFC). As a larger test, I ran on the standard library (`kani list -Z list -Z function-contracts -Z mem-predicates ./library --std`) and manually verified that the results were correct. I pasted the output below. Contracts: | | Function | Contract Harnesses (#[kani::proof_for_contract]) | | ----- | ------------------------------------------------ | ------------------------------------------------------ | | | alloc::layout::Layout::from_size_align_unchecked | alloc::layout::verify::check_from_size_align_unchecked | | | ascii::ascii_char::AsciiChar::from_u8 | ascii::ascii_char::verify::check_from_u8 | | | ascii::ascii_char::AsciiChar::from_u8_unchecked | ascii::ascii_char::verify::check_from_u8_unchecked | | | char::convert::from_u32_unchecked | char::convert::verify::check_from_u32_unchecked | | | char::methods::verify::as_ascii_clone | char::methods::verify::check_as_ascii_ascii_char | | | | char::methods::verify::check_as_ascii_non_ascii_char | | | intrinsics::typed_swap | intrinsics::verify::check_typed_swap_u8 | | | | intrinsics::verify::check_typed_swap_char | | | | intrinsics::verify::check_typed_swap_non_zero | | | mem::swap | mem::verify::check_swap_primitive | | | | mem::verify::check_swap_adt_no_drop | | | ptr::align_offset | ptr::verify::check_align_offset_zst | | | | ptr::verify::check_align_offset_u8 | | | | ptr::verify::check_align_offset_u16 | | | | ptr::verify::check_align_offset_u32 | | | | ptr::verify::check_align_offset_u64 | | | | ptr::verify::check_align_offset_u128 | | | | ptr::verify::check_align_offset_4096 | | | | ptr::verify::check_align_offset_5 | | | ptr::alignment::Alignment::as_nonzero | ptr::alignment::verify::check_as_nonzero | | | ptr::alignment::Alignment::as_usize | ptr::alignment::verify::check_as_usize | | | ptr::alignment::Alignment::log2 | ptr::alignment::verify::check_log2 | | | ptr::alignment::Alignment::mask | ptr::alignment::verify::check_mask | | | ptr::alignment::Alignment::new | ptr::alignment::verify::check_new | | | ptr::alignment::Alignment::new_unchecked | ptr::alignment::verify::check_new_unchecked | | | ptr::alignment::Alignment::of | ptr::alignment::verify::check_of_i32 | | | ptr::non_null::NonNull::::new | ptr::non_null::verify::non_null_check_new | | | ptr::non_null::NonNull::::new_unchecked | ptr::non_null::verify::non_null_check_new_unchecked | | | ptr::read_volatile | ptr::verify::check_read_u128 | | | ptr::unique::Unique::::as_non_null_ptr | ptr::unique::verify::check_as_non_null_ptr | | | ptr::unique::Unique::::as_ptr | ptr::unique::verify::check_as_ptr | | | ptr::unique::Unique::::new | ptr::unique::verify::check_new | | | ptr::unique::Unique::::new_unchecked | ptr::unique::verify::check_new_unchecked | | | ptr::verify::mod_inv_copy | ptr::verify::check_mod_inv | | | ptr::write_volatile | NONE | | Total | 24 | 34 | Standard Harnesses (#[kani::proof]): 1. ptr::unique::verify::check_as_mut 2. ptr::unique::verify::check_as_ref 3. ptr::unique::verify::check_cast Terminal view (`--pretty` format): list By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Felipe R. Monteiro Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- Cargo.lock | 11 ++ .../compiler_interface.rs | 7 +- .../src/kani_middle/codegen_units.rs | 7 +- kani-compiler/src/kani_middle/metadata.rs | 51 ++++- kani-driver/Cargo.toml | 3 +- kani-driver/src/args/list_args.rs | 127 ++++++++++++ kani-driver/src/args/mod.rs | 8 + kani-driver/src/list/collect_metadata.rs | 101 ++++++++++ kani-driver/src/list/mod.rs | 14 ++ kani-driver/src/list/output.rs | 180 ++++++++++++++++++ kani-driver/src/main.rs | 8 + kani-driver/src/metadata.rs | 2 + kani-driver/src/version.rs | 2 +- kani_metadata/src/lib.rs | 15 +- kani_metadata/src/unstable.rs | 2 + rfc/src/rfcs/0013-list.md | 112 ++++++----- tests/script-based-pre/cargo_list/Cargo.toml | 10 + tests/script-based-pre/cargo_list/config.yml | 4 + .../script-based-pre/cargo_list/list.expected | 52 +++++ tests/script-based-pre/cargo_list/list.sh | 10 + tests/script-based-pre/cargo_list/src/lib.rs | 68 +++++++ .../cargo_list/src/standard_harnesses.rs | 15 ++ tests/script-based-pre/kani_list/config.yml | 4 + .../script-based-pre/kani_list/list.expected | 52 +++++ tests/script-based-pre/kani_list/list.sh | 10 + tests/script-based-pre/kani_list/src/lib.rs | 71 +++++++ 26 files changed, 883 insertions(+), 63 deletions(-) create mode 100644 kani-driver/src/args/list_args.rs create mode 100644 kani-driver/src/list/collect_metadata.rs create mode 100644 kani-driver/src/list/mod.rs create mode 100644 kani-driver/src/list/output.rs create mode 100644 tests/script-based-pre/cargo_list/Cargo.toml create mode 100644 tests/script-based-pre/cargo_list/config.yml create mode 100644 tests/script-based-pre/cargo_list/list.expected create mode 100755 tests/script-based-pre/cargo_list/list.sh create mode 100644 tests/script-based-pre/cargo_list/src/lib.rs create mode 100644 tests/script-based-pre/cargo_list/src/standard_harnesses.rs create mode 100644 tests/script-based-pre/kani_list/config.yml create mode 100644 tests/script-based-pre/kani_list/list.expected create mode 100755 tests/script-based-pre/kani_list/list.sh create mode 100644 tests/script-based-pre/kani_list/src/lib.rs diff --git a/Cargo.lock b/Cargo.lock index 21997d7bc332..580cdf70946a 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -306,6 +306,15 @@ dependencies = [ "windows-sys 0.48.0", ] +[[package]] +name = "colour" +version = "2.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b536eebcabe54980476d120a182f7da2268fe02d22575cca99cee5fdda178280" +dependencies = [ + "winapi", +] + [[package]] name = "comfy-table" version = "7.1.1" @@ -767,6 +776,7 @@ dependencies = [ "anyhow", "cargo_metadata", "clap", + "colour", "comfy-table", "console", "glob", @@ -1419,6 +1429,7 @@ version = "1.0.128" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "6ff5456707a1de34e7e37f2a6fd3d3f808c318259cbd01ab6377795054b483d8" dependencies = [ + "indexmap", "itoa", "memchr", "ryu", diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index da211c58946c..25bc0cbe8ad1 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -20,9 +20,8 @@ use cbmc::RoundingMode; use cbmc::goto_program::Location; use cbmc::irep::goto_binary_serde::write_goto_binary_file; use cbmc::{InternedString, MachineModel}; -use kani_metadata::UnsupportedFeature; use kani_metadata::artifact::convert_type; -use kani_metadata::{ArtifactType, HarnessMetadata, KaniMetadata}; +use kani_metadata::{ArtifactType, HarnessMetadata, KaniMetadata, UnsupportedFeature}; use kani_metadata::{AssignsContract, CompilerArtifactStub}; use rustc_codegen_ssa::back::archive::{ ArArchiveBuilder, ArchiveBuilder, ArchiveBuilderBuilder, DEFAULT_OBJECT_READER, @@ -643,6 +642,10 @@ impl GotoCodegenResults { proof_harnesses: proofs, unsupported_features, test_harnesses: tests, + // We don't collect the contracts metadata because the FunctionWithContractPass + // removes any contracts logic for ReachabilityType::Test or ReachabilityType::PubFns, + // which are the two ReachabilityTypes under which the compiler calls this function. + contracted_functions: vec![], } } diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 071e880ffd9f..ebb12f7656b6 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -9,7 +9,7 @@ use crate::args::ReachabilityType; use crate::kani_middle::attributes::is_proof_harness; -use crate::kani_middle::metadata::gen_proof_metadata; +use crate::kani_middle::metadata::{gen_contracts_metadata, gen_proof_metadata}; use crate::kani_middle::reachability::filter_crate_items; use crate::kani_middle::resolve::expect_resolve_fn; use crate::kani_middle::stubbing::{check_compatibility, harness_stub_map}; @@ -93,7 +93,7 @@ impl CodegenUnits { /// Write compilation metadata into a file. pub fn write_metadata(&self, queries: &QueryDb, tcx: TyCtxt) { - let metadata = self.generate_metadata(); + let metadata = self.generate_metadata(tcx); let outpath = metadata_output_path(tcx); store_metadata(queries, &metadata, &outpath); } @@ -103,7 +103,7 @@ impl CodegenUnits { } /// Generate [KaniMetadata] for the target crate. - fn generate_metadata(&self) -> KaniMetadata { + fn generate_metadata(&self, tcx: TyCtxt) -> KaniMetadata { let (proof_harnesses, test_harnesses) = self.harness_info.values().cloned().partition(|md| md.attributes.is_proof_harness()); KaniMetadata { @@ -111,6 +111,7 @@ impl CodegenUnits { proof_harnesses, unsupported_features: vec![], test_harnesses, + contracted_functions: gen_contracts_metadata(tcx), } } } diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs index db6b6b06149a..c92b20cf49d6 100644 --- a/kani-compiler/src/kani_middle/metadata.rs +++ b/kani-compiler/src/kani_middle/metadata.rs @@ -3,15 +3,16 @@ //! This module handles Kani metadata generation. For example, generating HarnessMetadata for a //! given function. +use std::collections::HashMap; use std::path::Path; -use crate::kani_middle::attributes::test_harness_name; +use crate::kani_middle::attributes::{KaniAttributes, test_harness_name}; +use crate::kani_middle::{SourceLocation, stable_fn_def}; +use kani_metadata::ContractedFunction; use kani_metadata::{ArtifactType, HarnessAttributes, HarnessKind, HarnessMetadata}; use rustc_middle::ty::TyCtxt; -use stable_mir::CrateDef; use stable_mir::mir::mono::Instance; - -use super::{SourceLocation, attributes::KaniAttributes}; +use stable_mir::{CrateDef, CrateItems, DefId}; /// Create the harness metadata for a proof harness for a given function. pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) -> HarnessMetadata { @@ -40,6 +41,48 @@ pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) -> } } +/// Collects contract and contract harness metadata. +/// +/// For each function with contracts (or that is a target of a contract harness), +/// construct a `ContractedFunction` object for it. +pub fn gen_contracts_metadata(tcx: TyCtxt) -> Vec { + // We work with `stable_mir::CrateItem` instead of `stable_mir::Instance` to include generic items + let crate_items: CrateItems = stable_mir::all_local_items(); + + let mut fn_to_data: HashMap = HashMap::new(); + + for item in crate_items { + let function = item.name(); + let file = SourceLocation::new(item.span()).filename; + let attributes = KaniAttributes::for_def_id(tcx, item.def_id()); + + if attributes.has_contract() { + fn_to_data.insert(item.def_id(), ContractedFunction { + function, + file, + harnesses: vec![], + }); + } else if let Some((target_name, internal_def_id, _)) = + attributes.interpret_for_contract_attribute() + { + let target_def_id = stable_fn_def(tcx, internal_def_id) + .expect("The target of a proof for contract should be a function definition") + .def_id(); + if let Some(cf) = fn_to_data.get_mut(&target_def_id) { + cf.harnesses.push(function); + } else { + fn_to_data.insert(target_def_id, ContractedFunction { + function: target_name.to_string(), + file, + harnesses: vec![function], + }); + } + } + } + + fn_to_data.into_values().collect() +} + /// Create the harness metadata for a test description. #[allow(dead_code)] pub fn gen_test_metadata( diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index 555534959474..67214738fa7c 100644 --- a/kani-driver/Cargo.toml +++ b/kani-driver/Cargo.toml @@ -18,8 +18,9 @@ anyhow = "1" console = "0.15.1" once_cell = "1.19.0" serde = { version = "1", features = ["derive"] } -serde_json = "1" +serde_json = { version = "1", features = ["preserve_order"] } clap = { version = "4.4.11", features = ["derive"] } +colour = "2.1.0" glob = "0.3" toml = "0.8" regex = "1.6" diff --git a/kani-driver/src/args/list_args.rs b/kani-driver/src/args/list_args.rs new file mode 100644 index 000000000000..7129bd0a85c4 --- /dev/null +++ b/kani-driver/src/args/list_args.rs @@ -0,0 +1,127 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Implements the subcommand handling of the list subcommand + +use std::path::PathBuf; + +use crate::args::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, + + /// Output format + #[clap(long, default_value = "pretty")] + pub format: Format, +} + +/// List information relevant to verification +#[derive(Debug, Parser)] +pub struct StandaloneListArgs { + /// Rust file to verify + #[arg(required = true)] + pub input: PathBuf, + + #[arg(long, hide = true)] + pub crate_name: Option, + + #[command(flatten)] + pub verify_opts: VerificationArgs, + + /// Output format + #[clap(long, default_value = "pretty")] + pub format: Format, + + /// Pass this flag to run the `list` command on the standard library. + /// Ensure that the provided `path` is the `library` folder. + #[arg(long)] + pub std: bool, +} + +/// Message 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. + Pretty, + /// Print diagnostic messages in JSON format. + 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) { + return Err(Error::raw( + ErrorKind::MissingRequiredArgument, + "The `list` subcommand is unstable and requires -Z list", + )); + } + + Ok(()) + } +} + +impl ValidateArgs for StandaloneListArgs { + fn validate(&self) -> Result<(), Error> { + self.verify_opts.validate()?; + if !self.verify_opts.common_args.unstable_features.contains(UnstableFeature::List) { + return Err(Error::raw( + ErrorKind::MissingRequiredArgument, + "The `list` subcommand is unstable and requires -Z list", + )); + } + + if self.std { + if !self.input.exists() { + Err(Error::raw( + ErrorKind::InvalidValue, + format!( + "Invalid argument: `` argument `{}` does not exist", + self.input.display() + ), + )) + } else if !self.input.is_dir() { + Err(Error::raw( + ErrorKind::InvalidValue, + format!( + "Invalid argument: `` argument `{}` is not a directory", + self.input.display() + ), + )) + } else { + let full_path = self.input.canonicalize()?; + let dir = full_path.file_stem().unwrap(); + if dir != "library" { + Err(Error::raw( + ErrorKind::InvalidValue, + format!( + "Invalid argument: Expected `` to point to the `library` folder \ + containing the standard library crates.\n\ + Found `{}` folder instead", + dir.to_string_lossy() + ), + )) + } else { + Ok(()) + } + } + } else if self.input.is_file() { + Ok(()) + } else { + Err(Error::raw( + ErrorKind::InvalidValue, + format!( + "Invalid argument: Input invalid. `{}` is not a regular file.", + self.input.display() + ), + )) + } + } +} diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 30c6bd7073a6..8aa758219524 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -5,6 +5,7 @@ pub mod assess_args; pub mod cargo; pub mod common; +pub mod list_args; pub mod playback_args; pub mod std_args; @@ -94,6 +95,8 @@ pub enum StandaloneSubcommand { Playback(Box), /// Verify the rust standard library. VerifyStd(Box), + /// Execute the list subcommand + List(Box), } #[derive(Debug, clap::Parser)] @@ -119,6 +122,9 @@ pub enum CargoKaniSubcommand { /// Execute concrete playback testcases of a local package. Playback(Box), + + /// List metadata relevant to verification, e.g., harnesses. + List(Box), } // Common arguments for invoking Kani for verification purpose. This gets put into KaniContext, @@ -421,6 +427,7 @@ impl ValidateArgs for StandaloneArgs { match &self.command { Some(StandaloneSubcommand::VerifyStd(args)) => args.validate()?, + Some(StandaloneSubcommand::List(args)) => args.validate()?, // TODO: Invoke PlaybackArgs::validate() None | Some(StandaloneSubcommand::Playback(..)) => {} }; @@ -467,6 +474,7 @@ impl ValidateArgs for CargoKaniSubcommand { // Assess doesn't implement validation yet. CargoKaniSubcommand::Assess(_) => Ok(()), CargoKaniSubcommand::Playback(playback) => playback.validate(), + CargoKaniSubcommand::List(list) => list.validate(), } } } diff --git a/kani-driver/src/list/collect_metadata.rs b/kani-driver/src/list/collect_metadata.rs new file mode 100644 index 000000000000..99da0477314d --- /dev/null +++ b/kani-driver/src/list/collect_metadata.rs @@ -0,0 +1,101 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// This module invokes the compiler to gather the metadata for the list subcommand, then post-processes the output. + +use std::collections::{BTreeMap, BTreeSet}; + +use crate::{ + InvocationType, + args::list_args::{CargoListArgs, Format, StandaloneListArgs}, + list::Totals, + list::output::{json, pretty}, + project::{Project, cargo_project, standalone_project, std_project}, + session::KaniSession, + version::print_kani_version, +}; +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<()> { + // 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. + let mut standard_harnesses: BTreeMap> = BTreeMap::new(); + let mut contract_harnesses: BTreeMap> = BTreeMap::new(); + + let mut contracted_functions: BTreeSet = BTreeSet::new(); + + let mut total_standard_harnesses = 0; + let mut total_contract_harnesses = 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; + if let Some(harnesses) = standard_harnesses.get_mut(&harness_meta.original_file) + { + harnesses.insert(harness_meta.pretty_name); + } else { + standard_harnesses.insert( + harness_meta.original_file, + BTreeSet::from([harness_meta.pretty_name]), + ); + } + } + HarnessKind::ProofForContract { .. } => { + total_contract_harnesses += 1; + if let Some(harnesses) = contract_harnesses.get_mut(&harness_meta.original_file) + { + harnesses.insert(harness_meta.pretty_name); + } else { + contract_harnesses.insert( + harness_meta.original_file, + BTreeSet::from([harness_meta.pretty_name]), + ); + } + } + HarnessKind::Test => {} + } + } + + 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), + } +} + +pub fn list_cargo(args: CargoListArgs) -> Result<()> { + let session = KaniSession::new(args.verify_opts)?; + if !session.args.common_args.quiet { + print_kani_version(InvocationType::CargoKani(vec![])); + } + + let project = cargo_project(&session, false)?; + process_metadata(project.metadata, args.format) +} + +pub fn list_standalone(args: StandaloneListArgs) -> Result<()> { + let session = KaniSession::new(args.verify_opts)?; + if !session.args.common_args.quiet { + print_kani_version(InvocationType::Standalone); + } + + let project: Project = if args.std { + std_project(&args.input, &session)? + } else { + standalone_project(&args.input, args.crate_name, &session)? + }; + + process_metadata(project.metadata, args.format) +} diff --git a/kani-driver/src/list/mod.rs b/kani-driver/src/list/mod.rs new file mode 100644 index 000000000000..0987a0e9c927 --- /dev/null +++ b/kani-driver/src/list/mod.rs @@ -0,0 +1,14 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// Implements the list subcommand logic + +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, +} diff --git a/kani-driver/src/list/output.rs b/kani-driver/src/list/output.rs new file mode 100644 index 000000000000..79a5fcf6fe5e --- /dev/null +++ b/kani-driver/src/list/output.rs @@ -0,0 +1,180 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! This module handles outputting the result for the list subcommand + +use std::{ + cmp::max, + collections::{BTreeMap, BTreeSet}, + fs::File, + io::BufWriter, +}; + +use crate::{list::Totals, version::KANI_VERSION}; +use anyhow::Result; +use colour::print_ln_bold; +use kani_metadata::ContractedFunction; +use serde_json::json; + +// 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()) + } + + // 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![]; + + 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} |" + ); + 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); + } + + 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} |" + ); + + table_rows.push(totals_row); + table_rows.push(sep_row.clone()); + + table_rows +} + +/// Output results as a table printed to the terminal. +pub fn pretty( + standard_harnesses: BTreeMap>, + 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."; + const NO_HARNESSES_MSG: &str = "No standard harnesses found."; + + print_ln_bold!("\n{CONTRACTS_SECTION}"); + + if contracted_functions.is_empty() { + println!("{NO_CONTRACTS_MSG}"); + } else { + let table_rows = construct_contracts_table(contracted_functions, totals); + println!("{}", table_rows.join("\n")); + }; + + print_ln_bold!("\n{HARNESSES_SECTION}"); + if standard_harnesses.is_empty() { + println!("{NO_HARNESSES_MSG}"); + } + + let mut std_harness_index = 0; + + for (_, harnesses) in standard_harnesses { + for harness in harnesses { + println!("{}. {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(()) +} diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index e8ede555f180..88f92b3a70f6 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -12,6 +12,7 @@ use args_toml::join_args; use crate::args::StandaloneSubcommand; use crate::concrete_playback::playback::{playback_cargo, playback_standalone}; +use crate::list::collect_metadata::{list_cargo, list_standalone}; use crate::project::Project; use crate::session::KaniSession; use crate::version::print_kani_version; @@ -33,6 +34,7 @@ mod cbmc_property_renderer; mod concrete_playback; mod coverage; mod harness_runner; +mod list; mod metadata; mod project; mod session; @@ -67,6 +69,10 @@ 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); + } + let session = session::KaniSession::new(args.verify_opts)?; if !session.args.common_args.quiet { @@ -80,6 +86,7 @@ fn cargokani_main(input_args: Vec) -> Result<()> { Some(CargoKaniSubcommand::Playback(args)) => { return playback_cargo(*args); } + Some(CargoKaniSubcommand::List(_)) => unreachable!(), None => {} } @@ -98,6 +105,7 @@ 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::VerifyStd(args)) => { let session = KaniSession::new(args.verify_opts)?; if !session.args.common_args.quiet { diff --git a/kani-driver/src/metadata.rs b/kani-driver/src/metadata.rs index 625d8b4bbcaa..174ce55187a6 100644 --- a/kani-driver/src/metadata.rs +++ b/kani-driver/src/metadata.rs @@ -96,6 +96,7 @@ pub fn merge_kani_metadata(files: Vec) -> KaniMetadata { proof_harnesses: vec![], unsupported_features: vec![], test_harnesses: vec![], + contracted_functions: vec![], }; for md in files { // Note that we're taking ownership of the original vec, and so we can move the data into the new data structure. @@ -104,6 +105,7 @@ pub fn merge_kani_metadata(files: Vec) -> KaniMetadata { // https://github.com/model-checking/kani/issues/1758 result.unsupported_features.extend(md.unsupported_features); result.test_harnesses.extend(md.test_harnesses); + result.contracted_functions.extend(md.contracted_functions); } result } diff --git a/kani-driver/src/version.rs b/kani-driver/src/version.rs index 95d98b0d6d3e..e1b995c3cd53 100644 --- a/kani-driver/src/version.rs +++ b/kani-driver/src/version.rs @@ -7,7 +7,7 @@ const KANI_RUST_VERIFIER: &str = "Kani Rust Verifier"; /// We assume this is the same as the `kani-verifier` version, but we should /// make sure it's enforced through CI: /// -const KANI_VERSION: &str = env!("CARGO_PKG_VERSION"); +pub(crate) const KANI_VERSION: &str = env!("CARGO_PKG_VERSION"); /// Print Kani version. At present, this is only release version information. pub(crate) fn print_kani_version(invocation_type: InvocationType) { diff --git a/kani_metadata/src/lib.rs b/kani_metadata/src/lib.rs index fa5a8828b6be..96caf92133e9 100644 --- a/kani_metadata/src/lib.rs +++ b/kani_metadata/src/lib.rs @@ -3,9 +3,8 @@ extern crate clap; -use std::{collections::HashSet, path::PathBuf}; - use serde::{Deserialize, Serialize}; +use std::{collections::HashSet, path::PathBuf}; pub use artifact::ArtifactType; pub use cbmc_solver::CbmcSolver; @@ -32,6 +31,18 @@ pub struct KaniMetadata { pub unsupported_features: Vec, /// If crates are built in test-mode, then test harnesses will be recorded here. pub test_harnesses: Vec, + /// The functions with contracts in this crate + pub contracted_functions: Vec, +} + +#[derive(Debug, Clone, Serialize, Deserialize, Eq, PartialEq, PartialOrd, Ord)] +pub struct ContractedFunction { + /// The fully qualified name the user gave to the function (i.e. includes the module path). + pub function: String, + /// The (currently full-) path to the file this function was declared within. + pub file: String, + /// The pretty names of the proof harnesses (`#[kani::proof_for_contract]`) for this function + pub harnesses: Vec, } #[derive(Debug, Clone, Serialize, Deserialize)] diff --git a/kani_metadata/src/unstable.rs b/kani_metadata/src/unstable.rs index abab48304914..a602c33e0326 100644 --- a/kani_metadata/src/unstable.rs +++ b/kani_metadata/src/unstable.rs @@ -96,6 +96,8 @@ pub enum UnstableFeature { UninitChecks, /// Enable an unstable option or subcommand. UnstableOptions, + /// The list subcommand [RFC 13](https://model-checking.github.io/kani/rfc/rfcs/0013-list.html) + List, } impl UnstableFeature { diff --git a/rfc/src/rfcs/0013-list.md b/rfc/src/rfcs/0013-list.md index bdbf4681f430..0d2baee2b594 100644 --- a/rfc/src/rfcs/0013-list.md +++ b/rfc/src/rfcs/0013-list.md @@ -1,8 +1,8 @@ - **Feature Name:** List Subcommand - **Feature Request Issue:** [#2573](https://github.com/model-checking/kani/issues/2573), [#1612](https://github.com/model-checking/kani/issues/1612) - **RFC PR:** #3463 -- **Status:** Under Review -- **Version:** 1 +- **Status:** Unstable +- **Version:** 2 ------------------- @@ -20,53 +20,50 @@ This feature will not cause any regressions for exisiting users. ## User Experience -Users run a `list` subcommand, which prints metadata about the harnesses and contracts in each crate under verification. The subcommand will take the option `--message-format=[pretty|json]`, which changes the output format. The default is `pretty`, which prints to the terminal. The `json` option creates and writes to a JSON file instead. +Users run a `list` subcommand, which prints metadata about the harnesses and contracts in each crate under verification. The subcommand takes two options: +- `--message-format=[pretty|json]`: choose the output format. The default is `pretty`, which prints to the terminal. The `json` option creates and writes to a JSON file instead. +- `--std`: this option should be specified when listing the harnesses and contracts in the standard library. This option is only available for `kani list` (not `cargo kani list`), which mirrors the verification workflow for the standard library. -This subcommand will not fail. In the case that it does not find any harnesses or contracts, it will print a message informing the user of that fact. +This subcommand does not fail. In the case that it does not find any harnesses or contracts, it prints a message informing the user of that fact. ### Pretty Format -The default format, `pretty`, will print the harnesses and contracts in a project, along with the total counts of each. +The default format, `pretty`, prints a "Contracts" table and a "Standard Harnesses" list. +Each row of the "Contracts" table consists of a function under contract and its contract harnesses. +The results are printed in lexicographic order. For example: ``` Kani Rust Verifier 0.54.0 (standalone) -Standard Harnesses: -- example::verify::check_new -- example::verify::check_modify - -Contract Harnesses: -- example::verify::check_foo_u32 -- example::verify::check_foo_u64 -- example::verify::check_func -- example::verify::check_bar - Contracts: -|--------------------------|-----------------------------------------------| -| Function | Contract Harnesses | -|--------------------------|-----------------------------------------------| -| example::impl::func | example::verify::check_func | -|--------------------------|-----------------------------------------------| -| example::impl::bar | example::verify::check_bar | -|--------------------------|-----------------------------------------------| -| example::impl::foo | example::verify::check_foo_u32, | -| | example::verify::check_foo_u64 | -|--------------------------|-----------------------------------------------| -| example::prep::parse | NONE | -|--------------------------|-----------------------------------------------| - -Totals: -- Standard Harnesses: 2 -- Contract Harnesses: 4 -- Functions with Contracts: 4 -- Contracts: 10 +|-------|-------------------------|--------------------------------------------------| +| | Function | Contract Harnesses (#[kani::proof_for_contract]) | +|-------|-------------------------|--------------------------------------------------| +| | example::impl::bar | example::verify::check_bar | +|-------|-------------------------|--------------------------------------------------| +| | example::impl::baz | example::verify::check_baz | +|-------|-------------------------|--------------------------------------------------| +| | example::impl::foo | example::verify::check_foo_u32 | +| | | example::verify::check_foo_u64 | +|-------|-------------------------|--------------------------------------------------| +| | example::impl::func | example::verify::check_func | +|-------|-------------------------|--------------------------------------------------| +| | example::prep::parse | NONE | +|-------|-------------------------|--------------------------------------------------| +| Total | 5 | 5 | +|-------|-------------------------|--------------------------------------------------| + +Standard Harnesses (#[kani::proof]): +1. example::verify::check_modify +2. example::verify::check_new ``` -A "Standard Harness" is a `#[proof]` harness, while a "Contract Harness" is a `#[proof_for_contract]` harness. - -All sections will be present in the output, regardless of the result. If a list is empty, Kani will output a `NONE` string. +All sections will be present in the output, regardless of the result. +If there are no harnesses for a function under contract, Kani inserts `NONE` in the "Contract Harnesses" column. +If the "Contracts" section is empty, Kani prints a message that "No contracts or contract harnesses were found." +If the "Standard Harnesses" section is empty, Kani prints a message that "No standard harnesses were found." ### JSON Format @@ -96,6 +93,7 @@ For example: file: /Users/johnsmith/example/kani_contract_proofs.rs harnesses: [ example::verify::check_bar, + example::verify::check_baz, example::verify::check_foo_u32, example::verify::check_foo_u64, example::verify::check_func @@ -104,14 +102,14 @@ For example: ], contracts: [ { - function: example::impl::func + function: example::impl::bar file: /Users/johnsmith/example/impl.rs - harnesses: [example::verify::check_func] + harnesses: [example::verify::check_bar] }, { - function: example::impl::bar + function: example::impl::baz file: /Users/johnsmith/example/impl.rs - harnesses: [example::verify::check_bar] + harnesses: [example::verify::check_baz] }, { function: example::impl::foo @@ -121,6 +119,11 @@ For example: example::verify::check_foo_u64 ] }, + { + function: example::impl::func + file: /Users/johnsmith/example/impl.rs + harnesses: [example::verify::check_func] + }, { function: example::prep::parse file: /Users/johnsmith/example/prep.rs @@ -129,9 +132,8 @@ For example: ], totals: { standard-harnesses: 2, - contract-harnesses: 4, - functions-with-contracts: 4, - contracts: 10, + contract-harnesses: 5, + functions-with-contracts: 5, } } ``` @@ -141,9 +143,16 @@ If there is no result for a given field (e.g., there are no contracts), Kani wil ## Software Design -We will add a new subcommand to `kani-driver`. +### Driver/Metdata Changes -*We will update this section once the UX is finalized*. +We add a new `list` subcommand to `kani-driver`, which invokes the compiler to collect metadata, then post-processes that metadata and outputs the result. +We extend `KaniMetadata` to include a new field containing each function under contract and its contract harnesses. + +### Compiler Changes + +In `codegen_crate`, we update the generation of `KaniMetadata` to include the new contracts information. +We iterate through each local item in the crate. +Each time we find a function under contract or a contract harness, we include it in the metadata. ## Rationale and alternatives @@ -152,19 +161,22 @@ Users of Kani may have many questions about their project--not only where their 1. Where are the harnesses? 2. Where are the contracts? 3. Which contracts are verified, and by which harnesses? -4. How many harnesses and contracts are there? +4. How many harnesses and functions under contract are there? We believe these questions are the most important for our use cases of tracking verification progress for customers and the standard library. The UX is designed to answer these questions clearly and concisely. We could have a more verbose or granular output, e.g., printing the metadata on a per-crate or per-module level, or including stubs or other attributes. Such a design would have the benefit of providing more information, with the disadvantage of being more complex to implement and more information for the user to process. - If we do not implement this feature, users will have to obtain this metadata through manual searching, or by writing a script to do it themselves. This feature will improve our internal productivity by automating the process. +The Contracts table is close to Markdown, but not quite Markdown--it includes line separators between each row, when Markdown would only have a separator for the header. +We include the separator because without it, it can be difficult to tell from reading the terminal output which entries are in the same row. +The user can transform the table to Markdown by deleting these separators, and we can trivially add a Markdown option in the future if there is demand for it. + ## Open questions -1. Do we want to include more contracts information? We could print more granular information about contracts, e.g., the text of the contracts, the number of `requires`, `ensures`, or `modifies` contracts, or the locations of the contracts. +1. Do we want to include more contracts information? We could print more granular information about contracts, e.g., the text of the contracts or the number of contracts. 2. More generally, we could introduce additional options that collect information about other Kani attributes (e.g., stubs). The default would be to leave them out, but this way a user could get more verbose output if they so choose. -3. Do we want to add a filtering option? For instance, `--harnesses ` and `--contracts `, where `pattern` corresponds to a Rust-style path. For example, `kani list --harnesses "my_crate::my_module::*"` would include all harnesses with that path prefix, while `kani list --contracts "my_crate::my_module::*"` would include all functions under contract with that path prefix. +3. Do we want to add a filtering option? For instance, `--harnesses ` and `--contracts `, where `pattern` corresponds to a Rust-style path. For example, `kani list --harnesses "my_crate::my_module::*"` would include all harnesses with that path prefix, while `kani list --contracts "my_crate::my_module::*"` would include all functions under contract with that path prefix. (If we do this work, we could use it to improve our `--harness` [pattern handling for verification](https://github.com/model-checking/kani/blob/main/kani-driver/src/metadata.rs#L187-L189)). ## Out of scope / Future Improvements @@ -179,4 +191,4 @@ fn check() { See [this blog post](https://model-checking.github.io/kani-verifier-blog/2022/10/27/using-kani-with-the-bolero-property-testing-framework.html) for more information. -There's no easy way for us to know whether a harness comes from Bolero, since Bolero takes care of rewriting the test to use Kani syntax and invoking the Kani engine. By the time the harness gets to Kani, there's no way for us to tell it apart from a regular harness. Fixing this would require some changes to our Bolero integration. \ No newline at end of file +There's no easy way for us to know whether a harness comes from Bolero, since Bolero takes care of rewriting the test to use Kani syntax and invoking the Kani engine. By the time the harness gets to Kani, there's no way for us to tell it apart from a regular harness. Fixing this would require some changes to our Bolero integration. diff --git a/tests/script-based-pre/cargo_list/Cargo.toml b/tests/script-based-pre/cargo_list/Cargo.toml new file mode 100644 index 000000000000..2f213d2fccd7 --- /dev/null +++ b/tests/script-based-pre/cargo_list/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/cargo_list/config.yml b/tests/script-based-pre/cargo_list/config.yml new file mode 100644 index 000000000000..4eac6f79588c --- /dev/null +++ b/tests/script-based-pre/cargo_list/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/cargo_list/list.expected b/tests/script-based-pre/cargo_list/list.expected new file mode 100644 index 000000000000..fb168c5a3bd2 --- /dev/null +++ b/tests/script-based-pre/cargo_list/list.expected @@ -0,0 +1,52 @@ +{ + "kani-version": + "file-version": "0.1", + "standard-harnesses": { + "src/standard_harnesses.rs": [ + "standard_harnesses::example::verify::check_modify", + "standard_harnesses::example::verify::check_new" + ] + }, + "contract-harnesses": { + "src/lib.rs": [ + "example::verify::check_bar", + "example::verify::check_foo_u32", + "example::verify::check_foo_u64", + "example::verify::check_func" + ] + }, + "contracts": [ + { + "function": "example::implementation::bar", + "file": "src/lib.rs", + "harnesses": [ + "example::verify::check_bar" + ] + }, + { + "function": "example::implementation::foo", + "file": "src/lib.rs", + "harnesses": [ + "example::verify::check_foo_u32", + "example::verify::check_foo_u64" + ] + }, + { + "function": "example::implementation::func", + "file": "src/lib.rs", + "harnesses": [ + "example::verify::check_func" + ] + }, + { + "function": "example::prep::parse", + "file": "src/lib.rs", + "harnesses": [] + } + ], + "totals": { + "standard-harnesses": 2, + "contract-harnesses": 4, + "functions-under-contract": 4 + } +} diff --git a/tests/script-based-pre/cargo_list/list.sh b/tests/script-based-pre/cargo_list/list.sh new file mode 100755 index 000000000000..6b1ab80b0f5f --- /dev/null +++ b/tests/script-based-pre/cargo_list/list.sh @@ -0,0 +1,10 @@ +#!/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/src/lib.rs b/tests/script-based-pre/cargo_list/src/lib.rs new file mode 100644 index 000000000000..e7382a9124a3 --- /dev/null +++ b/tests/script-based-pre/cargo_list/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/src/standard_harnesses.rs b/tests/script-based-pre/cargo_list/src/standard_harnesses.rs new file mode 100644 index 000000000000..5df490461d0c --- /dev/null +++ b/tests/script-based-pre/cargo_list/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/config.yml b/tests/script-based-pre/kani_list/config.yml new file mode 100644 index 000000000000..4eac6f79588c --- /dev/null +++ b/tests/script-based-pre/kani_list/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/list.expected new file mode 100644 index 000000000000..e2ed4506eb4e --- /dev/null +++ b/tests/script-based-pre/kani_list/list.expected @@ -0,0 +1,52 @@ +{ + "kani-version": + "file-version": "0.1", + "standard-harnesses": { + "src/lib.rs": [ + "example::verify::check_modify", + "example::verify::check_new" + ] + }, + "contract-harnesses": { + "src/lib.rs": [ + "example::verify::check_bar", + "example::verify::check_foo_u32", + "example::verify::check_foo_u64", + "example::verify::check_func" + ] + }, + "contracts": [ + { + "function": "example::implementation::bar", + "file": "src/lib.rs", + "harnesses": [ + "example::verify::check_bar" + ] + }, + { + "function": "example::implementation::foo", + "file": "src/lib.rs", + "harnesses": [ + "example::verify::check_foo_u32", + "example::verify::check_foo_u64" + ] + }, + { + "function": "example::implementation::func", + "file": "src/lib.rs", + "harnesses": [ + "example::verify::check_func" + ] + }, + { + "function": "example::prep::parse", + "file": "src/lib.rs", + "harnesses": [] + } + ], + "totals": { + "standard-harnesses": 2, + "contract-harnesses": 4, + "functions-under-contract": 4 + } +} diff --git a/tests/script-based-pre/kani_list/list.sh b/tests/script-based-pre/kani_list/list.sh new file mode 100755 index 000000000000..e7bb6f081044 --- /dev/null +++ b/tests/script-based-pre/kani_list/list.sh @@ -0,0 +1,10 @@ +#!/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/src/lib.rs b/tests/script-based-pre/kani_list/src/lib.rs new file mode 100644 index 000000000000..69dbba5a9e0f --- /dev/null +++ b/tests/script-based-pre/kani_list/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() {} + } +}