Skip to content

Commit 6f9242b

Browse files
owen-mcowen-mc
authored
Merge pull request #15162 from owen-mc/go/stratify-cfg-succ
Go: Stratify `CFG::succ` to avoid recursion
2 parents 682aef9 + e2e91eb commit 6f9242b

File tree

1 file changed

+87
-45
lines changed

1 file changed

+87
-45
lines changed

‎go/ql/lib/semmle/go/controlflow/ControlFlowGraphImpl.qll

Lines changed: 87 additions & 45 deletions
Original file line numberDiff line numberDiff line change
@@ -623,13 +623,21 @@ module CFG {
623623
not cmpl.isNormal()
624624
}
625625

626-
predicate succ(ControlFlow::Node pred, ControlFlow::Node succ) {
626+
/**
627+
* Holds if `succ` is a successor of `pred`, ignoring the execution of any
628+
* deferred functions when a function ends.
629+
*/
630+
pragma[nomagic]
631+
predicate succ0(ControlFlow::Node pred, ControlFlow::Node succ) {
627632
exists(int i |
628633
lastNode(this.getChildTreeRanked(i), pred, normalCompletion()) and
629634
firstNode(this.getChildTreeRanked(i + 1), succ)
630635
)
631636
}
632637

638+
/** Holds if `succ` is a successor of `pred`. */
639+
predicate succ(ControlFlow::Node pred, ControlFlow::Node succ) { this.succ0(pred, succ) }
640+
633641
final ControlFlowTree getChildTreeRanked(int i) {
634642
exists(int j |
635643
result = this.getChildTree(j) and
@@ -727,8 +735,9 @@ module CFG {
727735
last = this.getNode() and cmpl = this.getCompletion()
728736
}
729737

730-
override predicate succ(ControlFlow::Node pred, ControlFlow::Node succ) {
731-
super.succ(pred, succ)
738+
pragma[nomagic]
739+
override predicate succ0(ControlFlow::Node pred, ControlFlow::Node succ) {
740+
super.succ0(pred, succ)
732741
or
733742
lastNode(this.getLastChildTree(), pred, normalCompletion()) and
734743
succ = this.getNode()
@@ -750,8 +759,9 @@ module CFG {
750759
cmpl = Done()
751760
}
752761

753-
override predicate succ(ControlFlow::Node pred, ControlFlow::Node succ) {
754-
super.succ(pred, succ)
762+
pragma[nomagic]
763+
override predicate succ0(ControlFlow::Node pred, ControlFlow::Node succ) {
764+
super.succ0(pred, succ)
755765
or
756766
pred = this.getNode() and
757767
firstNode(this.getFirstChildTree(), succ)
@@ -853,8 +863,9 @@ module CFG {
853863
cmpl = Done()
854864
}
855865

856-
override predicate succ(ControlFlow::Node pred, ControlFlow::Node succ) {
857-
ControlFlowTree.super.succ(pred, succ)
866+
pragma[nomagic]
867+
override predicate succ0(ControlFlow::Node pred, ControlFlow::Node succ) {
868+
ControlFlowTree.super.succ0(pred, succ)
858869
or
859870
exists(int i | lastNode(this.getLhs(i), pred, normalCompletion()) |
860871
firstNode(this.getLhs(i + 1), succ)
@@ -978,7 +989,8 @@ module CFG {
978989
)
979990
}
980991

981-
override predicate succ(ControlFlow::Node pred, ControlFlow::Node succ) {
992+
pragma[nomagic]
993+
override predicate succ0(ControlFlow::Node pred, ControlFlow::Node succ) {
982994
exists(Completion lcmpl |
983995
lastNode(this.getLeftOperand(), pred, lcmpl) and
984996
succ = this.getGuard(lcmpl.getOutcome())
@@ -1028,11 +1040,12 @@ module CFG {
10281040
not result instanceof TypeExpr
10291041
}
10301042

1031-
override predicate succ(ControlFlow::Node pred, ControlFlow::Node succ) {
1043+
pragma[nomagic]
1044+
override predicate succ0(ControlFlow::Node pred, ControlFlow::Node succ) {
10321045
// interpose implicit argument destructuring nodes between last argument
10331046
// and call itself; this is for cases like `f(g())` where `g` has multiple
10341047
// results
1035-
exists(ControlFlow::Node mid | PostOrderTree.super.succ(pred, mid) |
1048+
exists(ControlFlow::Node mid | PostOrderTree.super.succ0(pred, mid) |
10361049
if mid = this.getNode() then succ = this.getEpilogueNode(0) else succ = mid
10371050
)
10381051
or
@@ -1102,8 +1115,9 @@ module CFG {
11021115
lastNode(this.getStmt(this.getNumStmt() - 1), last, cmpl)
11031116
}
11041117

1105-
override predicate succ(ControlFlow::Node pred, ControlFlow::Node succ) {
1106-
ControlFlowTree.super.succ(pred, succ)
1118+
pragma[nomagic]
1119+
override predicate succ0(ControlFlow::Node pred, ControlFlow::Node succ) {
1120+
ControlFlowTree.super.succ0(pred, succ)
11071121
or
11081122
exists(int i |
11091123
lastNode(this.getExpr(i), pred, normalCompletion()) and
@@ -1172,7 +1186,8 @@ module CFG {
11721186
cmpl = Done()
11731187
}
11741188

1175-
override predicate succ(ControlFlow::Node pred, ControlFlow::Node succ) {
1189+
pragma[nomagic]
1190+
override predicate succ0(ControlFlow::Node pred, ControlFlow::Node succ) {
11761191
this.firstNode(pred) and
11771192
succ = this.getElementStart(0)
11781193
or
@@ -1250,7 +1265,8 @@ module CFG {
12501265
cmpl = Done()
12511266
}
12521267

1253-
override predicate succ(ControlFlow::Node pred, ControlFlow::Node succ) {
1268+
pragma[nomagic]
1269+
override predicate succ0(ControlFlow::Node pred, ControlFlow::Node succ) {
12541270
lastNode(this.getInit(), pred, normalCompletion()) and
12551271
firstNode(this.getCond(), succ)
12561272
or
@@ -1281,7 +1297,8 @@ module CFG {
12811297
(cmpl = Done() or cmpl = Panic())
12821298
}
12831299

1284-
override predicate succ(ControlFlow::Node pred, ControlFlow::Node succ) {
1300+
pragma[nomagic]
1301+
override predicate succ0(ControlFlow::Node pred, ControlFlow::Node succ) {
12851302
lastNode(this.getBase(), pred, normalCompletion()) and
12861303
(
12871304
succ = MkImplicitDeref(this.getBase())
@@ -1318,8 +1335,9 @@ module CFG {
13181335

13191336
override predicate lastNode(ControlFlow::Node last, Completion cmpl) { none() }
13201337

1321-
override predicate succ(ControlFlow::Node pred, ControlFlow::Node succ) {
1322-
ControlFlowTree.super.succ(pred, succ)
1338+
pragma[nomagic]
1339+
override predicate succ0(ControlFlow::Node pred, ControlFlow::Node succ) {
1340+
ControlFlowTree.super.succ0(pred, succ)
13231341
or
13241342
pred = MkEntryNode(this) and
13251343
firstNode(this.getDecl(0), succ)
@@ -1374,7 +1392,8 @@ module CFG {
13741392
i = 5 and result = this.getBody()
13751393
}
13761394

1377-
override predicate succ(ControlFlow::Node pred, ControlFlow::Node succ) {
1395+
pragma[nomagic]
1396+
override predicate succ0(ControlFlow::Node pred, ControlFlow::Node succ) {
13781397
exists(int i, ControlFlowTree predTree, Completion cmpl |
13791398
predTree = this.getChildTreeRanked(i) and
13801399
lastNode(predTree, pred, cmpl) and
@@ -1440,13 +1459,14 @@ module CFG {
14401459
// `defer` can be the first `defer` statement executed
14411460
// there is always a predecessor node because the `defer`'s call is always
14421461
// evaluated before the defer statement itself
1443-
MkDeferNode(defer) = succ(notDeferSucc*(this.getEntry()))
1462+
MkDeferNode(defer) = succ0(notDeferSucc0*(this.getEntry()))
14441463
)
14451464
}
14461465

14471466
override predicate lastNode(ControlFlow::Node last, Completion cmpl) { none() }
14481467

1449-
override predicate succ(ControlFlow::Node pred, ControlFlow::Node succ) {
1468+
pragma[nomagic]
1469+
override predicate succ0(ControlFlow::Node pred, ControlFlow::Node succ) {
14501470
exists(int i |
14511471
pred = this.getPrologueNode(i) and
14521472
succ = this.getPrologueNode(i + 1)
@@ -1460,10 +1480,19 @@ module CFG {
14601480
firstNode(ls, succ)
14611481
)
14621482
or
1483+
exists(int i |
1484+
pred = this.getEpilogueNode(i) and
1485+
succ = this.getEpilogueNode(i + 1)
1486+
)
1487+
}
1488+
1489+
override predicate succ(ControlFlow::Node pred, ControlFlow::Node succ) {
1490+
this.succ0(pred, succ)
1491+
or
14631492
exists(Completion cmpl |
14641493
lastNode(this.getBody(), pred, cmpl) and
14651494
// last node of function body can be reached without going through a `defer` statement
1466-
pred = notDeferSucc*(this.getEntry())
1495+
pred = notDeferSucc0*(this.getEntry())
14671496
|
14681497
// panic goes directly to exit, non-panic reads result variables first
14691498
if cmpl = Panic() then succ = MkExitNode(this) else succ = this.getEpilogueNode(0)
@@ -1473,7 +1502,7 @@ module CFG {
14731502
exists(DeferStmt defer | defer = this.getADeferStmt() |
14741503
succ = MkExprNode(defer.getCall()) and
14751504
// the last `DeferStmt` executed before pred is this `defer`
1476-
pred = notDeferSucc*(MkDeferNode(defer))
1505+
pred = notDeferSucc0*(MkDeferNode(defer))
14771506
)
14781507
or
14791508
exists(DeferStmt predDefer, DeferStmt succDefer |
@@ -1494,11 +1523,6 @@ module CFG {
14941523
or
14951524
succ = this.getEpilogueNode(0)
14961525
)
1497-
or
1498-
exists(int i |
1499-
pred = this.getEpilogueNode(i) and
1500-
succ = this.getEpilogueNode(i + 1)
1501-
)
15021526
}
15031527
}
15041528

@@ -1516,7 +1540,8 @@ module CFG {
15161540
cmpl = Done()
15171541
}
15181542

1519-
override predicate succ(ControlFlow::Node pred, ControlFlow::Node succ) {
1543+
pragma[nomagic]
1544+
override predicate succ0(ControlFlow::Node pred, ControlFlow::Node succ) {
15201545
lastNode(this.getOperand(), pred, normalCompletion()) and
15211546
succ = MkImplicitOne(this)
15221547
or
@@ -1547,7 +1572,8 @@ module CFG {
15471572
not cmpl.isNormal()
15481573
}
15491574

1550-
override predicate succ(ControlFlow::Node pred, ControlFlow::Node succ) {
1575+
pragma[nomagic]
1576+
override predicate succ0(ControlFlow::Node pred, ControlFlow::Node succ) {
15511577
lastNode(this.getDomain(), pred, normalCompletion()) and
15521578
succ = MkNextNode(this)
15531579
or
@@ -1622,7 +1648,8 @@ module CFG {
16221648

16231649
override Completion getCompletion() { result = Return() }
16241650

1625-
override predicate succ(ControlFlow::Node pred, ControlFlow::Node succ) {
1651+
pragma[nomagic]
1652+
override predicate succ0(ControlFlow::Node pred, ControlFlow::Node succ) {
16261653
exists(int i |
16271654
lastNode(this.getExpr(i), pred, normalCompletion()) and
16281655
succ = this.complete(i)
@@ -1678,8 +1705,9 @@ module CFG {
16781705
)
16791706
}
16801707

1681-
override predicate succ(ControlFlow::Node pred, ControlFlow::Node succ) {
1682-
ControlFlowTree.super.succ(pred, succ)
1708+
pragma[nomagic]
1709+
override predicate succ0(ControlFlow::Node pred, ControlFlow::Node succ) {
1710+
ControlFlowTree.super.succ0(pred, succ)
16831711
or
16841712
exists(CommClause cc, int i, Stmt comm |
16851713
cc = this.getNonDefaultCommClause(i) and
@@ -1777,7 +1805,8 @@ module CFG {
17771805
cmpl = Done()
17781806
}
17791807

1780-
override predicate succ(ControlFlow::Node pred, ControlFlow::Node succ) {
1808+
pragma[nomagic]
1809+
override predicate succ0(ControlFlow::Node pred, ControlFlow::Node succ) {
17811810
exists(int i | pred = this.getStepWithRank(i) and succ = this.getStepWithRank(i + 1))
17821811
}
17831812

@@ -1814,8 +1843,9 @@ module CFG {
18141843
(cmpl = Done() or cmpl = Panic())
18151844
}
18161845

1817-
override predicate succ(ControlFlow::Node pred, ControlFlow::Node succ) {
1818-
ControlFlowTree.super.succ(pred, succ)
1846+
pragma[nomagic]
1847+
override predicate succ0(ControlFlow::Node pred, ControlFlow::Node succ) {
1848+
ControlFlowTree.super.succ0(pred, succ)
18191849
or
18201850
not this = any(CommClause cc).getComm() and
18211851
lastNode(this.getValue(), pred, normalCompletion()) and
@@ -1843,8 +1873,9 @@ module CFG {
18431873
(cmpl = Done() or cmpl = Panic())
18441874
}
18451875

1846-
override predicate succ(ControlFlow::Node pred, ControlFlow::Node succ) {
1847-
ControlFlowTree.super.succ(pred, succ)
1876+
pragma[nomagic]
1877+
override predicate succ0(ControlFlow::Node pred, ControlFlow::Node succ) {
1878+
ControlFlowTree.super.succ0(pred, succ)
18481879
or
18491880
lastNode(this.getBase(), pred, normalCompletion()) and
18501881
(
@@ -1930,8 +1961,9 @@ module CFG {
19301961
)
19311962
}
19321963

1933-
override predicate succ(ControlFlow::Node pred, ControlFlow::Node succ) {
1934-
ControlFlowTree.super.succ(pred, succ)
1964+
pragma[nomagic]
1965+
override predicate succ0(ControlFlow::Node pred, ControlFlow::Node succ) {
1966+
ControlFlowTree.super.succ0(pred, succ)
19351967
or
19361968
lastNode(this.getInit(), pred, normalCompletion()) and
19371969
(
@@ -2004,8 +2036,9 @@ module CFG {
20042036
)
20052037
}
20062038

2007-
override predicate succ(ControlFlow::Node pred, ControlFlow::Node succ) {
2008-
ControlFlowTree.super.succ(pred, succ)
2039+
pragma[nomagic]
2040+
override predicate succ0(ControlFlow::Node pred, ControlFlow::Node succ) {
2041+
ControlFlowTree.super.succ0(pred, succ)
20092042
or
20102043
not this = any(RecvStmt recv).getExpr() and
20112044
lastNode(this.getOperand(), pred, normalCompletion()) and
@@ -2033,19 +2066,19 @@ module CFG {
20332066
}
20342067

20352068
/** Gets a successor of `nd` that is not a `defer` node */
2036-
private ControlFlow::Node notDeferSucc(ControlFlow::Node nd) {
2069+
private ControlFlow::Node notDeferSucc0(ControlFlow::Node nd) {
20372070
not result = MkDeferNode(_) and
2038-
result = succ(nd)
2071+
result = succ0(nd)
20392072
}
20402073

20412074
/** Gets `defer` statements that can be the first defer statement after `nd` in the CFG */
20422075
private ControlFlow::Node nextDefer(ControlFlow::Node nd) {
20432076
nd = MkDeferNode(_) and
20442077
result = MkDeferNode(_) and
20452078
(
2046-
result = succ(nd)
2079+
result = succ0(nd)
20472080
or
2048-
result = succ(notDeferSucc+(nd))
2081+
result = succ0(notDeferSucc0+(nd))
20492082
)
20502083
}
20512084

@@ -2074,6 +2107,15 @@ module CFG {
20742107
)
20752108
}
20762109

2110+
/**
2111+
* Gets a successor of `nd`, that is, a node that is executed after `nd`,
2112+
* ignoring the execution of any deferred functions when a function ends.
2113+
*/
2114+
pragma[nomagic]
2115+
private ControlFlow::Node succ0(ControlFlow::Node nd) {
2116+
any(ControlFlowTree tree).succ0(nd, result)
2117+
}
2118+
20772119
/** Gets a successor of `nd`, that is, a node that is executed after `nd`. */
20782120
cached
20792121
ControlFlow::Node succ(ControlFlow::Node nd) { any(ControlFlowTree tree).succ(nd, result) }

0 commit comments

Comments
 (0)