@@ -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
@@ -2180,12 +2180,12 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
21802180 ap instanceof ApNil
21812181 or
21822182 exists ( NodeEx mid , FlowState state0 |
2183- localStep ( node , state , mid , state0 , true , _, _) and
2183+ localStep ( node , state , mid , state0 , true , _, _, _ ) and
21842184 revFlow ( mid , state0 , returnCtx , returnAp , ap )
21852185 )
21862186 or
21872187 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
21892189 revFlow ( mid , state0 , returnCtx , returnAp , ap ) and
21902190 ap instanceof ApNil
21912191 )
@@ -2659,6 +2659,16 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
26592659 result = TStagePathNodeMid ( node , state , cc , summaryCtx , argT , argAp , t , ap )
26602660 }
26612661
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+
26622672 pragma [ nomagic]
26632673 private predicate fwdFlowThroughStep1 (
26642674 StagePathNode pn1 , StagePathNode pn2 , StagePathNode pn3 , DataFlowCall call , Cc cc ,
@@ -2696,21 +2706,74 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
26962706 )
26972707 }
26982708
2699- private predicate step (
2709+ private predicate localStep (
27002710 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
27022712 ) {
27032713 exists ( NodeEx mid , FlowState state0 , Typ t0 , LocalCc localCc |
27042714 pn1 = TStagePathNodeMid ( mid , state0 , cc , summaryCtx , argT , argAp , t0 , ap ) and
27052715 localCc = getLocalCc ( cc )
27062716 |
2707- localStep ( mid , state0 , node , state , true , _, localCc ) and
2717+ localStep ( mid , state0 , node , state , true , _, localCc , label ) and
27082718 t = t0
27092719 or
2710- localStep ( mid , state0 , node , state , false , t , localCc ) and
2720+ localStep ( mid , state0 , node , state , false , t , localCc , label ) and
27112721 ap instanceof ApNil
27122722 )
27132723 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
27142777 exists ( NodeEx mid , FlowState state0 , Typ t0 |
27152778 pn1 = TStagePathNodeMid ( mid , state0 , _, _, _, _, t0 , ap ) and
27162779 cc = ccNone ( ) and
@@ -2720,30 +2783,18 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
27202783 |
27212784 jumpStepEx ( mid , node ) and
27222785 state = state0 and
2723- t = t0
2786+ t = t0 and
2787+ label = ""
27242788 or
2725- additionalJumpStep ( mid , node , _ ) and
2789+ additionalJumpStep ( mid , node , label ) and
27262790 state = state0 and
27272791 t = getNodeTyp ( node ) and
27282792 ap instanceof ApNil
27292793 or
27302794 additionalJumpStateStep ( mid , state0 , node , state ) and
27312795 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"
27472798 )
27482799 or
27492800 // flow into a callable
@@ -2755,6 +2806,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
27552806 TStagePathNodeMid ( arg , state , outercc , outerSummaryCtx , outerArgT , outerArgAp , t , ap ) and
27562807 fwdFlowInStep ( arg , node , state , outercc , cc , outerSummaryCtx , outerArgT , outerArgAp ,
27572808 t , ap , allowsFlowThrough ) and
2809+ label = "" and
27582810 if allowsFlowThrough = true
27592811 then (
27602812 summaryCtx = TParamNodeSome ( node .asNode ( ) ) and
@@ -2772,39 +2824,44 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
27722824 pn1 = TStagePathNodeMid ( ret , state , innercc , summaryCtx , argT , argAp , t , ap ) and
27732825 fwdFlowIntoRet ( ret , state , innercc , summaryCtx , argT , argAp , t , ap , apa ) and
27742826 fwdFlowOutValidEdge ( _, ret , innercc , _, node , cc , apa , allowsFieldFlow ) and
2827+ label = "" and
27752828 if allowsFieldFlow = false then ap instanceof ApNil else any ( )
27762829 )
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+ )
27802840 }
27812841
27822842 query predicate subpaths (
27832843 StagePathNode arg , StagePathNode par , StagePathNode ret , StagePathNode out
27842844 ) {
27852845 exists (
27862846 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
27882848 |
27892849 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 )
27922851 )
27932852 }
27942853
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 = ""
28032864 )
2804- or
2805- pn1 .isArbitrarySource ( ) and pn2 .isSource ( )
2806- or
2807- pn1 .isSink ( ) and pn2 .isArbitrarySink ( )
28082865 }
28092866 }
28102867
@@ -2938,19 +2995,20 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
29382995 bindingset [ node2, state2]
29392996 predicate localStep (
29402997 NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
2941- Typ t , LocalCc lcc
2998+ Typ t , LocalCc lcc , string label
29422999 ) {
29433000 (
29443001 preservesValue = true and
2945- localFlowStepNodeCand1 ( node1 , node2 , _ ) and
3002+ localFlowStepNodeCand1 ( node1 , node2 , label ) and
29463003 state1 = state2
29473004 or
29483005 preservesValue = false and
2949- additionalLocalFlowStepNodeCand1 ( node1 , node2 , _ ) and
3006+ additionalLocalFlowStepNodeCand1 ( node1 , node2 , label ) and
29503007 state1 = state2
29513008 or
29523009 preservesValue = false and
2953- additionalLocalStateStep ( node1 , state1 , node2 , state2 )
3010+ additionalLocalStateStep ( node1 , state1 , node2 , state2 ) and
3011+ label = "Config"
29543012 ) and
29553013 exists ( t ) and
29563014 exists ( lcc )
@@ -3224,9 +3282,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
32243282
32253283 predicate localStep (
32263284 NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
3227- Typ t , LocalCc lcc
3285+ Typ t , LocalCc lcc , string label
32283286 ) {
3229- localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , _, _, _ ) and
3287+ localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , _, _, label ) and
32303288 exists ( t ) and
32313289 exists ( lcc )
32323290 }
@@ -3311,9 +3369,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
33113369 pragma [ nomagic]
33123370 predicate localStep (
33133371 NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
3314- Typ t , LocalCc lcc
3372+ Typ t , LocalCc lcc , string label
33153373 ) {
3316- localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , t , _, _ ) and
3374+ localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , t , _, label ) and
33173375 PrevStage:: revFlow ( node1 , pragma [ only_bind_into ] ( state1 ) , _) and
33183376 PrevStage:: revFlow ( node2 , pragma [ only_bind_into ] ( state2 ) , _) and
33193377 exists ( lcc )
@@ -3613,9 +3671,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
36133671
36143672 predicate localStep (
36153673 NodeEx node1 , FlowState state1 , NodeEx node2 , FlowState state2 , boolean preservesValue ,
3616- Typ t , LocalCc lcc
3674+ Typ t , LocalCc lcc , string label
36173675 ) {
3618- localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , t , lcc , _ ) and
3676+ localFlowBigStep ( node1 , state1 , node2 , state2 , preservesValue , t , lcc , label ) and
36193677 PrevStage:: revFlow ( node1 , pragma [ only_bind_into ] ( state1 ) , _) and
36203678 PrevStage:: revFlow ( node2 , pragma [ only_bind_into ] ( state2 ) , _)
36213679 }
0 commit comments