C#: Move uncertain-read logic into shared SSA implementation

Author: hvitved

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
@@ -1107,26 +1109,6 @@ 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
   AssignableRead getAReadAtNode(Definition def, ControlFlow::Node cfn) {
     exists(Ssa::SourceVariable v, ControlFlow::BasicBlock bb, int i |
@@ -1145,7 +1127,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,48 +1142,20 @@ 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)
     )

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

@@ -17,18 +17,18 @@ private module Liveness {
    * (certain or uncertain) writes.
    */
   private newtype TRefKind =
-    Read() or
-    Write(boolean certain) { certain = true or certain = false }
+    Read(boolean certain) { certain in [false, true] } or
+    Write(boolean certain) { certain in [false, true] }
 
   private class RefKind extends TRefKind {
     string toString() {
-      this = Read() and result = "read"
+      exists(boolean certain | this = Read(certain) and result = "read (" + certain + ")")
       or
       exists(boolean certain | this = Write(certain) and result = "write (" + certain + ")")
     }
 
     int getOrder() {
-      this = Read() and
+      this = Read(_) and
       result = 0
       or
       this = Write(_) and
@@ -40,7 +40,7 @@ private module Liveness {
    * Holds if the `i`th node of basic block `bb` is a reference to `v` of kind `k`.
    */
   private predicate ref(BasicBlock bb, int i, SourceVariable v, RefKind k) {
-    variableRead(bb, i, v) and k = Read()
+    exists(boolean certain | variableRead(bb, i, v, certain) | k = Read(certain))
     or
     exists(boolean certain | variableWrite(bb, i, v, certain) | k = Write(certain))
   }
@@ -95,7 +95,7 @@ private module Liveness {
    */
   predicate liveAtEntry(BasicBlock bb, SourceVariable v) {
     // The first read or certain write to `v` inside `bb` is a read
-    refRank(bb, _, v, Read()) = firstReadOrCertainWrite(bb, v)
+    refRank(bb, _, v, Read(_)) = firstReadOrCertainWrite(bb, v)
     or
     // There is no certain write to `v` inside `bb`, but `v` is live at entry
     // to a successor basic block of `bb`
@@ -120,7 +120,7 @@ private module Liveness {
       liveAtExit(bb, v)
       or
       ref(bb, i, v, kind) and
-      kind = Read()
+      kind = Read(_)
       or
       exists(RefKind nextKind |
         liveAtRank(bb, _, v, rnk + 1) and
@@ -237,7 +237,7 @@ private module SsaDefReaches {
    * Unlike `Liveness::ref`, this includes `phi` nodes.
    */
   predicate ssaRef(BasicBlock bb, int i, SourceVariable v, SsaRefKind k) {
-    variableRead(bb, i, v) and
+    variableRead(bb, i, v, _) and
     k = SsaRead()
     or
     exists(Definition def | def.definesAt(v, bb, i)) and
@@ -304,7 +304,7 @@ private module SsaDefReaches {
     exists(int rnk |
       ssaDefReachesRank(bb, def, rnk, v) and
       rnk = ssaRefRank(bb, i, v, SsaRead()) and
-      variableRead(bb, i, v)
+      variableRead(bb, i, v, _)
     )
   }
 
@@ -368,7 +368,7 @@ private module SsaDefReaches {
   predicate defAdjacentRead(Definition def, BasicBlock bb1, BasicBlock bb2, int i2) {
     varBlockReaches(def, bb1, bb2) and
     ssaRefRank(bb2, i2, def.getSourceVariable(), SsaRead()) = 1 and
-    variableRead(bb2, i2, _)
+    variableRead(bb2, i2, _, _)
   }
 }
 
@@ -394,6 +394,7 @@ private predicate ssaDefReachesEndOfBlockRec(BasicBlock bb, Definition def, Sour
  * block `bb`, at which point it is still live, without crossing another
  * SSA definition of `v`.
  */
+pragma[nomagic]
 predicate ssaDefReachesEndOfBlock(BasicBlock bb, Definition def, SourceVariable v) {
   exists(int last | last = maxSsaRefRank(bb, v) |
     ssaDefReachesRank(bb, def, last, v) and
@@ -412,10 +413,11 @@ predicate ssaDefReachesEndOfBlock(BasicBlock bb, Definition def, SourceVariable
  * basic block `bb`, without crossing another SSA definition of `v`. The read
  * is of kind `rk`.
  */
+pragma[nomagic]
 predicate ssaDefReachesRead(SourceVariable v, Definition def, BasicBlock bb, int i) {
   ssaDefReachesReadWithinBlock(v, def, bb, i)
   or
-  variableRead(bb, i, v) and
+  variableRead(bb, i, v, _) and
   ssaDefReachesEndOfBlock(getABasicBlockPredecessor(bb), def, v) and
   not ssaDefReachesReadWithinBlock(v, _, bb, i)
 }
@@ -427,25 +429,51 @@ predicate ssaDefReachesRead(SourceVariable v, Definition def, BasicBlock bb, int
  * or a write), `def` is read at index `i2` in basic block `bb2`, and there is a
  * path between them without any read of `def`.
  */
+pragma[nomagic]
 predicate adjacentDefRead(Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2) {
   exists(int rnk |
     rnk = ssaDefRank(def, _, bb1, i1, _) and
     rnk + 1 = ssaDefRank(def, _, bb1, i2, SsaRead()) and
-    variableRead(bb1, i2, _) and
+    variableRead(bb1, i2, _, _) and
     bb2 = bb1
   )
   or
   exists(SourceVariable v | ssaDefRank(def, v, bb1, i1, _) = maxSsaRefRank(bb1, v)) and
   defAdjacentRead(def, bb1, bb2, i2)
 }
 
+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)
+  or
+  exists(BasicBlock bb3, int i3 |
+    adjacentDefReachesRead(def, bb1, i1, bb3, i3) and
+    variableRead(bb3, i3, _, false) and
+    adjacentDefRead(def, bb3, i3, bb2, i2)
+  )
+}
+
+/**
+ * NB: If this predicate is exposed, it should be cached.
+ *
+ * Same as `adjacentDefRead`, but ignores uncertain reads.
+ */
+pragma[nomagic]
+predicate adjacentDefNoUncertainReads(Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2) {
+  adjacentDefReachesRead(def, bb1, i1, bb2, i2) and
+  variableRead(bb2, i2, _, true)
+}
+
 /**
  * NB: If this predicate is exposed, it should be cached.
  *
  * Holds if the node at index `i` in `bb` is a last reference to SSA definition
  * `def`. The reference is last because it can reach another write `next`,
  * without passing through another read or write.
  */
+pragma[nomagic]
 predicate lastRefRedef(Definition def, BasicBlock bb, int i, Definition next) {
   exists(int rnk, SourceVariable v, int j | rnk = ssaDefRank(def, v, bb, i, _) |
     // Next reference to `v` inside `bb` is a write
@@ -462,6 +490,29 @@ predicate lastRefRedef(Definition def, BasicBlock bb, int i, Definition next) {
   )
 }
 
+private predicate adjacentDefReachesUncertainRead(
+  Definition def, BasicBlock bb1, int i1, BasicBlock bb2, int i2
+) {
+  adjacentDefReachesRead(def, bb1, i1, bb2, i2) and
+  variableRead(bb2, i2, _, false)
+}
+
+/**
+ * NB: If this predicate is exposed, it should be cached.
+ *
+ * Same as `lastRefRedef`, but ignores uncertain reads.
+ */
+pragma[nomagic]
+predicate lastRefRedefNoUncertainReads(Definition def, BasicBlock bb, int i, Definition next) {
+  lastRefRedef(def, bb, i, next) and
+  not variableRead(bb, i, def.getSourceVariable(), false)
+  or
+  exists(BasicBlock bb0, int i0 |
+    lastRefRedef(def, bb0, i0, next) and
+    adjacentDefReachesUncertainRead(def, bb, i, bb0, i0)
+  )
+}
+
 /**
  * NB: If this predicate is exposed, it should be cached.
  *
@@ -472,6 +523,7 @@ predicate lastRefRedef(Definition def, BasicBlock bb, int i, Definition next) {
  * SSA definition for the underlying source variable, without passing through
  * another read.
  */
+pragma[nomagic]
 predicate lastRef(Definition def, BasicBlock bb, int i) {
   lastRefRedef(def, bb, i, _)
   or
@@ -487,6 +539,22 @@ predicate lastRef(Definition def, BasicBlock bb, int i) {
   )
 }
 
+/**
+ * NB: If this predicate is exposed, it should be cached.
+ *
+ * Same as `lastRefRedef`, but ignores uncertain reads.
+ */
+pragma[nomagic]
+predicate lastRefNoUncertainReads(Definition def, BasicBlock bb, int i) {
+  lastRef(def, bb, i) and
+  not variableRead(bb, i, def.getSourceVariable(), false)
+  or
+  exists(BasicBlock bb0, int i0 |
+    lastRef(def, bb0, i0) and
+    adjacentDefReachesUncertainRead(def, bb, i, bb0, i0)
+  )
+}
+
 /** A static single assignment (SSA) definition. */
 class Definition extends TDefinition {
   /** Gets the source variable underlying this SSA definition. */

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

@@ -16,4 +16,4 @@ class SourceVariable = SsaImpl::TSourceVariable;
 
 predicate variableWrite = SsaImpl::variableWrite/4;
 
-predicate variableRead = SsaImpl::variableRead/3;
+predicate variableRead = SsaImpl::variableRead/4;