distinguish recursion limit based overflow for diagnostics
also change the number of allowed fixpoint steps to be fixed instead of using the `log` of the total recursion depth.
This commit is contained in:
parent
d3d145ea1c
commit
5ec9b8d778
25 changed files with 91 additions and 125 deletions
|
@ -36,11 +36,13 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
|
|||
let Goal { param_env, predicate: (lhs, rhs, direction) } = goal;
|
||||
|
||||
let Some(lhs) = self.try_normalize_term(param_env, lhs)? else {
|
||||
return self.evaluate_added_goals_and_make_canonical_response(Certainty::OVERFLOW);
|
||||
return self
|
||||
.evaluate_added_goals_and_make_canonical_response(Certainty::overflow(true));
|
||||
};
|
||||
|
||||
let Some(rhs) = self.try_normalize_term(param_env, rhs)? else {
|
||||
return self.evaluate_added_goals_and_make_canonical_response(Certainty::OVERFLOW);
|
||||
return self
|
||||
.evaluate_added_goals_and_make_canonical_response(Certainty::overflow(true));
|
||||
};
|
||||
|
||||
let variance = match direction {
|
||||
|
|
|
@ -7,6 +7,7 @@ use rustc_infer::infer::{
|
|||
BoundRegionConversionTime, DefineOpaqueTypes, InferCtxt, InferOk, TyCtxtInferExt,
|
||||
};
|
||||
use rustc_infer::traits::query::NoSolution;
|
||||
use rustc_infer::traits::solve::MaybeCause;
|
||||
use rustc_infer::traits::ObligationCause;
|
||||
use rustc_middle::infer::canonical::CanonicalVarInfos;
|
||||
use rustc_middle::infer::unify_key::{ConstVariableOrigin, ConstVariableOriginKind};
|
||||
|
@ -29,7 +30,7 @@ use std::ops::ControlFlow;
|
|||
use crate::traits::vtable::{count_own_vtable_entries, prepare_vtable_segments, VtblSegment};
|
||||
|
||||
use super::inspect::ProofTreeBuilder;
|
||||
use super::{search_graph, GoalEvaluationKind};
|
||||
use super::{search_graph, GoalEvaluationKind, FIXPOINT_STEP_LIMIT};
|
||||
use super::{search_graph::SearchGraph, Goal};
|
||||
use super::{GoalSource, SolverMode};
|
||||
pub use select::InferCtxtSelectExt;
|
||||
|
@ -154,10 +155,6 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
|
|||
self.search_graph.solver_mode()
|
||||
}
|
||||
|
||||
pub(super) fn local_overflow_limit(&self) -> usize {
|
||||
self.search_graph.local_overflow_limit()
|
||||
}
|
||||
|
||||
/// Creates a root evaluation context and search graph. This should only be
|
||||
/// used from outside of any evaluation, and other methods should be preferred
|
||||
/// over using this manually (such as [`InferCtxtEvalExt::evaluate_root_goal`]).
|
||||
|
@ -167,7 +164,7 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
|
|||
f: impl FnOnce(&mut EvalCtxt<'_, 'tcx>) -> R,
|
||||
) -> (R, Option<inspect::GoalEvaluation<'tcx>>) {
|
||||
let mode = if infcx.intercrate { SolverMode::Coherence } else { SolverMode::Normal };
|
||||
let mut search_graph = search_graph::SearchGraph::new(infcx.tcx, mode);
|
||||
let mut search_graph = search_graph::SearchGraph::new(mode);
|
||||
|
||||
let mut ecx = EvalCtxt {
|
||||
search_graph: &mut search_graph,
|
||||
|
@ -388,16 +385,18 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
|
|||
&& source != GoalSource::ImplWhereBound
|
||||
};
|
||||
|
||||
if response.value.certainty == Certainty::OVERFLOW && !keep_overflow_constraints() {
|
||||
(Certainty::OVERFLOW, false)
|
||||
} else {
|
||||
let has_changed = !response.value.var_values.is_identity_modulo_regions()
|
||||
|| !response.value.external_constraints.opaque_types.is_empty();
|
||||
|
||||
let certainty =
|
||||
self.instantiate_and_apply_query_response(param_env, original_values, response);
|
||||
(certainty, has_changed)
|
||||
if let Certainty::Maybe(MaybeCause::Overflow { .. }) = response.value.certainty
|
||||
&& !keep_overflow_constraints()
|
||||
{
|
||||
return (response.value.certainty, false);
|
||||
}
|
||||
|
||||
let has_changed = !response.value.var_values.is_identity_modulo_regions()
|
||||
|| !response.value.external_constraints.opaque_types.is_empty();
|
||||
|
||||
let certainty =
|
||||
self.instantiate_and_apply_query_response(param_env, original_values, response);
|
||||
(certainty, has_changed)
|
||||
}
|
||||
|
||||
fn compute_goal(&mut self, goal: Goal<'tcx, ty::Predicate<'tcx>>) -> QueryResult<'tcx> {
|
||||
|
@ -466,8 +465,8 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
|
|||
let inspect = self.inspect.new_evaluate_added_goals();
|
||||
let inspect = core::mem::replace(&mut self.inspect, inspect);
|
||||
|
||||
let mut response = Ok(Certainty::OVERFLOW);
|
||||
for _ in 0..self.local_overflow_limit() {
|
||||
let mut response = Ok(Certainty::overflow(false));
|
||||
for _ in 0..FIXPOINT_STEP_LIMIT {
|
||||
// FIXME: This match is a bit ugly, it might be nice to change the inspect
|
||||
// stuff to use a closure instead. which should hopefully simplify this a bit.
|
||||
match self.evaluate_added_goals_step() {
|
||||
|
|
|
@ -80,11 +80,14 @@ impl<'tcx> TraitEngine<'tcx> for FulfillmentCtxt<'tcx> {
|
|||
.0
|
||||
{
|
||||
Ok((_, Certainty::Maybe(MaybeCause::Ambiguity))) => {
|
||||
FulfillmentErrorCode::Ambiguity { overflow: false }
|
||||
}
|
||||
Ok((_, Certainty::Maybe(MaybeCause::Overflow))) => {
|
||||
FulfillmentErrorCode::Ambiguity { overflow: true }
|
||||
FulfillmentErrorCode::Ambiguity { overflow: None }
|
||||
}
|
||||
Ok((
|
||||
_,
|
||||
Certainty::Maybe(MaybeCause::Overflow { suggest_increasing_limit }),
|
||||
)) => FulfillmentErrorCode::Ambiguity {
|
||||
overflow: Some(suggest_increasing_limit),
|
||||
},
|
||||
Ok((_, Certainty::Yes)) => {
|
||||
bug!("did not expect successful goal when collecting ambiguity errors")
|
||||
}
|
||||
|
|
|
@ -42,6 +42,17 @@ pub use fulfill::FulfillmentCtxt;
|
|||
pub(crate) use normalize::deeply_normalize_for_diagnostics;
|
||||
pub use normalize::{deeply_normalize, deeply_normalize_with_skipped_universes};
|
||||
|
||||
/// How many fixpoint iterations we should attempt inside of the solver before bailing
|
||||
/// with overflow.
|
||||
///
|
||||
/// We previously used `tcx.recursion_limit().0.checked_ilog2().unwrap_or(0)` for this.
|
||||
/// However, it feels unlikely that uncreasing the recursion limit by a power of two
|
||||
/// to get one more itereation is every useful or desirable. We now instead used a constant
|
||||
/// here. If there ever ends up some use-cases where a bigger number of fixpoint iterations
|
||||
/// is required, we can add a new attribute for that or revert this to be dependant on the
|
||||
/// recursion limit again. However, this feels very unlikely.
|
||||
const FIXPOINT_STEP_LIMIT: usize = 8;
|
||||
|
||||
#[derive(Debug, Clone, Copy)]
|
||||
enum SolverMode {
|
||||
/// Ordinary trait solving, using everywhere except for coherence.
|
||||
|
|
|
@ -1,3 +1,5 @@
|
|||
use crate::solve::FIXPOINT_STEP_LIMIT;
|
||||
|
||||
use super::inspect;
|
||||
use super::inspect::ProofTreeBuilder;
|
||||
use super::SolverMode;
|
||||
|
@ -99,7 +101,6 @@ impl<'tcx> ProvisionalCacheEntry<'tcx> {
|
|||
|
||||
pub(super) struct SearchGraph<'tcx> {
|
||||
mode: SolverMode,
|
||||
local_overflow_limit: usize,
|
||||
/// The stack of goals currently being computed.
|
||||
///
|
||||
/// An element is *deeper* in the stack if its index is *lower*.
|
||||
|
@ -116,10 +117,9 @@ pub(super) struct SearchGraph<'tcx> {
|
|||
}
|
||||
|
||||
impl<'tcx> SearchGraph<'tcx> {
|
||||
pub(super) fn new(tcx: TyCtxt<'tcx>, mode: SolverMode) -> SearchGraph<'tcx> {
|
||||
pub(super) fn new(mode: SolverMode) -> SearchGraph<'tcx> {
|
||||
Self {
|
||||
mode,
|
||||
local_overflow_limit: tcx.recursion_limit().0.checked_ilog2().unwrap_or(0) as usize,
|
||||
stack: Default::default(),
|
||||
provisional_cache: Default::default(),
|
||||
cycle_participants: Default::default(),
|
||||
|
@ -130,10 +130,6 @@ impl<'tcx> SearchGraph<'tcx> {
|
|||
self.mode
|
||||
}
|
||||
|
||||
pub(super) fn local_overflow_limit(&self) -> usize {
|
||||
self.local_overflow_limit
|
||||
}
|
||||
|
||||
/// Update the stack and reached depths on cache hits.
|
||||
#[instrument(level = "debug", skip(self))]
|
||||
fn on_cache_hit(&mut self, additional_depth: usize, encountered_overflow: bool) {
|
||||
|
@ -277,7 +273,7 @@ impl<'tcx> SearchGraph<'tcx> {
|
|||
}
|
||||
|
||||
inspect.goal_evaluation_kind(inspect::WipCanonicalGoalEvaluationKind::Overflow);
|
||||
return Self::response_no_constraints(tcx, input, Certainty::OVERFLOW);
|
||||
return Self::response_no_constraints(tcx, input, Certainty::overflow(true));
|
||||
};
|
||||
|
||||
// Try to fetch the goal from the global cache.
|
||||
|
@ -370,7 +366,7 @@ impl<'tcx> SearchGraph<'tcx> {
|
|||
} else if is_coinductive_cycle {
|
||||
Self::response_no_constraints(tcx, input, Certainty::Yes)
|
||||
} else {
|
||||
Self::response_no_constraints(tcx, input, Certainty::OVERFLOW)
|
||||
Self::response_no_constraints(tcx, input, Certainty::overflow(false))
|
||||
};
|
||||
} else {
|
||||
// No entry, we push this goal on the stack and try to prove it.
|
||||
|
@ -398,7 +394,7 @@ impl<'tcx> SearchGraph<'tcx> {
|
|||
// of this we continuously recompute the cycle until the result
|
||||
// of the previous iteration is equal to the final result, at which
|
||||
// point we are done.
|
||||
for _ in 0..self.local_overflow_limit() {
|
||||
for _ in 0..FIXPOINT_STEP_LIMIT {
|
||||
let result = prove_goal(self, inspect);
|
||||
let stack_entry = self.pop_stack();
|
||||
debug_assert_eq!(stack_entry.input, input);
|
||||
|
@ -431,7 +427,8 @@ impl<'tcx> SearchGraph<'tcx> {
|
|||
} else if stack_entry.has_been_used == HasBeenUsed::COINDUCTIVE_CYCLE {
|
||||
Self::response_no_constraints(tcx, input, Certainty::Yes) == result
|
||||
} else if stack_entry.has_been_used == HasBeenUsed::INDUCTIVE_CYCLE {
|
||||
Self::response_no_constraints(tcx, input, Certainty::OVERFLOW) == result
|
||||
Self::response_no_constraints(tcx, input, Certainty::overflow(false))
|
||||
== result
|
||||
} else {
|
||||
false
|
||||
};
|
||||
|
@ -452,7 +449,7 @@ impl<'tcx> SearchGraph<'tcx> {
|
|||
debug!("canonical cycle overflow");
|
||||
let current_entry = self.pop_stack();
|
||||
debug_assert!(current_entry.has_been_used.is_empty());
|
||||
let result = Self::response_no_constraints(tcx, input, Certainty::OVERFLOW);
|
||||
let result = Self::response_no_constraints(tcx, input, Certainty::overflow(false));
|
||||
(current_entry, result)
|
||||
});
|
||||
|
||||
|
|
|
@ -335,12 +335,16 @@ impl<'tcx> TypeErrCtxt<'_, 'tcx> {
|
|||
);
|
||||
}
|
||||
|
||||
fn report_overflow_no_abort(&self, obligation: PredicateObligation<'tcx>) -> ErrorGuaranteed {
|
||||
fn report_overflow_no_abort(
|
||||
&self,
|
||||
obligation: PredicateObligation<'tcx>,
|
||||
suggest_increasing_limit: bool,
|
||||
) -> ErrorGuaranteed {
|
||||
let obligation = self.resolve_vars_if_possible(obligation);
|
||||
let mut err = self.build_overflow_error(
|
||||
OverflowCause::TraitSolver(obligation.predicate),
|
||||
obligation.cause.span,
|
||||
true,
|
||||
suggest_increasing_limit,
|
||||
);
|
||||
self.note_obligation_cause(&mut err, &obligation);
|
||||
self.point_at_returns_when_relevant(&mut err, &obligation);
|
||||
|
@ -1422,11 +1426,11 @@ impl<'tcx> TypeErrCtxt<'_, 'tcx> {
|
|||
FulfillmentErrorCode::ProjectionError(ref e) => {
|
||||
self.report_projection_error(&error.obligation, e)
|
||||
}
|
||||
FulfillmentErrorCode::Ambiguity { overflow: false } => {
|
||||
FulfillmentErrorCode::Ambiguity { overflow: None } => {
|
||||
self.maybe_report_ambiguity(&error.obligation)
|
||||
}
|
||||
FulfillmentErrorCode::Ambiguity { overflow: true } => {
|
||||
self.report_overflow_no_abort(error.obligation.clone())
|
||||
FulfillmentErrorCode::Ambiguity { overflow: Some(suggest_increasing_limit) } => {
|
||||
self.report_overflow_no_abort(error.obligation.clone(), suggest_increasing_limit)
|
||||
}
|
||||
FulfillmentErrorCode::SubtypeError(ref expected_found, ref err) => self
|
||||
.report_mismatched_types(
|
||||
|
|
|
@ -138,7 +138,7 @@ impl<'tcx> TraitEngine<'tcx> for FulfillmentContext<'tcx> {
|
|||
_infcx: &InferCtxt<'tcx>,
|
||||
) -> Vec<FulfillmentError<'tcx>> {
|
||||
self.predicates
|
||||
.to_errors(FulfillmentErrorCode::Ambiguity { overflow: false })
|
||||
.to_errors(FulfillmentErrorCode::Ambiguity { overflow: None })
|
||||
.into_iter()
|
||||
.map(to_fulfillment_error)
|
||||
.collect()
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue