@@ -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,84 @@ 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 , int c ) {
2529+ c = fanOut ( pred ) and
2530+ c = max ( fanOut ( _) ) and
2531+ succ = pred .getASuccessorImpl ( _)
2532+ }
2533+
2534+ predicate maxFanIn ( PathNodeImpl pred , PathNodeImpl succ , int c ) {
2535+ c = fanIn ( succ ) and
2536+ c = max ( fanIn ( _) ) and
2537+ succ = pred .getASuccessorImpl ( _)
2538+ }
2539+
2540+ private int pathNodes ( Nd node ) {
2541+ result =
2542+ strictcount ( Cc cc , SummaryCtx summaryCtx , Typ t , Ap ap , TypOption stored |
2543+ exists ( TPathNodeMid ( node , cc , summaryCtx , t , ap , stored ) )
2544+ )
2545+ }
2546+
2547+ predicate maxPathNodes (
2548+ Nd node , Cc cc , SummaryCtx summaryCtx , Typ t , Ap ap , TypOption stored , int c
2549+ ) {
2550+ exists ( TPathNodeMid ( node , cc , summaryCtx , t , ap , stored ) ) and
2551+ c = pathNodes ( node ) and
2552+ c = max ( pathNodes ( _) )
2553+ }
25112554 }
25122555 /* End: Stage logic. */
25132556 }
@@ -3520,13 +3563,21 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
35203563 or
35213564 stage = "2 Fwd" and
35223565 n = 20 and
3523- Stage2:: stats ( true , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
3566+ Stage2:: Debug:: stats ( true , nodes , fields , conscand , states , tuples , calledges , tfnodes ,
3567+ tftuples )
35243568 or
35253569 stage = "2 Rev" and
35263570 n = 25 and
3527- Stage2:: stats ( false , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
3571+ Stage2:: Debug:: stats ( false , nodes , fields , conscand , states , tuples , calledges , tfnodes ,
3572+ tftuples )
35283573 }
35293574
3575+ predicate stage2maxFanOut = Stage2:: Debug:: maxFanOut / 3 ;
3576+
3577+ predicate stage2maxFanIn = Stage2:: Debug:: maxFanIn / 3 ;
3578+
3579+ predicate stage2maxPathNodes = Stage2:: Debug:: maxPathNodes / 7 ;
3580+
35303581 predicate stageStats3 (
35313582 int n , string stage , int nodes , int fields , int conscand , int states , int tuples ,
35323583 int calledges , int tfnodes , int tftuples
@@ -3535,13 +3586,21 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
35353586 or
35363587 stage = "3 Fwd" and
35373588 n = 30 and
3538- Stage3:: stats ( true , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
3589+ Stage3:: Debug:: stats ( true , nodes , fields , conscand , states , tuples , calledges , tfnodes ,
3590+ tftuples )
35393591 or
35403592 stage = "3 Rev" and
35413593 n = 35 and
3542- Stage3:: stats ( false , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
3594+ Stage3:: Debug:: stats ( false , nodes , fields , conscand , states , tuples , calledges , tfnodes ,
3595+ tftuples )
35433596 }
35443597
3598+ predicate stage3maxFanOut = Stage3:: Debug:: maxFanOut / 3 ;
3599+
3600+ predicate stage3maxFanIn = Stage3:: Debug:: maxFanIn / 3 ;
3601+
3602+ predicate stage3maxPathNodes = Stage3:: Debug:: maxPathNodes / 7 ;
3603+
35453604 predicate stageStats4 (
35463605 int n , string stage , int nodes , int fields , int conscand , int states , int tuples ,
35473606 int calledges , int tfnodes , int tftuples
@@ -3550,13 +3609,21 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
35503609 or
35513610 stage = "4 Fwd" and
35523611 n = 40 and
3553- Stage4:: stats ( true , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
3612+ Stage4:: Debug:: stats ( true , nodes , fields , conscand , states , tuples , calledges , tfnodes ,
3613+ tftuples )
35543614 or
35553615 stage = "4 Rev" and
35563616 n = 45 and
3557- Stage4:: stats ( false , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
3617+ Stage4:: Debug:: stats ( false , nodes , fields , conscand , states , tuples , calledges , tfnodes ,
3618+ tftuples )
35583619 }
35593620
3621+ predicate stage4maxFanOut = Stage4:: Debug:: maxFanOut / 3 ;
3622+
3623+ predicate stage4maxFanIn = Stage4:: Debug:: maxFanIn / 3 ;
3624+
3625+ predicate stage4maxPathNodes = Stage4:: Debug:: maxPathNodes / 7 ;
3626+
35603627 predicate stageStats5 (
35613628 int n , string stage , int nodes , int fields , int conscand , int states , int tuples ,
35623629 int calledges , int tfnodes , int tftuples
@@ -3565,13 +3632,21 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
35653632 or
35663633 stage = "5 Fwd" and
35673634 n = 50 and
3568- Stage5:: stats ( true , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
3635+ Stage5:: Debug:: stats ( true , nodes , fields , conscand , states , tuples , calledges , tfnodes ,
3636+ tftuples )
35693637 or
35703638 stage = "5 Rev" and
35713639 n = 55 and
3572- Stage5:: stats ( false , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
3640+ Stage5:: Debug:: stats ( false , nodes , fields , conscand , states , tuples , calledges , tfnodes ,
3641+ tftuples )
35733642 }
35743643
3644+ predicate stage5maxFanOut = Stage5:: Debug:: maxFanOut / 3 ;
3645+
3646+ predicate stage5maxFanIn = Stage5:: Debug:: maxFanIn / 3 ;
3647+
3648+ predicate stage5maxPathNodes = Stage5:: Debug:: maxPathNodes / 7 ;
3649+
35753650 predicate stageStats (
35763651 int n , string stage , int nodes , int fields , int conscand , int states , int tuples ,
35773652 int calledges , int tfnodes , int tftuples
@@ -3580,12 +3655,20 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
35803655 or
35813656 stage = "6 Fwd" and
35823657 n = 60 and
3583- Stage6:: stats ( true , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
3658+ Stage6:: Debug:: stats ( true , nodes , fields , conscand , states , tuples , calledges , tfnodes ,
3659+ tftuples )
35843660 or
35853661 stage = "6 Rev" and
35863662 n = 65 and
3587- Stage6:: stats ( false , nodes , fields , conscand , states , tuples , calledges , tfnodes , tftuples )
3663+ Stage6:: Debug:: stats ( false , nodes , fields , conscand , states , tuples , calledges , tfnodes ,
3664+ tftuples )
35883665 }
3666+
3667+ predicate stage6maxFanOut = Stage6:: Debug:: maxFanOut / 3 ;
3668+
3669+ predicate stage6maxFanIn = Stage6:: Debug:: maxFanIn / 3 ;
3670+
3671+ predicate stage6maxPathNodes = Stage6:: Debug:: maxPathNodes / 7 ;
35893672 }
35903673 }
35913674}
0 commit comments