Skip to content

Commit

Permalink
Shared: Address basic block review comments
Browse files Browse the repository at this point in the history
  • Loading branch information
@paldepind
paldepind committed Jan 20, 2025
1 parent e382ffc commit 62a459d
Show file tree
Hide file tree
Showing 2 changed files with 101 additions and 106 deletions.
146 changes: 100 additions & 46 deletions shared/controlflow/codeql/controlflow/BasicBlock.qll
View file
Original file line number Diff line number Diff line change
Expand Up @@ -80,7 +80,6 @@ module Make<LocationSig Location, InputSig<Location> Input> {
BasicBlock getAPredecessor(SuccessorType t) { result.getASuccessor(t) = this }

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

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

/**
* Holds if basic block `succ` is immediately controlled by this basic
* block with conditional value `s`. That is, `succ` is an immediate
* successor of this block, and `succ` can only be reached from
* the callable entry point by going via the `s` edge out of this basic block.
*/
pragma[nomagic]
predicate immediatelyControls(BasicBlock succ, SuccessorType s) {
succ = this.getASuccessor(s) and
forall(BasicBlock pred | pred = succ.getAPredecessor() and pred != this |
succ.dominates(pred)
)
}

/**
* Holds if basic block `controlled` is controlled by this basic block with
* conditional value `s`. That is, `controlled` can only be reached from
* the callable entry point by going via the `s` edge out of this basic block.
*/
predicate controls(BasicBlock controlled, SuccessorType s) {
// For this block to control the block `controlled` with `s` the following must be true:
// 1/ Execution must have passed through the test i.e. `this` must strictly dominate `controlled`.
// 2/ Execution must have passed through the `s` edge leaving `this`.
//
// Although "passed through the `s` edge" implies that `this.getASuccessor(s)` dominates `controlled`,
// the reverse is not true, as flow may have passed through another edge to get to `this.getASuccessor(s)`
// so we need to assert that `this.getASuccessor(s)` dominates `controlled` *and* that
// all predecessors of `this.getASuccessor(s)` are either `this` or dominated by `this.getASuccessor(s)`.
//
// For example, in the following C# snippet:
// ```csharp
// if (x)
// controlled;
// false_successor;
// uncontrolled;
// ```
// `false_successor` dominates `uncontrolled`, but not all of its predecessors are `this` (`if (x)`)
// or dominated by itself. Whereas in the following code:
// ```csharp
// if (x)
// while (controlled)
// also_controlled;
// false_successor;
// uncontrolled;
// ```
// the block `while controlled` is controlled because all of its predecessors are `this` (`if (x)`)
// or (in the case of `also_controlled`) dominated by itself.
//
// The additional constraint on the predecessors of the test successor implies
// that `this` strictly dominates `controlled` so that isn't necessary to check
// directly.
exists(BasicBlock succ | this.immediatelyControls(succ, s) | succ.dominates(controlled))
}

/**
* Holds if this basic block strictly post-dominates basic block `bb`.
*
Expand Down Expand Up @@ -188,6 +241,52 @@ module Make<LocationSig Location, InputSig<Location> Input> {
cached
newtype TBasicBlock = TBasicBlockStart(Node cfn) { startsBB(cfn) }

/** Holds if `cfn` starts a new basic block. */
private predicate startsBB(Node cfn) {
not exists(nodeGetAPredecessor(cfn, _)) and exists(nodeGetASuccessor(cfn, _))
or
nodeIsJoin(cfn)
or
nodeIsBranch(nodeGetAPredecessor(cfn, _))
or
// In cases such as
//
// ```rb
// if x and y
// foo
// else
// bar
// ```
//
// we have a CFG that looks like
//
// x --false--> [false] x and y --false--> bar
// \ |
// --true--> y --false--
// \
// --true--> [true] x and y --true--> foo
//
// and we want to ensure that both `foo` and `bar` start a new basic block.
exists(nodeGetAPredecessor(cfn, any(SuccessorType s | successorTypeIsCondition(s))))
}

/**
* Holds if `succ` is a control flow successor of `pred` within
* the same basic block.
*/
private predicate intraBBSucc(Node pred, Node succ) {
succ = nodeGetASuccessor(pred, _) and
not startsBB(succ)
}

/**
* Holds if `bbStart` is the first node in a basic block and `cfn` is the
* `i`th node in the same basic block.
*/
cached
predicate bbIndex(Node bbStart, Node cfn, int i) =
shortestDistances(startsBB/1, intraBBSucc/2)(bbStart, cfn, i)

/**
* Holds if the first node of basic block `succ` is a control flow
* successor of the last node of basic block `pred`.
Expand All @@ -213,51 +312,6 @@ module Make<LocationSig Location, InputSig<Location> Input> {

private import Cached

/** Holds if `cfn` starts a new basic block. */
private predicate startsBB(Node cfn) {
not exists(nodeGetAPredecessor(cfn, _)) and exists(nodeGetASuccessor(cfn, _))
or
nodeIsJoin(cfn)
or
nodeIsBranch(nodeGetAPredecessor(cfn, _))
or
// In cases such as
//
// ```rb
// if x and y
// foo
// else
// bar
// ```
//
// we have a CFG that looks like
//
// x --false--> [false] x or y --false--> bar
// \ |
// --true--> y --false--
// \
// --true--> [true] x or y --true--> foo
//
// and we want to ensure that both `foo` and `bar` start a new basic block.
exists(nodeGetAPredecessor(cfn, any(SuccessorType s | successorTypeIsCondition(s))))
}

/**
* Holds if `succ` is a control flow successor of `pred` within
* the same basic block.
*/
predicate intraBBSucc(Node pred, Node succ) {
succ = nodeGetASuccessor(pred, _) and
not startsBB(succ)
}

/**
* Holds if `bbStart` is the first node in a basic block and `cfn` is the
* `i`th node in the same basic block.
*/
private predicate bbIndex(Node bbStart, Node cfn, int i) =
shortestDistances(startsBB/1, intraBBSucc/2)(bbStart, cfn, i)

/** Holds if `bb` is an entry basic block. */
private predicate entryBB(BasicBlock bb) { nodeIsDominanceEntry(bb.getFirstNode()) }
}
61 changes: 1 addition & 60 deletions shared/controlflow/codeql/controlflow/Cfg.qll
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1591,13 +1591,8 @@ module MakeWithSplitting<
* without branches or joins.
*/
final class BasicBlock extends BasicBlockImpl::BasicBlock {
// We extend `BasicBlockImpl::BasicBlock` to add the `getScope`.
/** Gets the scope of this basic block. */
CfgScope getScope() {
if this instanceof EntryBasicBlock
then result = this.getFirstNode().getScope()
else result = this.getAPredecessor().getScope()
}
CfgScope getScope() { result = this.getFirstNode().getScope() }

/** Gets an immediate successor of this basic block, if any. */
BasicBlock getASuccessor() { result = super.getASuccessor() }
Expand Down Expand Up @@ -1725,60 +1720,6 @@ module MakeWithSplitting<
/** A basic block that terminates in a condition, splitting the subsequent control flow. */
final class ConditionBasicBlock extends BasicBlock {
ConditionBasicBlock() { this.getLastNode().isCondition() }

/**
* Holds if basic block `succ` is immediately controlled by this basic
* block with conditional value `s`. That is, `succ` is an immediate
* successor of this block, and `succ` can only be reached from
* the callable entry point by going via the `s` edge out of this basic block.
*/
pragma[nomagic]
predicate immediatelyControls(BasicBlock succ, SuccessorType s) {
succ = this.getASuccessor(s) and
forall(BasicBlock pred | pred = succ.getAPredecessor() and pred != this |
succ.dominates(pred)
)
}

/**
* Holds if basic block `controlled` is controlled by this basic block with
* conditional value `s`. That is, `controlled` can only be reached from
* the callable entry point by going via the `s` edge out of this basic block.
*/
predicate controls(BasicBlock controlled, SuccessorType s) {
// For this block to control the block `controlled` with `testIsTrue` the following must be true:
// 1/ Execution must have passed through the test i.e. `this` must strictly dominate `controlled`.
// 2/ Execution must have passed through the `testIsTrue` edge leaving `this`.
//
// Although "passed through the true edge" implies that `this.getATrueSuccessor()` dominates `controlled`,
// the reverse is not true, as flow may have passed through another edge to get to `this.getATrueSuccessor()`
// so we need to assert that `this.getATrueSuccessor()` dominates `controlled` *and* that
// all predecessors of `this.getATrueSuccessor()` are either `this` or dominated by `this.getATrueSuccessor()`.
//
// For example, in the following C# snippet:
// ```csharp
// if (x)
// controlled;
// false_successor;
// uncontrolled;
// ```
// `false_successor` dominates `uncontrolled`, but not all of its predecessors are `this` (`if (x)`)
// or dominated by itself. Whereas in the following code:
// ```csharp
// if (x)
// while (controlled)
// also_controlled;
// false_successor;
// uncontrolled;
// ```
// the block `while controlled` is controlled because all of its predecessors are `this` (`if (x)`)
// or (in the case of `also_controlled`) dominated by itself.
//
// The additional constraint on the predecessors of the test successor implies
// that `this` strictly dominates `controlled` so that isn't necessary to check
// directly.
exists(BasicBlock succ | this.immediatelyControls(succ, s) | succ.dominates(controlled))
}
}
}
}
Expand Down

0 comments on commit 62a459d

Please sign in to comment.