Fix stubbing bugs: FFI name resolution and generic parameter validation (#4565)

Fixes three stubbing bugs that block stabilization of the stubbing
feature.

Resolves #1953
Resolves #2686
Resolves #2673
Partial progress on #2007

## Bug 1: Foreign function stubs fail name resolution (#2686, #2673)

Functions declared in `extern "C" { fn foo(); }` blocks could not be
stubbed because the name resolution algorithm (`resolve_relative`) only
searched top-level module items. Foreign functions are children of
`ForeignMod` HIR items, not top-level items themselves.

Additionally, the stub validation in attributes.rs rejected foreign
functions with "function does not have a body, but is not an extern
function" — the check was intended to catch trait functions without
default bodies, but it also caught `extern "C"` functions.

Fix:
- resolve.rs: When a name is not found as a direct module item, also
search inside `ForeignMod` blocks by iterating their HIR foreign items.
- attributes.rs: Exclude `is_foreign_item` from the no-body rejection.

## Bug 2: Generic parameter names must match (#1953)

Stub validation compared MIR body types directly, which meant `bar<S>()
-> S` was rejected as a stub for `foo<T>() -> T` because the generic
parameter S produced a different Ty than T. The RFC explicitly states
this should work.

Fix:
- stubbing/mod.rs: Build a substitution mapping the stub's generic
parameters to the original's parameters by position, using
`GenericArgs::identity_for_item` as the base to correctly handle parent
type parameters (e.g., methods on `LocalType<T>`). Apply the
substitution to the stub's types before comparing.

## Bug 3: Lifetime mismatch detection (partial, #2007)

Type comparison now uses MIR body types (which have regions erased)
combined with the generic renaming substitution. This means lifetime
differences between the original and stub (e.g., `&'a self` vs `&char`
in method-to-function stubs) no longer cause false rejections. A
documentation note warns users that lifetime mismatches can still cause
subtle verification failures.

## Tests

New tests:
- stub_foreign_function.rs — basic extern "C" function stubbing
- stub_multiple_foreign_functions.rs — multiple foreign functions from
one extern block
- stub_generic_param_rename.rs — single generic param T → S
- stub_generic_multi_param_rename.rs — multiple generic params A, B → X,
Y

Promoted from fixme:
- fixme_issue_1953.rs → stub_generic_param_rename_simple.rs (was
ignored, now passes)

## Documentation

Updated docs/src/reference/experimental/stubbing.md:
- New "Stubbing foreign functions" section with example
- New "Stub compatibility and lifetime considerations" section warning
about lifetime mismatches

## Call-outs

- The generic param renaming uses `GenericArgs::identity_for_item` to
get the full substitution (including parent type `params`), then
overrides the function's own `params` by position. This correctly
handles methods on generic types like `LocalType<T>::pub_fn`.
- Region/lifetime comparison is intentionally relaxed (erased) — the old
code also didn't compare lifetimes (MIR body types have regions erased).
The difference is now documented.
- The FFI fix only handles local extern blocks. Foreign functions from
external crates (e.g., `libc::sysconf`) already worked via
`resolve_in_foreign_module` when the crate was resolved; the issue was
only with local extern "C" declarations.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

Author: feliperodri

docs/src/reference/experimental/stubbing.md

@@ -106,6 +106,40 @@ VERIFICATION:- SUCCESSFUL
 
 Kani shows that the assertion is successful, avoiding any issues that appear if we attempt to verify the code without stubbing.
 
+## Stubbing foreign functions
+
+Kani supports stubbing foreign functions declared in `extern` blocks. This is useful for
+replacing system calls, C library functions, or other FFI functions with verification-friendly
+implementations:
+
+```rust
+extern "C" {
+    fn my_c_function(input: u32) -> u32;
+}
+
+fn my_c_function_stub(input: u32) -> u32 {
+    input + 1
+}
+
+#[kani::proof]
+#[kani::stub(my_c_function, my_c_function_stub)]
+fn check_with_ffi_stub() {
+    let result = unsafe { my_c_function(42) };
+    assert_eq!(result, 43);
+}
+```
+
+## Stub compatibility and lifetime considerations
+
+When validating stub compatibility, Kani compares parameter and return types after erasing
+lifetime information. This means that a stub with different lifetime annotations than the
+original will be accepted. For example, a stub returning `&'static i32` will be accepted as
+a replacement for a function returning `&'a i32`.
+
+**Warning:** While Kani accepts such stubs, lifetime mismatches can cause subtle verification
+failures (e.g., "dereference failure: dead object"). If you encounter unexpected failures with
+stubs, check whether the lifetime annotations match.
+
 ## Limitations
 
 In the following, we describe all the limitations of the stubbing feature.

kani-compiler/src/kani_middle/attributes.rs

@@ -787,10 +787,14 @@ impl<'tcx> KaniAttributes<'tcx> {
                     let replace_res = self.resolve_path(current_module, replace, attr.span()).map(|res| res.def());
 
                     if let Ok(original_res) = original_res && let Ok(replace_res) = replace_res {
-                        // Emit an error if either function is local, yet doesn't have a body.
-                        // This can happen if a user specifies a trait fn without a default body, e.g. B::bar, where B is a trait.
-                        let o_bad = original_res.krate().is_local && !original_res.has_body();
-                        let r_bad = replace_res.krate().is_local && !replace_res.has_body();
+                        // Emit an error if either the original or the replacement is local yet
+                        // doesn't have a body. This catches trait fns without a default body
+                        // (e.g., B::bar where B is a trait). Foreign functions (extern "C") are
+                        // expected to not have bodies, so we exclude them on both sides.
+                        let o_def_id = rustc_internal::internal(self.tcx, original_res.def_id());
+                        let r_def_id = rustc_internal::internal(self.tcx, replace_res.def_id());
+                        let o_bad = original_res.krate().is_local && !original_res.has_body() && !self.tcx.is_foreign_item(o_def_id);
+                        let r_bad = replace_res.krate().is_local && !replace_res.has_body() && !self.tcx.is_foreign_item(r_def_id);
 
                         if o_bad || r_bad {
                             let mut err = self.tcx.dcx().struct_span_err(

kani-compiler/src/kani_middle/resolve.rs

@@ -454,6 +454,11 @@ fn resolve_relative(tcx: TyCtxt, current_module: LocalModDefId, name: &str) -> R
     debug!(?name, ?current_module, "resolve_relative");
 
     let mut glob_imports = vec![];
+    let mut foreign_items = vec![];
+    // Note: `find_map` short-circuits on `Some`, but the `ForeignMod` branch
+    // always returns `None`, so foreign items are always collected even if
+    // `find_map` returns early from a different branch. This is intentional:
+    // direct module items take precedence over foreign items.
     let result = tcx.hir_module_free_items(current_module).find_map(|item_id| {
         let item = tcx.hir_item(item_id);
         if item.kind.ident().is_some_and(|ident| ident.as_str() == name) {
@@ -473,10 +478,31 @@ fn resolve_relative(tcx: TyCtxt, current_module: LocalModDefId, name: &str) -> R
                 // since paths resolved via non-globs take precedence.
                 glob_imports.extend(use_path.res.present_items());
             }
+            // Collect foreign items declared inside `extern` blocks so we can
+            // search them if the name is not found as a direct module item.
+            // This handles `extern "C" { fn foo(); }` where `foo` is a child
+            // of the ForeignMod, not a top-level module item. (fixes #2686, #2673)
+            if let ItemKind::ForeignMod { items, .. } = item.kind {
+                for foreign_item in items {
+                    let fi = tcx.hir_foreign_item(*foreign_item);
+                    if fi.ident.as_str() == name {
+                        foreign_items.push(fi.owner_id.def_id.to_def_id());
+                    }
+                }
+            }
             None
         }
     });
-    result.map_or(RelativeResolution::Globs(glob_imports), RelativeResolution::Found)
+    if let Some(def_id) = result {
+        return RelativeResolution::Found(def_id);
+    }
+    // Take the first matching foreign item. If multiple `extern` blocks declare
+    // functions with the same name, that is a user error (rustc would reject it
+    // as a duplicate symbol), so we don't need ambiguity diagnostics here.
+    if let Some(def_id) = foreign_items.into_iter().next() {
+        return RelativeResolution::Found(def_id);
+    }
+    RelativeResolution::Globs(glob_imports)
 }
 
 /// Resolves a path relative to a local or foreign module.

kani-compiler/src/kani_middle/stubbing/mod.rs

@@ -119,21 +119,84 @@ pub fn check_compatibility(tcx: TyCtxt, old_def: FnDef, new_def: FnDef) -> Resul
     }
     // Check whether the types match. Index 0 refers to the returned value,
     // indices [1, `arg_count`] refer to the parameters.
-    // TODO: We currently force generic parameters in the stub to have exactly
-    // the same names as their counterparts in the original function/method;
-    // instead, we should be checking for the equivalence of types up to the
-    // renaming of generic parameters.
-    // <https://github.com/model-checking/kani/issues/1953>
+    // We compare types up to renaming of generic parameters (fixes #1953).
+    // Build a substitution from new generic params to old generic params by position.
+    // We need to handle both the function's own params AND parent type params.
+    let old_generics = tcx.generics_of(old_def_id);
+    let new_generics = tcx.generics_of(new_def_id);
+
+    let old_all_params: Vec<_> = old_generics.own_params.iter().collect();
+    let new_all_params: Vec<_> = new_generics.own_params.iter().collect();
+
+    // Build identity substitution for the new function, then override with
+    // old param names where positions match. Using identity_for_item ensures
+    // parent type params (e.g., T in `impl<T> MyStruct<T>`) are included.
+    let new_identity = ty::GenericArgs::identity_for_item(tcx, new_def_id);
+    let mut rename_args: Vec<ty::GenericArg<'_>> = new_identity.iter().collect();
+
+    for (i, new_param) in new_all_params.iter().enumerate() {
+        if i < old_all_params.len() {
+            let old_param = old_all_params[i];
+            let idx = new_param.index as usize;
+            if idx < rename_args.len() {
+                match (&old_param.kind, &new_param.kind) {
+                    (
+                        ty::GenericParamDefKind::Type { .. },
+                        ty::GenericParamDefKind::Type { .. },
+                    ) => {
+                        rename_args[idx] = ty::GenericArg::from(ty::Ty::new_param(
+                            tcx,
+                            old_param.index,
+                            old_param.name,
+                        ));
+                    }
+                    (ty::GenericParamDefKind::Lifetime, ty::GenericParamDefKind::Lifetime) => {
+                        rename_args[idx] = ty::GenericArg::from(ty::Region::new_early_param(
+                            tcx,
+                            ty::EarlyParamRegion { index: old_param.index, name: old_param.name },
+                        ));
+                    }
+                    (
+                        ty::GenericParamDefKind::Const { .. },
+                        ty::GenericParamDefKind::Const { .. },
+                    ) => {
+                        rename_args[idx] = ty::GenericArg::from(ty::Const::new_param(
+                            tcx,
+                            ty::ParamConst { index: old_param.index, name: old_param.name },
+                        ));
+                    }
+                    _ => {} // Keep identity for mismatched kinds; type comparison will catch it
+                }
+            }
+        }
+    }
+
+    // Compare types from the MIR bodies with generic parameter renaming applied.
+    // MIR body types already have regions erased, so lifetime differences
+    // (e.g., &'a self vs &char) don't cause false mismatches.
+    // The renaming substitution ensures different generic parameter names
+    // (e.g., T vs S) don't cause false mismatches either (fixes #1953).
+    // Note: Lifetime mismatches may still cause verification failures (#2007).
+    let rename_args = tcx.mk_args(&rename_args);
+
     let old_ret_ty = old_body.ret_local().ty;
     let new_ret_ty = new_body.ret_local().ty;
+    let old_ret_internal = rustc_internal::internal(tcx, old_ret_ty);
+    let new_ret_internal = rustc_internal::internal(tcx, new_ret_ty);
+    let new_ret_renamed = EarlyBinder::bind(new_ret_internal).instantiate(tcx, rename_args);
+
     let mut diff = vec![];
-    if old_ret_ty != new_ret_ty {
+    // Error messages show the user's original types (before renaming) for clarity.
+    if old_ret_internal != new_ret_renamed {
         diff.push(format!("Expected return type `{old_ret_ty}`, but found `{new_ret_ty}`"));
     }
     for (i, (old_arg, new_arg)) in
         old_body.arg_locals().iter().zip(new_body.arg_locals().iter()).enumerate()
     {
-        if old_arg.ty != new_arg.ty {
+        let old_ty_internal = rustc_internal::internal(tcx, old_arg.ty);
+        let new_ty_internal = rustc_internal::internal(tcx, new_arg.ty);
+        let new_renamed = EarlyBinder::bind(new_ty_internal).instantiate(tcx, rename_args);
+        if old_ty_internal != new_renamed {
             diff.push(format!(
                 "Expected type `{}` for parameter {}, but found `{}`",
                 old_arg.ty,
@@ -150,6 +213,9 @@ pub fn check_compatibility(tcx: TyCtxt, old_def: FnDef, new_def: FnDef) -> Resul
             diff.iter().join("\n - ")
         ))
     } else {
+        // Note: Lifetime mismatches between the original and stub are not currently
+        // detected (#2007). Differing lifetimes (e.g., `-> &'static T` vs `-> &'a T`)
+        // can cause subtle verification failures such as "dereference failure: dead object".
         Ok(())
     }
 }

tests/expected/stubbing-type-mismatch-after-rename/expected

@@ -0,0 +1,2 @@
+Cannot stub `original` by `wrong_return_type`
+Expected return type `T`, but found `bool`

tests/expected/stubbing-type-mismatch-after-rename/main.rs

@@ -0,0 +1,21 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: -Z stubbing
+//
+//! Test that a stub with a genuinely wrong return type is still rejected
+//! after the generic parameter renaming logic.
+
+fn original<T: Default>(_x: T) -> T {
+    T::default()
+}
+
+fn wrong_return_type<S: Default>(_x: S) -> bool {
+    true
+}
+
+#[kani::proof]
+#[kani::stub(original, wrong_return_type)]
+fn check_wrong_return_type() {
+    let _result: u32 = original(42u32);
+}

tests/kani/Stubbing/stub_foreign_function.rs

@@ -0,0 +1,22 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: -Z stubbing
+//
+//! Test that foreign functions declared in `extern "C"` blocks can be stubbed.
+//! Regression test for https://github.com/model-checking/kani/issues/2686
+
+extern "C" {
+    fn foreign_fn() -> u32;
+}
+
+fn foreign_fn_stub() -> u32 {
+    42
+}
+
+#[kani::proof]
+#[kani::stub(foreign_fn, foreign_fn_stub)]
+fn check_foreign_fn_stub() {
+    let result = unsafe { foreign_fn() };
+    assert_eq!(result, 42);
+}

tests/kani/Stubbing/stub_generic_multi_param_rename.rs

@@ -0,0 +1,21 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: -Z stubbing
+//
+//! Test that generic parameter renaming works with multiple type parameters.
+//! Regression test for https://github.com/model-checking/kani/issues/1953
+
+fn original<A, B>(_x: A, _y: B) -> bool {
+    false
+}
+
+fn stub<X, Y>(_x: X, _y: Y) -> bool {
+    true
+}
+
+#[kani::proof]
+#[kani::stub(original, stub)]
+fn check_multi_generic_rename() {
+    assert!(original(42u32, "hello"));
+}

tests/kani/Stubbing/stub_generic_param_rename.rs

@@ -0,0 +1,22 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: -Z stubbing
+//
+//! Test that generic parameter names can differ between original and stub.
+//! Regression test for https://github.com/model-checking/kani/issues/1953
+
+fn original<T: Default>(_x: T) -> T {
+    T::default()
+}
+
+fn stub_with_different_name<S: Default>(_x: S) -> S {
+    S::default()
+}
+
+#[kani::proof]
+#[kani::stub(original, stub_with_different_name)]
+fn check_generic_param_rename() {
+    let result: u32 = original(42u32);
+    assert_eq!(result, 0); // stub returns Default::default() which is 0
+}

tests/kani/Stubbing/fixme_issue_1953.rs …bing/stub_generic_param_rename_simple.rstests/kani/Stubbing/fixme_issue_1953.rs renamed to tests/kani/Stubbing/stub_generic_param_rename_simple.rs tests/kani/Stubbing/fixme_issue_1953.rs renamed to tests/kani/Stubbing/stub_generic_param_rename_simple.rs

@@ -3,9 +3,8 @@
 //
 // kani-flags: -Z stubbing --harness main
 //
-// We currently require a stub and the original/function method to have the same
-// names for generic parameters; instead, we should allow for renaming.
-// See <https://github.com/model-checking/kani/issues/1953> for more information.
+// Regression test: generic parameter names can differ between original and stub.
+// Previously this was a fixme test for https://github.com/model-checking/kani/issues/1953
 
 fn foo<T>(_x: T) -> bool {
     false