1- mod cache;
2-
3- use self :: cache:: ProvisionalEntry ;
41use super :: inspect;
52use super :: inspect:: ProofTreeBuilder ;
63use super :: SolverMode ;
7- use cache :: ProvisionalCache ;
4+ use rustc_data_structures :: fx :: FxHashMap ;
85use rustc_data_structures:: fx:: FxHashSet ;
96use rustc_index:: Idx ;
107use rustc_index:: IndexVec ;
@@ -27,8 +24,14 @@ struct StackEntry<'tcx> {
2724 // The maximum depth reached by this stack entry, only up-to date
2825 // for the top of the stack and lazily updated for the rest.
2926 reached_depth : StackDepth ,
27+ // In case of a cycle, the depth of the root.
28+ cycle_root_depth : StackDepth ,
29+
3030 encountered_overflow : bool ,
3131 has_been_used : bool ,
32+ /// Starts out as `None` and gets set when rerunning this
33+ /// goal in case we encounter a cycle.
34+ provisional_result : Option < QueryResult < ' tcx > > ,
3235
3336 /// We put only the root goal of a coinductive cycle into the global cache.
3437 ///
@@ -47,7 +50,7 @@ pub(super) struct SearchGraph<'tcx> {
4750 ///
4851 /// An element is *deeper* in the stack if its index is *lower*.
4952 stack : IndexVec < StackDepth , StackEntry < ' tcx > > ,
50- provisional_cache : ProvisionalCache < ' tcx > ,
53+ stack_entries : FxHashMap < CanonicalInput < ' tcx > , StackDepth > ,
5154}
5255
5356impl < ' tcx > SearchGraph < ' tcx > {
@@ -56,7 +59,7 @@ impl<'tcx> SearchGraph<'tcx> {
5659 mode,
5760 local_overflow_limit : tcx. recursion_limit ( ) . 0 . checked_ilog2 ( ) . unwrap_or ( 0 ) as usize ,
5861 stack : Default :: default ( ) ,
59- provisional_cache : ProvisionalCache :: empty ( ) ,
62+ stack_entries : Default :: default ( ) ,
6063 }
6164 }
6265
@@ -85,6 +88,7 @@ impl<'tcx> SearchGraph<'tcx> {
8588 /// would cause us to not track overflow and recursion depth correctly.
8689 fn pop_stack ( & mut self ) -> StackEntry < ' tcx > {
8790 let elem = self . stack . pop ( ) . unwrap ( ) ;
91+ assert ! ( self . stack_entries. remove( & elem. input) . is_some( ) ) ;
8892 if let Some ( last) = self . stack . raw . last_mut ( ) {
8993 last. reached_depth = last. reached_depth . max ( elem. reached_depth ) ;
9094 last. encountered_overflow |= elem. encountered_overflow ;
@@ -104,22 +108,17 @@ impl<'tcx> SearchGraph<'tcx> {
104108 }
105109
106110 pub ( super ) fn is_empty ( & self ) -> bool {
107- self . stack . is_empty ( ) && self . provisional_cache . is_empty ( )
111+ self . stack . is_empty ( )
108112 }
109113
110114 /// Whether we're currently in a cycle. This should only be used
111115 /// for debug assertions.
112116 pub ( super ) fn in_cycle ( & self ) -> bool {
113117 if let Some ( stack_depth) = self . stack . last_index ( ) {
114- // Either the current goal on the stack is the root of a cycle...
115- if self . stack [ stack_depth] . has_been_used {
116- return true ;
117- }
118-
119- // ...or it depends on a goal with a lower depth.
120- let current_goal = self . stack [ stack_depth] . input ;
121- let entry_index = self . provisional_cache . lookup_table [ & current_goal] ;
122- self . provisional_cache . entries [ entry_index] . depth != stack_depth
118+ // Either the current goal on the stack is the root of a cycle
119+ // or it depends on a goal with a lower depth.
120+ self . stack [ stack_depth] . has_been_used
121+ || self . stack [ stack_depth] . cycle_root_depth != stack_depth
123122 } else {
124123 false
125124 }
@@ -211,24 +210,23 @@ impl<'tcx> SearchGraph<'tcx> {
211210 }
212211 }
213212
214- // Look at the provisional cache to detect cycles.
215- let cache = & mut self . provisional_cache ;
216- match cache. lookup_table . entry ( input) {
213+ // Check whether we're in a cycle.
214+ match self . stack_entries . entry ( input) {
217215 // No entry, we push this goal on the stack and try to prove it.
218216 Entry :: Vacant ( v) => {
219217 let depth = self . stack . next_index ( ) ;
220218 let entry = StackEntry {
221219 input,
222220 available_depth,
223221 reached_depth : depth,
222+ cycle_root_depth : depth,
224223 encountered_overflow : false ,
225224 has_been_used : false ,
225+ provisional_result : None ,
226226 cycle_participants : Default :: default ( ) ,
227227 } ;
228228 assert_eq ! ( self . stack. push( entry) , depth) ;
229- let entry_index =
230- cache. entries . push ( ProvisionalEntry { response : None , depth, input } ) ;
231- v. insert ( entry_index) ;
229+ v. insert ( depth) ;
232230 }
233231 // We have a nested goal which relies on a goal `root` deeper in the stack.
234232 //
@@ -239,41 +237,40 @@ impl<'tcx> SearchGraph<'tcx> {
239237 //
240238 // Finally we can return either the provisional response for that goal if we have a
241239 // coinductive cycle or an ambiguous result if the cycle is inductive.
242- Entry :: Occupied ( entry_index ) => {
240+ Entry :: Occupied ( entry ) => {
243241 inspect. goal_evaluation_kind ( inspect:: WipGoalEvaluationKind :: CacheHit (
244242 CacheHit :: Provisional ,
245243 ) ) ;
246244
247- let entry_index = * entry_index. get ( ) ;
248- let stack_depth = cache. depth ( entry_index) ;
245+ let stack_depth = * entry. get ( ) ;
249246 debug ! ( "encountered cycle with depth {stack_depth:?}" ) ;
250-
251- cache. add_dependency_of_leaf_on ( entry_index) ;
252- let mut iter = self . stack . iter_mut ( ) ;
253- let root = iter. nth ( stack_depth. as_usize ( ) ) . unwrap ( ) ;
254- for e in iter {
255- root. cycle_participants . insert ( e. input ) ;
247+ // We start by updating the root depth of all cycle participants, and
248+ // add all cycle participants to the root.
249+ let root_depth = self . stack [ stack_depth] . cycle_root_depth ;
250+ let ( prev, participants) = self . stack . raw . split_at_mut ( stack_depth. as_usize ( ) + 1 ) ;
251+ let root = & mut prev[ root_depth. as_usize ( ) ] ;
252+ for entry in participants {
253+ debug_assert ! ( entry. cycle_root_depth >= root_depth) ;
254+ entry. cycle_root_depth = root_depth;
255+ root. cycle_participants . insert ( entry. input ) ;
256+ #[ allow( rustc:: potential_query_instability) ]
257+ root. cycle_participants . extend ( entry. cycle_participants . drain ( ) ) ;
256258 }
257259
258260 // If we're in a cycle, we have to retry proving the current goal
259261 // until we reach a fixpoint.
262+ //
263+ // FIXME: This previously incorrectly only set `root.has_been_used`
264+ // which should result in bugs. Try to write a test here.
260265 self . stack [ stack_depth] . has_been_used = true ;
261- return if let Some ( result) = cache . provisional_result ( entry_index ) {
266+ return if let Some ( result) = self . stack [ stack_depth ] . provisional_result {
262267 result
263268 } else {
264- // If we don't have a provisional result yet, the goal has to
265- // still be on the stack.
266- let mut goal_on_stack = false ;
267- let mut is_coinductive = true ;
268- for entry in self . stack . raw [ stack_depth. index ( ) ..]
269+ // If we don't have a provisional result yet we're in the first iteration,
270+ // so we start with no constraints.
271+ let is_coinductive = self . stack . raw [ stack_depth. index ( ) ..]
269272 . iter ( )
270- . skip_while ( |entry| entry. input != input)
271- {
272- goal_on_stack = true ;
273- is_coinductive &= entry. input . value . goal . predicate . is_coinductive ( tcx) ;
274- }
275- debug_assert ! ( goal_on_stack) ;
276-
273+ . all ( |entry| entry. input . value . goal . predicate . is_coinductive ( tcx) ) ;
277274 if is_coinductive {
278275 Self :: response_no_constraints ( tcx, input, Certainty :: Yes )
279276 } else {
@@ -294,40 +291,25 @@ impl<'tcx> SearchGraph<'tcx> {
294291 // of the previous iteration is equal to the final result, at which
295292 // point we are done.
296293 for _ in 0 ..self . local_overflow_limit ( ) {
297- let response = prove_goal ( self , inspect) ;
294+ let result = prove_goal ( self , inspect) ;
298295
299296 // Check whether the current goal is the root of a cycle and whether
300297 // we have to rerun because its provisional result differed from the
301298 // final result.
302- //
303- // Also update the response for this goal stored in the provisional
304- // cache.
305299 let stack_entry = self . pop_stack ( ) ;
306300 debug_assert_eq ! ( stack_entry. input, input) ;
307- let cache = & mut self . provisional_cache ;
308- let provisional_entry_index =
309- * cache. lookup_table . get ( & stack_entry. input ) . unwrap ( ) ;
310- let provisional_entry = & mut cache. entries [ provisional_entry_index] ;
311301 if stack_entry. has_been_used
312- && provisional_entry . response . map_or ( true , |r| r != response )
302+ && stack_entry . provisional_result . map_or ( true , |r| r != result )
313303 {
314- // If so, update the provisional result for this goal and remove
315- // all entries whose result depends on this goal from the provisional
316- // cache...
317- //
318- // That's not completely correct, as a nested goal can also only
319- // depend on a goal which is lower in the stack so it doesn't
320- // actually depend on the current goal. This should be fairly
321- // rare and is hopefully not relevant for performance.
322- provisional_entry. response = Some ( response) ;
323- #[ allow( rustc:: potential_query_instability) ]
324- cache. lookup_table . retain ( |_key, index| * index <= provisional_entry_index) ;
325- cache. entries . truncate ( provisional_entry_index. index ( ) + 1 ) ;
326-
327- // ...and finally push our goal back on the stack and reevaluate it.
328- self . stack . push ( StackEntry { has_been_used : false , ..stack_entry } ) ;
304+ // If so, update its provisional result and reevaluate it.
305+ let depth = self . stack . push ( StackEntry {
306+ has_been_used : false ,
307+ provisional_result : Some ( result) ,
308+ ..stack_entry
309+ } ) ;
310+ assert_eq ! ( self . stack_entries. insert( input, depth) , None ) ;
329311 } else {
330- return ( stack_entry, response ) ;
312+ return ( stack_entry, result ) ;
331313 }
332314 }
333315
@@ -343,17 +325,7 @@ impl<'tcx> SearchGraph<'tcx> {
343325 //
344326 // It is not possible for any nested goal to depend on something deeper on the
345327 // stack, as this would have also updated the depth of the current goal.
346- let cache = & mut self . provisional_cache ;
347- let provisional_entry_index = * cache. lookup_table . get ( & input) . unwrap ( ) ;
348- let provisional_entry = & mut cache. entries [ provisional_entry_index] ;
349- let depth = provisional_entry. depth ;
350- if depth == self . stack . next_index ( ) {
351- for ( i, entry) in cache. entries . drain_enumerated ( provisional_entry_index. index ( ) ..) {
352- let actual_index = cache. lookup_table . remove ( & entry. input ) ;
353- debug_assert_eq ! ( Some ( i) , actual_index) ;
354- debug_assert ! ( entry. depth == depth) ;
355- }
356-
328+ if final_entry. cycle_root_depth == self . stack . next_index ( ) {
357329 // When encountering a cycle, both inductive and coinductive, we only
358330 // move the root into the global cache. We also store all other cycle
359331 // participants involved.
@@ -371,8 +343,6 @@ impl<'tcx> SearchGraph<'tcx> {
371343 dep_node,
372344 result,
373345 )
374- } else {
375- provisional_entry. response = Some ( result) ;
376346 }
377347
378348 result
0 commit comments