Merge pull request github#4724 from hvitved/csharp/cfg/not-pattern

C#: Implement CFG for `not` patterns

Author: hvitved

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

@@ -232,36 +232,57 @@ private Expr getQualifier(QualifiableExpr e) {
   result = e.getChildExpr(-1)
 }
 
+pragma[noinline]
+private predicate typePatternMustHaveMatchingCompletion(
+  TypePatternExpr tpe, Type t, Type strippedType
+) {
+  exists(Expr e, Expr stripped | mustHaveMatchingCompletion(e, tpe) |
+    stripped = e.stripCasts() and
+    t = tpe.getCheckedType() and
+    strippedType = stripped.getType() and
+    not t.containsTypeParameters() and
+    not strippedType.containsTypeParameters()
+  )
+}
+
+pragma[noinline]
+private Type typePatternCommonSubTypeLeft(Type t) {
+  typePatternMustHaveMatchingCompletion(_, t, _) and
+  result.isImplicitlyConvertibleTo(t) and
+  not result instanceof DynamicType
+}
+
+pragma[noinline]
+private Type typePatternCommonSubTypeRight(Type strippedType) {
+  typePatternMustHaveMatchingCompletion(_, _, strippedType) and
+  result.isImplicitlyConvertibleTo(strippedType) and
+  not result instanceof DynamicType
+}
+
+pragma[noinline]
+private predicate typePatternCommonSubType(Type t, Type strippedType) {
+  typePatternCommonSubTypeLeft(t) = typePatternCommonSubTypeRight(strippedType)
+}
+
 /**
- * Holds if expression `e` constantly matches (`value = true`) or constantly
- * non-matches (`value = false`).
+ * Holds if pattern expression `pe` constantly matches (`value = true`) or
+ * constantly non-matches (`value = false`).
  */
-private predicate isMatchingConstant(Expr e, boolean value) {
-  exists(Switch s | mustHaveMatchingCompletion(s, e) |
-    exists(Expr stripped | stripped = s.getExpr().stripCasts() |
-      exists(Case c, string strippedValue |
-        c = s.getACase() and
-        e = c.getPattern() and
-        strippedValue = stripped.getValue()
-      |
-        if strippedValue = e.getValue() then value = true else value = false
-      )
-      or
-      exists(Case c, TypePatternExpr tpe, Type t, Type strippedType | c = s.getACase() |
-        tpe = c.getPattern() and
-        e = tpe and
-        t = tpe.getCheckedType() and
-        strippedType = stripped.getType() and
-        not t.isImplicitlyConvertibleTo(strippedType) and
-        not t instanceof Interface and
-        not t.containsTypeParameters() and
-        not strippedType.containsTypeParameters() and
-        value = false
-      )
-    )
-    or
-    e instanceof DiscardPatternExpr and
-    value = true
+private predicate isMatchingConstant(PatternExpr pe, boolean value) {
+  exists(Expr e, string exprValue, string patternValue |
+    mustHaveMatchingCompletion(e, pe) and
+    exprValue = e.stripCasts().getValue() and
+    patternValue = pe.getValue() and
+    if exprValue = patternValue then value = true else value = false
+  )
+  or
+  pe instanceof DiscardPatternExpr and
+  value = true
+  or
+  exists(Type t, Type strippedType |
+    typePatternMustHaveMatchingCompletion(pe, t, strippedType) and
+    not typePatternCommonSubType(t, strippedType) and
+    value = false
   )
 }
 
@@ -518,7 +539,20 @@ predicate switchMatching(Switch s, Case c, PatternExpr pe) {
   pe = c.getPattern()
 }
 
-private predicate mustHaveMatchingCompletion(Switch s, PatternExpr pe) { switchMatching(s, _, pe) }
+/**
+ * Holds if `pe` must have a matching completion, and `e` is the expression
+ * that is being matched.
+ */
+private predicate mustHaveMatchingCompletion(Expr e, PatternExpr pe) {
+  exists(Switch s |
+    switchMatching(s, _, pe) and
+    e = s.getExpr()
+  )
+  or
+  pe = any(IsExpr ie | inBooleanContext(ie) and e = ie.getExpr()).getPattern()
+  or
+  pe = any(UnaryPatternExpr upe | mustHaveMatchingCompletion(e, upe)).getPattern()
+}
 
 /**
  * Holds if a normal completion of `cfe` must be a matching completion. Thats is,
@@ -565,7 +599,13 @@ class SimpleCompletion extends NonNestedNormalCompletion, TSimpleCompletion {
  * completion (`NullnessCompletion`), a matching completion (`MatchingCompletion`),
  * or an emptiness completion (`EmptinessCompletion`).
  */
-abstract class ConditionalCompletion extends NonNestedNormalCompletion { }
+abstract class ConditionalCompletion extends NonNestedNormalCompletion {
+  /** Gets the Boolean value of this completion. */
+  abstract boolean getValue();
+
+  /** Gets the dual completion. */
+  abstract ConditionalCompletion getDual();
+}
 
 /**
  * A completion that represents evaluation of an expression
@@ -576,10 +616,9 @@ class BooleanCompletion extends ConditionalCompletion {
 
   BooleanCompletion() { this = TBooleanCompletion(value) }
 
-  /** Gets the Boolean value of this completion. */
-  boolean getValue() { result = value }
+  override boolean getValue() { result = value }
 
-  BooleanCompletion getDual() { result = TBooleanCompletion(value.booleanNot()) }
+  override BooleanCompletion getDual() { result = TBooleanCompletion(value.booleanNot()) }
 
   override BooleanSuccessor getAMatchingSuccessorType() { result.getValue() = value }
 
@@ -611,6 +650,10 @@ class NullnessCompletion extends ConditionalCompletion, TNullnessCompletion {
   /** Holds if the last sub expression of this expression evaluates to a non-`null` value. */
   predicate isNonNull() { value = false }
 
+  override boolean getValue() { result = value }
+
+  override NullnessCompletion getDual() { result = TNullnessCompletion(value.booleanNot()) }
+
   override NullnessSuccessor getAMatchingSuccessorType() { result.getValue() = value }
 
   override string toString() { if this.isNull() then result = "null" else result = "non-null" }
@@ -631,6 +674,10 @@ class MatchingCompletion extends ConditionalCompletion, TMatchingCompletion {
   /** Holds if there is not a match. */
   predicate isNonMatch() { value = false }
 
+  override boolean getValue() { result = value }
+
+  override MatchingCompletion getDual() { result = TMatchingCompletion(value.booleanNot()) }
+
   override MatchingSuccessor getAMatchingSuccessorType() { result.getValue() = value }
 
   override string toString() { if this.isMatch() then result = "match" else result = "no-match" }
@@ -648,6 +695,10 @@ class EmptinessCompletion extends ConditionalCompletion, TEmptinessCompletion {
   /** Holds if the emptiness test evaluates to `true`. */
   predicate isEmpty() { value = true }
 
+  override boolean getValue() { result = value }
+
+  override EmptinessCompletion getDual() { result = TEmptinessCompletion(value.booleanNot()) }
+
   override EmptinessSuccessor getAMatchingSuccessorType() { result.getValue() = value }
 
   override string toString() { if this.isEmpty() then result = "empty" else result = "non-empty" }