@@ -39,13 +39,15 @@ struct StackEntry<'tcx> {
39
39
/// for the top of the stack and lazily updated for the rest.
40
40
reached_depth : StackDepth ,
41
41
42
- /// Whether this entry is a non-root cycle participant.
42
+ /// If this entry is a non-root cycle participant, the depth of all
43
+ /// cycle heads accessed while computing this goal in increasing
44
+ /// order.
43
45
///
44
46
/// We must not move the result of non-root cycle participants to the
45
47
/// global cache. See [SearchGraph::cycle_participants] for more details.
46
48
/// We store the highest stack depth of a head of a cycle this goal is involved
47
49
/// in. This necessary to soundly cache its provisional result.
48
- non_root_cycle_participant : Option < StackDepth > ,
50
+ cycle_heads : Vec < StackDepth > ,
49
51
50
52
encountered_overflow : bool ,
51
53
@@ -66,10 +68,16 @@ struct DetachedEntry<'tcx> {
66
68
/// B :- C
67
69
/// C :- A + B + C
68
70
/// ```
69
- head : StackDepth ,
71
+ heads : Vec < StackDepth > ,
70
72
result : QueryResult < ' tcx > ,
71
73
}
72
74
75
+ impl < ' tcx > DetachedEntry < ' tcx > {
76
+ fn head ( & self ) -> StackDepth {
77
+ * self . heads . last ( ) . unwrap ( )
78
+ }
79
+ }
80
+
73
81
/// Stores the stack depth of a currently evaluated goal *and* already
74
82
/// computed results for goals which depend on other goals still on the stack.
75
83
///
@@ -97,11 +105,51 @@ impl<'tcx> ProvisionalCacheEntry<'tcx> {
97
105
}
98
106
}
99
107
108
+ #[ derive( Debug ) ]
109
+ struct ReuseableProvisionalCacheEntry < ' tcx > {
110
+ heads : Vec < StackDepth > ,
111
+ provisional_results : Vec < QueryResult < ' tcx > > ,
112
+ is_coinductive : bool ,
113
+
114
+ result : QueryResult < ' tcx > ,
115
+ }
116
+
117
+ impl < ' tcx > ReuseableProvisionalCacheEntry < ' tcx > {
118
+ fn is_applicable (
119
+ & self ,
120
+ tcx : TyCtxt < ' tcx > ,
121
+ stack : & IndexVec < StackDepth , StackEntry < ' tcx > > ,
122
+ ) -> bool {
123
+ itertools:: zip_eq ( & self . heads , & self . provisional_results ) . all ( |( & stack_depth, & result) | {
124
+ let actual = match stack[ stack_depth] . provisional_result {
125
+ Some ( actual) => actual,
126
+ None => {
127
+ let is_coinductive_cycle =
128
+ self . is_coinductive && SearchGraph :: stack_coinductive_from ( tcx, stack, stack_depth) ;
129
+ let input = stack[ stack_depth] . input ;
130
+ if is_coinductive_cycle {
131
+ SearchGraph :: response_no_constraints ( tcx, input, Certainty :: Yes )
132
+ } else {
133
+ SearchGraph :: response_no_constraints ( tcx, input, Certainty :: overflow ( false ) )
134
+ }
135
+ }
136
+ } ;
137
+
138
+ actual == result
139
+ } )
140
+ }
141
+ }
142
+
100
143
/// The provisional result for a given goal. It is only applicable if
101
144
/// we access the goal with the same stack as during the last itereation.
145
+ #[ derive( Debug ) ]
102
146
struct ProvisionalResult < ' tcx > {
103
147
stack : IndexVec < StackDepth , CanonicalInput < ' tcx > > ,
148
+
104
149
result : QueryResult < ' tcx > ,
150
+
151
+ provisional_cache_entries :
152
+ FxHashMap < CanonicalInput < ' tcx > , ReuseableProvisionalCacheEntry < ' tcx > > ,
105
153
}
106
154
107
155
impl < ' tcx > ProvisionalResult < ' tcx > {
@@ -154,13 +202,17 @@ impl<'tcx> CycleData<'tcx> {
154
202
& mut self ,
155
203
stack : & mut IndexVec < StackDepth , StackEntry < ' tcx > > ,
156
204
usage_kind : HasBeenUsed ,
157
- head : StackDepth ,
205
+ heads : & [ StackDepth ] ,
158
206
) {
207
+ let head = * heads. last ( ) . unwrap ( ) ;
159
208
stack[ head] . has_been_used |= usage_kind;
160
209
debug_assert ! ( !stack[ head] . has_been_used. is_empty( ) ) ;
161
210
self . root = self . root . min ( head) ;
162
211
for entry in & mut stack. raw [ head. index ( ) + 1 ..] {
163
- entry. non_root_cycle_participant = entry. non_root_cycle_participant . max ( Some ( head) ) ;
212
+ // TODO
213
+ entry. cycle_heads . extend ( heads) ;
214
+ entry. cycle_heads . sort ( ) ;
215
+ entry. cycle_heads . dedup ( ) ;
164
216
self . cycle_participants . insert ( entry. input ) ;
165
217
}
166
218
@@ -173,28 +225,63 @@ impl<'tcx> CycleData<'tcx> {
173
225
stack : & IndexVec < StackDepth , StackEntry < ' tcx > > ,
174
226
entry : & StackEntry < ' tcx > ,
175
227
result : QueryResult < ' tcx > ,
228
+ provisional_cache_entries : FxHashMap <
229
+ CanonicalInput < ' tcx > ,
230
+ ReuseableProvisionalCacheEntry < ' tcx > ,
231
+ > ,
176
232
) {
177
233
// Add this provisional result for this goal, optionally overwriting its previous entry.
178
- let provisional_result =
179
- ProvisionalResult { stack : stack. iter ( ) . map ( |e| e. input ) . collect ( ) , result } ;
234
+ let provisional_result = ProvisionalResult {
235
+ stack : stack. iter ( ) . map ( |e| e. input ) . collect ( ) ,
236
+ result,
237
+ provisional_cache_entries,
238
+ } ;
180
239
let provisional_results = self . provisional_results . entry ( entry. input ) . or_default ( ) ;
181
- provisional_results. retain ( |result| !result. is_applicable ( stack) ) ;
240
+ if cfg ! ( debug_assertions) {
241
+ if let Some ( r) = provisional_results. iter ( ) . find ( |r| r. is_applicable ( stack) ) {
242
+ bug ! ( "existing provisional result: {r:?}" ) ;
243
+ }
244
+ }
245
+
182
246
provisional_results. push ( provisional_result) ;
183
247
}
184
248
249
+ /// This also adds entries to the provisional cache.
185
250
fn get_provisional_result (
186
251
& mut self ,
187
- stack : & IndexVec < StackDepth , StackEntry < ' tcx > > ,
252
+ tcx : TyCtxt < ' tcx > ,
253
+ stack : & mut IndexVec < StackDepth , StackEntry < ' tcx > > ,
254
+ provisional_cache : & mut FxHashMap < CanonicalInput < ' tcx > , ProvisionalCacheEntry < ' tcx > > ,
188
255
input : CanonicalInput < ' tcx > ,
189
256
) -> Option < QueryResult < ' tcx > > {
190
- self . provisional_results . get ( & input) . and_then ( |results| {
191
- for result in results {
192
- if result. is_applicable ( stack) {
193
- return Some ( result. result ) ;
257
+ self . provisional_results . get_mut ( & input) . and_then ( |results| {
258
+ let idx = results. iter ( ) . position ( |r| r. is_applicable ( stack) ) ?;
259
+ let result = results. remove ( idx) ;
260
+
261
+ #[ allow( rustc:: potential_query_instability) ]
262
+ for ( input, entry) in result. provisional_cache_entries {
263
+ if entry. is_applicable ( tcx, stack) {
264
+ let cache_entry = provisional_cache. entry ( input) . or_default ( ) ;
265
+ let mut heads = entry. heads ;
266
+
267
+ for head in heads. iter ( ) . copied ( ) {
268
+ let is_coinductive_cycle =
269
+ entry. is_coinductive && SearchGraph :: stack_coinductive_from ( tcx, stack, head) ;
270
+
271
+ if is_coinductive_cycle {
272
+ stack[ head] . has_been_used |= HasBeenUsed :: COINDUCTIVE_CYCLE
273
+ } else {
274
+ stack[ head] . has_been_used |= HasBeenUsed :: INDUCTIVE_CYCLE
275
+ } ;
276
+ }
277
+ heads. push ( stack. next_index ( ) ) ;
278
+ cache_entry. with_inductive_stack =
279
+ Some ( DetachedEntry { heads : heads. clone ( ) , result : entry. result } ) ;
280
+ cache_entry. with_coinductive_stack =
281
+ Some ( DetachedEntry { heads, result : entry. result } ) ;
194
282
}
195
283
}
196
-
197
- None
284
+ Some ( result. result )
198
285
} )
199
286
}
200
287
}
@@ -316,11 +403,17 @@ impl<'tcx> SearchGraph<'tcx> {
316
403
fn clear_dependent_provisional_results (
317
404
provisional_cache : & mut FxHashMap < CanonicalInput < ' tcx > , ProvisionalCacheEntry < ' tcx > > ,
318
405
head : StackDepth ,
406
+ mut f : impl FnMut (
407
+ CanonicalInput < ' tcx > ,
408
+ Option < DetachedEntry < ' tcx > > ,
409
+ Option < DetachedEntry < ' tcx > > ,
410
+ ) ,
319
411
) {
320
412
#[ allow( rustc:: potential_query_instability) ]
321
- provisional_cache. retain ( |_, entry| {
322
- entry. with_coinductive_stack . take_if ( |p| p. head == head) ;
323
- entry. with_inductive_stack . take_if ( |p| p. head == head) ;
413
+ provisional_cache. retain ( |input, entry| {
414
+ let coinductive = entry. with_coinductive_stack . take_if ( |p| p. head ( ) == head) ;
415
+ let inductive = entry. with_inductive_stack . take_if ( |p| p. head ( ) == head) ;
416
+ f ( * input, coinductive, inductive) ;
324
417
!entry. is_empty ( )
325
418
} ) ;
326
419
}
@@ -388,12 +481,12 @@ impl<'tcx> SearchGraph<'tcx> {
388
481
if let Some ( entry) = cache_entry
389
482
. with_coinductive_stack
390
483
. as_ref ( )
391
- . filter ( |p| Self :: stack_coinductive_from ( tcx, & self . stack , p. head ) )
484
+ . filter ( |p| Self :: stack_coinductive_from ( tcx, & self . stack , p. head ( ) ) )
392
485
. or_else ( || {
393
486
cache_entry
394
487
. with_inductive_stack
395
488
. as_ref ( )
396
- . filter ( |p| !Self :: stack_coinductive_from ( tcx, & self . stack , p. head ) )
489
+ . filter ( |p| !Self :: stack_coinductive_from ( tcx, & self . stack , p. head ( ) ) )
397
490
} )
398
491
{
399
492
debug ! ( "provisional cache hit" ) ;
@@ -406,7 +499,7 @@ impl<'tcx> SearchGraph<'tcx> {
406
499
self . cycle_data . as_mut ( ) . unwrap ( ) . tag_cycle_participants (
407
500
& mut self . stack ,
408
501
HasBeenUsed :: empty ( ) ,
409
- entry. head ,
502
+ & entry. heads ,
410
503
) ;
411
504
return entry. result ;
412
505
} else if let Some ( stack_depth) = cache_entry. stack_depth {
@@ -426,7 +519,7 @@ impl<'tcx> SearchGraph<'tcx> {
426
519
} ;
427
520
428
521
let cycle_data = self . cycle_data . get_or_insert_with ( || CycleData :: new ( stack_depth) ) ;
429
- cycle_data. tag_cycle_participants ( & mut self . stack , usage_kind, stack_depth) ;
522
+ cycle_data. tag_cycle_participants ( & mut self . stack , usage_kind, & [ stack_depth] ) ;
430
523
431
524
// Return the provisional result or, if we're in the first iteration,
432
525
// start with no constraints.
@@ -440,21 +533,27 @@ impl<'tcx> SearchGraph<'tcx> {
440
533
} else {
441
534
// No entry, we push this goal on the stack and try to prove it.
442
535
let depth = self . stack . next_index ( ) ;
443
- let provisional_result = self
444
- . cycle_data
445
- . as_mut ( )
446
- . and_then ( |cycle_data| cycle_data. get_provisional_result ( & self . stack , input) ) ;
536
+ cache_entry. stack_depth = Some ( depth) ;
537
+ let provisional_result = self . cycle_data . as_mut ( ) . and_then ( |cycle_data| {
538
+ cycle_data. get_provisional_result (
539
+ tcx,
540
+ & mut self . stack ,
541
+ & mut self . provisional_cache ,
542
+ input,
543
+ )
544
+ } ) ;
545
+ let has_been_used =
546
+ provisional_result. map_or ( HasBeenUsed :: empty ( ) , |_| HasBeenUsed :: all ( ) ) ;
447
547
let entry = StackEntry {
448
548
input,
449
549
available_depth,
450
550
reached_depth : depth,
451
- non_root_cycle_participant : None ,
551
+ cycle_heads : Default :: default ( ) ,
452
552
encountered_overflow : false ,
453
- has_been_used : HasBeenUsed :: empty ( ) ,
553
+ has_been_used,
454
554
provisional_result,
455
555
} ;
456
556
assert_eq ! ( self . stack. push( entry) , depth) ;
457
- cache_entry. stack_depth = Some ( depth) ;
458
557
}
459
558
460
559
// This is for global caching, so we properly track query dependencies.
@@ -467,7 +566,7 @@ impl<'tcx> SearchGraph<'tcx> {
467
566
// of this we continuously recompute the cycle until the result
468
567
// of the previous iteration is equal to the final result, at which
469
568
// point we are done.
470
- for i in 0 ..FIXPOINT_STEP_LIMIT {
569
+ for _ in 0 ..FIXPOINT_STEP_LIMIT {
471
570
let result = prove_goal ( self , inspect) ;
472
571
let entry = self . pop_stack ( ) ;
473
572
debug_assert_eq ! ( entry. input, input) ;
@@ -485,13 +584,6 @@ impl<'tcx> SearchGraph<'tcx> {
485
584
// See tests/ui/traits/next-solver/cycles/fixpoint-rerun-all-cycle-heads.rs
486
585
// for an example.
487
586
488
- // Start by clearing all provisional cache entries which depend on this
489
- // the current goal.
490
- Self :: clear_dependent_provisional_results (
491
- & mut self . provisional_cache ,
492
- self . stack . next_index ( ) ,
493
- ) ;
494
-
495
587
// Check whether we reached a fixpoint, either because the final result
496
588
// is equal to the provisional result of the previous iteration, or because
497
589
// this was only the root of either coinductive or inductive cycles, and the
@@ -510,9 +602,63 @@ impl<'tcx> SearchGraph<'tcx> {
510
602
// If we did not reach a fixpoint, update the provisional result and reevaluate.
511
603
if reached_fixpoint {
512
604
let cycle_data = self . cycle_data . as_mut ( ) . unwrap ( ) ;
513
- cycle_data. add_provisional_result ( & self . stack , & entry, result) ;
605
+ let mut provisional_cache_entries = FxHashMap :: default ( ) ;
606
+ Self :: clear_dependent_provisional_results (
607
+ & mut self . provisional_cache ,
608
+ self . stack . next_index ( ) ,
609
+ |input, coinductive, inductive| {
610
+ let ( mut entry, is_coinductive) = match ( coinductive, inductive) {
611
+ ( Some ( entry) , None ) => ( entry, true ) ,
612
+ ( None , Some ( entry) ) => ( entry, false ) ,
613
+ _ => return ,
614
+ } ;
615
+
616
+ assert_eq ! ( entry. heads. pop( ) , Some ( self . stack. next_index( ) ) ) ;
617
+ let provisional_results = entry
618
+ . heads
619
+ . iter ( )
620
+ . map ( |& head| {
621
+ let is_coinductive_cycle = is_coinductive
622
+ && Self :: stack_coinductive_from ( tcx, & self . stack , head) ;
623
+ if let Some ( result) = self . stack [ head] . provisional_result {
624
+ result
625
+ } else if is_coinductive_cycle {
626
+ Self :: response_no_constraints (
627
+ tcx,
628
+ input,
629
+ Certainty :: Yes ,
630
+ )
631
+ } else {
632
+ Self :: response_no_constraints (
633
+ tcx,
634
+ input,
635
+ Certainty :: overflow ( false ) ,
636
+ )
637
+ }
638
+ } )
639
+ . collect ( ) ;
640
+ let entry = ReuseableProvisionalCacheEntry {
641
+ heads : entry. heads ,
642
+ provisional_results,
643
+ is_coinductive,
644
+ result : entry. result ,
645
+ } ;
646
+ provisional_cache_entries. insert ( input, entry) ;
647
+ } ,
648
+ ) ;
649
+ cycle_data. add_provisional_result (
650
+ & self . stack ,
651
+ & entry,
652
+ result,
653
+ provisional_cache_entries,
654
+ ) ;
514
655
return ( entry, result) ;
515
656
} else {
657
+ Self :: clear_dependent_provisional_results (
658
+ & mut self . provisional_cache ,
659
+ self . stack . next_index ( ) ,
660
+ |_, _, _| { } ,
661
+ ) ;
516
662
let depth = self . stack . push ( StackEntry {
517
663
has_been_used : HasBeenUsed :: empty ( ) ,
518
664
provisional_result : Some ( result) ,
@@ -534,17 +680,7 @@ impl<'tcx> SearchGraph<'tcx> {
534
680
// We're now done with this goal. In case this goal is involved in a larger cycle
535
681
// do not remove it from the provisional cache and update its provisional result.
536
682
// We only add the root of cycles to the global cache.
537
- if let Some ( head) = final_entry. non_root_cycle_participant {
538
- let coinductive_stack = Self :: stack_coinductive_from ( tcx, & self . stack , head) ;
539
-
540
- let entry = self . provisional_cache . get_mut ( & input) . unwrap ( ) ;
541
- entry. stack_depth = None ;
542
- if coinductive_stack {
543
- entry. with_coinductive_stack = Some ( DetachedEntry { head, result } ) ;
544
- } else {
545
- entry. with_inductive_stack = Some ( DetachedEntry { head, result } ) ;
546
- }
547
- } else {
683
+ if final_entry. cycle_heads . is_empty ( ) {
548
684
self . provisional_cache . remove ( & input) ;
549
685
let reached_depth = final_entry. reached_depth . as_usize ( ) - self . stack . len ( ) ;
550
686
// When encountering a cycle, both inductive and coinductive, we only
@@ -573,6 +709,17 @@ impl<'tcx> SearchGraph<'tcx> {
573
709
dep_node,
574
710
result,
575
711
)
712
+ } else {
713
+ let heads = final_entry. cycle_heads ;
714
+ let coinductive_stack =
715
+ Self :: stack_coinductive_from ( tcx, & self . stack , * heads. last ( ) . unwrap ( ) ) ;
716
+ let entry = self . provisional_cache . get_mut ( & input) . unwrap ( ) ;
717
+ entry. stack_depth = None ;
718
+ if coinductive_stack {
719
+ entry. with_coinductive_stack = Some ( DetachedEntry { heads, result } ) ;
720
+ } else {
721
+ entry. with_inductive_stack = Some ( DetachedEntry { heads, result } ) ;
722
+ }
576
723
}
577
724
578
725
result
0 commit comments