mirror of
https://github.com/github/codeql.git
synced 2026-04-29 18:55:14 +02:00
C++: Add shared SSA library and instantiate it with the IR.
This commit is contained in:
Mathias Vorreiter Pedersen
303
cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/Ssa.qll
Normal file
303
cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/Ssa.qll
Normal file
@@ -0,0 +1,303 @@
|
||||
import SsaImplCommon
|
||||
import SsaImplSpecific
|
||||
private import cpp as Cpp
|
||||
private import semmle.code.cpp.ir.IR
|
||||
private import DataFlowUtil
|
||||
private import DataFlowPrivate
|
||||
private import semmle.code.cpp.models.interfaces.Allocation as Alloc
|
||||
private import semmle.code.cpp.models.interfaces.DataFlow as DataFlow
|
||||
|
||||
cached
|
||||
private newtype TDefOrUse =
|
||||
TExplicitDef(Instruction store) { explicitWrite(_, store, _) } or
|
||||
TInitializeParam(Instruction instr) {
|
||||
instr instanceof InitializeParameterInstruction
|
||||
or
|
||||
instr instanceof InitializeIndirectionInstruction
|
||||
} or
|
||||
TExplicitUse(Operand op) { isExplicitUse(op) } or
|
||||
TReturnParamIndirection(Operand op) { returnParameterIndirection(op, _) }
|
||||
|
||||
pragma[nomagic]
|
||||
private int getRank(DefOrUse defOrUse, IRBlock block) {
|
||||
defOrUse =
|
||||
rank[result](int i, DefOrUse cand |
|
||||
block.getInstruction(i) = toInstruction(cand)
|
||||
|
|
||||
cand order by i
|
||||
)
|
||||
}
|
||||
|
||||
private class DefOrUse extends TDefOrUse {
|
||||
/** Gets the instruction associated with this definition, if any. */
|
||||
Instruction asDef() { none() }
|
||||
|
||||
/** Gets the operand associated with this use, if any. */
|
||||
Operand asUse() { none() }
|
||||
|
||||
/** Gets a textual representation of this element. */
|
||||
abstract string toString();
|
||||
|
||||
/** Gets the block of this definition or use. */
|
||||
abstract IRBlock getBlock();
|
||||
|
||||
/** Holds if this definition or use has rank `rank` in block `block`. */
|
||||
cached
|
||||
final predicate hasRankInBlock(IRBlock block, int rnk) {
|
||||
block = getBlock() and
|
||||
rnk = getRank(this, block)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if this element is at the specified location.
|
||||
* The location spans column `startcolumn` of line `startline` to
|
||||
* column `endcolumn` of line `endline` in file `filepath`.
|
||||
* For more information, see
|
||||
* [Locations](https://codeql.github.com/docs/writing-codeql-queries/providing-locations-in-codeql-queries/).
|
||||
*/
|
||||
abstract predicate hasLocationInfo(
|
||||
string filepath, int startline, int startcolumn, int endline, int endcolumn
|
||||
);
|
||||
}
|
||||
|
||||
private Instruction toInstruction(DefOrUse defOrUse) {
|
||||
result = defOrUse.asDef()
|
||||
or
|
||||
result = defOrUse.asUse().getUse()
|
||||
}
|
||||
|
||||
abstract class Def extends DefOrUse {
|
||||
Instruction store;
|
||||
|
||||
/** Gets the instruction of this definition. */
|
||||
Instruction getInstruction() { result = store }
|
||||
|
||||
/** Gets the variable that is defined by this definition. */
|
||||
abstract SourceVariable getVariable();
|
||||
|
||||
/** Holds if this definition is guaranteed to happen. */
|
||||
abstract predicate isCertain();
|
||||
|
||||
override Instruction asDef() { result = this.getInstruction() }
|
||||
|
||||
override string toString() { result = "Def" }
|
||||
|
||||
override IRBlock getBlock() { result = this.getInstruction().getBlock() }
|
||||
|
||||
override predicate hasLocationInfo(
|
||||
string filepath, int startline, int startcolumn, int endline, int endcolumn
|
||||
) {
|
||||
store.getLocation().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
|
||||
}
|
||||
}
|
||||
|
||||
private class ExplicitDef extends Def, TExplicitDef {
|
||||
ExplicitDef() { this = TExplicitDef(store) }
|
||||
|
||||
override SourceVariable getVariable() {
|
||||
exists(VariableInstruction var |
|
||||
explicitWrite(_, this.getInstruction(), var) and
|
||||
result.getVariable() = var.getIRVariable() and
|
||||
not result.isIndirection()
|
||||
)
|
||||
}
|
||||
|
||||
override predicate isCertain() { explicitWrite(true, this.getInstruction(), _) }
|
||||
}
|
||||
|
||||
private class ParameterDef extends Def, TInitializeParam {
|
||||
ParameterDef() { this = TInitializeParam(store) }
|
||||
|
||||
override SourceVariable getVariable() {
|
||||
result.getVariable() = store.(InitializeParameterInstruction).getIRVariable() and
|
||||
not result.isIndirection()
|
||||
or
|
||||
result.getVariable() = store.(InitializeIndirectionInstruction).getIRVariable() and
|
||||
result.isIndirection()
|
||||
}
|
||||
|
||||
override predicate isCertain() { any() }
|
||||
}
|
||||
|
||||
abstract class Use extends DefOrUse {
|
||||
Operand use;
|
||||
|
||||
override Operand asUse() { result = use }
|
||||
|
||||
/** Gets the underlying operand of this use. */
|
||||
Operand getOperand() { result = use }
|
||||
|
||||
override string toString() { result = "Use" }
|
||||
|
||||
/** Gets the variable that is used by this use. */
|
||||
abstract SourceVariable getVariable();
|
||||
|
||||
override IRBlock getBlock() { result = use.getUse().getBlock() }
|
||||
|
||||
override predicate hasLocationInfo(
|
||||
string filepath, int startline, int startcolumn, int endline, int endcolumn
|
||||
) {
|
||||
use.getLocation().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
|
||||
}
|
||||
}
|
||||
|
||||
private class ExplicitUse extends Use, TExplicitUse {
|
||||
ExplicitUse() { this = TExplicitUse(use) }
|
||||
|
||||
override SourceVariable getVariable() {
|
||||
exists(VariableInstruction var |
|
||||
use.getDef() = var and
|
||||
result.getVariable() = var.getIRVariable() and
|
||||
(
|
||||
if use.getUse() instanceof ReadSideEffectInstruction
|
||||
then result.isIndirection()
|
||||
else not result.isIndirection()
|
||||
)
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
private class ReturnParameterIndirection extends Use, TReturnParamIndirection {
|
||||
ReturnParameterIndirection() { this = TReturnParamIndirection(use) }
|
||||
|
||||
override SourceVariable getVariable() {
|
||||
exists(ReturnIndirectionInstruction ret |
|
||||
returnParameterIndirection(use, ret) and
|
||||
result.getVariable() = ret.getIRVariable() and
|
||||
result.isIndirection()
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
private predicate isExplicitUse(Operand op) {
|
||||
op.getDef() instanceof VariableAddressInstruction and
|
||||
not exists(LoadInstruction load |
|
||||
load.getSourceAddressOperand() = op and
|
||||
load.getAUse().getUse() instanceof InitializeIndirectionInstruction
|
||||
)
|
||||
}
|
||||
|
||||
private predicate returnParameterIndirection(Operand op, ReturnIndirectionInstruction ret) {
|
||||
ret.getSourceAddressOperand() = op
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `iFrom` computes an address that is used by `iTo`.
|
||||
*/
|
||||
predicate addressFlow(Instruction iFrom, Instruction iTo) {
|
||||
iTo.(CopyValueInstruction).getSourceValue() = iFrom
|
||||
or
|
||||
iTo.(ConvertInstruction).getUnary() = iFrom
|
||||
or
|
||||
iTo.(CheckedConvertOrNullInstruction).getUnary() = iFrom
|
||||
or
|
||||
iTo.(InheritanceConversionInstruction).getUnary() = iFrom
|
||||
or
|
||||
iTo.(PointerArithmeticInstruction).getLeft() = iFrom
|
||||
or
|
||||
iTo.(FieldAddressInstruction).getObjectAddress() = iFrom
|
||||
or
|
||||
iTo.(LoadInstruction).getSourceAddress() = iFrom
|
||||
or
|
||||
exists(WriteSideEffectInstruction write |
|
||||
write.getPrimaryInstruction() = iTo and
|
||||
write.getDestinationAddress() = iFrom
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* The reflexive, transitive closure of `addressFlow` that ends as the address of a
|
||||
* store or read operation.
|
||||
*/
|
||||
cached
|
||||
predicate addressFlowTC(Instruction iFrom, Instruction iTo) {
|
||||
iTo = [getDestinationAddress(_), getSourceAddress(_)] and
|
||||
addressFlow*(iFrom, iTo)
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets the destination address of `instr` if it is a `StoreInstruction` or
|
||||
* a `WriteSideEffectInstruction`. The destination address of a `WriteSideEffectInstruction` is adjusted
|
||||
* in the case of calls to operator `new` to give the destination address of a subsequent store (if any).
|
||||
*/
|
||||
Instruction getDestinationAddress(Instruction instr) {
|
||||
result =
|
||||
[
|
||||
instr.(StoreInstruction).getDestinationAddress(),
|
||||
instr.(WriteSideEffectInstruction).getDestinationAddress()
|
||||
]
|
||||
}
|
||||
|
||||
class ReferenceToInstruction extends CopyValueInstruction {
|
||||
ReferenceToInstruction() {
|
||||
this.getResultType() instanceof Cpp::ReferenceType and
|
||||
not this.getUnary().getResultType() instanceof Cpp::ReferenceType
|
||||
}
|
||||
|
||||
Instruction getSourceAddress() { result = getSourceAddressOperand().getDef() }
|
||||
|
||||
Operand getSourceAddressOperand() { result = this.getUnaryOperand() }
|
||||
}
|
||||
|
||||
/** Gets the source address of `instr` if it is an instruction that behaves like a `LoadInstruction`. */
|
||||
Instruction getSourceAddress(Instruction instr) { result = getSourceAddressOperand(instr).getDef() }
|
||||
|
||||
/**
|
||||
* Gets the operand that represents the source address of `instr` if it is an
|
||||
* instruction that behaves like a `LoadInstruction`.
|
||||
*/
|
||||
Operand getSourceAddressOperand(Instruction instr) {
|
||||
result =
|
||||
[
|
||||
instr.(LoadInstruction).getSourceAddressOperand(),
|
||||
instr.(ReadSideEffectInstruction).getArgumentOperand(),
|
||||
instr.(ReferenceToInstruction).getSourceAddressOperand()
|
||||
]
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets the source address of `node` if it's an instruction or operand that
|
||||
* behaves like a `LoadInstruction`.
|
||||
*/
|
||||
Instruction getSourceAddressFromNode(Node node) {
|
||||
result = getSourceAddress(node.asInstruction())
|
||||
or
|
||||
result = getSourceAddress(node.asOperand().(SideEffectOperand).getUse())
|
||||
}
|
||||
|
||||
/** Gets the source value of `instr` if it's an instruction that behaves like a `LoadInstruction`. */
|
||||
Instruction getSourceValue(Instruction instr) { result = getSourceValueOperand(instr).getDef() }
|
||||
|
||||
/**
|
||||
* Gets the operand that represents the source value of `instr` if it's an instruction
|
||||
* that behaves like a `LoadInstruction`.
|
||||
*/
|
||||
Operand getSourceValueOperand(Instruction instr) {
|
||||
result = instr.(LoadInstruction).getSourceValueOperand()
|
||||
or
|
||||
result = instr.(ReadSideEffectInstruction).getSideEffectOperand()
|
||||
or
|
||||
result = instr.(ReferenceToInstruction).getSourceValueOperand()
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `instr` is a `StoreInstruction` or a `WriteSideEffectInstruction` that writes to an address.
|
||||
* The addresses is computed using `address`, and `certain` is `true` if the write is guaranteed to overwrite
|
||||
* the entire variable.
|
||||
*/
|
||||
cached
|
||||
predicate explicitWrite(boolean certain, Instruction instr, Instruction address) {
|
||||
exists(StoreInstruction store |
|
||||
store = instr and addressFlowTC(address, store.getDestinationAddress())
|
||||
|
|
||||
if
|
||||
addressFlowTC(any(Instruction i |
|
||||
i instanceof FieldAddressInstruction or i instanceof PointerArithmeticInstruction
|
||||
), store.getDestinationAddress())
|
||||
then certain = false
|
||||
else certain = true
|
||||
)
|
||||
or
|
||||
addressFlowTC(address, instr.(WriteSideEffectInstruction).getDestinationAddress()) and
|
||||
certain = false
|
||||
}
|
||||
@@ -0,0 +1,637 @@
|
||||
/**
|
||||
* 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`.
|
||||
*/
|
||||
private predicate ref(BasicBlock bb, int i, SourceVariable v, RefKind k) {
|
||||
exists(boolean certain | variableRead(bb, i, v, certain) | k = Read(certain))
|
||||
or
|
||||
exists(boolean certain | variableWrite(bb, i, v, certain) | k = Write(certain))
|
||||
}
|
||||
|
||||
private newtype OrderedRefIndex =
|
||||
MkOrderedRefIndex(int i, int tag) {
|
||||
exists(RefKind rk | ref(_, i, _, rk) | tag = rk.getOrder())
|
||||
}
|
||||
|
||||
private OrderedRefIndex refOrd(BasicBlock bb, int i, SourceVariable v, RefKind k, int ord) {
|
||||
ref(bb, i, v, k) and
|
||||
result = MkOrderedRefIndex(i, ord) and
|
||||
ord = k.getOrder()
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets the (1-based) rank of the reference to `v` at the `i`th node of
|
||||
* basic block `bb`, which has the given reference kind `k`.
|
||||
*
|
||||
* Reads are considered before writes when they happen at the same index.
|
||||
*/
|
||||
private int refRank(BasicBlock bb, int i, SourceVariable v, RefKind k) {
|
||||
refOrd(bb, i, v, k, _) =
|
||||
rank[result](int j, int ord, OrderedRefIndex res |
|
||||
res = refOrd(bb, j, v, _, ord)
|
||||
|
|
||||
res order by j, ord
|
||||
)
|
||||
}
|
||||
|
||||
private int maxRefRank(BasicBlock bb, SourceVariable v) {
|
||||
result = refRank(bb, _, v, _) and
|
||||
not result + 1 = refRank(bb, _, v, _)
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets the (1-based) rank of the first reference to `v` inside basic block `bb`
|
||||
* that is either a read or a certain write.
|
||||
*/
|
||||
private int firstReadOrCertainWrite(BasicBlock bb, SourceVariable v) {
|
||||
result =
|
||||
min(int r, RefKind k |
|
||||
r = refRank(bb, _, v, k) and
|
||||
k != Write(false)
|
||||
|
|
||||
r
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if source variable `v` is live at the beginning of basic block `bb`.
|
||||
*/
|
||||
predicate liveAtEntry(BasicBlock bb, SourceVariable v) {
|
||||
// The first read or certain write to `v` inside `bb` is a read
|
||||
refRank(bb, _, v, Read(_)) = firstReadOrCertainWrite(bb, v)
|
||||
or
|
||||
// There is no certain write to `v` inside `bb`, but `v` is live at entry
|
||||
// to a successor basic block of `bb`
|
||||
not exists(firstReadOrCertainWrite(bb, v)) and
|
||||
liveAtExit(bb, v)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if source variable `v` is live at the end of basic block `bb`.
|
||||
*/
|
||||
predicate liveAtExit(BasicBlock bb, SourceVariable v) {
|
||||
liveAtEntry(getABasicBlockSuccessor(bb), v)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if variable `v` is live in basic block `bb` at index `i`.
|
||||
* The rank of `i` is `rnk` as defined by `refRank()`.
|
||||
*/
|
||||
private predicate liveAtRank(BasicBlock bb, int i, SourceVariable v, int rnk) {
|
||||
exists(RefKind kind | rnk = refRank(bb, i, v, kind) |
|
||||
rnk = maxRefRank(bb, v) and
|
||||
liveAtExit(bb, v)
|
||||
or
|
||||
ref(bb, i, v, kind) and
|
||||
kind = Read(_)
|
||||
or
|
||||
exists(RefKind nextKind |
|
||||
liveAtRank(bb, _, v, rnk + 1) and
|
||||
rnk + 1 = refRank(bb, _, v, nextKind) and
|
||||
nextKind != Write(true)
|
||||
)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if variable `v` is live after the (certain or uncertain) write at
|
||||
* index `i` inside basic block `bb`.
|
||||
*/
|
||||
predicate liveAfterWrite(BasicBlock bb, int i, SourceVariable v) {
|
||||
exists(int rnk | rnk = refRank(bb, i, v, Write(_)) | liveAtRank(bb, i, v, rnk))
|
||||
}
|
||||
}
|
||||
|
||||
private import Liveness
|
||||
|
||||
/** Holds if `bb1` strictly dominates `bb2`. */
|
||||
private predicate strictlyDominates(BasicBlock bb1, BasicBlock bb2) {
|
||||
bb1 = getImmediateBasicBlockDominator+(bb2)
|
||||
}
|
||||
|
||||
/** Holds if `bb1` dominates a predecessor of `bb2`. */
|
||||
private predicate dominatesPredecessor(BasicBlock bb1, BasicBlock bb2) {
|
||||
exists(BasicBlock pred | pred = getABasicBlockPredecessor(bb2) |
|
||||
bb1 = pred
|
||||
or
|
||||
strictlyDominates(bb1, pred)
|
||||
)
|
||||
}
|
||||
|
||||
/** Holds if `df` is in the dominance frontier of `bb`. */
|
||||
private predicate inDominanceFrontier(BasicBlock bb, BasicBlock df) {
|
||||
dominatesPredecessor(bb, df) and
|
||||
not strictlyDominates(bb, df)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `bb` is in the dominance frontier of a block containing a
|
||||
* definition of `v`.
|
||||
*/
|
||||
pragma[noinline]
|
||||
private predicate inDefDominanceFrontier(BasicBlock bb, SourceVariable v) {
|
||||
exists(BasicBlock defbb, Definition def |
|
||||
def.definesAt(v, defbb, _) and
|
||||
inDominanceFrontier(defbb, bb)
|
||||
)
|
||||
}
|
||||
|
||||
cached
|
||||
newtype TDefinition =
|
||||
TWriteDef(SourceVariable v, BasicBlock bb, int i) {
|
||||
variableWrite(bb, i, v, _) and
|
||||
liveAfterWrite(bb, i, v)
|
||||
} or
|
||||
TPhiNode(SourceVariable v, BasicBlock bb) {
|
||||
inDefDominanceFrontier(bb, v) and
|
||||
liveAtEntry(bb, v)
|
||||
}
|
||||
|
||||
private module SsaDefReaches {
|
||||
newtype TSsaRefKind =
|
||||
SsaRead() or
|
||||
SsaDef()
|
||||
|
||||
/**
|
||||
* A classification of SSA variable references into reads and definitions.
|
||||
*/
|
||||
class SsaRefKind extends TSsaRefKind {
|
||||
string toString() {
|
||||
this = SsaRead() and
|
||||
result = "SsaRead"
|
||||
or
|
||||
this = SsaDef() and
|
||||
result = "SsaDef"
|
||||
}
|
||||
|
||||
int getOrder() {
|
||||
this = SsaRead() and
|
||||
result = 0
|
||||
or
|
||||
this = SsaDef() and
|
||||
result = 1
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the `i`th node of basic block `bb` is a reference to `v`,
|
||||
* either a read (when `k` is `SsaRead()`) or an SSA definition (when `k`
|
||||
* is `SsaDef()`).
|
||||
*
|
||||
* Unlike `Liveness::ref`, this includes `phi` nodes.
|
||||
*/
|
||||
predicate ssaRef(BasicBlock bb, int i, SourceVariable v, SsaRefKind k) {
|
||||
variableRead(bb, i, v, _) and
|
||||
k = SsaRead()
|
||||
or
|
||||
exists(Definition def | def.definesAt(v, bb, i)) and
|
||||
k = SsaDef()
|
||||
}
|
||||
|
||||
private newtype OrderedSsaRefIndex =
|
||||
MkOrderedSsaRefIndex(int i, SsaRefKind k) { ssaRef(_, i, _, k) }
|
||||
|
||||
private OrderedSsaRefIndex ssaRefOrd(BasicBlock bb, int i, SourceVariable v, SsaRefKind k, int ord) {
|
||||
ssaRef(bb, i, v, k) and
|
||||
result = MkOrderedSsaRefIndex(i, k) and
|
||||
ord = k.getOrder()
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets the (1-based) rank of the reference to `v` at the `i`th node of basic
|
||||
* block `bb`, which has the given reference kind `k`.
|
||||
*
|
||||
* For example, if `bb` is a basic block with a phi node for `v` (considered
|
||||
* to be at index -1), reads `v` at node 2, and defines it at node 5, we have:
|
||||
*
|
||||
* ```ql
|
||||
* ssaRefRank(bb, -1, v, SsaDef()) = 1 // phi node
|
||||
* ssaRefRank(bb, 2, v, Read()) = 2 // read at node 2
|
||||
* ssaRefRank(bb, 5, v, SsaDef()) = 3 // definition at node 5
|
||||
* ```
|
||||
*
|
||||
* Reads are considered before writes when they happen at the same index.
|
||||
*/
|
||||
int ssaRefRank(BasicBlock bb, int i, SourceVariable v, SsaRefKind k) {
|
||||
ssaRefOrd(bb, i, v, k, _) =
|
||||
rank[result](int j, int ord, OrderedSsaRefIndex res |
|
||||
res = ssaRefOrd(bb, j, v, _, ord)
|
||||
|
|
||||
res order by j, ord
|
||||
)
|
||||
}
|
||||
|
||||
int maxSsaRefRank(BasicBlock bb, SourceVariable v) {
|
||||
result = ssaRefRank(bb, _, v, _) and
|
||||
not result + 1 = ssaRefRank(bb, _, v, _)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the SSA definition `def` reaches rank index `rnk` in its own
|
||||
* basic block `bb`.
|
||||
*/
|
||||
predicate ssaDefReachesRank(BasicBlock bb, Definition def, int rnk, SourceVariable v) {
|
||||
exists(int i |
|
||||
rnk = ssaRefRank(bb, i, v, SsaDef()) and
|
||||
def.definesAt(v, bb, i)
|
||||
)
|
||||
or
|
||||
ssaDefReachesRank(bb, def, rnk - 1, v) and
|
||||
rnk = ssaRefRank(bb, _, v, SsaRead())
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the SSA definition of `v` at `def` reaches index `i` in the same
|
||||
* basic block `bb`, without crossing another SSA definition of `v`.
|
||||
*/
|
||||
predicate ssaDefReachesReadWithinBlock(SourceVariable v, Definition def, BasicBlock bb, int i) {
|
||||
exists(int rnk |
|
||||
ssaDefReachesRank(bb, def, rnk, v) and
|
||||
rnk = ssaRefRank(bb, i, v, SsaRead())
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the SSA definition of `v` at `def` reaches uncertain SSA definition
|
||||
* `redef` in the same basic block, without crossing another SSA definition of `v`.
|
||||
*/
|
||||
predicate ssaDefReachesUncertainDefWithinBlock(
|
||||
SourceVariable v, Definition def, UncertainWriteDefinition redef
|
||||
) {
|
||||
exists(BasicBlock bb, int rnk, int i |
|
||||
ssaDefReachesRank(bb, def, rnk, v) and
|
||||
rnk = ssaRefRank(bb, i, v, SsaDef()) - 1 and
|
||||
redef.definesAt(v, bb, i)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Same as `ssaRefRank()`, but restricted to a particular SSA definition `def`.
|
||||
*/
|
||||
int ssaDefRank(Definition def, SourceVariable v, BasicBlock bb, int i, SsaRefKind k) {
|
||||
v = def.getSourceVariable() and
|
||||
result = ssaRefRank(bb, i, v, k) and
|
||||
(
|
||||
ssaDefReachesRead(_, def, bb, i)
|
||||
or
|
||||
def.definesAt(_, bb, i)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* 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) {
|
||||
exists(ssaDefRank(def, v, bb, _, _))
|
||||
}
|
||||
|
||||
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 `bb1`,
|
||||
* and the underlying variable for `def` is neither read nor written in any block
|
||||
* on the path between `bb1` and `bb2`.
|
||||
*/
|
||||
predicate varBlockReaches(Definition def, BasicBlock bb1, BasicBlock bb2) {
|
||||
defOccursInBlock(def, bb1, _) and
|
||||
bb2 = getABasicBlockSuccessor(bb1)
|
||||
or
|
||||
exists(BasicBlock mid |
|
||||
varBlockReaches(def, bb1, mid) and
|
||||
ssaDefReachesThroughBlock(def, mid) and
|
||||
bb2 = getABasicBlockSuccessor(mid)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `def` is accessed in basic block `bb1` (either a read or a write),
|
||||
* `def` is read at index `i2` in basic block `bb2`, `bb2` is in a transitive
|
||||
* successor block of `bb1`, and `def` is neither read nor written in any block
|
||||
* on a path between `bb1` and `bb2`.
|
||||
*/
|
||||
predicate defAdjacentRead(Definition def, BasicBlock bb1, BasicBlock bb2, int i2) {
|
||||
varBlockReaches(def, bb1, bb2) and
|
||||
ssaRefRank(bb2, i2, def.getSourceVariable(), SsaRead()) = 1
|
||||
}
|
||||
}
|
||||
|
||||
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(bb, v) |
|
||||
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
|
||||
variableRead(bb, i, v, _) and
|
||||
ssaDefReachesEndOfBlock(getABasicBlockPredecessor(bb), def, v) and
|
||||
not ssaDefReachesReadWithinBlock(v, _, bb, i)
|
||||
}
|
||||
|
||||
/**
|
||||
* NB: If this predicate is exposed, it should be cached.
|
||||
*
|
||||
* Holds if `def` is accessed at index `i1` in basic block `bb1` (either a read
|
||||
* or a write), `def` is read at index `i2` in basic block `bb2`, and there is a
|
||||
* path between them without any read of `def`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate adjacentDefRead(Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2) {
|
||||
exists(int rnk |
|
||||
rnk = ssaDefRank(def, _, bb1, i1, _) and
|
||||
rnk + 1 = ssaDefRank(def, _, bb1, i2, SsaRead()) and
|
||||
variableRead(bb1, i2, _, _) and
|
||||
bb2 = bb1
|
||||
)
|
||||
or
|
||||
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) {
|
||||
lastRefRedef(def, bb, i, _)
|
||||
or
|
||||
lastSsaRef(def, _, bb, i) and
|
||||
(
|
||||
// Can reach exit directly
|
||||
bb instanceof ExitBasicBlock
|
||||
or
|
||||
// Can reach a block using one or more steps, where `def` is no longer live
|
||||
exists(BasicBlock bb2 | varBlockReaches(def, bb, bb2) |
|
||||
not defOccursInBlock(def, bb2, _) and
|
||||
not ssaDefReachesEndOfBlock(bb2, def, _)
|
||||
)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* NB: If this predicate is exposed, it should be cached.
|
||||
*
|
||||
* Same as `lastRefRedef`, but ignores uncertain reads.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate lastRefNoUncertainReads(Definition def, BasicBlock bb, int i) {
|
||||
lastRef(def, bb, i) and
|
||||
not variableRead(bb, i, def.getSourceVariable(), false)
|
||||
or
|
||||
exists(BasicBlock bb0, int i0 |
|
||||
lastRef(def, bb0, i0) and
|
||||
adjacentDefReachesUncertainRead(def, bb, i, bb0, i0)
|
||||
)
|
||||
}
|
||||
|
||||
/** A static single assignment (SSA) definition. */
|
||||
class Definition extends TDefinition {
|
||||
/** Gets the source variable underlying this SSA definition. */
|
||||
SourceVariable getSourceVariable() { this.definesAt(result, _, _) }
|
||||
|
||||
/**
|
||||
* Holds if this SSA definition defines `v` at index `i` in basic block `bb`.
|
||||
* Phi nodes are considered to be at index `-1`, while normal variable writes
|
||||
* are at the index of the control flow node they wrap.
|
||||
*/
|
||||
final predicate definesAt(SourceVariable v, BasicBlock bb, int i) {
|
||||
this = TWriteDef(v, bb, i)
|
||||
or
|
||||
this = TPhiNode(v, bb) and i = -1
|
||||
}
|
||||
|
||||
/** Gets the basic block to which this SSA definition belongs. */
|
||||
final BasicBlock getBasicBlock() { this.definesAt(_, result, _) }
|
||||
|
||||
/** Gets a textual representation of this SSA definition. */
|
||||
string toString() { none() }
|
||||
}
|
||||
|
||||
/** An SSA definition that corresponds to a write. */
|
||||
class WriteDefinition extends Definition, TWriteDef {
|
||||
private SourceVariable v;
|
||||
private BasicBlock bb;
|
||||
private int i;
|
||||
|
||||
WriteDefinition() { this = TWriteDef(v, bb, i) }
|
||||
|
||||
override string toString() { result = "WriteDef" }
|
||||
}
|
||||
|
||||
/** A phi node. */
|
||||
class PhiNode extends Definition, TPhiNode {
|
||||
override string toString() { result = "Phi" }
|
||||
}
|
||||
|
||||
/**
|
||||
* An SSA definition that represents an uncertain update of the underlying
|
||||
* source variable.
|
||||
*/
|
||||
class UncertainWriteDefinition extends WriteDefinition {
|
||||
UncertainWriteDefinition() {
|
||||
exists(SourceVariable v, BasicBlock bb, int i |
|
||||
this.definesAt(v, bb, i) and
|
||||
variableWrite(bb, i, v, false)
|
||||
)
|
||||
}
|
||||
}
|
||||
@@ -0,0 +1,64 @@
|
||||
private import semmle.code.cpp.ir.IR
|
||||
private import DataFlowUtil
|
||||
private import DataFlowPrivate
|
||||
private import DataFlowImplCommon as DataFlowImplCommon
|
||||
private import Ssa as Ssa
|
||||
|
||||
class BasicBlock = IRBlock;
|
||||
|
||||
BasicBlock getImmediateBasicBlockDominator(BasicBlock bb) { result.immediatelyDominates(bb) }
|
||||
|
||||
BasicBlock getABasicBlockSuccessor(BasicBlock bb) { result = bb.getASuccessor() }
|
||||
|
||||
class ExitBasicBlock extends IRBlock {
|
||||
ExitBasicBlock() { this.getLastInstruction() instanceof ExitFunctionInstruction }
|
||||
}
|
||||
|
||||
private newtype TSourceVariable =
|
||||
TSourceIRVariable(IRVariable var) or
|
||||
TSourceIRVariableIndirection(InitializeIndirectionInstruction init)
|
||||
|
||||
abstract class SourceVariable extends TSourceVariable {
|
||||
IRVariable var;
|
||||
|
||||
IRVariable getVariable() { result = var }
|
||||
|
||||
abstract string toString();
|
||||
|
||||
predicate isIndirection() { none() }
|
||||
}
|
||||
|
||||
class SourceIRVariable extends SourceVariable, TSourceIRVariable {
|
||||
SourceIRVariable() { this = TSourceIRVariable(var) }
|
||||
|
||||
override string toString() { result = this.getVariable().toString() }
|
||||
}
|
||||
|
||||
class SourceIRVariableIndirection extends SourceVariable, TSourceIRVariableIndirection {
|
||||
InitializeIndirectionInstruction init;
|
||||
|
||||
SourceIRVariableIndirection() {
|
||||
this = TSourceIRVariableIndirection(init) and var = init.getIRVariable()
|
||||
}
|
||||
|
||||
override string toString() { result = "*" + this.getVariable().toString() }
|
||||
|
||||
override predicate isIndirection() { any() }
|
||||
}
|
||||
|
||||
predicate variableWrite(BasicBlock bb, int i, SourceVariable v, boolean certain) {
|
||||
DataFlowImplCommon::forceCachingInSameStage() and
|
||||
exists(Ssa::Def def |
|
||||
def.hasRankInBlock(bb, i) and
|
||||
v = def.getVariable() and
|
||||
(if def.isCertain() then certain = true else certain = false)
|
||||
)
|
||||
}
|
||||
|
||||
predicate variableRead(BasicBlock bb, int i, SourceVariable v, boolean certain) {
|
||||
exists(Ssa::Use use |
|
||||
use.hasRankInBlock(bb, i) and
|
||||
v = use.getVariable() and
|
||||
certain = true
|
||||
)
|
||||
}
|
||||
Reference in New Issue
Block a user