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

C#: Move PreBasicBlocks module into own file

Browse Source
This commit is contained in:
Tom Hvitved
2019-02-05 12:03:08 +01:00
parent 83fb32828f
commit 5306d1ea0d
4 changed files with 127 additions and 124 deletions
Download Patch File Download Diff File Expand all files Collapse all files

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

@@ -818,7 +818,7 @@ module ControlFlow {
* serve as their own entry-points, thus executing in some version of AST
* pre-order.
*/
private module Successor {
module Successor {
private import semmle.code.csharp.ExprOrStmtParent
private import semmle.code.csharp.controlflow.internal.NonReturning
@@ -2264,119 +2264,6 @@ 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)
}
private 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 getASuccessorByType(SuccessorType t) {
result = succ(this.getLastElement(), any(Completion c | t.matchesCompletion(c)))
}
PreBasicBlock getASuccessor() { result = this.getASuccessorByType(_) }
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 immediatelyDominates(PreBasicBlock bb) { bbIDominates(this, bb) }
predicate strictlyDominates(PreBasicBlock bb) { this.immediatelyDominates+(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
}
private predicate immediatelyControls(PreBasicBlock succ, ConditionalCompletion c) {
succ = succ(this.getLastElement(), c) and
forall(PreBasicBlock pred | pred = succ.getAPredecessor() and pred != this |
succ.dominates(pred)
)
}
predicate controls(PreBasicBlock controlled, ConditionalSuccessor s) {
exists(PreBasicBlock succ, ConditionalCompletion c | immediatelyControls(succ, c) |
succ.dominates(controlled) and
s.matchesCompletion(c)
)
}
}
}
/**
* Provides an SSA implementation based on "pre-basic-blocks", restricted
* to local scope variables and fields/properties that behave like local
@@ -2386,8 +2273,8 @@ module ControlFlow {
* being an internal class, all predicate documentation has been removed.
*/
module PreSsa {
private import PreBasicBlocks
private import AssignableDefinitions
private import semmle.code.csharp.controlflow.internal.PreBasicBlocks
/**
* A simple assignable. Either a local scope variable or a field/property
@@ -2489,7 +2376,7 @@ module ControlFlow {
}
private predicate assignableDefAt(
PreBasicBlocks::PreBasicBlock bb, int i, AssignableDefinition def, SimpleAssignable a
PreBasicBlock bb, int i, AssignableDefinition def, SimpleAssignable a
) {
bb.getElement(i) = def.getExpr() and
a = def.getTarget() and
@@ -2569,7 +2456,7 @@ module ControlFlow {
}
predicate assignableDefAtLive(
PreBasicBlocks::PreBasicBlock bb, int i, AssignableDefinition def, SimpleAssignable a
PreBasicBlock bb, int i, AssignableDefinition def, SimpleAssignable a
) {
assignableDefAt(bb, i, def, a) and
exists(int rnk | rnk = refRank(bb, i, a, Write(_)) |
@@ -3186,8 +3073,8 @@ module ControlFlow {
}
module BooleanSplitting {
private import PreBasicBlocks
private import PreSsa
private import semmle.code.csharp.controlflow.internal.PreBasicBlocks
/** A sub-classification of Boolean splits. */
abstract class BooleanSplitSubKind extends TBooleanSplitSubKind {
@@ -3859,12 +3746,13 @@ module ControlFlow {
cached
private module Cached {
private import semmle.code.csharp.controlflow.Guards as Guards
private import semmle.code.csharp.controlflow.internal.PreBasicBlocks
pragma[noinline]
private predicate phiNodeMaybeLive(
PreBasicBlocks::PreBasicBlock bb, PreSsa::SimpleAssignable a
PreBasicBlock bb, PreSsa::SimpleAssignable a
) {
exists(PreBasicBlocks::PreBasicBlock def | PreSsa::defAt(def, _, _, a) |
exists(PreBasicBlock def | PreSsa::defAt(def, _, _, a) |
def.inDominanceFrontier(bb)
)
}
@@ -3872,17 +3760,17 @@ module ControlFlow {
cached
newtype TPreSsaDef =
TExplicitPreSsaDef(
PreBasicBlocks::PreBasicBlock bb, int i, AssignableDefinition def,
PreBasicBlock bb, int i, AssignableDefinition def,
PreSsa::SimpleAssignable a
) {
Guards::Internal::CachedWithCFG::forceCachingInSameStage() and
PreSsa::assignableDefAtLive(bb, i, def, a)
} or
TImplicitEntryPreSsaDef(Callable c, PreBasicBlocks::PreBasicBlock bb, Assignable a) {
TImplicitEntryPreSsaDef(Callable c, PreBasicBlock bb, Assignable a) {
PreSsa::implicitEntryDef(c, bb, a) and
PreSsa::liveAtEntry(bb, a)
} or
TPhiPreSsaDef(PreBasicBlocks::PreBasicBlock bb, PreSsa::SimpleAssignable a) {
TPhiPreSsaDef(PreBasicBlock bb, PreSsa::SimpleAssignable a) {
phiNodeMaybeLive(bb, a) and
PreSsa::liveAtEntry(bb, a)
}

1
csharp/ql/src/semmle/code/csharp/controlflow/Guards.qll
View File

@@ -628,6 +628,7 @@ class NullGuardedDataFlowNode extends GuardedDataFlowNode {
/** INTERNAL: Do not use. */
module Internal {
private import ControlFlow::Internal
private import semmle.code.csharp.controlflow.internal.PreBasicBlocks as PreBasicBlocks
newtype TAbstractValue =
TBooleanValue(boolean b) { b = true or b = false } or

114
csharp/ql/src/semmle/code/csharp/controlflow/internal/PreBasicBlocks.qll Normal file
View File

@@ -0,0 +1,114 @@
/**
* INTERNAL: Do not use.
*
* 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.
*/
import csharp
private import semmle.code.csharp.controlflow.internal.Completion
private import semmle.code.csharp.controlflow.ControlFlowGraph::ControlFlow
private import Internal::Successor
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)
}
private 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 getASuccessorByType(SuccessorType t) {
result = succ(this.getLastElement(), any(Completion c | t.matchesCompletion(c)))
}
PreBasicBlock getASuccessor() { result = this.getASuccessorByType(_) }
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 immediatelyDominates(PreBasicBlock bb) { bbIDominates(this, bb) }
predicate strictlyDominates(PreBasicBlock bb) { this.immediatelyDominates+(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
}
private predicate immediatelyControls(PreBasicBlock succ, ConditionalCompletion c) {
succ = succ(this.getLastElement(), c) and
forall(PreBasicBlock pred | pred = succ.getAPredecessor() and pred != this |
succ.dominates(pred)
)
}
predicate controls(PreBasicBlock controlled, SuccessorTypes::ConditionalSuccessor s) {
exists(PreBasicBlock succ, ConditionalCompletion c | immediatelyControls(succ, c) |
succ.dominates(controlled) and
s.matchesCompletion(c)
)
}
}

2
csharp/ql/test/library-tests/controlflow/graph/PreBasicBlockConsistency.ql
View File

@@ -1,5 +1,5 @@
import csharp
import ControlFlow::Internal::PreBasicBlocks
import semmle.code.csharp.controlflow.internal.PreBasicBlocks
predicate bbStartInconsistency(ControlFlowElement cfe) {
exists(ControlFlow::BasicBlock bb | bb.getFirstNode() = cfe.getAControlFlowNode()) and