@@ -1365,27 +1365,31 @@ private predicate loadStep(
1365
1365
1366
1366
/**
1367
1367
* Holds if there is flow to `base.startProp`, and `base.startProp` flows to `nd.endProp` under `cfg/summary`.
1368
+ *
1369
+ * If `onlyRelevantInCall` is true, the `base` object will not be propagated out of return edges, because
1370
+ * the flow that originally reached `base.startProp` used a call edge.
1368
1371
*/
1369
1372
pragma [ nomagic]
1370
1373
private predicate reachableFromStoreBase (
1371
1374
string startProp , string endProp , DataFlow:: Node base , DataFlow:: Node nd ,
1372
- DataFlow:: Configuration cfg , PathSummary summary
1375
+ DataFlow:: Configuration cfg , PathSummary summary , boolean onlyRelevantInCall
1373
1376
) {
1374
1377
exists ( PathSummary s1 , PathSummary s2 , DataFlow:: Node rhs |
1375
- reachableFromSource ( rhs , cfg , s1 )
1378
+ reachableFromSource ( rhs , cfg , s1 ) and
1379
+ onlyRelevantInCall = s1 .hasCall ( )
1376
1380
or
1377
- reachableFromStoreBase ( _, _, _, rhs , cfg , s1 )
1381
+ reachableFromStoreBase ( _, _, _, rhs , cfg , s1 , onlyRelevantInCall )
1378
1382
|
1379
1383
storeStep ( rhs , nd , startProp , cfg , s2 ) and
1380
1384
endProp = startProp and
1381
1385
base = nd and
1382
1386
summary =
1383
- MkPathSummary ( false , s1 .hasCall ( ) .booleanOr ( s2 .hasCall ( ) ) , DataFlow:: FlowLabel:: data ( ) ,
1384
- DataFlow:: FlowLabel:: data ( ) )
1387
+ MkPathSummary ( false , s2 .hasCall ( ) , DataFlow:: FlowLabel:: data ( ) , DataFlow:: FlowLabel:: data ( ) )
1385
1388
)
1386
1389
or
1387
1390
exists ( PathSummary newSummary , PathSummary oldSummary |
1388
- reachableFromStoreBaseStep ( startProp , endProp , base , nd , cfg , oldSummary , newSummary ) and
1391
+ reachableFromStoreBaseStep ( startProp , endProp , base , nd , cfg , oldSummary , newSummary ,
1392
+ onlyRelevantInCall ) and
1389
1393
summary = oldSummary .appendValuePreserving ( newSummary )
1390
1394
)
1391
1395
}
@@ -1399,14 +1403,16 @@ private predicate reachableFromStoreBase(
1399
1403
pragma [ noinline]
1400
1404
private predicate reachableFromStoreBaseStep (
1401
1405
string startProp , string endProp , DataFlow:: Node base , DataFlow:: Node nd ,
1402
- DataFlow:: Configuration cfg , PathSummary oldSummary , PathSummary newSummary
1406
+ DataFlow:: Configuration cfg , PathSummary oldSummary , PathSummary newSummary ,
1407
+ boolean onlyRelevantInCall
1403
1408
) {
1404
1409
exists ( DataFlow:: Node mid |
1405
- reachableFromStoreBase ( startProp , endProp , base , mid , cfg , oldSummary ) and
1406
- flowStep ( mid , cfg , nd , newSummary )
1410
+ reachableFromStoreBase ( startProp , endProp , base , mid , cfg , oldSummary , onlyRelevantInCall ) and
1411
+ flowStep ( mid , cfg , nd , newSummary ) and
1412
+ onlyRelevantInCall .booleanAnd ( newSummary .hasReturn ( ) ) = false
1407
1413
or
1408
1414
exists ( string midProp |
1409
- reachableFromStoreBase ( startProp , midProp , base , mid , cfg , oldSummary ) and
1415
+ reachableFromStoreBase ( startProp , midProp , base , mid , cfg , oldSummary , onlyRelevantInCall ) and
1410
1416
isAdditionalLoadStoreStep ( mid , nd , midProp , endProp , cfg ) and
1411
1417
newSummary = PathSummary:: level ( )
1412
1418
)
@@ -1446,7 +1452,7 @@ private predicate storeToLoad(
1446
1452
PathSummary s1 , PathSummary s2
1447
1453
|
1448
1454
storeStep ( pred , storeBase , storeProp , cfg , s1 ) and
1449
- reachableFromStoreBase ( storeProp , loadProp , storeBase , loadBase , cfg , s2 ) and
1455
+ reachableFromStoreBase ( storeProp , loadProp , storeBase , loadBase , cfg , s2 , _ ) and
1450
1456
oldSummary = s1 .appendValuePreserving ( s2 ) and
1451
1457
loadStep ( loadBase , succ , loadProp , cfg , newSummary )
1452
1458
)
0 commit comments