From 16a9b37078521b391bad874e4a236ef5270a0b6d Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Sat, 1 Feb 2025 19:55:06 -0500 Subject: [PATCH 01/12] Automatic harness generation (standard harnesses only) --- kani-compiler/src/args.rs | 2 + .../codegen_aeneas_llbc/compiler_interface.rs | 2 +- .../compiler_interface.rs | 6 +- .../src/kani_middle/codegen_units.rs | 150 ++++++++++-- .../src/kani_middle/kani_functions.rs | 2 + kani-compiler/src/kani_middle/metadata.rs | 38 ++++ .../src/kani_middle/transform/automatic.rs | 129 +++++++++++ .../kani_middle/transform/kani_intrinsics.rs | 6 +- .../src/kani_middle/transform/mod.rs | 4 + kani-driver/src/args/autoverify_args.rs | 110 +++++++++ kani-driver/src/args/mod.rs | 8 + kani-driver/src/harness_runner.rs | 20 +- kani-driver/src/main.rs | 35 ++- kani-driver/src/session.rs | 17 +- kani_metadata/src/harness.rs | 2 + library/kani_core/src/lib.rs | 6 + .../Cargo.toml | 7 + .../config.yml | 4 + .../contracts.expected | 1 + .../contracts.sh | 5 + .../src/lib.rs | 16 ++ .../cargo_autoverify_filter/Cargo.toml | 7 + .../cargo_autoverify_filter/config.yml | 4 + .../cargo_autoverify_filter/filter.expected | 40 ++++ .../cargo_autoverify_filter/filter.sh | 5 + .../cargo_autoverify_filter/src/lib.rs | 213 ++++++++++++++++++ .../Cargo.toml | 7 + .../config.yml | 4 + .../harnesses_fail.expected | 47 ++++ .../harnesses_fail.sh | 9 + .../src/lib.rs | 57 +++++ .../cargo_autoverify_loops_fixme/Cargo.toml | 7 + .../cargo_autoverify_loops_fixme/config.yml | 4 + .../loops.expected | 1 + .../cargo_autoverify_loops_fixme/loops.sh | 5 + .../cargo_autoverify_loops_fixme/src/lib.rs | 28 +++ 36 files changed, 963 insertions(+), 45 deletions(-) create mode 100644 kani-compiler/src/kani_middle/transform/automatic.rs create mode 100644 kani-driver/src/args/autoverify_args.rs create mode 100644 tests/script-based-pre/cargo_autoverify_contracts_fixme/Cargo.toml create mode 100644 tests/script-based-pre/cargo_autoverify_contracts_fixme/config.yml create mode 100644 tests/script-based-pre/cargo_autoverify_contracts_fixme/contracts.expected create mode 100755 tests/script-based-pre/cargo_autoverify_contracts_fixme/contracts.sh create mode 100644 tests/script-based-pre/cargo_autoverify_contracts_fixme/src/lib.rs create mode 100644 tests/script-based-pre/cargo_autoverify_filter/Cargo.toml create mode 100644 tests/script-based-pre/cargo_autoverify_filter/config.yml create mode 100644 tests/script-based-pre/cargo_autoverify_filter/filter.expected create mode 100755 tests/script-based-pre/cargo_autoverify_filter/filter.sh create mode 100644 tests/script-based-pre/cargo_autoverify_filter/src/lib.rs create mode 100644 tests/script-based-pre/cargo_autoverify_harnesses_fail/Cargo.toml create mode 100644 tests/script-based-pre/cargo_autoverify_harnesses_fail/config.yml create mode 100644 tests/script-based-pre/cargo_autoverify_harnesses_fail/harnesses_fail.expected create mode 100755 tests/script-based-pre/cargo_autoverify_harnesses_fail/harnesses_fail.sh create mode 100644 tests/script-based-pre/cargo_autoverify_harnesses_fail/src/lib.rs create mode 100644 tests/script-based-pre/cargo_autoverify_loops_fixme/Cargo.toml create mode 100644 tests/script-based-pre/cargo_autoverify_loops_fixme/config.yml create mode 100644 tests/script-based-pre/cargo_autoverify_loops_fixme/loops.expected create mode 100755 tests/script-based-pre/cargo_autoverify_loops_fixme/loops.sh create mode 100644 tests/script-based-pre/cargo_autoverify_loops_fixme/src/lib.rs diff --git a/kani-compiler/src/args.rs b/kani-compiler/src/args.rs index 99254a08423a..9fe129dade03 100644 --- a/kani-compiler/src/args.rs +++ b/kani-compiler/src/args.rs @@ -30,6 +30,8 @@ pub enum ReachabilityType { PubFns, /// Start the cross-crate reachability analysis from all *test* (i.e. `#[test]`) harnesses in the local crate. Tests, + /// Start the cross-crate reachability analysis from all functions in the local crate that can be automatically verified. + Automatic, } /// Command line arguments that this instance of the compiler run was called diff --git a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs index e87bed0ea388..374d4a987682 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs @@ -253,7 +253,7 @@ impl CodegenBackend for LlbcCodegenBackend { units.store_modifies(&modifies_instances); units.write_metadata(&queries, tcx); } - ReachabilityType::Tests => todo!(), + ReachabilityType::Tests | ReachabilityType::Automatic => todo!(), ReachabilityType::None => {} ReachabilityType::PubFns => { let unit = CodegenUnit::default(); diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index a0ae5ae99eff..5192af2b1cea 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -264,7 +264,7 @@ impl CodegenBackend for GotocCodegenBackend { let reachability = queries.args().reachability_analysis; let mut results = GotoCodegenResults::new(tcx, reachability); match reachability { - ReachabilityType::Harnesses => { + ReachabilityType::Automatic | ReachabilityType::Harnesses => { let mut units = CodegenUnits::new(&queries, tcx); let mut modifies_instances = vec![]; let mut loop_contracts_instances = vec![]; @@ -375,7 +375,9 @@ impl CodegenBackend for GotocCodegenBackend { // Print compilation report. results.print_report(tcx); - if reachability != ReachabilityType::Harnesses { + if reachability != ReachabilityType::Harnesses + && reachability != ReachabilityType::Automatic + { // In a workspace, cargo seems to be using the same file prefix to build a crate that is // a package lib and also a dependency of another package. // To avoid overriding the metadata for its verification, we skip this step when diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 072528f9a765..725781f7b9c6 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -9,7 +9,10 @@ use crate::args::ReachabilityType; use crate::kani_middle::attributes::is_proof_harness; -use crate::kani_middle::metadata::{gen_contracts_metadata, gen_proof_metadata}; +use crate::kani_middle::kani_functions::{KaniIntrinsic, KaniModel}; +use crate::kani_middle::metadata::{ + gen_automatic_proof_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}; @@ -20,8 +23,8 @@ use rustc_middle::ty::TyCtxt; use rustc_session::config::OutputType; use rustc_smir::rustc_internal; use stable_mir::CrateDef; -use stable_mir::mir::mono::Instance; -use stable_mir::ty::{FnDef, IndexedVal, RigidTy, TyKind}; +use stable_mir::mir::{TerminatorKind, mono::Instance}; +use stable_mir::ty::{FnDef, GenericArgKind, GenericArgs, IndexedVal, RigidTy, TyKind}; use std::collections::{BTreeMap, BTreeSet, HashMap, HashSet}; use std::fs::File; use std::io::BufWriter; @@ -57,26 +60,42 @@ 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::>(); - - // 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 } + let base_filepath = tcx.output_filenames(()).path(OutputType::Object); + let base_filename = base_filepath.as_path(); + match queries.args().reachability_analysis { + ReachabilityType::Harnesses => { + let all_harnesses = get_all_manual_harnesses(tcx, base_filename); + // 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 } + } + ReachabilityType::Automatic => { + let mut all_harnesses = get_all_manual_harnesses(tcx, base_filename); + let kani_fns = queries.kani_functions(); + let any_inst = kani_fns.get(&KaniModel::Any.into()).unwrap(); + let verifiable_fns = filter_crate_items(tcx, |_, instance: Instance| -> bool { + is_eligible_for_automatic_harness(tcx, instance, *any_inst) + }); + let kani_harness_intrinsic = + kani_fns.get(&KaniIntrinsic::AutomaticHarness.into()).unwrap(); + let automatic_harnesses = get_all_automatic_harnesses( + tcx, + verifiable_fns, + *kani_harness_intrinsic, + base_filename, + ); + all_harnesses.extend(automatic_harnesses); + let units = group_by_stubs(tcx, &all_harnesses); + validate_units(tcx, &units); + debug!(?units, "CodegenUnits::new"); + CodegenUnits { units, harness_info: all_harnesses, crate_info } + } + _ => { + // Leave other reachability type handling as is for now. + CodegenUnits { units: vec![], harness_info: HashMap::default(), crate_info } + } } } @@ -252,3 +271,88 @@ fn apply_transitivity(tcx: TyCtxt, harness: Harness, stubs: Stubs) -> Stubs { } new_stubs } + +/// Fetch all manual harnesses (i.e., functions provided by the user) and generate their metadata +fn get_all_manual_harnesses( + tcx: TyCtxt, + base_filename: &Path, +) -> HashMap { + let harnesses = filter_crate_items(tcx, |_, instance| is_proof_harness(tcx, instance)); + harnesses + .into_iter() + .map(|harness| { + let metadata = gen_proof_metadata(tcx, harness, &base_filename); + (harness, metadata) + }) + .collect::>() +} + +/// For each function eligible for automatic verification, +/// generate a harness Instance for it, then generate its metadata. +/// Note that the body of each harness instance is still the dummy body of `kani_harness_intrinsic`; +/// the AutomaticHarnessPass will later transform the bodies of these instances to actually verify the function. +fn get_all_automatic_harnesses( + tcx: TyCtxt, + verifiable_fns: Vec, + kani_harness_intrinsic: FnDef, + base_filename: &Path, +) -> HashMap { + verifiable_fns + .into_iter() + .map(|fn_to_verify| { + // Set the generic arguments of the harness to be the function it is verifying + // so that later, in AutomaticHarnessPass, we can retrieve the function to verify + // and generate the harness body accordingly. + let harness = Instance::resolve( + kani_harness_intrinsic, + &GenericArgs(vec![GenericArgKind::Type(fn_to_verify.ty())]), + ) + .unwrap(); + let metadata = gen_automatic_proof_metadata(tcx, &base_filename, &fn_to_verify); + (harness, metadata) + }) + .collect::>() +} + +/// Determine whether `instance` is eligible for automatic verification. +/// `instance` is eligible iff: +/// 1. It is not a harness, +/// 2. It has a non-empty body, +/// 3. It is not an associated item of a Kani trait implementation (e.g., a kani::any implementation) +/// 4. All of its arguments implement Arbitrary +fn is_eligible_for_automatic_harness(tcx: TyCtxt, instance: Instance, any_inst: FnDef) -> bool { + if is_proof_harness(tcx, instance) || !instance.has_body() { + return false; + } + // Don't generate a harness for functions with empty bodies. + let body = instance.body().unwrap(); + if body.blocks.is_empty() + || (body.blocks[0].statements.is_empty() + && matches!(body.blocks[0].terminator.kind, TerminatorKind::Return)) + { + return false; + } + + // Don't generate harnesses for associated items of Kani trait implementations. + // FIXME -- find a less hardcoded way of doing this (perhaps upstream PR to StableMIR). + if instance.name().contains("kani::Arbitrary") || instance.name().contains("kani::Invariant") { + return false; + } + + // Each non-generic argument of instance must implement Arbitrary. + // FIXME -- this will only find Arbitrary implementations for types whose Arbitrary + // implementations have an inner call to kani::any, which not all implementations (e.g. PhantomPinned) do. + body.arg_locals().iter().all(|arg| { + let kani_any_body = + Instance::resolve(any_inst, &GenericArgs(vec![GenericArgKind::Type(arg.ty)])) + .unwrap() + .body() + .unwrap(); + if let TerminatorKind::Call { func, .. } = &kani_any_body.blocks[0].terminator.kind { + if let Some((def, args)) = func.ty(body.arg_locals()).unwrap().kind().fn_def() { + return Instance::resolve(def, &args).is_ok(); + } + } + false + }) +} diff --git a/kani-compiler/src/kani_middle/kani_functions.rs b/kani-compiler/src/kani_middle/kani_functions.rs index 8d1ab5ef939d..3182ced8fa61 100644 --- a/kani-compiler/src/kani_middle/kani_functions.rs +++ b/kani-compiler/src/kani_middle/kani_functions.rs @@ -48,6 +48,8 @@ pub enum KaniIntrinsic { CheckedAlignOf, #[strum(serialize = "CheckedSizeOfIntrinsic")] CheckedSizeOf, + #[strum(serialize = "AutomaticHarnessIntrinsic")] + AutomaticHarness, #[strum(serialize = "IsInitializedIntrinsic")] IsInitialized, #[strum(serialize = "ValidValueIntrinsic")] diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs index 67d32b0079c4..d85d02c75d49 100644 --- a/kani-compiler/src/kani_middle/metadata.rs +++ b/kani-compiler/src/kani_middle/metadata.rs @@ -39,6 +39,7 @@ pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) -> goto_file: Some(model_file), contract: Default::default(), has_loop_contracts: false, + is_automatically_generated: false, } } @@ -84,6 +85,42 @@ pub fn gen_contracts_metadata(tcx: TyCtxt) -> Vec { fn_to_data.into_values().collect() } +/// Generate metadata for automatically generated harnesses. +/// For now, we just use the data from the function we are verifying; since we only generate one automatic harness per function, +/// the metdata from that function uniquely identifies the harness. +/// In future iterations of this feature, we will likely have multiple harnesses for a single function (e.g., for generic functions), +/// in which case HarnessMetadata will need to change further to differentiate between those harnesses. +/// TODO Instead of just generating HarnessKind::Proof, generate HarnessKind::ProofForContract if fn_to_verify has a contract. +pub fn gen_automatic_proof_metadata( + _tcx: TyCtxt, + base_name: &Path, + fn_to_verify: &Instance, +) -> HarnessMetadata { + let def = fn_to_verify.def; + let pretty_name = fn_to_verify.name(); + let mangled_name = fn_to_verify.mangled_name(); + + // Leave the concrete playback instrumentation for now, but this feature does not actually support concrete playback. + let loc = SourceLocation::new(fn_to_verify.body().unwrap().span); + let file_stem = format!("{}_{mangled_name}", base_name.file_stem().unwrap().to_str().unwrap()); + let model_file = base_name.with_file_name(file_stem).with_extension(ArtifactType::SymTabGoto); + + HarnessMetadata { + pretty_name, + mangled_name, + crate_name: def.krate().name, + original_file: loc.filename, + original_start_line: loc.start_line, + original_end_line: loc.end_line, + attributes: HarnessAttributes::new(HarnessKind::Proof), + // TODO: This no longer needs to be an Option. + goto_file: Some(model_file), + contract: Default::default(), + has_loop_contracts: false, + is_automatically_generated: true, + } +} + /// Create the harness metadata for a test description. #[allow(dead_code)] pub fn gen_test_metadata( @@ -110,5 +147,6 @@ pub fn gen_test_metadata( goto_file: Some(model_file), contract: Default::default(), has_loop_contracts: false, + is_automatically_generated: false, } } diff --git a/kani-compiler/src/kani_middle/transform/automatic.rs b/kani-compiler/src/kani_middle/transform/automatic.rs new file mode 100644 index 000000000000..2549648045f2 --- /dev/null +++ b/kani-compiler/src/kani_middle/transform/automatic.rs @@ -0,0 +1,129 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This module transforms the body of an automatic harness to verify a function. +//! Upon entry to this module, a harness has the dummy body of the automatic_harness Kani intrinsic. +//! We obtain the function its meant to verify by inspecting its generic arguments, +//! then transform its body to be a harness for that function. + +use crate::args::ReachabilityType; +use crate::kani_middle::codegen_units::CodegenUnit; +use crate::kani_middle::kani_functions::{KaniIntrinsic, KaniModel}; +use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceInstruction}; +use crate::kani_middle::transform::{TransformPass, TransformationType}; +use crate::kani_queries::QueryDb; +use rustc_middle::ty::TyCtxt; +use stable_mir::mir::mono::Instance; +use stable_mir::mir::{Body, Operand, Place, TerminatorKind}; +use stable_mir::ty::{FnDef, GenericArgKind, GenericArgs}; +use tracing::debug; + +#[derive(Debug)] +pub struct AutomaticHarnessPass { + /// The FnDef of KaniModel::Any + kani_any: FnDef, + /// All of the automatic harness Instances that we generated in the CodegenUnits constructor + automatic_harnesses: Vec, +} + +impl AutomaticHarnessPass { + // FIXME: this is a bit clunky. + // Historically, in codegen_crate, we reset the BodyTransformation cache on a per-unit basis, + // so the BodyTransformation constructor only accepts a CodegenUnit and thus this constructor can only accept a unit. + // Later, we changed codegen to reset the cache on a per-harness basis (for uninitialized memory instrumentation). + // So BodyTransformation should really be changed to reflect that, so that this constructor can just save the one automatic harness it should transform + // and not all of the possibilities. + pub fn new(unit: &CodegenUnit, query_db: &QueryDb) -> Self { + let kani_fns = query_db.kani_functions(); + let harness_intrinsic = *kani_fns.get(&KaniIntrinsic::AutomaticHarness.into()).unwrap(); + let kani_any = *kani_fns.get(&KaniModel::Any.into()).unwrap(); + let automatic_harnesses = unit + .harnesses + .iter() + .cloned() + .filter(|harness| { + let (def, _) = harness.ty().kind().fn_def().unwrap(); + def == harness_intrinsic + }) + .collect::>(); + Self { kani_any, automatic_harnesses } + } +} + +impl TransformPass for AutomaticHarnessPass { + fn transformation_type() -> TransformationType + where + Self: Sized, + { + TransformationType::Stubbing + } + + fn is_enabled(&self, query_db: &QueryDb) -> bool + where + Self: Sized, + { + matches!(query_db.args().reachability_analysis, ReachabilityType::Automatic) + } + + fn transform(&mut self, _tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) { + debug!(function=?instance.name(), "AutomaticHarnessPass::transform"); + + if !self.automatic_harnesses.contains(&instance) { + return (false, body); + } + + // Retrieve the generic arguments of the harness, which is the type of the function it is verifying, + // and then resolve `fn_to_verify`. + let kind = instance.args().0[0].expect_ty().kind(); + let (def, args) = kind.fn_def().unwrap(); + let fn_to_verify = Instance::resolve(def, &args).unwrap(); + let fn_to_verify_body = fn_to_verify.body().unwrap(); + + let mut harness_body = MutableBody::from(body); + harness_body.clear_body(TerminatorKind::Return); + let mut source = SourceInstruction::Terminator { bb: 0 }; + + let mut arg_locals = vec![]; + + // For each argument of `fn_to_verify`, create a nondeterministic value of its type + // by generating a kani::any() call and saving the result in `arg_local`. + for local_decl in fn_to_verify_body.arg_locals().iter() { + let arg_local = harness_body.new_local( + local_decl.ty, + source.span(harness_body.blocks()), + local_decl.mutability, + ); + let kani_any_inst = Instance::resolve( + self.kani_any, + &GenericArgs(vec![GenericArgKind::Type(local_decl.ty)]), + ) + .unwrap(); + harness_body.insert_call( + &kani_any_inst, + &mut source, + InsertPosition::Before, + vec![], + Place::from(arg_local), + ); + arg_locals.push(arg_local); + } + + let func_to_verify_ret = fn_to_verify_body.ret_local(); + let ret_place = Place::from(harness_body.new_local( + func_to_verify_ret.ty, + source.span(harness_body.blocks()), + func_to_verify_ret.mutability, + )); + + // Call `fn_to_verify` on the nondeterministic arguments generated above. + harness_body.insert_call( + &fn_to_verify, + &mut source, + InsertPosition::Before, + arg_locals.iter().map(|lcl| Operand::Copy(Place::from(*lcl))).collect::>(), + ret_place, + ); + + (true, harness_body.into()) + } +} diff --git a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs index 206c0160a80d..d18b4b059063 100644 --- a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs @@ -74,8 +74,10 @@ impl TransformPass for IntrinsicGeneratorPass { KaniIntrinsic::CheckedSizeOf => (true, self.checked_size_of(body, instance)), KaniIntrinsic::IsInitialized => (true, self.is_initialized_body(body)), KaniIntrinsic::ValidValue => (true, self.valid_value_body(body)), - // This is handled in contracts pass for now. - KaniIntrinsic::WriteAny | KaniIntrinsic::AnyModifies => (false, body), + // The former two are handled in contracts pass for now, while the latter is handled in the the automatic harness pass. + KaniIntrinsic::WriteAny + | KaniIntrinsic::AnyModifies + | KaniIntrinsic::AutomaticHarness => (false, body), } } else { (false, body) diff --git a/kani-compiler/src/kani_middle/transform/mod.rs b/kani-compiler/src/kani_middle/transform/mod.rs index 8001b1f1d359..49e36461081c 100644 --- a/kani-compiler/src/kani_middle/transform/mod.rs +++ b/kani-compiler/src/kani_middle/transform/mod.rs @@ -26,6 +26,7 @@ use crate::kani_middle::transform::kani_intrinsics::IntrinsicGeneratorPass; use crate::kani_middle::transform::loop_contracts::LoopContractPass; use crate::kani_middle::transform::stubs::{ExternFnStubPass, FnStubPass}; use crate::kani_queries::QueryDb; +use automatic::AutomaticHarnessPass; use dump_mir_pass::DumpMirPass; use rustc_middle::ty::TyCtxt; use stable_mir::mir::Body; @@ -36,6 +37,7 @@ use std::fmt::Debug; use crate::kani_middle::transform::rustc_intrinsics::RustcIntrinsicsPass; pub use internal_mir::RustcInternalMir; +mod automatic; pub(crate) mod body; mod check_uninit; mod check_values; @@ -71,6 +73,8 @@ impl BodyTransformation { cache: Default::default(), }; let check_type = CheckType::new_assert_assume(queries); + // This has to come first, since creating harnesses affects later stubbing and contract passes. + transformer.add_pass(queries, AutomaticHarnessPass::new(unit, queries)); transformer.add_pass(queries, FnStubPass::new(&unit.stubs)); transformer.add_pass(queries, ExternFnStubPass::new(&unit.stubs)); transformer.add_pass(queries, FunctionWithContractPass::new(tcx, queries, &unit)); diff --git a/kani-driver/src/args/autoverify_args.rs b/kani-driver/src/args/autoverify_args.rs new file mode 100644 index 000000000000..c8f961643e40 --- /dev/null +++ b/kani-driver/src/args/autoverify_args.rs @@ -0,0 +1,110 @@ +// 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, VerificationArgs}; +use clap::{Error, Parser, error::ErrorKind}; +use kani_metadata::UnstableFeature; + +// TODO add --function option to only verify functions matching the substring +// (akin to --harness). + +/// Automatically verify functions in a crate. +#[derive(Debug, Parser)] +pub struct CargoAutoverifyArgs { + #[command(flatten)] + pub verify_opts: VerificationArgs, +} + +/// Automatically verify functions in a file. +#[derive(Debug, Parser)] +pub struct StandaloneAutoverifyArgs { + /// Rust crate's top file location. + #[arg(required = true)] + pub input: PathBuf, + + #[arg(long, hide = true)] + pub crate_name: Option, + + #[command(flatten)] + pub verify_opts: VerificationArgs, +} + +impl ValidateArgs for CargoAutoverifyArgs { + fn validate(&self) -> Result<(), Error> { + self.verify_opts.validate()?; + if !self + .verify_opts + .common_args + .unstable_features + .contains(UnstableFeature::UnstableOptions) + { + return Err(Error::raw( + ErrorKind::MissingRequiredArgument, + format!( + "The `autoverify` subcommand is unstable and requires -Z {}", + UnstableFeature::UnstableOptions.to_string() + ), + )); + } + + if self + .verify_opts + .common_args + .unstable_features + .contains(UnstableFeature::ConcretePlayback) + { + return Err(Error::raw( + ErrorKind::ArgumentConflict, + "The autoverify subcommand does not support concrete playback", + )); + } + + Ok(()) + } +} + +impl ValidateArgs for StandaloneAutoverifyArgs { + fn validate(&self) -> Result<(), Error> { + self.verify_opts.validate()?; + if !self + .verify_opts + .common_args + .unstable_features + .contains(UnstableFeature::UnstableOptions) + { + return Err(Error::raw( + ErrorKind::MissingRequiredArgument, + format!( + "The `autoverify` subcommand is unstable and requires -Z {}", + UnstableFeature::UnstableOptions.to_string() + ), + )); + } + if !self.input.is_file() { + return Err(Error::raw( + ErrorKind::InvalidValue, + format!( + "Invalid argument: Input invalid. `{}` is not a regular file.", + self.input.display() + ), + )); + } + + if self + .verify_opts + .common_args + .unstable_features + .contains(UnstableFeature::ConcretePlayback) + { + return Err(Error::raw( + ErrorKind::ArgumentConflict, + "The autoverify subcommand does not support concrete playback", + )); + } + + Ok(()) + } +} diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 9ba06826d200..c3a096b78665 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -3,6 +3,7 @@ //! Module that define Kani's command line interface. This includes all subcommands. pub mod assess_args; +pub mod autoverify_args; pub mod cargo; pub mod common; pub mod list_args; @@ -145,6 +146,8 @@ pub enum StandaloneSubcommand { VerifyStd(Box), /// List contracts and harnesses. List(Box), + /// Scan the input file for functions eligible for automatic (i.e., harness-free) verification and verify them. + Autoverify(Box), } #[derive(Debug, clap::Parser)] @@ -173,6 +176,9 @@ pub enum CargoKaniSubcommand { /// List contracts and harnesses. List(Box), + + /// Scan the crate for functions eligible for automatic (i.e., harness-free) verification and verify them. + Autoverify(Box), } // Common arguments for invoking Kani for verification purpose. This gets put into KaniContext, @@ -483,6 +489,7 @@ impl ValidateArgs for StandaloneArgs { match &self.command { Some(StandaloneSubcommand::VerifyStd(args)) => args.validate()?, Some(StandaloneSubcommand::List(args)) => args.validate()?, + Some(StandaloneSubcommand::Autoverify(args)) => args.validate()?, // TODO: Invoke PlaybackArgs::validate() None | Some(StandaloneSubcommand::Playback(..)) => {} }; @@ -528,6 +535,7 @@ impl ValidateArgs for CargoKaniSubcommand { match self { // Assess doesn't implement validation yet. CargoKaniSubcommand::Assess(_) => Ok(()), + CargoKaniSubcommand::Autoverify(autoverify) => autoverify.validate(), CargoKaniSubcommand::Playback(playback) => playback.validate(), CargoKaniSubcommand::List(list) => list.validate(), } diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index b78e1dc9d80b..320d574a01f8 100644 --- a/kani-driver/src/harness_runner.rs +++ b/kani-driver/src/harness_runner.rs @@ -167,14 +167,22 @@ impl KaniSession { harness: &HarnessMetadata, ) -> Result { let thread_index = rayon::current_thread_index().unwrap_or_default(); - if !self.args.common_args.quiet { - if rayon::current_num_threads() > 1 { - println!("Thread {thread_index}: Checking harness {}...", harness.pretty_name); - } else { - println!("Checking harness {}...", harness.pretty_name); - } + // If the harness is automatically generated, pretty_name refers to the function under verification. + let mut msg = if harness.is_automatically_generated { + format!( + "Automatic verification: Checking function {} against all possible inputs...", + harness.pretty_name + ) + } else { + format!("Checking harness {}...", harness.pretty_name) + }; + + if rayon::current_num_threads() > 1 { + msg = format!("Thread {thread_index}: {msg}"); } + println!("{msg}"); + let mut result = self.with_timer(|| self.run_cbmc(binary, harness), "run_cbmc")?; self.process_output(&result, harness, thread_index); diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index 07405a30a307..2282a2bdb342 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -72,21 +72,25 @@ fn cargokani_main(input_args: Vec) -> Result<()> { return list_cargo(*list_args, args.verify_opts); } - let session = session::KaniSession::new(args.verify_opts)?; - - if !session.args.common_args.quiet { - print_kani_version(InvocationType::CargoKani(input_args)); - } - - match args.command { - Some(CargoKaniSubcommand::Assess(args)) => { - return assess::run_assess(session, *args); + let session = match args.command { + Some(CargoKaniSubcommand::Assess(assess_args)) => { + let sess = session::KaniSession::new(args.verify_opts)?; + return assess::run_assess(sess, *assess_args); + } + Some(CargoKaniSubcommand::Autoverify(args)) => { + let mut sess = session::KaniSession::new(args.verify_opts)?; + sess.enable_autoverify(); + sess } Some(CargoKaniSubcommand::Playback(args)) => { return playback_cargo(*args); } Some(CargoKaniSubcommand::List(_)) => unreachable!(), - None => {} + None => session::KaniSession::new(args.verify_opts)?, + }; + + if !session.args.common_args.quiet { + print_kani_version(InvocationType::CargoKani(input_args)); } if session.args.assess { @@ -103,6 +107,17 @@ fn standalone_main() -> Result<()> { check_is_valid(&args); let (session, project) = match args.command { + Some(StandaloneSubcommand::Autoverify(args)) => { + let mut session = KaniSession::new(args.verify_opts)?; + session.enable_autoverify(); + + if !session.args.common_args.quiet { + print_kani_version(InvocationType::Standalone); + } + + let project = project::standalone_project(&args.input, args.crate_name, &session)?; + (session, project) + } Some(StandaloneSubcommand::Playback(args)) => return playback_standalone(*args), Some(StandaloneSubcommand::List(list_args)) => { return list_standalone(*list_args, args.verify_opts); diff --git a/kani-driver/src/session.rs b/kani-driver/src/session.rs index 187a17ae6981..db2a98358e45 100644 --- a/kani-driver/src/session.rs +++ b/kani-driver/src/session.rs @@ -28,6 +28,9 @@ pub struct KaniSession { /// The common command-line arguments pub args: VerificationArgs, + /// Automatically verify functions in the crate, in addition to running manual harnesses. + pub auto_verify: bool, + /// Include all publicly-visible symbols in the generated goto binary, not just those reachable from /// a proof harness. Useful when attempting to verify things that were not annotated with kani /// proof attributes. @@ -62,6 +65,7 @@ impl KaniSession { Ok(KaniSession { args, + auto_verify: false, codegen_tests: false, kani_compiler: install.kani_compiler()?, kani_lib_c: install.kani_lib_c()?, @@ -70,6 +74,10 @@ impl KaniSession { }) } + pub fn enable_autoverify(&mut self) { + self.auto_verify = true; + } + /// Record a temporary file so we can cleanup after ourselves at the end. /// Note that there will be no failure if the file does not exist. pub fn record_temporary_file>(&self, temp: &T) { @@ -88,13 +96,20 @@ impl KaniSession { /// Determine which symbols Kani should codegen (i.e. by slicing away symbols /// that are considered unreachable.) pub fn reachability_mode(&self) -> ReachabilityMode { - if self.codegen_tests { ReachabilityMode::Tests } else { ReachabilityMode::ProofHarnesses } + if self.codegen_tests { + ReachabilityMode::Tests + } else if self.auto_verify { + ReachabilityMode::Automatic + } else { + ReachabilityMode::ProofHarnesses + } } } #[derive(Debug, Copy, Clone, Display)] #[strum(serialize_all = "snake_case")] pub enum ReachabilityMode { + Automatic, #[strum(to_string = "harnesses")] ProofHarnesses, Tests, diff --git a/kani_metadata/src/harness.rs b/kani_metadata/src/harness.rs index 6932b15dc1a7..227fe8df09d4 100644 --- a/kani_metadata/src/harness.rs +++ b/kani_metadata/src/harness.rs @@ -38,6 +38,8 @@ pub struct HarnessMetadata { pub contract: Option, /// If the harness contains some usage of loop contracts. pub has_loop_contracts: bool, + /// If the harness was automatically generated or manually written. + pub is_automatically_generated: bool, } /// The attributes added by the user to control how a harness is executed. diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index 37a05821bd33..d3940160a91a 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -434,6 +434,12 @@ macro_rules! kani_intrinsics { } } + /// Used to hold the bodies of automatically generated harnesses. + #[kanitool::fn_marker = "AutomaticHarnessIntrinsic"] + pub fn automatic_harness() { + super::kani_intrinsic() + } + /// A way to break the ownerhip rules. Only used by contracts where we can /// guarantee it is done safely. #[inline(never)] diff --git a/tests/script-based-pre/cargo_autoverify_contracts_fixme/Cargo.toml b/tests/script-based-pre/cargo_autoverify_contracts_fixme/Cargo.toml new file mode 100644 index 000000000000..e04125cb6690 --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_contracts_fixme/Cargo.toml @@ -0,0 +1,7 @@ +[package] +name = "cargo_autoverify_contracts_fixme" +version = "0.1.0" +edition = "2024" + +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } diff --git a/tests/script-based-pre/cargo_autoverify_contracts_fixme/config.yml b/tests/script-based-pre/cargo_autoverify_contracts_fixme/config.yml new file mode 100644 index 000000000000..38bf8ee6c38c --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_contracts_fixme/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: contracts.sh +expected: contracts.expected diff --git a/tests/script-based-pre/cargo_autoverify_contracts_fixme/contracts.expected b/tests/script-based-pre/cargo_autoverify_contracts_fixme/contracts.expected new file mode 100644 index 000000000000..8f357ebd103d --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_contracts_fixme/contracts.expected @@ -0,0 +1 @@ +TODO write me \ No newline at end of file diff --git a/tests/script-based-pre/cargo_autoverify_contracts_fixme/contracts.sh b/tests/script-based-pre/cargo_autoverify_contracts_fixme/contracts.sh new file mode 100755 index 000000000000..c5bdc2bfa0ac --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_contracts_fixme/contracts.sh @@ -0,0 +1,5 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +cargo kani autoverify -Z unstable-options diff --git a/tests/script-based-pre/cargo_autoverify_contracts_fixme/src/lib.rs b/tests/script-based-pre/cargo_autoverify_contracts_fixme/src/lib.rs new file mode 100644 index 000000000000..7a8aa8e84f69 --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_contracts_fixme/src/lib.rs @@ -0,0 +1,16 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zautomatic-harnesses -Zfunction-contracts + +// The automatic harnesses feature will only generate standard harnesses (#[kani::proof]) +// for each function, even if it has a contract. +// That standard harness will ignore the function's contract, +// causing verification failure in this case (division by zero). +// Instead, we should detect the presence of contracts and generate a contract harness. + +#[kani::requires(divisor != 0)] +fn div(dividend: u32, divisor: u32) -> u32 { + dividend / divisor +} + +// TODO add more tests, including test(s) for unsafe functions. diff --git a/tests/script-based-pre/cargo_autoverify_filter/Cargo.toml b/tests/script-based-pre/cargo_autoverify_filter/Cargo.toml new file mode 100644 index 000000000000..db41718a0ec0 --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_filter/Cargo.toml @@ -0,0 +1,7 @@ +[package] +name = "cargo_autoverify_filter" +version = "0.1.0" +edition = "2024" + +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } diff --git a/tests/script-based-pre/cargo_autoverify_filter/config.yml b/tests/script-based-pre/cargo_autoverify_filter/config.yml new file mode 100644 index 000000000000..90ee1970e96c --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_filter/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: filter.sh +expected: filter.expected diff --git a/tests/script-based-pre/cargo_autoverify_filter/filter.expected b/tests/script-based-pre/cargo_autoverify_filter/filter.expected new file mode 100644 index 000000000000..e960e9180e91 --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_filter/filter.expected @@ -0,0 +1,40 @@ +Automatic verification: Checking function yes_harness::f_tuple against all possible inputs... +Automatic verification: Checking function yes_harness::f_maybe_uninit against all possible inputs... +Automatic verification: Checking function yes_harness::f_result against all possible inputs... +Automatic verification: Checking function yes_harness::f_option against all possible inputs... +Automatic verification: Checking function yes_harness::f_array against all possible inputs... +Automatic verification: Checking function yes_harness::f_nonzero_isize against all possible inputs... +Automatic verification: Checking function yes_harness::f_nonzero_i128 against all possible inputs... +Automatic verification: Checking function yes_harness::f_nonzero_i64 against all possible inputs... +Automatic verification: Checking function yes_harness::f_nonzero_i32 against all possible inputs... +Automatic verification: Checking function yes_harness::f_nonzero_i16 against all possible inputs... +Automatic verification: Checking function yes_harness::f_nonzero_i8 against all possible inputs... +Automatic verification: Checking function yes_harness::f_nonzero_usize against all possible inputs... +Automatic verification: Checking function yes_harness::f_nonzero_u128 against all possible inputs... +Automatic verification: Checking function yes_harness::f_nonzero_u64 against all possible inputs... +Automatic verification: Checking function yes_harness::f_nonzero_u32 against all possible inputs... +Automatic verification: Checking function yes_harness::f_nonzero_u16 against all possible inputs... +Automatic verification: Checking function yes_harness::f_nonzero_u8 against all possible inputs... +Automatic verification: Checking function yes_harness::f_f128 against all possible inputs... +Automatic verification: Checking function yes_harness::f_f16 against all possible inputs... +Automatic verification: Checking function yes_harness::f_f64 against all possible inputs... +Automatic verification: Checking function yes_harness::f_f32 against all possible inputs... +Automatic verification: Checking function yes_harness::f_char against all possible inputs... +Automatic verification: Checking function yes_harness::f_bool against all possible inputs... +Automatic verification: Checking function yes_harness::f_isize against all possible inputs... +Automatic verification: Checking function yes_harness::f_i128 against all possible inputs... +Automatic verification: Checking function yes_harness::f_i64 against all possible inputs... +Automatic verification: Checking function yes_harness::f_i32 against all possible inputs... +Automatic verification: Checking function yes_harness::f_i16 against all possible inputs... +Automatic verification: Checking function yes_harness::f_i8 against all possible inputs... +Automatic verification: Checking function yes_harness::f_usize against all possible inputs... +Automatic verification: Checking function yes_harness::f_u128 against all possible inputs... +Automatic verification: Checking function yes_harness::f_u64 against all possible inputs... +Automatic verification: Checking function yes_harness::f_u32 against all possible inputs... +Automatic verification: Checking function yes_harness::f_u16 against all possible inputs... +Automatic verification: Checking function yes_harness::f_u8 against all possible inputs... +Automatic verification: Checking function yes_harness::f_unsupported_return_type against all possible inputs... +Automatic verification: Checking function yes_harness::f_multiple_args against all possible inputs... +Automatic verification: Checking function yes_harness::f_derives_arbitrary against all possible inputs... +Automatic verification: Checking function yes_harness::f_manually_implements_arbitrary against all possible inputs... +Complete - 39 successfully verified harnesses, 0 failures, 39 total. \ No newline at end of file diff --git a/tests/script-based-pre/cargo_autoverify_filter/filter.sh b/tests/script-based-pre/cargo_autoverify_filter/filter.sh new file mode 100755 index 000000000000..c5bdc2bfa0ac --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_filter/filter.sh @@ -0,0 +1,5 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +cargo kani autoverify -Z unstable-options diff --git a/tests/script-based-pre/cargo_autoverify_filter/src/lib.rs b/tests/script-based-pre/cargo_autoverify_filter/src/lib.rs new file mode 100644 index 000000000000..14b77eb88e9f --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_filter/src/lib.rs @@ -0,0 +1,213 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Test that the automatic harness generation feature filters functions correctly, +// i.e., that it generates harnesses for a function iff: +// - It is not itself a harness +// - All of its arguments implement Arbitrary, either trivially or through a user-provided implementation +// The bodies of these functions are purposefully left as simple as possible; +// the point is not to test the generated harnesses themselves, +// but only that we generate the harnesses in the first place. + +#![feature(f16)] +#![feature(f128)] + +extern crate kani; +use kani::Arbitrary; + +#[derive(Arbitrary)] +struct DerivesArbitrary { + x: u8, + y: u32, +} + +struct ManuallyImplementsArbitrary { + x: u8, + y: u32, +} + +impl Arbitrary for ManuallyImplementsArbitrary { + fn any() -> Self { + Self { x: kani::any(), y: kani::any() } + } +} + +struct DoesntImplementArbitrary { + x: u8, + y: u32, +} + +mod yes_harness { + use crate::{DerivesArbitrary, ManuallyImplementsArbitrary}; + use std::mem::MaybeUninit; + use std::num::NonZero; + + // Kani-provided Arbitrary implementations + fn f_u8(x: u8) -> u8 { + x + } + fn f_u16(x: u16) -> u16 { + x + } + fn f_u32(x: u32) -> u32 { + x + } + fn f_u64(x: u64) -> u64 { + x + } + fn f_u128(x: u128) -> u128 { + x + } + fn f_usize(x: usize) -> usize { + x + } + fn f_i8(x: i8) -> i8 { + x + } + fn f_i16(x: i16) -> i16 { + x + } + fn f_i32(x: i32) -> i32 { + x + } + fn f_i64(x: i64) -> i64 { + x + } + fn f_i128(x: i128) -> i128 { + x + } + fn f_isize(x: isize) -> isize { + x + } + fn f_bool(x: bool) -> bool { + x + } + fn f_char(x: char) -> char { + x + } + fn f_f32(x: f32) -> f32 { + x + } + fn f_f64(x: f64) -> f64 { + x + } + fn f_f16(x: f16) -> f16 { + x + } + fn f_f128(x: f128) -> f128 { + x + } + fn f_nonzero_u8(x: NonZero) -> NonZero { + x + } + fn f_nonzero_u16(x: NonZero) -> NonZero { + x + } + fn f_nonzero_u32(x: NonZero) -> NonZero { + x + } + fn f_nonzero_u64(x: NonZero) -> NonZero { + x + } + fn f_nonzero_u128(x: NonZero) -> NonZero { + x + } + fn f_nonzero_usize(x: NonZero) -> NonZero { + x + } + fn f_nonzero_i8(x: NonZero) -> NonZero { + x + } + fn f_nonzero_i16(x: NonZero) -> NonZero { + x + } + fn f_nonzero_i32(x: NonZero) -> NonZero { + x + } + fn f_nonzero_i64(x: NonZero) -> NonZero { + x + } + fn f_nonzero_i128(x: NonZero) -> NonZero { + x + } + fn f_nonzero_isize(x: NonZero) -> NonZero { + x + } + fn f_array(x: [u8; 4]) -> [u8; 4] { + x + } + fn f_option(x: Option) -> Option { + x + } + fn f_result(x: Result) -> Result { + x + } + fn f_maybe_uninit(x: MaybeUninit) -> MaybeUninit { + x + } + fn f_tuple(x: (u8, u16, u32)) -> (u8, u16, u32) { + x + } + + // The return type doesn't implement Arbitrary, but that shouldn't matter + fn f_unsupported_return_type(x: u8) -> Vec { + vec![x] + } + + // Multiple arguments of different types, all of which implement Arbitrary + fn f_multiple_args(x: u8, y: u16, z: u32) -> (u8, u16, u32) { + (x, y, z) + } + + // User-defined types that implement Arbitrary + fn f_derives_arbitrary(x: DerivesArbitrary) -> DerivesArbitrary { + x + } + fn f_manually_implements_arbitrary( + x: ManuallyImplementsArbitrary, + ) -> ManuallyImplementsArbitrary { + x + } +} + +// These should have harnesses, but do not because we assume that every Arbitrary implementation +// will have an internal call to kani::Arbitrary::any, which these implementations do not. +mod fixme { + use std::marker::{PhantomData, PhantomPinned}; + fn f_phantom_data(x: PhantomData) -> PhantomData { + x + } + fn f_phantom_pinned(x: PhantomPinned) -> PhantomPinned { + x + } +} + +mod no_harness { + use crate::{DerivesArbitrary, DoesntImplementArbitrary}; + + fn empty_body(_x: u8, _y: u16) {} + fn unsupported_generic(x: u32, _y: T) -> u32 { + x + } + fn unsupported_ref(x: u32, _y: &i32) -> u32 { + x + } + fn unsupported_const_pointer(x: u32, _y: *const i32) -> u32 { + x + } + fn unsupported_mut_pointer(x: u32, _y: *mut i32) -> u32 { + x + } + fn unsupported_vec(x: u32, _y: Vec) -> u32 { + x + } + fn unsupported_slice(x: u32, _y: &[u8]) -> u32 { + x + } + fn doesnt_implement_arbitrary( + x: DoesntImplementArbitrary, + _y: DerivesArbitrary, + ) -> DoesntImplementArbitrary { + x + } +} diff --git a/tests/script-based-pre/cargo_autoverify_harnesses_fail/Cargo.toml b/tests/script-based-pre/cargo_autoverify_harnesses_fail/Cargo.toml new file mode 100644 index 000000000000..7c1fdab9efb3 --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_harnesses_fail/Cargo.toml @@ -0,0 +1,7 @@ +[package] +name = "cargo_autoverify_harnesses_fail" +version = "0.1.0" +edition = "2024" + +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } diff --git a/tests/script-based-pre/cargo_autoverify_harnesses_fail/config.yml b/tests/script-based-pre/cargo_autoverify_harnesses_fail/config.yml new file mode 100644 index 000000000000..f5b3400d03bf --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_harnesses_fail/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: harnesses_fail.sh +expected: harnesses_fail.expected diff --git a/tests/script-based-pre/cargo_autoverify_harnesses_fail/harnesses_fail.expected b/tests/script-based-pre/cargo_autoverify_harnesses_fail/harnesses_fail.expected new file mode 100644 index 000000000000..520d6d6c94b8 --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_harnesses_fail/harnesses_fail.expected @@ -0,0 +1,47 @@ +Checking harness panic_harness... +panic.assertion\ + - Status: FAILURE\ + - Description: "explicit panic" + +Checking harness integer_overflow_harness... +assertion\ + - Status: FAILURE\ + - Description: "attempt to add with overflow" + +Checking harness oob_unsafe_array_access_harness... +oob_unsafe_array_access.pointer_dereference\ + - Status: FAILURE\ + +Checking harness oob_safe_array_access_harness... + +>::index.assertion\ + - Status: FAILURE\ + - Description: "index out of bounds: the length is less than or equal to the given index" + + +Checking function panic against all possible inputs... + +Check 1: panic.assertion\ + - Status: FAILURE\ + - Description: "explicit panic" + +Checking function integer_overflow against all possible inputs... + +assertion\ + - Status: FAILURE + - Description: "attempt to add with overflow" + +Checking function oob_unsafe_array_access against all possible inputs... + +oob_unsafe_array_access.pointer_dereference\ + - Status: FAILURE\ + - Description: "dereference failure: pointer outside object bounds" + +Checking function oob_safe_array_access against all possible inputs... + +>::index.assertion\ + - Status: FAILURE\ + - Description: "index out of bounds: the length is less than or equal to the given index" + +Complete - 0 successfully verified harnesses, 8 failures, 8 total. + diff --git a/tests/script-based-pre/cargo_autoverify_harnesses_fail/harnesses_fail.sh b/tests/script-based-pre/cargo_autoverify_harnesses_fail/harnesses_fail.sh new file mode 100755 index 000000000000..ddd887daaa0a --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_harnesses_fail/harnesses_fail.sh @@ -0,0 +1,9 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +cargo kani autoverify -Z unstable-options +# We expect verification to fail, so the above command will produce an exit status of 1 +# However, we don't want the test to fail because of that exit status; we only want it to fail if the expected file doesn't match +# So, exit with a status code of 0 explicitly. +exit 0; diff --git a/tests/script-based-pre/cargo_autoverify_harnesses_fail/src/lib.rs b/tests/script-based-pre/cargo_autoverify_harnesses_fail/src/lib.rs new file mode 100644 index 000000000000..c91a4de37ca1 --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_harnesses_fail/src/lib.rs @@ -0,0 +1,57 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zautomatic-harnesses + +// Test the bodies of the automatically generated harnesses: +// do they catch the same failures as manual ones? +// Note that this also indirectly tests that the automatic harness +// subcommand also runs the manual harnesses in the crate. + +fn oob_safe_array_access(idx: usize) { + let v = vec![1, 2, 3]; + v[idx]; +} + +fn oob_unsafe_array_access(i: usize) -> u32 { + let a: &[u32] = &[1, 2, 3]; + if a.len() == 0 { + return 0; + } + return unsafe { *a.as_ptr().add(i % a.len() + 1) }; +} + +fn integer_overflow(x: i32) -> i32 { + if x <= i32::MAX - 100 { + let add_num = |mut x: i32, z: i64| x += z as i32; + add_num(x, 1); + // overflow + add_num(x, 101); + } + x +} + +fn panic() { + if kani::any() { + panic!(); + } +} + +#[kani::proof] +fn oob_safe_array_access_harness() { + oob_safe_array_access(kani::any()); +} + +#[kani::proof] +fn oob_unsafe_array_access_harness() { + oob_unsafe_array_access(kani::any()); +} + +#[kani::proof] +fn integer_overflow_harness() { + integer_overflow(kani::any()); +} + +#[kani::proof] +fn panic_harness() { + panic(); +} diff --git a/tests/script-based-pre/cargo_autoverify_loops_fixme/Cargo.toml b/tests/script-based-pre/cargo_autoverify_loops_fixme/Cargo.toml new file mode 100644 index 000000000000..63555fbe95b9 --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_loops_fixme/Cargo.toml @@ -0,0 +1,7 @@ +[package] +name = "cargo_autoverify_loops_fixme" +version = "0.1.0" +edition = "2024" + +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } diff --git a/tests/script-based-pre/cargo_autoverify_loops_fixme/config.yml b/tests/script-based-pre/cargo_autoverify_loops_fixme/config.yml new file mode 100644 index 000000000000..90ee1970e96c --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_loops_fixme/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: filter.sh +expected: filter.expected diff --git a/tests/script-based-pre/cargo_autoverify_loops_fixme/loops.expected b/tests/script-based-pre/cargo_autoverify_loops_fixme/loops.expected new file mode 100644 index 000000000000..8f357ebd103d --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_loops_fixme/loops.expected @@ -0,0 +1 @@ +TODO write me \ No newline at end of file diff --git a/tests/script-based-pre/cargo_autoverify_loops_fixme/loops.sh b/tests/script-based-pre/cargo_autoverify_loops_fixme/loops.sh new file mode 100755 index 000000000000..c5bdc2bfa0ac --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_loops_fixme/loops.sh @@ -0,0 +1,5 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +cargo kani autoverify -Z unstable-options diff --git a/tests/script-based-pre/cargo_autoverify_loops_fixme/src/lib.rs b/tests/script-based-pre/cargo_autoverify_loops_fixme/src/lib.rs new file mode 100644 index 000000000000..8dcc41d99fc6 --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_loops_fixme/src/lib.rs @@ -0,0 +1,28 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zautomatic-harnesses + +#![feature(stmt_expr_attributes)] +#![feature(proc_macro_hygiene)] + +// Test that automatic harnesses terminate on functions with loops. + +// Since foo()'s arguments implement Arbitrary, we will attempt to verify it, +// and enter an infinite loop. +// Instead, we should just skip this function, perhaps printing a message to the user that we skipped it. +fn infinite_loop() { + loop {} +} + +// Shouldn't skip this function -- it has a loop, but since it also has a loop contract, +// we can generate a contract harness for it and be assured that the proof will terminate. +fn has_loop_contract() { + let mut x: u8 = kani::any_where(|i| *i >= 2); + + #[kani::loop_invariant(x >= 2)] + while x > 2 { + x = x - 1; + } + + assert!(x == 2); +} From e46bb3a6b068a7709beaa751f2ecc0045a03c8c2 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Sun, 2 Feb 2025 17:52:31 -0500 Subject: [PATCH 02/12] contract harnesses support --- .../src/kani_middle/codegen_units.rs | 60 +++++++++++++------ kani-compiler/src/kani_middle/metadata.rs | 12 +++- .../src/kani_middle/transform/contracts.rs | 36 ++++++++--- .../Cargo.toml | 2 +- .../config.yml | 0 .../contracts.expected | 19 ++++++ .../cargo_autoverify_contracts/contracts.sh | 9 +++ .../cargo_autoverify_contracts/src/lib.rs | 50 ++++++++++++++++ .../contracts.expected | 1 - .../contracts.sh | 5 -- .../src/lib.rs | 16 ----- .../loops.expected | 1 - .../cargo_autoverify_loops_fixme/src/lib.rs | 37 ++++++++---- 13 files changed, 182 insertions(+), 66 deletions(-) rename tests/script-based-pre/{cargo_autoverify_contracts_fixme => cargo_autoverify_contracts}/Cargo.toml (74%) rename tests/script-based-pre/{cargo_autoverify_contracts_fixme => cargo_autoverify_contracts}/config.yml (100%) create mode 100644 tests/script-based-pre/cargo_autoverify_contracts/contracts.expected create mode 100755 tests/script-based-pre/cargo_autoverify_contracts/contracts.sh create mode 100644 tests/script-based-pre/cargo_autoverify_contracts/src/lib.rs delete mode 100644 tests/script-based-pre/cargo_autoverify_contracts_fixme/contracts.expected delete mode 100755 tests/script-based-pre/cargo_autoverify_contracts_fixme/contracts.sh delete mode 100644 tests/script-based-pre/cargo_autoverify_contracts_fixme/src/lib.rs delete mode 100644 tests/script-based-pre/cargo_autoverify_loops_fixme/loops.expected diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 725781f7b9c6..2948fc1186af 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -8,7 +8,7 @@ //! according to their stub configuration. use crate::args::ReachabilityType; -use crate::kani_middle::attributes::is_proof_harness; +use crate::kani_middle::attributes::{KaniAttributes, is_proof_harness}; use crate::kani_middle::kani_functions::{KaniIntrinsic, KaniModel}; use crate::kani_middle::metadata::{ gen_automatic_proof_metadata, gen_contracts_metadata, gen_proof_metadata, @@ -73,22 +73,35 @@ impl CodegenUnits { } ReachabilityType::Automatic => { let mut all_harnesses = get_all_manual_harnesses(tcx, base_filename); + let mut units = group_by_stubs(tcx, &all_harnesses); + validate_units(tcx, &units); + let kani_fns = queries.kani_functions(); - let any_inst = kani_fns.get(&KaniModel::Any.into()).unwrap(); - let verifiable_fns = filter_crate_items(tcx, |_, instance: Instance| -> bool { - is_eligible_for_automatic_harness(tcx, instance, *any_inst) - }); let kani_harness_intrinsic = kani_fns.get(&KaniIntrinsic::AutomaticHarness.into()).unwrap(); + let kani_any_inst = kani_fns.get(&KaniModel::Any.into()).unwrap(); + let verifiable_fns = filter_crate_items(tcx, |_, instance: Instance| -> bool { + is_eligible_for_automatic_harness(tcx, instance, *kani_any_inst) + }); let automatic_harnesses = get_all_automatic_harnesses( tcx, verifiable_fns, *kani_harness_intrinsic, base_filename, ); + // We generate one contract harness per function under contract, so each harness is in its own unit, + // and these harnesses have no stubs. + units.extend( + automatic_harnesses + .iter() + .map(|(harness, _)| CodegenUnit { + harnesses: vec![*harness], + stubs: HashMap::default(), + }) + .collect::>(), + ); all_harnesses.extend(automatic_harnesses); - let units = group_by_stubs(tcx, &all_harnesses); - validate_units(tcx, &units); + // No need to validate the units again because validation only checks stubs, and we haven't added any stubs. debug!(?units, "CodegenUnits::new"); CodegenUnits { units, harness_info: all_harnesses, crate_info } } @@ -113,7 +126,15 @@ impl CodegenUnits { /// We flag that the harness contains usage of loop contracts. pub fn store_loop_contracts(&mut self, harnesses: &[Harness]) { for harness in harnesses { - self.harness_info.get_mut(harness).unwrap().has_loop_contracts = true; + let metadata = self.harness_info.get_mut(harness).unwrap(); + metadata.has_loop_contracts = true; + // If we're generating this harness automatically and we encounter a loop contract, + // ensure that the HarnessKind is updated to be a contract harness + // targeting the function to verify. + if metadata.is_automatically_generated { + metadata.attributes.kind = + HarnessKind::ProofForContract { target_fn: metadata.pretty_name.clone() } + } } } @@ -315,16 +336,11 @@ fn get_all_automatic_harnesses( } /// Determine whether `instance` is eligible for automatic verification. -/// `instance` is eligible iff: -/// 1. It is not a harness, -/// 2. It has a non-empty body, -/// 3. It is not an associated item of a Kani trait implementation (e.g., a kani::any implementation) -/// 4. All of its arguments implement Arbitrary fn is_eligible_for_automatic_harness(tcx: TyCtxt, instance: Instance, any_inst: FnDef) -> bool { + // `instance` is ineligble if it is a harness or has an nonexistent/empty body if is_proof_harness(tcx, instance) || !instance.has_body() { return false; } - // Don't generate a harness for functions with empty bodies. let body = instance.body().unwrap(); if body.blocks.is_empty() || (body.blocks[0].statements.is_empty() @@ -333,14 +349,20 @@ fn is_eligible_for_automatic_harness(tcx: TyCtxt, instance: Instance, any_inst: return false; } - // Don't generate harnesses for associated items of Kani trait implementations. - // FIXME -- find a less hardcoded way of doing this (perhaps upstream PR to StableMIR). - if instance.name().contains("kani::Arbitrary") || instance.name().contains("kani::Invariant") { + // `instance` is ineligble if it is an associated item of a Kani trait implementation, + // or part of Kani contract instrumentation. + // FIXME -- find a less hardcoded way of checking the former condition (perhaps upstream PR to StableMIR). + if instance.name().contains("kani::Arbitrary") + || instance.name().contains("kani::Invariant") + || KaniAttributes::for_instance(tcx, instance) + .fn_marker() + .is_some_and(|m| m.as_str() == "kani_contract_mode") + { return false; } - // Each non-generic argument of instance must implement Arbitrary. - // FIXME -- this will only find Arbitrary implementations for types whose Arbitrary + // Each non-generic argument of `instance`` must implement Arbitrary. + // FIXME -- this is sound but not complete, since it will only work for types whose Arbitrary // implementations have an inner call to kani::any, which not all implementations (e.g. PhantomPinned) do. body.arg_locals().iter().all(|arg| { let kani_any_body = diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs index d85d02c75d49..449548f27045 100644 --- a/kani-compiler/src/kani_middle/metadata.rs +++ b/kani-compiler/src/kani_middle/metadata.rs @@ -90,9 +90,8 @@ pub fn gen_contracts_metadata(tcx: TyCtxt) -> Vec { /// the metdata from that function uniquely identifies the harness. /// In future iterations of this feature, we will likely have multiple harnesses for a single function (e.g., for generic functions), /// in which case HarnessMetadata will need to change further to differentiate between those harnesses. -/// TODO Instead of just generating HarnessKind::Proof, generate HarnessKind::ProofForContract if fn_to_verify has a contract. pub fn gen_automatic_proof_metadata( - _tcx: TyCtxt, + tcx: TyCtxt, base_name: &Path, fn_to_verify: &Instance, ) -> HarnessMetadata { @@ -105,6 +104,13 @@ pub fn gen_automatic_proof_metadata( let file_stem = format!("{}_{mangled_name}", base_name.file_stem().unwrap().to_str().unwrap()); let model_file = base_name.with_file_name(file_stem).with_extension(ArtifactType::SymTabGoto); + let kani_attributes = KaniAttributes::for_instance(tcx, *fn_to_verify); + let harness_kind = if kani_attributes.has_contract() { + HarnessKind::ProofForContract { target_fn: pretty_name.clone() } + } else { + HarnessKind::Proof + }; + HarnessMetadata { pretty_name, mangled_name, @@ -112,7 +118,7 @@ pub fn gen_automatic_proof_metadata( original_file: loc.filename, original_start_line: loc.start_line, original_end_line: loc.end_line, - attributes: HarnessAttributes::new(HarnessKind::Proof), + attributes: HarnessAttributes::new(harness_kind), // TODO: This no longer needs to be an Option. goto_file: Some(model_file), contract: Default::default(), diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs index fea8a8a1bc3c..7e93163a5dc0 100644 --- a/kani-compiler/src/kani_middle/transform/contracts.rs +++ b/kani-compiler/src/kani_middle/transform/contracts.rs @@ -1,6 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT //! This module contains code related to the MIR-to-MIR pass to enable contracts. +use crate::args::ReachabilityType; use crate::kani_middle::attributes::KaniAttributes; use crate::kani_middle::codegen_units::CodegenUnit; use crate::kani_middle::kani_functions::{KaniIntrinsic, KaniModel}; @@ -341,13 +342,34 @@ impl FunctionWithContractPass { /// verifying. pub fn new(tcx: TyCtxt, queries: &QueryDb, unit: &CodegenUnit) -> FunctionWithContractPass { if let Some(harness) = unit.harnesses.first() { - let attrs = KaniAttributes::for_instance(tcx, *harness); - let check_fn = attrs.interpret_for_contract_attribute().map(|(_, def_id, _)| def_id); - let replace_fns: HashSet<_> = attrs - .interpret_stub_verified_attribute() - .iter() - .map(|(_, def_id, _)| *def_id) - .collect(); + let (check_fn, replace_fns) = { + let harness_generic_args = harness.args().0; + // Manual harnesses have no arguments, so if there are generic arguments, + // we know this is an automatic harness + if matches!(queries.args().reachability_analysis, ReachabilityType::Automatic) + && !harness_generic_args.is_empty() + { + let kind = harness.args().0[0].expect_ty().kind(); + let (def, args) = kind.fn_def().unwrap(); + let fn_to_verify = Instance::resolve(def, &args).unwrap(); + // For automatic harnesses, the target is the function to verify, + // and stubs are empty. + ( + Some(rustc_internal::internal(tcx, fn_to_verify.def.def_id())), + HashSet::default(), + ) + } else { + let attrs = KaniAttributes::for_instance(tcx, *harness); + let check_fn = + attrs.interpret_for_contract_attribute().map(|(_, def_id, _)| def_id); + let replace_fns: HashSet<_> = attrs + .interpret_stub_verified_attribute() + .iter() + .map(|(_, def_id, _)| *def_id) + .collect(); + (check_fn, replace_fns) + } + }; let run_contract_fn = queries.kani_functions().get(&KaniModel::RunContract.into()).copied(); assert!(run_contract_fn.is_some(), "Failed to find Kani run contract function"); diff --git a/tests/script-based-pre/cargo_autoverify_contracts_fixme/Cargo.toml b/tests/script-based-pre/cargo_autoverify_contracts/Cargo.toml similarity index 74% rename from tests/script-based-pre/cargo_autoverify_contracts_fixme/Cargo.toml rename to tests/script-based-pre/cargo_autoverify_contracts/Cargo.toml index e04125cb6690..be3a32bdca8f 100644 --- a/tests/script-based-pre/cargo_autoverify_contracts_fixme/Cargo.toml +++ b/tests/script-based-pre/cargo_autoverify_contracts/Cargo.toml @@ -1,5 +1,5 @@ [package] -name = "cargo_autoverify_contracts_fixme" +name = "cargo_autoverify_contracts" version = "0.1.0" edition = "2024" diff --git a/tests/script-based-pre/cargo_autoverify_contracts_fixme/config.yml b/tests/script-based-pre/cargo_autoverify_contracts/config.yml similarity index 100% rename from tests/script-based-pre/cargo_autoverify_contracts_fixme/config.yml rename to tests/script-based-pre/cargo_autoverify_contracts/config.yml diff --git a/tests/script-based-pre/cargo_autoverify_contracts/contracts.expected b/tests/script-based-pre/cargo_autoverify_contracts/contracts.expected new file mode 100644 index 000000000000..c8bf50d6a0d1 --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_contracts/contracts.expected @@ -0,0 +1,19 @@ +Checking function should_fail::max against all possible inputs... +assertion\ + - Status: FAILURE\ + - Description: "|result : &u32| *result == x" + +Checking function should_pass::has_loop_contract against all possible inputs... +should_pass::has_loop_contract.assertion\ + - Status: SUCCESS\ + - Description: "assertion failed: x == 2" + +Checking function should_pass::has_recursion_gcd against all possible inputs... +assertion\ + - Status: SUCCESS\ + - Description: "|result : &u8| *result != 0 && x % *result == 0 && y % *result == 0" + +Checking function should_pass::div against all possible inputs... + +Verification failed for - should_fail::max +Complete - 3 successfully verified harnesses, 1 failures, 4 total. diff --git a/tests/script-based-pre/cargo_autoverify_contracts/contracts.sh b/tests/script-based-pre/cargo_autoverify_contracts/contracts.sh new file mode 100755 index 000000000000..7428e196fa84 --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_contracts/contracts.sh @@ -0,0 +1,9 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +cargo kani autoverify -Z unstable-options -Z function-contracts -Z loop-contracts +# We expect verification to fail, so the above command will produce an exit status of 1 +# However, we don't want the test to fail because of that exit status; we only want it to fail if the expected file doesn't match +# So, exit with a status code of 0 explicitly. +exit 0; diff --git a/tests/script-based-pre/cargo_autoverify_contracts/src/lib.rs b/tests/script-based-pre/cargo_autoverify_contracts/src/lib.rs new file mode 100644 index 000000000000..ead636fd51ec --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_contracts/src/lib.rs @@ -0,0 +1,50 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Test that the autoverify subcommand correctly verifies contracts, +// i.e., that it detects the presence of a contract and generates a contract +// harness instead of a standard harness. + +#![feature(stmt_expr_attributes)] +#![feature(proc_macro_hygiene)] + +mod should_pass { + #[kani::requires(divisor != 0)] + fn div(dividend: u32, divisor: u32) -> u32 { + dividend / divisor + } + + #[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) } + } + + fn has_loop_contract() { + let mut x: u8 = kani::any_where(|i| *i >= 2); + + #[kani::loop_invariant(x >= 2)] + while x > 2 { + x = x - 1; + } + + assert!(x == 2); + } +} + +mod should_fail { + #[kani::ensures(|result : &u32| *result == x)] + fn max(x: u32, y: u32) -> u32 { + if x > y { x } else { y } + } +} diff --git a/tests/script-based-pre/cargo_autoverify_contracts_fixme/contracts.expected b/tests/script-based-pre/cargo_autoverify_contracts_fixme/contracts.expected deleted file mode 100644 index 8f357ebd103d..000000000000 --- a/tests/script-based-pre/cargo_autoverify_contracts_fixme/contracts.expected +++ /dev/null @@ -1 +0,0 @@ -TODO write me \ No newline at end of file diff --git a/tests/script-based-pre/cargo_autoverify_contracts_fixme/contracts.sh b/tests/script-based-pre/cargo_autoverify_contracts_fixme/contracts.sh deleted file mode 100755 index c5bdc2bfa0ac..000000000000 --- a/tests/script-based-pre/cargo_autoverify_contracts_fixme/contracts.sh +++ /dev/null @@ -1,5 +0,0 @@ -#!/usr/bin/env bash -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -cargo kani autoverify -Z unstable-options diff --git a/tests/script-based-pre/cargo_autoverify_contracts_fixme/src/lib.rs b/tests/script-based-pre/cargo_autoverify_contracts_fixme/src/lib.rs deleted file mode 100644 index 7a8aa8e84f69..000000000000 --- a/tests/script-based-pre/cargo_autoverify_contracts_fixme/src/lib.rs +++ /dev/null @@ -1,16 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Zautomatic-harnesses -Zfunction-contracts - -// The automatic harnesses feature will only generate standard harnesses (#[kani::proof]) -// for each function, even if it has a contract. -// That standard harness will ignore the function's contract, -// causing verification failure in this case (division by zero). -// Instead, we should detect the presence of contracts and generate a contract harness. - -#[kani::requires(divisor != 0)] -fn div(dividend: u32, divisor: u32) -> u32 { - dividend / divisor -} - -// TODO add more tests, including test(s) for unsafe functions. diff --git a/tests/script-based-pre/cargo_autoverify_loops_fixme/loops.expected b/tests/script-based-pre/cargo_autoverify_loops_fixme/loops.expected deleted file mode 100644 index 8f357ebd103d..000000000000 --- a/tests/script-based-pre/cargo_autoverify_loops_fixme/loops.expected +++ /dev/null @@ -1 +0,0 @@ -TODO write me \ No newline at end of file diff --git a/tests/script-based-pre/cargo_autoverify_loops_fixme/src/lib.rs b/tests/script-based-pre/cargo_autoverify_loops_fixme/src/lib.rs index 8dcc41d99fc6..99ba72445b6d 100644 --- a/tests/script-based-pre/cargo_autoverify_loops_fixme/src/lib.rs +++ b/tests/script-based-pre/cargo_autoverify_loops_fixme/src/lib.rs @@ -1,28 +1,39 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Zautomatic-harnesses - -#![feature(stmt_expr_attributes)] -#![feature(proc_macro_hygiene)] // Test that automatic harnesses terminate on functions with loops. // Since foo()'s arguments implement Arbitrary, we will attempt to verify it, // and enter an infinite loop. -// Instead, we should just skip this function, perhaps printing a message to the user that we skipped it. +// Unclear what the best solution to this problem is; perhaps this is just a known limitation +// and the user needs to specify some command line flag to skip this function, +// or we can conservatively skip functions with loops that don't have loop contracts. fn infinite_loop() { loop {} } -// Shouldn't skip this function -- it has a loop, but since it also has a loop contract, -// we can generate a contract harness for it and be assured that the proof will terminate. -fn has_loop_contract() { - let mut x: u8 = kani::any_where(|i| *i >= 2); +/// Euclid's algorithm for calculating the GCD of two numbers +#[kani::requires(x != 0 && y != 0)] +#[kani::ensures(|result : &u8| *result != 0 && x % *result == 0 && y % *result == 0)] +fn gcd(mut x: u8, mut y: u8) -> u8 { + (x, y) = (if x > y { x } else { y }, if x > y { y } else { x }); + loop { + let res = x % y; + if res == 0 { + return y; + } - #[kani::loop_invariant(x >= 2)] - while x > 2 { - x = x - 1; + x = y; + y = res; } +} - assert!(x == 2); +// Since we can specify an unwinding bound in a manual harness, +// the proof will terminate. +// Automatic harnesses, however, do not support unwinding bounds, +// so the proof does not terminate. +#[kani::proof_for_contract(gcd)] +#[kani::unwind(12)] +fn gcd_harness() { + gcd(kani::any(), kani::any()); } From 53c534e715a69a407b5a302d3c61844530879d41 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Mon, 3 Feb 2025 18:05:43 -0500 Subject: [PATCH 03/12] Improve summary --- kani-driver/src/autoverify/mod.rs | 59 ++++++++++ kani-driver/src/harness_runner.rs | 106 ++++++++++-------- kani-driver/src/main.rs | 1 + kani-driver/src/session.rs | 7 +- .../contracts.expected | 19 +++- .../cargo_autoverify_contracts/src/lib.rs | 6 + .../cargo_autoverify_filter/filter.expected | 80 ++++++------- .../harnesses_fail.expected | 52 +++++---- .../src/lib.rs | 13 ++- 9 files changed, 228 insertions(+), 115 deletions(-) create mode 100644 kani-driver/src/autoverify/mod.rs diff --git a/kani-driver/src/autoverify/mod.rs b/kani-driver/src/autoverify/mod.rs new file mode 100644 index 000000000000..82a5372402f0 --- /dev/null +++ b/kani-driver/src/autoverify/mod.rs @@ -0,0 +1,59 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +use crate::call_cbmc::VerificationStatus; +use crate::harness_runner::HarnessResult; +use crate::session::KaniSession; +use anyhow::Result; + +impl KaniSession { + /// Enable autoverify mode. + pub fn enable_autoverify(&mut self) { + self.auto_verify = true; + } + + /// Prints the results from running the `autoverify` subcommand. + pub fn print_autoverify_summary(&self, automatic: Vec<&HarnessResult<'_>>) -> Result<()> { + let (successes, failures): (Vec<_>, Vec<_>) = + automatic.into_iter().partition(|r| r.result.status == VerificationStatus::Success); + + let succeeding = successes.len(); + let failing = failures.len(); + let total = succeeding + failing; + + // TODO: it would be nice if we had access to which functions the user included/excluded here + // so that we could print a comparison for them of any of the included functions that we skipped. + println!("Autoverify Summary:"); + println!( + "Note that Kani will only autoverify a function if it determines that each of its arguments implement the Arbitrary trait." + ); + println!( + "Examine the summary closely to determine which functions were automatically verified." + ); + + // Since autoverification skips over some functions, print the successes to make it easier to see what we verified in one place. + for success in successes { + println!("Verification succeeded for - {}", success.harness.pretty_name); + } + + for failure in failures { + println!("Verification failed for - {}", failure.harness.pretty_name); + } + + if total > 0 { + println!( + "Complete - {succeeding} successfully verified functions, {failing} failures, {total} total." + ); + } else { + println!(" + No functions were eligible for automatic verification. Functions can only be automatically verified if each of their arguments implement kani::Arbitrary."); + println!( + "If you specified --include-function or --exclude-function, make sure that your filters were not overly restrictive." + ); + } + + // Manual harness summary may come afterward, so separate them with a new line. + println!(); + Ok(()) + } +} diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index 320d574a01f8..a567467e85af 100644 --- a/kani-driver/src/harness_runner.rs +++ b/kani-driver/src/harness_runner.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use anyhow::{Result, bail}; -use kani_metadata::{ArtifactType, HarnessMetadata}; +use kani_metadata::{ArtifactType, HarnessKind, HarnessMetadata}; use rayon::prelude::*; use std::fs::File; use std::io::Write; @@ -11,7 +11,7 @@ use std::path::Path; use crate::args::OutputFormat; use crate::call_cbmc::{VerificationResult, VerificationStatus}; use crate::project::Project; -use crate::session::KaniSession; +use crate::session::{BUG_REPORT_URL, KaniSession}; use std::env::current_dir; use std::path::PathBuf; @@ -169,10 +169,17 @@ impl KaniSession { let thread_index = rayon::current_thread_index().unwrap_or_default(); // If the harness is automatically generated, pretty_name refers to the function under verification. let mut msg = if harness.is_automatically_generated { - format!( - "Automatic verification: Checking function {} against all possible inputs...", - harness.pretty_name - ) + if matches!(harness.attributes.kind, HarnessKind::Proof) { + format!( + "Autoverify: Checking function {} against all possible inputs...", + harness.pretty_name + ) + } else { + format!( + "Autoverify: Checking function {}'s contract against all possible inputs...", + harness.pretty_name + ) + } } else { format!("Checking harness {}...", harness.pretty_name) }; @@ -196,54 +203,65 @@ impl KaniSession { /// Note: Takes `self` "by ownership". This function wants to be able to drop before /// exiting with an error code, if needed. pub(crate) fn print_final_summary(self, results: &[HarnessResult<'_>]) -> Result<()> { + if self.args.common_args.quiet { + return Ok(()); + } + + let (automatic, manual): (Vec<_>, Vec<_>) = + results.iter().partition(|r| r.harness.is_automatically_generated); + + if self.auto_verify { + self.print_autoverify_summary(automatic)?; + } + let (successes, failures): (Vec<_>, Vec<_>) = - results.iter().partition(|r| r.result.status == VerificationStatus::Success); + manual.into_iter().partition(|r| r.result.status == VerificationStatus::Success); let succeeding = successes.len(); let failing = failures.len(); let total = succeeding + failing; - if self.args.concrete_playback.is_some() - && !self.args.common_args.quiet - && results.iter().all(|r| !r.result.generated_concrete_test) - { - println!( - "INFO: The concrete playback feature never generated unit tests because there were no failing harnesses." - ) + if self.args.concrete_playback.is_some() { + if failures.is_empty() { + println!( + "INFO: The concrete playback feature never generated unit tests because there were no failing harnesses." + ) + } else if failures.iter().all(|r| !r.result.generated_concrete_test) { + eprintln!( + "The concrete playback feature did not generate unit tests, but there were failing harnesses. Please file a bug report at {BUG_REPORT_URL}" + ) + } } // We currently omit a summary if there was just 1 harness - if !self.args.common_args.quiet { - if failing > 0 { - println!("Summary:"); - } - for failure in failures.iter() { - println!("Verification failed for - {}", failure.harness.pretty_name); - } + if failing > 0 { + println!("Manual Harness Summary:"); + } + for failure in failures.iter() { + println!("Verification failed for - {}", failure.harness.pretty_name); + } - if total > 0 { - println!( - "Complete - {succeeding} successfully verified harnesses, {failing} failures, {total} total." - ); - } else { - match self.args.harnesses.as_slice() { - [] => - // TODO: This could use a better message, possibly with links to Kani documentation. - // New users may encounter this and could use a pointer to how to write proof harnesses. - { - println!( - "No proof harnesses (functions with #[kani::proof]) were found to verify." - ) - } - [harness] => { - bail!("no harnesses matched the harness filter: `{harness}`") - } - harnesses => bail!( - "no harnesses matched the harness filters: `{}`", - harnesses.join("`, `") - ), - }; - } + if total > 0 { + println!( + "Complete - {succeeding} successfully verified harnesses, {failing} failures, {total} total." + ); + } else { + match self.args.harnesses.as_slice() { + [] => + // TODO: This could use a better message, possibly with links to Kani documentation. + // New users may encounter this and could use a pointer to how to write proof harnesses. + { + println!( + "No proof harnesses (functions with #[kani::proof]) were found to verify." + ) + } + [harness] => { + bail!("no harnesses matched the harness filter: `{harness}`") + } + harnesses => { + bail!("no harnesses matched the harness filters: `{}`", harnesses.join("`, `")) + } + }; } if self.args.coverage { diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index 2282a2bdb342..8618977ee4d0 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -22,6 +22,7 @@ use tracing::debug; mod args; mod args_toml; mod assess; +mod autoverify; mod call_cargo; mod call_cbmc; mod call_goto_cc; diff --git a/kani-driver/src/session.rs b/kani-driver/src/session.rs index db2a98358e45..719c98d10ce2 100644 --- a/kani-driver/src/session.rs +++ b/kani-driver/src/session.rs @@ -17,6 +17,9 @@ use tokio::process::Command as TokioCommand; use tracing::level_filters::LevelFilter; use tracing_subscriber::{EnvFilter, Registry, layer::SubscriberExt}; +pub const BUG_REPORT_URL: &str = + "https://github.com/model-checking/kani/issues/new?labels=bug&template=bug_report.md"; + /// Environment variable used to control this session log tracing. /// This is the same variable used to control `kani-compiler` logs. Note that you can still control /// the driver logs separately, by using the logger directives to select the kani-driver crate. @@ -74,10 +77,6 @@ impl KaniSession { }) } - pub fn enable_autoverify(&mut self) { - self.auto_verify = true; - } - /// Record a temporary file so we can cleanup after ourselves at the end. /// Note that there will be no failure if the file does not exist. pub fn record_temporary_file>(&self, temp: &T) { diff --git a/tests/script-based-pre/cargo_autoverify_contracts/contracts.expected b/tests/script-based-pre/cargo_autoverify_contracts/contracts.expected index c8bf50d6a0d1..4901a7019cd8 100644 --- a/tests/script-based-pre/cargo_autoverify_contracts/contracts.expected +++ b/tests/script-based-pre/cargo_autoverify_contracts/contracts.expected @@ -1,19 +1,28 @@ -Checking function should_fail::max against all possible inputs... +Autoverify: Checking function should_fail::max's contract against all possible inputs... assertion\ - Status: FAILURE\ - Description: "|result : &u32| *result == x" -Checking function should_pass::has_loop_contract against all possible inputs... +Autoverify: Checking function should_pass::has_loop_contract's contract against all possible inputs... should_pass::has_loop_contract.assertion\ - Status: SUCCESS\ - Description: "assertion failed: x == 2" -Checking function should_pass::has_recursion_gcd against all possible inputs... +Autoverify: Checking function should_pass::has_recursion_gcd's contract against all possible inputs... assertion\ - Status: SUCCESS\ - Description: "|result : &u8| *result != 0 && x % *result == 0 && y % *result == 0" -Checking function should_pass::div against all possible inputs... +Autoverify: Checking function should_pass::div's contract against all possible inputs... +Autoverify: Checking function should_pass::unchecked_mul's contract against all possible inputs... +arithmetic_overflow\ + - Status: SUCCESS\ + - Description: "attempt to compute `unchecked_mul` which would overflow" + +Verification succeeded for - should_pass::unchecked_mul +Verification succeeded for - should_pass::has_loop_contract +Verification succeeded for - should_pass::has_recursion_gcd +Verification succeeded for - should_pass::div Verification failed for - should_fail::max -Complete - 3 successfully verified harnesses, 1 failures, 4 total. +Complete - 4 successfully verified functions, 1 failures, 5 total. diff --git a/tests/script-based-pre/cargo_autoverify_contracts/src/lib.rs b/tests/script-based-pre/cargo_autoverify_contracts/src/lib.rs index ead636fd51ec..e2ac9654bd36 100644 --- a/tests/script-based-pre/cargo_autoverify_contracts/src/lib.rs +++ b/tests/script-based-pre/cargo_autoverify_contracts/src/lib.rs @@ -40,6 +40,12 @@ mod should_pass { assert!(x == 2); } + + // Test that we can autoverify functions for unsafe functions with contracts + #[kani::requires(!left.overflowing_mul(rhs).1)] + unsafe fn unchecked_mul(left: u8, rhs: u8) -> u8 { + left.unchecked_mul(rhs) + } } mod should_fail { diff --git a/tests/script-based-pre/cargo_autoverify_filter/filter.expected b/tests/script-based-pre/cargo_autoverify_filter/filter.expected index e960e9180e91..879c40eed631 100644 --- a/tests/script-based-pre/cargo_autoverify_filter/filter.expected +++ b/tests/script-based-pre/cargo_autoverify_filter/filter.expected @@ -1,40 +1,40 @@ -Automatic verification: Checking function yes_harness::f_tuple against all possible inputs... -Automatic verification: Checking function yes_harness::f_maybe_uninit against all possible inputs... -Automatic verification: Checking function yes_harness::f_result against all possible inputs... -Automatic verification: Checking function yes_harness::f_option against all possible inputs... -Automatic verification: Checking function yes_harness::f_array against all possible inputs... -Automatic verification: Checking function yes_harness::f_nonzero_isize against all possible inputs... -Automatic verification: Checking function yes_harness::f_nonzero_i128 against all possible inputs... -Automatic verification: Checking function yes_harness::f_nonzero_i64 against all possible inputs... -Automatic verification: Checking function yes_harness::f_nonzero_i32 against all possible inputs... -Automatic verification: Checking function yes_harness::f_nonzero_i16 against all possible inputs... -Automatic verification: Checking function yes_harness::f_nonzero_i8 against all possible inputs... -Automatic verification: Checking function yes_harness::f_nonzero_usize against all possible inputs... -Automatic verification: Checking function yes_harness::f_nonzero_u128 against all possible inputs... -Automatic verification: Checking function yes_harness::f_nonzero_u64 against all possible inputs... -Automatic verification: Checking function yes_harness::f_nonzero_u32 against all possible inputs... -Automatic verification: Checking function yes_harness::f_nonzero_u16 against all possible inputs... -Automatic verification: Checking function yes_harness::f_nonzero_u8 against all possible inputs... -Automatic verification: Checking function yes_harness::f_f128 against all possible inputs... -Automatic verification: Checking function yes_harness::f_f16 against all possible inputs... -Automatic verification: Checking function yes_harness::f_f64 against all possible inputs... -Automatic verification: Checking function yes_harness::f_f32 against all possible inputs... -Automatic verification: Checking function yes_harness::f_char against all possible inputs... -Automatic verification: Checking function yes_harness::f_bool against all possible inputs... -Automatic verification: Checking function yes_harness::f_isize against all possible inputs... -Automatic verification: Checking function yes_harness::f_i128 against all possible inputs... -Automatic verification: Checking function yes_harness::f_i64 against all possible inputs... -Automatic verification: Checking function yes_harness::f_i32 against all possible inputs... -Automatic verification: Checking function yes_harness::f_i16 against all possible inputs... -Automatic verification: Checking function yes_harness::f_i8 against all possible inputs... -Automatic verification: Checking function yes_harness::f_usize against all possible inputs... -Automatic verification: Checking function yes_harness::f_u128 against all possible inputs... -Automatic verification: Checking function yes_harness::f_u64 against all possible inputs... -Automatic verification: Checking function yes_harness::f_u32 against all possible inputs... -Automatic verification: Checking function yes_harness::f_u16 against all possible inputs... -Automatic verification: Checking function yes_harness::f_u8 against all possible inputs... -Automatic verification: Checking function yes_harness::f_unsupported_return_type against all possible inputs... -Automatic verification: Checking function yes_harness::f_multiple_args against all possible inputs... -Automatic verification: Checking function yes_harness::f_derives_arbitrary against all possible inputs... -Automatic verification: Checking function yes_harness::f_manually_implements_arbitrary against all possible inputs... -Complete - 39 successfully verified harnesses, 0 failures, 39 total. \ No newline at end of file +Autoverify: Checking function yes_harness::f_tuple against all possible inputs... +Autoverify: Checking function yes_harness::f_maybe_uninit against all possible inputs... +Autoverify: Checking function yes_harness::f_result against all possible inputs... +Autoverify: Checking function yes_harness::f_option against all possible inputs... +Autoverify: Checking function yes_harness::f_array against all possible inputs... +Autoverify: Checking function yes_harness::f_nonzero_isize against all possible inputs... +Autoverify: Checking function yes_harness::f_nonzero_i128 against all possible inputs... +Autoverify: Checking function yes_harness::f_nonzero_i64 against all possible inputs... +Autoverify: Checking function yes_harness::f_nonzero_i32 against all possible inputs... +Autoverify: Checking function yes_harness::f_nonzero_i16 against all possible inputs... +Autoverify: Checking function yes_harness::f_nonzero_i8 against all possible inputs... +Autoverify: Checking function yes_harness::f_nonzero_usize against all possible inputs... +Autoverify: Checking function yes_harness::f_nonzero_u128 against all possible inputs... +Autoverify: Checking function yes_harness::f_nonzero_u64 against all possible inputs... +Autoverify: Checking function yes_harness::f_nonzero_u32 against all possible inputs... +Autoverify: Checking function yes_harness::f_nonzero_u16 against all possible inputs... +Autoverify: Checking function yes_harness::f_nonzero_u8 against all possible inputs... +Autoverify: Checking function yes_harness::f_f128 against all possible inputs... +Autoverify: Checking function yes_harness::f_f16 against all possible inputs... +Autoverify: Checking function yes_harness::f_f64 against all possible inputs... +Autoverify: Checking function yes_harness::f_f32 against all possible inputs... +Autoverify: Checking function yes_harness::f_char against all possible inputs... +Autoverify: Checking function yes_harness::f_bool against all possible inputs... +Autoverify: Checking function yes_harness::f_isize against all possible inputs... +Autoverify: Checking function yes_harness::f_i128 against all possible inputs... +Autoverify: Checking function yes_harness::f_i64 against all possible inputs... +Autoverify: Checking function yes_harness::f_i32 against all possible inputs... +Autoverify: Checking function yes_harness::f_i16 against all possible inputs... +Autoverify: Checking function yes_harness::f_i8 against all possible inputs... +Autoverify: Checking function yes_harness::f_usize against all possible inputs... +Autoverify: Checking function yes_harness::f_u128 against all possible inputs... +Autoverify: Checking function yes_harness::f_u64 against all possible inputs... +Autoverify: Checking function yes_harness::f_u32 against all possible inputs... +Autoverify: Checking function yes_harness::f_u16 against all possible inputs... +Autoverify: Checking function yes_harness::f_u8 against all possible inputs... +Autoverify: Checking function yes_harness::f_unsupported_return_type against all possible inputs... +Autoverify: Checking function yes_harness::f_multiple_args against all possible inputs... +Autoverify: Checking function yes_harness::f_derives_arbitrary against all possible inputs... +Autoverify: Checking function yes_harness::f_manually_implements_arbitrary against all possible inputs... +Complete - 39 successfully verified functions, 0 failures, 39 total. \ No newline at end of file diff --git a/tests/script-based-pre/cargo_autoverify_harnesses_fail/harnesses_fail.expected b/tests/script-based-pre/cargo_autoverify_harnesses_fail/harnesses_fail.expected index 520d6d6c94b8..6d7fd2bec692 100644 --- a/tests/script-based-pre/cargo_autoverify_harnesses_fail/harnesses_fail.expected +++ b/tests/script-based-pre/cargo_autoverify_harnesses_fail/harnesses_fail.expected @@ -1,47 +1,57 @@ -Checking harness panic_harness... -panic.assertion\ +Autoverify: Checking function panic against all possible inputs... +Check 1: panic.assertion\ - Status: FAILURE\ - Description: "explicit panic" -Checking harness integer_overflow_harness... +Autoverify: Checking function integer_overflow against all possible inputs... assertion\ - - Status: FAILURE\ + - Status: FAILURE - Description: "attempt to add with overflow" -Checking harness oob_unsafe_array_access_harness... +Autoverify: Checking function oob_unsafe_array_access against all possible inputs... oob_unsafe_array_access.pointer_dereference\ - Status: FAILURE\ + - Description: "dereference failure: pointer outside object bounds" -Checking harness oob_safe_array_access_harness... +Autoverify: Checking function oob_safe_array_access against all possible inputs... +assertion\ + - Status: FAILURE\ + - Description: "index out of bounds: the length is less than or equal to the given index" ->::index.assertion\ +Autoverify: Checking function unchecked_mul against all possible inputs... +arithmetic_overflow\ - Status: FAILURE\ - - Description: "index out of bounds: the length is less than or equal to the given index" - + - Description: "attempt to compute `unchecked_mul` which would overflow" -Checking function panic against all possible inputs... +Verification failed for - panic +Verification failed for - integer_overflow +Verification failed for - oob_unsafe_array_access +Verification failed for - oob_safe_array_access +Verification failed for - unchecked_mul +Complete - 0 successfully verified functions, 5 failures, 5 total. -Check 1: panic.assertion\ +Checking harness panic_harness... +panic.assertion\ - Status: FAILURE\ - Description: "explicit panic" -Checking function integer_overflow against all possible inputs... - +Checking harness integer_overflow_harness... assertion\ - - Status: FAILURE + - Status: FAILURE\ - Description: "attempt to add with overflow" -Checking function oob_unsafe_array_access against all possible inputs... - +Checking harness oob_unsafe_array_access_harness... oob_unsafe_array_access.pointer_dereference\ - Status: FAILURE\ - - Description: "dereference failure: pointer outside object bounds" - -Checking function oob_safe_array_access against all possible inputs... ->::index.assertion\ +Checking harness oob_safe_array_access_harness... +assertion\ - Status: FAILURE\ - Description: "index out of bounds: the length is less than or equal to the given index" -Complete - 0 successfully verified harnesses, 8 failures, 8 total. +Checking harness unchecked_mul_harness... +arithmetic_overflow\ + - Status: FAILURE\ + - Description: "attempt to compute `unchecked_mul` which would overflow" +Complete - 0 successfully verified harnesses, 5 failures, 5 total. diff --git a/tests/script-based-pre/cargo_autoverify_harnesses_fail/src/lib.rs b/tests/script-based-pre/cargo_autoverify_harnesses_fail/src/lib.rs index c91a4de37ca1..072dae12c133 100644 --- a/tests/script-based-pre/cargo_autoverify_harnesses_fail/src/lib.rs +++ b/tests/script-based-pre/cargo_autoverify_harnesses_fail/src/lib.rs @@ -1,6 +1,5 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Zautomatic-harnesses // Test the bodies of the automatically generated harnesses: // do they catch the same failures as manual ones? @@ -36,6 +35,11 @@ fn panic() { } } +// Test that we can autoverify functions for unsafe functions +unsafe fn unchecked_mul(left: u8, rhs: u8) -> u8 { + left.unchecked_mul(rhs) +} + #[kani::proof] fn oob_safe_array_access_harness() { oob_safe_array_access(kani::any()); @@ -55,3 +59,10 @@ fn integer_overflow_harness() { fn panic_harness() { panic(); } + +#[kani::proof] +fn unchecked_mul_harness() { + unsafe { + unchecked_mul(kani::any(), kani::any()); + } +} From 0aed576af2f59ccdefb0c53c485a50591d2eabe5 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Mon, 3 Feb 2025 18:08:39 -0500 Subject: [PATCH 04/12] Add option to include or exclude partial function paths --- kani-compiler/src/args.rs | 6 ++++ .../src/kani_middle/codegen_units.rs | 23 +++++++++++-- kani-driver/src/args/autoverify_args.rs | 32 +++++++++++++++++-- kani-driver/src/assess/mod.rs | 2 +- kani-driver/src/autoverify/mod.rs | 13 ++++++++ kani-driver/src/call_cargo.rs | 11 +++---- kani-driver/src/list/collect_metadata.rs | 4 +-- kani-driver/src/main.rs | 13 ++++++-- kani-driver/src/project.rs | 2 +- kani-driver/src/session.rs | 4 +++ .../cargo_autoverify_exclude/Cargo.toml | 7 ++++ .../cargo_autoverify_exclude/config.yml | 4 +++ .../cargo_autoverify_exclude/exclude.expected | 4 +++ .../cargo_autoverify_exclude/exclude.sh | 5 +++ .../cargo_autoverify_exclude/src/lib.rs | 23 +++++++++++++ .../cargo_autoverify_include/Cargo.toml | 7 ++++ .../cargo_autoverify_include/config.yml | 4 +++ .../cargo_autoverify_include/include.expected | 4 +++ .../cargo_autoverify_include/include.sh | 5 +++ .../cargo_autoverify_include/src/lib.rs | 24 ++++++++++++++ 20 files changed, 180 insertions(+), 17 deletions(-) create mode 100644 tests/script-based-pre/cargo_autoverify_exclude/Cargo.toml create mode 100644 tests/script-based-pre/cargo_autoverify_exclude/config.yml create mode 100644 tests/script-based-pre/cargo_autoverify_exclude/exclude.expected create mode 100755 tests/script-based-pre/cargo_autoverify_exclude/exclude.sh create mode 100644 tests/script-based-pre/cargo_autoverify_exclude/src/lib.rs create mode 100644 tests/script-based-pre/cargo_autoverify_include/Cargo.toml create mode 100644 tests/script-based-pre/cargo_autoverify_include/config.yml create mode 100644 tests/script-based-pre/cargo_autoverify_include/include.expected create mode 100755 tests/script-based-pre/cargo_autoverify_include/include.sh create mode 100644 tests/script-based-pre/cargo_autoverify_include/src/lib.rs diff --git a/kani-compiler/src/args.rs b/kani-compiler/src/args.rs index 9fe129dade03..d93162da005d 100644 --- a/kani-compiler/src/args.rs +++ b/kani-compiler/src/args.rs @@ -90,6 +90,12 @@ pub struct Arguments { /// Print the final LLBC file to stdout. #[clap(long)] pub print_llbc: bool, + /// If we are running the autoverify subcommand, the functions to autoverify + #[arg(long = "autoverify-include-function", num_args(1))] + pub autoverify_included_functions: Vec, + /// If we are running the autoverify subcommand, the functions to exclude from autoverification + #[arg(long = "autoverify-exclude-function", num_args(1))] + pub autoverify_excluded_functions: Vec, } #[derive(Debug, Clone, Copy, AsRefStr, EnumString, VariantNames, PartialEq, Eq)] diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 2948fc1186af..62d089be6b21 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -62,7 +62,8 @@ impl CodegenUnits { let crate_info = CrateInfo { name: stable_mir::local_crate().name.as_str().into() }; let base_filepath = tcx.output_filenames(()).path(OutputType::Object); let base_filename = base_filepath.as_path(); - match queries.args().reachability_analysis { + let args = queries.args(); + match args.reachability_analysis { ReachabilityType::Harnesses => { let all_harnesses = get_all_manual_harnesses(tcx, base_filename); // Even if no_stubs is empty we still need to store rustc metadata. @@ -80,8 +81,18 @@ impl CodegenUnits { let kani_harness_intrinsic = kani_fns.get(&KaniIntrinsic::AutomaticHarness.into()).unwrap(); let kani_any_inst = kani_fns.get(&KaniModel::Any.into()).unwrap(); + let verifiable_fns = filter_crate_items(tcx, |_, instance: Instance| -> bool { - is_eligible_for_automatic_harness(tcx, instance, *kani_any_inst) + // If the user specified functions to include or exclude, only allow instances matching those filters. + let user_included = if !args.autoverify_included_functions.is_empty() { + fn_list_contains_instance(&instance, &args.autoverify_included_functions) + } else if !args.autoverify_excluded_functions.is_empty() { + !fn_list_contains_instance(&instance, &args.autoverify_excluded_functions) + } else { + true + }; + user_included + && is_eligible_for_automatic_harness(tcx, instance, *kani_any_inst) }); let automatic_harnesses = get_all_automatic_harnesses( tcx, @@ -378,3 +389,11 @@ fn is_eligible_for_automatic_harness(tcx: TyCtxt, instance: Instance, any_inst: false }) } + +/// Return whether the name of `instance` is included in `fn_list`. +/// If `exact = true`, then `instance`'s exact, fully-qualified name must be in `fn_list`; otherwise, `fn_list` +/// can have a substring of `instance`'s name. +fn fn_list_contains_instance(instance: &Instance, fn_list: &[String]) -> bool { + let pretty_name = instance.name(); + fn_list.contains(&pretty_name) || fn_list.iter().any(|fn_name| pretty_name.contains(fn_name)) +} diff --git a/kani-driver/src/args/autoverify_args.rs b/kani-driver/src/args/autoverify_args.rs index c8f961643e40..f6731ca94e04 100644 --- a/kani-driver/src/args/autoverify_args.rs +++ b/kani-driver/src/args/autoverify_args.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -//! Implements the subcommand handling of the list subcommand +//! Implements the subcommand handling of the autoverify subcommand use std::path::PathBuf; @@ -8,12 +8,35 @@ use crate::args::{ValidateArgs, VerificationArgs}; use clap::{Error, Parser, error::ErrorKind}; use kani_metadata::UnstableFeature; -// TODO add --function option to only verify functions matching the substring -// (akin to --harness). +#[derive(Debug, Parser)] +pub struct CommonAutoverifyArgs { + /// If specified, only autoverify functions that match this filter. This option can be provided + /// multiple times, which will verify all functions matching any of the filters. + /// Note that this filter will match against partial names, i.e., providing the name of a module will include all functions from that module. + /// Also note that if the function specified is unable to be automatically verified, this flag will have no effect. + #[arg( + long = "include-function", + num_args(1), + value_name = "FUNCTION", + conflicts_with = "exclude_function" + )] + pub include_function: Vec, + + /// If specified, only autoverify functions that do not match this filter. This option can be provided + /// multiple times, which will verify all functions that do not match any of the filters. + /// Note that this filter will match against partial names, i.e., providing the name of a module will exclude all functions from that module. + #[arg(long = "exclude-function", num_args(1), value_name = "FUNCTION")] + 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. +} /// Automatically verify functions in a crate. #[derive(Debug, Parser)] pub struct CargoAutoverifyArgs { + #[command(flatten)] + pub common_autoverify_args: CommonAutoverifyArgs, + #[command(flatten)] pub verify_opts: VerificationArgs, } @@ -28,6 +51,9 @@ pub struct StandaloneAutoverifyArgs { #[arg(long, hide = true)] pub crate_name: Option, + #[command(flatten)] + pub common_autoverify_args: CommonAutoverifyArgs, + #[command(flatten)] pub verify_opts: VerificationArgs, } diff --git a/kani-driver/src/assess/mod.rs b/kani-driver/src/assess/mod.rs index ec91918ac8b5..02b3da0974f8 100644 --- a/kani-driver/src/assess/mod.rs +++ b/kani-driver/src/assess/mod.rs @@ -53,7 +53,7 @@ fn assess_project(mut session: KaniSession) -> Result { session.args.jobs = Some(None); // -j, num_cpu } - let project = project::cargo_project(&session, true)?; + let project = project::cargo_project(&mut session, true)?; let cargo_metadata = project.cargo_metadata.as_ref().expect("built with cargo"); let packages_metadata = diff --git a/kani-driver/src/autoverify/mod.rs b/kani-driver/src/autoverify/mod.rs index 82a5372402f0..1f20534caa24 100644 --- a/kani-driver/src/autoverify/mod.rs +++ b/kani-driver/src/autoverify/mod.rs @@ -2,6 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use crate::call_cbmc::VerificationStatus; +use crate::call_single_file::to_rustc_arg; use crate::harness_runner::HarnessResult; use crate::session::KaniSession; use anyhow::Result; @@ -12,6 +13,18 @@ impl KaniSession { self.auto_verify = true; } + /// Add the compiler arguments specific to the `autoverify` subcommand. + pub fn add_auto_verify_args(&mut self, included: Vec, excluded: Vec) { + for func in included { + self.pkg_args + .push(to_rustc_arg(vec![format!("--autoverify-include-function {}", func)])); + } + for func in excluded { + self.pkg_args + .push(to_rustc_arg(vec![format!("--autoverify-exclude-function {}", func)])); + } + } + /// Prints the results from running the `autoverify` subcommand. pub fn print_autoverify_summary(&self, automatic: Vec<&HarnessResult<'_>>) -> Result<()> { let (successes, failures): (Vec<_>, Vec<_>) = diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index 0bc716115989..4c39b03183b6 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -126,7 +126,7 @@ crate-type = ["lib"] } /// Calls `cargo_build` to generate `*.symtab.json` files in `target_dir` - pub fn cargo_build(&self, keep_going: bool) -> Result { + pub fn cargo_build(&mut self, keep_going: bool) -> Result { let build_target = env!("TARGET"); // see build.rs let metadata = self.cargo_metadata(build_target)?; let target_dir = self @@ -183,13 +183,12 @@ crate-type = ["lib"] } // Arguments that will only be passed to the target package. - let mut pkg_args: Vec = vec![]; - pkg_args.extend(["--".to_string(), self.reachability_arg()]); + self.pkg_args.push(self.reachability_arg()); if let Some(backend_arg) = self.backend_arg() { - pkg_args.push(backend_arg); + self.pkg_args.push(backend_arg); } if self.args.no_assert_contracts { - pkg_args.push("--no-assert-contracts".into()); + self.pkg_args.push("--no-assert-contracts".into()); } let mut found_target = false; @@ -202,7 +201,7 @@ crate-type = ["lib"] cmd.args(&cargo_args) .args(vec!["-p", &package.id.to_string()]) .args(verification_target.to_args()) - .args(&pkg_args) + .args(&self.pkg_args) .env("RUSTC", &self.kani_compiler) // Use CARGO_ENCODED_RUSTFLAGS instead of RUSTFLAGS is preferred. See // https://doc.rust-lang.org/cargo/reference/environment-variables.html diff --git a/kani-driver/src/list/collect_metadata.rs b/kani-driver/src/list/collect_metadata.rs index a7901e997ab1..588cab0b63af 100644 --- a/kani-driver/src/list/collect_metadata.rs +++ b/kani-driver/src/list/collect_metadata.rs @@ -78,12 +78,12 @@ fn process_metadata(metadata: Vec) -> ListMetadata { pub fn list_cargo(args: CargoListArgs, mut verify_opts: VerificationArgs) -> Result<()> { let quiet = args.common_args.quiet; verify_opts.common_args = args.common_args; - let session = KaniSession::new(verify_opts)?; + let mut session = KaniSession::new(verify_opts)?; if !quiet { print_kani_version(InvocationType::CargoKani(vec![])); } - let project = cargo_project(&session, false)?; + let project = cargo_project(&mut session, false)?; let list_metadata = process_metadata(project.metadata); output_list_results(list_metadata, args.format, quiet) diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index 8618977ee4d0..59eaebe16aa6 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -73,7 +73,7 @@ fn cargokani_main(input_args: Vec) -> Result<()> { return list_cargo(*list_args, args.verify_opts); } - let session = match args.command { + let mut session = match args.command { Some(CargoKaniSubcommand::Assess(assess_args)) => { let sess = session::KaniSession::new(args.verify_opts)?; return assess::run_assess(sess, *assess_args); @@ -81,6 +81,11 @@ fn cargokani_main(input_args: Vec) -> Result<()> { Some(CargoKaniSubcommand::Autoverify(args)) => { let mut sess = session::KaniSession::new(args.verify_opts)?; sess.enable_autoverify(); + sess.add_auto_verify_args( + args.common_autoverify_args.include_function, + args.common_autoverify_args.exclude_function, + ); + sess } Some(CargoKaniSubcommand::Playback(args)) => { @@ -98,7 +103,7 @@ fn cargokani_main(input_args: Vec) -> Result<()> { return assess::run_assess(session, assess::AssessArgs::default()); } - let project = project::cargo_project(&session, false)?; + let project = project::cargo_project(&mut session, false)?; if session.args.only_codegen { Ok(()) } else { verify_project(project, session) } } @@ -111,6 +116,10 @@ fn standalone_main() -> Result<()> { Some(StandaloneSubcommand::Autoverify(args)) => { let mut session = KaniSession::new(args.verify_opts)?; session.enable_autoverify(); + session.add_auto_verify_args( + args.common_autoverify_args.include_function, + args.common_autoverify_args.exclude_function, + ); if !session.args.common_args.quiet { print_kani_version(InvocationType::Standalone); diff --git a/kani-driver/src/project.rs b/kani-driver/src/project.rs index da04cc0517ba..2a1aad2c1eff 100644 --- a/kani-driver/src/project.rs +++ b/kani-driver/src/project.rs @@ -175,7 +175,7 @@ impl Artifact { /// Generate a project using `cargo`. /// Accept a boolean to build as many targets as possible. The number of failures in that case can /// be collected from the project. -pub fn cargo_project(session: &KaniSession, keep_going: bool) -> Result { +pub fn cargo_project(session: &mut KaniSession, keep_going: bool) -> Result { let outputs = session.cargo_build(keep_going)?; let outdir = outputs.outdir.canonicalize()?; // For the MIR Linker we know there is only one metadata per crate. Use that in our favor. diff --git a/kani-driver/src/session.rs b/kani-driver/src/session.rs index 719c98d10ce2..9398969a9832 100644 --- a/kani-driver/src/session.rs +++ b/kani-driver/src/session.rs @@ -34,6 +34,9 @@ pub struct KaniSession { /// Automatically verify functions in the crate, in addition to running manual harnesses. pub auto_verify: bool, + /// The arguments that will be passed to the target package, i.e. kani_compiler. + pub pkg_args: Vec, + /// Include all publicly-visible symbols in the generated goto binary, not just those reachable from /// a proof harness. Useful when attempting to verify things that were not annotated with kani /// proof attributes. @@ -69,6 +72,7 @@ impl KaniSession { Ok(KaniSession { args, auto_verify: false, + pkg_args: vec!["--".to_string()], codegen_tests: false, kani_compiler: install.kani_compiler()?, kani_lib_c: install.kani_lib_c()?, diff --git a/tests/script-based-pre/cargo_autoverify_exclude/Cargo.toml b/tests/script-based-pre/cargo_autoverify_exclude/Cargo.toml new file mode 100644 index 000000000000..b27dd09bd126 --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_exclude/Cargo.toml @@ -0,0 +1,7 @@ +[package] +name = "cargo_autoverify_include" +version = "0.1.0" +edition = "2024" + +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } diff --git a/tests/script-based-pre/cargo_autoverify_exclude/config.yml b/tests/script-based-pre/cargo_autoverify_exclude/config.yml new file mode 100644 index 000000000000..d3c26a0301f4 --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_exclude/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: exclude.sh +expected: exclude.expected diff --git a/tests/script-based-pre/cargo_autoverify_exclude/exclude.expected b/tests/script-based-pre/cargo_autoverify_exclude/exclude.expected new file mode 100644 index 000000000000..b093236133a1 --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_exclude/exclude.expected @@ -0,0 +1,4 @@ +Autoverify: Checking function include::simple against all possible inputs... +VERIFICATION:- SUCCESSFUL +Verification succeeded for - include::simple +Complete - 1 successfully verified functions, 0 failures, 1 total. \ No newline at end of file diff --git a/tests/script-based-pre/cargo_autoverify_exclude/exclude.sh b/tests/script-based-pre/cargo_autoverify_exclude/exclude.sh new file mode 100755 index 000000000000..31d3b54e2725 --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_exclude/exclude.sh @@ -0,0 +1,5 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +cargo kani autoverify -Z unstable-options --exclude-function exclude diff --git a/tests/script-based-pre/cargo_autoverify_exclude/src/lib.rs b/tests/script-based-pre/cargo_autoverify_exclude/src/lib.rs new file mode 100644 index 000000000000..7757239126c0 --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_exclude/src/lib.rs @@ -0,0 +1,23 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Test that the automatic harness generation feature selects functions correctly +// when --exclude-function is provided. + +mod include { + fn simple(x: u8, _y: u16) -> u8 { + x + } + + // Doesn't implement Arbitrary, so still should not be included. + fn generic(x: u32, _y: T) -> u32 { + x + } +} + +// These functions are eligible for autoverification, but are excluded. +mod excluded { + fn simple(x: u8, _y: u16) -> u8 { + x + } +} diff --git a/tests/script-based-pre/cargo_autoverify_include/Cargo.toml b/tests/script-based-pre/cargo_autoverify_include/Cargo.toml new file mode 100644 index 000000000000..b27dd09bd126 --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_include/Cargo.toml @@ -0,0 +1,7 @@ +[package] +name = "cargo_autoverify_include" +version = "0.1.0" +edition = "2024" + +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } diff --git a/tests/script-based-pre/cargo_autoverify_include/config.yml b/tests/script-based-pre/cargo_autoverify_include/config.yml new file mode 100644 index 000000000000..8df48ec69865 --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_include/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: include.sh +expected: include.expected diff --git a/tests/script-based-pre/cargo_autoverify_include/include.expected b/tests/script-based-pre/cargo_autoverify_include/include.expected new file mode 100644 index 000000000000..b093236133a1 --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_include/include.expected @@ -0,0 +1,4 @@ +Autoverify: Checking function include::simple against all possible inputs... +VERIFICATION:- SUCCESSFUL +Verification succeeded for - include::simple +Complete - 1 successfully verified functions, 0 failures, 1 total. \ No newline at end of file diff --git a/tests/script-based-pre/cargo_autoverify_include/include.sh b/tests/script-based-pre/cargo_autoverify_include/include.sh new file mode 100755 index 000000000000..040a246290dd --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_include/include.sh @@ -0,0 +1,5 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +cargo kani autoverify -Z unstable-options --include-function include diff --git a/tests/script-based-pre/cargo_autoverify_include/src/lib.rs b/tests/script-based-pre/cargo_autoverify_include/src/lib.rs new file mode 100644 index 000000000000..68b30bf7afe8 --- /dev/null +++ b/tests/script-based-pre/cargo_autoverify_include/src/lib.rs @@ -0,0 +1,24 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Test that the automatic harness generation feature selects functions correctly +// when --include-function is provided. + +// Each function inside this module matches the filter. +mod include { + fn simple(x: u8, _y: u16) -> u8 { + x + } + + // Doesn't implement Arbitrary, so still should not be included. + fn generic(x: u32, _y: T) -> u32 { + x + } +} + +// These functions are eligible for autoverification, but do not match the filter. +mod excluded { + fn simple(x: u8, _y: u16) -> u8 { + x + } +} From bfeac3b907f7767754e776a818983c7a1d751375 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 4 Feb 2025 11:31:49 -0500 Subject: [PATCH 05/12] don't let --harness affect automatic harnesses --- kani-driver/src/autoverify/mod.rs | 5 +++-- kani-driver/src/metadata.rs | 4 ++++ 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/kani-driver/src/autoverify/mod.rs b/kani-driver/src/autoverify/mod.rs index 1f20534caa24..99bc97b9a05f 100644 --- a/kani-driver/src/autoverify/mod.rs +++ b/kani-driver/src/autoverify/mod.rs @@ -58,8 +58,9 @@ impl KaniSession { "Complete - {succeeding} successfully verified functions, {failing} failures, {total} total." ); } else { - println!(" - No functions were eligible for automatic verification. Functions can only be automatically verified if each of their arguments implement kani::Arbitrary."); + println!( + "No functions were eligible for automatic verification. Functions can only be automatically verified if each of their arguments implement kani::Arbitrary." + ); println!( "If you specified --include-function or --exclude-function, make sure that your filters were not overly restrictive." ); diff --git a/kani-driver/src/metadata.rs b/kani-driver/src/metadata.rs index 94a5393408d3..bd6556f8068c 100644 --- a/kani-driver/src/metadata.rs +++ b/kani-driver/src/metadata.rs @@ -176,6 +176,10 @@ fn find_proof_harnesses<'a>( debug!(?targets, "find_proof_harness"); let mut result = vec![]; for md in all_harnesses.iter() { + // --harnesses should not select automatic harnesses + if md.is_automatically_generated { + continue; + } if exact_filter { // Check for exact match only if targets.contains(&md.pretty_name) { From 15e172fe13023c67ba51584da413070b447f4235 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 4 Feb 2025 12:10:49 -0500 Subject: [PATCH 06/12] Don't filter out functions with empty bodies We approximated an empty body by checking for TerminatorKind::Return in the first basic block, but it turns out some identity functions have this MIR as well, so remove it. One could argue that identity functions aren't worth checking either, but we'd rather check more than less for now. --- kani-compiler/src/kani_middle/codegen_units.rs | 8 -------- .../cargo_autoverify_filter/filter.expected | 5 ++++- .../cargo_autoverify_filter/src/lib.rs | 11 ++++------- 3 files changed, 8 insertions(+), 16 deletions(-) diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 62d089be6b21..5298c675ad95 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -353,12 +353,6 @@ fn is_eligible_for_automatic_harness(tcx: TyCtxt, instance: Instance, any_inst: return false; } let body = instance.body().unwrap(); - if body.blocks.is_empty() - || (body.blocks[0].statements.is_empty() - && matches!(body.blocks[0].terminator.kind, TerminatorKind::Return)) - { - return false; - } // `instance` is ineligble if it is an associated item of a Kani trait implementation, // or part of Kani contract instrumentation. @@ -373,8 +367,6 @@ fn is_eligible_for_automatic_harness(tcx: TyCtxt, instance: Instance, any_inst: } // Each non-generic argument of `instance`` must implement Arbitrary. - // FIXME -- this is sound but not complete, since it will only work for types whose Arbitrary - // implementations have an inner call to kani::any, which not all implementations (e.g. PhantomPinned) do. body.arg_locals().iter().all(|arg| { let kani_any_body = Instance::resolve(any_inst, &GenericArgs(vec![GenericArgKind::Type(arg.ty)])) diff --git a/tests/script-based-pre/cargo_autoverify_filter/filter.expected b/tests/script-based-pre/cargo_autoverify_filter/filter.expected index 879c40eed631..120a7f158b38 100644 --- a/tests/script-based-pre/cargo_autoverify_filter/filter.expected +++ b/tests/script-based-pre/cargo_autoverify_filter/filter.expected @@ -37,4 +37,7 @@ Autoverify: Checking function yes_harness::f_unsupported_return_type against all Autoverify: Checking function yes_harness::f_multiple_args against all possible inputs... Autoverify: Checking function yes_harness::f_derives_arbitrary against all possible inputs... Autoverify: Checking function yes_harness::f_manually_implements_arbitrary against all possible inputs... -Complete - 39 successfully verified functions, 0 failures, 39 total. \ No newline at end of file +Autoverify: Checking function yes_harness::f_phantom_data against all possible inputs... +Autoverify: Checking function yes_harness::f_phantom_pinned against all possible inputs... +Autoverify: Checking function yes_harness::empty_body against all possible inputs... +Complete - 42 successfully verified functions, 0 failures, 42 total. \ No newline at end of file diff --git a/tests/script-based-pre/cargo_autoverify_filter/src/lib.rs b/tests/script-based-pre/cargo_autoverify_filter/src/lib.rs index 14b77eb88e9f..bb278c73a2e7 100644 --- a/tests/script-based-pre/cargo_autoverify_filter/src/lib.rs +++ b/tests/script-based-pre/cargo_autoverify_filter/src/lib.rs @@ -39,6 +39,7 @@ struct DoesntImplementArbitrary { mod yes_harness { use crate::{DerivesArbitrary, ManuallyImplementsArbitrary}; + use std::marker::{PhantomData, PhantomPinned}; use std::mem::MaybeUninit; use std::num::NonZero; @@ -168,24 +169,20 @@ mod yes_harness { ) -> ManuallyImplementsArbitrary { x } -} -// These should have harnesses, but do not because we assume that every Arbitrary implementation -// will have an internal call to kani::Arbitrary::any, which these implementations do not. -mod fixme { - use std::marker::{PhantomData, PhantomPinned}; fn f_phantom_data(x: PhantomData) -> PhantomData { x } + fn f_phantom_pinned(x: PhantomPinned) -> PhantomPinned { x } + + fn empty_body(_x: u8, _y: u16) {} } mod no_harness { use crate::{DerivesArbitrary, DoesntImplementArbitrary}; - - fn empty_body(_x: u8, _y: u16) {} fn unsupported_generic(x: u32, _y: T) -> u32 { x } From eaab5cfafeb9df4e1f5eb2f91ebfbecea0010157 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 4 Feb 2025 13:20:38 -0500 Subject: [PATCH 07/12] add chapter to book --- docs/src/SUMMARY.md | 1 + docs/src/reference/experimental/autoverify.md | 81 +++++++++++++++++++ 2 files changed, 82 insertions(+) create mode 100644 docs/src/reference/experimental/autoverify.md diff --git a/docs/src/SUMMARY.md b/docs/src/SUMMARY.md index d534cf1f7f22..e8b8e933c353 100644 --- a/docs/src/SUMMARY.md +++ b/docs/src/SUMMARY.md @@ -18,6 +18,7 @@ - [Reference](./reference.md) - [Attributes](./reference/attributes.md) - [Experimental features](./reference/experimental/experimental-features.md) + - [Automatic Verification](./reference/experimental/autoverify.md) - [Coverage](./reference/experimental/coverage.md) - [Stubbing](./reference/experimental/stubbing.md) - [Contracts](./reference/experimental/contracts.md) diff --git a/docs/src/reference/experimental/autoverify.md b/docs/src/reference/experimental/autoverify.md new file mode 100644 index 000000000000..40e0ad7ff8ca --- /dev/null +++ b/docs/src/reference/experimental/autoverify.md @@ -0,0 +1,81 @@ +# Automatic Verification + +Recall the harness for `estimate_size` that we wrote in [First Steps](../../tutorial-first-steps.md): +```rust +{{#include ../../tutorial/first-steps-v1/src/lib.rs:kani}} +``` + +This harness first declares a local variable `x` using `kani::any()`, then calls `estimate_size` with argument `x`. +Many proof harnesses follow this predictable format—to verify a function `foo`, we create arbitrary values for each of `foo`'s arguments, then call `foo` on those arguments. + +The `autoverify` feature scans a crate for functions whose arguments all implement the `kani::Arbitrary` trait, and then verifies those functions for you automatically. + +## Usage +Run either: +``` +# cargo kani autoverify -Z unstable-options +``` +or +``` +# kani autoverify -Z unstable-options +``` + +If Kani detects that all of a function `foo`'s arguments implement `kani::Arbitrary`, it will generate and run a `#[kani::proof]` harness, which prints: + +``` +Autoverify: Checking function foo against all possible inputs... + +``` + +However, if Kani detects that `foo` has a [contract](./contracts.md), it will instead generate a `#[kani::proof_for_contract]` harness and verify the contract: +``` +Autoverify: Checking function foo's contract against all possible inputs... + +``` + +Kani generates and runs these harnesses internally—the user never sees them. + +The `autoverify` subcommand has options `--include-function` and `--exclude-function` to include and exclude particular functions from autoverification. +These flags look for partial matches against the fully qualified name of a function. + +For example, if a module `my_module` has many functions, but we are only interested in `my_module::foo` and `my_module::bar`, we can run: +``` +cargo run autoverify -Z unstable-options --include-function foo include-function bar +``` +To exclude `my_module` from autoverification entirely, run: +``` +cargo run autoverify -Z unstable-options --exclude-function my_module +``` + +## Example +Using the `estimate_size` example from [First Steps](../../tutorial-first-steps.md) again: +```rust +{{#include ../../tutorial/first-steps-v1/src/lib.rs:code}} +``` + +We get: + +``` +# cargo kani autoverify -Z unstable-options +Autoverify: Checking function estimate_size against all possible inputs... +RESULTS: +Check 3: estimate_size.assertion.1 + - Status: FAILURE + - Description: "Oh no, a failing corner case!" +[...] + +Verification failed for - estimate_size +Complete - 0 successfully verified functions, 1 failures, 1 total. +``` + +## Request for comments +This feature is experimental and is therefore subject to change. +If you have ideas for improving the user experience of this feature, +please add them to [this GitHub issue](https://github.com/model-checking/kani/issues/3832). + +## Limitations +Kani will only autoverify a function if it can determine that all of the function's arguments implement Arbitrary. +It does not attempt to derive/implement Arbitrary for any types, even if those types could implement Arbitrary. +If a function contains a loop with a loop contract, Kani will detect the presence of a loop contract and verify that contract. +If, however, the loop does not have a contract, then there is currently no way to specify an unwinding bound for the function, meaning that Kani may hang as it tries to unwind the loop. +We recommend using the `--exclude-function` option to exclude any functions that have this issue (or `--harness-timeout` to bail after attempting verification for some amount of time). \ No newline at end of file From bfebfdbdf612cf4dc7d61952c1b29e396f93eb38 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 4 Feb 2025 15:28:35 -0500 Subject: [PATCH 08/12] fix formatting & regression failures --- .../src/kani_middle/codegen_units.rs | 4 +- kani-driver/src/args/autoverify_args.rs | 4 +- kani-driver/src/harness_runner.rs | 38 ++++++++++--------- kani-driver/src/metadata.rs | 1 + .../cargo_autoverify_contracts/Cargo.toml | 3 ++ .../cargo_autoverify_exclude/Cargo.toml | 3 ++ .../cargo_autoverify_filter/Cargo.toml | 3 ++ .../Cargo.toml | 3 ++ .../cargo_autoverify_include/Cargo.toml | 3 ++ .../cargo_autoverify_loops_fixme/Cargo.toml | 3 ++ 10 files changed, 43 insertions(+), 22 deletions(-) diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 5298c675ad95..6bfc681ab1c1 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -104,8 +104,8 @@ impl CodegenUnits { // and these harnesses have no stubs. units.extend( automatic_harnesses - .iter() - .map(|(harness, _)| CodegenUnit { + .keys() + .map(|harness| CodegenUnit { harnesses: vec![*harness], stubs: HashMap::default(), }) diff --git a/kani-driver/src/args/autoverify_args.rs b/kani-driver/src/args/autoverify_args.rs index f6731ca94e04..9b2ad1b3d6c9 100644 --- a/kani-driver/src/args/autoverify_args.rs +++ b/kani-driver/src/args/autoverify_args.rs @@ -71,7 +71,7 @@ impl ValidateArgs for CargoAutoverifyArgs { ErrorKind::MissingRequiredArgument, format!( "The `autoverify` subcommand is unstable and requires -Z {}", - UnstableFeature::UnstableOptions.to_string() + UnstableFeature::UnstableOptions ), )); } @@ -105,7 +105,7 @@ impl ValidateArgs for StandaloneAutoverifyArgs { ErrorKind::MissingRequiredArgument, format!( "The `autoverify` subcommand is unstable and requires -Z {}", - UnstableFeature::UnstableOptions.to_string() + UnstableFeature::UnstableOptions ), )); } diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index a567467e85af..e80351feb713 100644 --- a/kani-driver/src/harness_runner.rs +++ b/kani-driver/src/harness_runner.rs @@ -167,29 +167,31 @@ impl KaniSession { harness: &HarnessMetadata, ) -> Result { let thread_index = rayon::current_thread_index().unwrap_or_default(); - // If the harness is automatically generated, pretty_name refers to the function under verification. - let mut msg = if harness.is_automatically_generated { - if matches!(harness.attributes.kind, HarnessKind::Proof) { - format!( - "Autoverify: Checking function {} against all possible inputs...", - harness.pretty_name - ) + if !self.args.common_args.quiet { + // If the harness is automatically generated, pretty_name refers to the function under verification. + let mut msg = if harness.is_automatically_generated { + if matches!(harness.attributes.kind, HarnessKind::Proof) { + format!( + "Autoverify: Checking function {} against all possible inputs...", + harness.pretty_name + ) + } else { + format!( + "Autoverify: Checking function {}'s contract against all possible inputs...", + harness.pretty_name + ) + } } else { - format!( - "Autoverify: Checking function {}'s contract against all possible inputs...", - harness.pretty_name - ) + format!("Checking harness {}...", harness.pretty_name) + }; + + if rayon::current_num_threads() > 1 { + msg = format!("Thread {thread_index}: {msg}"); } - } else { - format!("Checking harness {}...", harness.pretty_name) - }; - if rayon::current_num_threads() > 1 { - msg = format!("Thread {thread_index}: {msg}"); + println!("{msg}"); } - println!("{msg}"); - let mut result = self.with_timer(|| self.run_cbmc(binary, harness), "run_cbmc")?; self.process_output(&result, harness, thread_index); diff --git a/kani-driver/src/metadata.rs b/kani-driver/src/metadata.rs index bd6556f8068c..d112591c6532 100644 --- a/kani-driver/src/metadata.rs +++ b/kani-driver/src/metadata.rs @@ -228,6 +228,7 @@ pub mod tests { goto_file: model_file, contract: Default::default(), has_loop_contracts: false, + is_automatically_generated: false, } } diff --git a/tests/script-based-pre/cargo_autoverify_contracts/Cargo.toml b/tests/script-based-pre/cargo_autoverify_contracts/Cargo.toml index be3a32bdca8f..6ac7ea38e31e 100644 --- a/tests/script-based-pre/cargo_autoverify_contracts/Cargo.toml +++ b/tests/script-based-pre/cargo_autoverify_contracts/Cargo.toml @@ -1,3 +1,6 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + [package] name = "cargo_autoverify_contracts" version = "0.1.0" diff --git a/tests/script-based-pre/cargo_autoverify_exclude/Cargo.toml b/tests/script-based-pre/cargo_autoverify_exclude/Cargo.toml index b27dd09bd126..5d8e213cc1bf 100644 --- a/tests/script-based-pre/cargo_autoverify_exclude/Cargo.toml +++ b/tests/script-based-pre/cargo_autoverify_exclude/Cargo.toml @@ -1,3 +1,6 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + [package] name = "cargo_autoverify_include" version = "0.1.0" diff --git a/tests/script-based-pre/cargo_autoverify_filter/Cargo.toml b/tests/script-based-pre/cargo_autoverify_filter/Cargo.toml index db41718a0ec0..386df028de57 100644 --- a/tests/script-based-pre/cargo_autoverify_filter/Cargo.toml +++ b/tests/script-based-pre/cargo_autoverify_filter/Cargo.toml @@ -1,3 +1,6 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + [package] name = "cargo_autoverify_filter" version = "0.1.0" diff --git a/tests/script-based-pre/cargo_autoverify_harnesses_fail/Cargo.toml b/tests/script-based-pre/cargo_autoverify_harnesses_fail/Cargo.toml index 7c1fdab9efb3..122823173023 100644 --- a/tests/script-based-pre/cargo_autoverify_harnesses_fail/Cargo.toml +++ b/tests/script-based-pre/cargo_autoverify_harnesses_fail/Cargo.toml @@ -1,3 +1,6 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + [package] name = "cargo_autoverify_harnesses_fail" version = "0.1.0" diff --git a/tests/script-based-pre/cargo_autoverify_include/Cargo.toml b/tests/script-based-pre/cargo_autoverify_include/Cargo.toml index b27dd09bd126..5d8e213cc1bf 100644 --- a/tests/script-based-pre/cargo_autoverify_include/Cargo.toml +++ b/tests/script-based-pre/cargo_autoverify_include/Cargo.toml @@ -1,3 +1,6 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + [package] name = "cargo_autoverify_include" version = "0.1.0" diff --git a/tests/script-based-pre/cargo_autoverify_loops_fixme/Cargo.toml b/tests/script-based-pre/cargo_autoverify_loops_fixme/Cargo.toml index 63555fbe95b9..1b4a9a4acae1 100644 --- a/tests/script-based-pre/cargo_autoverify_loops_fixme/Cargo.toml +++ b/tests/script-based-pre/cargo_autoverify_loops_fixme/Cargo.toml @@ -1,3 +1,6 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + [package] name = "cargo_autoverify_loops_fixme" version = "0.1.0" From ec674e8a47c93915fa7fdc2671396911dc057fcc Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Wed, 5 Feb 2025 20:00:29 -0500 Subject: [PATCH 09/12] change subcommand name to autoharness --- docs/src/SUMMARY.md | 2 +- .../{autoverify.md => autoharness.md} | 22 +++++----- kani-compiler/src/args.rs | 12 +++--- .../src/kani_middle/codegen_units.rs | 8 ++-- ...autoverify_args.rs => autoharness_args.rs} | 28 ++++++------ kani-driver/src/args/mod.rs | 10 ++--- .../src/{autoverify => autoharness}/mod.rs | 22 +++++----- kani-driver/src/harness_runner.rs | 8 ++-- kani-driver/src/main.rs | 22 +++++----- kani-driver/src/session.rs | 6 +-- .../Cargo.toml | 2 +- .../config.yml | 0 .../contracts.expected | 10 ++--- .../contracts.sh | 2 +- .../src/lib.rs | 4 +- .../Cargo.toml | 2 +- .../config.yml | 0 .../exclude.expected | 2 +- .../exclude.sh | 2 +- .../src/lib.rs | 0 .../Cargo.toml | 2 +- .../config.yml | 0 .../cargo_autoharness_filter/filter.expected | 43 +++++++++++++++++++ .../filter.sh | 2 +- .../src/lib.rs | 0 .../Cargo.toml | 2 +- .../config.yml | 0 .../harnesses_fail.expected | 10 ++--- .../harnesses_fail.sh | 2 +- .../src/lib.rs | 2 +- .../Cargo.toml | 2 +- .../config.yml | 0 .../include.expected | 2 +- .../include.sh | 2 +- .../src/lib.rs | 0 .../cargo_autoharness_loops_fixme/Cargo.toml | 10 +++++ .../config.yml | 0 .../loops.sh | 2 +- .../src/lib.rs | 0 .../cargo_autoverify_filter/filter.expected | 43 ------------------- .../cargo_autoverify_loops_fixme/Cargo.toml | 10 ----- 41 files changed, 149 insertions(+), 149 deletions(-) rename docs/src/reference/experimental/{autoverify.md => autoharness.md} (74%) rename kani-driver/src/args/{autoverify_args.rs => autoharness_args.rs} (80%) rename kani-driver/src/{autoverify => autoharness}/mod.rs (72%) rename tests/script-based-pre/{cargo_autoverify_contracts => cargo_autoharness_contracts}/Cargo.toml (84%) rename tests/script-based-pre/{cargo_autoverify_contracts => cargo_autoharness_contracts}/config.yml (100%) rename tests/script-based-pre/{cargo_autoverify_contracts => cargo_autoharness_contracts}/contracts.expected (60%) rename tests/script-based-pre/{cargo_autoverify_contracts => cargo_autoharness_contracts}/contracts.sh (81%) rename tests/script-based-pre/{cargo_autoverify_contracts => cargo_autoharness_contracts}/src/lib.rs (89%) rename tests/script-based-pre/{cargo_autoverify_include => cargo_autoharness_exclude}/Cargo.toml (85%) rename tests/script-based-pre/{cargo_autoverify_exclude => cargo_autoharness_exclude}/config.yml (100%) rename tests/script-based-pre/{cargo_autoverify_exclude => cargo_autoharness_exclude}/exclude.expected (63%) rename tests/script-based-pre/{cargo_autoverify_exclude => cargo_autoharness_exclude}/exclude.sh (57%) rename tests/script-based-pre/{cargo_autoverify_exclude => cargo_autoharness_exclude}/src/lib.rs (100%) rename tests/script-based-pre/{cargo_autoverify_exclude => cargo_autoharness_filter}/Cargo.toml (85%) rename tests/script-based-pre/{cargo_autoverify_filter => cargo_autoharness_filter}/config.yml (100%) create mode 100644 tests/script-based-pre/cargo_autoharness_filter/filter.expected rename tests/script-based-pre/{cargo_autoverify_filter => cargo_autoharness_filter}/filter.sh (69%) rename tests/script-based-pre/{cargo_autoverify_filter => cargo_autoharness_filter}/src/lib.rs (100%) rename tests/script-based-pre/{cargo_autoverify_harnesses_fail => cargo_autoharness_harnesses_fail}/Cargo.toml (82%) rename tests/script-based-pre/{cargo_autoverify_harnesses_fail => cargo_autoharness_harnesses_fail}/config.yml (100%) rename tests/script-based-pre/{cargo_autoverify_harnesses_fail => cargo_autoharness_harnesses_fail}/harnesses_fail.expected (80%) rename tests/script-based-pre/{cargo_autoverify_harnesses_fail => cargo_autoharness_harnesses_fail}/harnesses_fail.sh (89%) rename tests/script-based-pre/{cargo_autoverify_harnesses_fail => cargo_autoharness_harnesses_fail}/src/lib.rs (95%) rename tests/script-based-pre/{cargo_autoverify_filter => cargo_autoharness_include}/Cargo.toml (85%) rename tests/script-based-pre/{cargo_autoverify_include => cargo_autoharness_include}/config.yml (100%) rename tests/script-based-pre/{cargo_autoverify_include => cargo_autoharness_include}/include.expected (63%) rename tests/script-based-pre/{cargo_autoverify_include => cargo_autoharness_include}/include.sh (57%) rename tests/script-based-pre/{cargo_autoverify_include => cargo_autoharness_include}/src/lib.rs (100%) create mode 100644 tests/script-based-pre/cargo_autoharness_loops_fixme/Cargo.toml rename tests/script-based-pre/{cargo_autoverify_loops_fixme => cargo_autoharness_loops_fixme}/config.yml (100%) rename tests/script-based-pre/{cargo_autoverify_loops_fixme => cargo_autoharness_loops_fixme}/loops.sh (69%) rename tests/script-based-pre/{cargo_autoverify_loops_fixme => cargo_autoharness_loops_fixme}/src/lib.rs (100%) delete mode 100644 tests/script-based-pre/cargo_autoverify_filter/filter.expected delete mode 100644 tests/script-based-pre/cargo_autoverify_loops_fixme/Cargo.toml diff --git a/docs/src/SUMMARY.md b/docs/src/SUMMARY.md index e8b8e933c353..2bcdea7c4c2f 100644 --- a/docs/src/SUMMARY.md +++ b/docs/src/SUMMARY.md @@ -18,7 +18,7 @@ - [Reference](./reference.md) - [Attributes](./reference/attributes.md) - [Experimental features](./reference/experimental/experimental-features.md) - - [Automatic Verification](./reference/experimental/autoverify.md) + - [Automatic Verification](./reference/experimental/autoharness.md) - [Coverage](./reference/experimental/coverage.md) - [Stubbing](./reference/experimental/stubbing.md) - [Contracts](./reference/experimental/contracts.md) diff --git a/docs/src/reference/experimental/autoverify.md b/docs/src/reference/experimental/autoharness.md similarity index 74% rename from docs/src/reference/experimental/autoverify.md rename to docs/src/reference/experimental/autoharness.md index 40e0ad7ff8ca..5156c9e63956 100644 --- a/docs/src/reference/experimental/autoverify.md +++ b/docs/src/reference/experimental/autoharness.md @@ -8,43 +8,43 @@ Recall the harness for `estimate_size` that we wrote in [First Steps](../../tuto This harness first declares a local variable `x` using `kani::any()`, then calls `estimate_size` with argument `x`. Many proof harnesses follow this predictable format—to verify a function `foo`, we create arbitrary values for each of `foo`'s arguments, then call `foo` on those arguments. -The `autoverify` feature scans a crate for functions whose arguments all implement the `kani::Arbitrary` trait, and then verifies those functions for you automatically. +The `autoharness` feature scans a crate for functions whose arguments all implement the `kani::Arbitrary` trait, and then verifies those functions for you automatically. ## Usage Run either: ``` -# cargo kani autoverify -Z unstable-options +# cargo kani autoharness -Z unstable-options ``` or ``` -# kani autoverify -Z unstable-options +# kani autoharness -Z unstable-options ``` If Kani detects that all of a function `foo`'s arguments implement `kani::Arbitrary`, it will generate and run a `#[kani::proof]` harness, which prints: ``` -Autoverify: Checking function foo against all possible inputs... +Autoharness: Checking function foo against all possible inputs... ``` However, if Kani detects that `foo` has a [contract](./contracts.md), it will instead generate a `#[kani::proof_for_contract]` harness and verify the contract: ``` -Autoverify: Checking function foo's contract against all possible inputs... +Autoharness: Checking function foo's contract against all possible inputs... ``` Kani generates and runs these harnesses internally—the user never sees them. -The `autoverify` subcommand has options `--include-function` and `--exclude-function` to include and exclude particular functions from autoverification. +The `autoharness` subcommand has options `--include-function` and `--exclude-function` to include and exclude particular functions from autoverification. These flags look for partial matches against the fully qualified name of a function. For example, if a module `my_module` has many functions, but we are only interested in `my_module::foo` and `my_module::bar`, we can run: ``` -cargo run autoverify -Z unstable-options --include-function foo include-function bar +cargo run autoharness -Z unstable-options --include-function foo include-function bar ``` To exclude `my_module` from autoverification entirely, run: ``` -cargo run autoverify -Z unstable-options --exclude-function my_module +cargo run autoharness -Z unstable-options --exclude-function my_module ``` ## Example @@ -56,8 +56,8 @@ Using the `estimate_size` example from [First Steps](../../tutorial-first-steps. We get: ``` -# cargo kani autoverify -Z unstable-options -Autoverify: Checking function estimate_size against all possible inputs... +# cargo kani autoharness -Z unstable-options +Autoharness: Checking function estimate_size against all possible inputs... RESULTS: Check 3: estimate_size.assertion.1 - Status: FAILURE @@ -74,7 +74,7 @@ If you have ideas for improving the user experience of this feature, please add them to [this GitHub issue](https://github.com/model-checking/kani/issues/3832). ## Limitations -Kani will only autoverify a function if it can determine that all of the function's arguments implement Arbitrary. +Kani will only autoharness a function if it can determine that all of the function's arguments implement Arbitrary. It does not attempt to derive/implement Arbitrary for any types, even if those types could implement Arbitrary. If a function contains a loop with a loop contract, Kani will detect the presence of a loop contract and verify that contract. If, however, the loop does not have a contract, then there is currently no way to specify an unwinding bound for the function, meaning that Kani may hang as it tries to unwind the loop. diff --git a/kani-compiler/src/args.rs b/kani-compiler/src/args.rs index d93162da005d..92950a8eb409 100644 --- a/kani-compiler/src/args.rs +++ b/kani-compiler/src/args.rs @@ -90,12 +90,12 @@ pub struct Arguments { /// Print the final LLBC file to stdout. #[clap(long)] pub print_llbc: bool, - /// If we are running the autoverify subcommand, the functions to autoverify - #[arg(long = "autoverify-include-function", num_args(1))] - pub autoverify_included_functions: Vec, - /// If we are running the autoverify subcommand, the functions to exclude from autoverification - #[arg(long = "autoverify-exclude-function", num_args(1))] - pub autoverify_excluded_functions: Vec, + /// If we are running the autoharness subcommand, the functions to autoharness + #[arg(long = "autoharness-include-function", num_args(1))] + pub autoharness_included_functions: Vec, + /// If we are running the autoharness subcommand, the functions to exclude from autoverification + #[arg(long = "autoharness-exclude-function", num_args(1))] + pub autoharness_excluded_functions: Vec, } #[derive(Debug, Clone, Copy, AsRefStr, EnumString, VariantNames, PartialEq, Eq)] diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 6bfc681ab1c1..c29dc244d9fe 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -84,10 +84,10 @@ impl CodegenUnits { let verifiable_fns = filter_crate_items(tcx, |_, instance: Instance| -> bool { // If the user specified functions to include or exclude, only allow instances matching those filters. - let user_included = if !args.autoverify_included_functions.is_empty() { - fn_list_contains_instance(&instance, &args.autoverify_included_functions) - } else if !args.autoverify_excluded_functions.is_empty() { - !fn_list_contains_instance(&instance, &args.autoverify_excluded_functions) + let user_included = if !args.autoharness_included_functions.is_empty() { + fn_list_contains_instance(&instance, &args.autoharness_included_functions) + } else if !args.autoharness_excluded_functions.is_empty() { + !fn_list_contains_instance(&instance, &args.autoharness_excluded_functions) } else { true }; diff --git a/kani-driver/src/args/autoverify_args.rs b/kani-driver/src/args/autoharness_args.rs similarity index 80% rename from kani-driver/src/args/autoverify_args.rs rename to kani-driver/src/args/autoharness_args.rs index 9b2ad1b3d6c9..d7a69070bf41 100644 --- a/kani-driver/src/args/autoverify_args.rs +++ b/kani-driver/src/args/autoharness_args.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -//! Implements the subcommand handling of the autoverify subcommand +//! Implements the subcommand handling of the autoharness subcommand use std::path::PathBuf; @@ -9,8 +9,8 @@ use clap::{Error, Parser, error::ErrorKind}; use kani_metadata::UnstableFeature; #[derive(Debug, Parser)] -pub struct CommonAutoverifyArgs { - /// If specified, only autoverify functions that match this filter. This option can be provided +pub struct CommonAutoharnessArgs { + /// If specified, only autoharness functions that match this filter. This option can be provided /// multiple times, which will verify all functions matching any of the filters. /// Note that this filter will match against partial names, i.e., providing the name of a module will include all functions from that module. /// Also note that if the function specified is unable to be automatically verified, this flag will have no effect. @@ -22,7 +22,7 @@ pub struct CommonAutoverifyArgs { )] pub include_function: Vec, - /// If specified, only autoverify functions that do not match this filter. This option can be provided + /// If specified, only autoharness functions that do not match this filter. This option can be provided /// multiple times, which will verify all functions that do not match any of the filters. /// Note that this filter will match against partial names, i.e., providing the name of a module will exclude all functions from that module. #[arg(long = "exclude-function", num_args(1), value_name = "FUNCTION")] @@ -33,9 +33,9 @@ pub struct CommonAutoverifyArgs { /// Automatically verify functions in a crate. #[derive(Debug, Parser)] -pub struct CargoAutoverifyArgs { +pub struct CargoAutoharnessArgs { #[command(flatten)] - pub common_autoverify_args: CommonAutoverifyArgs, + pub common_autoharness_args: CommonAutoharnessArgs, #[command(flatten)] pub verify_opts: VerificationArgs, @@ -43,7 +43,7 @@ pub struct CargoAutoverifyArgs { /// Automatically verify functions in a file. #[derive(Debug, Parser)] -pub struct StandaloneAutoverifyArgs { +pub struct StandaloneAutoharnessArgs { /// Rust crate's top file location. #[arg(required = true)] pub input: PathBuf, @@ -52,13 +52,13 @@ pub struct StandaloneAutoverifyArgs { pub crate_name: Option, #[command(flatten)] - pub common_autoverify_args: CommonAutoverifyArgs, + pub common_autoharness_args: CommonAutoharnessArgs, #[command(flatten)] pub verify_opts: VerificationArgs, } -impl ValidateArgs for CargoAutoverifyArgs { +impl ValidateArgs for CargoAutoharnessArgs { fn validate(&self) -> Result<(), Error> { self.verify_opts.validate()?; if !self @@ -70,7 +70,7 @@ impl ValidateArgs for CargoAutoverifyArgs { return Err(Error::raw( ErrorKind::MissingRequiredArgument, format!( - "The `autoverify` subcommand is unstable and requires -Z {}", + "The `autoharness` subcommand is unstable and requires -Z {}", UnstableFeature::UnstableOptions ), )); @@ -84,7 +84,7 @@ impl ValidateArgs for CargoAutoverifyArgs { { return Err(Error::raw( ErrorKind::ArgumentConflict, - "The autoverify subcommand does not support concrete playback", + "The autoharness subcommand does not support concrete playback", )); } @@ -92,7 +92,7 @@ impl ValidateArgs for CargoAutoverifyArgs { } } -impl ValidateArgs for StandaloneAutoverifyArgs { +impl ValidateArgs for StandaloneAutoharnessArgs { fn validate(&self) -> Result<(), Error> { self.verify_opts.validate()?; if !self @@ -104,7 +104,7 @@ impl ValidateArgs for StandaloneAutoverifyArgs { return Err(Error::raw( ErrorKind::MissingRequiredArgument, format!( - "The `autoverify` subcommand is unstable and requires -Z {}", + "The `autoharness` subcommand is unstable and requires -Z {}", UnstableFeature::UnstableOptions ), )); @@ -127,7 +127,7 @@ impl ValidateArgs for StandaloneAutoverifyArgs { { return Err(Error::raw( ErrorKind::ArgumentConflict, - "The autoverify subcommand does not support concrete playback", + "The autoharness subcommand does not support concrete playback", )); } diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index c3a096b78665..b48fa426a8a6 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -3,7 +3,7 @@ //! Module that define Kani's command line interface. This includes all subcommands. pub mod assess_args; -pub mod autoverify_args; +pub mod autoharness_args; pub mod cargo; pub mod common; pub mod list_args; @@ -147,7 +147,7 @@ pub enum StandaloneSubcommand { /// List contracts and harnesses. List(Box), /// Scan the input file for functions eligible for automatic (i.e., harness-free) verification and verify them. - Autoverify(Box), + Autoharness(Box), } #[derive(Debug, clap::Parser)] @@ -178,7 +178,7 @@ pub enum CargoKaniSubcommand { List(Box), /// Scan the crate for functions eligible for automatic (i.e., harness-free) verification and verify them. - Autoverify(Box), + Autoharness(Box), } // Common arguments for invoking Kani for verification purpose. This gets put into KaniContext, @@ -489,7 +489,7 @@ impl ValidateArgs for StandaloneArgs { match &self.command { Some(StandaloneSubcommand::VerifyStd(args)) => args.validate()?, Some(StandaloneSubcommand::List(args)) => args.validate()?, - Some(StandaloneSubcommand::Autoverify(args)) => args.validate()?, + Some(StandaloneSubcommand::Autoharness(args)) => args.validate()?, // TODO: Invoke PlaybackArgs::validate() None | Some(StandaloneSubcommand::Playback(..)) => {} }; @@ -535,7 +535,7 @@ impl ValidateArgs for CargoKaniSubcommand { match self { // Assess doesn't implement validation yet. CargoKaniSubcommand::Assess(_) => Ok(()), - CargoKaniSubcommand::Autoverify(autoverify) => autoverify.validate(), + CargoKaniSubcommand::Autoharness(autoharness) => autoharness.validate(), CargoKaniSubcommand::Playback(playback) => playback.validate(), CargoKaniSubcommand::List(list) => list.validate(), } diff --git a/kani-driver/src/autoverify/mod.rs b/kani-driver/src/autoharness/mod.rs similarity index 72% rename from kani-driver/src/autoverify/mod.rs rename to kani-driver/src/autoharness/mod.rs index 99bc97b9a05f..69c49580cd77 100644 --- a/kani-driver/src/autoverify/mod.rs +++ b/kani-driver/src/autoharness/mod.rs @@ -8,25 +8,25 @@ use crate::session::KaniSession; use anyhow::Result; impl KaniSession { - /// Enable autoverify mode. - pub fn enable_autoverify(&mut self) { - self.auto_verify = true; + /// Enable autoharness mode. + pub fn enable_autoharness(&mut self) { + self.auto_harness = true; } - /// Add the compiler arguments specific to the `autoverify` subcommand. - pub fn add_auto_verify_args(&mut self, included: Vec, excluded: Vec) { + /// Add the compiler arguments specific to the `autoharness` subcommand. + pub fn add_auto_harness_args(&mut self, included: Vec, excluded: Vec) { for func in included { self.pkg_args - .push(to_rustc_arg(vec![format!("--autoverify-include-function {}", func)])); + .push(to_rustc_arg(vec![format!("--autoharness-include-function {}", func)])); } for func in excluded { self.pkg_args - .push(to_rustc_arg(vec![format!("--autoverify-exclude-function {}", func)])); + .push(to_rustc_arg(vec![format!("--autoharness-exclude-function {}", func)])); } } - /// Prints the results from running the `autoverify` subcommand. - pub fn print_autoverify_summary(&self, automatic: Vec<&HarnessResult<'_>>) -> Result<()> { + /// Prints the results from running the `autoharness` subcommand. + pub fn print_autoharness_summary(&self, automatic: Vec<&HarnessResult<'_>>) -> Result<()> { let (successes, failures): (Vec<_>, Vec<_>) = automatic.into_iter().partition(|r| r.result.status == VerificationStatus::Success); @@ -36,9 +36,9 @@ impl KaniSession { // TODO: it would be nice if we had access to which functions the user included/excluded here // so that we could print a comparison for them of any of the included functions that we skipped. - println!("Autoverify Summary:"); + println!("Autoharness Summary:"); println!( - "Note that Kani will only autoverify a function if it determines that each of its arguments implement the Arbitrary trait." + "Note that Kani will only generate an automatic harness for a function if it determines that each of its arguments implement the Arbitrary trait." ); println!( "Examine the summary closely to determine which functions were automatically verified." diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index e80351feb713..8d71d1acb52c 100644 --- a/kani-driver/src/harness_runner.rs +++ b/kani-driver/src/harness_runner.rs @@ -172,12 +172,12 @@ impl KaniSession { let mut msg = if harness.is_automatically_generated { if matches!(harness.attributes.kind, HarnessKind::Proof) { format!( - "Autoverify: Checking function {} against all possible inputs...", + "Autoharness: Checking function {} against all possible inputs...", harness.pretty_name ) } else { format!( - "Autoverify: Checking function {}'s contract against all possible inputs...", + "Autoharness: Checking function {}'s contract against all possible inputs...", harness.pretty_name ) } @@ -212,8 +212,8 @@ impl KaniSession { let (automatic, manual): (Vec<_>, Vec<_>) = results.iter().partition(|r| r.harness.is_automatically_generated); - if self.auto_verify { - self.print_autoverify_summary(automatic)?; + if self.auto_harness { + self.print_autoharness_summary(automatic)?; } let (successes, failures): (Vec<_>, Vec<_>) = diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index 59eaebe16aa6..9b82c8467e26 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -22,7 +22,7 @@ use tracing::debug; mod args; mod args_toml; mod assess; -mod autoverify; +mod autoharness; mod call_cargo; mod call_cbmc; mod call_goto_cc; @@ -78,12 +78,12 @@ fn cargokani_main(input_args: Vec) -> Result<()> { let sess = session::KaniSession::new(args.verify_opts)?; return assess::run_assess(sess, *assess_args); } - Some(CargoKaniSubcommand::Autoverify(args)) => { + Some(CargoKaniSubcommand::Autoharness(args)) => { let mut sess = session::KaniSession::new(args.verify_opts)?; - sess.enable_autoverify(); - sess.add_auto_verify_args( - args.common_autoverify_args.include_function, - args.common_autoverify_args.exclude_function, + sess.enable_autoharness(); + sess.add_auto_harness_args( + args.common_autoharness_args.include_function, + args.common_autoharness_args.exclude_function, ); sess @@ -113,12 +113,12 @@ fn standalone_main() -> Result<()> { check_is_valid(&args); let (session, project) = match args.command { - Some(StandaloneSubcommand::Autoverify(args)) => { + Some(StandaloneSubcommand::Autoharness(args)) => { let mut session = KaniSession::new(args.verify_opts)?; - session.enable_autoverify(); - session.add_auto_verify_args( - args.common_autoverify_args.include_function, - args.common_autoverify_args.exclude_function, + session.enable_autoharness(); + session.add_auto_harness_args( + args.common_autoharness_args.include_function, + args.common_autoharness_args.exclude_function, ); if !session.args.common_args.quiet { diff --git a/kani-driver/src/session.rs b/kani-driver/src/session.rs index 9398969a9832..7e5df4979688 100644 --- a/kani-driver/src/session.rs +++ b/kani-driver/src/session.rs @@ -32,7 +32,7 @@ pub struct KaniSession { pub args: VerificationArgs, /// Automatically verify functions in the crate, in addition to running manual harnesses. - pub auto_verify: bool, + pub auto_harness: bool, /// The arguments that will be passed to the target package, i.e. kani_compiler. pub pkg_args: Vec, @@ -71,7 +71,7 @@ impl KaniSession { Ok(KaniSession { args, - auto_verify: false, + auto_harness: false, pkg_args: vec!["--".to_string()], codegen_tests: false, kani_compiler: install.kani_compiler()?, @@ -101,7 +101,7 @@ impl KaniSession { pub fn reachability_mode(&self) -> ReachabilityMode { if self.codegen_tests { ReachabilityMode::Tests - } else if self.auto_verify { + } else if self.auto_harness { ReachabilityMode::Automatic } else { ReachabilityMode::ProofHarnesses diff --git a/tests/script-based-pre/cargo_autoverify_contracts/Cargo.toml b/tests/script-based-pre/cargo_autoharness_contracts/Cargo.toml similarity index 84% rename from tests/script-based-pre/cargo_autoverify_contracts/Cargo.toml rename to tests/script-based-pre/cargo_autoharness_contracts/Cargo.toml index 6ac7ea38e31e..10a47f48262b 100644 --- a/tests/script-based-pre/cargo_autoverify_contracts/Cargo.toml +++ b/tests/script-based-pre/cargo_autoharness_contracts/Cargo.toml @@ -2,7 +2,7 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [package] -name = "cargo_autoverify_contracts" +name = "cargo_autoharness_contracts" version = "0.1.0" edition = "2024" diff --git a/tests/script-based-pre/cargo_autoverify_contracts/config.yml b/tests/script-based-pre/cargo_autoharness_contracts/config.yml similarity index 100% rename from tests/script-based-pre/cargo_autoverify_contracts/config.yml rename to tests/script-based-pre/cargo_autoharness_contracts/config.yml diff --git a/tests/script-based-pre/cargo_autoverify_contracts/contracts.expected b/tests/script-based-pre/cargo_autoharness_contracts/contracts.expected similarity index 60% rename from tests/script-based-pre/cargo_autoverify_contracts/contracts.expected rename to tests/script-based-pre/cargo_autoharness_contracts/contracts.expected index 4901a7019cd8..1e25913b6765 100644 --- a/tests/script-based-pre/cargo_autoverify_contracts/contracts.expected +++ b/tests/script-based-pre/cargo_autoharness_contracts/contracts.expected @@ -1,21 +1,21 @@ -Autoverify: Checking function should_fail::max's contract against all possible inputs... +Autoharness: Checking function should_fail::max's contract against all possible inputs... assertion\ - Status: FAILURE\ - Description: "|result : &u32| *result == x" -Autoverify: Checking function should_pass::has_loop_contract's contract against all possible inputs... +Autoharness: Checking function should_pass::has_loop_contract's contract against all possible inputs... should_pass::has_loop_contract.assertion\ - Status: SUCCESS\ - Description: "assertion failed: x == 2" -Autoverify: Checking function should_pass::has_recursion_gcd's contract against all possible inputs... +Autoharness: Checking function should_pass::has_recursion_gcd's contract against all possible inputs... assertion\ - Status: SUCCESS\ - Description: "|result : &u8| *result != 0 && x % *result == 0 && y % *result == 0" -Autoverify: Checking function should_pass::div's contract against all possible inputs... +Autoharness: Checking function should_pass::div's contract against all possible inputs... -Autoverify: Checking function should_pass::unchecked_mul's contract against all possible inputs... +Autoharness: Checking function should_pass::unchecked_mul's contract against all possible inputs... arithmetic_overflow\ - Status: SUCCESS\ - Description: "attempt to compute `unchecked_mul` which would overflow" diff --git a/tests/script-based-pre/cargo_autoverify_contracts/contracts.sh b/tests/script-based-pre/cargo_autoharness_contracts/contracts.sh similarity index 81% rename from tests/script-based-pre/cargo_autoverify_contracts/contracts.sh rename to tests/script-based-pre/cargo_autoharness_contracts/contracts.sh index 7428e196fa84..caad53eb8ac4 100755 --- a/tests/script-based-pre/cargo_autoverify_contracts/contracts.sh +++ b/tests/script-based-pre/cargo_autoharness_contracts/contracts.sh @@ -2,7 +2,7 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT -cargo kani autoverify -Z unstable-options -Z function-contracts -Z loop-contracts +cargo kani autoharness -Z unstable-options -Z function-contracts -Z loop-contracts # We expect verification to fail, so the above command will produce an exit status of 1 # However, we don't want the test to fail because of that exit status; we only want it to fail if the expected file doesn't match # So, exit with a status code of 0 explicitly. diff --git a/tests/script-based-pre/cargo_autoverify_contracts/src/lib.rs b/tests/script-based-pre/cargo_autoharness_contracts/src/lib.rs similarity index 89% rename from tests/script-based-pre/cargo_autoverify_contracts/src/lib.rs rename to tests/script-based-pre/cargo_autoharness_contracts/src/lib.rs index e2ac9654bd36..c9f9dd3fd1b0 100644 --- a/tests/script-based-pre/cargo_autoverify_contracts/src/lib.rs +++ b/tests/script-based-pre/cargo_autoharness_contracts/src/lib.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// Test that the autoverify subcommand correctly verifies contracts, +// Test that the autoharness subcommand correctly verifies contracts, // i.e., that it detects the presence of a contract and generates a contract // harness instead of a standard harness. @@ -41,7 +41,7 @@ mod should_pass { assert!(x == 2); } - // Test that we can autoverify functions for unsafe functions with contracts + // Test that we can autoharness functions for unsafe functions with contracts #[kani::requires(!left.overflowing_mul(rhs).1)] unsafe fn unchecked_mul(left: u8, rhs: u8) -> u8 { left.unchecked_mul(rhs) diff --git a/tests/script-based-pre/cargo_autoverify_include/Cargo.toml b/tests/script-based-pre/cargo_autoharness_exclude/Cargo.toml similarity index 85% rename from tests/script-based-pre/cargo_autoverify_include/Cargo.toml rename to tests/script-based-pre/cargo_autoharness_exclude/Cargo.toml index 5d8e213cc1bf..cceaa1bb7651 100644 --- a/tests/script-based-pre/cargo_autoverify_include/Cargo.toml +++ b/tests/script-based-pre/cargo_autoharness_exclude/Cargo.toml @@ -2,7 +2,7 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [package] -name = "cargo_autoverify_include" +name = "cargo_autoharness_include" version = "0.1.0" edition = "2024" diff --git a/tests/script-based-pre/cargo_autoverify_exclude/config.yml b/tests/script-based-pre/cargo_autoharness_exclude/config.yml similarity index 100% rename from tests/script-based-pre/cargo_autoverify_exclude/config.yml rename to tests/script-based-pre/cargo_autoharness_exclude/config.yml diff --git a/tests/script-based-pre/cargo_autoverify_exclude/exclude.expected b/tests/script-based-pre/cargo_autoharness_exclude/exclude.expected similarity index 63% rename from tests/script-based-pre/cargo_autoverify_exclude/exclude.expected rename to tests/script-based-pre/cargo_autoharness_exclude/exclude.expected index b093236133a1..91d9eb4c399a 100644 --- a/tests/script-based-pre/cargo_autoverify_exclude/exclude.expected +++ b/tests/script-based-pre/cargo_autoharness_exclude/exclude.expected @@ -1,4 +1,4 @@ -Autoverify: Checking function include::simple against all possible inputs... +Autoharness: Checking function include::simple against all possible inputs... VERIFICATION:- SUCCESSFUL Verification succeeded for - include::simple Complete - 1 successfully verified functions, 0 failures, 1 total. \ No newline at end of file diff --git a/tests/script-based-pre/cargo_autoverify_exclude/exclude.sh b/tests/script-based-pre/cargo_autoharness_exclude/exclude.sh similarity index 57% rename from tests/script-based-pre/cargo_autoverify_exclude/exclude.sh rename to tests/script-based-pre/cargo_autoharness_exclude/exclude.sh index 31d3b54e2725..492325dc5c81 100755 --- a/tests/script-based-pre/cargo_autoverify_exclude/exclude.sh +++ b/tests/script-based-pre/cargo_autoharness_exclude/exclude.sh @@ -2,4 +2,4 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT -cargo kani autoverify -Z unstable-options --exclude-function exclude +cargo kani autoharness -Z unstable-options --exclude-function exclude diff --git a/tests/script-based-pre/cargo_autoverify_exclude/src/lib.rs b/tests/script-based-pre/cargo_autoharness_exclude/src/lib.rs similarity index 100% rename from tests/script-based-pre/cargo_autoverify_exclude/src/lib.rs rename to tests/script-based-pre/cargo_autoharness_exclude/src/lib.rs diff --git a/tests/script-based-pre/cargo_autoverify_exclude/Cargo.toml b/tests/script-based-pre/cargo_autoharness_filter/Cargo.toml similarity index 85% rename from tests/script-based-pre/cargo_autoverify_exclude/Cargo.toml rename to tests/script-based-pre/cargo_autoharness_filter/Cargo.toml index 5d8e213cc1bf..41f0d6133106 100644 --- a/tests/script-based-pre/cargo_autoverify_exclude/Cargo.toml +++ b/tests/script-based-pre/cargo_autoharness_filter/Cargo.toml @@ -2,7 +2,7 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [package] -name = "cargo_autoverify_include" +name = "cargo_autoharness_filter" version = "0.1.0" edition = "2024" diff --git a/tests/script-based-pre/cargo_autoverify_filter/config.yml b/tests/script-based-pre/cargo_autoharness_filter/config.yml similarity index 100% rename from tests/script-based-pre/cargo_autoverify_filter/config.yml rename to tests/script-based-pre/cargo_autoharness_filter/config.yml diff --git a/tests/script-based-pre/cargo_autoharness_filter/filter.expected b/tests/script-based-pre/cargo_autoharness_filter/filter.expected new file mode 100644 index 000000000000..9db37edf8232 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_filter/filter.expected @@ -0,0 +1,43 @@ +Autoharness: Checking function yes_harness::f_tuple against all possible inputs... +Autoharness: Checking function yes_harness::f_maybe_uninit against all possible inputs... +Autoharness: Checking function yes_harness::f_result against all possible inputs... +Autoharness: Checking function yes_harness::f_option against all possible inputs... +Autoharness: Checking function yes_harness::f_array against all possible inputs... +Autoharness: Checking function yes_harness::f_nonzero_isize against all possible inputs... +Autoharness: Checking function yes_harness::f_nonzero_i128 against all possible inputs... +Autoharness: Checking function yes_harness::f_nonzero_i64 against all possible inputs... +Autoharness: Checking function yes_harness::f_nonzero_i32 against all possible inputs... +Autoharness: Checking function yes_harness::f_nonzero_i16 against all possible inputs... +Autoharness: Checking function yes_harness::f_nonzero_i8 against all possible inputs... +Autoharness: Checking function yes_harness::f_nonzero_usize against all possible inputs... +Autoharness: Checking function yes_harness::f_nonzero_u128 against all possible inputs... +Autoharness: Checking function yes_harness::f_nonzero_u64 against all possible inputs... +Autoharness: Checking function yes_harness::f_nonzero_u32 against all possible inputs... +Autoharness: Checking function yes_harness::f_nonzero_u16 against all possible inputs... +Autoharness: Checking function yes_harness::f_nonzero_u8 against all possible inputs... +Autoharness: Checking function yes_harness::f_f128 against all possible inputs... +Autoharness: Checking function yes_harness::f_f16 against all possible inputs... +Autoharness: Checking function yes_harness::f_f64 against all possible inputs... +Autoharness: Checking function yes_harness::f_f32 against all possible inputs... +Autoharness: Checking function yes_harness::f_char against all possible inputs... +Autoharness: Checking function yes_harness::f_bool against all possible inputs... +Autoharness: Checking function yes_harness::f_isize against all possible inputs... +Autoharness: Checking function yes_harness::f_i128 against all possible inputs... +Autoharness: Checking function yes_harness::f_i64 against all possible inputs... +Autoharness: Checking function yes_harness::f_i32 against all possible inputs... +Autoharness: Checking function yes_harness::f_i16 against all possible inputs... +Autoharness: Checking function yes_harness::f_i8 against all possible inputs... +Autoharness: Checking function yes_harness::f_usize against all possible inputs... +Autoharness: Checking function yes_harness::f_u128 against all possible inputs... +Autoharness: Checking function yes_harness::f_u64 against all possible inputs... +Autoharness: Checking function yes_harness::f_u32 against all possible inputs... +Autoharness: Checking function yes_harness::f_u16 against all possible inputs... +Autoharness: Checking function yes_harness::f_u8 against all possible inputs... +Autoharness: Checking function yes_harness::f_unsupported_return_type against all possible inputs... +Autoharness: Checking function yes_harness::f_multiple_args against all possible inputs... +Autoharness: Checking function yes_harness::f_derives_arbitrary against all possible inputs... +Autoharness: Checking function yes_harness::f_manually_implements_arbitrary against all possible inputs... +Autoharness: Checking function yes_harness::f_phantom_data against all possible inputs... +Autoharness: Checking function yes_harness::f_phantom_pinned against all possible inputs... +Autoharness: Checking function yes_harness::empty_body against all possible inputs... +Complete - 42 successfully verified functions, 0 failures, 42 total. \ No newline at end of file diff --git a/tests/script-based-pre/cargo_autoverify_filter/filter.sh b/tests/script-based-pre/cargo_autoharness_filter/filter.sh similarity index 69% rename from tests/script-based-pre/cargo_autoverify_filter/filter.sh rename to tests/script-based-pre/cargo_autoharness_filter/filter.sh index c5bdc2bfa0ac..cec2f2e2a10b 100755 --- a/tests/script-based-pre/cargo_autoverify_filter/filter.sh +++ b/tests/script-based-pre/cargo_autoharness_filter/filter.sh @@ -2,4 +2,4 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT -cargo kani autoverify -Z unstable-options +cargo kani autoharness -Z unstable-options diff --git a/tests/script-based-pre/cargo_autoverify_filter/src/lib.rs b/tests/script-based-pre/cargo_autoharness_filter/src/lib.rs similarity index 100% rename from tests/script-based-pre/cargo_autoverify_filter/src/lib.rs rename to tests/script-based-pre/cargo_autoharness_filter/src/lib.rs diff --git a/tests/script-based-pre/cargo_autoverify_harnesses_fail/Cargo.toml b/tests/script-based-pre/cargo_autoharness_harnesses_fail/Cargo.toml similarity index 82% rename from tests/script-based-pre/cargo_autoverify_harnesses_fail/Cargo.toml rename to tests/script-based-pre/cargo_autoharness_harnesses_fail/Cargo.toml index 122823173023..948b9e1666a4 100644 --- a/tests/script-based-pre/cargo_autoverify_harnesses_fail/Cargo.toml +++ b/tests/script-based-pre/cargo_autoharness_harnesses_fail/Cargo.toml @@ -2,7 +2,7 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [package] -name = "cargo_autoverify_harnesses_fail" +name = "cargo_autoharness_harnesses_fail" version = "0.1.0" edition = "2024" diff --git a/tests/script-based-pre/cargo_autoverify_harnesses_fail/config.yml b/tests/script-based-pre/cargo_autoharness_harnesses_fail/config.yml similarity index 100% rename from tests/script-based-pre/cargo_autoverify_harnesses_fail/config.yml rename to tests/script-based-pre/cargo_autoharness_harnesses_fail/config.yml diff --git a/tests/script-based-pre/cargo_autoverify_harnesses_fail/harnesses_fail.expected b/tests/script-based-pre/cargo_autoharness_harnesses_fail/harnesses_fail.expected similarity index 80% rename from tests/script-based-pre/cargo_autoverify_harnesses_fail/harnesses_fail.expected rename to tests/script-based-pre/cargo_autoharness_harnesses_fail/harnesses_fail.expected index 6d7fd2bec692..486d6080a5f3 100644 --- a/tests/script-based-pre/cargo_autoverify_harnesses_fail/harnesses_fail.expected +++ b/tests/script-based-pre/cargo_autoharness_harnesses_fail/harnesses_fail.expected @@ -1,24 +1,24 @@ -Autoverify: Checking function panic against all possible inputs... +Autoharness: Checking function panic against all possible inputs... Check 1: panic.assertion\ - Status: FAILURE\ - Description: "explicit panic" -Autoverify: Checking function integer_overflow against all possible inputs... +Autoharness: Checking function integer_overflow against all possible inputs... assertion\ - Status: FAILURE - Description: "attempt to add with overflow" -Autoverify: Checking function oob_unsafe_array_access against all possible inputs... +Autoharness: Checking function oob_unsafe_array_access against all possible inputs... oob_unsafe_array_access.pointer_dereference\ - Status: FAILURE\ - Description: "dereference failure: pointer outside object bounds" -Autoverify: Checking function oob_safe_array_access against all possible inputs... +Autoharness: Checking function oob_safe_array_access against all possible inputs... assertion\ - Status: FAILURE\ - Description: "index out of bounds: the length is less than or equal to the given index" -Autoverify: Checking function unchecked_mul against all possible inputs... +Autoharness: Checking function unchecked_mul against all possible inputs... arithmetic_overflow\ - Status: FAILURE\ - Description: "attempt to compute `unchecked_mul` which would overflow" diff --git a/tests/script-based-pre/cargo_autoverify_harnesses_fail/harnesses_fail.sh b/tests/script-based-pre/cargo_autoharness_harnesses_fail/harnesses_fail.sh similarity index 89% rename from tests/script-based-pre/cargo_autoverify_harnesses_fail/harnesses_fail.sh rename to tests/script-based-pre/cargo_autoharness_harnesses_fail/harnesses_fail.sh index ddd887daaa0a..b34d3203311f 100755 --- a/tests/script-based-pre/cargo_autoverify_harnesses_fail/harnesses_fail.sh +++ b/tests/script-based-pre/cargo_autoharness_harnesses_fail/harnesses_fail.sh @@ -2,7 +2,7 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT -cargo kani autoverify -Z unstable-options +cargo kani autoharness -Z unstable-options # We expect verification to fail, so the above command will produce an exit status of 1 # However, we don't want the test to fail because of that exit status; we only want it to fail if the expected file doesn't match # So, exit with a status code of 0 explicitly. diff --git a/tests/script-based-pre/cargo_autoverify_harnesses_fail/src/lib.rs b/tests/script-based-pre/cargo_autoharness_harnesses_fail/src/lib.rs similarity index 95% rename from tests/script-based-pre/cargo_autoverify_harnesses_fail/src/lib.rs rename to tests/script-based-pre/cargo_autoharness_harnesses_fail/src/lib.rs index 072dae12c133..591c6b92ee5e 100644 --- a/tests/script-based-pre/cargo_autoverify_harnesses_fail/src/lib.rs +++ b/tests/script-based-pre/cargo_autoharness_harnesses_fail/src/lib.rs @@ -35,7 +35,7 @@ fn panic() { } } -// Test that we can autoverify functions for unsafe functions +// Test that we can autoharness functions for unsafe functions unsafe fn unchecked_mul(left: u8, rhs: u8) -> u8 { left.unchecked_mul(rhs) } diff --git a/tests/script-based-pre/cargo_autoverify_filter/Cargo.toml b/tests/script-based-pre/cargo_autoharness_include/Cargo.toml similarity index 85% rename from tests/script-based-pre/cargo_autoverify_filter/Cargo.toml rename to tests/script-based-pre/cargo_autoharness_include/Cargo.toml index 386df028de57..cceaa1bb7651 100644 --- a/tests/script-based-pre/cargo_autoverify_filter/Cargo.toml +++ b/tests/script-based-pre/cargo_autoharness_include/Cargo.toml @@ -2,7 +2,7 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [package] -name = "cargo_autoverify_filter" +name = "cargo_autoharness_include" version = "0.1.0" edition = "2024" diff --git a/tests/script-based-pre/cargo_autoverify_include/config.yml b/tests/script-based-pre/cargo_autoharness_include/config.yml similarity index 100% rename from tests/script-based-pre/cargo_autoverify_include/config.yml rename to tests/script-based-pre/cargo_autoharness_include/config.yml diff --git a/tests/script-based-pre/cargo_autoverify_include/include.expected b/tests/script-based-pre/cargo_autoharness_include/include.expected similarity index 63% rename from tests/script-based-pre/cargo_autoverify_include/include.expected rename to tests/script-based-pre/cargo_autoharness_include/include.expected index b093236133a1..91d9eb4c399a 100644 --- a/tests/script-based-pre/cargo_autoverify_include/include.expected +++ b/tests/script-based-pre/cargo_autoharness_include/include.expected @@ -1,4 +1,4 @@ -Autoverify: Checking function include::simple against all possible inputs... +Autoharness: Checking function include::simple against all possible inputs... VERIFICATION:- SUCCESSFUL Verification succeeded for - include::simple Complete - 1 successfully verified functions, 0 failures, 1 total. \ No newline at end of file diff --git a/tests/script-based-pre/cargo_autoverify_include/include.sh b/tests/script-based-pre/cargo_autoharness_include/include.sh similarity index 57% rename from tests/script-based-pre/cargo_autoverify_include/include.sh rename to tests/script-based-pre/cargo_autoharness_include/include.sh index 040a246290dd..1b3fcc285c88 100755 --- a/tests/script-based-pre/cargo_autoverify_include/include.sh +++ b/tests/script-based-pre/cargo_autoharness_include/include.sh @@ -2,4 +2,4 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT -cargo kani autoverify -Z unstable-options --include-function include +cargo kani autoharness -Z unstable-options --include-function include diff --git a/tests/script-based-pre/cargo_autoverify_include/src/lib.rs b/tests/script-based-pre/cargo_autoharness_include/src/lib.rs similarity index 100% rename from tests/script-based-pre/cargo_autoverify_include/src/lib.rs rename to tests/script-based-pre/cargo_autoharness_include/src/lib.rs diff --git a/tests/script-based-pre/cargo_autoharness_loops_fixme/Cargo.toml b/tests/script-based-pre/cargo_autoharness_loops_fixme/Cargo.toml new file mode 100644 index 000000000000..57d8cd0f0541 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_loops_fixme/Cargo.toml @@ -0,0 +1,10 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "cargo_autoharness_loops_fixme" +version = "0.1.0" +edition = "2024" + +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } diff --git a/tests/script-based-pre/cargo_autoverify_loops_fixme/config.yml b/tests/script-based-pre/cargo_autoharness_loops_fixme/config.yml similarity index 100% rename from tests/script-based-pre/cargo_autoverify_loops_fixme/config.yml rename to tests/script-based-pre/cargo_autoharness_loops_fixme/config.yml diff --git a/tests/script-based-pre/cargo_autoverify_loops_fixme/loops.sh b/tests/script-based-pre/cargo_autoharness_loops_fixme/loops.sh similarity index 69% rename from tests/script-based-pre/cargo_autoverify_loops_fixme/loops.sh rename to tests/script-based-pre/cargo_autoharness_loops_fixme/loops.sh index c5bdc2bfa0ac..cec2f2e2a10b 100755 --- a/tests/script-based-pre/cargo_autoverify_loops_fixme/loops.sh +++ b/tests/script-based-pre/cargo_autoharness_loops_fixme/loops.sh @@ -2,4 +2,4 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT -cargo kani autoverify -Z unstable-options +cargo kani autoharness -Z unstable-options diff --git a/tests/script-based-pre/cargo_autoverify_loops_fixme/src/lib.rs b/tests/script-based-pre/cargo_autoharness_loops_fixme/src/lib.rs similarity index 100% rename from tests/script-based-pre/cargo_autoverify_loops_fixme/src/lib.rs rename to tests/script-based-pre/cargo_autoharness_loops_fixme/src/lib.rs diff --git a/tests/script-based-pre/cargo_autoverify_filter/filter.expected b/tests/script-based-pre/cargo_autoverify_filter/filter.expected deleted file mode 100644 index 120a7f158b38..000000000000 --- a/tests/script-based-pre/cargo_autoverify_filter/filter.expected +++ /dev/null @@ -1,43 +0,0 @@ -Autoverify: Checking function yes_harness::f_tuple against all possible inputs... -Autoverify: Checking function yes_harness::f_maybe_uninit against all possible inputs... -Autoverify: Checking function yes_harness::f_result against all possible inputs... -Autoverify: Checking function yes_harness::f_option against all possible inputs... -Autoverify: Checking function yes_harness::f_array against all possible inputs... -Autoverify: Checking function yes_harness::f_nonzero_isize against all possible inputs... -Autoverify: Checking function yes_harness::f_nonzero_i128 against all possible inputs... -Autoverify: Checking function yes_harness::f_nonzero_i64 against all possible inputs... -Autoverify: Checking function yes_harness::f_nonzero_i32 against all possible inputs... -Autoverify: Checking function yes_harness::f_nonzero_i16 against all possible inputs... -Autoverify: Checking function yes_harness::f_nonzero_i8 against all possible inputs... -Autoverify: Checking function yes_harness::f_nonzero_usize against all possible inputs... -Autoverify: Checking function yes_harness::f_nonzero_u128 against all possible inputs... -Autoverify: Checking function yes_harness::f_nonzero_u64 against all possible inputs... -Autoverify: Checking function yes_harness::f_nonzero_u32 against all possible inputs... -Autoverify: Checking function yes_harness::f_nonzero_u16 against all possible inputs... -Autoverify: Checking function yes_harness::f_nonzero_u8 against all possible inputs... -Autoverify: Checking function yes_harness::f_f128 against all possible inputs... -Autoverify: Checking function yes_harness::f_f16 against all possible inputs... -Autoverify: Checking function yes_harness::f_f64 against all possible inputs... -Autoverify: Checking function yes_harness::f_f32 against all possible inputs... -Autoverify: Checking function yes_harness::f_char against all possible inputs... -Autoverify: Checking function yes_harness::f_bool against all possible inputs... -Autoverify: Checking function yes_harness::f_isize against all possible inputs... -Autoverify: Checking function yes_harness::f_i128 against all possible inputs... -Autoverify: Checking function yes_harness::f_i64 against all possible inputs... -Autoverify: Checking function yes_harness::f_i32 against all possible inputs... -Autoverify: Checking function yes_harness::f_i16 against all possible inputs... -Autoverify: Checking function yes_harness::f_i8 against all possible inputs... -Autoverify: Checking function yes_harness::f_usize against all possible inputs... -Autoverify: Checking function yes_harness::f_u128 against all possible inputs... -Autoverify: Checking function yes_harness::f_u64 against all possible inputs... -Autoverify: Checking function yes_harness::f_u32 against all possible inputs... -Autoverify: Checking function yes_harness::f_u16 against all possible inputs... -Autoverify: Checking function yes_harness::f_u8 against all possible inputs... -Autoverify: Checking function yes_harness::f_unsupported_return_type against all possible inputs... -Autoverify: Checking function yes_harness::f_multiple_args against all possible inputs... -Autoverify: Checking function yes_harness::f_derives_arbitrary against all possible inputs... -Autoverify: Checking function yes_harness::f_manually_implements_arbitrary against all possible inputs... -Autoverify: Checking function yes_harness::f_phantom_data against all possible inputs... -Autoverify: Checking function yes_harness::f_phantom_pinned against all possible inputs... -Autoverify: Checking function yes_harness::empty_body against all possible inputs... -Complete - 42 successfully verified functions, 0 failures, 42 total. \ No newline at end of file diff --git a/tests/script-based-pre/cargo_autoverify_loops_fixme/Cargo.toml b/tests/script-based-pre/cargo_autoverify_loops_fixme/Cargo.toml deleted file mode 100644 index 1b4a9a4acae1..000000000000 --- a/tests/script-based-pre/cargo_autoverify_loops_fixme/Cargo.toml +++ /dev/null @@ -1,10 +0,0 @@ -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -[package] -name = "cargo_autoverify_loops_fixme" -version = "0.1.0" -edition = "2024" - -[lints.rust] -unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } From 97876644a334a6a6258aea924dc61ba758ca3afa Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Wed, 5 Feb 2025 20:20:12 -0500 Subject: [PATCH 10/12] Improve documentation to make clear that it generates a harness --- docs/src/SUMMARY.md | 2 +- docs/src/reference/experimental/autoharness.md | 15 +++++++++------ 2 files changed, 10 insertions(+), 7 deletions(-) diff --git a/docs/src/SUMMARY.md b/docs/src/SUMMARY.md index 2bcdea7c4c2f..11d5318a0e2c 100644 --- a/docs/src/SUMMARY.md +++ b/docs/src/SUMMARY.md @@ -18,7 +18,7 @@ - [Reference](./reference.md) - [Attributes](./reference/attributes.md) - [Experimental features](./reference/experimental/experimental-features.md) - - [Automatic Verification](./reference/experimental/autoharness.md) + - [Automatic Harness Generation](./reference/experimental/autoharness.md) - [Coverage](./reference/experimental/coverage.md) - [Stubbing](./reference/experimental/stubbing.md) - [Contracts](./reference/experimental/contracts.md) diff --git a/docs/src/reference/experimental/autoharness.md b/docs/src/reference/experimental/autoharness.md index 5156c9e63956..022d6471ea0e 100644 --- a/docs/src/reference/experimental/autoharness.md +++ b/docs/src/reference/experimental/autoharness.md @@ -1,4 +1,4 @@ -# Automatic Verification +# Automatic Harness Generation Recall the harness for `estimate_size` that we wrote in [First Steps](../../tutorial-first-steps.md): ```rust @@ -8,7 +8,9 @@ Recall the harness for `estimate_size` that we wrote in [First Steps](../../tuto This harness first declares a local variable `x` using `kani::any()`, then calls `estimate_size` with argument `x`. Many proof harnesses follow this predictable format—to verify a function `foo`, we create arbitrary values for each of `foo`'s arguments, then call `foo` on those arguments. -The `autoharness` feature scans a crate for functions whose arguments all implement the `kani::Arbitrary` trait, and then verifies those functions for you automatically. +The `autoharness` subcommand leverages this observation to automatically generate and run harnesses. +Kani scans the crate for functions whose arguments all implement the `kani::Arbitrary` trait, generates harnesses for them, then runs them. +These harnesses are internal to Kani--i.e., Kani does not make any changes to your source code. ## Usage Run either: @@ -33,16 +35,16 @@ Autoharness: Checking function foo's contract against all possible inputs... ``` -Kani generates and runs these harnesses internally—the user never sees them. +Kani generates and runs these harnesses internally—the user only sees the verification results. -The `autoharness` subcommand has options `--include-function` and `--exclude-function` to include and exclude particular functions from autoverification. +The `autoharness` subcommand has options `--include-function` and `--exclude-function` to include and exclude particular functions. These flags look for partial matches against the fully qualified name of a function. For example, if a module `my_module` has many functions, but we are only interested in `my_module::foo` and `my_module::bar`, we can run: ``` cargo run autoharness -Z unstable-options --include-function foo include-function bar ``` -To exclude `my_module` from autoverification entirely, run: +To exclude `my_module` entirely, run: ``` cargo run autoharness -Z unstable-options --exclude-function my_module ``` @@ -74,8 +76,9 @@ If you have ideas for improving the user experience of this feature, please add them to [this GitHub issue](https://github.com/model-checking/kani/issues/3832). ## Limitations -Kani will only autoharness a function if it can determine that all of the function's arguments implement Arbitrary. +Kani will only generate an automatic harness for a function if it can determine that all of the function's arguments implement Arbitrary. It does not attempt to derive/implement Arbitrary for any types, even if those types could implement Arbitrary. + If a function contains a loop with a loop contract, Kani will detect the presence of a loop contract and verify that contract. If, however, the loop does not have a contract, then there is currently no way to specify an unwinding bound for the function, meaning that Kani may hang as it tries to unwind the loop. We recommend using the `--exclude-function` option to exclude any functions that have this issue (or `--harness-timeout` to bail after attempting verification for some amount of time). \ No newline at end of file From 4643132a5dc2bce098a7ba0f05c1c47406ba21db Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Mon, 10 Feb 2025 14:33:16 -0500 Subject: [PATCH 11/12] Rename reachability mode to AllFns --- kani-compiler/src/args.rs | 5 +++-- kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs | 2 +- .../src/codegen_cprover_gotoc/compiler_interface.rs | 4 ++-- kani-compiler/src/kani_middle/codegen_units.rs | 2 +- kani-compiler/src/kani_middle/transform/automatic.rs | 2 +- kani-compiler/src/kani_middle/transform/contracts.rs | 2 +- kani-driver/src/session.rs | 4 ++-- 7 files changed, 11 insertions(+), 10 deletions(-) diff --git a/kani-compiler/src/args.rs b/kani-compiler/src/args.rs index 92950a8eb409..e524b6e5ba2a 100644 --- a/kani-compiler/src/args.rs +++ b/kani-compiler/src/args.rs @@ -30,8 +30,9 @@ pub enum ReachabilityType { PubFns, /// Start the cross-crate reachability analysis from all *test* (i.e. `#[test]`) harnesses in the local crate. Tests, - /// Start the cross-crate reachability analysis from all functions in the local crate that can be automatically verified. - Automatic, + /// Start the cross-crate reachability analysis from all functions in the local crate. + /// Currently, this mode is only used for automatic harness generation. + AllFns, } /// Command line arguments that this instance of the compiler run was called diff --git a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs index 374d4a987682..f577d2886e6c 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs @@ -253,7 +253,7 @@ impl CodegenBackend for LlbcCodegenBackend { units.store_modifies(&modifies_instances); units.write_metadata(&queries, tcx); } - ReachabilityType::Tests | ReachabilityType::Automatic => todo!(), + ReachabilityType::Tests | ReachabilityType::AllFns => todo!(), ReachabilityType::None => {} ReachabilityType::PubFns => { let unit = CodegenUnit::default(); diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 5192af2b1cea..80137db06a6e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -264,7 +264,7 @@ impl CodegenBackend for GotocCodegenBackend { let reachability = queries.args().reachability_analysis; let mut results = GotoCodegenResults::new(tcx, reachability); match reachability { - ReachabilityType::Automatic | ReachabilityType::Harnesses => { + ReachabilityType::AllFns | ReachabilityType::Harnesses => { let mut units = CodegenUnits::new(&queries, tcx); let mut modifies_instances = vec![]; let mut loop_contracts_instances = vec![]; @@ -376,7 +376,7 @@ impl CodegenBackend for GotocCodegenBackend { results.print_report(tcx); if reachability != ReachabilityType::Harnesses - && reachability != ReachabilityType::Automatic + && reachability != ReachabilityType::AllFns { // In a workspace, cargo seems to be using the same file prefix to build a crate that is // a package lib and also a dependency of another package. diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index c29dc244d9fe..1fc659ea2f80 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -72,7 +72,7 @@ impl CodegenUnits { debug!(?units, "CodegenUnits::new"); CodegenUnits { units, harness_info: all_harnesses, crate_info } } - ReachabilityType::Automatic => { + ReachabilityType::AllFns => { let mut all_harnesses = get_all_manual_harnesses(tcx, base_filename); let mut units = group_by_stubs(tcx, &all_harnesses); validate_units(tcx, &units); diff --git a/kani-compiler/src/kani_middle/transform/automatic.rs b/kani-compiler/src/kani_middle/transform/automatic.rs index 2549648045f2..705a8ac26a88 100644 --- a/kani-compiler/src/kani_middle/transform/automatic.rs +++ b/kani-compiler/src/kani_middle/transform/automatic.rs @@ -62,7 +62,7 @@ impl TransformPass for AutomaticHarnessPass { where Self: Sized, { - matches!(query_db.args().reachability_analysis, ReachabilityType::Automatic) + matches!(query_db.args().reachability_analysis, ReachabilityType::AllFns) } fn transform(&mut self, _tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) { diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs index 7e93163a5dc0..bd613b3d6663 100644 --- a/kani-compiler/src/kani_middle/transform/contracts.rs +++ b/kani-compiler/src/kani_middle/transform/contracts.rs @@ -346,7 +346,7 @@ impl FunctionWithContractPass { let harness_generic_args = harness.args().0; // Manual harnesses have no arguments, so if there are generic arguments, // we know this is an automatic harness - if matches!(queries.args().reachability_analysis, ReachabilityType::Automatic) + if matches!(queries.args().reachability_analysis, ReachabilityType::AllFns) && !harness_generic_args.is_empty() { let kind = harness.args().0[0].expect_ty().kind(); diff --git a/kani-driver/src/session.rs b/kani-driver/src/session.rs index 7e5df4979688..6645db06e45e 100644 --- a/kani-driver/src/session.rs +++ b/kani-driver/src/session.rs @@ -102,7 +102,7 @@ impl KaniSession { if self.codegen_tests { ReachabilityMode::Tests } else if self.auto_harness { - ReachabilityMode::Automatic + ReachabilityMode::AllFns } else { ReachabilityMode::ProofHarnesses } @@ -112,7 +112,7 @@ impl KaniSession { #[derive(Debug, Copy, Clone, Display)] #[strum(serialize_all = "snake_case")] pub enum ReachabilityMode { - Automatic, + AllFns, #[strum(to_string = "harnesses")] ProofHarnesses, Tests, From 875086030d11b5530aaf6719b050d6c689b1ed12 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Mon, 10 Feb 2025 14:45:04 -0500 Subject: [PATCH 12/12] add expected file for loops fixme test --- .../cargo_autoharness_harnesses_fail/harnesses_fail.expected | 2 +- .../script-based-pre/cargo_autoharness_loops_fixme/config.yml | 4 ++-- .../cargo_autoharness_loops_fixme/loops.expected | 1 + 3 files changed, 4 insertions(+), 3 deletions(-) create mode 100644 tests/script-based-pre/cargo_autoharness_loops_fixme/loops.expected diff --git a/tests/script-based-pre/cargo_autoharness_harnesses_fail/harnesses_fail.expected b/tests/script-based-pre/cargo_autoharness_harnesses_fail/harnesses_fail.expected index 486d6080a5f3..7ceed3cc019a 100644 --- a/tests/script-based-pre/cargo_autoharness_harnesses_fail/harnesses_fail.expected +++ b/tests/script-based-pre/cargo_autoharness_harnesses_fail/harnesses_fail.expected @@ -1,5 +1,5 @@ Autoharness: Checking function panic against all possible inputs... -Check 1: panic.assertion\ +panic.assertion\ - Status: FAILURE\ - Description: "explicit panic" diff --git a/tests/script-based-pre/cargo_autoharness_loops_fixme/config.yml b/tests/script-based-pre/cargo_autoharness_loops_fixme/config.yml index 90ee1970e96c..fefb50875c7a 100644 --- a/tests/script-based-pre/cargo_autoharness_loops_fixme/config.yml +++ b/tests/script-based-pre/cargo_autoharness_loops_fixme/config.yml @@ -1,4 +1,4 @@ # Copyright Kani Contributors # SPDX-License-Identifier: Apache-2.0 OR MIT -script: filter.sh -expected: filter.expected +script: loops.sh +expected: loops.expected diff --git a/tests/script-based-pre/cargo_autoharness_loops_fixme/loops.expected b/tests/script-based-pre/cargo_autoharness_loops_fixme/loops.expected new file mode 100644 index 000000000000..4c43332f6db0 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_loops_fixme/loops.expected @@ -0,0 +1 @@ +It's not yet clear what the ideal output is for this test, so this expected file is just a placeholder. \ No newline at end of file