Merge pull request #5071 from hvitved/csharp/ssa/uncertain-reads

C#: Move uncertain-read logic into 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

@@ -954,10 +954,12 @@ private predicate variableReadPseudo(ControlFlow::BasicBlock bb, int i, Ssa::Sou
  *
  * This includes implicit reads via calls.
  */
-predicate variableRead(ControlFlow::BasicBlock bb, int i, Ssa::SourceVariable v) {
-  variableReadActual(bb, i, v)
+predicate variableRead(ControlFlow::BasicBlock bb, int i, Ssa::SourceVariable v, boolean certain) {
+  variableReadActual(bb, i, v) and
+  certain = true
   or
-  variableReadPseudo(bb, i, v)
+  variableReadPseudo(bb, i, v) and
+  certain = false
 }
 
 cached
@@ -1073,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
@@ -1107,24 +1109,9 @@ private module Cached {
     ssaDefReachesEndOfBlock(bb, def, _)
   }
 
-  private predicate adjacentDefReaches(
-    Definition def, ControlFlow::BasicBlock bb1, int i1, ControlFlow::BasicBlock bb2, int i2
-  ) {
-    adjacentDefRead(def, bb1, i1, bb2, i2)
-    or
-    exists(ControlFlow::BasicBlock bb3, int i3 |
-      adjacentDefReaches(def, bb1, i1, bb3, i3) and
-      variableReadPseudo(bb3, i3, _) and
-      adjacentDefRead(def, bb3, i3, bb2, i2)
-    )
-  }
-
-  pragma[noinline]
-  private predicate adjacentDefActualRead(
-    Definition def, ControlFlow::BasicBlock bb1, int i1, ControlFlow::BasicBlock bb2, int i2
-  ) {
-    adjacentDefReaches(def, bb1, i1, bb2, i2) and
-    variableReadActual(bb2, i2, _)
+  cached
+  Definition phiHasInputFromBlock(PhiNode phi, ControlFlow::BasicBlock bb) {
+    phiHasInputFromBlock(phi, result, bb)
   }
 
   cached
@@ -1145,7 +1132,7 @@ private module Cached {
   predicate firstReadSameVar(Definition def, ControlFlow::Node cfn) {
     exists(ControlFlow::BasicBlock bb1, int i1, ControlFlow::BasicBlock bb2, int i2 |
       def.definesAt(_, bb1, i1) and
-      adjacentDefActualRead(def, bb1, i1, bb2, i2) and
+      adjacentDefNoUncertainReads(def, bb1, i1, bb2, i2) and
       cfn = bb2.getNode(i2)
     )
   }
@@ -1160,53 +1147,30 @@ private module Cached {
     exists(ControlFlow::BasicBlock bb1, int i1, ControlFlow::BasicBlock bb2, int i2 |
       cfn1 = bb1.getNode(i1) and
       variableReadActual(bb1, i1, _) and
-      adjacentDefActualRead(def, bb1, i1, bb2, i2) and
+      adjacentDefNoUncertainReads(def, bb1, i1, bb2, i2) and
       cfn2 = bb2.getNode(i2)
     )
   }
 
-  private predicate adjacentDefPseudoRead(
-    Definition def, ControlFlow::BasicBlock bb1, int i1, ControlFlow::BasicBlock bb2, int i2
-  ) {
-    adjacentDefReaches(def, bb1, i1, bb2, i2) and
-    variableReadPseudo(bb2, i2, _)
-  }
-
-  private predicate reachesLastRefRedef(
-    Definition def, ControlFlow::BasicBlock bb, int i, Definition next
-  ) {
-    lastRefRedef(def, bb, i, next)
-    or
-    exists(ControlFlow::BasicBlock bb0, int i0 |
-      reachesLastRefRedef(def, bb0, i0, next) and
-      adjacentDefPseudoRead(def, bb, i, bb0, i0)
-    )
-  }
-
   cached
   predicate lastRefBeforeRedef(Definition def, ControlFlow::BasicBlock bb, int i, Definition next) {
-    reachesLastRefRedef(def, bb, i, next) and
-    not variableReadPseudo(bb, i, def.getSourceVariable())
-  }
-
-  private predicate reachesLastRef(Definition def, ControlFlow::BasicBlock bb, int i) {
-    lastRef(def, bb, i)
-    or
-    exists(ControlFlow::BasicBlock bb0, int i0 |
-      reachesLastRef(def, bb0, i0) and
-      adjacentDefPseudoRead(def, bb, i, bb0, i0)
-    )
+    lastRefRedefNoUncertainReads(def, bb, i, next)
   }
 
   cached
   predicate lastReadSameVar(Definition def, ControlFlow::Node cfn) {
     exists(ControlFlow::BasicBlock bb, int i |
-      reachesLastRef(def, bb, i) and
+      lastRefNoUncertainReads(def, bb, i) and
       variableReadActual(bb, i, _) and
       cfn = bb.getNode(i)
     )
   }
 
+  cached
+  Definition uncertainWriteDefinitionInput(UncertainWriteDefinition def) {
+    uncertainWriteDefinitionInput(def, result)
+  }
+
   cached
   predicate isLiveOutRefParameterDefinition(Ssa::Definition def, Parameter p) {
     p.isOutOrRef() and