Verify contracts on methods where the base type has multiple inherent impls

Carolyn Zech · Carolyn Zech · commit 62b66de56499 · 2025-01-13T16:13:33.000-05:00
Add a base_path_args field to the Path struct so that we can use the generic arguments to choose the appropriate implementation
diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs
@@ -24,7 +24,7 @@ use stable_mir::ty::{FnDef, RigidTy, Ty, TyKind};
 use std::collections::HashSet;
 use std::fmt;
 use std::iter::Peekable;
-use syn::{PathSegment, QSelf, TypePath};
+use syn::{PathArguments, PathSegment, QSelf, TypePath};
 use tracing::{debug, debug_span};
 
 mod type_resolution;
@@ -153,7 +153,7 @@ fn resolve_path<'tcx>(
         let next_item = 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, &name)
+                resolve_in_type_def(tcx, base, &path.base_path_args, &name)
             }
             DefKind::Trait => resolve_in_trait(tcx, base, &name),
             kind => {
@@ -246,12 +246,13 @@ impl fmt::Display for ResolveError<'_> {
 /// The segments of a path.
 type Segments = Vec<PathSegment>;
 
-/// A path consisting of a starting point and a bunch of segments. If `base`
+/// A path consisting of a starting point, any PathArguments for that starting point, and a bunch of segments. If `base`
 /// matches `Base::LocalModule { id: _, may_be_external_path : true }`, then
 /// `segments` cannot be empty.
 #[derive(Debug, Hash)]
 struct Path {
     pub base: DefId,
+    pub base_path_args: PathArguments,
     pub segments: Segments,
 }
 
@@ -285,7 +286,11 @@ fn resolve_prefix<'tcx>(
             let next_name = segment.ident.to_string();
             let result = resolve_external(tcx, &next_name);
             if let Some(def_id) = result {
-                Ok(Path { base: def_id, segments: segments.cloned().collect() })
+                Ok(Path {
+                    base: def_id,
+                    base_path_args: segment.arguments.clone(),
+                    segments: segments.cloned().collect(),
+                })
             } else {
                 Err(ResolveError::MissingItem {
                     tcx,
@@ -306,7 +311,11 @@ fn resolve_prefix<'tcx>(
                 None => current_module,
                 Some((hir_id, _)) => hir_id.owner.def_id,
             };
-            Ok(Path { base: crate_root.to_def_id(), segments: segments.cloned().collect() })
+            Ok(Path {
+                base: crate_root.to_def_id(),
+                base_path_args: segment.arguments.clone(),
+                segments: segments.cloned().collect(),
+            })
         }
         // Path starting with "self::"
         (None, Some(segment)) if segment.ident == SELF => {
@@ -334,7 +343,11 @@ fn resolve_prefix<'tcx>(
                         Err(err)
                     }
                 })?;
-            Ok(Path { base: def_id, segments: segments.cloned().collect() })
+            Ok(Path {
+                base: def_id,
+                base_path_args: segment.arguments.clone(),
+                segments: segments.cloned().collect(),
+            })
         }
         _ => {
             unreachable!("Empty path: `{path:?}`")
@@ -364,7 +377,11 @@ where
         }
     }
     debug!("base: {base_module:?}");
-    Ok(Path { base: base_module.to_def_id(), segments: segments.cloned().collect() })
+    Ok(Path {
+        base: base_module.to_def_id(),
+        base_path_args: PathArguments::None,
+        segments: segments.cloned().collect(),
+    })
 }
 
 /// Resolves an external crate name.
@@ -543,14 +560,19 @@ where
     if segments.next().is_some() {
         Err(ResolveError::UnexpectedType { tcx, item: def_id, expected: "module" })
     } else {
-        resolve_in_type_def(tcx, def_id, &name.ident.to_string())
+        resolve_in_type_def(tcx, def_id, &PathArguments::None, &name.ident.to_string())
     }
 }
 
+fn generic_args_to_string<T: ToTokens>(args: &T) -> String {
+    args.to_token_stream().to_string().chars().filter(|c| !c.is_whitespace()).collect::<String>()
+}
+
 /// Resolves a function in a type given its `def_id`.
 fn resolve_in_type_def<'tcx>(
     tcx: TyCtxt<'tcx>,
     type_id: DefId,
+    base_path_args: &PathArguments,
     name: &str,
 ) -> Result<DefId, ResolveError<'tcx>> {
     debug!(?name, ?type_id, "resolve_in_type");
@@ -566,12 +588,57 @@ fn resolve_in_type_def<'tcx>(
     match candidates.len() {
         0 => Err(ResolveError::MissingItem { tcx, base: type_id, unresolved: name.to_string() }),
         1 => Ok(candidates[0]),
-        _ => Err(ResolveError::AmbiguousPartialPath {
-            tcx,
-            name: name.into(),
-            base: type_id,
-            candidates,
-        }),
+        _ => {
+            let invalid_path_err = |generic_args, candidates: Vec<DefId>| -> ResolveError {
+                ResolveError::InvalidPath {
+                    msg: format!(
+                        "the generic arguments {} are invalid. The available implementations are: \n{}",
+                        &generic_args,
+                        &candidates
+                            .iter()
+                            .map(|def_id| tcx.def_path_str(def_id))
+                            .intersperse("\n".to_string())
+                            .collect::<String>()
+                    ),
+                }
+            };
+            // If there are multiple implementations, we need generic arguments on the base type to refine our options.
+            match base_path_args {
+                // If there aren't such arguments, report the ambiguity.
+                PathArguments::None => Err(ResolveError::AmbiguousPartialPath {
+                    tcx,
+                    name: name.into(),
+                    base: type_id,
+                    candidates,
+                }),
+                // Otherwise, use the provided generic arguments to refine our options.
+                PathArguments::AngleBracketed(args) => {
+                    let generic_args = generic_args_to_string(&args);
+                    let refined_candidates: Vec<DefId> = candidates
+                        .iter()
+                        .cloned()
+                        .filter(|item| {
+                            is_item_name_with_generic_args(tcx, *item, &generic_args, name)
+                        })
+                        .collect();
+                    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::<Vec<String>>()
+                        ),
+                    }
+                }
+                PathArguments::Parenthesized(args) => {
+                    Err(invalid_path_err(&generic_args_to_string(args), candidates))
+                }
+            }
+        }
     }
 }
 
@@ -625,7 +692,11 @@ where
                 base: ty,
                 unresolved: name.to_string(),
             })?;
-        Ok(Path { base: item, segments: segments.cloned().collect() })
+        Ok(Path {
+            base: item,
+            base_path_args: PathArguments::None,
+            segments: segments.cloned().collect(),
+        })
     } else {
         Err(ResolveError::InvalidPath { msg: format!("Unexpected primitive type `{ty}`") })
     }
@@ -636,3 +707,14 @@ fn is_item_name(tcx: TyCtxt, item: DefId, name: &str) -> bool {
     let last = item_path.split("::").last().unwrap();
     last == name
 }
+
+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)
+}
diff --git a/tests/kani/FunctionContracts/multiple_inherent_impls.rs b/tests/kani/FunctionContracts/multiple_inherent_impls.rs
@@ -0,0 +1,28 @@
+// 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 inherent impls,
+// c.f. https://github.com/model-checking/kani/issues/3773
+
+struct NonZero<T>(T);
+
+impl NonZero<u32> {
+    #[kani::requires(self.0.checked_mul(x).is_some())]
+    fn unchecked_mul(self, x: u32) -> u32 {
+        self.0 * x
+    }
+}
+
+impl NonZero<i32> {
+    #[kani::requires(self.0.checked_mul(x).is_some())]
+    fn unchecked_mul(self, x: i32) -> i32 {
+        self.0 * x
+    }
+}
+
+#[kani::proof_for_contract(NonZero::<i32>::unchecked_mul)]
+fn verify_unchecked_mul_ambiguous_path() {
+    let x: NonZero<i32> = NonZero(-1);
+    x.unchecked_mul(-2);
+}
diff --git a/tests/ui/function-contracts/incorrect_target_path.expected b/tests/ui/function-contracts/incorrect_target_path.expected
@@ -0,0 +1,15 @@
+Failed to resolve checking function NonZero::<g32>::unchecked_mul because the generic arguments ::<g32> are invalid. The available implementations are: 
+       NonZero::<u32>::unchecked_mul
+       NonZero::<i32>::unchecked_mul
+ |
+ | #[kani::proof_for_contract(NonZero::<g32>::unchecked_mul)]
+ | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+Failed to resolve checking function NonZero::unchecked_mul because there are multiple implementations of unchecked_mul in struct `NonZero`. Found:
+       NonZero::<u32>::unchecked_mul
+       NonZero::<i32>::unchecked_mul
+ |
+ | #[kani::proof_for_contract(NonZero::unchecked_mul)]
+ | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ |
+   = help: Replace NonZero::unchecked_mul with a specific implementation.
diff --git a/tests/ui/function-contracts/invalid_target_path.rs b/tests/ui/function-contracts/invalid_target_path.rs
@@ -0,0 +1,37 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+// Test that Kani errors if the target of the proof_for_contract is missing a generic argument that's required to disambiguate between multiple implementations
+// or if the generic argument is invalid.
+// c.f. https://github.com/model-checking/kani/issues/3773
+
+struct NonZero<T>(T);
+
+impl NonZero<u32> {
+    #[kani::requires(self.0.checked_mul(x).is_some())]
+    fn unchecked_mul(self, x: u32) -> u32 {
+        self.0 * x
+    }
+}
+
+impl NonZero<i32> {
+    #[kani::requires(self.0.checked_mul(x).is_some())]
+    fn unchecked_mul(self, x: i32) -> i32 {
+        self.0 * x
+    }
+}
+
+// Errors because there is more than one unchecked_mul implementation
+#[kani::proof_for_contract(NonZero::unchecked_mul)]
+fn verify_unchecked_mul_ambiguous_path() {
+    let x: NonZero<i32> = NonZero(-1);
+    x.unchecked_mul(-2);
+}
+
+// Errors because the g32 implementation doesn't exist
+#[kani::proof_for_contract(NonZero::<g32>::unchecked_mul)]
+fn verify_unchecked_mul_invalid_impl() {
+    let x: NonZero<i32> = NonZero(-1);
+    NonZero::<i32>::unchecked_mul(x, -2);
+}
diff --git a/tests/ui/stubbing/invalid-path/invalid_inherent_impls.expected b/tests/ui/stubbing/invalid-path/invalid_inherent_impls.expected
@@ -0,0 +1,18 @@
+error: Failed to resolve replacement function NonZero::unchecked_mul: there are multiple implementations of unchecked_mul in struct `NonZero`. Found:
+       NonZero::<u32>::unchecked_mul
+       NonZero::<i32>::unchecked_mul
+invalid_inherent_impls.rs
+   |
+   | #[kani::stub_verified(NonZero::unchecked_mul)]
+   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   |
+   = help: Replace NonZero::unchecked_mul with a specific implementation.
+
+error: Failed to resolve replacement function NonZero::<g32>::unchecked_mul: the generic arguments ::<g32> are invalid. The available implementations are: 
+       NonZero::<u32>::unchecked_mul
+       NonZero::<i32>::unchecked_mul
+invalid_inherent_impls.rs
+   |
+   | #[kani::stub_verified(NonZero::<g32>::unchecked_mul)]
+   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   |
diff --git a/tests/ui/stubbing/invalid-path/invalid_inherent_impls.rs b/tests/ui/stubbing/invalid-path/invalid_inherent_impls.rs
@@ -0,0 +1,40 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: --harness invalid_stub -Z stubbing
+
+// Test that Kani errors if the stub is missing a generic argument that's required to disambiguate between multiple implementations
+// or if the generic argument is invalid.
+// c.f. https://github.com/model-checking/kani/issues/3773
+
+struct NonZero<T>(T);
+
+impl NonZero<u32> {
+    #[kani::requires(self.0.checked_mul(x).is_some())]
+    fn unchecked_mul(self, x: u32) -> u32 {
+        self.0 * x
+    }
+}
+
+impl NonZero<i32> {
+    #[kani::requires(self.0.checked_mul(x).is_some())]
+    fn unchecked_mul(self, x: i32) -> i32 {
+        self.0 * x
+    }
+}
+
+// Errors because there is more than one unchecked_mul implementation
+#[kani::stub_verified(NonZero::unchecked_mul)]
+#[kani::proof]
+fn verify_unchecked_mul_ambiguous_path() {
+    let x: NonZero<i32> = NonZero(-1);
+    x.unchecked_mul(-2);
+}
+
+// Errors because the g32 implementation doesn't exist
+#[kani::stub_verified(NonZero::<g32>::unchecked_mul)]
+#[kani::proof]
+fn verify_unchecked_mul_invalid_impl() {
+    let x: NonZero<i32> = NonZero(-1);
+    NonZero::<i32>::unchecked_mul(x, -2);
+}
diff --git a/tests/ui/stubbing/invalid-path/invalid_mod.expected b/tests/ui/stubbing/invalid-path/invalid_mod.expected
@@ -1,4 +1,4 @@
 error: failed to resolve `crate::mod_a::method_a::invalid`: expected module, found function `mod_a::method_a`\
-invalid.rs:\
+invalid_mod.rs:\
 |\
 |     #[cfg_attr(kani, kani::stub(crate::mod_a::method_a::invalid, noop))]\
diff --git a/tests/ui/stubbing/invalid-path/invalid_mod.rs b/tests/ui/stubbing/invalid-path/invalid_mod.rs
