@@ -939,18 +939,21 @@ private predicate basicFlowStepNoBarrier(
939
939
* This predicate is field insensitive (it does not distinguish between `x` and `x.p`)
940
940
* and hence should only be used for purposes of approximation.
941
941
*/
942
- pragma [ inline ]
942
+ pragma [ noinline ]
943
943
private predicate exploratoryFlowStep (
944
944
DataFlow:: Node pred , DataFlow:: Node succ , DataFlow:: Configuration cfg
945
945
) {
946
- basicFlowStepNoBarrier ( pred , succ , _, cfg ) or
947
- exploratoryLoadStep ( pred , succ , cfg ) or
948
- isAdditionalLoadStoreStep ( pred , succ , _, _, cfg ) or
949
- // the following three disjuncts taken together over-approximate flow through
950
- // higher-order calls
951
- exploratoryCallbackStep ( pred , succ ) or
952
- succ = pred .( DataFlow:: FunctionNode ) .getAParameter ( ) or
953
- exploratoryBoundInvokeStep ( pred , succ )
946
+ isRelevantForward ( pred , cfg ) and
947
+ (
948
+ basicFlowStepNoBarrier ( pred , succ , _, cfg ) or
949
+ exploratoryLoadStep ( pred , succ , cfg ) or
950
+ isAdditionalLoadStoreStep ( pred , succ , _, _, cfg ) or
951
+ // the following three disjuncts taken together over-approximate flow through
952
+ // higher-order calls
953
+ exploratoryCallbackStep ( pred , succ ) or
954
+ succ = pred .( DataFlow:: FunctionNode ) .getAParameter ( ) or
955
+ exploratoryBoundInvokeStep ( pred , succ )
956
+ )
954
957
}
955
958
956
959
/**
@@ -1024,6 +1027,7 @@ private string getAPropertyUsedInLoadStore(DataFlow::Configuration cfg) {
1024
1027
* Holds if there exists a store-step from `pred` to `succ` under configuration `cfg`,
1025
1028
* and somewhere in the program there exists a load-step that could possibly read the stored value.
1026
1029
*/
1030
+ pragma [ noinline]
1027
1031
private predicate exploratoryForwardStoreStep (
1028
1032
DataFlow:: Node pred , DataFlow:: Node succ , DataFlow:: Configuration cfg
1029
1033
) {
@@ -1075,8 +1079,10 @@ private string getABackwardsRelevantStoreProperty(DataFlow::Configuration cfg) {
1075
1079
private predicate isRelevantForward ( DataFlow:: Node nd , DataFlow:: Configuration cfg ) {
1076
1080
isSource ( nd , cfg , _) and isLive ( )
1077
1081
or
1078
- exists ( DataFlow:: Node mid | isRelevantForward ( mid , cfg ) |
1079
- exploratoryFlowStep ( mid , nd , cfg ) or
1082
+ exists ( DataFlow:: Node mid |
1083
+ exploratoryFlowStep ( mid , nd , cfg )
1084
+ or
1085
+ isRelevantForward ( mid , cfg ) and
1080
1086
exploratoryForwardStoreStep ( mid , nd , cfg )
1081
1087
)
1082
1088
}
@@ -1098,11 +1104,10 @@ private predicate isRelevant(DataFlow::Node nd, DataFlow::Configuration cfg) {
1098
1104
private predicate isRelevantBackStep (
1099
1105
DataFlow:: Node mid , DataFlow:: Node nd , DataFlow:: Configuration cfg
1100
1106
) {
1107
+ exploratoryFlowStep ( nd , mid , cfg )
1108
+ or
1101
1109
isRelevantForward ( nd , cfg ) and
1102
- (
1103
- exploratoryFlowStep ( nd , mid , cfg ) or
1104
- exploratoryBackwardStoreStep ( nd , mid , cfg )
1105
- )
1110
+ exploratoryBackwardStoreStep ( nd , mid , cfg )
1106
1111
}
1107
1112
1108
1113
/**
@@ -1273,23 +1278,30 @@ private predicate parameterPropRead(
1273
1278
DataFlow:: Node arg , string prop , DataFlow:: Node succ , DataFlow:: Configuration cfg ,
1274
1279
PathSummary summary
1275
1280
) {
1276
- exists ( Function f , DataFlow:: Node read , DataFlow:: Node invk |
1281
+ exists ( Function f , DataFlow:: Node read , DataFlow:: Node invk , DataFlow:: Node parm |
1282
+ reachesReturn ( f , read , cfg , summary ) and
1283
+ parameterPropReadStep ( parm , read , prop , cfg , arg , invk , f , succ )
1284
+ )
1285
+ }
1286
+
1287
+ // all the non-recursive parts of parameterPropRead outlined into a precomputed predicate
1288
+ pragma [ noinline]
1289
+ private predicate parameterPropReadStep (
1290
+ DataFlow:: SourceNode parm , DataFlow:: Node read , string prop , DataFlow:: Configuration cfg ,
1291
+ DataFlow:: Node arg , DataFlow:: Node invk , Function f , DataFlow:: Node succ
1292
+ ) {
1293
+ (
1277
1294
not f .isAsyncOrGenerator ( ) and invk = succ
1278
1295
or
1279
1296
// load from an immediately awaited function call
1280
1297
f .isAsync ( ) and
1281
1298
invk = getAwaitOperand ( succ )
1282
- |
1283
- exists ( DataFlow:: SourceNode parm |
1284
- callInputStep ( f , invk , arg , parm , cfg ) and
1285
- (
1286
- reachesReturn ( f , read , cfg , summary ) and
1287
- read = parm .getAPropertyRead ( prop )
1288
- or
1289
- reachesReturn ( f , read , cfg , summary ) and
1290
- exists ( DataFlow:: Node use | parm .flowsTo ( use ) | isAdditionalLoadStep ( use , read , prop , cfg ) )
1291
- )
1292
- )
1299
+ ) and
1300
+ callInputStep ( f , invk , arg , parm , cfg ) and
1301
+ (
1302
+ read = parm .getAPropertyRead ( prop )
1303
+ or
1304
+ exists ( DataFlow:: Node use | parm .flowsTo ( use ) | isAdditionalLoadStep ( use , read , prop , cfg ) )
1293
1305
)
1294
1306
}
1295
1307
0 commit comments