@@ -2497,14 +2497,56 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
24972497 )
24982498 }
24992499
2500+ private module DistancePruning {
2501+ private predicate isAnySource ( PathNodeImpl n ) { n .isArbitrarySource ( ) }
2502+
2503+ private predicate isAnySink ( PathNodeImpl n ) { n .isArbitrarySink ( ) }
2504+
2505+ private predicate directStep ( PathNodeImpl n1 , PathNodeImpl n2 ) {
2506+ n1 .getANonHiddenSuccessor ( _) = n2 and directReach ( n2 )
2507+ }
2508+
2509+ private predicate directStepRev ( PathNodeImpl n1 , PathNodeImpl n2 ) {
2510+ directStep ( n2 , n1 )
2511+ }
2512+
2513+ private int srcDist1 ( PathNodeImpl n ) =
2514+ shortestDistances( isAnySource / 1 , directStep / 2 ) ( _, n , result )
2515+
2516+ private int sinkDist1 ( PathNodeImpl n ) =
2517+ shortestDistances( isAnySink / 1 , directStepRev / 2 ) ( _, n , result )
2518+
2519+ private int srcDist ( PathNodeImpl n ) { result = srcDist1 ( n ) - 1 }
2520+
2521+ private int sinkDist ( PathNodeImpl n ) { result = sinkDist1 ( n ) - 1 }
2522+
2523+ private int pathLength ( ) {
2524+ exists ( int fwdLen , int revLen |
2525+ result = fwdLen .maximum ( revLen ) and
2526+ fwdLen = max ( PathNodeImpl n | n .isSink ( ) | srcDist ( n ) ) and
2527+ revLen = max ( PathNodeImpl n | n .isSource ( ) | sinkDist ( n ) )
2528+ )
2529+ }
2530+
2531+ private int slack ( ) { result = 0 }
2532+
2533+ predicate nearShortestDirectReach ( PathNodeImpl n ) {
2534+ directReach ( n ) and
2535+ srcDist ( n ) + sinkDist ( n ) <= pathLength ( ) + slack ( )
2536+ }
2537+ }
2538+
2539+ // private predicate directReach_2 = directReach/1;
2540+ private predicate directReach_2 = DistancePruning:: nearShortestDirectReach / 1 ;
2541+
25002542 /**
25012543 * Holds if `n` can reach a return node in a summarized subpath that can reach a sink.
25022544 */
25032545 private predicate retReach ( PathNodeImpl n ) {
25042546 fwdReach ( n ) and
25052547 (
25062548 exists ( PathNodeImpl out | subpaths2 ( _, _, n , out ) |
2507- directReach ( out ) or retReach ( out )
2549+ directReach_2 ( out ) or retReach ( out )
25082550 )
25092551 or
25102552 exists ( PathNodeImpl mid |
@@ -2516,7 +2558,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
25162558 }
25172559
25182560 /** Holds if `n` can reach a sink or is used in a subpath that can reach a sink. */
2519- private predicate reach ( PathNodeImpl n ) { directReach ( n ) or retReach ( n ) }
2561+ private predicate reach ( PathNodeImpl n ) { directReach_2 ( n ) or retReach ( n ) }
25202562
25212563 /**
25222564 * A `Node` augmented with a call context (except for sinks) and an access path.
@@ -2568,7 +2610,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
25682610
25692611 /** Holds if `n1.getASuccessor() = n2` and `n2` can reach a sink. */
25702612 private predicate pathSucc ( PathNodeImpl n1 , PathNodeImpl n2 ) {
2571- n1 .getANonHiddenSuccessor ( _) = n2 and directReach ( n2 )
2613+ n1 .getANonHiddenSuccessor ( _) = n2 and directReach_2 ( n2 )
25722614 }
25732615
25742616 private predicate tcSrc ( PathNodeImpl n ) { n .isSource ( ) }
0 commit comments