diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 19f9cbd29b8..c4eeef34d26 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -1652,7 +1652,19 @@ impl GotocCtx<'_, '_> { } VtblEntry::MetadataSize => Some(vt_size.clone()), VtblEntry::MetadataAlign => Some(vt_align.clone()), - VtblEntry::Vacant => None, + VtblEntry::Vacant => { + // vtable_entries with the CONCRETE self type may mark a slot + // vacant where the vtable struct type (built with dyn self in + // trait_vtable_field_types) declares a method pointer: e.g. a + // method with an HRTB predicate a fixed-region function item + // does not satisfy. rustc pads such slots with null; mirror + // that, typed as the declared field. If the type side skipped + // the slot too, keep skipping it. + let field_name = ctx.vtable_field_name(idx); + Type::struct_tag(vtable_name) + .lookup_field_type(field_name, &ctx.symbol_table) + .map(|field_ty| Expr::pointer_constant(0, field_ty)) + } VtblEntry::TraitVPtr(trait_ref) => { let projections = match dst_mir_type.kind() { TyKind::RigidTy(RigidTy::Dynamic(predicates, ..)) => predicates diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 5341844199e..fa181272345 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -127,6 +127,16 @@ impl CodegenUnits { ] .iter() .all(|m| kani_fns.contains_key(&(*m).into())), + &NondetFnModels { + fn0: kani_fns.get(&KaniModel::NondetFn0.into()).copied(), + fn1: kani_fns.get(&KaniModel::NondetFn1.into()).copied(), + fn1_ref: kani_fns.get(&KaniModel::NondetFn1Ref.into()).copied(), + fn2: kani_fns.get(&KaniModel::NondetFn2.into()).copied(), + fn2_ref_ref: kani_fns.get(&KaniModel::NondetFn2RefRef.into()).copied(), + fn2_ref_val: kani_fns.get(&KaniModel::NondetFn2RefVal.into()).copied(), + fn2_val_ref: kani_fns.get(&KaniModel::NondetFn2ValRef.into()).copied(), + fn3: kani_fns.get(&KaniModel::NondetFn3.into()).copied(), + }, ); AUTOHARNESS_MD .set(AutoHarnessMetadata { @@ -540,6 +550,227 @@ fn args_satisfy_predicates(tcx: TyCtxt, def: FnDef, args: &GenericArgs) -> bool ocx.evaluate_obligations_error_on_ambiguity().is_empty() } +/// The nondet closure-model FnDefs, keyed by input shape. By-value models fix their +/// input regions early-bound; the ref-taking variants carry late-bound regions so their +/// fn items satisfy HRTB bounds like `for<'a> Fn(&'a T)`. +#[derive(Clone, Copy, Default)] +pub struct NondetFnModels { + pub fn0: Option, + pub fn1: Option, + pub fn1_ref: Option, + pub fn2: Option, + pub fn2_ref_ref: Option, + pub fn2_ref_val: Option, + pub fn2_val_ref: Option, + pub fn3: Option, +} + +/// Select the nondet model matching the (erased-region) input types' by-ref/by-value +/// shape, returning the model and its type arguments (references peeled: the model's own +/// signature reintroduces them with late-bound regions). Arity-3 ref shapes and deeper +/// are not modeled (1.5% corpus tail). +fn select_nondet_model<'tcx>( + models: &NondetFnModels, + input_tys: &[rustc_middle::ty::Ty<'tcx>], +) -> Option<(FnDef, Vec>)> { + let peel = |t: rustc_middle::ty::Ty<'tcx>| match t.kind() { + rustc_middle::ty::TyKind::Ref(_, inner, rustc_middle::ty::Mutability::Not) => Some(*inner), + _ => None, + }; + let shape: Vec> = input_tys.iter().map(|t| peel(*t)).collect(); + match shape.as_slice() { + [] => models.fn0.map(|m| (m, vec![])), + [None] => models.fn1.map(|m| (m, vec![input_tys[0]])), + [Some(t)] => models.fn1_ref.map(|m| (m, vec![*t])), + [None, None] => models.fn2.map(|m| (m, input_tys.to_vec())), + [Some(a), Some(b)] => models.fn2_ref_ref.map(|m| (m, vec![*a, *b])), + [Some(a), None] => models.fn2_ref_val.map(|m| (m, vec![*a, input_tys[1]])), + [None, Some(b)] => models.fn2_val_ref.map(|m| (m, vec![input_tys[0], *b])), + [None, None, None] => models.fn3.map(|m| (m, input_tys.to_vec())), + _ => None, + } +} + +/// An Fn-bound signature that references other generic parameters (e.g. `F: Fn(T) -> T`): +/// its concrete form depends on the instantiation chosen for those parameters, so the +/// candidate fn-item type is constructed per candidate choice +/// (c.f. [resolve_deferred_fn_slots]). +struct DeferredFnSpec<'tcx> { + inputs: rustc_middle::ty::Ty<'tcx>, + output: rustc_middle::ty::Ty<'tcx>, +} + +/// For type parameters bound by `Fn`/`FnMut`/`FnOnce`, derive a candidate instantiation: +/// the *function item type* of the matching-arity `kani::arbitrary::nondet_fn` model, +/// instantiated with the bound's argument and return types. Function items implement all +/// three `Fn` traits and are zero-sized; the models return a fresh nondeterministic value +/// per call, over-approximating every real closure's behavior. +/// +/// Returns a map from parameter index (among the identity args) to candidate types. +/// Signature types that themselves mention generic parameters are only usable if those +/// parameters appear EARLIER in the parameter list (they are substituted with the current +/// choice by the caller); v1 keeps it simple and only admits fully concrete signatures. +fn fn_bound_candidates<'tcx>( + tcx: TyCtxt<'tcx>, + def: FnDef, + nondet_fns: &NondetFnModels, +) -> (FxHashMap>, FxHashMap>) { + let def_id = rustc_internal::internal(tcx, def.def_id()); + let mut out: FxHashMap> = FxHashMap::default(); + let mut deferred: FxHashMap> = FxHashMap::default(); + let fn_once = tcx.lang_items().fn_once_trait(); + let fn_mut = tcx.lang_items().fn_mut_trait(); + let fn_tr = tcx.lang_items().fn_trait(); + // Collect Fn-ish trait predicates keyed by the self param index, with tupled inputs. + let mut sig_inputs: FxHashMap = FxHashMap::default(); + for (predicate, _span) in tcx.predicates_of(def_id).predicates { + let Some(tp) = predicate.as_trait_clause() else { continue }; + // HRTB bounds (e.g. for<'a> FnOnce(&'a Self)) carry late-bound regions; erase them + // rather than skipping the binder, which would leak escaping bound vars into the + // trait solver (ICE: !self_ty.has_escaping_bound_vars()). + let tp = tcx.instantiate_bound_regions_with_erased(tp); + let tid = Some(tp.def_id()); + if tid != fn_once && tid != fn_mut && tid != fn_tr { + continue; + } + let rustc_middle::ty::TyKind::Param(param_ty) = tp.self_ty().kind() else { continue }; + // Second generic arg of the Fn traits is the tupled inputs. + let Some(inputs) = tp.trait_ref.args.get(1).and_then(|a| a.as_type()) else { + continue; + }; + sig_inputs.insert(param_ty.index as usize, inputs); + } + if sig_inputs.is_empty() { + return (out, deferred); + } + // The return type comes from the FnOnce::Output projection bound. + let mut sig_output: FxHashMap = FxHashMap::default(); + for (predicate, _span) in tcx.predicates_of(def_id).predicates { + let Some(proj) = predicate.as_projection_clause() else { continue }; + let proj = tcx.instantiate_bound_regions_with_erased(proj); + let rustc_middle::ty::TyKind::Param(param_ty) = proj.projection_term.self_ty().kind() + else { + continue; + }; + if let Some(term_ty) = proj.term.as_type() { + sig_output.insert(param_ty.index as usize, term_ty); + } + } + for (idx, inputs) in sig_inputs { + let rustc_middle::ty::TyKind::Tuple(input_tys) = inputs.kind() else { continue }; + let output = sig_output.get(&idx).copied().unwrap_or(tcx.types.unit); + use rustc_middle::ty::TypeVisitableExt; + if inputs.has_param() || output.has_param() { + // Signature references other generic parameters: defer construction until a + // candidate choice for those parameters is made. + // SAFETY of the transmute-free 'static: predicates_of types live for the whole + // compilation session ('tcx); we only use them within this query's lifetime. + deferred.insert(idx, DeferredFnSpec { inputs, output }); + continue; + } + // nondet_fnN: generic args are the inputs followed by the return type. + let input_vec: Vec = input_tys.iter().collect(); + let Some((model, model_tys)) = select_nondet_model(nondet_fns, &input_vec) else { + continue; + }; + let mut args: Vec = + model_tys.iter().map(|t| GenericArgKind::Type(rustc_internal::stable(t))).collect(); + args.push(GenericArgKind::Type(rustc_internal::stable(output))); + let args = GenericArgs(args); + // Instance::resolve does not check trait bounds; the model requires R: Arbitrary + // (its body calls kani::any::()), so verify the model's own predicates or the + // assert in harness generation fires (e.g. FnOnce() -> error::Error in syn). + if !args_satisfy_predicates(tcx, model, &args) { + continue; + } + let Ok(inst) = Instance::resolve(model, &args) else { continue }; + // The function item TYPE of the resolved instance. + out.entry(idx).or_default().push(inst.ty()); + } + (out, deferred) +} + +/// Resolve deferred Fn-bound slots for a concrete candidate `choice`: substitute the +/// chosen types into the deferred signature, construct the matching-arity nondet_fn item +/// type, and overwrite the placeholder in `choice`. Returns false if any deferred slot +/// cannot be resolved for this choice (skip it). +#[allow(clippy::too_many_arguments)] +fn resolve_deferred_fn_slots<'tcx>( + tcx: TyCtxt<'tcx>, + identity_args: &GenericArgs, + type_slots: &[usize], + choice: &mut [Ty], + deferred: &FxHashMap>, + nondet_fns: &NondetFnModels, +) -> bool { + if deferred.is_empty() { + return true; + } + // Build a full internal substitution from the current choice (placeholders included: + // deferred slots hold unit, which is fine as long as no deferred signature references + // another Fn-bound parameter). + let mut next_type = 0usize; + let stable_args = GenericArgs( + identity_args + .0 + .iter() + .map(|arg| match arg { + GenericArgKind::Type(_) => { + let t = choice[next_type]; + next_type += 1; + GenericArgKind::Type(t) + } + GenericArgKind::Lifetime(_) => { + GenericArgKind::Lifetime(Region { kind: RegionKind::ReErased }) + } + GenericArgKind::Const(_) => GenericArgKind::Const( + TyConst::try_from_target_usize(AUTOHARNESS_CONST_GENERIC_VALUE).unwrap(), + ), + }) + .collect(), + ); + let args_internal = rustc_internal::internal(tcx, &stable_args); + for (&idx, spec) in deferred { + use rustc_middle::ty::TypeVisitableExt; + // `instantiate` yields an `Unnormalized` value on this toolchain; normalize before + // inspecting. The substitution may produce unnormalizable projections (e.g. + // ::Val for a choice that does not satisfy the bound); normalize here and + // skip the choice on failure, rather than letting Instance::resolve ICE on it. + let inputs = + rustc_middle::ty::EarlyBinder::bind(spec.inputs).instantiate(tcx, args_internal); + let output = + rustc_middle::ty::EarlyBinder::bind(spec.output).instantiate(tcx, args_internal); + let typing_env = rustc_middle::ty::TypingEnv::fully_monomorphized(); + let Ok(inputs) = tcx.try_normalize_erasing_regions(typing_env, inputs) else { + return false; + }; + let Ok(output) = tcx.try_normalize_erasing_regions(typing_env, output) else { + return false; + }; + // Bail if the substitution left any generic parameter unresolved. + if inputs.has_param() || output.has_param() { + return false; + } + let rustc_middle::ty::TyKind::Tuple(input_tys) = inputs.kind() else { return false }; + let input_vec: Vec = input_tys.iter().collect(); + let Some((model, model_tys)) = select_nondet_model(nondet_fns, &input_vec) else { + return false; + }; + let mut margs: Vec = + model_tys.iter().map(|t| GenericArgKind::Type(rustc_internal::stable(t))).collect(); + margs.push(GenericArgKind::Type(rustc_internal::stable(output))); + let margs = GenericArgs(margs); + // As in fn_bound_candidates: enforce the model's own R: Arbitrary bound. + if !args_satisfy_predicates(tcx, model, &margs) { + return false; + } + let Ok(inst) = Instance::resolve(model, &margs) else { return false }; + let Some(pos) = type_slots.iter().position(|&s| s == idx) else { return false }; + choice[pos] = inst.ty(); + } + true +} + /// Try to find a monomorphic instantiation of the generic function `fn_item` for which we can /// generate an automatic harness. Substitute each type parameter with the first candidate from /// `generic_instantiation_candidates` such that all of the function's trait bounds are satisfied @@ -547,7 +778,11 @@ fn args_satisfy_predicates(tcx: TyCtxt, def: FnDef, args: &GenericArgs) -> bool /// Return the reason (to be attached to [AutoHarnessSkipReason::GenericFn]) if no candidate /// satisfies the bounds, or if the function has const generic parameters, which we do not /// support instantiating yet. -fn choose_generic_instantiation(tcx: TyCtxt, fn_item: CrateItem) -> Result { +fn choose_generic_instantiation( + tcx: TyCtxt, + fn_item: CrateItem, + nondet_fns: &NondetFnModels, +) -> Result { let TyKind::RigidTy(RigidTy::FnDef(def, identity_args)) = fn_item.ty().kind() else { return Err("not a function definition".to_string()); }; @@ -568,6 +803,7 @@ fn choose_generic_instantiation(tcx: TyCtxt, fn_item: CrateItem) -> Result = identity_args .0 .iter() @@ -583,6 +819,17 @@ fn choose_generic_instantiation(tcx: TyCtxt, fn_item: CrateItem) -> Result Result = + let mut choice: Vec = odometer.iter().enumerate().map(|(i, &c)| slot_candidates[i][c]).collect(); + let deferred_ok = resolve_deferred_fn_slots( + tcx, + &identity_args, + &type_slots, + &mut choice, + &deferred_fn, + nondet_fns, + ); // Skip choices already tried in the uniform pass. let uniform = choice.iter().all(|ty| *ty == choice[0]) && generic_instantiation_candidates().contains(&choice[0]); - if !uniform { + if !uniform && deferred_ok { if let Some(instance) = try_choice(&choice) { return Ok(instance); } @@ -702,6 +957,7 @@ fn automatic_harness_partition( smart_pointer_models: SmartPointerModels, kani_assert_def: FnDef, unbounded_slice_available: bool, + nondet_fns: &NondetFnModels, ) -> (Vec<(Instance, AutoHarnessCaveats)>, BTreeMap) { let crate_fn_defs = rustc_public::local_crate().fn_defs().into_iter().collect::>(); // Filter out CrateItems that are functions, but not functions defined in the crate itself, i.e., rustc-inserted functions @@ -803,6 +1059,11 @@ fn automatic_harness_partition( continue; } } + // Function items (Fn-bound instantiations, c.f. fn_bound_candidates) are + // zero-sized values materialized as constants; no Arbitrary impl is involved. + if matches!(arg.ty.kind(), TyKind::RigidTy(RigidTy::FnDef(..))) { + continue; + } // Note: we deliberately do not insert the verdict into `ty_arbitrary_cache` here. // The cache stores whether a type implements (or can derive) Arbitrary, which is the // wrong semantics for types that are supported in argument position only (raw @@ -865,7 +1126,7 @@ fn automatic_harness_partition( // and its name (e.g. `foo::`) reflects that. let instance = match Instance::try_from(func) { Ok(instance) => instance, - Err(_) => match choose_generic_instantiation(tcx, func) { + Err(_) => match choose_generic_instantiation(tcx, func, nondet_fns) { Ok(instance) => instance, Err(detail) => { skipped.insert( diff --git a/kani-compiler/src/kani_middle/kani_functions.rs b/kani-compiler/src/kani_middle/kani_functions.rs index 8d81089774e..20d4fe00902 100644 --- a/kani-compiler/src/kani_middle/kani_functions.rs +++ b/kani-compiler/src/kani_middle/kani_functions.rs @@ -63,6 +63,22 @@ pub enum KaniIntrinsic { pub enum KaniModel { #[strum(serialize = "AlignOfDynObjectModel")] AlignOfDynObject, + #[strum(serialize = "NondetFn0Model")] + NondetFn0, + #[strum(serialize = "NondetFn1Model")] + NondetFn1, + #[strum(serialize = "NondetFn1RefModel")] + NondetFn1Ref, + #[strum(serialize = "NondetFn2Model")] + NondetFn2, + #[strum(serialize = "NondetFn2RefRefModel")] + NondetFn2RefRef, + #[strum(serialize = "NondetFn2RefValModel")] + NondetFn2RefVal, + #[strum(serialize = "NondetFn2ValRefModel")] + NondetFn2ValRef, + #[strum(serialize = "NondetFn3Model")] + NondetFn3, #[strum(serialize = "AlignOfValRawModel")] AlignOfVal, #[strum(serialize = "AnySliceMutUnboundedModel")] @@ -211,6 +227,14 @@ impl KaniModel { | KaniModel::AnySliceMutUnbounded | KaniModel::AnySliceRefUnbounded | KaniModel::AnyVecUnbounded + | KaniModel::NondetFn0 + | KaniModel::NondetFn1 + | KaniModel::NondetFn1Ref + | KaniModel::NondetFn2 + | KaniModel::NondetFn2RefRef + | KaniModel::NondetFn2RefVal + | KaniModel::NondetFn2ValRef + | KaniModel::NondetFn3 ) } } diff --git a/kani-compiler/src/kani_middle/transform/automatic.rs b/kani-compiler/src/kani_middle/transform/automatic.rs index 78f76ca6da6..763d3d9d681 100644 --- a/kani-compiler/src/kani_middle/transform/automatic.rs +++ b/kani-compiler/src/kani_middle/transform/automatic.rs @@ -1154,6 +1154,27 @@ fn call_kani_any_for_ty( invariant_cache: &mut FxHashMap, mined_cache: &mut FxHashMap>, ) -> Local { + // Function items (Fn-bound instantiations, c.f. fn_bound_candidates) are zero-sized: + // materialize the value as a zero-sized constant. + if matches!(ty.kind(), TyKind::RigidTy(RigidTy::FnDef(..))) { + let span = source.span(body.blocks()); + let lcl = body.new_local(ty, span, mutability); + body.assign_to( + Place::from(lcl), + Rvalue::Use( + Operand::Constant(ConstOperand { + span, + user_ty: None, + const_: MirConst::try_new_zero_sized(ty) + .expect("function item types are zero-sized"), + }), + WithRetag::No, + ), + source, + InsertPosition::Before, + ); + return lcl; + } // Unbounded generation for slices (&[T]/&mut [T]) and Vec of primitive // integer/float elements: fresh allocations of nondeterministic size, so results hold // for all lengths (mirrors the eligibility decision in automatic_harness_partition). diff --git a/library/kani/src/arbitrary.rs b/library/kani/src/arbitrary.rs index a109fc76f04..b5562cd0574 100644 --- a/library/kani/src/arbitrary.rs +++ b/library/kani/src/arbitrary.rs @@ -172,3 +172,71 @@ pub fn slice_validity_assume(_ptr: *const u8, _len: usize) { #[cfg(not(kani))] unreachable!("kani::slice_validity_assume is a verification-only hook"); } + +/// Nondeterministic functions for instantiating `Fn`/`FnMut`/`FnOnce`-bounded type +/// parameters of automatic harnesses: the parameter is instantiated with the *function +/// item type* of the matching-arity model below (function items implement all three `Fn` +/// traits and are zero-sized, so generating the value is trivial). Each call returns a +/// fresh nondeterministic value, which over-approximates the behavior of every real +/// closure with that signature (including stateful `FnMut` closures); verifying the +/// harness against this instantiation therefore covers the function-under-test's own code +/// for any closure behavior. +/// +/// These models are *optional* (c.f. `KaniModel::is_optional`). +#[kanitool::fn_marker = "NondetFn0Model"] +#[inline(never)] +#[doc(hidden)] +pub fn nondet_fn0() -> R { + crate::any() +} + +#[kanitool::fn_marker = "NondetFn1Model"] +#[inline(never)] +#[doc(hidden)] +pub fn nondet_fn1(_a: A) -> R { + crate::any() +} + +#[kanitool::fn_marker = "NondetFn1RefModel"] +#[inline(never)] +#[doc(hidden)] +/// Region-polymorphic: the fn item's late-bound lifetime lets it satisfy HRTB bounds +/// like `for<'a> Fn(&'a T) -> R` that the early-bound by-value models cannot. +pub fn nondet_fn1_ref(_a: &T) -> R { + crate::any() +} + +#[kanitool::fn_marker = "NondetFn2RefRefModel"] +#[inline(never)] +#[doc(hidden)] +pub fn nondet_fn2_ref_ref(_a: &A, _b: &B) -> R { + crate::any() +} + +#[kanitool::fn_marker = "NondetFn2RefValModel"] +#[inline(never)] +#[doc(hidden)] +pub fn nondet_fn2_ref_val(_a: &A, _b: B) -> R { + crate::any() +} + +#[kanitool::fn_marker = "NondetFn2ValRefModel"] +#[inline(never)] +#[doc(hidden)] +pub fn nondet_fn2_val_ref(_a: A, _b: &B) -> R { + crate::any() +} + +#[kanitool::fn_marker = "NondetFn2Model"] +#[inline(never)] +#[doc(hidden)] +pub fn nondet_fn2(_a: A, _b: B) -> R { + crate::any() +} + +#[kanitool::fn_marker = "NondetFn3Model"] +#[inline(never)] +#[doc(hidden)] +pub fn nondet_fn3(_a: A, _b: B, _c: C) -> R { + crate::any() +} diff --git a/tests/script-based-pre/cargo_autoharness_fn_bounds/Cargo.toml b/tests/script-based-pre/cargo_autoharness_fn_bounds/Cargo.toml new file mode 100644 index 00000000000..e798d3f6737 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_fn_bounds/Cargo.toml @@ -0,0 +1,6 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +[package] +name = "cargo_autoharness_fn_bounds" +version = "0.1.0" +edition = "2021" diff --git a/tests/script-based-pre/cargo_autoharness_fn_bounds/config.yml b/tests/script-based-pre/cargo_autoharness_fn_bounds/config.yml new file mode 100644 index 00000000000..1b1690fcd3e --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_fn_bounds/config.yml @@ -0,0 +1,5 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: fn_bounds.sh +expected: fn_bounds.expected +exit_code: 1 diff --git a/tests/script-based-pre/cargo_autoharness_fn_bounds/fn_bounds.expected b/tests/script-based-pre/cargo_autoharness_fn_bounds/fn_bounds.expected new file mode 100644 index 00000000000..16576486a44 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_fn_bounds/fn_bounds.expected @@ -0,0 +1,11 @@ + - Status: SATISFIED +| cargo_autoharness_fn_bounds | apply:: u8 {kani::arbitrary::nondet_fn1::}> | #[kani::proof] | Success | +| cargo_autoharness_fn_bounds | apply_generic:: i32 {kani::arbitrary::nondet_fn1::}> | #[kani::proof] | Success | +| cargo_autoharness_fn_bounds | branches:: bool {kani::arbitrary::nondet_fn1::}> | #[kani::proof] | Success | +| cargo_autoharness_fn_bounds | inspect_with:: fn(&'a u32) {kani::arbitrary::nondet_fn1_ref::}> | #[kani::proof] | Success | +| cargo_autoharness_fn_bounds | packet_size | #[kani::proof] | Success | +| cargo_autoharness_fn_bounds | run_once::}> | #[kani::proof] | Success | +| cargo_autoharness_fn_bounds | scoped:: fn(&'a u8) -> bool {kani::arbitrary::nondet_fn1_ref::}> | #[kani::proof] | Success | +| cargo_autoharness_fn_bounds | tuple_arg | #[kani::proof] | Success | +| cargo_autoharness_fn_bounds | apply_buggy:: u8 {kani::arbitrary::nondet_fn1::}> | #[kani::proof] | Failure | +| cargo_autoharness_fn_bounds | fold2:: u32 {kani::arbitrary::nondet_fn2::}> | #[kani::proof] | Failure | diff --git a/tests/script-based-pre/cargo_autoharness_fn_bounds/fn_bounds.sh b/tests/script-based-pre/cargo_autoharness_fn_bounds/fn_bounds.sh new file mode 100755 index 00000000000..ba322c8517d --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_fn_bounds/fn_bounds.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +# Fn-bounded type parameters instantiate with nondeterministic function items +# (fresh nondet result per call = over-approximation of every closure); Iterator-bounded +# ones with std::vec::IntoIter over unbounded nondeterministic vectors. +cargo kani autoharness -Z autoharness --output-format=regular diff --git a/tests/script-based-pre/cargo_autoharness_fn_bounds/src/lib.rs b/tests/script-based-pre/cargo_autoharness_fn_bounds/src/lib.rs new file mode 100644 index 00000000000..e3de5507f22 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_fn_bounds/src/lib.rs @@ -0,0 +1,83 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Fn-bounded generic functions: previously skipped ("no candidate type satisfies the +// function's trait bounds"), now instantiated with nondeterministic function items. + +// TEST NOTE: harnessed as apply::; PASSES (wrapping arithmetic). +pub fn apply u8>(f: F, x: u8) -> u8 { + f(x).wrapping_add(1) +} + +// TEST NOTE: FAILS: the closure result is unconstrained, so the addition can overflow — +// a real bug class in the generic function's own code, found for ANY closure behavior. +pub fn apply_buggy u8>(f: F, x: u8) -> u8 { + f(x) + 1 +} + +// TEST NOTE: FnMut with two arguments; the fold-style accumulation overflows: FAILS. +pub fn fold2 u32>(mut f: F, a: u32, b: u32) -> u32 { + f(a, b) + f(b, a) +} + +// TEST NOTE: FnOnce returning unit: PASSES (nothing to go wrong). +pub fn run_once ()>(f: F) { + f() +} + +// TEST NOTE: cover check must be SATISFIED: the nondet closure's results genuinely cover +// the range (both branches reachable). +pub fn branches bool>(f: F, x: u8) { + if f(x) { + kani::cover!(true, "true branch reachable"); + } else { + kani::cover!(true, "false branch reachable"); + } +} + +// TEST NOTE: harnessed as apply_generic::>: the closure +// signature references another generic parameter, resolved per candidate choice. +pub fn apply_generic T>(f: F, x: T) -> T { + f(x) +} + +// TEST NOTE (regression, tap ICE): HRTB closure bound (for<'a> via &Self sugar); +// previously leaked escaping bound vars into the trait solver. +pub fn inspect_with(f: F, v: u32) { + f(&v); +} + +// TEST NOTE (regression, nom ICE): enum variant holding an anonymous tuple field; +// previously the derive-style generator had no tuple vocabulary. +pub enum Packet { + Pair((u8, u16)), + Empty, +} +pub fn packet_size(p: Packet) -> usize { + match p { + Packet::Pair((a, _)) => a as usize, + Packet::Empty => 0, + } +} + +// TEST NOTE: top-level anonymous tuple argument, generated elementwise. +pub fn tuple_arg(t: (u8, bool)) -> u8 { + if t.1 { t.0 } else { 0 } +} + +// TEST NOTE (regression, reqwest ICE): HRTB closure param wrapped in a struct and +// coerced to a trait object. Requires the region-polymorphic nondet_fn1_ref model +// (an early-bound fn item leaves the method slot vacant in the concrete vtable). +struct ScopeFn(F); +trait Scope { + fn run(&self) -> bool; +} +impl bool> Scope for ScopeFn { + fn run(&self) -> bool { + (self.0)(&7) + } +} +pub fn scoped bool + 'static>(f: F) -> bool { + let s: Box = Box::new(ScopeFn(f)); + s.run() +}