@@ -917,22 +917,46 @@ module MakeImpl<InputSig Lang> {
917
917
)
918
918
}
919
919
920
+ predicate callEdgeArgParam (
921
+ DataFlowCall call , DataFlowCallable c , ArgNodeEx arg , ParamNodeEx p ,
922
+ boolean allowsFieldFlow , Ap ap
923
+ ) {
924
+ flowIntoCallNodeCand1 ( call , arg , p , allowsFieldFlow ) and
925
+ c = p .getEnclosingCallable ( ) and
926
+ exists ( ap )
927
+ }
928
+
929
+ predicate callEdgeReturn (
930
+ DataFlowCall call , DataFlowCallable c , RetNodeEx ret , ReturnKindExt kind , NodeEx out ,
931
+ boolean allowsFieldFlow , Ap ap
932
+ ) {
933
+ flowOutOfCallNodeCand1 ( call , ret , kind , out , allowsFieldFlow ) and
934
+ c = ret .getEnclosingCallable ( ) and
935
+ exists ( ap )
936
+ }
937
+
920
938
additional predicate stats (
921
- boolean fwd , int nodes , int fields , int conscand , int states , int tuples
939
+ boolean fwd , int nodes , int fields , int conscand , int states , int tuples , int calledges
922
940
) {
923
941
fwd = true and
924
942
nodes = count ( NodeEx node | fwdFlow ( node ) ) and
925
943
fields = count ( Content f0 | fwdFlowConsCand ( f0 ) ) and
926
944
conscand = - 1 and
927
945
states = count ( FlowState state | fwdFlowState ( state ) ) and
928
- tuples = count ( NodeEx n , boolean b | fwdFlow ( n , b ) )
946
+ tuples = count ( NodeEx n , boolean b | fwdFlow ( n , b ) ) and
947
+ calledges = - 1
929
948
or
930
949
fwd = false and
931
950
nodes = count ( NodeEx node | revFlow ( node , _) ) and
932
951
fields = count ( Content f0 | revFlowConsCand ( f0 ) ) and
933
952
conscand = - 1 and
934
953
states = count ( FlowState state | revFlowState ( state ) ) and
935
- tuples = count ( NodeEx n , boolean b | revFlow ( n , b ) )
954
+ tuples = count ( NodeEx n , boolean b | revFlow ( n , b ) ) and
955
+ calledges =
956
+ count ( DataFlowCall call , DataFlowCallable c |
957
+ callEdgeArgParam ( call , c , _, _, _, _) or
958
+ callEdgeReturn ( call , c , _, _, _, _, _)
959
+ )
936
960
}
937
961
/* End: Stage 1 logic. */
938
962
}
@@ -1093,6 +1117,16 @@ module MakeImpl<InputSig Lang> {
1093
1117
) ;
1094
1118
1095
1119
predicate readStepCand ( NodeEx n1 , Content c , NodeEx n2 ) ;
1120
+
1121
+ predicate callEdgeArgParam (
1122
+ DataFlowCall call , DataFlowCallable c , ArgNodeEx arg , ParamNodeEx p ,
1123
+ boolean allowsFieldFlow , Ap ap
1124
+ ) ;
1125
+
1126
+ predicate callEdgeReturn (
1127
+ DataFlowCall call , DataFlowCallable c , RetNodeEx ret , ReturnKindExt kind , NodeEx out ,
1128
+ boolean allowsFieldFlow , Ap ap
1129
+ ) ;
1096
1130
}
1097
1131
1098
1132
private module MkStage< StageSig PrevStage> {
@@ -1172,14 +1206,6 @@ module MakeImpl<InputSig Lang> {
1172
1206
Typ t , LocalCc lcc
1173
1207
) ;
1174
1208
1175
- predicate flowOutOfCall (
1176
- DataFlowCall call , RetNodeEx ret , ReturnKindExt kind , NodeEx out , boolean allowsFieldFlow
1177
- ) ;
1178
-
1179
- predicate flowIntoCall (
1180
- DataFlowCall call , ArgNodeEx arg , ParamNodeEx p , boolean allowsFieldFlow
1181
- ) ;
1182
-
1183
1209
bindingset [ node, state, t0, ap]
1184
1210
predicate filter ( NodeEx node , FlowState state , Typ t0 , Ap ap , Typ t ) ;
1185
1211
@@ -1202,35 +1228,13 @@ module MakeImpl<InputSig Lang> {
1202
1228
PrevStage:: revFlow ( node ) and result = getTyp ( node .getDataFlowType ( ) )
1203
1229
}
1204
1230
1205
- pragma [ nomagic]
1206
- private predicate flowIntoCallApa (
1207
- DataFlowCall call , DataFlowCallable c , ArgNodeEx arg , ParamNodeEx p ,
1208
- boolean allowsFieldFlow , ApApprox apa
1209
- ) {
1210
- flowIntoCall ( call , arg , p , allowsFieldFlow ) and
1211
- PrevStage:: revFlowAp ( p , pragma [ only_bind_into ] ( apa ) ) and
1212
- PrevStage:: revFlowAp ( arg , pragma [ only_bind_into ] ( apa ) ) and
1213
- c = p .getEnclosingCallable ( )
1214
- }
1215
-
1216
- pragma [ nomagic]
1217
- private predicate flowOutOfCallApa (
1218
- DataFlowCall call , DataFlowCallable c , RetNodeEx ret , ReturnKindExt kind , NodeEx out ,
1219
- boolean allowsFieldFlow , ApApprox apa
1220
- ) {
1221
- flowOutOfCall ( call , ret , kind , out , allowsFieldFlow ) and
1222
- PrevStage:: revFlowAp ( out , pragma [ only_bind_into ] ( apa ) ) and
1223
- PrevStage:: revFlowAp ( ret , pragma [ only_bind_into ] ( apa ) ) and
1224
- c = ret .getEnclosingCallable ( )
1225
- }
1226
-
1227
1231
pragma [ nomagic]
1228
1232
private predicate flowThroughOutOfCall (
1229
1233
DataFlowCall call , CcCall ccc , RetNodeEx ret , NodeEx out , boolean allowsFieldFlow ,
1230
1234
ApApprox argApa , ApApprox apa
1231
1235
) {
1232
1236
exists ( ReturnKindExt kind |
1233
- flowOutOfCallApa ( call , _, ret , kind , out , allowsFieldFlow , apa ) and
1237
+ PrevStage :: callEdgeReturn ( call , _, ret , kind , out , allowsFieldFlow , apa ) and
1234
1238
PrevStage:: callMayFlowThroughRev ( call ) and
1235
1239
PrevStage:: returnMayFlowThrough ( ret , argApa , apa , kind ) and
1236
1240
matchesCall ( ccc , call )
@@ -1434,7 +1438,7 @@ module MakeImpl<InputSig Lang> {
1434
1438
DataFlowCall call , DataFlowCallable c , ArgNodeEx arg , ParamNodeEx p ,
1435
1439
boolean allowsFieldFlow , ApApprox apa
1436
1440
) {
1437
- flowIntoCallApa ( call , c , arg , p , allowsFieldFlow , apa )
1441
+ PrevStage :: callEdgeArgParam ( call , c , arg , p , allowsFieldFlow , apa )
1438
1442
}
1439
1443
1440
1444
bindingset [ call, ctx]
@@ -1499,7 +1503,7 @@ module MakeImpl<InputSig Lang> {
1499
1503
DataFlowCall call , DataFlowCallable c , RetNodeEx ret , NodeEx out , boolean allowsFieldFlow ,
1500
1504
ApApprox apa
1501
1505
) {
1502
- flowOutOfCallApa ( call , c , ret , _, out , allowsFieldFlow , apa )
1506
+ PrevStage :: callEdgeReturn ( call , c , ret , _, out , allowsFieldFlow , apa )
1503
1507
}
1504
1508
1505
1509
bindingset [ c, ret, apa, innercc]
@@ -1510,7 +1514,7 @@ module MakeImpl<InputSig Lang> {
1510
1514
ApApprox apa , CcNoCall innercc
1511
1515
) {
1512
1516
viableImplNotCallContextReducedReverse ( innercc ) and
1513
- flowOutOfCallApa ( call , c , ret , _, out , allowsFieldFlow , apa )
1517
+ PrevStage :: callEdgeReturn ( call , c , ret , _, out , allowsFieldFlow , apa )
1514
1518
}
1515
1519
1516
1520
pragma [ nomagic]
@@ -1546,11 +1550,11 @@ module MakeImpl<InputSig Lang> {
1546
1550
predicate enableTypeFlow = Param:: enableTypeFlow / 0 ;
1547
1551
1548
1552
predicate relevantCallEdgeIn ( DataFlowCall call , DataFlowCallable c ) {
1549
- flowIntoCallApa ( call , c , _, _, _, _)
1553
+ PrevStage :: callEdgeArgParam ( call , c , _, _, _, _)
1550
1554
}
1551
1555
1552
1556
predicate relevantCallEdgeOut ( DataFlowCall call , DataFlowCallable c ) {
1553
- flowOutOfCallApa ( call , c , _, _, _, _, _)
1557
+ PrevStage :: callEdgeReturn ( call , c , _, _, _, _, _)
1554
1558
}
1555
1559
1556
1560
pragma [ nomagic]
@@ -1593,7 +1597,7 @@ module MakeImpl<InputSig Lang> {
1593
1597
DataFlowCall call , DataFlowCallable c , ArgNodeEx arg , ParamNodeEx p ,
1594
1598
boolean allowsFieldFlow , ApApprox apa
1595
1599
) {
1596
- flowIntoCallApa ( call , c , arg , p , allowsFieldFlow , apa ) and
1600
+ PrevStage :: callEdgeArgParam ( call , c , arg , p , allowsFieldFlow , apa ) and
1597
1601
FwdTypeFlowInput:: dataFlowTakenCallEdgeIn ( call , c , _)
1598
1602
}
1599
1603
@@ -1720,7 +1724,7 @@ module MakeImpl<InputSig Lang> {
1720
1724
Ap ap
1721
1725
) {
1722
1726
exists ( ApApprox apa , boolean allowsFieldFlow |
1723
- flowOutOfCallApa ( call , c , ret , _, out , allowsFieldFlow , apa ) and
1727
+ PrevStage :: callEdgeReturn ( call , c , ret , _, out , allowsFieldFlow , apa ) and
1724
1728
fwdFlow ( ret , _, _, _, _, _, _, ap , apa ) and
1725
1729
pos = ret .getReturnPosition ( ) and
1726
1730
if allowsFieldFlow = false then ap instanceof ApNil else any ( )
@@ -2064,6 +2068,35 @@ module MakeImpl<InputSig Lang> {
2064
2068
)
2065
2069
}
2066
2070
2071
+ predicate callEdgeArgParam (
2072
+ DataFlowCall call , DataFlowCallable c , ArgNodeEx arg , ParamNodeEx p ,
2073
+ boolean allowsFieldFlow , Ap ap
2074
+ ) {
2075
+ exists ( FlowState state |
2076
+ flowIntoCallAp ( call , c , arg , p , ap ) and
2077
+ revFlow ( arg , pragma [ only_bind_into ] ( state ) , pragma [ only_bind_into ] ( ap ) ) and
2078
+ revFlow ( p , pragma [ only_bind_into ] ( state ) , pragma [ only_bind_into ] ( ap ) ) and
2079
+ allowsFieldFlow = true
2080
+ |
2081
+ RevTypeFlowInput:: dataFlowTakenCallEdgeIn ( call , c , _) or
2082
+ RevTypeFlowInput:: dataFlowTakenCallEdgeOut ( call , c )
2083
+ )
2084
+ }
2085
+
2086
+ predicate callEdgeReturn (
2087
+ DataFlowCall call , DataFlowCallable c , RetNodeEx ret , ReturnKindExt kind , NodeEx out ,
2088
+ boolean allowsFieldFlow , Ap ap
2089
+ ) {
2090
+ exists ( FlowState state , ReturnPosition pos |
2091
+ flowOutOfCallAp ( call , c , ret , pos , out , ap ) and
2092
+ revFlow ( ret , pragma [ only_bind_into ] ( state ) , pragma [ only_bind_into ] ( ap ) ) and
2093
+ revFlow ( out , pragma [ only_bind_into ] ( state ) , pragma [ only_bind_into ] ( ap ) ) and
2094
+ kind = pos .getKind ( ) and
2095
+ allowsFieldFlow = true and
2096
+ RevTypeFlowInput:: dataFlowTakenCallEdgeIn ( call , c , _)
2097
+ )
2098
+ }
2099
+
2067
2100
additional predicate stats (
2068
2101
boolean fwd , int nodes , int fields , int conscand , int states , int tuples , int calledges ,
2069
2102
int tfnodes , int tftuples
@@ -2287,10 +2320,6 @@ module MakeImpl<InputSig Lang> {
2287
2320
exists ( lcc )
2288
2321
}
2289
2322
2290
- predicate flowOutOfCall = flowOutOfCallNodeCand1 / 5 ;
2291
-
2292
- predicate flowIntoCall = flowIntoCallNodeCand1 / 4 ;
2293
-
2294
2323
pragma [ nomagic]
2295
2324
private predicate expectsContentCand ( NodeEx node ) {
2296
2325
exists ( Content c |
@@ -2544,10 +2573,6 @@ module MakeImpl<InputSig Lang> {
2544
2573
exists ( lcc )
2545
2574
}
2546
2575
2547
- predicate flowOutOfCall = flowOutOfCallNodeCand2 / 5 ;
2548
-
2549
- predicate flowIntoCall = flowIntoCallNodeCand2 / 4 ;
2550
-
2551
2576
pragma [ nomagic]
2552
2577
private predicate expectsContentCand ( NodeEx node , Ap ap ) {
2553
2578
exists ( Content c |
@@ -2639,29 +2664,6 @@ module MakeImpl<InputSig Lang> {
2639
2664
exists ( lcc )
2640
2665
}
2641
2666
2642
- pragma [ nomagic]
2643
- predicate flowOutOfCall (
2644
- DataFlowCall call , RetNodeEx node1 , ReturnKindExt kind , NodeEx node2 ,
2645
- boolean allowsFieldFlow
2646
- ) {
2647
- exists ( FlowState state |
2648
- flowOutOfCallNodeCand2 ( call , node1 , kind , node2 , allowsFieldFlow ) and
2649
- PrevStage:: revFlow ( node2 , pragma [ only_bind_into ] ( state ) , _) and
2650
- PrevStage:: revFlow ( node1 , pragma [ only_bind_into ] ( state ) , _)
2651
- )
2652
- }
2653
-
2654
- pragma [ nomagic]
2655
- predicate flowIntoCall (
2656
- DataFlowCall call , ArgNodeEx node1 , ParamNodeEx node2 , boolean allowsFieldFlow
2657
- ) {
2658
- exists ( FlowState state |
2659
- flowIntoCallNodeCand2 ( call , node1 , node2 , allowsFieldFlow ) and
2660
- PrevStage:: revFlow ( node2 , pragma [ only_bind_into ] ( state ) , _) and
2661
- PrevStage:: revFlow ( node1 , pragma [ only_bind_into ] ( state ) , _)
2662
- )
2663
- }
2664
-
2665
2667
pragma [ nomagic]
2666
2668
private predicate clearSet ( NodeEx node , ContentSet c ) {
2667
2669
PrevStage:: revFlow ( node ) and
@@ -2944,29 +2946,6 @@ module MakeImpl<InputSig Lang> {
2944
2946
PrevStage:: revFlow ( node2 , pragma [ only_bind_into ] ( state2 ) , _)
2945
2947
}
2946
2948
2947
- pragma [ nomagic]
2948
- predicate flowOutOfCall (
2949
- DataFlowCall call , RetNodeEx node1 , ReturnKindExt kind , NodeEx node2 ,
2950
- boolean allowsFieldFlow
2951
- ) {
2952
- exists ( FlowState state |
2953
- flowOutOfCallNodeCand2 ( call , node1 , kind , node2 , allowsFieldFlow ) and
2954
- PrevStage:: revFlow ( node2 , pragma [ only_bind_into ] ( state ) , _) and
2955
- PrevStage:: revFlow ( node1 , pragma [ only_bind_into ] ( state ) , _)
2956
- )
2957
- }
2958
-
2959
- pragma [ nomagic]
2960
- predicate flowIntoCall (
2961
- DataFlowCall call , ArgNodeEx node1 , ParamNodeEx node2 , boolean allowsFieldFlow
2962
- ) {
2963
- exists ( FlowState state |
2964
- flowIntoCallNodeCand2 ( call , node1 , node2 , allowsFieldFlow ) and
2965
- PrevStage:: revFlow ( node2 , pragma [ only_bind_into ] ( state ) , _) and
2966
- PrevStage:: revFlow ( node1 , pragma [ only_bind_into ] ( state ) , _)
2967
- )
2968
- }
2969
-
2970
2949
bindingset [ node, state, t0, ap]
2971
2950
predicate filter ( NodeEx node , FlowState state , Typ t0 , Ap ap , Typ t ) {
2972
2951
strengthenType ( node , t0 , t ) and
@@ -4136,15 +4115,13 @@ module MakeImpl<InputSig Lang> {
4136
4115
) {
4137
4116
stage = "1 Fwd" and
4138
4117
n = 10 and
4139
- Stage1:: stats ( true , nodes , fields , conscand , states , tuples ) and
4140
- calledges = - 1 and
4118
+ Stage1:: stats ( true , nodes , fields , conscand , states , tuples , calledges ) and
4141
4119
tfnodes = - 1 and
4142
4120
tftuples = - 1
4143
4121
or
4144
4122
stage = "1 Rev" and
4145
4123
n = 15 and
4146
- Stage1:: stats ( false , nodes , fields , conscand , states , tuples ) and
4147
- calledges = - 1 and
4124
+ Stage1:: stats ( false , nodes , fields , conscand , states , tuples , calledges ) and
4148
4125
tfnodes = - 1 and
4149
4126
tftuples = - 1
4150
4127
or
0 commit comments