@@ -11,7 +11,6 @@ use rustc_middle::traits::solve::{CanonicalInput, Certainty, EvaluationCache, Qu
11
11
use rustc_middle:: ty;
12
12
use rustc_middle:: ty:: TyCtxt ;
13
13
use rustc_session:: Limit ;
14
- use std:: collections:: hash_map:: Entry ;
15
14
use std:: mem;
16
15
17
16
rustc_index:: newtype_index! {
@@ -30,7 +29,7 @@ struct StackEntry<'tcx> {
30
29
///
31
30
/// If so, it must not be moved to the global cache. See
32
31
/// [SearchGraph::cycle_participants] for more details.
33
- non_root_cycle_participant : bool ,
32
+ non_root_cycle_participant : Option < StackDepth > ,
34
33
35
34
encountered_overflow : bool ,
36
35
has_been_used : bool ,
@@ -39,14 +38,34 @@ struct StackEntry<'tcx> {
39
38
provisional_result : Option < QueryResult < ' tcx > > ,
40
39
}
41
40
41
+ struct DetachedEntry < ' tcx > {
42
+ highest_cycle_head : StackDepth ,
43
+ result : QueryResult < ' tcx > ,
44
+ }
45
+
46
+ #[ derive( Default ) ]
47
+ struct ProvisionalCacheEntry < ' tcx > {
48
+ stack_depth : Option < StackDepth > ,
49
+ true_to_highest : Option < DetachedEntry < ' tcx > > ,
50
+ false_to_highest : Option < DetachedEntry < ' tcx > > ,
51
+ }
52
+
53
+ impl < ' tcx > ProvisionalCacheEntry < ' tcx > {
54
+ fn is_empty ( & self ) -> bool {
55
+ self . stack_depth . is_none ( )
56
+ && self . true_to_highest . is_none ( )
57
+ && self . false_to_highest . is_none ( )
58
+ }
59
+ }
60
+
42
61
pub ( super ) struct SearchGraph < ' tcx > {
43
62
mode : SolverMode ,
44
63
local_overflow_limit : usize ,
45
64
/// The stack of goals currently being computed.
46
65
///
47
66
/// An element is *deeper* in the stack if its index is *lower*.
48
67
stack : IndexVec < StackDepth , StackEntry < ' tcx > > ,
49
- stack_entries : FxHashMap < CanonicalInput < ' tcx > , StackDepth > ,
68
+ provisional_cache : FxHashMap < CanonicalInput < ' tcx > , ProvisionalCacheEntry < ' tcx > > ,
50
69
/// We put only the root goal of a coinductive cycle into the global cache.
51
70
///
52
71
/// If we were to use that result when later trying to prove another cycle
@@ -63,7 +82,7 @@ impl<'tcx> SearchGraph<'tcx> {
63
82
mode,
64
83
local_overflow_limit : tcx. recursion_limit ( ) . 0 . checked_ilog2 ( ) . unwrap_or ( 0 ) as usize ,
65
84
stack : Default :: default ( ) ,
66
- stack_entries : Default :: default ( ) ,
85
+ provisional_cache : Default :: default ( ) ,
67
86
cycle_participants : Default :: default ( ) ,
68
87
}
69
88
}
@@ -93,7 +112,7 @@ impl<'tcx> SearchGraph<'tcx> {
93
112
/// would cause us to not track overflow and recursion depth correctly.
94
113
fn pop_stack ( & mut self ) -> StackEntry < ' tcx > {
95
114
let elem = self . stack . pop ( ) . unwrap ( ) ;
96
- assert ! ( self . stack_entries . remove ( & elem. input) . is_some ( ) ) ;
115
+ self . provisional_cache . get_mut ( & elem. input ) . unwrap ( ) . stack_depth = None ;
97
116
if let Some ( last) = self . stack . raw . last_mut ( ) {
98
117
last. reached_depth = last. reached_depth . max ( elem. reached_depth ) ;
99
118
last. encountered_overflow |= elem. encountered_overflow ;
@@ -114,7 +133,7 @@ impl<'tcx> SearchGraph<'tcx> {
114
133
115
134
pub ( super ) fn is_empty ( & self ) -> bool {
116
135
if self . stack . is_empty ( ) {
117
- debug_assert ! ( self . stack_entries . is_empty( ) ) ;
136
+ debug_assert ! ( self . provisional_cache . is_empty( ) ) ;
118
137
debug_assert ! ( self . cycle_participants. is_empty( ) ) ;
119
138
true
120
139
} else {
@@ -210,23 +229,41 @@ impl<'tcx> SearchGraph<'tcx> {
210
229
return result;
211
230
}
212
231
213
- // Check whether we're in a cycle.
214
- match self . stack_entries . entry ( input) {
215
- // No entry, we push this goal on the stack and try to prove it.
216
- Entry :: Vacant ( v) => {
217
- let depth = self . stack . next_index ( ) ;
218
- let entry = StackEntry {
219
- input,
220
- available_depth,
221
- reached_depth : depth,
222
- non_root_cycle_participant : false ,
223
- encountered_overflow : false ,
224
- has_been_used : false ,
225
- provisional_result : None ,
226
- } ;
227
- assert_eq ! ( self . stack. push( entry) , depth) ;
228
- v. insert ( depth) ;
232
+ // Check whether the goal is in the provisional cache.
233
+ let cache_entry = self . provisional_cache . entry ( input) . or_default ( ) ;
234
+ if let Some ( true_cycle) = & mut cache_entry. true_to_highest
235
+ && self . stack . raw [ true_cycle. highest_cycle_head . index ( ) ..]
236
+ . iter ( )
237
+ . any ( |entry| !entry. input . value . goal . predicate . is_coinductive ( tcx) )
238
+ {
239
+ // We have a nested goal which is already in the provisional cache, use
240
+ // its result.
241
+ let participants =
242
+ self . stack . raw . iter_mut ( ) . skip ( true_cycle. highest_cycle_head . index ( ) + 1 ) ;
243
+ for entry in participants {
244
+ entry. non_root_cycle_participant =
245
+ entry. non_root_cycle_participant . max ( Some ( true_cycle. highest_cycle_head ) ) ;
246
+ self . cycle_participants . insert ( entry. input ) ;
229
247
}
248
+ inspect. goal_evaluation_kind ( inspect:: WipCanonicalGoalEvaluationKind :: CycleInStack ) ;
249
+ return true_cycle. result ;
250
+ } else if let Some ( false_cycle) = & mut cache_entry. false_to_highest
251
+ && !self . stack . raw [ false_cycle. highest_cycle_head . index ( ) ..]
252
+ . iter ( )
253
+ . any ( |entry| !entry. input . value . goal . predicate . is_coinductive ( tcx) )
254
+ {
255
+ // We have a nested goal which is already in the provisional cache, use
256
+ // its result.
257
+ let participants =
258
+ self . stack . raw . iter_mut ( ) . skip ( false_cycle. highest_cycle_head . index ( ) + 1 ) ;
259
+ for entry in participants {
260
+ entry. non_root_cycle_participant =
261
+ entry. non_root_cycle_participant . max ( Some ( false_cycle. highest_cycle_head ) ) ;
262
+ self . cycle_participants . insert ( entry. input ) ;
263
+ }
264
+ inspect. goal_evaluation_kind ( inspect:: WipCanonicalGoalEvaluationKind :: CycleInStack ) ;
265
+ return false_cycle. result ;
266
+ } else if let Some ( stack_depth) = cache_entry. stack_depth {
230
267
// We have a nested goal which relies on a goal `root` deeper in the stack.
231
268
//
232
269
// We first store that we may have to reprove `root` in case the provisional
@@ -236,40 +273,51 @@ impl<'tcx> SearchGraph<'tcx> {
236
273
//
237
274
// Finally we can return either the provisional response for that goal if we have a
238
275
// coinductive cycle or an ambiguous result if the cycle is inductive.
239
- Entry :: Occupied ( entry) => {
240
- inspect. goal_evaluation_kind ( inspect:: WipCanonicalGoalEvaluationKind :: CycleInStack ) ;
241
-
242
- let stack_depth = * entry. get ( ) ;
243
- debug ! ( "encountered cycle with depth {stack_depth:?}" ) ;
244
- // We start by tagging all non-root cycle participants.
245
- let participants = self . stack . raw . iter_mut ( ) . skip ( stack_depth. as_usize ( ) + 1 ) ;
246
- for entry in participants {
247
- entry. non_root_cycle_participant = true ;
248
- self . cycle_participants . insert ( entry. input ) ;
249
- }
276
+ inspect. goal_evaluation_kind ( inspect:: WipCanonicalGoalEvaluationKind :: CycleInStack ) ;
277
+ debug ! ( "encountered cycle with depth {stack_depth:?}" ) ;
278
+ // We start by tagging all non-root cycle participants.
279
+ let participants = self . stack . raw . iter_mut ( ) . skip ( stack_depth. as_usize ( ) + 1 ) ;
280
+ for entry in participants {
281
+ entry. non_root_cycle_participant =
282
+ entry. non_root_cycle_participant . max ( Some ( stack_depth) ) ;
283
+ self . cycle_participants . insert ( entry. input ) ;
284
+ }
250
285
251
- // If we're in a cycle, we have to retry proving the cycle head
252
- // until we reach a fixpoint. It is not enough to simply retry the
253
- // `root` goal of this cycle.
254
- //
255
- // See tests/ui/traits/next-solver/cycles/fixpoint-rerun-all-cycle-heads.rs
256
- // for an example.
257
- self . stack [ stack_depth] . has_been_used = true ;
258
- return if let Some ( result) = self . stack [ stack_depth] . provisional_result {
259
- result
286
+ // If we're in a cycle, we have to retry proving the cycle head
287
+ // until we reach a fixpoint. It is not enough to simply retry the
288
+ // `root` goal of this cycle.
289
+ //
290
+ // See tests/ui/traits/next-solver/cycles/fixpoint-rerun-all-cycle-heads.rs
291
+ // for an example.
292
+ self . stack [ stack_depth] . has_been_used = true ;
293
+ return if let Some ( result) = self . stack [ stack_depth] . provisional_result {
294
+ result
295
+ } else {
296
+ // If we don't have a provisional result yet we're in the first iteration,
297
+ // so we start with no constraints.
298
+ let is_inductive = self . stack . raw [ stack_depth. index ( ) ..]
299
+ . iter ( )
300
+ . any ( |entry| !entry. input . value . goal . predicate . is_coinductive ( tcx) ) ;
301
+ if is_inductive {
302
+ Self :: response_no_constraints ( tcx, input, Certainty :: OVERFLOW )
260
303
} else {
261
- // If we don't have a provisional result yet we're in the first iteration,
262
- // so we start with no constraints.
263
- let is_inductive = self . stack . raw [ stack_depth. index ( ) ..]
264
- . iter ( )
265
- . any ( |entry| !entry. input . value . goal . predicate . is_coinductive ( tcx) ) ;
266
- if is_inductive {
267
- Self :: response_no_constraints ( tcx, input, Certainty :: OVERFLOW )
268
- } else {
269
- Self :: response_no_constraints ( tcx, input, Certainty :: Yes )
270
- }
271
- } ;
272
- }
304
+ Self :: response_no_constraints ( tcx, input, Certainty :: Yes )
305
+ }
306
+ } ;
307
+ } else {
308
+ // No entry, we push this goal on the stack and try to prove it.
309
+ let depth = self . stack . next_index ( ) ;
310
+ let entry = StackEntry {
311
+ input,
312
+ available_depth,
313
+ reached_depth : depth,
314
+ non_root_cycle_participant : None ,
315
+ encountered_overflow : false ,
316
+ has_been_used : false ,
317
+ provisional_result : None ,
318
+ } ;
319
+ assert_eq ! ( self . stack. push( entry) , depth) ;
320
+ cache_entry. stack_depth = Some ( depth) ;
273
321
}
274
322
275
323
// This is for global caching, so we properly track query dependencies.
@@ -290,6 +338,20 @@ impl<'tcx> SearchGraph<'tcx> {
290
338
// final result.
291
339
let stack_entry = self . pop_stack ( ) ;
292
340
debug_assert_eq ! ( stack_entry. input, input) ;
341
+
342
+ if stack_entry. has_been_used {
343
+ #[ allow( rustc:: potential_query_instability) ]
344
+ self . provisional_cache . retain ( |_, entry| {
345
+ entry
346
+ . true_to_highest
347
+ . take_if ( |p| p. highest_cycle_head == self . stack . next_index ( ) ) ;
348
+ entry
349
+ . false_to_highest
350
+ . take_if ( |p| p. highest_cycle_head == self . stack . next_index ( ) ) ;
351
+ !entry. is_empty ( )
352
+ } ) ;
353
+ }
354
+
293
355
if stack_entry. has_been_used
294
356
&& stack_entry. provisional_result . map_or ( true , |r| r != result)
295
357
{
@@ -299,7 +361,14 @@ impl<'tcx> SearchGraph<'tcx> {
299
361
provisional_result : Some ( result) ,
300
362
..stack_entry
301
363
} ) ;
302
- assert_eq ! ( self . stack_entries. insert( input, depth) , None ) ;
364
+ assert_eq ! (
365
+ self . provisional_cache
366
+ . entry( input)
367
+ . or_default( )
368
+ . stack_depth
369
+ . replace( depth) ,
370
+ None
371
+ ) ;
303
372
} else {
304
373
return ( stack_entry, result) ;
305
374
}
@@ -319,7 +388,18 @@ impl<'tcx> SearchGraph<'tcx> {
319
388
//
320
389
// It is not possible for any nested goal to depend on something deeper on the
321
390
// stack, as this would have also updated the depth of the current goal.
322
- if !final_entry. non_root_cycle_participant {
391
+ if let Some ( highest_cycle_head) = final_entry. non_root_cycle_participant {
392
+ let is_true = self . stack . raw [ highest_cycle_head. index ( ) ..]
393
+ . iter ( )
394
+ . any ( |entry| !entry. input . value . goal . predicate . is_coinductive ( tcx) ) ;
395
+
396
+ let entry = self . provisional_cache . entry ( input) . or_default ( ) ;
397
+ if is_true {
398
+ entry. true_to_highest = Some ( DetachedEntry { highest_cycle_head, result } )
399
+ } else {
400
+ entry. false_to_highest = Some ( DetachedEntry { highest_cycle_head, result } )
401
+ }
402
+ } else {
323
403
// When encountering a cycle, both inductive and coinductive, we only
324
404
// move the root into the global cache. We also store all other cycle
325
405
// participants involved.
@@ -328,6 +408,7 @@ impl<'tcx> SearchGraph<'tcx> {
328
408
// participant is on the stack. This is necessary to prevent unstable
329
409
// results. See the comment of `SearchGraph::cycle_participants` for
330
410
// more details.
411
+ self . provisional_cache . remove ( & input) ;
331
412
let reached_depth = final_entry. reached_depth . as_usize ( ) - self . stack . len ( ) ;
332
413
let cycle_participants = mem:: take ( & mut self . cycle_participants ) ;
333
414
self . global_cache ( tcx) . insert (
0 commit comments