mirror of
https://github.com/github/codeql.git
synced 2026-04-26 17:25:19 +02:00
Merge pull request #10203 from hvitved/ssa/param-module
SSA: Make shared library a parameterized module
This commit is contained in:
Tom Hvitved
@@ -462,9 +462,6 @@
|
||||
],
|
||||
"SSA C#": [
|
||||
"csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImplCommon.qll",
|
||||
"csharp/ql/lib/semmle/code/csharp/controlflow/internal/pressa/SsaImplCommon.qll",
|
||||
"csharp/ql/lib/semmle/code/csharp/dataflow/internal/basessa/SsaImplCommon.qll",
|
||||
"csharp/ql/lib/semmle/code/cil/internal/SsaImplCommon.qll",
|
||||
"ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImplCommon.qll",
|
||||
"cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaImplCommon.qll",
|
||||
"swift/ql/lib/codeql/swift/dataflow/internal/SsaImplCommon.qll"
|
||||
@@ -602,4 +599,4 @@
|
||||
"javascript/ql/lib/semmle/javascript/security/IncompleteMultiCharacterSanitizationQuery.qll",
|
||||
"ruby/ql/lib/codeql/ruby/security/IncompleteMultiCharacterSanitizationQuery.qll"
|
||||
]
|
||||
}
|
||||
}
|
||||
File diff suppressed because it is too large
Load Diff
@@ -1,18 +0,0 @@
|
||||
private import semmle.code.cpp.ir.IR
|
||||
private import SsaInternals as Ssa
|
||||
|
||||
class BasicBlock = IRBlock;
|
||||
|
||||
class SourceVariable = Ssa::SourceVariable;
|
||||
|
||||
BasicBlock getImmediateBasicBlockDominator(BasicBlock bb) { result.immediatelyDominates(bb) }
|
||||
|
||||
BasicBlock getABasicBlockSuccessor(BasicBlock bb) { result = bb.getASuccessor() }
|
||||
|
||||
class ExitBasicBlock extends IRBlock {
|
||||
ExitBasicBlock() { this.getLastInstruction() instanceof ExitFunctionInstruction }
|
||||
}
|
||||
|
||||
predicate variableWrite = Ssa::variableWrite/4;
|
||||
|
||||
predicate variableRead = Ssa::variableRead/4;
|
||||
@@ -1,10 +1,10 @@
|
||||
import SsaImplCommon
|
||||
private import cpp as Cpp
|
||||
private import semmle.code.cpp.ir.IR
|
||||
private import DataFlowUtil
|
||||
private import DataFlowImplCommon as DataFlowImplCommon
|
||||
private import semmle.code.cpp.models.interfaces.Allocation as Alloc
|
||||
private import semmle.code.cpp.models.interfaces.DataFlow as DataFlow
|
||||
private import SsaImplCommon as SsaImplCommon
|
||||
|
||||
private module SourceVariables {
|
||||
private newtype TSourceVariable =
|
||||
@@ -38,8 +38,6 @@ private module SourceVariables {
|
||||
}
|
||||
}
|
||||
|
||||
import SourceVariables
|
||||
|
||||
cached
|
||||
private newtype TDefOrUse =
|
||||
TExplicitDef(Instruction store) { explicitWrite(_, store, _) } or
|
||||
@@ -86,7 +84,7 @@ abstract class Def extends DefOrUse {
|
||||
Instruction getInstruction() { result = store }
|
||||
|
||||
/** Gets the variable that is defined by this definition. */
|
||||
abstract SourceVariable getSourceVariable();
|
||||
abstract SourceVariables::SourceVariable getSourceVariable();
|
||||
|
||||
/** Holds if this definition is guaranteed to happen. */
|
||||
abstract predicate isCertain();
|
||||
@@ -103,10 +101,10 @@ abstract class Def extends DefOrUse {
|
||||
private class ExplicitDef extends Def, TExplicitDef {
|
||||
ExplicitDef() { this = TExplicitDef(store) }
|
||||
|
||||
override SourceVariable getSourceVariable() {
|
||||
override SourceVariables::SourceVariable getSourceVariable() {
|
||||
exists(VariableInstruction var |
|
||||
explicitWrite(_, this.getInstruction(), var) and
|
||||
result.(SourceIRVariable).getIRVariable() = var.getIRVariable()
|
||||
result.(SourceVariables::SourceIRVariable).getIRVariable() = var.getIRVariable()
|
||||
)
|
||||
}
|
||||
|
||||
@@ -116,11 +114,11 @@ private class ExplicitDef extends Def, TExplicitDef {
|
||||
private class ParameterDef extends Def, TInitializeParam {
|
||||
ParameterDef() { this = TInitializeParam(store) }
|
||||
|
||||
override SourceVariable getSourceVariable() {
|
||||
result.(SourceIRVariable).getIRVariable() =
|
||||
override SourceVariables::SourceVariable getSourceVariable() {
|
||||
result.(SourceVariables::SourceIRVariable).getIRVariable() =
|
||||
store.(InitializeParameterInstruction).getIRVariable()
|
||||
or
|
||||
result.(SourceIRVariableIndirection).getUnderlyingIRVariable() =
|
||||
result.(SourceVariables::SourceIRVariableIndirection).getUnderlyingIRVariable() =
|
||||
store.(InitializeIndirectionInstruction).getIRVariable()
|
||||
}
|
||||
|
||||
@@ -138,7 +136,7 @@ abstract class Use extends DefOrUse {
|
||||
override string toString() { result = "Use" }
|
||||
|
||||
/** Gets the variable that is used by this use. */
|
||||
abstract SourceVariable getSourceVariable();
|
||||
abstract SourceVariables::SourceVariable getSourceVariable();
|
||||
|
||||
override IRBlock getBlock() { result = use.getUse().getBlock() }
|
||||
|
||||
@@ -148,12 +146,14 @@ abstract class Use extends DefOrUse {
|
||||
private class ExplicitUse extends Use, TExplicitUse {
|
||||
ExplicitUse() { this = TExplicitUse(use) }
|
||||
|
||||
override SourceVariable getSourceVariable() {
|
||||
override SourceVariables::SourceVariable getSourceVariable() {
|
||||
exists(VariableInstruction var |
|
||||
use.getDef() = var and
|
||||
if use.getUse() instanceof ReadSideEffectInstruction
|
||||
then result.(SourceIRVariableIndirection).getUnderlyingIRVariable() = var.getIRVariable()
|
||||
else result.(SourceIRVariable).getIRVariable() = var.getIRVariable()
|
||||
then
|
||||
result.(SourceVariables::SourceIRVariableIndirection).getUnderlyingIRVariable() =
|
||||
var.getIRVariable()
|
||||
else result.(SourceVariables::SourceIRVariable).getIRVariable() = var.getIRVariable()
|
||||
)
|
||||
}
|
||||
}
|
||||
@@ -161,10 +161,11 @@ private class ExplicitUse extends Use, TExplicitUse {
|
||||
private class ReturnParameterIndirection extends Use, TReturnParamIndirection {
|
||||
ReturnParameterIndirection() { this = TReturnParamIndirection(use) }
|
||||
|
||||
override SourceVariable getSourceVariable() {
|
||||
override SourceVariables::SourceVariable getSourceVariable() {
|
||||
exists(ReturnIndirectionInstruction ret |
|
||||
returnParameterIndirection(use, ret) and
|
||||
result.(SourceIRVariableIndirection).getUnderlyingIRVariable() = ret.getIRVariable()
|
||||
result.(SourceVariables::SourceIRVariableIndirection).getUnderlyingIRVariable() =
|
||||
ret.getIRVariable()
|
||||
)
|
||||
}
|
||||
}
|
||||
@@ -610,27 +611,45 @@ private module Cached {
|
||||
|
||||
import Cached
|
||||
|
||||
/**
|
||||
* Holds if the `i`'th write in block `bb` writes to the variable `v`.
|
||||
* `certain` is `true` if the write is guaranteed to overwrite the entire variable.
|
||||
*/
|
||||
predicate variableWrite(IRBlock bb, int i, SourceVariable v, boolean certain) {
|
||||
DataFlowImplCommon::forceCachingInSameStage() and
|
||||
exists(Def def |
|
||||
def.hasIndexInBlock(bb, i) and
|
||||
v = def.getSourceVariable() and
|
||||
(if def.isCertain() then certain = true else certain = false)
|
||||
)
|
||||
private module SsaInput implements SsaImplCommon::InputSig {
|
||||
private import semmle.code.cpp.ir.IR
|
||||
|
||||
class BasicBlock = IRBlock;
|
||||
|
||||
class SourceVariable = SourceVariables::SourceVariable;
|
||||
|
||||
BasicBlock getImmediateBasicBlockDominator(BasicBlock bb) { result.immediatelyDominates(bb) }
|
||||
|
||||
BasicBlock getABasicBlockSuccessor(BasicBlock bb) { result = bb.getASuccessor() }
|
||||
|
||||
class ExitBasicBlock extends IRBlock {
|
||||
ExitBasicBlock() { this.getLastInstruction() instanceof ExitFunctionInstruction }
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the `i`'th write in block `bb` writes to the variable `v`.
|
||||
* `certain` is `true` if the write is guaranteed to overwrite the entire variable.
|
||||
*/
|
||||
predicate variableWrite(BasicBlock bb, int i, SourceVariable v, boolean certain) {
|
||||
DataFlowImplCommon::forceCachingInSameStage() and
|
||||
exists(Def def |
|
||||
def.hasIndexInBlock(bb, i) and
|
||||
v = def.getSourceVariable() and
|
||||
(if def.isCertain() then certain = true else certain = false)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the `i`'th read in block `bb` reads to the variable `v`.
|
||||
* `certain` is `true` if the read is guaranteed. For C++, this is always the case.
|
||||
*/
|
||||
predicate variableRead(BasicBlock bb, int i, SourceVariable v, boolean certain) {
|
||||
exists(Use use |
|
||||
use.hasIndexInBlock(bb, i) and
|
||||
v = use.getSourceVariable() and
|
||||
certain = true
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the `i`'th read in block `bb` reads to the variable `v`.
|
||||
* `certain` is `true` if the read is guaranteed. For C++, this is always the case.
|
||||
*/
|
||||
predicate variableRead(IRBlock bb, int i, SourceVariable v, boolean certain) {
|
||||
exists(Use use |
|
||||
use.hasIndexInBlock(bb, i) and
|
||||
v = use.getSourceVariable() and
|
||||
certain = true
|
||||
)
|
||||
}
|
||||
import SsaImplCommon::Make<SsaInput>
|
||||
|
||||
@@ -1,8 +1,8 @@
|
||||
import csharp
|
||||
import semmle.code.csharp.dataflow.internal.SsaImplCommon::Consistency
|
||||
import semmle.code.csharp.dataflow.internal.SsaImpl::Consistency as Consistency
|
||||
import Ssa
|
||||
|
||||
class MyRelevantDefinition extends RelevantDefinition, Ssa::Definition {
|
||||
class MyRelevantDefinition extends Consistency::RelevantDefinition, Ssa::Definition {
|
||||
override predicate hasLocationInfo(
|
||||
string filepath, int startline, int startcolumn, int endline, int endcolumn
|
||||
) {
|
||||
@@ -10,6 +10,14 @@ class MyRelevantDefinition extends RelevantDefinition, Ssa::Definition {
|
||||
}
|
||||
}
|
||||
|
||||
query predicate nonUniqueDef = Consistency::nonUniqueDef/4;
|
||||
|
||||
query predicate readWithoutDef = Consistency::readWithoutDef/3;
|
||||
|
||||
query predicate deadDef = Consistency::deadDef/2;
|
||||
|
||||
query predicate notDominatedByDef = Consistency::notDominatedByDef/4;
|
||||
|
||||
query predicate localDeclWithSsaDef(LocalVariableDeclExpr d) {
|
||||
// Local variables in C# must be initialized before every use, so uninitialized
|
||||
// local variables should not have an SSA definition, as that would imply that
|
||||
|
||||
@@ -8,13 +8,12 @@ private import CIL
|
||||
* Provides classes for working with static single assignment (SSA) form.
|
||||
*/
|
||||
module Ssa {
|
||||
private import internal.SsaImplCommon as SsaImpl
|
||||
private import internal.SsaImpl
|
||||
private import internal.SsaImpl as SsaImpl
|
||||
|
||||
/** An SSA definition. */
|
||||
class Definition extends SsaImpl::Definition {
|
||||
/** Gets a read of this SSA definition. */
|
||||
final ReadAccess getARead() { result = getARead(this) }
|
||||
final ReadAccess getARead() { result = SsaImpl::getARead(this) }
|
||||
|
||||
/** Gets the underlying variable update, if any. */
|
||||
final VariableUpdate getVariableUpdate() {
|
||||
@@ -25,11 +24,11 @@ module Ssa {
|
||||
}
|
||||
|
||||
/** Gets a first read of this SSA definition. */
|
||||
final ReadAccess getAFirstRead() { result = getAFirstRead(this) }
|
||||
final ReadAccess getAFirstRead() { result = SsaImpl::getAFirstRead(this) }
|
||||
|
||||
/** Holds if `first` and `second` are adjacent reads of this SSA definition. */
|
||||
final predicate hasAdjacentReads(ReadAccess first, ReadAccess second) {
|
||||
hasAdjacentReads(this, first, second)
|
||||
SsaImpl::hasAdjacentReads(this, first, second)
|
||||
}
|
||||
|
||||
private Definition getAPhiInput() { result = this.(PhiNode).getAnInput() }
|
||||
@@ -52,7 +51,7 @@ module Ssa {
|
||||
final override Location getLocation() { result = this.getBasicBlock().getLocation() }
|
||||
|
||||
/** Gets an input to this phi node. */
|
||||
final Definition getAnInput() { result = getAPhiInput(this) }
|
||||
final Definition getAnInput() { result = SsaImpl::getAPhiInput(this) }
|
||||
|
||||
/**
|
||||
* Holds if if `def` is an input to this phi node, and a reference to `def` at
|
||||
@@ -60,7 +59,7 @@ module Ssa {
|
||||
* other references.
|
||||
*/
|
||||
final predicate hasLastInputRef(Definition def, BasicBlock bb, int i) {
|
||||
hasLastInputRef(this, def, bb, i)
|
||||
SsaImpl::hasLastInputRef(this, def, bb, i)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
@@ -1,8 +1,40 @@
|
||||
private import semmle.code.cil.CIL
|
||||
private import SsaImplCommon
|
||||
private import cil
|
||||
private import semmle.code.csharp.dataflow.internal.SsaImplCommon as SsaImplCommon
|
||||
|
||||
private module SsaInput implements SsaImplCommon::InputSig {
|
||||
class BasicBlock = CIL::BasicBlock;
|
||||
|
||||
BasicBlock getImmediateBasicBlockDominator(BasicBlock bb) { result = bb.getImmediateDominator() }
|
||||
|
||||
BasicBlock getABasicBlockSuccessor(BasicBlock bb) { result = bb.getASuccessor() }
|
||||
|
||||
class ExitBasicBlock = CIL::ExitBasicBlock;
|
||||
|
||||
class SourceVariable = CIL::StackVariable;
|
||||
|
||||
predicate variableWrite(BasicBlock bb, int i, SourceVariable v, boolean certain) {
|
||||
forceCachingInSameStage() and
|
||||
exists(CIL::VariableUpdate vu |
|
||||
vu.updatesAt(bb, i) and
|
||||
v = vu.getVariable() and
|
||||
certain = true
|
||||
)
|
||||
}
|
||||
|
||||
predicate variableRead(BasicBlock bb, int i, SourceVariable v, boolean certain) {
|
||||
exists(CIL::ReadAccess ra | bb.getNode(i) = ra |
|
||||
ra.getTarget() = v and
|
||||
certain = true
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
import SsaImplCommon::Make<SsaInput>
|
||||
|
||||
cached
|
||||
private module Cached {
|
||||
private import CIL
|
||||
|
||||
cached
|
||||
predicate forceCachingInSameStage() { any() }
|
||||
|
||||
|
||||
@@ -1,795 +0,0 @@
|
||||
/**
|
||||
* Provides a language-independent 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`.
|
||||
*/
|
||||
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, _)
|
||||
}
|
||||
|
||||
predicate lastRefIsRead(BasicBlock bb, SourceVariable v) {
|
||||
maxRefRank(bb, v) = refRank(bb, _, v, Read(_))
|
||||
}
|
||||
|
||||
/**
|
||||
* 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 `df` is in the dominance frontier of `bb`.
|
||||
*
|
||||
* This is equivalent to:
|
||||
*
|
||||
* ```ql
|
||||
* bb = getImmediateBasicBlockDominator*(getABasicBlockPredecessor(df)) and
|
||||
* not bb = getImmediateBasicBlockDominator+(df)
|
||||
* ```
|
||||
*/
|
||||
private predicate inDominanceFrontier(BasicBlock bb, BasicBlock df) {
|
||||
bb = getABasicBlockPredecessor(df) and not bb = getImmediateBasicBlockDominator(df)
|
||||
or
|
||||
exists(BasicBlock prev | inDominanceFrontier(prev, df) |
|
||||
bb = getImmediateBasicBlockDominator(prev) and
|
||||
not bb = getImmediateBasicBlockDominator(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 =
|
||||
SsaActualRead() or
|
||||
SsaPhiRead() or
|
||||
SsaDef()
|
||||
|
||||
class SsaRead = SsaActualRead or SsaPhiRead;
|
||||
|
||||
/**
|
||||
* A classification of SSA variable references into reads and definitions.
|
||||
*/
|
||||
class SsaRefKind extends TSsaRefKind {
|
||||
string toString() {
|
||||
this = SsaActualRead() and
|
||||
result = "SsaActualRead"
|
||||
or
|
||||
this = SsaPhiRead() and
|
||||
result = "SsaPhiRead"
|
||||
or
|
||||
this = SsaDef() and
|
||||
result = "SsaDef"
|
||||
}
|
||||
|
||||
int getOrder() {
|
||||
this instanceof SsaRead and
|
||||
result = 0
|
||||
or
|
||||
this = SsaDef() and
|
||||
result = 1
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `bb` is in the dominance frontier of a block containing a
|
||||
* read of `v`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate inReadDominanceFrontier(BasicBlock bb, SourceVariable v) {
|
||||
exists(BasicBlock readbb | inDominanceFrontier(readbb, bb) |
|
||||
lastRefIsRead(readbb, v)
|
||||
or
|
||||
phiRead(readbb, v)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if a phi-read node should be inserted for variable `v` at the beginning
|
||||
* of basic block `bb`.
|
||||
*
|
||||
* Phi-read nodes are like normal phi nodes, but they are inserted based on reads
|
||||
* instead of writes, and only if the dominance-frontier block does not already
|
||||
* contain a reference (read or write) to `v`. Unlike normal phi nodes, this is
|
||||
* an internal implementation detail that is not exposed.
|
||||
*
|
||||
* The motivation for adding phi-reads is to improve performance of the use-use
|
||||
* calculation in cases where there is a large number of reads that can reach the
|
||||
* same join-point, and from there reach a large number of basic blocks. Example:
|
||||
*
|
||||
* ```cs
|
||||
* if (a)
|
||||
* use(x);
|
||||
* else if (b)
|
||||
* use(x);
|
||||
* else if (c)
|
||||
* use(x);
|
||||
* else if (d)
|
||||
* use(x);
|
||||
* // many more ifs ...
|
||||
*
|
||||
* // phi-read for `x` inserted here
|
||||
*
|
||||
* // program not mentioning `x`, with large basic block graph
|
||||
*
|
||||
* use(x);
|
||||
* ```
|
||||
*
|
||||
* Without phi-reads, the analysis has to replicate reachability for each of
|
||||
* the guarded uses of `x`. However, with phi-reads, the analysis will limit
|
||||
* each conditional use of `x` to reach the basic block containing the phi-read
|
||||
* node for `x`, and only that basic block will have to compute reachability
|
||||
* through the remainder of the large program.
|
||||
*
|
||||
* Like normal reads, each phi-read node `phi-read` can be reached from exactly
|
||||
* one SSA definition (without passing through another definition): Assume, for
|
||||
* the sake of contradiction, that there are two reaching definitions `def1` and
|
||||
* `def2`. Now, if both `def1` and `def2` dominate `phi-read`, then the nearest
|
||||
* dominating definition will prevent the other from reaching `phi-read`. So, at
|
||||
* least one of `def1` and `def2` cannot dominate `phi-read`; assume it is `def1`.
|
||||
* Then `def1` must go through one of its dominance-frontier blocks in order to
|
||||
* reach `phi-read`. However, such a block will always start with a (normal) phi
|
||||
* node, which contradicts reachability.
|
||||
*
|
||||
* Also, like normal reads, the unique SSA definition `def` that reaches `phi-read`,
|
||||
* will dominate `phi-read`. Assuming it doesn't means that the path from `def`
|
||||
* to `phi-read` goes through a dominance-frontier block, and hence a phi node,
|
||||
* which contradicts reachability.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate phiRead(BasicBlock bb, SourceVariable v) {
|
||||
inReadDominanceFrontier(bb, v) and
|
||||
liveAtEntry(bb, v) and
|
||||
// only if there are no other references to `v` inside `bb`
|
||||
not ref(bb, _, v, _) and
|
||||
not exists(Definition def | def.definesAt(v, bb, _))
|
||||
}
|
||||
|
||||
/**
|
||||
* 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.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate ssaRef(BasicBlock bb, int i, SourceVariable v, SsaRefKind k) {
|
||||
variableRead(bb, i, v, _) and
|
||||
k = SsaActualRead()
|
||||
or
|
||||
phiRead(bb, v) and
|
||||
i = -1 and
|
||||
k = SsaPhiRead()
|
||||
or
|
||||
any(Definition 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, any(SsaRead k))
|
||||
}
|
||||
|
||||
/**
|
||||
* 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, any(SsaRead k))
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* 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)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the reference to `def` at index `i` in basic block `bb` is the
|
||||
* last reference to `v` inside `bb`.
|
||||
*/
|
||||
pragma[noinline]
|
||||
predicate lastSsaRef(Definition def, SourceVariable v, BasicBlock bb, int i) {
|
||||
ssaDefRank(def, v, bb, i, _) = maxSsaRefRank(bb, v)
|
||||
}
|
||||
|
||||
predicate defOccursInBlock(Definition def, BasicBlock bb, SourceVariable v, SsaRefKind k) {
|
||||
exists(ssaDefRank(def, v, bb, _, k))
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate ssaDefReachesThroughBlock(Definition def, BasicBlock bb) {
|
||||
ssaDefReachesEndOfBlock(bb, def, _) and
|
||||
not defOccursInBlock(_, bb, def.getSourceVariable(), _)
|
||||
}
|
||||
|
||||
/**
|
||||
* 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 _some_
|
||||
* predecessor of `bb2`, and the underlying variable for `def` is neither read
|
||||
* nor written in any block on the path between `bb1` and `bb2`.
|
||||
*
|
||||
* Phi reads are considered as normal reads for this predicate.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate varBlockReachesInclPhiRead(Definition def, BasicBlock bb1, BasicBlock bb2) {
|
||||
defOccursInBlock(def, bb1, _, _) and
|
||||
bb2 = getABasicBlockSuccessor(bb1)
|
||||
or
|
||||
exists(BasicBlock mid |
|
||||
varBlockReachesInclPhiRead(def, bb1, mid) and
|
||||
ssaDefReachesThroughBlock(def, mid) and
|
||||
bb2 = getABasicBlockSuccessor(mid)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate phiReadStep(Definition def, SourceVariable v, BasicBlock bb1, BasicBlock bb2) {
|
||||
varBlockReachesInclPhiRead(def, bb1, bb2) and
|
||||
defOccursInBlock(def, bb2, v, SsaPhiRead())
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate varBlockReachesExclPhiRead(Definition def, BasicBlock bb1, BasicBlock bb2) {
|
||||
varBlockReachesInclPhiRead(pragma[only_bind_into](def), bb1, pragma[only_bind_into](bb2)) and
|
||||
ssaRef(bb2, _, def.getSourceVariable(), [SsaActualRead().(TSsaRefKind), SsaDef()])
|
||||
or
|
||||
exists(BasicBlock mid |
|
||||
varBlockReachesExclPhiRead(def, mid, bb2) and
|
||||
phiReadStep(def, _, bb1, mid)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `def` is accessed in basic block `bb1` (either a read or a write),
|
||||
* the underlying variable `v` of `def` is accessed in basic block `bb2`
|
||||
* (either a read or a write), `bb2` is a transitive successor of `bb1`, and
|
||||
* `v` is neither read nor written in any block on the path between `bb1`
|
||||
* and `bb2`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate varBlockReaches(Definition def, BasicBlock bb1, BasicBlock bb2) {
|
||||
varBlockReachesExclPhiRead(def, bb1, bb2) and
|
||||
not defOccursInBlock(def, bb1, _, SsaPhiRead())
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
predicate defAdjacentRead(Definition def, BasicBlock bb1, BasicBlock bb2, int i2) {
|
||||
varBlockReaches(def, bb1, bb2) and
|
||||
ssaRefRank(bb2, i2, def.getSourceVariable(), SsaActualRead()) = 1
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `def` is accessed in basic block `bb` (either a read or a write),
|
||||
* `bb1` can reach a transitive successor `bb2` where `def` is no longer live,
|
||||
* and `v` is neither read nor written in any block on the path between `bb`
|
||||
* and `bb2`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate varBlockReachesExit(Definition def, BasicBlock bb) {
|
||||
exists(BasicBlock bb2 | varBlockReachesInclPhiRead(def, bb, bb2) |
|
||||
not defOccursInBlock(def, bb2, _, _) and
|
||||
not ssaDefReachesEndOfBlock(bb2, def, _)
|
||||
)
|
||||
or
|
||||
exists(BasicBlock mid |
|
||||
varBlockReachesExit(def, mid) and
|
||||
phiReadStep(def, _, bb, mid)
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
predicate phiReadExposedForTesting = phiRead/2;
|
||||
|
||||
private import SsaDefReaches
|
||||
|
||||
pragma[nomagic]
|
||||
predicate liveThrough(BasicBlock bb, SourceVariable v) {
|
||||
liveAtExit(bb, v) and
|
||||
not ssaRef(bb, _, v, SsaDef())
|
||||
}
|
||||
|
||||
/**
|
||||
* 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(pragma[only_bind_into](bb), pragma[only_bind_into](v)) and
|
||||
ssaDefReachesRank(bb, def, last, v) and
|
||||
liveAtExit(bb, v)
|
||||
)
|
||||
or
|
||||
// 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.
|
||||
ssaDefReachesEndOfBlock(getImmediateBasicBlockDominator(bb), def, pragma[only_bind_into](v)) and
|
||||
liveThrough(bb, pragma[only_bind_into](v))
|
||||
}
|
||||
|
||||
/**
|
||||
* 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
|
||||
ssaRef(bb, i, v, any(SsaRead k)) 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, SsaActualRead()) and
|
||||
variableRead(bb1, i2, _, _) and
|
||||
bb2 = bb1
|
||||
)
|
||||
or
|
||||
lastSsaRef(def, _, bb1, i1) and
|
||||
defAdjacentRead(def, bb1, bb2, i2)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate adjacentDefRead(
|
||||
Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2, SourceVariable v
|
||||
) {
|
||||
adjacentDefRead(def, bb1, i1, bb2, i2) and
|
||||
v = def.getSourceVariable()
|
||||
}
|
||||
|
||||
private predicate adjacentDefReachesRead(
|
||||
Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2
|
||||
) {
|
||||
exists(SourceVariable v | adjacentDefRead(def, bb1, i1, bb2, i2, v) |
|
||||
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(SourceVariable v |
|
||||
// Next reference to `v` inside `bb` is a write
|
||||
exists(int rnk, int j |
|
||||
rnk = ssaDefRank(def, v, bb, i, _) and
|
||||
next.definesAt(v, bb, j) and
|
||||
rnk + 1 = ssaRefRank(bb, j, v, SsaDef())
|
||||
)
|
||||
or
|
||||
// Can reach a write using one or more steps
|
||||
lastSsaRef(def, v, bb, i) and
|
||||
exists(BasicBlock bb2 |
|
||||
varBlockReaches(def, bb, bb2) and
|
||||
1 = ssaDefRank(next, v, bb2, _, 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) {
|
||||
// Can reach another definition
|
||||
lastRefRedef(def, bb, i, _)
|
||||
or
|
||||
exists(SourceVariable v | lastSsaRef(def, v, bb, i) |
|
||||
// Can reach exit directly
|
||||
bb instanceof ExitBasicBlock
|
||||
or
|
||||
// Can reach a block using one or more steps, where `def` is no longer live
|
||||
varBlockReachesExit(def, bb)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* 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)
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
/** Provides a set of consistency queries. */
|
||||
module Consistency {
|
||||
abstract class RelevantDefinition extends Definition {
|
||||
abstract predicate hasLocationInfo(
|
||||
string filepath, int startline, int startcolumn, int endline, int endcolumn
|
||||
);
|
||||
}
|
||||
|
||||
query predicate nonUniqueDef(RelevantDefinition def, SourceVariable v, BasicBlock bb, int i) {
|
||||
ssaDefReachesRead(v, def, bb, i) and
|
||||
not exists(unique(Definition def0 | ssaDefReachesRead(v, def0, bb, i)))
|
||||
}
|
||||
|
||||
query predicate readWithoutDef(SourceVariable v, BasicBlock bb, int i) {
|
||||
variableRead(bb, i, v, _) and
|
||||
not ssaDefReachesRead(v, _, bb, i)
|
||||
}
|
||||
|
||||
query predicate deadDef(RelevantDefinition def, SourceVariable v) {
|
||||
v = def.getSourceVariable() and
|
||||
not ssaDefReachesRead(_, def, _, _) and
|
||||
not phiHasInputFromBlock(_, def, _) and
|
||||
not uncertainWriteDefinitionInput(_, def)
|
||||
}
|
||||
|
||||
query predicate notDominatedByDef(RelevantDefinition def, SourceVariable v, BasicBlock bb, int i) {
|
||||
exists(BasicBlock bbDef, int iDef | def.definesAt(v, bbDef, iDef) |
|
||||
ssaDefReachesReadWithinBlock(v, def, bb, i) and
|
||||
(bb != bbDef or i < iDef)
|
||||
or
|
||||
ssaDefReachesRead(v, def, bb, i) and
|
||||
not ssaDefReachesReadWithinBlock(v, def, bb, i) and
|
||||
not def.definesAt(v, getImmediateBasicBlockDominator*(bb), _)
|
||||
)
|
||||
}
|
||||
}
|
||||
@@ -1,30 +0,0 @@
|
||||
/** Provides the CIL specific parameters for `SsaImplCommon.qll`. */
|
||||
|
||||
private import cil
|
||||
private import SsaImpl
|
||||
|
||||
class BasicBlock = CIL::BasicBlock;
|
||||
|
||||
BasicBlock getImmediateBasicBlockDominator(BasicBlock bb) { result = bb.getImmediateDominator() }
|
||||
|
||||
BasicBlock getABasicBlockSuccessor(BasicBlock bb) { result = bb.getASuccessor() }
|
||||
|
||||
class ExitBasicBlock = CIL::ExitBasicBlock;
|
||||
|
||||
class SourceVariable = CIL::StackVariable;
|
||||
|
||||
predicate variableWrite(BasicBlock bb, int i, SourceVariable v, boolean certain) {
|
||||
forceCachingInSameStage() and
|
||||
exists(CIL::VariableUpdate vu |
|
||||
vu.updatesAt(bb, i) and
|
||||
v = vu.getVariable() and
|
||||
certain = true
|
||||
)
|
||||
}
|
||||
|
||||
predicate variableRead(BasicBlock bb, int i, SourceVariable v, boolean certain) {
|
||||
exists(CIL::ReadAccess ra | bb.getNode(i) = ra |
|
||||
ra.getTarget() = v and
|
||||
certain = true
|
||||
)
|
||||
}
|
||||
@@ -192,8 +192,7 @@ class BasicBlock extends TBasicBlockStart {
|
||||
* Gets the basic block that immediately dominates this basic block, if any.
|
||||
*
|
||||
* That is, all paths reaching this basic block from some entry point
|
||||
* basic block must go through the result, which is an immediate basic block
|
||||
* predecessor of this basic block.
|
||||
* basic block must go through the result.
|
||||
*
|
||||
* Example:
|
||||
*
|
||||
@@ -207,8 +206,7 @@ class BasicBlock extends TBasicBlockStart {
|
||||
*
|
||||
* The basic block starting on line 2 is an immediate dominator of
|
||||
* the basic block online 4 (all paths from the entry point of `M`
|
||||
* to `return s.Length;` must go through the null check, and the null check
|
||||
* is an immediate predecessor of `return s.Length;`).
|
||||
* to `return s.Length;` must go through the null check.
|
||||
*/
|
||||
BasicBlock getImmediateDominator() { bbIDominates(result, this) }
|
||||
|
||||
|
||||
@@ -6,26 +6,158 @@ import csharp
|
||||
* scope variables.
|
||||
*/
|
||||
module PreSsa {
|
||||
import pressa.SsaImplSpecific
|
||||
private import pressa.SsaImplCommon as SsaImpl
|
||||
private import AssignableDefinitions
|
||||
private import semmle.code.csharp.controlflow.internal.ControlFlowGraphImpl
|
||||
private import semmle.code.csharp.controlflow.internal.PreBasicBlocks as PreBasicBlocks
|
||||
private import semmle.code.csharp.dataflow.internal.SsaImplCommon as SsaImplCommon
|
||||
|
||||
private predicate definitionAt(
|
||||
AssignableDefinition def, SsaInput::BasicBlock bb, int i, SsaInput::SourceVariable v
|
||||
) {
|
||||
bb.getElement(i) = def.getExpr() 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
|
||||
)
|
||||
or
|
||||
def.(ImplicitParameterDefinition).getParameter() = v and
|
||||
exists(Callable c | v = c.getAParameter() |
|
||||
scopeFirst(c, bb) and
|
||||
i = -1
|
||||
)
|
||||
}
|
||||
|
||||
predicate implicitEntryDef(Callable c, SsaInput::BasicBlock bb, SsaInput::SourceVariable v) {
|
||||
not v instanceof LocalScopeVariable and
|
||||
c = v.getACallable() and
|
||||
scopeFirst(c, bb)
|
||||
}
|
||||
|
||||
module SsaInput implements SsaImplCommon::InputSig {
|
||||
class BasicBlock = PreBasicBlocks::PreBasicBlock;
|
||||
|
||||
BasicBlock getImmediateBasicBlockDominator(BasicBlock bb) { result.immediatelyDominates(bb) }
|
||||
|
||||
BasicBlock getABasicBlockSuccessor(BasicBlock bb) { result = bb.getASuccessor() }
|
||||
|
||||
class ExitBasicBlock extends BasicBlock {
|
||||
ExitBasicBlock() { scopeLast(_, this.getLastElement(), _) }
|
||||
}
|
||||
|
||||
/** Holds if `a` is assigned in non-constructor callable `c`. */
|
||||
pragma[nomagic]
|
||||
private predicate assignableDefinition(Assignable a, Callable c) {
|
||||
exists(AssignableDefinition def | def.getTarget() = a |
|
||||
c = def.getEnclosingCallable() and
|
||||
not c instanceof Constructor
|
||||
)
|
||||
}
|
||||
|
||||
/** Holds if `a` is accessed in callable `c`. */
|
||||
pragma[nomagic]
|
||||
private predicate assignableAccess(Assignable a, Callable c) {
|
||||
exists(AssignableAccess aa | aa.getTarget() = a | c = aa.getEnclosingCallable())
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate assignableNoCapturing(Assignable a, Callable c) {
|
||||
assignableAccess(a, c) and
|
||||
/*
|
||||
* The code below is equivalent to
|
||||
* ```ql
|
||||
* not exists(Callable other | assignableDefinition(a, other) | other != c)
|
||||
* ```
|
||||
* but it avoids a Cartesian product in the compiler generated antijoin
|
||||
* predicate.
|
||||
*/
|
||||
|
||||
(
|
||||
not assignableDefinition(a, _)
|
||||
or
|
||||
c = unique(Callable c0 | assignableDefinition(a, c0) | c0)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate assignableNoComplexQualifiers(Assignable a) {
|
||||
forall(QualifiableExpr qe | qe.(AssignableAccess).getTarget() = a | qe.targetIsThisInstance())
|
||||
}
|
||||
|
||||
/**
|
||||
* A simple assignable. Either a local scope variable or a field/property
|
||||
* that behaves like a local scope variable.
|
||||
*/
|
||||
class SourceVariable extends Assignable {
|
||||
private Callable c;
|
||||
|
||||
SourceVariable() {
|
||||
(
|
||||
this instanceof LocalScopeVariable
|
||||
or
|
||||
this = any(Field f | not f.isVolatile())
|
||||
or
|
||||
this = any(TrivialProperty tp | not tp.isOverridableOrImplementable())
|
||||
) and
|
||||
assignableNoCapturing(this, c) and
|
||||
assignableNoComplexQualifiers(this)
|
||||
}
|
||||
|
||||
/** Gets a callable in which this simple assignable can be analyzed. */
|
||||
Callable getACallable() { result = c }
|
||||
}
|
||||
|
||||
predicate variableWrite(BasicBlock bb, int i, SourceVariable v, boolean certain) {
|
||||
exists(AssignableDefinition def |
|
||||
definitionAt(def, bb, i, v) and
|
||||
if def.getTargetAccess().isRefArgument() then certain = false else certain = true
|
||||
)
|
||||
or
|
||||
exists(Callable c |
|
||||
implicitEntryDef(c, bb, v) and
|
||||
i = -1 and
|
||||
certain = true
|
||||
)
|
||||
}
|
||||
|
||||
predicate variableRead(BasicBlock bb, int i, SourceVariable v, boolean certain) {
|
||||
exists(AssignableRead read |
|
||||
read = bb.getElement(i) and
|
||||
read.getTarget() = v and
|
||||
certain = true
|
||||
)
|
||||
or
|
||||
v =
|
||||
any(LocalScopeVariable lsv |
|
||||
lsv.getCallable() = bb.(ExitBasicBlock).getEnclosingCallable() and
|
||||
i = bb.length() and
|
||||
(lsv.isRef() or v.(Parameter).isOut()) and
|
||||
certain = false
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
private module SsaImpl = SsaImplCommon::Make<SsaInput>;
|
||||
|
||||
class Definition extends SsaImpl::Definition {
|
||||
final AssignableRead getARead() {
|
||||
exists(BasicBlock bb, int i |
|
||||
exists(SsaInput::BasicBlock bb, int i |
|
||||
SsaImpl::ssaDefReachesRead(_, this, bb, i) and
|
||||
result = bb.getElement(i)
|
||||
)
|
||||
}
|
||||
|
||||
final AssignableDefinition getDefinition() {
|
||||
exists(BasicBlock bb, int i, SourceVariable v |
|
||||
exists(SsaInput::BasicBlock bb, int i, SsaInput::SourceVariable v |
|
||||
this.definesAt(v, bb, i) and
|
||||
definitionAt(result, bb, i, v)
|
||||
)
|
||||
}
|
||||
|
||||
final AssignableRead getAFirstRead() {
|
||||
exists(BasicBlock bb1, int i1, BasicBlock bb2, int i2 |
|
||||
exists(SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2 |
|
||||
this.definesAt(_, bb1, i1) and
|
||||
SsaImpl::adjacentDefRead(this, bb1, i1, bb2, i2) and
|
||||
result = bb2.getElement(i2)
|
||||
@@ -42,14 +174,14 @@ module PreSsa {
|
||||
not result instanceof PhiNode
|
||||
}
|
||||
|
||||
final predicate isLiveAtEndOfBlock(BasicBlock bb) {
|
||||
final predicate isLiveAtEndOfBlock(SsaInput::BasicBlock bb) {
|
||||
SsaImpl::ssaDefReachesEndOfBlock(bb, this, _)
|
||||
}
|
||||
|
||||
Location getLocation() {
|
||||
result = this.getDefinition().getLocation()
|
||||
or
|
||||
exists(Callable c, BasicBlock bb, SourceVariable v |
|
||||
exists(Callable c, SsaInput::BasicBlock bb, SsaInput::SourceVariable v |
|
||||
this.definesAt(v, bb, -1) and
|
||||
implicitEntryDef(c, bb, v) and
|
||||
result = c.getLocation()
|
||||
@@ -64,9 +196,9 @@ module PreSsa {
|
||||
}
|
||||
|
||||
predicate adjacentReadPairSameVar(AssignableRead read1, AssignableRead read2) {
|
||||
exists(BasicBlock bb1, int i1, BasicBlock bb2, int i2 |
|
||||
exists(SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2 |
|
||||
read1 = bb1.getElement(i1) and
|
||||
variableRead(bb1, i1, _, true) and
|
||||
SsaInput::variableRead(bb1, i1, _, true) and
|
||||
SsaImpl::adjacentDefRead(_, bb1, i1, bb2, i2) and
|
||||
read2 = bb2.getElement(i2)
|
||||
)
|
||||
|
||||
@@ -1,795 +0,0 @@
|
||||
/**
|
||||
* Provides a language-independent 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`.
|
||||
*/
|
||||
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, _)
|
||||
}
|
||||
|
||||
predicate lastRefIsRead(BasicBlock bb, SourceVariable v) {
|
||||
maxRefRank(bb, v) = refRank(bb, _, v, Read(_))
|
||||
}
|
||||
|
||||
/**
|
||||
* 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 `df` is in the dominance frontier of `bb`.
|
||||
*
|
||||
* This is equivalent to:
|
||||
*
|
||||
* ```ql
|
||||
* bb = getImmediateBasicBlockDominator*(getABasicBlockPredecessor(df)) and
|
||||
* not bb = getImmediateBasicBlockDominator+(df)
|
||||
* ```
|
||||
*/
|
||||
private predicate inDominanceFrontier(BasicBlock bb, BasicBlock df) {
|
||||
bb = getABasicBlockPredecessor(df) and not bb = getImmediateBasicBlockDominator(df)
|
||||
or
|
||||
exists(BasicBlock prev | inDominanceFrontier(prev, df) |
|
||||
bb = getImmediateBasicBlockDominator(prev) and
|
||||
not bb = getImmediateBasicBlockDominator(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 =
|
||||
SsaActualRead() or
|
||||
SsaPhiRead() or
|
||||
SsaDef()
|
||||
|
||||
class SsaRead = SsaActualRead or SsaPhiRead;
|
||||
|
||||
/**
|
||||
* A classification of SSA variable references into reads and definitions.
|
||||
*/
|
||||
class SsaRefKind extends TSsaRefKind {
|
||||
string toString() {
|
||||
this = SsaActualRead() and
|
||||
result = "SsaActualRead"
|
||||
or
|
||||
this = SsaPhiRead() and
|
||||
result = "SsaPhiRead"
|
||||
or
|
||||
this = SsaDef() and
|
||||
result = "SsaDef"
|
||||
}
|
||||
|
||||
int getOrder() {
|
||||
this instanceof SsaRead and
|
||||
result = 0
|
||||
or
|
||||
this = SsaDef() and
|
||||
result = 1
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `bb` is in the dominance frontier of a block containing a
|
||||
* read of `v`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate inReadDominanceFrontier(BasicBlock bb, SourceVariable v) {
|
||||
exists(BasicBlock readbb | inDominanceFrontier(readbb, bb) |
|
||||
lastRefIsRead(readbb, v)
|
||||
or
|
||||
phiRead(readbb, v)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if a phi-read node should be inserted for variable `v` at the beginning
|
||||
* of basic block `bb`.
|
||||
*
|
||||
* Phi-read nodes are like normal phi nodes, but they are inserted based on reads
|
||||
* instead of writes, and only if the dominance-frontier block does not already
|
||||
* contain a reference (read or write) to `v`. Unlike normal phi nodes, this is
|
||||
* an internal implementation detail that is not exposed.
|
||||
*
|
||||
* The motivation for adding phi-reads is to improve performance of the use-use
|
||||
* calculation in cases where there is a large number of reads that can reach the
|
||||
* same join-point, and from there reach a large number of basic blocks. Example:
|
||||
*
|
||||
* ```cs
|
||||
* if (a)
|
||||
* use(x);
|
||||
* else if (b)
|
||||
* use(x);
|
||||
* else if (c)
|
||||
* use(x);
|
||||
* else if (d)
|
||||
* use(x);
|
||||
* // many more ifs ...
|
||||
*
|
||||
* // phi-read for `x` inserted here
|
||||
*
|
||||
* // program not mentioning `x`, with large basic block graph
|
||||
*
|
||||
* use(x);
|
||||
* ```
|
||||
*
|
||||
* Without phi-reads, the analysis has to replicate reachability for each of
|
||||
* the guarded uses of `x`. However, with phi-reads, the analysis will limit
|
||||
* each conditional use of `x` to reach the basic block containing the phi-read
|
||||
* node for `x`, and only that basic block will have to compute reachability
|
||||
* through the remainder of the large program.
|
||||
*
|
||||
* Like normal reads, each phi-read node `phi-read` can be reached from exactly
|
||||
* one SSA definition (without passing through another definition): Assume, for
|
||||
* the sake of contradiction, that there are two reaching definitions `def1` and
|
||||
* `def2`. Now, if both `def1` and `def2` dominate `phi-read`, then the nearest
|
||||
* dominating definition will prevent the other from reaching `phi-read`. So, at
|
||||
* least one of `def1` and `def2` cannot dominate `phi-read`; assume it is `def1`.
|
||||
* Then `def1` must go through one of its dominance-frontier blocks in order to
|
||||
* reach `phi-read`. However, such a block will always start with a (normal) phi
|
||||
* node, which contradicts reachability.
|
||||
*
|
||||
* Also, like normal reads, the unique SSA definition `def` that reaches `phi-read`,
|
||||
* will dominate `phi-read`. Assuming it doesn't means that the path from `def`
|
||||
* to `phi-read` goes through a dominance-frontier block, and hence a phi node,
|
||||
* which contradicts reachability.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate phiRead(BasicBlock bb, SourceVariable v) {
|
||||
inReadDominanceFrontier(bb, v) and
|
||||
liveAtEntry(bb, v) and
|
||||
// only if there are no other references to `v` inside `bb`
|
||||
not ref(bb, _, v, _) and
|
||||
not exists(Definition def | def.definesAt(v, bb, _))
|
||||
}
|
||||
|
||||
/**
|
||||
* 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.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate ssaRef(BasicBlock bb, int i, SourceVariable v, SsaRefKind k) {
|
||||
variableRead(bb, i, v, _) and
|
||||
k = SsaActualRead()
|
||||
or
|
||||
phiRead(bb, v) and
|
||||
i = -1 and
|
||||
k = SsaPhiRead()
|
||||
or
|
||||
any(Definition 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, any(SsaRead k))
|
||||
}
|
||||
|
||||
/**
|
||||
* 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, any(SsaRead k))
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* 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)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the reference to `def` at index `i` in basic block `bb` is the
|
||||
* last reference to `v` inside `bb`.
|
||||
*/
|
||||
pragma[noinline]
|
||||
predicate lastSsaRef(Definition def, SourceVariable v, BasicBlock bb, int i) {
|
||||
ssaDefRank(def, v, bb, i, _) = maxSsaRefRank(bb, v)
|
||||
}
|
||||
|
||||
predicate defOccursInBlock(Definition def, BasicBlock bb, SourceVariable v, SsaRefKind k) {
|
||||
exists(ssaDefRank(def, v, bb, _, k))
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate ssaDefReachesThroughBlock(Definition def, BasicBlock bb) {
|
||||
ssaDefReachesEndOfBlock(bb, def, _) and
|
||||
not defOccursInBlock(_, bb, def.getSourceVariable(), _)
|
||||
}
|
||||
|
||||
/**
|
||||
* 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 _some_
|
||||
* predecessor of `bb2`, and the underlying variable for `def` is neither read
|
||||
* nor written in any block on the path between `bb1` and `bb2`.
|
||||
*
|
||||
* Phi reads are considered as normal reads for this predicate.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate varBlockReachesInclPhiRead(Definition def, BasicBlock bb1, BasicBlock bb2) {
|
||||
defOccursInBlock(def, bb1, _, _) and
|
||||
bb2 = getABasicBlockSuccessor(bb1)
|
||||
or
|
||||
exists(BasicBlock mid |
|
||||
varBlockReachesInclPhiRead(def, bb1, mid) and
|
||||
ssaDefReachesThroughBlock(def, mid) and
|
||||
bb2 = getABasicBlockSuccessor(mid)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate phiReadStep(Definition def, SourceVariable v, BasicBlock bb1, BasicBlock bb2) {
|
||||
varBlockReachesInclPhiRead(def, bb1, bb2) and
|
||||
defOccursInBlock(def, bb2, v, SsaPhiRead())
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate varBlockReachesExclPhiRead(Definition def, BasicBlock bb1, BasicBlock bb2) {
|
||||
varBlockReachesInclPhiRead(pragma[only_bind_into](def), bb1, pragma[only_bind_into](bb2)) and
|
||||
ssaRef(bb2, _, def.getSourceVariable(), [SsaActualRead().(TSsaRefKind), SsaDef()])
|
||||
or
|
||||
exists(BasicBlock mid |
|
||||
varBlockReachesExclPhiRead(def, mid, bb2) and
|
||||
phiReadStep(def, _, bb1, mid)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `def` is accessed in basic block `bb1` (either a read or a write),
|
||||
* the underlying variable `v` of `def` is accessed in basic block `bb2`
|
||||
* (either a read or a write), `bb2` is a transitive successor of `bb1`, and
|
||||
* `v` is neither read nor written in any block on the path between `bb1`
|
||||
* and `bb2`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate varBlockReaches(Definition def, BasicBlock bb1, BasicBlock bb2) {
|
||||
varBlockReachesExclPhiRead(def, bb1, bb2) and
|
||||
not defOccursInBlock(def, bb1, _, SsaPhiRead())
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
predicate defAdjacentRead(Definition def, BasicBlock bb1, BasicBlock bb2, int i2) {
|
||||
varBlockReaches(def, bb1, bb2) and
|
||||
ssaRefRank(bb2, i2, def.getSourceVariable(), SsaActualRead()) = 1
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `def` is accessed in basic block `bb` (either a read or a write),
|
||||
* `bb1` can reach a transitive successor `bb2` where `def` is no longer live,
|
||||
* and `v` is neither read nor written in any block on the path between `bb`
|
||||
* and `bb2`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate varBlockReachesExit(Definition def, BasicBlock bb) {
|
||||
exists(BasicBlock bb2 | varBlockReachesInclPhiRead(def, bb, bb2) |
|
||||
not defOccursInBlock(def, bb2, _, _) and
|
||||
not ssaDefReachesEndOfBlock(bb2, def, _)
|
||||
)
|
||||
or
|
||||
exists(BasicBlock mid |
|
||||
varBlockReachesExit(def, mid) and
|
||||
phiReadStep(def, _, bb, mid)
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
predicate phiReadExposedForTesting = phiRead/2;
|
||||
|
||||
private import SsaDefReaches
|
||||
|
||||
pragma[nomagic]
|
||||
predicate liveThrough(BasicBlock bb, SourceVariable v) {
|
||||
liveAtExit(bb, v) and
|
||||
not ssaRef(bb, _, v, SsaDef())
|
||||
}
|
||||
|
||||
/**
|
||||
* 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(pragma[only_bind_into](bb), pragma[only_bind_into](v)) and
|
||||
ssaDefReachesRank(bb, def, last, v) and
|
||||
liveAtExit(bb, v)
|
||||
)
|
||||
or
|
||||
// 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.
|
||||
ssaDefReachesEndOfBlock(getImmediateBasicBlockDominator(bb), def, pragma[only_bind_into](v)) and
|
||||
liveThrough(bb, pragma[only_bind_into](v))
|
||||
}
|
||||
|
||||
/**
|
||||
* 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
|
||||
ssaRef(bb, i, v, any(SsaRead k)) 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, SsaActualRead()) and
|
||||
variableRead(bb1, i2, _, _) and
|
||||
bb2 = bb1
|
||||
)
|
||||
or
|
||||
lastSsaRef(def, _, bb1, i1) and
|
||||
defAdjacentRead(def, bb1, bb2, i2)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate adjacentDefRead(
|
||||
Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2, SourceVariable v
|
||||
) {
|
||||
adjacentDefRead(def, bb1, i1, bb2, i2) and
|
||||
v = def.getSourceVariable()
|
||||
}
|
||||
|
||||
private predicate adjacentDefReachesRead(
|
||||
Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2
|
||||
) {
|
||||
exists(SourceVariable v | adjacentDefRead(def, bb1, i1, bb2, i2, v) |
|
||||
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(SourceVariable v |
|
||||
// Next reference to `v` inside `bb` is a write
|
||||
exists(int rnk, int j |
|
||||
rnk = ssaDefRank(def, v, bb, i, _) and
|
||||
next.definesAt(v, bb, j) and
|
||||
rnk + 1 = ssaRefRank(bb, j, v, SsaDef())
|
||||
)
|
||||
or
|
||||
// Can reach a write using one or more steps
|
||||
lastSsaRef(def, v, bb, i) and
|
||||
exists(BasicBlock bb2 |
|
||||
varBlockReaches(def, bb, bb2) and
|
||||
1 = ssaDefRank(next, v, bb2, _, 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) {
|
||||
// Can reach another definition
|
||||
lastRefRedef(def, bb, i, _)
|
||||
or
|
||||
exists(SourceVariable v | lastSsaRef(def, v, bb, i) |
|
||||
// Can reach exit directly
|
||||
bb instanceof ExitBasicBlock
|
||||
or
|
||||
// Can reach a block using one or more steps, where `def` is no longer live
|
||||
varBlockReachesExit(def, bb)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* 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)
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
/** Provides a set of consistency queries. */
|
||||
module Consistency {
|
||||
abstract class RelevantDefinition extends Definition {
|
||||
abstract predicate hasLocationInfo(
|
||||
string filepath, int startline, int startcolumn, int endline, int endcolumn
|
||||
);
|
||||
}
|
||||
|
||||
query predicate nonUniqueDef(RelevantDefinition def, SourceVariable v, BasicBlock bb, int i) {
|
||||
ssaDefReachesRead(v, def, bb, i) and
|
||||
not exists(unique(Definition def0 | ssaDefReachesRead(v, def0, bb, i)))
|
||||
}
|
||||
|
||||
query predicate readWithoutDef(SourceVariable v, BasicBlock bb, int i) {
|
||||
variableRead(bb, i, v, _) and
|
||||
not ssaDefReachesRead(v, _, bb, i)
|
||||
}
|
||||
|
||||
query predicate deadDef(RelevantDefinition def, SourceVariable v) {
|
||||
v = def.getSourceVariable() and
|
||||
not ssaDefReachesRead(_, def, _, _) and
|
||||
not phiHasInputFromBlock(_, def, _) and
|
||||
not uncertainWriteDefinitionInput(_, def)
|
||||
}
|
||||
|
||||
query predicate notDominatedByDef(RelevantDefinition def, SourceVariable v, BasicBlock bb, int i) {
|
||||
exists(BasicBlock bbDef, int iDef | def.definesAt(v, bbDef, iDef) |
|
||||
ssaDefReachesReadWithinBlock(v, def, bb, i) and
|
||||
(bb != bbDef or i < iDef)
|
||||
or
|
||||
ssaDefReachesRead(v, def, bb, i) and
|
||||
not ssaDefReachesReadWithinBlock(v, def, bb, i) and
|
||||
not def.definesAt(v, getImmediateBasicBlockDominator*(bb), _)
|
||||
)
|
||||
}
|
||||
}
|
||||
@@ -1,130 +0,0 @@
|
||||
/** Provides the C# specific parameters for `SsaImplCommon.qll`. */
|
||||
|
||||
private import csharp
|
||||
private import AssignableDefinitions
|
||||
private import semmle.code.csharp.controlflow.internal.PreBasicBlocks as PreBasicBlocks
|
||||
private import semmle.code.csharp.controlflow.internal.ControlFlowGraphImpl
|
||||
|
||||
class BasicBlock = PreBasicBlocks::PreBasicBlock;
|
||||
|
||||
BasicBlock getImmediateBasicBlockDominator(BasicBlock bb) { result.immediatelyDominates(bb) }
|
||||
|
||||
BasicBlock getABasicBlockSuccessor(BasicBlock bb) { result = bb.getASuccessor() }
|
||||
|
||||
class ExitBasicBlock extends BasicBlock {
|
||||
ExitBasicBlock() { scopeLast(_, this.getLastElement(), _) }
|
||||
}
|
||||
|
||||
/** Holds if `a` is assigned in non-constructor callable `c`. */
|
||||
pragma[nomagic]
|
||||
private predicate assignableDefinition(Assignable a, Callable c) {
|
||||
exists(AssignableDefinition def | def.getTarget() = a |
|
||||
c = def.getEnclosingCallable() and
|
||||
not c instanceof Constructor
|
||||
)
|
||||
}
|
||||
|
||||
/** Holds if `a` is accessed in callable `c`. */
|
||||
pragma[nomagic]
|
||||
private predicate assignableAccess(Assignable a, Callable c) {
|
||||
exists(AssignableAccess aa | aa.getTarget() = a | c = aa.getEnclosingCallable())
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate assignableNoCapturing(Assignable a, Callable c) {
|
||||
assignableAccess(a, c) and
|
||||
/*
|
||||
* The code below is equivalent to
|
||||
* ```ql
|
||||
* not exists(Callable other | assignableDefinition(a, other) | other != c)
|
||||
* ```
|
||||
* but it avoids a Cartesian product in the compiler generated antijoin
|
||||
* predicate.
|
||||
*/
|
||||
|
||||
(
|
||||
not assignableDefinition(a, _)
|
||||
or
|
||||
c = unique(Callable c0 | assignableDefinition(a, c0) | c0)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate assignableNoComplexQualifiers(Assignable a) {
|
||||
forall(QualifiableExpr qe | qe.(AssignableAccess).getTarget() = a | qe.targetIsThisInstance())
|
||||
}
|
||||
|
||||
/**
|
||||
* A simple assignable. Either a local scope variable or a field/property
|
||||
* that behaves like a local scope variable.
|
||||
*/
|
||||
class SourceVariable extends Assignable {
|
||||
private Callable c;
|
||||
|
||||
SourceVariable() {
|
||||
(
|
||||
this instanceof LocalScopeVariable
|
||||
or
|
||||
this = any(Field f | not f.isVolatile())
|
||||
or
|
||||
this = any(TrivialProperty tp | not tp.isOverridableOrImplementable())
|
||||
) and
|
||||
assignableNoCapturing(this, c) and
|
||||
assignableNoComplexQualifiers(this)
|
||||
}
|
||||
|
||||
/** Gets a callable in which this simple assignable can be analyzed. */
|
||||
Callable getACallable() { result = c }
|
||||
}
|
||||
|
||||
predicate definitionAt(AssignableDefinition def, BasicBlock bb, int i, SourceVariable v) {
|
||||
bb.getElement(i) = def.getExpr() 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
|
||||
)
|
||||
or
|
||||
def.(ImplicitParameterDefinition).getParameter() = v and
|
||||
exists(Callable c | v = c.getAParameter() |
|
||||
scopeFirst(c, bb) and
|
||||
i = -1
|
||||
)
|
||||
}
|
||||
|
||||
predicate implicitEntryDef(Callable c, BasicBlock bb, SourceVariable v) {
|
||||
not v instanceof LocalScopeVariable and
|
||||
c = v.getACallable() and
|
||||
scopeFirst(c, bb)
|
||||
}
|
||||
|
||||
predicate variableWrite(BasicBlock bb, int i, SourceVariable v, boolean certain) {
|
||||
exists(AssignableDefinition def |
|
||||
definitionAt(def, bb, i, v) and
|
||||
if def.getTargetAccess().isRefArgument() then certain = false else certain = true
|
||||
)
|
||||
or
|
||||
exists(Callable c |
|
||||
implicitEntryDef(c, bb, v) and
|
||||
i = -1 and
|
||||
certain = true
|
||||
)
|
||||
}
|
||||
|
||||
predicate variableRead(BasicBlock bb, int i, SourceVariable v, boolean certain) {
|
||||
exists(AssignableRead read |
|
||||
read = bb.getElement(i) and
|
||||
read.getTarget() = v and
|
||||
certain = true
|
||||
)
|
||||
or
|
||||
v =
|
||||
any(LocalScopeVariable lsv |
|
||||
lsv.getCallable() = bb.(ExitBasicBlock).getEnclosingCallable() and
|
||||
i = bb.length() and
|
||||
(lsv.isRef() or v.(Parameter).isOut()) and
|
||||
certain = false
|
||||
)
|
||||
}
|
||||
@@ -4,19 +4,74 @@ import csharp
|
||||
* Provides a simple SSA implementation for local scope variables.
|
||||
*/
|
||||
module BaseSsa {
|
||||
import basessa.SsaImplSpecific
|
||||
private import basessa.SsaImplCommon as SsaImpl
|
||||
private import AssignableDefinitions
|
||||
private import semmle.code.csharp.dataflow.internal.SsaImplCommon as SsaImplCommon
|
||||
|
||||
/**
|
||||
* Holds if the `i`th node of basic block `bb` is assignable definition `def`,
|
||||
* targeting local scope variable `v`.
|
||||
*/
|
||||
private predicate definitionAt(
|
||||
AssignableDefinition def, ControlFlow::BasicBlock bb, int i, SsaInput::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
|
||||
)
|
||||
}
|
||||
|
||||
private module SsaInput implements SsaImplCommon::InputSig {
|
||||
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) }
|
||||
}
|
||||
|
||||
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
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
private module SsaImpl = SsaImplCommon::Make<SsaInput>;
|
||||
|
||||
class Definition extends SsaImpl::Definition {
|
||||
final AssignableRead getARead() {
|
||||
exists(BasicBlock bb, int i |
|
||||
exists(ControlFlow::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 |
|
||||
exists(ControlFlow::BasicBlock bb, int i, SsaInput::SourceVariable v |
|
||||
this.definesAt(v, bb, i) and
|
||||
definitionAt(result, bb, i, v)
|
||||
)
|
||||
|
||||
@@ -3,7 +3,53 @@
|
||||
*/
|
||||
|
||||
import csharp
|
||||
import SsaImplCommon
|
||||
private import SsaImplCommon as SsaImplCommon
|
||||
private import AssignableDefinitions
|
||||
|
||||
private module SsaInput implements SsaImplCommon::InputSig {
|
||||
class BasicBlock = ControlFlow::BasicBlock;
|
||||
|
||||
BasicBlock getImmediateBasicBlockDominator(BasicBlock bb) { result = bb.getImmediateDominator() }
|
||||
|
||||
BasicBlock getABasicBlockSuccessor(BasicBlock bb) { result = bb.getASuccessor() }
|
||||
|
||||
class ExitBasicBlock = ControlFlow::BasicBlocks::ExitBlock;
|
||||
|
||||
class SourceVariable = Ssa::SourceVariable;
|
||||
|
||||
/**
|
||||
* Holds if the `i`th node of basic block `bb` is a (potential) write to source
|
||||
* variable `v`. The Boolean `certain` indicates whether the write is certain.
|
||||
*
|
||||
* This includes implicit writes via calls.
|
||||
*/
|
||||
predicate variableWrite(ControlFlow::BasicBlock bb, int i, Ssa::SourceVariable v, boolean certain) {
|
||||
variableWriteDirect(bb, i, v, certain)
|
||||
or
|
||||
variableWriteQualifier(bb, i, v, certain)
|
||||
or
|
||||
updatesNamedFieldOrProp(bb, i, _, v, _) and
|
||||
certain = false
|
||||
or
|
||||
updatesCapturedVariable(bb, i, _, v, _, _) and
|
||||
certain = false
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the `i`th of basic block `bb` reads source variable `v`.
|
||||
*
|
||||
* This includes implicit reads via calls.
|
||||
*/
|
||||
predicate variableRead(ControlFlow::BasicBlock bb, int i, Ssa::SourceVariable v, boolean certain) {
|
||||
variableReadActual(bb, i, v) and
|
||||
certain = true
|
||||
or
|
||||
variableReadPseudo(bb, i, v) and
|
||||
certain = false
|
||||
}
|
||||
}
|
||||
|
||||
import SsaImplCommon::Make<SsaInput>
|
||||
|
||||
/**
|
||||
* Holds if the `i`th node of basic block `bb` reads source variable `v`.
|
||||
@@ -805,24 +851,6 @@ private module CapturedVariableImpl {
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the `i`th node of basic block `bb` is a (potential) write to source
|
||||
* variable `v`. The Boolean `certain` indicates whether the write is certain.
|
||||
*
|
||||
* This includes implicit writes via calls.
|
||||
*/
|
||||
predicate variableWrite(ControlFlow::BasicBlock bb, int i, Ssa::SourceVariable v, boolean certain) {
|
||||
variableWriteDirect(bb, i, v, certain)
|
||||
or
|
||||
variableWriteQualifier(bb, i, v, certain)
|
||||
or
|
||||
updatesNamedFieldOrProp(bb, i, _, v, _) and
|
||||
certain = false
|
||||
or
|
||||
updatesCapturedVariable(bb, i, _, v, _, _) and
|
||||
certain = false
|
||||
}
|
||||
|
||||
/**
|
||||
* Liveness analysis to restrict the size of the SSA representation for
|
||||
* captured variables.
|
||||
@@ -1039,19 +1067,6 @@ private predicate variableReadPseudo(ControlFlow::BasicBlock bb, int i, Ssa::Sou
|
||||
capturedReadIn(bb, i, v, _, _, _)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the `i`th of basic block `bb` reads source variable `v`.
|
||||
*
|
||||
* This includes implicit reads via calls.
|
||||
*/
|
||||
predicate variableRead(ControlFlow::BasicBlock bb, int i, Ssa::SourceVariable v, boolean certain) {
|
||||
variableReadActual(bb, i, v) and
|
||||
certain = true
|
||||
or
|
||||
variableReadPseudo(bb, i, v) and
|
||||
certain = false
|
||||
}
|
||||
|
||||
cached
|
||||
private module Cached {
|
||||
cached
|
||||
@@ -1151,7 +1166,7 @@ private module Cached {
|
||||
predicate variableWriteQualifier(
|
||||
ControlFlow::BasicBlock bb, int i, QualifiedFieldOrPropSourceVariable v, boolean certain
|
||||
) {
|
||||
variableWrite(bb, i, v.getQualifier(), certain) and
|
||||
SsaInput::variableWrite(bb, i, v.getQualifier(), certain) and
|
||||
// Eliminate corner case where a call definition can overlap with a
|
||||
// qualifier definition: if method `M` updates field `F`, then a call
|
||||
// to `M` is both an update of `x.M` and `x.M.M`, so the former call
|
||||
|
||||
File diff suppressed because it is too large
Load Diff
@@ -1,19 +0,0 @@
|
||||
/** Provides the C# specific parameters for `SsaImplCommon.qll`. */
|
||||
|
||||
private import csharp
|
||||
private import AssignableDefinitions
|
||||
private import SsaImpl as SsaImpl
|
||||
|
||||
class BasicBlock = ControlFlow::BasicBlock;
|
||||
|
||||
BasicBlock getImmediateBasicBlockDominator(BasicBlock bb) { result = bb.getImmediateDominator() }
|
||||
|
||||
BasicBlock getABasicBlockSuccessor(BasicBlock bb) { result = bb.getASuccessor() }
|
||||
|
||||
class ExitBasicBlock = ControlFlow::BasicBlocks::ExitBlock;
|
||||
|
||||
class SourceVariable = Ssa::SourceVariable;
|
||||
|
||||
predicate variableWrite = SsaImpl::variableWrite/4;
|
||||
|
||||
predicate variableRead = SsaImpl::variableRead/4;
|
||||
@@ -1,795 +0,0 @@
|
||||
/**
|
||||
* Provides a language-independent 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`.
|
||||
*/
|
||||
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, _)
|
||||
}
|
||||
|
||||
predicate lastRefIsRead(BasicBlock bb, SourceVariable v) {
|
||||
maxRefRank(bb, v) = refRank(bb, _, v, Read(_))
|
||||
}
|
||||
|
||||
/**
|
||||
* 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 `df` is in the dominance frontier of `bb`.
|
||||
*
|
||||
* This is equivalent to:
|
||||
*
|
||||
* ```ql
|
||||
* bb = getImmediateBasicBlockDominator*(getABasicBlockPredecessor(df)) and
|
||||
* not bb = getImmediateBasicBlockDominator+(df)
|
||||
* ```
|
||||
*/
|
||||
private predicate inDominanceFrontier(BasicBlock bb, BasicBlock df) {
|
||||
bb = getABasicBlockPredecessor(df) and not bb = getImmediateBasicBlockDominator(df)
|
||||
or
|
||||
exists(BasicBlock prev | inDominanceFrontier(prev, df) |
|
||||
bb = getImmediateBasicBlockDominator(prev) and
|
||||
not bb = getImmediateBasicBlockDominator(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 =
|
||||
SsaActualRead() or
|
||||
SsaPhiRead() or
|
||||
SsaDef()
|
||||
|
||||
class SsaRead = SsaActualRead or SsaPhiRead;
|
||||
|
||||
/**
|
||||
* A classification of SSA variable references into reads and definitions.
|
||||
*/
|
||||
class SsaRefKind extends TSsaRefKind {
|
||||
string toString() {
|
||||
this = SsaActualRead() and
|
||||
result = "SsaActualRead"
|
||||
or
|
||||
this = SsaPhiRead() and
|
||||
result = "SsaPhiRead"
|
||||
or
|
||||
this = SsaDef() and
|
||||
result = "SsaDef"
|
||||
}
|
||||
|
||||
int getOrder() {
|
||||
this instanceof SsaRead and
|
||||
result = 0
|
||||
or
|
||||
this = SsaDef() and
|
||||
result = 1
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `bb` is in the dominance frontier of a block containing a
|
||||
* read of `v`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate inReadDominanceFrontier(BasicBlock bb, SourceVariable v) {
|
||||
exists(BasicBlock readbb | inDominanceFrontier(readbb, bb) |
|
||||
lastRefIsRead(readbb, v)
|
||||
or
|
||||
phiRead(readbb, v)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if a phi-read node should be inserted for variable `v` at the beginning
|
||||
* of basic block `bb`.
|
||||
*
|
||||
* Phi-read nodes are like normal phi nodes, but they are inserted based on reads
|
||||
* instead of writes, and only if the dominance-frontier block does not already
|
||||
* contain a reference (read or write) to `v`. Unlike normal phi nodes, this is
|
||||
* an internal implementation detail that is not exposed.
|
||||
*
|
||||
* The motivation for adding phi-reads is to improve performance of the use-use
|
||||
* calculation in cases where there is a large number of reads that can reach the
|
||||
* same join-point, and from there reach a large number of basic blocks. Example:
|
||||
*
|
||||
* ```cs
|
||||
* if (a)
|
||||
* use(x);
|
||||
* else if (b)
|
||||
* use(x);
|
||||
* else if (c)
|
||||
* use(x);
|
||||
* else if (d)
|
||||
* use(x);
|
||||
* // many more ifs ...
|
||||
*
|
||||
* // phi-read for `x` inserted here
|
||||
*
|
||||
* // program not mentioning `x`, with large basic block graph
|
||||
*
|
||||
* use(x);
|
||||
* ```
|
||||
*
|
||||
* Without phi-reads, the analysis has to replicate reachability for each of
|
||||
* the guarded uses of `x`. However, with phi-reads, the analysis will limit
|
||||
* each conditional use of `x` to reach the basic block containing the phi-read
|
||||
* node for `x`, and only that basic block will have to compute reachability
|
||||
* through the remainder of the large program.
|
||||
*
|
||||
* Like normal reads, each phi-read node `phi-read` can be reached from exactly
|
||||
* one SSA definition (without passing through another definition): Assume, for
|
||||
* the sake of contradiction, that there are two reaching definitions `def1` and
|
||||
* `def2`. Now, if both `def1` and `def2` dominate `phi-read`, then the nearest
|
||||
* dominating definition will prevent the other from reaching `phi-read`. So, at
|
||||
* least one of `def1` and `def2` cannot dominate `phi-read`; assume it is `def1`.
|
||||
* Then `def1` must go through one of its dominance-frontier blocks in order to
|
||||
* reach `phi-read`. However, such a block will always start with a (normal) phi
|
||||
* node, which contradicts reachability.
|
||||
*
|
||||
* Also, like normal reads, the unique SSA definition `def` that reaches `phi-read`,
|
||||
* will dominate `phi-read`. Assuming it doesn't means that the path from `def`
|
||||
* to `phi-read` goes through a dominance-frontier block, and hence a phi node,
|
||||
* which contradicts reachability.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate phiRead(BasicBlock bb, SourceVariable v) {
|
||||
inReadDominanceFrontier(bb, v) and
|
||||
liveAtEntry(bb, v) and
|
||||
// only if there are no other references to `v` inside `bb`
|
||||
not ref(bb, _, v, _) and
|
||||
not exists(Definition def | def.definesAt(v, bb, _))
|
||||
}
|
||||
|
||||
/**
|
||||
* 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.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate ssaRef(BasicBlock bb, int i, SourceVariable v, SsaRefKind k) {
|
||||
variableRead(bb, i, v, _) and
|
||||
k = SsaActualRead()
|
||||
or
|
||||
phiRead(bb, v) and
|
||||
i = -1 and
|
||||
k = SsaPhiRead()
|
||||
or
|
||||
any(Definition 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, any(SsaRead k))
|
||||
}
|
||||
|
||||
/**
|
||||
* 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, any(SsaRead k))
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* 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)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the reference to `def` at index `i` in basic block `bb` is the
|
||||
* last reference to `v` inside `bb`.
|
||||
*/
|
||||
pragma[noinline]
|
||||
predicate lastSsaRef(Definition def, SourceVariable v, BasicBlock bb, int i) {
|
||||
ssaDefRank(def, v, bb, i, _) = maxSsaRefRank(bb, v)
|
||||
}
|
||||
|
||||
predicate defOccursInBlock(Definition def, BasicBlock bb, SourceVariable v, SsaRefKind k) {
|
||||
exists(ssaDefRank(def, v, bb, _, k))
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate ssaDefReachesThroughBlock(Definition def, BasicBlock bb) {
|
||||
ssaDefReachesEndOfBlock(bb, def, _) and
|
||||
not defOccursInBlock(_, bb, def.getSourceVariable(), _)
|
||||
}
|
||||
|
||||
/**
|
||||
* 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 _some_
|
||||
* predecessor of `bb2`, and the underlying variable for `def` is neither read
|
||||
* nor written in any block on the path between `bb1` and `bb2`.
|
||||
*
|
||||
* Phi reads are considered as normal reads for this predicate.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
private predicate varBlockReachesInclPhiRead(Definition def, BasicBlock bb1, BasicBlock bb2) {
|
||||
defOccursInBlock(def, bb1, _, _) and
|
||||
bb2 = getABasicBlockSuccessor(bb1)
|
||||
or
|
||||
exists(BasicBlock mid |
|
||||
varBlockReachesInclPhiRead(def, bb1, mid) and
|
||||
ssaDefReachesThroughBlock(def, mid) and
|
||||
bb2 = getABasicBlockSuccessor(mid)
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate phiReadStep(Definition def, SourceVariable v, BasicBlock bb1, BasicBlock bb2) {
|
||||
varBlockReachesInclPhiRead(def, bb1, bb2) and
|
||||
defOccursInBlock(def, bb2, v, SsaPhiRead())
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate varBlockReachesExclPhiRead(Definition def, BasicBlock bb1, BasicBlock bb2) {
|
||||
varBlockReachesInclPhiRead(pragma[only_bind_into](def), bb1, pragma[only_bind_into](bb2)) and
|
||||
ssaRef(bb2, _, def.getSourceVariable(), [SsaActualRead().(TSsaRefKind), SsaDef()])
|
||||
or
|
||||
exists(BasicBlock mid |
|
||||
varBlockReachesExclPhiRead(def, mid, bb2) and
|
||||
phiReadStep(def, _, bb1, mid)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `def` is accessed in basic block `bb1` (either a read or a write),
|
||||
* the underlying variable `v` of `def` is accessed in basic block `bb2`
|
||||
* (either a read or a write), `bb2` is a transitive successor of `bb1`, and
|
||||
* `v` is neither read nor written in any block on the path between `bb1`
|
||||
* and `bb2`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate varBlockReaches(Definition def, BasicBlock bb1, BasicBlock bb2) {
|
||||
varBlockReachesExclPhiRead(def, bb1, bb2) and
|
||||
not defOccursInBlock(def, bb1, _, SsaPhiRead())
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
predicate defAdjacentRead(Definition def, BasicBlock bb1, BasicBlock bb2, int i2) {
|
||||
varBlockReaches(def, bb1, bb2) and
|
||||
ssaRefRank(bb2, i2, def.getSourceVariable(), SsaActualRead()) = 1
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `def` is accessed in basic block `bb` (either a read or a write),
|
||||
* `bb1` can reach a transitive successor `bb2` where `def` is no longer live,
|
||||
* and `v` is neither read nor written in any block on the path between `bb`
|
||||
* and `bb2`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate varBlockReachesExit(Definition def, BasicBlock bb) {
|
||||
exists(BasicBlock bb2 | varBlockReachesInclPhiRead(def, bb, bb2) |
|
||||
not defOccursInBlock(def, bb2, _, _) and
|
||||
not ssaDefReachesEndOfBlock(bb2, def, _)
|
||||
)
|
||||
or
|
||||
exists(BasicBlock mid |
|
||||
varBlockReachesExit(def, mid) and
|
||||
phiReadStep(def, _, bb, mid)
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
predicate phiReadExposedForTesting = phiRead/2;
|
||||
|
||||
private import SsaDefReaches
|
||||
|
||||
pragma[nomagic]
|
||||
predicate liveThrough(BasicBlock bb, SourceVariable v) {
|
||||
liveAtExit(bb, v) and
|
||||
not ssaRef(bb, _, v, SsaDef())
|
||||
}
|
||||
|
||||
/**
|
||||
* 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(pragma[only_bind_into](bb), pragma[only_bind_into](v)) and
|
||||
ssaDefReachesRank(bb, def, last, v) and
|
||||
liveAtExit(bb, v)
|
||||
)
|
||||
or
|
||||
// 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.
|
||||
ssaDefReachesEndOfBlock(getImmediateBasicBlockDominator(bb), def, pragma[only_bind_into](v)) and
|
||||
liveThrough(bb, pragma[only_bind_into](v))
|
||||
}
|
||||
|
||||
/**
|
||||
* 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
|
||||
ssaRef(bb, i, v, any(SsaRead k)) 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, SsaActualRead()) and
|
||||
variableRead(bb1, i2, _, _) and
|
||||
bb2 = bb1
|
||||
)
|
||||
or
|
||||
lastSsaRef(def, _, bb1, i1) and
|
||||
defAdjacentRead(def, bb1, bb2, i2)
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate adjacentDefRead(
|
||||
Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2, SourceVariable v
|
||||
) {
|
||||
adjacentDefRead(def, bb1, i1, bb2, i2) and
|
||||
v = def.getSourceVariable()
|
||||
}
|
||||
|
||||
private predicate adjacentDefReachesRead(
|
||||
Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2
|
||||
) {
|
||||
exists(SourceVariable v | adjacentDefRead(def, bb1, i1, bb2, i2, v) |
|
||||
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(SourceVariable v |
|
||||
// Next reference to `v` inside `bb` is a write
|
||||
exists(int rnk, int j |
|
||||
rnk = ssaDefRank(def, v, bb, i, _) and
|
||||
next.definesAt(v, bb, j) and
|
||||
rnk + 1 = ssaRefRank(bb, j, v, SsaDef())
|
||||
)
|
||||
or
|
||||
// Can reach a write using one or more steps
|
||||
lastSsaRef(def, v, bb, i) and
|
||||
exists(BasicBlock bb2 |
|
||||
varBlockReaches(def, bb, bb2) and
|
||||
1 = ssaDefRank(next, v, bb2, _, 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) {
|
||||
// Can reach another definition
|
||||
lastRefRedef(def, bb, i, _)
|
||||
or
|
||||
exists(SourceVariable v | lastSsaRef(def, v, bb, i) |
|
||||
// Can reach exit directly
|
||||
bb instanceof ExitBasicBlock
|
||||
or
|
||||
// Can reach a block using one or more steps, where `def` is no longer live
|
||||
varBlockReachesExit(def, bb)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* 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)
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
/** Provides a set of consistency queries. */
|
||||
module Consistency {
|
||||
abstract class RelevantDefinition extends Definition {
|
||||
abstract predicate hasLocationInfo(
|
||||
string filepath, int startline, int startcolumn, int endline, int endcolumn
|
||||
);
|
||||
}
|
||||
|
||||
query predicate nonUniqueDef(RelevantDefinition def, SourceVariable v, BasicBlock bb, int i) {
|
||||
ssaDefReachesRead(v, def, bb, i) and
|
||||
not exists(unique(Definition def0 | ssaDefReachesRead(v, def0, bb, i)))
|
||||
}
|
||||
|
||||
query predicate readWithoutDef(SourceVariable v, BasicBlock bb, int i) {
|
||||
variableRead(bb, i, v, _) and
|
||||
not ssaDefReachesRead(v, _, bb, i)
|
||||
}
|
||||
|
||||
query predicate deadDef(RelevantDefinition def, SourceVariable v) {
|
||||
v = def.getSourceVariable() and
|
||||
not ssaDefReachesRead(_, def, _, _) and
|
||||
not phiHasInputFromBlock(_, def, _) and
|
||||
not uncertainWriteDefinitionInput(_, def)
|
||||
}
|
||||
|
||||
query predicate notDominatedByDef(RelevantDefinition def, SourceVariable v, BasicBlock bb, int i) {
|
||||
exists(BasicBlock bbDef, int iDef | def.definesAt(v, bbDef, iDef) |
|
||||
ssaDefReachesReadWithinBlock(v, def, bb, i) and
|
||||
(bb != bbDef or i < iDef)
|
||||
or
|
||||
ssaDefReachesRead(v, def, bb, i) and
|
||||
not ssaDefReachesReadWithinBlock(v, def, bb, i) and
|
||||
not def.definesAt(v, getImmediateBasicBlockDominator*(bb), _)
|
||||
)
|
||||
}
|
||||
}
|
||||
@@ -1,51 +0,0 @@
|
||||
/** 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
|
||||
)
|
||||
}
|
||||
@@ -7,7 +7,9 @@ class CallableWithSplitting extends Callable {
|
||||
CallableWithSplitting() { this = any(SplitControlFlowElement e).getEnclosingCallable() }
|
||||
}
|
||||
|
||||
query predicate defReadInconsistency(AssignableRead ar, Expr e, PreSsa::SourceVariable v, boolean b) {
|
||||
query predicate defReadInconsistency(
|
||||
AssignableRead ar, Expr e, PreSsa::SsaInput::SourceVariable v, boolean b
|
||||
) {
|
||||
// Exclude definitions in callables with CFG splitting, as SSA definitions may be
|
||||
// very different from pre-SSA definitions
|
||||
not ar.getEnclosingCallable() instanceof CallableWithSplitting and
|
||||
@@ -36,7 +38,8 @@ query predicate defReadInconsistency(AssignableRead ar, Expr e, PreSsa::SourceVa
|
||||
}
|
||||
|
||||
query predicate readReadInconsistency(
|
||||
LocalScopeVariableRead read1, LocalScopeVariableRead read2, PreSsa::SourceVariable v, boolean b
|
||||
LocalScopeVariableRead read1, LocalScopeVariableRead read2, PreSsa::SsaInput::SourceVariable v,
|
||||
boolean b
|
||||
) {
|
||||
// Exclude definitions in callables with CFG splitting, as SSA definitions may be
|
||||
// very different from pre-SSA definitions
|
||||
@@ -50,7 +53,7 @@ query predicate readReadInconsistency(
|
||||
b = false and
|
||||
v = read1.getTarget() and
|
||||
SsaImpl::adjacentReadPairSameVar(_, read1.getAControlFlowNode(), read2.getAControlFlowNode()) and
|
||||
read1.getTarget() instanceof PreSsa::SourceVariable and
|
||||
read1.getTarget() instanceof PreSsa::SsaInput::SourceVariable and
|
||||
not PreSsa::adjacentReadPairSameVar(read1, read2) and
|
||||
// Exclude split CFG elements because SSA may be more precise than pre-SSA
|
||||
// in those cases
|
||||
@@ -59,7 +62,9 @@ query predicate readReadInconsistency(
|
||||
)
|
||||
}
|
||||
|
||||
query predicate phiInconsistency(ControlFlowElement cfe, Expr e, PreSsa::SourceVariable v, boolean b) {
|
||||
query predicate phiInconsistency(
|
||||
ControlFlowElement cfe, Expr e, PreSsa::SsaInput::SourceVariable v, boolean b
|
||||
) {
|
||||
// Exclude definitions in callables with CFG splitting, as SSA definitions may be
|
||||
// very different from pre-SSA definitions
|
||||
not cfe.getEnclosingCallable() instanceof CallableWithSplitting and
|
||||
|
||||
@@ -1,5 +1,5 @@
|
||||
import csharp
|
||||
import semmle.code.csharp.dataflow.internal.SsaImplCommon
|
||||
import semmle.code.csharp.dataflow.internal.SsaImpl
|
||||
|
||||
from Ssa::SourceVariable v, ControlFlow::BasicBlock bb
|
||||
where phiReadExposedForTesting(bb, v)
|
||||
|
||||
@@ -1,10 +1,18 @@
|
||||
import codeql.ruby.dataflow.SSA
|
||||
import codeql.ruby.dataflow.internal.SsaImplCommon::Consistency
|
||||
import codeql.ruby.dataflow.internal.SsaImpl::Consistency as Consistency
|
||||
|
||||
class MyRelevantDefinition extends RelevantDefinition, Ssa::Definition {
|
||||
class MyRelevantDefinition extends Consistency::RelevantDefinition, Ssa::Definition {
|
||||
override predicate hasLocationInfo(
|
||||
string filepath, int startline, int startcolumn, int endline, int endcolumn
|
||||
) {
|
||||
this.getLocation().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
|
||||
}
|
||||
}
|
||||
|
||||
query predicate nonUniqueDef = Consistency::nonUniqueDef/4;
|
||||
|
||||
query predicate readWithoutDef = Consistency::readWithoutDef/3;
|
||||
|
||||
query predicate deadDef = Consistency::deadDef/2;
|
||||
|
||||
query predicate notDominatedByDef = Consistency::notDominatedByDef/4;
|
||||
|
||||
@@ -9,12 +9,11 @@ module Ssa {
|
||||
private import codeql.Locations
|
||||
private import codeql.ruby.CFG
|
||||
private import codeql.ruby.ast.Variable
|
||||
private import internal.SsaImplCommon as SsaImplCommon
|
||||
private import internal.SsaImpl as SsaImpl
|
||||
private import CfgNodes::ExprNodes
|
||||
|
||||
/** A static single assignment (SSA) definition. */
|
||||
class Definition extends SsaImplCommon::Definition {
|
||||
class Definition extends SsaImpl::Definition {
|
||||
/**
|
||||
* Gets the control flow node of this SSA definition, if any. Phi nodes are
|
||||
* examples of SSA definitions without a control flow node, as they are
|
||||
@@ -190,7 +189,7 @@ module Ssa {
|
||||
* puts x
|
||||
* ```
|
||||
*/
|
||||
class WriteDefinition extends Definition, SsaImplCommon::WriteDefinition {
|
||||
class WriteDefinition extends Definition, SsaImpl::WriteDefinition {
|
||||
private VariableWriteAccess write;
|
||||
|
||||
WriteDefinition() {
|
||||
@@ -223,7 +222,7 @@ module Ssa {
|
||||
/**
|
||||
* An SSA definition that corresponds to the value of `self` upon entry to a method, class or module.
|
||||
*/
|
||||
class SelfDefinition extends Definition, SsaImplCommon::WriteDefinition {
|
||||
class SelfDefinition extends Definition, SsaImpl::WriteDefinition {
|
||||
private SelfVariable v;
|
||||
|
||||
SelfDefinition() {
|
||||
@@ -254,7 +253,7 @@ module Ssa {
|
||||
* since the assignment to `x` is conditional, an unitialized definition for
|
||||
* `x` is inserted at the start of `m`.
|
||||
*/
|
||||
class UninitializedDefinition extends Definition, SsaImplCommon::WriteDefinition {
|
||||
class UninitializedDefinition extends Definition, SsaImpl::WriteDefinition {
|
||||
UninitializedDefinition() {
|
||||
exists(BasicBlock bb, int i, Variable v |
|
||||
this.definesAt(v, bb, i) and
|
||||
@@ -283,7 +282,7 @@ module Ssa {
|
||||
*
|
||||
* an entry definition for `y` is inserted at the start of the `do` block.
|
||||
*/
|
||||
class CapturedEntryDefinition extends Definition, SsaImplCommon::WriteDefinition {
|
||||
class CapturedEntryDefinition extends Definition, SsaImpl::WriteDefinition {
|
||||
CapturedEntryDefinition() {
|
||||
exists(BasicBlock bb, int i, Variable v |
|
||||
this.definesAt(v, bb, i) and
|
||||
@@ -312,7 +311,7 @@ module Ssa {
|
||||
*
|
||||
* a definition for `y` is inserted at the call to `times`.
|
||||
*/
|
||||
class CapturedCallDefinition extends Definition, SsaImplCommon::UncertainWriteDefinition {
|
||||
class CapturedCallDefinition extends Definition, SsaImpl::UncertainWriteDefinition {
|
||||
CapturedCallDefinition() {
|
||||
exists(Variable v, BasicBlock bb, int i |
|
||||
this.definesAt(v, bb, i) and
|
||||
@@ -343,7 +342,7 @@ module Ssa {
|
||||
*
|
||||
* a phi node for `x` is inserted just before the call `puts x`.
|
||||
*/
|
||||
class PhiNode extends Definition, SsaImplCommon::PhiNode {
|
||||
class PhiNode extends Definition, SsaImpl::PhiNode {
|
||||
/**
|
||||
* Gets an input of this phi node.
|
||||
*
|
||||
|
||||
@@ -1,19 +1,72 @@
|
||||
private import SsaImplCommon
|
||||
private import SsaImplSpecific as SsaImplSpecific
|
||||
private import SsaImplCommon as SsaImplCommon
|
||||
private import codeql.ruby.AST
|
||||
private import codeql.ruby.CFG
|
||||
private import codeql.ruby.CFG as CFG
|
||||
private import codeql.ruby.ast.Variable
|
||||
private import CfgNodes::ExprNodes
|
||||
private import CFG::CfgNodes::ExprNodes
|
||||
|
||||
private module SsaInput implements SsaImplCommon::InputSig {
|
||||
private import codeql.ruby.controlflow.BasicBlocks as BasicBlocks
|
||||
|
||||
class BasicBlock = BasicBlocks::BasicBlock;
|
||||
|
||||
BasicBlock getImmediateBasicBlockDominator(BasicBlock bb) { result = bb.getImmediateDominator() }
|
||||
|
||||
BasicBlock getABasicBlockSuccessor(BasicBlock bb) { result = bb.getASuccessor() }
|
||||
|
||||
class ExitBasicBlock = BasicBlocks::ExitBasicBlock;
|
||||
|
||||
class SourceVariable = LocalVariable;
|
||||
|
||||
/**
|
||||
* Holds if the statement at index `i` of basic block `bb` contains a write to variable `v`.
|
||||
* `certain` is true if the write definitely occurs.
|
||||
*/
|
||||
predicate variableWrite(BasicBlock bb, int i, SourceVariable v, boolean certain) {
|
||||
(
|
||||
exists(Scope scope | scope = v.(SelfVariable).getDeclaringScope() |
|
||||
// We consider the `self` variable to have a single write at the entry to a method block...
|
||||
scope = bb.(BasicBlocks::EntryBasicBlock).getScope() and
|
||||
i = 0
|
||||
or
|
||||
// ...or a class or module block.
|
||||
bb.getNode(i).getNode() = scope.(ModuleBase).getAControlFlowEntryNode()
|
||||
)
|
||||
or
|
||||
uninitializedWrite(bb, i, v)
|
||||
or
|
||||
capturedEntryWrite(bb, i, v)
|
||||
or
|
||||
variableWriteActual(bb, i, v, _)
|
||||
) and
|
||||
certain = true
|
||||
or
|
||||
capturedCallWrite(_, bb, i, v) and
|
||||
certain = false
|
||||
}
|
||||
|
||||
predicate variableRead(BasicBlock bb, int i, LocalVariable v, boolean certain) {
|
||||
variableReadActual(bb, i, v) and
|
||||
certain = true
|
||||
or
|
||||
capturedCallRead(_, bb, i, v) and
|
||||
certain = false
|
||||
or
|
||||
capturedExitRead(bb, i, v) and
|
||||
certain = false
|
||||
}
|
||||
}
|
||||
|
||||
import SsaImplCommon::Make<SsaInput>
|
||||
|
||||
/** Holds if `v` is uninitialized at index `i` in entry block `bb`. */
|
||||
predicate uninitializedWrite(EntryBasicBlock bb, int i, LocalVariable v) {
|
||||
predicate uninitializedWrite(CFG::EntryBasicBlock bb, int i, LocalVariable v) {
|
||||
v.getDeclaringScope() = bb.getScope() and
|
||||
i = -1
|
||||
}
|
||||
|
||||
/** Holds if `bb` contains a caputured read of variable `v`. */
|
||||
pragma[noinline]
|
||||
private predicate hasCapturedVariableRead(BasicBlock bb, LocalVariable v) {
|
||||
private predicate hasCapturedVariableRead(CFG::BasicBlock bb, LocalVariable v) {
|
||||
exists(LocalVariableReadAccess read |
|
||||
read = bb.getANode().getNode() and
|
||||
read.isCapturedAccess() and
|
||||
@@ -23,7 +76,7 @@ private predicate hasCapturedVariableRead(BasicBlock bb, LocalVariable v) {
|
||||
|
||||
/** Holds if `bb` contains a caputured write to variable `v`. */
|
||||
pragma[noinline]
|
||||
private predicate writesCapturedVariable(BasicBlock bb, LocalVariable v) {
|
||||
private predicate writesCapturedVariable(CFG::BasicBlock bb, LocalVariable v) {
|
||||
exists(LocalVariableWriteAccess write |
|
||||
write = bb.getANode().getNode() and
|
||||
write.isCapturedAccess() and
|
||||
@@ -35,7 +88,7 @@ private predicate writesCapturedVariable(BasicBlock bb, LocalVariable v) {
|
||||
* Holds if a pseudo read of captured variable `v` should be inserted
|
||||
* at index `i` in exit block `bb`.
|
||||
*/
|
||||
private predicate capturedExitRead(AnnotatedExitBasicBlock bb, int i, LocalVariable v) {
|
||||
private predicate capturedExitRead(CFG::AnnotatedExitBasicBlock bb, int i, LocalVariable v) {
|
||||
bb.isNormal() and
|
||||
writesCapturedVariable(bb.getAPredecessor*(), v) and
|
||||
i = bb.length()
|
||||
@@ -46,7 +99,7 @@ private predicate capturedExitRead(AnnotatedExitBasicBlock bb, int i, LocalVaria
|
||||
* or inside a (transitively) nested scope of `scope`.
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate hasCapturedRead(Variable v, CfgScope scope) {
|
||||
private predicate hasCapturedRead(Variable v, CFG::CfgScope scope) {
|
||||
any(LocalVariableReadAccess read |
|
||||
read.getVariable() = v and scope = read.getCfgScope().getOuterCfgScope*()
|
||||
).isCapturedAccess()
|
||||
@@ -57,13 +110,15 @@ private predicate hasCapturedRead(Variable v, CfgScope scope) {
|
||||
* outer scope of `scope`.
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate variableWriteInOuterScope(BasicBlock bb, LocalVariable v, CfgScope scope) {
|
||||
SsaImplSpecific::variableWrite(bb, _, v, _) and
|
||||
private predicate variableWriteInOuterScope(CFG::BasicBlock bb, LocalVariable v, CFG::CfgScope scope) {
|
||||
SsaInput::variableWrite(bb, _, v, _) and
|
||||
scope.getOuterCfgScope() = bb.getScope()
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate hasVariableWriteWithCapturedRead(BasicBlock bb, LocalVariable v, CfgScope scope) {
|
||||
private predicate hasVariableWriteWithCapturedRead(
|
||||
CFG::BasicBlock bb, LocalVariable v, CFG::CfgScope scope
|
||||
) {
|
||||
hasCapturedRead(v, scope) and
|
||||
variableWriteInOuterScope(bb, v, scope)
|
||||
}
|
||||
@@ -72,10 +127,8 @@ private predicate hasVariableWriteWithCapturedRead(BasicBlock bb, LocalVariable
|
||||
* Holds if the call `call` at index `i` in basic block `bb` may reach
|
||||
* a callable that reads captured variable `v`.
|
||||
*/
|
||||
private predicate capturedCallRead(
|
||||
CfgNodes::ExprNodes::CallCfgNode call, BasicBlock bb, int i, LocalVariable v
|
||||
) {
|
||||
exists(CfgScope scope |
|
||||
private predicate capturedCallRead(CallCfgNode call, CFG::BasicBlock bb, int i, LocalVariable v) {
|
||||
exists(CFG::CfgScope scope |
|
||||
hasVariableWriteWithCapturedRead(bb.getAPredecessor*(), v, scope) and
|
||||
call = bb.getNode(i)
|
||||
|
|
||||
@@ -88,30 +141,19 @@ private predicate capturedCallRead(
|
||||
}
|
||||
|
||||
/** Holds if `v` is read at index `i` in basic block `bb`. */
|
||||
private predicate variableReadActual(BasicBlock bb, int i, LocalVariable v) {
|
||||
private predicate variableReadActual(CFG::BasicBlock bb, int i, LocalVariable v) {
|
||||
exists(VariableReadAccess read |
|
||||
read.getVariable() = v and
|
||||
read = bb.getNode(i).getNode()
|
||||
)
|
||||
}
|
||||
|
||||
predicate variableRead(BasicBlock bb, int i, LocalVariable v, boolean certain) {
|
||||
variableReadActual(bb, i, v) and
|
||||
certain = true
|
||||
or
|
||||
capturedCallRead(_, bb, i, v) and
|
||||
certain = false
|
||||
or
|
||||
capturedExitRead(bb, i, v) and
|
||||
certain = false
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if captured variable `v` is written directly inside `scope`,
|
||||
* or inside a (transitively) nested scope of `scope`.
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate hasCapturedWrite(Variable v, CfgScope scope) {
|
||||
private predicate hasCapturedWrite(Variable v, CFG::CfgScope scope) {
|
||||
any(LocalVariableWriteAccess write |
|
||||
write.getVariable() = v and scope = write.getCfgScope().getOuterCfgScope*()
|
||||
).isCapturedAccess()
|
||||
@@ -122,13 +164,17 @@ private predicate hasCapturedWrite(Variable v, CfgScope scope) {
|
||||
* outer scope of `scope`.
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate variableReadActualInOuterScope(BasicBlock bb, LocalVariable v, CfgScope scope) {
|
||||
private predicate variableReadActualInOuterScope(
|
||||
CFG::BasicBlock bb, LocalVariable v, CFG::CfgScope scope
|
||||
) {
|
||||
variableReadActual(bb, _, v) and
|
||||
bb.getScope() = scope.getOuterCfgScope()
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate hasVariableReadWithCapturedWrite(BasicBlock bb, LocalVariable v, CfgScope scope) {
|
||||
private predicate hasVariableReadWithCapturedWrite(
|
||||
CFG::BasicBlock bb, LocalVariable v, CFG::CfgScope scope
|
||||
) {
|
||||
hasCapturedWrite(v, scope) and
|
||||
variableReadActualInOuterScope(bb, v, scope)
|
||||
}
|
||||
@@ -140,7 +186,7 @@ private module Cached {
|
||||
* `i` in entry block `bb`.
|
||||
*/
|
||||
cached
|
||||
predicate capturedEntryWrite(EntryBasicBlock bb, int i, LocalVariable v) {
|
||||
predicate capturedEntryWrite(CFG::EntryBasicBlock bb, int i, LocalVariable v) {
|
||||
hasCapturedVariableRead(bb.getASuccessor*(), v) and
|
||||
i = -1
|
||||
}
|
||||
@@ -150,10 +196,8 @@ private module Cached {
|
||||
* that writes captured variable `v`.
|
||||
*/
|
||||
cached
|
||||
predicate capturedCallWrite(
|
||||
CfgNodes::ExprNodes::CallCfgNode call, BasicBlock bb, int i, LocalVariable v
|
||||
) {
|
||||
exists(CfgScope scope |
|
||||
predicate capturedCallWrite(CallCfgNode call, CFG::BasicBlock bb, int i, LocalVariable v) {
|
||||
exists(CFG::CfgScope scope |
|
||||
hasVariableReadWithCapturedWrite(bb.getASuccessor*(), v, scope) and
|
||||
call = bb.getNode(i)
|
||||
|
|
||||
@@ -170,7 +214,9 @@ private module Cached {
|
||||
* AST write access is `write`.
|
||||
*/
|
||||
cached
|
||||
predicate variableWriteActual(BasicBlock bb, int i, LocalVariable v, VariableWriteAccess write) {
|
||||
predicate variableWriteActual(
|
||||
CFG::BasicBlock bb, int i, LocalVariable v, VariableWriteAccess write
|
||||
) {
|
||||
exists(AstNode n |
|
||||
write.getVariable() = v and
|
||||
n = bb.getNode(i).getNode()
|
||||
@@ -184,7 +230,7 @@ private module Cached {
|
||||
|
||||
cached
|
||||
VariableReadAccessCfgNode getARead(Definition def) {
|
||||
exists(LocalVariable v, BasicBlock bb, int i |
|
||||
exists(LocalVariable v, CFG::BasicBlock bb, int i |
|
||||
ssaDefReachesRead(v, def, bb, i) and
|
||||
variableReadActual(bb, i, v) and
|
||||
result = bb.getNode(i)
|
||||
@@ -193,9 +239,9 @@ private module Cached {
|
||||
|
||||
pragma[noinline]
|
||||
private predicate defReachesCallReadInOuterScope(
|
||||
Definition def, CfgNodes::ExprNodes::CallCfgNode call, LocalVariable v, CfgScope scope
|
||||
Definition def, CallCfgNode call, LocalVariable v, CFG::CfgScope scope
|
||||
) {
|
||||
exists(BasicBlock bb, int i |
|
||||
exists(CFG::BasicBlock bb, int i |
|
||||
ssaDefReachesRead(v, def, bb, i) and
|
||||
capturedCallRead(call, bb, i, v) and
|
||||
scope.getOuterCfgScope() = bb.getScope()
|
||||
@@ -203,8 +249,8 @@ private module Cached {
|
||||
}
|
||||
|
||||
pragma[noinline]
|
||||
private predicate hasCapturedEntryWrite(Definition entry, LocalVariable v, CfgScope scope) {
|
||||
exists(BasicBlock bb, int i |
|
||||
private predicate hasCapturedEntryWrite(Definition entry, LocalVariable v, CFG::CfgScope scope) {
|
||||
exists(CFG::BasicBlock bb, int i |
|
||||
capturedEntryWrite(bb, i, v) and
|
||||
entry.definesAt(v, bb, i) and
|
||||
bb.getScope().getOuterCfgScope*() = scope
|
||||
@@ -221,8 +267,8 @@ private module Cached {
|
||||
* ```
|
||||
*/
|
||||
cached
|
||||
predicate captureFlowIn(CfgNodes::ExprNodes::CallCfgNode call, Definition def, Definition entry) {
|
||||
exists(LocalVariable v, CfgScope scope |
|
||||
predicate captureFlowIn(CallCfgNode call, Definition def, Definition entry) {
|
||||
exists(LocalVariable v, CFG::CfgScope scope |
|
||||
defReachesCallReadInOuterScope(def, call, v, scope) and
|
||||
hasCapturedEntryWrite(entry, v, scope)
|
||||
|
|
||||
@@ -237,8 +283,10 @@ private module Cached {
|
||||
private import codeql.ruby.dataflow.SSA
|
||||
|
||||
pragma[noinline]
|
||||
private predicate defReachesExitReadInInnerScope(Definition def, LocalVariable v, CfgScope scope) {
|
||||
exists(BasicBlock bb, int i |
|
||||
private predicate defReachesExitReadInInnerScope(
|
||||
Definition def, LocalVariable v, CFG::CfgScope scope
|
||||
) {
|
||||
exists(CFG::BasicBlock bb, int i |
|
||||
ssaDefReachesRead(v, def, bb, i) and
|
||||
capturedExitRead(bb, i, v) and
|
||||
scope = bb.getScope().getOuterCfgScope*()
|
||||
@@ -247,9 +295,9 @@ private module Cached {
|
||||
|
||||
pragma[noinline]
|
||||
private predicate hasCapturedExitRead(
|
||||
Definition exit, CfgNodes::ExprNodes::CallCfgNode call, LocalVariable v, CfgScope scope
|
||||
Definition exit, CallCfgNode call, LocalVariable v, CFG::CfgScope scope
|
||||
) {
|
||||
exists(BasicBlock bb, int i |
|
||||
exists(CFG::BasicBlock bb, int i |
|
||||
capturedCallWrite(call, bb, i, v) and
|
||||
exit.definesAt(v, bb, i) and
|
||||
bb.getScope() = scope.getOuterCfgScope()
|
||||
@@ -267,8 +315,8 @@ private module Cached {
|
||||
* ```
|
||||
*/
|
||||
cached
|
||||
predicate captureFlowOut(CfgNodes::ExprNodes::CallCfgNode call, Definition def, Definition exit) {
|
||||
exists(LocalVariable v, CfgScope scope |
|
||||
predicate captureFlowOut(CallCfgNode call, Definition def, Definition exit) {
|
||||
exists(LocalVariable v, CFG::CfgScope scope |
|
||||
defReachesExitReadInInnerScope(def, v, scope) and
|
||||
hasCapturedExitRead(exit, call, v, _)
|
||||
|
|
||||
@@ -281,7 +329,7 @@ private module Cached {
|
||||
}
|
||||
|
||||
cached
|
||||
Definition phiHasInputFromBlock(PhiNode phi, BasicBlock bb) {
|
||||
Definition phiHasInputFromBlock(PhiNode phi, CFG::BasicBlock bb) {
|
||||
phiHasInputFromBlock(phi, result, bb)
|
||||
}
|
||||
|
||||
@@ -291,7 +339,7 @@ private module Cached {
|
||||
*/
|
||||
cached
|
||||
predicate firstRead(Definition def, VariableReadAccessCfgNode read) {
|
||||
exists(BasicBlock bb1, int i1, BasicBlock bb2, int i2 |
|
||||
exists(CFG::BasicBlock bb1, int i1, CFG::BasicBlock bb2, int i2 |
|
||||
def.definesAt(_, bb1, i1) and
|
||||
adjacentDefNoUncertainReads(def, bb1, i1, bb2, i2) and
|
||||
read = bb2.getNode(i2)
|
||||
@@ -307,7 +355,7 @@ private module Cached {
|
||||
predicate adjacentReadPair(
|
||||
Definition def, VariableReadAccessCfgNode read1, VariableReadAccessCfgNode read2
|
||||
) {
|
||||
exists(BasicBlock bb1, int i1, BasicBlock bb2, int i2 |
|
||||
exists(CFG::BasicBlock bb1, int i1, CFG::BasicBlock bb2, int i2 |
|
||||
read1 = bb1.getNode(i1) and
|
||||
variableReadActual(bb1, i1, _) and
|
||||
adjacentDefNoUncertainReads(def, bb1, i1, bb2, i2) and
|
||||
@@ -322,7 +370,7 @@ private module Cached {
|
||||
*/
|
||||
cached
|
||||
predicate lastRead(Definition def, VariableReadAccessCfgNode read) {
|
||||
exists(BasicBlock bb, int i |
|
||||
exists(CFG::BasicBlock bb, int i |
|
||||
lastRefNoUncertainReads(def, bb, i) and
|
||||
variableReadActual(bb, i, _) and
|
||||
read = bb.getNode(i)
|
||||
@@ -337,7 +385,7 @@ private module Cached {
|
||||
* The reference is either a read of `def` or `def` itself.
|
||||
*/
|
||||
cached
|
||||
predicate lastRefBeforeRedef(Definition def, BasicBlock bb, int i, Definition next) {
|
||||
predicate lastRefBeforeRedef(Definition def, CFG::BasicBlock bb, int i, Definition next) {
|
||||
lastRefRedefNoUncertainReads(def, bb, i, next)
|
||||
}
|
||||
|
||||
|
||||
File diff suppressed because it is too large
Load Diff
@@ -1,45 +0,0 @@
|
||||
/** Provides the Ruby specific parameters for `SsaImplCommon.qll`. */
|
||||
|
||||
private import SsaImpl as SsaImpl
|
||||
private import codeql.ruby.AST
|
||||
private import codeql.ruby.controlflow.BasicBlocks as BasicBlocks
|
||||
private import codeql.ruby.controlflow.ControlFlowGraph
|
||||
|
||||
class BasicBlock = BasicBlocks::BasicBlock;
|
||||
|
||||
BasicBlock getImmediateBasicBlockDominator(BasicBlock bb) { result = bb.getImmediateDominator() }
|
||||
|
||||
BasicBlock getABasicBlockSuccessor(BasicBlock bb) { result = bb.getASuccessor() }
|
||||
|
||||
class ExitBasicBlock = BasicBlocks::ExitBasicBlock;
|
||||
|
||||
class SourceVariable = LocalVariable;
|
||||
|
||||
/**
|
||||
* Holds if the statement at index `i` of basic block `bb` contains a write to variable `v`.
|
||||
* `certain` is true if the write definitely occurs.
|
||||
*/
|
||||
predicate variableWrite(BasicBlock bb, int i, SourceVariable v, boolean certain) {
|
||||
(
|
||||
exists(Scope scope | scope = v.(SelfVariable).getDeclaringScope() |
|
||||
// We consider the `self` variable to have a single write at the entry to a method block...
|
||||
scope = bb.(BasicBlocks::EntryBasicBlock).getScope() and
|
||||
i = 0
|
||||
or
|
||||
// ...or a class or module block.
|
||||
bb.getNode(i).getNode() = scope.(ModuleBase).getAControlFlowEntryNode()
|
||||
)
|
||||
or
|
||||
SsaImpl::uninitializedWrite(bb, i, v)
|
||||
or
|
||||
SsaImpl::capturedEntryWrite(bb, i, v)
|
||||
or
|
||||
SsaImpl::variableWriteActual(bb, i, v, _)
|
||||
) and
|
||||
certain = true
|
||||
or
|
||||
SsaImpl::capturedCallWrite(_, bb, i, v) and
|
||||
certain = false
|
||||
}
|
||||
|
||||
predicate variableRead = SsaImpl::variableRead/4;
|
||||
@@ -2,55 +2,131 @@ cached
|
||||
module Ssa {
|
||||
private import swift
|
||||
private import internal.SsaImplCommon as SsaImplCommon
|
||||
private import internal.SsaImplSpecific as SsaImplSpecific
|
||||
private import codeql.swift.controlflow.CfgNodes
|
||||
private import codeql.swift.controlflow.ControlFlowGraph
|
||||
private import codeql.swift.controlflow.BasicBlocks
|
||||
private import codeql.swift.controlflow.BasicBlocks as BasicBlocks
|
||||
|
||||
private module SsaInput implements SsaImplCommon::InputSig {
|
||||
private import internal.DataFlowPrivate
|
||||
private import codeql.swift.controlflow.ControlFlowGraph
|
||||
private import codeql.swift.controlflow.CfgNodes
|
||||
|
||||
class BasicBlock = BasicBlocks::BasicBlock;
|
||||
|
||||
BasicBlock getImmediateBasicBlockDominator(BasicBlock bb) {
|
||||
result = bb.getImmediateDominator()
|
||||
}
|
||||
|
||||
BasicBlock getABasicBlockSuccessor(BasicBlock bb) { result = bb.getASuccessor() }
|
||||
|
||||
class ExitBasicBlock = BasicBlocks::ExitBasicBlock;
|
||||
|
||||
class SourceVariable = VarDecl;
|
||||
|
||||
predicate variableWrite(BasicBlock bb, int i, SourceVariable v, boolean certain) {
|
||||
exists(AssignExpr assign |
|
||||
bb.getNode(i).getNode().asAstNode() = assign and
|
||||
assign.getDest() = v.getAnAccess() and
|
||||
certain = true
|
||||
)
|
||||
or
|
||||
exists(PatternBindingDecl decl, Pattern pattern |
|
||||
bb.getNode(i).getNode().asAstNode() = pattern and
|
||||
decl.getAPattern() = pattern and
|
||||
v.getParentPattern() = pattern and
|
||||
certain = true
|
||||
)
|
||||
or
|
||||
v instanceof ParamDecl and
|
||||
bb.getNode(i).getNode().asAstNode() = v and
|
||||
certain = true
|
||||
or
|
||||
// Mark the subexpression as a write of the local variable declared in the `TapExpr`.
|
||||
exists(TapExpr tap |
|
||||
v = tap.getVar() and
|
||||
bb.getNode(i).getNode().asAstNode() = tap.getSubExpr() and
|
||||
certain = true
|
||||
)
|
||||
}
|
||||
|
||||
predicate variableRead(BasicBlock bb, int i, SourceVariable v, boolean certain) {
|
||||
exists(DeclRefExpr ref |
|
||||
not isLValue(ref) and
|
||||
bb.getNode(i).getNode().asAstNode() = ref and
|
||||
v = ref.getDecl() and
|
||||
certain = true
|
||||
)
|
||||
or
|
||||
exists(InOutExpr expr |
|
||||
bb.getNode(i).getNode().asAstNode() = expr and
|
||||
expr.getSubExpr() = v.getAnAccess() and
|
||||
certain = true
|
||||
)
|
||||
or
|
||||
exists(ExitNode exit, AbstractFunctionDecl func |
|
||||
func.getAParam() = v or func.getSelfParam() = v
|
||||
|
|
||||
bb.getNode(i) = exit and
|
||||
modifiableParam(v) and
|
||||
bb.getScope() = func and
|
||||
certain = true
|
||||
)
|
||||
or
|
||||
// Mark the `TapExpr` as a read of the of the local variable.
|
||||
exists(TapExpr tap |
|
||||
v = tap.getVar() and
|
||||
bb.getNode(i).getNode().asAstNode() = tap and
|
||||
certain = true
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
private module SsaImpl = SsaImplCommon::Make<SsaInput>;
|
||||
|
||||
cached
|
||||
class Definition extends SsaImplCommon::Definition {
|
||||
class Definition extends SsaImpl::Definition {
|
||||
cached
|
||||
Location getLocation() { none() }
|
||||
|
||||
cached
|
||||
ControlFlowNode getARead() {
|
||||
exists(VarDecl v, BasicBlock bb, int i |
|
||||
SsaImplCommon::ssaDefReachesRead(v, this, bb, i) and
|
||||
SsaImplSpecific::variableRead(bb, i, v, true) and
|
||||
exists(VarDecl v, SsaInput::BasicBlock bb, int i |
|
||||
SsaImpl::ssaDefReachesRead(v, this, bb, i) and
|
||||
SsaInput::variableRead(bb, i, v, true) and
|
||||
result = bb.getNode(i)
|
||||
)
|
||||
}
|
||||
|
||||
cached
|
||||
ControlFlowNode getAFirstRead() {
|
||||
exists(BasicBlock bb1, int i1, BasicBlock bb2, int i2 |
|
||||
exists(SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2 |
|
||||
this.definesAt(_, bb1, i1) and
|
||||
SsaImplCommon::adjacentDefNoUncertainReads(this, bb1, i1, bb2, i2) and
|
||||
SsaImpl::adjacentDefNoUncertainReads(this, bb1, i1, bb2, i2) and
|
||||
result = bb2.getNode(i2)
|
||||
)
|
||||
}
|
||||
|
||||
cached
|
||||
predicate adjacentReadPair(ControlFlowNode read1, ControlFlowNode read2) {
|
||||
exists(BasicBlock bb1, int i1, BasicBlock bb2, int i2 |
|
||||
exists(SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2 |
|
||||
read1 = bb1.getNode(i1) and
|
||||
SsaImplSpecific::variableRead(bb1, i1, _, true) and
|
||||
SsaImplCommon::adjacentDefNoUncertainReads(this, bb1, i1, bb2, i2) and
|
||||
SsaInput::variableRead(bb1, i1, _, true) and
|
||||
SsaImpl::adjacentDefNoUncertainReads(this, bb1, i1, bb2, i2) and
|
||||
read2 = bb2.getNode(i2)
|
||||
)
|
||||
}
|
||||
|
||||
cached
|
||||
predicate lastRefRedef(BasicBlock bb, int i, Definition next) {
|
||||
SsaImplCommon::lastRefRedef(this, bb, i, next)
|
||||
predicate lastRefRedef(SsaInput::BasicBlock bb, int i, Definition next) {
|
||||
SsaImpl::lastRefRedef(this, bb, i, next)
|
||||
}
|
||||
}
|
||||
|
||||
cached
|
||||
class WriteDefinition extends Definition, SsaImplCommon::WriteDefinition {
|
||||
class WriteDefinition extends Definition, SsaImpl::WriteDefinition {
|
||||
cached
|
||||
override Location getLocation() {
|
||||
exists(BasicBlock bb, int i |
|
||||
exists(SsaInput::BasicBlock bb, int i |
|
||||
this.definesAt(_, bb, i) and
|
||||
result = bb.getNode(i).getLocation()
|
||||
)
|
||||
@@ -63,14 +139,16 @@ module Ssa {
|
||||
cached
|
||||
predicate assigns(CfgNode value) {
|
||||
exists(
|
||||
AssignExpr a, BasicBlock bb, int i // TODO: use CFG node for assignment expr
|
||||
AssignExpr a, SsaInput::BasicBlock bb, int i // TODO: use CFG node for assignment expr
|
||||
|
|
||||
this.definesAt(_, bb, i) and
|
||||
a = bb.getNode(i).getNode().asAstNode() and
|
||||
value.getNode().asAstNode() = a.getSource()
|
||||
)
|
||||
or
|
||||
exists(VarDecl var, BasicBlock bb, int blockIndex, PatternBindingDecl pbd, Expr init |
|
||||
exists(
|
||||
VarDecl var, SsaInput::BasicBlock bb, int blockIndex, PatternBindingDecl pbd, Expr init
|
||||
|
|
||||
this.definesAt(var, bb, blockIndex) and
|
||||
pbd.getAPattern() = bb.getNode(blockIndex).getNode().asAstNode() and
|
||||
init = var.getParentInitializer()
|
||||
@@ -84,17 +162,19 @@ module Ssa {
|
||||
}
|
||||
|
||||
cached
|
||||
class PhiDefinition extends Definition, SsaImplCommon::PhiNode {
|
||||
class PhiDefinition extends Definition, SsaImpl::PhiNode {
|
||||
cached
|
||||
override Location getLocation() {
|
||||
exists(BasicBlock bb, int i |
|
||||
exists(SsaInput::BasicBlock bb, int i |
|
||||
this.definesAt(_, bb, i) and
|
||||
result = bb.getLocation()
|
||||
)
|
||||
}
|
||||
|
||||
cached
|
||||
Definition getPhiInput(BasicBlock bb) { SsaImplCommon::phiHasInputFromBlock(this, result, bb) }
|
||||
Definition getPhiInput(SsaInput::BasicBlock bb) {
|
||||
SsaImpl::phiHasInputFromBlock(this, result, bb)
|
||||
}
|
||||
|
||||
cached
|
||||
Definition getAPhiInput() { result = this.getPhiInput(_) }
|
||||
|
||||
File diff suppressed because it is too large
Load Diff
@@ -1,74 +0,0 @@
|
||||
/** Provides the Swift specific parameters for `SsaImplCommon.qll`. */
|
||||
|
||||
private import swift
|
||||
private import codeql.swift.controlflow.BasicBlocks as BasicBlocks
|
||||
private import codeql.swift.controlflow.ControlFlowGraph
|
||||
private import codeql.swift.controlflow.CfgNodes
|
||||
private import DataFlowPrivate
|
||||
|
||||
class BasicBlock = BasicBlocks::BasicBlock;
|
||||
|
||||
BasicBlock getImmediateBasicBlockDominator(BasicBlock bb) { result = bb.getImmediateDominator() }
|
||||
|
||||
BasicBlock getABasicBlockSuccessor(BasicBlock bb) { result = bb.getASuccessor() }
|
||||
|
||||
class ExitBasicBlock = BasicBlocks::ExitBasicBlock;
|
||||
|
||||
class SourceVariable = VarDecl;
|
||||
|
||||
predicate variableWrite(BasicBlock bb, int i, SourceVariable v, boolean certain) {
|
||||
exists(AssignExpr assign |
|
||||
bb.getNode(i).getNode().asAstNode() = assign and
|
||||
assign.getDest() = v.getAnAccess() and
|
||||
certain = true
|
||||
)
|
||||
or
|
||||
exists(PatternBindingDecl decl, Pattern pattern |
|
||||
bb.getNode(i).getNode().asAstNode() = pattern and
|
||||
decl.getAPattern() = pattern and
|
||||
v.getParentPattern() = pattern and
|
||||
certain = true
|
||||
)
|
||||
or
|
||||
v instanceof ParamDecl and
|
||||
bb.getNode(i).getNode().asAstNode() = v and
|
||||
certain = true
|
||||
or
|
||||
// Mark the subexpression as a write of the local variable declared in the `TapExpr`.
|
||||
exists(TapExpr tap |
|
||||
v = tap.getVar() and
|
||||
bb.getNode(i).getNode().asAstNode() = tap.getSubExpr() and
|
||||
certain = true
|
||||
)
|
||||
}
|
||||
|
||||
predicate variableRead(BasicBlock bb, int i, SourceVariable v, boolean certain) {
|
||||
exists(DeclRefExpr ref |
|
||||
not isLValue(ref) and
|
||||
bb.getNode(i).getNode().asAstNode() = ref and
|
||||
v = ref.getDecl() and
|
||||
certain = true
|
||||
)
|
||||
or
|
||||
exists(InOutExpr expr |
|
||||
bb.getNode(i).getNode().asAstNode() = expr and
|
||||
expr.getSubExpr() = v.getAnAccess() and
|
||||
certain = true
|
||||
)
|
||||
or
|
||||
exists(ExitNode exit, AbstractFunctionDecl func |
|
||||
func.getAParam() = v or func.getSelfParam() = v
|
||||
|
|
||||
bb.getNode(i) = exit and
|
||||
modifiableParam(v) and
|
||||
bb.getScope() = func and
|
||||
certain = true
|
||||
)
|
||||
or
|
||||
// Mark the `TapExpr` as a read of the of the local variable.
|
||||
exists(TapExpr tap |
|
||||
v = tap.getVar() and
|
||||
bb.getNode(i).getNode().asAstNode() = tap and
|
||||
certain = true
|
||||
)
|
||||
}
|
||||
Reference in New Issue
Block a user