SSA: Add a shared signature for SSA and a module to implement it.

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<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,175 @@ 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.
+   */
+  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<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)
+      }
+
+      /** 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. */