/**

* Provides a language-independent implementation of static single assignment

* (SSA) form.

*/

overlay[local?]

module;

private import codeql.controlflow.BasicBlock as BB

private import codeql.util.Location

private import codeql.util.Unit

private signature class TypSig;

/** Provides the input specification of the SSA implementation. */

signature module InputSig<LocationSig Location, TypSig BasicBlock> {

/** A variable that can be SSA converted. */

class SourceVariable {

/** Gets a textual representation of this variable. */

string toString();

/** Gets the location of this variable. */

Location getLocation();

}

/**

* 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.

*

* Examples of uncertain writes are `ref` arguments in C#, where it is the callee

* that may or may not update the argument.

*/

predicate variableWrite(BasicBlock bb, int i, SourceVariable v, boolean certain);

/**

* Holds if the `i`th node of basic block `bb` reads source variable `v`. The

* Boolean `certain` indicates whether the read is certain.

*

* Examples of uncertain reads are pseudo-reads inserted at the end of a C# method

* with a `ref` or `out` parameter, where it is the caller that may or may not read

* the argument.

*/

predicate variableRead(BasicBlock bb, int i, SourceVariable v, boolean certain);

}

/**

* Provides classes and predicates for the SSA representation of variables.

*

* Class hierarchy:

* ```text

* SsaDefinition

* |- SsaWriteDefinition

* | |- SsaExplicitWrite

* | | \- SsaParameterInit

* | |- SsaImplicitWrite

* | | \- SsaImplicitEntryDefinition

* | \- SsaUncertainWrite (overlaps SsaImplicitWrite and potentially SsaExplicitWrite)

* \- SsaPhiDefinition

* ```

*/

signature module SsaSig<

LocationSig Location, TypSig ControlFlowNode, TypSig BasicBlock, TypSig Expr, TypSig Parameter,

TypSig VariableWrite>

{

/** A variable that can be SSA converted. */

class SourceVariable {

/** Gets a textual representation of this variable. */

string toString();

/** Gets the location of this variable. */

Location getLocation();

}

/** A static single assignment (SSA) definition. */

class SsaDefinition {

/** Gets the source variable underlying this SSA definition. */

SourceVariable getSourceVariable();

/**

* Holds if this SSA definition defines `v` at index `i` in basic block `bb`.

* Phi definitions are considered to be at index `-1`, while normal variable writes

* are at the index of the control flow node they wrap.

*/

predicate definesAt(SourceVariable v, BasicBlock bb, int i);

/** Gets the basic block to which this SSA definition belongs. */

BasicBlock getBasicBlock();

/**

* Gets the control flow node of this SSA definition.

*

* For SSA definitions occurring at the beginning of a basic block, such as

* phi definitions, this will get the first control flow node of the basic block.

*/

ControlFlowNode getControlFlowNode();

/** Gets a read of this SSA definition. */

Expr getARead();

/**

* Holds if this SSA definition is live at the end of basic block `bb`.

* That is, this definition reaches the end of basic block `bb`, at which

* point it is still live, without crossing another SSA definition of the

* same source variable.

*/

predicate isLiveAtEndOfBlock(BasicBlock bb);

/**

* Gets a definition that ultimately defines this SSA definition and is

* not itself a phi definition.

*

* Example:

*

* ```rb

* def m b

* i = 0 # defines i_0

* if b

* i = 1 # defines i_1

* else

* i = 2 # defines i_2

* end

* # defines i_3 = phi(i_1, i_2); ultimate definitions are i_1 and i_2

* puts i

* end

* ```

*/

SsaDefinition getAnUltimateDefinition();

/** Gets a textual representation of this SSA definition. */

string toString();

/** Gets the location of this SSA definition. */

Location getLocation();

}

/**

* A write definition. This includes every definition that is not a phi

* definition.

*/

class SsaWriteDefinition extends SsaDefinition;

/**

* An SSA definition that corresponds to an explicit variable update or

* declaration.

*/

class SsaExplicitWrite extends SsaWriteDefinition {

/** Gets the write underlying this SSA definition. */

VariableWrite getDefinition();

/**

* Gets the expression representing this write, if any. This is equivalent

* to `getDefinition().asExpr()`.

*/

Expr getDefiningExpr();

/**

* Gets the expression with the value being written, if any. This is

* equivalent to `getDefinition().getValue()`.

*/

Expr getValue();

}

/**

* An SSA definition representing the initialization of a parameter at the

* beginning of a callable.

*/

class SsaParameterInit extends SsaExplicitWrite {

/**

* Gets the parameter that this definition represents. This is equivalent

* to `getDefinition().isParameterInit(result)`

*/

Parameter getParameter();

}

/**

* An SSA definition that does not correspond to an explicit variable

* update or declaration.

*

* This includes implicit entry definitions for fields and captured

* variables, as well as field updates through side-effects and implicit

* definitions for fields whenever the qualifier is updated.

*/

class SsaImplicitWrite extends SsaWriteDefinition;

/**

* An SSA definition representing the implicit initialization of a variable

* at the beginning of a callable. This includes fields and captured

* variables, but excludes parameters as they have explicit declarations.

*/

class SsaImplicitEntryDefinition extends SsaImplicitWrite;

/** An SSA definition that represents an uncertain variable update. */

class SsaUncertainWrite extends SsaWriteDefinition {

/**

* Gets the immediately preceding definition. Since this update is uncertain,

* the value from the preceding definition might still be valid.

*/

SsaDefinition getPriorDefinition();

}

/**

* An SSA phi definition, that is, a pseudo definition for a variable at a

* point in the flow graph where otherwise two or more definitions for the

* variable would be visible.

*

* For example, in

* ```rb

* if b

* x = 0

* else

* x = 1

* end

* puts x

* ```

* a phi definition for `x` is inserted just before the call `puts x`.

*/

class SsaPhiDefinition extends SsaDefinition {

/** Holds if `inp` is an input to this phi definition along the edge originating in `bb`. */

predicate hasInputFromBlock(SsaDefinition inp, BasicBlock bb);

/**

* Gets an input of this phi definition.

*

* Example:

*

* ```rb

* def m b

* i = 0 # defines i_0

* if b

* i = 1 # defines i_1

* else

* i = 2 # defines i_2

* end

* # defines i_3 = phi(i_1, i_2); inputs are i_1 and i_2

* puts i

* end

* ```

*/

SsaDefinition getAnInput();

}

}

/**

* Provides an SSA implementation.

*

* The SSA construction is pruned based on liveness. That is, SSA definitions are only

* constructed for `Input::variableWrite`s when it is possible to reach an

* `Input::variableRead`, without going through a certain write (the same goes for `phi`

* nodes). Whenever a variable is both read and written at the same index in some basic

* block, the read is assumed to happen before the write.

*

* The result of invoking this parameterized module is not meant to be exposed directly;

* instead, one should define a language-specific layer on top, and make sure to cache

* all exposed predicates marked with

*

* ```

* NB: If this predicate is exposed, it should be cached.

* ```

*/

module Make<

LocationSig Location, BB::CfgSig<Location> Cfg, InputSig<Location, Cfg::BasicBlock> Input>

{

private import Cfg

private import Input

private BasicBlock getABasicBlockPredecessor(BasicBlock bb) { result.getASuccessor() = bb }

/**

* A classification of variable references into reads and

* (certain or uncertain) writes / definitions.

*/

private newtype TRefKind =

Read() or

Write(boolean certain) { certain in [false, true] } or

Def()

private class RefKind extends TRefKind {

string toString() {

this = Read() and result = "read"

or

exists(boolean certain | this = Write(certain) and result = "write (" + certain + ")")

or

this = Def() and result = "def"

}

int getOrder() {

this = Read() and

result = 0

or

this = Write(_) and

result = 1

or

this = Def() and

result = 1

}

}

/**

* Holds if the `i`th node of basic block `bb` is a reference to `v` of kind `k`.

*/

private signature predicate refSig(BasicBlock bb, int i, SourceVariable v, RefKind k);

private module RankRefs<refSig/4 ref> {

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.

*/

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

)

}

int maxRefRank(BasicBlock bb, SourceVariable v) {

result = refRank(bb, _, v, _) and

not result + 1 = refRank(bb, _, v, _)

}

}

/**

* Liveness analysis (based on source variables) to restrict the size of the

* SSA representation.

*/

private module Liveness {

/**

* Holds if the `i`th node of basic block `bb` is a reference to `v` of kind `k`.

*/

predicate varRef(BasicBlock bb, int i, SourceVariable v, RefKind k) {

variableRead(bb, i, v, _) and k = Read()

or

exists(boolean certain | variableWrite(bb, i, v, certain) | k = Write(certain))

}

private import RankRefs<varRef/4>

/**

* Gets the (1-based) rank of the first reference to `v` inside basic block `bb`

* that is either a read or a certain write.

*

* Note that uncertain writes have no impact on liveness: a variable is

* live before an uncertain write if and only if it is live after.

* The reference identified here therefore determines liveness at the

* beginning of `bb`: if it is a read then the variable is live and if it

* is a write then it is not. For basic blocks without reads or certain

* writes, liveness at the beginning of the block is equivalent to liveness

* at the end of the block.

*/

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(bb.getASuccessor(), v) }

/**

* Holds if variable `v` is live in basic block `bb` at rank `rnk`.

*/

private predicate liveAtRank(BasicBlock bb, SourceVariable v, int rnk) {

exists(RefKind kind | rnk = refRank(bb, _, v, kind) |

rnk = maxRefRank(bb, v) and

liveAtExit(bb, v)

or

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, v, rnk))

}

}

private import Liveness

/**

* 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

defbb.inDominanceFrontier(bb)

)

}

/**

* 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 | readbb.inDominanceFrontier(bb) |

ssaDefReachesRead(v, _, readbb, _) and

variableRead(readbb, _, v, true) and

not variableWrite(readbb, _, v, _)

or

synthPhiRead(readbb, v) and

not varRef(readbb, _, v, _)

)

}

/**

* Holds if we should synthesize a pseudo-read of `v` at the beginning of `bb`.

*

* These reads are named phi-reads, since they are constructed in the same

* way as ordinary phi nodes except all reads are treated as potential

* "definitions". This ensures that use-use flow has the same dominance

* properties as def-use flow.

*/

private predicate synthPhiRead(BasicBlock bb, SourceVariable v) {

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, _)

}

cached

private newtype TDefinitionExt =

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)

} or

TPhiReadNode(SourceVariable v, BasicBlock bb) { synthPhiRead(bb, v) }

private class TDefinition = TWriteDef or TPhiNode;

private module SsaDefReachesNew {

/**

* Holds if the `i`th node of basic block `bb` is a reference to `v`,

* either a read (when `k` is `Read()`) or an SSA definition (when

* `k` is `Def()`).

*

* Unlike `Liveness::varRef`, this includes `phi` nodes and pseudo-reads

* associated with uncertain writes.

*/

pragma[nomagic]

predicate ssaRef(BasicBlock bb, int i, SourceVariable v, RefKind k) {

variableRead(bb, i, v, _) and

k = Read()

or

variableWrite(bb, i, v, false) and

k = Read()

or

any(Definition def).definesAt(v, bb, i) and

k = Def()

}

private import RankRefs<ssaRef/4>

/**

* 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 = refRank(bb, i, v, Def()) and

def.definesAt(v, bb, i)

)

or

ssaDefReachesRank(bb, def, rnk - 1, v) and

rnk = refRank(bb, _, v, Read())

}

/**

* Holds if `v` is live at the end of basic block `bb` with the same value as at

* the end of the immediate dominator, `idom`, of `bb`.

*/

pragma[nomagic]

private predicate liveThrough(BasicBlock idom, BasicBlock bb, SourceVariable v) {

idom = bb.getImmediateDominator() and

liveAtExit(bb, v) and

not any(Definition def).definesAt(v, bb, _)

}

/**

* 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 = maxRefRank(pragma[only_bind_into](bb), pragma[only_bind_into](v)) and

ssaDefReachesRank(bb, def, last, v) and

liveAtExit(bb, v)

)

or

exists(BasicBlock idom |

// 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(idom, def, v) and

liveThrough(idom, bb, v)

)

}

/**

* Holds if the SSA definition of `v` at `def` reaches index `i` in its own

* 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 = refRank(bb, i, v, Read())

)

}

/**

* 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`.

*/

pragma[nomagic]

predicate ssaDefReachesRead(SourceVariable v, Definition def, BasicBlock bb, int i) {

ssaDefReachesReadWithinBlock(v, def, bb, i)

or

ssaRef(bb, i, v, Read()) and

ssaDefReachesEndOfBlock(bb.getImmediateDominator(), def, v) and

not ssaDefReachesReadWithinBlock(v, _, bb, i)

}

predicate uncertainWriteDefinitionInput(UncertainWriteDefinition def, Definition inp) {

exists(SourceVariable v, BasicBlock bb, int i |

def.definesAt(v, bb, i) and

ssaDefReachesRead(v, inp, bb, i)

)

}

}

private module AdjacentSsaRefs {

/**

* Holds if the `i`th node of basic block `bb` is a reference to `v`,

* either a read (when `k` is `Read()`) or an SSA definition (when

* `k` is `Def()`).

*

* Unlike `Liveness::varRef`, this includes phi nodes, phi reads, and

* pseudo-reads associated with uncertain writes, but excludes uncertain

* reads.

*/

pragma[nomagic]

predicate ssaRef(BasicBlock bb, int i, SourceVariable v, RefKind k) {

variableRead(bb, i, v, true) and

k = Read()

or

variableWrite(bb, i, v, false) and

k = Read()

or

any(Definition def).definesAt(v, bb, i) and

k = Def()

or

synthPhiRead(bb, v) and i = -1 and k = Def()

}

private import RankRefs<ssaRef/4>

/**

* Holds if `v` is live at the end of basic block `bb`, which contains no

* reference to `v`, and `idom` is the immediate dominator of `bb`.

*/

pragma[nomagic]

private predicate liveThrough(BasicBlock idom, BasicBlock bb, SourceVariable v) {

idom = bb.getImmediateDominator() and

liveAtExit(bb, v) and

not ssaRef(bb, _, v, _)

}

pragma[nomagic]

private predicate refReachesEndOfBlock(BasicBlock bbRef, int i, BasicBlock bb, SourceVariable v) {

maxRefRank(bb, v) = refRank(bb, i, v, _) and

liveAtExit(bb, v) and

bbRef = bb

or

exists(BasicBlock idom |

refReachesEndOfBlock(bbRef, i, idom, v) and

liveThrough(idom, bb, v)

)

}

/**

* Holds if `v` has adjacent references at index `i1` in basic block `bb1`

* and index `i2` in basic block `bb2`, that is, there is a path between

* the first reference to the second without any other reference to `v` in

* between. References include certain reads, SSA definitions, and

* pseudo-reads in the form of phi-reads. The first reference can be any of

* these kinds while the second is restricted to certain reads and

* uncertain writes.

*

* Note that the placement of phi-reads ensures that the first reference is

* uniquely determined by the second and that the first reference dominates

* the second.

*/

predicate adjacentRefRead(BasicBlock bb1, int i1, BasicBlock bb2, int i2, SourceVariable v) {

bb1 = bb2 and

refRank(bb1, i1, v, _) + 1 = refRank(bb2, i2, v, Read())

or

refReachesEndOfBlock(bb1, i1, bb2.getImmediateDominator(), v) and

1 = refRank(bb2, i2, v, Read())

}

/**

* Holds if the phi node or phi-read for `v` in basic block `bbPhi` takes

* input from basic block `input`, and that the reference to `v` at index

* `i` in basic block `bb` reaches the end of `input` without going through

* any other reference to `v`.

*/

predicate adjacentRefPhi(

BasicBlock bb, int i, BasicBlock input, BasicBlock bbPhi, SourceVariable v

) {

refReachesEndOfBlock(bb, i, input, v) and

input = getABasicBlockPredecessor(bbPhi) and

1 = refRank(bbPhi, -1, v, _)

}

private predicate adjacentRefs(BasicBlock bb1, int i1, BasicBlock bb2, int i2, SourceVariable v) {

adjacentRefRead(bb1, i1, bb2, i2, v)

or

adjacentRefPhi(bb1, i1, _, bb2, v) and i2 = -1

}

/**

* Holds if the reference to `v` at index `i1` in basic block `bb1` reaches

* the certain read at index `i2` in basic block `bb2` without going

* through any other certain read. The boolean `samevar` indicates whether

* the two references are to the same SSA variable.

*

* Note that since this relation skips over phi nodes and phi reads, it may

* be quadratic in the number of variable references for certain access

* patterns.

*/

predicate firstUseAfterRef(

BasicBlock bb1, int i1, BasicBlock bb2, int i2, SourceVariable v, boolean samevar

) {

adjacentRefs(bb1, i1, bb2, i2, v) and

variableRead(bb2, i2, v, _) and

samevar = true

or

exists(BasicBlock bb0, int i0, boolean samevar0 |

firstUseAfterRef(bb0, i0, bb2, i2, v, samevar0) and

adjacentRefs(bb1, i1, bb0, i0, v) and

not variableWrite(bb0, i0, v, true) and

if any(Definition def).definesAt(v, bb0, i0)

then samevar = false

else (

samevar = samevar0 and synthPhiRead(bb0, v) and i0 = -1

)

)

}

}

/**

* Holds if `def` reaches the certain read at index `i` in basic block `bb`

* without going through any other certain read. The boolean `samevar`

* indicates whether the read is a use of `def` or whether some number of phi

* nodes and/or uncertain reads occur between `def` and the read.

*

* Note that since this relation skips over phi nodes and phi reads, it may

* be quadratic in the number of variable references for certain access

* patterns.

*/

predicate firstUse(Definition def, BasicBlock bb, int i, boolean samevar) {

exists(BasicBlock bb1, int i1, SourceVariable v |

def.definesAt(v, bb1, i1) and

AdjacentSsaRefs::firstUseAfterRef(bb1, i1, bb, i, v, samevar)

)

}

/**

* Holds if the certain read at index `i1` in basic block `bb1` reaches the

* certain read at index `i2` in basic block `bb2` without going through any

* other certain read. The boolean `samevar` indicates whether the two reads

* are of the same SSA variable.

*

* Note that since this relation skips over phi nodes and phi reads, it may

* be quadratic in the number of variable references for certain access

* patterns.

*/

predicate adjacentUseUse(

BasicBlock bb1, int i1, BasicBlock bb2, int i2, SourceVariable v, boolean samevar

) {

exists(boolean samevar0 |

variableRead(bb1, i1, v, true) and

not variableWrite(bb1, i1, v, true) and

AdjacentSsaRefs::firstUseAfterRef(bb1, i1, bb2, i2, v, samevar0) and

if any(Definition def).definesAt(v, bb1, i1) then samevar = false else samevar = samevar0

)

}

private module SsaDefReaches {

deprecated newtype TSsaRefKind =

SsaActualRead() or

SsaPhiRead() or

SsaDef()

deprecated class SsaRead = SsaActualRead or SsaPhiRead;

deprecated class SsaDefExt = SsaDef or SsaPhiRead;

deprecated SsaDefExt ssaDefExt() { any() }

/**

* A classification of SSA variable references into reads and definitions.

*/

deprecated 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 the `i`th node of basic block `bb` is a reference to `v`,

* either a read (when `k` is `SsaActualRead()`), an SSA definition (when `k`

* is `SsaDef()`), or a phi-read (when `k` is `SsaPhiRead()`).

*

* Unlike `Liveness::varRef`, this includes `phi` (read) nodes.

*/

pragma[nomagic]

deprecated predicate ssaRef(BasicBlock bb, int i, SourceVariable v, SsaRefKind k) {

variableRead(bb, i, v, _) and

k = SsaActualRead()

or

any(Definition def).definesAt(v, bb, i) and

k = SsaDef()

or

synthPhiRead(bb, v) and i = -1 and k = SsaPhiRead()

}

/**

* Holds if the `i`th node of basic block `bb` is a reference to `v`, and

* this reference is not a phi-read.

*/

deprecated predicate ssaRefNonPhiRead(BasicBlock bb, int i, SourceVariable v) {

ssaRef(bb, i, v, [SsaActualRead().(TSsaRefKind), SsaDef()])

}

deprecated private newtype OrderedSsaRefIndex =

deprecated MkOrderedSsaRefIndex(int i, SsaRefKind k) { ssaRef(_, i, _, k) }

deprecated 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.

*/

deprecated 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

)

}

deprecated 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`.

*/

deprecated predicate ssaDefReachesRank(

BasicBlock bb, DefinitionExt def, int rnk, SourceVariable v

) {

exists(int 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, 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`.

*/

deprecated predicate ssaDefReachesReadWithinBlock(

SourceVariable v, DefinitionExt def, BasicBlock bb, int i

) {

exists(int rnk |

ssaDefReachesRank(bb, def, rnk, v) and

rnk = ssaRefRank(bb, i, v, SsaActualRead())

)

}

/**

* Same as `ssaRefRank()`, but restricted to a particular SSA definition `def`.

*/

deprecated int ssaDefRank(

DefinitionExt def, SourceVariable v, BasicBlock bb, int i, SsaRefKind k

) {

result = ssaRefRank(bb, i, v, k) and

(

ssaDefReachesReadExt(v, def, bb, i)

or

def.definesAt(v, bb, i, k)

)

}

/**

* Holds if the reference to `def` at index `i` in basic block `bb` is the

* last reference to `v` inside `bb`.

*/

pragma[noinline]

deprecated predicate lastSsaRefExt(DefinitionExt def, SourceVariable v, BasicBlock bb, int i) {

ssaDefRank(def, v, bb, i, _) = maxSsaRefRank(bb, v)

}

/** Gets a phi-read node into which `inp` is an input, if any. */

pragma[nomagic]

deprecated private DefinitionExt getAPhiReadOutput(DefinitionExt inp) {

phiHasInputFromBlockExt(result.(PhiReadNode), inp, _)

}

pragma[nomagic]

deprecated DefinitionExt getAnUltimateOutput(Definition def) {

result = getAPhiReadOutput*(def)

}

/**

* Same as `lastSsaRefExt`, but ignores phi-reads.

*/

pragma[noinline]

deprecated predicate lastSsaRef(Definition def, SourceVariable v, BasicBlock bb, int i) {

lastSsaRefExt(getAnUltimateOutput(def), v, bb, i) and

ssaRefNonPhiRead(bb, i, v)

}

deprecated predicate defOccursInBlock(

DefinitionExt def, BasicBlock bb, SourceVariable v, SsaRefKind k

) {

exists(ssaDefRank(def, v, bb, _, k))

}

pragma[noinline]

deprecated predicate ssaDefReachesThroughBlock(DefinitionExt def, BasicBlock bb) {

exists(SourceVariable v |

ssaDefReachesEndOfBlockExt0(bb, def, v) and

not defOccursInBlock(_, bb, v, _)

)

}

/**

* 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`.

*/

pragma[nomagic]

deprecated predicate varBlockReachesExt(

DefinitionExt def, SourceVariable v, BasicBlock bb1, BasicBlock bb2

) {

defOccursInBlock(def, bb1, v, _) and

bb2 = bb1.getASuccessor()

or

exists(BasicBlock mid |

varBlockReachesExt(def, v, bb1, mid) and

ssaDefReachesThroughBlock(def, mid) and

bb2 = mid.getASuccessor()

)

}

pragma[nomagic]

deprecated 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 varRef(bb2, _, v, _)

)

}

pragma[nomagic]

deprecated private predicate varBlockReachesExclPhiRead(

DefinitionExt def, SourceVariable v, BasicBlock bb1, BasicBlock bb2

) {

varBlockReachesExt(def, v, bb1, bb2) and

ssaRefNonPhiRead(bb2, _, v)

or

exists(PhiReadNode phi, BasicBlock mid |

varBlockReachesExclPhiRead(phi, v, mid, bb2) and

phiReadStep(def, phi, bb1, mid)

)

}

/**

* 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]

deprecated predicate varBlockReachesRef(

Definition def, SourceVariable v, BasicBlock bb1, BasicBlock bb2

) {

varBlockReachesExclPhiRead(getAnUltimateOutput(def), v, bb1, bb2) and

ssaRefNonPhiRead(bb1, _, v)

}

pragma[nomagic]

deprecated 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]

deprecated predicate defAdjacentRead(Definition def, BasicBlock bb1, BasicBlock bb2, int i2) {

exists(SourceVariable v | varBlockReachesRef(def, v, bb1, bb2) |

ssaRefRank(bb2, i2, v, SsaActualRead()) = 1

or

ssaRefRank(bb2, _, v, SsaPhiRead()) = 1 and