Auto merge of #142774 - lcnr:search_graph-2, r=oli-obk
`evaluate_goal` avoid unnecessary step
based on rust-lang/rust#142617.
This does not mess with the debug logging for the trait solver and is a very nice cleanup for rust-lang/rust#142735. E.g. for
```rust
#[derive(Clone)]
struct Wrapper<T>(T);
#[derive(Clone)]
struct Nested; // using a separate type to avoid the fast paths
fn is_clone<T: Clone>() {}
fn main() {
is_clone::<Wrapper<Nested>>();
}
```
We get the following proof tree with `RUSTC_LOG=rustc_type_ir::search_graph=debug,rustc_next_trait_solver=debug`
```
rustc_next_trait_solver::solve::eval_ctxt::evaluate_root_goal goal=Goal { param_env: ParamEnv { caller_bounds: [] }, predicate: Binder { value: TraitPredicate(<Wrapper<Nested> as std::clone::Clone>, polarity:Positive), bound_vars: [] } }, generate_proof_tree=No, span=src/main.rs:7:5: 7:34 (#0), stalled_on=None
rustc_type_ir::search_graph::evaluate_goal input=CanonicalQueryInput { canonical: Canonical { value: QueryInput { goal: Goal { param_env: ParamEnv { caller_bounds: [] }, predicate: Binder { value: TraitPredicate(<Wrapper<Nested> as std::clone::Clone>, polarity:Positive), bound_vars: [] } }, predefined_opaques_in_body: PredefinedOpaques(PredefinedOpaquesData { opaque_types: [] }) }, max_universe: U0, variables: [] }, typing_mode: Analysis { defining_opaque_types_and_generators: [] } }, step_kind_from_parent=Unknown
rustc_next_trait_solver::solve::eval_ctxt::probe::enter source=Impl(DefId(0:10 ~ main[21d2]::{impl#0}))
rustc_next_trait_solver::solve::eval_ctxt::add_goal source=ImplWhereBound, goal=Goal { param_env: ParamEnv { caller_bounds: [] }, predicate: Binder { value: TraitPredicate(<_ as std::marker::Sized>, polarity:Positive), bound_vars: [] } }
rustc_next_trait_solver::solve::eval_ctxt::add_goal source=ImplWhereBound, goal=Goal { param_env: ParamEnv { caller_bounds: [] }, predicate: Binder { value: TraitPredicate(<_ as std::clone::Clone>, polarity:Positive), bound_vars: [] } }
rustc_type_ir::search_graph::evaluate_goal input=CanonicalQueryInput { canonical: Canonical { value: QueryInput { goal: Goal { param_env: ParamEnv { caller_bounds: [] }, predicate: Binder { value: TraitPredicate(<Nested as std::clone::Clone>, polarity:Positive), bound_vars: [] } }, predefined_opaques_in_body: PredefinedOpaques(PredefinedOpaquesData { opaque_types: [] }) }, max_universe: U0, variables: [] }, typing_mode: Analysis { defining_opaque_types_and_generators: [] } }, step_kind_from_parent=Unknown
0ms DEBUG rustc_type_ir::search_graph global cache hit, required_depth=0
0ms DEBUG rustc_type_ir::search_graph return=Ok(Canonical { value: Response { certainty: Yes, var_values: CanonicalVarValues { var_values: [] }, external_constraints: ExternalConstraints(ExternalConstraintsData { region_constraints: [], opaque_types: [], normalization_nested_goals: NestedNormalizationGoals([]) }) }, max_universe: U0, variables: [] })
rustc_next_trait_solver::solve::eval_ctxt::probe::enter source=BuiltinImpl(Misc)
rustc_next_trait_solver::solve::trait_goals::merge_trait_candidates candidates=[Candidate { source: Impl(DefId(0:10 ~ main[21d2]::{impl#0})), result: Canonical { value: Response { certainty: Yes, var_values: CanonicalVarValues { var_values: [] }, external_constraints: ExternalConstraints(ExternalConstraintsData { region_constraints: [], opaque_types: [], normalization_nested_goals: NestedNormalizationGoals([]) }) }, max_universe: U0, variables: [] } }]
0ms DEBUG rustc_next_trait_solver::solve::trait_goals return=Ok((Canonical { value: Response { certainty: Yes, var_values: CanonicalVarValues { var_values: [] }, external_constraints: ExternalConstraints(ExternalConstraintsData { region_constraints: [], opaque_types: [], normalization_nested_goals: NestedNormalizationGoals([]) }) }, max_universe: U0, variables: [] }, Some(Misc)))
0ms DEBUG rustc_type_ir::search_graph insert global cache, evaluation_result=EvaluationResult { encountered_overflow: false, required_depth: 1, heads: CycleHeads { heads: {} }, nested_goals: NestedGoals { nested_goals: {} }, result: Ok(Canonical { value: Response { certainty: Yes, var_values: CanonicalVarValues { var_values: [] }, external_constraints: ExternalConstraints(ExternalConstraintsData { region_constraints: [], opaque_types: [], normalization_nested_goals: NestedNormalizationGoals([]) }) }, max_universe: U0, variables: [] }) }
0ms DEBUG rustc_type_ir::search_graph return=Ok(Canonical { value: Response { certainty: Yes, var_values: CanonicalVarValues { var_values: [] }, external_constraints: ExternalConstraints(ExternalConstraintsData { region_constraints: [], opaque_types: [], normalization_nested_goals: NestedNormalizationGoals([]) }) }, max_universe: U0, variables: [] })
```
This commit is contained in:
@@ -3,7 +3,7 @@ use std::ops::ControlFlow;
|
|||||||
|
|
||||||
#[cfg(feature = "nightly")]
|
#[cfg(feature = "nightly")]
|
||||||
use rustc_macros::HashStable_NoContext;
|
use rustc_macros::HashStable_NoContext;
|
||||||
use rustc_type_ir::data_structures::{HashMap, HashSet, ensure_sufficient_stack};
|
use rustc_type_ir::data_structures::{HashMap, HashSet};
|
||||||
use rustc_type_ir::fast_reject::DeepRejectCtxt;
|
use rustc_type_ir::fast_reject::DeepRejectCtxt;
|
||||||
use rustc_type_ir::inherent::*;
|
use rustc_type_ir::inherent::*;
|
||||||
use rustc_type_ir::relate::Relate;
|
use rustc_type_ir::relate::Relate;
|
||||||
@@ -336,13 +336,12 @@ where
|
|||||||
|
|
||||||
/// Creates a nested evaluation context that shares the same search graph as the
|
/// Creates a nested evaluation context that shares the same search graph as the
|
||||||
/// one passed in. This is suitable for evaluation, granted that the search graph
|
/// one passed in. This is suitable for evaluation, granted that the search graph
|
||||||
/// has had the nested goal recorded on its stack ([`SearchGraph::with_new_goal`]),
|
/// has had the nested goal recorded on its stack. This method only be used by
|
||||||
/// but it's preferable to use other methods that call this one rather than this
|
/// `search_graph::Delegate::compute_goal`.
|
||||||
/// method directly.
|
|
||||||
///
|
///
|
||||||
/// This function takes care of setting up the inference context, setting the anchor,
|
/// This function takes care of setting up the inference context, setting the anchor,
|
||||||
/// and registering opaques from the canonicalized input.
|
/// and registering opaques from the canonicalized input.
|
||||||
fn enter_canonical<R>(
|
pub(super) fn enter_canonical<R>(
|
||||||
cx: I,
|
cx: I,
|
||||||
search_graph: &'a mut SearchGraph<D>,
|
search_graph: &'a mut SearchGraph<D>,
|
||||||
canonical_input: CanonicalInput<I>,
|
canonical_input: CanonicalInput<I>,
|
||||||
@@ -398,56 +397,6 @@ where
|
|||||||
result
|
result
|
||||||
}
|
}
|
||||||
|
|
||||||
/// The entry point of the solver.
|
|
||||||
///
|
|
||||||
/// This function deals with (coinductive) cycles, overflow, and caching
|
|
||||||
/// and then calls [`EvalCtxt::compute_goal`] which contains the actual
|
|
||||||
/// logic of the solver.
|
|
||||||
///
|
|
||||||
/// Instead of calling this function directly, use either [EvalCtxt::evaluate_goal]
|
|
||||||
/// if you're inside of the solver or [SolverDelegateEvalExt::evaluate_root_goal] if you're
|
|
||||||
/// outside of it.
|
|
||||||
#[instrument(level = "debug", skip(cx, search_graph, goal_evaluation), ret)]
|
|
||||||
fn evaluate_canonical_goal(
|
|
||||||
cx: I,
|
|
||||||
search_graph: &'a mut SearchGraph<D>,
|
|
||||||
canonical_input: CanonicalInput<I>,
|
|
||||||
step_kind_from_parent: PathKind,
|
|
||||||
goal_evaluation: &mut ProofTreeBuilder<D>,
|
|
||||||
) -> QueryResult<I> {
|
|
||||||
let mut canonical_goal_evaluation =
|
|
||||||
goal_evaluation.new_canonical_goal_evaluation(canonical_input);
|
|
||||||
|
|
||||||
// Deal with overflow, caching, and coinduction.
|
|
||||||
//
|
|
||||||
// The actual solver logic happens in `ecx.compute_goal`.
|
|
||||||
let result = ensure_sufficient_stack(|| {
|
|
||||||
search_graph.with_new_goal(
|
|
||||||
cx,
|
|
||||||
canonical_input,
|
|
||||||
step_kind_from_parent,
|
|
||||||
&mut canonical_goal_evaluation,
|
|
||||||
|search_graph, cx, canonical_input, canonical_goal_evaluation| {
|
|
||||||
EvalCtxt::enter_canonical(
|
|
||||||
cx,
|
|
||||||
search_graph,
|
|
||||||
canonical_input,
|
|
||||||
canonical_goal_evaluation,
|
|
||||||
|ecx, goal| {
|
|
||||||
let result = ecx.compute_goal(goal);
|
|
||||||
ecx.inspect.query_result(result);
|
|
||||||
result
|
|
||||||
},
|
|
||||||
)
|
|
||||||
},
|
|
||||||
)
|
|
||||||
});
|
|
||||||
|
|
||||||
canonical_goal_evaluation.query_result(result);
|
|
||||||
goal_evaluation.canonical_goal_evaluation(canonical_goal_evaluation);
|
|
||||||
result
|
|
||||||
}
|
|
||||||
|
|
||||||
/// Recursively evaluates `goal`, returning whether any inference vars have
|
/// Recursively evaluates `goal`, returning whether any inference vars have
|
||||||
/// been constrained and the certainty of the result.
|
/// been constrained and the certainty of the result.
|
||||||
fn evaluate_goal(
|
fn evaluate_goal(
|
||||||
@@ -501,18 +450,16 @@ where
|
|||||||
let (orig_values, canonical_goal) = self.canonicalize_goal(goal);
|
let (orig_values, canonical_goal) = self.canonicalize_goal(goal);
|
||||||
let mut goal_evaluation =
|
let mut goal_evaluation =
|
||||||
self.inspect.new_goal_evaluation(goal, &orig_values, goal_evaluation_kind);
|
self.inspect.new_goal_evaluation(goal, &orig_values, goal_evaluation_kind);
|
||||||
let canonical_response = EvalCtxt::evaluate_canonical_goal(
|
let canonical_result = self.search_graph.evaluate_goal(
|
||||||
self.cx(),
|
self.cx(),
|
||||||
self.search_graph,
|
|
||||||
canonical_goal,
|
canonical_goal,
|
||||||
self.step_kind_for_source(source),
|
self.step_kind_for_source(source),
|
||||||
&mut goal_evaluation,
|
&mut goal_evaluation,
|
||||||
);
|
);
|
||||||
let response = match canonical_response {
|
goal_evaluation.query_result(canonical_result);
|
||||||
Err(e) => {
|
|
||||||
self.inspect.goal_evaluation(goal_evaluation);
|
self.inspect.goal_evaluation(goal_evaluation);
|
||||||
return Err(e);
|
let response = match canonical_result {
|
||||||
}
|
Err(e) => return Err(e),
|
||||||
Ok(response) => response,
|
Ok(response) => response,
|
||||||
};
|
};
|
||||||
|
|
||||||
@@ -521,7 +468,6 @@ where
|
|||||||
|
|
||||||
let (normalization_nested_goals, certainty) =
|
let (normalization_nested_goals, certainty) =
|
||||||
self.instantiate_and_apply_query_response(goal.param_env, &orig_values, response);
|
self.instantiate_and_apply_query_response(goal.param_env, &orig_values, response);
|
||||||
self.inspect.goal_evaluation(goal_evaluation);
|
|
||||||
|
|
||||||
// FIXME: We previously had an assert here that checked that recomputing
|
// FIXME: We previously had an assert here that checked that recomputing
|
||||||
// a goal after applying its constraints did not change its response.
|
// a goal after applying its constraints did not change its response.
|
||||||
@@ -582,7 +528,7 @@ where
|
|||||||
Ok((normalization_nested_goals, GoalEvaluation { certainty, has_changed, stalled_on }))
|
Ok((normalization_nested_goals, GoalEvaluation { certainty, has_changed, stalled_on }))
|
||||||
}
|
}
|
||||||
|
|
||||||
fn compute_goal(&mut self, goal: Goal<I, I::Predicate>) -> QueryResult<I> {
|
pub(super) fn compute_goal(&mut self, goal: Goal<I, I::Predicate>) -> QueryResult<I> {
|
||||||
let Goal { param_env, predicate } = goal;
|
let Goal { param_env, predicate } = goal;
|
||||||
let kind = predicate.kind();
|
let kind = predicate.kind();
|
||||||
if let Some(kind) = kind.no_bound_vars() {
|
if let Some(kind) = kind.no_bound_vars() {
|
||||||
|
|||||||
@@ -13,8 +13,7 @@ use rustc_type_ir::{self as ty, Interner};
|
|||||||
use crate::delegate::SolverDelegate;
|
use crate::delegate::SolverDelegate;
|
||||||
use crate::solve::eval_ctxt::canonical;
|
use crate::solve::eval_ctxt::canonical;
|
||||||
use crate::solve::{
|
use crate::solve::{
|
||||||
CanonicalInput, Certainty, GenerateProofTree, Goal, GoalEvaluationKind, GoalSource,
|
Certainty, GenerateProofTree, Goal, GoalEvaluationKind, GoalSource, QueryResult, inspect,
|
||||||
QueryResult, inspect,
|
|
||||||
};
|
};
|
||||||
|
|
||||||
/// The core data structure when building proof trees.
|
/// The core data structure when building proof trees.
|
||||||
@@ -54,7 +53,6 @@ where
|
|||||||
enum DebugSolver<I: Interner> {
|
enum DebugSolver<I: Interner> {
|
||||||
Root,
|
Root,
|
||||||
GoalEvaluation(WipGoalEvaluation<I>),
|
GoalEvaluation(WipGoalEvaluation<I>),
|
||||||
CanonicalGoalEvaluation(WipCanonicalGoalEvaluation<I>),
|
|
||||||
CanonicalGoalEvaluationStep(WipCanonicalGoalEvaluationStep<I>),
|
CanonicalGoalEvaluationStep(WipCanonicalGoalEvaluationStep<I>),
|
||||||
}
|
}
|
||||||
|
|
||||||
@@ -64,12 +62,6 @@ impl<I: Interner> From<WipGoalEvaluation<I>> for DebugSolver<I> {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
impl<I: Interner> From<WipCanonicalGoalEvaluation<I>> for DebugSolver<I> {
|
|
||||||
fn from(g: WipCanonicalGoalEvaluation<I>) -> DebugSolver<I> {
|
|
||||||
DebugSolver::CanonicalGoalEvaluation(g)
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
impl<I: Interner> From<WipCanonicalGoalEvaluationStep<I>> for DebugSolver<I> {
|
impl<I: Interner> From<WipCanonicalGoalEvaluationStep<I>> for DebugSolver<I> {
|
||||||
fn from(g: WipCanonicalGoalEvaluationStep<I>) -> DebugSolver<I> {
|
fn from(g: WipCanonicalGoalEvaluationStep<I>) -> DebugSolver<I> {
|
||||||
DebugSolver::CanonicalGoalEvaluationStep(g)
|
DebugSolver::CanonicalGoalEvaluationStep(g)
|
||||||
@@ -80,7 +72,10 @@ impl<I: Interner> From<WipCanonicalGoalEvaluationStep<I>> for DebugSolver<I> {
|
|||||||
struct WipGoalEvaluation<I: Interner> {
|
struct WipGoalEvaluation<I: Interner> {
|
||||||
pub uncanonicalized_goal: Goal<I, I::Predicate>,
|
pub uncanonicalized_goal: Goal<I, I::Predicate>,
|
||||||
pub orig_values: Vec<I::GenericArg>,
|
pub orig_values: Vec<I::GenericArg>,
|
||||||
pub evaluation: Option<WipCanonicalGoalEvaluation<I>>,
|
pub encountered_overflow: bool,
|
||||||
|
/// After we finished evaluating this is moved into `kind`.
|
||||||
|
pub final_revision: Option<WipCanonicalGoalEvaluationStep<I>>,
|
||||||
|
pub result: Option<QueryResult<I>>,
|
||||||
}
|
}
|
||||||
|
|
||||||
impl<I: Interner> WipGoalEvaluation<I> {
|
impl<I: Interner> WipGoalEvaluation<I> {
|
||||||
@@ -88,31 +83,12 @@ impl<I: Interner> WipGoalEvaluation<I> {
|
|||||||
inspect::GoalEvaluation {
|
inspect::GoalEvaluation {
|
||||||
uncanonicalized_goal: self.uncanonicalized_goal,
|
uncanonicalized_goal: self.uncanonicalized_goal,
|
||||||
orig_values: self.orig_values,
|
orig_values: self.orig_values,
|
||||||
evaluation: self.evaluation.unwrap().finalize(),
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
#[derive_where(PartialEq, Eq, Debug; I: Interner)]
|
|
||||||
struct WipCanonicalGoalEvaluation<I: Interner> {
|
|
||||||
goal: CanonicalInput<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>>,
|
|
||||||
result: Option<QueryResult<I>>,
|
|
||||||
}
|
|
||||||
|
|
||||||
impl<I: Interner> WipCanonicalGoalEvaluation<I> {
|
|
||||||
fn finalize(self) -> inspect::CanonicalGoalEvaluation<I> {
|
|
||||||
inspect::CanonicalGoalEvaluation {
|
|
||||||
goal: self.goal,
|
|
||||||
kind: if self.encountered_overflow {
|
kind: if self.encountered_overflow {
|
||||||
assert!(self.final_revision.is_none());
|
assert!(self.final_revision.is_none());
|
||||||
inspect::CanonicalGoalEvaluationKind::Overflow
|
inspect::GoalEvaluationKind::Overflow
|
||||||
} else {
|
} else {
|
||||||
let final_revision = self.final_revision.unwrap().finalize();
|
let final_revision = self.final_revision.unwrap().finalize();
|
||||||
inspect::CanonicalGoalEvaluationKind::Evaluation { final_revision }
|
inspect::GoalEvaluationKind::Evaluation { final_revision }
|
||||||
},
|
},
|
||||||
result: self.result.unwrap(),
|
result: self.result.unwrap(),
|
||||||
}
|
}
|
||||||
@@ -256,55 +232,27 @@ impl<D: SolverDelegate<Interner = I>, I: Interner> ProofTreeBuilder<D> {
|
|||||||
|
|
||||||
pub(in crate::solve) fn new_goal_evaluation(
|
pub(in crate::solve) fn new_goal_evaluation(
|
||||||
&mut self,
|
&mut self,
|
||||||
goal: Goal<I, I::Predicate>,
|
uncanonicalized_goal: Goal<I, I::Predicate>,
|
||||||
orig_values: &[I::GenericArg],
|
orig_values: &[I::GenericArg],
|
||||||
kind: GoalEvaluationKind,
|
kind: GoalEvaluationKind,
|
||||||
) -> ProofTreeBuilder<D> {
|
) -> ProofTreeBuilder<D> {
|
||||||
self.opt_nested(|| match kind {
|
self.opt_nested(|| match kind {
|
||||||
GoalEvaluationKind::Root => Some(WipGoalEvaluation {
|
GoalEvaluationKind::Root => Some(WipGoalEvaluation {
|
||||||
uncanonicalized_goal: goal,
|
uncanonicalized_goal,
|
||||||
orig_values: orig_values.to_vec(),
|
orig_values: orig_values.to_vec(),
|
||||||
evaluation: None,
|
encountered_overflow: false,
|
||||||
|
final_revision: None,
|
||||||
|
result: None,
|
||||||
}),
|
}),
|
||||||
GoalEvaluationKind::Nested => None,
|
GoalEvaluationKind::Nested => None,
|
||||||
})
|
})
|
||||||
}
|
}
|
||||||
|
|
||||||
pub(crate) fn new_canonical_goal_evaluation(
|
|
||||||
&mut self,
|
|
||||||
goal: CanonicalInput<I>,
|
|
||||||
) -> ProofTreeBuilder<D> {
|
|
||||||
self.nested(|| WipCanonicalGoalEvaluation {
|
|
||||||
goal,
|
|
||||||
encountered_overflow: false,
|
|
||||||
final_revision: None,
|
|
||||||
result: None,
|
|
||||||
})
|
|
||||||
}
|
|
||||||
|
|
||||||
pub(crate) 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()) {
|
|
||||||
(
|
|
||||||
DebugSolver::GoalEvaluation(goal_evaluation),
|
|
||||||
DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluation),
|
|
||||||
) => {
|
|
||||||
let prev = goal_evaluation.evaluation.replace(canonical_goal_evaluation);
|
|
||||||
assert_eq!(prev, None);
|
|
||||||
}
|
|
||||||
_ => unreachable!(),
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
pub(crate) fn canonical_goal_evaluation_overflow(&mut self) {
|
pub(crate) fn canonical_goal_evaluation_overflow(&mut self) {
|
||||||
if let Some(this) = self.as_mut() {
|
if let Some(this) = self.as_mut() {
|
||||||
match this {
|
match this {
|
||||||
DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluation) => {
|
DebugSolver::GoalEvaluation(goal_evaluation) => {
|
||||||
canonical_goal_evaluation.encountered_overflow = true;
|
goal_evaluation.encountered_overflow = true;
|
||||||
}
|
}
|
||||||
_ => unreachable!(),
|
_ => unreachable!(),
|
||||||
};
|
};
|
||||||
@@ -343,10 +291,10 @@ impl<D: SolverDelegate<Interner = I>, I: Interner> ProofTreeBuilder<D> {
|
|||||||
if let Some(this) = self.as_mut() {
|
if let Some(this) = self.as_mut() {
|
||||||
match (this, *goal_evaluation_step.state.unwrap()) {
|
match (this, *goal_evaluation_step.state.unwrap()) {
|
||||||
(
|
(
|
||||||
DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluations),
|
DebugSolver::GoalEvaluation(goal_evaluation),
|
||||||
DebugSolver::CanonicalGoalEvaluationStep(goal_evaluation_step),
|
DebugSolver::CanonicalGoalEvaluationStep(goal_evaluation_step),
|
||||||
) => {
|
) => {
|
||||||
canonical_goal_evaluations.final_revision = Some(goal_evaluation_step);
|
goal_evaluation.final_revision = Some(goal_evaluation_step);
|
||||||
}
|
}
|
||||||
_ => unreachable!(),
|
_ => unreachable!(),
|
||||||
}
|
}
|
||||||
@@ -489,8 +437,8 @@ impl<D: SolverDelegate<Interner = I>, I: Interner> ProofTreeBuilder<D> {
|
|||||||
pub(crate) fn query_result(&mut self, result: QueryResult<I>) {
|
pub(crate) fn query_result(&mut self, result: QueryResult<I>) {
|
||||||
if let Some(this) = self.as_mut() {
|
if let Some(this) = self.as_mut() {
|
||||||
match this {
|
match this {
|
||||||
DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluation) => {
|
DebugSolver::GoalEvaluation(goal_evaluation) => {
|
||||||
assert_eq!(canonical_goal_evaluation.result.replace(result), None);
|
assert_eq!(goal_evaluation.result.replace(result), None);
|
||||||
}
|
}
|
||||||
DebugSolver::CanonicalGoalEvaluationStep(evaluation_step) => {
|
DebugSolver::CanonicalGoalEvaluationStep(evaluation_step) => {
|
||||||
assert_eq!(
|
assert_eq!(
|
||||||
|
|||||||
@@ -1,13 +1,14 @@
|
|||||||
use std::convert::Infallible;
|
use std::convert::Infallible;
|
||||||
use std::marker::PhantomData;
|
use std::marker::PhantomData;
|
||||||
|
|
||||||
|
use rustc_type_ir::data_structures::ensure_sufficient_stack;
|
||||||
use rustc_type_ir::search_graph::{self, PathKind};
|
use rustc_type_ir::search_graph::{self, PathKind};
|
||||||
use rustc_type_ir::solve::{CanonicalInput, Certainty, NoSolution, QueryResult};
|
use rustc_type_ir::solve::{CanonicalInput, Certainty, NoSolution, QueryResult};
|
||||||
use rustc_type_ir::{Interner, TypingMode};
|
use rustc_type_ir::{Interner, TypingMode};
|
||||||
|
|
||||||
use super::inspect::ProofTreeBuilder;
|
|
||||||
use super::{FIXPOINT_STEP_LIMIT, has_no_inference_or_external_constraints};
|
|
||||||
use crate::delegate::SolverDelegate;
|
use crate::delegate::SolverDelegate;
|
||||||
|
use crate::solve::inspect::ProofTreeBuilder;
|
||||||
|
use crate::solve::{EvalCtxt, FIXPOINT_STEP_LIMIT, has_no_inference_or_external_constraints};
|
||||||
|
|
||||||
/// This type is never constructed. We only use it to implement `search_graph::Delegate`
|
/// 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.
|
/// for all types which impl `SolverDelegate` and doing it directly fails in coherence.
|
||||||
@@ -80,8 +81,8 @@ where
|
|||||||
|
|
||||||
fn on_stack_overflow(
|
fn on_stack_overflow(
|
||||||
cx: I,
|
cx: I,
|
||||||
inspect: &mut ProofTreeBuilder<D>,
|
|
||||||
input: CanonicalInput<I>,
|
input: CanonicalInput<I>,
|
||||||
|
inspect: &mut ProofTreeBuilder<D>,
|
||||||
) -> QueryResult<I> {
|
) -> QueryResult<I> {
|
||||||
inspect.canonical_goal_evaluation_overflow();
|
inspect.canonical_goal_evaluation_overflow();
|
||||||
response_no_constraints(cx, input, Certainty::overflow(true))
|
response_no_constraints(cx, input, Certainty::overflow(true))
|
||||||
@@ -106,6 +107,21 @@ where
|
|||||||
let certainty = from_result.unwrap().value.certainty;
|
let certainty = from_result.unwrap().value.certainty;
|
||||||
response_no_constraints(cx, for_input, certainty)
|
response_no_constraints(cx, for_input, certainty)
|
||||||
}
|
}
|
||||||
|
|
||||||
|
fn compute_goal(
|
||||||
|
search_graph: &mut SearchGraph<D>,
|
||||||
|
cx: I,
|
||||||
|
input: CanonicalInput<I>,
|
||||||
|
inspect: &mut Self::ProofTreeBuilder,
|
||||||
|
) -> QueryResult<I> {
|
||||||
|
ensure_sufficient_stack(|| {
|
||||||
|
EvalCtxt::enter_canonical(cx, search_graph, input, inspect, |ecx, goal| {
|
||||||
|
let result = ecx.compute_goal(goal);
|
||||||
|
ecx.inspect.query_result(result);
|
||||||
|
result
|
||||||
|
})
|
||||||
|
})
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
fn response_no_constraints<I: Interner>(
|
fn response_no_constraints<I: Interner>(
|
||||||
|
|||||||
@@ -37,7 +37,7 @@ pub struct InspectGoal<'a, 'tcx> {
|
|||||||
orig_values: Vec<ty::GenericArg<'tcx>>,
|
orig_values: Vec<ty::GenericArg<'tcx>>,
|
||||||
goal: Goal<'tcx, ty::Predicate<'tcx>>,
|
goal: Goal<'tcx, ty::Predicate<'tcx>>,
|
||||||
result: Result<Certainty, NoSolution>,
|
result: Result<Certainty, NoSolution>,
|
||||||
evaluation_kind: inspect::CanonicalGoalEvaluationKind<TyCtxt<'tcx>>,
|
evaluation_kind: inspect::GoalEvaluationKind<TyCtxt<'tcx>>,
|
||||||
normalizes_to_term_hack: Option<NormalizesToTermHack<'tcx>>,
|
normalizes_to_term_hack: Option<NormalizesToTermHack<'tcx>>,
|
||||||
source: GoalSource,
|
source: GoalSource,
|
||||||
}
|
}
|
||||||
@@ -393,8 +393,8 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
|
|||||||
let mut candidates = vec![];
|
let mut candidates = vec![];
|
||||||
let last_eval_step = match &self.evaluation_kind {
|
let last_eval_step = match &self.evaluation_kind {
|
||||||
// An annoying edge case in case the recursion limit is 0.
|
// An annoying edge case in case the recursion limit is 0.
|
||||||
inspect::CanonicalGoalEvaluationKind::Overflow => return vec![],
|
inspect::GoalEvaluationKind::Overflow => return vec![],
|
||||||
inspect::CanonicalGoalEvaluationKind::Evaluation { final_revision } => final_revision,
|
inspect::GoalEvaluationKind::Evaluation { final_revision } => final_revision,
|
||||||
};
|
};
|
||||||
|
|
||||||
let mut nested_goals = vec![];
|
let mut nested_goals = vec![];
|
||||||
@@ -426,10 +426,10 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
|
|||||||
) -> Self {
|
) -> Self {
|
||||||
let infcx = <&SolverDelegate<'tcx>>::from(infcx);
|
let infcx = <&SolverDelegate<'tcx>>::from(infcx);
|
||||||
|
|
||||||
let inspect::GoalEvaluation { uncanonicalized_goal, orig_values, evaluation } = root;
|
let inspect::GoalEvaluation { uncanonicalized_goal, orig_values, kind, result } = root;
|
||||||
// If there's a normalizes-to goal, AND the evaluation result with the result of
|
// If there's a normalizes-to goal, AND the evaluation result with the result of
|
||||||
// constraining the normalizes-to RHS and computing the nested goals.
|
// constraining the normalizes-to RHS and computing the nested goals.
|
||||||
let result = evaluation.result.and_then(|ok| {
|
let result = result.and_then(|ok| {
|
||||||
let nested_goals_certainty =
|
let nested_goals_certainty =
|
||||||
term_hack_and_nested_certainty.map_or(Ok(Certainty::Yes), |(_, c)| c)?;
|
term_hack_and_nested_certainty.map_or(Ok(Certainty::Yes), |(_, c)| c)?;
|
||||||
Ok(ok.value.certainty.and(nested_goals_certainty))
|
Ok(ok.value.certainty.and(nested_goals_certainty))
|
||||||
@@ -441,7 +441,7 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
|
|||||||
orig_values,
|
orig_values,
|
||||||
goal: eager_resolve_vars(infcx, uncanonicalized_goal),
|
goal: eager_resolve_vars(infcx, uncanonicalized_goal),
|
||||||
result,
|
result,
|
||||||
evaluation_kind: evaluation.kind,
|
evaluation_kind: kind,
|
||||||
normalizes_to_term_hack: term_hack_and_nested_certainty.map(|(n, _)| n),
|
normalizes_to_term_hack: term_hack_and_nested_certainty.map(|(n, _)| n),
|
||||||
source,
|
source,
|
||||||
}
|
}
|
||||||
|
|||||||
@@ -21,7 +21,7 @@ use std::marker::PhantomData;
|
|||||||
use derive_where::derive_where;
|
use derive_where::derive_where;
|
||||||
#[cfg(feature = "nightly")]
|
#[cfg(feature = "nightly")]
|
||||||
use rustc_macros::{Decodable_NoContext, Encodable_NoContext, HashStable_NoContext};
|
use rustc_macros::{Decodable_NoContext, Encodable_NoContext, HashStable_NoContext};
|
||||||
use tracing::debug;
|
use tracing::{debug, instrument};
|
||||||
|
|
||||||
use crate::data_structures::HashMap;
|
use crate::data_structures::HashMap;
|
||||||
|
|
||||||
@@ -56,7 +56,7 @@ pub trait Cx: Copy {
|
|||||||
fn evaluation_is_concurrent(&self) -> bool;
|
fn evaluation_is_concurrent(&self) -> bool;
|
||||||
}
|
}
|
||||||
|
|
||||||
pub trait Delegate {
|
pub trait Delegate: Sized {
|
||||||
type Cx: Cx;
|
type Cx: Cx;
|
||||||
/// Whether to use the provisional cache. Set to `false` by a fuzzer when
|
/// Whether to use the provisional cache. Set to `false` by a fuzzer when
|
||||||
/// validating the search graph.
|
/// validating the search graph.
|
||||||
@@ -94,8 +94,8 @@ pub trait Delegate {
|
|||||||
) -> bool;
|
) -> bool;
|
||||||
fn on_stack_overflow(
|
fn on_stack_overflow(
|
||||||
cx: Self::Cx,
|
cx: Self::Cx,
|
||||||
inspect: &mut Self::ProofTreeBuilder,
|
|
||||||
input: <Self::Cx as Cx>::Input,
|
input: <Self::Cx as Cx>::Input,
|
||||||
|
inspect: &mut Self::ProofTreeBuilder,
|
||||||
) -> <Self::Cx as Cx>::Result;
|
) -> <Self::Cx as Cx>::Result;
|
||||||
fn on_fixpoint_overflow(
|
fn on_fixpoint_overflow(
|
||||||
cx: Self::Cx,
|
cx: Self::Cx,
|
||||||
@@ -108,6 +108,13 @@ pub trait Delegate {
|
|||||||
for_input: <Self::Cx as Cx>::Input,
|
for_input: <Self::Cx as Cx>::Input,
|
||||||
from_result: <Self::Cx as Cx>::Result,
|
from_result: <Self::Cx as Cx>::Result,
|
||||||
) -> <Self::Cx as Cx>::Result;
|
) -> <Self::Cx as Cx>::Result;
|
||||||
|
|
||||||
|
fn compute_goal(
|
||||||
|
search_graph: &mut SearchGraph<Self>,
|
||||||
|
cx: Self::Cx,
|
||||||
|
input: <Self::Cx as Cx>::Input,
|
||||||
|
inspect: &mut Self::ProofTreeBuilder,
|
||||||
|
) -> <Self::Cx as Cx>::Result;
|
||||||
}
|
}
|
||||||
|
|
||||||
/// In the initial iteration of a cycle, we do not yet have a provisional
|
/// In the initial iteration of a cycle, we do not yet have a provisional
|
||||||
@@ -589,15 +596,15 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
|
|||||||
|
|
||||||
/// Probably the most involved method of the whole solver.
|
/// Probably the most involved method of the whole solver.
|
||||||
///
|
///
|
||||||
/// Given some goal which is proven via the `prove_goal` closure, this
|
/// While goals get computed via `D::compute_goal`, this function handles
|
||||||
/// handles caching, overflow, and coinductive cycles.
|
/// caching, overflow, and cycles.
|
||||||
pub fn with_new_goal(
|
#[instrument(level = "debug", skip(self, cx, inspect), ret)]
|
||||||
|
pub fn evaluate_goal(
|
||||||
&mut self,
|
&mut self,
|
||||||
cx: X,
|
cx: X,
|
||||||
input: X::Input,
|
input: X::Input,
|
||||||
step_kind_from_parent: PathKind,
|
step_kind_from_parent: PathKind,
|
||||||
inspect: &mut D::ProofTreeBuilder,
|
inspect: &mut D::ProofTreeBuilder,
|
||||||
evaluate_goal: impl Fn(&mut Self, X, X::Input, &mut D::ProofTreeBuilder) -> X::Result + Copy,
|
|
||||||
) -> X::Result {
|
) -> X::Result {
|
||||||
let Some(available_depth) =
|
let Some(available_depth) =
|
||||||
AvailableDepth::allowed_depth_for_nested::<D>(self.root_depth, &self.stack)
|
AvailableDepth::allowed_depth_for_nested::<D>(self.root_depth, &self.stack)
|
||||||
@@ -666,7 +673,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
|
|||||||
// must not be added to the global cache. Notably, this is the case for
|
// must not be added to the global cache. Notably, this is the case for
|
||||||
// trait solver cycles participants.
|
// trait solver cycles participants.
|
||||||
let (evaluation_result, dep_node) =
|
let (evaluation_result, dep_node) =
|
||||||
cx.with_cached_task(|| self.evaluate_goal_in_task(cx, input, inspect, evaluate_goal));
|
cx.with_cached_task(|| self.evaluate_goal_in_task(cx, input, inspect));
|
||||||
|
|
||||||
// We've finished computing the goal and have popped it from the stack,
|
// We've finished computing the goal and have popped it from the stack,
|
||||||
// lazily update its parent goal.
|
// lazily update its parent goal.
|
||||||
@@ -736,7 +743,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
|
|||||||
}
|
}
|
||||||
|
|
||||||
debug!("encountered stack overflow");
|
debug!("encountered stack overflow");
|
||||||
D::on_stack_overflow(cx, inspect, input)
|
D::on_stack_overflow(cx, input, inspect)
|
||||||
}
|
}
|
||||||
|
|
||||||
/// When reevaluating a goal with a changed provisional result, all provisional cache entry
|
/// When reevaluating a goal with a changed provisional result, all provisional cache entry
|
||||||
@@ -1064,7 +1071,6 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
|
|||||||
cx: X,
|
cx: X,
|
||||||
input: X::Input,
|
input: X::Input,
|
||||||
inspect: &mut D::ProofTreeBuilder,
|
inspect: &mut D::ProofTreeBuilder,
|
||||||
evaluate_goal: impl Fn(&mut Self, X, X::Input, &mut D::ProofTreeBuilder) -> X::Result + Copy,
|
|
||||||
) -> EvaluationResult<X> {
|
) -> EvaluationResult<X> {
|
||||||
// We reset `encountered_overflow` each time we rerun this goal
|
// We reset `encountered_overflow` each time we rerun this goal
|
||||||
// but need to make sure we currently propagate it to the global
|
// but need to make sure we currently propagate it to the global
|
||||||
@@ -1073,7 +1079,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
|
|||||||
let mut encountered_overflow = false;
|
let mut encountered_overflow = false;
|
||||||
let mut i = 0;
|
let mut i = 0;
|
||||||
loop {
|
loop {
|
||||||
let result = evaluate_goal(self, cx, input, inspect);
|
let result = D::compute_goal(self, cx, input, inspect);
|
||||||
let stack_entry = self.stack.pop();
|
let stack_entry = self.stack.pop();
|
||||||
encountered_overflow |= stack_entry.encountered_overflow;
|
encountered_overflow |= stack_entry.encountered_overflow;
|
||||||
debug_assert_eq!(stack_entry.input, input);
|
debug_assert_eq!(stack_entry.input, input);
|
||||||
|
|||||||
@@ -23,7 +23,7 @@ use std::hash::Hash;
|
|||||||
use derive_where::derive_where;
|
use derive_where::derive_where;
|
||||||
use rustc_type_ir_macros::{TypeFoldable_Generic, TypeVisitable_Generic};
|
use rustc_type_ir_macros::{TypeFoldable_Generic, TypeVisitable_Generic};
|
||||||
|
|
||||||
use crate::solve::{CandidateSource, CanonicalInput, Certainty, Goal, GoalSource, QueryResult};
|
use crate::solve::{CandidateSource, Certainty, Goal, GoalSource, QueryResult};
|
||||||
use crate::{Canonical, CanonicalVarValues, Interner};
|
use crate::{Canonical, CanonicalVarValues, Interner};
|
||||||
|
|
||||||
/// Some `data` together with information about how they relate to the input
|
/// Some `data` together with information about how they relate to the input
|
||||||
@@ -54,18 +54,12 @@ pub type CanonicalState<I, T> = Canonical<I, State<I, T>>;
|
|||||||
pub struct GoalEvaluation<I: Interner> {
|
pub struct GoalEvaluation<I: Interner> {
|
||||||
pub uncanonicalized_goal: Goal<I, I::Predicate>,
|
pub uncanonicalized_goal: Goal<I, I::Predicate>,
|
||||||
pub orig_values: Vec<I::GenericArg>,
|
pub orig_values: Vec<I::GenericArg>,
|
||||||
pub evaluation: CanonicalGoalEvaluation<I>,
|
pub kind: GoalEvaluationKind<I>,
|
||||||
}
|
|
||||||
|
|
||||||
#[derive_where(PartialEq, Eq, Hash, Debug; I: Interner)]
|
|
||||||
pub struct CanonicalGoalEvaluation<I: Interner> {
|
|
||||||
pub goal: CanonicalInput<I>,
|
|
||||||
pub kind: CanonicalGoalEvaluationKind<I>,
|
|
||||||
pub result: QueryResult<I>,
|
pub result: QueryResult<I>,
|
||||||
}
|
}
|
||||||
|
|
||||||
#[derive_where(PartialEq, Eq, Hash, Debug; I: Interner)]
|
#[derive_where(PartialEq, Eq, Hash, Debug; I: Interner)]
|
||||||
pub enum CanonicalGoalEvaluationKind<I: Interner> {
|
pub enum GoalEvaluationKind<I: Interner> {
|
||||||
Overflow,
|
Overflow,
|
||||||
Evaluation {
|
Evaluation {
|
||||||
/// This is always `ProbeKind::Root`.
|
/// This is always `ProbeKind::Root`.
|
||||||
|
|||||||
Reference in New Issue
Block a user