From b681a10bfe6d6eec2bc583fdcdd21322b6e2bc64 Mon Sep 17 00:00:00 2001 From: Mathias Vorreiter Pedersen Date: Mon, 23 May 2022 17:56:29 +0100 Subject: [PATCH] Swift: Add shared SSA library. --- .../swift/dataflow/internal/SsaImplCommon.qll | 659 ++++++++++++++++++ .../dataflow/internal/SsaImplSpecific.qll | 34 + 2 files changed, 693 insertions(+) create mode 100644 swift/ql/lib/codeql/swift/dataflow/internal/SsaImplCommon.qll create mode 100644 swift/ql/lib/codeql/swift/dataflow/internal/SsaImplSpecific.qll diff --git a/swift/ql/lib/codeql/swift/dataflow/internal/SsaImplCommon.qll b/swift/ql/lib/codeql/swift/dataflow/internal/SsaImplCommon.qll new file mode 100644 index 00000000000..eed0d050735 --- /dev/null +++ b/swift/ql/lib/codeql/swift/dataflow/internal/SsaImplCommon.qll @@ -0,0 +1,659 @@ +/** + * 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 `df` is in the dominance frontier of `bb`. + * + * This is equivalent to: + * + * ```ql + * bb = getImmediateBasicBlockDominator*(getABasicBlockPredecessor(df)) and + * not bb = getImmediateBasicBlockDominator+(df) + * ``` + */ +private predicate inDominanceFrontier(BasicBlock bb, BasicBlock df) { + bb = getABasicBlockPredecessor(df) and not bb = getImmediateBasicBlockDominator(df) + or + exists(BasicBlock prev | inDominanceFrontier(prev, df) | + bb = getImmediateBasicBlockDominator(prev) and + not bb = getImmediateBasicBlockDominator(df) + ) +} + +/** + * Holds if `bb` is in the dominance frontier of a block containing a + * definition of `v`. + */ +pragma[noinline] +private predicate inDefDominanceFrontier(BasicBlock bb, SourceVariable v) { + exists(BasicBlock defbb, Definition def | + def.definesAt(v, defbb, _) and + inDominanceFrontier(defbb, bb) + ) +} + +cached +newtype TDefinition = + TWriteDef(SourceVariable v, BasicBlock bb, int i) { + variableWrite(bb, i, v, _) and + liveAfterWrite(bb, i, v) + } or + TPhiNode(SourceVariable v, BasicBlock bb) { + inDefDominanceFrontier(bb, v) and + liveAtEntry(bb, v) + } + +private module SsaDefReaches { + newtype TSsaRefKind = + 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()) + ) + } + + /** + * 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) + ) + } +} + +/** Provides a set of consistency queries. */ +module Consistency { + abstract class RelevantDefinition extends Definition { + abstract predicate hasLocationInfo( + string filepath, int startline, int startcolumn, int endline, int endcolumn + ); + } + + query predicate nonUniqueDef(RelevantDefinition def, SourceVariable v, BasicBlock bb, int i) { + ssaDefReachesRead(v, def, bb, i) and + not exists(unique(Definition def0 | ssaDefReachesRead(v, def0, bb, i))) + } + + query predicate readWithoutDef(SourceVariable v, BasicBlock bb, int i) { + variableRead(bb, i, v, _) and + not ssaDefReachesRead(v, _, bb, i) + } + + query predicate deadDef(RelevantDefinition def, SourceVariable v) { + v = def.getSourceVariable() and + not ssaDefReachesRead(_, def, _, _) and + not phiHasInputFromBlock(_, def, _) and + not uncertainWriteDefinitionInput(_, def) + } + + query predicate notDominatedByDef(RelevantDefinition def, SourceVariable v, BasicBlock bb, int i) { + exists(BasicBlock bbDef, int iDef | def.definesAt(v, bbDef, iDef) | + ssaDefReachesReadWithinBlock(v, def, bb, i) and + (bb != bbDef or i < iDef) + or + ssaDefReachesRead(v, def, bb, i) and + not ssaDefReachesReadWithinBlock(v, def, bb, i) and + not def.definesAt(v, getImmediateBasicBlockDominator*(bb), _) + ) + } +} diff --git a/swift/ql/lib/codeql/swift/dataflow/internal/SsaImplSpecific.qll b/swift/ql/lib/codeql/swift/dataflow/internal/SsaImplSpecific.qll new file mode 100644 index 00000000000..0eed5427740 --- /dev/null +++ b/swift/ql/lib/codeql/swift/dataflow/internal/SsaImplSpecific.qll @@ -0,0 +1,34 @@ +/** Provides the Swift specific parameters for `SsaImplCommon.qll`. */ + +private import swift +private import codeql.swift.controlflow.BasicBlocks as BasicBlocks +private import codeql.swift.controlflow.ControlFlowGraph + +class BasicBlock = BasicBlocks::BasicBlock; + +BasicBlock getImmediateBasicBlockDominator(BasicBlock bb) { result = bb.getImmediateDominator() } + +BasicBlock getABasicBlockSuccessor(BasicBlock bb) { result = bb.getASuccessor() } + +class ExitBasicBlock = BasicBlocks::ExitBasicBlock; + +class SourceVariable = VarDecl; + +predicate variableWrite(BasicBlock bb, int i, SourceVariable v, boolean certain) { + exists(AssignExpr assign | + bb.getNode(i).getNode() = assign and + assign.getDest() = v.getAnAccess() and + certain = true + ) +} + +private predicate isLValue(DeclRefExpr ref) { any(AssignExpr assign).getDest() = ref } + +predicate variableRead(BasicBlock bb, int i, SourceVariable v, boolean certain) { + exists(DeclRefExpr ref | + not isLValue(ref) and + bb.getNode(i).getNode() = ref and + v = ref.getDecl() and + certain = true + ) +}