@@ -2486,6 +2486,264 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
2486
2486
callEdgeReturn ( call , c , _, _, _, _, _)
2487
2487
}
2488
2488
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
+
2489
2747
additional predicate stats (
2490
2748
boolean fwd , int nodes , int fields , int conscand , int states , int tuples , int calledges ,
2491
2749
int tfnodes , int tftuples
0 commit comments