@@ -2337,7 +2337,7 @@ private module LocalFlowBigStep {
23372337
23382338private import LocalFlowBigStep
23392339
2340- private module Stage2Point5Param implements MkStage< Stage2 > :: StageParam {
2340+ private module Stage3Param implements MkStage< Stage2 > :: StageParam {
23412341 private module PrevStage = Stage2;
23422342
23432343 class Ap = ApproxAccessPathFront ;
@@ -2409,12 +2409,12 @@ private module Stage2Point5Param implements MkStage<Stage2>::StageParam {
24092409 }
24102410}
24112411
2412- private module Stage2Point5 implements StageSig {
2413- import MkStage< Stage2 > :: Stage< Stage2Point5Param >
2412+ private module Stage3 implements StageSig {
2413+ import MkStage< Stage2 > :: Stage< Stage3Param >
24142414}
24152415
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 ;
24182418
24192419 class Ap = AccessPathFront ;
24202420
@@ -2531,8 +2531,8 @@ private module Stage3Param implements MkStage<Stage2Point5>::StageParam {
25312531 }
25322532}
25332533
2534- private module Stage3 implements StageSig {
2535- import MkStage< Stage2Point5 > :: Stage< Stage3Param >
2534+ private module Stage4 implements StageSig {
2535+ import MkStage< Stage3 > :: Stage< Stage4Param >
25362536}
25372537
25382538/**
@@ -2543,8 +2543,8 @@ private predicate flowCandSummaryCtx(
25432543 NodeEx node , FlowState state , AccessPathFront argApf , Configuration config
25442544) {
25452545 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 ,
25482548 config )
25492549 )
25502550}
@@ -2555,10 +2555,10 @@ private predicate flowCandSummaryCtx(
25552555 */
25562556private predicate expensiveLen2unfolding ( TypedContent tc , Configuration config ) {
25572557 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
25592559 nodes =
25602560 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 )
25622562 or
25632563 flowCandSummaryCtx ( n , state , any ( AccessPathFrontHead apf | apf .getHead ( ) = tc ) , config )
25642564 ) and
@@ -2572,11 +2572,11 @@ private predicate expensiveLen2unfolding(TypedContent tc, Configuration config)
25722572private newtype TAccessPathApprox =
25732573 TNil ( DataFlowType t ) or
25742574 TConsNil ( TypedContent tc , DataFlowType t ) {
2575- Stage3 :: consCand ( tc , TFrontNil ( t ) , _) and
2575+ Stage4 :: consCand ( tc , TFrontNil ( t ) , _) and
25762576 not expensiveLen2unfolding ( tc , _)
25772577 } or
25782578 TConsCons ( TypedContent tc1 , TypedContent tc2 , int len ) {
2579- Stage3 :: consCand ( tc1 , TFrontHead ( tc2 ) , _) and
2579+ Stage4 :: consCand ( tc1 , TFrontHead ( tc2 ) , _) and
25802580 len in [ 2 .. accessPathLimit ( ) ] and
25812581 not expensiveLen2unfolding ( tc1 , _)
25822582 } or
@@ -2706,7 +2706,7 @@ private class AccessPathApproxCons1 extends AccessPathApproxCons, TCons1 {
27062706 override AccessPathApprox pop ( TypedContent head ) {
27072707 head = tc and
27082708 (
2709- exists ( TypedContent tc2 | Stage3 :: consCand ( tc , TFrontHead ( tc2 ) , _) |
2709+ exists ( TypedContent tc2 | Stage4 :: consCand ( tc , TFrontHead ( tc2 ) , _) |
27102710 result = TConsCons ( tc2 , _, len - 1 )
27112711 or
27122712 len = 2 and
@@ -2717,7 +2717,7 @@ private class AccessPathApproxCons1 extends AccessPathApproxCons, TCons1 {
27172717 or
27182718 exists ( DataFlowType t |
27192719 len = 1 and
2720- Stage3 :: consCand ( tc , TFrontNil ( t ) , _) and
2720+ Stage4 :: consCand ( tc , TFrontNil ( t ) , _) and
27212721 result = TNil ( t )
27222722 )
27232723 )
@@ -2742,8 +2742,8 @@ private class AccessPathApproxOption extends TAccessPathApproxOption {
27422742 }
27432743}
27442744
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 ;
27472747
27482748 class Ap = AccessPathApprox ;
27492749
@@ -2814,7 +2814,7 @@ private module Stage4Param implements MkStage<Stage3>::StageParam {
28142814 predicate typecheckStore ( Ap ap , DataFlowType contentType ) { any ( ) }
28152815}
28162816
2817- private module Stage4 = MkStage< Stage3 > :: Stage< Stage4Param > ;
2817+ private module Stage5 = MkStage< Stage4 > :: Stage< Stage5Param > ;
28182818
28192819bindingset [ conf, result ]
28202820private Configuration unbindConf ( Configuration conf ) {
@@ -2828,8 +2828,8 @@ private predicate nodeMayUseSummary0(
28282828) {
28292829 exists ( AccessPathApprox apa0 |
28302830 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 ) ,
28332833 TAccessPathApproxSome ( apa ) , apa0 , config )
28342834 )
28352835}
@@ -2839,7 +2839,7 @@ private predicate nodeMayUseSummary(
28392839 NodeEx n , FlowState state , AccessPathApprox apa , Configuration config
28402840) {
28412841 exists ( DataFlowCallable c , ParameterPosition pos , ParamNodeEx p |
2842- Stage4 :: parameterMayFlowThrough ( p , apa , config ) and
2842+ Stage5 :: parameterMayFlowThrough ( p , apa , config ) and
28432843 nodeMayUseSummary0 ( n , c , pos , state , apa , config ) and
28442844 p .isParameterOf ( c , pos )
28452845 )
@@ -2849,8 +2849,8 @@ private newtype TSummaryCtx =
28492849 TSummaryCtxNone ( ) or
28502850 TSummaryCtxSome ( ParamNodeEx p , FlowState state , AccessPath ap ) {
28512851 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 )
28542854 )
28552855 }
28562856
@@ -2899,7 +2899,7 @@ private int count1to2unfold(AccessPathApproxCons1 apa, Configuration config) {
28992899 len = apa .len ( ) and
29002900 result =
29012901 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 ) ,
29032903 config )
29042904 )
29052905 )
@@ -2908,7 +2908,7 @@ private int count1to2unfold(AccessPathApproxCons1 apa, Configuration config) {
29082908private int countNodesUsingAccessPath ( AccessPathApprox apa , Configuration config ) {
29092909 result =
29102910 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 )
29122912 )
29132913}
29142914
@@ -2929,7 +2929,7 @@ private predicate expensiveLen1to2unfolding(AccessPathApproxCons1 apa, Configura
29292929private AccessPathApprox getATail ( AccessPathApprox apa , Configuration config ) {
29302930 exists ( TypedContent head |
29312931 apa .pop ( head ) = result and
2932- Stage4 :: consCand ( head , result , config )
2932+ Stage5 :: consCand ( head , result , config )
29332933 )
29342934}
29352935
@@ -3011,7 +3011,7 @@ private newtype TPathNode =
30113011 NodeEx node , FlowState state , CallContext cc , SummaryCtx sc , AccessPath ap , Configuration config
30123012 ) {
30133013 // A PathNode is introduced by a source ...
3014- Stage4 :: revFlow ( node , state , config ) and
3014+ Stage5 :: revFlow ( node , state , config ) and
30153015 sourceNode ( node , state , config ) and
30163016 (
30173017 if hasSourceCallCtx ( config )
@@ -3025,7 +3025,7 @@ private newtype TPathNode =
30253025 exists ( PathNodeMid mid |
30263026 pathStep ( mid , node , state , cc , sc , ap ) and
30273027 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 ) )
30293029 )
30303030 } or
30313031 TPathNodeSink ( NodeEx node , FlowState state , Configuration config ) {
@@ -3167,7 +3167,7 @@ private class AccessPathCons2 extends AccessPath, TAccessPathCons2 {
31673167 override TypedContent getHead ( ) { result = head1 }
31683168
31693169 override AccessPath getTail ( ) {
3170- Stage4 :: consCand ( head1 , result .getApprox ( ) , _) and
3170+ Stage5 :: consCand ( head1 , result .getApprox ( ) , _) and
31713171 result .getHead ( ) = head2 and
31723172 result .length ( ) = len - 1
31733173 }
@@ -3198,7 +3198,7 @@ private class AccessPathCons1 extends AccessPath, TAccessPathCons1 {
31983198 override TypedContent getHead ( ) { result = head }
31993199
32003200 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
32023202 }
32033203
32043204 override AccessPathFrontHead getFront ( ) { result = TFrontHead ( head ) }
@@ -3633,7 +3633,7 @@ private predicate pathReadStep(
36333633) {
36343634 ap0 = mid .getAp ( ) and
36353635 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
36373637 state = mid .getState ( ) and
36383638 cc = mid .getCallContext ( )
36393639}
@@ -3643,7 +3643,7 @@ private predicate pathStoreStep(
36433643 PathNodeMid mid , NodeEx node , FlowState state , AccessPath ap0 , TypedContent tc , CallContext cc
36443644) {
36453645 ap0 = mid .getAp ( ) and
3646- Stage4 :: storeStepCand ( mid .getNodeEx ( ) , _, tc , node , _, mid .getConfiguration ( ) ) and
3646+ Stage5 :: storeStepCand ( mid .getNodeEx ( ) , _, tc , node , _, mid .getConfiguration ( ) ) and
36473647 state = mid .getState ( ) and
36483648 cc = mid .getCallContext ( )
36493649}
@@ -3680,7 +3680,7 @@ private NodeEx getAnOutNodeFlow(
36803680 ReturnKindExt kind , DataFlowCall call , AccessPathApprox apa , Configuration config
36813681) {
36823682 result .asNode ( ) = kind .getAnOutNode ( call ) and
3683- Stage4 :: revFlow ( result , _, apa , config )
3683+ Stage5 :: revFlow ( result , _, apa , config )
36843684}
36853685
36863686/**
@@ -3716,7 +3716,7 @@ private predicate parameterCand(
37163716 DataFlowCallable callable , ParameterPosition pos , AccessPathApprox apa , Configuration config
37173717) {
37183718 exists ( ParamNodeEx p |
3719- Stage4 :: revFlow ( p , _, apa , config ) and
3719+ Stage5 :: revFlow ( p , _, apa , config ) and
37203720 p .isParameterOf ( callable , pos )
37213721 )
37223722}
@@ -3979,14 +3979,6 @@ predicate stageStats(
39793979 n = 25 and
39803980 Stage2:: stats ( false , nodes , fields , conscand , states , tuples , config )
39813981 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
39903982 stage = "3 Fwd" and
39913983 n = 30 and
39923984 Stage3:: stats ( true , nodes , fields , conscand , states , tuples , config )
@@ -4003,9 +3995,17 @@ predicate stageStats(
40033995 n = 45 and
40043996 Stage4:: stats ( false , nodes , fields , conscand , states , tuples , config )
40053997 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 )
40074007 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 )
40094009}
40104010
40114011private module FlowExploration {
0 commit comments