track cycle participants per entry

Author: lcnr

compiler/rustc_trait_selection/src/solve/search_graph.rs

@@ -51,12 +51,31 @@ struct StackEntry<'tcx> {
     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:
+    /// ```text
+    /// A :- B
+    /// B :- A, C
+    /// C :- D
+    /// D :- C
+    /// ```
+    cycle_participants: FxHashSet<CanonicalInput<'tcx>>,
     /// Starts out as `None` and gets set when rerunning this
     /// goal in case we encounter a cycle.
     provisional_result: Option<QueryResult<'tcx>>,
 }
 
 /// The provisional result for a goal which is not on the stack.
+#[derive(Debug)]
 struct DetachedEntry<'tcx> {
     /// The head of the smallest non-trivial cycle involving this entry.
     ///
@@ -83,7 +102,7 @@ struct DetachedEntry<'tcx> {
 ///
 /// The provisional cache can theoretically result in changes to the observable behavior,
 /// see tests/ui/traits/next-solver/cycles/provisional-cache-impacts-behavior.rs.
-#[derive(Default)]
+#[derive(Debug, Default)]
 struct ProvisionalCacheEntry<'tcx> {
     stack_depth: Option<StackDepth>,
     with_inductive_stack: Option<DetachedEntry<'tcx>>,
@@ -98,31 +117,19 @@ impl<'tcx> ProvisionalCacheEntry<'tcx> {
     }
 }
 
+#[derive(Debug)]
 pub(super) struct SearchGraph<'tcx> {
     mode: SolverMode,
     /// The stack of goals currently being computed.
     ///
     /// An element is *deeper* in the stack if its index is *lower*.
     stack: IndexVec<StackDepth, StackEntry<'tcx>>,
     provisional_cache: FxHashMap<CanonicalInput<'tcx>, ProvisionalCacheEntry<'tcx>>,
-    /// 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<CanonicalInput<'tcx>>,
 }
 
 impl<'tcx> SearchGraph<'tcx> {
     pub(super) fn new(mode: SolverMode) -> SearchGraph<'tcx> {
-        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 {
@@ -155,13 +162,7 @@ impl<'tcx> SearchGraph<'tcx> {
     }
 
     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.
@@ -211,15 +212,26 @@ impl<'tcx> SearchGraph<'tcx> {
     // their result does not get moved to the global cache.
     fn tag_cycle_participants(
         stack: &mut IndexVec<StackDepth, StackEntry<'tcx>>,
-        cycle_participants: &mut FxHashSet<CanonicalInput<'tcx>>,
         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));
         }
     }
 
@@ -246,6 +258,7 @@ impl<'tcx> SearchGraph<'tcx> {
         inspect: &mut ProofTreeBuilder<TyCtxt<'tcx>>,
         mut prove_goal: impl FnMut(&mut Self, &mut ProofTreeBuilder<TyCtxt<'tcx>>) -> QueryResult<'tcx>,
     ) -> QueryResult<'tcx> {
+        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() {
@@ -282,12 +295,7 @@ impl<'tcx> SearchGraph<'tcx> {
             // 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:?}");
@@ -304,12 +312,7 @@ impl<'tcx> SearchGraph<'tcx> {
             } 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.
@@ -330,6 +333,7 @@ impl<'tcx> SearchGraph<'tcx> {
                 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);
@@ -376,27 +380,28 @@ impl<'tcx> SearchGraph<'tcx> {
         } 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,
                 input,
                 proof_tree,
                 reached_depth,
                 final_entry.encountered_overflow,
-                cycle_participants,
+                final_entry.cycle_participants,
                 dep_node,
                 result,
             )
         }
 
+        self.check_invariants();
+
         result
     }
 
@@ -520,3 +525,77 @@ impl<'tcx> SearchGraph<'tcx> {
         Ok(super::response_no_constraints_raw(tcx, goal.max_universe, goal.variables, certainty))
     }
 }
+
+impl<'tcx> SearchGraph<'tcx> {
+    #[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<'tcx>| {
+                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);
+            }
+        }
+    }
+}

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<u32, i8>,
     X: IncompleteGuidance<u32, i16>,
 {
+    #[cfg(with)]
     impls_trait::<B<X>, _, _, _>(); // entering the cycle from `B` works
 
     // entering the cycle from `A` fails, but would work if we were to use the cache

tests/ui/traits/next-solver/cycles/coinduction/incompleteness-unstable-result.stderr renamed to tests/ui/traits/next-solver/cycles/coinduction/incompleteness-unstable-result.with.stderr

@@ -1,12 +1,12 @@
 error[E0277]: the trait bound `A<X>: Trait<_, _, _>` is not satisfied
-  --> $DIR/incompleteness-unstable-result.rs:63:19
+  --> $DIR/incompleteness-unstable-result.rs:65:19
    |
 LL |     impls_trait::<A<X>, _, _, _>();
    |                   ^^^^ the trait `Trait<_, _, _>` is not implemented for `A<X>`, which is required by `A<X>: Trait<_, _, _>`
    |
    = help: the trait `Trait<U, V, D>` is implemented for `A<T>`
 note: required for `A<X>` to implement `Trait<_, _, _>`
-  --> $DIR/incompleteness-unstable-result.rs:32:50
+  --> $DIR/incompleteness-unstable-result.rs:33:50
    |
 LL | impl<T: ?Sized, U: ?Sized, V: ?Sized, D: ?Sized> Trait<U, V, D> for A<T>
    |                                                  ^^^^^^^^^^^^^^     ^^^^
@@ -16,7 +16,7 @@ LL |     A<T>: Trait<U, D, V>,
    = note: 8 redundant requirements hidden
    = note: required for `A<X>` 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<T: ?Sized + Trait<U, V, D>, U: ?Sized, V: ?Sized, D: ?Sized>() {}
    |                            ^^^^^^^^^^^^^^ required by this bound in `impls_trait`

tests/ui/traits/next-solver/cycles/coinduction/incompleteness-unstable-result.without.stderr

@@ -0,0 +1,26 @@
+error[E0277]: the trait bound `A<X>: Trait<_, _, _>` is not satisfied
+  --> $DIR/incompleteness-unstable-result.rs:65:19
+   |
+LL |     impls_trait::<A<X>, _, _, _>();
+   |                   ^^^^ the trait `Trait<_, _, _>` is not implemented for `A<X>`, which is required by `A<X>: Trait<_, _, _>`
+   |
+   = help: the trait `Trait<U, V, D>` is implemented for `A<T>`
+note: required for `A<X>` to implement `Trait<_, _, _>`
+  --> $DIR/incompleteness-unstable-result.rs:33:50
+   |
+LL | impl<T: ?Sized, U: ?Sized, V: ?Sized, D: ?Sized> Trait<U, V, D> for A<T>
+   |                                                  ^^^^^^^^^^^^^^     ^^^^
+...
+LL |     A<T>: Trait<U, D, V>,
+   |           -------------- unsatisfied trait bound introduced here
+   = note: 8 redundant requirements hidden
+   = note: required for `A<X>` to implement `Trait<_, _, _>`
+note: required by a bound in `impls_trait`
+  --> $DIR/incompleteness-unstable-result.rs:52:28
+   |
+LL | fn impls_trait<T: ?Sized + Trait<U, V, D>, 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`.