From cf00d46c25503fb70791a173ef34f9577267a8f1 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 28 Jul 2026 01:06:28 +0000 Subject: [PATCH 1/5] Autoharness: support generic functions Previously, autoharness skipped all generic functions. Now, it generates a harness for a single monomorphic instantiation: each type parameter is substituted with the first candidate from a fixed list of primitive types (i32, u32, usize, bool, char) such that all of the function's trait bounds are satisfied, checked with the trait solver (rustc_trait_selection::ObligationCtxt). Lifetime parameters are erased. Functions whose bounds no candidate satisfies, or with const generic parameters, are still skipped as 'Generic Function'. The generated harness's name reflects the chosen instantiation (e.g. foo::), making explicit that verification covers only that instantiation; the documentation spells out this underapproximation. Functions with any number of type, lifetime, and (unsupported) const parameters are handled, including methods of generic impl blocks, impl-Trait arguments, and functions with contracts. For contract harnesses, harness metadata now stores the definition-level name of the target function rather than the instantiated one, since gen_contracts_metadata matches it against definition-level ContractedFunction names. This addresses the 'Generics' item of the automatic harness generation tracking issue, the last unchecked entry together with the invariants and pointers work. Towards #3832 Co-authored-by: Kiro --- .../src/reference/experimental/autoharness.md | 32 ++--- .../src/kani_middle/codegen_units.rs | 131 +++++++++++++++--- kani-compiler/src/kani_middle/metadata.rs | 6 +- kani-compiler/src/main.rs | 2 + .../exclude.expected | 34 ++--- .../cargo_autoharness_exclude/src/lib.rs | 2 +- .../cargo_autoharness_filter/filter.expected | 30 ++-- .../cargo_autoharness_filter/src/lib.rs | 7 +- .../cargo_autoharness_generics/Cargo.toml | 10 ++ .../cargo_autoharness_generics/config.yml | 5 + .../generics.expected | 11 ++ .../cargo_autoharness_generics/generics.sh | 5 + .../cargo_autoharness_generics/src/lib.rs | 81 +++++++++++ .../include.expected | 34 ++--- .../cargo_autoharness_include/src/lib.rs | 2 +- 15 files changed, 304 insertions(+), 88 deletions(-) create mode 100644 tests/script-based-pre/cargo_autoharness_generics/Cargo.toml create mode 100644 tests/script-based-pre/cargo_autoharness_generics/config.yml create mode 100644 tests/script-based-pre/cargo_autoharness_generics/generics.expected create mode 100755 tests/script-based-pre/cargo_autoharness_generics/generics.sh create mode 100644 tests/script-based-pre/cargo_autoharness_generics/src/lib.rs diff --git a/docs/src/reference/experimental/autoharness.md b/docs/src/reference/experimental/autoharness.md index a57ca448f1d1..a0a6866e9b34 100644 --- a/docs/src/reference/experimental/autoharness.md +++ b/docs/src/reference/experimental/autoharness.md @@ -115,7 +115,9 @@ Kani will detect if a struct or enum could implement `Arbitrary` and derive it a Note that this automatic derivation feature is only available for autoharness. ### Generic Functions -The current implementation does not generate harnesses for generic functions. +For a generic function, Kani generates a harness for a single monomorphic instantiation of the function: +it substitutes every type parameter with the first candidate from a fixed list of primitive types +(starting with `i32`) such that all of the function's trait bounds are satisfied, and erases lifetime parameters. For example, given: ```rust fn foo(x: T, y: T) { @@ -124,23 +126,19 @@ fn foo(x: T, y: T) { } } ``` -Kani would report that no functions were eligible for automatic harness generation. - -If, however, some caller of `foo` is eligible for an automatic harness, then a monomorphized version of `foo` may still be reachable during verification. -For instance, if we add `main`: -```rust -fn main() { - let x: u8 = 2; - let y: u8 = 2; - foo(x, y); -} +Kani generates and runs a harness that verifies `foo::`, and the summary table shows the +instantiated name, e.g.: ``` -and run the autoharness subcommand, we get: +| Crate | Selected Function | Kind of Automatic Harness | Verification Result | +| my_crate | foo:: | #[kani::proof] | Failure | ``` -Autoharness: Checking function main against all possible inputs... +Note that verifying a single instantiation is an underapproximation of all of the function's possible behaviors: +a successful result for `foo::` does not imply that other instantiations of `foo` are also safe. +Kani makes this explicit by displaying the instantiated name of the verified function. -Failed Checks: x and y are equal - File: "src/lib.rs", line 3, in foo:: +Kani skips a generic function (with skip reason "Generic Function") if: +- no candidate type satisfies the function's trait bounds, or +- the function has const generic parameters, which Kani does not instantiate yet. -VERIFICATION:- FAILED -``` +If some caller of a generic function is eligible for an automatic harness, then additional monomorphized +versions of the generic function may still be reachable (and thus verified) through the caller's harness. diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 4b9236c5d45c..537dd2781c05 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -24,13 +24,17 @@ use kani_metadata::{ use regex::RegexSet; use rustc_data_structures::fx::{FxHashMap, FxHashSet}; use rustc_hir::def_id::DefId; -use rustc_middle::ty::TyCtxt; +use rustc_infer::infer::TyCtxtInferExt; +use rustc_middle::ty::{self, TyCtxt, TypingMode}; use rustc_public::mir::mono::Instance; use rustc_public::rustc_internal; -use rustc_public::ty::{FnDef, GenericArgKind, GenericArgs, RigidTy, Ty, TyKind}; +use rustc_public::ty::{ + FnDef, GenericArgKind, GenericArgs, IntTy, Region, RegionKind, RigidTy, Ty, TyKind, UintTy, +}; use rustc_public::{CrateDef, CrateItem}; use rustc_public_bridge::IndexedVal; use rustc_session::config::OutputType; +use rustc_trait_selection::traits::{Obligation, ObligationCause, ObligationCtxt}; use std::collections::{BTreeMap, BTreeSet, HashMap, HashSet}; use std::fs::File; use std::io::BufWriter; @@ -410,6 +414,79 @@ fn autoharness_filtered_out( !included || excluded } +/// The candidate types for instantiating the type parameters of a generic function, in the order +/// in which we try them. We start with `i32` since that is Rust's default integer type, and +/// primitive types satisfy the most common trait bounds (`Copy`, `Clone`, `Ord`, `Hash`, +/// `Default`, `Debug`, etc.) as well as Kani's `Arbitrary`. +fn generic_instantiation_candidates() -> Vec { + vec![ + Ty::from_rigid_kind(RigidTy::Int(IntTy::I32)), + Ty::from_rigid_kind(RigidTy::Uint(UintTy::U32)), + Ty::from_rigid_kind(RigidTy::Uint(UintTy::Usize)), + Ty::from_rigid_kind(RigidTy::Bool), + Ty::from_rigid_kind(RigidTy::Char), + ] +} + +/// Check whether instantiating the generic parameters of `def` with `args` satisfies all of +/// `def`'s predicates (trait bounds and where clauses). +/// `args` must be fully monomorphic. +fn args_satisfy_predicates(tcx: TyCtxt, def: FnDef, args: &GenericArgs) -> bool { + let infcx = tcx.infer_ctxt().build(TypingMode::PostAnalysis); + let ocx = ObligationCtxt::new(&infcx); + let param_env = ty::ParamEnv::empty(); + let cause = ObligationCause::dummy(); + + let def_id = rustc_internal::internal(tcx, def.def_id()); + let args_internal = rustc_internal::internal(tcx, args); + let predicates = tcx.predicates_of(def_id).instantiate(tcx, args_internal); + for (predicate, _span) in predicates { + ocx.register_obligation(Obligation::new(tcx, cause.clone(), param_env, predicate)); + } + ocx.evaluate_obligations_error_on_ambiguity().is_empty() +} + +/// 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 +/// (using the same candidate for every type parameter), and erase lifetime parameters. +/// Return `None` 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) -> Option { + let TyKind::RigidTy(RigidTy::FnDef(def, identity_args)) = fn_item.ty().kind() else { + return None; + }; + + if identity_args.0.iter().any(|arg| matches!(arg, GenericArgKind::Const(_))) { + return None; + } + + for candidate in generic_instantiation_candidates() { + let args = GenericArgs( + identity_args + .0 + .iter() + .map(|arg| match arg { + GenericArgKind::Type(_) => GenericArgKind::Type(candidate), + GenericArgKind::Lifetime(_) => { + GenericArgKind::Lifetime(Region { kind: RegionKind::ReErased }) + } + GenericArgKind::Const(_) => unreachable!("const generics filtered out above"), + }) + .collect(), + ); + if !args_satisfy_predicates(tcx, def, &args) { + continue; + } + if let Ok(instance) = Instance::resolve(def, &args) + && instance.has_body() + { + return Some(instance); + } + } + None +} + /// Partition every function in the crate into (chosen, skipped), where `chosen` is a vector of the Instances for which we'll generate automatic harnesses, /// and `skipped` is a map of function names to the reason why we skipped them. fn automatic_harness_partition( @@ -435,21 +512,10 @@ fn automatic_harness_partition( // Cache whether a type implements or can derive Arbitrary let mut ty_arbitrary_cache: FxHashMap = FxHashMap::default(); - // If `func` is not eligible for an automatic harness, return the reason why; if it is eligible, return None. + // If `instance` is not eligible for an automatic harness, return the reason why; if it is eligible, return None. // Note that we only return one reason for ineligiblity, when there could be multiple; // we can revisit this implementation choice in the future if users request more verbose output. - let mut skip_reason = |fn_item: CrateItem| -> Option { - if KaniAttributes::for_def_id(tcx, fn_item.def_id()).is_kani_instrumentation() { - return Some(AutoHarnessSkipReason::KaniImpl); - } - - let instance = match Instance::try_from(fn_item) { - Ok(inst) => inst, - Err(_) => { - return Some(AutoHarnessSkipReason::GenericFn); - } - }; - + let mut skip_reason = |instance: Instance| -> Option { if !instance.has_body() { return Some(AutoHarnessSkipReason::NoBody); } @@ -475,7 +541,8 @@ fn automatic_harness_partition( } // Each argument of `instance` must implement Arbitrary. - // Note that we've already filtered out generic functions, so we know that each of these arguments has a concrete type. + // Note that generic functions have been instantiated with concrete types at this point, + // so we know that each of these arguments has a concrete type. let mut problematic_args = vec![]; for (idx, arg) in body.arg_locals().iter().enumerate() { if !ty_arbitrary_cache.contains_key(&arg.ty) { @@ -510,10 +577,36 @@ fn automatic_harness_partition( let mut skipped = BTreeMap::new(); for func in crate_fns { - if let Some(reason) = skip_reason(func) { - skipped.insert(crate::kani_middle::strip_local_crate_prefix(func.name()), reason); + if KaniAttributes::for_def_id(tcx, func.def_id()).is_kani_instrumentation() { + skipped.insert( + crate::kani_middle::strip_local_crate_prefix(func.name()), + AutoHarnessSkipReason::KaniImpl, + ); + continue; + } + + // For generic functions, try to find a monomorphic instantiation whose bounds are + // satisfied; the generated harness verifies the function for that instantiation only, + // and its name (e.g. `foo::`) reflects that. + let instance = match Instance::try_from(func) { + Ok(instance) => instance, + Err(_) => { + if let Some(instance) = choose_generic_instantiation(tcx, func) { + instance + } else { + skipped.insert( + crate::kani_middle::strip_local_crate_prefix(func.name()), + AutoHarnessSkipReason::GenericFn, + ); + continue; + } + } + }; + + if let Some(reason) = skip_reason(instance) { + skipped.insert(crate::kani_middle::strip_local_crate_prefix(instance.name()), reason); } else { - chosen.push(Instance::try_from(func).unwrap()); + chosen.push(instance); } } diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs index d2348ab7b132..5f8287bf64dc 100644 --- a/kani-compiler/src/kani_middle/metadata.rs +++ b/kani-compiler/src/kani_middle/metadata.rs @@ -139,7 +139,11 @@ pub fn gen_automatic_proof_metadata( 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() } + // Use the definition's name rather than the instance's (`pretty_name`), since the two + // differ for generic functions under contract (e.g. `foo::` vs. `foo`), and + // `gen_contracts_metadata` matches `target_fn` against the definition-level names stored + // in `ContractedFunction`. + HarnessKind::ProofForContract { target_fn: strip_local_crate_prefix(def.name()) } } else { HarnessKind::Proof }; diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs index cf00140c348c..f3d396fb4825 100644 --- a/kani-compiler/src/main.rs +++ b/kani-compiler/src/main.rs @@ -30,6 +30,7 @@ extern crate rustc_errors; extern crate rustc_hir; extern crate rustc_hir_pretty; extern crate rustc_index; +extern crate rustc_infer; extern crate rustc_interface; extern crate rustc_metadata; extern crate rustc_middle; @@ -40,6 +41,7 @@ extern crate rustc_public_bridge; extern crate rustc_session; extern crate rustc_span; extern crate rustc_target; +extern crate rustc_trait_selection; // We can't add this directly as a dependency because we need the version to match rustc extern crate tempfile; diff --git a/tests/script-based-pre/cargo_autoharness_exclude/exclude.expected b/tests/script-based-pre/cargo_autoharness_exclude/exclude.expected index 9c006d210262..5a714b76557d 100644 --- a/tests/script-based-pre/cargo_autoharness_exclude/exclude.expected +++ b/tests/script-based-pre/cargo_autoharness_exclude/exclude.expected @@ -1,29 +1,31 @@ -Kani generated automatic harnesses for 1 function(s): -+---------------------------+-------------------+ -| Crate | Selected Function | -+===============================================+ -| cargo_autoharness_include | include::simple | -+---------------------------+-------------------+ +Kani generated automatic harnesses for 2 function(s): ++---------------------------+-------------------------+ +| Crate | Selected Function | ++=====================================================+ +| cargo_autoharness_include | include::generic:: | +|---------------------------+-------------------------| +| cargo_autoharness_include | include::simple | ++---------------------------+-------------------------+ -Kani did not generate automatic harnesses for 2 function(s). +Kani did not generate automatic harnesses for 1 function(s). If you believe that the provided reason is incorrect and Kani should have generated an automatic harness, please comment on this issue: https://github.com/model-checking/kani/issues/3832 +---------------------------+------------------+--------------------------------+ | Crate | Skipped Function | Reason for Skipping | +===============================================================================+ | cargo_autoharness_include | excluded::simple | Did not match provided filters | -|---------------------------+------------------+--------------------------------| -| cargo_autoharness_include | include::generic | Generic Function | +---------------------------+------------------+--------------------------------+ +Autoharness: Checking function include::generic:: against all possible inputs... Autoharness: Checking function include::simple against all possible inputs... -VERIFICATION:- SUCCESSFUL Manual Harness Summary: No proof harnesses (functions with #[kani::proof]) were found to verify. Autoharness Summary: -+---------------------------+-------------------+---------------------------+---------------------+ -| Crate | Selected Function | Kind of Automatic Harness | Verification Result | -+=================================================================================================+ -| cargo_autoharness_include | include::simple | #[kani::proof] | Success | -+---------------------------+-------------------+---------------------------+---------------------+ -Complete - 1 successfully verified functions, 0 failures, 1 total. ++---------------------------+-------------------------+---------------------------+---------------------+ +| Crate | Selected Function | Kind of Automatic Harness | Verification Result | ++=======================================================================================================+ +| cargo_autoharness_include | include::generic:: | #[kani::proof] | Success | +|---------------------------+-------------------------+---------------------------+---------------------| +| cargo_autoharness_include | include::simple | #[kani::proof] | Success | ++---------------------------+-------------------------+---------------------------+---------------------+ +Complete - 2 successfully verified functions, 0 failures, 2 total. diff --git a/tests/script-based-pre/cargo_autoharness_exclude/src/lib.rs b/tests/script-based-pre/cargo_autoharness_exclude/src/lib.rs index 39676ed697ee..059459257292 100644 --- a/tests/script-based-pre/cargo_autoharness_exclude/src/lib.rs +++ b/tests/script-based-pre/cargo_autoharness_exclude/src/lib.rs @@ -9,7 +9,7 @@ mod include { x } - // Doesn't implement Arbitrary, so still should not be included. + // Generic functions get instantiated with a concrete type (e.g. `i32`). fn generic(x: u32, _y: T) -> u32 { x } diff --git a/tests/script-based-pre/cargo_autoharness_filter/filter.expected b/tests/script-based-pre/cargo_autoharness_filter/filter.expected index 6f9b30c0a23e..97d6298ad498 100644 --- a/tests/script-based-pre/cargo_autoharness_filter/filter.expected +++ b/tests/script-based-pre/cargo_autoharness_filter/filter.expected @@ -1,4 +1,4 @@ -Kani generated automatic harnesses for 44 function(s): +Kani generated automatic harnesses for 45 function(s): +--------------------------+----------------------------------------------+ | Crate | Selected Function | +=========================================================================+ @@ -22,6 +22,8 @@ Kani generated automatic harnesses for 44 function(s): |--------------------------+----------------------------------------------| | cargo_autoharness_filter | yes_harness::f_f64 | |--------------------------+----------------------------------------------| +| cargo_autoharness_filter | yes_harness::f_generic:: | +|--------------------------+----------------------------------------------| | cargo_autoharness_filter | yes_harness::f_i128 | |--------------------------+----------------------------------------------| | cargo_autoharness_filter | yes_harness::f_i16 | @@ -91,7 +93,7 @@ Kani generated automatic harnesses for 44 function(s): | cargo_autoharness_filter | yes_harness::f_usize | +--------------------------+----------------------------------------------+ -Kani did not generate automatic harnesses for 7 function(s). +Kani did not generate automatic harnesses for 6 function(s). If you believe that the provided reason is incorrect and Kani should have generated an automatic harness, please comment on this issue: https://github.com/model-checking/kani/issues/3832 +--------------------------+----------------------------------------+----------------------------------------------------------------------------------+ | Crate | Skipped Function | Reason for Skipping | @@ -100,8 +102,6 @@ If you believe that the provided reason is incorrect and Kani should have genera |--------------------------+----------------------------------------+----------------------------------------------------------------------------------| | cargo_autoharness_filter | no_harness::unsupported_const_pointer | Missing Arbitrary implementation for argument(s) _y: *const i32 | |--------------------------+----------------------------------------+----------------------------------------------------------------------------------| -| cargo_autoharness_filter | no_harness::unsupported_generic | Generic Function | -|--------------------------+----------------------------------------+----------------------------------------------------------------------------------| | cargo_autoharness_filter | no_harness::unsupported_mut_pointer | Missing Arbitrary implementation for argument(s) _y: *mut i32 | |--------------------------+----------------------------------------+----------------------------------------------------------------------------------| | cargo_autoharness_filter | no_harness::unsupported_no_arg_name | Missing Arbitrary implementation for argument(s) _: *const i32 | @@ -110,8 +110,16 @@ If you believe that the provided reason is incorrect and Kani should have genera |--------------------------+----------------------------------------+----------------------------------------------------------------------------------| | cargo_autoharness_filter | no_harness::unsupported_vec | Missing Arbitrary implementation for argument(s) _y: std::vec::Vec | +--------------------------+----------------------------------------+----------------------------------------------------------------------------------+ - +Autoharness: Checking function yes_harness::f_generic:: against all possible inputs... Autoharness: Checking function yes_harness::f_ref against all possible inputs... +Autoharness: Checking function yes_harness::empty_body against all possible inputs... +Autoharness: Checking function yes_harness::f_phantom_pinned against all possible inputs... +Autoharness: Checking function yes_harness::f_phantom_data against all possible inputs... +Autoharness: Checking function yes_harness::f_manually_implements_arbitrary against all possible inputs... +Autoharness: Checking function yes_harness::f_compiler_derives_arbitrary against all possible inputs... +Autoharness: Checking function yes_harness::f_derives_arbitrary against all possible inputs... +Autoharness: Checking function yes_harness::f_multiple_args against all possible inputs... +Autoharness: Checking function yes_harness::f_unsupported_return_type against all possible inputs... 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... @@ -133,7 +141,6 @@ 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_compiler_derives_arbitrary 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... @@ -148,13 +155,6 @@ 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... Manual Harness Summary: No proof harnesses (functions with #[kani::proof]) were found to verify. @@ -183,6 +183,8 @@ Autoharness Summary: |--------------------------+----------------------------------------------+---------------------------+---------------------| | cargo_autoharness_filter | yes_harness::f_f64 | #[kani::proof] | Success | |--------------------------+----------------------------------------------+---------------------------+---------------------| +| cargo_autoharness_filter | yes_harness::f_generic:: | #[kani::proof] | Success | +|--------------------------+----------------------------------------------+---------------------------+---------------------| | cargo_autoharness_filter | yes_harness::f_i128 | #[kani::proof] | Success | |--------------------------+----------------------------------------------+---------------------------+---------------------| | cargo_autoharness_filter | yes_harness::f_i16 | #[kani::proof] | Success | @@ -251,4 +253,4 @@ Autoharness Summary: |--------------------------+----------------------------------------------+---------------------------+---------------------| | cargo_autoharness_filter | yes_harness::f_usize | #[kani::proof] | Success | +--------------------------+----------------------------------------------+---------------------------+---------------------+ -Complete - 44 successfully verified functions, 0 failures, 44 total. +Complete - 45 successfully verified functions, 0 failures, 45 total. diff --git a/tests/script-based-pre/cargo_autoharness_filter/src/lib.rs b/tests/script-based-pre/cargo_autoharness_filter/src/lib.rs index 2fc387ba4a2b..87fb92a50ab8 100644 --- a/tests/script-based-pre/cargo_autoharness_filter/src/lib.rs +++ b/tests/script-based-pre/cargo_autoharness_filter/src/lib.rs @@ -192,13 +192,14 @@ mod yes_harness { fn f_ref(x: u32, _y: &i32) -> u32 { x } + + fn f_generic(x: u32, _y: T) -> u32 { + x + } } mod no_harness { use crate::{DerivesArbitrary, DoesntImplementArbitrary}; - fn unsupported_generic(x: u32, _y: T) -> u32 { - x - } fn unsupported_const_pointer(x: u32, _y: *const i32) -> u32 { x } diff --git a/tests/script-based-pre/cargo_autoharness_generics/Cargo.toml b/tests/script-based-pre/cargo_autoharness_generics/Cargo.toml new file mode 100644 index 000000000000..832b818ce535 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_generics/Cargo.toml @@ -0,0 +1,10 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "cargo_autoharness_generics" +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_generics/config.yml b/tests/script-based-pre/cargo_autoharness_generics/config.yml new file mode 100644 index 000000000000..3517a8b7d23d --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_generics/config.yml @@ -0,0 +1,5 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +script: generics.sh +expected: generics.expected +exit_code: 1 diff --git a/tests/script-based-pre/cargo_autoharness_generics/generics.expected b/tests/script-based-pre/cargo_autoharness_generics/generics.expected new file mode 100644 index 000000000000..e7f3b8d1098c --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_generics/generics.expected @@ -0,0 +1,11 @@ +| cargo_autoharness_generics | needs_exotic | Generic Function | +| cargo_autoharness_generics | with_const | Generic Function | +| cargo_autoharness_generics | Wrapper::::get | #[kani::proof] | Success | +| cargo_autoharness_generics | contracted:: | #[kani::proof_for_contract] | Success | +| cargo_autoharness_generics | first:: | #[kani::proof] | Success | +| cargo_autoharness_generics | identity:: | #[kani::proof] | Success | +| cargo_autoharness_generics | max3:: | #[kani::proof] | Success | +| cargo_autoharness_generics | pair:: | #[kani::proof] | Success | +| cargo_autoharness_generics | takes_impl:: | #[kani::proof] | Success | +| cargo_autoharness_generics | buggy_add:: | #[kani::proof] | Failure | +Complete - 7 successfully verified functions, 1 failures, 8 total. diff --git a/tests/script-based-pre/cargo_autoharness_generics/generics.sh b/tests/script-based-pre/cargo_autoharness_generics/generics.sh new file mode 100755 index 000000000000..65f949b65ad3 --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_generics/generics.sh @@ -0,0 +1,5 @@ +#!/usr/bin/env bash +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +cargo kani autoharness -Z autoharness -Z function-contracts diff --git a/tests/script-based-pre/cargo_autoharness_generics/src/lib.rs b/tests/script-based-pre/cargo_autoharness_generics/src/lib.rs new file mode 100644 index 000000000000..e23c4cb46ccb --- /dev/null +++ b/tests/script-based-pre/cargo_autoharness_generics/src/lib.rs @@ -0,0 +1,81 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Test that the autoharness subcommand supports generic functions by instantiating their type +// parameters with a concrete type: the first candidate (starting from `i32`) that satisfies all +// of the function's trait bounds. Lifetime parameters are erased; functions with const generic +// parameters or with bounds that no candidate satisfies are skipped. +// The "TEST NOTE" comments below explain the expected result for each function. + +// TEST NOTE: verified as `identity::`. +pub fn identity(x: T) -> T { + x +} + +// TEST NOTE: verified as `max3::`; primitives satisfy the bounds. +pub fn max3(a: T, b: T, c: T) -> T { + let mut m = a; + if b > m { + m = b; + } + if c > m { + m = c; + } + m +} + +// TEST NOTE: verified as `buggy_add::` and FAILS, since the addition can overflow. +// This demonstrates that instantiating a generic function can find real bugs. +pub fn buggy_add>(a: T, b: T) -> T { + a + b +} + +// TEST NOTE: verified as `pair::`; multiple type parameters are supported. +pub fn pair(x: T, _y: U) -> (T, U) { + (x, U::default()) +} + +// TEST NOTE: verified as `first::`; lifetime parameters are erased. +pub fn first<'a, T: Copy>(x: &'a T) -> T { + *x +} + +// TEST NOTE: verified as `takes_impl::`: `i32` does not satisfy `Into`, +// so the next candidate that does (`u32`) is chosen. +pub fn takes_impl(x: impl Into + Copy) -> u64 { + x.into() +} + +// TEST NOTE: skipped (Generic Function), since no candidate type implements `Exotic`. +pub trait Exotic { + fn exotic(&self) -> u8; +} +pub fn needs_exotic(x: T) -> u8 { + x.exotic() +} + +// TEST NOTE: skipped (Generic Function), since we do not instantiate const generic +// parameters yet. +pub fn with_const(_x: [u8; N]) -> usize { + N +} + +// TEST NOTE: verified as `Wrapper::::get`; generic parameters of the impl block are +// instantiated too. +pub struct Wrapper { + val: T, +} + +impl Wrapper { + pub fn get(&self) -> T { + self.val + } +} + +// TEST NOTE: verified as `contracted::` with a contract harness; the contract is checked +// for the chosen instantiation. +#[kani::requires(x < 1000)] +#[kani::ensures(|r| *r >= x)] +pub fn contracted>(_marker: T, x: u64) -> u64 { + x + 1 +} diff --git a/tests/script-based-pre/cargo_autoharness_include/include.expected b/tests/script-based-pre/cargo_autoharness_include/include.expected index 9c006d210262..5a714b76557d 100644 --- a/tests/script-based-pre/cargo_autoharness_include/include.expected +++ b/tests/script-based-pre/cargo_autoharness_include/include.expected @@ -1,29 +1,31 @@ -Kani generated automatic harnesses for 1 function(s): -+---------------------------+-------------------+ -| Crate | Selected Function | -+===============================================+ -| cargo_autoharness_include | include::simple | -+---------------------------+-------------------+ +Kani generated automatic harnesses for 2 function(s): ++---------------------------+-------------------------+ +| Crate | Selected Function | ++=====================================================+ +| cargo_autoharness_include | include::generic:: | +|---------------------------+-------------------------| +| cargo_autoharness_include | include::simple | ++---------------------------+-------------------------+ -Kani did not generate automatic harnesses for 2 function(s). +Kani did not generate automatic harnesses for 1 function(s). If you believe that the provided reason is incorrect and Kani should have generated an automatic harness, please comment on this issue: https://github.com/model-checking/kani/issues/3832 +---------------------------+------------------+--------------------------------+ | Crate | Skipped Function | Reason for Skipping | +===============================================================================+ | cargo_autoharness_include | excluded::simple | Did not match provided filters | -|---------------------------+------------------+--------------------------------| -| cargo_autoharness_include | include::generic | Generic Function | +---------------------------+------------------+--------------------------------+ +Autoharness: Checking function include::generic:: against all possible inputs... Autoharness: Checking function include::simple against all possible inputs... -VERIFICATION:- SUCCESSFUL Manual Harness Summary: No proof harnesses (functions with #[kani::proof]) were found to verify. Autoharness Summary: -+---------------------------+-------------------+---------------------------+---------------------+ -| Crate | Selected Function | Kind of Automatic Harness | Verification Result | -+=================================================================================================+ -| cargo_autoharness_include | include::simple | #[kani::proof] | Success | -+---------------------------+-------------------+---------------------------+---------------------+ -Complete - 1 successfully verified functions, 0 failures, 1 total. ++---------------------------+-------------------------+---------------------------+---------------------+ +| Crate | Selected Function | Kind of Automatic Harness | Verification Result | ++=======================================================================================================+ +| cargo_autoharness_include | include::generic:: | #[kani::proof] | Success | +|---------------------------+-------------------------+---------------------------+---------------------| +| cargo_autoharness_include | include::simple | #[kani::proof] | Success | ++---------------------------+-------------------------+---------------------------+---------------------+ +Complete - 2 successfully verified functions, 0 failures, 2 total. diff --git a/tests/script-based-pre/cargo_autoharness_include/src/lib.rs b/tests/script-based-pre/cargo_autoharness_include/src/lib.rs index 135f86f76874..38f69c4390e4 100644 --- a/tests/script-based-pre/cargo_autoharness_include/src/lib.rs +++ b/tests/script-based-pre/cargo_autoharness_include/src/lib.rs @@ -10,7 +10,7 @@ mod include { x } - // Doesn't implement Arbitrary, so still should not be included. + // Generic functions get instantiated with a concrete type (e.g. `i32`). fn generic(x: u32, _y: T) -> u32 { x } From 52aceefcab63ea839589e67d403ecb02e687dc02 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 28 Jul 2026 22:06:18 +0000 Subject: [PATCH 2/5] Report why a generic function could not be instantiated Rather than the single 'Generic Function' skip reason, attach a detail explaining what prevented instantiation: const generic parameters, or that no candidate type satisfies the function's trait bounds. This makes the skipped-functions table actionable and allows corpus evaluations to classify the generic-function gap precisely. Co-authored-by: Kiro --- .../src/kani_middle/codegen_units.rs | 33 +++++++++++-------- kani-driver/src/autoharness/mod.rs | 7 ++-- kani_metadata/src/lib.rs | 6 ++-- .../generics.expected | 4 +-- 4 files changed, 30 insertions(+), 20 deletions(-) diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 537dd2781c05..9e550dca6702 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -450,15 +450,16 @@ fn args_satisfy_predicates(tcx: TyCtxt, def: FnDef, args: &GenericArgs) -> bool /// 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 /// (using the same candidate for every type parameter), and erase lifetime parameters. -/// Return `None` 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) -> Option { +/// 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 { let TyKind::RigidTy(RigidTy::FnDef(def, identity_args)) = fn_item.ty().kind() else { - return None; + return Err("not a function definition".to_string()); }; if identity_args.0.iter().any(|arg| matches!(arg, GenericArgKind::Const(_))) { - return None; + return Err("const generic parameters are not supported yet".to_string()); } for candidate in generic_instantiation_candidates() { @@ -481,10 +482,17 @@ fn choose_generic_instantiation(tcx: TyCtxt, fn_item: CrateItem) -> Option>() + .join(", ") + )) } /// Partition every function in the crate into (chosen, skipped), where `chosen` is a vector of the Instances for which we'll generate automatic harnesses, @@ -590,17 +598,16 @@ fn automatic_harness_partition( // and its name (e.g. `foo::`) reflects that. let instance = match Instance::try_from(func) { Ok(instance) => instance, - Err(_) => { - if let Some(instance) = choose_generic_instantiation(tcx, func) { - instance - } else { + Err(_) => match choose_generic_instantiation(tcx, func) { + Ok(instance) => instance, + Err(detail) => { skipped.insert( crate::kani_middle::strip_local_crate_prefix(func.name()), - AutoHarnessSkipReason::GenericFn, + AutoHarnessSkipReason::GenericFn(detail), ); continue; } - } + }, }; if let Some(reason) = skip_reason(instance) { diff --git a/kani-driver/src/autoharness/mod.rs b/kani-driver/src/autoharness/mod.rs index 01904bb786d6..b7be4f961f0d 100644 --- a/kani-driver/src/autoharness/mod.rs +++ b/kani-driver/src/autoharness/mod.rs @@ -106,9 +106,10 @@ fn print_autoharness_metadata(metadata: Vec) { .join(", ") ), ]), - AutoHarnessSkipReason::GenericFn - | AutoHarnessSkipReason::NoBody - | AutoHarnessSkipReason::UserFilter => { + AutoHarnessSkipReason::GenericFn(ref detail) => { + Some(vec![md.crate_name.clone(), func, format!("{reason}: {detail}")]) + } + AutoHarnessSkipReason::NoBody | AutoHarnessSkipReason::UserFilter => { Some(vec![md.crate_name.clone(), func, reason.to_string()]) } // We don't report Kani implementations to the user to avoid exposing Kani functions we insert during instrumentation. diff --git a/kani_metadata/src/lib.rs b/kani_metadata/src/lib.rs index 2117c04aac17..4e7fa0d2694b 100644 --- a/kani_metadata/src/lib.rs +++ b/kani_metadata/src/lib.rs @@ -55,9 +55,11 @@ pub struct AutoHarnessMetadata { /// Reasons that Kani does not generate an automatic harness for a function. #[derive(Debug, Clone, Serialize, Deserialize, Display, EnumString)] pub enum AutoHarnessSkipReason { - /// The function is generic. + /// The function is generic and autoharness could not find a monomorphic instantiation to + /// verify. The payload gives the specific reason (e.g. const generic parameters, or trait + /// bounds that no candidate type satisfies). #[strum(serialize = "Generic Function")] - GenericFn, + GenericFn(String), /// A Kani-internal function: already a harness, implementation of a Kani associated item or Kani contract instrumentation functions). #[strum(serialize = "Kani implementation")] KaniImpl, diff --git a/tests/script-based-pre/cargo_autoharness_generics/generics.expected b/tests/script-based-pre/cargo_autoharness_generics/generics.expected index e7f3b8d1098c..4263f74b0479 100644 --- a/tests/script-based-pre/cargo_autoharness_generics/generics.expected +++ b/tests/script-based-pre/cargo_autoharness_generics/generics.expected @@ -1,5 +1,5 @@ -| cargo_autoharness_generics | needs_exotic | Generic Function | -| cargo_autoharness_generics | with_const | Generic Function | +| cargo_autoharness_generics | needs_exotic | Generic Function: no candidate type (i32, u32, usize, bool, char) satisfies the function's trait bounds | +| cargo_autoharness_generics | with_const | Generic Function: const generic parameters are not supported yet | | cargo_autoharness_generics | Wrapper::::get | #[kani::proof] | Success | | cargo_autoharness_generics | contracted:: | #[kani::proof_for_contract] | Success | | cargo_autoharness_generics | first:: | #[kani::proof] | Success | From c792ae43c3f8bea4ed8a31071b8c01ac0804cc9c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 29 Jul 2026 14:06:34 +0000 Subject: [PATCH 3/5] Autoharness: instantiate usize const generic parameters Instantiate usize const generic parameters (by far the most common case, e.g. array lengths) with the value 2, alongside the existing type-parameter instantiation; the summary table shows the chosen value as part of the instantiated name (e.g. with_const::<2>). Non-usize const parameters are still skipped, now with a precise reason; the check consults the internal generics since the public identity arguments do not carry the parameter's type. Co-authored-by: Kiro --- .../src/reference/experimental/autoharness.md | 4 ++- .../src/kani_middle/codegen_units.rs | 25 ++++++++++++++++--- .../generics.expected | 5 ++-- .../cargo_autoharness_generics/src/lib.rs | 14 ++++++++--- 4 files changed, 37 insertions(+), 11 deletions(-) diff --git a/docs/src/reference/experimental/autoharness.md b/docs/src/reference/experimental/autoharness.md index a0a6866e9b34..a54c661d6ab7 100644 --- a/docs/src/reference/experimental/autoharness.md +++ b/docs/src/reference/experimental/autoharness.md @@ -136,9 +136,11 @@ Note that verifying a single instantiation is an underapproximation of all of th a successful result for `foo::` does not imply that other instantiations of `foo` are also safe. Kani makes this explicit by displaying the instantiated name of the verified function. +`usize` const generic parameters (e.g. array lengths) are instantiated with the value 2. + Kani skips a generic function (with skip reason "Generic Function") if: - no candidate type satisfies the function's trait bounds, or -- the function has const generic parameters, which Kani does not instantiate yet. +- the function has non-`usize` const generic parameters, which Kani does not instantiate yet. If some caller of a generic function is eligible for an automatic harness, then additional monomorphized versions of the generic function may still be reachable (and thus verified) through the caller's harness. diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 9e550dca6702..3119efa70d47 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -29,7 +29,8 @@ use rustc_middle::ty::{self, TyCtxt, TypingMode}; use rustc_public::mir::mono::Instance; use rustc_public::rustc_internal; use rustc_public::ty::{ - FnDef, GenericArgKind, GenericArgs, IntTy, Region, RegionKind, RigidTy, Ty, TyKind, UintTy, + FnDef, GenericArgKind, GenericArgs, IntTy, Region, RegionKind, RigidTy, Ty, TyConst, TyKind, + UintTy, }; use rustc_public::{CrateDef, CrateItem}; use rustc_public_bridge::IndexedVal; @@ -414,6 +415,12 @@ fn autoharness_filtered_out( !included || excluded } +/// The value used to instantiate `usize` const generic parameters of generic functions +/// (e.g. array lengths). As with the choice of type-parameter candidates, verifying a single +/// instantiation underapproximates the function's behaviors; the summary table shows the +/// chosen value as part of the instantiated name. +const AUTOHARNESS_CONST_GENERIC_VALUE: u64 = 2; + /// The candidate types for instantiating the type parameters of a generic function, in the order /// in which we try them. We start with `i32` since that is Rust's default integer type, and /// primitive types satisfy the most common trait bounds (`Copy`, `Clone`, `Ord`, `Hash`, @@ -458,8 +465,16 @@ fn choose_generic_instantiation(tcx: TyCtxt, fn_item: CrateItem) -> Result Result { GenericArgKind::Lifetime(Region { kind: RegionKind::ReErased }) } - GenericArgKind::Const(_) => unreachable!("const generics filtered out above"), + GenericArgKind::Const(_) => GenericArgKind::Const( + TyConst::try_from_target_usize(AUTOHARNESS_CONST_GENERIC_VALUE).unwrap(), + ), }) .collect(), ); diff --git a/tests/script-based-pre/cargo_autoharness_generics/generics.expected b/tests/script-based-pre/cargo_autoharness_generics/generics.expected index 4263f74b0479..4aebef62731c 100644 --- a/tests/script-based-pre/cargo_autoharness_generics/generics.expected +++ b/tests/script-based-pre/cargo_autoharness_generics/generics.expected @@ -1,5 +1,5 @@ | cargo_autoharness_generics | needs_exotic | Generic Function: no candidate type (i32, u32, usize, bool, char) satisfies the function's trait bounds | -| cargo_autoharness_generics | with_const | Generic Function: const generic parameters are not supported yet | +| cargo_autoharness_generics | with_bool_const | Generic Function: non-usize const generic parameters are not supported yet | | cargo_autoharness_generics | Wrapper::::get | #[kani::proof] | Success | | cargo_autoharness_generics | contracted:: | #[kani::proof_for_contract] | Success | | cargo_autoharness_generics | first:: | #[kani::proof] | Success | @@ -7,5 +7,6 @@ | cargo_autoharness_generics | max3:: | #[kani::proof] | Success | | cargo_autoharness_generics | pair:: | #[kani::proof] | Success | | cargo_autoharness_generics | takes_impl:: | #[kani::proof] | Success | +| cargo_autoharness_generics | with_const::<2> | #[kani::proof] | Success | | cargo_autoharness_generics | buggy_add:: | #[kani::proof] | Failure | -Complete - 7 successfully verified functions, 1 failures, 8 total. +Complete - 8 successfully verified functions, 1 failures, 9 total. diff --git a/tests/script-based-pre/cargo_autoharness_generics/src/lib.rs b/tests/script-based-pre/cargo_autoharness_generics/src/lib.rs index e23c4cb46ccb..b690193d2da5 100644 --- a/tests/script-based-pre/cargo_autoharness_generics/src/lib.rs +++ b/tests/script-based-pre/cargo_autoharness_generics/src/lib.rs @@ -54,10 +54,16 @@ pub fn needs_exotic(x: T) -> u8 { x.exotic() } -// TEST NOTE: skipped (Generic Function), since we do not instantiate const generic -// parameters yet. -pub fn with_const(_x: [u8; N]) -> usize { - N +// TEST NOTE: verified as `with_const::<2>`; usize const generic parameters are instantiated +// with the value 2. +pub fn with_const(x: [u8; N]) -> usize { + x.len() + N +} + +// TEST NOTE: skipped (Generic Function), since non-usize const generic parameters are not +// supported yet. +pub fn with_bool_const(x: u8) -> u8 { + if B { x } else { 0 } } // TEST NOTE: verified as `Wrapper::::get`; generic parameters of the impl block are From 7e81251b1d3d36843fc7a4ddce6e9365fb038fe4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 31 Jul 2026 21:13:12 +0000 Subject: [PATCH 4/5] Autoharness: per-parameter and trait-impl-derived generic instantiation Extend the generic-instantiation search in three ways, found by evaluating autoharness on the top-100 crates.io crates, where ~8,700 functions were skipped because no candidate type satisfied their trait bounds: 1. Widen the primitive candidate list with u8, i64, u64, f64 and f32; float candidates alone unlock the numerous Float/FloatCore-bounded functions in num-traits and its dependents. 2. Search per-parameter candidate combinations (after the cheap uniform pass), so functions whose parameters need different types, e.g. fn cast, are instantiated. The search is capped at 256 trait-solver queries per function. 3. Derive additional per-parameter candidates from the concrete implementations of the traits each parameter is bound by (capped at 16 per parameter), so parameters bound by crate-local traits can be instantiated with the crate's own types implementing them. Co-authored-by: Kiro --- .../src/reference/experimental/autoharness.md | 10 +- .../src/kani_middle/codegen_units.rs | 152 ++++++++++++++++-- .../generics.expected | 30 ++-- .../cargo_autoharness_generics/src/lib.rs | 47 +++++- 4 files changed, 212 insertions(+), 27 deletions(-) diff --git a/docs/src/reference/experimental/autoharness.md b/docs/src/reference/experimental/autoharness.md index a54c661d6ab7..256649851f8a 100644 --- a/docs/src/reference/experimental/autoharness.md +++ b/docs/src/reference/experimental/autoharness.md @@ -116,8 +116,14 @@ Note that this automatic derivation feature is only available for autoharness. ### Generic Functions For a generic function, Kani generates a harness for a single monomorphic instantiation of the function: -it substitutes every type parameter with the first candidate from a fixed list of primitive types -(starting with `i32`) such that all of the function's trait bounds are satisfied, and erases lifetime parameters. +it substitutes the function's type parameters with concrete types such that all of the function's +trait bounds are satisfied, and erases lifetime parameters. Kani first tries a fixed list of +primitive types (starting with `i32`, and including the wider integer and float types) uniformly +for all parameters; if that fails, it searches per-parameter combinations, drawing additional +candidate types from the concrete implementations of the traits each parameter is bound by +(so, e.g., a parameter bound by a crate-local trait can be instantiated with a crate-local struct +implementing it). The search is capped, so functions with many type parameters or very complex +bounds may still be skipped. For example, given: ```rust fn foo(x: T, y: T) { diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 3119efa70d47..1e19d8e7f994 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -29,8 +29,8 @@ use rustc_middle::ty::{self, TyCtxt, TypingMode}; use rustc_public::mir::mono::Instance; use rustc_public::rustc_internal; use rustc_public::ty::{ - FnDef, GenericArgKind, GenericArgs, IntTy, Region, RegionKind, RigidTy, Ty, TyConst, TyKind, - UintTy, + FloatTy, FnDef, GenericArgKind, GenericArgs, IntTy, Region, RegionKind, RigidTy, Ty, TyConst, + TyKind, UintTy, }; use rustc_public::{CrateDef, CrateItem}; use rustc_public_bridge::IndexedVal; @@ -430,11 +430,59 @@ fn generic_instantiation_candidates() -> Vec { Ty::from_rigid_kind(RigidTy::Int(IntTy::I32)), Ty::from_rigid_kind(RigidTy::Uint(UintTy::U32)), Ty::from_rigid_kind(RigidTy::Uint(UintTy::Usize)), + Ty::from_rigid_kind(RigidTy::Uint(UintTy::U8)), + Ty::from_rigid_kind(RigidTy::Int(IntTy::I64)), + Ty::from_rigid_kind(RigidTy::Uint(UintTy::U64)), + Ty::from_rigid_kind(RigidTy::Float(FloatTy::F64)), + Ty::from_rigid_kind(RigidTy::Float(FloatTy::F32)), Ty::from_rigid_kind(RigidTy::Bool), Ty::from_rigid_kind(RigidTy::Char), ] } +/// Cap on trait-solver queries per function when searching for a satisfying instantiation, +/// so that functions with many type parameters do not blow up partitioning time. +const GENERIC_INSTANTIATION_ATTEMPT_LIMIT: usize = 256; + +/// Cap on the number of trait-impl-derived candidate types collected per type parameter. +const IMPL_DERIVED_CANDIDATE_LIMIT: usize = 16; + +/// For each type parameter of `def` (keyed by its index in the generic parameter list), +/// collect concrete types that implement the parameter's trait bounds, by enumerating the +/// non-blanket implementations of each trait the parameter is bound by. This finds candidates +/// for parameters bound by crate-local or third-party traits (e.g. num-traits' `Float`), +/// which no primitive candidate may satisfy. +/// Candidates are deduplicated, restricted to fully concrete types, and sorted for +/// determinism; each parameter's list is capped at [IMPL_DERIVED_CANDIDATE_LIMIT]. +fn impl_derived_candidates(tcx: TyCtxt, def: FnDef) -> FxHashMap> { + let def_id = rustc_internal::internal(tcx, def.def_id()); + let mut candidates: FxHashMap> = FxHashMap::default(); + for (predicate, _span) in tcx.predicates_of(def_id).predicates { + let Some(trait_pred) = predicate.as_trait_clause() else { continue }; + let trait_pred = trait_pred.skip_binder(); + let ty::Param(param_ty) = trait_pred.self_ty().kind() else { continue }; + let slot = candidates.entry(param_ty.index as usize).or_default(); + for impls in tcx.trait_impls_of(trait_pred.def_id()).non_blanket_impls().values() { + for &impl_def_id in impls { + let self_ty = tcx.type_of(impl_def_id).instantiate_identity(); + // Only fully concrete self types can be substituted directly. + if rustc_middle::ty::TypeVisitableExt::has_param(&self_ty) { + continue; + } + let stable_ty = rustc_internal::stable(self_ty); + if !slot.contains(&stable_ty) { + slot.push(stable_ty); + } + } + } + } + for slot in candidates.values_mut() { + slot.sort_by_key(|ty| ty.to_string()); + slot.truncate(IMPL_DERIVED_CANDIDATE_LIMIT); + } + candidates +} + /// Check whether instantiating the generic parameters of `def` with `args` satisfies all of /// `def`'s predicates (trait bounds and where clauses). /// `args` must be fully monomorphic. @@ -477,13 +525,43 @@ fn choose_generic_instantiation(tcx: TyCtxt, fn_item: CrateItem) -> Result = identity_args + .0 + .iter() + .enumerate() + .filter_map(|(idx, arg)| matches!(arg, GenericArgKind::Type(_)).then_some(idx)) + .collect(); + let slot_candidates: Vec> = type_slots + .iter() + .map(|&idx| { + let mut cands = generic_instantiation_candidates(); + for ty in impl_derived.get(&idx).into_iter().flatten() { + if !cands.contains(ty) { + cands.push(*ty); + } + } + cands + }) + .collect(); + let n_impl_derived: usize = impl_derived.values().map(|v| v.len()).sum(); + + // Build the argument list substituting `choice[i]` for the i-th type parameter. + let build_args = |choice: &[Ty]| { + let mut next_type = 0; + GenericArgs( identity_args .0 .iter() .map(|arg| match arg { - GenericArgKind::Type(_) => GenericArgKind::Type(candidate), + GenericArgKind::Type(_) => { + let ty = choice[next_type]; + next_type += 1; + GenericArgKind::Type(ty) + } GenericArgKind::Lifetime(_) => { GenericArgKind::Lifetime(Region { kind: RegionKind::ReErased }) } @@ -492,23 +570,73 @@ fn choose_generic_instantiation(tcx: TyCtxt, fn_item: CrateItem) -> Result Option { + attempts.set(attempts.get() + 1); + let args = build_args(choice); if !args_satisfy_predicates(tcx, def, &args) { - continue; + return None; } - if let Ok(instance) = Instance::resolve(def, &args) - && instance.has_body() - { + match Instance::resolve(def, &args) { + Ok(instance) if instance.has_body() => Some(instance), + _ => None, + } + }; + + // First pass: the same primitive candidate for every type parameter (the common case, + // and cheap). Second pass: the cartesian product of the per-parameter candidate lists, + // capped at GENERIC_INSTANTIATION_ATTEMPT_LIMIT trait-solver queries, which finds + // instantiations for functions whose parameters need *different* types (e.g. + // `fn cast`) or types implementing non-primitive-friendly bounds. + for candidate in generic_instantiation_candidates() { + if let Some(instance) = try_choice(&vec![candidate; type_slots.len()]) { return Ok(instance); } } + if !type_slots.is_empty() { + let mut odometer = vec![0usize; type_slots.len()]; + 'product: loop { + let choice: Vec = + odometer.iter().enumerate().map(|(i, &c)| slot_candidates[i][c]).collect(); + // 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 let Some(instance) = try_choice(&choice) { + return Ok(instance); + } + if attempts.get() >= GENERIC_INSTANTIATION_ATTEMPT_LIMIT { + break; + } + } + // Advance the odometer. + for i in (0..odometer.len()).rev() { + odometer[i] += 1; + if odometer[i] < slot_candidates[i].len() { + continue 'product; + } + odometer[i] = 0; + if i == 0 { + break 'product; + } + } + } + } Err(format!( - "no candidate type ({}) satisfies the function's trait bounds", + "no candidate type ({}{}) satisfies the function's trait bounds", generic_instantiation_candidates() .iter() .map(|ty| ty.to_string()) .collect::>() - .join(", ") + .join(", "), + if n_impl_derived > 0 { + format!(" and {n_impl_derived} types implementing the required traits") + } else { + String::new() + } )) } diff --git a/tests/script-based-pre/cargo_autoharness_generics/generics.expected b/tests/script-based-pre/cargo_autoharness_generics/generics.expected index 4aebef62731c..d83dec94ba3c 100644 --- a/tests/script-based-pre/cargo_autoharness_generics/generics.expected +++ b/tests/script-based-pre/cargo_autoharness_generics/generics.expected @@ -1,12 +1,18 @@ -| cargo_autoharness_generics | needs_exotic | Generic Function: no candidate type (i32, u32, usize, bool, char) satisfies the function's trait bounds | -| cargo_autoharness_generics | with_bool_const | Generic Function: non-usize const generic parameters are not supported yet | -| cargo_autoharness_generics | Wrapper::::get | #[kani::proof] | Success | -| cargo_autoharness_generics | contracted:: | #[kani::proof_for_contract] | Success | -| cargo_autoharness_generics | first:: | #[kani::proof] | Success | -| cargo_autoharness_generics | identity:: | #[kani::proof] | Success | -| cargo_autoharness_generics | max3:: | #[kani::proof] | Success | -| cargo_autoharness_generics | pair:: | #[kani::proof] | Success | -| cargo_autoharness_generics | takes_impl:: | #[kani::proof] | Success | -| cargo_autoharness_generics | with_const::<2> | #[kani::proof] | Success | -| cargo_autoharness_generics | buggy_add:: | #[kani::proof] | Failure | -Complete - 8 successfully verified functions, 1 failures, 9 total. +| cargo_autoharness_generics | needs_exotic | Generic Function: no candidate type (i32, u32, usize, u8, i64, u64, f64, f32, bool, char) satisfies the function's trait bounds | +| cargo_autoharness_generics | with_bool_const | Generic Function: non-usize const generic parameters are not supported yet | +| cargo_autoharness_generics | ::frob | #[kani::proof] | Success | +| cargo_autoharness_generics | ::half | #[kani::proof] | Success | +| cargo_autoharness_generics | ::half | #[kani::proof] | Success | +| cargo_autoharness_generics | Wrapper::::get | #[kani::proof] | Success | +| cargo_autoharness_generics | contracted:: | #[kani::proof_for_contract] | Success | +| cargo_autoharness_generics | first:: | #[kani::proof] | Success | +| cargo_autoharness_generics | frob_it:: | #[kani::proof] | Success | +| cargo_autoharness_generics | halve:: | #[kani::proof] | Success | +| cargo_autoharness_generics | identity:: | #[kani::proof] | Success | +| cargo_autoharness_generics | max3:: | #[kani::proof] | Success | +| cargo_autoharness_generics | mixed:: | #[kani::proof] | Success | +| cargo_autoharness_generics | pair:: | #[kani::proof] | Success | +| cargo_autoharness_generics | takes_impl:: | #[kani::proof] | Success | +| cargo_autoharness_generics | with_const::<2> | #[kani::proof] | Success | +| cargo_autoharness_generics | buggy_add:: | #[kani::proof] | Failure | +Complete - 14 successfully verified functions, 1 failures, 15 total. diff --git a/tests/script-based-pre/cargo_autoharness_generics/src/lib.rs b/tests/script-based-pre/cargo_autoharness_generics/src/lib.rs index b690193d2da5..1c6943912d68 100644 --- a/tests/script-based-pre/cargo_autoharness_generics/src/lib.rs +++ b/tests/script-based-pre/cargo_autoharness_generics/src/lib.rs @@ -46,7 +46,8 @@ pub fn takes_impl(x: impl Into + Copy) -> u64 { x.into() } -// TEST NOTE: skipped (Generic Function), since no candidate type implements `Exotic`. +// TEST NOTE: skipped (Generic Function), since no candidate type implements `Exotic` +// (the trait has no implementations at all). pub trait Exotic { fn exotic(&self) -> u8; } @@ -54,6 +55,50 @@ pub fn needs_exotic(x: T) -> u8 { x.exotic() } +// TEST NOTE: verified as `halve::`; no integral candidate satisfies the bound, but the +// float candidates do (mimics num-traits' `Float`). +pub trait FloatLike { + fn half(self) -> Self; +} +impl FloatLike for f64 { + fn half(self) -> Self { + self / 2.0 + } +} +impl FloatLike for f32 { + fn half(self) -> Self { + self / 2.0 + } +} +pub fn halve(x: T) -> T { + x.half() +} + +// TEST NOTE: verified as `frob_it::`; no primitive implements `Frobnicate`, so the +// candidate is derived from the trait's implementations. +pub trait Frobnicate { + fn frob(&self) -> u32; +} +#[derive(kani::Arbitrary)] +pub struct Widget { + pub id: u32, +} +impl Frobnicate for Widget { + fn frob(&self) -> u32 { + self.id.wrapping_add(1) + } +} +pub fn frob_it(w: W) -> u32 { + w.frob() +} + +// TEST NOTE: verified as `mixed::`; the parameters require *different* +// candidate types, found by the per-parameter search. +pub fn mixed(x: T, w: U) -> u32 { + let _ = x.half(); + w.frob() +} + // TEST NOTE: verified as `with_const::<2>`; usize const generic parameters are instantiated // with the value 2. pub fn with_const(x: [u8; N]) -> usize { From 4f66b6080a006c6796796282c0db771be954d93b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 7 Aug 2026 18:02:39 +0000 Subject: [PATCH 5/5] Autoharness: instantiate Fn-bounded type parameters with nondet closures Corpus data (top-500 crates.io): Fn-bound generic functions outnumber Iterator-bound ones 4:1 (2,373 vs 612 signatures); no primitive candidate can ever satisfy an Fn bound, so these functions were all skipped. Fn/FnMut/FnOnce-bounded type parameters are instantiated with the function item type of a matching nondet model (kani::arbitrary:: nondet_fn*): function items implement all three Fn traits and are zero-sized (the harness materializes the value as a zero-sized constant), and each call returns a fresh nondeterministic value, over-approximating every real closure with that signature -- including stateful FnMut ones. Design points, each validated on the crate that motivated it: - Models are selected by input SHAPE, not just arity: by-value models bind their input regions early-bound and cannot satisfy HRTB bounds like for<'a> Fn(&'a T), so the four dominant by-ref shapes (96% of the 3,768 ref-involving Fn bounds in the corpus) get region-polymorphic models (nondet_fn1_ref etc.) whose fn items carry late-bound regions. - Candidate derivation reads the Fn trait predicates (tupled inputs) and the FnOnce::Output projection, erasing late-bound regions rather than skipping binders (escaping bound vars panic the trait solver; tap). - Signatures referencing other generic parameters (fn apply T>) are collected as deferred specs: their slots carry a placeholder through the candidate search and are substituted per candidate choice (EarlyBinder::instantiate), normalized (unnormalizable projections such as ::Val abort the choice; tap), and admission-checked against the model's own R: Arbitrary bound (Instance::resolve does not check bounds; syn). - Vtables built for a concrete type may mark a method slot Vacant where the trait's vtable struct type declares a method pointer (an HRTB predicate the concrete fn item does not satisfy): pad the slot with a typed null, mirroring rustc's vtable layout (reqwest). Dispatchable methods use real slots via the region-polymorphic models. - Arity ceiling of 3 justified by data: 98.5% of corpus Fn-bound signatures have arity <= 3. The regression test pins bug-finding through nondet closures (overflow on unconstrained results at arities 1 and 2), cover-based reachability of closure-dependent branches, HRTB closures plain and dyn-coerced through a wrapper struct, param-referencing signatures, and tuple arguments. Co-authored-by: Kiro --- .../codegen_cprover_gotoc/codegen/operand.rs | 40 +-- .../codegen_cprover_gotoc/codegen/rvalue.rs | 28 +- .../src/kani_middle/codegen_units.rs | 267 +++++++++++++++++- .../src/kani_middle/kani_functions.rs | 16 ++ .../src/kani_middle/transform/automatic.rs | 25 +- library/kani/src/arbitrary.rs | 68 +++++ .../cargo_autoharness_fn_bounds/Cargo.toml | 6 + .../cargo_autoharness_fn_bounds/config.yml | 5 + .../fn_bounds.expected | 11 + .../cargo_autoharness_fn_bounds/fn_bounds.sh | 8 + .../cargo_autoharness_fn_bounds/src/lib.rs | 83 ++++++ 11 files changed, 530 insertions(+), 27 deletions(-) create mode 100644 tests/script-based-pre/cargo_autoharness_fn_bounds/Cargo.toml create mode 100644 tests/script-based-pre/cargo_autoharness_fn_bounds/config.yml create mode 100644 tests/script-based-pre/cargo_autoharness_fn_bounds/fn_bounds.expected create mode 100755 tests/script-based-pre/cargo_autoharness_fn_bounds/fn_bounds.sh create mode 100644 tests/script-based-pre/cargo_autoharness_fn_bounds/src/lib.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 624c4d6db19c..2c9b278565f7 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -231,24 +231,28 @@ impl<'tcx, 'r> GotocCtx<'tcx, 'r> { // We could eventually expand this, but keep it simple for now. See: // https://github.com/model-checking/kani/issues/2936 let overall_type = self.codegen_ty_stable(ty); - let field_values: Vec = field_types - .iter() - .map(|t| { - if self.is_zst_stable(*t) { - Some(Expr::init_unit( - self.codegen_ty_stable(*t), - &self.symbol_table, - )) - } else { - self.try_codegen_constant(alloc, *t, loc) - } - }) - .collect::>>()?; - Some(Expr::struct_expr_from_values( - overall_type, - field_values, - &self.symbol_table, - )) + // Pair values with their field names (declaration indices): the goto + // struct type is in LAYOUT order, which may differ from declaration + // order (e.g. #[repr] optimizations reordering a (T, u16) pair), so a + // positional struct_expr_from_values would mismatch. + let field_values: std::collections::BTreeMap = + variant + .fields() + .iter() + .zip(field_types.iter()) + .map(|(field, t)| { + let value = if self.is_zst_stable(*t) { + Some(Expr::init_unit( + self.codegen_ty_stable(*t), + &self.symbol_table, + )) + } else { + self.try_codegen_constant(alloc, *t, loc) + }; + value.map(|v| (field.name.clone().into(), v)) + }) + .collect::>()?; + Some(Expr::struct_expr(overall_type, field_values, &self.symbol_table)) } else { // Structures with more than one non-ZST element are handled with an extra // allocation. diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index d5fdf85db63c..48a15151bdda 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -955,7 +955,19 @@ impl GotocCtx<'_, '_> { pub fn codegen_get_discriminant(&mut self, e: Expr, ty: Ty, res_ty: Ty) -> Expr { let layout = self.layout_of_stable(ty); match &layout.variants { - Variants::Empty => unreachable!("Discriminant for uninhabited enum with no variants"), + Variants::Empty => { + // No value of an uninhabited enum can exist, so this read is dynamically + // dead code: emit an assert(false)-guarded nondet instead of ICEing (the + // MIR can still contain the read, e.g. matches on a Result<_, !>-like + // enum in dependencies). + let goto_res_ty = self.codegen_ty_stable(res_ty); + self.codegen_unimplemented_expr( + "discriminant of uninhabited enum", + goto_res_ty, + Location::none(), + "https://github.com/model-checking/kani/issues/3832", + ) + } Variants::Single { index } => { let discr_val = layout .ty @@ -1643,7 +1655,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 1e19d8e7f994..8616020bac09 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -108,6 +108,16 @@ impl CodegenUnits { args, &crate_info.name, *kani_fns.get(&KaniModel::Any.into()).unwrap(), + &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 { @@ -508,7 +518,230 @@ 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 { +/// 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. +/// 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>, +} + +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; + 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); + if inputs.has_param() || output.has_param() { + return false; + } + // 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 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; + }; + 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 +} + +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()); }; @@ -529,6 +762,7 @@ fn choose_generic_instantiation(tcx: TyCtxt, fn_item: CrateItem) -> Result = identity_args .0 .iter() @@ -544,6 +778,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); } @@ -647,6 +900,7 @@ fn automatic_harness_partition( args: &Arguments, crate_name: &str, kani_any_def: FnDef, + nondet_fns: &NondetFnModels, ) -> (Vec, 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 @@ -698,6 +952,11 @@ fn automatic_harness_partition( // so we know that each of these arguments has a concrete type. let mut problematic_args = vec![]; for (idx, arg) in body.arg_locals().iter().enumerate() { + // 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; + } if !ty_arbitrary_cache.contains_key(&arg.ty) { let impls_arbitrary = implements_arbitrary(arg.ty, kani_any_def, &mut ty_arbitrary_cache) @@ -743,7 +1002,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 d5b97aa5406c..4ce61e4c9cc7 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 = "AnyModel")] diff --git a/kani-compiler/src/kani_middle/transform/automatic.rs b/kani-compiler/src/kani_middle/transform/automatic.rs index 59ca3bd34abf..820a7090f495 100644 --- a/kani-compiler/src/kani_middle/transform/automatic.rs +++ b/kani-compiler/src/kani_middle/transform/automatic.rs @@ -19,11 +19,12 @@ use rustc_middle::ty::TyCtxt; use rustc_public::CrateDef; use rustc_public::mir::mono::Instance; use rustc_public::mir::{ - AggregateKind, BasicBlockIdx, Body, BorrowKind, Local, MutBorrowKind, Mutability, Operand, - Place, Rvalue, SwitchTargets, Terminator, TerminatorKind, + AggregateKind, BasicBlockIdx, Body, BorrowKind, ConstOperand, Local, MutBorrowKind, Mutability, + Operand, Place, Rvalue, SwitchTargets, Terminator, TerminatorKind, }; use rustc_public::ty::{ - AdtDef, AdtKind, FnDef, GenericArgKind, GenericArgs, RigidTy, Ty, TyKind, UintTy, VariantDef, + AdtDef, AdtKind, FnDef, GenericArgKind, GenericArgs, MirConst, RigidTy, Ty, TyKind, UintTy, + VariantDef, }; use rustc_public_bridge::IndexedVal; use tracing::debug; @@ -135,6 +136,24 @@ fn call_kani_any_for_ty( mutability: Mutability, source: &mut SourceInstruction, ) -> 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"), + })), + source, + InsertPosition::Before, + ); + return lcl; + } if let TyKind::RigidTy(RigidTy::Ref(region, inner_ty, inner_mutability)) = ty.kind() { let inner_lcl = call_kani_any_for_ty(kani_any, body, inner_ty, inner_mutability, source); let ref_lcl = body.new_local(ty, source.span(body.blocks()), mutability); diff --git a/library/kani/src/arbitrary.rs b/library/kani/src/arbitrary.rs index f16f06165d29..96ad188799b0 100644 --- a/library/kani/src/arbitrary.rs +++ b/library/kani/src/arbitrary.rs @@ -23,3 +23,71 @@ impl Arbitrary for std::time::Duration { std::time::Duration::new(u64::any(), nanos) } } + +/// 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 000000000000..e798d3f6737e --- /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 000000000000..1b1690fcd3ed --- /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 000000000000..16576486a442 --- /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 000000000000..ba322c8517db --- /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 000000000000..e3de5507f222 --- /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() +}