1
- mod cache;
2
-
3
- use self :: cache:: ProvisionalEntry ;
4
1
use super :: inspect;
5
2
use super :: inspect:: ProofTreeBuilder ;
6
3
use super :: SolverMode ;
7
- use cache :: ProvisionalCache ;
4
+ use rustc_data_structures :: fx :: FxHashMap ;
8
5
use rustc_data_structures:: fx:: FxHashSet ;
9
6
use rustc_index:: Idx ;
10
7
use rustc_index:: IndexVec ;
@@ -27,8 +24,14 @@ struct StackEntry<'tcx> {
27
24
// The maximum depth reached by this stack entry, only up-to date
28
25
// for the top of the stack and lazily updated for the rest.
29
26
reached_depth : StackDepth ,
27
+ // In case of a cycle, the depth of the root.
28
+ cycle_root_depth : StackDepth ,
29
+
30
30
encountered_overflow : bool ,
31
31
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 > > ,
32
35
33
36
/// We put only the root goal of a coinductive cycle into the global cache.
34
37
///
@@ -47,7 +50,7 @@ pub(super) struct SearchGraph<'tcx> {
47
50
///
48
51
/// An element is *deeper* in the stack if its index is *lower*.
49
52
stack : IndexVec < StackDepth , StackEntry < ' tcx > > ,
50
- provisional_cache : ProvisionalCache < ' tcx > ,
53
+ stack_entries : FxHashMap < CanonicalInput < ' tcx > , StackDepth > ,
51
54
}
52
55
53
56
impl < ' tcx > SearchGraph < ' tcx > {
@@ -56,7 +59,7 @@ impl<'tcx> SearchGraph<'tcx> {
56
59
mode,
57
60
local_overflow_limit : tcx. recursion_limit ( ) . 0 . checked_ilog2 ( ) . unwrap_or ( 0 ) as usize ,
58
61
stack : Default :: default ( ) ,
59
- provisional_cache : ProvisionalCache :: empty ( ) ,
62
+ stack_entries : Default :: default ( ) ,
60
63
}
61
64
}
62
65
@@ -85,6 +88,7 @@ impl<'tcx> SearchGraph<'tcx> {
85
88
/// would cause us to not track overflow and recursion depth correctly.
86
89
fn pop_stack ( & mut self ) -> StackEntry < ' tcx > {
87
90
let elem = self . stack . pop ( ) . unwrap ( ) ;
91
+ assert ! ( self . stack_entries. remove( & elem. input) . is_some( ) ) ;
88
92
if let Some ( last) = self . stack . raw . last_mut ( ) {
89
93
last. reached_depth = last. reached_depth . max ( elem. reached_depth ) ;
90
94
last. encountered_overflow |= elem. encountered_overflow ;
@@ -104,22 +108,17 @@ impl<'tcx> SearchGraph<'tcx> {
104
108
}
105
109
106
110
pub ( super ) fn is_empty ( & self ) -> bool {
107
- self . stack . is_empty ( ) && self . provisional_cache . is_empty ( )
111
+ self . stack . is_empty ( )
108
112
}
109
113
110
114
/// Whether we're currently in a cycle. This should only be used
111
115
/// for debug assertions.
112
116
pub ( super ) fn in_cycle ( & self ) -> bool {
113
117
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
123
122
} else {
124
123
false
125
124
}
@@ -211,24 +210,23 @@ impl<'tcx> SearchGraph<'tcx> {
211
210
}
212
211
}
213
212
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) {
217
215
// No entry, we push this goal on the stack and try to prove it.
218
216
Entry :: Vacant ( v) => {
219
217
let depth = self . stack . next_index ( ) ;
220
218
let entry = StackEntry {
221
219
input,
222
220
available_depth,
223
221
reached_depth : depth,
222
+ cycle_root_depth : depth,
224
223
encountered_overflow : false ,
225
224
has_been_used : false ,
225
+ provisional_result : None ,
226
226
cycle_participants : Default :: default ( ) ,
227
227
} ;
228
228
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) ;
232
230
}
233
231
// We have a nested goal which relies on a goal `root` deeper in the stack.
234
232
//
@@ -239,41 +237,50 @@ impl<'tcx> SearchGraph<'tcx> {
239
237
//
240
238
// Finally we can return either the provisional response for that goal if we have a
241
239
// coinductive cycle or an ambiguous result if the cycle is inductive.
242
- Entry :: Occupied ( entry_index ) => {
240
+ Entry :: Occupied ( entry ) => {
243
241
inspect. goal_evaluation_kind ( inspect:: WipCanonicalGoalEvaluationKind :: CacheHit (
244
242
CacheHit :: Provisional ,
245
243
) ) ;
246
244
247
- let entry_index = * entry_index. get ( ) ;
248
- let stack_depth = cache. depth ( entry_index) ;
245
+ let stack_depth = * entry. get ( ) ;
249
246
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
+ // FIXME(@lcnr): I believe that this line is needed as we could
257
+ // otherwise access a cache entry for the root of a cycle while
258
+ // computing the result for a cycle participant. This can result
259
+ // in unstable results due to incompleteness.
260
+ //
261
+ // However, a test for this would be an even more complex version of
262
+ // tests/ui/traits/new-solver/coinduction/incompleteness-unstable-result.rs.
263
+ // I did not bother to write such a test and we have no regression test
264
+ // for this. It would be good to have such a test :)
265
+ #[ allow( rustc:: potential_query_instability) ]
266
+ root. cycle_participants . extend ( entry. cycle_participants . drain ( ) ) ;
256
267
}
257
268
258
- // If we're in a cycle, we have to retry proving the current goal
259
- // until we reach a fixpoint.
269
+ // If we're in a cycle, we have to retry proving the cycle head
270
+ // until we reach a fixpoint. It is not enough to simply retry the
271
+ // `root` goal of this cycle.
272
+ //
273
+ // See tests/ui/traits/new-solver/cycles/fixpoint-rerun-all-cycle-heads.rs
274
+ // for an example.
260
275
self . stack [ stack_depth] . has_been_used = true ;
261
- return if let Some ( result) = cache . provisional_result ( entry_index ) {
276
+ return if let Some ( result) = self . stack [ stack_depth ] . provisional_result {
262
277
result
263
278
} 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 ( ) ..]
279
+ // If we don't have a provisional result yet we're in the first iteration,
280
+ // so we start with no constraints.
281
+ let is_coinductive = self . stack . raw [ stack_depth. index ( ) ..]
269
282
. 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
-
283
+ . all ( |entry| entry. input . value . goal . predicate . is_coinductive ( tcx) ) ;
277
284
if is_coinductive {
278
285
Self :: response_no_constraints ( tcx, input, Certainty :: Yes )
279
286
} else {
@@ -294,40 +301,25 @@ impl<'tcx> SearchGraph<'tcx> {
294
301
// of the previous iteration is equal to the final result, at which
295
302
// point we are done.
296
303
for _ in 0 ..self . local_overflow_limit ( ) {
297
- let response = prove_goal ( self , inspect) ;
304
+ let result = prove_goal ( self , inspect) ;
298
305
299
306
// Check whether the current goal is the root of a cycle and whether
300
307
// we have to rerun because its provisional result differed from the
301
308
// final result.
302
- //
303
- // Also update the response for this goal stored in the provisional
304
- // cache.
305
309
let stack_entry = self . pop_stack ( ) ;
306
310
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] ;
311
311
if stack_entry. has_been_used
312
- && provisional_entry . response . map_or ( true , |r| r != response )
312
+ && stack_entry . provisional_result . map_or ( true , |r| r != result )
313
313
{
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 } ) ;
314
+ // If so, update its provisional result and reevaluate it.
315
+ let depth = self . stack . push ( StackEntry {
316
+ has_been_used : false ,
317
+ provisional_result : Some ( result) ,
318
+ ..stack_entry
319
+ } ) ;
320
+ assert_eq ! ( self . stack_entries. insert( input, depth) , None ) ;
329
321
} else {
330
- return ( stack_entry, response ) ;
322
+ return ( stack_entry, result ) ;
331
323
}
332
324
}
333
325
@@ -343,17 +335,7 @@ impl<'tcx> SearchGraph<'tcx> {
343
335
//
344
336
// It is not possible for any nested goal to depend on something deeper on the
345
337
// 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
-
338
+ if final_entry. cycle_root_depth == self . stack . next_index ( ) {
357
339
// When encountering a cycle, both inductive and coinductive, we only
358
340
// move the root into the global cache. We also store all other cycle
359
341
// participants involved.
@@ -371,8 +353,6 @@ impl<'tcx> SearchGraph<'tcx> {
371
353
dep_node,
372
354
result,
373
355
)
374
- } else {
375
- provisional_entry. response = Some ( result) ;
376
356
}
377
357
378
358
result
0 commit comments