Skip to content

do not rerun trait solver cycles on ambiguity #125981

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 3 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 9 additions & 3 deletions compiler/rustc_trait_selection/src/solve/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -77,9 +77,15 @@ enum GoalEvaluationKind {
#[extension(trait CanonicalResponseExt)]
impl<'tcx> Canonical<'tcx, Response<TyCtxt<'tcx>>> {
fn has_no_inference_or_external_constraints(&self) -> bool {
self.value.external_constraints.region_constraints.is_empty()
&& self.value.var_values.is_identity()
&& self.value.external_constraints.opaque_types.is_empty()
let ExternalConstraintsData {
ref region_constraints,
ref opaque_types,
ref normalization_nested_goals,
} = *self.value.external_constraints;
self.value.var_values.is_identity()
&& region_constraints.is_empty()
&& opaque_types.is_empty()
&& normalization_nested_goals.is_empty()
}
}

Expand Down
87 changes: 60 additions & 27 deletions compiler/rustc_trait_selection/src/solve/search_graph.rs
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ use rustc_type_ir::Interner;
use super::inspect;
use super::inspect::ProofTreeBuilder;
use super::SolverMode;
use crate::solve::CanonicalResponseExt;
use crate::solve::FIXPOINT_STEP_LIMIT;

rustc_index::newtype_index! {
Expand Down Expand Up @@ -277,7 +278,7 @@ impl<'tcx> SearchGraph<TyCtxt<'tcx>> {

inspect
.canonical_goal_evaluation_kind(inspect::WipCanonicalGoalEvaluationKind::Overflow);
return Self::response_no_constraints(tcx, input, Certainty::overflow(true));
return response_no_constraints(tcx, input, Certainty::overflow(true));
};

if let Some(result) = self.lookup_global_cache(tcx, input, available_depth, inspect) {
Expand Down Expand Up @@ -334,9 +335,9 @@ impl<'tcx> SearchGraph<TyCtxt<'tcx>> {
return if let Some(result) = self.stack[stack_depth].provisional_result {
result
} else if is_coinductive_cycle {
Self::response_no_constraints(tcx, input, Certainty::Yes)
response_no_constraints(tcx, input, Certainty::Yes)
} else {
Self::response_no_constraints(tcx, input, Certainty::overflow(false))
response_no_constraints(tcx, input, Certainty::overflow(false))
};
} else {
// No entry, we push this goal on the stack and try to prove it.
Expand Down Expand Up @@ -364,7 +365,7 @@ impl<'tcx> SearchGraph<TyCtxt<'tcx>> {
let ((final_entry, result), dep_node) =
tcx.dep_graph.with_anon_task(tcx, dep_kinds::TraitSelect, || {
for _ in 0..FIXPOINT_STEP_LIMIT {
match self.fixpoint_step_in_task(tcx, input, inspect, &mut prove_goal) {
match self.fixpoint_step_in_task(input, inspect, &mut prove_goal) {
StepResult::Done(final_entry, result) => return (final_entry, result),
StepResult::HasChanged => debug!("fixpoint changed provisional results"),
}
Expand All @@ -373,7 +374,7 @@ impl<'tcx> SearchGraph<TyCtxt<'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(false));
let result = response_no_constraints(tcx, input, Certainty::overflow(false));
(current_entry, result)
});

Expand Down Expand Up @@ -473,7 +474,6 @@ impl<'tcx> SearchGraph<TyCtxt<'tcx>> {
/// point we are done.
fn fixpoint_step_in_task<F>(
&mut self,
tcx: TyCtxt<'tcx>,
input: CanonicalInput<TyCtxt<'tcx>>,
inspect: &mut ProofTreeBuilder<InferCtxt<'tcx>>,
prove_goal: &mut F,
Expand Down Expand Up @@ -504,22 +504,8 @@ impl<'tcx> SearchGraph<TyCtxt<'tcx>> {
self.stack.next_index(),
);

// Check whether we reached a fixpoint, either because the final result
// is equal to the provisional result of the previous iteration, or because
// this was only the root of either coinductive or inductive cycles, and the
// final result is equal to the initial response for that case.
let reached_fixpoint = if let Some(r) = stack_entry.provisional_result {
r == result
} 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(false)) == result
} else {
false
};

// If we did not reach a fixpoint, update the provisional result and reevaluate.
if reached_fixpoint {
if self.reached_fixpoint(&stack_entry, result) {
StepResult::Done(stack_entry, result)
} else {
let depth = self.stack.push(StackEntry {
Expand All @@ -532,15 +518,62 @@ impl<'tcx> SearchGraph<TyCtxt<'tcx>> {
}
}

fn response_no_constraints(
tcx: TyCtxt<'tcx>,
goal: CanonicalInput<TyCtxt<'tcx>>,
certainty: Certainty,
) -> QueryResult<TyCtxt<'tcx>> {
Ok(super::response_no_constraints_raw(tcx, goal.max_universe, goal.variables, certainty))
/// Check whether we reached a fixpoint we're done with the current cycle head.
///
/// This is the case if the final result is equal to the used provisional
/// result of the previous iteration or if the result of this iteration is
/// ambiguity with no constraints. We do not care about the previous provisional
/// result in this case.
fn reached_fixpoint(
&self,
stack_entry: &StackEntry<TyCtxt<'tcx>>,
result: QueryResult<TyCtxt<'tcx>>,
) -> bool {
if is_response_no_constraints(result, |c| matches!(c, Certainty::Maybe(_))) {
// If computing this goal results in ambiguity with no constraints,
// we do not rerun it. It's incredibly difficult to get a different
// response in the next iteration in this case. These changes would
// likely either be caused by incompleteness or can change the maybe
// cause from ambiguity to overflow. Returning ambiguity always
// preserves soundness and completeness even if the goal is be known
// to succeed or fail.
//
// This prevents exponential blowup affecting multiple major crates.
true
} else if let Some(r) = stack_entry.provisional_result {
// If we already have a provisional result for this cycle head from
// a previous iteration, simply check for a fixpoint.
r == result
} else if stack_entry.has_been_used == HasBeenUsed::COINDUCTIVE_CYCLE {
// If we only used this cycle head with inductive cycles, and the final
// response is trivially true, no need to rerun.
is_response_no_constraints(result, |c| c == Certainty::Yes)
} else {
// No need to check exclusively inductive cycles, as these are covered by the
// general overflow branch above.
false
}
}
}

fn response_no_constraints<'tcx>(
tcx: TyCtxt<'tcx>,
goal: CanonicalInput<TyCtxt<'tcx>>,
certainty: Certainty,
) -> QueryResult<TyCtxt<'tcx>> {
Ok(super::response_no_constraints_raw(tcx, goal.max_universe, goal.variables, certainty))
}

fn is_response_no_constraints<'tcx>(
result: QueryResult<TyCtxt<'tcx>>,
check_certainty: impl FnOnce(Certainty) -> bool,
) -> bool {
result.is_ok_and(|response| {
response.has_no_inference_or_external_constraints()
&& check_certainty(response.value.certainty)
})
}

impl<I: Interner> SearchGraph<I> {
#[allow(rustc::potential_query_instability)]
fn check_invariants(&self) {
Expand Down
Loading