C#: Replace matchesCompletion() with getAMatchingSuccessorType()

Author: hvitved

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

@@ -110,7 +110,7 @@ module AbstractValues {
 
     override predicate branch(ControlFlowElement cfe, ConditionalSuccessor s, Expr e) {
       s.(BooleanSuccessor).getValue() = this.getValue() and
-      exists(BooleanCompletion c | s.matchesCompletion(c) |
+      exists(BooleanCompletion c | s = c.getAMatchingSuccessorType() |
         c.isValidFor(cfe) and
         e = cfe
       )
@@ -161,7 +161,7 @@ module AbstractValues {
 
     override predicate branch(ControlFlowElement cfe, ConditionalSuccessor s, Expr e) {
       this = TNullValue(s.(NullnessSuccessor).getValue()) and
-      exists(NullnessCompletion c | s.matchesCompletion(c) |
+      exists(NullnessCompletion c | s = c.getAMatchingSuccessorType() |
         c.isValidFor(cfe) and
         e = cfe
       )
@@ -190,7 +190,7 @@ module AbstractValues {
 
     override predicate branch(ControlFlowElement cfe, ConditionalSuccessor s, Expr e) {
       this = TMatchValue(_, s.(MatchingSuccessor).getValue()) and
-      exists(MatchingCompletion c, Switch switch, Case case | s.matchesCompletion(c) |
+      exists(MatchingCompletion c, Switch switch, Case case | s = c.getAMatchingSuccessorType() |
         c.isValidFor(cfe) and
         switchMatching(switch, case, cfe) and
         e = switch.getExpr() and
@@ -227,7 +227,7 @@ module AbstractValues {
 
     override predicate branch(ControlFlowElement cfe, ConditionalSuccessor s, Expr e) {
       this = TEmptyCollectionValue(s.(EmptinessSuccessor).getValue()) and
-      exists(EmptinessCompletion c, ForeachStmt fs | s.matchesCompletion(c) |
+      exists(EmptinessCompletion c, ForeachStmt fs | s = c.getAMatchingSuccessorType() |
         c.isValidFor(cfe) and
         foreachEmptiness(fs, cfe) and
         e = fs.getIterableExpr()

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

@@ -24,10 +24,12 @@ private import semmle.code.csharp.commons.Assertions
 private import semmle.code.csharp.commons.Constants
 private import semmle.code.csharp.frameworks.System
 private import NonReturning
+private import SuccessorType
+private import SuccessorTypes
 
 // Internal representation of completions
 private newtype TCompletion =
-  TNormalCompletion() or
+  TSimpleCompletion() or
   TBooleanCompletion(boolean b) { b = true or b = false } or
   TNullnessCompletion(boolean isNull) { isNull = true or isNull = false } or
   TMatchingCompletion(boolean isMatch) { isMatch = true or isMatch = false } or
@@ -78,7 +80,7 @@ private predicate completionIsValidForStmt(Stmt s, Completion c) {
 /**
  * A completion of a statement or an expression.
  */
-class Completion extends TCompletion {
+abstract class Completion extends TCompletion {
   /**
    * Holds if this completion is valid for control flow element `cfe`.
    *
@@ -143,7 +145,7 @@ class Completion extends TCompletion {
     not mustHaveNullnessCompletion(cfe) and
     not mustHaveMatchingCompletion(cfe) and
     not mustHaveEmptinessCompletion(cfe) and
-    this = TNormalCompletion()
+    this = TSimpleCompletion()
   }
 
   /**
@@ -167,8 +169,11 @@ class Completion extends TCompletion {
    */
   Completion getOuterCompletion() { result = this }
 
+  /** Gets a successor type that matches this completion. */
+  abstract SuccessorType getAMatchingSuccessorType();
+
   /** Gets a textual representation of this completion. */
-  string toString() { none() }
+  abstract string toString();
 }
 
 /** Holds if expression `e` has the Boolean constant value `value`. */
@@ -529,10 +534,10 @@ private predicate mustHaveEmptinessCompletion(ControlFlowElement cfe) { foreachE
  */
 abstract class NormalCompletion extends Completion { }
 
-/**
- * A class to make `TNormalCompletion` a `NormalCompletion`
- */
-class SimpleCompletion extends NormalCompletion, TNormalCompletion {
+/** A simple (normal) completion. */
+class SimpleCompletion extends NormalCompletion, TSimpleCompletion {
+  override NormalSuccessor getAMatchingSuccessorType() { any() }
+
   override string toString() { result = "normal" }
 }
 
@@ -558,6 +563,8 @@ class BooleanCompletion extends ConditionalCompletion {
 
   BooleanCompletion getDual() { result = TBooleanCompletion(value.booleanNot()) }
 
+  override BooleanSuccessor getAMatchingSuccessorType() { result.getValue() = value }
+
   override string toString() { result = value.toString() }
 }
 
@@ -576,11 +583,17 @@ class FalseCompletion extends BooleanCompletion {
  * `null` or non-`null`.
  */
 class NullnessCompletion extends ConditionalCompletion, TNullnessCompletion {
+  private boolean value;
+
+  NullnessCompletion() { this = TNullnessCompletion(value) }
+
   /** Holds if the last sub expression of this expression evaluates to `null`. */
-  predicate isNull() { this = TNullnessCompletion(true) }
+  predicate isNull() { value = true }
 
   /** Holds if the last sub expression of this expression evaluates to a non-`null` value. */
-  predicate isNonNull() { this = TNullnessCompletion(false) }
+  predicate isNonNull() { value = false }
+
+  override NullnessSuccessor getAMatchingSuccessorType() { result.getValue() = value }
 
   override string toString() { if this.isNull() then result = "null" else result = "non-null" }
 }
@@ -590,11 +603,17 @@ class NullnessCompletion extends ConditionalCompletion, TNullnessCompletion {
  * `switch` statement.
  */
 class MatchingCompletion extends ConditionalCompletion, TMatchingCompletion {
+  private boolean value;
+
+  MatchingCompletion() { this = TMatchingCompletion(value) }
+
   /** Holds if there is a match. */
-  predicate isMatch() { this = TMatchingCompletion(true) }
+  predicate isMatch() { value = true }
 
   /** Holds if there is not a match. */
-  predicate isNonMatch() { this = TMatchingCompletion(false) }
+  predicate isNonMatch() { value = false }
+
+  override MatchingSuccessor getAMatchingSuccessorType() { result.getValue() = value }
 
   override string toString() { if this.isMatch() then result = "match" else result = "no-match" }
 }
@@ -604,8 +623,14 @@ class MatchingCompletion extends ConditionalCompletion, TMatchingCompletion {
  * a test in a `foreach` statement.
  */
 class EmptinessCompletion extends ConditionalCompletion, TEmptinessCompletion {
+  private boolean value;
+
+  EmptinessCompletion() { this = TEmptinessCompletion(value) }
+
   /** Holds if the emptiness test evaluates to `true`. */
-  predicate isEmpty() { this = TEmptinessCompletion(true) }
+  predicate isEmpty() { value = true }
+
+  override EmptinessSuccessor getAMatchingSuccessorType() { result.getValue() = value }
 
   override string toString() { if this.isEmpty() then result = "empty" else result = "non-empty" }
 }
@@ -616,7 +641,7 @@ class EmptinessCompletion extends ConditionalCompletion, TEmptinessCompletion {
  *
  * This completion is added for technical reasons only: when a loop
  * body can complete with a break completion, the loop itself completes
- * normally. However, if we choose `TNormalCompletion` as the completion
+ * normally. However, if we choose `TSimpleCompletion` as the completion
  * of the loop, we lose the information that the last element actually
  * completed with a break, meaning that the control flow edge out of the
  * breaking node cannot be marked with a `break` label.
@@ -634,10 +659,12 @@ class EmptinessCompletion extends ConditionalCompletion, TEmptinessCompletion {
  * The `break` on line 3 completes with a `TBreakCompletion`, therefore
  * the `while` loop can complete with a `TBreakNormalCompletion`, so we
  * get an edge `break --break--> return`. (If we instead used a
- * `TNormalCompletion`, we would get a less precise edge
+ * `TSimpleCompletion`, we would get a less precise edge
  * `break --normal--> return`.)
  */
 class BreakNormalCompletion extends NormalCompletion, TBreakNormalCompletion {
+  override BreakSuccessor getAMatchingSuccessorType() { any() }
+
   override string toString() { result = "normal (break)" }
 }
 
@@ -673,6 +700,8 @@ class NestedCompletion extends Completion, TNestedCompletion {
 
   override Completion getOuterCompletion() { result = outer }
 
+  override SuccessorType getAMatchingSuccessorType() { none() }
+
   override string toString() { result = outer + " [" + inner + "]" }
 }
 
@@ -686,6 +715,8 @@ class ReturnCompletion extends Completion {
     this = TNestedCompletion(_, TReturnCompletion())
   }
 
+  override ReturnSuccessor getAMatchingSuccessorType() { any() }
+
   override string toString() {
     // `NestedCompletion` defines `toString()` for the other case
     this = TReturnCompletion() and result = "return"
@@ -703,6 +734,8 @@ class BreakCompletion extends Completion {
     this = TNestedCompletion(_, TBreakCompletion())
   }
 
+  override BreakSuccessor getAMatchingSuccessorType() { any() }
+
   override string toString() {
     // `NestedCompletion` defines `toString()` for the other case
     this = TBreakCompletion() and result = "break"
@@ -720,6 +753,8 @@ class ContinueCompletion extends Completion {
     this = TNestedCompletion(_, TContinueCompletion())
   }
 
+  override ContinueSuccessor getAMatchingSuccessorType() { any() }
+
   override string toString() {
     // `NestedCompletion` defines `toString()` for the other case
     this = TContinueCompletion() and result = "continue"
@@ -741,6 +776,8 @@ class GotoCompletion extends Completion {
   /** Gets the label of the `goto` completion. */
   string getLabel() { result = label }
 
+  override GotoSuccessor getAMatchingSuccessorType() { result.getLabel() = label }
+
   override string toString() {
     // `NestedCompletion` defines `toString()` for the other case
     this = TGotoCompletion(label) and result = "goto(" + label + ")"
@@ -762,6 +799,8 @@ class ThrowCompletion extends Completion {
   /** Gets the type of the exception being thrown. */
   ExceptionClass getExceptionClass() { result = ec }
 
+  override ExceptionSuccessor getAMatchingSuccessorType() { result.getExceptionClass() = ec }
+
   override string toString() {
     // `NestedCompletion` defines `toString()` for the other case
     this = TThrowCompletion(ec) and result = "throw(" + ec + ")"
@@ -783,6 +822,8 @@ class ExitCompletion extends Completion {
     this = TNestedCompletion(_, TExitCompletion())
   }
 
+  override ExitSuccessor getAMatchingSuccessorType() { any() }
+
   override string toString() {
     // `NestedCompletion` defines `toString()` for the other case
     this = TExitCompletion() and result = "exit"

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

@@ -1619,7 +1619,7 @@ private module Cached {
         result = TElementNode(succElement, succSplits)
       |
         succSplits(predElement, predSplits, succElement, succSplits, c) and
-        t.matchesCompletion(c)
+        t = c.getAMatchingSuccessorType()
       )
     )
     or

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

@@ -54,7 +54,7 @@ class PreBasicBlock extends ControlFlowElement {
   PreBasicBlock() { startsBB(this) }
 
   PreBasicBlock getASuccessorByType(SuccessorType t) {
-    succ(this.getLastElement(), result, any(Completion c | t.matchesCompletion(c)))
+    succ(this.getLastElement(), result, any(Completion c | t = c.getAMatchingSuccessorType()))
   }
 
   PreBasicBlock getASuccessor() { result = this.getASuccessorByType(_) }
@@ -127,7 +127,7 @@ class ConditionBlock extends PreBasicBlock {
   predicate controls(PreBasicBlock controlled, SuccessorTypes::ConditionalSuccessor s) {
     exists(PreBasicBlock succ, ConditionalCompletion c | immediatelyControls(succ, c) |
       succ.dominates(controlled) and
-      s.matchesCompletion(c)
+      s = c.getAMatchingSuccessorType()
     )
   }
 }

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

@@ -635,7 +635,7 @@ module FinallySplitting {
         // If the entry into the `finally` block completes with any normal completion,
         // it simply means normal execution after the `finally` block
         this instanceof NormalSuccessor
-      else this.matchesCompletion(c)
+      else this = c.getAMatchingSuccessorType()
     }
   }
 
@@ -806,7 +806,7 @@ module FinallySplitting {
           // does not require another completion to be recovered
           inherited = false and
           (
-            type.matchesCompletion(c)
+            type = c.getAMatchingSuccessorType()
             or
             not c instanceof NormalCompletion
             or
@@ -816,7 +816,7 @@ module FinallySplitting {
           // Finally block can exit with completion `c` inherited from try/catch
           // block: must match this split
           inherited = true and
-          type.matchesCompletion(c) and
+          type = c.getAMatchingSuccessorType() and
           not type instanceof NormalSuccessor
         )
       )
@@ -1587,7 +1587,7 @@ predicate succEntrySplits(
 predicate succExitSplits(ControlFlowElement pred, Splits predSplits, Callable succ, SuccessorType t) {
   exists(Reachability::SameSplitsBlock b, Completion c | pred = b.getAnElement() |
     b.isReachable(predSplits) and
-    t.matchesCompletion(c) and
+    t = c.getAMatchingSuccessorType() and
     succExit(pred, succ, c) and
     forall(SplitImpl predSplit | predSplit = predSplits.getASplit() |
       predSplit.hasExitScope(pred, succ, c)