@@ -1719,7 +1719,8 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1719
1719
Typ t1 , Ap ap1 , Typ t2 , Ap ap2 , Content c , NodeEx node1 , NodeEx node2 , FlowState state ,
1720
1720
Cc cc , ParamNodeOption summaryCtx , TypOption argT , ApOption argAp
1721
1721
) {
1722
- fwdFlowRead0 ( t1 , ap1 , c , node1 , node2 , state , cc , summaryCtx , argT , argAp ) and
1722
+ fwdFlowRead0 ( pragma [ only_bind_into ] ( t1 ) , pragma [ only_bind_into ] ( ap1 ) ,
1723
+ pragma [ only_bind_into ] ( c ) , node1 , node2 , state , cc , summaryCtx , argT , argAp ) and
1723
1724
(
1724
1725
exists ( NodeEx storeSource |
1725
1726
fwdFlowConsCandStoreReadMatchingEnabled ( storeSource , t1 , ap1 , c , t2 , ap2 ) and
@@ -2646,7 +2647,16 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2646
2647
abstract Location getLocation ( ) ;
2647
2648
2648
2649
/** Gets the corresponding `Node`, if any. */
2649
- Node getNode ( ) { none ( ) }
2650
+ NodeEx getNodeEx ( ) { none ( ) }
2651
+
2652
+ /** Gets the summary context. */
2653
+ ParamNodeOption getSummaryCtx ( ) { none ( ) }
2654
+
2655
+ /** Gets the access path. */
2656
+ Ap getAp ( ) { none ( ) }
2657
+
2658
+ /** Gets the corresponding `Node`, if any. */
2659
+ final Node getNode ( ) { result = this .getNodeEx ( ) .asNode ( ) }
2650
2660
2651
2661
predicate isSource ( ) { none ( ) }
2652
2662
@@ -2690,7 +2700,11 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2690
2700
2691
2701
override Location getLocation ( ) { result = node .getLocation ( ) }
2692
2702
2693
- override Node getNode ( ) { result = node .asNode ( ) }
2703
+ override NodeEx getNodeEx ( ) { result = node }
2704
+
2705
+ override ParamNodeOption getSummaryCtx ( ) { result = summaryCtx }
2706
+
2707
+ override Ap getAp ( ) { result = ap }
2694
2708
2695
2709
override predicate isSource ( ) {
2696
2710
sourceNode ( node , state ) and
@@ -2728,8 +2742,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2728
2742
ParamNodeOption summaryCtx , TypOption argT , ApOption argAp , Typ t , Ap ap ,
2729
2743
boolean allowsFlowThrough
2730
2744
) {
2731
- exists ( ApApprox apa , boolean allowsFlowThrough0 |
2732
- FwdFlowIn< FwdFlowInNoRestriction > :: fwdFlowIn ( _, arg , _, p , state , outercc , innercc ,
2745
+ exists ( DataFlowCall call , ApApprox apa , boolean allowsFlowThrough0 |
2746
+ callEdgeArgParam ( call , _, arg , p , _, ap ) and
2747
+ FwdFlowIn< FwdFlowInNoRestriction > :: fwdFlowIn ( call , arg , _, p , state , outercc , innercc ,
2733
2748
summaryCtx , argT , argAp , t , ap , apa , _, allowsFlowThrough0 ) and
2734
2749
if PrevStage:: parameterMayFlowThrough ( p , apa )
2735
2750
then allowsFlowThrough = allowsFlowThrough0
@@ -2744,6 +2759,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2744
2759
RetNodeEx ret , ParamNodeEx innerSummaryCtx , Typ innerArgT , Ap innerArgAp ,
2745
2760
ApApprox innerArgApa
2746
2761
) {
2762
+ callEdgeReturn ( call , _, ret , _, _, _, ap ) and
2763
+ callMayFlowThroughRev ( call ) and
2764
+ returnMayFlowThrough ( ret , _, _, _) and
2765
+ matchesCall ( ccc , call ) and
2747
2766
fwdFlowThrough0 ( call , arg , cc , state , ccc , summaryCtx , argT , argAp , t , ap , apa , ret ,
2748
2767
innerSummaryCtx , innerArgT , innerArgAp , innerArgApa )
2749
2768
}
@@ -2797,6 +2816,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2797
2816
DataFlowCall call , CcCall ccc , RetNodeEx ret , boolean allowsFieldFlow ,
2798
2817
ApApprox innerArgApa , ApApprox apa
2799
2818
|
2819
+ callEdgeReturn ( call , _, ret , _, node , allowsFieldFlow , ap ) and
2800
2820
fwdFlowThroughStep1 ( pn1 , pn2 , pn3 , call , cc , state , ccc , summaryCtx , argT , argAp , t ,
2801
2821
ap , apa , ret , innerArgApa ) and
2802
2822
flowThroughOutOfCall ( call , ccc , ret , node , allowsFieldFlow , innerArgApa , apa ) and
@@ -2818,31 +2838,70 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2818
2838
localStep ( mid , state0 , node , state , false , t , localCc , label ) and
2819
2839
ap instanceof ApNil
2820
2840
)
2821
- or
2822
- // store
2823
- exists ( NodeEx mid , Content c , Typ t0 , Ap ap0 |
2841
+ }
2842
+
2843
+ private predicate storeStep (
2844
+ StagePathNode pn1 , Content c , NodeEx node , FlowState state , Cc cc ,
2845
+ ParamNodeOption summaryCtx , TypOption argT , ApOption argAp , Typ t , Ap ap , string label
2846
+ ) {
2847
+ exists ( NodeEx mid , Typ t0 , Ap ap0 |
2824
2848
pn1 = TStagePathNodeMid ( mid , state , cc , summaryCtx , argT , argAp , t0 , ap0 ) and
2825
2849
fwdFlowStore ( mid , t0 , ap0 , c , t , node , state , cc , summaryCtx , argT , argAp ) and
2850
+ storeStepCand ( mid , ap0 , c , node , _,
2851
+ any ( DataFlowType containerType | t = getTyp ( containerType ) ) ) and
2826
2852
ap = apCons ( c , t0 , ap0 ) and
2827
2853
label = ""
2828
2854
)
2829
- or
2830
- // read
2855
+ }
2856
+
2857
+ private predicate readStep (
2858
+ StagePathNode pn1 , Content c , NodeEx node , FlowState state , Cc cc ,
2859
+ ParamNodeOption summaryCtx , TypOption argT , ApOption argAp , Typ t , Ap ap , string label
2860
+ ) {
2831
2861
exists ( NodeEx mid , Typ t0 , Ap ap0 |
2832
2862
pn1 = TStagePathNodeMid ( mid , state , cc , summaryCtx , argT , argAp , t0 , ap0 ) and
2833
- fwdFlowRead ( t0 , ap0 , t , ap , _, mid , node , state , cc , summaryCtx , argT , argAp ) and
2863
+ fwdFlowRead ( t0 , ap0 , t , ap , c , mid , node , state , cc , summaryCtx , argT , argAp ) and
2864
+ readStepCand ( mid , c , node ) and
2834
2865
label = ""
2835
2866
)
2836
2867
}
2837
2868
2838
- private predicate localStep ( StagePathNode pn1 , StagePathNode pn2 , string label ) {
2869
+ predicate localStep ( StagePathNode pn1 , StagePathNode pn2 , string label ) {
2839
2870
exists (
2840
2871
NodeEx node , FlowState state , Cc cc , ParamNodeOption summaryCtx , TypOption argT ,
2841
2872
ApOption argAp , Typ t0 , Ap ap
2842
2873
|
2843
2874
localStep ( pn1 , node , state , cc , summaryCtx , argT , argAp , t0 , ap , label ) and
2844
2875
pn2 = typeStrengthenToStagePathNode ( node , state , cc , summaryCtx , argT , argAp , t0 , ap )
2845
2876
)
2877
+ }
2878
+
2879
+ predicate storeStep ( StagePathNode pn1 , Content c , StagePathNode pn2 , string label ) {
2880
+ exists (
2881
+ NodeEx node , FlowState state , Cc cc , ParamNodeOption summaryCtx , TypOption argT ,
2882
+ ApOption argAp , Typ t0 , Ap ap
2883
+ |
2884
+ storeStep ( pn1 , c , node , state , cc , summaryCtx , argT , argAp , t0 , ap , label ) and
2885
+ pn2 = typeStrengthenToStagePathNode ( node , state , cc , summaryCtx , argT , argAp , t0 , ap )
2886
+ )
2887
+ }
2888
+
2889
+ predicate readStep ( StagePathNode pn1 , Content c , StagePathNode pn2 , string label ) {
2890
+ exists (
2891
+ NodeEx node , FlowState state , Cc cc , ParamNodeOption summaryCtx , TypOption argT ,
2892
+ ApOption argAp , Typ t0 , Ap ap
2893
+ |
2894
+ readStep ( pn1 , c , node , state , cc , summaryCtx , argT , argAp , t0 , ap , label ) and
2895
+ pn2 = typeStrengthenToStagePathNode ( node , state , cc , summaryCtx , argT , argAp , t0 , ap )
2896
+ )
2897
+ }
2898
+
2899
+ private predicate localScopeStep ( StagePathNode pn1 , StagePathNode pn2 , string label ) {
2900
+ localStep ( pn1 , pn2 , label )
2901
+ or
2902
+ storeStep ( pn1 , _, pn2 , label )
2903
+ or
2904
+ readStep ( pn1 , _, pn2 , label )
2846
2905
or
2847
2906
summaryStep ( pn1 , pn2 , label )
2848
2907
}
@@ -2854,7 +2913,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2854
2913
or
2855
2914
exists ( StagePathNode mid , string l1 , string l2 |
2856
2915
summaryLabel ( pn1 , mid , l1 ) and
2857
- localStep ( mid , pn2 , l2 ) and
2916
+ localScopeStep ( mid , pn2 , l2 ) and
2858
2917
summaryLabel = mergeLabels ( l1 , l2 )
2859
2918
)
2860
2919
}
@@ -2917,16 +2976,20 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2917
2976
)
2918
2977
or
2919
2978
// flow out of a callable
2920
- exists ( RetNodeEx ret , CcNoCall innercc , boolean allowsFieldFlow , ApApprox apa |
2979
+ exists (
2980
+ DataFlowCall call , RetNodeEx ret , CcNoCall innercc , boolean allowsFieldFlow ,
2981
+ ApApprox apa
2982
+ |
2921
2983
pn1 = TStagePathNodeMid ( ret , state , innercc , summaryCtx , argT , argAp , t , ap ) and
2922
2984
fwdFlowIntoRet ( ret , state , innercc , summaryCtx , argT , argAp , t , ap , apa ) and
2923
2985
fwdFlowOutValidEdge ( _, ret , innercc , _, node , cc , apa , allowsFieldFlow ) and
2986
+ callEdgeReturn ( call , _, ret , _, node , allowsFieldFlow , ap ) and
2924
2987
label = "" and
2925
2988
if allowsFieldFlow = false then ap instanceof ApNil else any ( )
2926
2989
)
2927
2990
}
2928
2991
2929
- private predicate nonLocalStep ( StagePathNode pn1 , StagePathNode pn2 , string label ) {
2992
+ predicate nonLocalStep ( StagePathNode pn1 , StagePathNode pn2 , string label ) {
2930
2993
exists (
2931
2994
NodeEx node , FlowState state , Cc cc , ParamNodeOption summaryCtx , TypOption argT ,
2932
2995
ApOption argAp , Typ t0 , Ap ap
@@ -2951,7 +3014,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2951
3014
query predicate edges ( StagePathNode pn1 , StagePathNode pn2 , string key , string val ) {
2952
3015
key = "provenance" and
2953
3016
(
2954
- localStep ( pn1 , pn2 , val )
3017
+ localScopeStep ( pn1 , pn2 , val )
2955
3018
or
2956
3019
nonLocalStep ( pn1 , pn2 , val )
2957
3020
or
@@ -3417,73 +3480,49 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
3417
3480
3418
3481
predicate enableStoreReadMatching ( ) { any ( ) }
3419
3482
3420
- private class NodeExAlias = NodeEx ;
3483
+ final private class NodeExAlias = NodeEx ;
3484
+
3485
+ final private class ArgNodeExAlias = ArgNodeEx ;
3486
+
3487
+ final private class ParamNodeExAlias = ParamNodeEx ;
3421
3488
3422
3489
private module StoreReadMatchingInput implements StoreReadMatchingInputSig {
3423
3490
class NodeEx = NodeExAlias ;
3424
3491
3425
- predicate nodeRange ( NodeEx node , boolean fromArg ) {
3426
- exists ( PrevStage:: Ap ap |
3427
- PrevStage:: revFlowAp ( node , ap ) and
3428
- (
3429
- ap = true
3430
- or
3431
- PrevStage:: storeStepCand ( node , ap , _, _, _, _)
3432
- or
3433
- PrevStage:: readStepCand ( _, _, node )
3434
- )
3435
- |
3436
- exists ( PrevStage:: Cc cc | PrevStage:: fwdFlow ( node , _, cc , _, _, _, _, ap , _) |
3437
- PrevStage:: instanceofCcCall ( cc ) and
3438
- fromArg = true
3439
- or
3440
- PrevStage:: instanceofCcNoCall ( cc ) and
3441
- fromArg = false
3442
- )
3443
- )
3444
- }
3492
+ class ArgNodeEx = ArgNodeExAlias ;
3445
3493
3446
- predicate localValueStep ( NodeEx node1 , NodeEx node2 ) {
3447
- exists ( FlowState state , PrevStage:: ApOption returnAp |
3448
- PrevStage:: revFlow ( node1 , pragma [ only_bind_into ] ( state ) , _,
3449
- pragma [ only_bind_into ] ( returnAp ) , true ) and
3450
- PrevStage:: revFlow ( node2 , pragma [ only_bind_into ] ( state ) , _,
3451
- pragma [ only_bind_into ] ( returnAp ) , true ) and
3452
- Stage2Param:: localStep ( node1 , state , node2 , state , true , _, _, _)
3453
- )
3454
- }
3494
+ class ParamNodeEx = ParamNodeExAlias ;
3455
3495
3456
- predicate jumpValueStep = jumpStepEx / 2 ;
3496
+ class PathNode = PrevStage :: Graph :: StagePathNode ;
3457
3497
3458
- pragma [ nomagic]
3459
- private predicate flowThroughOutOfCall ( RetNodeEx ret , NodeEx out ) {
3460
- exists ( DataFlowCall call , CcCall ccc , ReturnKindExt kind |
3461
- PrevStage:: callEdgeReturn ( call , _, ret , kind , out , true , true ) and
3462
- PrevStage:: callMayFlowThroughRev ( call ) and
3463
- PrevStage:: returnMayFlowThrough ( ret , _, true , kind ) and
3464
- matchesCall ( ccc , call )
3465
- )
3498
+ predicate localStep ( PathNode node1 , PathNode node2 ) {
3499
+ PrevStage:: Graph:: localStep ( node1 , node2 , _)
3466
3500
}
3467
3501
3468
- predicate callEdgeArgParam ( NodeEx arg , NodeEx param ) {
3469
- PrevStage:: callEdgeArgParam ( _ , _ , arg , param , true , true )
3502
+ predicate nonLocalStep ( PathNode node1 , PathNode node2 ) {
3503
+ PrevStage:: Graph :: nonLocalStep ( node1 , node2 , _ )
3470
3504
}
3471
3505
3472
- predicate callEdgeReturn ( NodeEx ret , NodeEx out , boolean mayFlowThrough ) {
3473
- PrevStage:: callEdgeReturn ( _, _, ret , _, out , true , true ) and
3474
- if flowThroughOutOfCall ( ret , out ) then mayFlowThrough = true else mayFlowThrough = false
3475
- }
3506
+ predicate subpaths = PrevStage:: Graph:: subpaths / 4 ;
3476
3507
3477
- predicate readContentStep = PrevStage:: readStepCand / 3 ;
3508
+ predicate readContentStep ( PathNode node1 , Content c , PathNode node2 ) {
3509
+ PrevStage:: Graph:: readStep ( node1 , c , node2 , _)
3510
+ }
3478
3511
3479
- predicate storeContentStep ( NodeEx node1 , Content c , NodeEx node2 ) {
3480
- PrevStage:: storeStepCand ( node1 , _ , c , node2 , _ , _)
3512
+ predicate storeContentStep ( PathNode node1 , Content c , PathNode node2 ) {
3513
+ PrevStage:: Graph :: storeStep ( node1 , c , node2 , _)
3481
3514
}
3482
3515
3483
3516
predicate accessPathConfigLimit = Config:: accessPathLimit / 0 ;
3484
3517
}
3485
3518
3486
- predicate storeMayReachRead = StoreReadMatching< StoreReadMatchingInput > :: storeMayReachRead / 3 ;
3519
+ predicate storeMayReachRead ( NodeEx storeSource , Content c , NodeEx readTarget ) {
3520
+ exists ( StoreReadMatchingInput:: PathNode pn1 , StoreReadMatchingInput:: PathNode pn2 |
3521
+ StoreReadMatching< StoreReadMatchingInput > :: storeMayReachRead ( pn1 , c , pn2 ) and
3522
+ storeSource = pn1 .getNodeEx ( ) and
3523
+ readTarget = pn2 .getNodeEx ( )
3524
+ )
3525
+ }
3487
3526
}
3488
3527
3489
3528
private module Stage3 = MkStage< Stage2 > :: Stage< Stage3Param > ;
0 commit comments