C#: Teach null-guards library about pattern matching

change-notes/1.19/analysis-csharp.md

@@ -1,20 +1,20 @@
-# Improvements to C# analysis
-
-## General improvements
-
-* The control flow graph construction now takes simple Boolean conditions on local scope variables into account. For example, in `if (b) x = 0; if (b) x = 1;`, the control flow graph will reflect that taking the `true` (resp. `false`) branch in the first condition implies taking the same branch in the second condition. In effect, the first assignment to `x` will now be identified as being dead.
-
-## New queries
-
-| **Query**                   | **Tags**  | **Purpose**                                                        |
-|-----------------------------|-----------|--------------------------------------------------------------------|
-| *@name of query (Query ID)* | *Tags*    |*Aim of the new query and whether it is enabled by default or not*  |
-
-## Changes to existing queries
-
-| **Query**                  | **Expected impact**    | **Change**                                                       |
-|----------------------------|------------------------|------------------------------------------------------------------|
-| *@name of query (Query ID)*| *Impact on results*    | *How/why the query has changed*                                  |
-
-
-## Changes to QL libraries
+# Improvements to C# analysis
+
+## General improvements
+
+* The control flow graph construction now takes simple Boolean conditions on local scope variables into account. For example, in `if (b) x = 0; if (b) x = 1;`, the control flow graph will reflect that taking the `true` (resp. `false`) branch in the first condition implies taking the same branch in the second condition. In effect, the first assignment to `x` will now be identified as being dead.
+
+## New queries
+
+| **Query**                   | **Tags**  | **Purpose**                                                        |
+|-----------------------------|-----------|--------------------------------------------------------------------|
+| *@name of query (Query ID)* | *Tags*    |*Aim of the new query and whether it is enabled by default or not*  |
+
+## Changes to existing queries
+
+| **Query**                  | **Expected impact**    | **Change**                                                       |
+|----------------------------|------------------------|------------------------------------------------------------------|
+| *@name of query (Query ID)*| *Impact on results*    | *How/why the query has changed*                                  |
+
+
+## Changes to QL libraries

csharp/ql/src/Bad Practices/Control-Flow/ConstantCondition.ql

@@ -79,7 +79,7 @@ class ConstantNullnessCondition extends ConstantCondition {
       cfn = this.getAControlFlowNode() |
       exists(ControlFlow::SuccessorTypes::NullnessSuccessor t |
         exists(cfn.getASuccessorByType(t)) |
-        if t.isNull() then b = true else b = false
+        b = t.getValue()
       ) and
       strictcount(ControlFlow::SuccessorType t | exists(cfn.getASuccessorByType(t))) = 1
     )
@@ -102,7 +102,7 @@ class ConstantMatchingCondition extends ConstantCondition {
       cfn = this.getAControlFlowNode() |
       exists(ControlFlow::SuccessorTypes::MatchingSuccessor t |
         exists(cfn.getASuccessorByType(t)) |
-        if t.isMatch() then b = true else b = false
+        b = t.getValue()
       ) and
       strictcount(ControlFlow::SuccessorType t | exists(cfn.getASuccessorByType(t))) = 1
     )

csharp/ql/src/semmle/code/csharp/commons/StructuralComparison.qll

@@ -85,6 +85,7 @@ abstract class StructuralComparisonConfiguration extends string {
     value = x.getValue()
   }
 
+  pragma [nomagic]
   private predicate sameByStructure(Element x, Element y) {
     // At least one of `x` and `y` must not have a value, they must have
     // the same kind, and the same number of children
@@ -121,6 +122,7 @@ abstract class StructuralComparisonConfiguration extends string {
     not (x.(Expr).hasValue() and y.(Expr).hasValue())
   }
 
+  pragma [nomagic]
   private predicate sameInternal(Element x, Element y) {
     sameByValue(x, y)
     or
@@ -210,6 +212,7 @@ module Internal {
       value = x.getValue()
     }
 
+    pragma [nomagic]
     private predicate sameByStructure(Element x, Element y) {
       // At least one of `x` and `y` must not have a value, they must have
       // the same kind, and the same number of children
@@ -246,6 +249,7 @@ module Internal {
       not (x.(Expr).hasValue() and y.(Expr).hasValue())
     }
 
+    pragma [nomagic]
     private predicate sameInternal(Element x, Element y) {
       sameByValue(x, y)
       or

csharp/ql/src/semmle/code/csharp/controlflow/BasicBlocks.qll

@@ -3,6 +3,7 @@
  */
 
 import csharp
+private import ControlFlow::SuccessorTypes
 
 /**
  * A basic block, that is, a maximal straight-line sequence of control flow nodes
@@ -14,6 +15,11 @@ class BasicBlock extends TBasicBlockStart {
     result.getFirstNode() = getLastNode().getASuccessor()
   }
 
+  /** Gets an immediate successor of this basic block of a given flow type, if any. */
+  BasicBlock getASuccessorByType(ControlFlow::SuccessorType t) {
+    result.getFirstNode() = this.getLastNode().getASuccessorByType(t)
+  }
+
   /** Gets an immediate predecessor of this basic block, if any. */
   BasicBlock getAPredecessor() {
     result.getASuccessor() = this
@@ -75,6 +81,7 @@ class BasicBlock extends TBasicBlockStart {
    * The node on line 2 is an immediate `null` successor of the node
    * `x` on line 1.
    */
+  deprecated
   BasicBlock getANullSuccessor() {
     result.getFirstNode() = getLastNode().getANullSuccessor()
   }
@@ -94,6 +101,7 @@ class BasicBlock extends TBasicBlockStart {
    * The node `x?.M()`, representing the call to `M`, is a non-`null` successor
    * of the node `x`.
    */
+  deprecated
   BasicBlock getANonNullSuccessor() {
     result.getFirstNode() = getLastNode().getANonNullSuccessor()
   }
@@ -430,7 +438,7 @@ class ConditionBlock extends BasicBlock {
    * the callable entry point by going via the true edge (`testIsTrue = true`)
    * or false edge (`testIsTrue = false`) out of this basic block.
    */
-  predicate controls(BasicBlock controlled, boolean testIsTrue) {
+  predicate controls(BasicBlock controlled, ConditionalSuccessor s) {
     /*
      * For this block to control the block `controlled` with `testIsTrue` the following must be true:
      * Execution must have passed through the test i.e. `this` must strictly dominate `controlled`.
@@ -465,7 +473,7 @@ class ConditionBlock extends BasicBlock {
      * directly.
      */
     exists(BasicBlock succ |
-      isCandidateSuccessor(succ, testIsTrue) |
+      isCandidateSuccessor(succ, s) |
       succ.dominates(controlled)
     )
   }
@@ -476,11 +484,9 @@ class ConditionBlock extends BasicBlock {
    * the callable entry point by going via the `null` edge (`isNull = true`)
    * or non-`null` edge (`isNull = false`) out of this basic block.
    */
+  deprecated
   predicate controlsNullness(BasicBlock controlled, boolean isNull) {
-    exists(BasicBlock succ |
-      isCandidateSuccessorNullness(succ, isNull) |
-      succ.dominates(controlled)
-    )
+    this.controls(controlled, any(NullnessSuccessor s | s.getValue() = isNull))
   }
 
   /**
@@ -520,29 +526,11 @@ class ConditionBlock extends BasicBlock {
   // only `x & y` controls `A` if we do not take sub conditions into account.
   predicate controlsSubCond(BasicBlock controlled, boolean testIsTrue, Expr cond, boolean condIsTrue) {
     impliesSub(getLastNode().getElement(), cond, testIsTrue, condIsTrue) and
-    controls(controlled, testIsTrue)
+    controls(controlled, any(BooleanSuccessor s | s.getValue() = testIsTrue))
   }
 
-  private predicate isCandidateSuccessor(BasicBlock succ, boolean testIsTrue) {
-    (
-      testIsTrue = true and succ = this.getATrueSuccessor()
-      or
-      testIsTrue = false and succ = this.getAFalseSuccessor()
-    )
-    and
-    forall(BasicBlock pred |
-      pred = succ.getAPredecessor() and pred != this |
-      succ.dominates(pred)
-    )
-  }
-
-  private predicate isCandidateSuccessorNullness(BasicBlock succ, boolean isNull) {
-    (
-      isNull = true and succ = this.getANullSuccessor()
-      or
-      isNull = false and succ = this.getANonNullSuccessor()
-    )
-    and
+  private predicate isCandidateSuccessor(BasicBlock succ, ConditionalSuccessor s) {
+    succ = this.getASuccessorByType(s) and
     forall(BasicBlock pred |
       pred = succ.getAPredecessor() and pred != this |
       succ.dominates(pred)

csharp/ql/src/semmle/code/csharp/controlflow/Completion.qll

@@ -401,10 +401,21 @@ private predicate inNullnessContext(Expr e, boolean isNullnessCompletionForParen
   )
 }
 
+/**
+ * Holds if `cfe` is the element inside case statement `cs`, belonging to `switch`
+ * statement `ss`, that has the matching completion.
+ */
+predicate switchMatching(SwitchStmt ss, CaseStmt cs, ControlFlowElement cfe) {
+  ss.getACase() = cs and
+  (
+    cfe = cs.(ConstCase).getExpr()
+    or
+    cfe = cs.(TypeCase).getTypeAccess() // use type access to represent the type test
+  )
+}
+
 private predicate mustHaveMatchingCompletion(SwitchStmt ss, ControlFlowElement cfe) {
-  cfe = ss.getAConstCase().getExpr()
-  or
-  cfe = ss.getATypeCase().getTypeAccess() // use type access to represent the type test
+  switchMatching(ss, _, cfe)
 }
 
 /**

csharp/ql/src/semmle/code/csharp/controlflow/ControlFlowGraph.qll

@@ -255,6 +255,7 @@ module ControlFlow {
      * The node on line 2 is an immediate `null` successor of the node
      * `x` on line 1.
      */
+    deprecated
     Node getANullSuccessor() {
       result = getASuccessorByType(any(NullnessSuccessor t | t.isNull()))
     }
@@ -274,6 +275,7 @@ module ControlFlow {
      * The node `x?.M()`, representing the call to `M`, is a non-`null` successor
      * of the node `x`.
      */
+    deprecated
     Node getANonNullSuccessor() {
       result = getASuccessorByType(any(NullnessSuccessor t | not t.isNull()))
     }
@@ -400,7 +402,10 @@ module ControlFlow {
      * a nullness successor (`NullnessSuccessor`), a matching successor (`MatchingSuccessor`),
      * or an emptiness successor (`EmptinessSuccessor`).
      */
-    abstract class ConditionalSuccessor extends SuccessorType { }
+    abstract class ConditionalSuccessor extends SuccessorType {
+      /** Gets the Boolean value of this successor. */
+      abstract boolean getValue();
+    }
 
     /**
      * A Boolean control flow successor.
@@ -429,8 +434,7 @@ module ControlFlow {
      * ```
      */
     class BooleanSuccessor extends ConditionalSuccessor, TBooleanSuccessor {
-      /** Gets the value of this Boolean successor. */
-      boolean getValue() { this = TBooleanSuccessor(result) }
+      override boolean getValue() { this = TBooleanSuccessor(result) }
 
       override string toString() { result = getValue().toString() }
 
@@ -469,6 +473,8 @@ module ControlFlow {
       /** Holds if this is a `null` successor. */
       predicate isNull() { this = TNullnessSuccessor(true) }
 
+      override boolean getValue() { this = TNullnessSuccessor(result) }
+
       override string toString() {
         if this.isNull() then
           result = "null"
@@ -520,6 +526,8 @@ module ControlFlow {
       /** Holds if this is a match successor. */
       predicate isMatch() { this = TMatchingSuccessor(true) }
 
+      override boolean getValue() { this = TMatchingSuccessor(result) }
+
       override string toString() {
         if this.isMatch() then
           result = "match"
@@ -571,6 +579,8 @@ module ControlFlow {
       /** Holds if this is an empty successor. */
       predicate isEmpty() { this = TEmptinessSuccessor(true) }
 
+      override boolean getValue() { this = TEmptinessSuccessor(result) }
+
       override string toString() {
         if this.isEmpty() then
           result = "empty"