C#: Account for CFG splitting in AssignableDefinition::getAFirstRead() and AssignableRead::getANextRead()

Author: hvitved

csharp/ql/src/semmle/code/csharp/Assignable.qll

@@ -100,7 +100,10 @@ class AssignableRead extends AssignableAccess {
    * - The read of `this.Field` on line 11 is next to the read on line 10.
    */
   AssignableRead getANextRead() {
-    Ssa::Internal::adjacentReadPairSameVar(this, result)
+    forex(ControlFlow::Node cfn |
+      cfn = result.getAControlFlowNode() |
+      Ssa::Internal::adjacentReadPairSameVar(this.getAControlFlowNode(), cfn)
+    )
   }
 
   /**
@@ -502,9 +505,12 @@ class AssignableDefinition extends TAssignableDefinition {
    * `AssignableRead.getANextRead()`.
    */
   AssignableRead getAFirstRead() {
-    exists(Ssa::ExplicitDefinition def |
-      def.getADefinition() = this |
-      result = def.getAFirstRead()
+    forex(ControlFlow::Node cfn |
+      cfn = result.getAControlFlowNode() |
+      exists(Ssa::ExplicitDefinition def |
+        result = def.getAFirstReadAtNode(cfn) |
+        this = def.(Ssa::ExplicitDefinition).getADefinition()
+      )
     )
   }
 

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

@@ -423,20 +423,20 @@ private Ssa::Definition getAnUltimateDefinition(Ssa::Definition def) {
 }
 
 /**
- * Holds if SSA definition `def` can reach a read `ar`, without passing
+ * Holds if SSA definition `def` can reach a read at `cfn`, without passing
  * through an intermediate dereference that always (`always = true`) or
  * maybe (`always = false`) throws a null reference exception.
  */
-private predicate defReaches(Ssa::Definition def, AssignableRead ar, boolean always) {
-  ar = def.getAFirstRead() and
+private predicate defReaches(Ssa::Definition def, ControlFlow::Node cfn, boolean always) {
+  exists(def.getAFirstReadAtNode(cfn)) and
   (always = true or always = false)
   or
-  exists(AssignableRead mid |
+  exists(ControlFlow::Node mid |
     defReaches(def, mid, always) |
-    ar = mid.getANextRead() and
+    Ssa::Internal::adjacentReadPairSameVar(mid, cfn) and
     not mid = any(Dereference d |
       if always = true then d.isAlwaysNull(def.getSourceVariable()) else d.isMaybeNull(def, _, _, _, _)
-    )
+    ).getAControlFlowNode()
   )
 }
 
@@ -528,7 +528,7 @@ class Dereference extends G::DereferenceableExpr {
    */
   predicate isFirstAlwaysNull(Ssa::SourceVariable v) {
     this.isAlwaysNull(v) and
-    defReaches(v.getAnSsaDefinition(), this, true)
+    defReaches(v.getAnSsaDefinition(), this.getAControlFlowNode(), true)
   }
 
   /**
@@ -551,6 +551,6 @@ class Dereference extends G::DereferenceableExpr {
    */
   predicate isFirstMaybeNull(Ssa::Definition def, SourcePathNode source, SinkPathNode sink, string msg, Element reason) {
     this.isMaybeNull(def, source, sink, msg, reason) and
-    defReaches(def, this, false)
+    defReaches(def, this.getAControlFlowNode(), false)
   }
 }

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

@@ -760,16 +760,16 @@ module Ssa {
 
     private cached module Cached {
       /**
-       * Holds if `read` is a last read of the non-trivial SSA definition `def`.
-       * That is, `read` can reach the end of the enclosing callable, or another
+       * Holds if `cfn` is a last read of the non-trivial SSA definition `def`.
+       * That is, `cfn` can reach the end of the enclosing callable, or another
        * SSA definition for the underlying source variable, without passing through
        * another read.
        */
       cached
-      predicate lastRead(TrackedDefinition def, AssignableRead read) {
+      predicate lastRead(TrackedDefinition def, ControlFlow::Node cfn) {
         exists(TrackedVar v, BasicBlock bb, int i, int rnk |
-          read = def.getARead() and
-          variableRead(bb, i, v, read.getAControlFlowNode(), _) and
+          exists(def.getAReadAtNode(cfn)) and
+          variableRead(bb, i, v, cfn, _) and
           rnk = ssaRefRank(bb, i, v, SsaRead()) |
           // Next reference to `v` inside `bb` is a write
           rnk + 1 = ssaRefRank(bb, _, v, SsaDef())
@@ -854,27 +854,29 @@ module Ssa {
       }
 
       /**
-       * Holds if the value defined at non-trivial SSA definition `def` can reach `read`
-       * without passing through any other read.
+       * Holds if the value defined at non-trivial SSA definition `def` can reach a
+       * read at `cfn`, without passing through any other read.
        */
       cached
-      predicate firstReadSameVar(TrackedDefinition def, AssignableRead read) {
+      predicate firstReadSameVar(TrackedDefinition def, ControlFlow::Node cfn) {
         exists(TrackedVar v, BasicBlock b1, int i1, BasicBlock b2, int i2 |
           adjacentVarRefs(v, b1, i1, b2, i2) and
           definesAt(def, b1, i1, v) and
-          variableRead(b2, i2, v, read.getAControlFlowNode(), _)
+          variableRead(b2, i2, v, cfn, _)
         )
       }
 
       /**
-       * INTERNAL: Use `AssignableRead.getANextRead()` instead.
+       * Holds if the read at `cfn2` is a read of the same SSA definition as the
+       * read at `cfn1`, and `cfn2` can be reached from `cfn1` without passing
+       * through another read.
        */
       cached
-      predicate adjacentReadPairSameVar(AssignableRead read1, AssignableRead read2) {
+      predicate adjacentReadPairSameVar(ControlFlow::Node cfn1, ControlFlow::Node cfn2) {
         exists(TrackedVar v, BasicBlock bb1, int i1, BasicBlock bb2, int i2 |
           adjacentVarRefs(v, bb1, i1, bb2, i2) and
-          variableRead(bb1, i1, v, read1.getAControlFlowNode(), _) and
-          variableRead(bb2, i2, v, read2.getAControlFlowNode(), _)
+          variableRead(bb1, i1, v, cfn1, _) and
+          variableRead(bb2, i2, v, cfn2, _)
         )
       }
     }
@@ -2074,8 +2076,45 @@ module Ssa {
      * Subsequent reads can be found by following the steps defined by
      * `AssignableRead.getANextRead()`.
      */
-    AssignableRead getAFirstRead() {
-      firstReadSameVar(this, result)
+    AssignableRead getAFirstRead() { result = this.getAFirstReadAtNode(_) }
+
+    /**
+     * Gets a read of the source variable underlying this SSA definition at
+     * control flow node `cfn` that can be reached from this SSA definition
+     * without passing through any other SSA definition or read. Example:
+     *
+     * ```
+     * int Field;
+     *
+     * void SetField(int i) {
+     *   this.Field = i;
+     *   Use(this.Field);
+     *   if (i > 0)
+     *     this.Field = i - 1;
+     *   else if (i < 0)
+     *     SetField(1);
+     *   Use(this.Field);
+     *   Use(this.Field);
+     * }
+     * ```
+     *
+     * - The read of `i` on line 4 can be reached from the explicit SSA
+     *   definition (wrapping an implicit entry definition) on line 3.
+     * - The reads of `i` on lines 6 and 7 are not the first reads of any SSA
+     *   definition.
+     * - The read of `this.Field` on line 5 can be reached from the explicit SSA
+     *   definition on line 4.
+     * - The read of `this.Field` on line 10 can be reached from the phi node
+     *   between lines 9 and 10.
+     * - The read of `this.Field` on line 11 is not the first read of any SSA
+     *   definition.
+     *
+     * Subsequent reads can be found by following the steps defined by
+     * `AssignableRead.getANextRead()`.
+     */
+    AssignableRead getAFirstReadAtNode(ControlFlow::Node cfn) {
+      firstReadSameVar(this, cfn) and
+      result.getAControlFlowNode() = cfn
     }
 
     /**
@@ -2106,8 +2145,39 @@ module Ssa {
      * - The read of `this.Field` on line 11 is a last read of the phi node
      *   between lines 9 and 10.
      */
-    AssignableRead getALastRead() {
-      lastRead(this, result)
+    AssignableRead getALastRead() { result = this.getALastReadAtNode(_) }
+
+    /**
+     * Gets a last read of the source variable underlying this SSA definition at
+     * control flow node `cfn`. That is, a read that can reach the end of the
+     * enclosing callable, or another SSA definition for the source variable,
+     * without passing through any other read. Example:
+     *
+     * ```
+     * int Field;
+     *
+     * void SetField(int i) {
+     *   this.Field = i;
+     *   Use(this.Field);
+     *   if (i > 0)
+     *     this.Field = i - 1;
+     *   else if (i < 0)
+     *     SetField(1);
+     *   Use(this.Field);
+     *   Use(this.Field);
+     * }
+     * ```
+     *
+     * - The reads of `i` on lines 7 and 8 are the last reads for the implicit
+     *   parameter definition on line 3.
+     * - The read of `this.Field` on line 5 is a last read of the definition on
+     *   line 4.
+     * - The read of `this.Field` on line 11 is a last read of the phi node
+     *   between lines 9 and 10.
+     */
+    AssignableRead getALastReadAtNode(ControlFlow::Node cfn) {
+      lastRead(this, cfn) and
+      result.getAControlFlowNode() = cfn
     }
 
     /**

csharp/ql/test/library-tests/dataflow/ssa/DefAdjacentRead.expected

@@ -136,7 +136,6 @@
 | Properties.cs:75:23:75:23 | b | Properties.cs:75:23:75:35 | Action b = ... | Properties.cs:80:9:80:9 | access to local variable b |
 | Properties.cs:106:37:106:37 | p | Properties.cs:106:37:106:37 | p | Properties.cs:106:42:106:42 | access to parameter p |
 | Splitting.cs:3:18:3:18 | b | Splitting.cs:3:18:3:18 | b | Splitting.cs:6:13:6:13 | access to parameter b |
-| Splitting.cs:5:13:5:13 | x | Splitting.cs:7:13:7:19 | ... = ... | Splitting.cs:13:9:13:9 | access to local variable x |
 | Splitting.cs:5:13:5:13 | x | Splitting.cs:10:13:10:19 | ... = ... | Splitting.cs:11:13:11:13 | access to local variable x |
 | Splitting.cs:22:18:22:18 | b | Splitting.cs:22:18:22:18 | b | Splitting.cs:25:13:25:13 | access to parameter b |
 | Splitting.cs:24:13:24:13 | x | Splitting.cs:29:13:29:19 | ... = ... | Splitting.cs:30:13:30:13 | access to local variable x |

csharp/ql/test/library-tests/dataflow/ssa/PreSsaConsistency.expected

@@ -1,11 +1,3 @@
 defReadInconsistency
-| Splitting.cs:13:9:13:9 | access to local variable x | Splitting.cs:7:13:7:19 | ... = ... | Splitting.cs:5:13:5:13 | x | false |
 readReadInconsistency
-| Splitting.cs:11:13:11:13 | access to local variable x | Splitting.cs:13:9:13:9 | access to local variable x | Splitting.cs:5:13:5:13 | x | false |
 phiInconsistency
-| Splitting.cs:13:9:13:21 | ...; | Splitting.cs:7:13:7:19 | ... = ... | Splitting.cs:5:13:5:13 | x | true |
-| Splitting.cs:13:9:13:21 | ...; | Splitting.cs:10:13:10:19 | ... = ... | Splitting.cs:5:13:5:13 | x | true |
-| Splitting.cs:52:9:53:22 | if (...) ... | Splitting.cs:46:13:46:19 | ... = ... | Splitting.cs:44:13:44:13 | x | true |
-| Splitting.cs:52:9:53:22 | if (...) ... | Splitting.cs:49:13:49:19 | ... = ... | Splitting.cs:44:13:44:13 | x | true |
-| Splitting.cs:54:9:54:21 | ...; | Splitting.cs:46:13:46:19 | ... = ... | Splitting.cs:44:13:44:13 | x | false |
-| Splitting.cs:54:9:54:21 | ...; | Splitting.cs:49:13:49:19 | ... = ... | Splitting.cs:44:13:44:13 | x | false |

csharp/ql/test/library-tests/dataflow/ssa/PreSsaConsistency.ql

@@ -1,9 +1,19 @@
 import csharp
 import ControlFlow::Internal
 
-query predicate defReadInconsistency(
+class CallableWithSplitting extends Callable {
+  CallableWithSplitting() {
+    this = any(SplitControlFlowElement e).getEnclosingCallable()
+  }
+}
+
+query
+predicate defReadInconsistency(
   AssignableRead ar, Expr e, PreSsa::SimpleAssignable a, boolean b
 ) {
+  // Exclude definitions in callables with CFG splitting, as SSA definitions may be
+  // very different from pre-SSA definitions
+  not ar.getEnclosingCallable() instanceof CallableWithSplitting and
   exists(AssignableDefinition def | e = def.getExpr() |
     b = true and
     exists(PreSsa::Definition ssaDef | ssaDef.getAssignable() = a |
@@ -31,21 +41,33 @@ query predicate defReadInconsistency(
 query predicate readReadInconsistency(
   LocalScopeVariableRead read1, LocalScopeVariableRead read2, PreSsa::SimpleAssignable a, boolean b
 ) {
-  b = true and
-  a = read1.getTarget() and
-  PreSsa::adjacentReadPairSameVar(read1, read2) and
-  not Ssa::Internal::adjacentReadPairSameVar(read1, read2)
-  or
-  b = false and
-  a = read1.getTarget() and
-  Ssa::Internal::adjacentReadPairSameVar(read1, read2) and
-  read1.getTarget() instanceof PreSsa::SimpleAssignable and
-  not PreSsa::adjacentReadPairSameVar(read1, read2)
+  // Exclude definitions in callables with CFG splitting, as SSA definitions may be
+  // very different from pre-SSA definitions
+  not read1.getEnclosingCallable() instanceof CallableWithSplitting and
+  (
+    b = true and
+    a = read1.getTarget() and
+    PreSsa::adjacentReadPairSameVar(read1, read2) and
+    not Ssa::Internal::adjacentReadPairSameVar(read1.getAControlFlowNode(), read2.getAControlFlowNode())
+    or
+    b = false and
+    a = read1.getTarget() and
+    Ssa::Internal::adjacentReadPairSameVar(read1.getAControlFlowNode(), read2.getAControlFlowNode()) and
+    read1.getTarget() instanceof PreSsa::SimpleAssignable and
+    not PreSsa::adjacentReadPairSameVar(read1, read2) and
+    // Exclude split CFG elements because SSA may be more precise than pre-SSA
+    // in those cases
+    not read1 instanceof SplitControlFlowElement and
+    not read2 instanceof SplitControlFlowElement
+  )
 }
 
 query predicate phiInconsistency(
   ControlFlowElement cfe, Expr e, PreSsa::SimpleAssignable a, boolean b
 ) {
+  // Exclude definitions in callables with CFG splitting, as SSA definitions may be
+  // very different from pre-SSA definitions
+  not cfe.getEnclosingCallable() instanceof CallableWithSplitting and
   exists(AssignableDefinition adef | e = adef.getExpr() |
     b = true and
     exists(PreSsa::Definition def | a = def.getAssignable() |

csharp/ql/test/library-tests/dataflow/ssa/ReadAdjacentRead.expected

@@ -99,7 +99,6 @@
 | Properties.cs:104:16:104:20 | Props | Properties.cs:115:21:115:30 | access to field Props | Properties.cs:116:17:116:26 | access to field Props |
 | Properties.cs:104:16:104:20 | Props | Properties.cs:115:21:115:36 | access to field Props | Properties.cs:116:17:116:32 | access to field Props |
 | Splitting.cs:3:18:3:18 | b | Splitting.cs:6:13:6:13 | access to parameter b | Splitting.cs:15:13:15:13 | access to parameter b |
-| Splitting.cs:5:13:5:13 | x | Splitting.cs:11:13:11:13 | access to local variable x | Splitting.cs:13:9:13:9 | access to local variable x |
 | Splitting.cs:5:13:5:13 | x | Splitting.cs:13:9:13:9 | access to local variable x | Splitting.cs:14:9:14:9 | access to local variable x |
 | Splitting.cs:5:13:5:13 | x | Splitting.cs:14:9:14:9 | access to local variable x | Splitting.cs:17:13:17:13 | access to local variable x |
 | Splitting.cs:22:18:22:18 | b | Splitting.cs:25:13:25:13 | access to parameter b | Splitting.cs:35:13:35:13 | access to parameter b |

csharp/ql/test/library-tests/dataflow/ssa/SsaDefLastRead.expected

@@ -217,13 +217,11 @@
 | Properties.cs:114:20:114:35 | this.Props.Props | Properties.cs:113:9:113:22 | SSA call def(this.Props.Props) | Properties.cs:116:17:116:32 | access to field Props |
 | Properties.cs:115:21:115:39 | this.Props.Props.xs | Properties.cs:113:9:113:22 | SSA qualifier def(this.Props.Props.xs) | Properties.cs:116:17:116:35 | access to property xs |
 | Splitting.cs:3:18:3:18 | b | Splitting.cs:3:18:3:18 | SSA param(b) | Splitting.cs:15:13:15:13 | access to parameter b |
-| Splitting.cs:5:13:5:13 | x | Splitting.cs:7:13:7:19 | [b (line 3): true] SSA def(x) | Splitting.cs:14:9:14:9 | access to local variable x |
 | Splitting.cs:5:13:5:13 | x | Splitting.cs:7:13:7:19 | [b (line 3): true] SSA def(x) | Splitting.cs:17:13:17:13 | access to local variable x |
 | Splitting.cs:5:13:5:13 | x | Splitting.cs:10:13:10:19 | [b (line 3): false] SSA def(x) | Splitting.cs:14:9:14:9 | access to local variable x |
 | Splitting.cs:22:18:22:18 | b | Splitting.cs:22:18:22:18 | SSA param(b) | Splitting.cs:35:13:35:13 | access to parameter b |
 | Splitting.cs:24:13:24:13 | x | Splitting.cs:29:13:29:19 | [b (line 22): false] SSA def(x) | Splitting.cs:30:13:30:13 | access to local variable x |
 | Splitting.cs:24:13:24:13 | x | Splitting.cs:32:9:32:15 | [b (line 22): false] SSA def(x) | Splitting.cs:34:9:34:9 | access to local variable x |
-| Splitting.cs:24:13:24:13 | x | Splitting.cs:32:9:32:15 | [b (line 22): true] SSA def(x) | Splitting.cs:34:9:34:9 | access to local variable x |
 | Splitting.cs:24:13:24:13 | x | Splitting.cs:32:9:32:15 | [b (line 22): true] SSA def(x) | Splitting.cs:37:13:37:13 | access to local variable x |
 | Splitting.cs:42:18:42:18 | b | Splitting.cs:42:18:42:18 | SSA param(b) | Splitting.cs:52:13:52:13 | access to parameter b |
 | Splitting.cs:44:13:44:13 | x | Splitting.cs:49:13:49:19 | [b (line 42): false] SSA def(x) | Splitting.cs:50:13:50:13 | access to local variable x |