From b196714794a8518b4e5828e95aa7267a027c6e97 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Wed, 15 Oct 2025 10:54:24 +0200 Subject: [PATCH 1/3] SSA: Add a shared signature for SSA and a module to implement it. --- shared/ssa/codeql/ssa/Ssa.qll | 440 +++++++++++++++++++++++++++++++++- 1 file changed, 438 insertions(+), 2 deletions(-) diff --git a/shared/ssa/codeql/ssa/Ssa.qll b/shared/ssa/codeql/ssa/Ssa.qll index 20a447f91a99..562560c22f03 100644 --- a/shared/ssa/codeql/ssa/Ssa.qll +++ b/shared/ssa/codeql/ssa/Ssa.qll @@ -9,10 +9,10 @@ private import codeql.controlflow.BasicBlock as BB private import codeql.util.Location private import codeql.util.Unit -signature class BasicBlockSig; +private signature class TypSig; /** Provides the input specification of the SSA implementation. */ -signature module InputSig { +signature module InputSig { /** A variable that can be SSA converted. */ class SourceVariable { /** Gets a textual representation of this variable. */ @@ -42,6 +42,175 @@ signature module InputSig { predicate variableRead(BasicBlock bb, int i, SourceVariable v, boolean certain); } +/** + * Provides classes and predicates for the SSA representation of variables. + * + * Class hierarchy: + * ```text + * SsaDefinition + * |- SsaWriteDefinition + * | |- SsaExplicitWrite + * | | \- SsaParameterInit + * | |- SsaImplicitWrite + * | | \- SsaImplicitEntryDefinition + * | \- SsaUncertainWrite (overlaps SsaImplicitWrite and potentially SsaExplicitWrite) + * \- SsaPhiDefinition + * ``` + */ +signature module SsaSig< + LocationSig Location, TypSig ControlFlowNode, TypSig BasicBlock, TypSig Expr, TypSig Parameter, + TypSig VariableWrite> +{ + /** A variable that can be SSA converted. */ + class SourceVariable { + /** Gets a textual representation of this variable. */ + string toString(); + + /** Gets the location of this variable. */ + Location getLocation(); + } + + /** A static single assignment (SSA) definition. */ + class SsaDefinition { + /** Gets the source variable underlying this SSA definition. */ + SourceVariable getSourceVariable(); + + /** + * Holds if this SSA definition defines `v` at index `i` in basic block `bb`. + * Phi definitions are considered to be at index `-1`, while normal variable writes + * are at the index of the control flow node they wrap. + */ + predicate definesAt(SourceVariable v, BasicBlock bb, int i); + + /** Gets the basic block to which this SSA definition belongs. */ + BasicBlock getBasicBlock(); + + /** + * Gets the control flow node of this SSA definition. + * + * For SSA definitions occurring at the beginning of a basic block, such as + * phi definitions, this will get the first control flow node of the basic block. + */ + ControlFlowNode getControlFlowNode(); + + /** Gets a read of this SSA definition. */ + Expr getARead(); + + /** + * Holds if this SSA definition is live at the end of basic block `bb`. + * That is, this definition reaches the end of basic block `bb`, at which + * point it is still live, without crossing another SSA definition of the + * same source variable. + */ + predicate isLiveAtEndOfBlock(BasicBlock bb); + + /** + * Gets a definition that ultimately defines this SSA definition and is + * not itself a phi definition. + * + * Example: + * + * ```rb + * def m b + * i = 0 # defines i_0 + * if b + * i = 1 # defines i_1 + * else + * i = 2 # defines i_2 + * end + * # defines i_3 = phi(i_1, i_2); ultimate definitions are i_1 and i_2 + * puts i + * end + * ``` + */ + SsaDefinition getAnUltimateDefinition(); + + /** Gets a textual representation of this SSA definition. */ + string toString(); + + /** Gets the location of this SSA definition. */ + Location getLocation(); + } + + /** + * A write definition. This includes every definition that is not a phi + * definition. + */ + class SsaWriteDefinition extends SsaDefinition; + + /** + * An SSA definition that corresponds to an explicit variable update or + * declaration. + */ + class SsaExplicitWrite extends SsaWriteDefinition { + /** Gets the write underlying this SSA definition. */ + VariableWrite getDefinition(); + + /** + * Gets the expression representing this write, if any. This is equivalent + * to `getDefinition().asExpr()`. + */ + Expr getDefiningExpr(); + + /** + * Gets the expression with the value being written, if any. This is + * equivalent to `getDefinition().getValue()`. + */ + Expr getValue(); + } + + /** + * An SSA definition representing the initialization of a parameter at the + * beginning of a callable. + */ + class SsaParameterInit extends SsaExplicitWrite { + /** + * Gets the parameter that this definition represents. This is equivalent + * to `getDefinition().isParameterInit(result)` + */ + Parameter getParameter(); + } + + /** + * An SSA definition that does not correspond to an explicit variable + * update or declaration. + * + * This includes implicit entry definitions for fields and captured + * variables, as well as field updates through side-effects and implicit + * definitions for fields whenever the qualifier is updated. + */ + class SsaImplicitWrite extends SsaWriteDefinition; + + /** + * An SSA definition representing the implicit initialization of a variable + * at the beginning of a callable. This includes fields and captured + * variables, but excludes parameters as they have explicit declarations. + */ + class SsaImplicitEntryDefinition extends SsaImplicitWrite; + + /** An SSA definition that represents an uncertain variable update. */ + class SsaUncertainWrite extends SsaWriteDefinition { + /** + * Gets the immediately preceding definition. Since this update is uncertain, + * the value from the preceding definition might still be valid. + */ + SsaDefinition getPriorDefinition(); + } + + /** + * An SSA phi definition, that is, a pseudo definition for a variable at a + * point in the flow graph where otherwise two or more definitions for the + * variable would be visible. + */ + class SsaPhiDefinition extends SsaDefinition { + /** Holds if `inp` is an input to the phi definition along the edge originating in `bb`. */ + predicate hasInputFromBlock(SsaDefinition inp, BasicBlock bb); + + /** Gets an input of this phi definition. */ + SsaDefinition getAnInput(); + } +} + /** * Provides an SSA implementation. * @@ -1319,6 +1488,273 @@ module Make< override Location getLocation() { result = this.getBasicBlock().getLocation() } } + signature module SsaInputSig { + class Expr { + ControlFlowNode getControlFlowNode(); + + /** Gets a textual representation of this expression. */ + string toString(); + + /** Gets the location of this expression. */ + Location getLocation(); + } + + class Parameter; + + class VariableWrite { + /** Gets the expression representing this write, if any. */ + Expr asExpr(); + + /** + * Gets the expression with the value being written, if any. + * + * This can be the same expression as returned by `asExpr()`, which is the + * case for, for example, `++x` and `x += e`. For simple assignments like + * `x = e`, `asExpr()` gets the whole assignment expression while + * `getValue()` gets the right-hand side `e`. Post-crement operations like + * `x++` do not have an expression with the value being written. + */ + Expr getValue(); + + /** Holds if this write is an initialization of a parameter. */ + predicate isParameterInit(Parameter p); + + /** Gets a textual representation of this write. */ + string toString(); + + /** Gets the location of this write. */ + Location getLocation(); + } + + predicate explicitWrite(VariableWrite w, BasicBlock bb, int i, SourceVariable v); + + /** + * Holds if `closureVar` is a local variable inside a closure that captures + * `captured`, which is the same variable in its declaring scope. The + * capture occurs at index `i` in basic block `bb`, and + * `variableRead(bb, i, captured, false)` must hold in order to include a + * pseudo-read of the captured variable at the point of capture. + */ + predicate variableCapture( + SourceVariable captured, SourceVariable closureVar, BasicBlock bb, int i + ); + } + + module MakeSsa implements + SsaSig + { + class SourceVariable = Input::SourceVariable; + + private import SsaInput + private import Cached + + cached + private module Cached { + cached + predicate ssaDefReachesCertainRead(Definition def, Expr e) { + exists(SourceVariable v, BasicBlock bb, int i | + ssaDefReachesRead(v, def, bb, i) and + variableRead(bb, i, v, true) and + e.getControlFlowNode() = bb.getNode(i) + ) + } + + cached + predicate ssaDefReachesUncertainRead(SourceVariable v, Definition def, BasicBlock bb, int i) { + ssaDefReachesRead(v, def, bb, i) and + variableRead(bb, i, v, false) + } + + /** Holds if `init` is a closure variable that captures the value of `capturedvar`. */ + cached + predicate captures(SsaImplicitEntryDefinition init, Definition capturedvar) { + exists(BasicBlock bb, int i | + ssaDefReachesRead(_, capturedvar, bb, i) and + variableCapture(capturedvar.getSourceVariable(), init.getSourceVariable(), bb, i) + ) + } + + cached + predicate isLiveAtEndOfBlock(Definition def, BasicBlock bb) { + ssaDefReachesEndOfBlock(bb, def, _) + } + + cached + predicate phiHasInputFromBlockCached(PhiNode phi, Definition inp, BasicBlock bb) { + phiHasInputFromBlock(phi, inp, bb) + } + + cached + predicate uncertainWriteDefinitionInputCached(UncertainWriteDefinition def, Definition inp) { + uncertainWriteDefinitionInput(def, inp) + } + } + + additional predicate ssaDefReachesUncertainRead = Cached::ssaDefReachesUncertainRead/4; + + final private class FinalDefinition = Definition; + + /** A static single assignment (SSA) definition. */ + class SsaDefinition extends FinalDefinition { + /** + * Gets the control flow node of this SSA definition. + * + * For SSA definitions occurring at the beginning of a basic block, such as + * phi nodes, this will get the first control flow node of the basic block. + */ + ControlFlowNode getControlFlowNode() { + exists(BasicBlock bb, int i | this.definesAt(_, bb, i) | result = bb.getNode(0.maximum(i))) + } + + /** Gets a read of this SSA definition. */ + Expr getARead() { ssaDefReachesCertainRead(this, result) } + + /** + * Holds if this SSA definition is live at the end of basic block `bb`. + * That is, this definition reaches the end of basic block `bb`, at which + * point it is still live, without crossing another SSA definition of the + * same source variable. + */ + predicate isLiveAtEndOfBlock(BasicBlock bb) { isLiveAtEndOfBlock(this, bb) } + + /** + * Gets an SSA definition whose value can flow to this one in one step. This + * includes inputs to phi definitions, the prior definition of uncertain writes, + * and the captured ssa definition for a closure definition. + */ + private SsaDefinition getAPhiInputOrPriorDefinition() { + result = this.(SsaPhiDefinition).getAnInput() or + result = this.(SsaUncertainWrite).getPriorDefinition() or + this.(SsaImplicitEntryDefinition).captures(result) + } + + /** + * Gets a definition that ultimately defines this SSA definition and is + * not itself a phi definition. + * + * Example: + * + * ```rb + * def m b + * i = 0 # defines i_0 + * if b + * i = 1 # defines i_1 + * else + * i = 2 # defines i_2 + * end + * # defines i_3 = phi(i_1, i_2); ultimate definitions are i_1 and i_2 + * puts i + * end + * ``` + */ + SsaDefinition getAnUltimateDefinition() { + result = this.getAPhiInputOrPriorDefinition*() and not result instanceof SsaPhiDefinition + } + } + + /** + * A write definition. This includes every definition that is not a phi + * definition. + */ + class SsaWriteDefinition extends SsaDefinition instanceof WriteDefinition { } + + private predicate explicitWrite(WriteDefinition def, VariableWrite write) { + exists(BasicBlock bb, int i, SourceVariable v | + def.definesAt(v, bb, i) and + explicitWrite(write, bb, i, v) + ) + } + + /** + * An SSA definition that corresponds to an explicit variable update or + * declaration. + */ + class SsaExplicitWrite extends SsaWriteDefinition { + SsaExplicitWrite() { explicitWrite(this, _) } + + /** Gets the write underlying this SSA definition. */ + VariableWrite getDefinition() { explicitWrite(this, result) } + + /** + * Gets the expression representing this write, if any. This is equivalent + * to `getDefinition().asExpr()`. + */ + Expr getDefiningExpr() { result = this.getDefinition().asExpr() } + + /** + * Gets the expression with the value being written, if any. This is + * equivalent to `getDefinition().getValue()`. + */ + Expr getValue() { result = this.getDefinition().getValue() } + } + + private predicate parameterInit(WriteDefinition def, Parameter p) { + exists(VariableWrite write | explicitWrite(def, write) and write.isParameterInit(p)) + } + + /** + * An SSA definition representing the initialization of a parameter at the + * beginning of a callable. + */ + class SsaParameterInit extends SsaExplicitWrite { + SsaParameterInit() { parameterInit(this, _) } + + /** + * Gets the parameter that this definition represents. This is equivalent + * to `getDefinition().isParameterInit(result)` + */ + Parameter getParameter() { parameterInit(this, result) } + } + + /** + * An SSA definition that does not correspond to an explicit variable + * update or declaration. + * + * This includes implicit entry definitions for fields and captured + * variables, as well as field updates through side-effects and implicit + * definitions for fields whenever the qualifier is updated. + */ + class SsaImplicitWrite extends SsaWriteDefinition { + SsaImplicitWrite() { not explicitWrite(this, _) } + } + + /** + * An SSA definition representing the implicit initialization of a variable + * at the beginning of a callable. This includes fields and captured + * variables, but excludes parameters as they have explicit declarations. + */ + class SsaImplicitEntryDefinition extends SsaImplicitWrite { + SsaImplicitEntryDefinition() { this.definesAt(_, any(EntryBasicBlock bb), -1) } + + /** Holds if this is a closure definition that captures the value of `capturedvar`. */ + predicate captures(SsaDefinition capturedvar) { captures(this, capturedvar) } + } + + /** An SSA definition that represents an uncertain variable update. */ + class SsaUncertainWrite extends SsaWriteDefinition instanceof UncertainWriteDefinition { + /** + * Gets the immediately preceding definition. Since this update is uncertain, + * the value from the preceding definition might still be valid. + */ + SsaDefinition getPriorDefinition() { uncertainWriteDefinitionInputCached(this, result) } + } + + /** + * An SSA phi definition, that is, a pseudo definition for a variable at a + * point in the flow graph where otherwise two or more definitions for the + * variable would be visible. + */ + class SsaPhiDefinition extends SsaDefinition { + /** Holds if `inp` is an input to the phi definition along the edge originating in `bb`. */ + predicate hasInputFromBlock(SsaDefinition inp, BasicBlock bb) { + phiHasInputFromBlockCached(this, inp, bb) + } + + /** Gets an input of this phi definition. */ + SsaDefinition getAnInput() { this.hasInputFromBlock(result, _) } + } + } + /** Provides a set of consistency queries. */ module Consistency { /** Holds if a read can be reached from multiple definitions. */ From be626bf0ce484635e51cc9e456662c8b7d61f9bd Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Mon, 20 Oct 2025 14:02:43 +0200 Subject: [PATCH 2/3] SSA: Address some review comments. --- shared/ssa/codeql/ssa/Ssa.qll | 90 ++++++++++++++++++++++++++++------- 1 file changed, 74 insertions(+), 16 deletions(-) diff --git a/shared/ssa/codeql/ssa/Ssa.qll b/shared/ssa/codeql/ssa/Ssa.qll index 562560c22f03..6321e1b8d75c 100644 --- a/shared/ssa/codeql/ssa/Ssa.qll +++ b/shared/ssa/codeql/ssa/Ssa.qll @@ -201,12 +201,40 @@ signature module SsaSig< * An SSA phi definition, that is, a pseudo definition for a variable at a * point in the flow graph where otherwise two or more definitions for the * variable would be visible. + * + * For example, in + * ```rb + * if b + * x = 0 + * else + * x = 1 + * end + * puts x + * ``` + * a phi definition for `x` is inserted just before the call `puts x`. */ class SsaPhiDefinition extends SsaDefinition { - /** Holds if `inp` is an input to the phi definition along the edge originating in `bb`. */ + /** Holds if `inp` is an input to this phi definition along the edge originating in `bb`. */ predicate hasInputFromBlock(SsaDefinition inp, BasicBlock bb); - /** Gets an input of this phi definition. */ + /** + * Gets an input of this phi definition. + * + * Example: + * + * ```rb + * def m b + * i = 0 # defines i_0 + * if b + * i = 1 # defines i_1 + * else + * i = 2 # defines i_2 + * end + * # defines i_3 = phi(i_1, i_2); inputs are i_1 and i_2 + * puts i + * end + * ``` + */ SsaDefinition getAnInput(); } } @@ -1516,7 +1544,7 @@ module Make< */ Expr getValue(); - /** Holds if this write is an initialization of a parameter. */ + /** Holds if this write is an initialization of parameter `p`. */ predicate isParameterInit(Parameter p); /** Gets a textual representation of this write. */ @@ -1588,6 +1616,19 @@ module Make< predicate uncertainWriteDefinitionInputCached(UncertainWriteDefinition def, Definition inp) { uncertainWriteDefinitionInput(def, inp) } + + cached + predicate explicitWrite(WriteDefinition def, VariableWrite write) { + exists(BasicBlock bb, int i, SourceVariable v | + def.definesAt(v, bb, i) and + explicitWrite(write, bb, i, v) + ) + } + + cached + predicate parameterInit(WriteDefinition def, Parameter p) { + exists(VariableWrite write | explicitWrite(def, write) and write.isParameterInit(p)) + } } additional predicate ssaDefReachesUncertainRead = Cached::ssaDefReachesUncertainRead/4; @@ -1658,13 +1699,6 @@ module Make< */ class SsaWriteDefinition extends SsaDefinition instanceof WriteDefinition { } - private predicate explicitWrite(WriteDefinition def, VariableWrite write) { - exists(BasicBlock bb, int i, SourceVariable v | - def.definesAt(v, bb, i) and - explicitWrite(write, bb, i, v) - ) - } - /** * An SSA definition that corresponds to an explicit variable update or * declaration. @@ -1688,10 +1722,6 @@ module Make< Expr getValue() { result = this.getDefinition().getValue() } } - private predicate parameterInit(WriteDefinition def, Parameter p) { - exists(VariableWrite write | explicitWrite(def, write) and write.isParameterInit(p)) - } - /** * An SSA definition representing the initialization of a parameter at the * beginning of a callable. @@ -1743,14 +1773,42 @@ module Make< * An SSA phi definition, that is, a pseudo definition for a variable at a * point in the flow graph where otherwise two or more definitions for the * variable would be visible. + * + * For example, in + * ```rb + * if b + * x = 0 + * else + * x = 1 + * end + * puts x + * ``` + * a phi definition for `x` is inserted just before the call `puts x`. */ class SsaPhiDefinition extends SsaDefinition { - /** Holds if `inp` is an input to the phi definition along the edge originating in `bb`. */ + /** Holds if `inp` is an input to this phi definition along the edge originating in `bb`. */ predicate hasInputFromBlock(SsaDefinition inp, BasicBlock bb) { phiHasInputFromBlockCached(this, inp, bb) } - /** Gets an input of this phi definition. */ + /** + * Gets an input of this phi definition. + * + * Example: + * + * ```rb + * def m b + * i = 0 # defines i_0 + * if b + * i = 1 # defines i_1 + * else + * i = 2 # defines i_2 + * end + * # defines i_3 = phi(i_1, i_2); inputs are i_1 and i_2 + * puts i + * end + * ``` + */ SsaDefinition getAnInput() { this.hasInputFromBlock(result, _) } } } From 242f12d4befd7b1048d35d930f2a87a8ff2ddcf4 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Tue, 21 Oct 2025 10:52:49 +0200 Subject: [PATCH 3/3] SSA: Remove variable capture reference from shared class. --- shared/ssa/codeql/ssa/Ssa.qll | 26 +------------------------- 1 file changed, 1 insertion(+), 25 deletions(-) diff --git a/shared/ssa/codeql/ssa/Ssa.qll b/shared/ssa/codeql/ssa/Ssa.qll index 6321e1b8d75c..5edf51127b8e 100644 --- a/shared/ssa/codeql/ssa/Ssa.qll +++ b/shared/ssa/codeql/ssa/Ssa.qll @@ -1555,17 +1555,6 @@ module Make< } predicate explicitWrite(VariableWrite w, BasicBlock bb, int i, SourceVariable v); - - /** - * Holds if `closureVar` is a local variable inside a closure that captures - * `captured`, which is the same variable in its declaring scope. The - * capture occurs at index `i` in basic block `bb`, and - * `variableRead(bb, i, captured, false)` must hold in order to include a - * pseudo-read of the captured variable at the point of capture. - */ - predicate variableCapture( - SourceVariable captured, SourceVariable closureVar, BasicBlock bb, int i - ); } module MakeSsa implements @@ -1593,15 +1582,6 @@ module Make< variableRead(bb, i, v, false) } - /** Holds if `init` is a closure variable that captures the value of `capturedvar`. */ - cached - predicate captures(SsaImplicitEntryDefinition init, Definition capturedvar) { - exists(BasicBlock bb, int i | - ssaDefReachesRead(_, capturedvar, bb, i) and - variableCapture(capturedvar.getSourceVariable(), init.getSourceVariable(), bb, i) - ) - } - cached predicate isLiveAtEndOfBlock(Definition def, BasicBlock bb) { ssaDefReachesEndOfBlock(bb, def, _) @@ -1665,8 +1645,7 @@ module Make< */ private SsaDefinition getAPhiInputOrPriorDefinition() { result = this.(SsaPhiDefinition).getAnInput() or - result = this.(SsaUncertainWrite).getPriorDefinition() or - this.(SsaImplicitEntryDefinition).captures(result) + result = this.(SsaUncertainWrite).getPriorDefinition() } /** @@ -1755,9 +1734,6 @@ module Make< */ class SsaImplicitEntryDefinition extends SsaImplicitWrite { SsaImplicitEntryDefinition() { this.definesAt(_, any(EntryBasicBlock bb), -1) } - - /** Holds if this is a closure definition that captures the value of `capturedvar`. */ - predicate captures(SsaDefinition capturedvar) { captures(this, capturedvar) } } /** An SSA definition that represents an uncertain variable update. */