@@ -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
@@ -2174,12 +2174,12 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2174
2174
ap instanceof ApNil
2175
2175
or
2176
2176
exists ( NodeEx mid , FlowState state0 |
2177
- localStep ( node , state , mid , state0 , true , _, _) and
2177
+ localStep ( node , state , mid , state0 , true , _, _, _ ) and
2178
2178
revFlow ( mid , state0 , returnCtx , returnAp , ap )
2179
2179
)
2180
2180
or
2181
2181
exists ( NodeEx mid , FlowState state0 |
2182
- localStep ( node , pragma [ only_bind_into ] ( state ) , mid , state0 , false , _, _) and
2182
+ localStep ( node , pragma [ only_bind_into ] ( state ) , mid , state0 , false , _, _, _ ) and
2183
2183
revFlow ( mid , state0 , returnCtx , returnAp , ap ) and
2184
2184
ap instanceof ApNil
2185
2185
)
@@ -2638,6 +2638,16 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2638
2638
result = TStagePathNodeMid ( node , state , cc , summaryCtx , argT , argAp , t , ap )
2639
2639
}
2640
2640
2641
+ private StagePathNode typeStrengthenToStagePathNode (
2642
+ NodeEx node , FlowState state , Cc cc , ParamNodeOption summaryCtx , TypOption argT ,
2643
+ ApOption argAp , Typ t0 , Ap ap
2644
+ ) {
2645
+ exists ( Typ t |
2646
+ fwdFlow1 ( node , state , cc , summaryCtx , argT , argAp , t0 , t , ap , _) and
2647
+ result = TStagePathNodeMid ( node , state , cc , summaryCtx , argT , argAp , t , ap )
2648
+ )
2649
+ }
2650
+
2641
2651
pragma [ nomagic]
2642
2652
private predicate fwdFlowThroughStep1 (
2643
2653
StagePathNode pn1 , StagePathNode pn2 , StagePathNode pn3 , DataFlowCall call , Cc cc ,
@@ -2675,21 +2685,74 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2675
2685
)
2676
2686
}
2677
2687
2678
- private predicate step (
2688
+ private predicate localStep (
2679
2689
StagePathNode pn1 , NodeEx node , FlowState state , Cc cc , ParamNodeOption summaryCtx ,
2680
- TypOption argT , ApOption argAp , Typ t , Ap ap
2690
+ TypOption argT , ApOption argAp , Typ t , Ap ap , string label
2681
2691
) {
2682
2692
exists ( NodeEx mid , FlowState state0 , Typ t0 , LocalCc localCc |
2683
2693
pn1 = TStagePathNodeMid ( mid , state0 , cc , summaryCtx , argT , argAp , t0 , ap ) and
2684
2694
localCc = getLocalCc ( cc )
2685
2695
|
2686
- localStep ( mid , state0 , node , state , true , _, localCc ) and
2696
+ localStep ( mid , state0 , node , state , true , _, localCc , label ) and
2687
2697
t = t0
2688
2698
or
2689
- localStep ( mid , state0 , node , state , false , t , localCc ) and
2699
+ localStep ( mid , state0 , node , state , false , t , localCc , label ) and
2690
2700
ap instanceof ApNil
2691
2701
)
2692
2702
or
2703
+ // store
2704
+ exists ( NodeEx mid , Content c , Typ t0 , Ap ap0 |
2705
+ pn1 = TStagePathNodeMid ( mid , state , cc , summaryCtx , argT , argAp , t0 , ap0 ) and
2706
+ fwdFlowStore ( mid , t0 , ap0 , c , t , node , state , cc , summaryCtx , argT , argAp ) and
2707
+ ap = apCons ( c , t0 , ap0 ) and
2708
+ label = ""
2709
+ )
2710
+ or
2711
+ // read
2712
+ exists ( NodeEx mid , Typ t0 , Ap ap0 , Content c |
2713
+ pn1 = TStagePathNodeMid ( mid , state , cc , summaryCtx , argT , argAp , t0 , ap0 ) and
2714
+ fwdFlowRead ( t0 , ap0 , c , mid , node , state , cc , summaryCtx , argT , argAp ) and
2715
+ fwdFlowConsCand ( t0 , ap0 , c , t , ap ) and
2716
+ label = ""
2717
+ )
2718
+ }
2719
+
2720
+ private predicate localStep ( StagePathNode pn1 , StagePathNode pn2 , string label ) {
2721
+ exists (
2722
+ NodeEx node , FlowState state , Cc cc , ParamNodeOption summaryCtx , TypOption argT ,
2723
+ ApOption argAp , Typ t0 , Ap ap
2724
+ |
2725
+ localStep ( pn1 , node , state , cc , summaryCtx , argT , argAp , t0 , ap , label ) and
2726
+ pn2 = typeStrengthenToStagePathNode ( node , state , cc , summaryCtx , argT , argAp , t0 , ap )
2727
+ )
2728
+ or
2729
+ summaryStep ( pn1 , pn2 , label )
2730
+ }
2731
+
2732
+ private predicate summaryLabel ( StagePathNode pn1 , StagePathNode pn2 , string summaryLabel ) {
2733
+ pn1 = pn2 and
2734
+ summaryLabel = "" and
2735
+ subpaths ( _, pn1 , _, _)
2736
+ or
2737
+ exists ( StagePathNode mid , string l1 , string l2 |
2738
+ summaryLabel ( pn1 , mid , l1 ) and
2739
+ localStep ( mid , pn2 , l2 ) and
2740
+ summaryLabel = mergeLabels ( l1 , l2 )
2741
+ )
2742
+ }
2743
+
2744
+ private predicate summaryStep ( StagePathNode arg , StagePathNode out , string label ) {
2745
+ exists ( StagePathNode par , StagePathNode ret |
2746
+ subpaths ( arg , par , ret , out ) and
2747
+ summaryLabel ( par , ret , label )
2748
+ )
2749
+ }
2750
+
2751
+ private predicate nonLocalStep (
2752
+ StagePathNode pn1 , NodeEx node , FlowState state , Cc cc , ParamNodeOption summaryCtx ,
2753
+ TypOption argT , ApOption argAp , Typ t , Ap ap , string label
2754
+ ) {
2755
+ // jump
2693
2756
exists ( NodeEx mid , FlowState state0 , Typ t0 |
2694
2757
pn1 = TStagePathNodeMid ( mid , state0 , _, _, _, _, t0 , ap ) and
2695
2758
cc = ccNone ( ) and
@@ -2699,30 +2762,18 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2699
2762
|
2700
2763
jumpStepEx ( mid , node ) and
2701
2764
state = state0 and
2702
- t = t0
2765
+ t = t0 and
2766
+ label = ""
2703
2767
or
2704
- additionalJumpStep ( mid , node , _ ) and
2768
+ additionalJumpStep ( mid , node , label ) and
2705
2769
state = state0 and
2706
2770
t = getNodeTyp ( node ) and
2707
2771
ap instanceof ApNil
2708
2772
or
2709
2773
additionalJumpStateStep ( mid , state0 , node , state ) and
2710
2774
t = getNodeTyp ( node ) and
2711
- ap instanceof ApNil
2712
- )
2713
- or
2714
- // store
2715
- exists ( NodeEx mid , Content c , Typ t0 , Ap ap0 |
2716
- pn1 = TStagePathNodeMid ( mid , state , cc , summaryCtx , argT , argAp , t0 , ap0 ) and
2717
- fwdFlowStore ( mid , t0 , ap0 , c , t , node , state , cc , summaryCtx , argT , argAp ) and
2718
- ap = apCons ( c , t0 , ap0 )
2719
- )
2720
- or
2721
- // read
2722
- exists ( NodeEx mid , Typ t0 , Ap ap0 , Content c |
2723
- pn1 = TStagePathNodeMid ( mid , state , cc , summaryCtx , argT , argAp , t0 , ap0 ) and
2724
- fwdFlowRead ( t0 , ap0 , c , mid , node , state , cc , summaryCtx , argT , argAp ) and
2725
- fwdFlowConsCand ( t0 , ap0 , c , t , ap )
2775
+ ap instanceof ApNil and
2776
+ label = "Config"
2726
2777
)
2727
2778
or
2728
2779
// flow into a callable
@@ -2734,6 +2785,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2734
2785
TStagePathNodeMid ( arg , state , outercc , outerSummaryCtx , outerArgT , outerArgAp , t , ap ) and
2735
2786
fwdFlowInStep ( arg , node , state , outercc , cc , outerSummaryCtx , outerArgT , outerArgAp ,
2736
2787
t , ap , allowsFlowThrough ) and
2788
+ label = "" and
2737
2789
if allowsFlowThrough = true
2738
2790
then (
2739
2791
summaryCtx = TParamNodeSome ( node .asNode ( ) ) and
@@ -2751,39 +2803,44 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2751
2803
pn1 = TStagePathNodeMid ( ret , state , innercc , summaryCtx , argT , argAp , t , ap ) and
2752
2804
fwdFlowIntoRet ( ret , state , innercc , summaryCtx , argT , argAp , t , ap , apa ) and
2753
2805
fwdFlowOutValidEdge ( _, ret , innercc , _, node , cc , apa , allowsFieldFlow ) and
2806
+ label = "" and
2754
2807
if allowsFieldFlow = false then ap instanceof ApNil else any ( )
2755
2808
)
2756
- or
2757
- // flow through a callable
2758
- fwdFlowThroughStep2 ( pn1 , _, _, node , cc , state , summaryCtx , argT , argAp , t , ap )
2809
+ }
2810
+
2811
+ private predicate nonLocalStep ( StagePathNode pn1 , StagePathNode pn2 , string label ) {
2812
+ exists (
2813
+ NodeEx node , FlowState state , Cc cc , ParamNodeOption summaryCtx , TypOption argT ,
2814
+ ApOption argAp , Typ t0 , Ap ap
2815
+ |
2816
+ nonLocalStep ( pn1 , node , state , cc , summaryCtx , argT , argAp , t0 , ap , label ) and
2817
+ pn2 = typeStrengthenToStagePathNode ( node , state , cc , summaryCtx , argT , argAp , t0 , ap )
2818
+ )
2759
2819
}
2760
2820
2761
2821
query predicate subpaths (
2762
2822
StagePathNode arg , StagePathNode par , StagePathNode ret , StagePathNode out
2763
2823
) {
2764
2824
exists (
2765
2825
NodeEx node , FlowState state , Cc cc , ParamNodeOption summaryCtx , TypOption argT ,
2766
- ApOption argAp , Typ t0 , Typ t , Ap ap
2826
+ ApOption argAp , Typ t0 , Ap ap
2767
2827
|
2768
2828
fwdFlowThroughStep2 ( arg , par , ret , node , cc , state , summaryCtx , argT , argAp , t0 , ap ) and
2769
- fwdFlow1 ( node , state , cc , summaryCtx , argT , argAp , t0 , t , ap , _) and
2770
- out = TStagePathNodeMid ( node , state , cc , summaryCtx , argT , argAp , t , ap )
2829
+ out = typeStrengthenToStagePathNode ( node , state , cc , summaryCtx , argT , argAp , t0 , ap )
2771
2830
)
2772
2831
}
2773
2832
2774
- query predicate edges ( StagePathNode pn1 , StagePathNode pn2 ) {
2775
- exists (
2776
- NodeEx node , FlowState state , Cc cc , ParamNodeOption summaryCtx , TypOption argT ,
2777
- ApOption argAp , Typ t0 , Typ t , Ap ap
2778
- |
2779
- step ( pn1 , node , state , cc , summaryCtx , argT , argAp , t0 , ap ) and
2780
- fwdFlow1 ( node , state , cc , summaryCtx , argT , argAp , t0 , t , ap , _) and
2781
- pn2 = TStagePathNodeMid ( node , state , cc , summaryCtx , argT , argAp , t , ap )
2833
+ query predicate edges ( StagePathNode pn1 , StagePathNode pn2 , string key , string val ) {
2834
+ key = "provenance" and
2835
+ (
2836
+ localStep ( pn1 , pn2 , val )
2837
+ or
2838
+ nonLocalStep ( pn1 , pn2 , val )
2839
+ or
2840
+ pn1 .isArbitrarySource ( ) and pn2 .isSource ( ) and val = ""
2841
+ or
2842
+ pn1 .isSink ( ) and pn2 .isArbitrarySink ( ) and val = ""
2782
2843
)
2783
- or
2784
- pn1 .isArbitrarySource ( ) and pn2 .isSource ( )
2785
- or
2786
- pn1 .isSink ( ) and pn2 .isArbitrarySink ( )
2787
2844
}
2788
2845
}
2789
2846
@@ -2917,19 +2974,20 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2917
2974
bindingset [ node2, state2]
2918
2975
predicate localStep (
2919
2976
NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
2920
- Typ t , LocalCc lcc
2977
+ Typ t , LocalCc lcc , string label
2921
2978
) {
2922
2979
(
2923
2980
preservesValue = true and
2924
- localFlowStepNodeCand1 ( node1 , node2 , _ ) and
2981
+ localFlowStepNodeCand1 ( node1 , node2 , label ) and
2925
2982
state1 = state2
2926
2983
or
2927
2984
preservesValue = false and
2928
- additionalLocalFlowStepNodeCand1 ( node1 , node2 , _ ) and
2985
+ additionalLocalFlowStepNodeCand1 ( node1 , node2 , label ) and
2929
2986
state1 = state2
2930
2987
or
2931
2988
preservesValue = false and
2932
- additionalLocalStateStep ( node1 , state1 , node2 , state2 )
2989
+ additionalLocalStateStep ( node1 , state1 , node2 , state2 ) and
2990
+ label = "Config"
2933
2991
) and
2934
2992
exists ( t ) and
2935
2993
exists ( lcc )
@@ -3203,9 +3261,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
3203
3261
3204
3262
predicate localStep (
3205
3263
NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
3206
- Typ t , LocalCc lcc
3264
+ Typ t , LocalCc lcc , string label
3207
3265
) {
3208
- localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , _, _, _ ) and
3266
+ localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , _, _, label ) and
3209
3267
exists ( t ) and
3210
3268
exists ( lcc )
3211
3269
}
@@ -3290,9 +3348,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
3290
3348
pragma [ nomagic]
3291
3349
predicate localStep (
3292
3350
NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
3293
- Typ t , LocalCc lcc
3351
+ Typ t , LocalCc lcc , string label
3294
3352
) {
3295
- localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , t , _, _ ) and
3353
+ localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , t , _, label ) and
3296
3354
PrevStage:: revFlow ( node1 , pragma [ only_bind_into ] ( state1 ) , _) and
3297
3355
PrevStage:: revFlow ( node2 , pragma [ only_bind_into ] ( state2 ) , _) and
3298
3356
exists ( lcc )
@@ -3590,9 +3648,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
3590
3648
3591
3649
predicate localStep (
3592
3650
NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
3593
- Typ t , LocalCc lcc
3651
+ Typ t , LocalCc lcc , string label
3594
3652
) {
3595
- localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , t , lcc , _ ) and
3653
+ localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , t , lcc , label ) and
3596
3654
PrevStage:: revFlow ( node1 , pragma [ only_bind_into ] ( state1 ) , _) and
3597
3655
PrevStage:: revFlow ( node2 , pragma [ only_bind_into ] ( state2 ) , _)
3598
3656
}
0 commit comments