@@ -623,13 +623,15 @@ module CFG {
623
623
not cmpl .isNormal ( )
624
624
}
625
625
626
- predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
626
+ predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
627
627
exists ( int i |
628
628
lastNode ( this .getChildTreeRanked ( i ) , pred , normalCompletion ( ) ) and
629
629
firstNode ( this .getChildTreeRanked ( i + 1 ) , succ )
630
630
)
631
631
}
632
632
633
+ predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) { this .succSimple ( pred , succ ) }
634
+
633
635
final ControlFlowTree getChildTreeRanked ( int i ) {
634
636
exists ( int j |
635
637
result = this .getChildTree ( j ) and
@@ -727,8 +729,8 @@ module CFG {
727
729
last = this .getNode ( ) and cmpl = this .getCompletion ( )
728
730
}
729
731
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 )
732
734
or
733
735
lastNode ( this .getLastChildTree ( ) , pred , normalCompletion ( ) ) and
734
736
succ = this .getNode ( )
@@ -750,8 +752,8 @@ module CFG {
750
752
cmpl = Done ( )
751
753
}
752
754
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 )
755
757
or
756
758
pred = this .getNode ( ) and
757
759
firstNode ( this .getFirstChildTree ( ) , succ )
@@ -853,8 +855,8 @@ module CFG {
853
855
cmpl = Done ( )
854
856
}
855
857
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 )
858
860
or
859
861
exists ( int i | lastNode ( this .getLhs ( i ) , pred , normalCompletion ( ) ) |
860
862
firstNode ( this .getLhs ( i + 1 ) , succ )
@@ -978,7 +980,7 @@ module CFG {
978
980
)
979
981
}
980
982
981
- override predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
983
+ override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
982
984
exists ( Completion lcmpl |
983
985
lastNode ( this .getLeftOperand ( ) , pred , lcmpl ) and
984
986
succ = this .getGuard ( lcmpl .getOutcome ( ) )
@@ -1028,11 +1030,11 @@ module CFG {
1028
1030
not result instanceof TypeExpr
1029
1031
}
1030
1032
1031
- override predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1033
+ override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1032
1034
// interpose implicit argument destructuring nodes between last argument
1033
1035
// and call itself; this is for cases like `f(g())` where `g` has multiple
1034
1036
// results
1035
- exists ( ControlFlow:: Node mid | PostOrderTree .super .succ ( pred , mid ) |
1037
+ exists ( ControlFlow:: Node mid | PostOrderTree .super .succSimple ( pred , mid ) |
1036
1038
if mid = this .getNode ( ) then succ = this .getEpilogueNode ( 0 ) else succ = mid
1037
1039
)
1038
1040
or
@@ -1102,8 +1104,8 @@ module CFG {
1102
1104
lastNode ( this .getStmt ( this .getNumStmt ( ) - 1 ) , last , cmpl )
1103
1105
}
1104
1106
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 )
1107
1109
or
1108
1110
exists ( int i |
1109
1111
lastNode ( this .getExpr ( i ) , pred , normalCompletion ( ) ) and
@@ -1172,7 +1174,7 @@ module CFG {
1172
1174
cmpl = Done ( )
1173
1175
}
1174
1176
1175
- override predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1177
+ override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1176
1178
this .firstNode ( pred ) and
1177
1179
succ = this .getElementStart ( 0 )
1178
1180
or
@@ -1250,7 +1252,7 @@ module CFG {
1250
1252
cmpl = Done ( )
1251
1253
}
1252
1254
1253
- override predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1255
+ override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1254
1256
lastNode ( this .getInit ( ) , pred , normalCompletion ( ) ) and
1255
1257
firstNode ( this .getCond ( ) , succ )
1256
1258
or
@@ -1281,7 +1283,7 @@ module CFG {
1281
1283
( cmpl = Done ( ) or cmpl = Panic ( ) )
1282
1284
}
1283
1285
1284
- override predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1286
+ override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1285
1287
lastNode ( this .getBase ( ) , pred , normalCompletion ( ) ) and
1286
1288
(
1287
1289
succ = MkImplicitDeref ( this .getBase ( ) )
@@ -1318,8 +1320,8 @@ module CFG {
1318
1320
1319
1321
override predicate lastNode ( ControlFlow:: Node last , Completion cmpl ) { none ( ) }
1320
1322
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 )
1323
1325
or
1324
1326
pred = MkEntryNode ( this ) and
1325
1327
firstNode ( this .getDecl ( 0 ) , succ )
@@ -1374,7 +1376,7 @@ module CFG {
1374
1376
i = 5 and result = this .getBody ( )
1375
1377
}
1376
1378
1377
- override predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1379
+ override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1378
1380
exists ( int i , ControlFlowTree predTree , Completion cmpl |
1379
1381
predTree = this .getChildTreeRanked ( i ) and
1380
1382
lastNode ( predTree , pred , cmpl ) and
@@ -1440,13 +1442,13 @@ module CFG {
1440
1442
// `defer` can be the first `defer` statement executed
1441
1443
// there is always a predecessor node because the `defer`'s call is always
1442
1444
// evaluated before the defer statement itself
1443
- MkDeferNode ( defer ) = succ ( notDeferSucc * ( this .getEntry ( ) ) )
1445
+ MkDeferNode ( defer ) = succSimple ( notDeferSuccSimple * ( this .getEntry ( ) ) )
1444
1446
)
1445
1447
}
1446
1448
1447
1449
override predicate lastNode ( ControlFlow:: Node last , Completion cmpl ) { none ( ) }
1448
1450
1449
- override predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1451
+ override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1450
1452
exists ( int i |
1451
1453
pred = this .getPrologueNode ( i ) and
1452
1454
succ = this .getPrologueNode ( i + 1 )
@@ -1460,10 +1462,19 @@ module CFG {
1460
1462
firstNode ( ls , succ )
1461
1463
)
1462
1464
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
1463
1474
exists ( Completion cmpl |
1464
1475
lastNode ( this .getBody ( ) , pred , cmpl ) and
1465
1476
// last node of function body can be reached without going through a `defer` statement
1466
- pred = notDeferSucc * ( this .getEntry ( ) )
1477
+ pred = notDeferSuccSimple * ( this .getEntry ( ) )
1467
1478
|
1468
1479
// panic goes directly to exit, non-panic reads result variables first
1469
1480
if cmpl = Panic ( ) then succ = MkExitNode ( this ) else succ = this .getEpilogueNode ( 0 )
@@ -1473,7 +1484,7 @@ module CFG {
1473
1484
exists ( DeferStmt defer | defer = this .getADeferStmt ( ) |
1474
1485
succ = MkExprNode ( defer .getCall ( ) ) and
1475
1486
// the last `DeferStmt` executed before pred is this `defer`
1476
- pred = notDeferSucc * ( MkDeferNode ( defer ) )
1487
+ pred = notDeferSuccSimple * ( MkDeferNode ( defer ) )
1477
1488
)
1478
1489
or
1479
1490
exists ( DeferStmt predDefer , DeferStmt succDefer |
@@ -1494,11 +1505,6 @@ module CFG {
1494
1505
or
1495
1506
succ = this .getEpilogueNode ( 0 )
1496
1507
)
1497
- or
1498
- exists ( int i |
1499
- pred = this .getEpilogueNode ( i ) and
1500
- succ = this .getEpilogueNode ( i + 1 )
1501
- )
1502
1508
}
1503
1509
}
1504
1510
@@ -1516,7 +1522,7 @@ module CFG {
1516
1522
cmpl = Done ( )
1517
1523
}
1518
1524
1519
- override predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1525
+ override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1520
1526
lastNode ( this .getOperand ( ) , pred , normalCompletion ( ) ) and
1521
1527
succ = MkImplicitOne ( this )
1522
1528
or
@@ -1547,7 +1553,7 @@ module CFG {
1547
1553
not cmpl .isNormal ( )
1548
1554
}
1549
1555
1550
- override predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1556
+ override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1551
1557
lastNode ( this .getDomain ( ) , pred , normalCompletion ( ) ) and
1552
1558
succ = MkNextNode ( this )
1553
1559
or
@@ -1622,7 +1628,7 @@ module CFG {
1622
1628
1623
1629
override Completion getCompletion ( ) { result = Return ( ) }
1624
1630
1625
- override predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1631
+ override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1626
1632
exists ( int i |
1627
1633
lastNode ( this .getExpr ( i ) , pred , normalCompletion ( ) ) and
1628
1634
succ = this .complete ( i )
@@ -1678,8 +1684,8 @@ module CFG {
1678
1684
)
1679
1685
}
1680
1686
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 )
1683
1689
or
1684
1690
exists ( CommClause cc , int i , Stmt comm |
1685
1691
cc = this .getNonDefaultCommClause ( i ) and
@@ -1777,7 +1783,7 @@ module CFG {
1777
1783
cmpl = Done ( )
1778
1784
}
1779
1785
1780
- override predicate succ ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1786
+ override predicate succSimple ( ControlFlow:: Node pred , ControlFlow:: Node succ ) {
1781
1787
exists ( int i | pred = this .getStepWithRank ( i ) and succ = this .getStepWithRank ( i + 1 ) )
1782
1788
}
1783
1789
@@ -1814,8 +1820,8 @@ module CFG {
1814
1820
( cmpl = Done ( ) or cmpl = Panic ( ) )
1815
1821
}
1816
1822
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 )
1819
1825
or
1820
1826
not this = any ( CommClause cc ) .getComm ( ) and
1821
1827
lastNode ( this .getValue ( ) , pred , normalCompletion ( ) ) and
@@ -1843,8 +1849,8 @@ module CFG {
1843
1849
( cmpl = Done ( ) or cmpl = Panic ( ) )
1844
1850
}
1845
1851
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 )
1848
1854
or
1849
1855
lastNode ( this .getBase ( ) , pred , normalCompletion ( ) ) and
1850
1856
(
@@ -1930,8 +1936,8 @@ module CFG {
1930
1936
)
1931
1937
}
1932
1938
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 )
1935
1941
or
1936
1942
lastNode ( this .getInit ( ) , pred , normalCompletion ( ) ) and
1937
1943
(
@@ -2004,8 +2010,8 @@ module CFG {
2004
2010
)
2005
2011
}
2006
2012
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 )
2009
2015
or
2010
2016
not this = any ( RecvStmt recv ) .getExpr ( ) and
2011
2017
lastNode ( this .getOperand ( ) , pred , normalCompletion ( ) ) and
@@ -2033,19 +2039,19 @@ module CFG {
2033
2039
}
2034
2040
2035
2041
/** 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 ) {
2037
2043
not result = MkDeferNode ( _) and
2038
- result = succ ( nd )
2044
+ result = succSimple ( nd )
2039
2045
}
2040
2046
2041
2047
/** Gets `defer` statements that can be the first defer statement after `nd` in the CFG */
2042
2048
private ControlFlow:: Node nextDefer ( ControlFlow:: Node nd ) {
2043
2049
nd = MkDeferNode ( _) and
2044
2050
result = MkDeferNode ( _) and
2045
2051
(
2046
- result = succ ( nd )
2052
+ result = succSimple ( nd )
2047
2053
or
2048
- result = succ ( notDeferSucc + ( nd ) )
2054
+ result = succSimple ( notDeferSuccSimple + ( nd ) )
2049
2055
)
2050
2056
}
2051
2057
@@ -2074,6 +2080,12 @@ module CFG {
2074
2080
)
2075
2081
}
2076
2082
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
+
2077
2089
/** Gets a successor of `nd`, that is, a node that is executed after `nd`. */
2078
2090
cached
2079
2091
ControlFlow:: Node succ ( ControlFlow:: Node nd ) { any ( ControlFlowTree tree ) .succ ( nd , result ) }
0 commit comments