C#: Fix a bug and generalize guards implication logic

Author: hvitved

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

@@ -956,27 +956,27 @@ module Internal {
    */
   private predicate guardImpliesNotEqual(Expr guard, AbstractValue vGuard, PreSsa::Definition def, AbstractValue vDef) {
     relevantEq(def, vDef) and
-    exists(DereferenceableExpr de |
-      de = def.getARead() |
+    exists(AssignableRead ar |
+      ar = def.getARead() |
       // For example:
       //   if (de == null); vGuard = TBooleanValue(false); vDef = TNullValue(true)
       // but not
       //   if (de == "abc"); vGuard = TBooleanValue(false); vDef = TNullValue(false)
-      guard = getAnEqualityCheckVal(de, vGuard.getDualValue(), vDef) and
+      guard = getAnEqualityCheckVal(ar, vGuard.getDualValue(), vDef) and
       vDef.isSingleton()
       or
       // For example:
       //   if (de != null); vGuard = TBooleanValue(true); vDef = TNullValue(true)
       // or
       //   if (de == null); vGuard = TBooleanValue(true); vDef = TNullValue(false)
       exists(NullValue nv |
-        guard = de.getANullCheck(vGuard, any(boolean b | nv = TNullValue(b))) |
+        guard = ar.(DereferenceableExpr).getANullCheck(vGuard, any(boolean b | nv = TNullValue(b))) |
         vDef = nv.getDualValue()
       )
       or
       // For example:
-      //   if (de == null); vGuard = TBooleanValue(true); vDef = TNullValue(false)
-      guard = getAnEqualityCheckVal(de, vGuard, vDef.getDualValue())
+      //   if (de == false); vGuard = TBooleanValue(true); vDef = TBooleanValue(true)
+      guard = getAnEqualityCheckVal(ar, vGuard, vDef.getDualValue())
     )
   }
 
@@ -1040,7 +1040,7 @@ module Internal {
    * Holds if `e` has abstract value `v` and may be assigned to `def` without going
    * through back edges, and all other possible ultimate definitions of `def` do not
    * have abstract value `v`. The trivial case where `def` is an explicit update with
-   * source `e is excluded.
+   * source `e` is excluded.
    */
   private predicate uniqueValue(PreSsa::Definition def, Expr e, AbstractValue v) {
     possibleValue(def, false, e, v) and
@@ -1178,30 +1178,41 @@ module Internal {
         polarity = false
       )
       or
-      exists(ConditionalExpr cond, boolean branch, BoolLiteral boolLit, boolean b |
-        b = boolLit.getBoolValue() and
+      exists(ConditionalExpr cond, boolean branch, Expr e, AbstractValue v |
+        e = v.getAnExpr() and
         (
-          cond.getThen() = boolLit and branch = true
+          cond.getThen() = e and branch = true
           or
-          cond.getElse() = boolLit and branch = false
+          cond.getElse() = e and branch = false
         )
       |
         g1 = cond and
-        v1 = TBooleanValue(b.booleanNot()) and
+        v1 = v.getDualValue() and
         (
+          // g1 === g2 ? e : ...; 
           g2 = cond.getCondition() and
           v2 = TBooleanValue(branch.booleanNot())
           or
+          // g1 === ... ? g2 : e
           g2 = cond.getThen() and
           branch = false and
           v2 = v1
           or
+          // g1 === g2 ? ... : e
           g2 = cond.getElse() and
           branch = true and
           v2 = v1
         )
       )
       or
+      v1 = g1.getAValue() and
+      v1 = any(MatchValue mv |
+        mv.isMatch() and
+        g2 = g1 and
+        v2.getAnExpr() = mv.getCaseStmt().(ConstCase).getExpr() and
+        v1 != v2
+      )
+      or
       exists(boolean isNull |
         g1 = g2.(DereferenceableExpr).getANullCheck(v1, isNull) |
         v2 = any(NullValue nv | if nv.isNull() then isNull = true else isNull = false) and
@@ -1238,15 +1249,16 @@ module Internal {
       )
       or
       exists(PreSsa::Definition def, AbstractValue v |
-        // If `def = g2 ? v : ...` or `def = g2 ? ... : v` then a guard `g1`
-        // proving `def != v` ensures that `g2` evaluates to `b2`.
+        // If for example `def = g2 ? v : ...`, then a guard `g1` proving `def != v`
+        // ensures that `g2` evaluates to `false`.
         conditionalAssignVal(g2, v2.getDualValue(), def, v) and
         guardImpliesNotEqual(g1, v1, def, v)
       )
       or
       exists(PreSsa::Definition def, Expr e, AbstractValue v |
-        // If `def = g2 ? v : ...` and all other assignments to `def` are different from
-        // `v` then a guard proving `def == v` ensures that `g2` evaluates to `v2`.
+        // If for example `def = g2 ? v : ...` and all other assignments to `def` are
+        // different from `v`, then a guard proving `def == v` ensures that `g2`
+        // evaluates to `true`.
         uniqueValue(def, e, v) and
         guardImpliesEqual(g1, v1, def, v) and
         g2.preControlsDirect(any(PreBasicBlocks::PreBasicBlock bb | e = bb.getAnElement()), v2) and

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

@@ -190,7 +190,8 @@ private predicate defMaybeNull(Ssa::Definition def, string msg, Element reason)
 
 /**
  * Holds if `def1` being `null` in basic block `bb1` implies that `def2` might
- * be null in basic block `bb2`. The SSA definitions share the same source variable.
+ * be `null` in basic block `bb2`. The SSA definitions share the same source
+ * variable.
  */
 private predicate defNullImpliesStep(Ssa::Definition def1, BasicBlock bb1, Ssa::Definition def2, BasicBlock bb2) {
   exists(Ssa::SourceVariable v |
@@ -374,10 +375,6 @@ class Dereference extends G::DereferenceableExpr {
     defReaches(v.getAnSsaDefinition(), this, true)
   }
 
-  /**
-   * Holds if assignable access `aa` is the first dereference of an assignable
-   * in a block, where it is suspected of being `null`.
-   */
   pragma[noinline]
   private predicate nullDerefCandidate(Ssa::Definition origin) {
     exists(Ssa::Definition ssa, BasicBlock bb |

csharp/ql/test/library-tests/controlflow/guards/Guards.cs

@@ -209,4 +209,57 @@ void M17(object o, string[] args)
             }
         }
     }
+
+    void M18(bool b1)
+    {
+        var b2 = true;
+        if (b1)
+            b2 = false;
+        switch (b2)
+        {
+            case true :
+                return;
+            return;
+        }
+    }
+
+    void M19(bool b1)
+    {
+        var b2 = false;
+        if (b1)
+            b2 = true;
+        switch (b2)
+        {
+            case true :
+                return;
+            return;
+        }
+    }
+
+    void M20(bool b)
+    {
+        var i = 0;
+        if (b)
+            i = 1;
+        switch (i)
+        {
+            case 1 :
+                return;
+            return;
+        }
+    }
+
+    enum E { A, B, C }
+    void M21(bool b)
+    {
+        var e = E.A;
+        if (b)
+            e = E.B;
+        switch (e)
+        {
+            case E.B :
+                return;
+            return;
+        }
+    }
 }