diff --git a/Cargo.lock b/Cargo.lock index 63f86490e284..11838e1fb6f2 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -176,7 +176,7 @@ dependencies = [ "heck", "proc-macro2", "quote", - "syn", + "syn 2.0.77", ] [[package]] @@ -185,12 +185,44 @@ version = "0.7.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "1462739cb27611015575c0c11df5df7601141071f07518d56fcc1be504cbec97" +[[package]] +name = "cli-table" +version = "0.4.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b53f9241f288a7b12c56565f04aaeaeeab6b8923d42d99255d4ca428b4d97f89" +dependencies = [ + "cli-table-derive", + "csv", + "termcolor", + "unicode-width", +] + +[[package]] +name = "cli-table-derive" +version = "0.4.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3e83a93253aaae7c74eb7428ce4faa6e219ba94886908048888701819f82fb94" +dependencies = [ + "proc-macro2", + "quote", + "syn 1.0.109", +] + [[package]] name = "colorchoice" version = "1.0.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d3fd119d74b830634cea2a0f58bbd0d54540518a14397557951e79340abc28c0" +[[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" @@ -483,7 +515,7 @@ dependencies = [ "shell-words", "strum", "strum_macros", - "syn", + "syn 2.0.77", "tracing", "tracing-subscriber", "tracing-tree", @@ -496,6 +528,8 @@ dependencies = [ "anyhow", "cargo_metadata", "clap", + "cli-table", + "colour", "comfy-table", "console", "glob", @@ -541,7 +575,7 @@ dependencies = [ "proc-macro-error2", "proc-macro2", "quote", - "syn", + "syn 2.0.77", ] [[package]] @@ -819,7 +853,7 @@ dependencies = [ "proc-macro-error-attr2", "proc-macro2", "quote", - "syn", + "syn 2.0.77", ] [[package]] @@ -1027,7 +1061,7 @@ checksum = "243902eda00fad750862fc144cea25caca5e20d615af0a81bee94ca738f1df1f" dependencies = [ "proc-macro2", "quote", - "syn", + "syn 2.0.77", ] [[package]] @@ -1036,6 +1070,7 @@ version = "1.0.128" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "6ff5456707a1de34e7e37f2a6fd3d3f808c318259cbd01ab6377795054b483d8" dependencies = [ + "indexmap", "itoa", "memchr", "ryu", @@ -1134,7 +1169,18 @@ dependencies = [ "proc-macro2", "quote", "rustversion", - "syn", + "syn 2.0.77", +] + +[[package]] +name = "syn" +version = "1.0.109" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", ] [[package]] @@ -1161,6 +1207,15 @@ dependencies = [ "windows-sys 0.59.0", ] +[[package]] +name = "termcolor" +version = "1.4.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "06794f8f6c5c898b3275aebefa6b8a1cb24cd2c6c79397ab15774837a0bc5755" +dependencies = [ + "winapi-util", +] + [[package]] name = "thiserror" version = "1.0.63" @@ -1178,7 +1233,7 @@ checksum = "a4558b58466b9ad7ca0f102865eccc95938dca1a74a856f2b57b6629050da261" dependencies = [ "proc-macro2", "quote", - "syn", + "syn 2.0.77", ] [[package]] @@ -1275,7 +1330,7 @@ checksum = "34704c8d6ebcbc939824180af020566b01a7c01f80641264eba0999f6c2b6be7" dependencies = [ "proc-macro2", "quote", - "syn", + "syn 2.0.77", ] [[package]] @@ -1562,5 +1617,5 @@ checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e" dependencies = [ "proc-macro2", "quote", - "syn", + "syn 2.0.77", ] diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs index a871cd58f94f..0d0f9dc21d67 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs @@ -2,14 +2,15 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use crate::codegen_cprover_gotoc::{codegen::ty_stable::pointee_type_stable, GotocCtx}; use crate::kani_middle::attributes::KaniAttributes; +use crate::kani_middle::find_closure_in_body; use cbmc::goto_program::FunctionContract; use cbmc::goto_program::{Expr, Lambda, Location, Type}; use kani_metadata::AssignsContract; use rustc_hir::def_id::DefId as InternalDefId; use rustc_smir::rustc_internal; use stable_mir::mir::mono::{Instance, MonoItem}; -use stable_mir::mir::{Local, VarDebugInfoContents}; -use stable_mir::ty::{FnDef, RigidTy, TyKind}; +use stable_mir::mir::Local; +use stable_mir::ty::{RigidTy, TyKind}; use stable_mir::CrateDef; impl<'tcx> GotocCtx<'tcx> { @@ -87,33 +88,24 @@ impl<'tcx> GotocCtx<'tcx> { recursion_tracker } + fn find_closure(&mut self, inside: Instance, name: &str) -> Option { + let body = self.transformer.body(self.tcx, inside); + find_closure_in_body(&body, name) + } + /// Find the modifies recursively since we may have a recursion wrapper. /// I.e.: [recursion_wrapper ->]? check -> modifies. fn find_modifies(&mut self, instance: Instance) -> Option { let contract_attrs = KaniAttributes::for_instance(self.tcx, instance).contract_attributes()?; - let mut find_closure = |inside: Instance, name: &str| { - let body = self.transformer.body(self.tcx, inside); - body.var_debug_info.iter().find_map(|var_info| { - if var_info.name.as_str() == name { - let ty = match &var_info.value { - VarDebugInfoContents::Place(place) => place.ty(body.locals()).unwrap(), - VarDebugInfoContents::Const(const_op) => const_op.ty(), - }; - if let TyKind::RigidTy(RigidTy::Closure(def, args)) = ty.kind() { - return Some(Instance::resolve(FnDef(def.def_id()), &args).unwrap()); - } - } - None - }) - }; let check_instance = if contract_attrs.has_recursion { - let recursion_check = find_closure(instance, contract_attrs.recursion_check.as_str())?; - find_closure(recursion_check, contract_attrs.checked_with.as_str())? + let recursion_check = + self.find_closure(instance, contract_attrs.recursion_check.as_str())?; + self.find_closure(recursion_check, contract_attrs.checked_with.as_str())? } else { - find_closure(instance, contract_attrs.checked_with.as_str())? + self.find_closure(instance, contract_attrs.checked_with.as_str())? }; - find_closure(check_instance, contract_attrs.modifies_wrapper.as_str()) + self.find_closure(check_instance, contract_attrs.modifies_wrapper.as_str()) } /// Convert the Kani level contract into a CBMC level contract by creating a diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 9f700192f2f2..e57baa35f860 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -9,6 +9,7 @@ use crate::kani_middle::analysis; use crate::kani_middle::attributes::{is_test_harness_description, KaniAttributes}; use crate::kani_middle::check_reachable_items; use crate::kani_middle::codegen_units::{CodegenUnit, CodegenUnits}; +use crate::kani_middle::list::collect_contracted_fns; use crate::kani_middle::metadata::gen_test_metadata; use crate::kani_middle::provide; use crate::kani_middle::reachability::{ @@ -21,8 +22,7 @@ use cbmc::irep::goto_binary_serde::write_goto_binary_file; use cbmc::RoundingMode; use cbmc::{InternedString, MachineModel}; use kani_metadata::artifact::convert_type; -use kani_metadata::UnsupportedFeature; -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, DEFAULT_OBJECT_READER}; use rustc_codegen_ssa::back::metadata::create_wrapper_file; @@ -342,7 +342,10 @@ impl CodegenBackend for GotocCodegenBackend { results.harnesses.push(metadata); } } - ReachabilityType::None => {} + ReachabilityType::None => { + let units = CodegenUnits::new(&queries, tcx); + units.write_metadata(&queries, tcx); + } ReachabilityType::PubFns => { let unit = CodegenUnit::default(); let transformer = BodyTransformation::new(&queries, tcx, &unit); @@ -381,7 +384,7 @@ impl CodegenBackend for GotocCodegenBackend { write_file( &base_filename, ArtifactType::Metadata, - &results.generate_metadata(), + &results.generate_metadata(tcx), queries.args().output_pretty_json, ); } @@ -620,7 +623,7 @@ impl GotoCodegenResults { } } /// Method that generates `KaniMetadata` from the given compilation results. - pub fn generate_metadata(&self) -> KaniMetadata { + pub fn generate_metadata(&self, tcx: TyCtxt) -> KaniMetadata { // Maps the goto-context "unsupported features" data into the KaniMetadata "unsupported features" format. // TODO: Do we really need different formats?? let unsupported_features = self @@ -652,6 +655,7 @@ impl GotoCodegenResults { proof_harnesses: proofs, unsupported_features, test_harnesses: tests, + contracted_functions: collect_contracted_fns(tcx), } } diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index d16e4d2b93d1..36c3fbd28e3d 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -9,6 +9,7 @@ use crate::args::ReachabilityType; use crate::kani_middle::attributes::is_proof_harness; +use crate::kani_middle::list::collect_contracted_fns; use crate::kani_middle::metadata::gen_proof_metadata; use crate::kani_middle::reachability::filter_crate_items; use crate::kani_middle::resolve::expect_resolve_fn; @@ -57,26 +58,29 @@ pub struct CodegenUnit { impl CodegenUnits { pub fn new(queries: &QueryDb, tcx: TyCtxt) -> Self { let crate_info = CrateInfo { name: stable_mir::local_crate().name.as_str().into() }; - if queries.args().reachability_analysis == ReachabilityType::Harnesses { - let base_filepath = tcx.output_filenames(()).path(OutputType::Object); - let base_filename = base_filepath.as_path(); - let harnesses = filter_crate_items(tcx, |_, instance| is_proof_harness(tcx, instance)); - let all_harnesses = harnesses - .into_iter() - .map(|harness| { - let metadata = gen_proof_metadata(tcx, harness, &base_filename); - (harness, metadata) - }) - .collect::>(); + let base_filepath = tcx.output_filenames(()).path(OutputType::Object); + let base_filename = base_filepath.as_path(); + let harnesses = filter_crate_items(tcx, |_, instance| is_proof_harness(tcx, instance)); + let all_harnesses = harnesses + .into_iter() + .map(|harness| { + let metadata = gen_proof_metadata(tcx, harness, &base_filename); + (harness, metadata) + }) + .collect::>(); + if queries.args().reachability_analysis == ReachabilityType::Harnesses { // Even if no_stubs is empty we still need to store rustc metadata. let units = group_by_stubs(tcx, &all_harnesses); validate_units(tcx, &units); debug!(?units, "CodegenUnits::new"); CodegenUnits { units, harness_info: all_harnesses, crate_info } } else { - // Leave other reachability type handling as is for now. - CodegenUnits { units: vec![], harness_info: HashMap::default(), crate_info } + // Only ReachabilityType::Harnesses uses harness_info directly, + // but we collect it for the other ReachabilityTypes so that we can write the metadata to a file. + // Then, if the user invokes the list subcommand after verification, the metadata will already be cached + // and we do not need to recompile. + CodegenUnits { units: vec![], harness_info: all_harnesses, crate_info } } } @@ -93,7 +97,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 +107,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 +115,7 @@ impl CodegenUnits { proof_harnesses, unsupported_features: vec![], test_harnesses, + contracted_functions: collect_contracted_fns(tcx), } } } diff --git a/kani-compiler/src/kani_middle/list.rs b/kani-compiler/src/kani_middle/list.rs new file mode 100644 index 000000000000..5d03bb86cb20 --- /dev/null +++ b/kani-compiler/src/kani_middle/list.rs @@ -0,0 +1,103 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Collects contract and contract harness metadata for the list subcommand. + +use std::collections::HashMap; + +use crate::kani_middle::attributes::{matches_diagnostic as matches_function, KaniAttributes}; +use crate::kani_middle::{find_closure_in_body, InternalDefId, SourceLocation}; +use kani_metadata::ContractedFunction; +use rustc_middle::ty::TyCtxt; +use rustc_smir::rustc_internal; +use stable_mir::mir::mono::Instance; +use stable_mir::mir::{Body, TerminatorKind}; +use stable_mir::ty::{RigidTy, TyKind}; +use stable_mir::{CrateDef, CrateItems}; + +/// Map each function to its contract harnesses +/// `fns` includes all functions with contracts and all functions that are targets of a contract harness. +fn fns_to_harnesses(tcx: TyCtxt) -> HashMap> { + // 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 fns_to_harnesses: HashMap> = HashMap::new(); + + for item in crate_items { + let def_id = rustc_internal::internal(tcx, item.def_id()); + let fn_name = tcx.def_path_str(def_id); + let attributes = KaniAttributes::for_item(tcx, def_id); + + if attributes.has_contract() { + fns_to_harnesses.insert(def_id, vec![]); + } else if let Some((_, target_def_id, _)) = attributes.interpret_for_contract_attribute() { + if let Some(harnesses) = fns_to_harnesses.get_mut(&target_def_id) { + harnesses.push(fn_name); + } else { + fns_to_harnesses.insert(target_def_id, vec![fn_name]); + } + } + } + + fns_to_harnesses +} + +/// Count the number of contracts in `check_body`, where `check_body` is the body of the +/// kanitool::checked_with closure (c.f. kani_macros::sysroot::contracts). +/// In this closure, preconditions are denoted by kani::assume() calls and postconditions by kani::assert() calls. +/// The number of contracts is the number of times these functions are called inside the closure +fn count_contracts(tcx: TyCtxt, check_body: &Body) -> usize { + let mut count = 0; + + for bb in &check_body.blocks { + if let TerminatorKind::Call { ref func, .. } = bb.terminator.kind { + let fn_ty = func.ty(check_body.locals()).unwrap(); + if let TyKind::RigidTy(RigidTy::FnDef(fn_def, args)) = fn_ty.kind() { + if let Ok(instance) = Instance::resolve(fn_def, &args) { + // For each precondition or postcondition, increment the count + if matches_function(tcx, instance.def, "KaniAssume") + || matches_function(tcx, instance.def, "KaniAssert") + { + count += 1; + } + } + } + } + } + count +} + +/// For each function with contracts (or that is a target of a contract harness), +/// construct a ContractedFunction object for it and store it in `units`. +pub fn collect_contracted_fns(tcx: TyCtxt) -> Vec { + let mut contracted_fns = vec![]; + for (fn_def_id, harnesses) in fns_to_harnesses(tcx) { + let attrs = KaniAttributes::for_item(tcx, fn_def_id); + + // It's possible that a function is a target of a proof for contract but does not actually have contracts. + // If the function does have contracts, count them. + let total_contracts = if attrs.has_contract() { + let contract_attrs = + KaniAttributes::for_item(tcx, fn_def_id).contract_attributes().unwrap(); + let body: Body = rustc_internal::stable(tcx.optimized_mir(fn_def_id)); + let check_body: Body = + find_closure_in_body(&body, contract_attrs.checked_with.as_str()) + .unwrap() + .body() + .unwrap(); + + count_contracts(tcx, &check_body) + } else { + 0 + }; + + contracted_fns.push(ContractedFunction { + function: tcx.def_path_str(fn_def_id), + file: SourceLocation::new(rustc_internal::stable(tcx.def_span(fn_def_id))).filename, + harnesses, + total_contracts, + }); + } + + contracted_fns +} diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs index 2f0f22d49e1c..40686362cbca 100644 --- a/kani-compiler/src/kani_middle/metadata.rs +++ b/kani-compiler/src/kani_middle/metadata.rs @@ -13,7 +13,6 @@ use stable_mir::CrateDef; use super::{attributes::KaniAttributes, SourceLocation}; -/// 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 { let def = instance.def; let kani_attributes = KaniAttributes::for_instance(tcx, instance); diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index f281e5de5e88..0d99ba08ce85 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -18,7 +18,8 @@ use rustc_span::source_map::respan; use rustc_span::Span; use rustc_target::abi::call::FnAbi; use rustc_target::abi::{HasDataLayout, TargetDataLayout}; -use stable_mir::mir::mono::MonoItem; +use stable_mir::mir::mono::{Instance, MonoItem}; +use stable_mir::mir::{Body, VarDebugInfoContents}; use stable_mir::ty::{FnDef, RigidTy, Span as SpanStable, Ty, TyKind}; use stable_mir::visitor::{Visitable, Visitor as TyVisitor}; use stable_mir::CrateDef; @@ -31,6 +32,7 @@ pub mod attributes; pub mod codegen_units; pub mod coercion; mod intrinsics; +pub mod list; pub mod metadata; pub mod points_to; pub mod provide; @@ -238,3 +240,19 @@ pub fn stable_fn_def(tcx: TyCtxt, def_id: InternalDefId) -> Option { None } } + +/// Find the user-declared closure by the name `name` in `body`. +pub fn find_closure_in_body(body: &Body, name: &str) -> Option { + body.var_debug_info.iter().find_map(|var_info| { + if var_info.name.as_str() == name { + let ty = match &var_info.value { + VarDebugInfoContents::Place(place) => place.ty(body.locals()).unwrap(), + VarDebugInfoContents::Const(const_op) => const_op.ty(), + }; + if let TyKind::RigidTy(RigidTy::Closure(def, args)) = ty.kind() { + return Some(Instance::resolve(FnDef(def.def_id()), &args).unwrap()); + } + } + None + }) +} diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index 7485d2279ad6..85a93aff5940 100644 --- a/kani-driver/Cargo.toml +++ b/kani-driver/Cargo.toml @@ -18,8 +18,10 @@ 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"] } +cli-table = "0.4.9" +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..0b7a80875f3a --- /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::ErrorKind, Error, Parser, ValueEnum}; +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 c3cfc113af64..5f16fa2b5f02 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; @@ -93,6 +94,8 @@ pub enum StandaloneSubcommand { Playback(Box), /// Verify the rust standard library. VerifyStd(Box), + /// Execute the list subcommand + List(Box), } #[derive(Debug, clap::Parser)] @@ -118,6 +121,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, @@ -424,6 +430,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(..)) => {} }; @@ -470,6 +477,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..028adec68444 --- /dev/null +++ b/kani-driver/src/list/collect_metadata.rs @@ -0,0 +1,102 @@ +// 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; + +use crate::{ + args::list_args::{CargoListArgs, Format, StandaloneListArgs}, + list::output::{json, pretty}, + list::Totals, + project::{cargo_project, standalone_project, std_project, Project}, + session::KaniSession, + version::print_kani_version, + InvocationType, +}; +use anyhow::Result; +use kani_metadata::{ContractedFunction, HarnessKind, KaniMetadata}; + +fn process_metadata(metadata: Vec, format: Format) -> Result<()> { + // 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: Vec = vec![]; + + let mut total_standard_harnesses = 0; + let mut total_contract_harnesses = 0; + let mut total_contracts = 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.push(harness_meta.pretty_name); + } else { + standard_harnesses + .insert(harness_meta.original_file, vec![harness_meta.pretty_name]); + } + } + HarnessKind::ProofForContract { .. } => { + total_contract_harnesses += 1; + if let Some(harnesses) = contract_harnesses.get_mut(&harness_meta.original_file) + { + harnesses.push(harness_meta.pretty_name); + } else { + contract_harnesses + .insert(harness_meta.original_file, vec![harness_meta.pretty_name]); + } + } + HarnessKind::Test => {} + } + } + + for cf in &kani_meta.contracted_functions { + total_contracts += cf.total_contracts; + } + + contracted_functions.extend(kani_meta.contracted_functions.into_iter()); + } + + // Print in alphabetical order + contracted_functions.sort_by_key(|cf| cf.function.clone()); + + let totals = Totals { + standard_harnesses: total_standard_harnesses, + contract_harnesses: total_contract_harnesses, + contracted_functions: contracted_functions.len(), + contracts: total_contracts, + }; + + 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..74108c93fceb --- /dev/null +++ b/kani-driver/src/list/mod.rs @@ -0,0 +1,13 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// Implements the list subcommand logic + +pub mod collect_metadata; +mod output; + +struct Totals { + standard_harnesses: usize, + contract_harnesses: usize, + contracted_functions: usize, + contracts: usize, +} diff --git a/kani-driver/src/list/output.rs b/kani-driver/src/list/output.rs new file mode 100644 index 000000000000..80f134ee5dbf --- /dev/null +++ b/kani-driver/src/list/output.rs @@ -0,0 +1,110 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// This module handles outputting the result for the list subcommand + +use std::{collections::BTreeMap, fs::File, io::BufWriter}; + +use crate::{list::Totals, version::KANI_VERSION}; +use anyhow::Result; +use cli_table::{print_stdout, Cell, CellStruct, Style, Table}; +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"; + +pub fn pretty( + standard_harnesses: BTreeMap>, + contracted_functions: Vec, + totals: Totals, +) -> Result<()> { + fn format_contract_harnesses(harnesses: &mut [String]) -> String { + harnesses.sort(); + let joined = harnesses.join("\n"); + if joined.is_empty() { "NONE".to_string() } else { joined } + } + + print_ln_bold!("\nContracts:"); + println!( + "Each function in the table below either has contracts or is the target of a contract harness (#[kani::proof_for_contract])." + ); + + if contracted_functions.is_empty() { + println!("No contracts or contract harnesses found.") + } else { + let mut contracts_table: Vec> = vec![]; + + for mut cf in contracted_functions { + contracts_table.push(vec![ + "".cell(), + cf.function.cell(), + cf.total_contracts.cell(), + format_contract_harnesses(&mut cf.harnesses).cell(), + ]); + } + + contracts_table.push(vec![ + "Total".cell().bold(true), + totals.contracted_functions.cell(), + totals.contracts.cell(), + totals.contract_harnesses.cell(), + ]); + + print_stdout(contracts_table.table().title(vec![ + "".cell(), + "Function".cell().bold(true), + "# of Contracts".cell().bold(true), + "Contract Harnesses".cell().bold(true), + ]))?; + } + + print_ln_bold!("\nStandard Harnesses (#[kani::proof]):"); + if standard_harnesses.is_empty() { + println!("No standard harnesses found."); + } + + 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(()) +} + +pub fn json( + standard_harnesses: BTreeMap>, + contract_harnesses: BTreeMap>, + contracted_functions: Vec, + totals: Totals, +) -> Result<()> { + let filename = "kani-list.json"; + + let out_file = File::create(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, + "contracts": totals.contracts, + } + }); + + serde_json::to_writer_pretty(writer, &json_obj)?; + + Ok(()) +} diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index d3bd697d2ea4..c40a014ba861 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 3f9cd8f2bf84..8170f0ab291b 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/project.rs b/kani-driver/src/project.rs index e0d2d2edd139..694c448aa413 100644 --- a/kani-driver/src/project.rs +++ b/kani-driver/src/project.rs @@ -8,6 +8,7 @@ use crate::metadata::from_json; use crate::session::KaniSession; use crate::util::crate_name; use anyhow::{Context, Result}; +use kani_metadata::UnstableFeature; use kani_metadata::{ artifact::convert_type, ArtifactType, ArtifactType::*, HarnessMetadata, KaniMetadata, }; @@ -90,6 +91,18 @@ impl Project { cargo_metadata: Option, failed_targets: Option>, ) -> Result { + // For the list subcommand, we do not generate any goto, so skip extending the artifacts + if session.args.common_args.unstable_features.contains(UnstableFeature::List) { + return Ok(Project { + outdir, + input, + metadata, + artifacts: vec![], + cargo_metadata, + failed_targets, + }); + } + // For each harness (test or proof) from each metadata, read the path for the goto // SymTabGoto file. Use that path to find all the other artifacts. let mut artifacts = vec![]; 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..0a7229d18635 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,20 @@ 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)] +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 number of contracts applied to this function + pub total_contracts: usize, + /// 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 11df998c820f..db302498ef58 100644 --- a/kani_metadata/src/unstable.rs +++ b/kani_metadata/src/unstable.rs @@ -94,6 +94,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..48c626d8551b 100644 --- a/rfc/src/rfcs/0013-list.md +++ b/rfc/src/rfcs/0013-list.md @@ -2,7 +2,7 @@ - **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 +- **Version:** 2 ------------------- @@ -20,53 +20,53 @@ 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]`: change the output format. The default is `pretty`, which prints to the terminal. The `json` option creates and writes to a JSON file instead. +- `--std`: Include if we are running on 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, the number of contracts it has, and its contract harnesses. +A function is listed if it has contracts or it is the target of contract harness(es). 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 +Each function in the table below either has contracts +or is the target of a contract harness (#[kani::proof_for_contract]). + +|-------|-------------------------|----------------|-------------------------------------| +| | Function | # of Contracts | Contract Harnesses | +|-------|-------------------------|----------------|-------------------------------------| +| | example::impl::bar | 4 | example::verify::check_bar | +|-------|-------------------------|----------------|-------------------------------------| +| | example::impl::baz | 0 | example::verify::check_baz | +|-------|-------------------------|----------------|-------------------------------------| +| | example::impl::foo | 2 | example::verify::check_foo_u32 | +| | | | example::verify::check_foo_u64 | +|-------|-------------------------|----------------|-------------------------------------| +| | example::impl::func | 1 | example::verify::check_func | +|-------|-------------------------|----------------|-------------------------------------| +| | example::prep::parse | 1 | NONE | +|-------|-------------------------|----------------|-------------------------------------| +| Total | 5 | 8 | 5 | +|-------|-------------------------|----------------|-------------------------------------| + +Standard Harnesses (#[kani::proof]): +1. example::verify::check_new +2. example::verify::check_modify ``` -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" row. +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 +96,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,34 +105,44 @@ For example: ], contracts: [ { - function: example::impl::func + function: example::impl::bar + total_contracts: 4 file: /Users/johnsmith/example/impl.rs - harnesses: [example::verify::check_func] + harnesses: [example::verify::check_bar] }, { - function: example::impl::bar + function: example::impl::baz + total_contracts: 0 file: /Users/johnsmith/example/impl.rs - harnesses: [example::verify::check_bar] + harnesses: [example::verify::check_baz] }, { function: example::impl::foo + total_contracts: 2 file: /Users/johnsmith/example/impl.rs harnesses: [ example::verify::check_foo_u32, example::verify::check_foo_u64 ] }, + { + function: example::impl::func + total_contracts: 1 + file: /Users/johnsmith/example/impl.rs + harnesses: [example::verify::check_func] + }, { function: example::prep::parse + total_contracts: 1 file: /Users/johnsmith/example/prep.rs harnesses: [] } ], totals: { standard-harnesses: 2, - contract-harnesses: 4, - functions-with-contracts: 4, - contracts: 10, + contract-harnesses: 5, + functions-with-contracts: 5, + contracts: 8, } } ``` @@ -141,9 +152,98 @@ 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`. +### Metdata Changes +We introduce a new `ContractedFunction` struct to `kani_metadata`: +```rust +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 number of contracts applied to this function + pub total_contracts: usize, + /// The pretty names of the proof harnesses (`#[kani::proof_for_contract]`) for this function + pub harnesses: Vec, +} +``` +We extend `KaniMetadata` and `CodegenUnits` with new `contracted_functions: Vec` fields. + +### Compiler Changes + +This subcommand is concerned with two fields of `KaniMetadata`: `proof_harnesses` and `contracted_functions`. +In `codegen_crate()`, `kani-compiler` will check if we are running the list subcommand, and, if so, it constructs a new `CodegenUnits` object. +The `CodegenUnits` constructor handles initializing the `proof_harnesses` field for us. +We add new functionality to populate the `contracted_functions` field, which we explain in two parts: + +#### Part 1: Map Functions to Harnesses -*We will update this section once the UX is finalized*. +First, we iterate through each local item in the crate and construct a map of functions to contract harnesses. +The keys in this map are functions that either 1) have contracts or 2) are targets of contract harnesses. +These are not necessarily identical sets; functions under contract may not have harnesses, and targets of contract harnesses may not have contracts. + +Observe that we iterate through each local item in the crate (`stable_mir::CrateItem`), not each local *instance* (`stable_mir::Instance`). +This is so that we can include generic functions with contracts in the output. +`Instances` are monomorphized. +When we're verifying a contract harness, this monomorphization assumption is fine; if the harness calls the function under contract, a monomorphized version of the function must exist. +However, if we are just trying to list metadata, we cannot rely on this assumption that the function under contract gets called, and therefore cannot assume that a monomorphized version of the generic function exists. +For example, imagine running `kani list` on a file with only these contents: +```rust +#[kani::requires(true)] +fn foo(x: T) -> T { x } +``` +Kani should be able to find `foo` and report it has a contract, +but we cannot construct a `stable_mir::Instance` from `foo` because it requires monomorphization. + +#### Part 2: Count Contracts +For each function in the map from Part 1, we count its contracts, then construct a `ContractedFunction` object for it. + +Since we are counting the contracts at the MIR level, we work with the expanded version of the contract attribute macros. +We locate the body of the `kanitool::checked_with` closure, then count the number of `kani::assume()` and `kani::assert()` calls. +For example, given the following code (example taken from `kani_macros` contracts documentation): + +```rust +#[kani::requires(divisor != 0)] +#[kani::ensures(|result : &u32| *result <= dividend)] +fn div(dividend: u32, divisor: u32) -> u32 { + dividend / divisor +} +``` + +The generated `check` closure is: + +```rust +let mut __kani_check_div = + || -> u32 + { + kani::assume(divisor != 0); + let _wrapper_arg = (); + #[kanitool::is_contract_generated(wrapper)] + #[allow(dead_code, unused_variables, unused_mut)] + let mut __kani_modifies_div = + |_wrapper_arg| -> u32 { dividend / divisor }; + let result_kani_internal: u32 = + __kani_modifies_div(_wrapper_arg); + kani::assert(kani::internal::apply_closure(|result: &u32| + *result <= dividend, &result_kani_internal), + "|result : &u32| *result <= dividend"); + result_kani_internal + }; +; +``` + +Observe that there is one `kani::assume()` call for the `requires` contract and one `kani::assert()` +call for the `ensures` contract, so we can obtain the total number of contracts by counting these calls. + +Once these parts are complete, `CodegenUnits` contains all of the required metadata. +We use an existing method (`CodegenUnits::write_metadata`) to write this metadata to a file. + +### Driver Changes +We add a new subcommand to `kani-driver`. +This subcommand exists for both `cargo kani` and `kani` invocations. +The driver constructs a `Project` representing the input. +(For `kani` invocations, the driver either constructs a `standalone_project` or a `std_project` depending on whether the use passed the `--std` flag). +The `Project` is populated with `metadata: Vec` from `kani-compiler`. +We iterate through this metadata to print a table with the results or output a `kani-list.json` file, depending on the user-specified `format` argument. ## Rationale and alternatives @@ -160,11 +260,52 @@ We could have a more verbose or granular output, e.g., printing the metadata on 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. +### Modifies Clauses +As discussed in [Software Design](#software-design), the contracts count includes `requires` and `ensures` contracts only. +We do not include `modifies` clauses for two reasons: +1. `modifies` clauses are not really "contracts" in the same way that `requires` and `ensures` are--they are important for our contracts instrumentation (c.f. [#2594](https://github.com/model-checking/kani/issues/2594)), but it's not as if Kani goes and verifies that the function actually modifies the pointer. +For example, if I write this: + +```rust +#[kani::modifies(x)] +fn foo(x: &mut u32) {} + +#[kani::proof_for_contract(foo)] +fn check_foo() { + let mut x = 7; + foo(&mut x); +} +``` +verification succeeds even though `foo` does not modify the location to which `x` points. + +2. `kani_macros` folds the arguments to each `modifies` into a single tuple, e.g.: +```rust +#[modifies(x)] +#[modifies(y)] +fn foo(x: &mut u32, y: &mut u32) {} +``` + +```rust +#[modifies(x, y)] +fn foo(x: &mut u32, y: &mut u32) {} +``` + +are indistinguishable once the macro expansion finishes. +We could of course count the modifies clauses before macro expansion, but even if we do, it's not clear whether counting the number of *attributes* or *arguments* is more intuitive. +In the latter example above, do we have two modifies clauses (one each for `x` and `y`), or just one, since we only wrote one `#[modifies]`? + +I decided it was better to not include modifies clauses to avoid confusing the user. +Thus, for functions that only have modifies clauses, the subcommand will report that the user has zero contracts. +However, users could still be confused by this choice because Kani allows users to run `proof_for_contract` harnesses on functions that only have `modifies` clauses. +(If Kani detects no contract-related attributes at all, it errors.) +A user may be confused as to why the list subcommand reports zero contracts when they are running a `proof_for_contract` harness without errors. + + ## 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. 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 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..00f6ef48965e --- /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 = "sample_crate" +version = "0.1.0" +edition = "2021" + +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } \ No newline at end of file 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..816e3413c65f --- /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-pretty.expected diff --git a/tests/script-based-pre/cargo_list/list-pretty.expected b/tests/script-based-pre/cargo_list/list-pretty.expected new file mode 100644 index 000000000000..e86fd0d595b2 --- /dev/null +++ b/tests/script-based-pre/cargo_list/list-pretty.expected @@ -0,0 +1,36 @@ +Contracts: +Each function in the table below either has contracts or is the target of a contract harness (#[kani::proof_for_contract]). + +Function +# of Contracts +Contract Harnesses + +example::implementation::bar +4 +example::verify::check_bar + +example::implementation::baz +0 +example::verify::check_baz + +example::implementation::foo +2 +example::verify::check_foo_u32 + +example::verify::check_foo_u64 +example::implementation::func +1 +example::verify::check_func + +example::prep::parse +1 +NONE + +Total +5 +8 +5 + +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/list.sh b/tests/script-based-pre/cargo_list/list.sh new file mode 100755 index 000000000000..c394e8dff8de --- /dev/null +++ b/tests/script-based-pre/cargo_list/list.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +# The table in the expected omits the table borders because the runtest script +# does not evaluate the table borders in the captured output as equal to the table borders in the expected file. + +cargo kani list -Z list \ No newline at end of file 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..82044b6d7ea5 --- /dev/null +++ b/tests/script-based-pre/cargo_list/src/lib.rs @@ -0,0 +1,78 @@ +// 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 { + 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; + } + + pub fn baz(x: &mut i32) { + *x /= 1; + } + } + + mod prep { + #[kani::requires(s.len() < 10)] + fn parse(s: &str) -> u32 { + s.parse().unwrap() + } + } + + 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_for_contract(implementation::baz)] + fn check_baz() { + let mut x = 7; + implementation::baz(&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..816e3413c65f --- /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-pretty.expected diff --git a/tests/script-based-pre/kani_list/list-pretty.expected b/tests/script-based-pre/kani_list/list-pretty.expected new file mode 100644 index 000000000000..5d22cd0e7eb9 --- /dev/null +++ b/tests/script-based-pre/kani_list/list-pretty.expected @@ -0,0 +1,36 @@ +Contracts: +Each function in the table below either has contracts or is the target of a contract harness (#[kani::proof_for_contract]). + +Function +# of Contracts +Contract Harnesses + +example::implementation::bar +4 +example::verify::check_bar + +example::implementation::baz +0 +example::verify::check_baz + +example::implementation::foo +2 +example::verify::check_foo_u32 + +example::verify::check_foo_u64 +example::implementation::func +1 +example::verify::check_func + +example::prep::parse +1 +NONE + +Total +5 +8 +5 + +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/list.sh b/tests/script-based-pre/kani_list/list.sh new file mode 100755 index 000000000000..bbd852a8b054 --- /dev/null +++ b/tests/script-based-pre/kani_list/list.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +# The table in the expected omits the table borders because the runtest script +# does not evaluate the table borders in the captured output as equal to the table borders in the expected file. + +kani list -Z list src/lib.rs \ No newline at end of file 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..16bab7aaaebc --- /dev/null +++ b/tests/script-based-pre/kani_list/src/lib.rs @@ -0,0 +1,81 @@ +// 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 { + 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; + } + + pub fn baz(x: &mut i32) { + *x /= 1; + } + } + + mod prep { + #[kani::requires(s.len() < 10)] + fn parse(s: &str) -> u32 { + s.parse().unwrap() + } + } + + 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_for_contract(implementation::baz)] + fn check_baz() { + let mut x = 7; + implementation::baz(&mut x); + } + + #[kani::proof] + fn check_modify() {} + + #[kani::proof] + fn check_new() {} + } +}