Skip to content

Commit 62a459d

Browse files
paldepindpaldepind
committed
Shared: Address basic block review comments
1 parent e382ffc commit 62a459d

File tree

2 files changed

+101
-106
lines changed

2 files changed

+101
-106
lines changed

‎shared/controlflow/codeql/controlflow/BasicBlock.qll‎

Lines changed: 100 additions & 46 deletions
Original file line numberDiff line numberDiff line change
@@ -80,7 +80,6 @@ module Make<LocationSig Location, InputSig<Location> Input> {
8080
BasicBlock getAPredecessor(SuccessorType t) { result.getASuccessor(t) = this }
8181

8282
/** Gets the control flow node at a specific (zero-indexed) position in this basic block. */
83-
cached
8483
Node getNode(int pos) { bbIndex(this.getFirstNode(), result, pos) }
8584

8685
/** Gets a control flow node in this basic block. */
@@ -152,6 +151,60 @@ module Make<LocationSig Location, InputSig<Location> Input> {
152151
*/
153152
BasicBlock getImmediateDominator() { bbIDominates(result, this) }
154153

154+
/**
155+
* Holds if basic block `succ` is immediately controlled by this basic
156+
* block with conditional value `s`. That is, `succ` is an immediate
157+
* successor of this block, and `succ` can only be reached from
158+
* the callable entry point by going via the `s` edge out of this basic block.
159+
*/
160+
pragma[nomagic]
161+
predicate immediatelyControls(BasicBlock succ, SuccessorType s) {
162+
succ = this.getASuccessor(s) and
163+
forall(BasicBlock pred | pred = succ.getAPredecessor() and pred != this |
164+
succ.dominates(pred)
165+
)
166+
}
167+
168+
/**
169+
* Holds if basic block `controlled` is controlled by this basic block with
170+
* conditional value `s`. That is, `controlled` can only be reached from
171+
* the callable entry point by going via the `s` edge out of this basic block.
172+
*/
173+
predicate controls(BasicBlock controlled, SuccessorType s) {
174+
// For this block to control the block `controlled` with `s` the following must be true:
175+
// 1/ Execution must have passed through the test i.e. `this` must strictly dominate `controlled`.
176+
// 2/ Execution must have passed through the `s` edge leaving `this`.
177+
//
178+
// Although "passed through the `s` edge" implies that `this.getASuccessor(s)` dominates `controlled`,
179+
// the reverse is not true, as flow may have passed through another edge to get to `this.getASuccessor(s)`
180+
// so we need to assert that `this.getASuccessor(s)` dominates `controlled` *and* that
181+
// all predecessors of `this.getASuccessor(s)` are either `this` or dominated by `this.getASuccessor(s)`.
182+
//
183+
// For example, in the following C# snippet:
184+
// ```csharp
185+
// if (x)
186+
// controlled;
187+
// false_successor;
188+
// uncontrolled;
189+
// ```
190+
// `false_successor` dominates `uncontrolled`, but not all of its predecessors are `this` (`if (x)`)
191+
// or dominated by itself. Whereas in the following code:
192+
// ```csharp
193+
// if (x)
194+
// while (controlled)
195+
// also_controlled;
196+
// false_successor;
197+
// uncontrolled;
198+
// ```
199+
// the block `while controlled` is controlled because all of its predecessors are `this` (`if (x)`)
200+
// or (in the case of `also_controlled`) dominated by itself.
201+
//
202+
// The additional constraint on the predecessors of the test successor implies
203+
// that `this` strictly dominates `controlled` so that isn't necessary to check
204+
// directly.
205+
exists(BasicBlock succ | this.immediatelyControls(succ, s) | succ.dominates(controlled))
206+
}
207+
155208
/**
156209
* Holds if this basic block strictly post-dominates basic block `bb`.
157210
*
@@ -188,6 +241,52 @@ module Make<LocationSig Location, InputSig<Location> Input> {
188241
cached
189242
newtype TBasicBlock = TBasicBlockStart(Node cfn) { startsBB(cfn) }
190243

244+
/** Holds if `cfn` starts a new basic block. */
245+
private predicate startsBB(Node cfn) {
246+
not exists(nodeGetAPredecessor(cfn, _)) and exists(nodeGetASuccessor(cfn, _))
247+
or
248+
nodeIsJoin(cfn)
249+
or
250+
nodeIsBranch(nodeGetAPredecessor(cfn, _))
251+
or
252+
// In cases such as
253+
//
254+
// ```rb
255+
// if x and y
256+
// foo
257+
// else
258+
// bar
259+
// ```
260+
//
261+
// we have a CFG that looks like
262+
//
263+
// x --false--> [false] x and y --false--> bar
264+
// \ |
265+
// --true--> y --false--
266+
// \
267+
// --true--> [true] x and y --true--> foo
268+
//
269+
// and we want to ensure that both `foo` and `bar` start a new basic block.
270+
exists(nodeGetAPredecessor(cfn, any(SuccessorType s | successorTypeIsCondition(s))))
271+
}
272+
273+
/**
274+
* Holds if `succ` is a control flow successor of `pred` within
275+
* the same basic block.
276+
*/
277+
private predicate intraBBSucc(Node pred, Node succ) {
278+
succ = nodeGetASuccessor(pred, _) and
279+
not startsBB(succ)
280+
}
281+
282+
/**
283+
* Holds if `bbStart` is the first node in a basic block and `cfn` is the
284+
* `i`th node in the same basic block.
285+
*/
286+
cached
287+
predicate bbIndex(Node bbStart, Node cfn, int i) =
288+
shortestDistances(startsBB/1, intraBBSucc/2)(bbStart, cfn, i)
289+
191290
/**
192291
* Holds if the first node of basic block `succ` is a control flow
193292
* successor of the last node of basic block `pred`.
@@ -213,51 +312,6 @@ module Make<LocationSig Location, InputSig<Location> Input> {
213312

214313
private import Cached
215314

216-
/** Holds if `cfn` starts a new basic block. */
217-
private predicate startsBB(Node cfn) {
218-
not exists(nodeGetAPredecessor(cfn, _)) and exists(nodeGetASuccessor(cfn, _))
219-
or
220-
nodeIsJoin(cfn)
221-
or
222-
nodeIsBranch(nodeGetAPredecessor(cfn, _))
223-
or
224-
// In cases such as
225-
//
226-
// ```rb
227-
// if x and y
228-
// foo
229-
// else
230-
// bar
231-
// ```
232-
//
233-
// we have a CFG that looks like
234-
//
235-
// x --false--> [false] x or y --false--> bar
236-
// \ |
237-
// --true--> y --false--
238-
// \
239-
// --true--> [true] x or y --true--> foo
240-
//
241-
// and we want to ensure that both `foo` and `bar` start a new basic block.
242-
exists(nodeGetAPredecessor(cfn, any(SuccessorType s | successorTypeIsCondition(s))))
243-
}
244-
245-
/**
246-
* Holds if `succ` is a control flow successor of `pred` within
247-
* the same basic block.
248-
*/
249-
predicate intraBBSucc(Node pred, Node succ) {
250-
succ = nodeGetASuccessor(pred, _) and
251-
not startsBB(succ)
252-
}
253-
254-
/**
255-
* Holds if `bbStart` is the first node in a basic block and `cfn` is the
256-
* `i`th node in the same basic block.
257-
*/
258-
private predicate bbIndex(Node bbStart, Node cfn, int i) =
259-
shortestDistances(startsBB/1, intraBBSucc/2)(bbStart, cfn, i)
260-
261315
/** Holds if `bb` is an entry basic block. */
262316
private predicate entryBB(BasicBlock bb) { nodeIsDominanceEntry(bb.getFirstNode()) }
263317
}

‎shared/controlflow/codeql/controlflow/Cfg.qll‎

Lines changed: 1 addition & 60 deletions
Original file line numberDiff line numberDiff line change
@@ -1591,13 +1591,8 @@ module MakeWithSplitting<
15911591
* without branches or joins.
15921592
*/
15931593
final class BasicBlock extends BasicBlockImpl::BasicBlock {
1594-
// We extend `BasicBlockImpl::BasicBlock` to add the `getScope`.
15951594
/** Gets the scope of this basic block. */
1596-
CfgScope getScope() {
1597-
if this instanceof EntryBasicBlock
1598-
then result = this.getFirstNode().getScope()
1599-
else result = this.getAPredecessor().getScope()
1600-
}
1595+
CfgScope getScope() { result = this.getFirstNode().getScope() }
16011596

16021597
/** Gets an immediate successor of this basic block, if any. */
16031598
BasicBlock getASuccessor() { result = super.getASuccessor() }
@@ -1725,60 +1720,6 @@ module MakeWithSplitting<
17251720
/** A basic block that terminates in a condition, splitting the subsequent control flow. */
17261721
final class ConditionBasicBlock extends BasicBlock {
17271722
ConditionBasicBlock() { this.getLastNode().isCondition() }
1728-
1729-
/**
1730-
* Holds if basic block `succ` is immediately controlled by this basic
1731-
* block with conditional value `s`. That is, `succ` is an immediate
1732-
* successor of this block, and `succ` can only be reached from
1733-
* the callable entry point by going via the `s` edge out of this basic block.
1734-
*/
1735-
pragma[nomagic]
1736-
predicate immediatelyControls(BasicBlock succ, SuccessorType s) {
1737-
succ = this.getASuccessor(s) and
1738-
forall(BasicBlock pred | pred = succ.getAPredecessor() and pred != this |
1739-
succ.dominates(pred)
1740-
)
1741-
}
1742-
1743-
/**
1744-
* Holds if basic block `controlled` is controlled by this basic block with
1745-
* conditional value `s`. That is, `controlled` can only be reached from
1746-
* the callable entry point by going via the `s` edge out of this basic block.
1747-
*/
1748-
predicate controls(BasicBlock controlled, SuccessorType s) {
1749-
// For this block to control the block `controlled` with `testIsTrue` the following must be true:
1750-
// 1/ Execution must have passed through the test i.e. `this` must strictly dominate `controlled`.
1751-
// 2/ Execution must have passed through the `testIsTrue` edge leaving `this`.
1752-
//
1753-
// Although "passed through the true edge" implies that `this.getATrueSuccessor()` dominates `controlled`,
1754-
// the reverse is not true, as flow may have passed through another edge to get to `this.getATrueSuccessor()`
1755-
// so we need to assert that `this.getATrueSuccessor()` dominates `controlled` *and* that
1756-
// all predecessors of `this.getATrueSuccessor()` are either `this` or dominated by `this.getATrueSuccessor()`.
1757-
//
1758-
// For example, in the following C# snippet:
1759-
// ```csharp
1760-
// if (x)
1761-
// controlled;
1762-
// false_successor;
1763-
// uncontrolled;
1764-
// ```
1765-
// `false_successor` dominates `uncontrolled`, but not all of its predecessors are `this` (`if (x)`)
1766-
// or dominated by itself. Whereas in the following code:
1767-
// ```csharp
1768-
// if (x)
1769-
// while (controlled)
1770-
// also_controlled;
1771-
// false_successor;
1772-
// uncontrolled;
1773-
// ```
1774-
// the block `while controlled` is controlled because all of its predecessors are `this` (`if (x)`)
1775-
// or (in the case of `also_controlled`) dominated by itself.
1776-
//
1777-
// The additional constraint on the predecessors of the test successor implies
1778-
// that `this` strictly dominates `controlled` so that isn't necessary to check
1779-
// directly.
1780-
exists(BasicBlock succ | this.immediatelyControls(succ, s) | succ.dominates(controlled))
1781-
}
17821723
}
17831724
}
17841725
}

0 commit comments

Comments
 (0)