From 87453ff4a8a35c20b23ef8200c1a404b82383199 Mon Sep 17 00:00:00 2001 From: Kasim Te <91560+kasimte@users.noreply.github.com> Date: Tue, 29 Sep 2026 07:44:24 -0400 Subject: [PATCH 1/2] Resolve fn-pointer type arguments in contract target paths A Type::BareFn arm in resolve_ty builds the corresponding fn-pointer type (Rust ABI, non-variadic; lifetimes erased like every other path argument), so targets like u8> as Probe>::probe and the std adapters' , fn(&u8) -> u8> as Iterator>::__iterator_get_unchecked resolve. A non-Rust-ABI or variadic fn pointer keeps the uninstantiated type, as before. (cherry picked from commit ba34bb1f568c4ce388e0e4175df2bc90720576f6) --- .../kani_middle/resolve/type_resolution.rs | 39 +++++++++- .../generic_fn_pointer_cabi.expected | 1 + .../generic_fn_pointer_cabi.rs | 33 ++++++++ .../generic_fn_pointer_argument.rs | 76 +++++++++++++++++++ 4 files changed, 148 insertions(+), 1 deletion(-) create mode 100644 tests/expected/function-contract/generic_fn_pointer_cabi.expected create mode 100644 tests/expected/function-contract/generic_fn_pointer_cabi.rs create mode 100644 tests/kani/FunctionContracts/generic_fn_pointer_argument.rs diff --git a/kani-compiler/src/kani_middle/resolve/type_resolution.rs b/kani-compiler/src/kani_middle/resolve/type_resolution.rs index fe43d4841a5f..bd47d31b3c54 100644 --- a/kani-compiler/src/kani_middle/resolve/type_resolution.rs +++ b/kani-compiler/src/kani_middle/resolve/type_resolution.rs @@ -86,7 +86,44 @@ pub fn resolve_ty<'tcx>( Ok(Ty::new_tuple(&elems)) } Type::Never(_) => Ok(Ty::from_rigid_kind(RigidTy::Never)), - Type::BareFn(_) => unsupported("bare function"), + Type::BareFn(bare_fn) => { + // Rust-ABI, non-variadic fn pointers; lifetimes are erased like everywhere + // else in this resolver, so `fn(&u8) -> u8` and `for<'a> fn(&'a u8) -> u8` + // resolve to the same erased signature. + if bare_fn.variadic.is_some() { + return unsupported("variadic bare function"); + } + if bare_fn + .abi + .as_ref() + .is_some_and(|abi| abi.name.as_ref().is_none_or(|name| name.value() != "Rust")) + { + return unsupported("non-Rust-ABI bare function"); + } + let inputs = bare_fn + .inputs + .iter() + .map(|arg| resolve_ty(tcx, current_module, &arg.ty)) + .collect::, _>>()?; + let output = match &bare_fn.output { + syn::ReturnType::Default => Ty::new_tuple(&[]), + syn::ReturnType::Type(_, ty) => resolve_ty(tcx, current_module, ty)?, + }; + let safety = if bare_fn.unsafety.is_some() { + rustc_hir::Safety::Unsafe + } else { + rustc_hir::Safety::Safe + }; + let sig = tcx.mk_fn_sig_rust_abi( + inputs.iter().map(|ty| rustc_internal::internal(tcx, *ty)), + rustc_internal::internal(tcx, output), + safety, + ); + Ok(rustc_internal::stable(rustc_middle::ty::Ty::new_fn_ptr( + tcx, + rustc_middle::ty::Binder::dummy(sig), + ))) + } Type::Macro(_) => invalid("macro"), Type::Group(_) => invalid("group paths"), Type::ImplTrait(_) => invalid("trait impl paths"), diff --git a/tests/expected/function-contract/generic_fn_pointer_cabi.expected b/tests/expected/function-contract/generic_fn_pointer_cabi.expected new file mode 100644 index 000000000000..6d8f83f0349c --- /dev/null +++ b/tests/expected/function-contract/generic_fn_pointer_cabi.expected @@ -0,0 +1 @@ +unable to find implementation of associated function `Probe::probe` for Wrap diff --git a/tests/expected/function-contract/generic_fn_pointer_cabi.rs b/tests/expected/function-contract/generic_fn_pointer_cabi.rs new file mode 100644 index 000000000000..6d01e2cf0629 --- /dev/null +++ b/tests/expected/function-contract/generic_fn_pointer_cabi.rs @@ -0,0 +1,33 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +// A fn-pointer argument with a non-Rust ABI is not built by the `Type::BareFn` arm; +// the path keeps the uninstantiated type and fails to resolve, as before (see +// tests/kani/FunctionContracts/generic_fn_pointer_argument.rs for the supported cases). + +struct Wrap(T); + +trait Probe { + fn probe(&self) -> u32; +} + +impl Probe for Wrap u8> { + #[kani::ensures(|r| *r == 1)] + fn probe(&self) -> u32 { + 1 + } +} + +mod verify { + use super::*; + + #[kani::proof_for_contract( u8> as Probe>::probe)] + fn check_c_abi_fn_pointer() { + extern "C" fn id(x: u8) -> u8 { + x + } + let w = Wrap(id as extern "C" fn(u8) -> u8); + let _ = w.probe(); + } +} diff --git a/tests/kani/FunctionContracts/generic_fn_pointer_argument.rs b/tests/kani/FunctionContracts/generic_fn_pointer_argument.rs new file mode 100644 index 000000000000..ccf13723b157 --- /dev/null +++ b/tests/kani/FunctionContracts/generic_fn_pointer_argument.rs @@ -0,0 +1,76 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +// `proof_for_contract` on a target whose type arguments include a fn-pointer type. +// `resolve_ty` now builds the fn-pointer type from a `Type::BareFn` argument (Rust ABI, +// non-variadic; lifetimes erased like every other path argument), so these resolve and +// verify: +// * a plain fn-pointer argument (`fn(u8) -> u8`), +// * a reference-carrying fn pointer (`fn(&u8) -> u8`) — the impl's stored type is +// late-bound (`for<'a> fn(&'a u8) -> u8`); the erased argument still matches it, +// * an `unsafe` fn pointer (safety carried through the built signature). +// The two safe impls have distinct postconditions, so each harness only verifies if +// resolution picks *its* fn-pointer instantiation, not merely one of them. +// `generic_fn_pointer_cabi.rs` (expected suite) guards that a non-Rust-ABI fn pointer +// keeps the uninstantiated type and still fails to resolve. + +struct Wrap(T); + +trait Probe { + fn probe(&self) -> u32; +} + +impl Probe for Wrap u8> { + #[kani::ensures(|r| *r == 0)] + fn probe(&self) -> u32 { + 0 + } +} + +// Distinct postcondition from the `fn(u8) -> u8` impl, so a harness only verifies if +// resolution lands on *this* fn-pointer instantiation rather than the sibling. +impl Probe for Wrap u8> { + #[kani::ensures(|r| *r == 7)] + fn probe(&self) -> u32 { + 7 + } +} + +impl Probe for Wrap u8> { + #[kani::ensures(|r| *r == 3)] + fn probe(&self) -> u32 { + 3 + } +} + +mod verify { + use super::*; + + #[kani::proof_for_contract( u8> as Probe>::probe)] + fn check_plain_fn_pointer() { + fn id(x: u8) -> u8 { + x + } + let w = Wrap(id as fn(u8) -> u8); + let _ = w.probe(); + } + + #[kani::proof_for_contract( u8> as Probe>::probe)] + fn check_reference_carrying_fn_pointer() { + fn deref(x: &u8) -> u8 { + *x + } + let w = Wrap(deref as fn(&u8) -> u8); + let _ = w.probe(); + } + + #[kani::proof_for_contract( u8> as Probe>::probe)] + fn check_unsafe_fn_pointer() { + unsafe fn id(x: u8) -> u8 { + x + } + let w = Wrap(id as unsafe fn(u8) -> u8); + let _ = w.probe(); + } +} From 79d0b0e820c9de758bf9521fadd71267629d5faa Mon Sep 17 00:00:00 2001 From: Kasim Te <91560+kasimte@users.noreply.github.com> Date: Wed, 30 Sep 2026 14:03:19 -0400 Subject: [PATCH 2/2] Disclose higher-ranked fn-pointer limitation; add fixme test Erased regions make a higher-ranked fn-pointer target resolve to a coexisting 'static sibling impl. Corrects the comments that claimed the erased argument always matches, and adds h_hr as a fixme test. Binding the late-bound regions is tracked in #4933. Addresses review feedback on #4916 (Resolves #4909). --- .../kani_middle/resolve/type_resolution.rs | 6 ++- .../generic_fn_pointer_higher_ranked.expected | 1 + .../generic_fn_pointer_higher_ranked.rs | 39 +++++++++++++++++++ .../generic_fn_pointer_argument.rs | 5 ++- 4 files changed, 47 insertions(+), 4 deletions(-) create mode 100644 tests/expected/function-contract/generic_fn_pointer_higher_ranked.expected create mode 100644 tests/expected/function-contract/generic_fn_pointer_higher_ranked.rs diff --git a/kani-compiler/src/kani_middle/resolve/type_resolution.rs b/kani-compiler/src/kani_middle/resolve/type_resolution.rs index bd47d31b3c54..4ee14c40746b 100644 --- a/kani-compiler/src/kani_middle/resolve/type_resolution.rs +++ b/kani-compiler/src/kani_middle/resolve/type_resolution.rs @@ -88,8 +88,10 @@ pub fn resolve_ty<'tcx>( Type::Never(_) => Ok(Ty::from_rigid_kind(RigidTy::Never)), Type::BareFn(bare_fn) => { // Rust-ABI, non-variadic fn pointers; lifetimes are erased like everywhere - // else in this resolver, so `fn(&u8) -> u8` and `for<'a> fn(&'a u8) -> u8` - // resolve to the same erased signature. + // else in this resolver. A higher-ranked argument (`fn(&u8) -> u8`) + // therefore matches an erased impl; if a `fn(&'static u8) -> u8` sibling + // impl also exists, it resolves to that one instead (binding the late-bound + // regions is a follow-up; see https://github.com/model-checking/kani/issues/4933). if bare_fn.variadic.is_some() { return unsupported("variadic bare function"); } diff --git a/tests/expected/function-contract/generic_fn_pointer_higher_ranked.expected b/tests/expected/function-contract/generic_fn_pointer_higher_ranked.expected new file mode 100644 index 000000000000..0fe629adae7e --- /dev/null +++ b/tests/expected/function-contract/generic_fn_pointer_higher_ranked.expected @@ -0,0 +1 @@ +is not reachable from the harness diff --git a/tests/expected/function-contract/generic_fn_pointer_higher_ranked.rs b/tests/expected/function-contract/generic_fn_pointer_higher_ranked.rs new file mode 100644 index 000000000000..496f332ff05b --- /dev/null +++ b/tests/expected/function-contract/generic_fn_pointer_higher_ranked.rs @@ -0,0 +1,39 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +// FIXME: a higher-ranked fn-pointer target mis-resolves to a coexisting `'static` +// sibling impl. `resolve_ty` erases the fn pointer's lifetimes, so +// ` u8> as Probe>::probe` resolves to the `fn(&'static u8) -> u8` +// impl instead of its own, and `h_hr` cannot reach its target. Binding the late-bound +// regions (so the higher-ranked type stays distinct) is tracked at +// https://github.com/model-checking/kani/issues/4933. Both impls can coexist (rustc +// only warns with `coherence_leak_check`). +#![allow(coherence_leak_check)] + +struct Wrap(T); +trait Probe { + fn probe(&self) -> u32; +} + +impl Probe for Wrap u8> { + #[kani::ensures(|r| *r == 7)] + fn probe(&self) -> u32 { + 7 + } +} + +impl Probe for Wrap u8> { + #[kani::ensures(|r| *r == 9)] + fn probe(&self) -> u32 { + 9 + } +} + +#[kani::proof_for_contract( u8> as Probe>::probe)] +fn h_hr() { + fn d(x: &u8) -> u8 { + *x + } + let _ = Wrap(d as fn(&u8) -> u8).probe(); +} diff --git a/tests/kani/FunctionContracts/generic_fn_pointer_argument.rs b/tests/kani/FunctionContracts/generic_fn_pointer_argument.rs index ccf13723b157..df06455ddaf7 100644 --- a/tests/kani/FunctionContracts/generic_fn_pointer_argument.rs +++ b/tests/kani/FunctionContracts/generic_fn_pointer_argument.rs @@ -7,8 +7,9 @@ // non-variadic; lifetimes erased like every other path argument), so these resolve and // verify: // * a plain fn-pointer argument (`fn(u8) -> u8`), -// * a reference-carrying fn pointer (`fn(&u8) -> u8`) — the impl's stored type is -// late-bound (`for<'a> fn(&'a u8) -> u8`); the erased argument still matches it, +// * a reference-carrying fn pointer (`fn(&u8) -> u8`), whose impl's stored type is +// late-bound (`for<'a> fn(&'a u8) -> u8`); the erased argument matches it when no +// `fn(&'static u8) -> u8` sibling impl exists (see generic_fn_pointer_higher_ranked.rs), // * an `unsafe` fn pointer (safety carried through the built signature). // The two safe impls have distinct postconditions, so each harness only verifies if // resolution picks *its* fn-pointer instantiation, not merely one of them.