From 3822d149af7f46105d9800184d2a6c339770971a Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Tue, 11 Feb 2025 11:22:46 +0100 Subject: [PATCH 01/30] SSA: Elaborate qldoc. --- shared/ssa/codeql/ssa/Ssa.qll | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/shared/ssa/codeql/ssa/Ssa.qll b/shared/ssa/codeql/ssa/Ssa.qll index dacc323f43e6..62a48c220664 100644 --- a/shared/ssa/codeql/ssa/Ssa.qll +++ b/shared/ssa/codeql/ssa/Ssa.qll @@ -189,6 +189,14 @@ module Make Input> { /** * 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 = From 36613e150b49797c9d6c9f03a3ab386ccd6fc076 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Tue, 11 Feb 2025 11:23:29 +0100 Subject: [PATCH 02/30] SSA: Remove superfluous conjunct (implied by refRank). --- shared/ssa/codeql/ssa/Ssa.qll | 1 - 1 file changed, 1 deletion(-) diff --git a/shared/ssa/codeql/ssa/Ssa.qll b/shared/ssa/codeql/ssa/Ssa.qll index 62a48c220664..d715bfa4d736 100644 --- a/shared/ssa/codeql/ssa/Ssa.qll +++ b/shared/ssa/codeql/ssa/Ssa.qll @@ -237,7 +237,6 @@ module Make Input> { rnk = maxRefRank(bb, v) and liveAtExit(bb, v) or - ref(bb, i, v, kind) and kind = Read(_) or exists(RefKind nextKind | From b62432fc80884220631d718f78a84fadfb276d34 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Fri, 14 Feb 2025 14:36:52 +0100 Subject: [PATCH 03/30] SSA: Remove superfluous boolean. --- shared/ssa/codeql/ssa/Ssa.qll | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/shared/ssa/codeql/ssa/Ssa.qll b/shared/ssa/codeql/ssa/Ssa.qll index d715bfa4d736..743aa6cec9b7 100644 --- a/shared/ssa/codeql/ssa/Ssa.qll +++ b/shared/ssa/codeql/ssa/Ssa.qll @@ -123,18 +123,18 @@ module Make Input> { * (certain or uncertain) writes. */ private newtype TRefKind = - Read(boolean certain) { certain in [false, true] } or + Read() 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 + ")") + this = Read() and result = "read" or exists(boolean certain | this = Write(certain) and result = "write (" + certain + ")") } int getOrder() { - this = Read(_) and + this = Read() and result = 0 or this = Write(_) and @@ -146,7 +146,7 @@ module Make Input> { * Holds if the `i`th node of basic block `bb` is a reference to `v` of kind `k`. */ predicate ref(BasicBlock bb, int i, SourceVariable v, RefKind k) { - exists(boolean certain | variableRead(bb, i, v, certain) | k = Read(certain)) + variableRead(bb, i, v, _) and k = Read() or exists(boolean certain | variableWrite(bb, i, v, certain) | k = Write(certain)) } @@ -183,7 +183,7 @@ module Make Input> { } predicate lastRefIsRead(BasicBlock bb, SourceVariable v) { - maxRefRank(bb, v) = refRank(bb, _, v, Read(_)) + maxRefRank(bb, v) = refRank(bb, _, v, Read()) } /** @@ -213,7 +213,7 @@ module Make Input> { */ 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) + 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` @@ -237,7 +237,7 @@ module Make Input> { rnk = maxRefRank(bb, v) and liveAtExit(bb, v) or - kind = Read(_) + kind = Read() or exists(RefKind nextKind | liveAtRank(bb, _, v, rnk + 1) and From c5e28842fbba5ef026aaa142ee745d52c9719836 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Fri, 14 Feb 2025 17:07:10 +0100 Subject: [PATCH 04/30] SSA: Remove superfluous column from liveAtRank. --- shared/ssa/codeql/ssa/Ssa.qll | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/shared/ssa/codeql/ssa/Ssa.qll b/shared/ssa/codeql/ssa/Ssa.qll index 743aa6cec9b7..efd03cf8e9c3 100644 --- a/shared/ssa/codeql/ssa/Ssa.qll +++ b/shared/ssa/codeql/ssa/Ssa.qll @@ -229,18 +229,17 @@ module Make Input> { } /** - * Holds if variable `v` is live in basic block `bb` at index `i`. - * The rank of `i` is `rnk` as defined by `refRank()`. + * Holds if variable `v` is live in basic block `bb` at rank `rnk`. */ - private predicate liveAtRank(BasicBlock bb, int i, SourceVariable v, int rnk) { - exists(RefKind kind | rnk = refRank(bb, i, v, kind) | + 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 + liveAtRank(bb, v, rnk + 1) and rnk + 1 = refRank(bb, _, v, nextKind) and nextKind != Write(true) ) @@ -252,7 +251,7 @@ module Make Input> { * 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)) + exists(int rnk | rnk = refRank(bb, i, v, Write(_)) | liveAtRank(bb, v, rnk)) } } From 5723d274285e329894ed971f628e01fc307c9aff Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Fri, 14 Feb 2025 15:42:47 +0100 Subject: [PATCH 05/30] SSA: Make inReadDominanceFrontier a bit smaller without affecting phi-read creation. --- shared/ssa/codeql/ssa/Ssa.qll | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/shared/ssa/codeql/ssa/Ssa.qll b/shared/ssa/codeql/ssa/Ssa.qll index efd03cf8e9c3..0f50680c2492 100644 --- a/shared/ssa/codeql/ssa/Ssa.qll +++ b/shared/ssa/codeql/ssa/Ssa.qll @@ -182,10 +182,6 @@ module Make Input> { not result + 1 = refRank(bb, _, v, _) } - predicate lastRefIsRead(BasicBlock bb, SourceVariable v) { - maxRefRank(bb, v) = refRank(bb, _, v, Read()) - } - /** * Gets the (1-based) rank of the first reference to `v` inside basic block `bb` * that is either a read or a certain write. @@ -295,7 +291,8 @@ module Make Input> { pragma[nomagic] private predicate inReadDominanceFrontier(BasicBlock bb, SourceVariable v) { exists(BasicBlock readbb | inDominanceFrontier(readbb, bb) | - lastRefIsRead(readbb, v) + variableRead(readbb, _, v, _) and + not variableWrite(readbb, _, v, _) or exists(TPhiReadNode(v, readbb)) and not ref(readbb, _, v, _) From f80cd97232f3fe8e30b4e45714a86b663789b9ae Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Mon, 17 Feb 2025 09:55:03 +0100 Subject: [PATCH 06/30] SSA: Factor out phi-read construction in its own predicate. --- shared/ssa/codeql/ssa/Ssa.qll | 24 +++++++++++++++++------- 1 file changed, 17 insertions(+), 7 deletions(-) diff --git a/shared/ssa/codeql/ssa/Ssa.qll b/shared/ssa/codeql/ssa/Ssa.qll index 0f50680c2492..9229fab20291 100644 --- a/shared/ssa/codeql/ssa/Ssa.qll +++ b/shared/ssa/codeql/ssa/Ssa.qll @@ -294,11 +294,26 @@ module Make Input> { variableRead(readbb, _, v, _) and not variableWrite(readbb, _, v, _) or - exists(TPhiReadNode(v, readbb)) and + synthPhiRead(readbb, v) and not ref(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 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) { @@ -309,12 +324,7 @@ module Make Input> { 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, _) - } + TPhiReadNode(SourceVariable v, BasicBlock bb) { synthPhiRead(bb, v) } private class TDefinition = TWriteDef or TPhiNode; From 81b303516057ea4024d6e2c8a94c71a9aefa557e Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Mon, 17 Feb 2025 10:01:58 +0100 Subject: [PATCH 07/30] SSA: Inline predicate --- shared/ssa/codeql/ssa/Ssa.qll | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/shared/ssa/codeql/ssa/Ssa.qll b/shared/ssa/codeql/ssa/Ssa.qll index 9229fab20291..994c1c795ea3 100644 --- a/shared/ssa/codeql/ssa/Ssa.qll +++ b/shared/ssa/codeql/ssa/Ssa.qll @@ -376,7 +376,10 @@ module Make Input> { variableRead(bb, i, v, _) and k = SsaActualRead() or - any(DefinitionExt def).definesAt(v, bb, i, k) + any(Definition def).definesAt(v, bb, i) and + k = SsaDef() + or + synthPhiRead(bb, v) and i = -1 and k = SsaPhiRead() } /** From 613323ee3ae16ab169d3300a9c2f2f06f731898a Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Mon, 17 Feb 2025 10:35:55 +0100 Subject: [PATCH 08/30] SSA: Copy parts of SsaDefReaches verbatim to new module. --- shared/ssa/codeql/ssa/Ssa.qll | 120 ++++++++++++++++++++++++++++++++++ 1 file changed, 120 insertions(+) diff --git a/shared/ssa/codeql/ssa/Ssa.qll b/shared/ssa/codeql/ssa/Ssa.qll index 994c1c795ea3..4e4b5229e216 100644 --- a/shared/ssa/codeql/ssa/Ssa.qll +++ b/shared/ssa/codeql/ssa/Ssa.qll @@ -328,6 +328,126 @@ module Make Input> { private class TDefinition = TWriteDef or TPhiNode; + private module SsaDefReachesNew { + newtype TSsaRefKind = + SsaActualRead() or + SsaPhiRead() or + SsaDef() + + class SsaRead = SsaActualRead or SsaPhiRead; + + class SsaDefExt = SsaDef or SsaPhiRead; + + SsaDefExt ssaDefExt() { any() } + + /** + * A classification of SSA variable references into reads and definitions. + */ + 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::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 + any(Definition def).definesAt(v, bb, i) and + k = SsaDef() + or + synthPhiRead(bb, v) and i = -1 and k = SsaPhiRead() + } + + 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, 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`. + */ + 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()) + ) + } + } + private module SsaDefReaches { newtype TSsaRefKind = SsaActualRead() or From ea08c6032613c475d3357d8c002ac5c73ca594ed Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Mon, 17 Feb 2025 10:43:35 +0100 Subject: [PATCH 09/30] SSA: Copy 3 predicates from the outer scope verbatim into the new Reaches module. --- shared/ssa/codeql/ssa/Ssa.qll | 46 +++++++++++++++++++++++++++++++++++ 1 file changed, 46 insertions(+) diff --git a/shared/ssa/codeql/ssa/Ssa.qll b/shared/ssa/codeql/ssa/Ssa.qll index 4e4b5229e216..4245944aeef1 100644 --- a/shared/ssa/codeql/ssa/Ssa.qll +++ b/shared/ssa/codeql/ssa/Ssa.qll @@ -436,6 +436,37 @@ module Make Input> { rnk = ssaRefRank(bb, _, v, SsaActualRead()) } + pragma[nomagic] + predicate liveThroughExt(BasicBlock bb, SourceVariable v) { + liveAtExit(bb, v) and + not ssaRef(bb, _, v, ssaDefExt()) + } + + /** + * 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 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 + 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. + ssaDefReachesEndOfBlockExt(getImmediateBasicBlockDominator(bb), def, pragma[only_bind_into](v)) and + liveThroughExt(bb, pragma[only_bind_into](v)) + } + /** * 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`. @@ -446,6 +477,21 @@ module Make Input> { rnk = ssaRefRank(bb, i, v, SsaActualRead()) ) } + + /** + * 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`. + */ + 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) + } } private module SsaDefReaches { From 6e272d07af9da39f5e4ef712015839ae72a25223 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Mon, 17 Feb 2025 12:25:11 +0100 Subject: [PATCH 10/30] SSA: Ignore phi-reads in the new def-reaches module. --- shared/ssa/codeql/ssa/Ssa.qll | 48 ++++++++++++----------------------- 1 file changed, 16 insertions(+), 32 deletions(-) diff --git a/shared/ssa/codeql/ssa/Ssa.qll b/shared/ssa/codeql/ssa/Ssa.qll index 4245944aeef1..6547f2805c60 100644 --- a/shared/ssa/codeql/ssa/Ssa.qll +++ b/shared/ssa/codeql/ssa/Ssa.qll @@ -331,15 +331,8 @@ module Make Input> { private module SsaDefReachesNew { newtype TSsaRefKind = SsaActualRead() or - SsaPhiRead() or SsaDef() - class SsaRead = SsaActualRead or SsaPhiRead; - - class SsaDefExt = SsaDef or SsaPhiRead; - - SsaDefExt ssaDefExt() { any() } - /** * A classification of SSA variable references into reads and definitions. */ @@ -348,15 +341,12 @@ module Make Input> { this = SsaActualRead() and result = "SsaActualRead" or - this = SsaPhiRead() and - result = "SsaPhiRead" - or this = SsaDef() and result = "SsaDef" } int getOrder() { - this instanceof SsaRead and + this = SsaActualRead() and result = 0 or this = SsaDef() and @@ -366,10 +356,10 @@ module Make Input> { /** * 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()`). + * either a read (when `k` is `SsaActualRead()`) or an SSA definition (when + * `k` is `SsaDef()`). * - * Unlike `Liveness::ref`, this includes `phi` (read) nodes. + * Unlike `Liveness::ref`, this includes `phi` nodes. */ pragma[nomagic] predicate ssaRef(BasicBlock bb, int i, SourceVariable v, SsaRefKind k) { @@ -378,8 +368,6 @@ module Make Input> { or any(Definition def).definesAt(v, bb, i) and k = SsaDef() - or - synthPhiRead(bb, v) and i = -1 and k = SsaPhiRead() } private newtype OrderedSsaRefIndex = @@ -426,10 +414,10 @@ module Make Input> { * Holds if the SSA definition `def` reaches rank index `rnk` in its own * basic block `bb`. */ - predicate ssaDefReachesRank(BasicBlock bb, DefinitionExt def, int rnk, SourceVariable v) { + predicate ssaDefReachesRank(BasicBlock bb, Definition def, int rnk, SourceVariable v) { exists(int i | - rnk = ssaRefRank(bb, i, v, ssaDefExt()) and - def.definesAt(v, bb, i, _) + rnk = ssaRefRank(bb, i, v, SsaDef()) and + def.definesAt(v, bb, i) ) or ssaDefReachesRank(bb, def, rnk - 1, v) and @@ -437,20 +425,18 @@ module Make Input> { } pragma[nomagic] - predicate liveThroughExt(BasicBlock bb, SourceVariable v) { + private predicate liveThrough(BasicBlock bb, SourceVariable v) { liveAtExit(bb, v) and - not ssaRef(bb, _, v, ssaDefExt()) + 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 ssaDefReachesEndOfBlockExt(BasicBlock bb, DefinitionExt def, SourceVariable v) { + predicate ssaDefReachesEndOfBlock(BasicBlock bb, Definition 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 @@ -463,15 +449,15 @@ module Make 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. - ssaDefReachesEndOfBlockExt(getImmediateBasicBlockDominator(bb), def, pragma[only_bind_into](v)) and - liveThroughExt(bb, pragma[only_bind_into](v)) + ssaDefReachesEndOfBlock(getImmediateBasicBlockDominator(bb), def, pragma[only_bind_into](v)) and + liveThrough(bb, pragma[only_bind_into](v)) } /** - * Holds if the SSA definition of `v` at `def` reaches index `i` in the same + * 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, DefinitionExt def, BasicBlock bb, int i) { + predicate ssaDefReachesReadWithinBlock(SourceVariable v, Definition def, BasicBlock bb, int i) { exists(int rnk | ssaDefReachesRank(bb, def, rnk, v) and rnk = ssaRefRank(bb, i, v, SsaActualRead()) @@ -479,17 +465,15 @@ module Make Input> { } /** - * 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`. */ pragma[nomagic] - predicate ssaDefReachesReadExt(SourceVariable v, DefinitionExt def, BasicBlock bb, int i) { + predicate ssaDefReachesRead(SourceVariable v, Definition def, BasicBlock bb, int i) { ssaDefReachesReadWithinBlock(v, def, bb, i) or ssaRef(bb, i, v, SsaActualRead()) and - ssaDefReachesEndOfBlockExt(getABasicBlockPredecessor(bb), def, v) and + ssaDefReachesEndOfBlock(getABasicBlockPredecessor(bb), def, v) and not ssaDefReachesReadWithinBlock(v, _, bb, i) } } From 77ccff6be8e55af937e25d09e2eb2ebf735e2369 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Mon, 17 Feb 2025 12:33:18 +0100 Subject: [PATCH 11/30] SSA: Replace exported def-reaches predicates (behaviour-preserving). --- shared/ssa/codeql/ssa/Ssa.qll | 27 ++------------------------- 1 file changed, 2 insertions(+), 25 deletions(-) diff --git a/shared/ssa/codeql/ssa/Ssa.qll b/shared/ssa/codeql/ssa/Ssa.qll index 6547f2805c60..ed988348867c 100644 --- a/shared/ssa/codeql/ssa/Ssa.qll +++ b/shared/ssa/codeql/ssa/Ssa.qll @@ -796,28 +796,12 @@ module Make Input> { 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) - ) - } + predicate ssaDefReachesEndOfBlock = SsaDefReachesNew::ssaDefReachesEndOfBlock/3; /** * NB: If this predicate is exposed, it should be cached. @@ -870,14 +854,7 @@ module Make Input> { * * 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, SsaActualRead()) and - ssaDefReachesEndOfBlock(getABasicBlockPredecessor(bb), def, v) and - not exists(Definition other | ssaDefReachesReadWithinBlock(v, other, bb, i)) - } + predicate ssaDefReachesRead = SsaDefReachesNew::ssaDefReachesRead/4; /** * NB: If this predicate is exposed, it should be cached. From 7e441d9ecaf9ace22865661991334382db268e6c Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Mon, 17 Feb 2025 12:36:18 +0100 Subject: [PATCH 12/30] SSA: Fold getImmediateBasicBlockDominator into loop-invariant predicate. --- shared/ssa/codeql/ssa/Ssa.qll | 25 ++++++++++++++++--------- 1 file changed, 16 insertions(+), 9 deletions(-) diff --git a/shared/ssa/codeql/ssa/Ssa.qll b/shared/ssa/codeql/ssa/Ssa.qll index ed988348867c..c98182d36752 100644 --- a/shared/ssa/codeql/ssa/Ssa.qll +++ b/shared/ssa/codeql/ssa/Ssa.qll @@ -424,8 +424,13 @@ module Make Input> { rnk = ssaRefRank(bb, _, v, SsaActualRead()) } + /** + * 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 bb, SourceVariable v) { + private predicate liveThrough(BasicBlock idom, BasicBlock bb, SourceVariable v) { + idom = getImmediateBasicBlockDominator(bb) and liveAtExit(bb, v) and not ssaRef(bb, _, v, SsaDef()) } @@ -443,14 +448,16 @@ module Make Input> { 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)) + 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) + ) } /** From a4fee2e299a681694abd2110749c67b5b986c087 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Mon, 17 Feb 2025 12:37:58 +0100 Subject: [PATCH 13/30] SSA: Minor perf tweak to reduce tuple duplication. --- shared/ssa/codeql/ssa/Ssa.qll | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/shared/ssa/codeql/ssa/Ssa.qll b/shared/ssa/codeql/ssa/Ssa.qll index c98182d36752..835d3698dbbf 100644 --- a/shared/ssa/codeql/ssa/Ssa.qll +++ b/shared/ssa/codeql/ssa/Ssa.qll @@ -480,7 +480,7 @@ module Make Input> { ssaDefReachesReadWithinBlock(v, def, bb, i) or ssaRef(bb, i, v, SsaActualRead()) and - ssaDefReachesEndOfBlock(getABasicBlockPredecessor(bb), def, v) and + ssaDefReachesEndOfBlock(getImmediateBasicBlockDominator(bb), def, v) and not ssaDefReachesReadWithinBlock(v, _, bb, i) } } From d5ac5b4654f55803349c751fce5e0467c65ae984 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Mon, 17 Feb 2025 12:54:42 +0100 Subject: [PATCH 14/30] SSA: Replace uncertainWriteDefinitionInput implementation. This yields a tiny bit of additional tuples consistent with the prior Java implementation. --- shared/ssa/codeql/ssa/Ssa.qll | 23 +++++++++++++++++------ 1 file changed, 17 insertions(+), 6 deletions(-) diff --git a/shared/ssa/codeql/ssa/Ssa.qll b/shared/ssa/codeql/ssa/Ssa.qll index 835d3698dbbf..6fedceb15f53 100644 --- a/shared/ssa/codeql/ssa/Ssa.qll +++ b/shared/ssa/codeql/ssa/Ssa.qll @@ -359,13 +359,17 @@ module Make Input> { * either a read (when `k` is `SsaActualRead()`) or an SSA definition (when * `k` is `SsaDef()`). * - * Unlike `Liveness::ref`, this includes `phi` nodes. + * Unlike `Liveness::ref`, this includes `phi` nodes and pseudo-reads + * associated with uncertain writes. */ pragma[nomagic] predicate ssaRef(BasicBlock bb, int i, SourceVariable v, SsaRefKind k) { variableRead(bb, i, v, _) and k = SsaActualRead() or + variableWrite(bb, i, v, false) and + k = SsaActualRead() + or any(Definition def).definesAt(v, bb, i) and k = SsaDef() } @@ -483,6 +487,13 @@ module Make Input> { ssaDefReachesEndOfBlock(getImmediateBasicBlockDominator(bb), 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 SsaDefReaches { @@ -861,7 +872,10 @@ module Make Input> { * * Same as `ssaDefReachesReadExt`, but ignores phi-reads. */ - predicate ssaDefReachesRead = SsaDefReachesNew::ssaDefReachesRead/4; + predicate ssaDefReachesRead(SourceVariable v, Definition def, BasicBlock bb, int i) { + SsaDefReachesNew::ssaDefReachesRead(v, def, bb, i) and + variableRead(bb, i, v, _) + } /** * NB: If this predicate is exposed, it should be cached. @@ -994,10 +1008,7 @@ module Make Input> { * `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) - } + predicate uncertainWriteDefinitionInput = SsaDefReachesNew::uncertainWriteDefinitionInput/2; /** Holds if `bb` is a control-flow exit point. */ private predicate exitBlock(BasicBlock bb) { not exists(getABasicBlockSuccessor(bb)) } From 11166fc42dadf43310ae49a86f906fd81ddda0bc Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Mon, 17 Feb 2025 13:03:04 +0100 Subject: [PATCH 15/30] SSA: Restrict phi-read creation to be based on reachable reads. --- shared/ssa/codeql/ssa/Ssa.qll | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/shared/ssa/codeql/ssa/Ssa.qll b/shared/ssa/codeql/ssa/Ssa.qll index 6fedceb15f53..f32f54e966fd 100644 --- a/shared/ssa/codeql/ssa/Ssa.qll +++ b/shared/ssa/codeql/ssa/Ssa.qll @@ -291,7 +291,7 @@ module Make Input> { pragma[nomagic] private predicate inReadDominanceFrontier(BasicBlock bb, SourceVariable v) { exists(BasicBlock readbb | inDominanceFrontier(readbb, bb) | - variableRead(readbb, _, v, _) and + ssaDefReachesRead(v, _, readbb, _) and not variableWrite(readbb, _, v, _) or synthPhiRead(readbb, v) and From 411aff6748bb44c0658680684cb009ae2ebc650e Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Mon, 17 Feb 2025 14:08:16 +0100 Subject: [PATCH 16/30] SSA: Refactor ranking into parameterised module. --- shared/ssa/codeql/ssa/Ssa.qll | 178 +++++++++++++--------------------- 1 file changed, 65 insertions(+), 113 deletions(-) diff --git a/shared/ssa/codeql/ssa/Ssa.qll b/shared/ssa/codeql/ssa/Ssa.qll index f32f54e966fd..f5409db3aef5 100644 --- a/shared/ssa/codeql/ssa/Ssa.qll +++ b/shared/ssa/codeql/ssa/Ssa.qll @@ -114,43 +114,41 @@ module Make Input> { } /** - * Liveness analysis (based on source variables) to restrict the size of the - * SSA representation. + * A classification of variable references into reads and + * (certain or uncertain) writes / definitions. */ - private module Liveness { - /** - * A classification of variable references into reads (of a given kind) and - * (certain or uncertain) writes. - */ - private newtype TRefKind = - Read() or - Write(boolean certain) { certain in [false, true] } - - private class RefKind extends TRefKind { - string toString() { - this = Read() and result = "read" - or - exists(boolean certain | this = Write(certain) and result = "write (" + certain + ")") - } - - int getOrder() { - this = Read() and - result = 0 - or - this = Write(_) and - result = 1 - } + 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" } - /** - * Holds if the `i`th node of basic block `bb` is a reference to `v` of kind `k`. - */ - predicate ref(BasicBlock bb, int i, SourceVariable v, RefKind k) { - variableRead(bb, i, v, _) and k = Read() + int getOrder() { + this = Read() and + result = 0 or - exists(boolean certain | variableWrite(bb, i, v, certain) | k = Write(certain)) + 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 { private newtype OrderedRefIndex = MkOrderedRefIndex(int i, int tag) { exists(RefKind rk | ref(_, i, _, rk) | tag = rk.getOrder()) @@ -168,7 +166,7 @@ module Make Input> { * * Reads are considered before writes when they happen at the same index. */ - private int refRank(BasicBlock bb, int i, SourceVariable v, RefKind k) { + 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) @@ -177,10 +175,27 @@ module Make Input> { ) } - private int maxRefRank(BasicBlock bb, SourceVariable v) { + 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 /** * Gets the (1-based) rank of the first reference to `v` inside basic block `bb` @@ -295,7 +310,7 @@ module Make Input> { not variableWrite(readbb, _, v, _) or synthPhiRead(readbb, v) and - not ref(readbb, _, v, _) + not varRef(readbb, _, v, _) ) } @@ -329,90 +344,27 @@ module Make Input> { private class TDefinition = TWriteDef or TPhiNode; private module SsaDefReachesNew { - newtype TSsaRefKind = - SsaActualRead() or - SsaDef() - - /** - * A classification of SSA variable references into reads and definitions. - */ - class SsaRefKind extends TSsaRefKind { - string toString() { - this = SsaActualRead() and - result = "SsaActualRead" - or - this = SsaDef() and - result = "SsaDef" - } - - int getOrder() { - this = SsaActualRead() 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()`) or an SSA definition (when - * `k` is `SsaDef()`). + * either a read (when `k` is `Read()`) or an SSA definition (when + * `k` is `Def()`). * - * Unlike `Liveness::ref`, this includes `phi` nodes and pseudo-reads + * Unlike `Liveness::varRef`, this includes `phi` nodes and pseudo-reads * associated with uncertain writes. */ pragma[nomagic] - predicate ssaRef(BasicBlock bb, int i, SourceVariable v, SsaRefKind k) { + predicate ssaRef(BasicBlock bb, int i, SourceVariable v, RefKind k) { variableRead(bb, i, v, _) and - k = SsaActualRead() + k = Read() or variableWrite(bb, i, v, false) and - k = SsaActualRead() + k = Read() or any(Definition 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 - ) + k = Def() } - int maxSsaRefRank(BasicBlock bb, SourceVariable v) { - result = ssaRefRank(bb, _, v, _) and - not result + 1 = ssaRefRank(bb, _, v, _) - } + private import RankRefs /** * Holds if the SSA definition `def` reaches rank index `rnk` in its own @@ -420,12 +372,12 @@ module Make Input> { */ predicate ssaDefReachesRank(BasicBlock bb, Definition def, int rnk, SourceVariable v) { exists(int i | - rnk = ssaRefRank(bb, i, v, SsaDef()) and + rnk = refRank(bb, i, v, Def()) and def.definesAt(v, bb, i) ) or ssaDefReachesRank(bb, def, rnk - 1, v) and - rnk = ssaRefRank(bb, _, v, SsaActualRead()) + rnk = refRank(bb, _, v, Read()) } /** @@ -436,7 +388,7 @@ module Make Input> { private predicate liveThrough(BasicBlock idom, BasicBlock bb, SourceVariable v) { idom = getImmediateBasicBlockDominator(bb) and liveAtExit(bb, v) and - not ssaRef(bb, _, v, SsaDef()) + not ssaRef(bb, _, v, Def()) } /** @@ -447,7 +399,7 @@ module Make Input> { pragma[nomagic] predicate ssaDefReachesEndOfBlock(BasicBlock bb, Definition def, SourceVariable v) { exists(int last | - last = maxSsaRefRank(pragma[only_bind_into](bb), pragma[only_bind_into](v)) and + last = maxRefRank(pragma[only_bind_into](bb), pragma[only_bind_into](v)) and ssaDefReachesRank(bb, def, last, v) and liveAtExit(bb, v) ) @@ -471,7 +423,7 @@ module Make Input> { predicate ssaDefReachesReadWithinBlock(SourceVariable v, Definition def, BasicBlock bb, int i) { exists(int rnk | ssaDefReachesRank(bb, def, rnk, v) and - rnk = ssaRefRank(bb, i, v, SsaActualRead()) + rnk = refRank(bb, i, v, Read()) ) } @@ -483,7 +435,7 @@ module Make Input> { predicate ssaDefReachesRead(SourceVariable v, Definition def, BasicBlock bb, int i) { ssaDefReachesReadWithinBlock(v, def, bb, i) or - ssaRef(bb, i, v, SsaActualRead()) and + ssaRef(bb, i, v, Read()) and ssaDefReachesEndOfBlock(getImmediateBasicBlockDominator(bb), def, v) and not ssaDefReachesReadWithinBlock(v, _, bb, i) } @@ -537,7 +489,7 @@ module Make Input> { * 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` (read) nodes. + * Unlike `Liveness::varRef`, this includes `phi` (read) nodes. */ pragma[nomagic] predicate ssaRef(BasicBlock bb, int i, SourceVariable v, SsaRefKind k) { @@ -697,7 +649,7 @@ module Make Input> { 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, _) + not varRef(bb2, _, v, _) ) } From d6dc91d191633cb7a002428506b56200b080e5fa Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Mon, 17 Feb 2025 14:10:08 +0100 Subject: [PATCH 17/30] SSA: Inline predicate to simplify negation. --- shared/ssa/codeql/ssa/Ssa.qll | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/shared/ssa/codeql/ssa/Ssa.qll b/shared/ssa/codeql/ssa/Ssa.qll index f5409db3aef5..1e7495795af0 100644 --- a/shared/ssa/codeql/ssa/Ssa.qll +++ b/shared/ssa/codeql/ssa/Ssa.qll @@ -388,7 +388,7 @@ module Make Input> { private predicate liveThrough(BasicBlock idom, BasicBlock bb, SourceVariable v) { idom = getImmediateBasicBlockDominator(bb) and liveAtExit(bb, v) and - not ssaRef(bb, _, v, Def()) + not any(Definition def).definesAt(v, bb, _) } /** From 35f50bac977dc2ade70f6b0dfbc63576bea7167b Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Mon, 17 Feb 2025 15:44:00 +0100 Subject: [PATCH 18/30] SSA: Reimplement use-use. --- shared/ssa/codeql/ssa/Ssa.qll | 85 +++++++++++++++++++++++++++++++++++ 1 file changed, 85 insertions(+) diff --git a/shared/ssa/codeql/ssa/Ssa.qll b/shared/ssa/codeql/ssa/Ssa.qll index 1e7495795af0..2138e6b1a2cc 100644 --- a/shared/ssa/codeql/ssa/Ssa.qll +++ b/shared/ssa/codeql/ssa/Ssa.qll @@ -448,6 +448,91 @@ module Make Input> { } } + 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 + + /** + * 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 = getImmediateBasicBlockDominator(bb) 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, getImmediateBasicBlockDominator(bb2), 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 module SsaDefReaches { newtype TSsaRefKind = SsaActualRead() or From 194afbb7f8ea3e7c3d44f50cf0d79a995ad6faa9 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Tue, 18 Feb 2025 09:35:49 +0100 Subject: [PATCH 19/30] Java: Simplify SSA for variable capture. --- .../code/java/dataflow/internal/SsaImpl.qll | 17 +---------------- 1 file changed, 1 insertion(+), 16 deletions(-) diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll b/java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll index bcc68cfd8739..9937d0b696eb 100644 --- a/java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll +++ b/java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll @@ -490,26 +490,11 @@ private module Cached { ) } - pragma[nomagic] - private predicate captureDefReaches(Definition def, SsaInput::BasicBlock bb2, int i2) { - variableCapture(def.getSourceVariable(), _, _, _) and - exists(SsaInput::BasicBlock bb1, int i1 | - Impl::adjacentDefRead(def, bb1, i1, bb2, i2) and - def.definesAt(_, bb1, i1) - ) - or - exists(SsaInput::BasicBlock bb3, int i3 | - captureDefReaches(def, bb3, i3) and - SsaInput::variableRead(bb3, i3, _, _) and - Impl::adjacentDefRead(def, bb3, i3, bb2, i2) - ) - } - /** Holds if `init` is a closure variable that captures the value of `capturedvar`. */ cached predicate captures(SsaImplicitInit init, SsaVariable capturedvar) { exists(BasicBlock bb, int i | - captureDefReaches(capturedvar, bb, i) and + Impl::ssaDefReachesRead(_, capturedvar, bb, i) and variableCapture(capturedvar.getSourceVariable(), init.getSourceVariable(), bb, i) ) } From cf2136fbc70be2a94bf17d6265e944faa7b4a8bc Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Tue, 18 Feb 2025 13:38:17 +0100 Subject: [PATCH 20/30] SSA: Export simple firstUse and adjacentUseUse predicates. --- shared/ssa/codeql/ssa/Ssa.qll | 73 +++++++++++++++++++++++++++++++++++ 1 file changed, 73 insertions(+) diff --git a/shared/ssa/codeql/ssa/Ssa.qll b/shared/ssa/codeql/ssa/Ssa.qll index 2138e6b1a2cc..cee87527739f 100644 --- a/shared/ssa/codeql/ssa/Ssa.qll +++ b/shared/ssa/codeql/ssa/Ssa.qll @@ -531,6 +531,79 @@ module Make Input> { 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 { From 537950646445365c4e74e695c4d02bc671418b5c Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Tue, 18 Feb 2025 13:45:04 +0100 Subject: [PATCH 21/30] Java: Use firstUse and adjacentUseUse predicates. --- .../code/java/dataflow/internal/SsaImpl.qll | 63 ++++--------------- 1 file changed, 11 insertions(+), 52 deletions(-) diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll b/java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll index 9937d0b696eb..d5fdf4ef829a 100644 --- a/java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll +++ b/java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll @@ -508,34 +508,15 @@ private module Cached { Impl::uncertainWriteDefinitionInput(redef, def) } - pragma[nomagic] - private predicate defReaches(Definition def, DataFlowIntegration::Node node) { - exists(DataFlowIntegration::SsaDefinitionExtNode nodeFrom | - nodeFrom.getDefinitionExt() = def and - DataFlowIntegrationImpl::localFlowStep(_, nodeFrom, node, false) - ) - or - exists(DataFlowIntegration::Node mid | - defReaches(def, mid) and - DataFlowIntegrationImpl::localFlowStep(_, mid, node, _) - | - // flow into phi input node - mid instanceof DataFlowIntegration::SsaInputNode - or - // flow into definition - mid instanceof DataFlowIntegration::SsaDefinitionExtNode - ) - } - /** * Holds if the value defined at `def` can reach `use` without passing through * any other uses, but possibly through phi nodes and uncertain implicit updates. */ cached predicate firstUse(Definition def, VarRead use) { - exists(DataFlowIntegration::ExprNode nodeTo | - nodeTo.getExpr() = use and - defReaches(def, nodeTo) + exists(BasicBlock bb, int i | + Impl::firstUse(def, bb, i, _) and + use.getControlFlowNode() = bb.getNode(i) ) } @@ -594,30 +575,6 @@ private module Cached { cached module SsaPublic { - pragma[nomagic] - private predicate useReaches(VarRead use, DataFlowIntegration::Node node, boolean sameVar) { - exists(DataFlowIntegration::ExprNode nodeFrom | - nodeFrom.getExpr() = use and - DataFlowIntegration::localFlowStep(_, nodeFrom, node, true) and - sameVar = true - ) - or - exists(DataFlowIntegration::Node mid, boolean sameVarMid | - useReaches(use, mid, sameVarMid) and - DataFlowIntegration::localFlowStep(_, mid, node, _) - | - exists(Impl::DefinitionExt def | - // flow into definition - def = mid.(DataFlowIntegration::SsaDefinitionExtNode).getDefinitionExt() - or - // flow into phi input node - def = mid.(DataFlowIntegration::SsaInputNode).getDefinitionExt() - | - if def instanceof Impl::PhiReadNode then sameVar = sameVarMid else sameVar = false - ) - ) - } - /** * 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 @@ -625,9 +582,10 @@ private module Cached { */ cached predicate adjacentUseUseSameVar(VarRead use1, VarRead use2) { - exists(DataFlowIntegration::ExprNode nodeTo | - nodeTo.getExpr() = use2 and - useReaches(use1, nodeTo, true) + exists(BasicBlock bb1, int i1, BasicBlock bb2, int i2 | + use1.getControlFlowNode() = bb1.getNode(i1) and + use2.getControlFlowNode() = bb2.getNode(i2) and + Impl::adjacentUseUse(bb1, i1, bb2, i2, _, true) ) } @@ -639,9 +597,10 @@ private module Cached { */ cached predicate adjacentUseUse(VarRead use1, VarRead use2) { - exists(DataFlowIntegration::ExprNode nodeTo | - nodeTo.getExpr() = use2 and - useReaches(use1, nodeTo, _) + exists(BasicBlock bb1, int i1, BasicBlock bb2, int i2 | + use1.getControlFlowNode() = bb1.getNode(i1) and + use2.getControlFlowNode() = bb2.getNode(i2) and + Impl::adjacentUseUse(bb1, i1, bb2, i2, _, _) ) } } From 291ea6f6eb0522773134058a0857110c338718ae Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Tue, 18 Feb 2025 13:50:14 +0100 Subject: [PATCH 22/30] Java: Move SSA data flow test and extend it to cover phi-read input edges. --- .../ql/test/library-tests/dataflow/ssa/A.java | 24 ++++++++++++++ .../library-tests/dataflow/ssa/test.expected | 0 .../test/library-tests/dataflow/ssa/test.ql | 31 +++++++++++++++++++ .../pattern-switch/dfg/GuardTest.java | 7 ----- 4 files changed, 55 insertions(+), 7 deletions(-) create mode 100644 java/ql/test/library-tests/dataflow/ssa/A.java create mode 100644 java/ql/test/library-tests/dataflow/ssa/test.expected create mode 100644 java/ql/test/library-tests/dataflow/ssa/test.ql diff --git a/java/ql/test/library-tests/dataflow/ssa/A.java b/java/ql/test/library-tests/dataflow/ssa/A.java new file mode 100644 index 000000000000..79303697d646 --- /dev/null +++ b/java/ql/test/library-tests/dataflow/ssa/A.java @@ -0,0 +1,24 @@ +public class A { + Object source() { return null; } + void sink(Object o) { } + + boolean isSafe(Object o) { return o == null; } + + void foo() { + Object x = source(); + if (!isSafe(x)) { + x = null; + } + sink(x); + + x = source(); + if (!isSafe(x)) { + if (isSafe(x)) { + sink(x); + } else { + throw new RuntimeException(); + } + } + sink(x); + } +} diff --git a/java/ql/test/library-tests/dataflow/ssa/test.expected b/java/ql/test/library-tests/dataflow/ssa/test.expected new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/java/ql/test/library-tests/dataflow/ssa/test.ql b/java/ql/test/library-tests/dataflow/ssa/test.ql new file mode 100644 index 000000000000..cb601dab5eb1 --- /dev/null +++ b/java/ql/test/library-tests/dataflow/ssa/test.ql @@ -0,0 +1,31 @@ +import java +import semmle.code.java.controlflow.Guards +import semmle.code.java.dataflow.DataFlow + +private predicate isSafe(Guard g, Expr checked, boolean branch) { + exists(MethodCall mc | g = mc | + mc.getMethod().hasName("isSafe") and + checked = mc.getAnArgument() and + branch = true + ) +} + +module TestConfig implements DataFlow::ConfigSig { + predicate isSource(DataFlow::Node source) { + source.asExpr().(MethodCall).getMethod().hasName("source") + } + + predicate isSink(DataFlow::Node sink) { + exists(MethodCall mc | mc.getMethod().hasName("sink") and mc.getAnArgument() = sink.asExpr()) + } + + predicate isBarrier(DataFlow::Node node) { + node = DataFlow::BarrierGuard::getABarrierNode() + } +} + +module Flow = DataFlow::Global; + +from DataFlow::Node source, DataFlow::Node sink +where Flow::flow(source, sink) +select source, sink diff --git a/java/ql/test/library-tests/pattern-switch/dfg/GuardTest.java b/java/ql/test/library-tests/pattern-switch/dfg/GuardTest.java index e0d3494aa208..f49b69f3b610 100644 --- a/java/ql/test/library-tests/pattern-switch/dfg/GuardTest.java +++ b/java/ql/test/library-tests/pattern-switch/dfg/GuardTest.java @@ -24,13 +24,6 @@ case String s when isSafe(s): break; } - - String s2 = "string"; - - if (!isSafe(s2)) { - s2 = null; - } - sink(s2); } } From ed40035b9cb9c81dc5e90bcf7ace6caac38ccdaf Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Wed, 19 Feb 2025 16:20:57 +0100 Subject: [PATCH 23/30] C#/Ruby/Rust: Fix bug in adjacentReadPairSameVar. --- csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll | 2 +- ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll | 2 +- rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll index bccadc5fee03..68dd6d292fb0 100644 --- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll +++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll @@ -949,7 +949,7 @@ private module Cached { predicate adjacentReadPairSameVar(Definition def, ControlFlow::Node cfn1, ControlFlow::Node cfn2) { exists(ControlFlow::BasicBlock bb1, int i1, ControlFlow::BasicBlock bb2, int i2 | cfn1 = bb1.getNode(i1) and - variableReadActual(bb1, i1, _) and + variableReadActual(bb1, i1, def.getSourceVariable()) and adjacentDefSkipUncertainReads(def, bb1, i1, bb2, i2) and cfn2 = bb2.getNode(i2) ) diff --git a/ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll b/ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll index 7185f0389aaa..39ce557d65a6 100644 --- a/ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll +++ b/ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll @@ -409,7 +409,7 @@ private module Cached { ) { exists(Cfg::BasicBlock bb1, int i1, Cfg::BasicBlock bb2, int i2 | read1 = bb1.getNode(i1) and - variableReadActual(bb1, i1, _) and + variableReadActual(bb1, i1, def.getSourceVariable()) and adjacentDefSkipUncertainReads(def, bb1, i1, bb2, i2) and read2 = bb2.getNode(i2) ) diff --git a/rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll b/rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll index a0b724ceab59..c3ba6404f451 100644 --- a/rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll +++ b/rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll @@ -330,7 +330,7 @@ private module Cached { predicate adjacentReadPair(Definition def, CfgNode read1, CfgNode read2) { exists(BasicBlock bb1, int i1, BasicBlock bb2, int i2 | read1 = bb1.getNode(i1) and - variableReadActual(bb1, i1, _) and + variableReadActual(bb1, i1, def.getSourceVariable()) and adjacentDefSkipUncertainReads(def, bb1, i1, bb2, i2) and read2 = bb2.getNode(i2) ) From 17ae747b0814ebcd5dcf087feb5ace5ae2df13e3 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Wed, 19 Feb 2025 16:24:21 +0100 Subject: [PATCH 24/30] C#: Switch use-use predicates to new implementation. --- .../code/csharp/dataflow/internal/SsaImpl.qll | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll index 68dd6d292fb0..561fbe6770be 100644 --- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll +++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll @@ -933,10 +933,8 @@ private module Cached { */ cached predicate firstReadSameVar(Definition def, ControlFlow::Node cfn) { - exists(ControlFlow::BasicBlock bb1, int i1, ControlFlow::BasicBlock bb2, int i2 | - def.definesAt(_, bb1, i1) and - adjacentDefSkipUncertainReads(def, bb1, i1, bb2, i2) and - cfn = bb2.getNode(i2) + exists(ControlFlow::BasicBlock bb, int i | + Impl::firstUse(def, bb, i, true) and cfn = bb.getNode(i) ) } @@ -947,10 +945,13 @@ private module Cached { */ cached predicate adjacentReadPairSameVar(Definition def, ControlFlow::Node cfn1, ControlFlow::Node cfn2) { - exists(ControlFlow::BasicBlock bb1, int i1, ControlFlow::BasicBlock bb2, int i2 | + exists( + ControlFlow::BasicBlock bb1, int i1, ControlFlow::BasicBlock bb2, int i2, + Ssa::SourceVariable v + | + Impl::ssaDefReachesRead(v, def, bb1, i1) and + Impl::adjacentUseUse(bb1, i1, bb2, i2, v, true) and cfn1 = bb1.getNode(i1) and - variableReadActual(bb1, i1, def.getSourceVariable()) and - adjacentDefSkipUncertainReads(def, bb1, i1, bb2, i2) and cfn2 = bb2.getNode(i2) ) } From b0a5e620032fc372ce38d26c81c4cbb62d27fca5 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Wed, 19 Feb 2025 16:27:52 +0100 Subject: [PATCH 25/30] C#: Clean up unused. --- .../code/csharp/dataflow/internal/SsaImpl.qll | 28 ++----------------- 1 file changed, 3 insertions(+), 25 deletions(-) diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll index 561fbe6770be..61787debca4f 100644 --- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll +++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll @@ -734,7 +734,7 @@ private predicate variableReadPseudo(ControlFlow::BasicBlock bb, int i, Ssa::Sou } pragma[noinline] -private predicate adjacentDefRead( +deprecated private predicate adjacentDefRead( Definition def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2, SsaInput::SourceVariable v ) { @@ -742,7 +742,7 @@ private predicate adjacentDefRead( v = def.getSourceVariable() } -private predicate adjacentDefReachesRead( +deprecated private predicate adjacentDefReachesRead( Definition def, SsaInput::SourceVariable v, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2 ) { @@ -760,18 +760,7 @@ private predicate adjacentDefReachesRead( ) } -/** Same as `adjacentDefRead`, but skips uncertain reads. */ -pragma[nomagic] -private predicate adjacentDefSkipUncertainReads( - Definition def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2 -) { - exists(SsaInput::SourceVariable v | - adjacentDefReachesRead(def, v, bb1, i1, bb2, i2) and - SsaInput::variableRead(bb2, i2, v, true) - ) -} - -private predicate adjacentDefReachesUncertainRead( +deprecated private predicate adjacentDefReachesUncertainRead( Definition def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2 ) { exists(SsaInput::SourceVariable v | @@ -956,17 +945,6 @@ private module Cached { ) } - cached - predicate lastRefBeforeRedef(Definition def, ControlFlow::BasicBlock bb, int i, Definition next) { - Impl::lastRefRedef(def, bb, i, next) and - not SsaInput::variableRead(bb, i, def.getSourceVariable(), false) - or - exists(SsaInput::BasicBlock bb0, int i0 | - Impl::lastRefRedef(def, bb0, i0, next) and - adjacentDefReachesUncertainRead(def, bb, i, bb0, i0) - ) - } - cached Definition uncertainWriteDefinitionInput(UncertainWriteDefinition def) { Impl::uncertainWriteDefinitionInput(def, result) From 4ddc5c9d751de14dff9efacb2c0ea0f95ed4588d Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Wed, 19 Feb 2025 16:34:36 +0100 Subject: [PATCH 26/30] Ruby: Switch use-use predicates to new implementation. --- .../codeql/ruby/dataflow/internal/SsaImpl.qll | 46 ++----------------- 1 file changed, 4 insertions(+), 42 deletions(-) diff --git a/ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll b/ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll index 39ce557d65a6..b8757e489dcf 100644 --- a/ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll +++ b/ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll @@ -222,15 +222,6 @@ private predicate hasVariableReadWithCapturedWrite( variableReadActualInOuterScope(bb, i, v, scope) } -pragma[noinline] -private predicate adjacentDefRead( - Definition def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2, - SsaInput::SourceVariable v -) { - Impl::adjacentDefRead(def, bb1, i1, bb2, i2) and - v = def.getSourceVariable() -} - pragma[noinline] deprecated private predicate adjacentDefReadExt( DefinitionExt def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2, @@ -240,22 +231,6 @@ deprecated private predicate adjacentDefReadExt( v = def.getSourceVariable() } -private predicate adjacentDefReachesRead( - Definition def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2 -) { - exists(SsaInput::SourceVariable v | adjacentDefRead(def, bb1, i1, bb2, i2, v) | - def.definesAt(v, bb1, i1) - or - SsaInput::variableRead(bb1, i1, v, true) - ) - or - exists(SsaInput::BasicBlock bb3, int i3 | - adjacentDefReachesRead(def, bb1, i1, bb3, i3) and - SsaInput::variableRead(bb3, i3, _, false) and - Impl::adjacentDefRead(def, bb3, i3, bb2, i2) - ) -} - deprecated private predicate adjacentDefReachesReadExt( DefinitionExt def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2 ) { @@ -272,15 +247,6 @@ deprecated private predicate adjacentDefReachesReadExt( ) } -/** Same as `adjacentDefRead`, but skips uncertain reads. */ -pragma[nomagic] -private predicate adjacentDefSkipUncertainReads( - Definition def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2 -) { - adjacentDefReachesRead(def, bb1, i1, bb2, i2) and - SsaInput::variableRead(bb2, i2, _, true) -} - deprecated private predicate adjacentDefReachesUncertainReadExt( DefinitionExt def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2 ) { @@ -391,11 +357,7 @@ private module Cached { */ cached predicate firstRead(Definition def, VariableReadAccessCfgNode read) { - exists(Cfg::BasicBlock bb1, int i1, Cfg::BasicBlock bb2, int i2 | - def.definesAt(_, bb1, i1) and - adjacentDefSkipUncertainReads(def, bb1, i1, bb2, i2) and - read = bb2.getNode(i2) - ) + exists(Cfg::BasicBlock bb, int i | Impl::firstUse(def, bb, i, true) and read = bb.getNode(i)) } /** @@ -407,10 +369,10 @@ private module Cached { predicate adjacentReadPair( Definition def, VariableReadAccessCfgNode read1, VariableReadAccessCfgNode read2 ) { - exists(Cfg::BasicBlock bb1, int i1, Cfg::BasicBlock bb2, int i2 | + exists(Cfg::BasicBlock bb1, int i1, Cfg::BasicBlock bb2, int i2, LocalVariable v | + Impl::ssaDefReachesRead(v, def, bb1, i1) and + Impl::adjacentUseUse(bb1, i1, bb2, i2, v, true) and read1 = bb1.getNode(i1) and - variableReadActual(bb1, i1, def.getSourceVariable()) and - adjacentDefSkipUncertainReads(def, bb1, i1, bb2, i2) and read2 = bb2.getNode(i2) ) } From 7e596032f1763d0b15d8c953932d5d311a51bb3c Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Wed, 19 Feb 2025 16:38:37 +0100 Subject: [PATCH 27/30] Rust: Switch use-use predicates to new implementation. --- .../codeql/rust/dataflow/internal/SsaImpl.qll | 45 ++----------------- 1 file changed, 4 insertions(+), 41 deletions(-) diff --git a/rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll b/rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll index c3ba6404f451..91725e00bea0 100644 --- a/rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll +++ b/rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll @@ -120,14 +120,6 @@ module ExposedForTestingOnly { predicate phiHasInputFromBlockExt = Impl::phiHasInputFromBlockExt/3; } -pragma[noinline] -private predicate adjacentDefRead( - Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2, SsaInput::SourceVariable v -) { - Impl::adjacentDefRead(def, bb1, i1, bb2, i2) and - v = def.getSourceVariable() -} - /** Holds if `v` is read at index `i` in basic block `bb`. */ private predicate variableReadActual(BasicBlock bb, int i, Variable v) { exists(VariableAccess read | @@ -167,31 +159,6 @@ private predicate hasVariableReadWithCapturedWrite( variableReadActualInOuterScope(bb, i, v, scope) } -private predicate adjacentDefReachesRead( - Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2 -) { - exists(SsaInput::SourceVariable v | adjacentDefRead(def, bb1, i1, bb2, i2, v) | - def.definesAt(v, bb1, i1) - or - SsaInput::variableRead(bb1, i1, v, true) - ) - or - exists(BasicBlock bb3, int i3 | - adjacentDefReachesRead(def, bb1, i1, bb3, i3) and - SsaInput::variableRead(bb3, i3, _, false) and - Impl::adjacentDefRead(def, bb3, i3, bb2, i2) - ) -} - -/** Same as `adjacentDefRead`, but skips uncertain reads. */ -pragma[nomagic] -private predicate adjacentDefSkipUncertainReads( - Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2 -) { - adjacentDefReachesRead(def, bb1, i1, bb2, i2) and - SsaInput::variableRead(bb2, i2, _, true) -} - private VariableAccess getACapturedVariableAccess(BasicBlock bb, Variable v) { result = bb.getANode().getAstNode() and result.isCapture() and @@ -314,11 +281,7 @@ private module Cached { */ cached predicate firstRead(Definition def, CfgNode read) { - exists(BasicBlock bb1, int i1, BasicBlock bb2, int i2 | - def.definesAt(_, bb1, i1) and - adjacentDefSkipUncertainReads(def, bb1, i1, bb2, i2) and - read = bb2.getNode(i2) - ) + exists(BasicBlock bb, int i | Impl::firstUse(def, bb, i, true) and read = bb.getNode(i)) } /** @@ -328,10 +291,10 @@ private module Cached { */ cached predicate adjacentReadPair(Definition def, CfgNode read1, CfgNode read2) { - exists(BasicBlock bb1, int i1, BasicBlock bb2, int i2 | + exists(BasicBlock bb1, int i1, BasicBlock bb2, int i2, Variable v | + Impl::ssaDefReachesRead(v, def, bb1, i1) and + Impl::adjacentUseUse(bb1, i1, bb2, i2, v, true) and read1 = bb1.getNode(i1) and - variableReadActual(bb1, i1, def.getSourceVariable()) and - adjacentDefSkipUncertainReads(def, bb1, i1, bb2, i2) and read2 = bb2.getNode(i2) ) } From b76e5f55c64e809289878879d46e0cb29829804d Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Wed, 19 Feb 2025 16:41:49 +0100 Subject: [PATCH 28/30] SSA: Deprecate unused predicate. --- shared/ssa/codeql/ssa/Ssa.qll | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/shared/ssa/codeql/ssa/Ssa.qll b/shared/ssa/codeql/ssa/Ssa.qll index cee87527739f..d33c208e86d2 100644 --- a/shared/ssa/codeql/ssa/Ssa.qll +++ b/shared/ssa/codeql/ssa/Ssa.qll @@ -779,7 +779,7 @@ module Make Input> { pragma[noinline] predicate ssaDefReachesThroughBlock(DefinitionExt def, BasicBlock bb) { exists(SourceVariable v | - ssaDefReachesEndOfBlockExt(bb, def, v) and + ssaDefReachesEndOfBlockExt0(bb, def, v) and not defOccursInBlock(_, bb, v, _) ) } @@ -863,7 +863,7 @@ module Make Input> { predicate varBlockReachesExitExt(DefinitionExt def, BasicBlock bb) { exists(BasicBlock bb2 | varBlockReachesExt(def, _, bb, bb2) | not defOccursInBlock(def, bb2, _, _) and - not ssaDefReachesEndOfBlockExt(bb2, def, _) + not ssaDefReachesEndOfBlockExt0(bb2, def, _) ) } @@ -872,7 +872,7 @@ module Make Input> { exists(BasicBlock bb2, SourceVariable v | varBlockReachesExt(def, v, bb, bb2) and not defOccursInBlock(def, bb2, _, _) and - not ssaDefReachesEndOfBlockExt(bb2, def, _) and + not ssaDefReachesEndOfBlockExt0(bb2, def, _) and not any(PhiReadNode phi).definesAt(v, bb2, _, _) ) or @@ -907,7 +907,7 @@ module Make Input> { * SSA definition of `v`. */ pragma[nomagic] - predicate ssaDefReachesEndOfBlockExt(BasicBlock bb, DefinitionExt def, SourceVariable v) { + private predicate ssaDefReachesEndOfBlockExt0(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 @@ -920,10 +920,12 @@ module Make 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. - ssaDefReachesEndOfBlockExt(getImmediateBasicBlockDominator(bb), def, pragma[only_bind_into](v)) and + ssaDefReachesEndOfBlockExt0(getImmediateBasicBlockDominator(bb), def, pragma[only_bind_into](v)) and liveThroughExt(bb, pragma[only_bind_into](v)) } + deprecated predicate ssaDefReachesEndOfBlockExt = ssaDefReachesEndOfBlockExt0/3; + /** * NB: If this predicate is exposed, it should be cached. * @@ -955,7 +957,7 @@ module Make Input> { exists(SourceVariable v, BasicBlock bbDef | phi.definesAt(v, bbDef, _, _) and getABasicBlockPredecessor(bbDef) = bb and - ssaDefReachesEndOfBlockExt(bb, inp, v) + ssaDefReachesEndOfBlockExt0(bb, inp, v) | phi instanceof PhiNode or phi instanceof PhiReadNode @@ -973,7 +975,7 @@ module Make Input> { ssaDefReachesReadWithinBlock(v, def, bb, i) or ssaRef(bb, i, v, SsaActualRead()) and - ssaDefReachesEndOfBlockExt(getABasicBlockPredecessor(bb), def, v) and + ssaDefReachesEndOfBlockExt0(getABasicBlockPredecessor(bb), def, v) and not ssaDefReachesReadWithinBlock(v, _, bb, i) } From 8e609b19f5f339401610192e7559796143b494ff Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Thu, 20 Feb 2025 10:33:44 +0100 Subject: [PATCH 29/30] Ruby: Accept qltest change. This is a result of the bugfix in the commit named "C#/Ruby/Rust: Fix bug in adjacentReadPairSameVar" --- ruby/ql/test/library-tests/variables/ssa.expected | 1 - 1 file changed, 1 deletion(-) diff --git a/ruby/ql/test/library-tests/variables/ssa.expected b/ruby/ql/test/library-tests/variables/ssa.expected index 05acf5dbb59e..b998016a39ff 100644 --- a/ruby/ql/test/library-tests/variables/ssa.expected +++ b/ruby/ql/test/library-tests/variables/ssa.expected @@ -527,7 +527,6 @@ adjacentReads | nested_scopes.rb:8:5:35:7 | self (N) | nested_scopes.rb:8:5:35:7 | self | nested_scopes.rb:30:16:30:19 | self | nested_scopes.rb:34:7:34:12 | self | | nested_scopes.rb:13:11:13:11 | a | nested_scopes.rb:13:11:13:11 | a | nested_scopes.rb:14:16:14:16 | a | nested_scopes.rb:15:11:15:11 | a | | nested_scopes.rb:27:7:29:9 | self (show) | nested_scopes.rb:27:7:29:9 | self | nested_scopes.rb:28:11:28:16 | self | nested_scopes.rb:28:16:28:16 | self | -| nested_scopes.rb:30:16:30:19 | self (class << ...) | nested_scopes.rb:30:7:33:9 | self | nested_scopes.rb:30:16:30:19 | self | nested_scopes.rb:32:11:32:16 | self | | parameters.rb:1:9:5:3 | self | parameters.rb:1:1:62:1 | self | parameters.rb:3:4:3:9 | self | parameters.rb:4:4:4:9 | self | | parameters.rb:7:26:7:31 | pizzas | parameters.rb:7:26:7:31 | pizzas | parameters.rb:8:6:8:11 | pizzas | parameters.rb:11:14:11:19 | pizzas | | parameters.rb:25:1:28:3 | self (opt_param) | parameters.rb:25:1:28:3 | self | parameters.rb:26:3:26:11 | self | parameters.rb:27:3:27:11 | self | From 8c0cc077c84918473a966b28e12e916277f15636 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Thu, 20 Feb 2025 15:49:23 +0100 Subject: [PATCH 30/30] Ssa: Fix qldoc duplicate word. --- shared/ssa/codeql/ssa/Ssa.qll | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/shared/ssa/codeql/ssa/Ssa.qll b/shared/ssa/codeql/ssa/Ssa.qll index d33c208e86d2..407169cc6be7 100644 --- a/shared/ssa/codeql/ssa/Ssa.qll +++ b/shared/ssa/codeql/ssa/Ssa.qll @@ -318,7 +318,7 @@ module Make Input> { * 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 all reads are treated as potential + * 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. */