mirror of
https://github.com/github/codeql.git
synced 2026-04-30 19:26:02 +02:00
C#: Use shared SSA implementation for BaseSsa
This commit is contained in:
Tom Hvitved
@@ -428,6 +428,7 @@
|
||||
],
|
||||
"SSA C#": [
|
||||
"csharp/ql/src/semmle/code/csharp/dataflow/internal/SsaImplCommon.qll",
|
||||
"csharp/ql/src/semmle/code/csharp/controlflow/internal/pressa/SsaImplCommon.qll"
|
||||
"csharp/ql/src/semmle/code/csharp/controlflow/internal/pressa/SsaImplCommon.qll",
|
||||
"csharp/ql/src/semmle/code/csharp/dataflow/internal/basessa/SsaImplCommon.qll"
|
||||
]
|
||||
}
|
||||
@@ -1,125 +1,43 @@
|
||||
import csharp
|
||||
|
||||
/**
|
||||
* INTERNAL: Do not use.
|
||||
*
|
||||
* Provides a simple SSA implementation for local scope variables.
|
||||
*/
|
||||
module BaseSsa {
|
||||
private import ControlFlow
|
||||
private import AssignableDefinitions
|
||||
import basessa.SsaImplSpecific
|
||||
private import basessa.SsaImplCommon as SsaImpl
|
||||
|
||||
pragma[noinline]
|
||||
Callable getAnAssigningCallable(LocalScopeVariable v) {
|
||||
result = any(AssignableDefinition def | def.getTarget() = v).getEnclosingCallable()
|
||||
class Definition extends SsaImpl::Definition {
|
||||
final AssignableRead getARead() {
|
||||
exists(BasicBlock bb, int i |
|
||||
SsaImpl::ssaDefReachesRead(_, this, bb, i) and
|
||||
result.getAControlFlowNode() = bb.getNode(i)
|
||||
)
|
||||
}
|
||||
|
||||
final AssignableDefinition getDefinition() {
|
||||
exists(BasicBlock bb, int i, SourceVariable v |
|
||||
this.definesAt(v, bb, i) and
|
||||
definitionAt(result, bb, i, v)
|
||||
)
|
||||
}
|
||||
|
||||
private Definition getAPhiInputOrPriorDefinition() {
|
||||
result = this.(PhiNode).getAnInput() or
|
||||
SsaImpl::uncertainWriteDefinitionInput(this, result)
|
||||
}
|
||||
|
||||
final Definition getAnUltimateDefinition() {
|
||||
result = this.getAPhiInputOrPriorDefinition*() and
|
||||
not result instanceof PhiNode
|
||||
}
|
||||
|
||||
Location getLocation() { result = this.getDefinition().getLocation() }
|
||||
}
|
||||
|
||||
private class SimpleLocalScopeVariable extends LocalScopeVariable {
|
||||
SimpleLocalScopeVariable() { not getAnAssigningCallable(this) != getAnAssigningCallable(this) }
|
||||
}
|
||||
class PhiNode extends SsaImpl::PhiNode, Definition {
|
||||
override Location getLocation() { result = this.getBasicBlock().getLocation() }
|
||||
|
||||
/**
|
||||
* Holds if the `i`th node of basic block `bb` is assignable definition `def`,
|
||||
* targeting local scope variable `v`.
|
||||
*/
|
||||
private predicate defAt(BasicBlock bb, int i, AssignableDefinition def, SimpleLocalScopeVariable v) {
|
||||
bb.getNode(i) = def.getAControlFlowNode() and
|
||||
v = def.getTarget() and
|
||||
// In cases like `(x, x) = (0, 1)`, we discard the first (dead) definition of `x`
|
||||
not exists(TupleAssignmentDefinition first, TupleAssignmentDefinition second | first = def |
|
||||
second.getAssignment() = first.getAssignment() and
|
||||
second.getEvaluationOrder() > first.getEvaluationOrder() and
|
||||
second.getTarget() = v
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if basic block `bb` would need to start with a phi node for local scope
|
||||
* variable `v` in an SSA representation.
|
||||
*/
|
||||
private predicate needsPhiNode(BasicBlock bb, SimpleLocalScopeVariable v) {
|
||||
exists(BasicBlock def | def.inDominanceFrontier(bb) |
|
||||
defAt(def, _, _, v) or
|
||||
needsPhiNode(def, v)
|
||||
)
|
||||
}
|
||||
|
||||
private newtype SsaRefKind =
|
||||
SsaRead() or
|
||||
SsaDef()
|
||||
|
||||
/**
|
||||
* Holds if the `i`th node of basic block `bb` is a reference to `v`,
|
||||
* either a read (when `k` is `SsaRead()`) or a write including phi nodes
|
||||
* (when `k` is `SsaDef()`).
|
||||
*/
|
||||
private predicate ssaRef(BasicBlock bb, int i, SimpleLocalScopeVariable v, SsaRefKind k) {
|
||||
bb.getNode(i).getElement() = v.getAnAccess().(VariableRead) and
|
||||
k = SsaRead()
|
||||
or
|
||||
defAt(bb, i, _, v) and
|
||||
k = SsaDef()
|
||||
or
|
||||
needsPhiNode(bb, v) and
|
||||
i = -1 and
|
||||
k = SsaDef()
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets the (1-based) rank of the reference to `v` at the `i`th node of basic
|
||||
* block `bb`, which has the given reference kind `k`.
|
||||
*/
|
||||
private int ssaRefRank(BasicBlock bb, int i, SimpleLocalScopeVariable v, SsaRefKind k) {
|
||||
i = rank[result](int j | ssaRef(bb, j, v, _)) and
|
||||
ssaRef(bb, i, v, k)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if definition `def` of local scope variable `v` inside basic block
|
||||
* `bb` reaches the reference at rank `rnk`, without passing through another
|
||||
* definition of `v`, including phi nodes.
|
||||
*/
|
||||
private predicate defReachesRank(
|
||||
BasicBlock bb, AssignableDefinition def, SimpleLocalScopeVariable v, int rnk
|
||||
) {
|
||||
exists(int i | rnk = ssaRefRank(bb, i, v, SsaDef()) | defAt(bb, i, def, v))
|
||||
or
|
||||
defReachesRank(bb, def, v, rnk - 1) and
|
||||
rnk = ssaRefRank(bb, _, v, SsaRead())
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if definition `def` of local scope variable `v` reaches the end of
|
||||
* basic block `bb` without passing through another definition of `v`, including
|
||||
* phi nodes.
|
||||
*/
|
||||
private predicate reachesEndOf(AssignableDefinition def, SimpleLocalScopeVariable v, BasicBlock bb) {
|
||||
exists(int rnk |
|
||||
defReachesRank(bb, def, v, rnk) and
|
||||
rnk = max(ssaRefRank(bb, _, v, _))
|
||||
)
|
||||
or
|
||||
exists(BasicBlock mid |
|
||||
reachesEndOf(def, v, mid) and
|
||||
not exists(ssaRefRank(bb, _, v, SsaDef())) and
|
||||
bb = mid.getASuccessor()
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets a read of the SSA definition for variable `v` at definition `def`. That is,
|
||||
* a read that is guaranteed to read the value assigned at definition `def`.
|
||||
*/
|
||||
cached
|
||||
AssignableRead getARead(AssignableDefinition def, SimpleLocalScopeVariable v) {
|
||||
exists(BasicBlock bb, int i, int rnk |
|
||||
result.getAControlFlowNode() = bb.getNode(i) and
|
||||
rnk = ssaRefRank(bb, i, v, SsaRead())
|
||||
|
|
||||
defReachesRank(bb, def, v, rnk)
|
||||
or
|
||||
reachesEndOf(def, v, bb.getAPredecessor()) and
|
||||
not ssaRefRank(bb, _, v, SsaDef()) < rnk
|
||||
)
|
||||
final Definition getAnInput() { SsaImpl::phiHasInputFromBlock(this, result, _) }
|
||||
}
|
||||
}
|
||||
|
||||
@@ -16,7 +16,10 @@ module Steps {
|
||||
* Gets a read that is guaranteed to read the value assigned at definition `def`.
|
||||
*/
|
||||
private AssignableRead getARead(AssignableDefinition def) {
|
||||
result = BaseSsa::getARead(def, _)
|
||||
exists(BaseSsa::Definition ssaDef |
|
||||
ssaDef.getDefinition() = def and
|
||||
result = ssaDef.getARead()
|
||||
)
|
||||
or
|
||||
exists(LocalScopeVariable v | def.getTarget() = v |
|
||||
result = v.getAnAccess() and
|
||||
|
||||
@@ -0,0 +1,619 @@
|
||||
/**
|
||||
* Provides a language-independant implementation of static single assignment
|
||||
* (SSA) form.
|
||||
*/
|
||||
|
||||
private import SsaImplSpecific
|
||||
|
||||
private BasicBlock getABasicBlockPredecessor(BasicBlock bb) { getABasicBlockSuccessor(result) = bb }
|
||||
|
||||
/**
|
||||
* Liveness analysis (based on source variables) to restrict the size of the
|
||||
* SSA representation.
|
||||
*/
|
||||
private module Liveness {
|
||||
/**
|
||||
* A classification of variable references into reads (of a given kind) and
|
||||
* (certain or uncertain) writes.
|
||||
*/
|
||||
private newtype TRefKind =
|
||||
Read(boolean certain) { certain in [false, true] } or
|
||||
Write(boolean certain) { certain in [false, true] }
|
||||
|
||||
private class RefKind extends TRefKind {
|
||||
string toString() {
|
||||
exists(boolean certain | this = Read(certain) and result = "read (" + certain + ")")
|
||||
or
|
||||
exists(boolean certain | this = Write(certain) and result = "write (" + certain + ")")
|
||||
}
|
||||
|
||||
int getOrder() {
|
||||
this = Read(_) and
|
||||
result = 0
|
||||
or
|
||||
this = Write(_) and
|
||||
result = 1
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the `i`th node of basic block `bb` is a reference to `v` of kind `k`.
|
||||
*/
|
||||
private predicate ref(BasicBlock bb, int i, SourceVariable v, RefKind k) {
|
||||
exists(boolean certain | variableRead(bb, i, v, certain) | k = Read(certain))
|
||||
or
|
||||
exists(boolean certain | variableWrite(bb, i, v, certain) | k = Write(certain))
|
||||
}
|
||||
|
||||
private newtype OrderedRefIndex =
|
||||
MkOrderedRefIndex(int i, int tag) {
|
||||
exists(RefKind rk | ref(_, i, _, rk) | tag = rk.getOrder())
|
||||
}
|
||||
|
||||
private OrderedRefIndex refOrd(BasicBlock bb, int i, SourceVariable v, RefKind k, int ord) {
|
||||
ref(bb, i, v, k) and
|
||||
result = MkOrderedRefIndex(i, ord) and
|
||||
ord = k.getOrder()
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets the (1-based) rank of the reference to `v` at the `i`th node of
|
||||
* basic block `bb`, which has the given reference kind `k`.
|
||||
*
|
||||
* Reads are considered before writes when they happen at the same index.
|
||||
*/
|
||||
private int refRank(BasicBlock bb, int i, SourceVariable v, RefKind k) {
|
||||
refOrd(bb, i, v, k, _) =
|
||||
rank[result](int j, int ord, OrderedRefIndex res |
|
||||
res = refOrd(bb, j, v, _, ord)
|
||||
|
|
||||
res order by j, ord
|
||||
)
|
||||
}
|
||||
|
||||
private int maxRefRank(BasicBlock bb, SourceVariable v) {
|
||||
result = refRank(bb, _, v, _) and
|
||||
not result + 1 = refRank(bb, _, v, _)
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets the (1-based) rank of the first reference to `v` inside basic block `bb`
|
||||
* that is either a read or a certain write.
|
||||
*/
|
||||
private int firstReadOrCertainWrite(BasicBlock bb, SourceVariable v) {
|
||||
result =
|
||||
min(int r, RefKind k |
|
||||
r = refRank(bb, _, v, k) and
|
||||
k != Write(false)
|
||||
|
|
||||
r
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if source variable `v` is live at the beginning of basic block `bb`.
|
||||
*/
|
||||
predicate liveAtEntry(BasicBlock bb, SourceVariable v) {
|
||||
// The first read or certain write to `v` inside `bb` is a read
|
||||
refRank(bb, _, v, Read(_)) = firstReadOrCertainWrite(bb, v)
|
||||
or
|
||||
// There is no certain write to `v` inside `bb`, but `v` is live at entry
|
||||
// to a successor basic block of `bb`
|
||||
not exists(firstReadOrCertainWrite(bb, v)) and
|
||||
liveAtExit(bb, v)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if source variable `v` is live at the end of basic block `bb`.
|
||||
*/
|
||||
predicate liveAtExit(BasicBlock bb, SourceVariable v) {
|
||||
liveAtEntry(getABasicBlockSuccessor(bb), v)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if variable `v` is live in basic block `bb` at index `i`.
|
||||
* The rank of `i` is `rnk` as defined by `refRank()`.
|
||||
*/
|
||||
private predicate liveAtRank(BasicBlock bb, int i, SourceVariable v, int rnk) {
|
||||
exists(RefKind kind | rnk = refRank(bb, i, v, kind) |
|
||||
rnk = maxRefRank(bb, v) and
|
||||
liveAtExit(bb, v)
|
||||
or
|
||||
ref(bb, i, v, kind) and
|
||||
kind = Read(_)
|
||||
or
|
||||
exists(RefKind nextKind |
|
||||
liveAtRank(bb, _, v, rnk + 1) and
|
||||
rnk + 1 = refRank(bb, _, v, nextKind) and
|
||||
nextKind != Write(true)
|
||||
)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if variable `v` is live after the (certain or uncertain) write at
|
||||
* index `i` inside basic block `bb`.
|
||||
*/
|
||||
predicate liveAfterWrite(BasicBlock bb, int i, SourceVariable v) {
|
||||
exists(int rnk | rnk = refRank(bb, i, v, Write(_)) | liveAtRank(bb, i, v, rnk))
|
||||
}
|
||||
}
|
||||
|
||||
private import Liveness
|
||||
|
||||
/** Holds if `bb1` strictly dominates `bb2`. */
|
||||
private predicate strictlyDominates(BasicBlock bb1, BasicBlock bb2) {
|
||||
bb1 = getImmediateBasicBlockDominator+(bb2)
|
||||
}
|
||||
|
||||
/** Holds if `bb1` dominates a predecessor of `bb2`. */
|
||||
private predicate dominatesPredecessor(BasicBlock bb1, BasicBlock bb2) {
|
||||
exists(BasicBlock pred | pred = getABasicBlockPredecessor(bb2) |
|
||||
bb1 = pred
|
||||
or
|
||||
strictlyDominates(bb1, pred)
|
||||
)
|
||||
}
|
||||
|
||||
/** Holds if `df` is in the dominance frontier of `bb`. */
|
||||
private predicate inDominanceFrontier(BasicBlock bb, BasicBlock df) {
|
||||
dominatesPredecessor(bb, df) and
|
||||
not strictlyDominates(bb, df)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `bb` is in the dominance frontier of a block containing a
|
||||
* definition of `v`.
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate inDefDominanceFrontier(BasicBlock bb, SourceVariable v) {
|
||||
exists(BasicBlock defbb, Definition def |
|
||||
def.definesAt(v, defbb, _) and
|
||||
inDominanceFrontier(defbb, bb)
|
||||
)
|
||||
}
|
||||
|
||||
cached
|
||||
newtype TDefinition =
|
||||
TWriteDef(SourceVariable v, BasicBlock bb, int i) {
|
||||
variableWrite(bb, i, v, _) and
|
||||
liveAfterWrite(bb, i, v)
|
||||
} or
|
||||
TPhiNode(SourceVariable v, BasicBlock bb) {
|
||||
inDefDominanceFrontier(bb, v) and
|
||||
liveAtEntry(bb, v)
|
||||
}
|
||||
|
||||
private module SsaDefReaches {
|
||||
newtype TSsaRefKind =
|
||||
SsaRead() or
|
||||
SsaDef()
|
||||
|
||||
/**
|
||||
* A classification of SSA variable references into reads and definitions.
|
||||
*/
|
||||
class SsaRefKind extends TSsaRefKind {
|
||||
string toString() {
|
||||
this = SsaRead() and
|
||||
result = "SsaRead"
|
||||
or
|
||||
this = SsaDef() and
|
||||
result = "SsaDef"
|
||||
}
|
||||
|
||||
int getOrder() {
|
||||
this = SsaRead() and
|
||||
result = 0
|
||||
or
|
||||
this = SsaDef() and
|
||||
result = 1
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the `i`th node of basic block `bb` is a reference to `v`,
|
||||
* either a read (when `k` is `SsaRead()`) or an SSA definition (when `k`
|
||||
* is `SsaDef()`).
|
||||
*
|
||||
* Unlike `Liveness::ref`, this includes `phi` nodes.
|
||||
*/
|
||||
predicate ssaRef(BasicBlock bb, int i, SourceVariable v, SsaRefKind k) {
|
||||
variableRead(bb, i, v, _) and
|
||||
k = SsaRead()
|
||||
or
|
||||
exists(Definition def | def.definesAt(v, bb, i)) and
|
||||
k = SsaDef()
|
||||
}
|
||||
|
||||
private newtype OrderedSsaRefIndex =
|
||||
MkOrderedSsaRefIndex(int i, SsaRefKind k) { ssaRef(_, i, _, k) }
|
||||
|
||||
private OrderedSsaRefIndex ssaRefOrd(BasicBlock bb, int i, SourceVariable v, SsaRefKind k, int ord) {
|
||||
ssaRef(bb, i, v, k) and
|
||||
result = MkOrderedSsaRefIndex(i, k) and
|
||||
ord = k.getOrder()
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets the (1-based) rank of the reference to `v` at the `i`th node of basic
|
||||
* block `bb`, which has the given reference kind `k`.
|
||||
*
|
||||
* For example, if `bb` is a basic block with a phi node for `v` (considered
|
||||
* to be at index -1), reads `v` at node 2, and defines it at node 5, we have:
|
||||
*
|
||||
* ```ql
|
||||
* ssaRefRank(bb, -1, v, SsaDef()) = 1 // phi node
|
||||
* ssaRefRank(bb, 2, v, Read()) = 2 // read at node 2
|
||||
* ssaRefRank(bb, 5, v, SsaDef()) = 3 // definition at node 5
|
||||
* ```
|
||||
*
|
||||
* Reads are considered before writes when they happen at the same index.
|
||||
*/
|
||||
int ssaRefRank(BasicBlock bb, int i, SourceVariable v, SsaRefKind k) {
|
||||
ssaRefOrd(bb, i, v, k, _) =
|
||||
rank[result](int j, int ord, OrderedSsaRefIndex res |
|
||||
res = ssaRefOrd(bb, j, v, _, ord)
|
||||
|
|
||||
res order by j, ord
|
||||
)
|
||||
}
|
||||
|
||||
int maxSsaRefRank(BasicBlock bb, SourceVariable v) {
|
||||
result = ssaRefRank(bb, _, v, _) and
|
||||
not result + 1 = ssaRefRank(bb, _, v, _)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the SSA definition `def` reaches rank index `rnk` in its own
|
||||
* basic block `bb`.
|
||||
*/
|
||||
predicate ssaDefReachesRank(BasicBlock bb, Definition def, int rnk, SourceVariable v) {
|
||||
exists(int i |
|
||||
rnk = ssaRefRank(bb, i, v, SsaDef()) and
|
||||
def.definesAt(v, bb, i)
|
||||
)
|
||||
or
|
||||
ssaDefReachesRank(bb, def, rnk - 1, v) and
|
||||
rnk = ssaRefRank(bb, _, v, SsaRead())
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the SSA definition of `v` at `def` reaches index `i` in the same
|
||||
* basic block `bb`, without crossing another SSA definition of `v`.
|
||||
*/
|
||||
predicate ssaDefReachesReadWithinBlock(SourceVariable v, Definition def, BasicBlock bb, int i) {
|
||||
exists(int rnk |
|
||||
ssaDefReachesRank(bb, def, rnk, v) and
|
||||
rnk = ssaRefRank(bb, i, v, SsaRead()) and
|
||||
variableRead(bb, i, v, _)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the SSA definition of `v` at `def` reaches uncertain SSA definition
|
||||
* `redef` in the same basic block, without crossing another SSA definition of `v`.
|
||||
*/
|
||||
predicate ssaDefReachesUncertainDefWithinBlock(
|
||||
SourceVariable v, Definition def, UncertainWriteDefinition redef
|
||||
) {
|
||||
exists(BasicBlock bb, int rnk, int i |
|
||||
ssaDefReachesRank(bb, def, rnk, v) and
|
||||
rnk = ssaRefRank(bb, i, v, SsaDef()) - 1 and
|
||||
redef.definesAt(v, bb, i)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Same as `ssaRefRank()`, but restricted to a particular SSA definition `def`.
|
||||
*/
|
||||
int ssaDefRank(Definition def, SourceVariable v, BasicBlock bb, int i, SsaRefKind k) {
|
||||
v = def.getSourceVariable() and
|
||||
result = ssaRefRank(bb, i, v, k) and
|
||||
(
|
||||
ssaDefReachesRead(_, def, bb, i)
|
||||
or
|
||||
def.definesAt(_, bb, i)
|
||||
)
|
||||
}
|
||||
|
||||
predicate defOccursInBlock(Definition def, BasicBlock bb, SourceVariable v) {
|
||||
exists(ssaDefRank(def, v, bb, _, _))
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private BasicBlock getAMaybeLiveSuccessor(Definition def, BasicBlock bb) {
|
||||
result = getABasicBlockSuccessor(bb) and
|
||||
not defOccursInBlock(_, bb, def.getSourceVariable()) and
|
||||
ssaDefReachesEndOfBlock(bb, def, _)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `def` is accessed in basic block `bb1` (either a read or a write),
|
||||
* `bb2` is a transitive successor of `bb1`, `def` is live at the end of `bb1`,
|
||||
* and the underlying variable for `def` is neither read nor written in any block
|
||||
* on the path between `bb1` and `bb2`.
|
||||
*/
|
||||
predicate varBlockReaches(Definition def, BasicBlock bb1, BasicBlock bb2) {
|
||||
defOccursInBlock(def, bb1, _) and
|
||||
bb2 = getABasicBlockSuccessor(bb1)
|
||||
or
|
||||
exists(BasicBlock mid | varBlockReaches(def, bb1, mid) | bb2 = getAMaybeLiveSuccessor(def, mid))
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `def` is accessed in basic block `bb1` (either a read or a write),
|
||||
* `def` is read at index `i2` in basic block `bb2`, `bb2` is in a transitive
|
||||
* successor block of `bb1`, and `def` is neither read nor written in any block
|
||||
* on a path between `bb1` and `bb2`.
|
||||
*/
|
||||
predicate defAdjacentRead(Definition def, BasicBlock bb1, BasicBlock bb2, int i2) {
|
||||
varBlockReaches(def, bb1, bb2) and
|
||||
ssaRefRank(bb2, i2, def.getSourceVariable(), SsaRead()) = 1 and
|
||||
variableRead(bb2, i2, _, _)
|
||||
}
|
||||
}
|
||||
|
||||
private import SsaDefReaches
|
||||
|
||||
pragma[noinline]
|
||||
private predicate ssaDefReachesEndOfBlockRec(BasicBlock bb, Definition def, SourceVariable v) {
|
||||
exists(BasicBlock idom | ssaDefReachesEndOfBlock(idom, def, v) |
|
||||
// The construction of SSA form ensures that each read of a variable is
|
||||
// dominated by its definition. An SSA definition therefore reaches a
|
||||
// control flow node if it is the _closest_ SSA definition that dominates
|
||||
// the node. If two definitions dominate a node then one must dominate the
|
||||
// other, so therefore the definition of _closest_ is given by the dominator
|
||||
// tree. Thus, reaching definitions can be calculated in terms of dominance.
|
||||
idom = getImmediateBasicBlockDominator(bb)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* NB: If this predicate is exposed, it should be cached.
|
||||
*
|
||||
* Holds if the SSA definition of `v` at `def` reaches the end of basic
|
||||
* block `bb`, at which point it is still live, without crossing another
|
||||
* SSA definition of `v`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate ssaDefReachesEndOfBlock(BasicBlock bb, Definition def, SourceVariable v) {
|
||||
exists(int last | last = maxSsaRefRank(bb, v) |
|
||||
ssaDefReachesRank(bb, def, last, v) and
|
||||
liveAtExit(bb, v)
|
||||
)
|
||||
or
|
||||
ssaDefReachesEndOfBlockRec(bb, def, v) and
|
||||
liveAtExit(bb, v) and
|
||||
not ssaRef(bb, _, v, SsaDef())
|
||||
}
|
||||
|
||||
/**
|
||||
* NB: If this predicate is exposed, it should be cached.
|
||||
*
|
||||
* Holds if `inp` is an input to the phi node `phi` along the edge originating in `bb`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate phiHasInputFromBlock(PhiNode phi, Definition inp, BasicBlock bb) {
|
||||
exists(SourceVariable v, BasicBlock bbDef |
|
||||
phi.definesAt(v, bbDef, _) and
|
||||
getABasicBlockPredecessor(bbDef) = bb and
|
||||
ssaDefReachesEndOfBlock(bb, inp, v)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* NB: If this predicate is exposed, it should be cached.
|
||||
*
|
||||
* Holds if the SSA definition of `v` at `def` reaches a read at index `i` in
|
||||
* basic block `bb`, without crossing another SSA definition of `v`. The read
|
||||
* is of kind `rk`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate ssaDefReachesRead(SourceVariable v, Definition def, BasicBlock bb, int i) {
|
||||
ssaDefReachesReadWithinBlock(v, def, bb, i)
|
||||
or
|
||||
variableRead(bb, i, v, _) and
|
||||
ssaDefReachesEndOfBlock(getABasicBlockPredecessor(bb), def, v) and
|
||||
not ssaDefReachesReadWithinBlock(v, _, bb, i)
|
||||
}
|
||||
|
||||
/**
|
||||
* NB: If this predicate is exposed, it should be cached.
|
||||
*
|
||||
* Holds if `def` is accessed at index `i1` in basic block `bb1` (either a read
|
||||
* or a write), `def` is read at index `i2` in basic block `bb2`, and there is a
|
||||
* path between them without any read of `def`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate adjacentDefRead(Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2) {
|
||||
exists(int rnk |
|
||||
rnk = ssaDefRank(def, _, bb1, i1, _) and
|
||||
rnk + 1 = ssaDefRank(def, _, bb1, i2, SsaRead()) and
|
||||
variableRead(bb1, i2, _, _) and
|
||||
bb2 = bb1
|
||||
)
|
||||
or
|
||||
exists(SourceVariable v | ssaDefRank(def, v, bb1, i1, _) = maxSsaRefRank(bb1, v)) and
|
||||
defAdjacentRead(def, bb1, bb2, i2)
|
||||
}
|
||||
|
||||
private predicate adjacentDefReachesRead(
|
||||
Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2
|
||||
) {
|
||||
adjacentDefRead(def, bb1, i1, bb2, i2) and
|
||||
exists(SourceVariable v | v = def.getSourceVariable() |
|
||||
ssaRef(bb1, i1, v, SsaDef())
|
||||
or
|
||||
variableRead(bb1, i1, v, true)
|
||||
)
|
||||
or
|
||||
exists(BasicBlock bb3, int i3 |
|
||||
adjacentDefReachesRead(def, bb1, i1, bb3, i3) and
|
||||
variableRead(bb3, i3, _, false) and
|
||||
adjacentDefRead(def, bb3, i3, bb2, i2)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* NB: If this predicate is exposed, it should be cached.
|
||||
*
|
||||
* Same as `adjacentDefRead`, but ignores uncertain reads.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate adjacentDefNoUncertainReads(Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2) {
|
||||
adjacentDefReachesRead(def, bb1, i1, bb2, i2) and
|
||||
variableRead(bb2, i2, _, true)
|
||||
}
|
||||
|
||||
/**
|
||||
* NB: If this predicate is exposed, it should be cached.
|
||||
*
|
||||
* Holds if the node at index `i` in `bb` is a last reference to SSA definition
|
||||
* `def`. The reference is last because it can reach another write `next`,
|
||||
* without passing through another read or write.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate lastRefRedef(Definition def, BasicBlock bb, int i, Definition next) {
|
||||
exists(int rnk, SourceVariable v, int j | rnk = ssaDefRank(def, v, bb, i, _) |
|
||||
// Next reference to `v` inside `bb` is a write
|
||||
next.definesAt(v, bb, j) and
|
||||
rnk + 1 = ssaRefRank(bb, j, v, SsaDef())
|
||||
or
|
||||
// Can reach a write using one or more steps
|
||||
rnk = maxSsaRefRank(bb, v) and
|
||||
exists(BasicBlock bb2 |
|
||||
varBlockReaches(def, bb, bb2) and
|
||||
next.definesAt(v, bb2, j) and
|
||||
1 = ssaRefRank(bb2, j, v, SsaDef())
|
||||
)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* NB: If this predicate is exposed, it should be cached.
|
||||
*
|
||||
* Holds if `inp` is an immediately preceding definition of uncertain definition
|
||||
* `def`. Since `def` is uncertain, the value from the preceding definition might
|
||||
* still be valid.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate uncertainWriteDefinitionInput(UncertainWriteDefinition def, Definition inp) {
|
||||
lastRefRedef(inp, _, _, def)
|
||||
}
|
||||
|
||||
private predicate adjacentDefReachesUncertainRead(
|
||||
Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2
|
||||
) {
|
||||
adjacentDefReachesRead(def, bb1, i1, bb2, i2) and
|
||||
variableRead(bb2, i2, _, false)
|
||||
}
|
||||
|
||||
/**
|
||||
* NB: If this predicate is exposed, it should be cached.
|
||||
*
|
||||
* Same as `lastRefRedef`, but ignores uncertain reads.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate lastRefRedefNoUncertainReads(Definition def, BasicBlock bb, int i, Definition next) {
|
||||
lastRefRedef(def, bb, i, next) and
|
||||
not variableRead(bb, i, def.getSourceVariable(), false)
|
||||
or
|
||||
exists(BasicBlock bb0, int i0 |
|
||||
lastRefRedef(def, bb0, i0, next) and
|
||||
adjacentDefReachesUncertainRead(def, bb, i, bb0, i0)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* NB: If this predicate is exposed, it should be cached.
|
||||
*
|
||||
* Holds if the node at index `i` in `bb` is a last reference to SSA
|
||||
* definition `def`.
|
||||
*
|
||||
* That is, the node can reach the end of the enclosing callable, or another
|
||||
* SSA definition for the underlying source variable, without passing through
|
||||
* another read.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate lastRef(Definition def, BasicBlock bb, int i) {
|
||||
lastRefRedef(def, bb, i, _)
|
||||
or
|
||||
exists(SourceVariable v | ssaDefRank(def, v, bb, i, _) = maxSsaRefRank(bb, v) |
|
||||
// Can reach exit directly
|
||||
bb instanceof ExitBasicBlock
|
||||
or
|
||||
// Can reach a block using one or more steps, where `def` is no longer live
|
||||
exists(BasicBlock bb2 | varBlockReaches(def, bb, bb2) |
|
||||
not defOccursInBlock(def, bb2, _) and
|
||||
not ssaDefReachesEndOfBlock(bb2, def, _)
|
||||
)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* NB: If this predicate is exposed, it should be cached.
|
||||
*
|
||||
* Same as `lastRefRedef`, but ignores uncertain reads.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate lastRefNoUncertainReads(Definition def, BasicBlock bb, int i) {
|
||||
lastRef(def, bb, i) and
|
||||
not variableRead(bb, i, def.getSourceVariable(), false)
|
||||
or
|
||||
exists(BasicBlock bb0, int i0 |
|
||||
lastRef(def, bb0, i0) and
|
||||
adjacentDefReachesUncertainRead(def, bb, i, bb0, i0)
|
||||
)
|
||||
}
|
||||
|
||||
/** A static single assignment (SSA) definition. */
|
||||
class Definition extends TDefinition {
|
||||
/** Gets the source variable underlying this SSA definition. */
|
||||
SourceVariable getSourceVariable() { this.definesAt(result, _, _) }
|
||||
|
||||
/**
|
||||
* Holds if this SSA definition defines `v` at index `i` in basic block `bb`.
|
||||
* Phi nodes are considered to be at index `-1`, while normal variable writes
|
||||
* are at the index of the control flow node they wrap.
|
||||
*/
|
||||
final predicate definesAt(SourceVariable v, BasicBlock bb, int i) {
|
||||
this = TWriteDef(v, bb, i)
|
||||
or
|
||||
this = TPhiNode(v, bb) and i = -1
|
||||
}
|
||||
|
||||
/** Gets the basic block to which this SSA definition belongs. */
|
||||
final BasicBlock getBasicBlock() { this.definesAt(_, result, _) }
|
||||
|
||||
/** Gets a textual representation of this SSA definition. */
|
||||
string toString() { none() }
|
||||
}
|
||||
|
||||
/** An SSA definition that corresponds to a write. */
|
||||
class WriteDefinition extends Definition, TWriteDef {
|
||||
private SourceVariable v;
|
||||
private BasicBlock bb;
|
||||
private int i;
|
||||
|
||||
WriteDefinition() { this = TWriteDef(v, bb, i) }
|
||||
|
||||
override string toString() { result = "WriteDef" }
|
||||
}
|
||||
|
||||
/** A phi node. */
|
||||
class PhiNode extends Definition, TPhiNode {
|
||||
override string toString() { result = "Phi" }
|
||||
}
|
||||
|
||||
/**
|
||||
* An SSA definition that represents an uncertain update of the underlying
|
||||
* source variable.
|
||||
*/
|
||||
class UncertainWriteDefinition extends WriteDefinition {
|
||||
UncertainWriteDefinition() {
|
||||
exists(SourceVariable v, BasicBlock bb, int i |
|
||||
this.definesAt(v, bb, i) and
|
||||
variableWrite(bb, i, v, false)
|
||||
)
|
||||
}
|
||||
}
|
||||
@@ -0,0 +1,51 @@
|
||||
/** Provides the C# specific parameters for `SsaImplCommon.qll`. */
|
||||
|
||||
private import csharp
|
||||
private import AssignableDefinitions
|
||||
|
||||
class BasicBlock = ControlFlow::BasicBlock;
|
||||
|
||||
BasicBlock getImmediateBasicBlockDominator(BasicBlock bb) { result = bb.getImmediateDominator() }
|
||||
|
||||
BasicBlock getABasicBlockSuccessor(BasicBlock bb) { result = bb.getASuccessor() }
|
||||
|
||||
class ExitBasicBlock = ControlFlow::BasicBlocks::ExitBlock;
|
||||
|
||||
pragma[noinline]
|
||||
private Callable getAnAssigningCallable(LocalScopeVariable v) {
|
||||
result = any(AssignableDefinition def | def.getTarget() = v).getEnclosingCallable()
|
||||
}
|
||||
|
||||
class SourceVariable extends LocalScopeVariable {
|
||||
SourceVariable() { not getAnAssigningCallable(this) != getAnAssigningCallable(this) }
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the `i`th node of basic block `bb` is assignable definition `def`,
|
||||
* targeting local scope variable `v`.
|
||||
*/
|
||||
predicate definitionAt(AssignableDefinition def, BasicBlock bb, int i, SourceVariable v) {
|
||||
bb.getNode(i) = def.getAControlFlowNode() and
|
||||
v = def.getTarget() and
|
||||
// In cases like `(x, x) = (0, 1)`, we discard the first (dead) definition of `x`
|
||||
not exists(TupleAssignmentDefinition first, TupleAssignmentDefinition second | first = def |
|
||||
second.getAssignment() = first.getAssignment() and
|
||||
second.getEvaluationOrder() > first.getEvaluationOrder() and
|
||||
second.getTarget() = v
|
||||
)
|
||||
}
|
||||
|
||||
predicate variableWrite(BasicBlock bb, int i, SourceVariable v, boolean certain) {
|
||||
exists(AssignableDefinition def |
|
||||
definitionAt(def, bb, i, v) and
|
||||
if def.isCertain() then certain = true else certain = false
|
||||
)
|
||||
}
|
||||
|
||||
predicate variableRead(BasicBlock bb, int i, SourceVariable v, boolean certain) {
|
||||
exists(AssignableRead read |
|
||||
read.getAControlFlowNode() = bb.getNode(i) and
|
||||
read.getTarget() = v and
|
||||
certain = true
|
||||
)
|
||||
}
|
||||
@@ -312,8 +312,13 @@ private module Internal {
|
||||
1 < strictcount(this.getADynamicTarget().getUnboundDeclaration()) and
|
||||
c = this.getCall().getEnclosingCallable().getUnboundDeclaration() and
|
||||
(
|
||||
exists(AssignableDefinitions::ImplicitParameterDefinition pdef, Parameter p |
|
||||
this.getQualifier() = BaseSsa::getARead(pdef, p) and
|
||||
exists(
|
||||
BaseSsa::Definition def, AssignableDefinitions::ImplicitParameterDefinition pdef,
|
||||
Parameter p
|
||||
|
|
||||
pdef = def.getDefinition() and
|
||||
p = pdef.getTarget() and
|
||||
this.getQualifier() = def.getARead() and
|
||||
p.getPosition() = i and
|
||||
c.getAParameter() = p and
|
||||
not p.isParams()
|
||||
|
||||
@@ -1,9 +1,11 @@
|
||||
import csharp
|
||||
import semmle.code.csharp.dataflow.internal.BaseSSA
|
||||
|
||||
from AssignableRead ar, AssignableDefinition def, LocalScopeVariable v
|
||||
from AssignableRead ar, BaseSsa::Definition ssaDef, AssignableDefinition def, LocalScopeVariable v
|
||||
where
|
||||
ar = BaseSsa::getARead(def, v) and
|
||||
ar = ssaDef.getARead() and
|
||||
def = ssaDef.getDefinition() and
|
||||
v = def.getTarget() and
|
||||
not exists(Ssa::ExplicitDefinition edef |
|
||||
edef.getADefinition() = def and
|
||||
edef.getARead() = ar
|
||||
|
||||
Reference in New Issue
Block a user