Contracts/Stubs for multiple inherent impls: fix checking the generic args path for equality

kani-compiler/src/kani_middle/resolve.rs

@@ -708,13 +708,63 @@ fn is_item_name(tcx: TyCtxt, item: DefId, name: &str) -> bool {
     last == name
 }
 
+/// Use this when we don't just care about the item name matching (c.f. is_item_name),
+/// but also if the generic arguments are the same, e.g. <u32>::unchecked_add.
 fn is_item_name_with_generic_args(
     tcx: TyCtxt,
     item: DefId,
     generic_args: &str,
     name: &str,
 ) -> bool {
     let item_path = tcx.def_path_str(item);
-    let all_but_base_type = item_path.find("::").map_or("", |idx| &item_path[idx..]);
-    all_but_base_type == format!("{generic_args}::{name}")
+    last_two_items_of_path_match(&item_path, generic_args, name)
+}
+
+// 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();
+
+    if parts.len() < 2 {
+        return false;
+    }
+
+    let actual_last_two =
+        format!("{}{}{}{}", "::", parts[parts.len() - 2], "::", parts[parts.len() - 1]);
+
+    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
+}
+
+#[cfg(test)]
+mod tests {
+    mod simple_last_two_items_of_path_match {
+        use crate::kani_middle::resolve::last_two_items_of_path_match;
+
+        #[test]
+        fn length_one_item_prefix() {
+            let generic_args = "::<u32>";
+            let name = "unchecked_add";
+            let item_path = format!("NonZero{}::{}", generic_args, name);
+            assert!(last_two_items_of_path_match(&item_path, generic_args, name))
+        }
+
+        #[test]
+        fn length_three_item_prefix() {
+            let generic_args = "::<u32>";
+            let name = "unchecked_add";
+            let item_path = format!("core::num::NonZero{}::{}", generic_args, name);
+            assert!(last_two_items_of_path_match(&item_path, generic_args, name))
+        }
+
+        #[test]
+        fn wrong_generic_arg() {
+            let generic_args = "::<u64>";
+            let name = "unchecked_add";
+            let item_path = format!("core::num::NonZero{}::{}", "::<u32>", name);
+            assert!(!last_two_items_of_path_match(&item_path, generic_args, name))
+        }
+    }
 }

tests/kani/FunctionContracts/multiple_inherent_impls.rs

@@ -26,3 +26,37 @@ fn verify_unchecked_mul_ambiguous_path() {
     let x: NonZero<i32> = NonZero(-1);
     x.unchecked_mul(-2);
 }
+
+// Test that the resolution still works if the function in question is nested inside multiple modules,
+// i.e. the absolute path to the function can be arbitrarily long.
+// As long as the generic arguments and function name match, resolution should succeed.
+// This mimics the actual structure of NonZero relative to its harnesses in the standard library.
+pub mod num {
+    pub mod negative {
+        pub struct NegativeNumber<T>(pub T);
+
+        impl NegativeNumber<i32> {
+            #[kani::requires(self.0.checked_mul(x).is_some())]
+            pub fn unchecked_mul(self, x: i32) -> i32 {
+                self.0 * x
+            }
+        }
+
+        impl NegativeNumber<i16> {
+            #[kani::requires(self.0.checked_mul(x).is_some())]
+            pub fn unchecked_mul(self, x: i16) -> i16 {
+                self.0 * x
+            }
+        }
+    }
+}
+
+mod verify {
+    use crate::num::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);
+    }
+}