зеркало из https://github.com/github/codeql.git
SSA: Expose phi-reads
This commit is contained in:
Tom Hvitved
Родитель
32f60fd112
Коммит
81a1fa167a
|
|
@ -264,8 +264,22 @@ module Make<InputSig Input> {
|
|||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* 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
|
||||
exists(TPhiReadNode(v, readbb)) and
|
||||
not ref(readbb, _, v, _)
|
||||
)
|
||||
}
|
||||
|
||||
cached
|
||||
newtype TDefinition =
|
||||
private newtype TDefinitionExt =
|
||||
TWriteDef(SourceVariable v, BasicBlock bb, int i) {
|
||||
variableWrite(bb, i, v, _) and
|
||||
liveAfterWrite(bb, i, v)
|
||||
|
|
@ -273,8 +287,16 @@ module Make<InputSig Input> {
|
|||
TPhiNode(SourceVariable v, BasicBlock bb) {
|
||||
inDefDominanceFrontier(bb, v) and
|
||||
liveAtEntry(bb, v)
|
||||
} or
|
||||
TPhiReadNode(SourceVariable v, BasicBlock bb) {
|
||||
inReadDominanceFrontier(bb, v) and
|
||||
liveAtEntry(bb, v) and
|
||||
// no need to create a phi-read if there is already a normal phi
|
||||
not any(PhiNode def).definesAt(v, bb, _)
|
||||
}
|
||||
|
||||
private class TDefinition = TWriteDef or TPhiNode;
|
||||
|
||||
private module SsaDefReaches {
|
||||
newtype TSsaRefKind =
|
||||
SsaActualRead() or
|
||||
|
|
@ -283,6 +305,10 @@ module Make<InputSig Input> {
|
|||
|
||||
class SsaRead = SsaActualRead or SsaPhiRead;
|
||||
|
||||
class SsaDefExt = SsaDef or SsaPhiRead;
|
||||
|
||||
SsaDefExt ssaDefExt() { any() }
|
||||
|
||||
/**
|
||||
* A classification of SSA variable references into reads and definitions.
|
||||
*/
|
||||
|
|
@ -307,98 +333,27 @@ module Make<InputSig Input> {
|
|||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* 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()`).
|
||||
* either a read (when `k` is `SsaActualRead()`), an SSA definition (when `k`
|
||||
* is `SsaDef()`), or a phi-read (when `k` is `SsaPhiRead()`).
|
||||
*
|
||||
* Unlike `Liveness::ref`, this includes `phi` nodes.
|
||||
* Unlike `Liveness::ref`, this includes `phi` (read) 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()
|
||||
any(DefinitionExt def).definesAt(v, bb, i, k)
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if the `i`th node of basic block `bb` is a reference to `v`, and
|
||||
* this reference is not a phi-read.
|
||||
*/
|
||||
predicate ssaRefNonPhiRead(BasicBlock bb, int i, SourceVariable v) {
|
||||
ssaRef(bb, i, v, [SsaActualRead().(TSsaRefKind), SsaDef()])
|
||||
}
|
||||
|
||||
private newtype OrderedSsaRefIndex =
|
||||
|
|
@ -445,37 +400,36 @@ module Make<InputSig Input> {
|
|||
* 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) {
|
||||
predicate ssaDefReachesRank(BasicBlock bb, DefinitionExt def, int rnk, SourceVariable v) {
|
||||
exists(int i |
|
||||
rnk = ssaRefRank(bb, i, v, SsaDef()) and
|
||||
def.definesAt(v, bb, i)
|
||||
rnk = ssaRefRank(bb, i, v, ssaDefExt()) and
|
||||
def.definesAt(v, bb, i, _)
|
||||
)
|
||||
or
|
||||
ssaDefReachesRank(bb, def, rnk - 1, v) and
|
||||
rnk = ssaRefRank(bb, _, v, any(SsaRead k))
|
||||
rnk = ssaRefRank(bb, _, v, SsaActualRead())
|
||||
}
|
||||
|
||||
/**
|
||||
* 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) {
|
||||
predicate ssaDefReachesReadWithinBlock(SourceVariable v, DefinitionExt def, BasicBlock bb, int i) {
|
||||
exists(int rnk |
|
||||
ssaDefReachesRank(bb, def, rnk, v) and
|
||||
rnk = ssaRefRank(bb, i, v, any(SsaRead k))
|
||||
rnk = ssaRefRank(bb, i, v, SsaActualRead())
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* 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
|
||||
int ssaDefRank(DefinitionExt def, SourceVariable v, BasicBlock bb, int i, SsaRefKind k) {
|
||||
result = ssaRefRank(bb, i, v, k) and
|
||||
(
|
||||
ssaDefReachesRead(_, def, bb, i)
|
||||
ssaDefReachesReadExt(v, def, bb, i)
|
||||
or
|
||||
def.definesAt(_, bb, i)
|
||||
def.definesAt(v, bb, i, k)
|
||||
)
|
||||
}
|
||||
|
||||
|
|
@ -484,18 +438,38 @@ module Make<InputSig Input> {
|
|||
* last reference to `v` inside `bb`.
|
||||
*/
|
||||
pragma[noinline]
|
||||
predicate lastSsaRef(Definition def, SourceVariable v, BasicBlock bb, int i) {
|
||||
predicate lastSsaRefExt(DefinitionExt 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) {
|
||||
/** Gets a phi-read node into which `inp` is an input, if any. */
|
||||
pragma[nomagic]
|
||||
private DefinitionExt getAPhiReadOutput(DefinitionExt inp) {
|
||||
phiHasInputFromBlockExt(result.(PhiReadNode), inp, _)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
DefinitionExt getAnUltimateOutput(Definition def) { result = getAPhiReadOutput*(def) }
|
||||
|
||||
/**
|
||||
* Same as `lastSsaRefExt`, but ignores phi-reads.
|
||||
*/
|
||||
pragma[noinline]
|
||||
predicate lastSsaRef(Definition def, SourceVariable v, BasicBlock bb, int i) {
|
||||
lastSsaRefExt(getAnUltimateOutput(def), v, bb, i) and
|
||||
ssaRefNonPhiRead(bb, i, v)
|
||||
}
|
||||
|
||||
predicate defOccursInBlock(DefinitionExt 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(), _)
|
||||
private predicate ssaDefReachesThroughBlock(DefinitionExt def, BasicBlock bb) {
|
||||
exists(SourceVariable v |
|
||||
ssaDefReachesEndOfBlockExt(bb, def, v) and
|
||||
not defOccursInBlock(_, bb, v, _)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
@ -503,85 +477,114 @@ module Make<InputSig Input> {
|
|||
* `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
|
||||
predicate varBlockReachesExt(DefinitionExt def, SourceVariable v, BasicBlock bb1, BasicBlock bb2) {
|
||||
defOccursInBlock(def, bb1, v, _) and
|
||||
bb2 = getABasicBlockSuccessor(bb1)
|
||||
or
|
||||
exists(BasicBlock mid |
|
||||
varBlockReachesInclPhiRead(def, bb1, mid) and
|
||||
varBlockReachesExt(def, v, 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())
|
||||
private predicate phiReadStep(DefinitionExt def, PhiReadNode phi, BasicBlock bb1, BasicBlock bb2) {
|
||||
exists(SourceVariable v |
|
||||
varBlockReachesExt(pragma[only_bind_into](def), v, bb1, pragma[only_bind_into](bb2)) and
|
||||
phi.definesAt(v, bb2, _, _) and
|
||||
not ref(bb2, _, v, _)
|
||||
)
|
||||
}
|
||||
|
||||
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()])
|
||||
private predicate varBlockReachesExclPhiRead(
|
||||
DefinitionExt def, SourceVariable v, BasicBlock bb1, BasicBlock bb2
|
||||
) {
|
||||
varBlockReachesExt(def, v, bb1, bb2) and
|
||||
ssaRefNonPhiRead(bb2, _, v)
|
||||
or
|
||||
exists(BasicBlock mid |
|
||||
varBlockReachesExclPhiRead(def, mid, bb2) and
|
||||
phiReadStep(def, _, bb1, mid)
|
||||
exists(PhiReadNode phi, BasicBlock mid |
|
||||
varBlockReachesExclPhiRead(phi, v, mid, bb2) and
|
||||
phiReadStep(def, phi, 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`.
|
||||
* Same as `varBlockReachesExt`, but ignores phi-reads, and furthermore
|
||||
* `bb2` is restricted to blocks in which the underlying variable `v` of
|
||||
* `def` is referenced (either a read or a write).
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate varBlockReaches(Definition def, BasicBlock bb1, BasicBlock bb2) {
|
||||
varBlockReachesExclPhiRead(def, bb1, bb2) and
|
||||
not defOccursInBlock(def, bb1, _, SsaPhiRead())
|
||||
predicate varBlockReachesRef(Definition def, SourceVariable v, BasicBlock bb1, BasicBlock bb2) {
|
||||
varBlockReachesExclPhiRead(getAnUltimateOutput(def), v, bb1, bb2) and
|
||||
ssaRefNonPhiRead(bb1, _, v)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
predicate defAdjacentReadExt(DefinitionExt def, BasicBlock bb1, BasicBlock bb2, int i2) {
|
||||
exists(SourceVariable v |
|
||||
varBlockReachesExt(def, v, bb1, bb2) and
|
||||
ssaRefRank(bb2, i2, v, SsaActualRead()) = 1
|
||||
)
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
predicate defAdjacentRead(Definition def, BasicBlock bb1, BasicBlock bb2, int i2) {
|
||||
varBlockReaches(def, bb1, bb2) and
|
||||
ssaRefRank(bb2, i2, def.getSourceVariable(), SsaActualRead()) = 1
|
||||
exists(SourceVariable v | varBlockReachesRef(def, v, bb1, bb2) |
|
||||
ssaRefRank(bb2, i2, v, SsaActualRead()) = 1
|
||||
or
|
||||
ssaRefRank(bb2, _, v, SsaPhiRead()) = 1 and
|
||||
ssaRefRank(bb2, i2, v, SsaActualRead()) = 2
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* 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,
|
||||
* `bb` 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) |
|
||||
predicate varBlockReachesExitExt(DefinitionExt def, BasicBlock bb) {
|
||||
exists(BasicBlock bb2 | varBlockReachesExt(def, _, bb, bb2) |
|
||||
not defOccursInBlock(def, bb2, _, _) and
|
||||
not ssaDefReachesEndOfBlock(bb2, def, _)
|
||||
)
|
||||
or
|
||||
exists(BasicBlock mid |
|
||||
varBlockReachesExit(def, mid) and
|
||||
phiReadStep(def, _, bb, mid)
|
||||
not ssaDefReachesEndOfBlockExt(bb2, def, _)
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
predicate phiReadExposedForTesting = phiRead/2;
|
||||
pragma[nomagic]
|
||||
private predicate varBlockReachesExitExclPhiRead(DefinitionExt def, BasicBlock bb) {
|
||||
exists(BasicBlock bb2, SourceVariable v |
|
||||
varBlockReachesExt(def, v, bb, bb2) and
|
||||
not defOccursInBlock(def, bb2, _, _) and
|
||||
not ssaDefReachesEndOfBlockExt(bb2, def, _) and
|
||||
not any(PhiReadNode phi).definesAt(v, bb2, _, _)
|
||||
)
|
||||
or
|
||||
exists(PhiReadNode phi, BasicBlock bb2 |
|
||||
varBlockReachesExitExclPhiRead(phi, bb2) and
|
||||
phiReadStep(def, phi, bb, bb2)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* Same as `varBlockReachesExitExt`, but ignores phi-reads.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate varBlockReachesExit(Definition def, BasicBlock bb) {
|
||||
varBlockReachesExitExclPhiRead(getAnUltimateOutput(def), bb)
|
||||
}
|
||||
}
|
||||
|
||||
private import SsaDefReaches
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate liveThrough(BasicBlock bb, SourceVariable v) {
|
||||
private predicate liveThroughExt(BasicBlock bb, SourceVariable v) {
|
||||
liveAtExit(bb, v) and
|
||||
not ssaRef(bb, _, v, SsaDef())
|
||||
not ssaRef(bb, _, v, ssaDefExt())
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
@ -592,7 +595,7 @@ module Make<InputSig Input> {
|
|||
* SSA definition of `v`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate ssaDefReachesEndOfBlock(BasicBlock bb, Definition def, SourceVariable v) {
|
||||
predicate ssaDefReachesEndOfBlockExt(BasicBlock bb, DefinitionExt 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
|
||||
|
|
@ -605,8 +608,31 @@ module Make<InputSig Input> {
|
|||
// 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))
|
||||
ssaDefReachesEndOfBlockExt(getImmediateBasicBlockDominator(bb), def, pragma[only_bind_into](v)) and
|
||||
liveThroughExt(bb, pragma[only_bind_into](v))
|
||||
}
|
||||
|
||||
pragma[nomagic]
|
||||
private predicate phiReadReachesEndOfBlock(BasicBlock pred, BasicBlock bb, SourceVariable v) {
|
||||
exists(PhiReadNode phi |
|
||||
ssaDefReachesEndOfBlockExt(bb, phi, v) and
|
||||
pred = getImmediateBasicBlockDominator(phi.getBasicBlock())
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* NB: If this predicate is exposed, it should be cached.
|
||||
*
|
||||
* Same as `ssaDefReachesEndOfBlockExt`, but ignores phi-reads.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate ssaDefReachesEndOfBlock(BasicBlock bb, Definition def, SourceVariable v) {
|
||||
ssaDefReachesEndOfBlockExt(bb, def, v)
|
||||
or
|
||||
exists(BasicBlock mid |
|
||||
ssaDefReachesEndOfBlock(mid, def, v) and
|
||||
phiReadReachesEndOfBlock(mid, bb, v)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
@ -623,20 +649,50 @@ module Make<InputSig Input> {
|
|||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* NB: If this predicate is exposed, it should be cached.
|
||||
*
|
||||
* Holds if `inp` is an input to the phi (read) node `phi` along the edge originating in `bb`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate phiHasInputFromBlockExt(DefinitionExt phi, DefinitionExt inp, BasicBlock bb) {
|
||||
exists(SourceVariable v, BasicBlock bbDef |
|
||||
phi.definesAt(v, bbDef, _, _) and
|
||||
getABasicBlockPredecessor(bbDef) = bb and
|
||||
ssaDefReachesEndOfBlockExt(bb, inp, v)
|
||||
|
|
||||
phi instanceof PhiNode or
|
||||
phi instanceof PhiReadNode
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* 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`.
|
||||
* basic block `bb`, without crossing another SSA definition of `v`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate ssaDefReachesReadExt(SourceVariable v, DefinitionExt def, BasicBlock bb, int i) {
|
||||
ssaDefReachesReadWithinBlock(v, def, bb, i)
|
||||
or
|
||||
ssaRef(bb, i, v, SsaActualRead()) and
|
||||
ssaDefReachesEndOfBlockExt(getABasicBlockPredecessor(bb), def, v) and
|
||||
not ssaDefReachesReadWithinBlock(v, _, bb, i)
|
||||
}
|
||||
|
||||
/**
|
||||
* NB: If this predicate is exposed, it should be cached.
|
||||
*
|
||||
* Same as `ssaDefReachesReadExt`, but ignores phi-reads.
|
||||
*/
|
||||
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
|
||||
ssaRef(bb, i, v, SsaActualRead()) and
|
||||
ssaDefReachesEndOfBlock(getABasicBlockPredecessor(bb), def, v) and
|
||||
not ssaDefReachesReadWithinBlock(v, _, bb, i)
|
||||
not exists(Definition other | ssaDefReachesReadWithinBlock(v, other, bb, i))
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
@ -647,14 +703,32 @@ module Make<InputSig Input> {
|
|||
* path between them without any read of `def`.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate adjacentDefRead(Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2) {
|
||||
predicate adjacentDefReadExt(
|
||||
DefinitionExt def, SourceVariable v, 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
|
||||
rnk = ssaDefRank(def, v, bb1, i1, _) and
|
||||
rnk + 1 = ssaDefRank(def, v, bb1, i2, SsaActualRead()) and
|
||||
variableRead(bb1, i2, v, _) and
|
||||
bb2 = bb1
|
||||
)
|
||||
or
|
||||
lastSsaRefExt(def, v, bb1, i1) and
|
||||
defAdjacentReadExt(def, bb1, bb2, i2)
|
||||
}
|
||||
|
||||
/**
|
||||
* NB: If this predicate is exposed, it should be cached.
|
||||
*
|
||||
* Same as `adjacentDefReadExt`, but ignores phi-reads.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate adjacentDefRead(Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2) {
|
||||
exists(SourceVariable v |
|
||||
adjacentDefReadExt(getAnUltimateOutput(def), v, bb1, i1, bb2, i2) and
|
||||
ssaRefNonPhiRead(bb1, i1, v)
|
||||
)
|
||||
or
|
||||
lastSsaRef(def, _, bb1, i1) and
|
||||
defAdjacentRead(def, bb1, bb2, i2)
|
||||
}
|
||||
|
|
@ -704,19 +778,41 @@ module Make<InputSig Input> {
|
|||
* without passing through another read or write.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate lastRefRedefExt(
|
||||
DefinitionExt def, SourceVariable v, BasicBlock bb, int i, DefinitionExt next
|
||||
) {
|
||||
// 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, ssaDefExt())
|
||||
)
|
||||
or
|
||||
// Can reach a write using one or more steps
|
||||
lastSsaRefExt(def, v, bb, i) and
|
||||
exists(BasicBlock bb2 |
|
||||
varBlockReachesExt(def, v, bb, bb2) and
|
||||
1 = ssaDefRank(next, v, bb2, _, ssaDefExt())
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* NB: If this predicate is exposed, it should be cached.
|
||||
*
|
||||
* Same as `lastRefRedefExt`, but ignores phi-reads.
|
||||
*/
|
||||
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
|
||||
lastRefRedefExt(getAnUltimateOutput(def), v, bb, i, next) and
|
||||
ssaRefNonPhiRead(bb, i, v)
|
||||
)
|
||||
or
|
||||
// Can reach a write using one or more steps
|
||||
exists(SourceVariable v |
|
||||
lastSsaRef(def, v, bb, i) and
|
||||
exists(BasicBlock bb2 |
|
||||
varBlockReaches(def, bb, bb2) and
|
||||
varBlockReachesRef(def, v, bb, bb2) and
|
||||
1 = ssaDefRank(next, v, bb2, _, SsaDef())
|
||||
)
|
||||
)
|
||||
|
|
@ -770,6 +866,25 @@ module Make<InputSig Input> {
|
|||
* another read.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate lastRefExt(DefinitionExt def, BasicBlock bb, int i) {
|
||||
// Can reach another definition
|
||||
lastRefRedefExt(def, _, bb, i, _)
|
||||
or
|
||||
exists(SourceVariable v | lastSsaRefExt(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
|
||||
varBlockReachesExitExt(def, bb)
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* NB: If this predicate is exposed, it should be cached.
|
||||
*
|
||||
* Same as `lastRefExt`, but ignores phi-reads.
|
||||
*/
|
||||
pragma[nomagic]
|
||||
predicate lastRef(Definition def, BasicBlock bb, int i) {
|
||||
// Can reach another definition
|
||||
lastRefRedef(def, bb, i, _)
|
||||
|
|
@ -819,7 +934,7 @@ module Make<InputSig Input> {
|
|||
final BasicBlock getBasicBlock() { this.definesAt(_, result, _) }
|
||||
|
||||
/** Gets a textual representation of this SSA definition. */
|
||||
string toString() { none() }
|
||||
string toString() { result = "SSA def(" + this.getSourceVariable() + ")" }
|
||||
}
|
||||
|
||||
/** An SSA definition that corresponds to a write. */
|
||||
|
|
@ -829,13 +944,11 @@ module Make<InputSig Input> {
|
|||
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" }
|
||||
override string toString() { result = "SSA phi(" + this.getSourceVariable() + ")" }
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
@ -851,6 +964,120 @@ module Make<InputSig Input> {
|
|||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* An extended static single assignment (SSA) definition.
|
||||
*
|
||||
* This is either a normal SSA definition (`Definition`) or a
|
||||
* phi-read node (`PhiReadNode`).
|
||||
*/
|
||||
class DefinitionExt extends TDefinitionExt {
|
||||
/** 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, SsaRefKind kind) {
|
||||
this.(Definition).definesAt(v, bb, i) and
|
||||
kind = SsaDef()
|
||||
or
|
||||
this = TPhiReadNode(v, bb) and i = -1 and kind = SsaPhiRead()
|
||||
}
|
||||
|
||||
/** 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() { result = this.(Definition).toString() }
|
||||
}
|
||||
|
||||
/**
|
||||
* A phi-read node.
|
||||
*
|
||||
* 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 normal phi node.
|
||||
*
|
||||
* 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.
|
||||
*
|
||||
* Another motivation for phi-reads is when a large number of reads can reach
|
||||
* another large number of reads:
|
||||
*
|
||||
* ```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
|
||||
*
|
||||
* if (a)
|
||||
* use(x);
|
||||
* else if (b)
|
||||
* use(x);
|
||||
* else if (c)
|
||||
* use(x);
|
||||
* else if (d)
|
||||
* use(x);
|
||||
* // many more ifs ...
|
||||
* ```
|
||||
*
|
||||
* Without phi-reads, one needs to add `n*m` data-flow edges (assuming `n` reads
|
||||
* before the phi-read and `m` reads after the phi-read), whereas if we include
|
||||
* phi-reads in the data-flow graph, we only need to add `n+m` edges.
|
||||
*
|
||||
* 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.
|
||||
*/
|
||||
class PhiReadNode extends DefinitionExt, TPhiReadNode {
|
||||
override string toString() { result = "SSA phi read(" + this.getSourceVariable() + ")" }
|
||||
}
|
||||
|
||||
/** Provides a set of consistency queries. */
|
||||
module Consistency {
|
||||
/** A definition that is relevant for the consistency queries. */
|
||||
|
|
@ -861,18 +1088,40 @@ module Make<InputSig Input> {
|
|||
);
|
||||
}
|
||||
|
||||
/** A definition that is relevant for the consistency queries. */
|
||||
abstract class RelevantDefinitionExt extends DefinitionExt {
|
||||
/** Override this predicate to ensure locations in consistency results. */
|
||||
abstract predicate hasLocationInfo(
|
||||
string filepath, int startline, int startcolumn, int endline, int endcolumn
|
||||
);
|
||||
}
|
||||
|
||||
/** Holds if a read can be reached from multiple definitions. */
|
||||
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)))
|
||||
}
|
||||
|
||||
/** Holds if a read can be reached from multiple definitions. */
|
||||
query predicate nonUniqueDefExt(
|
||||
RelevantDefinitionExt def, SourceVariable v, BasicBlock bb, int i
|
||||
) {
|
||||
ssaDefReachesReadExt(v, def, bb, i) and
|
||||
not exists(unique(DefinitionExt def0 | ssaDefReachesReadExt(v, def0, bb, i)))
|
||||
}
|
||||
|
||||
/** Holds if a read cannot be reached from a definition. */
|
||||
query predicate readWithoutDef(SourceVariable v, BasicBlock bb, int i) {
|
||||
variableRead(bb, i, v, _) and
|
||||
not ssaDefReachesRead(v, _, bb, i)
|
||||
}
|
||||
|
||||
/** Holds if a read cannot be reached from a definition. */
|
||||
query predicate readWithoutDefExt(SourceVariable v, BasicBlock bb, int i) {
|
||||
variableRead(bb, i, v, _) and
|
||||
not ssaDefReachesReadExt(v, _, bb, i)
|
||||
}
|
||||
|
||||
/** Holds if a definition cannot reach a read. */
|
||||
query predicate deadDef(RelevantDefinition def, SourceVariable v) {
|
||||
v = def.getSourceVariable() and
|
||||
|
|
@ -881,6 +1130,14 @@ module Make<InputSig Input> {
|
|||
not uncertainWriteDefinitionInput(_, def)
|
||||
}
|
||||
|
||||
/** Holds if a definition cannot reach a read. */
|
||||
query predicate deadDefExt(RelevantDefinitionExt def, SourceVariable v) {
|
||||
v = def.getSourceVariable() and
|
||||
not ssaDefReachesReadExt(_, def, _, _) and
|
||||
not phiHasInputFromBlockExt(_, def, _) and
|
||||
not uncertainWriteDefinitionInput(_, def)
|
||||
}
|
||||
|
||||
/** Holds if a read is not dominated by a definition. */
|
||||
query predicate notDominatedByDef(RelevantDefinition def, SourceVariable v, BasicBlock bb, int i) {
|
||||
exists(BasicBlock bbDef, int iDef | def.definesAt(v, bbDef, iDef) |
|
||||
|
|
@ -892,5 +1149,19 @@ module Make<InputSig Input> {
|
|||
not def.definesAt(v, getImmediateBasicBlockDominator*(bb), _)
|
||||
)
|
||||
}
|
||||
|
||||
/** Holds if a read is not dominated by a definition. */
|
||||
query predicate notDominatedByDefExt(
|
||||
RelevantDefinitionExt 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
|
||||
ssaDefReachesReadExt(v, def, bb, i) and
|
||||
not ssaDefReachesReadWithinBlock(v, def, bb, i) and
|
||||
not def.definesAt(v, getImmediateBasicBlockDominator*(bb), _, _)
|
||||
)
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
Загрузка…
Ссылка в новой задаче