@@ -1582,17 +1582,8 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1582
1582
)
1583
1583
or
1584
1584
// read
1585
- exists ( Typ t0 , Ap ap0 , Content c |
1586
- fwdFlowRead ( t0 , ap0 , c , _, node , state , cc , summaryCtx , argT , argAp ) and
1587
- apa = getApprox ( ap )
1588
- |
1589
- exists ( NodeEx storeSource |
1590
- fwdFlowConsCandStoreReadMatchingEnabled ( storeSource , t0 , ap0 , c , t , ap ) and
1591
- storeMayReachReadInlineLate ( storeSource , c , node )
1592
- )
1593
- or
1594
- fwdFlowConsCandStoreReadMatchingDisabled ( t0 , ap0 , c , t , ap )
1595
- )
1585
+ fwdFlowRead ( _, _, t , ap , _, _, node , state , cc , summaryCtx , argT , argAp ) and
1586
+ apa = getApprox ( ap )
1596
1587
or
1597
1588
// flow into a callable
1598
1589
exists ( boolean allowsFlowThrough |
@@ -1720,7 +1711,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1720
1711
}
1721
1712
1722
1713
pragma [ nomagic]
1723
- private predicate fwdFlowRead (
1714
+ private predicate fwdFlowRead0 (
1724
1715
Typ t , Ap ap , Content c , NodeEx node1 , NodeEx node2 , FlowState state , Cc cc ,
1725
1716
ParamNodeOption summaryCtx , TypOption argT , ApOption argAp
1726
1717
) {
@@ -1731,6 +1722,22 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1731
1722
)
1732
1723
}
1733
1724
1725
+ pragma [ inline]
1726
+ private predicate fwdFlowRead (
1727
+ Typ t1 , Ap ap1 , Typ t2 , Ap ap2 , Content c , NodeEx node1 , NodeEx node2 , FlowState state ,
1728
+ Cc cc , ParamNodeOption summaryCtx , TypOption argT , ApOption argAp
1729
+ ) {
1730
+ fwdFlowRead0 ( t1 , ap1 , c , node1 , node2 , state , cc , summaryCtx , argT , argAp ) and
1731
+ (
1732
+ exists ( NodeEx storeSource |
1733
+ fwdFlowConsCandStoreReadMatchingEnabled ( storeSource , t1 , ap1 , c , t2 , ap2 ) and
1734
+ storeMayReachReadInlineLate ( storeSource , c , node2 )
1735
+ )
1736
+ or
1737
+ fwdFlowConsCandStoreReadMatchingDisabled ( t1 , ap1 , c , t2 , ap2 )
1738
+ )
1739
+ }
1740
+
1734
1741
pragma [ nomagic]
1735
1742
private predicate fwdFlowIntoArg (
1736
1743
ArgNodeEx arg , FlowState state , Cc outercc , ParamNodeOption summaryCtx , TypOption argT ,
@@ -2151,14 +2158,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2151
2158
2152
2159
pragma [ nomagic]
2153
2160
private predicate readStepFwd ( NodeEx n1 , Ap ap1 , Content c , NodeEx n2 , Ap ap2 ) {
2154
- exists ( Typ t1 | fwdFlowRead ( t1 , ap1 , c , n1 , n2 , _, _, _, _, _) |
2155
- exists ( NodeEx storeSource |
2156
- fwdFlowConsCandStoreReadMatchingEnabled ( storeSource , t1 , ap1 , c , _, ap2 ) and
2157
- storeMayReachReadInlineLate ( storeSource , c , n2 )
2158
- )
2159
- or
2160
- fwdFlowConsCandStoreReadMatchingDisabled ( t1 , ap1 , c , _, ap2 )
2161
- )
2161
+ fwdFlowRead ( _, ap1 , _, ap2 , c , n1 , n2 , _, _, _, _, _)
2162
2162
}
2163
2163
2164
2164
pragma [ nomagic]
@@ -2275,7 +2275,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2275
2275
revFlowStore ( ap0 , c , ap , _, node , state , _, returnCtx , returnAp )
2276
2276
|
2277
2277
exists ( NodeEx readTarget |
2278
- revFlowConsCand ( readTarget , ap0 , c , ap ) and
2278
+ revFlowConsCandStoreReadMatchingEnabled ( readTarget , ap0 , c , ap ) and
2279
2279
storeMayReachReadInlineLate ( node , c , readTarget )
2280
2280
)
2281
2281
or
@@ -2340,11 +2340,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2340
2340
storeStepFwd ( node , t , ap , c , mid , ap0 )
2341
2341
}
2342
2342
2343
- /**
2344
- * Holds if reverse flow with access path `tail` reaches a read of `c`
2345
- * resulting in access path `cons`.
2346
- */
2347
- pragma [ nomagic]
2343
+ pragma [ inline]
2348
2344
private predicate revFlowConsCand ( NodeEx readTarget , Ap cons , Content c , Ap tail ) {
2349
2345
exists ( Ap tail0 |
2350
2346
revFlow ( readTarget , _, _, _, tail ) and
@@ -2356,6 +2352,23 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2356
2352
/**
2357
2353
* Holds if reverse flow with access path `tail` reaches a read of `c`
2358
2354
* resulting in access path `cons`.
2355
+ *
2356
+ * This predicate is only evaluated when `enableStoreReadMatching()` holds.
2357
+ */
2358
+ pragma [ nomagic]
2359
+ private predicate revFlowConsCandStoreReadMatchingEnabled (
2360
+ NodeEx readTarget , Ap cons , Content c , Ap tail
2361
+ ) {
2362
+ enableStoreReadMatching ( ) and
2363
+ revFlowConsCand ( readTarget , cons , c , tail )
2364
+ }
2365
+
2366
+ /**
2367
+ * Holds if reverse flow with access path `tail` reaches a read of `c`
2368
+ * resulting in access path `cons`.
2369
+ *
2370
+ * This predicate is only evaluated when `enableStoreReadMatching()`
2371
+ * doesn't hold.
2359
2372
*/
2360
2373
pragma [ nomagic]
2361
2374
private predicate revFlowConsCandStoreReadMatchingDisabled ( Ap cons , Content c , Ap tail ) {
@@ -2823,17 +2836,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2823
2836
)
2824
2837
or
2825
2838
// read
2826
- exists ( NodeEx mid , Typ t0 , Ap ap0 , Content c |
2839
+ exists ( NodeEx mid , Typ t0 , Ap ap0 |
2827
2840
pn1 = TStagePathNodeMid ( mid , state , cc , summaryCtx , argT , argAp , t0 , ap0 ) and
2828
- fwdFlowRead ( t0 , ap0 , c , mid , node , state , cc , summaryCtx , argT , argAp ) and
2841
+ fwdFlowRead ( t0 , ap0 , t , ap , _ , mid , node , state , cc , summaryCtx , argT , argAp ) and
2829
2842
label = ""
2830
- |
2831
- exists ( NodeEx storeSource |
2832
- fwdFlowConsCandStoreReadMatchingEnabled ( storeSource , t0 , ap0 , c , t , ap ) and
2833
- storeMayReachReadInlineLate ( storeSource , c , node )
2834
- )
2835
- or
2836
- fwdFlowConsCandStoreReadMatchingDisabled ( t0 , ap0 , c , t , ap )
2837
2843
)
2838
2844
}
2839
2845
@@ -3421,28 +3427,20 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
3421
3427
3422
3428
private class NodeExAlias = NodeEx ;
3423
3429
3424
- final private class ApaFinal = PrevStage:: Ap ;
3425
-
3426
3430
private module StoreReadMatchingInput implements StoreReadMatchingInputSig {
3427
3431
class NodeEx = NodeExAlias ;
3428
3432
3429
- class Ap extends ApaFinal {
3430
- Content getHead ( ) { this = true and exists ( result ) }
3431
- }
3432
-
3433
- predicate nodeApRange ( NodeEx node , Ap ap ) { PrevStage:: revFlowAp ( node , ap ) }
3434
-
3435
3433
predicate localValueStep ( NodeEx node1 , NodeEx node2 ) {
3436
- exists ( FlowState state , Ap ap , PrevStage:: ApOption returnAp |
3434
+ exists ( FlowState state , PrevStage:: ApOption returnAp |
3437
3435
PrevStage:: revFlow ( node1 , pragma [ only_bind_into ] ( state ) , _,
3438
- pragma [ only_bind_into ] ( returnAp ) , pragma [ only_bind_into ] ( ap ) ) and
3436
+ pragma [ only_bind_into ] ( returnAp ) , true ) and
3439
3437
PrevStage:: revFlow ( node2 , pragma [ only_bind_into ] ( state ) , _,
3440
- pragma [ only_bind_into ] ( returnAp ) , pragma [ only_bind_into ] ( ap ) ) and
3438
+ pragma [ only_bind_into ] ( returnAp ) , true ) and
3441
3439
Stage2Param:: localStep ( node1 , state , node2 , state , true , _, _, _)
3442
3440
)
3443
3441
}
3444
3442
3445
- predicate jumpValueStep ( NodeEx node1 , NodeEx node2 ) { jumpStepEx ( node1 , node2 ) }
3443
+ predicate jumpValueStep = jumpStepEx / 2 ;
3446
3444
3447
3445
predicate callEdgeArgParam ( NodeEx arg , NodeEx param ) {
3448
3446
PrevStage:: callEdgeArgParam ( _, _, arg , param , true , _)
@@ -3452,15 +3450,13 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
3452
3450
PrevStage:: callEdgeReturn ( _, _, ret , _, out , true , _)
3453
3451
}
3454
3452
3455
- predicate readContentStep ( NodeEx node1 , Content c , NodeEx node2 ) {
3456
- PrevStage:: readStepCand ( node1 , c , node2 )
3457
- }
3453
+ predicate readContentStep = PrevStage:: readStepCand / 3 ;
3458
3454
3459
3455
predicate storeContentStep ( NodeEx node1 , Content c , NodeEx node2 ) {
3460
3456
PrevStage:: storeStepCand ( node1 , _, c , node2 , _, _)
3461
3457
}
3462
3458
3463
- int accessPathConfigLimit ( ) { result = Config:: accessPathLimit ( ) }
3459
+ predicate accessPathConfigLimit = Config:: accessPathLimit / 0 ;
3464
3460
}
3465
3461
3466
3462
predicate storeMayReachRead = StoreReadMatching< StoreReadMatchingInput > :: storeMayReachRead / 3 ;
0 commit comments