Skip to content

Commit 820d2cb

Browse files
committed
Shared: Use edge dominance in basic block library
1 parent 7619f1d commit 820d2cb

File tree

16 files changed

+142
-75
lines changed

16 files changed

+142
-75
lines changed

csharp/ql/lib/semmle/code/csharp/controlflow/BasicBlocks.qll

Lines changed: 30 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -202,6 +202,29 @@ final class BasicBlock extends BasicBlocksImpl::BasicBlock {
202202
*/
203203
BasicBlock getImmediateDominator() { result = super.getImmediateDominator() }
204204

205+
/**
206+
* Holds if the edge with successor type `s` out of this basic block is a
207+
* dominating edge for `dominated`.
208+
*
209+
* That is, all paths reaching `dominated` from the entry point basic
210+
* block must go through the `s` edge out of this basic block.
211+
*
212+
* Edge dominance is similar to node dominance except it concerns edges
213+
* instead of nodes: A basic block is dominated by a _basic block_ `bb` if it
214+
* can only be reached through `bb` and dominated by an _edge_ `s` if it can
215+
* only be reached through `s`.
216+
*
217+
* Note that where all basic blocks (except the entry basic block) are
218+
* strictly dominated by at least one basic block, a basic block may not be
219+
* dominated by any edge. If an edge dominates a basic block `bb`, then
220+
* both endpoints of the edge dominates `bb`. The converse is not the case,
221+
* as there may be multiple paths between the endpoints with none of them
222+
* dominating.
223+
*/
224+
predicate edgeDominates(BasicBlock dominated, ControlFlow::SuccessorType s) {
225+
super.edgeDominates(dominated, s)
226+
}
227+
205228
/**
206229
* Holds if this basic block strictly post-dominates basic block `bb`.
207230
*
@@ -296,11 +319,14 @@ final class JoinBlockPredecessor extends BasicBlock, BasicBlocksImpl::JoinPredec
296319
* control flow.
297320
*/
298321
final class ConditionBlock extends BasicBlock, BasicBlocksImpl::ConditionBasicBlock {
299-
predicate immediatelyControls(BasicBlock succ, ConditionalSuccessor s) {
300-
super.immediatelyControls(succ, s)
322+
/** DEPRECATED: Use `edgeDominates` instead. */
323+
deprecated predicate immediatelyControls(BasicBlock succ, ConditionalSuccessor s) {
324+
this.getASuccessor(s) = succ and
325+
BasicBlocksImpl::dominatingEdge(this, succ)
301326
}
302327

303-
predicate controls(BasicBlock controlled, ConditionalSuccessor s) {
304-
super.controls(controlled, s)
328+
/** DEPRECATED: Use `edgeDominates` instead. */
329+
deprecated predicate controls(BasicBlock controlled, ConditionalSuccessor s) {
330+
super.edgeDominates(controlled, s)
305331
}
306332
}

csharp/ql/lib/semmle/code/csharp/controlflow/ControlFlowElement.qll

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -225,6 +225,6 @@ class ControlFlowElement extends ExprOrStmtParent, @control_flow_element {
225225
this.controlsBlockSplit(controlled, s, cb)
226226
or
227227
cb.getLastNode() = this.getAControlFlowNode() and
228-
cb.controls(controlled, s)
228+
cb.edgeDominates(controlled, s)
229229
}
230230
}

csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1119,7 +1119,7 @@ private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInpu
11191119
exists(ConditionBlock conditionBlock, ControlFlow::SuccessorTypes::ConditionalSuccessor s |
11201120
guard.getAControlFlowNode() = conditionBlock.getLastNode() and
11211121
s.getValue() = branch and
1122-
conditionBlock.controls(bb, s)
1122+
conditionBlock.edgeDominates(bb, s)
11231123
)
11241124
}
11251125

csharp/ql/test/library-tests/controlflow/graph/Condition.ql

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,8 @@ import ControlFlow
44
query predicate conditionBlock(
55
BasicBlocks::ConditionBlock cb, BasicBlock controlled, boolean testIsTrue
66
) {
7-
cb.controls(controlled, any(SuccessorTypes::ConditionalSuccessor s | testIsTrue = s.getValue()))
7+
cb.edgeDominates(controlled,
8+
any(SuccessorTypes::ConditionalSuccessor s | testIsTrue = s.getValue()))
89
}
910

1011
ControlFlow::Node successor(ControlFlow::Node node, boolean kind) {

ruby/ql/lib/codeql/ruby/controlflow/BasicBlocks.qll

Lines changed: 32 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -168,6 +168,29 @@ final class BasicBlock extends BasicBlocksImpl::BasicBlock {
168168
*/
169169
BasicBlock getImmediateDominator() { result = super.getImmediateDominator() }
170170

171+
/**
172+
* Holds if the edge with successor type `s` out of this basic block is a
173+
* dominating edge for `dominated`.
174+
*
175+
* That is, all paths reaching `dominated` from the entry point basic
176+
* block must go through the `s` edge out of this basic block.
177+
*
178+
* Edge dominance is similar to node dominance except it concerns edges
179+
* instead of nodes: A basic block is dominated by a _basic block_ `bb` if it
180+
* can only be reached through `bb` and dominated by an _edge_ `s` if it can
181+
* only be reached through `s`.
182+
*
183+
* Note that where all basic blocks (except the entry basic block) are
184+
* strictly dominated by at least one basic block, a basic block may not be
185+
* dominated by any edge. If an edge dominates a basic block `bb`, then
186+
* both endpoints of the edge dominates `bb`. The converse is not the case,
187+
* as there may be multiple paths between the endpoints with none of them
188+
* dominating.
189+
*/
190+
predicate edgeDominates(BasicBlock dominated, SuccessorType s) {
191+
super.edgeDominates(dominated, s)
192+
}
193+
171194
/**
172195
* Holds if this basic block strictly post-dominates basic block `bb`.
173196
*
@@ -248,21 +271,26 @@ final class JoinBlockPredecessor extends BasicBlock, BasicBlocksImpl::JoinPredec
248271
*/
249272
final class ConditionBlock extends BasicBlock, BasicBlocksImpl::ConditionBasicBlock {
250273
/**
274+
* DEPRECATED: Use `edgeDominates` instead.
275+
*
251276
* Holds if basic block `succ` is immediately controlled by this basic
252277
* block with conditional value `s`. That is, `succ` is an immediate
253278
* successor of this block, and `succ` can only be reached from
254279
* the callable entry point by going via the `s` edge out of this basic block.
255280
*/
256-
predicate immediatelyControls(BasicBlock succ, ConditionalSuccessor s) {
257-
super.immediatelyControls(succ, s)
281+
deprecated predicate immediatelyControls(BasicBlock succ, ConditionalSuccessor s) {
282+
this.getASuccessor(s) = succ and
283+
BasicBlocksImpl::dominatingEdge(this, succ)
258284
}
259285

260286
/**
287+
* DEPRECATED: Use `edgeDominates` instead.
288+
*
261289
* Holds if basic block `controlled` is controlled by this basic block with
262290
* conditional value `s`. That is, `controlled` can only be reached from the
263291
* callable entry point by going via the `s` edge out of this basic block.
264292
*/
265-
predicate controls(BasicBlock controlled, ConditionalSuccessor s) {
266-
super.controls(controlled, s)
293+
deprecated predicate controls(BasicBlock controlled, ConditionalSuccessor s) {
294+
super.edgeDominates(controlled, s)
267295
}
268296
}

ruby/ql/lib/codeql/ruby/controlflow/internal/Guards.qll

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,6 @@ predicate guardControlsBlock(CfgNodes::AstCfgNode guard, BasicBlock bb, boolean
66
exists(ConditionBlock conditionBlock, SuccessorTypes::ConditionalSuccessor s |
77
guard = conditionBlock.getLastNode() and
88
s.getValue() = branch and
9-
conditionBlock.controls(bb, s)
9+
conditionBlock.edgeDominates(bb, s)
1010
)
1111
}

ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowPrivate.qll

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2387,7 +2387,7 @@ module TypeInference {
23872387
|
23882388
m = resolveConstantReadAccess(pattern.getExpr()) and
23892389
cb.getLastNode() = pattern and
2390-
cb.controls(read.getBasicBlock(),
2390+
cb.edgeDominates(read.getBasicBlock(),
23912391
any(SuccessorTypes::MatchingSuccessor match | match.getValue() = true)) and
23922392
caseRead = def.getARead() and
23932393
read = def.getARead() and

ruby/ql/lib/codeql/ruby/security/ConditionalBypassCustomizations.qll

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@ module ConditionalBypass {
4747

4848
SensitiveActionGuardConditional() {
4949
exists(ConditionBlock cb, BasicBlock controlled |
50-
cb.controls(controlled, _) and
50+
cb.edgeDominates(controlled, _) and
5151
controlled.getANode() = action.asExpr() and
5252
cb.getLastNode() = this.asExpr()
5353
)

ruby/ql/test/library-tests/controlflow/graph/BasicBlocks.ql

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -10,8 +10,8 @@ query predicate immediateDominator(BasicBlock bb1, BasicBlock bb2) {
1010
bb1.getImmediateDominator() = bb2
1111
}
1212

13-
query predicate controls(ConditionBlock bb1, BasicBlock bb2, SuccessorType t) {
14-
bb1.controls(bb2, t)
13+
query predicate controls(ConditionBlock bb1, BasicBlock bb2, SuccessorTypes::ConditionalSuccessor t) {
14+
bb1.edgeDominates(bb2, t)
1515
}
1616

1717
query predicate successor(ConditionBlock bb1, BasicBlock bb2, SuccessorType t) {

ruby/ql/test/library-tests/dataflow/barrier-guards/barrier-guards.ql

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ query predicate newStyleBarrierGuards(DataFlow::Node n) {
1414

1515
query predicate controls(CfgNode condition, BasicBlock bb, SuccessorTypes::ConditionalSuccessor s) {
1616
exists(ConditionBlock cb |
17-
cb.controls(bb, s) and
17+
cb.edgeDominates(bb, s) and
1818
condition = cb.getLastNode()
1919
)
2020
}

rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -491,7 +491,7 @@ private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInpu
491491
exists(ConditionBasicBlock conditionBlock, ConditionalSuccessor s |
492492
guard = conditionBlock.getLastNode() and
493493
s.getValue() = branch and
494-
conditionBlock.controls(bb, s)
494+
conditionBlock.edgeDominates(bb, s)
495495
)
496496
}
497497

rust/ql/test/library-tests/controlflow/BasicBlocks.ql

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ query predicate immediateDominator(BasicBlock bb1, BasicBlock bb2) {
1111
}
1212

1313
query predicate controls(ConditionBasicBlock bb1, BasicBlock bb2, SuccessorType t) {
14-
bb1.controls(bb2, t)
14+
bb1.edgeDominates(bb2, t)
1515
}
1616

1717
query predicate successor(ConditionBasicBlock bb1, BasicBlock bb2, SuccessorType t) {

shared/controlflow/codeql/controlflow/BasicBlock.qll

Lines changed: 52 additions & 51 deletions
Original file line numberDiff line numberDiff line change
@@ -169,90 +169,59 @@ module Make<LocationSig Location, InputSig<Location> Input> {
169169
BasicBlock getImmediateDominator() { bbIDominates(result, this) }
170170

171171
/**
172-
* Holds if basic block `succ` is immediately controlled by this basic
173-
* block with successor type `s`.
172+
* Holds if the edge with successor type `s` out of this basic block is a
173+
* dominating edge for `dominated`.
174174
*
175-
* That is, `succ` is an immediate successor of this block, and `succ` can
176-
* only be reached from the entry block by going via the `s` edge out of
177-
* this basic block.
178-
*/
179-
pragma[nomagic]
180-
predicate immediatelyControls(BasicBlock succ, SuccessorType s) {
181-
succ = this.getASuccessor(s) and
182-
bbIDominates(this, succ) and
183-
// The above is not sufficient to ensure that `succ` can only be reached
184-
// through `s`. To see why, consider this example corresponding to an
185-
// `if` statement without an `else` block and whe `A` is the basic block
186-
// following the `if` statement:
187-
// ```
188-
// ... --> cond --[true]--> ... --> A
189-
// \ /
190-
// ----[false]-----------
191-
// ```
192-
// Here `A` is a direct successor of `cond` along the `false` edge and it
193-
// is immediately dominated by `cond`, but `A` is not controlled by the
194-
// `false` edge since it is also possible to reach `A` via the `true`
195-
// edge.
196-
//
197-
// Note that the first and third conjunct implies the second. But
198-
// explicitly including the second conjunct leads to a better join order.
199-
forall(BasicBlock pred | pred = succ.getAPredecessor() and pred != this |
200-
succ.dominates(pred)
201-
)
202-
}
203-
204-
/**
205-
* Holds if basic block `controlled` is controlled by this basic block with
206-
* successor type `s`.
207-
*
208-
* That is, all paths reaching `controlled` from the entry point basic
175+
* That is, all paths reaching `dominated` from the entry point basic
209176
* block must go through the `s` edge out of this basic block.
210177
*
211-
* Control is similar to dominance except it concerns edges instead of
212-
* nodes: A basic block is _dominated_ by a _basic block_ `bb` if it can
213-
* only be reached through `bb` and _controlled_ by an _edge_ `s` if it can
214-
* only be reached through `s`.
178+
* Edge dominance is similar to node dominance except it concerns edges
179+
* instead of nodes: A basic block is dominated by a _basic block_ `bb` if
180+
* it can only be reached through `bb` and dominated by an _edge_ `s` if it
181+
* can only be reached through `s`.
215182
*
216183
* Note that where all basic blocks (except the entry basic block) are
217184
* strictly dominated by at least one basic block, a basic block may not be
218-
* controlled by any edge. If an edge controls a basic block `bb`, then
185+
* dominated by any edge. If an edge dominates a basic block `bb`, then
219186
* both endpoints of the edge dominates `bb`. The converse is not the case,
220187
* as there may be multiple paths between the endpoints with none of them
221188
* dominating.
222189
*/
223-
predicate controls(BasicBlock controlled, SuccessorType s) {
224-
// For this block to control the block `controlled` with `s` the following must be true:
225-
// 1/ Execution must have passed through the test i.e. `this` must strictly dominate `controlled`.
190+
predicate edgeDominates(BasicBlock dominated, SuccessorType s) {
191+
// For this block to control the block `dominated` with `s` the following must be true:
192+
// 1/ Execution must have passed through the test i.e. `this` must strictly dominate `dominated`.
226193
// 2/ Execution must have passed through the `s` edge leaving `this`.
227194
//
228-
// Although "passed through the `s` edge" implies that `this.getASuccessor(s)` dominates `controlled`,
195+
// Although "passed through the `s` edge" implies that `this.getASuccessor(s)` dominates `dominated`,
229196
// the reverse is not true, as flow may have passed through another edge to get to `this.getASuccessor(s)`
230-
// so we need to assert that `this.getASuccessor(s)` dominates `controlled` *and* that
197+
// so we need to assert that `this.getASuccessor(s)` dominates `dominated` *and* that
231198
// all predecessors of `this.getASuccessor(s)` are either `this` or dominated by `this.getASuccessor(s)`.
232199
//
233200
// For example, in the following C# snippet:
234201
// ```csharp
235202
// if (x)
236-
// controlled;
203+
// dominated;
237204
// false_successor;
238205
// uncontrolled;
239206
// ```
240207
// `false_successor` dominates `uncontrolled`, but not all of its predecessors are `this` (`if (x)`)
241208
// or dominated by itself. Whereas in the following code:
242209
// ```csharp
243210
// if (x)
244-
// while (controlled)
211+
// while (dominated)
245212
// also_controlled;
246213
// false_successor;
247214
// uncontrolled;
248215
// ```
249-
// the block `while controlled` is controlled because all of its predecessors are `this` (`if (x)`)
216+
// the block `while dominated` is dominated because all of its predecessors are `this` (`if (x)`)
250217
// or (in the case of `also_controlled`) dominated by itself.
251218
//
252219
// The additional constraint on the predecessors of the test successor implies
253-
// that `this` strictly dominates `controlled` so that isn't necessary to check
220+
// that `this` strictly dominates `dominated` so that isn't necessary to check
254221
// directly.
255-
exists(BasicBlock succ | this.immediatelyControls(succ, s) | succ.dominates(controlled))
222+
exists(BasicBlock succ |
223+
succ = this.getASuccessor(s) and dominatingEdge(this, succ) and succ.dominates(dominated)
224+
)
256225
}
257226

258227
/**
@@ -282,6 +251,38 @@ module Make<LocationSig Location, InputSig<Location> Input> {
282251
string toString() { result = this.getFirstNode().toString() }
283252
}
284253

254+
/**
255+
* Holds if `bb1` has `bb2` as a direct successor and the edge between `bb1`
256+
* and `bb2` is a dominating edge.
257+
*
258+
* An edge `(bb1, bb2)` is dominating if there exists a basic block that can
259+
* only be reached from the entry block by going through `(bb1, bb2)`. This
260+
* implies that `(bb1, bb2)` dominates its endpoint `bb2`. I.e., `bb2` can
261+
* only be reached from the entry block by going via `(bb1, bb2)`.
262+
*/
263+
pragma[nomagic]
264+
predicate dominatingEdge(BasicBlock bb1, BasicBlock bb2) {
265+
bb1.getASuccessor(_) = bb2 and
266+
bbIDominates(bb1, bb2) and
267+
// The above is not sufficient to ensure that `bb1` can only be reached
268+
// through `(bb1, bb2)`. To see why, consider this example corresponding to
269+
// an `if` statement without an `else` block and whe `A` is the basic block
270+
// following the `if` statement:
271+
// ```
272+
// ... --> cond --[true]--> ... --> A
273+
// \ /
274+
// ----[false]-----------
275+
// ```
276+
// Here `A` is a direct successor of `cond` along the `false` edge and it
277+
// is immediately dominated by `cond`, but `A` is not controlled by the
278+
// `false` edge since it is also possible to reach `A` via the `true`
279+
// edge.
280+
//
281+
// Note that the first and third conjunct implies the second. But
282+
// explicitly including the second conjunct leads to a better join order.
283+
forall(BasicBlock pred | pred = bb2.getAPredecessor() and pred != bb1 | bb2.dominates(pred))
284+
}
285+
285286
cached
286287
private module Cached {
287288
/**

shared/controlflow/codeql/controlflow/Cfg.qll

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1594,6 +1594,8 @@ module MakeWithSplitting<
15941594

15951595
final class BasicBlock = BasicBlockImpl::BasicBlock;
15961596

1597+
predicate dominatingEdge = BasicBlockImpl::dominatingEdge/2;
1598+
15971599
/**
15981600
* An entry basic block, that is, a basic block whose first node is
15991601
* an entry node.

0 commit comments

Comments
 (0)