diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 8ed90b2c975e..ef32d99042c1 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -42,8 +42,8 @@ use rustc_session::config::{CrateType, OutputFilenames, OutputType}; use rustc_session::output::out_filename; use rustc_smir::rustc_internal; use rustc_target::spec::PanicStrategy; +use stable_mir::CrateDef; use stable_mir::mir::mono::{Instance, MonoItem}; -use stable_mir::{CrateDef, DefId}; use std::any::Any; use std::collections::BTreeMap; use std::fmt::Write; @@ -212,6 +212,27 @@ impl GotocCodegenBackend { (gcx, items, contract_info) } + + /// Given a contract harness, get the DefId of its target. + /// For manual harnesses, extract it from the #[proof_for_contract] attribute. + /// For automatic harnesses, extract the target from the harness's GenericArgs. + fn target_def_id_for_harness( + &self, + tcx: TyCtxt, + harness: &Instance, + is_automatic_harness: bool, + ) -> Option { + if is_automatic_harness { + let kind = harness.args().0[0].expect_ty().kind(); + let (fn_to_verify_def, _) = kind.fn_def().unwrap(); + let def_id = fn_to_verify_def.def_id(); + let attrs = KaniAttributes::for_def_id(tcx, def_id); + if attrs.has_contract() { Some(rustc_internal::internal(tcx, def_id)) } else { None } + } else { + let harness_attrs = KaniAttributes::for_def_id(tcx, harness.def.def_id()); + harness_attrs.interpret_for_contract_attribute().map(|(_, id, _)| id) + } + } } impl CodegenBackend for GotocCodegenBackend { @@ -275,8 +296,9 @@ impl CodegenBackend for GotocCodegenBackend { for harness in &unit.harnesses { let transformer = BodyTransformation::new(&queries, tcx, &unit); let model_path = units.harness_model_path(*harness).unwrap(); + let is_automatic_harness = units.is_automatic_harness(harness); let contract_metadata = - contract_metadata_for_harness(tcx, harness.def.def_id()); + self.target_def_id_for_harness(tcx, harness, is_automatic_harness); let (gcx, items, contract_info) = self.codegen_items( tcx, &[MonoItem::Fn(*harness)], @@ -453,11 +475,6 @@ impl ArchiveBuilderBuilder for ArArchiveBuilderBuilder { } } -fn contract_metadata_for_harness(tcx: TyCtxt, def_id: DefId) -> Option { - let attrs = KaniAttributes::for_def_id(tcx, def_id); - attrs.interpret_for_contract_attribute().map(|(_, id, _)| id) -} - fn check_target(session: &Session) { // The requirement below is needed to build a valid CBMC machine model // in function `machine_model_from_session` from diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index c3b6e45c15b9..7a9f494d997e 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -97,7 +97,7 @@ impl CodegenUnits { chosen: chosen.iter().map(|func| func.name()).collect::>(), skipped, }) - .expect("Initializing the autoharness metdata failed"); + .expect("Initializing the autoharness metadata failed"); let automatic_harnesses = get_all_automatic_harnesses( tcx, @@ -133,6 +133,10 @@ impl CodegenUnits { self.units.iter() } + pub fn is_automatic_harness(&self, harness: &Harness) -> bool { + self.harness_info.get(harness).is_some_and(|md| md.is_automatically_generated) + } + /// We store which instance of modifies was generated. pub fn store_modifies(&mut self, harness_modifies: &[(Harness, AssignsContract)]) { for (harness, modifies) in harness_modifies { @@ -340,7 +344,12 @@ fn get_all_automatic_harnesses( &GenericArgs(vec![GenericArgKind::Type(fn_to_verify.ty())]), ) .unwrap(); - let metadata = gen_automatic_proof_metadata(tcx, &base_filename, &fn_to_verify); + let metadata = gen_automatic_proof_metadata( + tcx, + &base_filename, + &fn_to_verify, + harness.mangled_name(), + ); (harness, metadata) }) .collect::>() diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs index 50487ce45714..4a7a0aa07b94 100644 --- a/kani-compiler/src/kani_middle/metadata.rs +++ b/kani-compiler/src/kani_middle/metadata.rs @@ -112,12 +112,13 @@ pub fn gen_contracts_metadata( /// 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), +/// TODO: 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. pub fn gen_automatic_proof_metadata( tcx: TyCtxt, base_name: &Path, fn_to_verify: &Instance, + harness_mangled_name: String, ) -> HarnessMetadata { let def = fn_to_verify.def; let pretty_name = fn_to_verify.name(); @@ -137,8 +138,10 @@ pub fn gen_automatic_proof_metadata( }; HarnessMetadata { + // pretty_name is what gets displayed to the user, and that should be the name of the function being verified, hence using fn_to_verify name pretty_name, - mangled_name, + // We pass --function mangled_name to CBMC to select the entry point, which should be the mangled name of the automatic harness intrinsic + mangled_name: harness_mangled_name, crate_name: def.krate().name, original_file: loc.filename, original_start_line: loc.start_line, diff --git a/kani-compiler/src/kani_middle/transform/automatic.rs b/kani-compiler/src/kani_middle/transform/automatic.rs index 705a8ac26a88..76d21043355a 100644 --- a/kani-compiler/src/kani_middle/transform/automatic.rs +++ b/kani-compiler/src/kani_middle/transform/automatic.rs @@ -7,21 +7,24 @@ //! then transform its body to be a harness for that function. 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}; +use crate::kani_middle::kani_functions::{KaniHook, 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::CrateDef; use stable_mir::mir::mono::Instance; -use stable_mir::mir::{Body, Operand, Place, TerminatorKind}; -use stable_mir::ty::{FnDef, GenericArgKind, GenericArgs}; +use stable_mir::mir::{Body, Mutability, Operand, Place, TerminatorKind}; +use stable_mir::ty::{FnDef, GenericArgKind, GenericArgs, RigidTy, Ty}; use tracing::debug; #[derive(Debug)] pub struct AutomaticHarnessPass { /// The FnDef of KaniModel::Any kani_any: FnDef, + init_contracts_hook: Instance, /// All of the automatic harness Instances that we generated in the CodegenUnits constructor automatic_harnesses: Vec, } @@ -37,6 +40,9 @@ impl AutomaticHarnessPass { 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 init_contracts_hook = *kani_fns.get(&KaniHook::InitContracts.into()).unwrap(); + let init_contracts_hook = + Instance::resolve(init_contracts_hook, &GenericArgs(vec![])).unwrap(); let automatic_harnesses = unit .harnesses .iter() @@ -46,7 +52,7 @@ impl AutomaticHarnessPass { def == harness_intrinsic }) .collect::>(); - Self { kani_any, automatic_harnesses } + Self { kani_any, init_contracts_hook, automatic_harnesses } } } @@ -65,7 +71,7 @@ impl TransformPass for AutomaticHarnessPass { matches!(query_db.args().reachability_analysis, ReachabilityType::AllFns) } - fn transform(&mut self, _tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) { + fn transform(&mut self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) { debug!(function=?instance.name(), "AutomaticHarnessPass::transform"); if !self.automatic_harnesses.contains(&instance) { @@ -83,6 +89,23 @@ impl TransformPass for AutomaticHarnessPass { harness_body.clear_body(TerminatorKind::Return); let mut source = SourceInstruction::Terminator { bb: 0 }; + // Contract harnesses need a free(NULL) statement, c.f. kani_core::init_contracts(). + let attrs = KaniAttributes::for_def_id(tcx, def.def_id()); + if attrs.has_contract() { + let ret_local = harness_body.new_local( + Ty::from_rigid_kind(RigidTy::Tuple(vec![])), + source.span(harness_body.blocks()), + Mutability::Not, + ); + harness_body.insert_call( + &self.init_contracts_hook, + &mut source, + InsertPosition::Before, + vec![], + Place::from(ret_local), + ); + } + let mut arg_locals = vec![]; // For each argument of `fn_to_verify`, create a nondeterministic value of its type diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs index df5e4209e900..f7ca09b93a41 100644 --- a/kani-compiler/src/kani_middle/transform/contracts.rs +++ b/kani-compiler/src/kani_middle/transform/contracts.rs @@ -350,12 +350,11 @@ impl FunctionWithContractPass { && !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(); + let (fn_to_verify_def, _) = kind.fn_def().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())), + Some(rustc_internal::internal(tcx, fn_to_verify_def.def_id())), HashSet::default(), ) } else { diff --git a/tests/script-based-pre/cargo_autoharness_contracts/contracts.expected b/tests/script-based-pre/cargo_autoharness_contracts/contracts.expected index 7f3b92ffef86..e5aa3a29009a 100644 --- a/tests/script-based-pre/cargo_autoharness_contracts/contracts.expected +++ b/tests/script-based-pre/cargo_autoharness_contracts/contracts.expected @@ -1,17 +1,21 @@ -Kani generated automatic harnesses for 5 function(s): -+--------------------------------+ -| Selected Function | -+================================+ -| should_fail::max | -|--------------------------------| -| should_pass::div | -|--------------------------------| -| should_pass::has_loop_contract | -|--------------------------------| -| should_pass::has_recursion_gcd | -|--------------------------------| -| should_pass::unchecked_mul | -+--------------------------------+ +Kani generated automatic harnesses for 7 function(s): ++---------------------------------------------+ +| Selected Function | ++=============================================+ +| should_fail::max | +|---------------------------------------------| +| should_pass::alignment::Alignment | +|---------------------------------------------| +| should_pass::alignment::Alignment::as_usize | +|---------------------------------------------| +| should_pass::div | +|---------------------------------------------| +| should_pass::has_loop_contract | +|---------------------------------------------| +| should_pass::has_recursion_gcd | +|---------------------------------------------| +| should_pass::unchecked_mul | ++---------------------------------------------+ Skipped Functions: None. Kani generated automatic harnesses for all functions in the available crate(s). @@ -37,23 +41,37 @@ arithmetic_overflow\ - Status: SUCCESS\ - Description: "attempt to compute `unchecked_mul` which would overflow" +Autoharness: Checking function should_pass::alignment::Alignment::as_usize's contract against all possible inputs... + +should_pass::alignment::Alignment::as_usize\ + - Status: SUCCESS\ + - Description: "Rust intrinsic assumption failed" + +should_pass::alignment::Alignment::as_usize\ + - Status: SUCCESS\ + - Description: "|result| result.is_power_of_two()" + Manual Harness Summary: No proof harnesses (functions with #[kani::proof]) were found to verify. Autoharness Summary: -+--------------------------------+-----------------------------+---------------------+ -| Selected Function | Kind of Automatic Harness | Verification Result | -+====================================================================================+ -| should_pass::div | #[kani::proof_for_contract] | Success | -|--------------------------------+-----------------------------+---------------------| -| should_pass::has_loop_contract | #[kani::proof] | Success | -|--------------------------------+-----------------------------+---------------------| -| should_pass::has_recursion_gcd | #[kani::proof_for_contract] | Success | -|--------------------------------+-----------------------------+---------------------| -| should_pass::unchecked_mul | #[kani::proof_for_contract] | Success | -|--------------------------------+-----------------------------+---------------------| -| should_fail::max | #[kani::proof_for_contract] | Failure | -+--------------------------------+-----------------------------+---------------------+ ++---------------------------------------------+-----------------------------+---------------------+ +| Selected Function | Kind of Automatic Harness | Verification Result | ++=================================================================================================+ +| should_pass::alignment::Alignment | #[kani::proof] | Success | +|---------------------------------------------+-----------------------------+---------------------| +| should_pass::alignment::Alignment::as_usize | #[kani::proof_for_contract] | Success | +|---------------------------------------------+-----------------------------+---------------------| +| should_pass::div | #[kani::proof_for_contract] | Success | +|---------------------------------------------+-----------------------------+---------------------| +| should_pass::has_loop_contract | #[kani::proof] | Success | +|---------------------------------------------+-----------------------------+---------------------| +| should_pass::has_recursion_gcd | #[kani::proof_for_contract] | Success | +|---------------------------------------------+-----------------------------+---------------------| +| should_pass::unchecked_mul | #[kani::proof_for_contract] | Success | +|---------------------------------------------+-----------------------------+---------------------| +| should_fail::max | #[kani::proof_for_contract] | Failure | ++---------------------------------------------+-----------------------------+---------------------+ Note that `kani autoharness` sets default --harness-timeout of 60s and --default-unwind of 20. If verification failed because of timing out or too low of an unwinding bound, try passing larger values for these arguments (or, if possible, writing a loop contract). -Complete - 4 successfully verified functions, 1 failures, 5 total. +Complete - 6 successfully verified functions, 1 failures, 7 total. diff --git a/tests/script-based-pre/cargo_autoharness_contracts/src/lib.rs b/tests/script-based-pre/cargo_autoharness_contracts/src/lib.rs index c66b3dab4fbe..39bd828c682d 100644 --- a/tests/script-based-pre/cargo_autoharness_contracts/src/lib.rs +++ b/tests/script-based-pre/cargo_autoharness_contracts/src/lib.rs @@ -46,6 +46,90 @@ mod should_pass { unsafe fn unchecked_mul(left: u8, rhs: u8) -> u8 { unsafe { left.unchecked_mul(rhs) } } + + // Check that we can create automatic harnesses for more complex situtations, i.e., + // functions with contracts that reference nested data structures that derive Arbitrary. + mod alignment { + // FIXME: Note that since this is a tuple struct, we generate an extra harness for the Alignment constructor, + // c.f. https://github.com/model-checking/kani/issues/3832#issuecomment-2730580836 + #[derive(kani::Arbitrary)] + pub struct Alignment(AlignmentEnum); + + #[derive(kani::Arbitrary)] + enum AlignmentEnum { + _Align1Shl0 = 1 << 0, + _Align1Shl1 = 1 << 1, + _Align1Shl2 = 1 << 2, + _Align1Shl3 = 1 << 3, + _Align1Shl4 = 1 << 4, + _Align1Shl5 = 1 << 5, + _Align1Shl6 = 1 << 6, + _Align1Shl7 = 1 << 7, + _Align1Shl8 = 1 << 8, + _Align1Shl9 = 1 << 9, + _Align1Shl10 = 1 << 10, + _Align1Shl11 = 1 << 11, + _Align1Shl12 = 1 << 12, + _Align1Shl13 = 1 << 13, + _Align1Shl14 = 1 << 14, + _Align1Shl15 = 1 << 15, + _Align1Shl16 = 1 << 16, + _Align1Shl17 = 1 << 17, + _Align1Shl18 = 1 << 18, + _Align1Shl19 = 1 << 19, + _Align1Shl20 = 1 << 20, + _Align1Shl21 = 1 << 21, + _Align1Shl22 = 1 << 22, + _Align1Shl23 = 1 << 23, + _Align1Shl24 = 1 << 24, + _Align1Shl25 = 1 << 25, + _Align1Shl26 = 1 << 26, + _Align1Shl27 = 1 << 27, + _Align1Shl28 = 1 << 28, + _Align1Shl29 = 1 << 29, + _Align1Shl30 = 1 << 30, + _Align1Shl31 = 1 << 31, + _Align1Shl32 = 1 << 32, + _Align1Shl33 = 1 << 33, + _Align1Shl34 = 1 << 34, + _Align1Shl35 = 1 << 35, + _Align1Shl36 = 1 << 36, + _Align1Shl37 = 1 << 37, + _Align1Shl38 = 1 << 38, + _Align1Shl39 = 1 << 39, + _Align1Shl40 = 1 << 40, + _Align1Shl41 = 1 << 41, + _Align1Shl42 = 1 << 42, + _Align1Shl43 = 1 << 43, + _Align1Shl44 = 1 << 44, + _Align1Shl45 = 1 << 45, + _Align1Shl46 = 1 << 46, + _Align1Shl47 = 1 << 47, + _Align1Shl48 = 1 << 48, + _Align1Shl49 = 1 << 49, + _Align1Shl50 = 1 << 50, + _Align1Shl51 = 1 << 51, + _Align1Shl52 = 1 << 52, + _Align1Shl53 = 1 << 53, + _Align1Shl54 = 1 << 54, + _Align1Shl55 = 1 << 55, + _Align1Shl56 = 1 << 56, + _Align1Shl57 = 1 << 57, + _Align1Shl58 = 1 << 58, + _Align1Shl59 = 1 << 59, + _Align1Shl60 = 1 << 60, + _Align1Shl61 = 1 << 61, + _Align1Shl62 = 1 << 62, + _Align1Shl63 = 1 << 63, + } + + impl Alignment { + #[kani::ensures(|result| result.is_power_of_two())] + pub fn as_usize(self) -> usize { + self.0 as usize + } + } + } } mod should_fail { diff --git a/tests/script-based-pre/cargo_autoharness_type_invariant/Cargo.toml b/tests/script-based-pre/cargo_autoharness_type_invariant/Cargo.toml new file mode 100644 index 000000000000..abcecba4b6c2 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_type_invariant/Cargo.toml @@ -0,0 +1,10 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "cargo_autoharness_type_invariant" +version = "0.1.0" +edition = "2024" + +[lints.rust] +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } diff --git a/tests/script-based-pre/cargo_autoharness_type_invariant/config.yml b/tests/script-based-pre/cargo_autoharness_type_invariant/config.yml new file mode 100644 index 000000000000..5762f901d15e --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_type_invariant/config.yml @@ -0,0 +1,4 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: type-invariant.sh +expected: type-invariant.expected diff --git a/tests/script-based-pre/cargo_autoharness_type_invariant/src/lib.rs b/tests/script-based-pre/cargo_autoharness_type_invariant/src/lib.rs new file mode 100644 index 000000000000..4aca2eef9193 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_type_invariant/src/lib.rs @@ -0,0 +1,112 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Test that the autoharness subcommand respects the invariants specified in the type's kani::any() implementation. +// In other words, test that autoharness is actually finding and using the appropriate kani::any() implementation, +// rather than letting CBMC generate nondetermistic values for the type. +// In this example, we check that the methods that take `Duration` as an argument generate Durations that respect the type invariant that nanos < NANOS_PER_SEC. +// See the "TEST NOTE" inline comments for how we specifically check this. + +// Simplified code from https://github.com/model-checking/verify-rust-std/blob/3f4234a19211e677d51df3061db67477b29af171/library/core/src/time.rs#L1 + +use kani::Invariant; + +const NANOS_PER_SEC: u32 = 1_000_000_000; + +#[derive(kani::Arbitrary)] +#[derive(Clone, Copy)] +pub struct Nanoseconds(u32); + +#[derive(Clone, Copy)] +#[derive(kani::Invariant)] +pub struct Duration { + secs: u64, + nanos: Nanoseconds, +} + +impl kani::Invariant for Nanoseconds { + fn is_safe(&self) -> bool { + self.as_inner() < NANOS_PER_SEC + } +} + +impl Nanoseconds { + #[kani::requires(val < NANOS_PER_SEC)] + #[kani::ensures(|nano| nano.is_safe())] + pub const unsafe fn new_unchecked(val: u32) -> Self { + // SAFETY: caller promises that val < NANOS_PER_SEC + Self(val) + } + + pub const fn as_inner(self) -> u32 { + // SAFETY: This is a transparent wrapper, so unwrapping it is sound + unsafe { core::mem::transmute(self) } + } +} + +impl kani::Arbitrary for Duration { + fn any() -> Self { + let d = Duration { secs: kani::any(), nanos: kani::any() }; + kani::assume(d.is_safe()); + d + } +} + +impl Duration { + // TEST NOTE: the automatic harness for this method fails because it can panic. + #[kani::ensures(|duration| duration.is_safe())] + pub const fn new(secs: u64, nanos: u32) -> Duration { + if nanos < NANOS_PER_SEC { + // SAFETY: nanos < NANOS_PER_SEC, therefore nanos is within the valid range + Duration { secs, nanos: unsafe { Nanoseconds::new_unchecked(nanos) } } + } else { + let secs = secs + .checked_add((nanos / NANOS_PER_SEC) as u64) + .expect("overflow in Duration::new"); + let nanos = nanos % NANOS_PER_SEC; + // SAFETY: nanos % NANOS_PER_SEC < NANOS_PER_SEC, therefore nanos is within the valid range + Duration { secs, nanos: unsafe { Nanoseconds::new_unchecked(nanos) } } + } + } + + pub const fn abs_diff(self, other: Duration) -> Duration { + if let Some(res) = self.checked_sub(other) { res } else { other.checked_sub(self).unwrap() } + } + + #[kani::ensures(|duration| duration.is_none() || duration.unwrap().is_safe())] + pub const fn checked_add(self, rhs: Duration) -> Option { + if let Some(mut secs) = self.secs.checked_add(rhs.secs) { + // TEST NOTE: this addition doesn't overflow iff `self` and `rhs` respect the Duration type invariant + let mut nanos = self.nanos.as_inner() + rhs.nanos.as_inner(); + if nanos >= NANOS_PER_SEC { + nanos -= NANOS_PER_SEC; + if let Some(new_secs) = secs.checked_add(1) { + secs = new_secs; + } else { + return None; + } + } + Some(Duration::new(secs, nanos)) + } else { + None + } + } + + #[kani::ensures(|duration| duration.is_none() || duration.unwrap().is_safe())] + pub const fn checked_sub(self, rhs: Duration) -> Option { + if let Some(mut secs) = self.secs.checked_sub(rhs.secs) { + let nanos = if self.nanos.as_inner() >= rhs.nanos.as_inner() { + self.nanos.as_inner() - rhs.nanos.as_inner() + } else if let Some(sub_secs) = secs.checked_sub(1) { + secs = sub_secs; + // TEST NOTE: this arithmetic doesn't overflow iff `self` and `rhs` respect the Duration type invariant + self.nanos.as_inner() + NANOS_PER_SEC - rhs.nanos.as_inner() + } else { + return None; + }; + Some(Duration::new(secs, nanos)) + } else { + None + } + } +} diff --git a/tests/script-based-pre/cargo_autoharness_type_invariant/type-invariant.expected b/tests/script-based-pre/cargo_autoharness_type_invariant/type-invariant.expected new file mode 100644 index 000000000000..bd15576d5369 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_type_invariant/type-invariant.expected @@ -0,0 +1,110 @@ +Kani generated automatic harnesses for 7 function(s): ++----------------------------+ +| Selected Function | ++============================+ +| Duration::abs_diff | +|----------------------------| +| Duration::checked_add | +|----------------------------| +| Duration::checked_sub | +|----------------------------| +| Duration::new | +|----------------------------| +| Nanoseconds | +|----------------------------| +| Nanoseconds::as_inner | +|----------------------------| +| Nanoseconds::new_unchecked | ++----------------------------+ + +Autoharness: Checking function Nanoseconds::new_unchecked's contract against all possible inputs... +Nanoseconds::new_unchecked\ + - Status: SUCCESS\ + - Description: "|nano| nano.is_safe()" + +Autoharness: Checking function Duration::checked_sub's contract against all possible inputs... +Duration::checked_sub\ + - Status: SUCCESS\ + - Description: "attempt to add with overflow" + +Duration::checked_sub\ + - Status: SUCCESS\ + - Description: "attempt to subtract with overflow" + +Nanoseconds::new_unchecked\ + - Status: SUCCESS\ + - Description: "val < NANOS_PER_SEC" + +Duration::checked_sub\ + - Status: SUCCESS\ + - Description: "|duration| duration.is_none() || duration.unwrap().is_safe()" + +Duration::new\ + - Status: SUCCESS\ + - Description: "|duration| duration.is_safe()" + +Autoharness: Checking function Duration::checked_add's contract against all possible inputs... +Nanoseconds::new_unchecked\ + - Status: SUCCESS\ + - Description: "val < NANOS_PER_SEC" + +Duration::new\ + - Status: SUCCESS\ + - Description: "|duration| duration.is_safe()" + +Duration::checked_add\ + - Status: SUCCESS\ + - Description: "|duration| duration.is_none() || duration.unwrap().is_safe()" + +Duration::checked_add\ + - Status: SUCCESS\ + - Description: "attempt to add with overflow" + +Duration::checked_add\ + - Status: SUCCESS\ + - Description: "attempt to subtract with overflow" + +Autoharness: Checking function Duration::abs_diff against all possible inputs... +Duration::checked_sub\ + - Status: SUCCESS\ + - Description: "attempt to subtract with overflow" + +Duration::checked_sub\ + - Status: SUCCESS\ + - Description: "attempt to subtract with overflow" + +Autoharness: Checking function Duration::new's contract against all possible inputs... +Nanoseconds::new_unchecked\ + - Status: SUCCESS\ + - Description: "val < NANOS_PER_SEC" + +Duration::new\ + - Status: SUCCESS\ + - Description: "|duration| duration.is_safe()" + +std::option::expect_failed\ + - Status: FAILURE\ + - Description: "This is a placeholder message; Kani doesn't support message formatted at runtime" + + +Autoharness Summary: ++----------------------------+-----------------------------+---------------------+ +| Selected Function | Kind of Automatic Harness | Verification Result | ++================================================================================+ +| Duration::abs_diff | #[kani::proof] | Success | +|----------------------------+-----------------------------+---------------------| +| Duration::checked_add | #[kani::proof_for_contract] | Success | +|----------------------------+-----------------------------+---------------------| +| Duration::checked_sub | #[kani::proof_for_contract] | Success | +|----------------------------+-----------------------------+---------------------| +| Nanoseconds | #[kani::proof] | Success | +|----------------------------+-----------------------------+---------------------| +| Nanoseconds::as_inner | #[kani::proof] | Success | +|----------------------------+-----------------------------+---------------------| +| Nanoseconds::new_unchecked | #[kani::proof_for_contract] | Success | +|----------------------------+-----------------------------+---------------------| +| Duration::new | #[kani::proof_for_contract] | Failure | ++----------------------------+-----------------------------+---------------------+ +Note that `kani autoharness` sets default --harness-timeout of 60s and --default-unwind of 20. +If verification failed because of timing out or too low of an unwinding bound, try passing larger values for these arguments (or, if possible, writing a loop contract). +Complete - 6 successfully verified functions, 1 failures, 7 total. diff --git a/tests/script-based-pre/cargo_autoharness_type_invariant/type-invariant.sh b/tests/script-based-pre/cargo_autoharness_type_invariant/type-invariant.sh new file mode 100755 index 000000000000..34e177be9134 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_type_invariant/type-invariant.sh @@ -0,0 +1,9 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +cargo kani autoharness -Z autoharness +# 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;