Rollup merge of #125510 - lcnr:change-proof-trees-to-be-shallow, r=compiler-errors
remove proof tree formatting, make em shallow Debugging via tracing `RUSTC_LOG=rustc_trait_selection::solve=debug` is now imo slightly more readable then the actual proof tree formatter. Removing everything that's not needed for the `analyse` visitor allows us to remove a bunch of code. I personally believe that we should continue to use tracing over proof trees for debugging: - it eagerly prints, allowing us to debug ICEs - the proof tree builder ends up going out of sync with the actual runtime behavior, which is confusing - using shallow proof trees is a lot more performant as we frequently do not recurse into all nested goals when using an analyse visitor - this allows us to clean up the implementation and remove some code r? ```@compiler-errors```
This commit is contained in:
commit
00c51bda3f
16 changed files with 135 additions and 505 deletions
|
@ -1,6 +1,3 @@
|
|||
use std::io::Write;
|
||||
use std::ops::ControlFlow;
|
||||
|
||||
use rustc_data_structures::stack::ensure_sufficient_stack;
|
||||
use rustc_hir::def_id::DefId;
|
||||
use rustc_infer::infer::at::ToTrace;
|
||||
|
@ -20,10 +17,10 @@ use rustc_middle::ty::{
|
|||
self, InferCtxtLike, OpaqueTypeKey, Ty, TyCtxt, TypeFoldable, TypeSuperVisitable,
|
||||
TypeVisitable, TypeVisitableExt, TypeVisitor,
|
||||
};
|
||||
use rustc_session::config::DumpSolverProofTree;
|
||||
use rustc_span::DUMMY_SP;
|
||||
use rustc_type_ir::{self as ir, CanonicalVarValues, Interner};
|
||||
use rustc_type_ir_macros::{Lift_Generic, TypeFoldable_Generic, TypeVisitable_Generic};
|
||||
use std::ops::ControlFlow;
|
||||
|
||||
use crate::traits::coherence;
|
||||
use crate::traits::vtable::{count_own_vtable_entries, prepare_vtable_segments, VtblSegment};
|
||||
|
@ -135,8 +132,7 @@ impl<I: Interner> NestedGoals<I> {
|
|||
#[derive(PartialEq, Eq, Debug, Hash, HashStable, Clone, Copy)]
|
||||
pub enum GenerateProofTree {
|
||||
Yes,
|
||||
IfEnabled,
|
||||
Never,
|
||||
No,
|
||||
}
|
||||
|
||||
#[extension(pub trait InferCtxtEvalExt<'tcx>)]
|
||||
|
@ -182,7 +178,7 @@ impl<'a, 'tcx> EvalCtxt<'a, InferCtxt<'tcx>> {
|
|||
infcx,
|
||||
search_graph: &mut search_graph,
|
||||
nested_goals: NestedGoals::new(),
|
||||
inspect: ProofTreeBuilder::new_maybe_root(infcx.tcx, generate_proof_tree),
|
||||
inspect: ProofTreeBuilder::new_maybe_root(generate_proof_tree),
|
||||
|
||||
// Only relevant when canonicalizing the response,
|
||||
// which we don't do within this evaluation context.
|
||||
|
@ -197,23 +193,14 @@ impl<'a, 'tcx> EvalCtxt<'a, InferCtxt<'tcx>> {
|
|||
};
|
||||
let result = f(&mut ecx);
|
||||
|
||||
let tree = ecx.inspect.finalize();
|
||||
if let (Some(tree), DumpSolverProofTree::Always) = (
|
||||
&tree,
|
||||
infcx.tcx.sess.opts.unstable_opts.next_solver.map(|c| c.dump_tree).unwrap_or_default(),
|
||||
) {
|
||||
let mut lock = std::io::stdout().lock();
|
||||
let _ = lock.write_fmt(format_args!("{tree:?}\n"));
|
||||
let _ = lock.flush();
|
||||
}
|
||||
|
||||
let proof_tree = ecx.inspect.finalize();
|
||||
assert!(
|
||||
ecx.nested_goals.is_empty(),
|
||||
"root `EvalCtxt` should not have any goals added to it"
|
||||
);
|
||||
|
||||
assert!(search_graph.is_empty());
|
||||
(result, tree)
|
||||
(result, proof_tree)
|
||||
}
|
||||
|
||||
/// Creates a nested evaluation context that shares the same search graph as the
|
||||
|
@ -483,7 +470,6 @@ impl<'a, 'tcx> EvalCtxt<'a, InferCtxt<'tcx>> {
|
|||
// the certainty of all the goals.
|
||||
#[instrument(level = "trace", skip(self))]
|
||||
pub(super) fn try_evaluate_added_goals(&mut self) -> Result<Certainty, NoSolution> {
|
||||
self.inspect.start_evaluate_added_goals();
|
||||
let mut response = Ok(Certainty::overflow(false));
|
||||
for _ in 0..FIXPOINT_STEP_LIMIT {
|
||||
// FIXME: This match is a bit ugly, it might be nice to change the inspect
|
||||
|
@ -501,8 +487,6 @@ impl<'a, 'tcx> EvalCtxt<'a, InferCtxt<'tcx>> {
|
|||
}
|
||||
}
|
||||
|
||||
self.inspect.evaluate_added_goals_result(response);
|
||||
|
||||
if response.is_err() {
|
||||
self.tainted = Err(NoSolution);
|
||||
}
|
||||
|
@ -515,7 +499,6 @@ impl<'a, 'tcx> EvalCtxt<'a, InferCtxt<'tcx>> {
|
|||
/// Goals for the next step get directly added to the nested goals of the `EvalCtxt`.
|
||||
fn evaluate_added_goals_step(&mut self) -> Result<Option<Certainty>, NoSolution> {
|
||||
let tcx = self.tcx();
|
||||
self.inspect.start_evaluate_added_goals_step();
|
||||
let mut goals = core::mem::take(&mut self.nested_goals);
|
||||
|
||||
// If this loop did not result in any progress, what's our final certainty.
|
||||
|
|
|
@ -79,7 +79,7 @@ impl<'tcx> ObligationStorage<'tcx> {
|
|||
// change.
|
||||
self.overflowed.extend(self.pending.extract_if(|o| {
|
||||
let goal = o.clone().into();
|
||||
let result = infcx.evaluate_root_goal(goal, GenerateProofTree::Never).0;
|
||||
let result = infcx.evaluate_root_goal(goal, GenerateProofTree::No).0;
|
||||
match result {
|
||||
Ok((has_changed, _)) => has_changed,
|
||||
_ => false,
|
||||
|
@ -159,7 +159,7 @@ impl<'tcx> TraitEngine<'tcx> for FulfillmentCtxt<'tcx> {
|
|||
let mut has_changed = false;
|
||||
for obligation in self.obligations.unstalled_for_select() {
|
||||
let goal = obligation.clone().into();
|
||||
let result = infcx.evaluate_root_goal(goal, GenerateProofTree::IfEnabled).0;
|
||||
let result = infcx.evaluate_root_goal(goal, GenerateProofTree::No).0;
|
||||
self.inspect_evaluated_obligation(infcx, &obligation, &result);
|
||||
let (changed, certainty) = match result {
|
||||
Ok(result) => result,
|
||||
|
@ -246,7 +246,7 @@ fn fulfillment_error_for_stalled<'tcx>(
|
|||
root_obligation: PredicateObligation<'tcx>,
|
||||
) -> FulfillmentError<'tcx> {
|
||||
let (code, refine_obligation) = infcx.probe(|_| {
|
||||
match infcx.evaluate_root_goal(root_obligation.clone().into(), GenerateProofTree::Never).0 {
|
||||
match infcx.evaluate_root_goal(root_obligation.clone().into(), GenerateProofTree::No).0 {
|
||||
Ok((_, Certainty::Maybe(MaybeCause::Ambiguity))) => {
|
||||
(FulfillmentErrorCode::Ambiguity { overflow: None }, true)
|
||||
}
|
||||
|
|
|
@ -317,7 +317,6 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
|
|||
inspect::ProbeStep::RecordImplArgs { impl_args: i } => {
|
||||
assert_eq!(impl_args.replace(i), None);
|
||||
}
|
||||
inspect::ProbeStep::EvaluateGoals(_) => (),
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -359,13 +358,7 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
|
|||
warn!("unexpected root evaluation: {:?}", self.evaluation_kind);
|
||||
return vec![];
|
||||
}
|
||||
inspect::CanonicalGoalEvaluationKind::Evaluation { revisions } => {
|
||||
if let Some(last) = revisions.last() {
|
||||
last
|
||||
} else {
|
||||
return vec![];
|
||||
}
|
||||
}
|
||||
inspect::CanonicalGoalEvaluationKind::Evaluation { final_revision } => final_revision,
|
||||
};
|
||||
|
||||
let mut nested_goals = vec![];
|
||||
|
@ -392,9 +385,7 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
|
|||
normalizes_to_term_hack: Option<NormalizesToTermHack<'tcx>>,
|
||||
source: GoalSource,
|
||||
) -> Self {
|
||||
let inspect::GoalEvaluation { uncanonicalized_goal, kind, evaluation } = root;
|
||||
let inspect::GoalEvaluationKind::Root { orig_values } = kind else { unreachable!() };
|
||||
|
||||
let inspect::GoalEvaluation { uncanonicalized_goal, orig_values, evaluation } = root;
|
||||
let result = evaluation.result.and_then(|ok| {
|
||||
if let Some(term_hack) = normalizes_to_term_hack {
|
||||
infcx
|
||||
|
|
|
@ -5,20 +5,17 @@
|
|||
//! see the comment on [ProofTreeBuilder].
|
||||
use std::mem;
|
||||
|
||||
use crate::solve::eval_ctxt::canonical;
|
||||
use crate::solve::{self, inspect, GenerateProofTree};
|
||||
use rustc_infer::infer::InferCtxt;
|
||||
use rustc_middle::bug;
|
||||
use rustc_middle::infer::canonical::CanonicalVarValues;
|
||||
use rustc_middle::traits::query::NoSolution;
|
||||
use rustc_middle::ty::{self, TyCtxt};
|
||||
use rustc_next_trait_solver::solve::{
|
||||
CanonicalInput, Certainty, Goal, GoalSource, QueryInput, QueryResult,
|
||||
};
|
||||
use rustc_session::config::DumpSolverProofTree;
|
||||
use rustc_type_ir::Interner;
|
||||
|
||||
use crate::solve::eval_ctxt::canonical;
|
||||
use crate::solve::{self, inspect, GenerateProofTree};
|
||||
|
||||
/// The core data structure when building proof trees.
|
||||
///
|
||||
/// In case the current evaluation does not generate a proof
|
||||
|
@ -53,7 +50,7 @@ enum DebugSolver<I: Interner> {
|
|||
Root,
|
||||
GoalEvaluation(WipGoalEvaluation<I>),
|
||||
CanonicalGoalEvaluation(WipCanonicalGoalEvaluation<I>),
|
||||
GoalEvaluationStep(WipGoalEvaluationStep<I>),
|
||||
CanonicalGoalEvaluationStep(WipCanonicalGoalEvaluationStep<I>),
|
||||
}
|
||||
|
||||
impl<I: Interner> From<WipGoalEvaluation<I>> for DebugSolver<I> {
|
||||
|
@ -68,9 +65,9 @@ impl<I: Interner> From<WipCanonicalGoalEvaluation<I>> for DebugSolver<I> {
|
|||
}
|
||||
}
|
||||
|
||||
impl<I: Interner> From<WipGoalEvaluationStep<I>> for DebugSolver<I> {
|
||||
fn from(g: WipGoalEvaluationStep<I>) -> DebugSolver<I> {
|
||||
DebugSolver::GoalEvaluationStep(g)
|
||||
impl<I: Interner> From<WipCanonicalGoalEvaluationStep<I>> for DebugSolver<I> {
|
||||
fn from(g: WipCanonicalGoalEvaluationStep<I>) -> DebugSolver<I> {
|
||||
DebugSolver::CanonicalGoalEvaluationStep(g)
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -78,7 +75,7 @@ impl<I: Interner> From<WipGoalEvaluationStep<I>> for DebugSolver<I> {
|
|||
#[derivative(PartialEq(bound = ""), Eq(bound = ""), Debug(bound = ""))]
|
||||
struct WipGoalEvaluation<I: Interner> {
|
||||
pub uncanonicalized_goal: Goal<I, I::Predicate>,
|
||||
pub kind: WipGoalEvaluationKind<I>,
|
||||
pub orig_values: Vec<I::GenericArg>,
|
||||
pub evaluation: Option<WipCanonicalGoalEvaluation<I>>,
|
||||
}
|
||||
|
||||
|
@ -86,31 +83,19 @@ impl<I: Interner> WipGoalEvaluation<I> {
|
|||
fn finalize(self) -> inspect::GoalEvaluation<I> {
|
||||
inspect::GoalEvaluation {
|
||||
uncanonicalized_goal: self.uncanonicalized_goal,
|
||||
kind: match self.kind {
|
||||
WipGoalEvaluationKind::Root { orig_values } => {
|
||||
inspect::GoalEvaluationKind::Root { orig_values }
|
||||
}
|
||||
WipGoalEvaluationKind::Nested => inspect::GoalEvaluationKind::Nested,
|
||||
},
|
||||
orig_values: self.orig_values,
|
||||
evaluation: self.evaluation.unwrap().finalize(),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(derivative::Derivative)]
|
||||
#[derivative(PartialEq(bound = ""), Eq(bound = ""), Debug(bound = ""))]
|
||||
pub(in crate::solve) enum WipGoalEvaluationKind<I: Interner> {
|
||||
Root { orig_values: Vec<I::GenericArg> },
|
||||
Nested,
|
||||
}
|
||||
|
||||
#[derive(derivative::Derivative)]
|
||||
#[derivative(PartialEq(bound = ""), Eq(bound = ""))]
|
||||
pub(in crate::solve) enum WipCanonicalGoalEvaluationKind<I: Interner> {
|
||||
Overflow,
|
||||
CycleInStack,
|
||||
ProvisionalCacheHit,
|
||||
Interned { revisions: I::GoalEvaluationSteps },
|
||||
Interned { final_revision: I::CanonicalGoalEvaluationStepRef },
|
||||
}
|
||||
|
||||
impl<I: Interner> std::fmt::Debug for WipCanonicalGoalEvaluationKind<I> {
|
||||
|
@ -119,7 +104,9 @@ impl<I: Interner> std::fmt::Debug for WipCanonicalGoalEvaluationKind<I> {
|
|||
Self::Overflow => write!(f, "Overflow"),
|
||||
Self::CycleInStack => write!(f, "CycleInStack"),
|
||||
Self::ProvisionalCacheHit => write!(f, "ProvisionalCacheHit"),
|
||||
Self::Interned { revisions: _ } => f.debug_struct("Interned").finish_non_exhaustive(),
|
||||
Self::Interned { final_revision: _ } => {
|
||||
f.debug_struct("Interned").finish_non_exhaustive()
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
@ -131,13 +118,15 @@ struct WipCanonicalGoalEvaluation<I: Interner> {
|
|||
kind: Option<WipCanonicalGoalEvaluationKind<I>>,
|
||||
/// Only used for uncached goals. After we finished evaluating
|
||||
/// the goal, this is interned and moved into `kind`.
|
||||
revisions: Vec<WipGoalEvaluationStep<I>>,
|
||||
final_revision: Option<WipCanonicalGoalEvaluationStep<I>>,
|
||||
result: Option<QueryResult<I>>,
|
||||
}
|
||||
|
||||
impl<I: Interner> WipCanonicalGoalEvaluation<I> {
|
||||
fn finalize(self) -> inspect::CanonicalGoalEvaluation<I> {
|
||||
assert!(self.revisions.is_empty());
|
||||
// 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::CanonicalGoalEvaluationKind::Overflow
|
||||
|
@ -148,8 +137,8 @@ impl<I: Interner> WipCanonicalGoalEvaluation<I> {
|
|||
WipCanonicalGoalEvaluationKind::ProvisionalCacheHit => {
|
||||
inspect::CanonicalGoalEvaluationKind::ProvisionalCacheHit
|
||||
}
|
||||
WipCanonicalGoalEvaluationKind::Interned { revisions } => {
|
||||
inspect::CanonicalGoalEvaluationKind::Evaluation { revisions }
|
||||
WipCanonicalGoalEvaluationKind::Interned { final_revision } => {
|
||||
inspect::CanonicalGoalEvaluationKind::Evaluation { final_revision }
|
||||
}
|
||||
};
|
||||
|
||||
|
@ -159,29 +148,7 @@ impl<I: Interner> WipCanonicalGoalEvaluation<I> {
|
|||
|
||||
#[derive(derivative::Derivative)]
|
||||
#[derivative(PartialEq(bound = ""), Eq(bound = ""), Debug(bound = ""))]
|
||||
struct WipAddedGoalsEvaluation<I: Interner> {
|
||||
evaluations: Vec<Vec<WipGoalEvaluation<I>>>,
|
||||
result: Option<Result<Certainty, NoSolution>>,
|
||||
}
|
||||
|
||||
impl<I: Interner> WipAddedGoalsEvaluation<I> {
|
||||
fn finalize(self) -> inspect::AddedGoalsEvaluation<I> {
|
||||
inspect::AddedGoalsEvaluation {
|
||||
evaluations: self
|
||||
.evaluations
|
||||
.into_iter()
|
||||
.map(|evaluations| {
|
||||
evaluations.into_iter().map(WipGoalEvaluation::finalize).collect()
|
||||
})
|
||||
.collect(),
|
||||
result: self.result.unwrap(),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(derivative::Derivative)]
|
||||
#[derivative(PartialEq(bound = ""), Eq(bound = ""), Debug(bound = ""))]
|
||||
struct WipGoalEvaluationStep<I: Interner> {
|
||||
struct WipCanonicalGoalEvaluationStep<I: Interner> {
|
||||
/// Unlike `EvalCtxt::var_values`, we append a new
|
||||
/// generic arg here whenever we create a new inference
|
||||
/// variable.
|
||||
|
@ -194,7 +161,7 @@ struct WipGoalEvaluationStep<I: Interner> {
|
|||
evaluation: WipProbe<I>,
|
||||
}
|
||||
|
||||
impl<I: Interner> WipGoalEvaluationStep<I> {
|
||||
impl<I: Interner> WipCanonicalGoalEvaluationStep<I> {
|
||||
fn current_evaluation_scope(&mut self) -> &mut WipProbe<I> {
|
||||
let mut current = &mut self.evaluation;
|
||||
for _ in 0..self.probe_depth {
|
||||
|
@ -206,24 +173,16 @@ impl<I: Interner> WipGoalEvaluationStep<I> {
|
|||
current
|
||||
}
|
||||
|
||||
fn added_goals_evaluation(&mut self) -> &mut WipAddedGoalsEvaluation<I> {
|
||||
let mut current = &mut self.evaluation;
|
||||
loop {
|
||||
match current.steps.last_mut() {
|
||||
Some(WipProbeStep::NestedProbe(p)) => current = p,
|
||||
Some(WipProbeStep::EvaluateGoals(evaluation)) => return evaluation,
|
||||
_ => bug!(),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn finalize(self) -> inspect::GoalEvaluationStep<I> {
|
||||
fn finalize(self) -> inspect::CanonicalGoalEvaluationStep<I> {
|
||||
let evaluation = self.evaluation.finalize();
|
||||
match evaluation.kind {
|
||||
inspect::ProbeKind::Root { .. } => (),
|
||||
_ => unreachable!("unexpected root evaluation: {evaluation:?}"),
|
||||
}
|
||||
inspect::GoalEvaluationStep { instantiated_goal: self.instantiated_goal, evaluation }
|
||||
inspect::CanonicalGoalEvaluationStep {
|
||||
instantiated_goal: self.instantiated_goal,
|
||||
evaluation,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -250,7 +209,6 @@ impl<I: Interner> WipProbe<I> {
|
|||
#[derivative(PartialEq(bound = ""), Eq(bound = ""), Debug(bound = ""))]
|
||||
enum WipProbeStep<I: Interner> {
|
||||
AddGoal(GoalSource, inspect::CanonicalState<I, Goal<I, I::Predicate>>),
|
||||
EvaluateGoals(WipAddedGoalsEvaluation<I>),
|
||||
NestedProbe(WipProbe<I>),
|
||||
MakeCanonicalResponse { shallow_certainty: Certainty },
|
||||
RecordImplArgs { impl_args: inspect::CanonicalState<I, I::GenericArgs> },
|
||||
|
@ -260,7 +218,6 @@ impl<I: Interner> WipProbeStep<I> {
|
|||
fn finalize(self) -> inspect::ProbeStep<I> {
|
||||
match self {
|
||||
WipProbeStep::AddGoal(source, goal) => inspect::ProbeStep::AddGoal(source, goal),
|
||||
WipProbeStep::EvaluateGoals(eval) => inspect::ProbeStep::EvaluateGoals(eval.finalize()),
|
||||
WipProbeStep::NestedProbe(probe) => inspect::ProbeStep::NestedProbe(probe.finalize()),
|
||||
WipProbeStep::RecordImplArgs { impl_args } => {
|
||||
inspect::ProbeStep::RecordImplArgs { impl_args }
|
||||
|
@ -278,6 +235,15 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
|
|||
ProofTreeBuilder { state: Some(Box::new(state.into())) }
|
||||
}
|
||||
|
||||
fn opt_nested<T: Into<DebugSolver<TyCtxt<'tcx>>>>(
|
||||
&self,
|
||||
state: impl FnOnce() -> Option<T>,
|
||||
) -> Self {
|
||||
ProofTreeBuilder {
|
||||
state: self.state.as_ref().and_then(|_| Some(state()?.into())).map(Box::new),
|
||||
}
|
||||
}
|
||||
|
||||
fn nested<T: Into<DebugSolver<TyCtxt<'tcx>>>>(&self, state: impl FnOnce() -> T) -> Self {
|
||||
ProofTreeBuilder { state: self.state.as_ref().map(|_| Box::new(state().into())) }
|
||||
}
|
||||
|
@ -302,22 +268,10 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
|
|||
}
|
||||
|
||||
pub fn new_maybe_root(
|
||||
tcx: TyCtxt<'tcx>,
|
||||
generate_proof_tree: GenerateProofTree,
|
||||
) -> ProofTreeBuilder<TyCtxt<'tcx>> {
|
||||
match generate_proof_tree {
|
||||
GenerateProofTree::Never => ProofTreeBuilder::new_noop(),
|
||||
GenerateProofTree::IfEnabled => {
|
||||
let opts = &tcx.sess.opts.unstable_opts;
|
||||
match opts.next_solver.map(|c| c.dump_tree).unwrap_or_default() {
|
||||
DumpSolverProofTree::Always => ProofTreeBuilder::new_root(),
|
||||
// `OnError` is handled by reevaluating goals in error
|
||||
// reporting with `GenerateProofTree::Yes`.
|
||||
DumpSolverProofTree::OnError | DumpSolverProofTree::Never => {
|
||||
ProofTreeBuilder::new_noop()
|
||||
}
|
||||
}
|
||||
}
|
||||
GenerateProofTree::No => ProofTreeBuilder::new_noop(),
|
||||
GenerateProofTree::Yes => ProofTreeBuilder::new_root(),
|
||||
}
|
||||
}
|
||||
|
@ -340,15 +294,13 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
|
|||
orig_values: &[ty::GenericArg<'tcx>],
|
||||
kind: solve::GoalEvaluationKind,
|
||||
) -> ProofTreeBuilder<TyCtxt<'tcx>> {
|
||||
self.nested(|| WipGoalEvaluation {
|
||||
uncanonicalized_goal: goal,
|
||||
kind: match kind {
|
||||
solve::GoalEvaluationKind::Root => {
|
||||
WipGoalEvaluationKind::Root { orig_values: orig_values.to_vec() }
|
||||
}
|
||||
solve::GoalEvaluationKind::Nested => WipGoalEvaluationKind::Nested,
|
||||
},
|
||||
evaluation: None,
|
||||
self.opt_nested(|| match kind {
|
||||
solve::GoalEvaluationKind::Root => Some(WipGoalEvaluation {
|
||||
uncanonicalized_goal: goal,
|
||||
orig_values: orig_values.to_vec(),
|
||||
evaluation: None,
|
||||
}),
|
||||
solve::GoalEvaluationKind::Nested => None,
|
||||
})
|
||||
}
|
||||
|
||||
|
@ -359,24 +311,22 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
|
|||
self.nested(|| WipCanonicalGoalEvaluation {
|
||||
goal,
|
||||
kind: None,
|
||||
revisions: vec![],
|
||||
final_revision: None,
|
||||
result: None,
|
||||
})
|
||||
}
|
||||
|
||||
pub fn finalize_evaluation(
|
||||
pub fn finalize_canonical_goal_evaluation(
|
||||
&mut self,
|
||||
tcx: TyCtxt<'tcx>,
|
||||
) -> Option<&'tcx [inspect::GoalEvaluationStep<TyCtxt<'tcx>>]> {
|
||||
) -> Option<&'tcx inspect::CanonicalGoalEvaluationStep<TyCtxt<'tcx>>> {
|
||||
self.as_mut().map(|this| match this {
|
||||
DebugSolver::CanonicalGoalEvaluation(evaluation) => {
|
||||
let revisions = mem::take(&mut evaluation.revisions)
|
||||
.into_iter()
|
||||
.map(WipGoalEvaluationStep::finalize);
|
||||
let revisions = &*tcx.arena.alloc_from_iter(revisions);
|
||||
let kind = WipCanonicalGoalEvaluationKind::Interned { revisions };
|
||||
let final_revision = mem::take(&mut evaluation.final_revision).unwrap();
|
||||
let final_revision = &*tcx.arena.alloc(final_revision.finalize());
|
||||
let kind = WipCanonicalGoalEvaluationKind::Interned { final_revision };
|
||||
assert_eq!(evaluation.kind.replace(kind), None);
|
||||
revisions
|
||||
final_revision
|
||||
}
|
||||
_ => unreachable!(),
|
||||
})
|
||||
|
@ -400,7 +350,10 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
|
|||
}
|
||||
}
|
||||
|
||||
pub fn goal_evaluation_kind(&mut self, kind: WipCanonicalGoalEvaluationKind<TyCtxt<'tcx>>) {
|
||||
pub fn canonical_goal_evaluation_kind(
|
||||
&mut self,
|
||||
kind: WipCanonicalGoalEvaluationKind<TyCtxt<'tcx>>,
|
||||
) {
|
||||
if let Some(this) = self.as_mut() {
|
||||
match this {
|
||||
DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluation) => {
|
||||
|
@ -413,17 +366,11 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
|
|||
|
||||
pub fn goal_evaluation(&mut self, goal_evaluation: ProofTreeBuilder<TyCtxt<'tcx>>) {
|
||||
if let Some(this) = self.as_mut() {
|
||||
match (this, *goal_evaluation.state.unwrap()) {
|
||||
(
|
||||
DebugSolver::GoalEvaluationStep(state),
|
||||
DebugSolver::GoalEvaluation(goal_evaluation),
|
||||
) => state
|
||||
.added_goals_evaluation()
|
||||
.evaluations
|
||||
.last_mut()
|
||||
.unwrap()
|
||||
.push(goal_evaluation),
|
||||
(this @ DebugSolver::Root, goal_evaluation) => *this = goal_evaluation,
|
||||
match this {
|
||||
DebugSolver::Root => *this = *goal_evaluation.state.unwrap(),
|
||||
DebugSolver::CanonicalGoalEvaluationStep(_) => {
|
||||
assert!(goal_evaluation.state.is_none())
|
||||
}
|
||||
_ => unreachable!(),
|
||||
}
|
||||
}
|
||||
|
@ -434,7 +381,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
|
|||
var_values: CanonicalVarValues<'tcx>,
|
||||
instantiated_goal: QueryInput<TyCtxt<'tcx>, ty::Predicate<'tcx>>,
|
||||
) -> ProofTreeBuilder<TyCtxt<'tcx>> {
|
||||
self.nested(|| WipGoalEvaluationStep {
|
||||
self.nested(|| WipCanonicalGoalEvaluationStep {
|
||||
var_values: var_values.var_values.to_vec(),
|
||||
instantiated_goal,
|
||||
evaluation: WipProbe {
|
||||
|
@ -452,9 +399,9 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
|
|||
match (this, *goal_evaluation_step.state.unwrap()) {
|
||||
(
|
||||
DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluations),
|
||||
DebugSolver::GoalEvaluationStep(goal_evaluation_step),
|
||||
DebugSolver::CanonicalGoalEvaluationStep(goal_evaluation_step),
|
||||
) => {
|
||||
canonical_goal_evaluations.revisions.push(goal_evaluation_step);
|
||||
canonical_goal_evaluations.final_revision = Some(goal_evaluation_step);
|
||||
}
|
||||
_ => unreachable!(),
|
||||
}
|
||||
|
@ -464,7 +411,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
|
|||
pub fn add_var_value<T: Into<ty::GenericArg<'tcx>>>(&mut self, arg: T) {
|
||||
match self.as_mut() {
|
||||
None => {}
|
||||
Some(DebugSolver::GoalEvaluationStep(state)) => {
|
||||
Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
|
||||
state.var_values.push(arg.into());
|
||||
}
|
||||
Some(s) => bug!("tried to add var values to {s:?}"),
|
||||
|
@ -474,7 +421,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
|
|||
pub fn enter_probe(&mut self) {
|
||||
match self.as_mut() {
|
||||
None => {}
|
||||
Some(DebugSolver::GoalEvaluationStep(state)) => {
|
||||
Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
|
||||
let initial_num_var_values = state.var_values.len();
|
||||
state.current_evaluation_scope().steps.push(WipProbeStep::NestedProbe(WipProbe {
|
||||
initial_num_var_values,
|
||||
|
@ -491,7 +438,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
|
|||
pub fn probe_kind(&mut self, probe_kind: inspect::ProbeKind<TyCtxt<'tcx>>) {
|
||||
match self.as_mut() {
|
||||
None => {}
|
||||
Some(DebugSolver::GoalEvaluationStep(state)) => {
|
||||
Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
|
||||
let prev = state.current_evaluation_scope().kind.replace(probe_kind);
|
||||
assert_eq!(prev, None);
|
||||
}
|
||||
|
@ -506,7 +453,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
|
|||
) {
|
||||
match self.as_mut() {
|
||||
None => {}
|
||||
Some(DebugSolver::GoalEvaluationStep(state)) => {
|
||||
Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
|
||||
let final_state = canonical::make_canonical_state(
|
||||
infcx,
|
||||
&state.var_values,
|
||||
|
@ -543,7 +490,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
|
|||
) {
|
||||
match self.as_mut() {
|
||||
None => {}
|
||||
Some(DebugSolver::GoalEvaluationStep(state)) => {
|
||||
Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
|
||||
let goal = canonical::make_canonical_state(
|
||||
infcx,
|
||||
&state.var_values,
|
||||
|
@ -563,7 +510,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
|
|||
impl_args: ty::GenericArgsRef<'tcx>,
|
||||
) {
|
||||
match self.as_mut() {
|
||||
Some(DebugSolver::GoalEvaluationStep(state)) => {
|
||||
Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
|
||||
let impl_args = canonical::make_canonical_state(
|
||||
infcx,
|
||||
&state.var_values,
|
||||
|
@ -582,7 +529,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
|
|||
|
||||
pub fn make_canonical_response(&mut self, shallow_certainty: Certainty) {
|
||||
match self.as_mut() {
|
||||
Some(DebugSolver::GoalEvaluationStep(state)) => {
|
||||
Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
|
||||
state
|
||||
.current_evaluation_scope()
|
||||
.steps
|
||||
|
@ -596,7 +543,7 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
|
|||
pub fn finish_probe(mut self) -> ProofTreeBuilder<TyCtxt<'tcx>> {
|
||||
match self.as_mut() {
|
||||
None => {}
|
||||
Some(DebugSolver::GoalEvaluationStep(state)) => {
|
||||
Some(DebugSolver::CanonicalGoalEvaluationStep(state)) => {
|
||||
assert_ne!(state.probe_depth, 0);
|
||||
let num_var_values = state.current_evaluation_scope().initial_num_var_values;
|
||||
state.var_values.truncate(num_var_values);
|
||||
|
@ -608,46 +555,13 @@ impl<'tcx> ProofTreeBuilder<TyCtxt<'tcx>> {
|
|||
self
|
||||
}
|
||||
|
||||
pub fn start_evaluate_added_goals(&mut self) {
|
||||
match self.as_mut() {
|
||||
None => {}
|
||||
Some(DebugSolver::GoalEvaluationStep(state)) => {
|
||||
state.current_evaluation_scope().steps.push(WipProbeStep::EvaluateGoals(
|
||||
WipAddedGoalsEvaluation { evaluations: vec![], result: None },
|
||||
));
|
||||
}
|
||||
_ => bug!(),
|
||||
}
|
||||
}
|
||||
|
||||
pub fn start_evaluate_added_goals_step(&mut self) {
|
||||
match self.as_mut() {
|
||||
None => {}
|
||||
Some(DebugSolver::GoalEvaluationStep(state)) => {
|
||||
state.added_goals_evaluation().evaluations.push(vec![]);
|
||||
}
|
||||
_ => bug!(),
|
||||
}
|
||||
}
|
||||
|
||||
pub fn evaluate_added_goals_result(&mut self, result: Result<Certainty, NoSolution>) {
|
||||
match self.as_mut() {
|
||||
None => {}
|
||||
Some(DebugSolver::GoalEvaluationStep(state)) => {
|
||||
let prev = state.added_goals_evaluation().result.replace(result);
|
||||
assert_eq!(prev, None);
|
||||
}
|
||||
_ => bug!(),
|
||||
}
|
||||
}
|
||||
|
||||
pub fn query_result(&mut self, result: QueryResult<TyCtxt<'tcx>>) {
|
||||
if let Some(this) = self.as_mut() {
|
||||
match this {
|
||||
DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluation) => {
|
||||
assert_eq!(canonical_goal_evaluation.result.replace(result), None);
|
||||
}
|
||||
DebugSolver::GoalEvaluationStep(evaluation_step) => {
|
||||
DebugSolver::CanonicalGoalEvaluationStep(evaluation_step) => {
|
||||
assert_eq!(
|
||||
evaluation_step
|
||||
.evaluation
|
||||
|
|
|
@ -274,7 +274,8 @@ impl<'tcx> SearchGraph<TyCtxt<'tcx>> {
|
|||
last.encountered_overflow = true;
|
||||
}
|
||||
|
||||
inspect.goal_evaluation_kind(inspect::WipCanonicalGoalEvaluationKind::Overflow);
|
||||
inspect
|
||||
.canonical_goal_evaluation_kind(inspect::WipCanonicalGoalEvaluationKind::Overflow);
|
||||
return Self::response_no_constraints(tcx, input, Certainty::overflow(true));
|
||||
};
|
||||
|
||||
|
@ -302,8 +303,9 @@ impl<'tcx> SearchGraph<TyCtxt<'tcx>> {
|
|||
// 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
|
||||
.goal_evaluation_kind(inspect::WipCanonicalGoalEvaluationKind::ProvisionalCacheHit);
|
||||
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 {
|
||||
|
@ -314,7 +316,9 @@ impl<'tcx> SearchGraph<TyCtxt<'tcx>> {
|
|||
//
|
||||
// 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.goal_evaluation_kind(inspect::WipCanonicalGoalEvaluationKind::CycleInStack);
|
||||
inspect.canonical_goal_evaluation_kind(
|
||||
inspect::WipCanonicalGoalEvaluationKind::CycleInStack,
|
||||
);
|
||||
let is_coinductive_cycle = Self::stack_coinductive_from(tcx, &self.stack, stack_depth);
|
||||
let usage_kind = if is_coinductive_cycle {
|
||||
HasBeenUsed::COINDUCTIVE_CYCLE
|
||||
|
@ -371,7 +375,7 @@ impl<'tcx> SearchGraph<TyCtxt<'tcx>> {
|
|||
(current_entry, result)
|
||||
});
|
||||
|
||||
let proof_tree = inspect.finalize_evaluation(tcx);
|
||||
let proof_tree = inspect.finalize_canonical_goal_evaluation(tcx);
|
||||
|
||||
// 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.
|
||||
|
@ -433,9 +437,9 @@ impl<'tcx> SearchGraph<TyCtxt<'tcx>> {
|
|||
// the goal. We simply overwrite the existing entry once we're done,
|
||||
// caching the proof tree.
|
||||
if !inspect.is_noop() {
|
||||
if let Some(revisions) = proof_tree {
|
||||
let kind = inspect::WipCanonicalGoalEvaluationKind::Interned { revisions };
|
||||
inspect.goal_evaluation_kind(kind);
|
||||
if let Some(final_revision) = proof_tree {
|
||||
let kind = inspect::WipCanonicalGoalEvaluationKind::Interned { final_revision };
|
||||
inspect.canonical_goal_evaluation_kind(kind);
|
||||
} else {
|
||||
return None;
|
||||
}
|
||||
|
|
|
@ -7,15 +7,11 @@ pub mod suggestions;
|
|||
mod type_err_ctxt_ext;
|
||||
|
||||
use super::{Obligation, ObligationCause, ObligationCauseCode, PredicateObligation};
|
||||
use crate::infer::InferCtxt;
|
||||
use crate::solve::{GenerateProofTree, InferCtxtEvalExt};
|
||||
use rustc_hir as hir;
|
||||
use rustc_hir::def_id::DefId;
|
||||
use rustc_hir::intravisit::Visitor;
|
||||
use rustc_middle::traits::solve::Goal;
|
||||
use rustc_middle::ty::{self, Ty, TyCtxt};
|
||||
use rustc_span::Span;
|
||||
use std::io::Write;
|
||||
use std::ops::ControlFlow;
|
||||
|
||||
pub use self::infer_ctxt_ext::*;
|
||||
|
@ -184,16 +180,3 @@ pub enum DefIdOrName {
|
|||
DefId(DefId),
|
||||
Name(&'static str),
|
||||
}
|
||||
|
||||
pub fn dump_proof_tree<'tcx>(o: &Obligation<'tcx, ty::Predicate<'tcx>>, infcx: &InferCtxt<'tcx>) {
|
||||
infcx.probe(|_| {
|
||||
let goal = Goal { predicate: o.predicate, param_env: o.param_env };
|
||||
let tree = infcx
|
||||
.evaluate_root_goal(goal, GenerateProofTree::Yes)
|
||||
.1
|
||||
.expect("proof tree should have been generated");
|
||||
let mut lock = std::io::stdout().lock();
|
||||
let _ = lock.write_fmt(format_args!("{tree:?}\n"));
|
||||
let _ = lock.flush();
|
||||
});
|
||||
}
|
||||
|
|
|
@ -46,7 +46,6 @@ use rustc_middle::ty::{
|
|||
TypeVisitableExt, Upcast,
|
||||
};
|
||||
use rustc_middle::{bug, span_bug};
|
||||
use rustc_session::config::DumpSolverProofTree;
|
||||
use rustc_session::Limit;
|
||||
use rustc_span::def_id::LOCAL_CRATE;
|
||||
use rustc_span::symbol::sym;
|
||||
|
@ -56,8 +55,8 @@ use std::fmt;
|
|||
use std::iter;
|
||||
|
||||
use super::{
|
||||
dump_proof_tree, ArgKind, CandidateSimilarity, FindExprBySpan, FindTypeParam,
|
||||
GetSafeTransmuteErrorAndReason, HasNumericInferVisitor, ImplCandidate, UnsatisfiedConst,
|
||||
ArgKind, CandidateSimilarity, FindExprBySpan, FindTypeParam, GetSafeTransmuteErrorAndReason,
|
||||
HasNumericInferVisitor, ImplCandidate, UnsatisfiedConst,
|
||||
};
|
||||
|
||||
pub use rustc_infer::traits::error_reporting::*;
|
||||
|
@ -369,13 +368,6 @@ impl<'tcx> TypeErrCtxt<'_, 'tcx> {
|
|||
error: &SelectionError<'tcx>,
|
||||
) -> ErrorGuaranteed {
|
||||
let tcx = self.tcx;
|
||||
|
||||
if tcx.sess.opts.unstable_opts.next_solver.map(|c| c.dump_tree).unwrap_or_default()
|
||||
== DumpSolverProofTree::OnError
|
||||
{
|
||||
dump_proof_tree(root_obligation, self.infcx);
|
||||
}
|
||||
|
||||
let mut span = obligation.cause.span;
|
||||
|
||||
let mut err = match *error {
|
||||
|
@ -1529,12 +1521,6 @@ impl<'tcx> TypeErrCtxt<'_, 'tcx> {
|
|||
|
||||
#[instrument(skip(self), level = "debug")]
|
||||
fn report_fulfillment_error(&self, error: &FulfillmentError<'tcx>) -> ErrorGuaranteed {
|
||||
if self.tcx.sess.opts.unstable_opts.next_solver.map(|c| c.dump_tree).unwrap_or_default()
|
||||
== DumpSolverProofTree::OnError
|
||||
{
|
||||
dump_proof_tree(&error.root_obligation, self.infcx);
|
||||
}
|
||||
|
||||
match error.code {
|
||||
FulfillmentErrorCode::Select(ref selection_error) => self.report_selection_error(
|
||||
error.obligation.clone(),
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue