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/2] 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/2] 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(); + } }