@@ -1406,7 +1406,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1406
1406
bindingset [ node2, state2]
1407
1407
predicate localStep (
1408
1408
NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
1409
- Typ t , LocalCc lcc
1409
+ Typ t , LocalCc lcc , string label
1410
1410
) ;
1411
1411
1412
1412
bindingset [ node, state, t0, ap]
@@ -1524,10 +1524,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1524
1524
fwdFlow ( mid , state0 , cc , summaryCtx , argT , argAp , t0 , ap , apa ) and
1525
1525
localCc = getLocalCc ( cc )
1526
1526
|
1527
- localStep ( mid , state0 , node , state , true , _, localCc ) and
1527
+ localStep ( mid , state0 , node , state , true , _, localCc , _ ) and
1528
1528
t = t0
1529
1529
or
1530
- localStep ( mid , state0 , node , state , false , t , localCc ) and
1530
+ localStep ( mid , state0 , node , state , false , t , localCc , _ ) and
1531
1531
ap instanceof ApNil
1532
1532
)
1533
1533
or
@@ -2180,12 +2180,12 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2180
2180
ap instanceof ApNil
2181
2181
or
2182
2182
exists ( NodeEx mid , FlowState state0 |
2183
- localStep ( node , state , mid , state0 , true , _, _) and
2183
+ localStep ( node , state , mid , state0 , true , _, _, _ ) and
2184
2184
revFlow ( mid , state0 , returnCtx , returnAp , ap )
2185
2185
)
2186
2186
or
2187
2187
exists ( NodeEx mid , FlowState state0 |
2188
- localStep ( node , pragma [ only_bind_into ] ( state ) , mid , state0 , false , _, _) and
2188
+ localStep ( node , pragma [ only_bind_into ] ( state ) , mid , state0 , false , _, _, _ ) and
2189
2189
revFlow ( mid , state0 , returnCtx , returnAp , ap ) and
2190
2190
ap instanceof ApNil
2191
2191
)
@@ -2659,6 +2659,16 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2659
2659
result = TStagePathNodeMid ( node , state , cc , summaryCtx , argT , argAp , t , ap )
2660
2660
}
2661
2661
2662
+ private StagePathNode typeStrengthenToStagePathNode (
2663
+ NodeEx node , FlowState state , Cc cc , ParamNodeOption summaryCtx , TypOption argT ,
2664
+ ApOption argAp , Typ t0 , Ap ap
2665
+ ) {
2666
+ exists ( Typ t |
2667
+ fwdFlow1 ( node , state , cc , summaryCtx , argT , argAp , t0 , t , ap , _) and
2668
+ result = TStagePathNodeMid ( node , state , cc , summaryCtx , argT , argAp , t , ap )
2669
+ )
2670
+ }
2671
+
2662
2672
pragma [ nomagic]
2663
2673
private predicate fwdFlowThroughStep1 (
2664
2674
StagePathNode pn1 , StagePathNode pn2 , StagePathNode pn3 , DataFlowCall call , Cc cc ,
@@ -2696,21 +2706,74 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2696
2706
)
2697
2707
}
2698
2708
2699
- private predicate step (
2709
+ private predicate localStep (
2700
2710
StagePathNode pn1 , NodeEx node , FlowState state , Cc cc , ParamNodeOption summaryCtx ,
2701
- TypOption argT , ApOption argAp , Typ t , Ap ap
2711
+ TypOption argT , ApOption argAp , Typ t , Ap ap , string label
2702
2712
) {
2703
2713
exists ( NodeEx mid , FlowState state0 , Typ t0 , LocalCc localCc |
2704
2714
pn1 = TStagePathNodeMid ( mid , state0 , cc , summaryCtx , argT , argAp , t0 , ap ) and
2705
2715
localCc = getLocalCc ( cc )
2706
2716
|
2707
- localStep ( mid , state0 , node , state , true , _, localCc ) and
2717
+ localStep ( mid , state0 , node , state , true , _, localCc , label ) and
2708
2718
t = t0
2709
2719
or
2710
- localStep ( mid , state0 , node , state , false , t , localCc ) and
2720
+ localStep ( mid , state0 , node , state , false , t , localCc , label ) and
2711
2721
ap instanceof ApNil
2712
2722
)
2713
2723
or
2724
+ // store
2725
+ exists ( NodeEx mid , Content c , Typ t0 , Ap ap0 |
2726
+ pn1 = TStagePathNodeMid ( mid , state , cc , summaryCtx , argT , argAp , t0 , ap0 ) and
2727
+ fwdFlowStore ( mid , t0 , ap0 , c , t , node , state , cc , summaryCtx , argT , argAp ) and
2728
+ ap = apCons ( c , t0 , ap0 ) and
2729
+ label = ""
2730
+ )
2731
+ or
2732
+ // read
2733
+ exists ( NodeEx mid , Typ t0 , Ap ap0 , Content c |
2734
+ pn1 = TStagePathNodeMid ( mid , state , cc , summaryCtx , argT , argAp , t0 , ap0 ) and
2735
+ fwdFlowRead ( t0 , ap0 , c , mid , node , state , cc , summaryCtx , argT , argAp ) and
2736
+ fwdFlowConsCand ( t0 , ap0 , c , t , ap ) and
2737
+ label = ""
2738
+ )
2739
+ }
2740
+
2741
+ private predicate localStep ( StagePathNode pn1 , StagePathNode pn2 , string label ) {
2742
+ exists (
2743
+ NodeEx node , FlowState state , Cc cc , ParamNodeOption summaryCtx , TypOption argT ,
2744
+ ApOption argAp , Typ t0 , Ap ap
2745
+ |
2746
+ localStep ( pn1 , node , state , cc , summaryCtx , argT , argAp , t0 , ap , label ) and
2747
+ pn2 = typeStrengthenToStagePathNode ( node , state , cc , summaryCtx , argT , argAp , t0 , ap )
2748
+ )
2749
+ or
2750
+ summaryStep ( pn1 , pn2 , label )
2751
+ }
2752
+
2753
+ private predicate summaryLabel ( StagePathNode pn1 , StagePathNode pn2 , string summaryLabel ) {
2754
+ pn1 = pn2 and
2755
+ summaryLabel = "" and
2756
+ subpaths ( _, pn1 , _, _)
2757
+ or
2758
+ exists ( StagePathNode mid , string l1 , string l2 |
2759
+ summaryLabel ( pn1 , mid , l1 ) and
2760
+ localStep ( mid , pn2 , l2 ) and
2761
+ summaryLabel = mergeLabels ( l1 , l2 )
2762
+ )
2763
+ }
2764
+
2765
+ private predicate summaryStep ( StagePathNode arg , StagePathNode out , string label ) {
2766
+ exists ( StagePathNode par , StagePathNode ret |
2767
+ subpaths ( arg , par , ret , out ) and
2768
+ summaryLabel ( par , ret , label )
2769
+ )
2770
+ }
2771
+
2772
+ private predicate nonLocalStep (
2773
+ StagePathNode pn1 , NodeEx node , FlowState state , Cc cc , ParamNodeOption summaryCtx ,
2774
+ TypOption argT , ApOption argAp , Typ t , Ap ap , string label
2775
+ ) {
2776
+ // jump
2714
2777
exists ( NodeEx mid , FlowState state0 , Typ t0 |
2715
2778
pn1 = TStagePathNodeMid ( mid , state0 , _, _, _, _, t0 , ap ) and
2716
2779
cc = ccNone ( ) and
@@ -2720,30 +2783,18 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2720
2783
|
2721
2784
jumpStepEx ( mid , node ) and
2722
2785
state = state0 and
2723
- t = t0
2786
+ t = t0 and
2787
+ label = ""
2724
2788
or
2725
- additionalJumpStep ( mid , node , _ ) and
2789
+ additionalJumpStep ( mid , node , label ) and
2726
2790
state = state0 and
2727
2791
t = getNodeTyp ( node ) and
2728
2792
ap instanceof ApNil
2729
2793
or
2730
2794
additionalJumpStateStep ( mid , state0 , node , state ) and
2731
2795
t = getNodeTyp ( node ) and
2732
- ap instanceof ApNil
2733
- )
2734
- or
2735
- // store
2736
- exists ( NodeEx mid , Content c , Typ t0 , Ap ap0 |
2737
- pn1 = TStagePathNodeMid ( mid , state , cc , summaryCtx , argT , argAp , t0 , ap0 ) and
2738
- fwdFlowStore ( mid , t0 , ap0 , c , t , node , state , cc , summaryCtx , argT , argAp ) and
2739
- ap = apCons ( c , t0 , ap0 )
2740
- )
2741
- or
2742
- // read
2743
- exists ( NodeEx mid , Typ t0 , Ap ap0 , Content c |
2744
- pn1 = TStagePathNodeMid ( mid , state , cc , summaryCtx , argT , argAp , t0 , ap0 ) and
2745
- fwdFlowRead ( t0 , ap0 , c , mid , node , state , cc , summaryCtx , argT , argAp ) and
2746
- fwdFlowConsCand ( t0 , ap0 , c , t , ap )
2796
+ ap instanceof ApNil and
2797
+ label = "Config"
2747
2798
)
2748
2799
or
2749
2800
// flow into a callable
@@ -2755,6 +2806,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2755
2806
TStagePathNodeMid ( arg , state , outercc , outerSummaryCtx , outerArgT , outerArgAp , t , ap ) and
2756
2807
fwdFlowInStep ( arg , node , state , outercc , cc , outerSummaryCtx , outerArgT , outerArgAp ,
2757
2808
t , ap , allowsFlowThrough ) and
2809
+ label = "" and
2758
2810
if allowsFlowThrough = true
2759
2811
then (
2760
2812
summaryCtx = TParamNodeSome ( node .asNode ( ) ) and
@@ -2772,39 +2824,44 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2772
2824
pn1 = TStagePathNodeMid ( ret , state , innercc , summaryCtx , argT , argAp , t , ap ) and
2773
2825
fwdFlowIntoRet ( ret , state , innercc , summaryCtx , argT , argAp , t , ap , apa ) and
2774
2826
fwdFlowOutValidEdge ( _, ret , innercc , _, node , cc , apa , allowsFieldFlow ) and
2827
+ label = "" and
2775
2828
if allowsFieldFlow = false then ap instanceof ApNil else any ( )
2776
2829
)
2777
- or
2778
- // flow through a callable
2779
- fwdFlowThroughStep2 ( pn1 , _, _, node , cc , state , summaryCtx , argT , argAp , t , ap )
2830
+ }
2831
+
2832
+ private predicate nonLocalStep ( StagePathNode pn1 , StagePathNode pn2 , string label ) {
2833
+ exists (
2834
+ NodeEx node , FlowState state , Cc cc , ParamNodeOption summaryCtx , TypOption argT ,
2835
+ ApOption argAp , Typ t0 , Ap ap
2836
+ |
2837
+ nonLocalStep ( pn1 , node , state , cc , summaryCtx , argT , argAp , t0 , ap , label ) and
2838
+ pn2 = typeStrengthenToStagePathNode ( node , state , cc , summaryCtx , argT , argAp , t0 , ap )
2839
+ )
2780
2840
}
2781
2841
2782
2842
query predicate subpaths (
2783
2843
StagePathNode arg , StagePathNode par , StagePathNode ret , StagePathNode out
2784
2844
) {
2785
2845
exists (
2786
2846
NodeEx node , FlowState state , Cc cc , ParamNodeOption summaryCtx , TypOption argT ,
2787
- ApOption argAp , Typ t0 , Typ t , Ap ap
2847
+ ApOption argAp , Typ t0 , Ap ap
2788
2848
|
2789
2849
fwdFlowThroughStep2 ( arg , par , ret , node , cc , state , summaryCtx , argT , argAp , t0 , ap ) and
2790
- fwdFlow1 ( node , state , cc , summaryCtx , argT , argAp , t0 , t , ap , _) and
2791
- out = TStagePathNodeMid ( node , state , cc , summaryCtx , argT , argAp , t , ap )
2850
+ out = typeStrengthenToStagePathNode ( node , state , cc , summaryCtx , argT , argAp , t0 , ap )
2792
2851
)
2793
2852
}
2794
2853
2795
- query predicate edges ( StagePathNode pn1 , StagePathNode pn2 ) {
2796
- exists (
2797
- NodeEx node , FlowState state , Cc cc , ParamNodeOption summaryCtx , TypOption argT ,
2798
- ApOption argAp , Typ t0 , Typ t , Ap ap
2799
- |
2800
- step ( pn1 , node , state , cc , summaryCtx , argT , argAp , t0 , ap ) and
2801
- fwdFlow1 ( node , state , cc , summaryCtx , argT , argAp , t0 , t , ap , _) and
2802
- pn2 = TStagePathNodeMid ( node , state , cc , summaryCtx , argT , argAp , t , ap )
2854
+ query predicate edges ( StagePathNode pn1 , StagePathNode pn2 , string key , string val ) {
2855
+ key = "provenance" and
2856
+ (
2857
+ localStep ( pn1 , pn2 , val )
2858
+ or
2859
+ nonLocalStep ( pn1 , pn2 , val )
2860
+ or
2861
+ pn1 .isArbitrarySource ( ) and pn2 .isSource ( ) and val = ""
2862
+ or
2863
+ pn1 .isSink ( ) and pn2 .isArbitrarySink ( ) and val = ""
2803
2864
)
2804
- or
2805
- pn1 .isArbitrarySource ( ) and pn2 .isSource ( )
2806
- or
2807
- pn1 .isSink ( ) and pn2 .isArbitrarySink ( )
2808
2865
}
2809
2866
}
2810
2867
@@ -2938,19 +2995,20 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2938
2995
bindingset [ node2, state2]
2939
2996
predicate localStep (
2940
2997
NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
2941
- Typ t , LocalCc lcc
2998
+ Typ t , LocalCc lcc , string label
2942
2999
) {
2943
3000
(
2944
3001
preservesValue = true and
2945
- localFlowStepNodeCand1 ( node1 , node2 , _ ) and
3002
+ localFlowStepNodeCand1 ( node1 , node2 , label ) and
2946
3003
state1 = state2
2947
3004
or
2948
3005
preservesValue = false and
2949
- additionalLocalFlowStepNodeCand1 ( node1 , node2 , _ ) and
3006
+ additionalLocalFlowStepNodeCand1 ( node1 , node2 , label ) and
2950
3007
state1 = state2
2951
3008
or
2952
3009
preservesValue = false and
2953
- additionalLocalStateStep ( node1 , state1 , node2 , state2 )
3010
+ additionalLocalStateStep ( node1 , state1 , node2 , state2 ) and
3011
+ label = "Config"
2954
3012
) and
2955
3013
exists ( t ) and
2956
3014
exists ( lcc )
@@ -3224,9 +3282,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
3224
3282
3225
3283
predicate localStep (
3226
3284
NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
3227
- Typ t , LocalCc lcc
3285
+ Typ t , LocalCc lcc , string label
3228
3286
) {
3229
- localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , _, _, _ ) and
3287
+ localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , _, _, label ) and
3230
3288
exists ( t ) and
3231
3289
exists ( lcc )
3232
3290
}
@@ -3311,9 +3369,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
3311
3369
pragma [ nomagic]
3312
3370
predicate localStep (
3313
3371
NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
3314
- Typ t , LocalCc lcc
3372
+ Typ t , LocalCc lcc , string label
3315
3373
) {
3316
- localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , t , _, _ ) and
3374
+ localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , t , _, label ) and
3317
3375
PrevStage:: revFlow ( node1 , pragma [ only_bind_into ] ( state1 ) , _) and
3318
3376
PrevStage:: revFlow ( node2 , pragma [ only_bind_into ] ( state2 ) , _) and
3319
3377
exists ( lcc )
@@ -3613,9 +3671,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
3613
3671
3614
3672
predicate localStep (
3615
3673
NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
3616
- Typ t , LocalCc lcc
3674
+ Typ t , LocalCc lcc , string label
3617
3675
) {
3618
- localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , t , lcc , _ ) and
3676
+ localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , t , lcc , label ) and
3619
3677
PrevStage:: revFlow ( node1 , pragma [ only_bind_into ] ( state1 ) , _) and
3620
3678
PrevStage:: revFlow ( node2 , pragma [ only_bind_into ] ( state2 ) , _)
3621
3679
}
0 commit comments