@@ -1715,7 +1715,7 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
17151715 * Provides a graph representation of the data flow in this stage suitable for use in a `path-problem` query.
17161716 */
17171717 additional module Graph {
1718- private newtype TPathNode =
1718+ newtype TPathNode =
17191719 TPathNodeMid ( Nd node , Cc cc , SummaryCtx summaryCtx , Typ t , Ap ap , TypOption stored ) {
17201720 fwdFlow ( node , cc , summaryCtx , t , ap , stored ) and
17211721 revFlow ( node , _, _, ap )
@@ -2473,41 +2473,81 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
24732473 }
24742474 }
24752475
2476- additional predicate stats (
2477- boolean fwd , int nodes , int fields , int conscand , int states , int tuples , int calledges ,
2478- int tfnodes , int tftuples
2479- ) {
2480- fwd = true and
2481- nodes = count ( NodeEx node | fwdFlow ( any ( Nd n | n .getNodeEx ( ) = node ) , _, _, _, _, _) ) and
2482- fields = count ( Content f0 | fwdConsCand ( f0 , _) ) and
2483- conscand = count ( Content f0 , Ap ap | fwdConsCand ( f0 , ap ) ) and
2484- states = count ( FlowState state | fwdFlow ( any ( Nd n | n .getState ( ) = state ) , _, _, _, _, _) ) and
2485- tuples =
2486- count ( Nd n , Cc cc , SummaryCtx summaryCtx , Typ t , Ap ap , TypOption stored |
2487- fwdFlow ( n , cc , summaryCtx , t , ap , stored )
2488- ) and
2489- calledges =
2490- count ( Call call , Callable c |
2491- FwdTypeFlowInput:: dataFlowTakenCallEdgeIn ( call , c , _) or
2492- FwdTypeFlowInput:: dataFlowTakenCallEdgeOut ( call , c )
2493- ) and
2494- FwdTypeFlow:: typeFlowStats ( tfnodes , tftuples )
2495- or
2496- fwd = false and
2497- nodes = count ( NodeEx node | revFlow ( any ( Nd n | n .getNodeEx ( ) = node ) , _, _, _) ) and
2498- fields = count ( Content f0 | consCand ( f0 , _) ) and
2499- conscand = count ( Content f0 , Ap ap | consCand ( f0 , ap ) ) and
2500- states = count ( FlowState state | revFlow ( any ( Nd n | n .getState ( ) = state ) , _, _, _) ) and
2501- tuples =
2502- count ( Nd n , ReturnCtx returnCtx , ApOption retAp , Ap ap |
2503- revFlow ( n , returnCtx , retAp , ap )
2504- ) and
2505- calledges =
2506- count ( Call call , Callable c |
2507- RevTypeFlowInput:: dataFlowTakenCallEdgeIn ( call , c , _) or
2508- RevTypeFlowInput:: dataFlowTakenCallEdgeOut ( call , c )
2509- ) and
2510- RevTypeFlow:: typeFlowStats ( tfnodes , tftuples )
2476+ /** Provides predicates for debugging. */
2477+ additional module Debug {
2478+ private import Graph
2479+
2480+ predicate stats (
2481+ boolean fwd , int nodes , int fields , int conscand , int states , int tuples , int calledges ,
2482+ int tfnodes , int tftuples
2483+ ) {
2484+ fwd = true and
2485+ nodes = count ( NodeEx node | fwdFlow ( any ( Nd n | n .getNodeEx ( ) = node ) , _, _, _, _, _) ) and
2486+ fields = count ( Content f0 | fwdConsCand ( f0 , _) ) and
2487+ conscand = count ( Content f0 , Ap ap | fwdConsCand ( f0 , ap ) ) and
2488+ states =
2489+ count ( FlowState state | fwdFlow ( any ( Nd n | n .getState ( ) = state ) , _, _, _, _, _) ) and
2490+ tuples =
2491+ count ( Nd n , Cc cc , SummaryCtx summaryCtx , Typ t , Ap ap , TypOption stored |
2492+ fwdFlow ( n , cc , summaryCtx , t , ap , stored )
2493+ ) and
2494+ calledges =
2495+ count ( Call call , Callable c |
2496+ FwdTypeFlowInput:: dataFlowTakenCallEdgeIn ( call , c , _) or
2497+ FwdTypeFlowInput:: dataFlowTakenCallEdgeOut ( call , c )
2498+ ) and
2499+ FwdTypeFlow:: typeFlowStats ( tfnodes , tftuples )
2500+ or
2501+ fwd = false and
2502+ nodes = count ( NodeEx node | revFlow ( any ( Nd n | n .getNodeEx ( ) = node ) , _, _, _) ) and
2503+ fields = count ( Content f0 | consCand ( f0 , _) ) and
2504+ conscand = count ( Content f0 , Ap ap | consCand ( f0 , ap ) ) and
2505+ states = count ( FlowState state | revFlow ( any ( Nd n | n .getState ( ) = state ) , _, _, _) ) and
2506+ tuples =
2507+ count ( Nd n , ReturnCtx returnCtx , ApOption retAp , Ap ap |
2508+ revFlow ( n , returnCtx , retAp , ap )
2509+ ) and
2510+ calledges =
2511+ count ( Call call , Callable c |
2512+ RevTypeFlowInput:: dataFlowTakenCallEdgeIn ( call , c , _) or
2513+ RevTypeFlowInput:: dataFlowTakenCallEdgeOut ( call , c )
2514+ ) and
2515+ RevTypeFlow:: typeFlowStats ( tfnodes , tftuples )
2516+ }
2517+
2518+ private int fanOut ( PathNodeImpl n ) {
2519+ result = strictcount ( n .getASuccessorImpl ( _) ) and
2520+ not n .isArbitrarySource ( )
2521+ }
2522+
2523+ private int fanIn ( PathNodeImpl n ) {
2524+ result = strictcount ( PathNodeImpl pred | n = pred .getASuccessorImpl ( _) ) and
2525+ not n .isArbitrarySink ( )
2526+ }
2527+
2528+ predicate maxFanOut ( PathNodeImpl pred , PathNodeImpl succ ) {
2529+ fanOut ( pred ) = max ( fanOut ( _) ) and
2530+ succ = pred .getASuccessorImpl ( _)
2531+ }
2532+
2533+ predicate maxFanIn ( PathNodeImpl pred , PathNodeImpl succ ) {
2534+ fanIn ( succ ) = max ( fanIn ( _) ) and
2535+ succ = pred .getASuccessorImpl ( _)
2536+ }
2537+
2538+ private int pathNodes ( Nd node ) {
2539+ result =
2540+ strictcount ( Cc cc , SummaryCtx summaryCtx , Typ t , Ap ap , TypOption stored |
2541+ exists ( TPathNodeMid ( node , cc , summaryCtx , t , ap , stored ) )
2542+ )
2543+ }
2544+
2545+ predicate maxPathNodes (
2546+ Nd node , Cc cc , SummaryCtx summaryCtx , Typ t , Ap ap , TypOption stored
2547+ ) {
2548+ exists ( TPathNodeMid ( node , cc , summaryCtx , t , ap , stored ) ) and
2549+ pathNodes ( node ) = max ( pathNodes ( _) )
2550+ }
25112551 }
25122552 /* End: Stage logic. */
25132553 }
@@ -3520,13 +3560,21 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
35203560 or
35213561 stage = "2 Fwd" and
35223562 n = 20 and
3523- Stage2:: stats ( true , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
3563+ Stage2:: Debug:: stats ( true , nodes , fields , conscand , states , tuples , calledges , tfnodes ,
3564+ tftuples )
35243565 or
35253566 stage = "2 Rev" and
35263567 n = 25 and
3527- Stage2:: stats ( false , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
3568+ Stage2:: Debug:: stats ( false , nodes , fields , conscand , states , tuples , calledges , tfnodes ,
3569+ tftuples )
35283570 }
35293571
3572+ predicate stage2maxFanOut = Stage2:: Debug:: maxFanOut / 2 ;
3573+
3574+ predicate stage2maxFanIn = Stage2:: Debug:: maxFanIn / 2 ;
3575+
3576+ predicate stage2maxPathNodes = Stage2:: Debug:: maxPathNodes / 6 ;
3577+
35303578 predicate stageStats3 (
35313579 int n , string stage , int nodes , int fields , int conscand , int states , int tuples ,
35323580 int calledges , int tfnodes , int tftuples
@@ -3535,13 +3583,21 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
35353583 or
35363584 stage = "3 Fwd" and
35373585 n = 30 and
3538- Stage3:: stats ( true , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
3586+ Stage3:: Debug:: stats ( true , nodes , fields , conscand , states , tuples , calledges , tfnodes ,
3587+ tftuples )
35393588 or
35403589 stage = "3 Rev" and
35413590 n = 35 and
3542- Stage3:: stats ( false , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
3591+ Stage3:: Debug:: stats ( false , nodes , fields , conscand , states , tuples , calledges , tfnodes ,
3592+ tftuples )
35433593 }
35443594
3595+ predicate stage3maxFanOut = Stage3:: Debug:: maxFanOut / 2 ;
3596+
3597+ predicate stage3maxFanIn = Stage3:: Debug:: maxFanIn / 2 ;
3598+
3599+ predicate stage3maxPathNodes = Stage3:: Debug:: maxPathNodes / 6 ;
3600+
35453601 predicate stageStats4 (
35463602 int n , string stage , int nodes , int fields , int conscand , int states , int tuples ,
35473603 int calledges , int tfnodes , int tftuples
@@ -3550,13 +3606,21 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
35503606 or
35513607 stage = "4 Fwd" and
35523608 n = 40 and
3553- Stage4:: stats ( true , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
3609+ Stage4:: Debug:: stats ( true , nodes , fields , conscand , states , tuples , calledges , tfnodes ,
3610+ tftuples )
35543611 or
35553612 stage = "4 Rev" and
35563613 n = 45 and
3557- Stage4:: stats ( false , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
3614+ Stage4:: Debug:: stats ( false , nodes , fields , conscand , states , tuples , calledges , tfnodes ,
3615+ tftuples )
35583616 }
35593617
3618+ predicate stage4maxFanOut = Stage4:: Debug:: maxFanOut / 2 ;
3619+
3620+ predicate stage4maxFanIn = Stage4:: Debug:: maxFanIn / 2 ;
3621+
3622+ predicate stage4maxPathNodes = Stage4:: Debug:: maxPathNodes / 6 ;
3623+
35603624 predicate stageStats5 (
35613625 int n , string stage , int nodes , int fields , int conscand , int states , int tuples ,
35623626 int calledges , int tfnodes , int tftuples
@@ -3565,13 +3629,21 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
35653629 or
35663630 stage = "5 Fwd" and
35673631 n = 50 and
3568- Stage5:: stats ( true , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
3632+ Stage5:: Debug:: stats ( true , nodes , fields , conscand , states , tuples , calledges , tfnodes ,
3633+ tftuples )
35693634 or
35703635 stage = "5 Rev" and
35713636 n = 55 and
3572- Stage5:: stats ( false , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
3637+ Stage5:: Debug:: stats ( false , nodes , fields , conscand , states , tuples , calledges , tfnodes ,
3638+ tftuples )
35733639 }
35743640
3641+ predicate stage5maxFanOut = Stage5:: Debug:: maxFanOut / 2 ;
3642+
3643+ predicate stage5maxFanIn = Stage5:: Debug:: maxFanIn / 2 ;
3644+
3645+ predicate stage5maxPathNodes = Stage5:: Debug:: maxPathNodes / 6 ;
3646+
35753647 predicate stageStats (
35763648 int n , string stage , int nodes , int fields , int conscand , int states , int tuples ,
35773649 int calledges , int tfnodes , int tftuples
@@ -3580,12 +3652,20 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
35803652 or
35813653 stage = "6 Fwd" and
35823654 n = 60 and
3583- Stage6:: stats ( true , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
3655+ Stage6:: Debug:: stats ( true , nodes , fields , conscand , states , tuples , calledges , tfnodes ,
3656+ tftuples )
35843657 or
35853658 stage = "6 Rev" and
35863659 n = 65 and
3587- Stage6:: stats ( false , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
3660+ Stage6:: Debug:: stats ( false , nodes , fields , conscand , states , tuples , calledges , tfnodes ,
3661+ tftuples )
35883662 }
3663+
3664+ predicate stage6maxFanOut = Stage6:: Debug:: maxFanOut / 2 ;
3665+
3666+ predicate stage6maxFanIn = Stage6:: Debug:: maxFanIn / 2 ;
3667+
3668+ predicate stage6maxPathNodes = Stage6:: Debug:: maxPathNodes / 6 ;
35893669 }
35903670 }
35913671}
0 commit comments