@@ -1267,56 +1267,47 @@ private predicate loadStep(
1267
1267
* If `onlyRelevantInCall` is true, the `base` object will not be propagated out of return edges, because
1268
1268
* the flow that originally reached `base.startProp` used a call edge.
1269
1269
*/
1270
- pragma [ nomagic ]
1270
+ pragma [ noopt ]
1271
1271
private predicate reachableFromStoreBase (
1272
1272
string startProp , string endProp , DataFlow:: Node base , DataFlow:: Node nd ,
1273
- DataFlow:: Configuration cfg , PathSummary summary , boolean onlyRelevantInCall
1273
+ DataFlow:: Configuration cfg , TPathSummary summary , boolean onlyRelevantInCall
1274
1274
) {
1275
- exists ( PathSummary s1 , PathSummary s2 , DataFlow:: Node rhs |
1276
- reachableFromSource ( rhs , cfg , s1 ) and
1277
- onlyRelevantInCall = s1 .hasCall ( )
1278
- or
1279
- reachableFromStoreBase ( _, _, _, rhs , cfg , s1 , onlyRelevantInCall )
1280
- |
1275
+ exists ( TPathSummary s1 , TPathSummary s2 , DataFlow:: Node rhs |
1281
1276
storeStep ( rhs , nd , startProp , cfg , s2 ) and
1282
1277
endProp = startProp and
1283
1278
base = nd and
1284
- summary =
1285
- MkPathSummary ( false , s2 .hasCall ( ) , DataFlow:: FlowLabel:: data ( ) , DataFlow:: FlowLabel:: data ( ) )
1279
+ exists ( boolean hasCall , DataFlow:: FlowLabel data |
1280
+ hasCall = hasCall ( s2 ) and
1281
+ data = DataFlow:: FlowLabel:: data ( ) and
1282
+ summary = MkPathSummary ( false , hasCall , data , data )
1283
+ )
1284
+ |
1285
+ reachableFromSource ( rhs , cfg , s1 ) and
1286
+ onlyRelevantInCall = hasCall ( s1 )
1287
+ or
1288
+ reachableFromStoreBase ( _, _, _, rhs , cfg , s1 , onlyRelevantInCall )
1286
1289
)
1287
1290
or
1288
- exists ( PathSummary newSummary , PathSummary oldSummary |
1289
- reachableFromStoreBaseStep ( startProp , endProp , base , nd , cfg , oldSummary , newSummary ,
1290
- onlyRelevantInCall ) and
1291
- summary = oldSummary .appendValuePreserving ( newSummary )
1292
- )
1293
- }
1294
-
1295
- /**
1296
- * Holds if `base` is the base of a write to property `endProp`, and `nd` is reachable
1297
- * from `base` under configuration `cfg` (possibly through callees) along a path whose
1298
- * last step is summarized by `newSummary`, and the previous steps are summarized
1299
- * by `oldSummary`.
1300
- */
1301
- pragma [ noinline]
1302
- private predicate reachableFromStoreBaseStep (
1303
- string startProp , string endProp , DataFlow:: Node base , DataFlow:: Node nd ,
1304
- DataFlow:: Configuration cfg , PathSummary oldSummary , PathSummary newSummary ,
1305
- boolean onlyRelevantInCall
1306
- ) {
1307
- exists ( DataFlow:: Node mid |
1291
+ exists ( DataFlow:: Node mid , PathSummary oldSummary , PathSummary newSummary |
1308
1292
reachableFromStoreBase ( startProp , endProp , base , mid , cfg , oldSummary , onlyRelevantInCall ) and
1309
1293
flowStep ( mid , cfg , nd , newSummary ) and
1310
- onlyRelevantInCall .booleanAnd ( newSummary .hasReturn ( ) ) = false
1294
+ exists ( boolean hasReturn |
1295
+ hasReturn = newSummary .hasReturn ( ) and
1296
+ onlyRelevantInCall .booleanAnd ( hasReturn ) = false
1297
+ )
1311
1298
or
1312
1299
exists ( string midProp |
1313
1300
reachableFromStoreBase ( startProp , midProp , base , mid , cfg , oldSummary , onlyRelevantInCall ) and
1314
1301
isAdditionalLoadStoreStep ( mid , nd , midProp , endProp , cfg ) and
1315
1302
newSummary = PathSummary:: level ( )
1316
1303
)
1304
+ |
1305
+ summary = oldSummary .appendValuePreserving ( newSummary )
1317
1306
)
1318
1307
}
1319
1308
1309
+ private boolean hasCall ( PathSummary summary ) { result = summary .hasCall ( ) }
1310
+
1320
1311
/**
1321
1312
* Holds if the value of `pred` is written to a property of some base object, and that base
1322
1313
* object may flow into the base of property read `succ` under configuration `cfg` along
0 commit comments