Skip to content

Commit f2ca52d

Browse files
committed
Java/C++: Move range util backEdge predicate to shared pack.
1 parent 8d3ed68 commit f2ca52d

File tree

8 files changed

+58
-61
lines changed

8 files changed

+58
-61
lines changed

cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticCFG.qll

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -12,9 +12,6 @@ class SemBasicBlock extends Specific::BasicBlock {
1212
/** Holds if this block (transitively) dominates `otherblock`. */
1313
final predicate bbDominates(SemBasicBlock otherBlock) { Specific::bbDominates(this, otherBlock) }
1414

15-
/** Holds if this block has dominance information. */
16-
final predicate hasDominanceInformation() { Specific::hasDominanceInformation(this) }
17-
1815
/** Gets an expression that is evaluated in this basic block. */
1916
final SemExpr getAnExpr() { result.getBasicBlock() = this }
2017

cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticExprSpecific.qll

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -199,8 +199,6 @@ module SemanticExprConfig {
199199
dominator.dominates(dominated)
200200
}
201201

202-
predicate hasDominanceInformation(BasicBlock block) { any() }
203-
204202
private predicate id(Cpp::Locatable x, Cpp::Locatable y) { x = y }
205203

206204
private predicate idOf(Cpp::Locatable x, int y) = equivalenceRelation(id/2)(x, y)

cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticSSA.qll

Lines changed: 0 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -63,36 +63,3 @@ class SemSsaReadPositionBlock extends SemSsaReadPosition {
6363

6464
SemExpr getAnExpr() { result = this.getBlock().getAnExpr() }
6565
}
66-
67-
/**
68-
* Holds if `inp` is an input to `phi` along a back edge.
69-
*/
70-
predicate semBackEdge(SemSsaPhiNode phi, SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge) {
71-
edge.phiInput(phi, inp) and
72-
// Conservatively assume that every edge is a back edge if we don't have dominance information.
73-
(
74-
phi.getBasicBlock().bbDominates(edge.getOrigBlock()) or
75-
irreducibleSccEdge(edge.getOrigBlock(), phi.getBasicBlock()) or
76-
not edge.getOrigBlock().hasDominanceInformation()
77-
)
78-
}
79-
80-
/**
81-
* Holds if the edge from b1 to b2 is part of a multiple-entry cycle in an irreducible control flow
82-
* graph.
83-
*
84-
* An ireducible control flow graph is one where the usual dominance-based back edge detection does
85-
* not work, because there is a cycle with multiple entry points, meaning there are
86-
* mutually-reachable basic blocks where neither dominates the other. For such a graph, we first
87-
* remove all detectable back-edges using the normal condition that the predecessor block is
88-
* dominated by the successor block, then mark all edges in a cycle in the resulting graph as back
89-
* edges.
90-
*/
91-
private predicate irreducibleSccEdge(SemBasicBlock b1, SemBasicBlock b2) {
92-
trimmedEdge(b1, b2) and trimmedEdge+(b2, b1)
93-
}
94-
95-
private predicate trimmedEdge(SemBasicBlock pred, SemBasicBlock succ) {
96-
pred.getASuccessor() = succ and
97-
not succ.bbDominates(pred)
98-
}

cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisImpl.qll

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -72,6 +72,8 @@ module Sem implements Semantic {
7272

7373
class BasicBlock = SemBasicBlock;
7474

75+
BasicBlock getABasicBlockSuccessor(BasicBlock bb) { result = bb.getASuccessor() }
76+
7577
class Guard = SemGuard;
7678

7779
predicate implies_v2 = semImplies_v2/4;
@@ -100,8 +102,6 @@ module Sem implements Semantic {
100102

101103
class SsaReadPositionBlock = SemSsaReadPositionBlock;
102104

103-
predicate backEdge = semBackEdge/3;
104-
105105
predicate conversionCannotOverflow(Type fromType, Type toType) {
106106
SemanticType::conversionCannotOverflow(fromType, toType)
107107
}

java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -211,7 +211,11 @@ module Sem implements Semantic {
211211

212212
class BasicBlock = J::BasicBlock;
213213

214-
class Guard extends GL::Guard {
214+
BasicBlock getABasicBlockSuccessor(BasicBlock bb) { result = bb.getABBSuccessor() }
215+
216+
final private class FinalGuard = GL::Guard;
217+
218+
class Guard extends FinalGuard {
215219
Expr asExpr() { result = this }
216220
}
217221

@@ -261,17 +265,15 @@ module Sem implements Semantic {
261265

262266
class SsaReadPositionPhiInputEdge extends SsaReadPosition instanceof SsaReadPos::SsaReadPositionPhiInputEdge
263267
{
268+
BasicBlock getOrigBlock() { result = super.getOrigBlock() }
269+
264270
predicate phiInput(SsaPhiNode phi, SsaVariable inp) { super.phiInput(phi, inp) }
265271
}
266272

267273
class SsaReadPositionBlock extends SsaReadPosition instanceof SsaReadPos::SsaReadPositionBlock {
268274
BasicBlock getBlock() { result = super.getBlock() }
269275
}
270276

271-
predicate backEdge(SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge) {
272-
RU::backEdge(phi, inp, edge)
273-
}
274-
275277
predicate conversionCannotOverflow = safeCast/2;
276278
}
277279

java/ql/lib/semmle/code/java/dataflow/RangeUtils.qll

Lines changed: 4 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,10 @@ private import SSA
77
private import semmle.code.java.controlflow.internal.GuardsLogic
88
private import semmle.code.java.dataflow.internal.rangeanalysis.SsaReadPositionCommon
99
private import semmle.code.java.Constants
10+
private import semmle.code.java.dataflow.RangeAnalysis
11+
private import codeql.rangeanalysis.internal.RangeUtils
12+
13+
private predicate backEdge = MakeUtils<Sem, IntDelta>::backEdge/3;
1014

1115
/**
1216
* Holds if `v` is an input to `phi` that is not along a back edge, and the
@@ -181,18 +185,6 @@ Expr ssaRead(SsaVariable v, int delta) {
181185
result.(AssignExpr).getSource() = ssaRead(v, delta)
182186
}
183187

184-
/**
185-
* Holds if `inp` is an input to `phi` along a back edge.
186-
*/
187-
predicate backEdge(SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge) {
188-
edge.phiInput(phi, inp) and
189-
// Conservatively assume that every edge is a back edge if we don't have dominance information.
190-
(
191-
phi.getBasicBlock().bbDominates(edge.getOrigBlock()) or
192-
not hasDominanceInformation(edge.getOrigBlock())
193-
)
194-
}
195-
196188
/**
197189
* Holds if `guard` directly controls the position `controlled` with the
198190
* value `testIsTrue`.

shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll

Lines changed: 12 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -142,7 +142,13 @@ signature module Semantic {
142142
Expr getBranchExpr(boolean branch);
143143
}
144144

145-
class BasicBlock;
145+
class BasicBlock {
146+
/** Holds if this block (transitively) dominates `otherblock`. */
147+
predicate bbDominates(BasicBlock otherBlock);
148+
}
149+
150+
/** Gets an immediate successor of basic block `bb`, if any. */
151+
BasicBlock getABasicBlockSuccessor(BasicBlock bb);
146152

147153
class Guard {
148154
string toString();
@@ -176,6 +182,8 @@ signature module Semantic {
176182

177183
class SsaVariable {
178184
Expr getAUse();
185+
186+
BasicBlock getBasicBlock();
179187
}
180188

181189
class SsaPhiNode extends SsaVariable;
@@ -189,15 +197,15 @@ signature module Semantic {
189197
}
190198

191199
class SsaReadPositionPhiInputEdge extends SsaReadPosition {
200+
BasicBlock getOrigBlock();
201+
192202
predicate phiInput(SsaPhiNode phi, SsaVariable inp);
193203
}
194204

195205
class SsaReadPositionBlock extends SsaReadPosition {
196206
BasicBlock getBlock();
197207
}
198208

199-
predicate backEdge(SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge);
200-
201209
predicate conversionCannotOverflow(Type fromType, Type toType);
202210
}
203211

@@ -928,7 +936,7 @@ module RangeStage<
928936
origdelta = D::fromFloat(0) and
929937
reason = TSemNoReason()
930938
|
931-
if Sem::backEdge(phi, inp, edge)
939+
if backEdge(phi, inp, edge)
932940
then
933941
fromBackEdge = true and
934942
(

shared/rangeanalysis/codeql/rangeanalysis/internal/RangeUtils.qll

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -34,4 +34,37 @@ module MakeUtils<Semantic Lang, DeltaSig D> {
3434
or
3535
result.(Lang::CopyValueExpr).getOperand() = ssaRead(v, delta)
3636
}
37+
38+
/**
39+
* Holds if `inp` is an input to `phi` along a back edge.
40+
*/
41+
predicate backEdge(
42+
Lang::SsaPhiNode phi, Lang::SsaVariable inp, Lang::SsaReadPositionPhiInputEdge edge
43+
) {
44+
edge.phiInput(phi, inp) and
45+
(
46+
phi.getBasicBlock().bbDominates(edge.getOrigBlock()) or
47+
irreducibleSccEdge(edge.getOrigBlock(), phi.getBasicBlock())
48+
)
49+
}
50+
51+
/**
52+
* Holds if the edge from b1 to b2 is part of a multiple-entry cycle in an irreducible control flow
53+
* graph. Or if the edge is part of a cycle in unreachable code.
54+
*
55+
* An irreducible control flow graph is one where the usual dominance-based back edge detection does
56+
* not work, because there is a cycle with multiple entry points, meaning there are
57+
* mutually-reachable basic blocks where neither dominates the other. For such a graph, we first
58+
* remove all detectable back-edges using the normal condition that the predecessor block is
59+
* dominated by the successor block, then mark all edges in a cycle in the resulting graph as back
60+
* edges.
61+
*/
62+
private predicate irreducibleSccEdge(Lang::BasicBlock b1, Lang::BasicBlock b2) {
63+
trimmedEdge(b1, b2) and trimmedEdge+(b2, b1)
64+
}
65+
66+
private predicate trimmedEdge(Lang::BasicBlock pred, Lang::BasicBlock succ) {
67+
Lang::getABasicBlockSuccessor(pred) = succ and
68+
not succ.bbDominates(pred)
69+
}
3770
}

0 commit comments

Comments
 (0)