Skip to content

Commit

Permalink
Unrolled build for rust-lang#115838
Browse files Browse the repository at this point in the history
Rollup merge of rust-lang#115838 - lcnr:added-goals, r=compiler-errors

inspect: closer to proof trees for coherence

a continuation of rust-lang#115751. Now explicitly store the added goals

r? ```@compiler-errors```
  • Loading branch information
rust-timer committed Sep 18, 2023
2 parents 078eb11 + 0cb800e commit 2a5c7ed
Show file tree
Hide file tree
Showing 7 changed files with 160 additions and 92 deletions.
33 changes: 24 additions & 9 deletions compiler/rustc_middle/src/traits/solve/inspect.rs
Original file line number Diff line number Diff line change
Expand Up @@ -14,23 +14,29 @@ pub enum CacheHit {
Global,
}

#[derive(Eq, PartialEq)]
pub enum GoalEvaluationKind {
Root,
Nested { is_normalizes_to_hack: IsNormalizesToHack },
}

#[derive(Eq, PartialEq)]
pub struct GoalEvaluation<'tcx> {
pub uncanonicalized_goal: Goal<'tcx, ty::Predicate<'tcx>>,
pub is_normalizes_to_hack: IsNormalizesToHack,
pub kind: GoalEvaluationKind,
pub evaluation: CanonicalGoalEvaluation<'tcx>,
pub returned_goals: Vec<Goal<'tcx, ty::Predicate<'tcx>>>,
}

#[derive(Eq, PartialEq)]
pub struct CanonicalGoalEvaluation<'tcx> {
pub goal: CanonicalInput<'tcx>,
pub kind: GoalEvaluationKind<'tcx>,
pub kind: CanonicalGoalEvaluationKind<'tcx>,
pub result: QueryResult<'tcx>,
}

#[derive(Eq, PartialEq)]
pub enum GoalEvaluationKind<'tcx> {
pub enum CanonicalGoalEvaluationKind<'tcx> {
Overflow,
CacheHit(CacheHit),
Uncached { revisions: Vec<GoalEvaluationStep<'tcx>> },
Expand All @@ -52,22 +58,31 @@ pub struct GoalEvaluationStep<'tcx> {
pub instantiated_goal: QueryInput<'tcx, ty::Predicate<'tcx>>,

/// The actual evaluation of the goal, always `ProbeKind::Root`.
pub evaluation: GoalCandidate<'tcx>,
pub evaluation: Probe<'tcx>,
}

/// A self-contained computation during trait solving. This either
/// corresponds to a `EvalCtxt::probe(_X)` call or the root evaluation
/// of a goal.
#[derive(Eq, PartialEq)]
pub struct GoalCandidate<'tcx> {
pub added_goals_evaluations: Vec<AddedGoalsEvaluation<'tcx>>,
pub candidates: Vec<GoalCandidate<'tcx>>,
pub struct Probe<'tcx> {
pub steps: Vec<ProbeStep<'tcx>>,
pub kind: ProbeKind<'tcx>,
}

impl Debug for GoalCandidate<'_> {
impl Debug for Probe<'_> {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
ProofTreeFormatter::new(f).format_candidate(self)
ProofTreeFormatter::new(f).format_probe(self)
}
}

#[derive(Eq, PartialEq)]
pub enum ProbeStep<'tcx> {
AddGoal(Goal<'tcx, ty::Predicate<'tcx>>),
EvaluateGoals(AddedGoalsEvaluation<'tcx>),
NestedProbe(Probe<'tcx>),
}

#[derive(Debug, PartialEq, Eq)]
pub enum ProbeKind<'tcx> {
/// The root inference context while proving a goal.
Expand Down
34 changes: 19 additions & 15 deletions compiler/rustc_middle/src/traits/solve/inspect/format.rs
Original file line number Diff line number Diff line change
Expand Up @@ -40,9 +40,12 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
}

pub(super) fn format_goal_evaluation(&mut self, eval: &GoalEvaluation<'_>) -> std::fmt::Result {
let goal_text = match eval.is_normalizes_to_hack {
IsNormalizesToHack::Yes => "NORMALIZES-TO HACK GOAL",
IsNormalizesToHack::No => "GOAL",
let goal_text = match eval.kind {
GoalEvaluationKind::Root => "ROOT GOAL",
GoalEvaluationKind::Nested { is_normalizes_to_hack } => match is_normalizes_to_hack {
IsNormalizesToHack::No => "GOAL",
IsNormalizesToHack::Yes => "NORMALIZES-TO HACK GOAL",
},
};
writeln!(self.f, "{}: {:?}", goal_text, eval.uncanonicalized_goal)?;
self.nested(|this| this.format_canonical_goal_evaluation(&eval.evaluation))?;
Expand All @@ -68,16 +71,16 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
writeln!(self.f, "GOAL: {:?}", eval.goal)?;

match &eval.kind {
GoalEvaluationKind::Overflow => {
CanonicalGoalEvaluationKind::Overflow => {
writeln!(self.f, "OVERFLOW: {:?}", eval.result)
}
GoalEvaluationKind::CacheHit(CacheHit::Global) => {
CanonicalGoalEvaluationKind::CacheHit(CacheHit::Global) => {
writeln!(self.f, "GLOBAL CACHE HIT: {:?}", eval.result)
}
GoalEvaluationKind::CacheHit(CacheHit::Provisional) => {
CanonicalGoalEvaluationKind::CacheHit(CacheHit::Provisional) => {
writeln!(self.f, "PROVISIONAL CACHE HIT: {:?}", eval.result)
}
GoalEvaluationKind::Uncached { revisions } => {
CanonicalGoalEvaluationKind::Uncached { revisions } => {
for (n, step) in revisions.iter().enumerate() {
writeln!(self.f, "REVISION {n}")?;
self.nested(|this| this.format_evaluation_step(step))?;
Expand All @@ -92,11 +95,11 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
evaluation_step: &GoalEvaluationStep<'_>,
) -> std::fmt::Result {
writeln!(self.f, "INSTANTIATED: {:?}", evaluation_step.instantiated_goal)?;
self.format_candidate(&evaluation_step.evaluation)
self.format_probe(&evaluation_step.evaluation)
}

pub(super) fn format_candidate(&mut self, candidate: &GoalCandidate<'_>) -> std::fmt::Result {
match &candidate.kind {
pub(super) fn format_probe(&mut self, probe: &Probe<'_>) -> std::fmt::Result {
match &probe.kind {
ProbeKind::Root { result } => {
writeln!(self.f, "ROOT RESULT: {result:?}")
}
Expand All @@ -118,11 +121,12 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
}?;

self.nested(|this| {
for candidate in &candidate.candidates {
this.format_candidate(candidate)?;
}
for nested in &candidate.added_goals_evaluations {
this.format_added_goals_evaluation(nested)?;
for step in &probe.steps {
match step {
ProbeStep::AddGoal(goal) => writeln!(this.f, "ADDED GOAL: {goal:?}")?,
ProbeStep::EvaluateGoals(eval) => this.format_added_goals_evaluation(eval)?,
ProbeStep::NestedProbe(probe) => this.format_probe(probe)?,
}
}
Ok(())
})
Expand Down
27 changes: 17 additions & 10 deletions compiler/rustc_trait_selection/src/solve/eval_ctxt.rs
Original file line number Diff line number Diff line change
Expand Up @@ -28,8 +28,8 @@ use std::ops::ControlFlow;
use crate::traits::vtable::{count_own_vtable_entries, prepare_vtable_segments, VtblSegment};

use super::inspect::ProofTreeBuilder;
use super::search_graph;
use super::SolverMode;
use super::{search_graph, GoalEvaluationKind};
use super::{search_graph::SearchGraph, Goal};
pub use select::InferCtxtSelectExt;

Expand Down Expand Up @@ -85,7 +85,7 @@ pub struct EvalCtxt<'a, 'tcx> {
// evaluation code.
tainted: Result<(), NoSolution>,

inspect: ProofTreeBuilder<'tcx>,
pub(super) inspect: ProofTreeBuilder<'tcx>,
}

#[derive(Debug, Clone)]
Expand Down Expand Up @@ -164,7 +164,7 @@ impl<'tcx> InferCtxtEvalExt<'tcx> for InferCtxt<'tcx> {
Option<inspect::GoalEvaluation<'tcx>>,
) {
EvalCtxt::enter_root(self, generate_proof_tree, |ecx| {
ecx.evaluate_goal(IsNormalizesToHack::No, goal)
ecx.evaluate_goal(GoalEvaluationKind::Root, goal)
})
}
}
Expand Down Expand Up @@ -340,11 +340,11 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
/// been constrained and the certainty of the result.
fn evaluate_goal(
&mut self,
is_normalizes_to_hack: IsNormalizesToHack,
goal_evaluation_kind: GoalEvaluationKind,
goal: Goal<'tcx, ty::Predicate<'tcx>>,
) -> Result<(bool, Certainty, Vec<Goal<'tcx, ty::Predicate<'tcx>>>), NoSolution> {
let (orig_values, canonical_goal) = self.canonicalize_goal(goal);
let mut goal_evaluation = self.inspect.new_goal_evaluation(goal, is_normalizes_to_hack);
let mut goal_evaluation = self.inspect.new_goal_evaluation(goal, goal_evaluation_kind);
let encountered_overflow = self.search_graph.encountered_overflow();
let canonical_response = EvalCtxt::evaluate_canonical_goal(
self.tcx(),
Expand Down Expand Up @@ -389,7 +389,10 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
// solver cycle.
if cfg!(debug_assertions)
&& has_changed
&& is_normalizes_to_hack == IsNormalizesToHack::No
&& !matches!(
goal_evaluation_kind,
GoalEvaluationKind::Nested { is_normalizes_to_hack: IsNormalizesToHack::Yes }
)
&& !self.search_graph.in_cycle()
{
// The nested evaluation has to happen with the original state
Expand Down Expand Up @@ -561,8 +564,10 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
},
);

let (_, certainty, instantiate_goals) =
self.evaluate_goal(IsNormalizesToHack::Yes, unconstrained_goal)?;
let (_, certainty, instantiate_goals) = self.evaluate_goal(
GoalEvaluationKind::Nested { is_normalizes_to_hack: IsNormalizesToHack::Yes },
unconstrained_goal,
)?;
self.add_goals(instantiate_goals);

// Finally, equate the goal's RHS with the unconstrained var.
Expand Down Expand Up @@ -596,8 +601,10 @@ impl<'a, 'tcx> EvalCtxt<'a, 'tcx> {
}

for goal in goals.goals.drain(..) {
let (has_changed, certainty, instantiate_goals) =
self.evaluate_goal(IsNormalizesToHack::No, goal)?;
let (has_changed, certainty, instantiate_goals) = self.evaluate_goal(
GoalEvaluationKind::Nested { is_normalizes_to_hack: IsNormalizesToHack::No },
goal,
)?;
self.add_goals(instantiate_goals);
if has_changed {
unchanged_certainty = None;
Expand Down
4 changes: 2 additions & 2 deletions compiler/rustc_trait_selection/src/solve/eval_ctxt/probe.rs
Original file line number Diff line number Diff line change
Expand Up @@ -24,13 +24,13 @@ where
search_graph: outer_ecx.search_graph,
nested_goals: outer_ecx.nested_goals.clone(),
tainted: outer_ecx.tainted,
inspect: outer_ecx.inspect.new_goal_candidate(),
inspect: outer_ecx.inspect.new_probe(),
};
let r = nested_ecx.infcx.probe(|_| f(&mut nested_ecx));
if !outer_ecx.inspect.is_noop() {
let probe_kind = probe_kind(&r);
nested_ecx.inspect.probe_kind(probe_kind);
outer_ecx.inspect.goal_candidate(nested_ecx.inspect);
outer_ecx.inspect.finish_probe(nested_ecx.inspect);
}
r
}
Expand Down

0 comments on commit 2a5c7ed

Please sign in to comment.