diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 5ac0344c9fbd..66cebf9c8f6f 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -13,6 +13,7 @@ //! - For every static, collect initializer and drop functions. //! //! We have kept this module agnostic of any Kani code in case we can contribute this back to rustc. +use rustc_span::ErrorGuaranteed; use tracing::{debug, debug_span, trace, warn}; use rustc_data_structures::fingerprint::Fingerprint; @@ -26,6 +27,7 @@ use rustc_middle::mir::mono::MonoItem; use rustc_middle::mir::visit::Visitor as MirVisitor; use rustc_middle::mir::{ Body, CastKind, Constant, ConstantKind, Location, Rvalue, Terminator, TerminatorKind, + UnevaluatedConst, }; use rustc_middle::span_bug; use rustc_middle::ty::adjustment::PointerCoercion; @@ -458,7 +460,23 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> { // The `monomorphize` call should have evaluated that constant already. Ok(const_val) => const_val, Err(ErrorHandled::TooGeneric(span)) => { - span_bug!(span, "Unexpected polymorphic constant: {:?}", literal) + if graceful_const_resolution_err( + self.tcx, + &un_eval, + span, + self.instance.def_id(), + ) + .is_some() + { + return; + } else { + span_bug!( + span, + "Unexpected polymorphic constant: {:?} {:?}", + literal, + constant.literal + ) + } } Err(error) => { warn!(?error, "Error already reported"); @@ -494,6 +512,12 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> { // implement the same traits as those in the // original function/method. A trait mismatch shows // up here, when we try to resolve a trait method + + // FIXME: This assumes the type resolving the + // trait is the first argument, but that isn't + // necessarily true. It could be any argument or + // even the return type, for instance for a + // trait like `FromIterator`. let generic_ty = outer_args[0].ty(self.body, tcx).peel_refs(); let receiver_ty = tcx.subst_and_normalize_erasing_regions( substs, @@ -508,7 +532,7 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> { "`{receiver_ty}` doesn't implement \ `{trait_}`. The function `{caller}` \ cannot be stubbed by `{}` due to \ - generic bounds not being met.", + generic bounds not being met. Callee: {callee}", tcx.def_path_str(stub) ), ); @@ -555,6 +579,36 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> { } } +/// Try to construct a nice error message when const evaluation fails. +/// +/// This function handles the `Trt::CNST` case where there is one trait (`Trt`) +/// which defined a constant `CNST` that we failed to resolve. As such we expect +/// that the trait can be resolved from the constant and that only one generic +/// parameter, the instantiation of `Trt`, is present. +/// +/// If these expectations are not met we return `None`. We do not know in what +/// situation that would be the case and if they are even possible. +fn graceful_const_resolution_err<'tcx>( + tcx: TyCtxt<'tcx>, + mono_const: &UnevaluatedConst<'tcx>, + span: rustc_span::Span, + parent_fn: DefId, +) -> Option { + let implementor = match mono_const.args.as_slice() { + [one] => one.as_type(), + _ => None, + }?; + let trait_ = tcx.trait_of_item(mono_const.def)?; + let msg = format!( + "Type `{implementor}` does not implement trait `{}`. \ + This is likely because `{}` is used as a stub but its \ + generic bounds are not being met.", + tcx.def_path_str(trait_), + tcx.def_path_str(parent_fn) + ); + Some(tcx.sess.span_err(span, msg)) +} + /// Convert a `MonoItem` into a stable `Fingerprint` which can be used as a stable hash across /// compilation sessions. This allow us to provide a stable deterministic order to codegen. fn to_fingerprint(tcx: TyCtxt, item: &MonoItem) -> Fingerprint { diff --git a/tests/expected/issue-2589/issue_2589.expected b/tests/expected/issue-2589/issue_2589.expected new file mode 100644 index 000000000000..0352a8933b6d --- /dev/null +++ b/tests/expected/issue-2589/issue_2589.expected @@ -0,0 +1 @@ +error: Type `std::string::String` does not implement trait `Dummy`. This is likely because `original` is used as a stub but its generic bounds are not being met. diff --git a/tests/expected/issue-2589/issue_2589.rs b/tests/expected/issue-2589/issue_2589.rs new file mode 100644 index 000000000000..a9442091c1e3 --- /dev/null +++ b/tests/expected/issue-2589/issue_2589.rs @@ -0,0 +1,21 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// kani-flags: -Z stubbing + +fn original() {} + +trait Dummy { + const TRUE: bool = true; +} + +fn stub() { + // Do nothing. + assert!(T::TRUE); +} + +#[kani::proof] +#[kani::stub(original, stub)] +fn check_mismatch() { + original::(); +}