C#: Only cache TDefinition in the shared SSA implementation

Author: hvitved

csharp/ql/src/semmle/code/csharp/dataflow/SSA.qll

@@ -384,9 +384,18 @@ module Ssa {
       result.getAControlFlowNode() = cfn
     }
 
+    /**
+     * Gets an SSA definition whose value can flow to this one in one step. This
+     * includes inputs to phi nodes and the prior definitions of uncertain writes.
+     */
+    private Definition getAPhiInputOrPriorDefinition() {
+      result = this.(PhiNode).getAnInput() or
+      result = this.(UncertainDefinition).getPriorDefinition()
+    }
+
     /**
      * Gets a definition that ultimately defines this SSA definition and is
-     * not itself a pseudo node. Example:
+     * not itself a phi node. Example:
      *
      * ```csharp
      * int Field;
@@ -413,8 +422,9 @@ module Ssa {
      *   definition on line 4, the explicit definition on line 7, and the implicit
      *   definition on line 9.
      */
-    final override Definition getAnUltimateDefinition() {
-      result = SsaImpl::Definition.super.getAnUltimateDefinition()
+    final Definition getAnUltimateDefinition() {
+      result = this.getAPhiInputOrPriorDefinition*() and
+      not result instanceof PhiNode
     }
 
     /**
@@ -425,7 +435,7 @@ module Ssa {
     /**
      * Gets the syntax element associated with this SSA definition, if any.
      * This is either an expression, for example `x = 0`, a parameter, or a
-     * callable. Pseudo nodes have no associated syntax element.
+     * callable. Phi nodes have no associated syntax element.
      */
     Element getElement() { result = this.getControlFlowNode().getElement() }
 
@@ -681,7 +691,12 @@ module Ssa {
      *   definition on line 4, the explicit definition on line 7, and the implicit
      *   call definition on line 9 as inputs.
      */
-    final override Definition getAnInput() { result = SsaImpl::PhiNode.super.getAnInput() }
+    final Definition getAnInput() { this.hasInputFromBlock(result, _) }
+
+    /** Holds if `inp` is an input to this phi node along the edge originating in `bb`. */
+    predicate hasInputFromBlock(Definition inp, ControlFlow::BasicBlock bb) {
+      inp = SsaImpl::phiHasInputFromBlock(this, bb)
+    }
 
     override string toString() {
       result = getToStringPrefix(this) + "SSA phi(" + getSourceVariable() + ")"
@@ -704,5 +719,11 @@ module Ssa {
    * need not be certain), an implicit non-local update via a call, or an
    * uncertain update of the qualifier.
    */
-  class UncertainDefinition extends Definition, SsaImpl::UncertainWriteDefinition { }
+  class UncertainDefinition extends Definition, SsaImpl::UncertainWriteDefinition {
+    /**
+     * Gets the immediately preceding definition. Since this update is uncertain,
+     * the value from the preceding definition might still be valid.
+     */
+    Definition getPriorDefinition() { result = SsaImpl::uncertainWriteDefinitionInput(this) }
+  }
 }

csharp/ql/src/semmle/code/csharp/dataflow/internal/SsaImpl.qll

@@ -1075,7 +1075,7 @@ private module Cached {
     Ssa::ExplicitDefinition def, Ssa::ImplicitEntryDefinition edef,
     ControlFlow::Nodes::ElementNode c, boolean additionalCalls
   ) {
-    exists(Ssa::SourceVariable v, Definition def0, ControlFlow::BasicBlock bb, int i |
+    exists(Ssa::SourceVariable v, Ssa::Definition def0, ControlFlow::BasicBlock bb, int i |
       v = def.getSourceVariable() and
       capturedReadIn(_, _, v, edef.getSourceVariable(), c, additionalCalls) and
       def = def0.getAnUltimateDefinition() and
@@ -1109,6 +1109,11 @@ private module Cached {
     ssaDefReachesEndOfBlock(bb, def, _)
   }
 
+  cached
+  Definition phiHasInputFromBlock(PhiNode phi, ControlFlow::BasicBlock bb) {
+    phiHasInputFromBlock(phi, result, bb)
+  }
+
   cached
   AssignableRead getAReadAtNode(Definition def, ControlFlow::Node cfn) {
     exists(Ssa::SourceVariable v, ControlFlow::BasicBlock bb, int i |
@@ -1161,6 +1166,11 @@ private module Cached {
     )
   }
 
+  cached
+  Definition uncertainWriteDefinitionInput(UncertainWriteDefinition def) {
+    uncertainWriteDefinitionInput(def, result)
+  }
+
   cached
   predicate isLiveOutRefParameterDefinition(Ssa::Definition def, Parameter p) {
     p.isOutOrRef() and

csharp/ql/src/semmle/code/csharp/dataflow/internal/SsaImplCommon.qll

@@ -174,34 +174,15 @@ private predicate inDefDominanceFrontier(BasicBlock bb, SourceVariable v) {
 }
 
 cached
-private module Cached {
-  cached
-  newtype TDefinition =
-    TWriteDef(SourceVariable v, BasicBlock bb, int i) {
-      variableWrite(bb, i, v, _) and
-      liveAfterWrite(bb, i, v)
-    } or
-    TPhiNode(SourceVariable v, BasicBlock bb) {
-      inDefDominanceFrontier(bb, v) and
-      liveAtEntry(bb, v)
-    }
-
-  cached
-  predicate uncertainWriteDefinitionInput(UncertainWriteDefinition def, Definition inp) {
-    lastRefRedef(inp, _, _, def)
-  }
-
-  cached
-  predicate phiHasInputFromBlock(PhiNode phi, Definition inp, BasicBlock bb) {
-    exists(SourceVariable v, BasicBlock bbDef |
-      phi.definesAt(v, bbDef, _) and
-      getABasicBlockPredecessor(bbDef) = bb and
-      ssaDefReachesEndOfBlock(bb, inp, v)
-    )
+newtype TDefinition =
+  TWriteDef(SourceVariable v, BasicBlock bb, int i) {
+    variableWrite(bb, i, v, _) and
+    liveAfterWrite(bb, i, v)
+  } or
+  TPhiNode(SourceVariable v, BasicBlock bb) {
+    inDefDominanceFrontier(bb, v) and
+    liveAtEntry(bb, v)
   }
-}
-
-import Cached
 
 private module SsaDefReaches {
   newtype TSsaRefKind =
@@ -406,6 +387,20 @@ predicate ssaDefReachesEndOfBlock(BasicBlock bb, Definition def, SourceVariable
   not ssaRef(bb, _, v, SsaDef())
 }
 
+/**
+ * NB: If this predicate is exposed, it should be cached.
+ *
+ * Holds if `inp` is an input to the phi node `phi` along the edge originating in `bb`.
+ */
+pragma[nomagic]
+predicate phiHasInputFromBlock(PhiNode phi, Definition inp, BasicBlock bb) {
+  exists(SourceVariable v, BasicBlock bbDef |
+    phi.definesAt(v, bbDef, _) and
+    getABasicBlockPredecessor(bbDef) = bb and
+    ssaDefReachesEndOfBlock(bb, inp, v)
+  )
+}
+
 /**
  * NB: If this predicate is exposed, it should be cached.
  *
@@ -446,7 +441,11 @@ private predicate adjacentDefReachesRead(
   Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2
 ) {
   adjacentDefRead(def, bb1, i1, bb2, i2) and
-  not variableRead(bb1, i1, def.getSourceVariable(), false)
+  exists(SourceVariable v | v = def.getSourceVariable() |
+    ssaRef(bb1, i1, v, SsaDef())
+    or
+    variableRead(bb1, i1, v, true)
+  )
   or
   exists(BasicBlock bb3, int i3 |
     adjacentDefReachesRead(def, bb1, i1, bb3, i3) and
@@ -490,6 +489,18 @@ predicate lastRefRedef(Definition def, BasicBlock bb, int i, Definition next) {
   )
 }
 
+/**
+ * NB: If this predicate is exposed, it should be cached.
+ *
+ * Holds if `inp` is an immediately preceding definition of uncertain definition
+ * `def`. Since `def` is uncertain, the value from the preceding definition might
+ * still be valid.
+ */
+pragma[nomagic]
+predicate uncertainWriteDefinitionInput(UncertainWriteDefinition def, Definition inp) {
+  lastRefRedef(inp, _, _, def)
+}
+
 private predicate adjacentDefReachesUncertainRead(
   Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2
 ) {
@@ -574,24 +585,6 @@ class Definition extends TDefinition {
   /** Gets the basic block to which this SSA definition belongs. */
   final BasicBlock getBasicBlock() { this.definesAt(_, result, _) }
 
-  /**
-   * Gets an SSA definition whose value can flow to this one in one step. This
-   * includes inputs to phi nodes and the prior definitions of uncertain writes.
-   */
-  private Definition getAPseudoInputOrPriorDefinition() {
-    result = this.(PhiNode).getAnInput() or
-    result = this.(UncertainWriteDefinition).getPriorDefinition()
-  }
-
-  /**
-   * Gets a definition that ultimately defines this SSA definition and is
-   * not itself a phi node.
-   */
-  Definition getAnUltimateDefinition() {
-    result = this.getAPseudoInputOrPriorDefinition*() and
-    not result instanceof PhiNode
-  }
-
   /** Gets a textual representation of this SSA definition. */
   string toString() { none() }
 }
@@ -609,12 +602,6 @@ class WriteDefinition extends Definition, TWriteDef {
 
 /** A phi node. */
 class PhiNode extends Definition, TPhiNode {
-  /** Gets an input of this phi node. */
-  Definition getAnInput() { this.hasInputFromBlock(result, _) }
-
-  /** Holds if `inp` is an input to the phi node along the edge originating in `bb`. */
-  predicate hasInputFromBlock(Definition inp, BasicBlock bb) { phiHasInputFromBlock(this, inp, bb) }
-
   override string toString() { result = "Phi" }
 }
 
@@ -629,10 +616,4 @@ class UncertainWriteDefinition extends WriteDefinition {
       variableWrite(bb, i, v, false)
     )
   }
-
-  /**
-   * Gets the immediately preceding definition. Since this update is uncertain,
-   * the value from the preceding definition might still be valid.
-   */
-  Definition getPriorDefinition() { uncertainWriteDefinitionInput(this, result) }
 }