Resolve multi-candidate methods on impls defined outside the type's module - #4778
Resolve multi-candidate methods on impls defined outside the type's module#4778kasimte wants to merge 2 commits into
Conversation
…odule resolve_in_type_def refines multiple same-named inherent-impl candidates by comparing the user's turbofish generic arguments against the last two ::-separated segments of def_path_str(candidate). When a candidate's impl block lives in a different module than its self type, def_path_str renders it as `path::to::module::<impl path::to::Type<Args>>::method` instead of `Type::<Args>::method`, and no user-spellable turbofish can match that <impl ...> wrapper. Real instance: Box<dyn Any(+Send)(+Sync), A>::downcast_unchecked's three impls live in alloc/src/boxed/convert.rs while Box is defined in boxed.rs. Add a fallback in last_two_items_of_path_match: when the direct comparison fails and the candidate's second-to-last path segment is in <impl SELF_TYPE> form, extract SELF_TYPE's own generic arguments and retry the comparison against those. The retry strips the redundant parens def_path_str adds around a trait-object bound in a generic-argument list (e.g. `(dyn Any + 'static)` -> `dyn Any + 'static`) before comparing; tuple-type parens are semantic and preserved.
github-actions
Bot
added
Z-EndToEndBenchCI
There was a problem hiding this comment.
Warning
Copilot couldn't run its full agentic review because it didn't start before the timeout. Make sure your repository has a runner available, or add a copilot-code-review.yml file specifying one with the runs-on attribute. See the docs for more details.
Pull request overview
Fixes Kani’s method contract resolution when multiple inherent impl candidates exist and the impl blocks are defined outside the self type’s home module (where def_path_str renders candidates as <impl path::Type<Args>>), and adds regression tests to cover this case.
Changes:
- Extend
last_two_items_of_path_matchto unwrap<impl SELF_TYPE>renderings and retry matching against extracted generic args. - Add helpers to extract self-type generic args and normalize redundant parens around trait-object bounds.
- Add unit tests plus an end-to-end regression test covering cross-module multiple-impl resolution.
Reviewed changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated 3 comments.
| File | Description |
|---|---|
| tests/kani/FunctionContracts/cross_module_multiple_impls.rs | Adds an integration regression reproducing cross-module multiple-impl resolution for proof_for_contract. |
| kani-compiler/src/kani_middle/resolve.rs | Implements <impl SELF_TYPE> fallback matching and adds targeted unit tests. |
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
| fn impl_self_type_generic_args(part: &str) -> Option<&str> { | ||
| let self_type = part.strip_prefix("<impl ")?.strip_suffix('>')?; | ||
| let start = self_type.find('<')?; | ||
| let mut depth = 0; | ||
| for (i, c) in self_type[start..].char_indices() { | ||
| match c { | ||
| '<' => depth += 1, | ||
| '>' => { | ||
| depth -= 1; | ||
| if depth == 0 { | ||
| return Some(&self_type[start + 1..start + i]); | ||
| } | ||
| } | ||
| _ => {} | ||
| } | ||
| } | ||
| None | ||
| } |
There was a problem hiding this comment.
Addressed in f3a28a3: extraction returns None unless the depth-0 close consumes the self type's full generic list, so a truncated extraction is impossible (impl_self_type_fn_ptr_args_decline). For accuracy: through the full pipeline, arrow-bearing candidate paths already fail one stage earlier — the top-level :: split leaves them unmatchable — so this is helper-level hardening; either way the outcome is the clean failed-to-resolve described in the body's call-out.
|
|
||
| for (i, c) in args.char_indices() { | ||
| match c { | ||
| '<' | '(' => depth += 1, | ||
| '>' | ')' => depth -= 1, | ||
| ',' if depth == 0 => { | ||
| parts.push(&args[part_start..i]); | ||
| part_start = i + 1; | ||
| } | ||
| _ => {} | ||
| } | ||
| } |
There was a problem hiding this comment.
Addressed in f3a28a3: strip_redundant_parens returns its input unchanged when the list contains -> — the construct that could drive the depth negative — so such lists skip normalization entirely rather than risk a wrong split. Unit test: strip_redundant_parens_arrow_list_unchanged.
| if last_two.chars().eq(actual_last_two.chars().filter(|c| !c.is_whitespace())) { | ||
| return true; | ||
| } |
There was a problem hiding this comment.
In production the user side cannot carry whitespace — generic_args_to_string (resolve.rs:593) strips it when rendering the turbofish, which is why the pre-existing comparison filtered one side only; the spaced strings in the new unit tests exercise the helper directly, bypassing that rendering step. f3a28a3 filters both sides anyway so the helper is self-contained and consistent with the fallback path (whitespace_insensitive_primary_match).
- Trim each top-level argument before the paren checks: the ", " separator's space otherwise defeats fully_parenthesized for every trait-object bound after the first argument position, wrongly declining the bare spelling there. - Drop the paren-strip call on the user's turbofish and correct the comment that claimed both-sides stripping: the caller renders the turbofish whitespace-free with its `::<...>` wrapper intact, which keeps every comma below top level, so the call could never strip anything. def_path_str's disambiguation parens are stripped from the candidate side only; the user spells the bound bare. - Decline renderings the bracket counting cannot parse: extraction returns None unless it consumes the self type's full generic list (a premature close, e.g. the `>` of a fn-pointer's `->`, declines), and arrow-bearing argument lists skip paren normalization. These are helper-level guards: on the full pipeline the top-level `::` split already leaves arrow-bearing candidate paths unmatchable, so such candidates were and remain a clean failed-to-resolve. - Make the primary comparison whitespace-insensitive on both sides rather than relying on the caller's pre-stripping. - Pin the trait-object paren-strip end-to-end: the regression test gains a cross-module dyn-argument candidate pair (fails to resolve if the strip is disabled), alongside four new unit tests.
Resolves #4777.
last_two_items_of_path_matchcompares the user's turbofish againstdef_path_str's rendering of each candidate. Impls living outside their type's home module render as<impl Type<Args>>, which no user-spellable path can equal — so multi-candidate methods in that position (e.g. the threeBox<dyn Any(+Send)(+Sync), A>::downcast_uncheckedimpls in alloc'sboxed/convert.rs) fail to resolve under every spelling, while single-candidate methods skip refinement and work.This is the out-of-module half of #3773 (whose fix and
multiple_inherent_impls.rstest cover the same-module rendering). It adds a fallback that unwraps the<impl SELF_TYPE>form, extracts SELF_TYPE's generic arguments, strips the disambiguation parenthesesdef_path_stradds around trait-object bounds (tuple-type parentheses are semantic and preserved), and retries the comparison.Scope: this keeps the existing string-comparison approach and only unblocks the out-of-module rendering; the milder same-module symptom (concrete turbofish arguments not matching a structured self-type such as
MaybeUninit<u32>vs the impl'sMaybeUninit<T>— the generic-parameter spelling works there) is unchanged, and a semantic-resolution rewrite would subsume both. Two smaller spelling asymmetries are also known and left to that same follow-up: a trait-object bound nested inside another generic argument still requires def_path_str's parenthesized spelling (normalization is not recursive), and same-module dyn-argument candidates still require it too (the primary comparison does no paren normalization). Happy to take direction if the deeper rewrite is preferred.Tests: eight unit tests in the existing
simple_last_two_items_of_path_matchmodule (dyn-args match + mismatch, dyn in second argument position, tuple parens preserved, non-generic no-fallback, fn-pointer renderings decline cleanly, arrow-bearing lists skip normalization, spaced turbofish matches on the primary path) and a new end-to-end regression testtests/kani/FunctionContracts/cross_module_multiple_impls.rswith tuple and trait-object candidate pairs (fails to resolve without the fix, verifies with it; the dyn pair fails if the paren-strip is disabled). Also validated on the motivating case: all threeBox<dyn Any…>::downcast_uncheckedcontracts in verify-rust-std resolve and verify asproof_for_contracttargets under the patched resolver.Applies cleanly on current
main(last_two_items_of_path_matchis unchanged there). One call-out: candidates whose rendered path contains->(fn-pointer /Fn-sugar types) are not unwrapped by the fallback — the top-level::split already leaves such paths unmatchable, and the helpers additionally decline anything their bracket counting cannot parse — so these keep the existing failed-to-resolve behavior rather than matching a different candidate (unit-tested).Motivating case: model-checking/verify-rust-std#669 — the three
Box<dyn Any…>::downcast_uncheckedcontract targets there.By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.