C#: Replace BreakNormalCompletion with a nested completion

Author: hvitved

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

@@ -36,23 +36,28 @@ private newtype TCompletion =
   TEmptinessCompletion(boolean isEmpty) { isEmpty = true or isEmpty = false } or
   TReturnCompletion() or
   TBreakCompletion() or
-  TBreakNormalCompletion() or
   TContinueCompletion() or
   TGotoCompletion(string label) { label = any(GotoStmt gs).getLabel() } or
   TThrowCompletion(ExceptionClass ec) or
   TExitCompletion() or
-  TNestedCompletion(ConditionalCompletion inner, Completion outer) {
-    outer = TReturnCompletion()
-    or
-    outer = TBreakCompletion()
-    or
-    outer = TContinueCompletion()
-    or
-    outer = TGotoCompletion(_)
-    or
-    outer = TThrowCompletion(_)
+  TNestedCompletion(Completion inner, Completion outer) {
+    inner instanceof NormalCompletion and
+    (
+      outer = TReturnCompletion()
+      or
+      outer = TBreakCompletion()
+      or
+      outer = TContinueCompletion()
+      or
+      outer = TGotoCompletion(_)
+      or
+      outer = TThrowCompletion(_)
+      or
+      outer = TExitCompletion()
+    )
     or
-    outer = TExitCompletion()
+    inner = TBreakCompletion() and
+    outer instanceof NonNestedNormalCompletion
   }
 
 pragma[noinline]
@@ -534,8 +539,10 @@ private predicate mustHaveEmptinessCompletion(ControlFlowElement cfe) { foreachE
  */
 abstract class NormalCompletion extends Completion { }
 
+abstract private class NonNestedNormalCompletion extends NormalCompletion { }
+
 /** A simple (normal) completion. */
-class SimpleCompletion extends NormalCompletion, TSimpleCompletion {
+class SimpleCompletion extends NonNestedNormalCompletion, TSimpleCompletion {
   override NormalSuccessor getAMatchingSuccessorType() { any() }
 
   override string toString() { result = "normal" }
@@ -547,7 +554,7 @@ class SimpleCompletion extends NormalCompletion, TSimpleCompletion {
  * completion (`NullnessCompletion`), a matching completion (`MatchingCompletion`),
  * or an emptiness completion (`EmptinessCompletion`).
  */
-abstract class ConditionalCompletion extends NormalCompletion { }
+abstract class ConditionalCompletion extends NonNestedNormalCompletion { }
 
 /**
  * A completion that represents evaluation of an expression
@@ -635,39 +642,6 @@ class EmptinessCompletion extends ConditionalCompletion, TEmptinessCompletion {
   override string toString() { if this.isEmpty() then result = "empty" else result = "non-empty" }
 }
 
-/**
- * A completion that represents evaluation of a statement or
- * expression resulting in a loop break.
- *
- * 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 `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.
- *
- * Example:
- *
- * ```csharp
- * while (...) {
- *    ...
- *    break;
- * }
- * return;
- * ```
- *
- * 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
- * `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)" }
-}
-
 /**
  * A nested completion. For example, in
  *
@@ -691,12 +665,17 @@ class BreakNormalCompletion extends NormalCompletion, TBreakNormalCompletion {
  * and an inner `false` completion. `b2` also has a (normal) `true` completion.
  */
 class NestedCompletion extends Completion, TNestedCompletion {
-  private ConditionalCompletion inner;
-  private Completion outer;
+  Completion inner;
+  Completion outer;
 
   NestedCompletion() { this = TNestedCompletion(inner, outer) }
 
-  override ConditionalCompletion getInnerCompletion() { result = inner }
+  /** Gets a completion that is compatible with the inner completion. */
+  Completion getAnInnerCompatibleCompletion() {
+    result.getOuterCompletion() = this.getInnerCompletion()
+  }
+
+  override Completion getInnerCompletion() { result = inner }
 
   override Completion getOuterCompletion() { result = outer }
 
@@ -705,6 +684,57 @@ class NestedCompletion extends Completion, TNestedCompletion {
   override string toString() { result = outer + " [" + inner + "]" }
 }
 
+/**
+ * A nested completion for a loop that exists with a `break`.
+ *
+ * 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 `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.
+ *
+ * Example:
+ *
+ * ```csharp
+ * while (...) {
+ *    ...
+ *    break;
+ * }
+ * return;
+ * ```
+ *
+ * The `break` on line 3 completes with a `TBreakCompletion`, therefore
+ * the `while` loop can complete with a `NestedBreakCompletion`, so we
+ * get an edge `break --break--> return`. (If we instead used a
+ * `TSimpleCompletion`, we would get a less precise edge
+ * `break --normal--> return`.)
+ */
+class NestedBreakCompletion extends NormalCompletion, NestedCompletion {
+  NestedBreakCompletion() {
+    inner = TBreakCompletion() and
+    outer instanceof NonNestedNormalCompletion
+  }
+
+  override BreakCompletion getInnerCompletion() { result = inner }
+
+  override SimpleCompletion getOuterCompletion() { result = outer }
+
+  override Completion getAnInnerCompatibleCompletion() {
+    result = inner and
+    outer = TSimpleCompletion()
+    or
+    result = TNestedCompletion(outer, inner)
+  }
+
+  override SuccessorType getAMatchingSuccessorType() {
+    outer instanceof SimpleCompletion and
+    result instanceof BreakSuccessor
+    or
+    result = outer.(ConditionalCompletion).getAMatchingSuccessorType()
+  }
+}
+
 /**
  * A completion that represents evaluation of a statement or an
  * expression resulting in a return from a callable.

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

@@ -1040,8 +1040,7 @@ module Statements {
       c instanceof NormalCompletion
       or
       // A statement exits with a `break` completion
-      last(this.getStmt(_), last, any(BreakCompletion bc)) and
-      c instanceof BreakNormalCompletion
+      last(this.getStmt(_), last, c.(NestedBreakCompletion).getAnInnerCompatibleCompletion())
       or
       // A statement exits abnormally
       last(this.getStmt(_), last, c) and
@@ -1123,12 +1122,8 @@ module Statements {
       last(this.getCondition(), last, c) and
       c instanceof FalseCompletion
       or
-      // Body exits with a break completion; the loop exits normally
-      // Note: we use a `BreakNormalCompletion` rather than a `NormalCompletion`
-      // in order to be able to get the correct break label in the control flow
-      // graph from the `result` node to the node after the loop.
-      last(body, last, any(BreakCompletion bc)) and
-      c instanceof BreakNormalCompletion
+      // Body exits with a break completion
+      last(body, last, c.(NestedBreakCompletion).getAnInnerCompatibleCompletion())
       or
       // Body exits with a completion that does not continue the loop
       last(body, last, c) and
@@ -1252,12 +1247,8 @@ module Statements {
       last = this and
       c.(EmptinessCompletion).isEmpty()
       or
-      // Body exits with a break completion; the loop exits normally
-      // Note: we use a `BreakNormalCompletion` rather than a `NormalCompletion`
-      // in order to be able to get the correct break label in the control flow
-      // graph from the `result` node to the node after the loop.
-      last(this.getBody(), last, any(BreakCompletion bc)) and
-      c instanceof BreakNormalCompletion
+      // Body exits with a break completion
+      last(this.getBody(), last, c.(NestedBreakCompletion).getAnInnerCompatibleCompletion())
       or
       // Body exits abnormally
       last(this.getBody(), last, c) and
@@ -1375,15 +1366,10 @@ module Statements {
       or
       // If the `finally` block completes normally, it inherits any non-normal
       // completion that was current before the `finally` block was entered
-      exists(NormalCompletion finally, Completion outer | this.lastFinally(last, finally, outer) |
-        c =
-          any(NestedCompletion nc |
-            nc.getInnerCompletion() = finally and nc.getOuterCompletion() = outer
-          )
-        or
-        not finally instanceof ConditionalCompletion and
-        c = outer
-      )
+      c =
+        any(NestedCompletion nc |
+          this.lastFinally(last, nc.getAnInnerCompatibleCompletion(), nc.getOuterCompletion())
+        )
     }
 
     /**

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

@@ -860,8 +860,7 @@ module FinallySplitting {
       (
         exit(pred, c, _)
         or
-        exit(pred, any(BreakCompletion bc), _) and
-        c instanceof BreakNormalCompletion
+        exit(pred, c.(NestedBreakCompletion).getAnInnerCompatibleCompletion(), _)
       )
     }
 
@@ -870,8 +869,7 @@ module FinallySplitting {
       (
         exit(last, c, _)
         or
-        exit(last, any(BreakCompletion bc), _) and
-        c instanceof BreakNormalCompletion
+        exit(last, c.(NestedBreakCompletion).getAnInnerCompatibleCompletion(), _)
       )
     }
 

csharp/ql/test/library-tests/controlflow/graph/Condition.expected

@@ -1307,6 +1307,7 @@ conditionFlow
 | BreakInTry.cs:31:21:31:32 | ... == ... | BreakInTry.cs:22:9:34:9 | foreach (... ... in ...) ... | false |
 | BreakInTry.cs:31:21:31:32 | ... == ... | BreakInTry.cs:32:21:32:21 | ; | true |
 | BreakInTry.cs:31:21:31:32 | [finally: break] ... == ... | BreakInTry.cs:32:21:32:21 | [finally: break] ; | true |
+| BreakInTry.cs:31:21:31:32 | [finally: break] ... == ... | BreakInTry.cs:35:7:35:7 | ; | false |
 | BreakInTry.cs:42:17:42:28 | ... == ... | BreakInTry.cs:43:17:43:23 | return ...; | true |
 | BreakInTry.cs:42:17:42:28 | ... == ... | BreakInTry.cs:46:9:52:9 | {...} | false |
 | BreakInTry.cs:49:21:49:31 | ... == ... | BreakInTry.cs:47:13:51:13 | foreach (... ... in ...) ... | false |