fix: Make kani attribute nameres work with generic args having ::

kani-compiler/src/kani_middle/resolve.rs

@@ -125,21 +125,25 @@ fn resolve_path<'tcx>(
 ) -> Result<DefId, ResolveError<'tcx>> {
     debug!(?path, "resolve_path");
     let path = resolve_prefix(tcx, current_module, path)?;
-    path.segments.into_iter().try_fold(path.base, |base, segment| {
-        let name = segment.ident.to_string();
-        let def_kind = tcx.def_kind(base);
-        match def_kind {
-            DefKind::ForeignMod | DefKind::Mod => resolve_in_module(tcx, base, &name),
-            DefKind::Struct | DefKind::Enum | DefKind::Union => {
-                resolve_in_type_def(tcx, base, &path.base_path_args, &name)
-            }
-            DefKind::Trait => resolve_in_trait_def(tcx, base, &name),
-            kind => {
-                debug!(?base, ?kind, "resolve_path: unexpected item");
-                Err(ResolveError::UnexpectedType { tcx, item: base, expected: "module" })
-            }
-        }
-    })
+    path.segments
+        .into_iter()
+        .try_fold((path.base, path.base_path_args.clone()), |(base, base_path_args), segment| {
+            let name = segment.ident.to_string();
+            let def_kind = tcx.def_kind(base);
+            let base = match def_kind {
+                DefKind::ForeignMod | DefKind::Mod => resolve_in_module(tcx, base, &name),
+                DefKind::Struct | DefKind::Enum | DefKind::Union => {
+                    resolve_in_type_def(tcx, base, &base_path_args, &name)
+                }
+                DefKind::Trait => resolve_in_trait_def(tcx, base, &name),
+                kind => {
+                    debug!(?base, ?kind, "resolve_path: unexpected item");
+                    Err(ResolveError::UnexpectedType { tcx, item: base, expected: "module" })
+                }
+            };
+            base.map(|base| (base, segment.arguments))
+        })
+        .map(|it| it.0)
 }
 
 /// Provide information about where the resolution failed.
@@ -781,7 +785,31 @@ fn is_item_name_with_generic_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 {
-    let parts: Vec<&str> = item_path.split("::").collect();
+    let mut angle_bracket_depth = 0;
+    let mut parts = Vec::new();
+    let mut part_start = 0;
+
+    for (i, c) in item_path.char_indices() {
+        match c {
+            '<' => {
+                angle_bracket_depth += 1;
+            }
+            '>' => {
+                angle_bracket_depth -= 1;
+            }
+            ':' if angle_bracket_depth == 0
+                && i > 0
+                && item_path.chars().nth(i - 1) == Some(':') =>
+            {
+                if part_start < i {
+                    parts.push(&item_path[part_start..i - 1]);
+                }
+                part_start = i + 1;
+            }
+            _ => {}
+        }
+    }
+    parts.push(&item_path[part_start..]);
 
     if parts.len() < 2 {
         return false;
@@ -793,7 +821,7 @@ 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 == actual_last_two
+    last_two.chars().eq(actual_last_two.chars().filter(|c| !c.is_whitespace()))
 }
 
 #[cfg(test)]
@@ -824,5 +852,13 @@ mod tests {
             let item_path = format!("core::num::NonZero{}::{}", "::<u32>", name);
             assert!(!last_two_items_of_path_match(&item_path, generic_args, name))
         }
+
+        #[test]
+        fn generic_args_with_segmented_params() {
+            let generic_args = "::<core::mem::MaybeUninit<T>,A>";
+            let name = "assume_init";
+            let item_path = format!("rc::Rc{}::{}", "::<core::mem::MaybeUninit<T>, A>", name);
+            assert!(last_two_items_of_path_match(&item_path, generic_args, name))
+        }
     }
 }

tests/kani/FunctionContracts/multiple_inherent_impls.rs

@@ -49,14 +49,47 @@ pub mod num {
             }
         }
     }
+
+    pub mod even {
+        pub struct EvenNumber<T>(pub T);
+
+        impl EvenNumber<i32> {
+            #[kani::requires(self.0.checked_mul(x).is_some())]
+            pub fn unchecked_mul(self, x: i32) -> i32 {
+                self.0 * x
+            }
+        }
+    }
+
+    pub struct AnyNumber<T>(pub T);
+
+    impl AnyNumber<negative::NegativeNumber<i32>> {
+        #[kani::requires(self.0.0.checked_mul(x).is_some())]
+        pub fn unchecked_mul(self, x: i32) -> i32 {
+            self.0.0 * x
+        }
+    }
+
+    impl AnyNumber<even::EvenNumber<i32>> {
+        #[kani::requires(self.0.0.checked_mul(x).is_some())]
+        pub fn unchecked_mul(self, x: i32) -> i32 {
+            self.0.0 * x
+        }
+    }
 }
 
 mod verify {
-    use crate::num::negative::*;
+    use crate::num::{AnyNumber, even::*, negative::*};
 
     #[kani::proof_for_contract(NegativeNumber::<i32>::unchecked_mul)]
     fn verify_unchecked_mul_ambiguous_path() {
         let x: NegativeNumber<i32> = NegativeNumber(-1);
         x.unchecked_mul(-2);
     }
+
+    #[kani::proof_for_contract(AnyNumber::<num::even::EvenNumber<i32>>::unchecked_mul)]
+    fn verify_unchecked_mul_resolution_with_segmented_args() {
+        let x: AnyNumber<EvenNumber<i32>> = AnyNumber(EvenNumber(2));
+        x.unchecked_mul(3);
+    }
 }