Verify contracts/stubs for generic types with multiple inherent implementations

kani-compiler/src/kani_middle/attributes.rs

@@ -213,13 +213,20 @@ impl<'tcx> KaniAttributes<'tcx> {
                 let def = self
                     .resolve_from_mod(name.as_str())
                     .map_err(|e| {
-                        self.tcx.dcx().span_err(
+                        let mut err = self.tcx.dcx().struct_span_err(
                             attr.span,
                             format!(
                                 "Failed to resolve replacement function {}: {e}",
                                 name.as_str()
                             ),
-                        )
+                        );
+                        if let ResolveError::AmbiguousPartialPath { .. } = e {
+                            err = err.with_help(format!(
+                                "Replace {} with a specific implementation.",
+                                name.as_str()
+                            ));
+                        }
+                        err.emit();
                     })
                     .ok()?;
                 Some((name, def, attr.span))
@@ -242,13 +249,20 @@ impl<'tcx> KaniAttributes<'tcx> {
             self.resolve_from_mod(name.as_str())
                 .map(|ok| (name, ok, target.span))
                 .map_err(|resolve_err| {
-                    self.tcx.dcx().span_err(
+                    let mut err = self.tcx.dcx().struct_span_err(
                         target.span,
                         format!(
                             "Failed to resolve checking function {} because {resolve_err}",
                             name.as_str()
                         ),
-                    )
+                    );
+                    if let ResolveError::AmbiguousPartialPath { .. } = resolve_err {
+                        err = err.with_help(format!(
+                            "Replace {} with a specific implementation.",
+                            name.as_str()
+                        ));
+                    }
+                    err.emit();
                 })
                 .ok()
         })

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 => {
@@ -170,6 +170,8 @@ fn resolve_path<'tcx>(
 pub enum ResolveError<'tcx> {
     /// Ambiguous glob resolution.
     AmbiguousGlob { tcx: TyCtxt<'tcx>, name: String, base: DefId, candidates: Vec<DefId> },
+    /// Ambiguous partial path (multiple inherent impls, c.f. https://github.com/model-checking/kani/issues/3773)
+    AmbiguousPartialPath { tcx: TyCtxt<'tcx>, name: String, base: DefId, candidates: Vec<DefId> },
     /// Use super past the root of a crate.
     ExtraSuper,
     /// Invalid path.
@@ -208,6 +210,18 @@ impl fmt::Display for ResolveError<'_> {
                         .collect::<String>()
                 )
             }
+            ResolveError::AmbiguousPartialPath { tcx, base, name, candidates } => {
+                let location = description(*tcx, *base);
+                write!(
+                    f,
+                    "there are multiple implementations of {name} in {location}. Found:\n{}",
+                    candidates
+                        .iter()
+                        .map(|def_id| tcx.def_path_str(*def_id))
+                        .intersperse("\n".to_string())
+                        .collect::<String>()
+                )
+            }
             ResolveError::InvalidPath { msg } => write!(f, "{msg}"),
             ResolveError::UnexpectedType { tcx, item: def_id, expected } => write!(
                 f,
@@ -232,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,
 }
 
@@ -271,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,
@@ -292,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 => {
@@ -320,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:?}`")
@@ -350,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.
@@ -529,26 +560,86 @@ 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");
-    let missing_item_err =
-        || ResolveError::MissingItem { tcx, base: type_id, unresolved: name.to_string() };
     // Try the inherent `impl` blocks (i.e., non-trait `impl`s).
-    tcx.inherent_impls(type_id)
+    let candidates: Vec<DefId> = tcx
+        .inherent_impls(type_id)
         .iter()
         .flat_map(|impl_id| tcx.associated_item_def_ids(impl_id))
         .cloned()
-        .find(|item| is_item_name(tcx, *item, name))
-        .ok_or_else(missing_item_err)
+        .filter(|item| is_item_name(tcx, *item, name))
+        .collect();
+
+    match candidates.len() {
+        0 => Err(ResolveError::MissingItem { tcx, base: type_id, unresolved: name.to_string() }),
+        1 => Ok(candidates[0]),
+        _ => {
+            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))
+                }
+            }
+        }
+    }
 }
 
 /// Resolves a function in a trait.
@@ -601,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}`") })
     }
@@ -612,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)
+}

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

tests/ui/function-contracts/invalid_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.

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

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)]
+   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   |