Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add shared basic block library #18497

Merged
merged 13 commits into from
Jan 24, 2025
Merged
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Shared: Address basic block review comments
paldepind committed Jan 20, 2025

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
commit 62a459d3d7be8706272a080322ef9d0c6e9ae836
146 changes: 100 additions & 46 deletions shared/controlflow/codeql/controlflow/BasicBlock.qll
Original file line number Diff line number Diff line change
@@ -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. */
@@ -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`.
*
@@ -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`.
@@ -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
Original file line number Diff line number Diff line change
@@ -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() }
@@ -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))
}
}
}
}