Skip to content

Commit

Permalink
Fix issue 2589 (#2787)
Browse files Browse the repository at this point in the history
Co-authored-by: Felipe R. Monteiro <[email protected]>
  • Loading branch information
JustusAdam and feliperodri authored Sep 25, 2023
1 parent c7c0f18 commit e95a7bb
Show file tree
Hide file tree
Showing 3 changed files with 78 additions and 2 deletions.
58 changes: 56 additions & 2 deletions kani-compiler/src/kani_middle/reachability.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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;
Expand Down Expand Up @@ -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");
Expand Down Expand Up @@ -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,
Expand All @@ -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)
),
);
Expand Down Expand Up @@ -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<ErrorGuaranteed> {
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 {
Expand Down
1 change: 1 addition & 0 deletions tests/expected/issue-2589/issue_2589.expected
Original file line number Diff line number Diff line change
@@ -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.
21 changes: 21 additions & 0 deletions tests/expected/issue-2589/issue_2589.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
//
// kani-flags: -Z stubbing

fn original<T>() {}

trait Dummy {
const TRUE: bool = true;
}

fn stub<T: Dummy>() {
// Do nothing.
assert!(T::TRUE);
}

#[kani::proof]
#[kani::stub(original, stub)]
fn check_mismatch() {
original::<String>();
}

0 comments on commit e95a7bb

Please sign in to comment.