mirror of
https://github.com/github/codeql.git
synced 2025-12-16 16:53:25 +01:00
Merge pull request #20646 from aschackmull/ssa/ssa-sig
SSA: Add a shared signature for SSA and a module to implement it.
This commit is contained in:
Anders Schack-Mulligen
@@ -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<LocationSig Location, BasicBlockSig BasicBlock> {
|
||||
signature module InputSig<LocationSig Location, TypSig BasicBlock> {
|
||||
/** A variable that can be SSA converted. */
|
||||
class SourceVariable {
|
||||
/** Gets a textual representation of this variable. */
|
||||
@@ -42,6 +42,203 @@ signature module InputSig<LocationSig Location, BasicBlockSig BasicBlock> {
|
||||
predicate variableRead(BasicBlock bb, int i, SourceVariable v, boolean certain);
|
||||
}
|
||||
|
||||
/**
|
||||
* Provides classes and predicates for the SSA representation of variables.
|
||||
*
|
||||
* Class hierarchy:
|
||||
* ```text
|
||||
* SsaDefinition
|
||||
* |- SsaWriteDefinition
|
||||
* | |- SsaExplicitWrite
|
||||
* | | \- SsaParameterInit
|
||||
* | |- SsaImplicitWrite
|
||||
* | | \- SsaImplicitEntryDefinition
|
||||
* | \- SsaUncertainWrite (overlaps SsaImplicitWrite and potentially SsaExplicitWrite)
|
||||
* \- SsaPhiDefinition
|
||||
* ```
|
||||
*/
|
||||
signature module SsaSig<
|
||||
LocationSig Location, TypSig ControlFlowNode, TypSig BasicBlock, TypSig Expr, TypSig Parameter,
|
||||
TypSig VariableWrite>
|
||||
{
|
||||
/** A variable that can be SSA converted. */
|
||||
class SourceVariable {
|
||||
/** Gets a textual representation of this variable. */
|
||||
string toString();
|
||||
|
||||
/** Gets the location of this variable. */
|
||||
Location getLocation();
|
||||
}
|
||||
|
||||
/** A static single assignment (SSA) definition. */
|
||||
class SsaDefinition {
|
||||
/** Gets the source variable underlying this SSA definition. */
|
||||
SourceVariable getSourceVariable();
|
||||
|
||||
/**
|
||||
* Holds if this SSA definition defines `v` at index `i` in basic block `bb`.
|
||||
* Phi definitions are considered to be at index `-1`, while normal variable writes
|
||||
* are at the index of the control flow node they wrap.
|
||||
*/
|
||||
predicate definesAt(SourceVariable v, BasicBlock bb, int i);
|
||||
|
||||
/** Gets the basic block to which this SSA definition belongs. */
|
||||
BasicBlock getBasicBlock();
|
||||
|
||||
/**
|
||||
* Gets the control flow node of this SSA definition.
|
||||
*
|
||||
* For SSA definitions occurring at the beginning of a basic block, such as
|
||||
* phi definitions, this will get the first control flow node of the basic block.
|
||||
*/
|
||||
ControlFlowNode getControlFlowNode();
|
||||
|
||||
/** Gets a read of this SSA definition. */
|
||||
Expr getARead();
|
||||
|
||||
/**
|
||||
* Holds if this SSA definition is live at the end of basic block `bb`.
|
||||
* That is, this definition reaches the end of basic block `bb`, at which
|
||||
* point it is still live, without crossing another SSA definition of the
|
||||
* same source variable.
|
||||
*/
|
||||
predicate isLiveAtEndOfBlock(BasicBlock bb);
|
||||
|
||||
/**
|
||||
* Gets a definition that ultimately defines this SSA definition and is
|
||||
* not itself a phi definition.
|
||||
*
|
||||
* Example:
|
||||
*
|
||||
* ```rb
|
||||
* def m b
|
||||
* i = 0 # defines i_0
|
||||
* if b
|
||||
* i = 1 # defines i_1
|
||||
* else
|
||||
* i = 2 # defines i_2
|
||||
* end
|
||||
* # defines i_3 = phi(i_1, i_2); ultimate definitions are i_1 and i_2
|
||||
* puts i
|
||||
* end
|
||||
* ```
|
||||
*/
|
||||
SsaDefinition getAnUltimateDefinition();
|
||||
|
||||
/** Gets a textual representation of this SSA definition. */
|
||||
string toString();
|
||||
|
||||
/** Gets the location of this SSA definition. */
|
||||
Location getLocation();
|
||||
}
|
||||
|
||||
/**
|
||||
* A write definition. This includes every definition that is not a phi
|
||||
* definition.
|
||||
*/
|
||||
class SsaWriteDefinition extends SsaDefinition;
|
||||
|
||||
/**
|
||||
* An SSA definition that corresponds to an explicit variable update or
|
||||
* declaration.
|
||||
*/
|
||||
class SsaExplicitWrite extends SsaWriteDefinition {
|
||||
/** Gets the write underlying this SSA definition. */
|
||||
VariableWrite getDefinition();
|
||||
|
||||
/**
|
||||
* Gets the expression representing this write, if any. This is equivalent
|
||||
* to `getDefinition().asExpr()`.
|
||||
*/
|
||||
Expr getDefiningExpr();
|
||||
|
||||
/**
|
||||
* Gets the expression with the value being written, if any. This is
|
||||
* equivalent to `getDefinition().getValue()`.
|
||||
*/
|
||||
Expr getValue();
|
||||
}
|
||||
|
||||
/**
|
||||
* An SSA definition representing the initialization of a parameter at the
|
||||
* beginning of a callable.
|
||||
*/
|
||||
class SsaParameterInit extends SsaExplicitWrite {
|
||||
/**
|
||||
* Gets the parameter that this definition represents. This is equivalent
|
||||
* to `getDefinition().isParameterInit(result)`
|
||||
*/
|
||||
Parameter getParameter();
|
||||
}
|
||||
|
||||
/**
|
||||
* An SSA definition that does not correspond to an explicit variable
|
||||
* update or declaration.
|
||||
*
|
||||
* This includes implicit entry definitions for fields and captured
|
||||
* variables, as well as field updates through side-effects and implicit
|
||||
* definitions for fields whenever the qualifier is updated.
|
||||
*/
|
||||
class SsaImplicitWrite extends SsaWriteDefinition;
|
||||
|
||||
/**
|
||||
* An SSA definition representing the implicit initialization of a variable
|
||||
* at the beginning of a callable. This includes fields and captured
|
||||
* variables, but excludes parameters as they have explicit declarations.
|
||||
*/
|
||||
class SsaImplicitEntryDefinition extends SsaImplicitWrite;
|
||||
|
||||
/** An SSA definition that represents an uncertain variable update. */
|
||||
class SsaUncertainWrite extends SsaWriteDefinition {
|
||||
/**
|
||||
* Gets the immediately preceding definition. Since this update is uncertain,
|
||||
* the value from the preceding definition might still be valid.
|
||||
*/
|
||||
SsaDefinition getPriorDefinition();
|
||||
}
|
||||
|
||||
/**
|
||||
* An SSA phi definition, that is, a pseudo definition for a variable at a
|
||||
* point in the flow graph where otherwise two or more definitions for the
|
||||
* variable would be visible.
|
||||
*
|
||||
* For example, in
|
||||
* ```rb
|
||||
* if b
|
||||
* x = 0
|
||||
* else
|
||||
* x = 1
|
||||
* end
|
||||
* puts x
|
||||
* ```
|
||||
* a phi definition for `x` is inserted just before the call `puts x`.
|
||||
*/
|
||||
class SsaPhiDefinition extends SsaDefinition {
|
||||
/** Holds if `inp` is an input to this phi definition along the edge originating in `bb`. */
|
||||
predicate hasInputFromBlock(SsaDefinition inp, BasicBlock bb);
|
||||
|
||||
/**
|
||||
* Gets an input of this phi definition.
|
||||
*
|
||||
* Example:
|
||||
*
|
||||
* ```rb
|
||||
* def m b
|
||||
* i = 0 # defines i_0
|
||||
* if b
|
||||
* i = 1 # defines i_1
|
||||
* else
|
||||
* i = 2 # defines i_2
|
||||
* end
|
||||
* # defines i_3 = phi(i_1, i_2); inputs are i_1 and i_2
|
||||
* puts i
|
||||
* end
|
||||
* ```
|
||||
*/
|
||||
SsaDefinition getAnInput();
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* Provides an SSA implementation.
|
||||
*
|
||||
@@ -1319,6 +1516,279 @@ 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 parameter `p`. */
|
||||
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);
|
||||
}
|
||||
|
||||
module MakeSsa<SsaInputSig SsaInput> implements
|
||||
SsaSig<Location, ControlFlowNode, BasicBlock, SsaInput::Expr, SsaInput::Parameter, SsaInput::VariableWrite>
|
||||
{
|
||||
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)
|
||||
}
|
||||
|
||||
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)
|
||||
}
|
||||
|
||||
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;
|
||||
|
||||
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()
|
||||
}
|
||||
|
||||
/**
|
||||
* 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 { }
|
||||
|
||||
/**
|
||||
* 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() }
|
||||
}
|
||||
|
||||
/**
|
||||
* 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) }
|
||||
}
|
||||
|
||||
/** 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.
|
||||
*
|
||||
* For example, in
|
||||
* ```rb
|
||||
* if b
|
||||
* x = 0
|
||||
* else
|
||||
* x = 1
|
||||
* end
|
||||
* puts x
|
||||
* ```
|
||||
* a phi definition for `x` is inserted just before the call `puts x`.
|
||||
*/
|
||||
class SsaPhiDefinition extends SsaDefinition {
|
||||
/** Holds if `inp` is an input to this phi definition along the edge originating in `bb`. */
|
||||
predicate hasInputFromBlock(SsaDefinition inp, BasicBlock bb) {
|
||||
phiHasInputFromBlockCached(this, inp, bb)
|
||||
}
|
||||
|
||||
/**
|
||||
* Gets an input of this phi definition.
|
||||
*
|
||||
* Example:
|
||||
*
|
||||
* ```rb
|
||||
* def m b
|
||||
* i = 0 # defines i_0
|
||||
* if b
|
||||
* i = 1 # defines i_1
|
||||
* else
|
||||
* i = 2 # defines i_2
|
||||
* end
|
||||
* # defines i_3 = phi(i_1, i_2); inputs are i_1 and i_2
|
||||
* puts i
|
||||
* end
|
||||
* ```
|
||||
*/
|
||||
SsaDefinition getAnInput() { this.hasInputFromBlock(result, _) }
|
||||
}
|
||||
}
|
||||
|
||||
/** Provides a set of consistency queries. */
|
||||
module Consistency {
|
||||
/** Holds if a read can be reached from multiple definitions. */
|
||||
|
||||
Reference in New Issue
Block a user