Skip to content

Commit a07e3de

Browse files
Auto merge of #143054 - lcnr:search_graph-3, r=<try>
search graph: improve rebasing and add forced ambiguity support This slightly strengthens rebasing and actually checks for the property we want to maintain. Consider the following very minor changes in benchmarks: | | dropped entries old | new | compute_goal old | new | |---|----|----|---|----| | diesel | 20412 | 4533 | 5144336 | 5128470 | | nalgebra | 2570 | 112 | 779257 | 778571 | | `./x.py b --stage 2`¹ | 17234 | 7680 |14242763 | 142375634 | ¹ with the alias-relate fast-path to avoid the hang in rayon 😅 There are two additional optimizations we can and should do here: - we should be able to just always rebase if cycle heads already have a provisional result from a previous iteration - we currently only apply provisional cache entries if the `path_to_entry` matches exactly. We should be able to extend this e.g. if you have an entry for `B` in `ABA` where the path `BA` is coinductive, then we can use this entry even if the current path from `A` to `B` is inductive. --- Finally, I've added support for `PathKind::ForcedAmbiguity` which always forced the initial provisional result to be ambiguous. A am using this for cycles involving negative reasons, which is currently only used by the fuzzer in https://github.com/lcnr/search_graph_fuzz. Consider the following setup: A goal `A` which only holds if `B` does not hold, and `B` which only holds if `A` does not hold. - A only holds if B does not hold, results in X - B only holds if A does not hold, results in !X - A cycle, provisional result X - B only holds if A does not hold, results in X - A only holds if B does not hold, results in !X - B cycle, provisional result X With negative reasoning, the result of cycle participants depends on their position in the cycle. This means using cache entries while other entries are on the stack/have been popped is wrong. It's also generally just kinda iffy. By always forcing the initial provisional result of such cycles to be ambiguity, we can avoid this, as "not maybe" is just "maybe" again. Rust kind of has negative reasoning due to incompleteness, consider the following setup: - `T::Foo eq u32` - normalize `T::Foo` - via impl -> `u32` - via param_env -> `T` - nested goals... `T::Foo eq u32` holds exactly if the nested goals of the `param_env` candidate do not hold, as preferring that candidate over the impl causes the alias-relate to fail. This means the current provisional cache may cause us to ignore `param_env` preference in rare cases. This is not unsound and I don't care about it, as we already have this behavior when rerunning on changed fixpoint results: - `T: Trait` - via impl ok - via env - `T: Trait` non-productive cycle - result OK, rerun changed provisional result - `T: Trait` - via impl ok - via env - `T: Trait` using the provisional result, can be thought of as recursively expanding the proof tree - via impl ok - via env <don't care> - prefer the env candidate, reached fixpoint --- One could imaging changing `ParamEnv` candidates or the impl shadowing check to use `PathKind::ForcedAmbiguity` to make the search graph less observable instead of only using it for fuzzing. However, incomplete candidate preference isn't really negative reasoning and doing this is a breaking change rust-lang/trait-system-refactor-initiative#114 r? `@compiler-errors`
2 parents 8f21a5c + ff3254b commit a07e3de

File tree

7 files changed

+157
-245
lines changed

7 files changed

+157
-245
lines changed

compiler/rustc_next_trait_solver/src/solve/eval_ctxt/mod.rs

Lines changed: 8 additions & 61 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ use std::ops::ControlFlow;
33

44
#[cfg(feature = "nightly")]
55
use rustc_macros::HashStable_NoContext;
6-
use rustc_type_ir::data_structures::{HashMap, HashSet, ensure_sufficient_stack};
6+
use rustc_type_ir::data_structures::{HashMap, HashSet};
77
use rustc_type_ir::fast_reject::DeepRejectCtxt;
88
use rustc_type_ir::inherent::*;
99
use rustc_type_ir::relate::Relate;
@@ -342,7 +342,7 @@ where
342342
///
343343
/// This function takes care of setting up the inference context, setting the anchor,
344344
/// and registering opaques from the canonicalized input.
345-
fn enter_canonical<R>(
345+
pub(super) fn enter_canonical<R>(
346346
cx: I,
347347
search_graph: &'a mut SearchGraph<D>,
348348
canonical_input: CanonicalInput<I>,
@@ -398,56 +398,6 @@ where
398398
result
399399
}
400400

401-
/// The entry point of the solver.
402-
///
403-
/// This function deals with (coinductive) cycles, overflow, and caching
404-
/// and then calls [`EvalCtxt::compute_goal`] which contains the actual
405-
/// logic of the solver.
406-
///
407-
/// Instead of calling this function directly, use either [EvalCtxt::evaluate_goal]
408-
/// if you're inside of the solver or [SolverDelegateEvalExt::evaluate_root_goal] if you're
409-
/// outside of it.
410-
#[instrument(level = "debug", skip(cx, search_graph, goal_evaluation), ret)]
411-
fn evaluate_canonical_goal(
412-
cx: I,
413-
search_graph: &'a mut SearchGraph<D>,
414-
canonical_input: CanonicalInput<I>,
415-
step_kind_from_parent: PathKind,
416-
goal_evaluation: &mut ProofTreeBuilder<D>,
417-
) -> QueryResult<I> {
418-
let mut canonical_goal_evaluation =
419-
goal_evaluation.new_canonical_goal_evaluation(canonical_input);
420-
421-
// Deal with overflow, caching, and coinduction.
422-
//
423-
// The actual solver logic happens in `ecx.compute_goal`.
424-
let result = ensure_sufficient_stack(|| {
425-
search_graph.with_new_goal(
426-
cx,
427-
canonical_input,
428-
step_kind_from_parent,
429-
&mut canonical_goal_evaluation,
430-
|search_graph, cx, canonical_input, canonical_goal_evaluation| {
431-
EvalCtxt::enter_canonical(
432-
cx,
433-
search_graph,
434-
canonical_input,
435-
canonical_goal_evaluation,
436-
|ecx, goal| {
437-
let result = ecx.compute_goal(goal);
438-
ecx.inspect.query_result(result);
439-
result
440-
},
441-
)
442-
},
443-
)
444-
});
445-
446-
canonical_goal_evaluation.query_result(result);
447-
goal_evaluation.canonical_goal_evaluation(canonical_goal_evaluation);
448-
result
449-
}
450-
451401
/// Recursively evaluates `goal`, returning whether any inference vars have
452402
/// been constrained and the certainty of the result.
453403
fn evaluate_goal(
@@ -501,18 +451,16 @@ where
501451
let (orig_values, canonical_goal) = self.canonicalize_goal(goal);
502452
let mut goal_evaluation =
503453
self.inspect.new_goal_evaluation(goal, &orig_values, goal_evaluation_kind);
504-
let canonical_response = EvalCtxt::evaluate_canonical_goal(
454+
let canonical_result = self.search_graph.evaluate_goal(
505455
self.cx(),
506-
self.search_graph,
507456
canonical_goal,
508457
self.step_kind_for_source(source),
509458
&mut goal_evaluation,
510459
);
511-
let response = match canonical_response {
512-
Err(e) => {
513-
self.inspect.goal_evaluation(goal_evaluation);
514-
return Err(e);
515-
}
460+
goal_evaluation.query_result(canonical_result);
461+
self.inspect.goal_evaluation(goal_evaluation);
462+
let response = match canonical_result {
463+
Err(e) => return Err(e),
516464
Ok(response) => response,
517465
};
518466

@@ -521,7 +469,6 @@ where
521469

522470
let (normalization_nested_goals, certainty) =
523471
self.instantiate_and_apply_query_response(goal.param_env, &orig_values, response);
524-
self.inspect.goal_evaluation(goal_evaluation);
525472

526473
// FIXME: We previously had an assert here that checked that recomputing
527474
// a goal after applying its constraints did not change its response.
@@ -582,7 +529,7 @@ where
582529
Ok((normalization_nested_goals, GoalEvaluation { certainty, has_changed, stalled_on }))
583530
}
584531

585-
fn compute_goal(&mut self, goal: Goal<I, I::Predicate>) -> QueryResult<I> {
532+
pub(super) fn compute_goal(&mut self, goal: Goal<I, I::Predicate>) -> QueryResult<I> {
586533
let Goal { param_env, predicate } = goal;
587534
let kind = predicate.kind();
588535
if let Some(kind) = kind.no_bound_vars() {

compiler/rustc_next_trait_solver/src/solve/inspect/build.rs

Lines changed: 18 additions & 70 deletions
Original file line numberDiff line numberDiff line change
@@ -13,8 +13,7 @@ use rustc_type_ir::{self as ty, Interner};
1313
use crate::delegate::SolverDelegate;
1414
use crate::solve::eval_ctxt::canonical;
1515
use crate::solve::{
16-
CanonicalInput, Certainty, GenerateProofTree, Goal, GoalEvaluationKind, GoalSource,
17-
QueryResult, inspect,
16+
Certainty, GenerateProofTree, Goal, GoalEvaluationKind, GoalSource, QueryResult, inspect,
1817
};
1918

2019
/// The core data structure when building proof trees.
@@ -54,7 +53,6 @@ where
5453
enum DebugSolver<I: Interner> {
5554
Root,
5655
GoalEvaluation(WipGoalEvaluation<I>),
57-
CanonicalGoalEvaluation(WipCanonicalGoalEvaluation<I>),
5856
CanonicalGoalEvaluationStep(WipCanonicalGoalEvaluationStep<I>),
5957
}
6058

@@ -64,12 +62,6 @@ impl<I: Interner> From<WipGoalEvaluation<I>> for DebugSolver<I> {
6462
}
6563
}
6664

67-
impl<I: Interner> From<WipCanonicalGoalEvaluation<I>> for DebugSolver<I> {
68-
fn from(g: WipCanonicalGoalEvaluation<I>) -> DebugSolver<I> {
69-
DebugSolver::CanonicalGoalEvaluation(g)
70-
}
71-
}
72-
7365
impl<I: Interner> From<WipCanonicalGoalEvaluationStep<I>> for DebugSolver<I> {
7466
fn from(g: WipCanonicalGoalEvaluationStep<I>) -> DebugSolver<I> {
7567
DebugSolver::CanonicalGoalEvaluationStep(g)
@@ -80,39 +72,23 @@ impl<I: Interner> From<WipCanonicalGoalEvaluationStep<I>> for DebugSolver<I> {
8072
struct WipGoalEvaluation<I: Interner> {
8173
pub uncanonicalized_goal: Goal<I, I::Predicate>,
8274
pub orig_values: Vec<I::GenericArg>,
83-
pub evaluation: Option<WipCanonicalGoalEvaluation<I>>,
75+
pub encountered_overflow: bool,
76+
/// After we finished evaluating this is moved into `kind`.
77+
pub final_revision: Option<WipCanonicalGoalEvaluationStep<I>>,
78+
pub result: Option<QueryResult<I>>,
8479
}
8580

8681
impl<I: Interner> WipGoalEvaluation<I> {
8782
fn finalize(self) -> inspect::GoalEvaluation<I> {
8883
inspect::GoalEvaluation {
8984
uncanonicalized_goal: self.uncanonicalized_goal,
9085
orig_values: self.orig_values,
91-
evaluation: self.evaluation.unwrap().finalize(),
92-
}
93-
}
94-
}
95-
96-
#[derive_where(PartialEq, Eq, Debug; I: Interner)]
97-
struct WipCanonicalGoalEvaluation<I: Interner> {
98-
goal: CanonicalInput<I>,
99-
encountered_overflow: bool,
100-
/// Only used for uncached goals. After we finished evaluating
101-
/// the goal, this is interned and moved into `kind`.
102-
final_revision: Option<WipCanonicalGoalEvaluationStep<I>>,
103-
result: Option<QueryResult<I>>,
104-
}
105-
106-
impl<I: Interner> WipCanonicalGoalEvaluation<I> {
107-
fn finalize(self) -> inspect::CanonicalGoalEvaluation<I> {
108-
inspect::CanonicalGoalEvaluation {
109-
goal: self.goal,
11086
kind: if self.encountered_overflow {
11187
assert!(self.final_revision.is_none());
112-
inspect::CanonicalGoalEvaluationKind::Overflow
88+
inspect::GoalEvaluationKind::Overflow
11389
} else {
11490
let final_revision = self.final_revision.unwrap().finalize();
115-
inspect::CanonicalGoalEvaluationKind::Evaluation { final_revision }
91+
inspect::GoalEvaluationKind::Evaluation { final_revision }
11692
},
11793
result: self.result.unwrap(),
11894
}
@@ -256,55 +232,27 @@ impl<D: SolverDelegate<Interner = I>, I: Interner> ProofTreeBuilder<D> {
256232

257233
pub(in crate::solve) fn new_goal_evaluation(
258234
&mut self,
259-
goal: Goal<I, I::Predicate>,
235+
uncanonicalized_goal: Goal<I, I::Predicate>,
260236
orig_values: &[I::GenericArg],
261237
kind: GoalEvaluationKind,
262238
) -> ProofTreeBuilder<D> {
263239
self.opt_nested(|| match kind {
264240
GoalEvaluationKind::Root => Some(WipGoalEvaluation {
265-
uncanonicalized_goal: goal,
241+
uncanonicalized_goal,
266242
orig_values: orig_values.to_vec(),
267-
evaluation: None,
243+
encountered_overflow: false,
244+
final_revision: None,
245+
result: None,
268246
}),
269247
GoalEvaluationKind::Nested => None,
270248
})
271249
}
272250

273-
pub(crate) fn new_canonical_goal_evaluation(
274-
&mut self,
275-
goal: CanonicalInput<I>,
276-
) -> ProofTreeBuilder<D> {
277-
self.nested(|| WipCanonicalGoalEvaluation {
278-
goal,
279-
encountered_overflow: false,
280-
final_revision: None,
281-
result: None,
282-
})
283-
}
284-
285-
pub(crate) fn canonical_goal_evaluation(
286-
&mut self,
287-
canonical_goal_evaluation: ProofTreeBuilder<D>,
288-
) {
289-
if let Some(this) = self.as_mut() {
290-
match (this, *canonical_goal_evaluation.state.unwrap()) {
291-
(
292-
DebugSolver::GoalEvaluation(goal_evaluation),
293-
DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluation),
294-
) => {
295-
let prev = goal_evaluation.evaluation.replace(canonical_goal_evaluation);
296-
assert_eq!(prev, None);
297-
}
298-
_ => unreachable!(),
299-
}
300-
}
301-
}
302-
303251
pub(crate) fn canonical_goal_evaluation_overflow(&mut self) {
304252
if let Some(this) = self.as_mut() {
305253
match this {
306-
DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluation) => {
307-
canonical_goal_evaluation.encountered_overflow = true;
254+
DebugSolver::GoalEvaluation(goal_evaluation) => {
255+
goal_evaluation.encountered_overflow = true;
308256
}
309257
_ => unreachable!(),
310258
};
@@ -343,10 +291,10 @@ impl<D: SolverDelegate<Interner = I>, I: Interner> ProofTreeBuilder<D> {
343291
if let Some(this) = self.as_mut() {
344292
match (this, *goal_evaluation_step.state.unwrap()) {
345293
(
346-
DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluations),
294+
DebugSolver::GoalEvaluation(goal_evaluation),
347295
DebugSolver::CanonicalGoalEvaluationStep(goal_evaluation_step),
348296
) => {
349-
canonical_goal_evaluations.final_revision = Some(goal_evaluation_step);
297+
goal_evaluation.final_revision = Some(goal_evaluation_step);
350298
}
351299
_ => unreachable!(),
352300
}
@@ -489,8 +437,8 @@ impl<D: SolverDelegate<Interner = I>, I: Interner> ProofTreeBuilder<D> {
489437
pub(crate) fn query_result(&mut self, result: QueryResult<I>) {
490438
if let Some(this) = self.as_mut() {
491439
match this {
492-
DebugSolver::CanonicalGoalEvaluation(canonical_goal_evaluation) => {
493-
assert_eq!(canonical_goal_evaluation.result.replace(result), None);
440+
DebugSolver::GoalEvaluation(goal_evaluation) => {
441+
assert_eq!(goal_evaluation.result.replace(result), None);
494442
}
495443
DebugSolver::CanonicalGoalEvaluationStep(evaluation_step) => {
496444
assert_eq!(

compiler/rustc_next_trait_solver/src/solve/search_graph.rs

Lines changed: 22 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,14 @@
11
use std::convert::Infallible;
22
use std::marker::PhantomData;
33

4+
use rustc_type_ir::data_structures::ensure_sufficient_stack;
45
use rustc_type_ir::search_graph::{self, PathKind};
56
use rustc_type_ir::solve::{CanonicalInput, Certainty, NoSolution, QueryResult};
67
use rustc_type_ir::{Interner, TypingMode};
78

8-
use super::inspect::ProofTreeBuilder;
9-
use super::{FIXPOINT_STEP_LIMIT, has_no_inference_or_external_constraints};
109
use crate::delegate::SolverDelegate;
10+
use crate::solve::inspect::ProofTreeBuilder;
11+
use crate::solve::{EvalCtxt, FIXPOINT_STEP_LIMIT, has_no_inference_or_external_constraints};
1112

1213
/// This type is never constructed. We only use it to implement `search_graph::Delegate`
1314
/// for all types which impl `SolverDelegate` and doing it directly fails in coherence.
@@ -47,7 +48,9 @@ where
4748
) -> QueryResult<I> {
4849
match kind {
4950
PathKind::Coinductive => response_no_constraints(cx, input, Certainty::Yes),
50-
PathKind::Unknown => response_no_constraints(cx, input, Certainty::overflow(false)),
51+
PathKind::Unknown | PathKind::ForcedAmbiguity => {
52+
response_no_constraints(cx, input, Certainty::overflow(false))
53+
}
5154
// Even though we know these cycles to be unproductive, we still return
5255
// overflow during coherence. This is both as we are not 100% confident in
5356
// the implementation yet and any incorrect errors would be unsound there.
@@ -80,8 +83,8 @@ where
8083

8184
fn on_stack_overflow(
8285
cx: I,
83-
inspect: &mut ProofTreeBuilder<D>,
8486
input: CanonicalInput<I>,
87+
inspect: &mut ProofTreeBuilder<D>,
8588
) -> QueryResult<I> {
8689
inspect.canonical_goal_evaluation_overflow();
8790
response_no_constraints(cx, input, Certainty::overflow(true))
@@ -106,6 +109,21 @@ where
106109
let certainty = from_result.unwrap().value.certainty;
107110
response_no_constraints(cx, for_input, certainty)
108111
}
112+
113+
fn compute_goal(
114+
search_graph: &mut SearchGraph<D>,
115+
cx: I,
116+
input: CanonicalInput<I>,
117+
inspect: &mut Self::ProofTreeBuilder,
118+
) -> QueryResult<I> {
119+
ensure_sufficient_stack(|| {
120+
EvalCtxt::enter_canonical(cx, search_graph, input, inspect, |ecx, goal| {
121+
let result = ecx.compute_goal(goal);
122+
ecx.inspect.query_result(result);
123+
result
124+
})
125+
})
126+
}
109127
}
110128

111129
fn response_no_constraints<I: Interner>(

compiler/rustc_trait_selection/src/solve/inspect/analyse.rs

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,7 @@ pub struct InspectGoal<'a, 'tcx> {
3737
orig_values: Vec<ty::GenericArg<'tcx>>,
3838
goal: Goal<'tcx, ty::Predicate<'tcx>>,
3939
result: Result<Certainty, NoSolution>,
40-
evaluation_kind: inspect::CanonicalGoalEvaluationKind<TyCtxt<'tcx>>,
40+
evaluation_kind: inspect::GoalEvaluationKind<TyCtxt<'tcx>>,
4141
normalizes_to_term_hack: Option<NormalizesToTermHack<'tcx>>,
4242
source: GoalSource,
4343
}
@@ -393,8 +393,8 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
393393
let mut candidates = vec![];
394394
let last_eval_step = match &self.evaluation_kind {
395395
// An annoying edge case in case the recursion limit is 0.
396-
inspect::CanonicalGoalEvaluationKind::Overflow => return vec![],
397-
inspect::CanonicalGoalEvaluationKind::Evaluation { final_revision } => final_revision,
396+
inspect::GoalEvaluationKind::Overflow => return vec![],
397+
inspect::GoalEvaluationKind::Evaluation { final_revision } => final_revision,
398398
};
399399

400400
let mut nested_goals = vec![];
@@ -426,10 +426,10 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
426426
) -> Self {
427427
let infcx = <&SolverDelegate<'tcx>>::from(infcx);
428428

429-
let inspect::GoalEvaluation { uncanonicalized_goal, orig_values, evaluation } = root;
429+
let inspect::GoalEvaluation { uncanonicalized_goal, orig_values, kind, result } = root;
430430
// If there's a normalizes-to goal, AND the evaluation result with the result of
431431
// constraining the normalizes-to RHS and computing the nested goals.
432-
let result = evaluation.result.and_then(|ok| {
432+
let result = result.and_then(|ok| {
433433
let nested_goals_certainty =
434434
term_hack_and_nested_certainty.map_or(Ok(Certainty::Yes), |(_, c)| c)?;
435435
Ok(ok.value.certainty.and(nested_goals_certainty))
@@ -441,7 +441,7 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
441441
orig_values,
442442
goal: eager_resolve_vars(infcx, uncanonicalized_goal),
443443
result,
444-
evaluation_kind: evaluation.kind,
444+
evaluation_kind: kind,
445445
normalizes_to_term_hack: term_hack_and_nested_certainty.map(|(n, _)| n),
446446
source,
447447
}

0 commit comments

Comments
 (0)