1
Fork 0

assert that solver results are stable

This commit is contained in:
lcnr 2023-01-27 10:01:16 +01:00
parent 9c3fe58917
commit 85e6f38e79
3 changed files with 46 additions and 8 deletions

View file

@ -174,6 +174,7 @@ impl<'tcx> InferCtxtEvalExt<'tcx> for InferCtxt<'tcx> {
search_graph: &mut search_graph, search_graph: &mut search_graph,
infcx: self, infcx: self,
var_values: CanonicalVarValues::dummy(), var_values: CanonicalVarValues::dummy(),
in_projection_eq_hack: false,
} }
.evaluate_goal(goal); .evaluate_goal(goal);
@ -187,6 +188,10 @@ struct EvalCtxt<'a, 'tcx> {
var_values: CanonicalVarValues<'tcx>, var_values: CanonicalVarValues<'tcx>,
search_graph: &'a mut search_graph::SearchGraph<'tcx>, search_graph: &'a mut search_graph::SearchGraph<'tcx>,
/// This field is used by a debug assertion in [`EvalCtxt::evaluate_goal`],
/// see the comment in that method for more details.
in_projection_eq_hack: bool,
} }
impl<'a, 'tcx> EvalCtxt<'a, 'tcx> { impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
@ -213,7 +218,8 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
loop { loop {
let (ref infcx, goal, var_values) = let (ref infcx, goal, var_values) =
tcx.infer_ctxt().build_with_canonical(DUMMY_SP, &canonical_goal); tcx.infer_ctxt().build_with_canonical(DUMMY_SP, &canonical_goal);
let mut ecx = EvalCtxt { infcx, var_values, search_graph }; let mut ecx =
EvalCtxt { infcx, var_values, search_graph, in_projection_eq_hack: false };
let result = ecx.compute_goal(goal); let result = ecx.compute_goal(goal);
// FIXME: `Response` should be `Copy` // FIXME: `Response` should be `Copy`
@ -243,10 +249,28 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
let canonical_goal = self.infcx.canonicalize_query(goal, &mut orig_values); let canonical_goal = self.infcx.canonicalize_query(goal, &mut orig_values);
let canonical_response = let canonical_response =
EvalCtxt::evaluate_canonical_goal(self.tcx(), self.search_graph, canonical_goal)?; EvalCtxt::evaluate_canonical_goal(self.tcx(), self.search_graph, canonical_goal)?;
Ok((
!canonical_response.value.var_values.is_identity(), let has_changed = !canonical_response.value.var_values.is_identity();
instantiate_canonical_query_response(self.infcx, &orig_values, canonical_response), let certainty =
)) instantiate_canonical_query_response(self.infcx, &orig_values, canonical_response);
// Check that rerunning this query with its inference constraints applied
// doesn't result in new inference constraints and has the same result.
//
// If we have projection goals like `<T as Trait>::Assoc == u32` we recursively
// call `exists<U> <T as Trait>::Assoc == U` to enable better caching. This goal
// could constrain `U` to `u32` which would cause this check to result in a
// solver cycle.
if cfg!(debug_assertions) && has_changed && !self.in_projection_eq_hack {
let mut orig_values = OriginalQueryValues::default();
let canonical_goal = self.infcx.canonicalize_query(goal, &mut orig_values);
let canonical_response =
EvalCtxt::evaluate_canonical_goal(self.tcx(), self.search_graph, canonical_goal)?;
assert!(canonical_response.value.var_values.is_identity());
assert_eq!(certainty, canonical_response.value.certainty);
}
Ok((has_changed, certainty))
} }
fn compute_goal(&mut self, goal: Goal<'tcx, ty::Predicate<'tcx>>) -> QueryResult<'tcx> { fn compute_goal(&mut self, goal: Goal<'tcx, ty::Predicate<'tcx>>) -> QueryResult<'tcx> {

View file

@ -45,8 +45,9 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
projection_ty: goal.predicate.projection_ty, projection_ty: goal.predicate.projection_ty,
term: unconstrained_rhs, term: unconstrained_rhs,
}); });
let (_has_changed, normalize_certainty) = let (_has_changed, normalize_certainty) = self.in_projection_eq_hack(|this| {
self.evaluate_goal(goal.with(self.tcx(), unconstrained_predicate))?; this.evaluate_goal(goal.with(this.tcx(), unconstrained_predicate))
})?;
let nested_eq_goals = let nested_eq_goals =
self.infcx.eq(goal.param_env, unconstrained_rhs, predicate.term)?; self.infcx.eq(goal.param_env, unconstrained_rhs, predicate.term)?;
@ -55,6 +56,15 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
} }
} }
/// This sets a flag used by a debug assert in [`EvalCtxt::evaluate_goal`],
/// see the comment in that method for more details.
fn in_projection_eq_hack<T>(&mut self, f: impl FnOnce(&mut Self) -> T) -> T {
self.in_projection_eq_hack = true;
let result = f(self);
self.in_projection_eq_hack = false;
result
}
/// Is the projection predicate is of the form `exists<T> <Ty as Trait>::Assoc = T`. /// Is the projection predicate is of the form `exists<T> <Ty as Trait>::Assoc = T`.
/// ///
/// This is the case if the `term` is an inference variable in the innermost universe /// This is the case if the `term` is an inference variable in the innermost universe

View file

@ -45,6 +45,7 @@ impl<'tcx> SearchGraph<'tcx> {
/// Tries putting the new goal on the stack, returning an error if it is already cached. /// Tries putting the new goal on the stack, returning an error if it is already cached.
/// ///
/// This correctly updates the provisional cache if there is a cycle. /// This correctly updates the provisional cache if there is a cycle.
#[instrument(level = "debug", skip(self, tcx), ret)]
pub(super) fn try_push_stack( pub(super) fn try_push_stack(
&mut self, &mut self,
tcx: TyCtxt<'tcx>, tcx: TyCtxt<'tcx>,
@ -79,8 +80,10 @@ impl<'tcx> SearchGraph<'tcx> {
Entry::Occupied(entry_index) => { Entry::Occupied(entry_index) => {
let entry_index = *entry_index.get(); let entry_index = *entry_index.get();
cache.add_dependency_of_leaf_on(entry_index);
let stack_depth = cache.depth(entry_index); let stack_depth = cache.depth(entry_index);
debug!("encountered cycle with depth {stack_depth:?}");
cache.add_dependency_of_leaf_on(entry_index);
self.stack[stack_depth].has_been_used = true; self.stack[stack_depth].has_been_used = true;
// NOTE: The goals on the stack aren't the only goals involved in this cycle. // NOTE: The goals on the stack aren't the only goals involved in this cycle.
@ -117,6 +120,7 @@ impl<'tcx> SearchGraph<'tcx> {
/// updated the provisional cache and we have to recompute the current goal. /// updated the provisional cache and we have to recompute the current goal.
/// ///
/// FIXME: Refer to the rustc-dev-guide entry once it exists. /// FIXME: Refer to the rustc-dev-guide entry once it exists.
#[instrument(level = "debug", skip(self, tcx, actual_goal), ret)]
pub(super) fn try_finalize_goal( pub(super) fn try_finalize_goal(
&mut self, &mut self,
tcx: TyCtxt<'tcx>, tcx: TyCtxt<'tcx>,