@@ -1021,6 +1021,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1021
1021
callEdgeReturn ( call , c , _, _, _, _, _)
1022
1022
}
1023
1023
1024
+ predicate storeMayReachRead ( NodeEx storeSource , Content c , NodeEx readTarget ) { none ( ) }
1025
+
1026
+ predicate providesStoreReadMatching ( ) { none ( ) }
1027
+
1024
1028
additional predicate stats (
1025
1029
boolean fwd , int nodes , int fields , int conscand , int states , int tuples , int calledges
1026
1030
) {
@@ -1320,6 +1324,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1320
1324
predicate relevantCallEdgeIn ( DataFlowCall call , DataFlowCallable c ) ;
1321
1325
1322
1326
predicate relevantCallEdgeOut ( DataFlowCall call , DataFlowCallable c ) ;
1327
+
1328
+ predicate storeMayReachRead ( NodeEx storeSource , Content c , NodeEx readTarget ) ;
1329
+
1330
+ default predicate providesStoreReadMatching ( ) { any ( ) }
1323
1331
}
1324
1332
1325
1333
private module MkStage< StageSig PrevStage> {
@@ -1425,8 +1433,6 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1425
1433
predicate typecheckStore ( Typ typ , DataFlowType contentType ) ;
1426
1434
1427
1435
default predicate enableTypeFlow ( ) { any ( ) }
1428
-
1429
- default predicate enableStoreReadMatching ( ) { any ( ) }
1430
1436
}
1431
1437
1432
1438
module Stage< StageParam Param> implements StageSig {
@@ -1457,43 +1463,49 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1457
1463
1458
1464
private class NodeExAlias = NodeEx ;
1459
1465
1466
+ final private class ApFinal = Ap ;
1467
+
1460
1468
private module StoreReadMatchingInput implements StoreReadMatchingInputSig {
1461
1469
class NodeEx = NodeExAlias ;
1462
1470
1463
- final private class ApApproxFinal = PrevStage:: Ap ;
1464
-
1465
- class Ap extends ApApproxFinal {
1466
- Content getHead ( ) { result = PrevStage:: getAHeadContent ( this ) }
1471
+ class Ap extends ApFinal {
1472
+ Content getHead ( ) { result = getAHeadContent ( this ) }
1467
1473
}
1468
1474
1469
- predicate revFlow ( NodeEx node , Ap ap ) {
1470
- enableStoreReadMatching ( ) and PrevStage:: revFlowAp ( node , ap )
1471
- }
1475
+ predicate nodeApRange ( NodeEx node , Ap ap ) { revFlowAp ( node , ap ) }
1472
1476
1473
- predicate localValueStep ( NodeEx node1 , NodeEx node2 ) { localValueStep ( node1 , node2 , _) }
1477
+ predicate localValueStep ( NodeEx node1 , NodeEx node2 ) {
1478
+ exists ( FlowState state , Ap ap , ApOption returnAp |
1479
+ revFlow ( node1 , pragma [ only_bind_into ] ( state ) , _, pragma [ only_bind_into ] ( returnAp ) ,
1480
+ pragma [ only_bind_into ] ( ap ) ) and
1481
+ revFlow ( node2 , pragma [ only_bind_into ] ( state ) , _, pragma [ only_bind_into ] ( returnAp ) ,
1482
+ pragma [ only_bind_into ] ( ap ) ) and
1483
+ localValueStep ( node1 , node2 , _)
1484
+ )
1485
+ }
1474
1486
1475
1487
predicate jumpValueStep ( NodeEx node1 , NodeEx node2 ) { jumpStepEx ( node1 , node2 ) }
1476
1488
1477
- predicate callEdgeArgParam ( NodeEx arg , NodeEx param , Ap ap ) {
1478
- PrevStage :: callEdgeArgParam ( _, _, arg , param , true , ap )
1489
+ predicate callEdgeArgParam ( NodeEx arg , NodeEx param ) {
1490
+ callEdgeArgParam ( _, _, arg , param , true , _ )
1479
1491
}
1480
1492
1481
- predicate callEdgeReturn ( NodeEx ret , NodeEx out , Ap ap ) {
1482
- PrevStage :: callEdgeReturn ( _, _, ret , _, out , true , ap )
1493
+ predicate callEdgeReturn ( NodeEx ret , NodeEx out ) {
1494
+ callEdgeReturn ( _, _, ret , _, out , true , _ )
1483
1495
}
1484
1496
1485
1497
predicate readContentStep ( NodeEx node1 , Content c , NodeEx node2 ) {
1486
- PrevStage :: readStepCand ( node1 , c , node2 )
1498
+ readStepCand0 ( node1 , c , node2 )
1487
1499
}
1488
1500
1489
1501
predicate storeContentStep ( NodeEx node1 , Content c , NodeEx node2 ) {
1490
- PrevStage :: storeStepCand ( node1 , _, c , node2 , _, _)
1502
+ storeStepCand0 ( node1 , _, c , node2 , _, _)
1491
1503
}
1492
1504
1493
1505
int accessPathConfigLimit ( ) { result = Config:: accessPathLimit ( ) }
1494
1506
}
1495
1507
1496
- private import StoreReadMatching< StoreReadMatchingInput >
1508
+ import StoreReadMatching< StoreReadMatchingInput >
1497
1509
1498
1510
/**
1499
1511
* Holds if `node` is reachable with access path `ap` from a source.
@@ -1529,7 +1541,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1529
1541
private predicate storeMayReachReadInlineLate (
1530
1542
NodeEx storeSource , Content c , NodeEx readTarget
1531
1543
) {
1532
- storeMayReachRead ( storeSource , c , readTarget )
1544
+ PrevStage :: storeMayReachRead ( storeSource , c , readTarget )
1533
1545
}
1534
1546
1535
1547
bindingset [ node1, state1]
@@ -1656,8 +1668,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1656
1668
fwdFlow ( node1 , state , cc , summaryCtx , argT , argAp , t1 , ap1 , apa1 ) and
1657
1669
PrevStage:: storeStepCand ( node1 , apa1 , c , node2 , contentType , containerType ) and
1658
1670
t2 = getTyp ( containerType ) and
1659
- typecheckStore ( t1 , contentType ) and
1660
- if enableStoreReadMatching ( ) then storeMayReachRead ( node1 , c , _) else any ( )
1671
+ typecheckStore ( t1 , contentType )
1661
1672
)
1662
1673
}
1663
1674
@@ -1666,13 +1677,14 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1666
1677
* store of `c` on a container of type `t2` resulting in access path
1667
1678
* `cons`. `storeSource` is a relevant store source.
1668
1679
*
1669
- * This predicate is only evaluated when `enableStoreReadMatching()` holds.
1680
+ * This predicate is only evaluated when `PrevStage::providesStoreReadMatching()`
1681
+ * holds.
1670
1682
*/
1671
1683
pragma [ nomagic]
1672
1684
private predicate fwdFlowConsCandStoreReadMatchingEnabled (
1673
1685
NodeEx storeSource , Typ t2 , Ap cons , Content c , Typ t1 , Ap tail
1674
1686
) {
1675
- enableStoreReadMatching ( ) and
1687
+ PrevStage :: providesStoreReadMatching ( ) and
1676
1688
fwdFlowStore ( storeSource , t1 , tail , c , t2 , _, _, _, _, _, _) and
1677
1689
cons = apCons ( c , t1 , tail )
1678
1690
or
@@ -1687,14 +1699,14 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1687
1699
* store of `c` on a container of type `t2` resulting in access path
1688
1700
* `cons`.
1689
1701
*
1690
- * This predicate is only evaluated when `enableStoreReadMatching ()`
1702
+ * This predicate is only evaluated when `PrevStage::providesStoreReadMatching ()`
1691
1703
* doesn't hold.
1692
1704
*/
1693
1705
pragma [ nomagic]
1694
1706
private predicate fwdFlowConsCandStoreReadMatchingDisabled (
1695
1707
Typ t2 , Ap cons , Content c , Typ t1 , Ap tail
1696
1708
) {
1697
- not enableStoreReadMatching ( ) and
1709
+ not PrevStage :: providesStoreReadMatching ( ) and
1698
1710
fwdFlowStore ( _, t1 , tail , c , t2 , _, _, _, _, _, _) and
1699
1711
cons = apCons ( c , t1 , tail )
1700
1712
or
@@ -1707,8 +1719,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1707
1719
pragma [ nomagic]
1708
1720
private predicate readStepCand ( NodeEx node1 , ApHeadContent apc , Content c , NodeEx node2 ) {
1709
1721
PrevStage:: readStepCand ( node1 , c , node2 ) and
1710
- apc = projectToHeadContent ( c ) and
1711
- if enableStoreReadMatching ( ) then storeMayReachRead ( _, c , node2 ) else any ( )
1722
+ apc = projectToHeadContent ( c )
1712
1723
}
1713
1724
1714
1725
bindingset [ node1, apc]
@@ -2360,7 +2371,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2360
2371
*/
2361
2372
pragma [ nomagic]
2362
2373
private predicate revFlowConsCandStoreReadMatchingDisabled ( Ap cons , Content c , Ap tail ) {
2363
- not enableStoreReadMatching ( ) and
2374
+ not PrevStage :: providesStoreReadMatching ( ) and
2364
2375
revFlowConsCand ( _, cons , c , tail )
2365
2376
}
2366
2377
@@ -2481,7 +2492,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2481
2492
}
2482
2493
2483
2494
pragma [ nomagic]
2484
- predicate storeStepCand (
2495
+ private predicate storeStepCand0 (
2485
2496
NodeEx node1 , Ap ap1 , Content c , NodeEx node2 , DataFlowType contentType ,
2486
2497
DataFlowType containerType
2487
2498
) {
@@ -2493,7 +2504,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2493
2504
}
2494
2505
2495
2506
pragma [ nomagic]
2496
- predicate readStepCand ( NodeEx node1 , Content c , NodeEx node2 ) {
2507
+ private predicate readStepCand0 ( NodeEx node1 , Content c , NodeEx node2 ) {
2497
2508
exists ( Ap ap1 , Ap ap2 |
2498
2509
revFlow ( node2 , _, _, _, pragma [ only_bind_into ] ( ap2 ) ) and
2499
2510
readStepFwd ( node1 , ap1 , c , node2 , ap2 ) and
@@ -2514,12 +2525,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2514
2525
private predicate fwdConsCand ( Content c , Typ t , Ap ap ) { storeStepFwd ( _, t , ap , c , _, _) }
2515
2526
2516
2527
private predicate revConsCand ( NodeEx readTarget , Content c , Typ t , Ap ap ) {
2517
- exists ( NodeEx storeSource , Ap ap2 |
2518
- revFlowStore ( ap2 , c , ap , t , storeSource , _, _, _, _) and
2519
- revFlowConsCand ( readTarget , ap2 , c , ap ) and
2520
- if enableStoreReadMatching ( )
2521
- then storeMayReachRead ( storeSource , c , readTarget )
2522
- else any ( )
2528
+ exists ( Ap ap2 |
2529
+ revFlowStore ( ap2 , c , ap , t , _, _, _, _, _) and
2530
+ revFlowConsCand ( readTarget , ap2 , c , ap )
2523
2531
)
2524
2532
}
2525
2533
@@ -2622,6 +2630,21 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2622
2630
callEdgeReturn ( call , c , _, _, _, _, _)
2623
2631
}
2624
2632
2633
+ pragma [ nomagic]
2634
+ predicate storeStepCand (
2635
+ NodeEx node1 , Ap ap1 , Content c , NodeEx node2 , DataFlowType contentType ,
2636
+ DataFlowType containerType
2637
+ ) {
2638
+ storeStepCand0 ( node1 , ap1 , c , node2 , contentType , containerType ) and
2639
+ storeMayReachRead ( node1 , c , _)
2640
+ }
2641
+
2642
+ pragma [ nomagic]
2643
+ predicate readStepCand ( NodeEx node1 , Content c , NodeEx node2 ) {
2644
+ readStepCand0 ( node1 , c , node2 ) and
2645
+ storeMayReachRead ( _, c , node2 )
2646
+ }
2647
+
2625
2648
additional predicate stats (
2626
2649
boolean fwd , int nodes , int fields , int conscand , int states , int tuples , int calledges ,
2627
2650
int tfnodes , int tftuples
@@ -2797,8 +2820,6 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2797
2820
predicate typecheckStore ( Typ typ , DataFlowType contentType ) { any ( ) }
2798
2821
2799
2822
predicate enableTypeFlow ( ) { none ( ) }
2800
-
2801
- predicate enableStoreReadMatching ( ) { none ( ) }
2802
2823
}
2803
2824
2804
2825
private module Stage2 = MkStage< Stage1 > :: Stage< Stage2Param > ;
@@ -3445,7 +3466,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
3445
3466
pragma [ nomagic]
3446
3467
predicate localValueStep ( NodeEx node1 , NodeEx node2 , LocalCc lcc ) {
3447
3468
exists ( FlowState state |
3448
- localFlowBigStep ( node1 , _, node2 , _, true , _, _ , _) and
3469
+ localFlowBigStep ( node1 , _, node2 , _, true , _, lcc , _) and
3449
3470
PrevStage:: revFlow ( node1 , pragma [ only_bind_into ] ( state ) , _) and
3450
3471
PrevStage:: revFlow ( node2 , pragma [ only_bind_into ] ( state ) , _) and
3451
3472
exists ( lcc )
@@ -3456,7 +3477,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
3456
3477
predicate localTaintStep (
3457
3478
NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , Typ t , LocalCc lcc
3458
3479
) {
3459
- localFlowBigStep ( node1 , state1 , node2 , state2 , false , t , _ , _) and
3480
+ localFlowBigStep ( node1 , state1 , node2 , state2 , false , t , lcc , _) and
3460
3481
PrevStage:: revFlow ( node1 , pragma [ only_bind_into ] ( state1 ) , _) and
3461
3482
PrevStage:: revFlow ( node2 , pragma [ only_bind_into ] ( state2 ) , _) and
3462
3483
exists ( lcc )
0 commit comments