@@ -2486,6 +2486,264 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
24862486 callEdgeReturn ( call , c , _, _, _, _, _)
24872487 }
24882488
2489+ additional module Graph {
2490+ private newtype TStagePathNode =
2491+ TStagePathNodeMid (
2492+ NodeEx node , FlowState state , Cc cc , ParamNodeOption summaryCtx , TypOption argT ,
2493+ ApOption argAp , Typ t , Ap ap
2494+ ) {
2495+ fwdFlow ( node , state , cc , summaryCtx , argT , argAp , t , ap , _) and
2496+ revFlow ( node , state , _, _, ap )
2497+ } or
2498+ TStagePathNodeSrcGrp ( ) or
2499+ TStagePathNodeSinkGrp ( )
2500+
2501+ class StagePathNode extends TStagePathNode {
2502+ abstract string toString ( ) ;
2503+
2504+ abstract Location getLocation ( ) ;
2505+
2506+ predicate isSource ( ) { none ( ) }
2507+
2508+ predicate isSink ( ) { none ( ) }
2509+
2510+ predicate isArbitrarySource ( ) { this instanceof TStagePathNodeSrcGrp }
2511+
2512+ predicate isArbitrarySink ( ) { this instanceof TStagePathNodeSinkGrp }
2513+ }
2514+
2515+ class StagePathNodeSrcGrp extends StagePathNode , TStagePathNodeSrcGrp {
2516+ override string toString ( ) { result = "<any source>" }
2517+
2518+ override Location getLocation ( ) { result .hasLocationInfo ( "" , 0 , 0 , 0 , 0 ) }
2519+ }
2520+
2521+ class StagePathNodeSinkGrp extends StagePathNode , TStagePathNodeSinkGrp {
2522+ override string toString ( ) { result = "<any sink>" }
2523+
2524+ override Location getLocation ( ) { result .hasLocationInfo ( "" , 0 , 0 , 0 , 0 ) }
2525+ }
2526+
2527+ class StagePathNodeMid extends StagePathNode , TStagePathNodeMid {
2528+ NodeEx node ;
2529+ FlowState state ;
2530+ Cc cc ;
2531+ ParamNodeOption summaryCtx ;
2532+ TypOption argT ;
2533+ ApOption argAp ;
2534+ Typ t ;
2535+ Ap ap ;
2536+
2537+ StagePathNodeMid ( ) {
2538+ this = TStagePathNodeMid ( node , state , cc , summaryCtx , argT , argAp , t , ap )
2539+ }
2540+
2541+ override string toString ( ) {
2542+ result =
2543+ node .toString ( ) + " " + cc .toString ( ) + " " + t .toString ( ) + " " + ap .toString ( )
2544+ }
2545+
2546+ override Location getLocation ( ) { result = node .getLocation ( ) }
2547+
2548+ override predicate isSource ( ) {
2549+ sourceNode ( node , state ) and
2550+ ( if hasSourceCallCtx ( ) then cc = ccSomeCall ( ) else cc = ccNone ( ) ) and
2551+ summaryCtx = TParamNodeNone ( ) and
2552+ t = getNodeTyp ( node ) and
2553+ ap instanceof ApNil
2554+ }
2555+
2556+ override predicate isSink ( ) {
2557+ sinkNode ( node , state ) and
2558+ ( if hasSinkCallCtx ( ) then instanceofCcNoCall ( cc ) else any ( ) ) and
2559+ ap instanceof ApNil
2560+ }
2561+ }
2562+
2563+ pragma [ nomagic]
2564+ private predicate fwdFlowInStep (
2565+ ArgNodeEx arg , ParamNodeEx p , FlowState state , Cc outercc , CcCall innercc ,
2566+ ParamNodeOption summaryCtx , TypOption argT , ApOption argAp , Typ t , Ap ap ,
2567+ boolean allowsFlowThrough
2568+ ) {
2569+ exists ( ApApprox apa , boolean allowsFlowThrough0 |
2570+ FwdFlowIn< FwdFlowInNoRestriction > :: fwdFlowIn ( _, arg , _, p , state , outercc , innercc ,
2571+ summaryCtx , argT , argAp , t , ap , apa , _, allowsFlowThrough0 ) and
2572+ if PrevStage:: parameterMayFlowThrough ( p , apa )
2573+ then allowsFlowThrough = allowsFlowThrough0
2574+ else allowsFlowThrough = false
2575+ )
2576+ }
2577+
2578+ pragma [ nomagic]
2579+ private predicate fwdFlowThroughStep0 (
2580+ DataFlowCall call , ArgNodeEx arg , Cc cc , FlowState state , CcCall ccc ,
2581+ ParamNodeOption summaryCtx , TypOption argT , ApOption argAp , Typ t , Ap ap , ApApprox apa ,
2582+ RetNodeEx ret , ParamNodeEx innerSummaryCtx , Typ innerArgT , Ap innerArgAp ,
2583+ ApApprox innerArgApa
2584+ ) {
2585+ fwdFlowThrough0 ( call , arg , cc , state , ccc , summaryCtx , argT , argAp , t , ap , apa , ret ,
2586+ innerSummaryCtx , innerArgT , innerArgAp , innerArgApa )
2587+ }
2588+
2589+ bindingset [ node, state, cc, summaryCtx, argT, argAp, t, ap]
2590+ pragma [ inline_late]
2591+ private StagePathNode mkStagePathNode (
2592+ NodeEx node , FlowState state , Cc cc , ParamNodeOption summaryCtx , TypOption argT ,
2593+ ApOption argAp , Typ t , Ap ap
2594+ ) {
2595+ result = TStagePathNodeMid ( node , state , cc , summaryCtx , argT , argAp , t , ap )
2596+ }
2597+
2598+ pragma [ nomagic]
2599+ private predicate fwdFlowThroughStep1 (
2600+ StagePathNode pn1 , StagePathNode pn2 , StagePathNode pn3 , DataFlowCall call , Cc cc ,
2601+ FlowState state , CcCall ccc , ParamNodeOption summaryCtx , TypOption argT , ApOption argAp ,
2602+ Typ t , Ap ap , ApApprox apa , RetNodeEx ret , ApApprox innerArgApa
2603+ ) {
2604+ exists ( FlowState state0 , ArgNodeEx arg , ParamNodeEx p , Typ innerArgT , Ap innerArgAp |
2605+ fwdFlowThroughStep0 ( call , arg , cc , state , ccc , summaryCtx , argT , argAp , t , ap , apa ,
2606+ ret , p , innerArgT , innerArgAp , innerArgApa ) and
2607+ revFlow ( arg , state0 , _, _, _) and
2608+ pn1 = mkStagePathNode ( arg , state0 , cc , summaryCtx , argT , argAp , innerArgT , innerArgAp ) and
2609+ pn2 =
2610+ mkStagePathNode ( p , state0 , ccc , TParamNodeSome ( p .asNode ( ) ) ,
2611+ TypOption:: some ( innerArgT ) , apSome ( innerArgAp ) , innerArgT , innerArgAp ) and
2612+ pn3 =
2613+ mkStagePathNode ( ret , state , ccc , TParamNodeSome ( p .asNode ( ) ) ,
2614+ TypOption:: some ( innerArgT ) , apSome ( innerArgAp ) , t , ap )
2615+ )
2616+ }
2617+
2618+ pragma [ nomagic]
2619+ private predicate fwdFlowThroughStep2 (
2620+ StagePathNode pn1 , StagePathNode pn2 , StagePathNode pn3 , NodeEx node , Cc cc ,
2621+ FlowState state , ParamNodeOption summaryCtx , TypOption argT , ApOption argAp , Typ t ,
2622+ Ap ap
2623+ ) {
2624+ exists (
2625+ DataFlowCall call , CcCall ccc , RetNodeEx ret , boolean allowsFieldFlow ,
2626+ ApApprox innerArgApa , ApApprox apa
2627+ |
2628+ fwdFlowThroughStep1 ( pn1 , pn2 , pn3 , call , cc , state , ccc , summaryCtx , argT , argAp , t ,
2629+ ap , apa , ret , innerArgApa ) and
2630+ flowThroughOutOfCall ( call , ccc , ret , node , allowsFieldFlow , innerArgApa , apa ) and
2631+ if allowsFieldFlow = false then ap instanceof ApNil else any ( )
2632+ )
2633+ }
2634+
2635+ private predicate step (
2636+ StagePathNode pn1 , NodeEx node , FlowState state , Cc cc , ParamNodeOption summaryCtx ,
2637+ TypOption argT , ApOption argAp , Typ t , Ap ap
2638+ ) {
2639+ exists ( NodeEx mid , FlowState state0 , Typ t0 , LocalCc localCc |
2640+ pn1 = TStagePathNodeMid ( mid , state0 , cc , summaryCtx , argT , argAp , t0 , ap ) and
2641+ localCc = getLocalCc ( cc )
2642+ |
2643+ localStep ( mid , state0 , node , state , true , _, localCc ) and
2644+ t = t0
2645+ or
2646+ localStep ( mid , state0 , node , state , false , t , localCc ) and
2647+ ap instanceof ApNil
2648+ )
2649+ or
2650+ exists ( NodeEx mid , FlowState state0 , Typ t0 |
2651+ pn1 = TStagePathNodeMid ( mid , state0 , _, _, _, _, t0 , ap ) and
2652+ cc = ccNone ( ) and
2653+ summaryCtx = TParamNodeNone ( ) and
2654+ argT instanceof TypOption:: None and
2655+ argAp = apNone ( )
2656+ |
2657+ jumpStepEx ( mid , node ) and
2658+ state = state0 and
2659+ t = t0
2660+ or
2661+ additionalJumpStep ( mid , node , _) and
2662+ state = state0 and
2663+ t = getNodeTyp ( node ) and
2664+ ap instanceof ApNil
2665+ or
2666+ additionalJumpStateStep ( mid , state0 , node , state ) and
2667+ t = getNodeTyp ( node ) and
2668+ ap instanceof ApNil
2669+ )
2670+ or
2671+ // store
2672+ exists ( NodeEx mid , Content c , Typ t0 , Ap ap0 |
2673+ pn1 = TStagePathNodeMid ( mid , state , cc , summaryCtx , argT , argAp , t0 , ap0 ) and
2674+ fwdFlowStore ( mid , t0 , ap0 , c , t , node , state , cc , summaryCtx , argT , argAp ) and
2675+ ap = apCons ( c , t0 , ap0 )
2676+ )
2677+ or
2678+ // read
2679+ exists ( NodeEx mid , Typ t0 , Ap ap0 , Content c |
2680+ pn1 = TStagePathNodeMid ( mid , state , cc , summaryCtx , argT , argAp , t0 , ap0 ) and
2681+ fwdFlowRead ( t0 , ap0 , c , mid , node , state , cc , summaryCtx , argT , argAp ) and
2682+ fwdFlowConsCand ( t0 , ap0 , c , t , ap )
2683+ )
2684+ or
2685+ // flow into a callable
2686+ exists (
2687+ ArgNodeEx arg , boolean allowsFlowThrough , Cc outercc , ParamNodeOption outerSummaryCtx ,
2688+ TypOption outerArgT , ApOption outerArgAp
2689+ |
2690+ pn1 =
2691+ TStagePathNodeMid ( arg , state , outercc , outerSummaryCtx , outerArgT , outerArgAp , t , ap ) and
2692+ fwdFlowInStep ( arg , node , state , outercc , cc , outerSummaryCtx , outerArgT , outerArgAp ,
2693+ t , ap , allowsFlowThrough ) and
2694+ if allowsFlowThrough = true
2695+ then (
2696+ summaryCtx = TParamNodeSome ( node .asNode ( ) ) and
2697+ argT = TypOption:: some ( t ) and
2698+ argAp = apSome ( ap )
2699+ ) else (
2700+ summaryCtx = TParamNodeNone ( ) and
2701+ argT instanceof TypOption:: None and
2702+ argAp = apNone ( )
2703+ )
2704+ )
2705+ or
2706+ // flow out of a callable
2707+ exists ( RetNodeEx ret , CcNoCall innercc , boolean allowsFieldFlow , ApApprox apa |
2708+ pn1 = TStagePathNodeMid ( ret , state , innercc , summaryCtx , argT , argAp , t , ap ) and
2709+ fwdFlowIntoRet ( ret , state , innercc , summaryCtx , argT , argAp , t , ap , apa ) and
2710+ fwdFlowOutValidEdge ( _, ret , innercc , _, node , cc , apa , allowsFieldFlow ) and
2711+ if allowsFieldFlow = false then ap instanceof ApNil else any ( )
2712+ )
2713+ or
2714+ // flow through a callable
2715+ fwdFlowThroughStep2 ( pn1 , _, _, node , cc , state , summaryCtx , argT , argAp , t , ap )
2716+ }
2717+
2718+ query predicate subpaths (
2719+ StagePathNode arg , StagePathNode par , StagePathNode ret , StagePathNode out
2720+ ) {
2721+ exists (
2722+ NodeEx node , FlowState state , Cc cc , ParamNodeOption summaryCtx , TypOption argT ,
2723+ ApOption argAp , Typ t0 , Typ t , Ap ap
2724+ |
2725+ fwdFlowThroughStep2 ( arg , par , ret , node , cc , state , summaryCtx , argT , argAp , t0 , ap ) and
2726+ fwdFlow1 ( node , state , cc , summaryCtx , argT , argAp , t0 , t , ap , _) and
2727+ out = TStagePathNodeMid ( node , state , cc , summaryCtx , argT , argAp , t , ap )
2728+ )
2729+ }
2730+
2731+ query predicate edges ( StagePathNode pn1 , StagePathNode pn2 ) {
2732+ exists (
2733+ NodeEx node , FlowState state , Cc cc , ParamNodeOption summaryCtx , TypOption argT ,
2734+ ApOption argAp , Typ t0 , Typ t , Ap ap
2735+ |
2736+ step ( pn1 , node , state , cc , summaryCtx , argT , argAp , t0 , ap ) and
2737+ fwdFlow1 ( node , state , cc , summaryCtx , argT , argAp , t0 , t , ap , _) and
2738+ pn2 = TStagePathNodeMid ( node , state , cc , summaryCtx , argT , argAp , t , ap )
2739+ )
2740+ or
2741+ pn1 .isArbitrarySource ( ) and pn2 .isSource ( )
2742+ or
2743+ pn1 .isSink ( ) and pn2 .isArbitrarySink ( )
2744+ }
2745+ }
2746+
24892747 additional predicate stats (
24902748 boolean fwd , int nodes , int fields , int conscand , int states , int tuples , int calledges ,
24912749 int tfnodes , int tftuples
0 commit comments