@@ -44,6 +44,19 @@ pub trait Cx: Copy {
44
44
45
45
pub trait Delegate {
46
46
type Cx : Cx ;
47
+ type ValidationScope ;
48
+ /// Returning `Some` disables the global cache for the current goal.
49
+ ///
50
+ /// The `ValidationScope` is used when fuzzing the search graph to track
51
+ /// for which goals the global cache has been disabled. This is necessary
52
+ /// as we may otherwise ignore the global cache entry for some goal `G`
53
+ /// only to later use it, failing to detect a cycle goal and potentially
54
+ /// changing the result.
55
+ fn enter_validation_scope (
56
+ cx : Self :: Cx ,
57
+ input : <Self :: Cx as Cx >:: Input ,
58
+ ) -> Option < Self :: ValidationScope > ;
59
+
47
60
const FIXPOINT_STEP_LIMIT : usize ;
48
61
49
62
type ProofTreeBuilder ;
@@ -356,11 +369,21 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
356
369
return D :: on_stack_overflow ( cx, inspect, input) ;
357
370
} ;
358
371
359
- if D :: inspect_is_noop ( inspect) {
360
- if let Some ( result) = self . lookup_global_cache ( cx, input, available_depth) {
361
- return result;
362
- }
363
- }
372
+ let validate_cache = if !D :: inspect_is_noop ( inspect) {
373
+ None
374
+ } else if let Some ( scope) = D :: enter_validation_scope ( cx, input) {
375
+ // When validating the global cache we need to track the goals for which the
376
+ // global cache has been disabled as it may otherwise change the result for
377
+ // cyclic goals. We don't care about goals which are not on the current stack
378
+ // so it's fine to drop their scope eagerly.
379
+ self . lookup_global_cache_untracked ( cx, input, available_depth)
380
+ . inspect ( |expected| debug ! ( ?expected, "validate cache entry" ) )
381
+ . map ( |r| ( scope, r) )
382
+ } else if let Some ( result) = self . lookup_global_cache ( cx, input, available_depth) {
383
+ return result;
384
+ } else {
385
+ None
386
+ } ;
364
387
365
388
// Check whether the goal is in the provisional cache.
366
389
// The provisional result may rely on the path to its cycle roots,
@@ -452,6 +475,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
452
475
// do not remove it from the provisional cache and update its provisional result.
453
476
// We only add the root of cycles to the global cache.
454
477
if let Some ( head) = final_entry. non_root_cycle_participant {
478
+ debug_assert ! ( validate_cache. is_none( ) ) ;
455
479
let coinductive_stack = Self :: stack_coinductive_from ( cx, & self . stack , head) ;
456
480
457
481
let entry = self . provisional_cache . get_mut ( & input) . unwrap ( ) ;
@@ -463,16 +487,29 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
463
487
}
464
488
} else {
465
489
self . provisional_cache . remove ( & input) ;
466
- if D :: inspect_is_noop ( inspect) {
490
+ if let Some ( ( _scope, expected) ) = validate_cache {
491
+ // Do not try to move a goal into the cache again if we're testing
492
+ // the global cache.
493
+ assert_eq ! ( result, expected, "input={input:?}" ) ;
494
+ } else if D :: inspect_is_noop ( inspect) {
467
495
self . insert_global_cache ( cx, input, final_entry, result, dep_node)
468
496
}
469
497
}
470
498
471
- self . check_invariants ( ) ;
472
-
473
499
result
474
500
}
475
501
502
+ fn lookup_global_cache_untracked (
503
+ & self ,
504
+ cx : X ,
505
+ input : X :: Input ,
506
+ available_depth : AvailableDepth ,
507
+ ) -> Option < X :: Result > {
508
+ cx. with_global_cache ( self . mode , |cache| {
509
+ cache. get ( cx, input, & self . stack , available_depth) . map ( |c| c. result )
510
+ } )
511
+ }
512
+
476
513
/// Try to fetch a previously computed result from the global cache,
477
514
/// making sure to only do so if it would match the result of reevaluating
478
515
/// this goal.
@@ -496,7 +533,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
496
533
let reached_depth = self . stack . next_index ( ) . plus ( additional_depth) ;
497
534
self . update_parent_goal ( reached_depth, encountered_overflow) ;
498
535
499
- debug ! ( "global cache hit" ) ;
536
+ debug ! ( ?additional_depth , "global cache hit" ) ;
500
537
Some ( result)
501
538
} )
502
539
}
@@ -518,6 +555,7 @@ impl<D: Delegate<Cx = X>, X: Cx> SearchGraph<D> {
518
555
dep_node : X :: DepNodeIndex ,
519
556
) {
520
557
let additional_depth = final_entry. reached_depth . as_usize ( ) - self . stack . len ( ) ;
558
+ debug ! ( ?final_entry, ?result, "insert global cache" ) ;
521
559
cx. with_global_cache ( self . mode , |cache| {
522
560
cache. insert (
523
561
cx,
0 commit comments