@@ -720,7 +720,9 @@ module MakeImpl<InputSig Lang> {
720
720
* the enclosing callable in order to reach a sink.
721
721
*/
722
722
pragma [ nomagic]
723
- private predicate revFlow ( NodeEx node , boolean toReturn ) {
723
+ // private
724
+ additional
725
+ predicate revFlow ( NodeEx node , boolean toReturn ) {
724
726
revFlow0 ( node , toReturn ) and
725
727
fwdFlow ( node )
726
728
}
@@ -1076,6 +1078,43 @@ module MakeImpl<InputSig Lang> {
1076
1078
result = getAdditionalFlowIntoCallNodeTerm ( arg .projectToNode ( ) , p .projectToNode ( ) )
1077
1079
}
1078
1080
1081
+ pragma [ nomagic]
1082
+ private predicate returnCallEdge1 ( DataFlowCallable c , DataFlowCall call , NodeEx out ) {
1083
+ exists ( RetNodeEx ret |
1084
+ flowOutOfCallNodeCand1 ( call , ret , _, out ) and c = ret .getEnclosingCallable ( )
1085
+ )
1086
+ }
1087
+
1088
+ private int simpleDispatchFanoutOnReturn ( DataFlowCall call , NodeEx out ) {
1089
+ result =
1090
+ strictcount ( DataFlowCallable c | returnCallEdge1 ( c , call , out ) )
1091
+ }
1092
+
1093
+ private int ctxDispatchFanoutOnReturn ( NodeEx out , DataFlowCall ctx ) {
1094
+ exists ( DataFlowCall call , DataFlowCallable c |
1095
+ simpleDispatchFanoutOnReturn ( call , out ) > 1 and
1096
+ not Stage1:: revFlow ( out , false ) and
1097
+ call .getEnclosingCallable ( ) = c and
1098
+ returnCallEdge1 ( c , ctx , _) and
1099
+ mayBenefitFromCallContextExt ( call , _) and
1100
+ result = count ( DataFlowCallable tgt |
1101
+ tgt = viableImplInCallContextExt ( call , ctx ) and
1102
+ returnCallEdge1 ( tgt , call , out )
1103
+ )
1104
+ )
1105
+ }
1106
+
1107
+ private int ctxDispatchFanoutOnReturn ( NodeEx out ) {
1108
+ result = max ( DataFlowCall ctx | | ctxDispatchFanoutOnReturn ( out , ctx ) )
1109
+ }
1110
+
1111
+ private int dispatchFanoutOnReturn ( NodeEx out ) {
1112
+ result = ctxDispatchFanoutOnReturn ( out )
1113
+ or
1114
+ not exists ( ctxDispatchFanoutOnReturn ( out ) ) and
1115
+ result = simpleDispatchFanoutOnReturn ( _, out )
1116
+ }
1117
+
1079
1118
/**
1080
1119
* Gets the amount of forward branching on the origin of a cross-call path
1081
1120
* edge in the graph of paths between sources and sinks that ignores call
@@ -1092,6 +1131,17 @@ module MakeImpl<InputSig Lang> {
1092
1131
// ) + sum(ParamNodeEx p1 | | getLanguageSpecificFlowIntoCallNodeCand1(n1, p1))
1093
1132
}
1094
1133
1134
+ // pragma[nomagic]
1135
+ // private int branch_out(NodeEx n1) {
1136
+ // result =
1137
+ // // strictcount(DataFlowCallable c | exists(NodeEx n |
1138
+ // // flowOutOfCallNodeCand1(_, n1, _, n) or flowIntoCallNodeCand1(_, n1, n) | c = n.getEnclosingCallable())
1139
+ // // ) + sum(ParamNodeEx p1 | | getLanguageSpecificFlowIntoCallNodeCand1(n1, p1))
1140
+ // strictcount(NodeEx n |
1141
+ // flowOutOfCallNodeCand1(_, n1, _, n) //or flowIntoCallNodeCand1(_, n1, n)
1142
+ // ) //+ sum(ParamNodeEx p1 | | getLanguageSpecificFlowIntoCallNodeCand1(n1, p1))
1143
+ // }
1144
+
1095
1145
/**
1096
1146
* Gets the amount of backward branching on the target of a cross-call path
1097
1147
* edge in the graph of paths between sources and sinks that ignores call
@@ -1108,6 +1158,28 @@ module MakeImpl<InputSig Lang> {
1108
1158
// ) + sum(ArgNodeEx arg2 | | getLanguageSpecificFlowIntoCallNodeCand1(arg2, n2))
1109
1159
}
1110
1160
1161
+ // pragma[nomagic]
1162
+ // private int join_out(NodeEx n2) {
1163
+ // result =
1164
+ // // strictcount(DataFlowCallable c | exists(NodeEx n |
1165
+ // // flowOutOfCallNodeCand1(_, n, _, n2) or flowIntoCallNodeCand1(_, n, n2) | c = n.getEnclosingCallable())
1166
+ // // ) + sum(ArgNodeEx arg2 | | getLanguageSpecificFlowIntoCallNodeCand1(arg2, n2))
1167
+ // strictcount(NodeEx n |
1168
+ // flowOutOfCallNodeCand1(_, n, _, n2) //or flowIntoCallNodeCand1(_, n, n2)
1169
+ // ) //+ sum(ArgNodeEx arg2 | | getLanguageSpecificFlowIntoCallNodeCand1(arg2, n2))
1170
+ // }
1171
+
1172
+ // pragma[nomagic]
1173
+ // private int join_out_v2(NodeEx n2) {
1174
+ // result =
1175
+ // strictcount(DataFlowCallable c | exists(NodeEx n |
1176
+ // flowOutOfCallNodeCand1(_, n, _, n2) and c = n.getEnclosingCallable())
1177
+ // )
1178
+ // // strictcount(NodeEx n |
1179
+ // // flowOutOfCallNodeCand1(_, n, _, n2)
1180
+ // // )
1181
+ // }
1182
+
1111
1183
/**
1112
1184
* Holds if data can flow out of `call` from `ret` to `out`, either
1113
1185
* through a `ReturnNode` or through an argument that has been mutated, and
@@ -1121,15 +1193,93 @@ module MakeImpl<InputSig Lang> {
1121
1193
) {
1122
1194
flowOutOfCallNodeCand1 ( call , ret , kind , out ) and
1123
1195
exists ( int j | //b, int j |
1124
- // b = branch(ret) and
1125
- j = join ( out ) and
1126
- // if b.minimum(j) <= Config::fieldFlowBranchLimit()
1196
+ j = dispatchFanoutOnReturn ( out ) and
1197
+ j > 0 and
1127
1198
if j <= Config:: fieldFlowBranchLimit ( )
1199
+
1200
+ // exists(int b, int j |
1201
+ // b = branch(ret) and
1202
+ // j = join(out) and
1203
+ // if b.minimum(j) <= Config::fieldFlowBranchLimit()
1204
+
1205
+ // exists(int j | //b, int j |
1206
+ // // b = branch(ret) and
1207
+ // j = join_out_v2(out) and
1208
+ // // if b.minimum(j) <= Config::fieldFlowBranchLimit()
1209
+ // if j <= Config::fieldFlowBranchLimit()
1210
+
1128
1211
then allowsFieldFlow = true
1129
1212
else allowsFieldFlow = false
1130
1213
)
1131
1214
}
1132
1215
1216
+ // pragma[nomagic]
1217
+ // private predicate flowOutOfCallNodeCand1_v2(
1218
+ // DataFlowCall call, RetNodeEx ret, ReturnKindExt kind, NodeEx out, boolean allowsFieldFlow
1219
+ // ) {
1220
+ // flowOutOfCallNodeCand1(call, ret, kind, out) and
1221
+ // // exists(int b, int j |
1222
+ // // b = branch_out(ret) and
1223
+ // // j = join_out(out) and
1224
+ // // if b.minimum(j) <= Config::fieldFlowBranchLimit()
1225
+ // exists(int j | //b, int j |
1226
+ // // b = branch(ret) and
1227
+ // j = join_out_v2(out) and
1228
+ // // if b.minimum(j) <= Config::fieldFlowBranchLimit()
1229
+ // if j <= Config::fieldFlowBranchLimit()
1230
+ // then allowsFieldFlow = true
1231
+ // else allowsFieldFlow = false
1232
+ // )
1233
+ // }
1234
+
1235
+ // pragma[nomagic]
1236
+ // predicate hasSummary(NodeEx out) {
1237
+ // exists(RetNodeEx ret |
1238
+ // flowOutOfCallNodeCand1(_, ret, _, out) and
1239
+ // ret.toString().matches("[summary]%")
1240
+ // )
1241
+ // }
1242
+
1243
+ // predicate cmp(int d, string allow) {
1244
+ // d = strictcount(DataFlowCall call, RetNodeEx ret, ReturnKindExt kind, NodeEx out |
1245
+ // exists(boolean aff1, boolean aff2 |
1246
+ // flowOutOfCallNodeCand1(call, ret, kind, out, aff1) and
1247
+ // flowOutOfCallNodeCand1_v2(call, ret, kind, out, aff2) and
1248
+ // aff1 != aff2
1249
+ // and if aff2 = true then allow = "add" else allow = "remove"
1250
+ // )
1251
+ // )
1252
+ // }
1253
+
1254
+ // predicate cmplist(DataFlowCall call, RetNodeEx ret, ReturnKindExt kind, NodeEx out, string allow, int b1, int j1, int j2) {
1255
+ // exists(boolean aff1, boolean aff2 |
1256
+ // flowOutOfCallNodeCand1(call, ret, kind, out, aff1) and
1257
+ // flowOutOfCallNodeCand1_v2(call, ret, kind, out, aff2) and
1258
+ // aff1 != aff2
1259
+ // and if aff2 = true then allow = "add" else allow = "remove"
1260
+ // )
1261
+ // and b1 = branch(ret) and j1 = join(out) and j2 = join_out_v2(out)
1262
+ // and not hasSummary(out)
1263
+ // }
1264
+
1265
+ // predicate cmplist_2(DataFlowCall call, RetNodeEx ret, ReturnKindExt kind, NodeEx out, string allow, int b1, int j1, int j2, int j3) {
1266
+ // exists(boolean aff1, boolean aff2 |
1267
+ // flowOutOfCallNodeCand1(call, ret, kind, out, aff1) and
1268
+ // flowOutOfCallNodeCand1_v2(call, ret, kind, out, aff2)
1269
+ // |
1270
+ // // aff1 = false and aff2 = true and allow = "add"
1271
+ // // or
1272
+ // aff1 = true and aff2 = false and allow = "keep"
1273
+ // or
1274
+ // aff1 = false and aff2 = false and allow = "add cc"
1275
+ // )
1276
+ // and b1 = branch(ret) and j1 = join(out) and j2 = join_out_v2(out)
1277
+ // and j3 = dispatchFanoutOnReturn(out)
1278
+ // // and not hasSummary(out)
1279
+ // // and reducedViableImplInReturn(ret.getEnclosingCallable(), call)
1280
+ // and j3 <= 2
1281
+ // }
1282
+
1133
1283
/**
1134
1284
* Holds if data can flow into `call` and that this step is part of a
1135
1285
* path from a source to a sink. The `allowsFieldFlow` flag indicates whether
0 commit comments