Skip to content

Commit eac55ee

Browse files
committed
dedup GoalEvaluationStep and GoalCandidate
also handle 2 panics when dumping proof trees for the whole test suite - need to actually tell the proof tree builder about overflow - need to handle a recursion_limit of 0 :<
1 parent 8225a2e commit eac55ee

File tree

5 files changed

+75
-56
lines changed

5 files changed

+75
-56
lines changed

compiler/rustc_middle/src/traits/solve/inspect.rs

+11-4
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,7 @@ pub struct CanonicalGoalEvaluation<'tcx> {
3131

3232
#[derive(Eq, PartialEq)]
3333
pub enum GoalEvaluationKind<'tcx> {
34+
Overflow,
3435
CacheHit(CacheHit),
3536
Uncached { revisions: Vec<GoalEvaluationStep<'tcx>> },
3637
}
@@ -50,10 +51,8 @@ pub struct AddedGoalsEvaluation<'tcx> {
5051
pub struct GoalEvaluationStep<'tcx> {
5152
pub instantiated_goal: QueryInput<'tcx, ty::Predicate<'tcx>>,
5253

53-
pub added_goals_evaluations: Vec<AddedGoalsEvaluation<'tcx>>,
54-
pub candidates: Vec<GoalCandidate<'tcx>>,
55-
56-
pub result: QueryResult<'tcx>,
54+
/// The actual evaluation of the goal, always `ProbeKind::Root`.
55+
pub evaluation: GoalCandidate<'tcx>,
5756
}
5857

5958
#[derive(Eq, PartialEq)]
@@ -63,8 +62,16 @@ pub struct GoalCandidate<'tcx> {
6362
pub kind: ProbeKind<'tcx>,
6463
}
6564

65+
impl Debug for GoalCandidate<'_> {
66+
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
67+
ProofTreeFormatter::new(f).format_candidate(self)
68+
}
69+
}
70+
6671
#[derive(Debug, PartialEq, Eq)]
6772
pub enum ProbeKind<'tcx> {
73+
/// The root inference context while proving a goal.
74+
Root { result: QueryResult<'tcx> },
6875
/// Probe entered when normalizing the self ty during candidate assembly
6976
NormalizedSelfTyAssembly,
7077
/// Some candidate to prove the current goal.

compiler/rustc_middle/src/traits/solve/inspect/format.rs

+8-10
Original file line numberDiff line numberDiff line change
@@ -68,6 +68,9 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
6868
writeln!(self.f, "GOAL: {:?}", eval.goal)?;
6969

7070
match &eval.kind {
71+
GoalEvaluationKind::Overflow => {
72+
writeln!(self.f, "OVERFLOW: {:?}", eval.result)
73+
}
7174
GoalEvaluationKind::CacheHit(CacheHit::Global) => {
7275
writeln!(self.f, "GLOBAL CACHE HIT: {:?}", eval.result)
7376
}
@@ -76,7 +79,7 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
7679
}
7780
GoalEvaluationKind::Uncached { revisions } => {
7881
for (n, step) in revisions.iter().enumerate() {
79-
writeln!(self.f, "REVISION {n}: {:?}", step.result)?;
82+
writeln!(self.f, "REVISION {n}")?;
8083
self.nested(|this| this.format_evaluation_step(step))?;
8184
}
8285
writeln!(self.f, "RESULT: {:?}", eval.result)
@@ -89,19 +92,14 @@ impl<'a, 'b> ProofTreeFormatter<'a, 'b> {
8992
evaluation_step: &GoalEvaluationStep<'_>,
9093
) -> std::fmt::Result {
9194
writeln!(self.f, "INSTANTIATED: {:?}", evaluation_step.instantiated_goal)?;
92-
93-
for candidate in &evaluation_step.candidates {
94-
self.nested(|this| this.format_candidate(candidate))?;
95-
}
96-
for nested in &evaluation_step.added_goals_evaluations {
97-
self.nested(|this| this.format_added_goals_evaluation(nested))?;
98-
}
99-
100-
Ok(())
95+
self.format_candidate(&evaluation_step.evaluation)
10196
}
10297

10398
pub(super) fn format_candidate(&mut self, candidate: &GoalCandidate<'_>) -> std::fmt::Result {
10499
match &candidate.kind {
100+
ProbeKind::Root { result } => {
101+
writeln!(self.f, "ROOT RESULT: {result:?}")
102+
}
105103
ProbeKind::NormalizedSelfTyAssembly => {
106104
writeln!(self.f, "NORMALIZING SELF TY FOR ASSEMBLY:")
107105
}

compiler/rustc_trait_selection/src/solve/inspect.rs

+44-37
Original file line numberDiff line numberDiff line change
@@ -28,28 +28,34 @@ impl<'tcx> WipGoalEvaluation<'tcx> {
2828
}
2929
}
3030

31+
#[derive(Eq, PartialEq, Debug)]
32+
pub enum WipGoalEvaluationKind {
33+
Overflow,
34+
CacheHit(CacheHit),
35+
}
36+
3137
#[derive(Eq, PartialEq, Debug)]
3238
pub struct WipCanonicalGoalEvaluation<'tcx> {
3339
pub goal: CanonicalInput<'tcx>,
34-
pub cache_hit: Option<CacheHit>,
35-
pub evaluation_steps: Vec<WipGoalEvaluationStep<'tcx>>,
40+
pub kind: Option<WipGoalEvaluationKind>,
41+
pub revisions: Vec<WipGoalEvaluationStep<'tcx>>,
3642
pub result: Option<QueryResult<'tcx>>,
3743
}
3844

3945
impl<'tcx> WipCanonicalGoalEvaluation<'tcx> {
4046
pub fn finalize(self) -> inspect::CanonicalGoalEvaluation<'tcx> {
41-
let kind = match self.cache_hit {
42-
Some(hit) => inspect::GoalEvaluationKind::CacheHit(hit),
43-
None => {
44-
assert!(!self.evaluation_steps.is_empty());
45-
inspect::GoalEvaluationKind::Uncached {
46-
revisions: self
47-
.evaluation_steps
48-
.into_iter()
49-
.map(WipGoalEvaluationStep::finalize)
50-
.collect(),
51-
}
47+
let kind = match self.kind {
48+
Some(WipGoalEvaluationKind::Overflow) => inspect::GoalEvaluationKind::Overflow,
49+
Some(WipGoalEvaluationKind::CacheHit(hit)) => {
50+
inspect::GoalEvaluationKind::CacheHit(hit)
5251
}
52+
None => inspect::GoalEvaluationKind::Uncached {
53+
revisions: self
54+
.revisions
55+
.into_iter()
56+
.map(WipGoalEvaluationStep::finalize)
57+
.collect(),
58+
},
5359
};
5460

5561
inspect::CanonicalGoalEvaluation { goal: self.goal, kind, result: self.result.unwrap() }
@@ -81,24 +87,17 @@ impl<'tcx> WipAddedGoalsEvaluation<'tcx> {
8187
pub struct WipGoalEvaluationStep<'tcx> {
8288
pub instantiated_goal: QueryInput<'tcx, ty::Predicate<'tcx>>,
8389

84-
pub added_goals_evaluations: Vec<WipAddedGoalsEvaluation<'tcx>>,
85-
pub candidates: Vec<WipGoalCandidate<'tcx>>,
86-
87-
pub result: Option<QueryResult<'tcx>>,
90+
pub evaluation: WipGoalCandidate<'tcx>,
8891
}
8992

9093
impl<'tcx> WipGoalEvaluationStep<'tcx> {
9194
pub fn finalize(self) -> inspect::GoalEvaluationStep<'tcx> {
92-
inspect::GoalEvaluationStep {
93-
instantiated_goal: self.instantiated_goal,
94-
added_goals_evaluations: self
95-
.added_goals_evaluations
96-
.into_iter()
97-
.map(WipAddedGoalsEvaluation::finalize)
98-
.collect(),
99-
candidates: self.candidates.into_iter().map(WipGoalCandidate::finalize).collect(),
100-
result: self.result.unwrap(),
95+
let evaluation = self.evaluation.finalize();
96+
match evaluation.kind {
97+
ProbeKind::Root { .. } => (),
98+
_ => unreachable!("unexpected root evaluation: {evaluation:?}"),
10199
}
100+
inspect::GoalEvaluationStep { instantiated_goal: self.instantiated_goal, evaluation }
102101
}
103102
}
104103

@@ -269,8 +268,8 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
269268
) -> ProofTreeBuilder<'tcx> {
270269
self.nested(|| WipCanonicalGoalEvaluation {
271270
goal,
272-
cache_hit: None,
273-
evaluation_steps: vec![],
271+
kind: None,
272+
revisions: vec![],
274273
result: None,
275274
})
276275
}
@@ -287,11 +286,11 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
287286
}
288287
}
289288

290-
pub fn cache_hit(&mut self, cache_hit: CacheHit) {
289+
pub fn goal_evaluation_kind(&mut self, kind: WipGoalEvaluationKind) {
291290
if let Some(this) = self.as_mut() {
292291
match this {
293292
DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluation) => {
294-
assert_eq!(canonical_goal_evaluation.cache_hit.replace(cache_hit), None);
293+
assert_eq!(canonical_goal_evaluation.kind.replace(kind), None);
295294
}
296295
_ => unreachable!(),
297296
};
@@ -330,9 +329,11 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
330329
) -> ProofTreeBuilder<'tcx> {
331330
self.nested(|| WipGoalEvaluationStep {
332331
instantiated_goal,
333-
added_goals_evaluations: vec![],
334-
candidates: vec![],
335-
result: None,
332+
evaluation: WipGoalCandidate {
333+
added_goals_evaluations: vec![],
334+
candidates: vec![],
335+
kind: None,
336+
},
336337
})
337338
}
338339
pub fn goal_evaluation_step(&mut self, goal_evaluation_step: ProofTreeBuilder<'tcx>) {
@@ -342,7 +343,7 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
342343
DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluations),
343344
DebugSolver::GoalEvaluationStep(goal_evaluation_step),
344345
) => {
345-
canonical_goal_evaluations.evaluation_steps.push(goal_evaluation_step);
346+
canonical_goal_evaluations.revisions.push(goal_evaluation_step);
346347
}
347348
_ => unreachable!(),
348349
}
@@ -373,7 +374,10 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
373374
match (this, candidate.state.unwrap().tree) {
374375
(
375376
DebugSolver::GoalCandidate(WipGoalCandidate { candidates, .. })
376-
| DebugSolver::GoalEvaluationStep(WipGoalEvaluationStep { candidates, .. }),
377+
| DebugSolver::GoalEvaluationStep(WipGoalEvaluationStep {
378+
evaluation: WipGoalCandidate { candidates, .. },
379+
..
380+
}),
377381
DebugSolver::GoalCandidate(candidate),
378382
) => candidates.push(candidate),
379383
_ => unreachable!(),
@@ -412,7 +416,7 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
412416
match (this, added_goals_evaluation.state.unwrap().tree) {
413417
(
414418
DebugSolver::GoalEvaluationStep(WipGoalEvaluationStep {
415-
added_goals_evaluations,
419+
evaluation: WipGoalCandidate { added_goals_evaluations, .. },
416420
..
417421
})
418422
| DebugSolver::GoalCandidate(WipGoalCandidate {
@@ -432,7 +436,10 @@ impl<'tcx> ProofTreeBuilder<'tcx> {
432436
assert_eq!(canonical_goal_evaluation.result.replace(result), None);
433437
}
434438
DebugSolver::GoalEvaluationStep(evaluation_step) => {
435-
assert_eq!(evaluation_step.result.replace(result), None);
439+
assert_eq!(
440+
evaluation_step.evaluation.kind.replace(ProbeKind::Root { result }),
441+
None
442+
);
436443
}
437444
_ => unreachable!(),
438445
}

compiler/rustc_trait_selection/src/solve/mod.rs

+3-3
Original file line numberDiff line numberDiff line change
@@ -233,9 +233,9 @@ impl<'tcx> EvalCtxt<'_, 'tcx> {
233233

234234
#[instrument(level = "debug", skip(self, goals))]
235235
fn add_goals(&mut self, goals: impl IntoIterator<Item = Goal<'tcx, ty::Predicate<'tcx>>>) {
236-
let current_len = self.nested_goals.goals.len();
237-
self.nested_goals.goals.extend(goals);
238-
debug!("added_goals={:?}", &self.nested_goals.goals[current_len..]);
236+
for goal in goals {
237+
self.add_goal(goal);
238+
}
239239
}
240240

241241
/// Try to merge multiple possible ways to prove a goal, if that is not possible returns `None`.

compiler/rustc_trait_selection/src/solve/search_graph/mod.rs

+9-2
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
mod cache;
22

33
use self::cache::ProvisionalEntry;
4+
use super::inspect;
45
use super::inspect::ProofTreeBuilder;
56
use super::SolverMode;
67
use cache::ProvisionalCache;
@@ -185,6 +186,8 @@ impl<'tcx> SearchGraph<'tcx> {
185186
if let Some(last) = self.stack.raw.last_mut() {
186187
last.encountered_overflow = true;
187188
}
189+
190+
inspect.goal_evaluation_kind(inspect::WipGoalEvaluationKind::Overflow);
188191
return Self::response_no_constraints(tcx, input, Certainty::OVERFLOW);
189192
};
190193

@@ -200,7 +203,9 @@ impl<'tcx> SearchGraph<'tcx> {
200203
available_depth,
201204
)
202205
{
203-
inspect.cache_hit(CacheHit::Global);
206+
inspect.goal_evaluation_kind(inspect::WipGoalEvaluationKind::CacheHit(
207+
CacheHit::Global,
208+
));
204209
self.on_cache_hit(reached_depth, encountered_overflow);
205210
return result;
206211
}
@@ -235,7 +240,9 @@ impl<'tcx> SearchGraph<'tcx> {
235240
// Finally we can return either the provisional response for that goal if we have a
236241
// coinductive cycle or an ambiguous result if the cycle is inductive.
237242
Entry::Occupied(entry_index) => {
238-
inspect.cache_hit(CacheHit::Provisional);
243+
inspect.goal_evaluation_kind(inspect::WipGoalEvaluationKind::CacheHit(
244+
CacheHit::Provisional,
245+
));
239246

240247
let entry_index = *entry_index.get();
241248
let stack_depth = cache.depth(entry_index);

0 commit comments

Comments
 (0)