hohn/codeql
1
0
Fork 0
mirror of https://github.com/github/codeql.git synced 2026-04-30 19:26:02 +02:00
Code Issues Packages Projects Releases Wiki Activity

C#: Add internal PreBasicBlocks library

Browse Source
This commit is contained in:
Tom Hvitved
2018-09-12 15:09:50 +02:00
parent f146e34e26
commit b8caa117f1
3 changed files with 174 additions and 11 deletions
Download Patch File Download Diff File Expand all files Collapse all files

135
csharp/ql/src/semmle/code/csharp/controlflow/ControlFlowGraph.qll
View File

@@ -34,7 +34,7 @@ module ControlFlow {
/** Holds if this control flow node has conditional successors. */
predicate isCondition() {
exists(getASuccessorByType(any(SuccessorTypes::ConditionalSuccessor e)))
exists(getASuccessorByType(any(ConditionalSuccessor e)))
}
/** Gets the basic block that this control flow node belongs to. */
@@ -216,7 +216,7 @@ module ControlFlow {
* on line 1.
*/
Node getATrueSuccessor() {
result = getASuccessorByType(any(SuccessorTypes::BooleanSuccessor t | t.getValue() = true))
result = getASuccessorByType(any(BooleanSuccessor t | t.getValue() = true))
}
/**
@@ -236,7 +236,7 @@ module ControlFlow {
* on line 1.
*/
Node getAFalseSuccessor() {
result = getASuccessorByType(any(SuccessorTypes::BooleanSuccessor t | t.getValue() = false))
result = getASuccessorByType(any(BooleanSuccessor t | t.getValue() = false))
}
/**
@@ -256,7 +256,7 @@ module ControlFlow {
* `x` on line 1.
*/
Node getANullSuccessor() {
result = getASuccessorByType(any(SuccessorTypes::NullnessSuccessor t | t.isNull()))
result = getASuccessorByType(any(NullnessSuccessor t | t.isNull()))
}
/**
@@ -275,7 +275,7 @@ module ControlFlow {
* of the node `x`.
*/
Node getANonNullSuccessor() {
result = getASuccessorByType(any(SuccessorTypes::NullnessSuccessor t | not t.isNull()))
result = getASuccessorByType(any(NullnessSuccessor t | not t.isNull()))
}
/** Holds if this node has more than one predecessor. */
@@ -775,6 +775,7 @@ module ControlFlow {
}
}
}
private import SuccessorTypes
/**
* INTERNAL: Do not use.
@@ -2382,6 +2383,118 @@ module ControlFlow {
}
import Successor
/**
* Provides a basic block implementation on control flow elements. That is,
* a "pre-CFG" where the nodes are (unsplit) control flow elements and the
* successor releation is `succ = succ(pred, _)`.
*
* The logic is duplicated from the implementation in `BasicBlocks.qll`, and
* being an internal class, all predicate documentation has been removed.
*/
module PreBasicBlocks {
private predicate startsBB(ControlFlowElement cfe) {
not cfe = succ(_, _) and
(
exists(succ(cfe, _))
or
exists(succExit(cfe, _))
)
or
strictcount(ControlFlowElement pred, Completion c | cfe = succ(pred, c)) > 1
or
exists(ControlFlowElement pred, int i |
cfe = succ(pred, _) and
i = count(ControlFlowElement succ, Completion c | succ = succ(pred, c)) |
i > 1
or
i = 1 and
exists(succExit(pred, _))
)
}
private predicate intraBBSucc(ControlFlowElement pred, ControlFlowElement succ) {
succ = succ(pred, _) and
not startsBB(succ)
}
predicate bbIndex(ControlFlowElement bbStart, ControlFlowElement cfe, int i) =
shortestDistances(startsBB/1, intraBBSucc/2)(bbStart, cfe, i)
private predicate succBB(PreBasicBlock pred, PreBasicBlock succ) {
succ = pred.getASuccessor()
}
private predicate entryBB(PreBasicBlock bb) {
bb = succEntry(_)
}
private predicate bbIDominates(PreBasicBlock dom, PreBasicBlock bb) =
idominance(entryBB/1, succBB/2)(_, dom, bb)
class PreBasicBlock extends ControlFlowElement {
PreBasicBlock() {
startsBB(this)
}
PreBasicBlock getASuccessor() {
result = succ(this.getLastElement(), _)
}
PreBasicBlock getAPredecessor() {
result.getASuccessor() = this
}
ControlFlowElement getElement(int pos) {
bbIndex(this, result, pos)
}
ControlFlowElement getAnElement() {
result = this.getElement(_)
}
ControlFlowElement getFirstElement() {
result = this
}
ControlFlowElement getLastElement() {
result = this.getElement(length() - 1)
}
int length() {
result = strictcount(getAnElement())
}
predicate strictlyDominates(PreBasicBlock bb) {
bbIDominates+(this, bb)
}
predicate dominates(PreBasicBlock bb) {
bb = this
or
this.strictlyDominates(bb)
}
predicate inDominanceFrontier(PreBasicBlock df) {
this.dominatesPredecessor(df) and
not this.strictlyDominates(df)
}
private predicate dominatesPredecessor(PreBasicBlock df) {
this.dominates(df.getAPredecessor())
}
}
class ConditionBlock extends PreBasicBlock {
ConditionBlock() {
strictcount(ConditionalCompletion c |
exists(succ(this.getLastElement(), c))
or
exists(succExit(this.getLastElement(), c))
) > 1
}
}
}
/**
* Provides classes and predicates relevant for splitting the control flow graph.
*/
@@ -2464,7 +2577,7 @@ module ControlFlow {
*/
class FinallySplitType extends SuccessorType {
FinallySplitType() {
not this instanceof SuccessorTypes::ConditionalSuccessor
not this instanceof ConditionalSuccessor
}
/** Holds if this split type matches entry into a `finally` block with completion `c`. */
@@ -2472,7 +2585,7 @@ module ControlFlow {
if c instanceof NormalCompletion then
// If the entry into the `finally` block completes with any normal completion,
// it simply means normal execution after the `finally` block
this instanceof SuccessorTypes::NormalSuccessor
this instanceof NormalSuccessor
else
this.matchesCompletion(c)
}
@@ -2561,7 +2674,7 @@ module ControlFlow {
}
override string toString() {
if type instanceof SuccessorTypes::NormalSuccessor then
if type instanceof NormalSuccessor then
result = ""
else
result = "finally: " + type.toString()
@@ -2603,12 +2716,12 @@ module ControlFlow {
or
not c instanceof NormalCompletion
or
type instanceof SuccessorTypes::NormalSuccessor
type instanceof NormalSuccessor
) else (
// Finally block can exit with completion `c` derived from try/catch
// block: must match this split
type.matchesCompletion(c) and
not type instanceof SuccessorTypes::NormalSuccessor
not type instanceof NormalSuccessor
)
)
}
@@ -2895,7 +3008,7 @@ module ControlFlow {
pragma [noinline]
predicate succEntrySplits(Callable pred, ControlFlowElement succ, Splits succSplits, SuccessorType t) {
succ = succEntry(pred) and
t instanceof SuccessorTypes::NormalSuccessor and
t instanceof NormalSuccessor and
succSplits = TSplitsNil() // initially no splits
}

0
csharp/ql/test/library-tests/controlflow/graph/PreBasicBlockConsistency.expected Normal file
View File

50
csharp/ql/test/library-tests/controlflow/graph/PreBasicBlockConsistency.ql Normal file
View File

@@ -0,0 +1,50 @@
import csharp
import ControlFlow::Internal::PreBasicBlocks
predicate bbStartInconsistency(ControlFlowElement cfe) {
exists(ControlFlow::BasicBlock bb |
bb.getFirstNode() = cfe.getAControlFlowNode()
) and
not cfe = any(PreBasicBlock bb).getFirstElement()
}
predicate bbSuccInconsistency(ControlFlowElement pred, ControlFlowElement succ) {
exists(ControlFlow::BasicBlock predBB, ControlFlow::BasicBlock succBB |
predBB.getLastNode() = pred.getAControlFlowNode() and
succBB = predBB.getASuccessor() and
succBB.getFirstNode() = succ.getAControlFlowNode()
) and
not exists(PreBasicBlock predBB, PreBasicBlock succBB |
predBB.getLastElement() = pred and
succBB = predBB.getASuccessor() and
succBB.getFirstElement() = succ
)
}
predicate bbIntraSuccInconsistency(ControlFlowElement pred, ControlFlowElement succ) {
exists(ControlFlow::BasicBlock bb, int i |
pred.getAControlFlowNode() = bb.getNode(i) and
succ.getAControlFlowNode() = bb.getNode(i + 1)
) and
not exists(PreBasicBlock bb |
bb.getLastElement() = pred and
bb.getASuccessor().getFirstElement() = succ
) and
not exists(PreBasicBlock bb, int i |
bb.getElement(i) = pred and
bb.getElement(i + 1) = succ
)
}
from ControlFlowElement cfe1, ControlFlowElement cfe2, string s
where
bbStartInconsistency(cfe1) and
cfe2 = cfe1 and
s = "start inconsistency"
or
bbSuccInconsistency(cfe1, cfe2) and
s = "succ inconsistency"
or
bbIntraSuccInconsistency(cfe1, cfe2) and
s = "intra succ inconsistency"
select cfe1, cfe2, s