From 23b563fc4ed2fa6408ea0561991f248da52cf557 Mon Sep 17 00:00:00 2001 From: Kasim Te <91560+kasimte@users.noreply.github.com> Date: Mon, 31 Aug 2026 10:52:30 -0400 Subject: [PATCH 1/4] Resolve multi-candidate methods on impls defined outside the type's module 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::>::method` instead of `Type::::method`, and no user-spellable turbofish can match that wrapper. Real instance: Box::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 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. --- kani-compiler/src/kani_middle/resolve.rs | 147 +++++++++++++++++- .../cross_module_multiple_impls.rs | 48 ++++++ 2 files changed, 194 insertions(+), 1 deletion(-) create mode 100644 tests/kani/FunctionContracts/cross_module_multiple_impls.rs diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs index 4e5ffa4cce3c..2430576d7df4 100644 --- a/kani-compiler/src/kani_middle/resolve.rs +++ b/kani-compiler/src/kani_middle/resolve.rs @@ -821,7 +821,106 @@ fn last_two_items_of_path_match(item_path: &str, generic_args: &str, name: &str) let last_two = format!("{}{}{}", generic_args, "::", name); // The last two components of the item_path should be the same as ::{generic_args}::{name} - last_two.chars().eq(actual_last_two.chars().filter(|c| !c.is_whitespace())) + if last_two.chars().eq(actual_last_two.chars().filter(|c| !c.is_whitespace())) { + return true; + } + + // A method whose impl block lives outside its self type's home module is rendered + // by def_path_str as `>` instead of `Type::`; unwrap + // that form and retry against Args. def_path_str also wraps trait-object bounds in + // redundant parens inside a generic-argument list (e.g. `(dyn Any + 'static)`), so + // strip those, and whitespace, from both sides before comparing. + if let Some(self_type_args) = impl_self_type_generic_args(parts[parts.len() - 2]) { + let unwrapped_last_two = + format!("::<{}>::{}", strip_redundant_parens(self_type_args), parts[parts.len() - 1]); + let last_two = format!("{}::{}", strip_redundant_parens(generic_args), name); + return last_two + .chars() + .filter(|c| !c.is_whitespace()) + .eq(unwrapped_last_two.chars().filter(|c| !c.is_whitespace())); + } + + false +} + +/// If `part` is the `` form def_path_str uses for a method whose impl +/// block lives outside SELF_TYPE's home module, returns the bracket-balanced contents +/// of SELF_TYPE's outermost `<...>` (its generic arguments). `None` if `part` isn't +/// that form, or SELF_TYPE isn't generic. +fn impl_self_type_generic_args(part: &str) -> Option<&str> { + let self_type = part.strip_prefix("')?; + 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 +} + +/// Splits a `,`-separated generic-argument list on its top-level commas and strips one +/// layer of parens from a top-level argument only when it wraps a trait-object bound +/// (`(dyn …)`); tuple-type parens are semantic and preserved. +fn strip_redundant_parens(args: &str) -> String { + let mut depth = 0i32; + let mut parts = Vec::new(); + let mut part_start = 0; + + 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; + } + _ => {} + } + } + parts.push(&args[part_start..]); + + parts + .into_iter() + .map(|part| { + if fully_parenthesized(part) && part[1..].trim_start().starts_with("dyn ") { + &part[1..part.len() - 1] + } else { + part + } + }) + .collect::>() + .join(",") +} + +/// Whether `s` starts with `(`, ends with `)`, and that opening paren's match is the +/// closing one at the end (as opposed to e.g. `(a)(b)`, which is wrapped but not by a +/// single pair). +fn fully_parenthesized(s: &str) -> bool { + if !s.starts_with('(') || !s.ends_with(')') { + return false; + } + let mut depth = 0i32; + for (i, c) in s.char_indices() { + match c { + '(' => depth += 1, + ')' => { + depth -= 1; + if depth == 0 { + return i == s.len() - 1; + } + } + _ => {} + } + } + false } #[cfg(test)] @@ -860,5 +959,51 @@ mod tests { let item_path = format!("rc::Rc{}::{}", "::, A>", name); assert!(last_two_items_of_path_match(&item_path, generic_args, name)) } + + // When a method's impl block lives outside its self type's home module (e.g. the + // dyn-self `downcast_unchecked` impls in alloc's boxed::convert vs. boxed::Box), + // def_path_str renders it as `>` instead of `Type::`, + // with the trait-object bound additionally wrapped in redundant parens. + #[test] + fn impl_self_type_dyn_args_match() { + let generic_args = "::"; + let name = "downcast_unchecked"; + let item_path = format!( + "boxed::convert::>::{name}" + ); + assert!(last_two_items_of_path_match(&item_path, generic_args, name)) + } + + #[test] + fn impl_self_type_dyn_args_mismatch() { + let generic_args = "::"; + let name = "downcast_unchecked"; + let item_path = format!( + "boxed::convert::>::{name}" + ); + assert!(!last_two_items_of_path_match(&item_path, generic_args, name)) + } + + // Unlike a trait-object bound, a tuple type's parens are semantic, not disambiguation + // wrapping: `S<(u32, u64), A>` has two generic args (a tuple, and A), not three. The + // bare, unparenthesized spelling must not falsely match; the user can still spell the + // tuple with parens to match how def_path_str renders it. + #[test] + fn impl_self_type_tuple_args_not_stripped() { + let name = "method"; + let item_path = format!("m::>::{name}"); + assert!(!last_two_items_of_path_match(&item_path, "::", name)); + assert!(last_two_items_of_path_match(&item_path, "::<(u32, u64), A>", name)); + } + + // A non-generic self type outside its home module (``, no `<...>` on S) + // has no generic args to refine against, so the fallback must not spuriously match. + #[test] + fn impl_self_type_non_generic_no_fallback() { + let generic_args = "::"; + let name = "method"; + let item_path = format!("m::::{name}"); + assert!(!last_two_items_of_path_match(&item_path, generic_args, name)) + } } } diff --git a/tests/kani/FunctionContracts/cross_module_multiple_impls.rs b/tests/kani/FunctionContracts/cross_module_multiple_impls.rs new file mode 100644 index 000000000000..0b31db0b6063 --- /dev/null +++ b/tests/kani/FunctionContracts/cross_module_multiple_impls.rs @@ -0,0 +1,48 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +// Check that Kani can verify contracts on methods where the base type has multiple +// same-named methods across impl blocks that live OUTSIDE the type's home module. This +// extends the same-module case in multiple_inherent_impls.rs (c.f. +// https://github.com/model-checking/kani/issues/3773) to the `>` +// path form def_path_str renders when an impl's module differs from its self type's. +// One candidate's generic argument is a tuple type, so this also exercises the +// tuple-vs-trait-object-bound paren distinction in that path's disambiguation. +pub mod ty { + pub struct S(pub T); +} + +pub mod ops { + use crate::ty::S; + + impl S<(u32, u64)> { + #[kani::requires(self.0.0.checked_mul(2).is_some() && self.0.1.checked_mul(2).is_some())] + pub fn double(self) -> (u32, u64) { + (self.0.0 * 2, self.0.1 * 2) + } + } + + impl S { + #[kani::requires(self.0.checked_mul(2).is_some())] + pub fn double(self) -> u64 { + self.0 * 2 + } + } +} + +mod verify { + use crate::ty::S; + + #[kani::proof_for_contract(S::<(u32, u64)>::double)] + fn verify_double_tuple_arg() { + let x: S<(u32, u64)> = S((2, 3)); + x.double(); + } + + #[kani::proof_for_contract(S::::double)] + fn verify_double_u64() { + let x: S = S(2); + x.double(); + } +} From f3a28a3823279c4c6c06fca2ec1667658a956509 Mon Sep 17 00:00:00 2001 From: Kasim Te <91560+kasimte@users.noreply.github.com> Date: Wed, 2 Sep 2026 21:04:47 -0400 Subject: [PATCH 2/4] Harden generic-argument normalization in the multi-candidate fallback - 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. --- kani-compiler/src/kani_middle/resolve.rs | 94 +++++++++++++++++-- .../cross_module_multiple_impls.rs | 40 +++++++- 2 files changed, 121 insertions(+), 13 deletions(-) diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs index 2430576d7df4..d0f1c6e678d0 100644 --- a/kani-compiler/src/kani_middle/resolve.rs +++ b/kani-compiler/src/kani_middle/resolve.rs @@ -820,20 +820,26 @@ fn last_two_items_of_path_match(item_path: &str, generic_args: &str, name: &str) let last_two = format!("{}{}{}", generic_args, "::", name); - // The last two components of the item_path should be the same as ::{generic_args}::{name} - if last_two.chars().eq(actual_last_two.chars().filter(|c| !c.is_whitespace())) { + // The last two components of the item_path should be the same as ::{generic_args}::{name}, + // compared whitespace-insensitively on both sides (the caller pre-strips generic_args, + // but the helper shouldn't rely on that). + if last_two + .chars() + .filter(|c| !c.is_whitespace()) + .eq(actual_last_two.chars().filter(|c| !c.is_whitespace())) + { return true; } // A method whose impl block lives outside its self type's home module is rendered // by def_path_str as `>` instead of `Type::`; unwrap // that form and retry against Args. def_path_str also wraps trait-object bounds in - // redundant parens inside a generic-argument list (e.g. `(dyn Any + 'static)`), so - // strip those, and whitespace, from both sides before comparing. + // redundant parens inside a generic-argument list (e.g. `(dyn Any + 'static)`); + // strip those from the candidate side; the user spells the bound bare. if let Some(self_type_args) = impl_self_type_generic_args(parts[parts.len() - 2]) { let unwrapped_last_two = format!("::<{}>::{}", strip_redundant_parens(self_type_args), parts[parts.len() - 1]); - let last_two = format!("{}::{}", strip_redundant_parens(generic_args), name); + let last_two = format!("{}::{}", generic_args, name); return last_two .chars() .filter(|c| !c.is_whitespace()) @@ -846,7 +852,8 @@ fn last_two_items_of_path_match(item_path: &str, generic_args: &str, name: &str) /// If `part` is the `` form def_path_str uses for a method whose impl /// block lives outside SELF_TYPE's home module, returns the bracket-balanced contents /// of SELF_TYPE's outermost `<...>` (its generic arguments). `None` if `part` isn't -/// that form, or SELF_TYPE isn't generic. +/// that form, SELF_TYPE isn't generic, or its generic list can't be parsed by bracket +/// counting (e.g. an argument contains `->`). fn impl_self_type_generic_args(part: &str) -> Option<&str> { let self_type = part.strip_prefix("')?; let start = self_type.find('<')?; @@ -857,7 +864,12 @@ fn impl_self_type_generic_args(part: &str) -> Option<&str> { '>' => { depth -= 1; if depth == 0 { - return Some(&self_type[start + 1..start + i]); + // A close before the final char means bracket counting mis-parsed + // the list (e.g. the `>` of a fn-pointer's `->`): decline. + if start + i == self_type.len() - 1 { + return Some(&self_type[start + 1..start + i]); + } + return None; } } _ => {} @@ -868,8 +880,15 @@ fn impl_self_type_generic_args(part: &str) -> Option<&str> { /// Splits a `,`-separated generic-argument list on its top-level commas and strips one /// layer of parens from a top-level argument only when it wraps a trait-object bound -/// (`(dyn …)`); tuple-type parens are semantic and preserved. +/// (`(dyn …)`); tuple-type parens are semantic and preserved. Lists containing `->` +/// are returned unchanged. fn strip_redundant_parens(args: &str) -> String { + // `->` (fn-pointer / `Fn`-sugar renderings) would corrupt the depth counting + // below; skip normalization for such lists. + if args.contains("->") { + return args.to_string(); + } + let mut depth = 0i32; let mut parts = Vec::new(); let mut part_start = 0; @@ -890,6 +909,9 @@ fn strip_redundant_parens(args: &str) -> String { parts .into_iter() .map(|part| { + // The top-level split leaves the ", " separator's space on every part + // after the first; trim so the paren check sees the argument itself. + let part = part.trim(); if fully_parenthesized(part) && part[1..].trim_start().starts_with("dyn ") { &part[1..part.len() - 1] } else { @@ -926,7 +948,9 @@ fn fully_parenthesized(s: &str) -> bool { #[cfg(test)] mod tests { mod simple_last_two_items_of_path_match { - use crate::kani_middle::resolve::last_two_items_of_path_match; + use crate::kani_middle::resolve::{ + impl_self_type_generic_args, last_two_items_of_path_match, strip_redundant_parens, + }; #[test] fn length_one_item_prefix() { @@ -1005,5 +1029,57 @@ mod tests { let item_path = format!("m::::{name}"); assert!(!last_two_items_of_path_match(&item_path, generic_args, name)) } + + // A generic argument containing `->` (fn-pointer / `Fn`-sugar rendering) defeats + // simple bracket counting: the arrow's `>` reads as a close. Extraction must + // decline (clean no-match), never return a truncated argument list. Note the + // full pipeline declines such candidates one stage earlier (the top-level `::` + // split leaves them unmatchable), so the direct assert is what exercises this + // guard; the end-to-end assert pins the pipeline's own no-match. + #[test] + fn impl_self_type_fn_ptr_args_decline() { + assert_eq!(impl_self_type_generic_args(" u32, A>>"), None); + let name = "method"; + let item_path = format!("m::x:: u32, A>>::{name}"); + assert!(!last_two_items_of_path_match(&item_path, "::u32,A>", name)); + } + + // An arrow-bearing list corrupts the comma-depth scan (the `>` of `->` closes + // nothing), which could split at a nested comma and strip parens that aren't + // top-level. Normalization is skipped wholesale for such lists; unstripped + // parens can only fail to match, never match the wrong candidate. + #[test] + fn strip_redundant_parens_arrow_list_unchanged() { + let args = "::u32,(dyn Any + 'static),B>"; + assert_eq!(strip_redundant_parens(args), args); + } + + // generic_args_to_string strips whitespace before this helper ever runs, but the + // helper shouldn't rely on its caller: a spaced turbofish must match on the + // primary (same-module) path too, as it already does on the fallback path. + #[test] + fn whitespace_insensitive_primary_match() { + assert!(last_two_items_of_path_match("m::S::::f", "::", "f")); + } + + // def_path_str separates arguments with ", ", so every argument after the first + // arrives from the top-level split with a leading space. The paren-strip must + // still recognize a trait-object bound there; the bare spelling matches + // regardless of the bound's position in the list. + #[test] + fn impl_self_type_dyn_second_position() { + assert_eq!( + strip_redundant_parens("u32, (dyn core::any::Any + 'static)"), + "u32,dyn core::any::Any + 'static" + ); + let name = "method"; + let item_path = + format!("m::x::>::{name}"); + assert!(last_two_items_of_path_match( + &item_path, + "::", + name + )); + } } } diff --git a/tests/kani/FunctionContracts/cross_module_multiple_impls.rs b/tests/kani/FunctionContracts/cross_module_multiple_impls.rs index 0b31db0b6063..c7d330df80f4 100644 --- a/tests/kani/FunctionContracts/cross_module_multiple_impls.rs +++ b/tests/kani/FunctionContracts/cross_module_multiple_impls.rs @@ -7,14 +7,19 @@ // extends the same-module case in multiple_inherent_impls.rs (c.f. // https://github.com/model-checking/kani/issues/3773) to the `>` // path form def_path_str renders when an impl's module differs from its self type's. -// One candidate's generic argument is a tuple type, so this also exercises the -// tuple-vs-trait-object-bound paren distinction in that path's disambiguation. +// One candidate's generic argument is a tuple type, exercising the +// tuple-vs-trait-object-bound paren distinction in that path's disambiguation; the `D` +// pair puts a trait object in the argument position, pinning the paren-strip itself +// (def_path_str renders that candidate as `>`, +// which must match the bare `dyn` spelling below). pub mod ty { pub struct S(pub T); + pub struct D(pub u32, pub Box); } pub mod ops { - use crate::ty::S; + use crate::ty::{D, S}; + use std::any::Any; impl S<(u32, u64)> { #[kani::requires(self.0.0.checked_mul(2).is_some() && self.0.1.checked_mul(2).is_some())] @@ -29,10 +34,25 @@ pub mod ops { self.0 * 2 } } + + impl D { + #[kani::requires(self.0.checked_mul(2).is_some())] + pub fn double_tag(self) -> u32 { + self.0 * 2 + } + } + + impl D { + #[kani::requires(self.0.checked_mul(2).is_some())] + pub fn double_tag(self) -> u32 { + self.0 * 2 + } + } } mod verify { - use crate::ty::S; + use crate::ty::{D, S}; + use std::any::Any; #[kani::proof_for_contract(S::<(u32, u64)>::double)] fn verify_double_tuple_arg() { @@ -45,4 +65,16 @@ mod verify { let x: S = S(2); x.double(); } + + #[kani::proof_for_contract(D::::double_tag)] + fn verify_double_tag_dyn() { + let x: D = D(2, Box::new(5u32)); + x.double_tag(); + } + + #[kani::proof_for_contract(D::::double_tag)] + fn verify_double_tag_u32() { + let x: D = D(2, Box::new(5u32)); + x.double_tag(); + } } From d4bd173c92ae5f00fdcb4890af80ed0ac912a126 Mon Sep 17 00:00:00 2001 From: Kasim Te <91560+kasimte@users.noreply.github.com> Date: Tue, 22 Sep 2026 23:04:17 -0400 Subject: [PATCH 3/4] Normalize trait-object parens on both sides of both path comparisons --- kani-compiler/src/kani_middle/resolve.rs | 110 ++++++++++++++---- .../cross_module_multiple_impls.rs | 47 +++++++- 2 files changed, 134 insertions(+), 23 deletions(-) diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs index 0190d97b543e..71e44f6371f8 100644 --- a/kani-compiler/src/kani_middle/resolve.rs +++ b/kani-compiler/src/kani_middle/resolve.rs @@ -880,6 +880,34 @@ fn is_item_name_with_generic_args( last_two_items_of_path_match(&item_path, generic_args, name) } +/// True if `s` has a `,` at bracket depth 0 (a tuple/list separator, not one nested +/// inside `<...>` or `(...)`). Whitespace-independent. +fn has_top_level_comma(s: &str) -> bool { + let mut depth = 0i32; + for c in s.chars() { + match c { + '<' | '(' => depth += 1, + '>' | ')' => depth -= 1, + ',' if depth == 0 => return true, + _ => {} + } + } + false +} + +/// Normalizes one side of a `::::name` comparison string: redundant trait-object +/// parens are stripped from each TOP-LEVEL generic argument and all whitespace is +/// removed, so the parenthesized rendering `def_path_str` uses and the bare spelling a +/// user writes compare equal in either impl location. A trait object nested inside +/// another argument keeps its rendered parens (a residual the semantic rewrite removes). +fn normalized_last_two(s: &str) -> String { + let s: String = s.chars().filter(|c| !c.is_whitespace()).collect(); + let Some((head, name)) = s.rsplit_once("::") else { return s }; + let Some((prefix, rest)) = head.split_once('<') else { return s }; + let Some(args) = rest.strip_suffix('>') else { return s }; + format!("{prefix}<{}>::{name}", strip_redundant_parens(args)) +} + // This is just a helper function for is_item_name_with_generic_args. // It's in a separate function so we can unit-test it without a mock TyCtxt or DefIds. fn last_two_items_of_path_match(item_path: &str, generic_args: &str, name: &str) -> bool { @@ -918,30 +946,23 @@ fn last_two_items_of_path_match(item_path: &str, generic_args: &str, name: &str) let last_two = format!("{}{}{}", generic_args, "::", name); - // The last two components of the item_path should be the same as ::{generic_args}::{name}, - // compared whitespace-insensitively on both sides (the caller pre-strips generic_args, - // but the helper shouldn't rely on that). - if last_two - .chars() - .filter(|c| !c.is_whitespace()) - .eq(actual_last_two.chars().filter(|c| !c.is_whitespace())) - { + // The last two components of the item_path should be the same as + // ::{generic_args}::{name}. Both sides are normalized identically (redundant + // trait-object parens stripped from top-level arguments, whitespace removed), so the + // parenthesized rendering def_path_str uses and the bare spelling a user writes match + // in either impl location. + let normalized_query = normalized_last_two(&last_two); + if normalized_query == normalized_last_two(&actual_last_two) { return true; } // A method whose impl block lives outside its self type's home module is rendered // by def_path_str as `>` instead of `Type::`; unwrap - // that form and retry against Args. def_path_str also wraps trait-object bounds in - // redundant parens inside a generic-argument list (e.g. `(dyn Any + 'static)`); - // strip those from the candidate side; the user spells the bound bare. + // that form and retry against Args through the same normalization (so either paren + // spelling matches in either impl location). if let Some(self_type_args) = impl_self_type_generic_args(parts[parts.len() - 2]) { - let unwrapped_last_two = - format!("::<{}>::{}", strip_redundant_parens(self_type_args), parts[parts.len() - 1]); - let last_two = format!("{}::{}", generic_args, name); - return last_two - .chars() - .filter(|c| !c.is_whitespace()) - .eq(unwrapped_last_two.chars().filter(|c| !c.is_whitespace())); + let unwrapped_last_two = format!("::<{}>::{}", self_type_args, parts[parts.len() - 1]); + return normalized_query == normalized_last_two(&unwrapped_last_two); } false @@ -977,9 +998,10 @@ fn impl_self_type_generic_args(part: &str) -> Option<&str> { } /// Splits a `,`-separated generic-argument list on its top-level commas and strips one -/// layer of parens from a top-level argument only when it wraps a trait-object bound -/// (`(dyn …)`); tuple-type parens are semantic and preserved. Lists containing `->` -/// are returned unchanged. +/// layer of parens from any top-level argument whose interior has no top-level comma — +/// the redundant grouping def_path_str adds around a trait-object bound (`(dyn …)`). +/// Tuple-type parens (a top-level comma) are semantic and preserved. Lists containing +/// `->` are returned unchanged. fn strip_redundant_parens(args: &str) -> String { // `->` (fn-pointer / `Fn`-sugar renderings) would corrupt the depth counting // below; skip normalization for such lists. @@ -1010,7 +1032,12 @@ fn strip_redundant_parens(args: &str) -> String { // The top-level split leaves the ", " separator's space on every part // after the first; trim so the paren check sees the argument itself. let part = part.trim(); - if fully_parenthesized(part) && part[1..].trim_start().starts_with("dyn ") { + // A fully-parenthesized argument whose interior has no top-level comma is + // redundant grouping def_path_str adds around a trait-object bound + // (`(dyn Any + 'static)`); the user writes it bare. A top-level comma means a + // tuple type, whose parens are semantic and must stay. Whitespace-independent, + // so it matches whether or not the caller pre-stripped spaces. + if fully_parenthesized(part) && !has_top_level_comma(&part[1..part.len() - 1]) { &part[1..part.len() - 1] } else { part @@ -1179,5 +1206,44 @@ mod tests { name )); } + + // A trait-object argument on an impl BESIDE its type (primary path): def_path_str + // renders `(dyn ...)`, and generic_args_to_string hands us a whitespace-free user + // side — so both must normalize equal. Inputs here are whitespace-free, matching + // what the pipeline actually produces (a spaced input would hide the bug). + #[test] + fn dyn_bound_parens_in_module() { + let name = "double_tag"; + let item_path = format!("ty::D::<(dynstd::any::Any+'static)>::{name}"); + assert!(last_two_items_of_path_match(&item_path, "::", name)); + assert!(last_two_items_of_path_match( + &item_path, + "::<(dynstd::any::Any+'static)>", + name + )); + } + + // Same, on the cross-module `` fallback path. + #[test] + fn dyn_bound_parens_cross_module() { + let name = "double_tag"; + let item_path = format!("ops::>::{name}"); + assert!(last_two_items_of_path_match(&item_path, "::", name)); + assert!(last_two_items_of_path_match( + &item_path, + "::<(dynstd::any::Any+'static)>", + name + )); + } + + // A tuple argument's parens are semantic: they must NOT be stripped, so a tuple + // never matches the same types spelled as a flat argument list. + #[test] + fn tuple_parens_preserved() { + let name = "f"; + let item_path = format!("m::S::<(u32,u64),A>::{name}"); + assert!(last_two_items_of_path_match(&item_path, "::<(u32,u64),A>", name)); + assert!(!last_two_items_of_path_match(&item_path, "::", name)); + } } } diff --git a/tests/kani/FunctionContracts/cross_module_multiple_impls.rs b/tests/kani/FunctionContracts/cross_module_multiple_impls.rs index c7d330df80f4..5bfc0af9005a 100644 --- a/tests/kani/FunctionContracts/cross_module_multiple_impls.rs +++ b/tests/kani/FunctionContracts/cross_module_multiple_impls.rs @@ -11,12 +11,35 @@ // tuple-vs-trait-object-bound paren distinction in that path's disambiguation; the `D` // pair puts a trait object in the argument position, pinning the paren-strip itself // (def_path_str renders that candidate as `>`, -// which must match the bare `dyn` spelling below). +// which must match the bare `dyn` spelling below). The `ty_local::L` pair keeps both +// impls BESIDE the type, exercising the same trait-object paren distinction on the +// primary (non-fallback) path; harnesses spell the bound both ways (`dyn ...` and the +// parenthesized `(dyn ...)` def_path_str prints in resolution errors) in both locations. pub mod ty { pub struct S(pub T); pub struct D(pub u32, pub Box); } +pub mod ty_local { + use std::any::Any; + + pub struct L(pub u32, pub Box); + + impl L { + #[kani::requires(self.0.checked_mul(2).is_some())] + pub fn double_tag(self) -> u32 { + self.0 * 2 + } + } + + impl L { + #[kani::requires(self.0.checked_mul(2).is_some())] + pub fn double_tag(self) -> u32 { + self.0 * 2 + } + } +} + pub mod ops { use crate::ty::{D, S}; use std::any::Any; @@ -52,6 +75,7 @@ pub mod ops { mod verify { use crate::ty::{D, S}; + use crate::ty_local::L; use std::any::Any; #[kani::proof_for_contract(S::<(u32, u64)>::double)] @@ -77,4 +101,25 @@ mod verify { let x: D = D(2, Box::new(5u32)); x.double_tag(); } + + // Cross-module, parenthesized `dyn` spelling (the exact form def_path_str prints). + #[kani::proof_for_contract(D::<(dyn std::any::Any + 'static)>::double_tag)] + fn verify_double_tag_dyn_cross_module_parens() { + let x: D = D(2, Box::new(5u32)); + x.double_tag(); + } + + // In-module multi-impl with a trait-object argument, bare spelling (primary path). + #[kani::proof_for_contract(L::::double_tag)] + fn verify_double_tag_dyn_in_module() { + let x: L = L(2, Box::new(5u32)); + x.double_tag(); + } + + // In-module multi-impl, parenthesized spelling. + #[kani::proof_for_contract(L::<(dyn std::any::Any + 'static)>::double_tag)] + fn verify_double_tag_dyn_in_module_parens() { + let x: L = L(2, Box::new(5u32)); + x.double_tag(); + } } From 128838744a1c962998b4f49a086a931c97fcccef Mon Sep 17 00:00:00 2001 From: Kasim Te <91560+kasimte@users.noreply.github.com> Date: Tue, 22 Sep 2026 23:04:36 -0400 Subject: [PATCH 4/4] Report multiple refined candidates as a resolution error instead of panicking --- kani-compiler/src/kani_middle/resolve.rs | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs index 71e44f6371f8..ef38b1f3adc8 100644 --- a/kani-compiler/src/kani_middle/resolve.rs +++ b/kani-compiler/src/kani_middle/resolve.rs @@ -758,14 +758,16 @@ fn resolve_in_type_def<'tcx>( match refined_candidates.len() { 0 => Err(invalid_path_err(&generic_args, candidates)), 1 => Ok(refined_candidates[0]), - // since is_item_name_with_generic_args looks at the entire item path after the base type, it shouldn't be possible to have more than one match - _ => unreachable!( - "Got multiple refined candidates {:?}", - refined_candidates - .iter() - .map(|def_id| tcx.def_path_str(*def_id)) - .collect::>() - ), + // Item paths differ past the base type, so more than one match + // should not happen — but the comparison is normalization-based, + // so report the ambiguity (with the still-colliding candidates) + // rather than crashing the compiler. + _ => Err(ResolveError::AmbiguousPartialPath { + tcx, + name: name.into(), + base: type_id, + candidates: refined_candidates, + }), } } PathArguments::Parenthesized(args) => {