@@ -12,7 +12,6 @@ use rustc_middle::traits::solve::CacheData;
12
12
use rustc_middle:: traits:: solve:: { CanonicalInput , Certainty , EvaluationCache , QueryResult } ;
13
13
use rustc_middle:: ty:: TyCtxt ;
14
14
use rustc_session:: Limit ;
15
- use std:: mem;
16
15
17
16
rustc_index:: newtype_index! {
18
17
#[ orderable]
@@ -98,13 +97,30 @@ impl<'tcx> ProvisionalCacheEntry<'tcx> {
98
97
}
99
98
}
100
99
101
- pub ( super ) struct SearchGraph < ' tcx > {
102
- mode : SolverMode ,
103
- /// The stack of goals currently being computed.
104
- ///
105
- /// An element is *deeper* in the stack if its index is *lower*.
106
- stack : IndexVec < StackDepth , StackEntry < ' tcx > > ,
107
- provisional_cache : FxHashMap < CanonicalInput < ' tcx > , ProvisionalCacheEntry < ' tcx > > ,
100
+ /// The provisional result for a given goal. It is only applicable if
101
+ /// we access the goal with the same stack as during the last itereation.
102
+ struct ProvisionalResult < ' tcx > {
103
+ stack : IndexVec < StackDepth , CanonicalInput < ' tcx > > ,
104
+ result : QueryResult < ' tcx > ,
105
+ }
106
+
107
+ impl < ' tcx > ProvisionalResult < ' tcx > {
108
+ fn is_applicable ( & self , stack : & IndexVec < StackDepth , StackEntry < ' tcx > > ) -> bool {
109
+ self . stack . len ( ) == stack. len ( )
110
+ && itertools:: zip_eq ( & self . stack , stack. iter ( ) . map ( |e| & e. input ) ) . all ( |( l, r) | l == r)
111
+ }
112
+ }
113
+
114
+ struct CycleData < ' tcx > {
115
+ /// The lowest stack depth of all participants. The root is the only cycle
116
+ /// participant which will get moved to the global cache.
117
+ root : StackDepth ,
118
+
119
+ /// The provisional results for all nested cycle heads we've already computed.
120
+ /// The next time we evaluate these cycle heads we use that result in the first
121
+ /// iteration.
122
+ provisional_results : FxHashMap < CanonicalInput < ' tcx > , Vec < ProvisionalResult < ' tcx > > > ,
123
+
108
124
/// We put only the root goal of a coinductive cycle into the global cache.
109
125
///
110
126
/// If we were to use that result when later trying to prove another cycle
@@ -115,13 +131,100 @@ pub(super) struct SearchGraph<'tcx> {
115
131
cycle_participants : FxHashSet < CanonicalInput < ' tcx > > ,
116
132
}
117
133
134
+ impl < ' tcx > CycleData < ' tcx > {
135
+ fn new ( root : StackDepth ) -> CycleData < ' tcx > {
136
+ CycleData {
137
+ root,
138
+ provisional_results : Default :: default ( ) ,
139
+ cycle_participants : Default :: default ( ) ,
140
+ }
141
+ }
142
+
143
+ /// When encountering a solver cycle, the result of the current goal
144
+ /// depends on goals lower on the stack.
145
+ ///
146
+ /// We have to therefore be careful when caching goals. Only the final result
147
+ /// of the cycle root, i.e. the lowest goal on the stack involved in this cycle,
148
+ /// is moved to the global cache while all others are stored in a provisional cache.
149
+ ///
150
+ /// We update both the head of this cycle to rerun its evaluation until
151
+ /// we reach a fixpoint and all other cycle participants to make sure that
152
+ /// their result does not get moved to the global cache.
153
+ fn tag_cycle_participants (
154
+ & mut self ,
155
+ stack : & mut IndexVec < StackDepth , StackEntry < ' tcx > > ,
156
+ usage_kind : HasBeenUsed ,
157
+ head : StackDepth ,
158
+ ) {
159
+ stack[ head] . has_been_used |= usage_kind;
160
+ debug_assert ! ( !stack[ head] . has_been_used. is_empty( ) ) ;
161
+ self . root = self . root . min ( head) ;
162
+ for entry in & mut stack. raw [ head. index ( ) + 1 ..] {
163
+ entry. non_root_cycle_participant = entry. non_root_cycle_participant . max ( Some ( head) ) ;
164
+ self . cycle_participants . insert ( entry. input ) ;
165
+ }
166
+
167
+ debug ! ( ?self . root, ?stack) ;
168
+ }
169
+
170
+ /// Add the provisional result for a given goal to the storage.
171
+ fn add_provisional_result (
172
+ & mut self ,
173
+ stack : & IndexVec < StackDepth , StackEntry < ' tcx > > ,
174
+ entry : & StackEntry < ' tcx > ,
175
+ result : QueryResult < ' tcx > ,
176
+ ) {
177
+ // 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 } ;
180
+ let provisional_results = self . provisional_results . entry ( entry. input ) . or_default ( ) ;
181
+ provisional_results. retain ( |result| !result. is_applicable ( stack) ) ;
182
+ provisional_results. push ( provisional_result) ;
183
+ }
184
+
185
+ fn get_provisional_result (
186
+ & mut self ,
187
+ stack : & IndexVec < StackDepth , StackEntry < ' tcx > > ,
188
+ input : CanonicalInput < ' tcx > ,
189
+ ) -> 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 ) ;
194
+ }
195
+ }
196
+
197
+ None
198
+ } )
199
+ }
200
+ }
201
+
202
+ pub ( super ) struct SearchGraph < ' tcx > {
203
+ mode : SolverMode ,
204
+ /// The stack of goals currently being computed.
205
+ ///
206
+ /// An element is *deeper* in the stack if its index is *lower*.
207
+ stack : IndexVec < StackDepth , StackEntry < ' tcx > > ,
208
+
209
+ /// In case we're currently in a solver cycle, we have to track a
210
+ /// lot of additional data.
211
+ cycle_data : Option < CycleData < ' tcx > > ,
212
+
213
+ /// A cache for the result of nested goals which depend on goals currently on the
214
+ /// stack. We remove cached results once we pop any goal used while computing it.
215
+ ///
216
+ /// This is not part of `cycle_data` as it contains all stack entries even while we're
217
+ /// not yet in a cycle.
218
+ provisional_cache : FxHashMap < CanonicalInput < ' tcx > , ProvisionalCacheEntry < ' tcx > > ,
219
+ }
220
+
118
221
impl < ' tcx > SearchGraph < ' tcx > {
119
222
pub ( super ) fn new ( mode : SolverMode ) -> SearchGraph < ' tcx > {
120
223
Self {
121
224
mode,
122
225
stack : Default :: default ( ) ,
226
+ cycle_data : None ,
123
227
provisional_cache : Default :: default ( ) ,
124
- cycle_participants : Default :: default ( ) ,
125
228
}
126
229
}
127
230
@@ -165,9 +268,10 @@ impl<'tcx> SearchGraph<'tcx> {
165
268
}
166
269
167
270
pub ( super ) fn is_empty ( & self ) -> bool {
168
- if self . stack . is_empty ( ) {
169
- debug_assert ! ( self . provisional_cache. is_empty( ) ) ;
170
- debug_assert ! ( self . cycle_participants. is_empty( ) ) ;
271
+ let Self { mode : _, stack, cycle_data, provisional_cache } = self ;
272
+ if stack. is_empty ( ) {
273
+ debug_assert ! ( cycle_data. is_none( ) ) ;
274
+ debug_assert ! ( provisional_cache. is_empty( ) ) ;
171
275
true
172
276
} else {
173
277
false
@@ -209,30 +313,6 @@ impl<'tcx> SearchGraph<'tcx> {
209
313
. all ( |entry| entry. input . value . goal . predicate . is_coinductive ( tcx) )
210
314
}
211
315
212
- // When encountering a solver cycle, the result of the current goal
213
- // depends on goals lower on the stack.
214
- //
215
- // We have to therefore be careful when caching goals. Only the final result
216
- // of the cycle root, i.e. the lowest goal on the stack involved in this cycle,
217
- // is moved to the global cache while all others are stored in a provisional cache.
218
- //
219
- // We update both the head of this cycle to rerun its evaluation until
220
- // we reach a fixpoint and all other cycle participants to make sure that
221
- // their result does not get moved to the global cache.
222
- fn tag_cycle_participants (
223
- stack : & mut IndexVec < StackDepth , StackEntry < ' tcx > > ,
224
- cycle_participants : & mut FxHashSet < CanonicalInput < ' tcx > > ,
225
- usage_kind : HasBeenUsed ,
226
- head : StackDepth ,
227
- ) {
228
- stack[ head] . has_been_used |= usage_kind;
229
- debug_assert ! ( !stack[ head] . has_been_used. is_empty( ) ) ;
230
- for entry in & mut stack. raw [ head. index ( ) + 1 ..] {
231
- entry. non_root_cycle_participant = entry. non_root_cycle_participant . max ( Some ( head) ) ;
232
- cycle_participants. insert ( entry. input ) ;
233
- }
234
- }
235
-
236
316
fn clear_dependent_provisional_results (
237
317
provisional_cache : & mut FxHashMap < CanonicalInput < ' tcx > , ProvisionalCacheEntry < ' tcx > > ,
238
318
head : StackDepth ,
@@ -322,9 +402,9 @@ impl<'tcx> SearchGraph<'tcx> {
322
402
// already set correctly while computing the cache entry.
323
403
inspect
324
404
. goal_evaluation_kind ( inspect:: WipCanonicalGoalEvaluationKind :: ProvisionalCacheHit ) ;
325
- Self :: tag_cycle_participants (
405
+
406
+ self . cycle_data . as_mut ( ) . unwrap ( ) . tag_cycle_participants (
326
407
& mut self . stack ,
327
- & mut self . cycle_participants ,
328
408
HasBeenUsed :: empty ( ) ,
329
409
entry. head ,
330
410
) ;
@@ -344,12 +424,9 @@ impl<'tcx> SearchGraph<'tcx> {
344
424
} else {
345
425
HasBeenUsed :: INDUCTIVE_CYCLE
346
426
} ;
347
- Self :: tag_cycle_participants (
348
- & mut self . stack ,
349
- & mut self . cycle_participants ,
350
- usage_kind,
351
- stack_depth,
352
- ) ;
427
+
428
+ 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) ;
353
430
354
431
// Return the provisional result or, if we're in the first iteration,
355
432
// start with no constraints.
@@ -363,14 +440,18 @@ impl<'tcx> SearchGraph<'tcx> {
363
440
} else {
364
441
// No entry, we push this goal on the stack and try to prove it.
365
442
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) ) ;
366
447
let entry = StackEntry {
367
448
input,
368
449
available_depth,
369
450
reached_depth : depth,
370
451
non_root_cycle_participant : None ,
371
452
encountered_overflow : false ,
372
453
has_been_used : HasBeenUsed :: empty ( ) ,
373
- provisional_result : None ,
454
+ provisional_result,
374
455
} ;
375
456
assert_eq ! ( self . stack. push( entry) , depth) ;
376
457
cache_entry. stack_depth = Some ( depth) ;
@@ -386,14 +467,15 @@ impl<'tcx> SearchGraph<'tcx> {
386
467
// of this we continuously recompute the cycle until the result
387
468
// of the previous iteration is equal to the final result, at which
388
469
// point we are done.
389
- for _ in 0 ..FIXPOINT_STEP_LIMIT {
470
+ for i in 0 ..FIXPOINT_STEP_LIMIT {
390
471
let result = prove_goal ( self , inspect) ;
391
- let stack_entry = self . pop_stack ( ) ;
392
- debug_assert_eq ! ( stack_entry . input, input) ;
472
+ let entry = self . pop_stack ( ) ;
473
+ debug_assert_eq ! ( entry . input, input) ;
393
474
394
- // If the current goal is not the root of a cycle, we are done.
395
- if stack_entry. has_been_used . is_empty ( ) {
396
- return ( stack_entry, result) ;
475
+ // For goals which are not the head of a cycle, this is
476
+ // trivial.
477
+ if entry. has_been_used . is_empty ( ) {
478
+ return ( entry, result) ;
397
479
}
398
480
399
481
// If it is a cycle head, we have to keep trying to prove it until
@@ -414,25 +496,27 @@ impl<'tcx> SearchGraph<'tcx> {
414
496
// is equal to the provisional result of the previous iteration, or because
415
497
// this was only the root of either coinductive or inductive cycles, and the
416
498
// final result is equal to the initial response for that case.
417
- let reached_fixpoint = if let Some ( r) = stack_entry . provisional_result {
499
+ let reached_fixpoint = if let Some ( r) = entry . provisional_result {
418
500
r == result
419
- } else if stack_entry . has_been_used == HasBeenUsed :: COINDUCTIVE_CYCLE {
420
- Self :: response_no_constraints ( tcx, input, Certainty :: Yes ) == result
421
- } else if stack_entry . has_been_used == HasBeenUsed :: INDUCTIVE_CYCLE {
422
- Self :: response_no_constraints ( tcx, input, Certainty :: overflow ( false ) )
501
+ } else if entry . has_been_used == HasBeenUsed :: COINDUCTIVE_CYCLE {
502
+ Self :: response_no_constraints ( tcx, entry . input , Certainty :: Yes ) == result
503
+ } else if entry . has_been_used == HasBeenUsed :: INDUCTIVE_CYCLE {
504
+ Self :: response_no_constraints ( tcx, entry . input , Certainty :: overflow ( false ) )
423
505
== result
424
506
} else {
425
507
false
426
508
} ;
427
509
428
510
// If we did not reach a fixpoint, update the provisional result and reevaluate.
429
511
if reached_fixpoint {
430
- return ( stack_entry, result) ;
512
+ let cycle_data = self . cycle_data . as_mut ( ) . unwrap ( ) ;
513
+ cycle_data. add_provisional_result ( & self . stack , & entry, result) ;
514
+ return ( entry, result) ;
431
515
} else {
432
516
let depth = self . stack . push ( StackEntry {
433
517
has_been_used : HasBeenUsed :: empty ( ) ,
434
518
provisional_result : Some ( result) ,
435
- ..stack_entry
519
+ ..entry
436
520
} ) ;
437
521
debug_assert_eq ! ( self . provisional_cache[ & input] . stack_depth, Some ( depth) ) ;
438
522
}
@@ -463,7 +547,6 @@ impl<'tcx> SearchGraph<'tcx> {
463
547
} else {
464
548
self . provisional_cache . remove ( & input) ;
465
549
let reached_depth = final_entry. reached_depth . as_usize ( ) - self . stack . len ( ) ;
466
- let cycle_participants = mem:: take ( & mut self . cycle_participants ) ;
467
550
// When encountering a cycle, both inductive and coinductive, we only
468
551
// move the root into the global cache. We also store all other cycle
469
552
// participants involved.
@@ -472,6 +555,14 @@ impl<'tcx> SearchGraph<'tcx> {
472
555
// participant is on the stack. This is necessary to prevent unstable
473
556
// results. See the comment of `SearchGraph::cycle_participants` for
474
557
// more details.
558
+ let cycle_participants = if let Some ( cycle_data) =
559
+ self . cycle_data . take_if ( |data| data. root == self . stack . next_index ( ) )
560
+ {
561
+ cycle_data. cycle_participants
562
+ } else {
563
+ Default :: default ( )
564
+ } ;
565
+
475
566
self . global_cache ( tcx) . insert (
476
567
tcx,
477
568
input,
0 commit comments