From f56b2074c688f09be47e6ca82f604eabaa0b8f35 Mon Sep 17 00:00:00 2001
From: lcnr <rust@lcnr.de>
Date: Thu, 11 Jul 2024 15:39:17 +0200
Subject: [PATCH 1/2] solve -> solve/mod
---
compiler/rustc_type_ir/src/{solve.rs => solve/mod.rs} | 0
1 file changed, 0 insertions(+), 0 deletions(-)
rename compiler/rustc_type_ir/src/{solve.rs => solve/mod.rs} (100%)
diff --git a/compiler/rustc_type_ir/src/solve.rs b/compiler/rustc_type_ir/src/solve/mod.rs
similarity index 100%
rename from compiler/rustc_type_ir/src/solve.rs
rename to compiler/rustc_type_ir/src/solve/mod.rs
From 15f770b1436c2be227c9338040e53d64f211fe63 Mon Sep 17 00:00:00 2001
From: lcnr <rust@lcnr.de>
Date: Thu, 11 Jul 2024 23:13:12 +0200
Subject: [PATCH 2/2] enable fuzzing of `SearchGraph`
fully move it into `rustc_type_ir` and make it
independent of `Interner`.
---
compiler/rustc_middle/src/traits/solve.rs | 4 -
.../rustc_middle/src/traits/solve/cache.rs | 121 ----
compiler/rustc_middle/src/ty/context.rs | 29 +-
.../src/solve/eval_ctxt/mod.rs | 14 +-
.../src/solve/inspect/build.rs | 69 +-
.../src/solve/search_graph.rs | 623 ++----------------
compiler/rustc_query_system/src/cache.rs | 2 +-
compiler/rustc_type_ir/src/inherent.rs | 30 +-
compiler/rustc_type_ir/src/interner.rs | 48 +-
compiler/rustc_type_ir/src/lib.rs | 1 +
.../src/search_graph/global_cache.rs | 118 ++++
.../rustc_type_ir/src/search_graph/mod.rs | 605 +++++++++++++++++
.../src/search_graph/validate.rs | 75 +++
13 files changed, 982 insertions(+), 757 deletions(-)
delete mode 100644 compiler/rustc_middle/src/traits/solve/cache.rs
create mode 100644 compiler/rustc_type_ir/src/search_graph/global_cache.rs
create mode 100644 compiler/rustc_type_ir/src/search_graph/mod.rs
create mode 100644 compiler/rustc_type_ir/src/search_graph/validate.rs
diff --git a/compiler/rustc_middle/src/traits/solve.rs b/compiler/rustc_middle/src/traits/solve.rs
index 7bc4c60f10272..f659bf8125a0e 100644
--- a/compiler/rustc_middle/src/traits/solve.rs
+++ b/compiler/rustc_middle/src/traits/solve.rs
@@ -8,10 +8,6 @@ use crate::ty::{
self, FallibleTypeFolder, TyCtxt, TypeFoldable, TypeFolder, TypeVisitable, TypeVisitor,
};
-mod cache;
-
-pub use cache::EvaluationCache;
-
pub type Goal<'tcx, P> = ir::solve::Goal<TyCtxt<'tcx>, P>;
pub type QueryInput<'tcx, P> = ir::solve::QueryInput<TyCtxt<'tcx>, P>;
pub type QueryResult<'tcx> = ir::solve::QueryResult<TyCtxt<'tcx>>;
diff --git a/compiler/rustc_middle/src/traits/solve/cache.rs b/compiler/rustc_middle/src/traits/solve/cache.rs
deleted file mode 100644
index 72a8d4eb4050c..0000000000000
--- a/compiler/rustc_middle/src/traits/solve/cache.rs
+++ /dev/null
@@ -1,121 +0,0 @@
-use super::{inspect, CanonicalInput, QueryResult};
-use crate::ty::TyCtxt;
-use rustc_data_structures::fx::{FxHashMap, FxHashSet};
-use rustc_data_structures::sync::Lock;
-use rustc_query_system::cache::WithDepNode;
-use rustc_query_system::dep_graph::DepNodeIndex;
-use rustc_session::Limit;
-use rustc_type_ir::solve::CacheData;
-
-/// The trait solver cache used by `-Znext-solver`.
-///
-/// FIXME(@lcnr): link to some official documentation of how
-/// this works.
-#[derive(Default)]
-pub struct EvaluationCache<'tcx> {
- map: Lock<FxHashMap<CanonicalInput<'tcx>, CacheEntry<'tcx>>>,
-}
-
-impl<'tcx> rustc_type_ir::inherent::EvaluationCache<TyCtxt<'tcx>> for &'tcx EvaluationCache<'tcx> {
- /// Insert a final result into the global cache.
- fn insert(
- &self,
- tcx: TyCtxt<'tcx>,
- key: CanonicalInput<'tcx>,
- proof_tree: Option<&'tcx inspect::CanonicalGoalEvaluationStep<TyCtxt<'tcx>>>,
- additional_depth: usize,
- encountered_overflow: bool,
- cycle_participants: FxHashSet<CanonicalInput<'tcx>>,
- dep_node: DepNodeIndex,
- result: QueryResult<'tcx>,
- ) {
- let mut map = self.map.borrow_mut();
- let entry = map.entry(key).or_default();
- let data = WithDepNode::new(dep_node, QueryData { result, proof_tree });
- entry.cycle_participants.extend(cycle_participants);
- if encountered_overflow {
- entry.with_overflow.insert(additional_depth, data);
- } else {
- entry.success = Some(Success { data, additional_depth });
- }
-
- if cfg!(debug_assertions) {
- drop(map);
- let expected = CacheData { result, proof_tree, additional_depth, encountered_overflow };
- let actual = self.get(tcx, key, [], additional_depth);
- if !actual.as_ref().is_some_and(|actual| expected == *actual) {
- bug!("failed to lookup inserted element for {key:?}: {expected:?} != {actual:?}");
- }
- }
- }
-
- /// Try to fetch a cached result, checking the recursion limit
- /// and handling root goals of coinductive cycles.
- ///
- /// If this returns `Some` the cache result can be used.
- fn get(
- &self,
- tcx: TyCtxt<'tcx>,
- key: CanonicalInput<'tcx>,
- stack_entries: impl IntoIterator<Item = CanonicalInput<'tcx>>,
- available_depth: usize,
- ) -> Option<CacheData<TyCtxt<'tcx>>> {
- let map = self.map.borrow();
- let entry = map.get(&key)?;
-
- for stack_entry in stack_entries {
- if entry.cycle_participants.contains(&stack_entry) {
- return None;
- }
- }
-
- if let Some(ref success) = entry.success {
- if Limit(available_depth).value_within_limit(success.additional_depth) {
- let QueryData { result, proof_tree } = success.data.get(tcx);
- return Some(CacheData {
- result,
- proof_tree,
- additional_depth: success.additional_depth,
- encountered_overflow: false,
- });
- }
- }
-
- entry.with_overflow.get(&available_depth).map(|e| {
- let QueryData { result, proof_tree } = e.get(tcx);
- CacheData {
- result,
- proof_tree,
- additional_depth: available_depth,
- encountered_overflow: true,
- }
- })
- }
-}
-
-struct Success<'tcx> {
- data: WithDepNode<QueryData<'tcx>>,
- additional_depth: usize,
-}
-
-#[derive(Clone, Copy)]
-pub struct QueryData<'tcx> {
- pub result: QueryResult<'tcx>,
- pub proof_tree: Option<&'tcx inspect::CanonicalGoalEvaluationStep<TyCtxt<'tcx>>>,
-}
-
-/// The cache entry for a goal `CanonicalInput`.
-///
-/// This contains results whose computation never hit the
-/// recursion limit in `success`, and all results which hit
-/// the recursion limit in `with_overflow`.
-#[derive(Default)]
-struct CacheEntry<'tcx> {
- success: Option<Success<'tcx>>,
- /// We have to be careful when caching roots of cycles.
- ///
- /// See the doc comment of `StackEntry::cycle_participants` for more
- /// details.
- cycle_participants: FxHashSet<CanonicalInput<'tcx>>,
- with_overflow: FxHashMap<usize, WithDepNode<QueryData<'tcx>>>,
-}
diff --git a/compiler/rustc_middle/src/ty/context.rs b/compiler/rustc_middle/src/ty/context.rs
index aee42bfe3aaca..9e24ea485b26e 100644
--- a/compiler/rustc_middle/src/ty/context.rs
+++ b/compiler/rustc_middle/src/ty/context.rs
@@ -59,6 +59,7 @@ use rustc_hir::lang_items::LangItem;
use rustc_hir::{HirId, Node, TraitCandidate};
use rustc_index::IndexVec;
use rustc_macros::{HashStable, TyDecodable, TyEncodable};
+use rustc_query_system::cache::WithDepNode;
use rustc_query_system::dep_graph::DepNodeIndex;
use rustc_query_system::ich::StableHashingContext;
use rustc_serialize::opaque::{FileEncodeResult, FileEncoder};
@@ -75,7 +76,7 @@ use rustc_type_ir::fold::TypeFoldable;
use rustc_type_ir::lang_items::TraitSolverLangItem;
use rustc_type_ir::solve::SolverMode;
use rustc_type_ir::TyKind::*;
-use rustc_type_ir::{CollectAndApply, Interner, TypeFlags, WithCachedTypeInfo};
+use rustc_type_ir::{search_graph, CollectAndApply, Interner, TypeFlags, WithCachedTypeInfo};
use tracing::{debug, instrument};
use std::assert_matches::assert_matches;
@@ -164,12 +165,26 @@ impl<'tcx> Interner for TyCtxt<'tcx> {
type Clause = Clause<'tcx>;
type Clauses = ty::Clauses<'tcx>;
- type EvaluationCache = &'tcx solve::EvaluationCache<'tcx>;
+ type Tracked<T: fmt::Debug + Clone> = WithDepNode<T>;
+ fn mk_tracked<T: fmt::Debug + Clone>(
+ self,
+ data: T,
+ dep_node: DepNodeIndex,
+ ) -> Self::Tracked<T> {
+ WithDepNode::new(dep_node, data)
+ }
+ fn get_tracked<T: fmt::Debug + Clone>(self, tracked: &Self::Tracked<T>) -> T {
+ tracked.get(self)
+ }
- fn evaluation_cache(self, mode: SolverMode) -> &'tcx solve::EvaluationCache<'tcx> {
+ fn with_global_cache<R>(
+ self,
+ mode: SolverMode,
+ f: impl FnOnce(&mut search_graph::GlobalCache<Self>) -> R,
+ ) -> R {
match mode {
- SolverMode::Normal => &self.new_solver_evaluation_cache,
- SolverMode::Coherence => &self.new_solver_coherence_evaluation_cache,
+ SolverMode::Normal => f(&mut *self.new_solver_evaluation_cache.lock()),
+ SolverMode::Coherence => f(&mut *self.new_solver_coherence_evaluation_cache.lock()),
}
}
@@ -1283,8 +1298,8 @@ pub struct GlobalCtxt<'tcx> {
pub evaluation_cache: traits::EvaluationCache<'tcx>,
/// Caches the results of goal evaluation in the new solver.
- pub new_solver_evaluation_cache: solve::EvaluationCache<'tcx>,
- pub new_solver_coherence_evaluation_cache: solve::EvaluationCache<'tcx>,
+ pub new_solver_evaluation_cache: Lock<search_graph::GlobalCache<TyCtxt<'tcx>>>,
+ pub new_solver_coherence_evaluation_cache: Lock<search_graph::GlobalCache<TyCtxt<'tcx>>>,
pub canonical_param_env_cache: CanonicalParamEnvCache<'tcx>,
diff --git a/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs b/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs
index c90f8e761633b..c23bc8f09ad16 100644
--- a/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs
@@ -16,9 +16,9 @@ use crate::delegate::SolverDelegate;
use crate::solve::inspect::{self, ProofTreeBuilder};
use crate::solve::search_graph::SearchGraph;
use crate::solve::{
- search_graph, CanonicalInput, CanonicalResponse, Certainty, Goal, GoalEvaluationKind,
- GoalSource, MaybeCause, NestedNormalizationGoals, NoSolution, PredefinedOpaquesData,
- QueryResult, SolverMode, FIXPOINT_STEP_LIMIT,
+ CanonicalInput, CanonicalResponse, Certainty, Goal, GoalEvaluationKind, GoalSource, MaybeCause,
+ NestedNormalizationGoals, NoSolution, PredefinedOpaquesData, QueryResult, SolverMode,
+ FIXPOINT_STEP_LIMIT,
};
pub(super) mod canonical;
@@ -72,7 +72,7 @@ where
/// new placeholders to the caller.
pub(super) max_input_universe: ty::UniverseIndex,
- pub(super) search_graph: &'a mut SearchGraph<I>,
+ pub(super) search_graph: &'a mut SearchGraph<D>,
nested_goals: NestedGoals<I>,
@@ -200,7 +200,7 @@ where
generate_proof_tree: GenerateProofTree,
f: impl FnOnce(&mut EvalCtxt<'_, D>) -> R,
) -> (R, Option<inspect::GoalEvaluation<I>>) {
- let mut search_graph = search_graph::SearchGraph::new(delegate.solver_mode());
+ let mut search_graph = SearchGraph::new(delegate.solver_mode());
let mut ecx = EvalCtxt {
delegate,
@@ -241,7 +241,7 @@ where
/// and registering opaques from the canonicalized input.
fn enter_canonical<R>(
cx: I,
- search_graph: &'a mut search_graph::SearchGraph<I>,
+ search_graph: &'a mut SearchGraph<D>,
canonical_input: CanonicalInput<I>,
canonical_goal_evaluation: &mut ProofTreeBuilder<D>,
f: impl FnOnce(&mut EvalCtxt<'_, D>, Goal<I, I::Predicate>) -> R,
@@ -296,7 +296,7 @@ where
#[instrument(level = "debug", skip(cx, search_graph, goal_evaluation), ret)]
fn evaluate_canonical_goal(
cx: I,
- search_graph: &'a mut search_graph::SearchGraph<I>,
+ search_graph: &'a mut SearchGraph<D>,
canonical_input: CanonicalInput<I>,
goal_evaluation: &mut ProofTreeBuilder<D>,
) -> QueryResult<I> {
diff --git a/compiler/rustc_next_trait_solver/src/solve/inspect/build.rs b/compiler/rustc_next_trait_solver/src/solve/inspect/build.rs
index b50676e8d5327..3e266ddac71fd 100644
--- a/compiler/rustc_next_trait_solver/src/solve/inspect/build.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/inspect/build.rs
@@ -8,7 +8,7 @@ use std::marker::PhantomData;
use std::mem;
use rustc_type_ir::inherent::*;
-use rustc_type_ir::{self as ty, Interner};
+use rustc_type_ir::{self as ty, search_graph, Interner};
use crate::delegate::SolverDelegate;
use crate::solve::eval_ctxt::canonical;
@@ -38,7 +38,7 @@ use crate::solve::{
/// trees. At the end of trait solving `ProofTreeBuilder::finalize`
/// is called to recursively convert the whole structure to a
/// finished proof tree.
-pub(in crate::solve) struct ProofTreeBuilder<D, I = <D as SolverDelegate>::Interner>
+pub(crate) struct ProofTreeBuilder<D, I = <D as SolverDelegate>::Interner>
where
D: SolverDelegate<Interner = I>,
I: Interner,
@@ -321,23 +321,6 @@ impl<D: SolverDelegate<Interner = I>, I: Interner> ProofTreeBuilder<D> {
})
}
- pub fn finalize_canonical_goal_evaluation(
- &mut self,
- cx: I,
- ) -> Option<I::CanonicalGoalEvaluationStepRef> {
- self.as_mut().map(|this| match this {
- DebugSolver::CanonicalGoalEvaluation(evaluation) => {
- let final_revision = mem::take(&mut evaluation.final_revision).unwrap();
- let final_revision =
- cx.intern_canonical_goal_evaluation_step(final_revision.finalize());
- let kind = WipCanonicalGoalEvaluationKind::Interned { final_revision };
- assert_eq!(evaluation.kind.replace(kind), None);
- final_revision
- }
- _ => unreachable!(),
- })
- }
-
pub fn canonical_goal_evaluation(&mut self, canonical_goal_evaluation: ProofTreeBuilder<D>) {
if let Some(this) = self.as_mut() {
match (this, *canonical_goal_evaluation.state.unwrap()) {
@@ -571,3 +554,51 @@ impl<D: SolverDelegate<Interner = I>, I: Interner> ProofTreeBuilder<D> {
}
}
}
+
+impl<D, I> search_graph::ProofTreeBuilder<I> for ProofTreeBuilder<D>
+where
+ D: SolverDelegate<Interner = I>,
+ I: Interner,
+{
+ fn try_apply_proof_tree(
+ &mut self,
+ proof_tree: Option<I::CanonicalGoalEvaluationStepRef>,
+ ) -> bool {
+ if !self.is_noop() {
+ if let Some(final_revision) = proof_tree {
+ let kind = WipCanonicalGoalEvaluationKind::Interned { final_revision };
+ self.canonical_goal_evaluation_kind(kind);
+ true
+ } else {
+ false
+ }
+ } else {
+ true
+ }
+ }
+
+ fn on_provisional_cache_hit(&mut self) {
+ self.canonical_goal_evaluation_kind(WipCanonicalGoalEvaluationKind::ProvisionalCacheHit);
+ }
+
+ fn on_cycle_in_stack(&mut self) {
+ self.canonical_goal_evaluation_kind(WipCanonicalGoalEvaluationKind::CycleInStack);
+ }
+
+ fn finalize_canonical_goal_evaluation(
+ &mut self,
+ tcx: I,
+ ) -> Option<I::CanonicalGoalEvaluationStepRef> {
+ self.as_mut().map(|this| match this {
+ DebugSolver::CanonicalGoalEvaluation(evaluation) => {
+ let final_revision = mem::take(&mut evaluation.final_revision).unwrap();
+ let final_revision =
+ tcx.intern_canonical_goal_evaluation_step(final_revision.finalize());
+ let kind = WipCanonicalGoalEvaluationKind::Interned { final_revision };
+ assert_eq!(evaluation.kind.replace(kind), None);
+ final_revision
+ }
+ _ => unreachable!(),
+ })
+ }
+}
diff --git a/compiler/rustc_next_trait_solver/src/solve/search_graph.rs b/compiler/rustc_next_trait_solver/src/solve/search_graph.rs
index 69d52dcad7a59..fe053a506e712 100644
--- a/compiler/rustc_next_trait_solver/src/solve/search_graph.rs
+++ b/compiler/rustc_next_trait_solver/src/solve/search_graph.rs
@@ -1,599 +1,90 @@
-use std::mem;
+use std::marker::PhantomData;
-use rustc_index::{Idx, IndexVec};
-use rustc_type_ir::data_structures::{HashMap, HashSet};
use rustc_type_ir::inherent::*;
+use rustc_type_ir::search_graph::{self, CycleKind, UsageKind};
+use rustc_type_ir::solve::{CanonicalInput, Certainty, QueryResult};
use rustc_type_ir::Interner;
-use tracing::debug;
+use super::inspect::{self, ProofTreeBuilder};
+use super::FIXPOINT_STEP_LIMIT;
use crate::delegate::SolverDelegate;
-use crate::solve::inspect::{self, ProofTreeBuilder};
-use crate::solve::{
- CacheData, CanonicalInput, Certainty, QueryResult, SolverMode, FIXPOINT_STEP_LIMIT,
-};
-#[derive(Copy, Clone, PartialEq, Eq, Debug)]
-pub struct SolverLimit(usize);
-
-rustc_index::newtype_index! {
- #[orderable]
- #[gate_rustc_only]
- pub struct StackDepth {}
-}
-
-bitflags::bitflags! {
- /// Whether and how this goal has been used as the root of a
- /// cycle. We track the kind of cycle as we're otherwise forced
- /// to always rerun at least once.
- #[derive(Debug, Clone, Copy, PartialEq, Eq)]
- struct HasBeenUsed: u8 {
- const INDUCTIVE_CYCLE = 1 << 0;
- const COINDUCTIVE_CYCLE = 1 << 1;
- }
-}
-
-#[derive(derivative::Derivative)]
-#[derivative(Debug(bound = ""))]
-struct StackEntry<I: Interner> {
- input: CanonicalInput<I>,
-
- available_depth: SolverLimit,
-
- /// The maximum depth reached by this stack entry, only up-to date
- /// for the top of the stack and lazily updated for the rest.
- reached_depth: StackDepth,
-
- /// Whether this entry is a non-root cycle participant.
- ///
- /// We must not move the result of non-root cycle participants to the
- /// global cache. We store the highest stack depth of a head of a cycle
- /// this goal is involved in. This necessary to soundly cache its
- /// provisional result.
- non_root_cycle_participant: Option<StackDepth>,
-
- encountered_overflow: bool,
-
- has_been_used: HasBeenUsed,
-
- /// We put only the root goal of a coinductive cycle into the global cache.
- ///
- /// If we were to use that result when later trying to prove another cycle
- /// participant, we can end up with unstable query results.
- ///
- /// See tests/ui/next-solver/coinduction/incompleteness-unstable-result.rs for
- /// an example of where this is needed.
- ///
- /// There can be multiple roots on the same stack, so we need to track
- /// cycle participants per root:
- /// ```plain
- /// A :- B
- /// B :- A, C
- /// C :- D
- /// D :- C
- /// ```
- nested_goals: HashSet<CanonicalInput<I>>,
- /// Starts out as `None` and gets set when rerunning this
- /// goal in case we encounter a cycle.
- provisional_result: Option<QueryResult<I>>,
-}
-
-/// The provisional result for a goal which is not on the stack.
-#[derive(Debug)]
-struct DetachedEntry<I: Interner> {
- /// The head of the smallest non-trivial cycle involving this entry.
- ///
- /// Given the following rules, when proving `A` the head for
- /// the provisional entry of `C` would be `B`.
- /// ```plain
- /// A :- B
- /// B :- C
- /// C :- A + B + C
- /// ```
- head: StackDepth,
- result: QueryResult<I>,
-}
-
-/// Stores the stack depth of a currently evaluated goal *and* already
-/// computed results for goals which depend on other goals still on the stack.
-///
-/// The provisional result may depend on whether the stack above it is inductive
-/// or coinductive. Because of this, we store separate provisional results for
-/// each case. If an provisional entry is not applicable, it may be the case
-/// that we already have provisional result while computing a goal. In this case
-/// we prefer the provisional result to potentially avoid fixpoint iterations.
-/// See tests/ui/traits/next-solver/cycles/mixed-cycles-2.rs for an example.
-///
-/// The provisional cache can theoretically result in changes to the observable behavior,
-/// see tests/ui/traits/next-solver/cycles/provisional-cache-impacts-behavior.rs.
-#[derive(derivative::Derivative)]
-#[derivative(Default(bound = ""))]
-struct ProvisionalCacheEntry<I: Interner> {
- stack_depth: Option<StackDepth>,
- with_inductive_stack: Option<DetachedEntry<I>>,
- with_coinductive_stack: Option<DetachedEntry<I>>,
-}
-
-impl<I: Interner> ProvisionalCacheEntry<I> {
- fn is_empty(&self) -> bool {
- self.stack_depth.is_none()
- && self.with_inductive_stack.is_none()
- && self.with_coinductive_stack.is_none()
- }
+/// This type is never constructed. We only use it to implement `search_graph::Delegate`
+/// for all types which impl `SolverDelegate` and doing it directly fails in coherence.
+pub(super) struct SearchGraphDelegate<D: SolverDelegate> {
+ _marker: PhantomData<D>,
}
+pub(super) type SearchGraph<D> = search_graph::SearchGraph<SearchGraphDelegate<D>>;
+impl<D, I> search_graph::Delegate for SearchGraphDelegate<D>
+where
+ D: SolverDelegate<Interner = I>,
+ I: Interner,
+{
+ type Cx = D::Interner;
-pub(super) struct SearchGraph<I: Interner> {
- mode: SolverMode,
- /// The stack of goals currently being computed.
- ///
- /// An element is *deeper* in the stack if its index is *lower*.
- stack: IndexVec<StackDepth, StackEntry<I>>,
- provisional_cache: HashMap<CanonicalInput<I>, ProvisionalCacheEntry<I>>,
-}
+ const FIXPOINT_STEP_LIMIT: usize = FIXPOINT_STEP_LIMIT;
-impl<I: Interner> SearchGraph<I> {
- pub(super) fn new(mode: SolverMode) -> SearchGraph<I> {
- Self { mode, stack: Default::default(), provisional_cache: Default::default() }
- }
+ type ProofTreeBuilder = ProofTreeBuilder<D>;
- pub(super) fn solver_mode(&self) -> SolverMode {
- self.mode
+ fn recursion_limit(cx: I) -> usize {
+ cx.recursion_limit()
}
- fn update_parent_goal(&mut self, reached_depth: StackDepth, encountered_overflow: bool) {
- if let Some(parent) = self.stack.raw.last_mut() {
- parent.reached_depth = parent.reached_depth.max(reached_depth);
- parent.encountered_overflow |= encountered_overflow;
- }
- }
-
- pub(super) fn is_empty(&self) -> bool {
- self.stack.is_empty()
- }
-
- /// Returns the remaining depth allowed for nested goals.
- ///
- /// This is generally simply one less than the current depth.
- /// However, if we encountered overflow, we significantly reduce
- /// the remaining depth of all nested goals to prevent hangs
- /// in case there is exponential blowup.
- fn allowed_depth_for_nested(
+ fn initial_provisional_result(
cx: I,
- stack: &IndexVec<StackDepth, StackEntry<I>>,
- ) -> Option<SolverLimit> {
- if let Some(last) = stack.raw.last() {
- if last.available_depth.0 == 0 {
- return None;
- }
-
- Some(if last.encountered_overflow {
- SolverLimit(last.available_depth.0 / 4)
- } else {
- SolverLimit(last.available_depth.0 - 1)
- })
- } else {
- Some(SolverLimit(cx.recursion_limit()))
- }
- }
-
- fn stack_coinductive_from(
- cx: I,
- stack: &IndexVec<StackDepth, StackEntry<I>>,
- head: StackDepth,
- ) -> bool {
- stack.raw[head.index()..]
- .iter()
- .all(|entry| entry.input.value.goal.predicate.is_coinductive(cx))
- }
-
- // When encountering a solver cycle, the result of the current goal
- // depends on goals lower on the stack.
- //
- // We have to therefore be careful when caching goals. Only the final result
- // of the cycle root, i.e. the lowest goal on the stack involved in this cycle,
- // is moved to the global cache while all others are stored in a provisional cache.
- //
- // We update both the head of this cycle to rerun its evaluation until
- // we reach a fixpoint and all other cycle participants to make sure that
- // their result does not get moved to the global cache.
- fn tag_cycle_participants(
- stack: &mut IndexVec<StackDepth, StackEntry<I>>,
- usage_kind: HasBeenUsed,
- head: StackDepth,
- ) {
- stack[head].has_been_used |= usage_kind;
- debug_assert!(!stack[head].has_been_used.is_empty());
-
- // The current root of these cycles. Note that this may not be the final
- // root in case a later goal depends on a goal higher up the stack.
- let mut current_root = head;
- while let Some(parent) = stack[current_root].non_root_cycle_participant {
- current_root = parent;
- debug_assert!(!stack[current_root].has_been_used.is_empty());
- }
-
- let (stack, cycle_participants) = stack.raw.split_at_mut(head.index() + 1);
- let current_cycle_root = &mut stack[current_root.as_usize()];
- for entry in cycle_participants {
- entry.non_root_cycle_participant = entry.non_root_cycle_participant.max(Some(head));
- current_cycle_root.nested_goals.insert(entry.input);
- current_cycle_root.nested_goals.extend(mem::take(&mut entry.nested_goals));
+ kind: CycleKind,
+ input: CanonicalInput<I>,
+ ) -> QueryResult<I> {
+ match kind {
+ CycleKind::Coinductive => response_no_constraints(cx, input, Certainty::Yes),
+ CycleKind::Inductive => response_no_constraints(cx, input, Certainty::overflow(false)),
}
}
- fn clear_dependent_provisional_results(
- provisional_cache: &mut HashMap<CanonicalInput<I>, ProvisionalCacheEntry<I>>,
- head: StackDepth,
- ) {
- #[allow(rustc::potential_query_instability)]
- provisional_cache.retain(|_, entry| {
- if entry.with_coinductive_stack.as_ref().is_some_and(|p| p.head == head) {
- entry.with_coinductive_stack.take();
- }
- if entry.with_inductive_stack.as_ref().is_some_and(|p| p.head == head) {
- entry.with_inductive_stack.take();
- }
- !entry.is_empty()
- });
- }
-
- /// The trait solver behavior is different for coherence
- /// so we use a separate cache. Alternatively we could use
- /// a single cache and share it between coherence and ordinary
- /// trait solving.
- pub(super) fn global_cache(&self, cx: I) -> I::EvaluationCache {
- cx.evaluation_cache(self.mode)
- }
-
- /// Probably the most involved method of the whole solver.
- ///
- /// Given some goal which is proven via the `prove_goal` closure, this
- /// handles caching, overflow, and coinductive cycles.
- pub(super) fn with_new_goal<D: SolverDelegate<Interner = I>>(
- &mut self,
+ fn reached_fixpoint(
cx: I,
+ kind: UsageKind,
input: CanonicalInput<I>,
- inspect: &mut ProofTreeBuilder<D>,
- mut prove_goal: impl FnMut(&mut Self, &mut ProofTreeBuilder<D>) -> QueryResult<I>,
- ) -> QueryResult<I> {
- self.check_invariants();
- // Check for overflow.
- let Some(available_depth) = Self::allowed_depth_for_nested(cx, &self.stack) else {
- if let Some(last) = self.stack.raw.last_mut() {
- last.encountered_overflow = true;
- }
-
- inspect
- .canonical_goal_evaluation_kind(inspect::WipCanonicalGoalEvaluationKind::Overflow);
- return Self::response_no_constraints(cx, input, Certainty::overflow(true));
- };
-
- if let Some(result) = self.lookup_global_cache(cx, input, available_depth, inspect) {
- debug!("global cache hit");
- return result;
- }
-
- // Check whether the goal is in the provisional cache.
- // The provisional result may rely on the path to its cycle roots,
- // so we have to check the path of the current goal matches that of
- // the cache entry.
- let cache_entry = self.provisional_cache.entry(input).or_default();
- if let Some(entry) = cache_entry
- .with_coinductive_stack
- .as_ref()
- .filter(|p| Self::stack_coinductive_from(cx, &self.stack, p.head))
- .or_else(|| {
- cache_entry
- .with_inductive_stack
- .as_ref()
- .filter(|p| !Self::stack_coinductive_from(cx, &self.stack, p.head))
- })
- {
- debug!("provisional cache hit");
- // We have a nested goal which is already in the provisional cache, use
- // its result. We do not provide any usage kind as that should have been
- // already set correctly while computing the cache entry.
- inspect.canonical_goal_evaluation_kind(
- inspect::WipCanonicalGoalEvaluationKind::ProvisionalCacheHit,
- );
- Self::tag_cycle_participants(&mut self.stack, HasBeenUsed::empty(), entry.head);
- return entry.result;
- } else if let Some(stack_depth) = cache_entry.stack_depth {
- debug!("encountered cycle with depth {stack_depth:?}");
- // We have a nested goal which directly relies on a goal deeper in the stack.
- //
- // We start by tagging all cycle participants, as that's necessary for caching.
- //
- // Finally we can return either the provisional response or the initial response
- // in case we're in the first fixpoint iteration for this goal.
- inspect.canonical_goal_evaluation_kind(
- inspect::WipCanonicalGoalEvaluationKind::CycleInStack,
- );
- let is_coinductive_cycle = Self::stack_coinductive_from(cx, &self.stack, stack_depth);
- let usage_kind = if is_coinductive_cycle {
- HasBeenUsed::COINDUCTIVE_CYCLE
- } else {
- HasBeenUsed::INDUCTIVE_CYCLE
- };
- Self::tag_cycle_participants(&mut self.stack, usage_kind, stack_depth);
-
- // Return the provisional result or, if we're in the first iteration,
- // start with no constraints.
- return if let Some(result) = self.stack[stack_depth].provisional_result {
- result
- } else if is_coinductive_cycle {
- Self::response_no_constraints(cx, input, Certainty::Yes)
- } else {
- Self::response_no_constraints(cx, input, Certainty::overflow(false))
- };
+ provisional_result: Option<QueryResult<I>>,
+ result: QueryResult<I>,
+ ) -> bool {
+ if let Some(r) = provisional_result {
+ r == result
} else {
- // No entry, we push this goal on the stack and try to prove it.
- let depth = self.stack.next_index();
- let entry = StackEntry {
- input,
- available_depth,
- reached_depth: depth,
- non_root_cycle_participant: None,
- encountered_overflow: false,
- has_been_used: HasBeenUsed::empty(),
- nested_goals: Default::default(),
- provisional_result: None,
- };
- assert_eq!(self.stack.push(entry), depth);
- cache_entry.stack_depth = Some(depth);
- }
-
- // This is for global caching, so we properly track query dependencies.
- // Everything that affects the `result` should be performed within this
- // `with_anon_task` closure. If computing this goal depends on something
- // not tracked by the cache key and from outside of this anon task, it
- // must not be added to the global cache. Notably, this is the case for
- // trait solver cycles participants.
- let ((final_entry, result), dep_node) = cx.with_cached_task(|| {
- for _ in 0..FIXPOINT_STEP_LIMIT {
- match self.fixpoint_step_in_task(cx, input, inspect, &mut prove_goal) {
- StepResult::Done(final_entry, result) => return (final_entry, result),
- StepResult::HasChanged => debug!("fixpoint changed provisional results"),
+ match kind {
+ UsageKind::Single(CycleKind::Coinductive) => {
+ response_no_constraints(cx, input, Certainty::Yes) == result
}
+ UsageKind::Single(CycleKind::Inductive) => {
+ response_no_constraints(cx, input, Certainty::overflow(false)) == result
+ }
+ UsageKind::Mixed => false,
}
-
- debug!("canonical cycle overflow");
- let current_entry = self.stack.pop().unwrap();
- debug_assert!(current_entry.has_been_used.is_empty());
- let result = Self::response_no_constraints(cx, input, Certainty::overflow(false));
- (current_entry, result)
- });
-
- let proof_tree = inspect.finalize_canonical_goal_evaluation(cx);
-
- self.update_parent_goal(final_entry.reached_depth, final_entry.encountered_overflow);
-
- // We're now done with this goal. In case this goal is involved in a larger cycle
- // do not remove it from the provisional cache and update its provisional result.
- // We only add the root of cycles to the global cache.
- if let Some(head) = final_entry.non_root_cycle_participant {
- let coinductive_stack = Self::stack_coinductive_from(cx, &self.stack, head);
-
- let entry = self.provisional_cache.get_mut(&input).unwrap();
- entry.stack_depth = None;
- if coinductive_stack {
- entry.with_coinductive_stack = Some(DetachedEntry { head, result });
- } else {
- entry.with_inductive_stack = Some(DetachedEntry { head, result });
- }
- } else {
- self.provisional_cache.remove(&input);
- let reached_depth = final_entry.reached_depth.as_usize() - self.stack.len();
- // When encountering a cycle, both inductive and coinductive, we only
- // move the root into the global cache. We also store all other cycle
- // participants involved.
- //
- // We must not use the global cache entry of a root goal if a cycle
- // participant is on the stack. This is necessary to prevent unstable
- // results. See the comment of `StackEntry::nested_goals` for
- // more details.
- self.global_cache(cx).insert(
- cx,
- input,
- proof_tree,
- reached_depth,
- final_entry.encountered_overflow,
- final_entry.nested_goals,
- dep_node,
- result,
- )
}
-
- self.check_invariants();
-
- result
}
- /// Try to fetch a previously computed result from the global cache,
- /// making sure to only do so if it would match the result of reevaluating
- /// this goal.
- fn lookup_global_cache<D: SolverDelegate<Interner = I>>(
- &mut self,
+ fn on_stack_overflow(
cx: I,
- input: CanonicalInput<I>,
- available_depth: SolverLimit,
inspect: &mut ProofTreeBuilder<D>,
- ) -> Option<QueryResult<I>> {
- let CacheData { result, proof_tree, additional_depth, encountered_overflow } = self
- .global_cache(cx)
- // FIXME: Awkward `Limit -> usize -> Limit`.
- .get(cx, input, self.stack.iter().map(|e| e.input), available_depth.0)?;
-
- // If we're building a proof tree and the current cache entry does not
- // contain a proof tree, we do not use the entry but instead recompute
- // the goal. We simply overwrite the existing entry once we're done,
- // caching the proof tree.
- if !inspect.is_noop() {
- if let Some(final_revision) = proof_tree {
- let kind = inspect::WipCanonicalGoalEvaluationKind::Interned { final_revision };
- inspect.canonical_goal_evaluation_kind(kind);
- } else {
- return None;
- }
- }
-
- // Adjust the parent goal as if we actually computed this goal.
- let reached_depth = self.stack.next_index().plus(additional_depth);
- self.update_parent_goal(reached_depth, encountered_overflow);
-
- Some(result)
- }
-}
-
-enum StepResult<I: Interner> {
- Done(StackEntry<I>, QueryResult<I>),
- HasChanged,
-}
-
-impl<I: Interner> SearchGraph<I> {
- /// When we encounter a coinductive cycle, we have to fetch the
- /// result of that cycle while we are still computing it. Because
- /// 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.
- fn fixpoint_step_in_task<D, F>(
- &mut self,
- cx: I,
input: CanonicalInput<I>,
- inspect: &mut ProofTreeBuilder<D>,
- prove_goal: &mut F,
- ) -> StepResult<I>
- where
- D: SolverDelegate<Interner = I>,
- F: FnMut(&mut Self, &mut ProofTreeBuilder<D>) -> QueryResult<I>,
- {
- let result = prove_goal(self, inspect);
- let stack_entry = self.stack.pop().unwrap();
- debug_assert_eq!(stack_entry.input, input);
-
- // If the current goal is not the root of a cycle, we are done.
- if stack_entry.has_been_used.is_empty() {
- return StepResult::Done(stack_entry, result);
- }
-
- // If it is a cycle head, we have to keep trying to prove it until
- // we reach a fixpoint. We need to do so for all cycle heads,
- // not only for the root.
- //
- // See tests/ui/traits/next-solver/cycles/fixpoint-rerun-all-cycle-heads.rs
- // for an example.
-
- // Start by clearing all provisional cache entries which depend on this
- // the current goal.
- Self::clear_dependent_provisional_results(
- &mut self.provisional_cache,
- 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(cx, input, Certainty::Yes) == result
- } else if stack_entry.has_been_used == HasBeenUsed::INDUCTIVE_CYCLE {
- Self::response_no_constraints(cx, input, Certainty::overflow(false)) == result
- } else {
- false
- };
-
- // If we did not reach a fixpoint, update the provisional result and reevaluate.
- if reached_fixpoint {
- StepResult::Done(stack_entry, result)
- } else {
- let depth = self.stack.push(StackEntry {
- has_been_used: HasBeenUsed::empty(),
- provisional_result: Some(result),
- ..stack_entry
- });
- debug_assert_eq!(self.provisional_cache[&input].stack_depth, Some(depth));
- StepResult::HasChanged
- }
- }
-
- fn response_no_constraints(
- cx: I,
- goal: CanonicalInput<I>,
- certainty: Certainty,
) -> QueryResult<I> {
- Ok(super::response_no_constraints_raw(cx, goal.max_universe, goal.variables, certainty))
+ inspect.canonical_goal_evaluation_kind(inspect::WipCanonicalGoalEvaluationKind::Overflow);
+ response_no_constraints(cx, input, Certainty::overflow(true))
}
- #[allow(rustc::potential_query_instability)]
- fn check_invariants(&self) {
- if !cfg!(debug_assertions) {
- return;
- }
-
- let SearchGraph { mode: _, stack, provisional_cache } = self;
- if stack.is_empty() {
- assert!(provisional_cache.is_empty());
- }
-
- for (depth, entry) in stack.iter_enumerated() {
- let StackEntry {
- input,
- available_depth: _,
- reached_depth: _,
- non_root_cycle_participant,
- encountered_overflow: _,
- has_been_used,
- ref nested_goals,
- provisional_result,
- } = *entry;
- let cache_entry = provisional_cache.get(&entry.input).unwrap();
- assert_eq!(cache_entry.stack_depth, Some(depth));
- if let Some(head) = non_root_cycle_participant {
- assert!(head < depth);
- assert!(nested_goals.is_empty());
- assert_ne!(stack[head].has_been_used, HasBeenUsed::empty());
-
- let mut current_root = head;
- while let Some(parent) = stack[current_root].non_root_cycle_participant {
- current_root = parent;
- }
- assert!(stack[current_root].nested_goals.contains(&input));
- }
-
- if !nested_goals.is_empty() {
- assert!(provisional_result.is_some() || !has_been_used.is_empty());
- for entry in stack.iter().take(depth.as_usize()) {
- assert_eq!(nested_goals.get(&entry.input), None);
- }
- }
- }
-
- for (&input, entry) in &self.provisional_cache {
- let ProvisionalCacheEntry { stack_depth, with_coinductive_stack, with_inductive_stack } =
- entry;
- assert!(
- stack_depth.is_some()
- || with_coinductive_stack.is_some()
- || with_inductive_stack.is_some()
- );
-
- if let &Some(stack_depth) = stack_depth {
- assert_eq!(stack[stack_depth].input, input);
- }
-
- let check_detached = |detached_entry: &DetachedEntry<I>| {
- let DetachedEntry { head, result: _ } = *detached_entry;
- assert_ne!(stack[head].has_been_used, HasBeenUsed::empty());
- };
-
- if let Some(with_coinductive_stack) = with_coinductive_stack {
- check_detached(with_coinductive_stack);
- }
+ fn on_fixpoint_overflow(cx: I, input: CanonicalInput<I>) -> QueryResult<I> {
+ response_no_constraints(cx, input, Certainty::overflow(false))
+ }
- if let Some(with_inductive_stack) = with_inductive_stack {
- check_detached(with_inductive_stack);
- }
- }
+ fn step_is_coinductive(cx: I, input: CanonicalInput<I>) -> bool {
+ input.value.goal.predicate.is_coinductive(cx)
}
}
+
+fn response_no_constraints<I: Interner>(
+ cx: I,
+ goal: CanonicalInput<I>,
+ certainty: Certainty,
+) -> QueryResult<I> {
+ Ok(super::response_no_constraints_raw(cx, goal.max_universe, goal.variables, certainty))
+}
diff --git a/compiler/rustc_query_system/src/cache.rs b/compiler/rustc_query_system/src/cache.rs
index 6e862db0b2547..d8a5bdba7b8a7 100644
--- a/compiler/rustc_query_system/src/cache.rs
+++ b/compiler/rustc_query_system/src/cache.rs
@@ -40,7 +40,7 @@ impl<Key: Eq + Hash, Value: Clone> Cache<Key, Value> {
}
}
-#[derive(Clone, Eq, PartialEq)]
+#[derive(Debug, Clone, Eq, PartialEq)]
pub struct WithDepNode<T> {
dep_node: DepNodeIndex,
cached_value: T,
diff --git a/compiler/rustc_type_ir/src/inherent.rs b/compiler/rustc_type_ir/src/inherent.rs
index de86a8536f7af..f05d626b47032 100644
--- a/compiler/rustc_type_ir/src/inherent.rs
+++ b/compiler/rustc_type_ir/src/inherent.rs
@@ -8,11 +8,10 @@ use std::hash::Hash;
use rustc_ast_ir::Mutability;
-use crate::data_structures::HashSet;
use crate::elaborate::Elaboratable;
use crate::fold::{TypeFoldable, TypeSuperFoldable};
use crate::relate::Relate;
-use crate::solve::{CacheData, CanonicalInput, QueryResult, Reveal};
+use crate::solve::Reveal;
use crate::visit::{Flags, TypeSuperVisitable, TypeVisitable};
use crate::{self as ty, CollectAndApply, Interner, UpcastFrom};
@@ -539,33 +538,6 @@ pub trait Features<I: Interner>: Copy {
fn associated_const_equality(self) -> bool;
}
-pub trait EvaluationCache<I: Interner> {
- /// Insert a final result into the global cache.
- fn insert(
- &self,
- tcx: I,
- key: CanonicalInput<I>,
- proof_tree: Option<I::CanonicalGoalEvaluationStepRef>,
- additional_depth: usize,
- encountered_overflow: bool,
- cycle_participants: HashSet<CanonicalInput<I>>,
- dep_node: I::DepNodeIndex,
- result: QueryResult<I>,
- );
-
- /// Try to fetch a cached result, checking the recursion limit
- /// and handling root goals of coinductive cycles.
- ///
- /// If this returns `Some` the cache result can be used.
- fn get(
- &self,
- tcx: I,
- key: CanonicalInput<I>,
- stack_entries: impl IntoIterator<Item = CanonicalInput<I>>,
- available_depth: usize,
- ) -> Option<CacheData<I>>;
-}
-
pub trait DefId<I: Interner>: Copy + Debug + Hash + Eq + TypeFoldable<I> {
fn is_local(self) -> bool;
diff --git a/compiler/rustc_type_ir/src/interner.rs b/compiler/rustc_type_ir/src/interner.rs
index fdd1553d389d2..14ebbb12fe2f0 100644
--- a/compiler/rustc_type_ir/src/interner.rs
+++ b/compiler/rustc_type_ir/src/interner.rs
@@ -10,8 +10,11 @@ use crate::inherent::*;
use crate::ir_print::IrPrint;
use crate::lang_items::TraitSolverLangItem;
use crate::relate::Relate;
+use crate::search_graph;
use crate::solve::inspect::CanonicalGoalEvaluationStep;
-use crate::solve::{ExternalConstraintsData, PredefinedOpaquesData, SolverMode};
+use crate::solve::{
+ CanonicalInput, ExternalConstraintsData, PredefinedOpaquesData, QueryResult, SolverMode,
+};
use crate::visit::{Flags, TypeSuperVisitable, TypeVisitable};
use crate::{self as ty};
@@ -86,6 +89,13 @@ pub trait Interner:
) -> Self::ExternalConstraints;
type DepNodeIndex;
+ type Tracked<T: Debug + Clone>: Debug;
+ fn mk_tracked<T: Debug + Clone>(
+ self,
+ data: T,
+ dep_node: Self::DepNodeIndex,
+ ) -> Self::Tracked<T>;
+ fn get_tracked<T: Debug + Clone>(self, tracked: &Self::Tracked<T>) -> T;
fn with_cached_task<T>(self, task: impl FnOnce() -> T) -> (T, Self::DepNodeIndex);
// Kinds of tys
@@ -125,8 +135,11 @@ pub trait Interner:
type Clause: Clause<Self>;
type Clauses: Copy + Debug + Hash + Eq + TypeSuperVisitable<Self> + Flags;
- type EvaluationCache: EvaluationCache<Self>;
- fn evaluation_cache(self, mode: SolverMode) -> Self::EvaluationCache;
+ fn with_global_cache<R>(
+ self,
+ mode: SolverMode,
+ f: impl FnOnce(&mut search_graph::GlobalCache<Self>) -> R,
+ ) -> R;
fn expand_abstract_consts<T: TypeFoldable<Self>>(self, t: T) -> T;
@@ -373,3 +386,32 @@ impl<T, R, E> CollectAndApply<T, R> for Result<T, E> {
})
}
}
+
+impl<I: Interner> search_graph::Cx for I {
+ type ProofTree = Option<I::CanonicalGoalEvaluationStepRef>;
+ type Input = CanonicalInput<I>;
+ type Result = QueryResult<I>;
+
+ type DepNodeIndex = I::DepNodeIndex;
+ type Tracked<T: Debug + Clone> = I::Tracked<T>;
+ fn mk_tracked<T: Debug + Clone>(
+ self,
+ data: T,
+ dep_node_index: I::DepNodeIndex,
+ ) -> I::Tracked<T> {
+ I::mk_tracked(self, data, dep_node_index)
+ }
+ fn get_tracked<T: Debug + Clone>(self, tracked: &I::Tracked<T>) -> T {
+ I::get_tracked(self, tracked)
+ }
+ fn with_cached_task<T>(self, task: impl FnOnce() -> T) -> (T, I::DepNodeIndex) {
+ I::with_cached_task(self, task)
+ }
+ fn with_global_cache<R>(
+ self,
+ mode: SolverMode,
+ f: impl FnOnce(&mut search_graph::GlobalCache<Self>) -> R,
+ ) -> R {
+ I::with_global_cache(self, mode, f)
+ }
+}
diff --git a/compiler/rustc_type_ir/src/lib.rs b/compiler/rustc_type_ir/src/lib.rs
index b14a65fc77958..37ee66fa222ae 100644
--- a/compiler/rustc_type_ir/src/lib.rs
+++ b/compiler/rustc_type_ir/src/lib.rs
@@ -30,6 +30,7 @@ pub mod lang_items;
pub mod lift;
pub mod outlives;
pub mod relate;
+pub mod search_graph;
pub mod solve;
// These modules are not `pub` since they are glob-imported.
diff --git a/compiler/rustc_type_ir/src/search_graph/global_cache.rs b/compiler/rustc_type_ir/src/search_graph/global_cache.rs
new file mode 100644
index 0000000000000..5ccda931f9c5f
--- /dev/null
+++ b/compiler/rustc_type_ir/src/search_graph/global_cache.rs
@@ -0,0 +1,118 @@
+use rustc_index::IndexVec;
+
+use super::{AvailableDepth, Cx, StackDepth, StackEntry};
+use crate::data_structures::{HashMap, HashSet};
+
+#[derive(derivative::Derivative)]
+#[derivative(Debug(bound = ""), Clone(bound = ""), Copy(bound = ""))]
+struct QueryData<X: Cx> {
+ result: X::Result,
+ proof_tree: X::ProofTree,
+}
+
+struct Success<X: Cx> {
+ data: X::Tracked<QueryData<X>>,
+ additional_depth: usize,
+}
+
+/// The cache entry for a given input.
+///
+/// This contains results whose computation never hit the
+/// recursion limit in `success`, and all results which hit
+/// the recursion limit in `with_overflow`.
+#[derive(derivative::Derivative)]
+#[derivative(Default(bound = ""))]
+struct CacheEntry<X: Cx> {
+ success: Option<Success<X>>,
+ /// We have to be careful when caching roots of cycles.
+ ///
+ /// See the doc comment of `StackEntry::cycle_participants` for more
+ /// details.
+ nested_goals: HashSet<X::Input>,
+ with_overflow: HashMap<usize, X::Tracked<QueryData<X>>>,
+}
+
+#[derive(derivative::Derivative)]
+#[derivative(Debug(bound = ""))]
+pub(super) struct CacheData<'a, X: Cx> {
+ pub(super) result: X::Result,
+ pub(super) proof_tree: X::ProofTree,
+ pub(super) additional_depth: usize,
+ pub(super) encountered_overflow: bool,
+ // FIXME: This is currently unused, but impacts the design
+ // by requiring a closure for `Cx::with_global_cache`.
+ pub(super) nested_goals: &'a HashSet<X::Input>,
+}
+
+#[derive(derivative::Derivative)]
+#[derivative(Default(bound = ""))]
+pub struct GlobalCache<X: Cx> {
+ map: HashMap<X::Input, CacheEntry<X>>,
+}
+
+impl<X: Cx> GlobalCache<X> {
+ /// Insert a final result into the global cache.
+ pub(super) fn insert(
+ &mut self,
+ cx: X,
+ input: X::Input,
+
+ result: X::Result,
+ proof_tree: X::ProofTree,
+ dep_node: X::DepNodeIndex,
+
+ additional_depth: usize,
+ encountered_overflow: bool,
+ nested_goals: &HashSet<X::Input>,
+ ) {
+ let data = cx.mk_tracked(QueryData { result, proof_tree }, dep_node);
+ let entry = self.map.entry(input).or_default();
+ entry.nested_goals.extend(nested_goals);
+ if encountered_overflow {
+ entry.with_overflow.insert(additional_depth, data);
+ } else {
+ entry.success = Some(Success { data, additional_depth });
+ }
+ }
+
+ /// Try to fetch a cached result, checking the recursion limit
+ /// and handling root goals of coinductive cycles.
+ ///
+ /// If this returns `Some` the cache result can be used.
+ pub(super) fn get<'a>(
+ &'a self,
+ cx: X,
+ input: X::Input,
+ stack: &IndexVec<StackDepth, StackEntry<X>>,
+ available_depth: AvailableDepth,
+ ) -> Option<CacheData<'a, X>> {
+ let entry = self.map.get(&input)?;
+ if stack.iter().any(|e| entry.nested_goals.contains(&e.input)) {
+ return None;
+ }
+
+ if let Some(ref success) = entry.success {
+ if available_depth.cache_entry_is_applicable(success.additional_depth) {
+ let QueryData { result, proof_tree } = cx.get_tracked(&success.data);
+ return Some(CacheData {
+ result,
+ proof_tree,
+ additional_depth: success.additional_depth,
+ encountered_overflow: false,
+ nested_goals: &entry.nested_goals,
+ });
+ }
+ }
+
+ entry.with_overflow.get(&available_depth.0).map(|e| {
+ let QueryData { result, proof_tree } = cx.get_tracked(e);
+ CacheData {
+ result,
+ proof_tree,
+ additional_depth: available_depth.0,
+ encountered_overflow: true,
+ nested_goals: &entry.nested_goals,
+ }
+ })
+ }
+}
diff --git a/compiler/rustc_type_ir/src/search_graph/mod.rs b/compiler/rustc_type_ir/src/search_graph/mod.rs
new file mode 100644
index 0000000000000..c2204becdfd71
--- /dev/null
+++ b/compiler/rustc_type_ir/src/search_graph/mod.rs
@@ -0,0 +1,605 @@
+use std::fmt::Debug;
+use std::hash::Hash;
+use std::marker::PhantomData;
+use std::mem;
+
+use rustc_index::{Idx, IndexVec};
+use tracing::debug;
+
+use crate::data_structures::{HashMap, HashSet};
+use crate::solve::SolverMode;
+
+mod global_cache;
+use global_cache::CacheData;
+pub use global_cache::GlobalCache;
+mod validate;
+
+/// The search graph does not simply use `Interner` directly
+/// to enable its fuzzing without having to stub the rest of
+/// the interner. We don't make this a super trait of `Interner`
+/// as users of the shared type library shouldn't have to care
+/// about `Input` and `Result` as they are implementation details
+/// of the search graph.
+pub trait Cx: Copy {
+ type ProofTree: Debug + Copy;
+ type Input: Debug + Eq + Hash + Copy;
+ type Result: Debug + Eq + Hash + Copy;
+
+ type DepNodeIndex;
+ type Tracked<T: Debug + Clone>: Debug;
+ fn mk_tracked<T: Debug + Clone>(
+ self,
+ data: T,
+ dep_node_index: Self::DepNodeIndex,
+ ) -> Self::Tracked<T>;
+ fn get_tracked<T: Debug + Clone>(self, tracked: &Self::Tracked<T>) -> T;
+ fn with_cached_task<T>(self, task: impl FnOnce() -> T) -> (T, Self::DepNodeIndex);
+
+ fn with_global_cache<R>(
+ self,
+ mode: SolverMode,
+ f: impl FnOnce(&mut GlobalCache<Self>) -> R,
+ ) -> R;
+}
+
+pub trait ProofTreeBuilder<X: Cx> {
+ fn try_apply_proof_tree(&mut self, proof_tree: X::ProofTree) -> bool;
+ fn on_provisional_cache_hit(&mut self);
+ fn on_cycle_in_stack(&mut self);
+ fn finalize_canonical_goal_evaluation(&mut self, cx: X) -> X::ProofTree;
+}
+
+pub trait Delegate {
+ type Cx: Cx;
+ const FIXPOINT_STEP_LIMIT: usize;
+ type ProofTreeBuilder: ProofTreeBuilder<Self::Cx>;
+
+ fn recursion_limit(cx: Self::Cx) -> usize;
+
+ fn initial_provisional_result(
+ cx: Self::Cx,
+ kind: CycleKind,
+ input: <Self::Cx as Cx>::Input,
+ ) -> <Self::Cx as Cx>::Result;
+ fn reached_fixpoint(
+ cx: Self::Cx,
+ kind: UsageKind,
+ input: <Self::Cx as Cx>::Input,
+ provisional_result: Option<<Self::Cx as Cx>::Result>,
+ result: <Self::Cx as Cx>::Result,
+ ) -> bool;
+ fn on_stack_overflow(
+ cx: Self::Cx,
+ inspect: &mut Self::ProofTreeBuilder,
+ input: <Self::Cx as Cx>::Input,
+ ) -> <Self::Cx as Cx>::Result;
+ fn on_fixpoint_overflow(
+ cx: Self::Cx,
+ input: <Self::Cx as Cx>::Input,
+ ) -> <Self::Cx as Cx>::Result;
+
+ fn step_is_coinductive(cx: Self::Cx, input: <Self::Cx as Cx>::Input) -> bool;
+}
+
+/// In the initial iteration of a cycle, we do not yet have a provisional
+/// result. In the case we return an initial provisional result depending
+/// on the kind of cycle.
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+pub enum CycleKind {
+ Coinductive,
+ Inductive,
+}
+
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+pub enum UsageKind {
+ Single(CycleKind),
+ Mixed,
+}
+impl UsageKind {
+ fn merge(self, other: Self) -> Self {
+ match (self, other) {
+ (UsageKind::Single(lhs), UsageKind::Single(rhs)) => {
+ if lhs == rhs {
+ UsageKind::Single(lhs)
+ } else {
+ UsageKind::Mixed
+ }
+ }
+ (UsageKind::Mixed, UsageKind::Mixed)
+ | (UsageKind::Mixed, UsageKind::Single(_))
+ | (UsageKind::Single(_), UsageKind::Mixed) => UsageKind::Mixed,
+ }
+ }
+}
+
+#[derive(Debug, Clone, Copy)]
+struct AvailableDepth(usize);
+impl AvailableDepth {
+ /// Returns the remaining depth allowed for nested goals.
+ ///
+ /// This is generally simply one less than the current depth.
+ /// However, if we encountered overflow, we significantly reduce
+ /// the remaining depth of all nested goals to prevent hangs
+ /// in case there is exponential blowup.
+ fn allowed_depth_for_nested<D: Delegate>(
+ cx: D::Cx,
+ stack: &IndexVec<StackDepth, StackEntry<D::Cx>>,
+ ) -> Option<AvailableDepth> {
+ if let Some(last) = stack.raw.last() {
+ if last.available_depth.0 == 0 {
+ return None;
+ }
+
+ Some(if last.encountered_overflow {
+ AvailableDepth(last.available_depth.0 / 2)
+ } else {
+ AvailableDepth(last.available_depth.0 - 1)
+ })
+ } else {
+ Some(AvailableDepth(D::recursion_limit(cx)))
+ }
+ }
+
+ /// Whether we're allowed to use a global cache entry which required
+ /// the given depth.
+ fn cache_entry_is_applicable(self, additional_depth: usize) -> bool {
+ self.0 >= additional_depth
+ }
+}
+
+rustc_index::newtype_index! {
+ #[orderable]
+ #[gate_rustc_only]
+ pub struct StackDepth {}
+}
+
+#[derive(derivative::Derivative)]
+#[derivative(Debug(bound = ""))]
+struct StackEntry<X: Cx> {
+ input: X::Input,
+
+ available_depth: AvailableDepth,
+
+ /// The maximum depth reached by this stack entry, only up-to date
+ /// for the top of the stack and lazily updated for the rest.
+ reached_depth: StackDepth,
+
+ /// Whether this entry is a non-root cycle participant.
+ ///
+ /// We must not move the result of non-root cycle participants to the
+ /// global cache. We store the highest stack depth of a head of a cycle
+ /// this goal is involved in. This necessary to soundly cache its
+ /// provisional result.
+ non_root_cycle_participant: Option<StackDepth>,
+
+ encountered_overflow: bool,
+
+ has_been_used: Option<UsageKind>,
+
+ /// We put only the root goal of a coinductive cycle into the global cache.
+ ///
+ /// If we were to use that result when later trying to prove another cycle
+ /// participant, we can end up with unstable query results.
+ ///
+ /// See tests/ui/next-solver/coinduction/incompleteness-unstable-result.rs for
+ /// an example of where this is needed.
+ ///
+ /// There can be multiple roots on the same stack, so we need to track
+ /// cycle participants per root:
+ /// ```plain
+ /// A :- B
+ /// B :- A, C
+ /// C :- D
+ /// D :- C
+ /// ```
+ nested_goals: HashSet<X::Input>,
+ /// Starts out as `None` and gets set when rerunning this
+ /// goal in case we encounter a cycle.
+ provisional_result: Option<X::Result>,
+}
+
+/// The provisional result for a goal which is not on the stack.
+#[derive(Debug)]
+struct DetachedEntry<X: Cx> {
+ /// The head of the smallest non-trivial cycle involving this entry.
+ ///
+ /// Given the following rules, when proving `A` the head for
+ /// the provisional entry of `C` would be `B`.
+ /// ```plain
+ /// A :- B
+ /// B :- C
+ /// C :- A + B + C
+ /// ```
+ head: StackDepth,
+ result: X::Result,
+}
+
+/// Stores the stack depth of a currently evaluated goal *and* already
+/// computed results for goals which depend on other goals still on the stack.
+///
+/// The provisional result may depend on whether the stack above it is inductive
+/// or coinductive. Because of this, we store separate provisional results for
+/// each case. If an provisional entry is not applicable, it may be the case
+/// that we already have provisional result while computing a goal. In this case
+/// we prefer the provisional result to potentially avoid fixpoint iterations.
+/// See tests/ui/traits/next-solver/cycles/mixed-cycles-2.rs for an example.
+///
+/// The provisional cache can theoretically result in changes to the observable behavior,
+/// see tests/ui/traits/next-solver/cycles/provisional-cache-impacts-behavior.rs.
+#[derive(derivative::Derivative)]
+#[derivative(Default(bound = ""))]
+struct ProvisionalCacheEntry<X: Cx> {
+ stack_depth: Option<StackDepth>,
+ with_inductive_stack: Option<DetachedEntry<X>>,
+ with_coinductive_stack: Option<DetachedEntry<X>>,
+}
+
+impl<X: Cx> ProvisionalCacheEntry<X> {
+ fn is_empty(&self) -> bool {
+ self.stack_depth.is_none()
+ && self.with_inductive_stack.is_none()
+ && self.with_coinductive_stack.is_none()
+ }
+}
+
+pub struct SearchGraph<D: Delegate<Cx = X>, X: Cx = <D as Delegate>::Cx> {
+ mode: SolverMode,
+ /// The stack of goals currently being computed.
+ ///
+ /// An element is *deeper* in the stack if its index is *lower*.
+ stack: IndexVec<StackDepth, StackEntry<X>>,
+ provisional_cache: HashMap<X::Input, ProvisionalCacheEntry<X>>,
+
+ _marker: PhantomData<D>,
+}
+
+impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
+ pub fn new(mode: SolverMode) -> SearchGraph<D> {
+ Self {
+ mode,
+ stack: Default::default(),
+ provisional_cache: Default::default(),
+ _marker: PhantomData,
+ }
+ }
+
+ pub fn solver_mode(&self) -> SolverMode {
+ self.mode
+ }
+
+ fn update_parent_goal(&mut self, reached_depth: StackDepth, encountered_overflow: bool) {
+ if let Some(parent) = self.stack.raw.last_mut() {
+ parent.reached_depth = parent.reached_depth.max(reached_depth);
+ parent.encountered_overflow |= encountered_overflow;
+ }
+ }
+
+ pub fn is_empty(&self) -> bool {
+ self.stack.is_empty()
+ }
+
+ fn stack_coinductive_from(
+ cx: X,
+ stack: &IndexVec<StackDepth, StackEntry<X>>,
+ head: StackDepth,
+ ) -> bool {
+ stack.raw[head.index()..].iter().all(|entry| D::step_is_coinductive(cx, entry.input))
+ }
+
+ // When encountering a solver cycle, the result of the current goal
+ // depends on goals lower on the stack.
+ //
+ // We have to therefore be careful when caching goals. Only the final result
+ // of the cycle root, i.e. the lowest goal on the stack involved in this cycle,
+ // is moved to the global cache while all others are stored in a provisional cache.
+ //
+ // We update both the head of this cycle to rerun its evaluation until
+ // we reach a fixpoint and all other cycle participants to make sure that
+ // their result does not get moved to the global cache.
+ fn tag_cycle_participants(
+ stack: &mut IndexVec<StackDepth, StackEntry<X>>,
+ usage_kind: Option<UsageKind>,
+ head: StackDepth,
+ ) {
+ if let Some(usage_kind) = usage_kind {
+ stack[head].has_been_used =
+ Some(stack[head].has_been_used.map_or(usage_kind, |prev| prev.merge(usage_kind)));
+ }
+ debug_assert!(stack[head].has_been_used.is_some());
+
+ // The current root of these cycles. Note that this may not be the final
+ // root in case a later goal depends on a goal higher up the stack.
+ let mut current_root = head;
+ while let Some(parent) = stack[current_root].non_root_cycle_participant {
+ current_root = parent;
+ debug_assert!(stack[current_root].has_been_used.is_some());
+ }
+
+ let (stack, cycle_participants) = stack.raw.split_at_mut(head.index() + 1);
+ let current_cycle_root = &mut stack[current_root.as_usize()];
+ for entry in cycle_participants {
+ entry.non_root_cycle_participant = entry.non_root_cycle_participant.max(Some(head));
+ current_cycle_root.nested_goals.insert(entry.input);
+ current_cycle_root.nested_goals.extend(mem::take(&mut entry.nested_goals));
+ }
+ }
+
+ fn clear_dependent_provisional_results(
+ provisional_cache: &mut HashMap<X::Input, ProvisionalCacheEntry<X>>,
+ head: StackDepth,
+ ) {
+ #[allow(rustc::potential_query_instability)]
+ provisional_cache.retain(|_, entry| {
+ if entry.with_coinductive_stack.as_ref().is_some_and(|p| p.head == head) {
+ entry.with_coinductive_stack.take();
+ }
+ if entry.with_inductive_stack.as_ref().is_some_and(|p| p.head == head) {
+ entry.with_inductive_stack.take();
+ }
+ !entry.is_empty()
+ });
+ }
+
+ /// Probably the most involved method of the whole solver.
+ ///
+ /// Given some goal which is proven via the `prove_goal` closure, this
+ /// handles caching, overflow, and coinductive cycles.
+ pub fn with_new_goal(
+ &mut self,
+ cx: X,
+ input: X::Input,
+ inspect: &mut D::ProofTreeBuilder,
+ mut prove_goal: impl FnMut(&mut Self, &mut D::ProofTreeBuilder) -> X::Result,
+ ) -> X::Result {
+ self.check_invariants();
+ // Check for overflow.
+ let Some(available_depth) = AvailableDepth::allowed_depth_for_nested::<D>(cx, &self.stack)
+ else {
+ if let Some(last) = self.stack.raw.last_mut() {
+ last.encountered_overflow = true;
+ }
+
+ debug!("encountered stack overflow");
+ return D::on_stack_overflow(cx, inspect, input);
+ };
+
+ if let Some(result) = self.lookup_global_cache(cx, input, available_depth, inspect) {
+ return result;
+ }
+
+ // Check whether the goal is in the provisional cache.
+ // The provisional result may rely on the path to its cycle roots,
+ // so we have to check the path of the current goal matches that of
+ // the cache entry.
+ let cache_entry = self.provisional_cache.entry(input).or_default();
+ if let Some(entry) = cache_entry
+ .with_coinductive_stack
+ .as_ref()
+ .filter(|p| Self::stack_coinductive_from(cx, &self.stack, p.head))
+ .or_else(|| {
+ cache_entry
+ .with_inductive_stack
+ .as_ref()
+ .filter(|p| !Self::stack_coinductive_from(cx, &self.stack, p.head))
+ })
+ {
+ debug!("provisional cache hit");
+ // We have a nested goal which is already in the provisional cache, use
+ // its result. We do not provide any usage kind as that should have been
+ // already set correctly while computing the cache entry.
+ inspect.on_provisional_cache_hit();
+ Self::tag_cycle_participants(&mut self.stack, None, entry.head);
+ return entry.result;
+ } else if let Some(stack_depth) = cache_entry.stack_depth {
+ debug!("encountered cycle with depth {stack_depth:?}");
+ // We have a nested goal which directly relies on a goal deeper in the stack.
+ //
+ // We start by tagging all cycle participants, as that's necessary for caching.
+ //
+ // Finally we can return either the provisional response or the initial response
+ // in case we're in the first fixpoint iteration for this goal.
+ inspect.on_cycle_in_stack();
+
+ let is_coinductive_cycle = Self::stack_coinductive_from(cx, &self.stack, stack_depth);
+ let cycle_kind =
+ if is_coinductive_cycle { CycleKind::Coinductive } else { CycleKind::Inductive };
+ Self::tag_cycle_participants(
+ &mut self.stack,
+ Some(UsageKind::Single(cycle_kind)),
+ stack_depth,
+ );
+
+ // Return the provisional result or, if we're in the first iteration,
+ // start with no constraints.
+ return if let Some(result) = self.stack[stack_depth].provisional_result {
+ result
+ } else {
+ D::initial_provisional_result(cx, cycle_kind, input)
+ };
+ } else {
+ // No entry, we push this goal on the stack and try to prove it.
+ let depth = self.stack.next_index();
+ let entry = StackEntry {
+ input,
+ available_depth,
+ reached_depth: depth,
+ non_root_cycle_participant: None,
+ encountered_overflow: false,
+ has_been_used: None,
+ nested_goals: Default::default(),
+ provisional_result: None,
+ };
+ assert_eq!(self.stack.push(entry), depth);
+ cache_entry.stack_depth = Some(depth);
+ };
+
+ // This is for global caching, so we properly track query dependencies.
+ // Everything that affects the `result` should be performed within this
+ // `with_anon_task` closure. If computing this goal depends on something
+ // not tracked by the cache key and from outside of this anon task, it
+ // must not be added to the global cache. Notably, this is the case for
+ // trait solver cycles participants.
+ let ((final_entry, result), dep_node) = cx.with_cached_task(|| {
+ for _ in 0..D::FIXPOINT_STEP_LIMIT {
+ match self.fixpoint_step_in_task(cx, input, inspect, &mut prove_goal) {
+ StepResult::Done(final_entry, result) => return (final_entry, result),
+ StepResult::HasChanged => debug!("fixpoint changed provisional results"),
+ }
+ }
+
+ debug!("canonical cycle overflow");
+ let current_entry = self.stack.pop().unwrap();
+ debug_assert!(current_entry.has_been_used.is_none());
+ let result = D::on_fixpoint_overflow(cx, input);
+ (current_entry, result)
+ });
+
+ let proof_tree = inspect.finalize_canonical_goal_evaluation(cx);
+
+ self.update_parent_goal(final_entry.reached_depth, final_entry.encountered_overflow);
+
+ // We're now done with this goal. In case this goal is involved in a larger cycle
+ // do not remove it from the provisional cache and update its provisional result.
+ // We only add the root of cycles to the global cache.
+ if let Some(head) = final_entry.non_root_cycle_participant {
+ let coinductive_stack = Self::stack_coinductive_from(cx, &self.stack, head);
+
+ let entry = self.provisional_cache.get_mut(&input).unwrap();
+ entry.stack_depth = None;
+ if coinductive_stack {
+ entry.with_coinductive_stack = Some(DetachedEntry { head, result });
+ } else {
+ entry.with_inductive_stack = Some(DetachedEntry { head, result });
+ }
+ } else {
+ // When encountering a cycle, both inductive and coinductive, we only
+ // move the root into the global cache. We also store all other cycle
+ // participants involved.
+ //
+ // We must not use the global cache entry of a root goal if a cycle
+ // participant is on the stack. This is necessary to prevent unstable
+ // results. See the comment of `StackEntry::nested_goals` for
+ // more details.
+ self.provisional_cache.remove(&input);
+ let additional_depth = final_entry.reached_depth.as_usize() - self.stack.len();
+ cx.with_global_cache(self.mode, |cache| {
+ cache.insert(
+ cx,
+ input,
+ result,
+ proof_tree,
+ dep_node,
+ additional_depth,
+ final_entry.encountered_overflow,
+ &final_entry.nested_goals,
+ )
+ })
+ }
+
+ self.check_invariants();
+
+ result
+ }
+
+ /// Try to fetch a previously computed result from the global cache,
+ /// making sure to only do so if it would match the result of reevaluating
+ /// this goal.
+ fn lookup_global_cache(
+ &mut self,
+ cx: X,
+ input: X::Input,
+ available_depth: AvailableDepth,
+ inspect: &mut D::ProofTreeBuilder,
+ ) -> Option<X::Result> {
+ cx.with_global_cache(self.mode, |cache| {
+ let CacheData {
+ result,
+ proof_tree,
+ additional_depth,
+ encountered_overflow,
+ nested_goals: _, // FIXME: consider nested goals here.
+ } = cache.get(cx, input, &self.stack, available_depth)?;
+
+ // If we're building a proof tree and the current cache entry does not
+ // contain a proof tree, we do not use the entry but instead recompute
+ // the goal. We simply overwrite the existing entry once we're done,
+ // caching the proof tree.
+ if !inspect.try_apply_proof_tree(proof_tree) {
+ return None;
+ }
+
+ // Update the reached depth of the current goal to make sure
+ // its state is the same regardless of whether we've used the
+ // global cache or not.
+ let reached_depth = self.stack.next_index().plus(additional_depth);
+ self.update_parent_goal(reached_depth, encountered_overflow);
+
+ debug!("global cache hit");
+ Some(result)
+ })
+ }
+}
+
+enum StepResult<X: Cx> {
+ Done(StackEntry<X>, X::Result),
+ HasChanged,
+}
+
+impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
+ /// When we encounter a coinductive cycle, we have to fetch the
+ /// result of that cycle while we are still computing it. Because
+ /// 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.
+ fn fixpoint_step_in_task<F>(
+ &mut self,
+ cx: X,
+ input: X::Input,
+ inspect: &mut D::ProofTreeBuilder,
+ prove_goal: &mut F,
+ ) -> StepResult<X>
+ where
+ F: FnMut(&mut Self, &mut D::ProofTreeBuilder) -> X::Result,
+ {
+ let result = prove_goal(self, inspect);
+ let stack_entry = self.stack.pop().unwrap();
+ debug_assert_eq!(stack_entry.input, input);
+
+ // If the current goal is not the root of a cycle, we are done.
+ let Some(usage_kind) = stack_entry.has_been_used else {
+ return StepResult::Done(stack_entry, result);
+ };
+
+ // If it is a cycle head, we have to keep trying to prove it until
+ // we reach a fixpoint. We need to do so for all cycle heads,
+ // not only for the root.
+ //
+ // See tests/ui/traits/next-solver/cycles/fixpoint-rerun-all-cycle-heads.rs
+ // for an example.
+
+ // Start by clearing all provisional cache entries which depend on this
+ // the current goal.
+ Self::clear_dependent_provisional_results(
+ &mut self.provisional_cache,
+ 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.
+ //
+ // If we did not reach a fixpoint, update the provisional result and reevaluate.
+ if D::reached_fixpoint(cx, usage_kind, input, stack_entry.provisional_result, result) {
+ StepResult::Done(stack_entry, result)
+ } else {
+ let depth = self.stack.push(StackEntry {
+ has_been_used: None,
+ provisional_result: Some(result),
+ ..stack_entry
+ });
+ debug_assert_eq!(self.provisional_cache[&input].stack_depth, Some(depth));
+ StepResult::HasChanged
+ }
+ }
+}
diff --git a/compiler/rustc_type_ir/src/search_graph/validate.rs b/compiler/rustc_type_ir/src/search_graph/validate.rs
new file mode 100644
index 0000000000000..1ae806834ba7d
--- /dev/null
+++ b/compiler/rustc_type_ir/src/search_graph/validate.rs
@@ -0,0 +1,75 @@
+use super::*;
+
+impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
+ #[allow(rustc::potential_query_instability)]
+ pub(super) fn check_invariants(&self) {
+ if !cfg!(debug_assertions) {
+ return;
+ }
+
+ let SearchGraph { mode: _, stack, provisional_cache, _marker } = self;
+ if stack.is_empty() {
+ assert!(provisional_cache.is_empty());
+ }
+
+ for (depth, entry) in stack.iter_enumerated() {
+ let StackEntry {
+ input,
+ available_depth: _,
+ reached_depth: _,
+ non_root_cycle_participant,
+ encountered_overflow: _,
+ has_been_used,
+ ref nested_goals,
+ provisional_result,
+ } = *entry;
+ let cache_entry = provisional_cache.get(&entry.input).unwrap();
+ assert_eq!(cache_entry.stack_depth, Some(depth));
+ if let Some(head) = non_root_cycle_participant {
+ assert!(head < depth);
+ assert!(nested_goals.is_empty());
+ assert_ne!(stack[head].has_been_used, None);
+
+ let mut current_root = head;
+ while let Some(parent) = stack[current_root].non_root_cycle_participant {
+ current_root = parent;
+ }
+ assert!(stack[current_root].nested_goals.contains(&input));
+ }
+
+ if !nested_goals.is_empty() {
+ assert!(provisional_result.is_some() || has_been_used.is_some());
+ for entry in stack.iter().take(depth.as_usize()) {
+ assert_eq!(nested_goals.get(&entry.input), None);
+ }
+ }
+ }
+
+ for (&input, entry) in &self.provisional_cache {
+ let ProvisionalCacheEntry { stack_depth, with_coinductive_stack, with_inductive_stack } =
+ entry;
+ assert!(
+ stack_depth.is_some()
+ || with_coinductive_stack.is_some()
+ || with_inductive_stack.is_some()
+ );
+
+ if let &Some(stack_depth) = stack_depth {
+ assert_eq!(stack[stack_depth].input, input);
+ }
+
+ let check_detached = |detached_entry: &DetachedEntry<X>| {
+ let DetachedEntry { head, result: _ } = *detached_entry;
+ assert_ne!(stack[head].has_been_used, None);
+ };
+
+ if let Some(with_coinductive_stack) = with_coinductive_stack {
+ check_detached(with_coinductive_stack);
+ }
+
+ if let Some(with_inductive_stack) = with_inductive_stack {
+ check_detached(with_inductive_stack);
+ }
+ }
+ }
+}