diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index a186c3fb5d23..6d366f432e2a 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/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() }) diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs index bf2102208e6e..cd1b72c6dc66 100644 --- 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 => { @@ -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 }, + /// 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 }, /// Use super past the root of a crate. ExtraSuper, /// Invalid path. @@ -208,6 +210,18 @@ impl fmt::Display for ResolveError<'_> { .collect::() ) } + 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::() + ) + } 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; -/// 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(args: &T) -> String { + args.to_token_stream().to_string().chars().filter(|c| !c.is_whitespace()).collect::() +} + /// 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> { 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 = 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| -> 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::() + ), + } + }; + // 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 = 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::>() + ), + } + } + 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) +} diff --git a/tests/kani/FunctionContracts/multiple_inherent_impls.rs b/tests/kani/FunctionContracts/multiple_inherent_impls.rs new file mode 100644 index 000000000000..cdd25337cd36 --- /dev/null +++ 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); + +impl NonZero { + #[kani::requires(self.0.checked_mul(x).is_some())] + fn unchecked_mul(self, x: u32) -> u32 { + self.0 * x + } +} + +impl NonZero { + #[kani::requires(self.0.checked_mul(x).is_some())] + fn unchecked_mul(self, x: i32) -> i32 { + self.0 * x + } +} + +#[kani::proof_for_contract(NonZero::::unchecked_mul)] +fn verify_unchecked_mul_ambiguous_path() { + let x: NonZero = NonZero(-1); + x.unchecked_mul(-2); +} diff --git a/tests/ui/function-contracts/invalid_target_path.expected b/tests/ui/function-contracts/invalid_target_path.expected new file mode 100644 index 000000000000..bdf28539002c --- /dev/null +++ b/tests/ui/function-contracts/invalid_target_path.expected @@ -0,0 +1,15 @@ +Failed to resolve checking function NonZero::::unchecked_mul because the generic arguments :: are invalid. The available implementations are: + NonZero::::unchecked_mul + NonZero::::unchecked_mul + | + | #[kani::proof_for_contract(NonZero::::unchecked_mul)] + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +Failed to resolve checking function NonZero::unchecked_mul because there are multiple implementations of unchecked_mul in struct `NonZero`. Found: + NonZero::::unchecked_mul + NonZero::::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 new file mode 100644 index 000000000000..20850b148d14 --- /dev/null +++ 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); + +impl NonZero { + #[kani::requires(self.0.checked_mul(x).is_some())] + fn unchecked_mul(self, x: u32) -> u32 { + self.0 * x + } +} + +impl NonZero { + #[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 = NonZero(-1); + x.unchecked_mul(-2); +} + +// Errors because the g32 implementation doesn't exist +#[kani::proof_for_contract(NonZero::::unchecked_mul)] +fn verify_unchecked_mul_invalid_impl() { + let x: NonZero = NonZero(-1); + NonZero::::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 new file mode 100644 index 000000000000..f050072530f7 --- /dev/null +++ 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::::unchecked_mul + NonZero::::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::::unchecked_mul: the generic arguments :: are invalid. The available implementations are: + NonZero::::unchecked_mul + NonZero::::unchecked_mul +invalid_inherent_impls.rs + | + | #[kani::stub_verified(NonZero::::unchecked_mul)] + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + | diff --git a/tests/ui/stubbing/invalid-path/invalid_inherent_impls.rs b/tests/ui/stubbing/invalid-path/invalid_inherent_impls.rs new file mode 100644 index 000000000000..f41745a2f26d --- /dev/null +++ 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); + +impl NonZero { + #[kani::requires(self.0.checked_mul(x).is_some())] + fn unchecked_mul(self, x: u32) -> u32 { + self.0 * x + } +} + +impl NonZero { + #[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 = NonZero(-1); + x.unchecked_mul(-2); +} + +// Errors because the g32 implementation doesn't exist +#[kani::stub_verified(NonZero::::unchecked_mul)] +#[kani::proof] +fn verify_unchecked_mul_invalid_impl() { + let x: NonZero = NonZero(-1); + NonZero::::unchecked_mul(x, -2); +} diff --git a/tests/ui/stubbing/invalid-path/expected b/tests/ui/stubbing/invalid-path/invalid_mod.expected similarity index 91% rename from tests/ui/stubbing/invalid-path/expected rename to tests/ui/stubbing/invalid-path/invalid_mod.expected index 5584cde0871b..f64b7d305fc4 100644 --- a/tests/ui/stubbing/invalid-path/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.rs b/tests/ui/stubbing/invalid-path/invalid_mod.rs similarity index 100% rename from tests/ui/stubbing/invalid-path/invalid.rs rename to tests/ui/stubbing/invalid-path/invalid_mod.rs