From f99c9ffd88cd6d1954c444e86fe98b3e05333edd Mon Sep 17 00:00:00 2001 From: lcnr Date: Mon, 20 May 2024 03:12:05 +0000 Subject: [PATCH] track cycle participants per entry --- .../src/solve/search_graph.rs | 178 +++++++++++++----- .../incompleteness-unstable-result.rs | 2 + ...ncompleteness-unstable-result.with.stderr} | 6 +- ...ompleteness-unstable-result.without.stderr | 26 +++ 4 files changed, 159 insertions(+), 53 deletions(-) rename tests/ui/traits/next-solver/cycles/coinduction/{incompleteness-unstable-result.stderr => incompleteness-unstable-result.with.stderr} (87%) create mode 100644 tests/ui/traits/next-solver/cycles/coinduction/incompleteness-unstable-result.without.stderr diff --git a/compiler/rustc_trait_selection/src/solve/search_graph.rs b/compiler/rustc_trait_selection/src/solve/search_graph.rs index 6cc674dcfed1c..bcd210f789bfe 100644 --- a/compiler/rustc_trait_selection/src/solve/search_graph.rs +++ b/compiler/rustc_trait_selection/src/solve/search_graph.rs @@ -47,20 +47,39 @@ struct StackEntry { /// Whether this entry is a non-root cycle participant. /// /// We must not move the result of non-root cycle participants to the - /// global cache. See [SearchGraph::cycle_participants] for more details. - /// We store the highest stack depth of a head of a cycle this goal is involved - /// in. This necessary to soundly cache its provisional result. + /// global cache. We store the highest stack depth of a head of a cycle + /// this goal is involved in. This necessary to soundly cache its + /// provisional result. non_root_cycle_participant: Option, encountered_overflow: bool, has_been_used: HasBeenUsed, + + /// We put only the root goal of a coinductive cycle into the global cache. + /// + /// If we were to use that result when later trying to prove another cycle + /// participant, we can end up with unstable query results. + /// + /// See tests/ui/next-solver/coinduction/incompleteness-unstable-result.rs for + /// an example of where this is needed. + /// + /// There can be multiple roots on the same stack, so we need to track + /// cycle participants per root: + /// ```plain + /// A :- B + /// B :- A, C + /// C :- D + /// D :- C + /// ``` + cycle_participants: FxHashSet>, /// Starts out as `None` and gets set when rerunning this /// goal in case we encounter a cycle. provisional_result: Option>, } /// The provisional result for a goal which is not on the stack. +#[derive(Debug)] struct DetachedEntry { /// The head of the smallest non-trivial cycle involving this entry. /// @@ -110,24 +129,11 @@ pub(super) struct SearchGraph { /// An element is *deeper* in the stack if its index is *lower*. stack: IndexVec>, provisional_cache: FxHashMap, ProvisionalCacheEntry>, - /// We put only the root goal of a coinductive cycle into the global cache. - /// - /// If we were to use that result when later trying to prove another cycle - /// participant, we can end up with unstable query results. - /// - /// See tests/ui/next-solver/coinduction/incompleteness-unstable-result.rs for - /// an example of where this is needed. - cycle_participants: FxHashSet>, } impl SearchGraph { pub(super) fn new(mode: SolverMode) -> SearchGraph { - Self { - mode, - stack: Default::default(), - provisional_cache: Default::default(), - cycle_participants: Default::default(), - } + Self { mode, stack: Default::default(), provisional_cache: Default::default() } } pub(super) fn solver_mode(&self) -> SolverMode { @@ -149,13 +155,7 @@ impl SearchGraph { } pub(super) fn is_empty(&self) -> bool { - if self.stack.is_empty() { - debug_assert!(self.provisional_cache.is_empty()); - debug_assert!(self.cycle_participants.is_empty()); - true - } else { - false - } + self.stack.is_empty() } /// Returns the remaining depth allowed for nested goals. @@ -205,15 +205,26 @@ impl SearchGraph { // their result does not get moved to the global cache. fn tag_cycle_participants( stack: &mut IndexVec>, - cycle_participants: &mut FxHashSet>, usage_kind: HasBeenUsed, head: StackDepth, ) { stack[head].has_been_used |= usage_kind; debug_assert!(!stack[head].has_been_used.is_empty()); - for entry in &mut stack.raw[head.index() + 1..] { + + // The current root of these cycles. Note that this may not be the final + // root in case a later goal depends on a goal higher up the stack. + let mut current_root = head; + while let Some(parent) = stack[current_root].non_root_cycle_participant { + current_root = parent; + debug_assert!(!stack[current_root].has_been_used.is_empty()); + } + + let (stack, cycle_participants) = stack.raw.split_at_mut(head.index() + 1); + let current_cycle_root = &mut stack[current_root.as_usize()]; + for entry in cycle_participants { entry.non_root_cycle_participant = entry.non_root_cycle_participant.max(Some(head)); - cycle_participants.insert(entry.input); + current_cycle_root.cycle_participants.insert(entry.input); + current_cycle_root.cycle_participants.extend(mem::take(&mut entry.cycle_participants)); } } @@ -256,6 +267,7 @@ impl<'tcx> SearchGraph> { &mut ProofTreeBuilder>, ) -> QueryResult>, ) -> QueryResult> { + self.check_invariants(); // Check for overflow. let Some(available_depth) = Self::allowed_depth_for_nested(tcx, &self.stack) else { if let Some(last) = self.stack.raw.last_mut() { @@ -292,12 +304,7 @@ impl<'tcx> SearchGraph> { // already set correctly while computing the cache entry. inspect .goal_evaluation_kind(inspect::WipCanonicalGoalEvaluationKind::ProvisionalCacheHit); - Self::tag_cycle_participants( - &mut self.stack, - &mut self.cycle_participants, - HasBeenUsed::empty(), - entry.head, - ); + Self::tag_cycle_participants(&mut self.stack, HasBeenUsed::empty(), entry.head); return entry.result; } else if let Some(stack_depth) = cache_entry.stack_depth { debug!("encountered cycle with depth {stack_depth:?}"); @@ -314,12 +321,7 @@ impl<'tcx> SearchGraph> { } else { HasBeenUsed::INDUCTIVE_CYCLE }; - Self::tag_cycle_participants( - &mut self.stack, - &mut self.cycle_participants, - usage_kind, - stack_depth, - ); + Self::tag_cycle_participants(&mut self.stack, usage_kind, stack_depth); // Return the provisional result or, if we're in the first iteration, // start with no constraints. @@ -340,6 +342,7 @@ impl<'tcx> SearchGraph> { non_root_cycle_participant: None, encountered_overflow: false, has_been_used: HasBeenUsed::empty(), + cycle_participants: Default::default(), provisional_result: None, }; assert_eq!(self.stack.push(entry), depth); @@ -386,14 +389,13 @@ impl<'tcx> SearchGraph> { } else { self.provisional_cache.remove(&input); let reached_depth = final_entry.reached_depth.as_usize() - self.stack.len(); - let cycle_participants = mem::take(&mut self.cycle_participants); // When encountering a cycle, both inductive and coinductive, we only // move the root into the global cache. We also store all other cycle // participants involved. // // We must not use the global cache entry of a root goal if a cycle // participant is on the stack. This is necessary to prevent unstable - // results. See the comment of `SearchGraph::cycle_participants` for + // results. See the comment of `StackEntry::cycle_participants` for // more details. self.global_cache(tcx).insert( tcx, @@ -401,12 +403,14 @@ impl<'tcx> SearchGraph> { proof_tree, reached_depth, final_entry.encountered_overflow, - cycle_participants, + final_entry.cycle_participants, dep_node, result, ) } + self.check_invariants(); + result } @@ -416,10 +420,10 @@ impl<'tcx> SearchGraph> { fn lookup_global_cache( &mut self, tcx: TyCtxt<'tcx>, - input: CanonicalInput<'tcx>, + input: CanonicalInput>, available_depth: Limit, inspect: &mut ProofTreeBuilder>, - ) -> Option> { + ) -> Option>> { let CacheData { result, proof_tree, additional_depth, encountered_overflow } = self .global_cache(tcx) .get(tcx, input, self.stack.iter().map(|e| e.input), available_depth)?; @@ -450,12 +454,12 @@ impl<'tcx> SearchGraph> { } } -enum StepResult<'tcx> { - Done(StackEntry<'tcx>, QueryResult<'tcx>), +enum StepResult { + Done(StackEntry, QueryResult), HasChanged, } -impl<'tcx> SearchGraph<'tcx> { +impl<'tcx> SearchGraph> { /// When we encounter a coinductive cycle, we have to fetch the /// result of that cycle while we are still computing it. Because /// of this we continuously recompute the cycle until the result @@ -464,12 +468,12 @@ impl<'tcx> SearchGraph<'tcx> { fn fixpoint_step_in_task( &mut self, tcx: TyCtxt<'tcx>, - input: CanonicalInput<'tcx>, + input: CanonicalInput>, inspect: &mut ProofTreeBuilder>, prove_goal: &mut F, - ) -> StepResult<'tcx> + ) -> StepResult> where - F: FnMut(&mut Self, &mut ProofTreeBuilder>) -> QueryResult<'tcx>, + F: FnMut(&mut Self, &mut ProofTreeBuilder>) -> QueryResult>, { let result = prove_goal(self, inspect); let stack_entry = self.pop_stack(); @@ -530,3 +534,77 @@ impl<'tcx> SearchGraph<'tcx> { Ok(super::response_no_constraints_raw(tcx, goal.max_universe, goal.variables, certainty)) } } + +impl SearchGraph { + #[allow(rustc::potential_query_instability)] + fn check_invariants(&self) { + if !cfg!(debug_assertions) { + return; + } + + let SearchGraph { mode: _, stack, provisional_cache } = self; + if stack.is_empty() { + assert!(provisional_cache.is_empty()); + } + + for (depth, entry) in stack.iter_enumerated() { + let StackEntry { + input, + available_depth: _, + reached_depth: _, + non_root_cycle_participant, + encountered_overflow: _, + has_been_used, + ref cycle_participants, + provisional_result, + } = *entry; + let cache_entry = provisional_cache.get(&entry.input).unwrap(); + assert_eq!(cache_entry.stack_depth, Some(depth)); + if let Some(head) = non_root_cycle_participant { + assert!(head < depth); + assert!(cycle_participants.is_empty()); + assert_ne!(stack[head].has_been_used, HasBeenUsed::empty()); + + let mut current_root = head; + while let Some(parent) = stack[current_root].non_root_cycle_participant { + current_root = parent; + } + assert!(stack[current_root].cycle_participants.contains(&input)); + } + + if !cycle_participants.is_empty() { + assert!(provisional_result.is_some() || !has_been_used.is_empty()); + for entry in stack.iter().take(depth.as_usize()) { + assert_eq!(cycle_participants.get(&entry.input), None); + } + } + } + + for (&input, entry) in &self.provisional_cache { + let ProvisionalCacheEntry { stack_depth, with_coinductive_stack, with_inductive_stack } = + entry; + assert!( + stack_depth.is_some() + || with_coinductive_stack.is_some() + || with_inductive_stack.is_some() + ); + + if let &Some(stack_depth) = stack_depth { + assert_eq!(stack[stack_depth].input, input); + } + + let check_detached = |detached_entry: &DetachedEntry| { + let DetachedEntry { head, result: _ } = *detached_entry; + assert_ne!(stack[head].has_been_used, HasBeenUsed::empty()); + }; + + if let Some(with_coinductive_stack) = with_coinductive_stack { + check_detached(with_coinductive_stack); + } + + if let Some(with_inductive_stack) = with_inductive_stack { + check_detached(with_inductive_stack); + } + } + } +} diff --git a/tests/ui/traits/next-solver/cycles/coinduction/incompleteness-unstable-result.rs b/tests/ui/traits/next-solver/cycles/coinduction/incompleteness-unstable-result.rs index 7eea81ce03c66..920f8add50795 100644 --- a/tests/ui/traits/next-solver/cycles/coinduction/incompleteness-unstable-result.rs +++ b/tests/ui/traits/next-solver/cycles/coinduction/incompleteness-unstable-result.rs @@ -1,3 +1,4 @@ +//@ revisions: with without //@ compile-flags: -Znext-solver #![feature(rustc_attrs)] @@ -56,6 +57,7 @@ where X: IncompleteGuidance, X: IncompleteGuidance, { + #[cfg(with)] impls_trait::, _, _, _>(); // entering the cycle from `B` works // entering the cycle from `A` fails, but would work if we were to use the cache diff --git a/tests/ui/traits/next-solver/cycles/coinduction/incompleteness-unstable-result.stderr b/tests/ui/traits/next-solver/cycles/coinduction/incompleteness-unstable-result.with.stderr similarity index 87% rename from tests/ui/traits/next-solver/cycles/coinduction/incompleteness-unstable-result.stderr rename to tests/ui/traits/next-solver/cycles/coinduction/incompleteness-unstable-result.with.stderr index ffa3f29e4bd6f..a81229e5e355c 100644 --- a/tests/ui/traits/next-solver/cycles/coinduction/incompleteness-unstable-result.stderr +++ b/tests/ui/traits/next-solver/cycles/coinduction/incompleteness-unstable-result.with.stderr @@ -1,12 +1,12 @@ error[E0277]: the trait bound `A: Trait<_, _, _>` is not satisfied - --> $DIR/incompleteness-unstable-result.rs:63:19 + --> $DIR/incompleteness-unstable-result.rs:65:19 | LL | impls_trait::, _, _, _>(); | ^^^^ the trait `Trait<_, _, _>` is not implemented for `A`, which is required by `A: Trait<_, _, _>` | = help: the trait `Trait` is implemented for `A` note: required for `A` to implement `Trait<_, _, _>` - --> $DIR/incompleteness-unstable-result.rs:32:50 + --> $DIR/incompleteness-unstable-result.rs:33:50 | LL | impl Trait for A | ^^^^^^^^^^^^^^ ^^^^ @@ -16,7 +16,7 @@ LL | A: Trait, = note: 8 redundant requirements hidden = note: required for `A` to implement `Trait<_, _, _>` note: required by a bound in `impls_trait` - --> $DIR/incompleteness-unstable-result.rs:51:28 + --> $DIR/incompleteness-unstable-result.rs:52:28 | LL | fn impls_trait, U: ?Sized, V: ?Sized, D: ?Sized>() {} | ^^^^^^^^^^^^^^ required by this bound in `impls_trait` diff --git a/tests/ui/traits/next-solver/cycles/coinduction/incompleteness-unstable-result.without.stderr b/tests/ui/traits/next-solver/cycles/coinduction/incompleteness-unstable-result.without.stderr new file mode 100644 index 0000000000000..a81229e5e355c --- /dev/null +++ b/tests/ui/traits/next-solver/cycles/coinduction/incompleteness-unstable-result.without.stderr @@ -0,0 +1,26 @@ +error[E0277]: the trait bound `A: Trait<_, _, _>` is not satisfied + --> $DIR/incompleteness-unstable-result.rs:65:19 + | +LL | impls_trait::, _, _, _>(); + | ^^^^ the trait `Trait<_, _, _>` is not implemented for `A`, which is required by `A: Trait<_, _, _>` + | + = help: the trait `Trait` is implemented for `A` +note: required for `A` to implement `Trait<_, _, _>` + --> $DIR/incompleteness-unstable-result.rs:33:50 + | +LL | impl Trait for A + | ^^^^^^^^^^^^^^ ^^^^ +... +LL | A: Trait, + | -------------- unsatisfied trait bound introduced here + = note: 8 redundant requirements hidden + = note: required for `A` to implement `Trait<_, _, _>` +note: required by a bound in `impls_trait` + --> $DIR/incompleteness-unstable-result.rs:52:28 + | +LL | fn impls_trait, U: ?Sized, V: ?Sized, D: ?Sized>() {} + | ^^^^^^^^^^^^^^ required by this bound in `impls_trait` + +error: aborting due to 1 previous error + +For more information about this error, try `rustc --explain E0277`.