Fix stubbing bugs: FFI name resolution and generic parameter validation#4565
Merged
tautschnig merged 4 commits intomodel-checking:mainfrom Mar 27, 2026
Merged
Conversation
Fix three stubbing bugs that block stabilization. All existing tests pass (564 kani + 442 expected, 0 failures). Fix model-checking#2686, model-checking#2673: Foreign function stubs fail name resolution Functions declared in `extern "C" { fn foo(); }` blocks were not found by the stub name resolution because `resolve_relative` only searched top-level module items. Foreign functions are children of `ForeignMod` items, not top-level items themselves. Fix: When a name is not found as a direct module item, also search inside `ForeignMod` blocks by iterating their HIR foreign items. Additionally, the "no body" validation in attributes.rs rejected foreign functions with "function does not have a body, but is not an extern function". Fix: exclude `is_foreign_item` from this check. Fix model-checking#1953: Generic parameter names must match between original and stub 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 type than `T`. Fix: Build a substitution mapping the stub's generic parameters to the original's parameters (by position), then apply it before comparing types. Uses `GenericArgs::identity_for_item` as the base to correctly handle parent type parameters (e.g., methods on `LocalType<T>`). Partial progress on model-checking#2007: Lifetime mismatch detection 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`) no longer cause false rejections. A TODO note documents that lifetime mismatches can still cause subtle verification failures. Tests added: - stub_foreign_function.rs: regression test for model-checking#2686 - stub_generic_param_rename.rs: regression test for model-checking#1953 Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
Promote fixme_issue_1953.rs to a regular passing test now that model-checking#1953 is fixed (renamed to stub_generic_param_rename_simple.rs). Add additional test scenarios: - stub_multiple_foreign_functions.rs: multiple extern "C" functions stubbed from the same block (model-checking#2686) - stub_generic_multi_param_rename.rs: multiple generic type parameters with different names (model-checking#1953) Update stubbing documentation (stubbing.md): - Add 'Stubbing foreign functions' section with example showing how to stub extern "C" functions. - Add 'Stub compatibility and lifetime considerations' section warning that lifetime mismatches are accepted but can cause subtle verification failures (model-checking#2007). Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
resolve.rs: - Add comment explaining find_map short-circuit semantics with ForeignMod - Add comment explaining first-match behavior for duplicate foreign names (rustc rejects duplicate symbols, so no ambiguity diagnostic needed) attributes.rs: - Clarify comment that is_foreign_item exclusion applies to both the original and replacement sides stubbing/mod.rs: - Rename `substs` to `rename_args` to align with rustc naming convention - Remove unused `typing_env` variable - Simplify param collection (remove unnecessary tuple wrapping) - Add comment clarifying error messages show user's original types Tests: - Add negative test (stubbing-type-mismatch-after-rename) verifying that a genuinely wrong return type is still rejected after generic renaming - Fix misleading comment in stub_multiple_foreign_functions.rs Documentation: - Replace trivially-true assertion in FFI example with meaningful one Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
Run ./scripts/kani-fmt.sh to fix formatting of long tuple pattern match arms in check_compatibility that exceeded the line length limit. Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
tautschnig
approved these changes
Mar 27, 2026
Merged
via the queue into
model-checking:main
with commit Mar 27, 2026
105be6b
40 of 42 checks passed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
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 ofForeignModHIR 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:
ForeignModblocks by iterating their HIR foreign items.is_foreign_itemfrom the no-body rejection.Bug 2: Generic parameter names must match (#1953)
Stub validation compared MIR body types directly, which meant
bar<S>() -> Swas rejected as a stub forfoo<T>() -> Tbecause the generic parameter S produced a different Ty than T. The RFC explicitly states this should work.Fix:
GenericArgs::identity_for_itemas the base to correctly handle parent type parameters (e.g., methods onLocalType<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 selfvs&charin 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:
Promoted from fixme:
Documentation
Updated docs/src/reference/experimental/stubbing.md:
Call-outs
GenericArgs::identity_for_itemto get the full substitution (including parent typeparams), then overrides the function's ownparamsby position. This correctly handles methods on generic types likeLocalType<T>::pub_fn.libc::sysconf) already worked viaresolve_in_foreign_modulewhen 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.