Resolve fn-pointer type arguments in contract target paths

kani-compiler/src/kani_middle/resolve/type_resolution.rs

@@ -86,7 +86,46 @@ 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. 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");
+            }
+            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::<Result<Vec<_>, _>>()?;
+            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"),

tests/expected/function-contract/generic_fn_pointer_cabi.expected

@@ -0,0 +1 @@
+unable to find implementation of associated function `Probe::probe` for Wrap

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>(T);
+
+trait Probe {
+    fn probe(&self) -> u32;
+}
+
+impl Probe for Wrap<extern "C" fn(u8) -> u8> {
+    #[kani::ensures(|r| *r == 1)]
+    fn probe(&self) -> u32 {
+        1
+    }
+}
+
+mod verify {
+    use super::*;
+
+    #[kani::proof_for_contract(<Wrap<extern "C" fn(u8) -> 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();
+    }
+}

tests/expected/function-contract/generic_fn_pointer_higher_ranked.expected

@@ -0,0 +1 @@
+is not reachable from the harness

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
+// `<Wrap<fn(&u8) -> 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>(T);
+trait Probe {
+    fn probe(&self) -> u32;
+}
+
+impl Probe for Wrap<fn(&u8) -> u8> {
+    #[kani::ensures(|r| *r == 7)]
+    fn probe(&self) -> u32 {
+        7
+    }
+}
+
+impl Probe for Wrap<fn(&'static u8) -> u8> {
+    #[kani::ensures(|r| *r == 9)]
+    fn probe(&self) -> u32 {
+        9
+    }
+}
+
+#[kani::proof_for_contract(<Wrap<fn(&u8) -> u8> as Probe>::probe)]
+fn h_hr() {
+    fn d(x: &u8) -> u8 {
+        *x
+    }
+    let _ = Wrap(d as fn(&u8) -> u8).probe();
+}

tests/kani/FunctionContracts/generic_fn_pointer_argument.rs

@@ -0,0 +1,77 @@
+// 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`), 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.
+// `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>(T);
+
+trait Probe {
+    fn probe(&self) -> u32;
+}
+
+impl Probe for Wrap<fn(u8) -> 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<fn(&u8) -> u8> {
+    #[kani::ensures(|r| *r == 7)]
+    fn probe(&self) -> u32 {
+        7
+    }
+}
+
+impl Probe for Wrap<unsafe fn(u8) -> u8> {
+    #[kani::ensures(|r| *r == 3)]
+    fn probe(&self) -> u32 {
+        3
+    }
+}
+
+mod verify {
+    use super::*;
+
+    #[kani::proof_for_contract(<Wrap<fn(u8) -> 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(<Wrap<fn(&u8) -> 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(<Wrap<unsafe fn(u8) -> 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();
+    }
+}