@@ -94,7 +94,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
94
94
*/
95
95
int fieldFlowBranchLimit ( ) ;
96
96
97
- /** Gets the access path limit. */
97
+ /** Gets the access path limit. A maximum limit of 5 is allowed. */
98
98
int accessPathLimit ( ) ;
99
99
100
100
/**
@@ -2562,10 +2562,15 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2562
2562
/** Input from previous iteration. */
2563
2563
private signature predicate storeReachesReadSig ( NodeEx node1 , NodeEx node2 ) ;
2564
2564
2565
+ private signature int iterationSig ( ) ;
2566
+
2565
2567
private module StoreReachesRead<
2566
2568
storeReachesReadSig / 2 storeReachesReadPrevDelta,
2567
- storeReachesReadSig / 2 storeReachesReadPrevPrev>
2569
+ storeReachesReadSig / 2 storeReachesReadPrevPrev, iterationSig / 0 iteration >
2568
2570
{
2571
+ private predicate enabled ( ) { Config:: accessPathLimit ( ) > iteration ( ) }
2572
+
2573
+ // private predicate enabled() { any() }
2569
2574
pragma [ nomagic]
2570
2575
private predicate step ( NodeEx node1 , NodeEx node2 , boolean usesPrevDelta ) {
2571
2576
valueStep ( node1 , node2 ) and
@@ -2591,7 +2596,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2591
2596
}
2592
2597
2593
2598
private predicate stepNodeOrContent ( ContentOrNodeContent n1 , ContentOrNodeContent n2 ) {
2594
- step ( n1 .asNodeEx ( ) , n2 .asNodeEx ( ) , _)
2599
+ exists ( boolean usesPrevDelta | step ( n1 .asNodeEx ( ) , n2 .asNodeEx ( ) , usesPrevDelta ) |
2600
+ usesPrevDelta = false or enabled ( )
2601
+ )
2595
2602
or
2596
2603
storeStepCand0 ( _, _, n1 .asContent ( ) , n2 .asNodeEx ( ) , _, _)
2597
2604
or
@@ -2618,23 +2625,33 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2618
2625
}
2619
2626
2620
2627
private predicate isStoreTarget ( NodeAndBoolean node ) {
2628
+ enabled ( ) and
2621
2629
exists ( Content c |
2622
2630
contentIsReadAndStored ( c ) and
2623
2631
storeStepCand0 ( _, _, c , node .getNodeEx ( ) , _, _) and
2624
2632
node .getBoolean ( ) = false
2625
2633
)
2626
2634
}
2627
2635
2636
+ private boolean mustUsePrevDelta ( ) {
2637
+ exists ( int iteration |
2638
+ iteration = iteration ( ) and
2639
+ if iteration > 0 then result = true else result = false
2640
+ )
2641
+ }
2642
+
2628
2643
private predicate isReadSource ( NodeAndBoolean node ) {
2644
+ enabled ( ) and
2629
2645
exists ( Content c |
2630
2646
contentIsReadAndStored ( c ) and
2631
2647
readStepCand0 ( node .getNodeEx ( ) , c , _) and
2632
- node .getBoolean ( ) = true
2648
+ node .getBoolean ( ) = mustUsePrevDelta ( )
2633
2649
)
2634
2650
}
2635
2651
2636
2652
pragma [ nomagic]
2637
2653
private predicate step0 ( NodeAndBoolean node1 , NodeAndBoolean node2 ) {
2654
+ enabled ( ) and
2638
2655
exists ( boolean usesPrevDelta |
2639
2656
step ( node1 .getNodeEx ( ) , node2 .getNodeEx ( ) , usesPrevDelta )
2640
2657
|
@@ -2649,6 +2666,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2649
2666
private predicate storeStepCandIsReadAndStored (
2650
2667
NodeEx node1 , Content c , NodeAndBoolean node2
2651
2668
) {
2669
+ enabled ( ) and
2652
2670
contentIsReadAndStored ( c ) and
2653
2671
storeStepCand0 ( node1 , _, c , node2 .getNodeEx ( ) , _, _) and
2654
2672
node2 .getBoolean ( ) = false
@@ -2658,9 +2676,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2658
2676
private predicate readStepCandIsReadAndStored (
2659
2677
NodeAndBoolean node1 , Content c , NodeEx node2
2660
2678
) {
2679
+ enabled ( ) and
2661
2680
contentIsReadAndStored ( c ) and
2662
2681
readStepCand0 ( node1 .getNodeEx ( ) , c , node2 ) and
2663
- node1 .getBoolean ( ) = true
2682
+ node1 .getBoolean ( ) = mustUsePrevDelta ( )
2664
2683
}
2665
2684
2666
2685
pragma [ nomagic]
@@ -2680,12 +2699,14 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2680
2699
}
2681
2700
}
2682
2701
2683
- private predicate storeReachesReadPrevDelta0 ( NodeEx node1 , NodeEx node2 ) { node1 = node2 }
2702
+ private predicate storeReachesReadPrevDelta0 ( NodeEx node1 , NodeEx node2 ) { none ( ) }
2684
2703
2685
2704
private predicate storeReachesReadPrevPrev0 ( NodeEx node1 , NodeEx node2 ) { none ( ) }
2686
2705
2706
+ private int iteration0 ( ) { result = 0 }
2707
+
2687
2708
private module StoreReachesRead1 =
2688
- StoreReachesRead< storeReachesReadPrevDelta0 / 2 , storeReachesReadPrevPrev0 / 2 > ;
2709
+ StoreReachesRead< storeReachesReadPrevDelta0 / 2 , storeReachesReadPrevPrev0 / 2 , iteration0 / 0 > ;
2689
2710
2690
2711
private predicate storeReachesReadPrevDelta1 ( NodeEx storeSource , NodeEx readTarget ) {
2691
2712
StoreReachesRead1:: storeReachesReadDelta ( storeSource , readTarget )
@@ -2701,30 +2722,45 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2701
2722
none ( )
2702
2723
}
2703
2724
2725
+ private int iteration1 ( ) { result = 1 }
2726
+
2704
2727
private module StoreReachesRead2 =
2705
- StoreReachesRead< storeReachesReadPrevDelta1 / 2 , storeReachesReadPrevPrev1 / 2 > ;
2728
+ StoreReachesRead< storeReachesReadPrevDelta1 / 2 , storeReachesReadPrevPrev1 / 2 , iteration1 / 0 > ;
2706
2729
2707
2730
private predicate storeReachesReadPrevDelta2 = StoreReachesRead2:: storeReachesReadDelta / 2 ;
2708
2731
2709
2732
private predicate storeReachesReadPrevPrev2 = StoreReachesRead2:: storeReachesReadPrev / 2 ;
2710
2733
2734
+ private int iteration2 ( ) { result = 2 }
2735
+
2711
2736
private module StoreReachesRead3 =
2712
- StoreReachesRead< storeReachesReadPrevDelta2 / 2 , storeReachesReadPrevPrev2 / 2 > ;
2737
+ StoreReachesRead< storeReachesReadPrevDelta2 / 2 , storeReachesReadPrevPrev2 / 2 , iteration2 / 0 > ;
2713
2738
2714
2739
private predicate storeReachesReadPrevDelta3 = StoreReachesRead3:: storeReachesReadDelta / 2 ;
2715
2740
2716
2741
private predicate storeReachesReadPrevPrev3 = StoreReachesRead3:: storeReachesReadPrev / 2 ;
2717
2742
2743
+ private int iteration3 ( ) { result = 3 }
2744
+
2718
2745
private module StoreReachesRead4 =
2719
- StoreReachesRead< storeReachesReadPrevDelta3 / 2 , storeReachesReadPrevPrev3 / 2 > ;
2746
+ StoreReachesRead< storeReachesReadPrevDelta3 / 2 , storeReachesReadPrevPrev3 / 2 , iteration3 / 0 > ;
2747
+
2748
+ private predicate storeReachesReadPrevDelta4 = StoreReachesRead4:: storeReachesReadDelta / 2 ;
2749
+
2750
+ private predicate storeReachesReadPrevPrev4 = StoreReachesRead4:: storeReachesReadPrev / 2 ;
2751
+
2752
+ private int iteration4 ( ) { result = 4 }
2753
+
2754
+ private module StoreReachesRead5 =
2755
+ StoreReachesRead< storeReachesReadPrevDelta4 / 2 , storeReachesReadPrevPrev4 / 2 , iteration4 / 0 > ;
2720
2756
2721
2757
predicate storeReachesRead ( NodeEx storeSource , NodeEx readTarget ) {
2722
- StoreReachesRead4 :: storeReachesReadDelta ( storeSource , readTarget )
2758
+ StoreReachesRead5 :: storeReachesReadDelta ( storeSource , readTarget )
2723
2759
or
2724
- StoreReachesRead4 :: storeReachesReadPrev ( storeSource , readTarget )
2760
+ StoreReachesRead5 :: storeReachesReadPrev ( storeSource , readTarget )
2725
2761
}
2726
2762
2727
- predicate contentIsReadAndStored = StoreReachesRead4 :: contentIsReadAndStored / 1 ;
2763
+ predicate contentIsReadAndStored = StoreReachesRead5 :: contentIsReadAndStored / 1 ;
2728
2764
}
2729
2765
2730
2766
predicate storeReachesRead = StoreReadReachability:: storeReachesRead / 2 ;
0 commit comments