Skip to content

Commit

Permalink
Add shared basic block library
Browse files Browse the repository at this point in the history
  • Loading branch information
@paldepind
paldepind committed Jan 15, 2025
1 parent 5bbd244 commit 1c9e7cc
Show file tree
Hide file tree
Showing 12 changed files with 380 additions and 1,022 deletions.
281 changes: 27 additions & 254 deletions csharp/ql/lib/semmle/code/csharp/controlflow/BasicBlocks.qll
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,27 +3,18 @@
*/

import csharp
private import codeql.basicblock.BasicBlock as BB
private import ControlFlow::SuccessorTypes
private import ControlFlow::SuccessorTypes as ST
private import ControlFlow as CFG

Check warning

Code scanning / CodeQL

Names only differing by case Warning

CFG is only different by casing from Cfg that is used elsewhere for modules.
private import semmle.code.csharp.controlflow.internal.ControlFlowGraphImpl as CfgImpl
import CfgImpl::BasicBlock as BasicBlockImpl

/**
* A basic block, that is, a maximal straight-line sequence of control flow nodes
* without branches or joins.
*/
class BasicBlock extends TBasicBlockStart {
/** Gets an immediate successor of this basic block, if any. */
BasicBlock getASuccessor() { result.getFirstNode() = this.getLastNode().getASuccessor() }

/** Gets an immediate successor of this basic block of a given type, if any. */
BasicBlock getASuccessorByType(ControlFlow::SuccessorType t) {
result.getFirstNode() = this.getLastNode().getASuccessorByType(t)
}

/** Gets an immediate predecessor of this basic block, if any. */
BasicBlock getAPredecessor() { result.getASuccessor() = this }
final class BasicBlock extends BasicBlockImpl::BasicBlock {
BasicBlock getASuccessorByType(ControlFlow::SuccessorType t) { result = this.getASuccessor(t) }

/** Gets an immediate predecessor of this basic block of a given type, if any. */
BasicBlock getAPredecessorByType(ControlFlow::SuccessorType t) {
result.getASuccessorByType(t) = this
result = this.getAPredecessor(t)
}

/**
Expand Down Expand Up @@ -65,23 +56,20 @@ class BasicBlock extends TBasicBlockStart {
}

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

/** Gets a control flow node in this basic block. */
ControlFlow::Node getANode() { result = this.getNode(_) }
ControlFlow::Node getANode() { result = super.getANode() }

/** Gets the first control flow node in this basic block. */
ControlFlow::Node getFirstNode() { this = TBasicBlockStart(result) }
ControlFlow::Node getFirstNode() { result = super.getFirstNode() }

/** Gets the last control flow node in this basic block. */
ControlFlow::Node getLastNode() { result = this.getNode(this.length() - 1) }
ControlFlow::Node getLastNode() { result = super.getLastNode() }

/** Gets the callable that this basic block belongs to. */
final Callable getCallable() { result = this.getFirstNode().getEnclosingCallable() }

/** Gets the length of this basic block. */
int length() { result = strictcount(this.getANode()) }

/**
* Holds if this basic block immediately dominates basic block `bb`.
*
Expand All @@ -103,7 +91,7 @@ class BasicBlock extends TBasicBlockStart {
* basic block on line 4 (all paths from the entry point of `M`
* to `return s.Length;` must go through the null check).
*/
predicate immediatelyDominates(BasicBlock bb) { bbIDominates(this, bb) }
predicate immediatelyDominates(BasicBlock bb) { super.immediatelyDominates(bb) }

/**
* Holds if this basic block strictly dominates basic block `bb`.
Expand All @@ -126,7 +114,7 @@ class BasicBlock extends TBasicBlockStart {
* basic block on line 4 (all paths from the entry point of `M`
* to `return s.Length;` must go through the null check).
*/
predicate strictlyDominates(BasicBlock bb) { bbIDominates+(this, bb) }
predicate strictlyDominates(BasicBlock bb) { super.strictlyDominates(bb) }

/**
* Holds if this basic block dominates basic block `bb`.
Expand Down Expand Up @@ -178,15 +166,7 @@ class BasicBlock extends TBasicBlockStart {
* `Console.Write(x);`. Also, the basic block starting on line 2
* does not dominate the basic block on line 6.
*/
predicate inDominanceFrontier(BasicBlock df) {
this.dominatesPredecessor(df) and
not this.strictlyDominates(df)
}

/**
* Holds if this basic block dominates a predecessor of `df`.
*/
private predicate dominatesPredecessor(BasicBlock df) { this.dominates(df.getAPredecessor()) }
predicate inDominanceFrontier(BasicBlock df) { super.inDominanceFrontier(df) }

/**
* Gets the basic block that immediately dominates this basic block, if any.
Expand All @@ -208,7 +188,7 @@ class BasicBlock extends TBasicBlockStart {
* the basic block online 4 (all paths from the entry point of `M`
* to `return s.Length;` must go through the null check.
*/
BasicBlock getImmediateDominator() { bbIDominates(result, this) }
BasicBlock getImmediateDominator() { result = super.getImmediateDominator() }

/**
* Holds if this basic block strictly post-dominates basic block `bb`.
Expand All @@ -234,7 +214,7 @@ class BasicBlock extends TBasicBlockStart {
* line 3 (all paths to the exit point of `M` from `return s.Length;`
* must go through the `WriteLine` call).
*/
predicate strictlyPostDominates(BasicBlock bb) { bbIPostDominates+(this, bb) }
predicate strictlyPostDominates(BasicBlock bb) { super.strictlyPostDominates(bb) }

/**
* Holds if this basic block post-dominates basic block `bb`.
Expand Down Expand Up @@ -262,10 +242,7 @@ class BasicBlock extends TBasicBlockStart {
* This predicate is *reflexive*, so for example `Console.WriteLine("M");`
* post-dominates itself.
*/
predicate postDominates(BasicBlock bb) {
this.strictlyPostDominates(bb) or
this = bb
}
predicate postDominates(BasicBlock bb) { super.postDominates(bb) }

/**
* Holds if this basic block is in a loop in the control flow graph. This
Expand All @@ -274,230 +251,26 @@ class BasicBlock extends TBasicBlockStart {
* necessary back edges are unreachable.
*/
predicate inLoop() { this.getASuccessor+() = this }

/** Gets a textual representation of this basic block. */
string toString() { result = this.getFirstNode().toString() }

/** Gets the location of this basic block. */
Location getLocation() { result = this.getFirstNode().getLocation() }
}

/**
* Internal implementation details.
*/
cached
private module Internal {
/** Internal representation of basic blocks. */
cached
newtype TBasicBlock = TBasicBlockStart(ControlFlow::Node cfn) { startsBB(cfn) }

/** Holds if `cfn` starts a new basic block. */
private predicate startsBB(ControlFlow::Node cfn) {
not exists(cfn.getAPredecessor()) and exists(cfn.getASuccessor())
or
cfn.isJoin()
or
cfn.getAPredecessor().isBranch()
or
/*
* In cases such as
* ```csharp
* if (b)
* M()
* ```
* where the `false` edge out of `b` is not present (because we can prove it
* impossible), we still split up the basic block in two, in order to generate
* a `ConditionBlock` which can be used by the guards library.
*/

exists(cfn.getAPredecessorByType(any(ControlFlow::SuccessorTypes::ConditionalSuccessor s)))
}

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

/**
* Holds if `cfn` is the `i`th node in basic block `bb`.
*
* In other words, `i` is the shortest distance from a node `bb`
* that starts a basic block to `cfn` along the `intraBBSucc` relation.
*/
cached
predicate bbIndex(ControlFlow::Node bbStart, ControlFlow::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`.
*/
private predicate succBB(BasicBlock pred, BasicBlock succ) { succ = pred.getASuccessor() }

/** Holds if `dom` is an immediate dominator of `bb`. */
cached
predicate bbIDominates(BasicBlock dom, BasicBlock bb) =
idominance(entryBB/1, succBB/2)(_, dom, bb)

/** Holds if `pred` is a basic block predecessor of `succ`. */
private predicate predBB(BasicBlock succ, BasicBlock pred) { succBB(pred, succ) }

/** Holds if `bb` is an exit basic block that represents normal exit. */
private predicate normalExitBB(BasicBlock bb) {
bb.getANode().(ControlFlow::Nodes::AnnotatedExitNode).isNormal()
}

/** Holds if `dom` is an immediate post-dominator of `bb`. */
cached
predicate bbIPostDominates(BasicBlock dom, BasicBlock bb) =
idominance(normalExitBB/1, predBB/2)(_, dom, bb)
}

private import Internal

/**
* An entry basic block, that is, a basic block whose first node is
* the entry node of a callable.
*/
class EntryBasicBlock extends BasicBlock {
EntryBasicBlock() { entryBB(this) }
}

/** Holds if `bb` is an entry basic block. */
private predicate entryBB(BasicBlock bb) {
bb.getFirstNode() instanceof ControlFlow::Nodes::EntryNode
}

/**
* An annotated exit basic block, that is, a basic block that contains
* an annotated exit node.
*/
class AnnotatedExitBasicBlock extends BasicBlock {
private boolean isNormal;

AnnotatedExitBasicBlock() {
this.getANode() =
any(ControlFlow::Nodes::AnnotatedExitNode n |
if n.isNormal() then isNormal = true else isNormal = false
)
}

/** Holds if this block represents a normal exit. */
predicate isNormal() { isNormal = true }
}

/**
* An exit basic block, that is, a basic block whose last node is
* the exit node of a callable.
*/
class ExitBasicBlock extends BasicBlock {
ExitBasicBlock() { this.getLastNode() instanceof ControlFlow::Nodes::ExitNode }
}

private module JoinBlockPredecessors {
private import ControlFlow::Nodes
private import semmle.code.csharp.controlflow.internal.ControlFlowGraphImpl as Impl
final class EntryBasicBlock extends BasicBlock, BasicBlockImpl::EntryBasicBlock { }

int getId(JoinBlockPredecessor jbp) {
exists(Impl::AstNode n | result = n.getId() |
n = jbp.getFirstNode().getAstNode()
or
n = jbp.(EntryBasicBlock).getCallable()
)
}
final class AnnotatedExitBasicBlock extends BasicBlock, BasicBlockImpl::AnnotatedExitBasicBlock { }

string getSplitString(JoinBlockPredecessor jbp) {
result = jbp.getFirstNode().(ElementNode).getSplitsString()
or
not exists(jbp.getFirstNode().(ElementNode).getSplitsString()) and
result = ""
}
}

/** A basic block with more than one predecessor. */
class JoinBlock extends BasicBlock {
JoinBlock() { this.getFirstNode().isJoin() }
final class ExitBasicBlock extends BasicBlock, BasicBlockImpl::ExitBasicBlock { }

/**
* Gets the `i`th predecessor of this join block, with respect to some
* arbitrary order.
*/
cached
JoinBlockPredecessor getJoinBlockPredecessor(int i) {
result =
rank[i + 1](JoinBlockPredecessor jbp |
jbp = this.getAPredecessor()
|
jbp order by JoinBlockPredecessors::getId(jbp), JoinBlockPredecessors::getSplitString(jbp)
)
}
}

/** A basic block that is an immediate predecessor of a join block. */
class JoinBlockPredecessor extends BasicBlock {
JoinBlockPredecessor() { this.getASuccessor() instanceof JoinBlock }
final class JoinBlock extends BasicBlock, BasicBlockImpl::JoinBasicBlock {
JoinBlockPredecessor getJoinBlockPredecessor(int i) { result = super.getJoinBlockPredecessor(i) }
}

/** A basic block that terminates in a condition, splitting the subsequent control flow. */
class ConditionBlock extends BasicBlock {
ConditionBlock() { this.getLastNode().isCondition() }
final class JoinBlockPredecessor extends BasicBlock, BasicBlockImpl::JoinPredecessorBasicBlock { }

/**
* 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]
final class ConditionBlock extends BasicBlock, BasicBlockImpl::ConditionBasicBlock {
predicate immediatelyControls(BasicBlock succ, ConditionalSuccessor s) {
succ = this.getASuccessorByType(s) and
forall(BasicBlock pred | pred = succ.getAPredecessor() and pred != this | succ.dominates(pred))
super.immediatelyControls(succ, s)
}

/**
* 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, ConditionalSuccessor s) {
/*
* For this block to control the block `controlled` with `testIsTrue` the following must be true:
* Execution must have passed through the test i.e. `this` must strictly dominate `controlled`.
* 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))
super.controls(controlled, s)
}
}
4 changes: 4 additions & 0 deletions csharp/ql/lib/semmle/code/csharp/controlflow/internal/ControlFlowGraphImpl.qll
View file
Original file line number Diff line number Diff line change
Expand Up @@ -95,6 +95,10 @@ private module CfgInput implements CfgShared::InputSig<Location> {
t instanceof ST::SuccessorTypes::ExceptionSuccessor or
t instanceof ST::SuccessorTypes::ExitSuccessor
}

predicate idOfAstNode(AstNode node, int id) { node.getId() = id }

predicate idOfCfgScope(CfgScope node, int id) { idOfAstNode(node, id) }
}

private module CfgSplittingInput implements CfgShared::SplittingInputSig<Location, CfgInput> {
Expand Down
Loading

0 comments on commit 1c9e7cc

Please sign in to comment.