@@ -18,6 +18,14 @@ rustc_index::newtype_index! {
18
18
pub struct StackDepth { }
19
19
}
20
20
21
+ bitflags:: bitflags! {
22
+ #[ derive( Debug , Clone , Copy , PartialEq , Eq ) ]
23
+ struct HasBeenUsed : u8 {
24
+ const INDUCTIVE_CYCLE = 1 << 0 ;
25
+ const COINDUCTIVE_CYCLE = 1 << 1 ;
26
+ }
27
+ }
28
+
21
29
#[ derive( Debug ) ]
22
30
struct StackEntry < ' tcx > {
23
31
input : CanonicalInput < ' tcx > ,
@@ -32,7 +40,7 @@ struct StackEntry<'tcx> {
32
40
non_root_cycle_participant : Option < StackDepth > ,
33
41
34
42
encountered_overflow : bool ,
35
- has_been_used : bool ,
43
+ has_been_used : HasBeenUsed ,
36
44
/// Starts out as `None` and gets set when rerunning this
37
45
/// goal in case we encounter a cycle.
38
46
provisional_result : Option < QueryResult < ' tcx > > ,
@@ -195,9 +203,11 @@ impl<'tcx> SearchGraph<'tcx> {
195
203
fn tag_cycle_participants (
196
204
stack : & mut IndexVec < StackDepth , StackEntry < ' tcx > > ,
197
205
cycle_participants : & mut FxHashSet < CanonicalInput < ' tcx > > ,
206
+ usage_kind : HasBeenUsed ,
198
207
head : StackDepth ,
199
208
) {
200
- stack[ head] . has_been_used = true ;
209
+ stack[ head] . has_been_used |= usage_kind;
210
+ debug_assert ! ( !stack[ head] . has_been_used. is_empty( ) ) ;
201
211
for entry in & mut stack. raw [ head. index ( ) + 1 ..] {
202
212
entry. non_root_cycle_participant = entry. non_root_cycle_participant . max ( Some ( head) ) ;
203
213
cycle_participants. insert ( entry. input ) ;
@@ -272,29 +282,33 @@ impl<'tcx> SearchGraph<'tcx> {
272
282
273
283
// Check whether the goal is in the provisional cache.
274
284
let cache_entry = self . provisional_cache . entry ( input) . or_default ( ) ;
275
- if let Some ( with_coinductive_stack) = & mut cache_entry. with_coinductive_stack
285
+ if let Some ( with_coinductive_stack) = & cache_entry. with_coinductive_stack
276
286
&& Self :: stack_coinductive_from ( tcx, & self . stack , with_coinductive_stack. head )
277
287
{
278
288
// We have a nested goal which is already in the provisional cache, use
279
- // its result.
289
+ // its result. We do not provide any usage kind as that should have been
290
+ // already set correctly while computing the cache entry.
280
291
inspect
281
292
. goal_evaluation_kind ( inspect:: WipCanonicalGoalEvaluationKind :: ProvisionalCacheHit ) ;
282
293
Self :: tag_cycle_participants (
283
294
& mut self . stack ,
284
295
& mut self . cycle_participants ,
296
+ HasBeenUsed :: empty ( ) ,
285
297
with_coinductive_stack. head ,
286
298
) ;
287
299
return with_coinductive_stack. result ;
288
- } else if let Some ( with_inductive_stack) = & mut cache_entry. with_inductive_stack
300
+ } else if let Some ( with_inductive_stack) = & cache_entry. with_inductive_stack
289
301
&& !Self :: stack_coinductive_from ( tcx, & self . stack , with_inductive_stack. head )
290
302
{
291
303
// We have a nested goal which is already in the provisional cache, use
292
- // its result.
304
+ // its result. We do not provide any usage kind as that should have been
305
+ // already set correctly while computing the cache entry.
293
306
inspect
294
307
. goal_evaluation_kind ( inspect:: WipCanonicalGoalEvaluationKind :: ProvisionalCacheHit ) ;
295
308
Self :: tag_cycle_participants (
296
309
& mut self . stack ,
297
310
& mut self . cycle_participants ,
311
+ HasBeenUsed :: empty ( ) ,
298
312
with_inductive_stack. head ,
299
313
) ;
300
314
return with_inductive_stack. result ;
@@ -310,21 +324,27 @@ impl<'tcx> SearchGraph<'tcx> {
310
324
// Finally we can return either the provisional response for that goal if we have a
311
325
// coinductive cycle or an ambiguous result if the cycle is inductive.
312
326
inspect. goal_evaluation_kind ( inspect:: WipCanonicalGoalEvaluationKind :: CycleInStack ) ;
327
+ let is_coinductive_cycle = Self :: stack_coinductive_from ( tcx, & self . stack , stack_depth) ;
328
+ let usage_kind = if is_coinductive_cycle {
329
+ HasBeenUsed :: COINDUCTIVE_CYCLE
330
+ } else {
331
+ HasBeenUsed :: INDUCTIVE_CYCLE
332
+ } ;
313
333
Self :: tag_cycle_participants (
314
334
& mut self . stack ,
315
335
& mut self . cycle_participants ,
336
+ usage_kind,
316
337
stack_depth,
317
338
) ;
339
+
340
+ // Return the provisional result or, if we're in the first iteration,
341
+ // start with no constraints.
318
342
return if let Some ( result) = self . stack [ stack_depth] . provisional_result {
319
343
result
344
+ } else if is_coinductive_cycle {
345
+ Self :: response_no_constraints ( tcx, input, Certainty :: Yes )
320
346
} else {
321
- // If we don't have a provisional result yet we're in the first iteration,
322
- // so we start with no constraints.
323
- if Self :: stack_coinductive_from ( tcx, & self . stack , stack_depth) {
324
- Self :: response_no_constraints ( tcx, input, Certainty :: Yes )
325
- } else {
326
- Self :: response_no_constraints ( tcx, input, Certainty :: OVERFLOW )
327
- }
347
+ Self :: response_no_constraints ( tcx, input, Certainty :: OVERFLOW )
328
348
} ;
329
349
} else {
330
350
// No entry, we push this goal on the stack and try to prove it.
@@ -335,7 +355,7 @@ impl<'tcx> SearchGraph<'tcx> {
335
355
reached_depth : depth,
336
356
non_root_cycle_participant : None ,
337
357
encountered_overflow : false ,
338
- has_been_used : false ,
358
+ has_been_used : HasBeenUsed :: empty ( ) ,
339
359
provisional_result : None ,
340
360
} ;
341
361
assert_eq ! ( self . stack. push( entry) , depth) ;
@@ -354,41 +374,58 @@ impl<'tcx> SearchGraph<'tcx> {
354
374
// point we are done.
355
375
for _ in 0 ..self . local_overflow_limit ( ) {
356
376
let result = prove_goal ( self , inspect) ;
377
+ let stack_entry = self . pop_stack ( ) ;
378
+ debug_assert_eq ! ( stack_entry. input, input) ;
379
+
380
+ // If the current goal is not the root of a cycle, we are done.
381
+ if stack_entry. has_been_used . is_empty ( ) {
382
+ return ( stack_entry, result) ;
383
+ }
357
384
358
- // Check whether the current goal is the root of a cycle.
359
- // If so, we have to retry proving the cycle head
360
- // until its result reaches a fixpoint. We need to do so for
361
- // all cycle heads, not only for the root.
385
+ // If it is a cycle head, we have to keep trying to prove it until
386
+ // we reach a fixpoint. We need to do so for all cycle heads,
387
+ // not only for the root.
362
388
//
363
389
// See tests/ui/traits/next-solver/cycles/fixpoint-rerun-all-cycle-heads.rs
364
390
// for an example.
365
- let stack_entry = self . pop_stack ( ) ;
366
- debug_assert_eq ! ( stack_entry. input, input) ;
367
- if stack_entry. has_been_used {
368
- Self :: clear_dependent_provisional_results (
369
- & mut self . provisional_cache ,
370
- self . stack . next_index ( ) ,
371
- ) ;
372
- }
373
391
374
- if stack_entry. has_been_used
375
- && stack_entry. provisional_result . map_or ( true , |r| r != result)
376
- {
377
- // If so, update its provisional result and reevaluate it.
392
+ // Start by clearing all provisional cache entries which depend on this
393
+ // the current goal.
394
+ Self :: clear_dependent_provisional_results (
395
+ & mut self . provisional_cache ,
396
+ self . stack . next_index ( ) ,
397
+ ) ;
398
+
399
+ // Check whether we reached a fixpoint, either because the final result
400
+ // is equal to the provisional result of the previous iteration, or because
401
+ // this was only the root of either coinductive or inductive cycles, and the
402
+ // final result is equal to the initial response for that case.
403
+ let reached_fixpoint = if let Some ( r) = stack_entry. provisional_result {
404
+ r == result
405
+ } else if stack_entry. has_been_used == HasBeenUsed :: COINDUCTIVE_CYCLE {
406
+ Self :: response_no_constraints ( tcx, input, Certainty :: Yes ) == result
407
+ } else if stack_entry. has_been_used == HasBeenUsed :: INDUCTIVE_CYCLE {
408
+ Self :: response_no_constraints ( tcx, input, Certainty :: OVERFLOW ) == result
409
+ } else {
410
+ false
411
+ } ;
412
+
413
+ if reached_fixpoint {
414
+ return ( stack_entry, result) ;
415
+ } else {
416
+ // Did not reach a fixpoint, update the provisional result and reevaluate.
378
417
let depth = self . stack . push ( StackEntry {
379
- has_been_used : false ,
418
+ has_been_used : HasBeenUsed :: empty ( ) ,
380
419
provisional_result : Some ( result) ,
381
420
..stack_entry
382
421
} ) ;
383
422
debug_assert_eq ! ( self . provisional_cache[ & input] . stack_depth, Some ( depth) ) ;
384
- } else {
385
- return ( stack_entry, result) ;
386
423
}
387
424
}
388
425
389
426
debug ! ( "canonical cycle overflow" ) ;
390
427
let current_entry = self . pop_stack ( ) ;
391
- debug_assert ! ( ! current_entry. has_been_used) ;
428
+ debug_assert ! ( current_entry. has_been_used. is_empty ( ) ) ;
392
429
let result = Self :: response_no_constraints ( tcx, input, Certainty :: OVERFLOW ) ;
393
430
( current_entry, result)
394
431
} ) ;
0 commit comments