@@ -623,13 +623,15 @@ module CFG {
623623 not cmpl .isNormal ( )
624624 }
625625
626- predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
626+ predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
627627 exists ( int i |
628628 lastNode ( this .getChildTreeRanked ( i ) , pred , normalCompletion ( ) ) and
629629 firstNode ( this .getChildTreeRanked ( i + 1 ) , succ )
630630 )
631631 }
632632
633+ predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) { this .succSimple ( pred , succ ) }
634+
633635 final ControlFlowTree getChildTreeRanked ( int i ) {
634636 exists ( int j |
635637 result = this .getChildTree ( j ) and
@@ -727,8 +729,8 @@ module CFG {
727729 last = this .getNode ( ) and cmpl = this .getCompletion ( )
728730 }
729731
730- override predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
731- super .succ ( pred , succ )
732+ override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
733+ super .succSimple ( pred , succ )
732734 or
733735 lastNode ( this .getLastChildTree ( ) , pred , normalCompletion ( ) ) and
734736 succ = this .getNode ( )
@@ -750,8 +752,8 @@ module CFG {
750752 cmpl = Done ( )
751753 }
752754
753- override predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
754- super .succ ( pred , succ )
755+ override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
756+ super .succSimple ( pred , succ )
755757 or
756758 pred = this .getNode ( ) and
757759 firstNode ( this .getFirstChildTree ( ) , succ )
@@ -853,8 +855,8 @@ module CFG {
853855 cmpl = Done ( )
854856 }
855857
856- override predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
857- ControlFlowTree .super .succ ( pred , succ )
858+ override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
859+ ControlFlowTree .super .succSimple ( pred , succ )
858860 or
859861 exists ( int i | lastNode ( this .getLhs ( i ) , pred , normalCompletion ( ) ) |
860862 firstNode ( this .getLhs ( i + 1 ) , succ )
@@ -978,7 +980,7 @@ module CFG {
978980 )
979981 }
980982
981- override predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
983+ override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
982984 exists ( Completion lcmpl |
983985 lastNode ( this .getLeftOperand ( ) , pred , lcmpl ) and
984986 succ = this .getGuard ( lcmpl .getOutcome ( ) )
@@ -1028,11 +1030,11 @@ module CFG {
10281030 not result instanceof TypeExpr
10291031 }
10301032
1031- override predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1033+ override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
10321034 // interpose implicit argument destructuring nodes between last argument
10331035 // and call itself; this is for cases like `f(g())` where `g` has multiple
10341036 // results
1035- exists ( ControlFlow:: Node mid | PostOrderTree .super .succ ( pred , mid ) |
1037+ exists ( ControlFlow:: Node mid | PostOrderTree .super .succSimple ( pred , mid ) |
10361038 if mid = this .getNode ( ) then succ = this .getEpilogueNode ( 0 ) else succ = mid
10371039 )
10381040 or
@@ -1102,8 +1104,8 @@ module CFG {
11021104 lastNode ( this .getStmt ( this .getNumStmt ( ) - 1 ) , last , cmpl )
11031105 }
11041106
1105- override predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1106- ControlFlowTree .super .succ ( pred , succ )
1107+ override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1108+ ControlFlowTree .super .succSimple ( pred , succ )
11071109 or
11081110 exists ( int i |
11091111 lastNode ( this .getExpr ( i ) , pred , normalCompletion ( ) ) and
@@ -1172,7 +1174,7 @@ module CFG {
11721174 cmpl = Done ( )
11731175 }
11741176
1175- override predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1177+ override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
11761178 this .firstNode ( pred ) and
11771179 succ = this .getElementStart ( 0 )
11781180 or
@@ -1250,7 +1252,7 @@ module CFG {
12501252 cmpl = Done ( )
12511253 }
12521254
1253- override predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1255+ override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
12541256 lastNode ( this .getInit ( ) , pred , normalCompletion ( ) ) and
12551257 firstNode ( this .getCond ( ) , succ )
12561258 or
@@ -1281,7 +1283,7 @@ module CFG {
12811283 ( cmpl = Done ( ) or cmpl = Panic ( ) )
12821284 }
12831285
1284- override predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1286+ override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
12851287 lastNode ( this .getBase ( ) , pred , normalCompletion ( ) ) and
12861288 (
12871289 succ = MkImplicitDeref ( this .getBase ( ) )
@@ -1318,8 +1320,8 @@ module CFG {
13181320
13191321 override predicate lastNode ( ControlFlow:: Node last , Completion cmpl ) { none ( ) }
13201322
1321- override predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1322- ControlFlowTree .super .succ ( pred , succ )
1323+ override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1324+ ControlFlowTree .super .succSimple ( pred , succ )
13231325 or
13241326 pred = MkEntryNode ( this ) and
13251327 firstNode ( this .getDecl ( 0 ) , succ )
@@ -1374,7 +1376,7 @@ module CFG {
13741376 i = 5 and result = this .getBody ( )
13751377 }
13761378
1377- override predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1379+ override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
13781380 exists ( int i , ControlFlowTree predTree , Completion cmpl |
13791381 predTree = this .getChildTreeRanked ( i ) and
13801382 lastNode ( predTree , pred , cmpl ) and
@@ -1440,13 +1442,13 @@ module CFG {
14401442 // `defer` can be the first `defer` statement executed
14411443 // there is always a predecessor node because the `defer`'s call is always
14421444 // evaluated before the defer statement itself
1443- MkDeferNode ( defer ) = succ ( notDeferSucc * ( this .getEntry ( ) ) )
1445+ MkDeferNode ( defer ) = succSimple ( notDeferSuccSimple * ( this .getEntry ( ) ) )
14441446 )
14451447 }
14461448
14471449 override predicate lastNode ( ControlFlow:: Node last , Completion cmpl ) { none ( ) }
14481450
1449- override predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1451+ override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
14501452 exists ( int i |
14511453 pred = this .getPrologueNode ( i ) and
14521454 succ = this .getPrologueNode ( i + 1 )
@@ -1460,10 +1462,19 @@ module CFG {
14601462 firstNode ( ls , succ )
14611463 )
14621464 or
1465+ exists ( int i |
1466+ pred = this .getEpilogueNode ( i ) and
1467+ succ = this .getEpilogueNode ( i + 1 )
1468+ )
1469+ }
1470+
1471+ override predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1472+ this .succSimple ( pred , succ )
1473+ or
14631474 exists ( Completion cmpl |
14641475 lastNode ( this .getBody ( ) , pred , cmpl ) and
14651476 // last node of function body can be reached without going through a `defer` statement
1466- pred = notDeferSucc * ( this .getEntry ( ) )
1477+ pred = notDeferSuccSimple * ( this .getEntry ( ) )
14671478 |
14681479 // panic goes directly to exit, non-panic reads result variables first
14691480 if cmpl = Panic ( ) then succ = MkExitNode ( this ) else succ = this .getEpilogueNode ( 0 )
@@ -1473,7 +1484,7 @@ module CFG {
14731484 exists ( DeferStmt defer | defer = this .getADeferStmt ( ) |
14741485 succ = MkExprNode ( defer .getCall ( ) ) and
14751486 // the last `DeferStmt` executed before pred is this `defer`
1476- pred = notDeferSucc * ( MkDeferNode ( defer ) )
1487+ pred = notDeferSuccSimple * ( MkDeferNode ( defer ) )
14771488 )
14781489 or
14791490 exists ( DeferStmt predDefer , DeferStmt succDefer |
@@ -1494,11 +1505,6 @@ module CFG {
14941505 or
14951506 succ = this .getEpilogueNode ( 0 )
14961507 )
1497- or
1498- exists ( int i |
1499- pred = this .getEpilogueNode ( i ) and
1500- succ = this .getEpilogueNode ( i + 1 )
1501- )
15021508 }
15031509 }
15041510
@@ -1516,7 +1522,7 @@ module CFG {
15161522 cmpl = Done ( )
15171523 }
15181524
1519- override predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1525+ override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
15201526 lastNode ( this .getOperand ( ) , pred , normalCompletion ( ) ) and
15211527 succ = MkImplicitOne ( this )
15221528 or
@@ -1547,7 +1553,7 @@ module CFG {
15471553 not cmpl .isNormal ( )
15481554 }
15491555
1550- override predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1556+ override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
15511557 lastNode ( this .getDomain ( ) , pred , normalCompletion ( ) ) and
15521558 succ = MkNextNode ( this )
15531559 or
@@ -1622,7 +1628,7 @@ module CFG {
16221628
16231629 override Completion getCompletion ( ) { result = Return ( ) }
16241630
1625- override predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1631+ override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
16261632 exists ( int i |
16271633 lastNode ( this .getExpr ( i ) , pred , normalCompletion ( ) ) and
16281634 succ = this .complete ( i )
@@ -1678,8 +1684,8 @@ module CFG {
16781684 )
16791685 }
16801686
1681- override predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1682- ControlFlowTree .super .succ ( pred , succ )
1687+ override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1688+ ControlFlowTree .super .succSimple ( pred , succ )
16831689 or
16841690 exists ( CommClause cc , int i , Stmt comm |
16851691 cc = this .getNonDefaultCommClause ( i ) and
@@ -1777,7 +1783,7 @@ module CFG {
17771783 cmpl = Done ( )
17781784 }
17791785
1780- override predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1786+ override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
17811787 exists ( int i | pred = this .getStepWithRank ( i ) and succ = this .getStepWithRank ( i + 1 ) )
17821788 }
17831789
@@ -1814,8 +1820,8 @@ module CFG {
18141820 ( cmpl = Done ( ) or cmpl = Panic ( ) )
18151821 }
18161822
1817- override predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1818- ControlFlowTree .super .succ ( pred , succ )
1823+ override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1824+ ControlFlowTree .super .succSimple ( pred , succ )
18191825 or
18201826 not this = any ( CommClause cc ) .getComm ( ) and
18211827 lastNode ( this .getValue ( ) , pred , normalCompletion ( ) ) and
@@ -1843,8 +1849,8 @@ module CFG {
18431849 ( cmpl = Done ( ) or cmpl = Panic ( ) )
18441850 }
18451851
1846- override predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1847- ControlFlowTree .super .succ ( pred , succ )
1852+ override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1853+ ControlFlowTree .super .succSimple ( pred , succ )
18481854 or
18491855 lastNode ( this .getBase ( ) , pred , normalCompletion ( ) ) and
18501856 (
@@ -1930,8 +1936,8 @@ module CFG {
19301936 )
19311937 }
19321938
1933- override predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1934- ControlFlowTree .super .succ ( pred , succ )
1939+ override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1940+ ControlFlowTree .super .succSimple ( pred , succ )
19351941 or
19361942 lastNode ( this .getInit ( ) , pred , normalCompletion ( ) ) and
19371943 (
@@ -2004,8 +2010,8 @@ module CFG {
20042010 )
20052011 }
20062012
2007- override predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
2008- ControlFlowTree .super .succ ( pred , succ )
2013+ override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
2014+ ControlFlowTree .super .succSimple ( pred , succ )
20092015 or
20102016 not this = any ( RecvStmt recv ) .getExpr ( ) and
20112017 lastNode ( this .getOperand ( ) , pred , normalCompletion ( ) ) and
@@ -2033,19 +2039,19 @@ module CFG {
20332039 }
20342040
20352041 /** Gets a successor of `nd` that is not a `defer` node */
2036- private ControlFlow:: Node notDeferSucc ( ControlFlow:: Node nd ) {
2042+ private ControlFlow:: Node notDeferSuccSimple ( ControlFlow:: Node nd ) {
20372043 not result = MkDeferNode ( _) and
2038- result = succ ( nd )
2044+ result = succSimple ( nd )
20392045 }
20402046
20412047 /** Gets `defer` statements that can be the first defer statement after `nd` in the CFG */
20422048 private ControlFlow:: Node nextDefer ( ControlFlow:: Node nd ) {
20432049 nd = MkDeferNode ( _) and
20442050 result = MkDeferNode ( _) and
20452051 (
2046- result = succ ( nd )
2052+ result = succSimple ( nd )
20472053 or
2048- result = succ ( notDeferSucc + ( nd ) )
2054+ result = succSimple ( notDeferSuccSimple + ( nd ) )
20492055 )
20502056 }
20512057
@@ -2074,6 +2080,12 @@ module CFG {
20742080 )
20752081 }
20762082
2083+ /** Gets a successor of `nd`, that is, a node that is executed after `nd`. */
2084+ cached
2085+ ControlFlow:: Node succSimple ( ControlFlow:: Node nd ) {
2086+ any ( ControlFlowTree tree ) .succSimple ( nd , result )
2087+ }
2088+
20772089 /** Gets a successor of `nd`, that is, a node that is executed after `nd`. */
20782090 cached
20792091 ControlFlow:: Node succ ( ControlFlow:: Node nd ) { any ( ControlFlowTree tree ) .succ ( nd , result ) }
0 commit comments