diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index cf8b33232f40..e60455ed8bc2 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -36,7 +36,7 @@ use std::sync::OnceLock; use tracing::debug; /// An identifier for the harness function. -type Harness = Instance; +pub type Harness = Instance; /// A set of stubs. pub type Stubs = HashMap; @@ -92,8 +92,7 @@ impl CodegenUnits { args, *kani_fns.get(&KaniModel::Any.into()).unwrap(), ); - let chosen_fn_names = - chosen.iter().map(|func| func.name().clone()).collect::>(); + let chosen_fn_names = chosen.iter().map(|func| func.name()).collect::>(); AUTOHARNESS_MD .set(AutoHarnessMetadata { chosen: chosen_fn_names, skipped }) .expect("Initializing the autoharness metdata failed"); @@ -167,7 +166,7 @@ impl CodegenUnits { proof_harnesses, unsupported_features: vec![], test_harnesses, - contracted_functions: gen_contracts_metadata(tcx), + contracted_functions: gen_contracts_metadata(tcx, &self.harness_info), autoharness_md: AUTOHARNESS_MD.get().cloned(), } } diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs index b24b39578df5..50487ce45714 100644 --- a/kani-compiler/src/kani_middle/metadata.rs +++ b/kani-compiler/src/kani_middle/metadata.rs @@ -7,6 +7,7 @@ use std::collections::HashMap; use std::path::Path; use crate::kani_middle::attributes::{KaniAttributes, test_harness_name}; +use crate::kani_middle::codegen_units::Harness; use crate::kani_middle::{SourceLocation, stable_fn_def}; use kani_metadata::ContractedFunction; use kani_metadata::{ArtifactType, HarnessAttributes, HarnessKind, HarnessMetadata}; @@ -47,7 +48,10 @@ pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) -> /// /// 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 { +pub fn gen_contracts_metadata( + tcx: TyCtxt, + harness_info: &HashMap, +) -> 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(); @@ -61,8 +65,8 @@ pub fn gen_contracts_metadata(tcx: TyCtxt) -> Vec { 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() + // This logic finds manual contract harnesses only (automatic harnesses are a Kani intrinsic, not crate items annotated with the proof_for_contract attribute). + } else if let Some((_, 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") @@ -73,7 +77,9 @@ pub fn gen_contracts_metadata(tcx: TyCtxt) -> Vec { fn_to_data.insert( target_def_id, ContractedFunction { - function: target_name.to_string(), + // Note that we use the item's fully qualified-name, rather than the target name specified in the attribute. + // This is necessary for the automatic contract harness lookup, see below. + function: item.name(), file, harnesses: vec![function], }, @@ -82,6 +88,24 @@ pub fn gen_contracts_metadata(tcx: TyCtxt) -> Vec { } } + // Find automatically generated contract harnesses (if the `autoharness` subcommand is running) + for (harness, metadata) in harness_info { + if !metadata.is_automatically_generated { + continue; + } + if let HarnessKind::ProofForContract { target_fn } = &metadata.attributes.kind { + // FIXME: This is a bit hacky. We can't resolve the target_fn to a DefId because we need somewhere to start the name resolution from. + // For a manual harness, we could just start from the harness, but since automatic harnesses are Kani intrinsics, we can't resolve the target starting from them. + // Instead, we rely on the fact that the ContractedFunction objects store the function's fully qualified name, + // and that `gen_automatic_proof_metadata` uses the fully qualified name as well. + // Once we implement multiple automatic harnesses for a single function, we will have to revise the HarnessMetadata anyway, + // and then we can revisit the idea of storing the target_fn's DefId somewhere. + let (_, target_cf) = + fn_to_data.iter_mut().find(|(_, cf)| &cf.function == target_fn).unwrap(); + target_cf.harnesses.push(harness.name()); + } + } + fn_to_data.into_values().collect() } diff --git a/kani-driver/src/args/autoharness_args.rs b/kani-driver/src/args/autoharness_args.rs index bdba0e340d8d..3dc8f6973703 100644 --- a/kani-driver/src/args/autoharness_args.rs +++ b/kani-driver/src/args/autoharness_args.rs @@ -4,6 +4,7 @@ use std::path::PathBuf; +use crate::args::list_args::Format; use crate::args::{ValidateArgs, VerificationArgs, validate_std_path}; use clap::{Error, Parser, error::ErrorKind}; use kani_metadata::UnstableFeature; @@ -29,6 +30,13 @@ pub struct CommonAutoharnessArgs { pub exclude_function: Vec, // TODO: It would be nice if we could borrow --exact here from VerificationArgs to differentiate between partial/exact matches, // like --harnesses does. Sharing arguments with VerificationArgs doesn't work with our current structure, though. + /// Run the `list` subcommand after generating the automatic harnesses. Requires -Z list. Note that this option implies --only-codegen. + #[arg(long)] + pub list: bool, + + /// The format of the `list` output. Requires --list. + #[arg(long, default_value = "pretty", requires = "list")] + pub format: Format, } /// Automatically verify functions in a crate. @@ -76,6 +84,24 @@ impl ValidateArgs for CargoAutoharnessArgs { )); } + if self.common_autoharness_args.list + && !self.verify_opts.common_args.unstable_features.contains(UnstableFeature::List) + { + return Err(Error::raw( + ErrorKind::MissingRequiredArgument, + format!("The `list` feature is unstable and requires -Z {}", UnstableFeature::List), + )); + } + + if self.common_autoharness_args.format == Format::Pretty + && self.verify_opts.common_args.quiet + { + return Err(Error::raw( + ErrorKind::ArgumentConflict, + "The `--quiet` flag is not compatible with the `pretty` format, since `pretty` prints to the terminal. Either specify a different format or don't pass `--quiet`.", + )); + } + if self .verify_opts .common_args @@ -105,6 +131,24 @@ impl ValidateArgs for StandaloneAutoharnessArgs { )); } + if self.common_autoharness_args.list + && !self.verify_opts.common_args.unstable_features.contains(UnstableFeature::List) + { + return Err(Error::raw( + ErrorKind::MissingRequiredArgument, + format!("The `list` feature is unstable and requires -Z {}", UnstableFeature::List), + )); + } + + if self.common_autoharness_args.format == Format::Pretty + && self.verify_opts.common_args.quiet + { + return Err(Error::raw( + ErrorKind::ArgumentConflict, + "The `--quiet` flag is not compatible with the `pretty` format, since `pretty` prints to the terminal. Either specify a different format or don't pass `--quiet`.", + )); + } + if self.std { validate_std_path(&self.input)?; } else if !self.input.is_file() { diff --git a/kani-driver/src/args/list_args.rs b/kani-driver/src/args/list_args.rs index 35d26f22eb36..1d84f5706812 100644 --- a/kani-driver/src/args/list_args.rs +++ b/kani-driver/src/args/list_args.rs @@ -64,6 +64,13 @@ impl ValidateArgs for CargoListArgs { )); } + if self.format == Format::Pretty && self.common_args.quiet { + return Err(Error::raw( + ErrorKind::ArgumentConflict, + "The `--quiet` flag is not compatible with the `pretty` format, since `pretty` prints to the terminal. Either specify a different format or don't pass `--quiet`.", + )); + } + Ok(()) } } @@ -78,6 +85,13 @@ impl ValidateArgs for StandaloneListArgs { )); } + if self.format == Format::Pretty && self.common_args.quiet { + return Err(Error::raw( + ErrorKind::ArgumentConflict, + "The `--quiet` flag is not compatible with the `pretty` format, since `pretty` prints to the terminal. Either specify a different format or don't pass `--quiet`.", + )); + } + if self.std { validate_std_path(&self.input) } else if self.input.is_file() { diff --git a/kani-driver/src/autoharness/mod.rs b/kani-driver/src/autoharness/mod.rs index 251a35570720..83162621dd1b 100644 --- a/kani-driver/src/autoharness/mod.rs +++ b/kani-driver/src/autoharness/mod.rs @@ -4,11 +4,15 @@ use std::str::FromStr; use crate::args::Timeout; -use crate::args::autoharness_args::{CargoAutoharnessArgs, StandaloneAutoharnessArgs}; +use crate::args::autoharness_args::{ + CargoAutoharnessArgs, CommonAutoharnessArgs, StandaloneAutoharnessArgs, +}; use crate::call_cbmc::VerificationStatus; use crate::call_single_file::to_rustc_arg; use crate::harness_runner::HarnessResult; -use crate::project::{standalone_project, std_project}; +use crate::list::collect_metadata::process_metadata; +use crate::list::output::output_list_results; +use crate::project::{Project, standalone_project, std_project}; use crate::session::KaniSession; use crate::{InvocationType, print_kani_version, project, verify_project}; use anyhow::Result; @@ -20,30 +24,18 @@ const LOOP_UNWIND_DEFAULT: u32 = 20; pub fn autoharness_cargo(args: CargoAutoharnessArgs) -> Result<()> { let mut session = KaniSession::new(args.verify_opts)?; - session.enable_autoharness(); - session.add_default_bounds(); - session.add_auto_harness_args( - args.common_autoharness_args.include_function, - args.common_autoharness_args.exclude_function, - ); + setup_session(&mut session, &args.common_autoharness_args); + if !session.args.common_args.quiet { print_kani_version(InvocationType::CargoKani(vec![])); } let project = project::cargo_project(&mut session, false)?; - if !session.args.common_args.quiet { - print_metadata(project.metadata.clone()); - } - if session.args.only_codegen { Ok(()) } else { verify_project(project, session) } + postprocess_project(project, session, args.common_autoharness_args) } pub fn autoharness_standalone(args: StandaloneAutoharnessArgs) -> Result<()> { let mut session = KaniSession::new(args.verify_opts)?; - session.enable_autoharness(); - session.add_default_bounds(); - session.add_auto_harness_args( - args.common_autoharness_args.include_function, - args.common_autoharness_args.exclude_function, - ); + setup_session(&mut session, &args.common_autoharness_args); if !session.args.common_args.quiet { print_kani_version(InvocationType::Standalone); @@ -55,14 +47,41 @@ pub fn autoharness_standalone(args: StandaloneAutoharnessArgs) -> Result<()> { standalone_project(&args.input, args.crate_name, &session)? }; + postprocess_project(project, session, args.common_autoharness_args) +} + +/// Execute autoharness-specific KaniSession configuration. +fn setup_session(session: &mut KaniSession, common_autoharness_args: &CommonAutoharnessArgs) { + session.enable_autoharness(); + session.add_default_bounds(); + session.add_auto_harness_args( + &common_autoharness_args.include_function, + &common_autoharness_args.exclude_function, + ); +} + +/// After generating the automatic harnesses, postprocess metadata and run verification. +fn postprocess_project( + project: Project, + session: KaniSession, + common_autoharness_args: CommonAutoharnessArgs, +) -> Result<()> { if !session.args.common_args.quiet { - print_metadata(project.metadata.clone()); + print_autoharness_metadata(project.metadata.clone()); + } + if common_autoharness_args.list { + let list_metadata = process_metadata(project.metadata.clone()); + return output_list_results( + list_metadata, + common_autoharness_args.format, + session.args.common_args.quiet, + ); } if session.args.only_codegen { Ok(()) } else { verify_project(project, session) } } /// Print automatic harness metadata to the terminal. -fn print_metadata(metadata: Vec) { +fn print_autoharness_metadata(metadata: Vec) { let mut chosen_table = PrettyTable::new(); chosen_table.set_header(vec!["Chosen Function"]); @@ -135,7 +154,7 @@ impl KaniSession { } /// Add the compiler arguments specific to the `autoharness` subcommand. - pub fn add_auto_harness_args(&mut self, included: Vec, excluded: Vec) { + pub fn add_auto_harness_args(&mut self, included: &[String], excluded: &[String]) { for func in included { self.pkg_args .push(to_rustc_arg(vec![format!("--autoharness-include-function {}", func)])); diff --git a/kani-driver/src/list/collect_metadata.rs b/kani-driver/src/list/collect_metadata.rs index 588cab0b63af..5a5ed290dcad 100644 --- a/kani-driver/src/list/collect_metadata.rs +++ b/kani-driver/src/list/collect_metadata.rs @@ -20,7 +20,7 @@ use anyhow::Result; use kani_metadata::{ContractedFunction, HarnessKind, KaniMetadata}; /// Process the KaniMetadata output from kani-compiler and output the list subcommand results -fn process_metadata(metadata: Vec) -> ListMetadata { +pub fn process_metadata(metadata: Vec) -> ListMetadata { // We use ordered maps and sets so that the output is in lexicographic order (and consistent across invocations). // Map each file to a vector of its harnesses. diff --git a/kani-driver/src/list/mod.rs b/kani-driver/src/list/mod.rs index 982c71d0120f..0a5aa523ea6a 100644 --- a/kani-driver/src/list/mod.rs +++ b/kani-driver/src/list/mod.rs @@ -6,9 +6,9 @@ use kani_metadata::ContractedFunction; use std::collections::{BTreeMap, BTreeSet}; pub mod collect_metadata; -mod output; +pub mod output; -struct ListMetadata { +pub struct ListMetadata { // Files mapped to their #[kani::proof] harnesses standard_harnesses: BTreeMap>, // Total number of #[kani::proof] harnesses diff --git a/tests/script-based-pre/cargo_autoharness_list/Cargo.toml b/tests/script-based-pre/cargo_autoharness_list/Cargo.toml new file mode 100644 index 000000000000..6c32a94cc3a3 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_list/Cargo.toml @@ -0,0 +1,10 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "cargo_autoharness_list" +version = "0.1.0" +edition = "2024" + +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } diff --git a/tests/script-based-pre/cargo_autoharness_list/config.yml b/tests/script-based-pre/cargo_autoharness_list/config.yml new file mode 100644 index 000000000000..4eac6f79588c --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_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_autoharness_list/list.expected b/tests/script-based-pre/cargo_autoharness_list/list.expected new file mode 100644 index 000000000000..bd20978a480e --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_list/list.expected @@ -0,0 +1,26 @@ +Kani generated automatic harnesses for 3 function(s): ++---------------------------+ +| Chosen Function | ++===========================+ +| f_u8 | +|---------------------------| +| has_recursion_gcd | +|---------------------------| +| verify::has_recursion_gcd | ++---------------------------+ + +Skipped Functions: None. Kani generated automatic harnesses for all functions in the available crate(s). + +Contracts: ++-------+---------------------------+-----------------------------------------------------------------------------+ +| | Function | Contract Harnesses (#[kani::proof_for_contract]) | ++=================================================================================================================+ +| | has_recursion_gcd | my_harness, my_harness_2, kani::internal::automatic_harness | +|-------+---------------------------+-----------------------------------------------------------------------------| +| | verify::has_recursion_gcd | verify::my_harness, verify::my_harness_2, kani::internal::automatic_harness | +|-------+---------------------------+-----------------------------------------------------------------------------| +| Total | 2 | 6 | ++-------+---------------------------+-----------------------------------------------------------------------------+ + +Standard Harnesses (#[kani::proof]): +1. f_u8 diff --git a/tests/script-based-pre/cargo_autoharness_list/list.sh b/tests/script-based-pre/cargo_autoharness_list/list.sh new file mode 100755 index 000000000000..7deb9a0667cc --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_list/list.sh @@ -0,0 +1,5 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +cargo kani autoharness -Z autoharness --list -Z list -Z function-contracts diff --git a/tests/script-based-pre/cargo_autoharness_list/src/lib.rs b/tests/script-based-pre/cargo_autoharness_list/src/lib.rs new file mode 100644 index 000000000000..47901cab8739 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_list/src/lib.rs @@ -0,0 +1,65 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Test that `kani autoharness --list` finds all of the manual and automatic harnesses +// and correctly matches them to their target function. +// Note that the proof_for_contract attributes use different, but equivalent, paths to their target functions; +// this tests that we can group the harnesses under the same target function even when the attribute value strings differ. + +fn f_u8(x: u8) -> u8 { + x +} + +#[kani::requires(x != 0 && y != 0)] +#[kani::ensures(|result : &u8| *result != 0 && x % *result == 0 && y % *result == 0)] +#[kani::recursion] +fn has_recursion_gcd(x: u8, y: u8) -> u8 { + let mut max = x; + let mut min = y; + if min > max { + let val = max; + max = min; + min = val; + } + + let res = max % min; + if res == 0 { min } else { has_recursion_gcd(min, res) } +} + +#[kani::proof_for_contract(crate::has_recursion_gcd)] +fn my_harness() { + has_recursion_gcd(kani::any(), kani::any()); +} + +#[kani::proof_for_contract(has_recursion_gcd)] +fn my_harness_2() { + has_recursion_gcd(kani::any(), kani::any()); +} + +mod verify { + #[kani::requires(x != 0 && y != 0)] + #[kani::ensures(|result : &u8| *result != 0 && x % *result == 0 && y % *result == 0)] + #[kani::recursion] + fn has_recursion_gcd(x: u8, y: u8) -> u8 { + let mut max = x; + let mut min = y; + if min > max { + let val = max; + max = min; + min = val; + } + + let res = max % min; + if res == 0 { min } else { has_recursion_gcd(min, res) } + } + + #[kani::proof_for_contract(crate::verify::has_recursion_gcd)] + fn my_harness() { + has_recursion_gcd(kani::any(), kani::any()); + } + + #[kani::proof_for_contract(has_recursion_gcd)] + fn my_harness_2() { + has_recursion_gcd(kani::any(), kani::any()); + } +}