hohn/codeql
1
0
Fork 0
mirror of https://github.com/github/codeql.git synced 2026-05-14 19:29:28 +02:00
Code Issues Packages Projects Releases Wiki Activity

Make Go use the shared SSA library (codeql.ssa.Ssa)

Browse Source 
Co-authored-by: owen-mc <62447351+owen-mc@users.noreply.github.com>
Agent-Logs-Url: https://github.com/github/codeql/sessions/b400ebd5-4095-401e-8811-fb550600b3c4
This commit is contained in:
copilot-swe-agent[bot]
2026-03-23 17:08:30 +00:00
committed by Owen Mansel-Chan
parent e3bcd3bdd5
commit e467cf6482
5 changed files with 164 additions and 486 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
go/ql/lib/change-notes/2026-03-23-use-shared-ssa.md Normal file
View File

@@ -0,0 +1,4 @@
---
category: minorAnalysis
---
* The Go SSA library now uses the shared SSA library (`codeql.ssa.Ssa`), consistent with other CodeQL languages such as C#, Java, Ruby, Rust, and Swift. This may result in minor changes to SSA construction in some edge cases.

1
go/ql/lib/qlpack.yml
View File

@@ -10,6 +10,7 @@ dependencies:
codeql/controlflow: ${workspace}
codeql/dataflow: ${workspace}
codeql/mad: ${workspace}
codeql/ssa: ${workspace}
codeql/threat-models: ${workspace}
codeql/tutorial: ${workspace}
codeql/util: ${workspace}

11
go/ql/lib/semmle/go/controlflow/BasicBlocks.qll
View File

@@ -48,6 +48,17 @@ class BasicBlock = BbImpl::BasicBlock;
class EntryBasicBlock = BbImpl::EntryBasicBlock;
/** Provides a `CfgSig` view of Go's control-flow graph for use with the shared SSA library. */
module Cfg implements BB::CfgSig<Location> {
class ControlFlowNode = BbImpl::ControlFlowNode;
class BasicBlock = BbImpl::BasicBlock;
class EntryBasicBlock = BbImpl::EntryBasicBlock;
predicate dominatingEdge = BbImpl::dominatingEdge/2;
}
cached
private predicate reachableBB(BasicBlock bb) {
bb instanceof EntryBasicBlock

151
go/ql/lib/semmle/go/dataflow/SSA.qll
View File

@@ -63,9 +63,9 @@ private predicate unresolvedIdentifier(Ident id, string name) {
/**
* An SSA variable.
*/
class SsaVariable extends TSsaDefinition {
class SsaVariable extends Definition {
/** Gets the source variable corresponding to this SSA variable. */
SsaSourceVariable getSourceVariable() { result = this.(SsaDefinition).getSourceVariable() }
SsaSourceVariable getSourceVariable() { this.definesAt(result, _, _) }
/** Gets the (unique) definition of this SSA variable. */
SsaDefinition getDefinition() { result = this }
@@ -74,21 +74,31 @@ class SsaVariable extends TSsaDefinition {
Type getType() { result = this.getSourceVariable().getType() }
/** Gets a use in basic block `bb` that refers to this SSA variable. */
IR::Instruction getAUseIn(ReachableBasicBlock bb) {
IR::Instruction getAUseIn(BasicBlock bb) {
exists(int i, SsaSourceVariable v | v = this.getSourceVariable() |
result = bb.getNode(i) and
this = getDefinition(bb, i, v)
ssaDefReachesRead(v, this, bb, i) and
useAt(bb, i, v)
)
}
/** Gets a use that refers to this SSA variable. */
IR::Instruction getAUse() { result = this.getAUseIn(_) }
/** Gets a textual representation of this element. */
string toString() { result = this.getDefinition().prettyPrintRef() }
/**
* Gets a textual representation of this element.
*
* The format is `kind@LINE:COL`, where `kind` is one of `def`, `capture`, or `phi`.
*/
override string toString() {
exists(Location loc | loc = this.(SsaDefinition).getLocation() |
result =
this.(SsaDefinition).getKind() + "@" + loc.getStartLine() + ":" + loc.getStartColumn()
)
}
/** Gets the location of this SSA variable. */
Location getLocation() { result = this.getDefinition().getLocation() }
Location getLocation() { result = this.(SsaDefinition).getLocation() }
/**
* DEPRECATED: Use `getLocation()` instead.
@@ -109,50 +119,28 @@ class SsaVariable extends TSsaDefinition {
/**
* An SSA definition.
*/
class SsaDefinition extends TSsaDefinition {
class SsaDefinition extends Definition {
/** Gets the SSA variable defined by this definition. */
SsaVariable getVariable() { result = this }
/** Gets the source variable defined by this definition. */
abstract SsaSourceVariable getSourceVariable();
SsaSourceVariable getSourceVariable() { this.definesAt(result, _, _) }
/**
* Gets the basic block to which this definition belongs.
*/
abstract ReachableBasicBlock getBasicBlock();
/**
* INTERNAL: Use `getBasicBlock()` and `getSourceVariable()` instead.
*
* Holds if this is a definition of source variable `v` at index `idx` in basic block `bb`.
*
* Phi nodes are considered to be at index `-1`, all other definitions at the index of
* the control flow node they correspond to.
*/
abstract predicate definesAt(ReachableBasicBlock bb, int idx, SsaSourceVariable v);
/**
* INTERNAL: Use `toString()` instead.
*
* Gets a pretty-printed representation of this SSA definition.
*/
abstract string prettyPrintDef();
/**
* INTERNAL: Do not use.
*
* Gets a pretty-printed representation of a reference to this SSA definition.
*/
abstract string prettyPrintRef();
BasicBlock getBasicBlock() { this.definesAt(_, result, _) }
/** Gets the innermost function or file to which this SSA definition belongs. */
ControlFlow::Root getRoot() { result = this.getBasicBlock().getScope() }
/** Gets a textual representation of this element. */
string toString() { result = this.prettyPrintDef() }
/** Gets the source location for this element. */
abstract Location getLocation();
/**
* INTERNAL: Do not use.
*
* Gets a short string identifying the kind of this SSA definition,
* used in reference formatting (e.g., `"def"`, `"capture"`, `"phi"`).
*/
string getKind() { none() }
/**
* DEPRECATED: Use `getLocation()` instead.
@@ -180,32 +168,25 @@ class SsaDefinition extends TSsaDefinition {
/**
* An SSA definition that corresponds to an explicit assignment or other variable definition.
*/
class SsaExplicitDefinition extends SsaDefinition, TExplicitDef {
class SsaExplicitDefinition extends SsaDefinition, WriteDefinition {
SsaExplicitDefinition() {
exists(BasicBlock bb, int i, SsaSourceVariable v |
this.definesAt(v, bb, i) and
defAt(bb, i, v)
)
}
/** Gets the instruction where the definition happens. */
IR::Instruction getInstruction() {
exists(BasicBlock bb, int i | this = TExplicitDef(bb, i, _) | result = bb.getNode(i))
exists(BasicBlock bb, int i | this.definesAt(_, bb, i) | result = bb.getNode(i))
}
/** Gets the right-hand side of the definition. */
IR::Instruction getRhs() { this.getInstruction().writes(_, result) }
override predicate definesAt(ReachableBasicBlock bb, int i, SsaSourceVariable v) {
this = TExplicitDef(bb, i, v)
}
override string getKind() { result = "def" }
override ReachableBasicBlock getBasicBlock() { this.definesAt(result, _, _) }
override SsaSourceVariable getSourceVariable() { this = TExplicitDef(_, _, result) }
override string prettyPrintRef() {
exists(Location loc | loc = this.getLocation() |
result = "def@" + loc.getStartLine() + ":" + loc.getStartColumn()
)
}
override string prettyPrintDef() { result = "definition of " + this.getSourceVariable() }
override Location getLocation() { result = this.getInstruction().getLocation() }
override string toString() { result = "definition of " + this.getSourceVariable() }
}
/** Provides a helper predicate for working with explicit SSA definitions. */
@@ -220,19 +201,6 @@ module SsaExplicitDefinition {
* An SSA definition that does not correspond to an explicit variable definition.
*/
abstract class SsaImplicitDefinition extends SsaDefinition {
/**
* INTERNAL: Do not use.
*
* Gets the definition kind to include in `prettyPrintRef`.
*/
abstract string getKind();
override string prettyPrintRef() {
exists(Location loc | loc = this.getLocation() |
result = this.getKind() + "@" + loc.getStartLine() + ":" + loc.getStartColumn()
)
}
override Location getLocation() { result = this.getBasicBlock().getLocation() }
}
@@ -243,24 +211,16 @@ abstract class SsaImplicitDefinition extends SsaDefinition {
* Capturing definitions appear at the beginning of such functions, as well as
* at any function call that may affect the value of the variable.
*/
class SsaVariableCapture extends SsaImplicitDefinition, TCapture {
override predicate definesAt(ReachableBasicBlock bb, int i, SsaSourceVariable v) {
this = TCapture(bb, i, v)
}
override ReachableBasicBlock getBasicBlock() { this.definesAt(result, _, _) }
override SsaSourceVariable getSourceVariable() { this.definesAt(_, _, result) }
override string getKind() { result = "capture" }
override string prettyPrintDef() { result = "capture variable " + this.getSourceVariable() }
class SsaVariableCapture extends SsaImplicitDefinition, UncertainWriteDefinition {
override Location getLocation() {
exists(ReachableBasicBlock bb, int i | this.definesAt(bb, i, _) |
exists(BasicBlock bb, int i | this.definesAt(_, bb, i) |
result = bb.getNode(i).getLocation()
)
}
override string getKind() { result = "capture" }
override string toString() { result = "capture variable " + this.getSourceVariable() }
}
/**
@@ -277,7 +237,10 @@ abstract class SsaPseudoDefinition extends SsaImplicitDefinition {
* Gets a textual representation of the inputs of this pseudo-definition
* in lexicographical order.
*/
string ppInputs() { result = concat(this.getAnInput().getDefinition().prettyPrintRef(), ", ") }
string ppInputs() {
result =
concat(SsaVariable inp | inp = this.getAnInput() | inp.toString() order by inp.toString())
}
}
/**
@@ -285,26 +248,14 @@ abstract class SsaPseudoDefinition extends SsaImplicitDefinition {
* in the flow graph where otherwise two or more definitions for the variable
* would be visible.
*/
class SsaPhiNode extends SsaPseudoDefinition, TPhi {
override SsaVariable getAnInput() {
result = getDefReachingEndOf(this.getBasicBlock().getAPredecessor(_), this.getSourceVariable())
}
override predicate definesAt(ReachableBasicBlock bb, int i, SsaSourceVariable v) {
bb = this.getBasicBlock() and v = this.getSourceVariable() and i = -1
}
override ReachableBasicBlock getBasicBlock() { this = TPhi(result, _) }
override SsaSourceVariable getSourceVariable() { this = TPhi(_, result) }
class SsaPhiNode extends SsaPseudoDefinition, PhiNode {
override SsaVariable getAnInput() { phiHasInputFromBlock(this, result, _) }
override string getKind() { result = "phi" }
override string prettyPrintDef() {
override string toString() {
result = this.getSourceVariable() + " = phi(" + this.ppInputs() + ")"
}
override Location getLocation() { result = this.getBasicBlock().getLocation() }
}
/**

483
go/ql/lib/semmle/go/dataflow/SsaImpl.qll
View File

@@ -7,76 +7,25 @@ overlay[local]
module;
import go
private import codeql.ssa.Ssa as SsaImplCommon
private import semmle.go.controlflow.BasicBlocks as BasicBlocks
private class BasicBlock = BasicBlocks::BasicBlock;
cached
private module Internal {
/** Holds if the `i`th node of `bb` defines `v`. */
cached
predicate defAt(ReachableBasicBlock bb, int i, SsaSourceVariable v) {
predicate defAt(BasicBlock bb, int i, SsaSourceVariable v) {
bb.getNode(i).(IR::Instruction).writes(v, _)
}
/** Holds if the `i`th node of `bb` reads `v`. */
cached
predicate useAt(ReachableBasicBlock bb, int i, SsaSourceVariable v) {
predicate useAt(BasicBlock bb, int i, SsaSourceVariable v) {
bb.getNode(i).(IR::Instruction).reads(v)
}
/**
* A data type representing SSA definitions.
*
* We distinguish three kinds of SSA definitions:
*
* 1. Variable definitions, including declarations, assignments and increments/decrements.
* 2. Pseudo-definitions for captured variables at the beginning of the capturing function
* as well as after calls.
* 3. Phi nodes.
*
* SSA definitions are only introduced where necessary. In particular,
* unreachable code has no SSA definitions associated with it, and neither
* have dead assignments (that is, assignments whose value is never read).
*/
cached
newtype TSsaDefinition =
/**
* An SSA definition that corresponds to an explicit assignment or other variable definition.
*/
TExplicitDef(ReachableBasicBlock bb, int i, SsaSourceVariable v) {
defAt(bb, i, v) and
(liveAfterDef(bb, i, v) or v.isCaptured())
} or
/**
* An SSA definition representing the capturing of an SSA-convertible variable
* in the closure of a nested function.
*
* Capturing definitions appear at the beginning of such functions, as well as
* at any function call that may affect the value of the variable.
*/
TCapture(ReachableBasicBlock bb, int i, SsaSourceVariable v) {
mayCapture(bb, i, v) and
liveAfterDef(bb, i, v)
} or
/**
* An SSA phi node, 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.
*/
TPhi(ReachableJoinBlock bb, SsaSourceVariable v) {
liveAtEntry(bb, v) and
inDefDominanceFrontier(bb, v)
}
/**
* Holds if `bb` is in the dominance frontier of a block containing a definition of `v`.
*/
pragma[noinline]
private predicate inDefDominanceFrontier(ReachableJoinBlock bb, SsaSourceVariable v) {
exists(ReachableBasicBlock defbb, SsaDefinition def |
def.definesAt(defbb, _, v) and
defbb.inDominanceFrontier(bb)
)
}
/**
* Holds if `v` is a captured variable which is declared in `declFun` and read in `useFun`.
*/
@@ -87,7 +36,7 @@ private module Internal {
}
/** Holds if the `i`th node of `bb` in function `f` is an entry node. */
private predicate entryNode(FuncDef f, ReachableBasicBlock bb, int i) {
private predicate entryNode(FuncDef f, BasicBlock bb, int i) {
f = bb.getScope() and
bb.getNode(i).isEntryNode()
}
@@ -95,17 +44,17 @@ private module Internal {
/**
* Holds if the `i`th node of `bb` in function `f` is a function call.
*/
private predicate callNode(FuncDef f, ReachableBasicBlock bb, int i) {
private predicate callNode(FuncDef f, BasicBlock bb, int i) {
f = bb.getScope() and
bb.getNode(i).(IR::EvalInstruction).getExpr() instanceof CallExpr
}
/**
* Holds if the `i`th node of basic block `bb` may induce a pseudo-definition for
* modeling updates to captured variable `v`. Whether the definition is actually
* introduced depends on whether `v` is live at this point in the program.
* modeling updates to captured variable `v`.
*/
private predicate mayCapture(ReachableBasicBlock bb, int i, SsaSourceVariable v) {
cached
predicate mayCapture(BasicBlock bb, int i, SsaSourceVariable v) {
exists(FuncDef capturingContainer, FuncDef declContainer |
// capture initial value of variable declared in enclosing scope
readsCapturedVar(capturingContainer, v, declContainer) and
@@ -119,347 +68,109 @@ private module Internal {
)
}
/** A classification of variable references into reads and writes. */
private newtype RefKind =
ReadRef() or
WriteRef()
/**
* Holds if the `i`th node of basic block `bb` is a reference to `v`, either a read
* (when `tp` is `ReadRef()`) or a direct or indirect write (when `tp` is `WriteRef()`).
*/
private predicate ref(ReachableBasicBlock bb, int i, SsaSourceVariable v, RefKind tp) {
useAt(bb, i, v) and tp = ReadRef()
or
(mayCapture(bb, i, v) or defAt(bb, i, v)) and
tp = WriteRef()
}
/**
* 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 `tp`.
*/
private int refRank(ReachableBasicBlock bb, int i, SsaSourceVariable v, RefKind tp) {
i = rank[result](int j | ref(bb, j, v, _)) and
ref(bb, i, v, tp)
}
/**
* Gets the maximum rank among all references to `v` in basic block `bb`.
*/
private int maxRefRank(ReachableBasicBlock bb, SsaSourceVariable v) {
result = max(refRank(bb, _, v, _))
}
/**
* Holds if variable `v` is live after the `i`th node of basic block `bb`, where
* `i` is the index of a node that may assign or capture `v`.
*
* For the purposes of this predicate, function calls are considered as writes of captured variables.
*/
private predicate liveAfterDef(ReachableBasicBlock bb, int i, SsaSourceVariable v) {
exists(int r | r = refRank(bb, i, v, WriteRef()) |
// the next reference to `v` inside `bb` is a read
r + 1 = refRank(bb, _, v, ReadRef())
or
// this is the last reference to `v` inside `bb`, but `v` is live at entry
// to a successor basic block of `bb`
r = maxRefRank(bb, v) and
liveAtSuccEntry(bb, v)
)
}
/**
* Holds if variable `v` is live at the beginning of basic block `bb`.
*
* For the purposes of this predicate, function calls are considered as writes of captured variables.
*/
private predicate liveAtEntry(ReachableBasicBlock bb, SsaSourceVariable v) {
// the first reference to `v` inside `bb` is a read
refRank(bb, _, v, ReadRef()) = 1
or
// there is no reference to `v` inside `bb`, but `v` is live at entry
// to a successor basic block of `bb`
not exists(refRank(bb, _, v, _)) and
liveAtSuccEntry(bb, v)
}
/**
* Holds if `v` is live at the beginning of any successor of basic block `bb`.
*/
private predicate liveAtSuccEntry(ReachableBasicBlock bb, SsaSourceVariable v) {
liveAtEntry(bb.getASuccessor(_), v)
}
/**
* Holds if `v` is assigned outside its declaring function.
*/
private predicate assignedThroughClosure(SsaSourceVariable v) {
cached
predicate assignedThroughClosure(SsaSourceVariable v) {
any(IR::Instruction def | def.writes(v, _)).getRoot() != v.getDeclaringFunction()
}
/**
* Holds if the `i`th node of `bb` is a use or an SSA definition of variable `v`, with
* `k` indicating whether it is the former or the latter.
*
* Note this includes phi nodes, whereas `ref` above only includes explicit writes and captures.
*/
private predicate ssaRef(ReachableBasicBlock bb, int i, SsaSourceVariable v, RefKind k) {
useAt(bb, i, v) and k = ReadRef()
or
any(SsaDefinition def).definesAt(bb, i, v) and k = WriteRef()
}
/**
* Gets the (1-based) rank of the `i`th node of `bb` among all SSA definitions
* and uses of `v` in `bb`, with `k` indicating whether it is a definition or a use.
*
* For example, if `bb` is a basic block with a phi node for `v` (considered
* to be at index -1), uses `v` at node 2 and defines it at node 5, we have:
*
* ```
* ssaRefRank(bb, -1, v, WriteRef()) = 1 // phi node
* ssaRefRank(bb, 2, v, ReadRef()) = 2 // use at node 2
* ssaRefRank(bb, 5, v, WriteRef()) = 3 // definition at node 5
* ```
*/
private int ssaRefRank(ReachableBasicBlock bb, int i, SsaSourceVariable v, RefKind k) {
i = rank[result](int j | ssaRef(bb, j, v, _)) and
ssaRef(bb, i, v, k)
}
/**
* Gets the minimum rank of a read in `bb` such that all references to `v` between that
* read and the read at index `i` are reads (and not writes).
*/
private int rewindReads(ReachableBasicBlock bb, int i, SsaSourceVariable v) {
exists(int r | r = ssaRefRank(bb, i, v, ReadRef()) |
exists(int j, RefKind k | r - 1 = ssaRefRank(bb, j, v, k) |
k = ReadRef() and result = rewindReads(bb, j, v)
or
k = WriteRef() and result = r
)
or
r = 1 and result = r
)
}
/**
* Gets the SSA definition of `v` in `bb` that reaches the read of `v` at node `i`, if any.
*/
private SsaDefinition getLocalDefinition(ReachableBasicBlock bb, int i, SsaSourceVariable v) {
exists(int r | r = rewindReads(bb, i, v) |
exists(int j | result.definesAt(bb, j, v) and ssaRefRank(bb, j, v, _) = r - 1)
)
}
/**
* Gets an SSA definition of `v` that reaches the end of the immediate dominator of `bb`.
*/
pragma[noinline]
private SsaDefinition getDefReachingEndOfImmediateDominator(
ReachableBasicBlock bb, SsaSourceVariable v
) {
result = getDefReachingEndOf(bb.getImmediateDominator(), v)
}
/**
* Gets an SSA definition of `v` that reaches the end of basic block `bb`.
*/
cached
SsaDefinition getDefReachingEndOf(ReachableBasicBlock bb, SsaSourceVariable v) {
exists(int lastRef | lastRef = max(int i | ssaRef(bb, i, v, _)) |
result = getLocalDefinition(bb, lastRef, v)
or
result.definesAt(bb, lastRef, v) and
liveAtSuccEntry(bb, v)
)
or
// In SSA form, the (unique) reaching definition of a use is the closest
// definition that dominates the use. If two definitions dominate a node
// then one must dominate the other, so we can find the reaching definition
// by following the idominance relation backwards.
result = getDefReachingEndOfImmediateDominator(bb, v) and
not exists(SsaDefinition ssa | ssa.definesAt(bb, _, v)) and
liveAtSuccEntry(bb, v)
}
/**
* Gets the unique SSA definition of `v` whose value reaches the `i`th node of `bb`,
* which is a use of `v`.
*/
cached
SsaDefinition getDefinition(ReachableBasicBlock bb, int i, SsaSourceVariable v) {
result = getLocalDefinition(bb, i, v)
or
rewindReads(bb, i, v) = 1 and result = getDefReachingEndOf(bb.getImmediateDominator(), v)
}
private module AdjacentUsesImpl {
/** Holds if `v` is defined or used in `b`. */
private predicate varOccursInBlock(SsaSourceVariable v, ReachableBasicBlock b) {
ssaRef(b, _, v, _)
}
/** Holds if `v` occurs in `b` or one of `b`'s transitive successors. */
private predicate blockPrecedesVar(SsaSourceVariable v, ReachableBasicBlock b) {
varOccursInBlock(v, b)
or
exists(getDefReachingEndOf(b, v))
}
module SsaInput implements SsaImplCommon::InputSig<Location, BasicBlock> {
class SourceVariable = SsaSourceVariable;
/**
* Holds if `v` occurs in `b1` and `b2` is one of `b1`'s successors.
* 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.
*
* Factored out of `varBlockReaches` to force join order compared to the larger
* set `blockPrecedesVar(v, b2)`.
* Certain writes are explicit definitions; uncertain writes are captures.
*/
pragma[noinline]
private predicate varBlockReachesBaseCand(
SsaSourceVariable v, ReachableBasicBlock b1, ReachableBasicBlock b2
) {
varOccursInBlock(v, b1) and
b2 = b1.getASuccessor(_)
}
/**
* Holds if `b2` is a transitive successor of `b1` and `v` occurs in `b1` and
* in `b2` or one of its transitive successors but not in any block on the path
* between `b1` and `b2`. Unlike `varBlockReaches` this may include blocks `b2`
* where `v` is dead.
*
* Factored out of `varBlockReaches` to force join order compared to the larger
* set `blockPrecedesVar(v, b2)`.
*/
pragma[noinline]
private predicate varBlockReachesRecCand(
SsaSourceVariable v, ReachableBasicBlock b1, ReachableBasicBlock mid, ReachableBasicBlock b2
) {
varBlockReaches(v, b1, mid) and
not varOccursInBlock(v, mid) and
b2 = mid.getASuccessor(_)
}
/**
* Holds if `b2` is a transitive successor of `b1` and `v` occurs in `b1` and
* in `b2` or one of its transitive successors but not in any block on the path
* between `b1` and `b2`.
*/
private predicate varBlockReaches(
SsaSourceVariable v, ReachableBasicBlock b1, ReachableBasicBlock b2
) {
varBlockReachesBaseCand(v, b1, b2) and
blockPrecedesVar(v, b2)
predicate variableWrite(BasicBlock bb, int i, SourceVariable v, boolean certain) {
defAt(bb, i, v) and certain = true
or
varBlockReachesRecCand(v, b1, _, b2) and
blockPrecedesVar(v, b2)
mayCapture(bb, i, v) and certain = false
}
/**
* Holds if `b2` is a transitive successor of `b1` and `v` occurs in `b1` and
* `b2` but not in any block on the path between `b1` and `b2`.
* Holds if the `i`th node of basic block `bb` reads source variable `v`.
*/
private predicate varBlockStep(
SsaSourceVariable v, ReachableBasicBlock b1, ReachableBasicBlock b2
) {
varBlockReaches(v, b1, b2) and
varOccursInBlock(v, b2)
predicate variableRead(BasicBlock bb, int i, SourceVariable v, boolean certain) {
useAt(bb, i, v) and certain = true
}
/**
* Gets the maximum rank among all SSA references to `v` in basic block `bb`.
*/
private int maxSsaRefRank(ReachableBasicBlock bb, SsaSourceVariable v) {
result = max(ssaRefRank(bb, _, v, _))
}
/**
* Holds if `v` occurs at index `i1` in `b1` and at index `i2` in `b2` and
* there is a path between them without any occurrence of `v`.
*/
pragma[nomagic]
predicate adjacentVarRefs(
SsaSourceVariable v, ReachableBasicBlock b1, int i1, ReachableBasicBlock b2, int i2
) {
exists(int rankix |
b1 = b2 and
ssaRefRank(b1, i1, v, _) = rankix and
ssaRefRank(b2, i2, v, _) = rankix + 1
)
or
maxSsaRefRank(b1, v) = ssaRefRank(b1, i1, v, _) and
varBlockStep(v, b1, b2) and
ssaRefRank(b2, i2, v, _) = 1
}
predicate variableUse(SsaSourceVariable v, IR::Instruction use, ReachableBasicBlock bb, int i) {
bb.getNode(i) = use and
exists(SsaVariable sv |
sv.getSourceVariable() = v and
use = sv.getAUse()
)
}
}
private import AdjacentUsesImpl
/**
* Holds if the value defined at `def` can reach `use` without passing through
* any other uses, but possibly through phi nodes.
*/
cached
predicate firstUse(SsaDefinition def, IR::Instruction use) {
exists(SsaSourceVariable v, ReachableBasicBlock b1, int i1, ReachableBasicBlock b2, int i2 |
adjacentVarRefs(v, b1, i1, b2, i2) and
def.definesAt(b1, i1, v) and
variableUse(v, use, b2, i2)
)
or
exists(
SsaSourceVariable v, SsaPhiNode redef, ReachableBasicBlock b1, int i1, ReachableBasicBlock b2,
int i2
|
adjacentVarRefs(v, b1, i1, b2, i2) and
def.definesAt(b1, i1, v) and
redef.definesAt(b2, i2, v) and
firstUse(redef, use)
)
}
/**
* Holds if `use1` and `use2` form an adjacent use-use-pair of the same SSA
* variable, that is, the value read in `use1` can reach `use2` without passing
* through any other use or any SSA definition of the variable.
*/
cached
predicate adjacentUseUseSameVar(IR::Instruction use1, IR::Instruction use2) {
exists(SsaSourceVariable v, ReachableBasicBlock b1, int i1, ReachableBasicBlock b2, int i2 |
adjacentVarRefs(v, b1, i1, b2, i2) and
variableUse(v, use1, b1, i1) and
variableUse(v, use2, b2, i2)
)
}
/**
* Holds if `use1` and `use2` form an adjacent use-use-pair of the same
* `SsaSourceVariable`, that is, the value read in `use1` can reach `use2`
* without passing through any other use or any SSA definition of the variable
* except for phi nodes and uncertain implicit updates.
*/
cached
predicate adjacentUseUse(IR::Instruction use1, IR::Instruction use2) {
adjacentUseUseSameVar(use1, use2)
or
exists(
SsaSourceVariable v, SsaPhiNode def, ReachableBasicBlock b1, int i1, ReachableBasicBlock b2,
int i2
|
adjacentVarRefs(v, b1, i1, b2, i2) and
variableUse(v, use1, b1, i1) and
def.definesAt(b2, i2, v) and
firstUse(def, use2)
)
}
}
import Internal
import SsaImplCommon::Make<Location, BasicBlocks::Cfg, SsaInput> as Impl
final class Definition = Impl::Definition;
final class WriteDefinition = Impl::WriteDefinition;
final class UncertainWriteDefinition = Impl::UncertainWriteDefinition;
final class PhiNode = Impl::PhiNode;
module Consistency = Impl::Consistency;
/**
* NB: This predicate should be cached.
*
* Holds if the SSA definition of `v` at `def` reaches a read at index `i` in
* basic block `bb`.
*/
cached
predicate ssaDefReachesRead(SsaSourceVariable v, Definition def, BasicBlock bb, int i) {
Impl::ssaDefReachesRead(v, def, bb, i)
}
/**
* NB: This predicate should be cached.
*
* Holds if the SSA definition of `v` at `def` reaches the end of basic block `bb`.
*/
cached
predicate ssaDefReachesEndOfBlock(BasicBlock bb, Definition def, SsaSourceVariable v) {
Impl::ssaDefReachesEndOfBlock(bb, def, v)
}
/**
* NB: This predicate should be cached.
*
* Holds if `inp` is an input to the phi node `phi` along the edge originating in `bb`.
*/
cached
predicate phiHasInputFromBlock(PhiNode phi, Definition inp, BasicBlock bb) {
Impl::phiHasInputFromBlock(phi, inp, bb)
}
/**
* NB: This predicate should be cached.
*
* Holds if `def` reaches the first use `use` without going through any other use,
* but possibly through phi nodes.
*/
cached
predicate firstUse(Definition def, IR::Instruction use) {
exists(BasicBlock bb, int i |
Impl::firstUse(def, bb, i, _) and
use = bb.getNode(i)
)
}
/**
* NB: This predicate should be cached.
*
* Holds if `use1` and `use2` form an adjacent use-use-pair of the same SSA
* variable, that is, the value read in `use1` can reach `use2` without passing
* through any other use or any SSA definition of the variable except for phi nodes
* and uncertain implicit updates.
*/
cached
predicate adjacentUseUse(IR::Instruction use1, IR::Instruction use2) {
exists(BasicBlock bb1, int i1, BasicBlock bb2, int i2 |
Impl::adjacentUseUse(bb1, i1, bb2, i2, _, _) and
use1 = bb1.getNode(i1) and
use2 = bb2.getNode(i2)
)
}