Contracts/Stubs for multiple inherent impls: fix checking the generic args path for equality (#4051)

#3829 fixed an issue where we couldn't verify contracts or stubs for
types with multiple inherent impls. However, the logic to check for path
equality incorrectly assumed that there would only be one element in the
path before the generic argument, when in fact the path can be
arbitrarily long if there are modules involved. Change the logic to just
look at the last two elements, since we can expect those will be the
generic argument and the method name.

Before this PR, the new test would fail with this error:

```
error: Failed to resolve checking function NegativeNumber::<i32>::unchecked_mul because the generic arguments ::<i32> are invalid. The available implementations are: 
       num::negative::NegativeNumber::<i32>::unchecked_mul
       num::negative::NegativeNumber::<i16>::unchecked_mul
  --> /Users/cmzech/kani/tests/kani/FunctionContracts/multiple_inherent_impls.rs:57:5
   |
57 |     #[kani::proof_for_contract(NegativeNumber::<i32>::unchecked_mul)]
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   |
   = note: this error originates in the attribute macro `kani::proof_for_contract` (in Nightly builds, run with -Z macro-backtrace for more info)
```

because we'd try to compare
`::negative::NegativeNumber::<i32>::unchecked_mul` to
`::<i32>::unchecked_mul` and find they weren't equal.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: Carolyn Zech

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);
+    }
+}