@@ -1406,7 +1406,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
14061406 bindingset [ node2, state2]
14071407 predicate localStep (
14081408 NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
1409- Typ t , LocalCc lcc
1409+ Typ t , LocalCc lcc , string label
14101410 ) ;
14111411
14121412 bindingset [ node, state, t0, ap]
@@ -1524,10 +1524,10 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
15241524 fwdFlow ( mid , state0 , cc , summaryCtx , argT , argAp , t0 , ap , apa ) and
15251525 localCc = getLocalCc ( cc )
15261526 |
1527- localStep ( mid , state0 , node , state , true , _, localCc ) and
1527+ localStep ( mid , state0 , node , state , true , _, localCc , _ ) and
15281528 t = t0
15291529 or
1530- localStep ( mid , state0 , node , state , false , t , localCc ) and
1530+ localStep ( mid , state0 , node , state , false , t , localCc , _ ) and
15311531 ap instanceof ApNil
15321532 )
15331533 or
@@ -2174,12 +2174,12 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
21742174 ap instanceof ApNil
21752175 or
21762176 exists ( NodeEx mid , FlowState state0 |
2177- localStep ( node , state , mid , state0 , true , _, _) and
2177+ localStep ( node , state , mid , state0 , true , _, _, _ ) and
21782178 revFlow ( mid , state0 , returnCtx , returnAp , ap )
21792179 )
21802180 or
21812181 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
21832183 revFlow ( mid , state0 , returnCtx , returnAp , ap ) and
21842184 ap instanceof ApNil
21852185 )
@@ -2638,6 +2638,16 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
26382638 result = TStagePathNodeMid ( node , state , cc , summaryCtx , argT , argAp , t , ap )
26392639 }
26402640
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+
26412651 pragma [ nomagic]
26422652 private predicate fwdFlowThroughStep1 (
26432653 StagePathNode pn1 , StagePathNode pn2 , StagePathNode pn3 , DataFlowCall call , Cc cc ,
@@ -2675,21 +2685,74 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
26752685 )
26762686 }
26772687
2678- private predicate step (
2688+ private predicate localStep (
26792689 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
26812691 ) {
26822692 exists ( NodeEx mid , FlowState state0 , Typ t0 , LocalCc localCc |
26832693 pn1 = TStagePathNodeMid ( mid , state0 , cc , summaryCtx , argT , argAp , t0 , ap ) and
26842694 localCc = getLocalCc ( cc )
26852695 |
2686- localStep ( mid , state0 , node , state , true , _, localCc ) and
2696+ localStep ( mid , state0 , node , state , true , _, localCc , label ) and
26872697 t = t0
26882698 or
2689- localStep ( mid , state0 , node , state , false , t , localCc ) and
2699+ localStep ( mid , state0 , node , state , false , t , localCc , label ) and
26902700 ap instanceof ApNil
26912701 )
26922702 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
26932756 exists ( NodeEx mid , FlowState state0 , Typ t0 |
26942757 pn1 = TStagePathNodeMid ( mid , state0 , _, _, _, _, t0 , ap ) and
26952758 cc = ccNone ( ) and
@@ -2699,30 +2762,18 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
26992762 |
27002763 jumpStepEx ( mid , node ) and
27012764 state = state0 and
2702- t = t0
2765+ t = t0 and
2766+ label = ""
27032767 or
2704- additionalJumpStep ( mid , node , _ ) and
2768+ additionalJumpStep ( mid , node , label ) and
27052769 state = state0 and
27062770 t = getNodeTyp ( node ) and
27072771 ap instanceof ApNil
27082772 or
27092773 additionalJumpStateStep ( mid , state0 , node , state ) and
27102774 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"
27262777 )
27272778 or
27282779 // flow into a callable
@@ -2734,6 +2785,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
27342785 TStagePathNodeMid ( arg , state , outercc , outerSummaryCtx , outerArgT , outerArgAp , t , ap ) and
27352786 fwdFlowInStep ( arg , node , state , outercc , cc , outerSummaryCtx , outerArgT , outerArgAp ,
27362787 t , ap , allowsFlowThrough ) and
2788+ label = "" and
27372789 if allowsFlowThrough = true
27382790 then (
27392791 summaryCtx = TParamNodeSome ( node .asNode ( ) ) and
@@ -2751,39 +2803,44 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
27512803 pn1 = TStagePathNodeMid ( ret , state , innercc , summaryCtx , argT , argAp , t , ap ) and
27522804 fwdFlowIntoRet ( ret , state , innercc , summaryCtx , argT , argAp , t , ap , apa ) and
27532805 fwdFlowOutValidEdge ( _, ret , innercc , _, node , cc , apa , allowsFieldFlow ) and
2806+ label = "" and
27542807 if allowsFieldFlow = false then ap instanceof ApNil else any ( )
27552808 )
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+ )
27592819 }
27602820
27612821 query predicate subpaths (
27622822 StagePathNode arg , StagePathNode par , StagePathNode ret , StagePathNode out
27632823 ) {
27642824 exists (
27652825 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
27672827 |
27682828 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 )
27712830 )
27722831 }
27732832
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 = ""
27822843 )
2783- or
2784- pn1 .isArbitrarySource ( ) and pn2 .isSource ( )
2785- or
2786- pn1 .isSink ( ) and pn2 .isArbitrarySink ( )
27872844 }
27882845 }
27892846
@@ -2917,19 +2974,20 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
29172974 bindingset [ node2, state2]
29182975 predicate localStep (
29192976 NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
2920- Typ t , LocalCc lcc
2977+ Typ t , LocalCc lcc , string label
29212978 ) {
29222979 (
29232980 preservesValue = true and
2924- localFlowStepNodeCand1 ( node1 , node2 , _ ) and
2981+ localFlowStepNodeCand1 ( node1 , node2 , label ) and
29252982 state1 = state2
29262983 or
29272984 preservesValue = false and
2928- additionalLocalFlowStepNodeCand1 ( node1 , node2 , _ ) and
2985+ additionalLocalFlowStepNodeCand1 ( node1 , node2 , label ) and
29292986 state1 = state2
29302987 or
29312988 preservesValue = false and
2932- additionalLocalStateStep ( node1 , state1 , node2 , state2 )
2989+ additionalLocalStateStep ( node1 , state1 , node2 , state2 ) and
2990+ label = "Config"
29332991 ) and
29342992 exists ( t ) and
29352993 exists ( lcc )
@@ -3203,9 +3261,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
32033261
32043262 predicate localStep (
32053263 NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
3206- Typ t , LocalCc lcc
3264+ Typ t , LocalCc lcc , string label
32073265 ) {
3208- localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , _, _, _ ) and
3266+ localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , _, _, label ) and
32093267 exists ( t ) and
32103268 exists ( lcc )
32113269 }
@@ -3290,9 +3348,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
32903348 pragma [ nomagic]
32913349 predicate localStep (
32923350 NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
3293- Typ t , LocalCc lcc
3351+ Typ t , LocalCc lcc , string label
32943352 ) {
3295- localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , t , _, _ ) and
3353+ localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , t , _, label ) and
32963354 PrevStage:: revFlow ( node1 , pragma [ only_bind_into ] ( state1 ) , _) and
32973355 PrevStage:: revFlow ( node2 , pragma [ only_bind_into ] ( state2 ) , _) and
32983356 exists ( lcc )
@@ -3590,9 +3648,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
35903648
35913649 predicate localStep (
35923650 NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
3593- Typ t , LocalCc lcc
3651+ Typ t , LocalCc lcc , string label
35943652 ) {
3595- localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , t , lcc , _ ) and
3653+ localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , t , lcc , label ) and
35963654 PrevStage:: revFlow ( node1 , pragma [ only_bind_into ] ( state1 ) , _) and
35973655 PrevStage:: revFlow ( node2 , pragma [ only_bind_into ] ( state2 ) , _)
35983656 }
0 commit comments