@@ -583,6 +583,20 @@ private module Stage1 {
583583 predicate revFlow ( Node node , boolean toReturn , ApOption returnAp , Ap ap , Configuration config ) {
584584 revFlow ( node , toReturn , config ) and exists ( returnAp ) and exists ( ap )
585585 }
586+
587+ predicate stats ( boolean fwd , int nodes , int fields , int conscand , int tuples , Configuration config ) {
588+ fwd = true and
589+ nodes = count ( Node node | fwdFlow ( node , config ) ) and
590+ fields = count ( Content f0 | fwdFlowIsStored ( f0 , config ) ) and
591+ conscand = - 1 and
592+ tuples = count ( Node n , boolean b | fwdFlow ( n , b , config ) )
593+ or
594+ fwd = false and
595+ nodes = count ( Node node | revFlow ( node , _, config ) ) and
596+ fields = count ( Content f0 | revFlowIsRead ( f0 , config ) ) and
597+ conscand = - 1 and
598+ tuples = count ( Node n , boolean b | revFlow ( n , b , config ) )
599+ }
586600 /* End: Stage 1 logic. */
587601}
588602
@@ -1161,6 +1175,20 @@ private module Stage2 {
11611175 predicate consCand ( TypedContent tc , Ap ap , Configuration config ) {
11621176 storeStepCand ( _, ap , tc , _, _, config )
11631177 }
1178+
1179+ predicate stats ( boolean fwd , int nodes , int fields , int conscand , int tuples , Configuration config ) {
1180+ fwd = true and
1181+ nodes = count ( Node node | fwdFlow ( node , _, _, _, config ) ) and
1182+ fields = count ( TypedContent f0 | fwdConsCand ( f0 , _, config ) ) and
1183+ conscand = count ( TypedContent f0 , Ap ap | fwdConsCand ( f0 , ap , config ) ) and
1184+ tuples = count ( Node n , Cc cc , ApOption argAp , Ap ap | fwdFlow ( n , cc , argAp , ap , config ) )
1185+ or
1186+ fwd = false and
1187+ nodes = count ( Node node | revFlow ( node , _, _, _, config ) ) and
1188+ fields = count ( TypedContent f0 | consCand ( f0 , _, config ) ) and
1189+ conscand = count ( TypedContent f0 , Ap ap | consCand ( f0 , ap , config ) ) and
1190+ tuples = count ( Node n , boolean b , ApOption retAp , Ap ap | revFlow ( n , b , retAp , ap , config ) )
1191+ }
11641192 /* End: Stage 2 logic. */
11651193}
11661194
@@ -1711,6 +1739,20 @@ private module Stage3 {
17111739 predicate consCand ( TypedContent tc , Ap ap , Configuration config ) {
17121740 storeStepCand ( _, ap , tc , _, _, config )
17131741 }
1742+
1743+ predicate stats ( boolean fwd , int nodes , int fields , int conscand , int tuples , Configuration config ) {
1744+ fwd = true and
1745+ nodes = count ( Node node | fwdFlow ( node , _, _, _, config ) ) and
1746+ fields = count ( TypedContent f0 | fwdConsCand ( f0 , _, config ) ) and
1747+ conscand = count ( TypedContent f0 , Ap ap | fwdConsCand ( f0 , ap , config ) ) and
1748+ tuples = count ( Node n , Cc cc , ApOption argAp , Ap ap | fwdFlow ( n , cc , argAp , ap , config ) )
1749+ or
1750+ fwd = false and
1751+ nodes = count ( Node node | revFlow ( node , _, _, _, config ) ) and
1752+ fields = count ( TypedContent f0 | consCand ( f0 , _, config ) ) and
1753+ conscand = count ( TypedContent f0 , Ap ap | consCand ( f0 , ap , config ) ) and
1754+ tuples = count ( Node n , boolean b , ApOption retAp , Ap ap | revFlow ( n , b , retAp , ap , config ) )
1755+ }
17141756 /* End: Stage 3 logic. */
17151757}
17161758
@@ -2336,6 +2378,20 @@ private module Stage4 {
23362378 predicate consCand ( TypedContent tc , Ap ap , Configuration config ) {
23372379 storeStepCand ( _, ap , tc , _, _, config )
23382380 }
2381+
2382+ predicate stats ( boolean fwd , int nodes , int fields , int conscand , int tuples , Configuration config ) {
2383+ fwd = true and
2384+ nodes = count ( Node node | fwdFlow ( node , _, _, _, config ) ) and
2385+ fields = count ( TypedContent f0 | fwdConsCand ( f0 , _, config ) ) and
2386+ conscand = count ( TypedContent f0 , Ap ap | fwdConsCand ( f0 , ap , config ) ) and
2387+ tuples = count ( Node n , Cc cc , ApOption argAp , Ap ap | fwdFlow ( n , cc , argAp , ap , config ) )
2388+ or
2389+ fwd = false and
2390+ nodes = count ( Node node | revFlow ( node , _, _, _, config ) ) and
2391+ fields = count ( TypedContent f0 | consCand ( f0 , _, config ) ) and
2392+ conscand = count ( TypedContent f0 , Ap ap | consCand ( f0 , ap , config ) ) and
2393+ tuples = count ( Node n , boolean b , ApOption retAp , Ap ap | revFlow ( n , b , retAp , ap , config ) )
2394+ }
23392395 /* End: Stage 4 logic. */
23402396}
23412397
@@ -3122,6 +3178,48 @@ predicate flowsTo(Node source, Node sink, Configuration configuration) {
31223178 flowsTo ( _, _, source , sink , configuration )
31233179}
31243180
3181+ private predicate finalStats ( boolean fwd , int nodes , int fields , int conscand , int tuples ) {
3182+ fwd = true and
3183+ nodes = count ( Node n0 | exists ( PathNode pn | pn .getNode ( ) = n0 ) ) and
3184+ fields =
3185+ count ( TypedContent f0 | exists ( PathNodeMid pn | pn .getAp ( ) .getFront ( ) .headUsesContent ( f0 ) ) ) and
3186+ conscand = count ( AccessPath ap | exists ( PathNodeMid pn | pn .getAp ( ) = ap ) ) and
3187+ tuples = count ( PathNode pn )
3188+ or
3189+ fwd = false and
3190+ nodes = count ( Node n0 | exists ( PathNode pn | pn .getNode ( ) = n0 and reach ( pn ) ) ) and
3191+ fields =
3192+ count ( TypedContent f0 |
3193+ exists ( PathNodeMid pn | pn .getAp ( ) .getFront ( ) .headUsesContent ( f0 ) and reach ( pn ) )
3194+ ) and
3195+ conscand = count ( AccessPath ap | exists ( PathNodeMid pn | pn .getAp ( ) = ap and reach ( pn ) ) ) and
3196+ tuples = count ( PathNode pn | reach ( pn ) )
3197+ }
3198+
3199+ predicate stageStats (
3200+ int n , string stage , int nodes , int fields , int conscand , int tuples , Configuration config
3201+ ) {
3202+ stage = "1 Fwd" and n = 10 and Stage1:: stats ( true , nodes , fields , conscand , tuples , config )
3203+ or
3204+ stage = "1 Rev" and n = 15 and Stage1:: stats ( false , nodes , fields , conscand , tuples , config )
3205+ or
3206+ stage = "2 Fwd" and n = 20 and Stage2:: stats ( true , nodes , fields , conscand , tuples , config )
3207+ or
3208+ stage = "2 Rev" and n = 25 and Stage2:: stats ( false , nodes , fields , conscand , tuples , config )
3209+ or
3210+ stage = "3 Fwd" and n = 30 and Stage3:: stats ( true , nodes , fields , conscand , tuples , config )
3211+ or
3212+ stage = "3 Rev" and n = 35 and Stage3:: stats ( false , nodes , fields , conscand , tuples , config )
3213+ or
3214+ stage = "4 Fwd" and n = 40 and Stage4:: stats ( true , nodes , fields , conscand , tuples , config )
3215+ or
3216+ stage = "4 Rev" and n = 45 and Stage4:: stats ( false , nodes , fields , conscand , tuples , config )
3217+ or
3218+ stage = "5 Fwd" and n = 50 and finalStats ( true , nodes , fields , conscand , tuples )
3219+ or
3220+ stage = "5 Rev" and n = 55 and finalStats ( false , nodes , fields , conscand , tuples )
3221+ }
3222+
31253223private module FlowExploration {
31263224 private predicate callableStep ( DataFlowCallable c1 , DataFlowCallable c2 , Configuration config ) {
31273225 exists ( Node node1 , Node node2 |
0 commit comments