@@ -2337,7 +2337,7 @@ private module LocalFlowBigStep {
2337
2337
2338
2338
private import LocalFlowBigStep
2339
2339
2340
- private module Stage2Point5Param implements MkStage< Stage2 > :: StageParam {
2340
+ private module Stage3Param implements MkStage< Stage2 > :: StageParam {
2341
2341
private module PrevStage = Stage2;
2342
2342
2343
2343
class Ap = ApproxAccessPathFront ;
@@ -2409,12 +2409,12 @@ private module Stage2Point5Param implements MkStage<Stage2>::StageParam {
2409
2409
}
2410
2410
}
2411
2411
2412
- private module Stage2Point5 implements StageSig {
2413
- import MkStage< Stage2 > :: Stage< Stage2Point5Param >
2412
+ private module Stage3 implements StageSig {
2413
+ import MkStage< Stage2 > :: Stage< Stage3Param >
2414
2414
}
2415
2415
2416
- private module Stage3Param implements MkStage< Stage2Point5 > :: StageParam {
2417
- private module PrevStage = Stage2Point5 ;
2416
+ private module Stage4Param implements MkStage< Stage3 > :: StageParam {
2417
+ private module PrevStage = Stage3 ;
2418
2418
2419
2419
class Ap = AccessPathFront ;
2420
2420
@@ -2531,8 +2531,8 @@ private module Stage3Param implements MkStage<Stage2Point5>::StageParam {
2531
2531
}
2532
2532
}
2533
2533
2534
- private module Stage3 implements StageSig {
2535
- import MkStage< Stage2Point5 > :: Stage< Stage3Param >
2534
+ private module Stage4 implements StageSig {
2535
+ import MkStage< Stage3 > :: Stage< Stage4Param >
2536
2536
}
2537
2537
2538
2538
/**
@@ -2543,8 +2543,8 @@ private predicate flowCandSummaryCtx(
2543
2543
NodeEx node , FlowState state , AccessPathFront argApf , Configuration config
2544
2544
) {
2545
2545
exists ( AccessPathFront apf |
2546
- Stage3 :: revFlow ( node , state , TReturnCtxMaybeFlowThrough ( _) , _, apf , config ) and
2547
- Stage3 :: fwdFlow ( node , state , any ( Stage3 :: CcCall ccc ) , _, TAccessPathFrontSome ( argApf ) , apf ,
2546
+ Stage4 :: revFlow ( node , state , TReturnCtxMaybeFlowThrough ( _) , _, apf , config ) and
2547
+ Stage4 :: fwdFlow ( node , state , any ( Stage4 :: CcCall ccc ) , _, TAccessPathFrontSome ( argApf ) , apf ,
2548
2548
config )
2549
2549
)
2550
2550
}
@@ -2555,10 +2555,10 @@ private predicate flowCandSummaryCtx(
2555
2555
*/
2556
2556
private predicate expensiveLen2unfolding ( TypedContent tc , Configuration config ) {
2557
2557
exists ( int tails , int nodes , int apLimit , int tupleLimit |
2558
- tails = strictcount ( AccessPathFront apf | Stage3 :: consCand ( tc , apf , config ) ) and
2558
+ tails = strictcount ( AccessPathFront apf | Stage4 :: consCand ( tc , apf , config ) ) and
2559
2559
nodes =
2560
2560
strictcount ( NodeEx n , FlowState state |
2561
- Stage3 :: revFlow ( n , state , any ( AccessPathFrontHead apf | apf .getHead ( ) = tc ) , config )
2561
+ Stage4 :: revFlow ( n , state , any ( AccessPathFrontHead apf | apf .getHead ( ) = tc ) , config )
2562
2562
or
2563
2563
flowCandSummaryCtx ( n , state , any ( AccessPathFrontHead apf | apf .getHead ( ) = tc ) , config )
2564
2564
) and
@@ -2572,11 +2572,11 @@ private predicate expensiveLen2unfolding(TypedContent tc, Configuration config)
2572
2572
private newtype TAccessPathApprox =
2573
2573
TNil ( DataFlowType t ) or
2574
2574
TConsNil ( TypedContent tc , DataFlowType t ) {
2575
- Stage3 :: consCand ( tc , TFrontNil ( t ) , _) and
2575
+ Stage4 :: consCand ( tc , TFrontNil ( t ) , _) and
2576
2576
not expensiveLen2unfolding ( tc , _)
2577
2577
} or
2578
2578
TConsCons ( TypedContent tc1 , TypedContent tc2 , int len ) {
2579
- Stage3 :: consCand ( tc1 , TFrontHead ( tc2 ) , _) and
2579
+ Stage4 :: consCand ( tc1 , TFrontHead ( tc2 ) , _) and
2580
2580
len in [ 2 .. accessPathLimit ( ) ] and
2581
2581
not expensiveLen2unfolding ( tc1 , _)
2582
2582
} or
@@ -2706,7 +2706,7 @@ private class AccessPathApproxCons1 extends AccessPathApproxCons, TCons1 {
2706
2706
override AccessPathApprox pop ( TypedContent head ) {
2707
2707
head = tc and
2708
2708
(
2709
- exists ( TypedContent tc2 | Stage3 :: consCand ( tc , TFrontHead ( tc2 ) , _) |
2709
+ exists ( TypedContent tc2 | Stage4 :: consCand ( tc , TFrontHead ( tc2 ) , _) |
2710
2710
result = TConsCons ( tc2 , _, len - 1 )
2711
2711
or
2712
2712
len = 2 and
@@ -2717,7 +2717,7 @@ private class AccessPathApproxCons1 extends AccessPathApproxCons, TCons1 {
2717
2717
or
2718
2718
exists ( DataFlowType t |
2719
2719
len = 1 and
2720
- Stage3 :: consCand ( tc , TFrontNil ( t ) , _) and
2720
+ Stage4 :: consCand ( tc , TFrontNil ( t ) , _) and
2721
2721
result = TNil ( t )
2722
2722
)
2723
2723
)
@@ -2742,8 +2742,8 @@ private class AccessPathApproxOption extends TAccessPathApproxOption {
2742
2742
}
2743
2743
}
2744
2744
2745
- private module Stage4Param implements MkStage< Stage3 > :: StageParam {
2746
- private module PrevStage = Stage3 ;
2745
+ private module Stage5Param implements MkStage< Stage4 > :: StageParam {
2746
+ private module PrevStage = Stage4 ;
2747
2747
2748
2748
class Ap = AccessPathApprox ;
2749
2749
@@ -2814,7 +2814,7 @@ private module Stage4Param implements MkStage<Stage3>::StageParam {
2814
2814
predicate typecheckStore ( Ap ap , DataFlowType contentType ) { any ( ) }
2815
2815
}
2816
2816
2817
- private module Stage4 = MkStage< Stage3 > :: Stage< Stage4Param > ;
2817
+ private module Stage5 = MkStage< Stage4 > :: Stage< Stage5Param > ;
2818
2818
2819
2819
bindingset [ conf, result ]
2820
2820
private Configuration unbindConf ( Configuration conf ) {
@@ -2828,8 +2828,8 @@ private predicate nodeMayUseSummary0(
2828
2828
) {
2829
2829
exists ( AccessPathApprox apa0 |
2830
2830
c = n .getEnclosingCallable ( ) and
2831
- Stage4 :: revFlow ( n , state , TReturnCtxMaybeFlowThrough ( _) , _, apa0 , config ) and
2832
- Stage4 :: fwdFlow ( n , state , any ( CallContextCall ccc ) , TParameterPositionSome ( pos ) ,
2831
+ Stage5 :: revFlow ( n , state , TReturnCtxMaybeFlowThrough ( _) , _, apa0 , config ) and
2832
+ Stage5 :: fwdFlow ( n , state , any ( CallContextCall ccc ) , TParameterPositionSome ( pos ) ,
2833
2833
TAccessPathApproxSome ( apa ) , apa0 , config )
2834
2834
)
2835
2835
}
@@ -2839,7 +2839,7 @@ private predicate nodeMayUseSummary(
2839
2839
NodeEx n , FlowState state , AccessPathApprox apa , Configuration config
2840
2840
) {
2841
2841
exists ( DataFlowCallable c , ParameterPosition pos , ParamNodeEx p |
2842
- Stage4 :: parameterMayFlowThrough ( p , apa , config ) and
2842
+ Stage5 :: parameterMayFlowThrough ( p , apa , config ) and
2843
2843
nodeMayUseSummary0 ( n , c , pos , state , apa , config ) and
2844
2844
p .isParameterOf ( c , pos )
2845
2845
)
@@ -2849,8 +2849,8 @@ private newtype TSummaryCtx =
2849
2849
TSummaryCtxNone ( ) or
2850
2850
TSummaryCtxSome ( ParamNodeEx p , FlowState state , AccessPath ap ) {
2851
2851
exists ( Configuration config |
2852
- Stage4 :: parameterMayFlowThrough ( p , ap .getApprox ( ) , config ) and
2853
- Stage4 :: revFlow ( p , state , _, config )
2852
+ Stage5 :: parameterMayFlowThrough ( p , ap .getApprox ( ) , config ) and
2853
+ Stage5 :: revFlow ( p , state , _, config )
2854
2854
)
2855
2855
}
2856
2856
@@ -2899,7 +2899,7 @@ private int count1to2unfold(AccessPathApproxCons1 apa, Configuration config) {
2899
2899
len = apa .len ( ) and
2900
2900
result =
2901
2901
strictcount ( AccessPathFront apf |
2902
- Stage4 :: consCand ( tc , any ( AccessPathApprox ap | ap .getFront ( ) = apf and ap .len ( ) = len - 1 ) ,
2902
+ Stage5 :: consCand ( tc , any ( AccessPathApprox ap | ap .getFront ( ) = apf and ap .len ( ) = len - 1 ) ,
2903
2903
config )
2904
2904
)
2905
2905
)
@@ -2908,7 +2908,7 @@ private int count1to2unfold(AccessPathApproxCons1 apa, Configuration config) {
2908
2908
private int countNodesUsingAccessPath ( AccessPathApprox apa , Configuration config ) {
2909
2909
result =
2910
2910
strictcount ( NodeEx n , FlowState state |
2911
- Stage4 :: revFlow ( n , state , apa , config ) or nodeMayUseSummary ( n , state , apa , config )
2911
+ Stage5 :: revFlow ( n , state , apa , config ) or nodeMayUseSummary ( n , state , apa , config )
2912
2912
)
2913
2913
}
2914
2914
@@ -2929,7 +2929,7 @@ private predicate expensiveLen1to2unfolding(AccessPathApproxCons1 apa, Configura
2929
2929
private AccessPathApprox getATail ( AccessPathApprox apa , Configuration config ) {
2930
2930
exists ( TypedContent head |
2931
2931
apa .pop ( head ) = result and
2932
- Stage4 :: consCand ( head , result , config )
2932
+ Stage5 :: consCand ( head , result , config )
2933
2933
)
2934
2934
}
2935
2935
@@ -3011,7 +3011,7 @@ private newtype TPathNode =
3011
3011
NodeEx node , FlowState state , CallContext cc , SummaryCtx sc , AccessPath ap , Configuration config
3012
3012
) {
3013
3013
// A PathNode is introduced by a source ...
3014
- Stage4 :: revFlow ( node , state , config ) and
3014
+ Stage5 :: revFlow ( node , state , config ) and
3015
3015
sourceNode ( node , state , config ) and
3016
3016
(
3017
3017
if hasSourceCallCtx ( config )
@@ -3025,7 +3025,7 @@ private newtype TPathNode =
3025
3025
exists ( PathNodeMid mid |
3026
3026
pathStep ( mid , node , state , cc , sc , ap ) and
3027
3027
pragma [ only_bind_into ] ( config ) = mid .getConfiguration ( ) and
3028
- Stage4 :: revFlow ( node , state , ap .getApprox ( ) , pragma [ only_bind_into ] ( config ) )
3028
+ Stage5 :: revFlow ( node , state , ap .getApprox ( ) , pragma [ only_bind_into ] ( config ) )
3029
3029
)
3030
3030
} or
3031
3031
TPathNodeSink ( NodeEx node , FlowState state , Configuration config ) {
@@ -3167,7 +3167,7 @@ private class AccessPathCons2 extends AccessPath, TAccessPathCons2 {
3167
3167
override TypedContent getHead ( ) { result = head1 }
3168
3168
3169
3169
override AccessPath getTail ( ) {
3170
- Stage4 :: consCand ( head1 , result .getApprox ( ) , _) and
3170
+ Stage5 :: consCand ( head1 , result .getApprox ( ) , _) and
3171
3171
result .getHead ( ) = head2 and
3172
3172
result .length ( ) = len - 1
3173
3173
}
@@ -3198,7 +3198,7 @@ private class AccessPathCons1 extends AccessPath, TAccessPathCons1 {
3198
3198
override TypedContent getHead ( ) { result = head }
3199
3199
3200
3200
override AccessPath getTail ( ) {
3201
- Stage4 :: consCand ( head , result .getApprox ( ) , _) and result .length ( ) = len - 1
3201
+ Stage5 :: consCand ( head , result .getApprox ( ) , _) and result .length ( ) = len - 1
3202
3202
}
3203
3203
3204
3204
override AccessPathFrontHead getFront ( ) { result = TFrontHead ( head ) }
@@ -3633,7 +3633,7 @@ private predicate pathReadStep(
3633
3633
) {
3634
3634
ap0 = mid .getAp ( ) and
3635
3635
tc = ap0 .getHead ( ) and
3636
- Stage4 :: readStepCand ( mid .getNodeEx ( ) , tc .getContent ( ) , node , mid .getConfiguration ( ) ) and
3636
+ Stage5 :: readStepCand ( mid .getNodeEx ( ) , tc .getContent ( ) , node , mid .getConfiguration ( ) ) and
3637
3637
state = mid .getState ( ) and
3638
3638
cc = mid .getCallContext ( )
3639
3639
}
@@ -3643,7 +3643,7 @@ private predicate pathStoreStep(
3643
3643
PathNodeMid mid , NodeEx node , FlowState state , AccessPath ap0 , TypedContent tc , CallContext cc
3644
3644
) {
3645
3645
ap0 = mid .getAp ( ) and
3646
- Stage4 :: storeStepCand ( mid .getNodeEx ( ) , _, tc , node , _, mid .getConfiguration ( ) ) and
3646
+ Stage5 :: storeStepCand ( mid .getNodeEx ( ) , _, tc , node , _, mid .getConfiguration ( ) ) and
3647
3647
state = mid .getState ( ) and
3648
3648
cc = mid .getCallContext ( )
3649
3649
}
@@ -3680,7 +3680,7 @@ private NodeEx getAnOutNodeFlow(
3680
3680
ReturnKindExt kind , DataFlowCall call , AccessPathApprox apa , Configuration config
3681
3681
) {
3682
3682
result .asNode ( ) = kind .getAnOutNode ( call ) and
3683
- Stage4 :: revFlow ( result , _, apa , config )
3683
+ Stage5 :: revFlow ( result , _, apa , config )
3684
3684
}
3685
3685
3686
3686
/**
@@ -3716,7 +3716,7 @@ private predicate parameterCand(
3716
3716
DataFlowCallable callable , ParameterPosition pos , AccessPathApprox apa , Configuration config
3717
3717
) {
3718
3718
exists ( ParamNodeEx p |
3719
- Stage4 :: revFlow ( p , _, apa , config ) and
3719
+ Stage5 :: revFlow ( p , _, apa , config ) and
3720
3720
p .isParameterOf ( callable , pos )
3721
3721
)
3722
3722
}
@@ -3979,14 +3979,6 @@ predicate stageStats(
3979
3979
n = 25 and
3980
3980
Stage2:: stats ( false , nodes , fields , conscand , states , tuples , config )
3981
3981
or
3982
- stage = "2.5 Fwd" and
3983
- n = 25 and
3984
- Stage2Point5:: stats ( true , nodes , fields , conscand , states , tuples , config )
3985
- or
3986
- stage = "2.5 Rev" and
3987
- n = 27 and
3988
- Stage2Point5:: stats ( false , nodes , fields , conscand , states , tuples , config )
3989
- or
3990
3982
stage = "3 Fwd" and
3991
3983
n = 30 and
3992
3984
Stage3:: stats ( true , nodes , fields , conscand , states , tuples , config )
@@ -4003,9 +3995,17 @@ predicate stageStats(
4003
3995
n = 45 and
4004
3996
Stage4:: stats ( false , nodes , fields , conscand , states , tuples , config )
4005
3997
or
4006
- stage = "5 Fwd" and n = 50 and finalStats ( true , nodes , fields , conscand , states , tuples )
3998
+ stage = "5 Fwd" and
3999
+ n = 50 and
4000
+ Stage5:: stats ( true , nodes , fields , conscand , states , tuples , config )
4001
+ or
4002
+ stage = "5 Rev" and
4003
+ n = 55 and
4004
+ Stage5:: stats ( false , nodes , fields , conscand , states , tuples , config )
4005
+ or
4006
+ stage = "6 Fwd" and n = 60 and finalStats ( true , nodes , fields , conscand , states , tuples )
4007
4007
or
4008
- stage = "5 Rev" and n = 55 and finalStats ( false , nodes , fields , conscand , states , tuples )
4008
+ stage = "6 Rev" and n = 65 and finalStats ( false , nodes , fields , conscand , states , tuples )
4009
4009
}
4010
4010
4011
4011
private module FlowExploration {
0 commit comments