Rollup merge of #128828 - lcnr:search-graph-11, r=compiler-errors
`-Znext-solver` caching This PR has two major changes while also fixing multiple issues found via fuzzing. The main optimization is the ability to not discard provisional cache entries when popping the highest cycle head the entry depends on. This fixes the hang in Fuchsia with `-Znext-solver=coherence`. It also bails if the result of a fixpoint iteration is ambiguous, even without reaching a fixpoint. This is necessary to avoid exponential blowup if a coinductive cycle results in ambiguity, e.g. due to unknowable candidates in coherence. Updating stack entries pretty much exclusively happens lazily now, so `fn check_invariants` ended up being mostly useless and I've removed it. See https://gist.github.com/lcnr/8de338fdb2685581e17727bbfab0622a for the invariants we would be able to assert with it. For a general overview, see the in-process update of the relevant rustc-dev-guide chapter: https://hackmd.io/1ALkSjKlSCyQG-dVb_PUHw r? ```@compiler-errors```
This commit is contained in:
commit
59ad2aec49
13 changed files with 895 additions and 634 deletions
|
@ -61,10 +61,6 @@ macro_rules! arena_types {
|
|||
[] dtorck_constraint: rustc_middle::traits::query::DropckConstraint<'tcx>,
|
||||
[] candidate_step: rustc_middle::traits::query::CandidateStep<'tcx>,
|
||||
[] autoderef_bad_ty: rustc_middle::traits::query::MethodAutoderefBadTy<'tcx>,
|
||||
[] canonical_goal_evaluation:
|
||||
rustc_type_ir::solve::inspect::CanonicalGoalEvaluationStep<
|
||||
rustc_middle::ty::TyCtxt<'tcx>
|
||||
>,
|
||||
[] query_region_constraints: rustc_middle::infer::canonical::QueryRegionConstraints<'tcx>,
|
||||
[] type_op_subtype:
|
||||
rustc_middle::infer::canonical::Canonical<'tcx,
|
||||
|
|
|
@ -107,8 +107,6 @@ impl<'tcx> Interner for TyCtxt<'tcx> {
|
|||
self.mk_predefined_opaques_in_body(data)
|
||||
}
|
||||
type DefiningOpaqueTypes = &'tcx ty::List<LocalDefId>;
|
||||
type CanonicalGoalEvaluationStepRef =
|
||||
&'tcx solve::inspect::CanonicalGoalEvaluationStep<TyCtxt<'tcx>>;
|
||||
type CanonicalVars = CanonicalVarInfos<'tcx>;
|
||||
fn mk_canonical_var_infos(self, infos: &[ty::CanonicalVarInfo<Self>]) -> Self::CanonicalVars {
|
||||
self.mk_canonical_var_infos(infos)
|
||||
|
@ -277,13 +275,6 @@ impl<'tcx> Interner for TyCtxt<'tcx> {
|
|||
self.debug_assert_args_compatible(def_id, args);
|
||||
}
|
||||
|
||||
fn intern_canonical_goal_evaluation_step(
|
||||
self,
|
||||
step: solve::inspect::CanonicalGoalEvaluationStep<TyCtxt<'tcx>>,
|
||||
) -> &'tcx solve::inspect::CanonicalGoalEvaluationStep<TyCtxt<'tcx>> {
|
||||
self.arena.alloc(step)
|
||||
}
|
||||
|
||||
fn mk_type_list_from_iter<I, T>(self, args: I) -> T::Output
|
||||
where
|
||||
I: Iterator<Item = T>,
|
||||
|
|
|
@ -5,11 +5,10 @@
|
|||
//! see the comment on [ProofTreeBuilder].
|
||||
|
||||
use std::marker::PhantomData;
|
||||
use std::mem;
|
||||
|
||||
use derive_where::derive_where;
|
||||
use rustc_type_ir::inherent::*;
|
||||
use rustc_type_ir::{self as ty, search_graph, Interner};
|
||||
use rustc_type_ir::{self as ty, Interner};
|
||||
|
||||
use crate::delegate::SolverDelegate;
|
||||
use crate::solve::eval_ctxt::canonical;
|
||||
|
@ -94,31 +93,10 @@ impl<I: Interner> WipGoalEvaluation<I> {
|
|||
}
|
||||
}
|
||||
|
||||
#[derive_where(PartialEq, Eq; I: Interner)]
|
||||
pub(in crate::solve) enum WipCanonicalGoalEvaluationKind<I: Interner> {
|
||||
Overflow,
|
||||
CycleInStack,
|
||||
ProvisionalCacheHit,
|
||||
Interned { final_revision: I::CanonicalGoalEvaluationStepRef },
|
||||
}
|
||||
|
||||
impl<I: Interner> std::fmt::Debug for WipCanonicalGoalEvaluationKind<I> {
|
||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||
match self {
|
||||
Self::Overflow => write!(f, "Overflow"),
|
||||
Self::CycleInStack => write!(f, "CycleInStack"),
|
||||
Self::ProvisionalCacheHit => write!(f, "ProvisionalCacheHit"),
|
||||
Self::Interned { final_revision: _ } => {
|
||||
f.debug_struct("Interned").finish_non_exhaustive()
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[derive_where(PartialEq, Eq, Debug; I: Interner)]
|
||||
struct WipCanonicalGoalEvaluation<I: Interner> {
|
||||
goal: CanonicalInput<I>,
|
||||
kind: Option<WipCanonicalGoalEvaluationKind<I>>,
|
||||
encountered_overflow: bool,
|
||||
/// Only used for uncached goals. After we finished evaluating
|
||||
/// the goal, this is interned and moved into `kind`.
|
||||
final_revision: Option<WipCanonicalGoalEvaluationStep<I>>,
|
||||
|
@ -127,25 +105,17 @@ struct WipCanonicalGoalEvaluation<I: Interner> {
|
|||
|
||||
impl<I: Interner> WipCanonicalGoalEvaluation<I> {
|
||||
fn finalize(self) -> inspect::CanonicalGoalEvaluation<I> {
|
||||
// We've already interned the final revision in
|
||||
// `fn finalize_canonical_goal_evaluation`.
|
||||
assert!(self.final_revision.is_none());
|
||||
let kind = match self.kind.unwrap() {
|
||||
WipCanonicalGoalEvaluationKind::Overflow => {
|
||||
inspect::CanonicalGoalEvaluation {
|
||||
goal: self.goal,
|
||||
kind: if self.encountered_overflow {
|
||||
assert!(self.final_revision.is_none());
|
||||
inspect::CanonicalGoalEvaluationKind::Overflow
|
||||
}
|
||||
WipCanonicalGoalEvaluationKind::CycleInStack => {
|
||||
inspect::CanonicalGoalEvaluationKind::CycleInStack
|
||||
}
|
||||
WipCanonicalGoalEvaluationKind::ProvisionalCacheHit => {
|
||||
inspect::CanonicalGoalEvaluationKind::ProvisionalCacheHit
|
||||
}
|
||||
WipCanonicalGoalEvaluationKind::Interned { final_revision } => {
|
||||
} else {
|
||||
let final_revision = self.final_revision.unwrap().finalize();
|
||||
inspect::CanonicalGoalEvaluationKind::Evaluation { final_revision }
|
||||
}
|
||||
};
|
||||
|
||||
inspect::CanonicalGoalEvaluation { goal: self.goal, kind, result: self.result.unwrap() }
|
||||
},
|
||||
result: self.result.unwrap(),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -308,7 +278,7 @@ impl<D: SolverDelegate<Interner = I>, I: Interner> ProofTreeBuilder<D> {
|
|||
) -> ProofTreeBuilder<D> {
|
||||
self.nested(|| WipCanonicalGoalEvaluation {
|
||||
goal,
|
||||
kind: None,
|
||||
encountered_overflow: false,
|
||||
final_revision: None,
|
||||
result: None,
|
||||
})
|
||||
|
@ -329,11 +299,11 @@ impl<D: SolverDelegate<Interner = I>, I: Interner> ProofTreeBuilder<D> {
|
|||
}
|
||||
}
|
||||
|
||||
pub fn canonical_goal_evaluation_kind(&mut self, kind: WipCanonicalGoalEvaluationKind<I>) {
|
||||
pub fn canonical_goal_evaluation_overflow(&mut self) {
|
||||
if let Some(this) = self.as_mut() {
|
||||
match this {
|
||||
DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluation) => {
|
||||
assert_eq!(canonical_goal_evaluation.kind.replace(kind), None);
|
||||
canonical_goal_evaluation.encountered_overflow = true;
|
||||
}
|
||||
_ => unreachable!(),
|
||||
};
|
||||
|
@ -547,51 +517,3 @@ 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!(),
|
||||
})
|
||||
}
|
||||
}
|
||||
|
|
|
@ -1,12 +1,13 @@
|
|||
use std::convert::Infallible;
|
||||
use std::marker::PhantomData;
|
||||
|
||||
use rustc_type_ir::inherent::*;
|
||||
use rustc_type_ir::search_graph::{self, CycleKind, UsageKind};
|
||||
use rustc_type_ir::search_graph::{self, PathKind};
|
||||
use rustc_type_ir::solve::{CanonicalInput, Certainty, QueryResult};
|
||||
use rustc_type_ir::Interner;
|
||||
|
||||
use super::inspect::{self, ProofTreeBuilder};
|
||||
use super::FIXPOINT_STEP_LIMIT;
|
||||
use super::inspect::ProofTreeBuilder;
|
||||
use super::{has_no_inference_or_external_constraints, FIXPOINT_STEP_LIMIT};
|
||||
use crate::delegate::SolverDelegate;
|
||||
|
||||
/// This type is never constructed. We only use it to implement `search_graph::Delegate`
|
||||
|
@ -22,43 +23,48 @@ where
|
|||
{
|
||||
type Cx = D::Interner;
|
||||
|
||||
const ENABLE_PROVISIONAL_CACHE: bool = true;
|
||||
type ValidationScope = Infallible;
|
||||
fn enter_validation_scope(
|
||||
_cx: Self::Cx,
|
||||
_input: CanonicalInput<I>,
|
||||
) -> Option<Self::ValidationScope> {
|
||||
None
|
||||
}
|
||||
|
||||
const FIXPOINT_STEP_LIMIT: usize = FIXPOINT_STEP_LIMIT;
|
||||
|
||||
type ProofTreeBuilder = ProofTreeBuilder<D>;
|
||||
fn inspect_is_noop(inspect: &mut Self::ProofTreeBuilder) -> bool {
|
||||
inspect.is_noop()
|
||||
}
|
||||
|
||||
const DIVIDE_AVAILABLE_DEPTH_ON_OVERFLOW: usize = 4;
|
||||
fn recursion_limit(cx: I) -> usize {
|
||||
cx.recursion_limit()
|
||||
}
|
||||
|
||||
fn initial_provisional_result(
|
||||
cx: I,
|
||||
kind: CycleKind,
|
||||
kind: PathKind,
|
||||
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)),
|
||||
PathKind::Coinductive => response_no_constraints(cx, input, Certainty::Yes),
|
||||
PathKind::Inductive => response_no_constraints(cx, input, Certainty::overflow(false)),
|
||||
}
|
||||
}
|
||||
|
||||
fn reached_fixpoint(
|
||||
cx: I,
|
||||
kind: UsageKind,
|
||||
fn is_initial_provisional_result(
|
||||
cx: Self::Cx,
|
||||
kind: PathKind,
|
||||
input: CanonicalInput<I>,
|
||||
provisional_result: Option<QueryResult<I>>,
|
||||
result: QueryResult<I>,
|
||||
) -> bool {
|
||||
if let Some(r) = provisional_result {
|
||||
r == result
|
||||
} else {
|
||||
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,
|
||||
match kind {
|
||||
PathKind::Coinductive => response_no_constraints(cx, input, Certainty::Yes) == result,
|
||||
PathKind::Inductive => {
|
||||
response_no_constraints(cx, input, Certainty::overflow(false)) == result
|
||||
}
|
||||
}
|
||||
}
|
||||
|
@ -68,7 +74,7 @@ where
|
|||
inspect: &mut ProofTreeBuilder<D>,
|
||||
input: CanonicalInput<I>,
|
||||
) -> QueryResult<I> {
|
||||
inspect.canonical_goal_evaluation_kind(inspect::WipCanonicalGoalEvaluationKind::Overflow);
|
||||
inspect.canonical_goal_evaluation_overflow();
|
||||
response_no_constraints(cx, input, Certainty::overflow(true))
|
||||
}
|
||||
|
||||
|
@ -76,6 +82,22 @@ where
|
|||
response_no_constraints(cx, input, Certainty::overflow(false))
|
||||
}
|
||||
|
||||
fn is_ambiguous_result(result: QueryResult<I>) -> bool {
|
||||
result.is_ok_and(|response| {
|
||||
has_no_inference_or_external_constraints(response)
|
||||
&& matches!(response.value.certainty, Certainty::Maybe(_))
|
||||
})
|
||||
}
|
||||
|
||||
fn propagate_ambiguity(
|
||||
cx: I,
|
||||
for_input: CanonicalInput<I>,
|
||||
from_result: QueryResult<I>,
|
||||
) -> QueryResult<I> {
|
||||
let certainty = from_result.unwrap().value.certainty;
|
||||
response_no_constraints(cx, for_input, certainty)
|
||||
}
|
||||
|
||||
fn step_is_coinductive(cx: I, input: CanonicalInput<I>) -> bool {
|
||||
input.value.goal.predicate.is_coinductive(cx)
|
||||
}
|
||||
|
|
|
@ -334,13 +334,9 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
|
|||
|
||||
pub fn candidates(&'a self) -> Vec<InspectCandidate<'a, 'tcx>> {
|
||||
let mut candidates = vec![];
|
||||
let last_eval_step = match self.evaluation_kind {
|
||||
inspect::CanonicalGoalEvaluationKind::Overflow
|
||||
| inspect::CanonicalGoalEvaluationKind::CycleInStack
|
||||
| inspect::CanonicalGoalEvaluationKind::ProvisionalCacheHit => {
|
||||
warn!("unexpected root evaluation: {:?}", self.evaluation_kind);
|
||||
return vec![];
|
||||
}
|
||||
let last_eval_step = match &self.evaluation_kind {
|
||||
// An annoying edge case in case the recursion limit is 0.
|
||||
inspect::CanonicalGoalEvaluationKind::Overflow => return vec![],
|
||||
inspect::CanonicalGoalEvaluationKind::Evaluation { final_revision } => final_revision,
|
||||
};
|
||||
|
||||
|
|
|
@ -8,7 +8,7 @@ use derive_where::derive_where;
|
|||
use rustc_macros::{HashStable_NoContext, TyDecodable, TyEncodable};
|
||||
#[cfg(feature = "nightly")]
|
||||
use rustc_serialize::Decodable;
|
||||
use tracing::debug;
|
||||
use tracing::instrument;
|
||||
|
||||
use crate::data_structures::SsoHashSet;
|
||||
use crate::fold::{FallibleTypeFolder, TypeFoldable, TypeFolder, TypeSuperFoldable};
|
||||
|
@ -817,28 +817,20 @@ impl<'a, I: Interner> ArgFolder<'a, I> {
|
|||
/// As indicated in the diagram, here the same type `&'a i32` is instantiated once, but in the
|
||||
/// first case we do not increase the De Bruijn index and in the second case we do. The reason
|
||||
/// is that only in the second case have we passed through a fn binder.
|
||||
#[instrument(level = "trace", skip(self), fields(binders_passed = self.binders_passed), ret)]
|
||||
fn shift_vars_through_binders<T: TypeFoldable<I>>(&self, val: T) -> T {
|
||||
debug!(
|
||||
"shift_vars(val={:?}, binders_passed={:?}, has_escaping_bound_vars={:?})",
|
||||
val,
|
||||
self.binders_passed,
|
||||
val.has_escaping_bound_vars()
|
||||
);
|
||||
|
||||
if self.binders_passed == 0 || !val.has_escaping_bound_vars() {
|
||||
return val;
|
||||
val
|
||||
} else {
|
||||
ty::fold::shift_vars(self.cx, val, self.binders_passed)
|
||||
}
|
||||
|
||||
let result = ty::fold::shift_vars(TypeFolder::cx(self), val, self.binders_passed);
|
||||
debug!("shift_vars: shifted result = {:?}", result);
|
||||
|
||||
result
|
||||
}
|
||||
|
||||
fn shift_region_through_binders(&self, region: I::Region) -> I::Region {
|
||||
if self.binders_passed == 0 || !region.has_escaping_bound_vars() {
|
||||
return region;
|
||||
region
|
||||
} else {
|
||||
ty::fold::shift_region(self.cx, region, self.binders_passed)
|
||||
}
|
||||
ty::fold::shift_region(self.cx, region, self.binders_passed)
|
||||
}
|
||||
}
|
||||
|
|
|
@ -48,7 +48,7 @@
|
|||
use std::mem;
|
||||
|
||||
use rustc_index::{Idx, IndexVec};
|
||||
use tracing::debug;
|
||||
use tracing::instrument;
|
||||
|
||||
use crate::data_structures::Lrc;
|
||||
use crate::inherent::*;
|
||||
|
@ -417,15 +417,14 @@ pub fn shift_region<I: Interner>(cx: I, region: I::Region, amount: u32) -> I::Re
|
|||
}
|
||||
}
|
||||
|
||||
#[instrument(level = "trace", skip(cx), ret)]
|
||||
pub fn shift_vars<I: Interner, T>(cx: I, value: T, amount: u32) -> T
|
||||
where
|
||||
T: TypeFoldable<I>,
|
||||
{
|
||||
debug!("shift_vars(value={:?}, amount={})", value, amount);
|
||||
|
||||
if amount == 0 || !value.has_escaping_bound_vars() {
|
||||
return value;
|
||||
value
|
||||
} else {
|
||||
value.fold_with(&mut Shifter::new(cx, amount))
|
||||
}
|
||||
|
||||
value.fold_with(&mut Shifter::new(cx, amount))
|
||||
}
|
||||
|
|
|
@ -11,7 +11,6 @@ use crate::inherent::*;
|
|||
use crate::ir_print::IrPrint;
|
||||
use crate::lang_items::TraitSolverLangItem;
|
||||
use crate::relate::Relate;
|
||||
use crate::solve::inspect::CanonicalGoalEvaluationStep;
|
||||
use crate::solve::{
|
||||
CanonicalInput, ExternalConstraintsData, PredefinedOpaquesData, QueryResult, SolverMode,
|
||||
};
|
||||
|
@ -65,11 +64,6 @@ pub trait Interner:
|
|||
+ Eq
|
||||
+ TypeVisitable<Self>
|
||||
+ SliceLike<Item = Self::LocalDefId>;
|
||||
type CanonicalGoalEvaluationStepRef: Copy
|
||||
+ Debug
|
||||
+ Hash
|
||||
+ Eq
|
||||
+ Deref<Target = CanonicalGoalEvaluationStep<Self>>;
|
||||
|
||||
type CanonicalVars: Copy
|
||||
+ Debug
|
||||
|
@ -177,11 +171,6 @@ pub trait Interner:
|
|||
|
||||
fn debug_assert_args_compatible(self, def_id: Self::DefId, args: Self::GenericArgs);
|
||||
|
||||
fn intern_canonical_goal_evaluation_step(
|
||||
self,
|
||||
step: CanonicalGoalEvaluationStep<Self>,
|
||||
) -> Self::CanonicalGoalEvaluationStepRef;
|
||||
|
||||
fn mk_type_list_from_iter<I, T>(self, args: I) -> T::Output
|
||||
where
|
||||
I: Iterator<Item = T>,
|
||||
|
@ -390,7 +379,6 @@ 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>;
|
||||
|
||||
|
|
|
@ -1,18 +1,17 @@
|
|||
use derive_where::derive_where;
|
||||
use rustc_index::IndexVec;
|
||||
|
||||
use super::{AvailableDepth, Cx, StackDepth, StackEntry};
|
||||
use crate::data_structures::{HashMap, HashSet};
|
||||
|
||||
#[derive_where(Debug, Clone, Copy; X: Cx)]
|
||||
struct QueryData<X: Cx> {
|
||||
result: X::Result,
|
||||
proof_tree: X::ProofTree,
|
||||
}
|
||||
use super::{AvailableDepth, Cx, NestedGoals};
|
||||
use crate::data_structures::HashMap;
|
||||
|
||||
struct Success<X: Cx> {
|
||||
data: X::Tracked<QueryData<X>>,
|
||||
additional_depth: usize,
|
||||
nested_goals: NestedGoals<X>,
|
||||
result: X::Tracked<X::Result>,
|
||||
}
|
||||
|
||||
struct WithOverflow<X: Cx> {
|
||||
nested_goals: NestedGoals<X>,
|
||||
result: X::Tracked<X::Result>,
|
||||
}
|
||||
|
||||
/// The cache entry for a given input.
|
||||
|
@ -23,24 +22,15 @@ struct Success<X: Cx> {
|
|||
#[derive_where(Default; X: Cx)]
|
||||
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>>>,
|
||||
with_overflow: HashMap<usize, WithOverflow<X>>,
|
||||
}
|
||||
|
||||
#[derive_where(Debug; X: Cx)]
|
||||
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`.
|
||||
#[allow(dead_code)]
|
||||
pub(super) nested_goals: &'a HashSet<X::Input>,
|
||||
pub(super) nested_goals: &'a NestedGoals<X>,
|
||||
}
|
||||
#[derive_where(Default; X: Cx)]
|
||||
pub struct GlobalCache<X: Cx> {
|
||||
|
@ -55,20 +45,21 @@ impl<X: Cx> GlobalCache<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>,
|
||||
nested_goals: NestedGoals<X>,
|
||||
) {
|
||||
let data = cx.mk_tracked(QueryData { result, proof_tree }, dep_node);
|
||||
let result = cx.mk_tracked(result, 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);
|
||||
let with_overflow = WithOverflow { nested_goals, result };
|
||||
let prev = entry.with_overflow.insert(additional_depth, with_overflow);
|
||||
assert!(prev.is_none());
|
||||
} else {
|
||||
entry.success = Some(Success { data, additional_depth });
|
||||
let prev = entry.success.replace(Success { additional_depth, nested_goals, result });
|
||||
assert!(prev.is_none());
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -80,36 +71,37 @@ impl<X: Cx> GlobalCache<X> {
|
|||
&'a self,
|
||||
cx: X,
|
||||
input: X::Input,
|
||||
stack: &IndexVec<StackDepth, StackEntry<X>>,
|
||||
available_depth: AvailableDepth,
|
||||
mut candidate_is_applicable: impl FnMut(&NestedGoals<X>) -> bool,
|
||||
) -> 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);
|
||||
if let Some(Success { additional_depth, ref nested_goals, ref result }) = entry.success {
|
||||
if available_depth.cache_entry_is_applicable(additional_depth)
|
||||
&& candidate_is_applicable(nested_goals)
|
||||
{
|
||||
return Some(CacheData {
|
||||
result,
|
||||
proof_tree,
|
||||
additional_depth: success.additional_depth,
|
||||
result: cx.get_tracked(&result),
|
||||
additional_depth,
|
||||
encountered_overflow: false,
|
||||
nested_goals: &entry.nested_goals,
|
||||
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,
|
||||
let additional_depth = available_depth.0;
|
||||
if let Some(WithOverflow { nested_goals, result }) =
|
||||
entry.with_overflow.get(&additional_depth)
|
||||
{
|
||||
if candidate_is_applicable(nested_goals) {
|
||||
return Some(CacheData {
|
||||
result: cx.get_tracked(result),
|
||||
additional_depth,
|
||||
encountered_overflow: true,
|
||||
nested_goals,
|
||||
});
|
||||
}
|
||||
})
|
||||
}
|
||||
|
||||
None
|
||||
}
|
||||
}
|
||||
|
|
File diff suppressed because it is too large
Load diff
|
@ -1,75 +0,0 @@
|
|||
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);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
|
@ -69,9 +69,7 @@ pub struct CanonicalGoalEvaluation<I: Interner> {
|
|||
#[derive_where(PartialEq, Eq, Hash, Debug; I: Interner)]
|
||||
pub enum CanonicalGoalEvaluationKind<I: Interner> {
|
||||
Overflow,
|
||||
CycleInStack,
|
||||
ProvisionalCacheHit,
|
||||
Evaluation { final_revision: I::CanonicalGoalEvaluationStepRef },
|
||||
Evaluation { final_revision: CanonicalGoalEvaluationStep<I> },
|
||||
}
|
||||
|
||||
#[derive_where(PartialEq, Eq, Hash, Debug; I: Interner)]
|
||||
|
|
|
@ -340,11 +340,3 @@ impl MaybeCause {
|
|||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[derive_where(PartialEq, Eq, Debug; I: Interner)]
|
||||
pub struct CacheData<I: Interner> {
|
||||
pub result: QueryResult<I>,
|
||||
pub proof_tree: Option<I::CanonicalGoalEvaluationStepRef>,
|
||||
pub additional_depth: usize,
|
||||
pub encountered_overflow: bool,
|
||||
}
|
||||
|
|
Loading…
Add table
Reference in a new issue