From 8a35813e1c816071aec83c979269c3fea40d3555 Mon Sep 17 00:00:00 2001
From: Tom Hvitved <tom@semmle.com>
Date: Wed, 3 Jul 2019 10:52:43 +0200
Subject: [PATCH 1/3] C#: Unify `goto` completions

---
 csharp/ql/src/semmle/code/csharp/Stmt.qll     | 13 ++-
 .../csharp/controlflow/ControlFlowGraph.qll   | 34 +++----
 .../controlflow/internal/Completion.qll       | 98 ++++---------------
 .../controlflow/internal/SuccessorType.qll    | 67 ++-----------
 .../controlflow/graph/BasicBlock.expected     |  3 +-
 .../graph/BasicBlockDominance.expected        | 37 ++++++-
 .../controlflow/graph/ConditionBlock.expected | 15 +--
 .../controlflow/graph/Dominance.expected      |  5 +-
 .../controlflow/graph/ElementGraph.expected   | 10 +-
 .../controlflow/graph/ExitElement.expected    | 14 +--
 .../controlflow/graph/NodeGraph.expected      | 10 +-
 .../ql/test/library-tests/goto/Goto1.expected |  8 +-
 12 files changed, 111 insertions(+), 203 deletions(-)

diff --git a/csharp/ql/src/semmle/code/csharp/Stmt.qll b/csharp/ql/src/semmle/code/csharp/Stmt.qll
index 8b10088530e7..dc8587a5bb83 100644
--- a/csharp/ql/src/semmle/code/csharp/Stmt.qll
+++ b/csharp/ql/src/semmle/code/csharp/Stmt.qll
@@ -669,7 +669,10 @@ class ContinueStmt extends JumpStmt, @continue_stmt {
  * Either a `goto` label (`GotoLabelStmt`), a `goto case` (`GotoCaseStmt`), or
  * a `goto default` (`GotoDefaultStmt`).
  */
-class GotoStmt extends JumpStmt, @goto_any_stmt { }
+class GotoStmt extends JumpStmt, @goto_any_stmt {
+  /** Gets the label that this `goto` statement jumps to. */
+  string getLabel() { none() }
+}
 
 /**
  * A `goto` statement that jumps to a labeled statement, for example line 4 in
@@ -684,8 +687,7 @@ class GotoStmt extends JumpStmt, @goto_any_stmt { }
  * ```
  */
 class GotoLabelStmt extends GotoStmt, @goto_stmt {
-  /** Gets the label that this `goto` statement jumps to. */
-  string getLabel() { exprorstmt_name(this, result) }
+  override string getLabel() { exprorstmt_name(this, result) }
 
   override string toString() { result = "goto ...;" }
 
@@ -716,8 +718,7 @@ class GotoCaseStmt extends GotoStmt, @goto_case_stmt {
   /** Gets the constant expression that this `goto case` statement jumps to. */
   Expr getExpr() { result = this.getChild(0) }
 
-  /** Gets the label that this `goto case` statement jumps to. */
-  string getLabel() { result = getExpr().getValue() }
+  override string getLabel() { result = getExpr().getValue() }
 
   override string toString() { result = "goto case ...;" }
 }
@@ -740,6 +741,8 @@ class GotoCaseStmt extends GotoStmt, @goto_case_stmt {
  */
 class GotoDefaultStmt extends GotoStmt, @goto_default_stmt {
   override string toString() { result = "goto default;" }
+
+  override string getLabel() { result = "default" }
 }
 
 /**
diff --git a/csharp/ql/src/semmle/code/csharp/controlflow/ControlFlowGraph.qll b/csharp/ql/src/semmle/code/csharp/controlflow/ControlFlowGraph.qll
index 0146e44c4c2c..6b9e37a14d46 100644
--- a/csharp/ql/src/semmle/code/csharp/controlflow/ControlFlowGraph.qll
+++ b/csharp/ql/src/semmle/code/csharp/controlflow/ControlFlowGraph.qll
@@ -1087,6 +1087,12 @@ module ControlFlow {
           )
       }
 
+      pragma[noinline]
+      private LabeledStmt getLabledStmt(string label, Callable c) {
+        result.getEnclosingCallable() = c and
+        label = result.getLabel()
+      }
+
       /**
        * Gets a potential last element executed within control flow element `cfe`,
        * as well as its completion.
@@ -1148,8 +1154,8 @@ module ControlFlow {
           rec = TLastRecSwitchAbnormalCompletion() and
           not c instanceof BreakCompletion and
           not c instanceof NormalCompletion and
-          not c instanceof GotoDefaultCompletion and
-          not c instanceof GotoCaseCompletion and
+          not getLabledStmt(c.(GotoCompletion).getLabel(), cfe.getEnclosingCallable()) instanceof
+            CaseStmt and
           c = c0
           or
           rec = TLastRecInvalidOperationException() and
@@ -1515,24 +1521,6 @@ module ControlFlow {
             c instanceof NormalCompletion and
             result = first(ss.getStmt(i + 1))
           )
-          or
-          exists(GotoCompletion gc |
-            cfe = last(ss.getAStmt(), gc) and
-            gc = c
-          |
-            // Flow from last element of a statement with a `goto default` completion
-            // to first element `default` statement
-            gc instanceof GotoDefaultCompletion and
-            result = first(ss.getDefaultCase())
-            or
-            // Flow from last element of a statement with a `goto case` completion
-            // to first element of relevant case
-            exists(ConstCase cc |
-              cc = ss.getAConstCase() and
-              cc.getLabel() = gc.(GotoCaseCompletion).getLabel() and
-              result = first(cc.getBody())
-            )
-          )
         )
         or
         exists(Case case |
@@ -1766,13 +1754,13 @@ module ControlFlow {
         or
         // Flow from element with `goto` completion to first element of relevant
         // target
-        c = any(GotoLabelCompletion glc |
-            cfe = last(_, glc) and
+        c = any(GotoCompletion gc |
+            cfe = last(_, gc) and
             // Special case: when a `goto` happens inside a `try` statement with a
             // `finally` block, flow does not go directly to the target, but instead
             // to the `finally` block (and from there possibly to the target)
             not cfe = getBlockOrCatchFinallyPred(any(TryStmt ts | ts.hasFinally()), _) and
-            result = first(glc.getGotoStmt().getTarget())
+            result = first(getLabledStmt(gc.getLabel(), cfe.getEnclosingCallable()))
           )
         or
         // Standard left-to-right evaluation
diff --git a/csharp/ql/src/semmle/code/csharp/controlflow/internal/Completion.qll b/csharp/ql/src/semmle/code/csharp/controlflow/internal/Completion.qll
index 178ccf8bab5f..440d611bf341 100644
--- a/csharp/ql/src/semmle/code/csharp/controlflow/internal/Completion.qll
+++ b/csharp/ql/src/semmle/code/csharp/controlflow/internal/Completion.qll
@@ -35,9 +35,7 @@ private newtype TCompletion =
   TBreakCompletion() or
   TBreakNormalCompletion() or
   TContinueCompletion() or
-  TGotoLabelCompletion(GotoLabelStmt goto) or
-  TGotoCaseCompletion(GotoCaseStmt goto) or
-  TGotoDefaultCompletion() or
+  TGotoCompletion(string label) { label = any(GotoStmt gs).getLabel() } or
   TThrowCompletion(ExceptionClass ec) or
   TExitCompletion() or
   TNestedCompletion(NormalCompletion inner, Completion outer) {
@@ -47,11 +45,7 @@ private newtype TCompletion =
     or
     outer = TContinueCompletion()
     or
-    outer = TGotoLabelCompletion(_)
-    or
-    outer = TGotoCaseCompletion(_)
-    or
-    outer = TGotoDefaultCompletion()
+    outer = TGotoCompletion(_)
     or
     outer = TThrowCompletion(_)
     or
@@ -122,22 +116,17 @@ class Completion extends TCompletion {
                   if cfe instanceof ContinueStmt
                   then this = TContinueCompletion()
                   else
-                    if cfe instanceof GotoDefaultStmt
-                    then this = TGotoDefaultCompletion()
+                    if cfe instanceof GotoStmt
+                    then this = TGotoCompletion(cfe.(GotoStmt).getLabel())
                     else
-                      if cfe instanceof GotoStmt
-                      then
-                        this = TGotoLabelCompletion(cfe) or
-                        this = TGotoCaseCompletion(cfe)
+                      if cfe instanceof ReturnStmt
+                      then this = TReturnCompletion()
                       else
-                        if cfe instanceof ReturnStmt
-                        then this = TReturnCompletion()
-                        else
-                          if cfe instanceof YieldBreakStmt
-                          then
-                            // `yield break` behaves like a return statement
-                            this = TReturnCompletion()
-                          else this = TNormalCompletion()
+                        if cfe instanceof YieldBreakStmt
+                        then
+                          // `yield break` behaves like a return statement
+                          this = TReturnCompletion()
+                        else this = TNormalCompletion()
     )
   }
 
@@ -726,69 +715,20 @@ class ContinueCompletion extends Completion {
  * A completion that represents evaluation of a statement or an
  * expression resulting in a `goto` jump.
  */
-abstract class GotoCompletion extends Completion { }
-
-/**
- * A completion that represents evaluation of a statement or an
- * expression resulting in a `goto label` jump.
- */
-class GotoLabelCompletion extends GotoCompletion {
-  private GotoLabelStmt goto;
-
-  GotoLabelCompletion() {
-    this = TGotoLabelCompletion(goto) or
-    this = TNestedCompletion(_, TGotoLabelCompletion(goto))
-  }
-
-  /** Gets the target of the `goto label` completion. */
-  string getLabel() { result = this.getGotoStmt().getLabel() }
-
-  /** Gets the statement that resulted in this `goto label` completion. */
-  GotoLabelStmt getGotoStmt() { result = goto }
-
-  override string toString() {
-    // `NestedCompletion` defines `toString()` for the other case
-    this = TGotoLabelCompletion(goto) and result = "goto(" + this.getLabel() + ")"
-  }
-}
-
-/**
- * A completion that represents evaluation of a statement or an
- * expression resulting in a `goto case` jump.
- */
-class GotoCaseCompletion extends GotoCompletion {
-  private GotoCaseStmt goto;
+class GotoCompletion extends Completion {
+  private string label;
 
-  GotoCaseCompletion() {
-    this = TGotoCaseCompletion(goto) or
-    this = TNestedCompletion(_, TGotoCaseCompletion(goto))
+  GotoCompletion() {
+    this = TGotoCompletion(label) or
+    this = TNestedCompletion(_, TGotoCompletion(label))
   }
 
-  /** Gets the target of the `goto case` completion. */
-  string getLabel() { result = this.getGotoStmt().getLabel() }
-
-  /** Gets the statement that resulted in this `goto case` completion. */
-  GotoCaseStmt getGotoStmt() { result = goto }
-
-  override string toString() {
-    // `NestedCompletion` defines `toString()` for the other case
-    this = TGotoCaseCompletion(goto) and result = "goto case(" + this.getLabel() + ")"
-  }
-}
-
-/**
- * A completion that represents evaluation of a statement or an
- * expression resulting in a `goto default` jump.
- */
-class GotoDefaultCompletion extends GotoCompletion {
-  GotoDefaultCompletion() {
-    this = TGotoDefaultCompletion() or
-    this = TNestedCompletion(_, TGotoDefaultCompletion())
-  }
+  /** Gets the label of the `goto` completion. */
+  string getLabel() { result = label }
 
   override string toString() {
     // `NestedCompletion` defines `toString()` for the other case
-    this = TGotoDefaultCompletion() and result = "goto default"
+    this = TGotoCompletion(label) and result = "goto(" + label + ")"
   }
 }
 
diff --git a/csharp/ql/src/semmle/code/csharp/controlflow/internal/SuccessorType.qll b/csharp/ql/src/semmle/code/csharp/controlflow/internal/SuccessorType.qll
index 653b0bb8f168..3f265236fb41 100644
--- a/csharp/ql/src/semmle/code/csharp/controlflow/internal/SuccessorType.qll
+++ b/csharp/ql/src/semmle/code/csharp/controlflow/internal/SuccessorType.qll
@@ -18,9 +18,7 @@ private newtype TSuccessorType =
   TReturnSuccessor() or
   TBreakSuccessor() or
   TContinueSuccessor() or
-  TGotoLabelSuccessor(GotoLabelStmt goto) or
-  TGotoCaseSuccessor(GotoCaseStmt goto) or
-  TGotoDefaultSuccessor() or
+  TGotoSuccessor(string label) { label = any(GotoStmt gs).getLabel() } or
   TExceptionSuccessor(ExceptionClass ec) { exists(ThrowCompletion c | c.getExceptionClass() = ec) } or
   TExitSuccessor()
 
@@ -300,7 +298,7 @@ module SuccessorTypes {
   }
 
   /**
-   * A `goto label` control flow successor.
+   * A `goto` control flow successor.
    *
    * Example:
    *
@@ -319,68 +317,17 @@ module SuccessorTypes {
    * The node `Return: return x` is a `goto label` successor of the node
    * `goto Return;`.
    */
-  class GotoLabelSuccessor extends SuccessorType, TGotoLabelSuccessor {
-    /** Gets the statement that resulted in this `goto` successor. */
-    GotoLabelStmt getGotoStmt() { this = TGotoLabelSuccessor(result) }
+  class GotoSuccessor extends SuccessorType, TGotoSuccessor {
+    /** Gets the `goto` label. */
+    string getLabel() { this = TGotoSuccessor(result) }
 
-    override string toString() { result = "goto(" + getGotoStmt().getLabel() + ")" }
+    override string toString() { result = "goto(" + this.getLabel() + ")" }
 
     override predicate matchesCompletion(Completion c) {
-      c.(GotoLabelCompletion).getGotoStmt() = getGotoStmt()
+      c.(GotoCompletion).getLabel() = this.getLabel()
     }
   }
 
-  /**
-   * A `goto case` control flow successor.
-   *
-   * Example:
-   *
-   * ```
-   * switch (x)
-   * {
-   *     case 0  : return 1;
-   *     case 1  : goto case 0;
-   *     default : return -1;
-   * }
-   * ```
-   *
-   * The node `case 0  : return 1;` is a  `goto case` successor of the node
-   * `goto case 0;`.
-   */
-  class GotoCaseSuccessor extends SuccessorType, TGotoCaseSuccessor {
-    /** Gets the statement that resulted in this `goto case` successor. */
-    GotoCaseStmt getGotoStmt() { this = TGotoCaseSuccessor(result) }
-
-    override string toString() { result = "goto(" + getGotoStmt().getLabel() + ")" }
-
-    override predicate matchesCompletion(Completion c) {
-      c.(GotoCaseCompletion).getGotoStmt() = getGotoStmt()
-    }
-  }
-
-  /**
-   * A `goto default` control flow successor.
-   *
-   * Example:
-   *
-   * ```
-   * switch (x)
-   * {
-   *     case 0  : return 1;
-   *     case 1  : goto default;
-   *     default : return -1;
-   * }
-   * ```
-   *
-   * The node `default : return -1;` is a `goto default` successor of the node
-   * `goto default;`.
-   */
-  class GotoDefaultSuccessor extends SuccessorType, TGotoDefaultSuccessor {
-    override string toString() { result = "goto default" }
-
-    override predicate matchesCompletion(Completion c) { c instanceof GotoDefaultCompletion }
-  }
-
   /**
    * An exceptional control flow successor.
    *
diff --git a/csharp/ql/test/library-tests/controlflow/graph/BasicBlock.expected b/csharp/ql/test/library-tests/controlflow/graph/BasicBlock.expected
index a36d265f0ba8..adc3efdf92dd 100644
--- a/csharp/ql/test/library-tests/controlflow/graph/BasicBlock.expected
+++ b/csharp/ql/test/library-tests/controlflow/graph/BasicBlock.expected
@@ -425,8 +425,9 @@
 | cflow.cs:30:18:33:37 | if (...) ... | cflow.cs:30:22:30:31 | ... == ... | 6 |
 | cflow.cs:31:17:31:42 | ...; | cflow.cs:31:17:31:41 | call to method WriteLine | 3 |
 | cflow.cs:33:17:33:37 | ...; | cflow.cs:33:17:33:36 | call to method WriteLine | 3 |
-| cflow.cs:37:17:37:22 | enter Switch | cflow.cs:41:18:41:18 | 1 | 6 |
+| cflow.cs:37:17:37:22 | enter Switch | cflow.cs:39:17:39:17 | access to parameter a | 4 |
 | cflow.cs:37:17:37:22 | exit Switch | cflow.cs:37:17:37:22 | exit Switch | 1 |
+| cflow.cs:41:13:41:19 | case ...: | cflow.cs:41:18:41:18 | 1 | 2 |
 | cflow.cs:42:17:42:39 | ...; | cflow.cs:43:17:43:28 | goto case ...; | 5 |
 | cflow.cs:44:13:44:19 | case ...: | cflow.cs:44:18:44:18 | 2 | 2 |
 | cflow.cs:45:17:45:39 | ...; | cflow.cs:46:17:46:28 | goto case ...; | 5 |
diff --git a/csharp/ql/test/library-tests/controlflow/graph/BasicBlockDominance.expected b/csharp/ql/test/library-tests/controlflow/graph/BasicBlockDominance.expected
index 048c993bfbd4..6af4b8078636 100644
--- a/csharp/ql/test/library-tests/controlflow/graph/BasicBlockDominance.expected
+++ b/csharp/ql/test/library-tests/controlflow/graph/BasicBlockDominance.expected
@@ -679,8 +679,8 @@
 | post | Switch.cs:10:10:10:11 | exit M2 | Switch.cs:30:13:30:20 | default: |
 | post | Switch.cs:15:17:15:23 | return ...; | Switch.cs:15:17:15:23 | return ...; |
 | post | Switch.cs:16:13:16:19 | case ...: | Switch.cs:16:13:16:19 | case ...: |
+| post | Switch.cs:16:13:16:19 | case ...: | Switch.cs:23:27:23:27 | 0 |
 | post | Switch.cs:17:23:17:37 | object creation of type Exception | Switch.cs:17:23:17:37 | object creation of type Exception |
-| post | Switch.cs:17:23:17:37 | object creation of type Exception | Switch.cs:23:27:23:27 | 0 |
 | post | Switch.cs:18:13:18:22 | case ...: | Switch.cs:18:13:18:22 | case ...: |
 | post | Switch.cs:19:17:19:29 | goto default; | Switch.cs:19:17:19:29 | goto default; |
 | post | Switch.cs:20:13:20:23 | case ...: | Switch.cs:20:13:20:23 | case ...: |
@@ -891,7 +891,10 @@
 | post | cflow.cs:37:17:37:22 | enter Switch | cflow.cs:37:17:37:22 | enter Switch |
 | post | cflow.cs:37:17:37:22 | exit Switch | cflow.cs:37:17:37:22 | enter Switch |
 | post | cflow.cs:37:17:37:22 | exit Switch | cflow.cs:37:17:37:22 | exit Switch |
+| post | cflow.cs:37:17:37:22 | exit Switch | cflow.cs:41:13:41:19 | case ...: |
+| post | cflow.cs:37:17:37:22 | exit Switch | cflow.cs:42:17:42:39 | ...; |
 | post | cflow.cs:37:17:37:22 | exit Switch | cflow.cs:44:13:44:19 | case ...: |
+| post | cflow.cs:37:17:37:22 | exit Switch | cflow.cs:45:17:45:39 | ...; |
 | post | cflow.cs:37:17:37:22 | exit Switch | cflow.cs:47:13:47:19 | case ...: |
 | post | cflow.cs:37:17:37:22 | exit Switch | cflow.cs:48:17:48:39 | ...; |
 | post | cflow.cs:37:17:37:22 | exit Switch | cflow.cs:51:9:59:9 | switch (...) {...} |
@@ -902,23 +905,38 @@
 | post | cflow.cs:37:17:37:22 | exit Switch | cflow.cs:64:27:64:54 | object creation of type NullReferenceException |
 | post | cflow.cs:37:17:37:22 | exit Switch | cflow.cs:65:17:65:22 | break; |
 | post | cflow.cs:37:17:37:22 | exit Switch | cflow.cs:67:16:67:16 | access to parameter a |
+| post | cflow.cs:41:13:41:19 | case ...: | cflow.cs:37:17:37:22 | enter Switch |
+| post | cflow.cs:41:13:41:19 | case ...: | cflow.cs:41:13:41:19 | case ...: |
+| post | cflow.cs:41:13:41:19 | case ...: | cflow.cs:45:17:45:39 | ...; |
 | post | cflow.cs:42:17:42:39 | ...; | cflow.cs:42:17:42:39 | ...; |
 | post | cflow.cs:44:13:44:19 | case ...: | cflow.cs:37:17:37:22 | enter Switch |
+| post | cflow.cs:44:13:44:19 | case ...: | cflow.cs:41:13:41:19 | case ...: |
+| post | cflow.cs:44:13:44:19 | case ...: | cflow.cs:42:17:42:39 | ...; |
 | post | cflow.cs:44:13:44:19 | case ...: | cflow.cs:44:13:44:19 | case ...: |
+| post | cflow.cs:44:13:44:19 | case ...: | cflow.cs:45:17:45:39 | ...; |
 | post | cflow.cs:45:17:45:39 | ...; | cflow.cs:45:17:45:39 | ...; |
 | post | cflow.cs:47:13:47:19 | case ...: | cflow.cs:37:17:37:22 | enter Switch |
+| post | cflow.cs:47:13:47:19 | case ...: | cflow.cs:41:13:41:19 | case ...: |
+| post | cflow.cs:47:13:47:19 | case ...: | cflow.cs:42:17:42:39 | ...; |
 | post | cflow.cs:47:13:47:19 | case ...: | cflow.cs:44:13:44:19 | case ...: |
+| post | cflow.cs:47:13:47:19 | case ...: | cflow.cs:45:17:45:39 | ...; |
 | post | cflow.cs:47:13:47:19 | case ...: | cflow.cs:47:13:47:19 | case ...: |
 | post | cflow.cs:48:17:48:39 | ...; | cflow.cs:48:17:48:39 | ...; |
 | post | cflow.cs:51:9:59:9 | switch (...) {...} | cflow.cs:37:17:37:22 | enter Switch |
+| post | cflow.cs:51:9:59:9 | switch (...) {...} | cflow.cs:41:13:41:19 | case ...: |
+| post | cflow.cs:51:9:59:9 | switch (...) {...} | cflow.cs:42:17:42:39 | ...; |
 | post | cflow.cs:51:9:59:9 | switch (...) {...} | cflow.cs:44:13:44:19 | case ...: |
+| post | cflow.cs:51:9:59:9 | switch (...) {...} | cflow.cs:45:17:45:39 | ...; |
 | post | cflow.cs:51:9:59:9 | switch (...) {...} | cflow.cs:47:13:47:19 | case ...: |
 | post | cflow.cs:51:9:59:9 | switch (...) {...} | cflow.cs:48:17:48:39 | ...; |
 | post | cflow.cs:51:9:59:9 | switch (...) {...} | cflow.cs:51:9:59:9 | switch (...) {...} |
 | post | cflow.cs:54:17:54:48 | ...; | cflow.cs:54:17:54:48 | ...; |
 | post | cflow.cs:56:13:56:20 | default: | cflow.cs:56:13:56:20 | default: |
 | post | cflow.cs:60:9:66:9 | switch (...) {...} | cflow.cs:37:17:37:22 | enter Switch |
+| post | cflow.cs:60:9:66:9 | switch (...) {...} | cflow.cs:41:13:41:19 | case ...: |
+| post | cflow.cs:60:9:66:9 | switch (...) {...} | cflow.cs:42:17:42:39 | ...; |
 | post | cflow.cs:60:9:66:9 | switch (...) {...} | cflow.cs:44:13:44:19 | case ...: |
+| post | cflow.cs:60:9:66:9 | switch (...) {...} | cflow.cs:45:17:45:39 | ...; |
 | post | cflow.cs:60:9:66:9 | switch (...) {...} | cflow.cs:47:13:47:19 | case ...: |
 | post | cflow.cs:60:9:66:9 | switch (...) {...} | cflow.cs:48:17:48:39 | ...; |
 | post | cflow.cs:60:9:66:9 | switch (...) {...} | cflow.cs:51:9:59:9 | switch (...) {...} |
@@ -2558,6 +2576,7 @@
 | pre | cflow.cs:33:17:33:37 | ...; | cflow.cs:33:17:33:37 | ...; |
 | pre | cflow.cs:37:17:37:22 | enter Switch | cflow.cs:37:17:37:22 | enter Switch |
 | pre | cflow.cs:37:17:37:22 | enter Switch | cflow.cs:37:17:37:22 | exit Switch |
+| pre | cflow.cs:37:17:37:22 | enter Switch | cflow.cs:41:13:41:19 | case ...: |
 | pre | cflow.cs:37:17:37:22 | enter Switch | cflow.cs:42:17:42:39 | ...; |
 | pre | cflow.cs:37:17:37:22 | enter Switch | cflow.cs:44:13:44:19 | case ...: |
 | pre | cflow.cs:37:17:37:22 | enter Switch | cflow.cs:45:17:45:39 | ...; |
@@ -2572,9 +2591,25 @@
 | pre | cflow.cs:37:17:37:22 | enter Switch | cflow.cs:65:17:65:22 | break; |
 | pre | cflow.cs:37:17:37:22 | enter Switch | cflow.cs:67:16:67:16 | access to parameter a |
 | pre | cflow.cs:37:17:37:22 | exit Switch | cflow.cs:37:17:37:22 | exit Switch |
+| pre | cflow.cs:41:13:41:19 | case ...: | cflow.cs:37:17:37:22 | exit Switch |
+| pre | cflow.cs:41:13:41:19 | case ...: | cflow.cs:41:13:41:19 | case ...: |
+| pre | cflow.cs:41:13:41:19 | case ...: | cflow.cs:42:17:42:39 | ...; |
+| pre | cflow.cs:41:13:41:19 | case ...: | cflow.cs:44:13:44:19 | case ...: |
+| pre | cflow.cs:41:13:41:19 | case ...: | cflow.cs:45:17:45:39 | ...; |
+| pre | cflow.cs:41:13:41:19 | case ...: | cflow.cs:47:13:47:19 | case ...: |
+| pre | cflow.cs:41:13:41:19 | case ...: | cflow.cs:48:17:48:39 | ...; |
+| pre | cflow.cs:41:13:41:19 | case ...: | cflow.cs:51:9:59:9 | switch (...) {...} |
+| pre | cflow.cs:41:13:41:19 | case ...: | cflow.cs:54:17:54:48 | ...; |
+| pre | cflow.cs:41:13:41:19 | case ...: | cflow.cs:56:13:56:20 | default: |
+| pre | cflow.cs:41:13:41:19 | case ...: | cflow.cs:60:9:66:9 | switch (...) {...} |
+| pre | cflow.cs:41:13:41:19 | case ...: | cflow.cs:63:17:64:55 | if (...) ... |
+| pre | cflow.cs:41:13:41:19 | case ...: | cflow.cs:64:27:64:54 | object creation of type NullReferenceException |
+| pre | cflow.cs:41:13:41:19 | case ...: | cflow.cs:65:17:65:22 | break; |
+| pre | cflow.cs:41:13:41:19 | case ...: | cflow.cs:67:16:67:16 | access to parameter a |
 | pre | cflow.cs:42:17:42:39 | ...; | cflow.cs:42:17:42:39 | ...; |
 | pre | cflow.cs:44:13:44:19 | case ...: | cflow.cs:37:17:37:22 | exit Switch |
 | pre | cflow.cs:44:13:44:19 | case ...: | cflow.cs:44:13:44:19 | case ...: |
+| pre | cflow.cs:44:13:44:19 | case ...: | cflow.cs:45:17:45:39 | ...; |
 | pre | cflow.cs:44:13:44:19 | case ...: | cflow.cs:47:13:47:19 | case ...: |
 | pre | cflow.cs:44:13:44:19 | case ...: | cflow.cs:48:17:48:39 | ...; |
 | pre | cflow.cs:44:13:44:19 | case ...: | cflow.cs:51:9:59:9 | switch (...) {...} |
diff --git a/csharp/ql/test/library-tests/controlflow/graph/ConditionBlock.expected b/csharp/ql/test/library-tests/controlflow/graph/ConditionBlock.expected
index ca5822cba63d..f735a41420f1 100644
--- a/csharp/ql/test/library-tests/controlflow/graph/ConditionBlock.expected
+++ b/csharp/ql/test/library-tests/controlflow/graph/ConditionBlock.expected
@@ -288,6 +288,7 @@
 | Switch.cs:14:18:14:20 | "a" | Switch.cs:27:13:27:39 | case ...: | false |
 | Switch.cs:14:18:14:20 | "a" | Switch.cs:27:32:27:38 | call to method Throw | false |
 | Switch.cs:14:18:14:20 | "a" | Switch.cs:30:13:30:20 | default: | false |
+| Switch.cs:16:18:16:18 | 0 | Switch.cs:17:23:17:37 | object creation of type Exception | true |
 | Switch.cs:16:18:16:18 | 0 | Switch.cs:18:13:18:22 | case ...: | false |
 | Switch.cs:16:18:16:18 | 0 | Switch.cs:19:17:19:29 | goto default; | false |
 | Switch.cs:16:18:16:18 | 0 | Switch.cs:20:13:20:23 | case ...: | false |
@@ -422,19 +423,9 @@
 | cflow.cs:28:22:28:31 | ... == ... | cflow.cs:33:17:33:37 | ...; | false |
 | cflow.cs:30:22:30:31 | ... == ... | cflow.cs:31:17:31:42 | ...; | true |
 | cflow.cs:30:22:30:31 | ... == ... | cflow.cs:33:17:33:37 | ...; | false |
-| cflow.cs:41:18:41:18 | 1 | cflow.cs:37:17:37:22 | exit Switch | false |
-| cflow.cs:41:18:41:18 | 1 | cflow.cs:44:13:44:19 | case ...: | false |
-| cflow.cs:41:18:41:18 | 1 | cflow.cs:47:13:47:19 | case ...: | false |
-| cflow.cs:41:18:41:18 | 1 | cflow.cs:48:17:48:39 | ...; | false |
-| cflow.cs:41:18:41:18 | 1 | cflow.cs:51:9:59:9 | switch (...) {...} | false |
-| cflow.cs:41:18:41:18 | 1 | cflow.cs:54:17:54:48 | ...; | false |
-| cflow.cs:41:18:41:18 | 1 | cflow.cs:56:13:56:20 | default: | false |
-| cflow.cs:41:18:41:18 | 1 | cflow.cs:60:9:66:9 | switch (...) {...} | false |
-| cflow.cs:41:18:41:18 | 1 | cflow.cs:63:17:64:55 | if (...) ... | false |
-| cflow.cs:41:18:41:18 | 1 | cflow.cs:64:27:64:54 | object creation of type NullReferenceException | false |
-| cflow.cs:41:18:41:18 | 1 | cflow.cs:65:17:65:22 | break; | false |
-| cflow.cs:41:18:41:18 | 1 | cflow.cs:67:16:67:16 | access to parameter a | false |
+| cflow.cs:41:18:41:18 | 1 | cflow.cs:42:17:42:39 | ...; | true |
 | cflow.cs:44:18:44:18 | 2 | cflow.cs:37:17:37:22 | exit Switch | false |
+| cflow.cs:44:18:44:18 | 2 | cflow.cs:45:17:45:39 | ...; | true |
 | cflow.cs:44:18:44:18 | 2 | cflow.cs:47:13:47:19 | case ...: | false |
 | cflow.cs:44:18:44:18 | 2 | cflow.cs:48:17:48:39 | ...; | false |
 | cflow.cs:44:18:44:18 | 2 | cflow.cs:51:9:59:9 | switch (...) {...} | false |
diff --git a/csharp/ql/test/library-tests/controlflow/graph/Dominance.expected b/csharp/ql/test/library-tests/controlflow/graph/Dominance.expected
index 1396a925f9d6..0ba1a48ed223 100644
--- a/csharp/ql/test/library-tests/controlflow/graph/Dominance.expected
+++ b/csharp/ql/test/library-tests/controlflow/graph/Dominance.expected
@@ -1413,9 +1413,9 @@
 | post | Switch.cs:12:17:12:17 | access to parameter o | Switch.cs:12:9:32:9 | switch (...) {...} |
 | post | Switch.cs:14:13:14:21 | case ...: | Switch.cs:12:17:12:17 | access to parameter o |
 | post | Switch.cs:14:18:14:20 | "a" | Switch.cs:14:13:14:21 | case ...: |
+| post | Switch.cs:16:13:16:19 | case ...: | Switch.cs:23:17:23:28 | goto case ...; |
 | post | Switch.cs:16:18:16:18 | 0 | Switch.cs:16:13:16:19 | case ...: |
 | post | Switch.cs:17:17:17:38 | throw ...; | Switch.cs:17:23:17:37 | object creation of type Exception |
-| post | Switch.cs:17:23:17:37 | object creation of type Exception | Switch.cs:23:17:23:28 | goto case ...; |
 | post | Switch.cs:18:18:18:21 | null | Switch.cs:18:13:18:22 | case ...: |
 | post | Switch.cs:20:18:20:22 | Int32 i | Switch.cs:20:13:20:23 | case ...: |
 | post | Switch.cs:21:21:21:21 | access to parameter o | Switch.cs:21:17:22:27 | if (...) ... |
@@ -1702,12 +1702,14 @@
 | post | cflow.cs:39:9:50:9 | switch (...) {...} | cflow.cs:38:5:68:5 | {...} |
 | post | cflow.cs:39:17:39:17 | access to parameter a | cflow.cs:39:9:50:9 | switch (...) {...} |
 | post | cflow.cs:41:13:41:19 | case ...: | cflow.cs:39:17:39:17 | access to parameter a |
+| post | cflow.cs:41:13:41:19 | case ...: | cflow.cs:46:17:46:28 | goto case ...; |
 | post | cflow.cs:41:18:41:18 | 1 | cflow.cs:41:13:41:19 | case ...: |
 | post | cflow.cs:42:17:42:38 | call to method WriteLine | cflow.cs:42:35:42:37 | "1" |
 | post | cflow.cs:42:35:42:37 | "1" | cflow.cs:42:17:42:39 | ...; |
 | post | cflow.cs:43:17:43:28 | goto case ...; | cflow.cs:43:27:43:27 | 2 |
 | post | cflow.cs:43:27:43:27 | 2 | cflow.cs:42:17:42:38 | call to method WriteLine |
 | post | cflow.cs:44:13:44:19 | case ...: | cflow.cs:41:18:41:18 | 1 |
+| post | cflow.cs:44:13:44:19 | case ...: | cflow.cs:43:17:43:28 | goto case ...; |
 | post | cflow.cs:44:18:44:18 | 2 | cflow.cs:44:13:44:19 | case ...: |
 | post | cflow.cs:45:17:45:38 | call to method WriteLine | cflow.cs:45:35:45:37 | "2" |
 | post | cflow.cs:45:35:45:37 | "2" | cflow.cs:45:17:45:39 | ...; |
@@ -4262,6 +4264,7 @@
 | pre | cflow.cs:42:35:42:37 | "1" | cflow.cs:42:17:42:38 | call to method WriteLine |
 | pre | cflow.cs:43:27:43:27 | 2 | cflow.cs:43:17:43:28 | goto case ...; |
 | pre | cflow.cs:44:13:44:19 | case ...: | cflow.cs:44:18:44:18 | 2 |
+| pre | cflow.cs:44:18:44:18 | 2 | cflow.cs:45:17:45:39 | ...; |
 | pre | cflow.cs:44:18:44:18 | 2 | cflow.cs:47:13:47:19 | case ...: |
 | pre | cflow.cs:45:17:45:38 | call to method WriteLine | cflow.cs:46:27:46:27 | 1 |
 | pre | cflow.cs:45:17:45:39 | ...; | cflow.cs:45:35:45:37 | "2" |
diff --git a/csharp/ql/test/library-tests/controlflow/graph/ElementGraph.expected b/csharp/ql/test/library-tests/controlflow/graph/ElementGraph.expected
index 0bbc17d827ac..3e5e436d6fd4 100644
--- a/csharp/ql/test/library-tests/controlflow/graph/ElementGraph.expected
+++ b/csharp/ql/test/library-tests/controlflow/graph/ElementGraph.expected
@@ -1153,7 +1153,7 @@
 | Switch.cs:18:13:18:22 | case ...: | Switch.cs:18:18:18:21 | null | semmle.label | successor |
 | Switch.cs:18:18:18:21 | null | Switch.cs:19:17:19:29 | goto default; | semmle.label | match |
 | Switch.cs:18:18:18:21 | null | Switch.cs:20:13:20:23 | case ...: | semmle.label | no-match |
-| Switch.cs:19:17:19:29 | goto default; | Switch.cs:30:13:30:20 | default: | semmle.label | goto default |
+| Switch.cs:19:17:19:29 | goto default; | Switch.cs:30:13:30:20 | default: | semmle.label | goto(default) |
 | Switch.cs:20:13:20:23 | case ...: | Switch.cs:20:18:20:22 | Int32 i | semmle.label | successor |
 | Switch.cs:20:18:20:22 | Int32 i | Switch.cs:21:17:22:27 | if (...) ... | semmle.label | match |
 | Switch.cs:20:18:20:22 | Int32 i | Switch.cs:24:13:24:56 | case ...: | semmle.label | no-match |
@@ -1162,7 +1162,7 @@
 | Switch.cs:21:21:21:29 | ... == ... | Switch.cs:22:21:22:27 | return ...; | semmle.label | true |
 | Switch.cs:21:21:21:29 | ... == ... | Switch.cs:23:27:23:27 | 0 | semmle.label | false |
 | Switch.cs:21:26:21:29 | null | Switch.cs:21:21:21:29 | ... == ... | semmle.label | successor |
-| Switch.cs:23:17:23:28 | goto case ...; | Switch.cs:17:23:17:37 | object creation of type Exception | semmle.label | goto(0) |
+| Switch.cs:23:17:23:28 | goto case ...; | Switch.cs:16:13:16:19 | case ...: | semmle.label | goto(0) |
 | Switch.cs:23:27:23:27 | 0 | Switch.cs:23:17:23:28 | goto case ...; | semmle.label | successor |
 | Switch.cs:24:13:24:56 | case ...: | Switch.cs:24:18:24:25 | String s | semmle.label | successor |
 | Switch.cs:24:18:24:25 | String s | Switch.cs:24:32:24:55 | ... && ... | semmle.label | match |
@@ -1454,7 +1454,7 @@
 | cflow.cs:42:17:42:38 | call to method WriteLine | cflow.cs:43:27:43:27 | 2 | semmle.label | successor |
 | cflow.cs:42:17:42:39 | ...; | cflow.cs:42:35:42:37 | "1" | semmle.label | successor |
 | cflow.cs:42:35:42:37 | "1" | cflow.cs:42:17:42:38 | call to method WriteLine | semmle.label | successor |
-| cflow.cs:43:17:43:28 | goto case ...; | cflow.cs:45:17:45:39 | ...; | semmle.label | goto(2) |
+| cflow.cs:43:17:43:28 | goto case ...; | cflow.cs:44:13:44:19 | case ...: | semmle.label | goto(2) |
 | cflow.cs:43:27:43:27 | 2 | cflow.cs:43:17:43:28 | goto case ...; | semmle.label | successor |
 | cflow.cs:44:13:44:19 | case ...: | cflow.cs:44:18:44:18 | 2 | semmle.label | successor |
 | cflow.cs:44:18:44:18 | 2 | cflow.cs:45:17:45:39 | ...; | semmle.label | match |
@@ -1462,7 +1462,7 @@
 | cflow.cs:45:17:45:38 | call to method WriteLine | cflow.cs:46:27:46:27 | 1 | semmle.label | successor |
 | cflow.cs:45:17:45:39 | ...; | cflow.cs:45:35:45:37 | "2" | semmle.label | successor |
 | cflow.cs:45:35:45:37 | "2" | cflow.cs:45:17:45:38 | call to method WriteLine | semmle.label | successor |
-| cflow.cs:46:17:46:28 | goto case ...; | cflow.cs:42:17:42:39 | ...; | semmle.label | goto(1) |
+| cflow.cs:46:17:46:28 | goto case ...; | cflow.cs:41:13:41:19 | case ...: | semmle.label | goto(1) |
 | cflow.cs:46:27:46:27 | 1 | cflow.cs:46:17:46:28 | goto case ...; | semmle.label | successor |
 | cflow.cs:47:13:47:19 | case ...: | cflow.cs:47:18:47:18 | 3 | semmle.label | successor |
 | cflow.cs:47:18:47:18 | 3 | cflow.cs:48:17:48:39 | ...; | semmle.label | match |
@@ -2059,7 +2059,7 @@
 | cflow.cs:359:13:359:19 | case ...: | cflow.cs:359:18:359:18 | 0 | semmle.label | successor |
 | cflow.cs:359:18:359:18 | 0 | cflow.cs:360:17:360:29 | goto default; | semmle.label | match |
 | cflow.cs:359:18:359:18 | 0 | cflow.cs:361:13:361:19 | case ...: | semmle.label | no-match |
-| cflow.cs:360:17:360:29 | goto default; | cflow.cs:366:13:366:20 | default: | semmle.label | goto default |
+| cflow.cs:360:17:360:29 | goto default; | cflow.cs:366:13:366:20 | default: | semmle.label | goto(default) |
 | cflow.cs:361:13:361:19 | case ...: | cflow.cs:361:18:361:18 | 1 | semmle.label | successor |
 | cflow.cs:361:18:361:18 | 1 | cflow.cs:362:17:362:37 | ...; | semmle.label | match |
 | cflow.cs:361:18:361:18 | 1 | cflow.cs:364:13:364:19 | case ...: | semmle.label | no-match |
diff --git a/csharp/ql/test/library-tests/controlflow/graph/ExitElement.expected b/csharp/ql/test/library-tests/controlflow/graph/ExitElement.expected
index 117327738fdd..07afaff6bed8 100644
--- a/csharp/ql/test/library-tests/controlflow/graph/ExitElement.expected
+++ b/csharp/ql/test/library-tests/controlflow/graph/ExitElement.expected
@@ -1594,10 +1594,10 @@
 | Switch.cs:17:17:17:38 | throw ...; | Switch.cs:17:17:17:38 | throw ...; | throw(Exception) |
 | Switch.cs:17:23:17:37 | object creation of type Exception | Switch.cs:17:23:17:37 | object creation of type Exception | normal |
 | Switch.cs:18:13:18:22 | case ...: | Switch.cs:18:18:18:21 | null | no-match |
-| Switch.cs:18:13:18:22 | case ...: | Switch.cs:19:17:19:29 | goto default; | goto default |
+| Switch.cs:18:13:18:22 | case ...: | Switch.cs:19:17:19:29 | goto default; | goto(default) |
 | Switch.cs:18:18:18:21 | null | Switch.cs:18:18:18:21 | null | match |
 | Switch.cs:18:18:18:21 | null | Switch.cs:18:18:18:21 | null | no-match |
-| Switch.cs:19:17:19:29 | goto default; | Switch.cs:19:17:19:29 | goto default; | goto default |
+| Switch.cs:19:17:19:29 | goto default; | Switch.cs:19:17:19:29 | goto default; | goto(default) |
 | Switch.cs:20:13:20:23 | case ...: | Switch.cs:20:18:20:22 | Int32 i | no-match |
 | Switch.cs:20:13:20:23 | case ...: | Switch.cs:21:21:21:29 | ... == ... | false |
 | Switch.cs:20:13:20:23 | case ...: | Switch.cs:22:21:22:27 | return ...; | return |
@@ -1610,7 +1610,7 @@
 | Switch.cs:21:21:21:29 | ... == ... | Switch.cs:21:21:21:29 | ... == ... | true |
 | Switch.cs:21:26:21:29 | null | Switch.cs:21:26:21:29 | null | normal |
 | Switch.cs:22:21:22:27 | return ...; | Switch.cs:22:21:22:27 | return ...; | return |
-| Switch.cs:23:17:23:28 | goto case ...; | Switch.cs:23:17:23:28 | goto case ...; | goto case(0) |
+| Switch.cs:23:17:23:28 | goto case ...; | Switch.cs:23:17:23:28 | goto case ...; | goto(0) |
 | Switch.cs:23:27:23:27 | 0 | Switch.cs:23:27:23:27 | 0 | normal |
 | Switch.cs:24:13:24:56 | case ...: | Switch.cs:24:18:24:25 | String s | no-match |
 | Switch.cs:24:13:24:56 | case ...: | Switch.cs:24:32:24:43 | ... > ... | false |
@@ -2025,7 +2025,7 @@
 | cflow.cs:42:17:42:38 | call to method WriteLine | cflow.cs:42:17:42:38 | call to method WriteLine | normal |
 | cflow.cs:42:17:42:39 | ...; | cflow.cs:42:17:42:38 | call to method WriteLine | normal |
 | cflow.cs:42:35:42:37 | "1" | cflow.cs:42:35:42:37 | "1" | normal |
-| cflow.cs:43:17:43:28 | goto case ...; | cflow.cs:43:17:43:28 | goto case ...; | goto case(2) |
+| cflow.cs:43:17:43:28 | goto case ...; | cflow.cs:43:17:43:28 | goto case ...; | goto(2) |
 | cflow.cs:43:27:43:27 | 2 | cflow.cs:43:27:43:27 | 2 | normal |
 | cflow.cs:44:13:44:19 | case ...: | cflow.cs:44:18:44:18 | 2 | no-match |
 | cflow.cs:44:13:44:19 | case ...: | cflow.cs:45:17:45:38 | call to method WriteLine | normal |
@@ -2034,7 +2034,7 @@
 | cflow.cs:45:17:45:38 | call to method WriteLine | cflow.cs:45:17:45:38 | call to method WriteLine | normal |
 | cflow.cs:45:17:45:39 | ...; | cflow.cs:45:17:45:38 | call to method WriteLine | normal |
 | cflow.cs:45:35:45:37 | "2" | cflow.cs:45:35:45:37 | "2" | normal |
-| cflow.cs:46:17:46:28 | goto case ...; | cflow.cs:46:17:46:28 | goto case ...; | goto case(1) |
+| cflow.cs:46:17:46:28 | goto case ...; | cflow.cs:46:17:46:28 | goto case ...; | goto(1) |
 | cflow.cs:46:27:46:27 | 1 | cflow.cs:46:27:46:27 | 1 | normal |
 | cflow.cs:47:13:47:19 | case ...: | cflow.cs:47:18:47:18 | 3 | no-match |
 | cflow.cs:47:13:47:19 | case ...: | cflow.cs:48:17:48:38 | call to method WriteLine | normal |
@@ -2868,10 +2868,10 @@
 | cflow.cs:357:17:357:32 | ... + ... | cflow.cs:357:17:357:32 | ... + ... | normal |
 | cflow.cs:357:32:357:32 | 3 | cflow.cs:357:32:357:32 | 3 | normal |
 | cflow.cs:359:13:359:19 | case ...: | cflow.cs:359:18:359:18 | 0 | no-match |
-| cflow.cs:359:13:359:19 | case ...: | cflow.cs:360:17:360:29 | goto default; | goto default |
+| cflow.cs:359:13:359:19 | case ...: | cflow.cs:360:17:360:29 | goto default; | goto(default) |
 | cflow.cs:359:18:359:18 | 0 | cflow.cs:359:18:359:18 | 0 | match |
 | cflow.cs:359:18:359:18 | 0 | cflow.cs:359:18:359:18 | 0 | no-match |
-| cflow.cs:360:17:360:29 | goto default; | cflow.cs:360:17:360:29 | goto default; | goto default |
+| cflow.cs:360:17:360:29 | goto default; | cflow.cs:360:17:360:29 | goto default; | goto(default) |
 | cflow.cs:361:13:361:19 | case ...: | cflow.cs:361:18:361:18 | 1 | no-match |
 | cflow.cs:361:13:361:19 | case ...: | cflow.cs:362:17:362:36 | call to method WriteLine | normal |
 | cflow.cs:361:18:361:18 | 1 | cflow.cs:361:18:361:18 | 1 | match |
diff --git a/csharp/ql/test/library-tests/controlflow/graph/NodeGraph.expected b/csharp/ql/test/library-tests/controlflow/graph/NodeGraph.expected
index 1695127da937..2123a119900c 100644
--- a/csharp/ql/test/library-tests/controlflow/graph/NodeGraph.expected
+++ b/csharp/ql/test/library-tests/controlflow/graph/NodeGraph.expected
@@ -1606,7 +1606,7 @@
 | Switch.cs:18:13:18:22 | case ...: | Switch.cs:18:18:18:21 | null | semmle.label | successor |
 | Switch.cs:18:18:18:21 | null | Switch.cs:19:17:19:29 | goto default; | semmle.label | match |
 | Switch.cs:18:18:18:21 | null | Switch.cs:20:13:20:23 | case ...: | semmle.label | no-match |
-| Switch.cs:19:17:19:29 | goto default; | Switch.cs:30:13:30:20 | default: | semmle.label | goto default |
+| Switch.cs:19:17:19:29 | goto default; | Switch.cs:30:13:30:20 | default: | semmle.label | goto(default) |
 | Switch.cs:20:13:20:23 | case ...: | Switch.cs:20:18:20:22 | Int32 i | semmle.label | successor |
 | Switch.cs:20:18:20:22 | Int32 i | Switch.cs:21:17:22:27 | if (...) ... | semmle.label | match |
 | Switch.cs:20:18:20:22 | Int32 i | Switch.cs:24:13:24:56 | case ...: | semmle.label | no-match |
@@ -1616,7 +1616,7 @@
 | Switch.cs:21:21:21:29 | ... == ... | Switch.cs:23:27:23:27 | 0 | semmle.label | false |
 | Switch.cs:21:26:21:29 | null | Switch.cs:21:21:21:29 | ... == ... | semmle.label | successor |
 | Switch.cs:22:21:22:27 | return ...; | Switch.cs:10:10:10:11 | exit M2 | semmle.label | return |
-| Switch.cs:23:17:23:28 | goto case ...; | Switch.cs:17:23:17:37 | object creation of type Exception | semmle.label | goto(0) |
+| Switch.cs:23:17:23:28 | goto case ...; | Switch.cs:16:13:16:19 | case ...: | semmle.label | goto(0) |
 | Switch.cs:23:27:23:27 | 0 | Switch.cs:23:17:23:28 | goto case ...; | semmle.label | successor |
 | Switch.cs:24:13:24:56 | case ...: | Switch.cs:24:18:24:25 | String s | semmle.label | successor |
 | Switch.cs:24:18:24:25 | String s | Switch.cs:24:32:24:55 | ... && ... | semmle.label | match |
@@ -1959,7 +1959,7 @@
 | cflow.cs:42:17:42:38 | call to method WriteLine | cflow.cs:43:27:43:27 | 2 | semmle.label | successor |
 | cflow.cs:42:17:42:39 | ...; | cflow.cs:42:35:42:37 | "1" | semmle.label | successor |
 | cflow.cs:42:35:42:37 | "1" | cflow.cs:42:17:42:38 | call to method WriteLine | semmle.label | successor |
-| cflow.cs:43:17:43:28 | goto case ...; | cflow.cs:45:17:45:39 | ...; | semmle.label | goto(2) |
+| cflow.cs:43:17:43:28 | goto case ...; | cflow.cs:44:13:44:19 | case ...: | semmle.label | goto(2) |
 | cflow.cs:43:27:43:27 | 2 | cflow.cs:43:17:43:28 | goto case ...; | semmle.label | successor |
 | cflow.cs:44:13:44:19 | case ...: | cflow.cs:44:18:44:18 | 2 | semmle.label | successor |
 | cflow.cs:44:18:44:18 | 2 | cflow.cs:45:17:45:39 | ...; | semmle.label | match |
@@ -1967,7 +1967,7 @@
 | cflow.cs:45:17:45:38 | call to method WriteLine | cflow.cs:46:27:46:27 | 1 | semmle.label | successor |
 | cflow.cs:45:17:45:39 | ...; | cflow.cs:45:35:45:37 | "2" | semmle.label | successor |
 | cflow.cs:45:35:45:37 | "2" | cflow.cs:45:17:45:38 | call to method WriteLine | semmle.label | successor |
-| cflow.cs:46:17:46:28 | goto case ...; | cflow.cs:42:17:42:39 | ...; | semmle.label | goto(1) |
+| cflow.cs:46:17:46:28 | goto case ...; | cflow.cs:41:13:41:19 | case ...: | semmle.label | goto(1) |
 | cflow.cs:46:27:46:27 | 1 | cflow.cs:46:17:46:28 | goto case ...; | semmle.label | successor |
 | cflow.cs:47:13:47:19 | case ...: | cflow.cs:47:18:47:18 | 3 | semmle.label | successor |
 | cflow.cs:47:18:47:18 | 3 | cflow.cs:48:17:48:39 | ...; | semmle.label | match |
@@ -2806,7 +2806,7 @@
 | cflow.cs:359:13:359:19 | case ...: | cflow.cs:359:18:359:18 | 0 | semmle.label | successor |
 | cflow.cs:359:18:359:18 | 0 | cflow.cs:360:17:360:29 | goto default; | semmle.label | match |
 | cflow.cs:359:18:359:18 | 0 | cflow.cs:361:13:361:19 | case ...: | semmle.label | no-match |
-| cflow.cs:360:17:360:29 | goto default; | cflow.cs:366:13:366:20 | default: | semmle.label | goto default |
+| cflow.cs:360:17:360:29 | goto default; | cflow.cs:366:13:366:20 | default: | semmle.label | goto(default) |
 | cflow.cs:361:13:361:19 | case ...: | cflow.cs:361:18:361:18 | 1 | semmle.label | successor |
 | cflow.cs:361:18:361:18 | 1 | cflow.cs:362:17:362:37 | ...; | semmle.label | match |
 | cflow.cs:361:18:361:18 | 1 | cflow.cs:364:13:364:19 | case ...: | semmle.label | no-match |
diff --git a/csharp/ql/test/library-tests/goto/Goto1.expected b/csharp/ql/test/library-tests/goto/Goto1.expected
index 3e5d62214d9a..69b32aa4314c 100644
--- a/csharp/ql/test/library-tests/goto/Goto1.expected
+++ b/csharp/ql/test/library-tests/goto/Goto1.expected
@@ -13,13 +13,13 @@
 | goto.cs:12:18:12:21 | null | goto.cs:12:24:12:25 | s3: | semmle.label | match |
 | goto.cs:12:18:12:21 | null | goto.cs:13:13:13:21 | case ...: | semmle.label | no-match |
 | goto.cs:12:24:12:25 | s3: | goto.cs:12:38:12:40 | "1" | semmle.label | successor |
-| goto.cs:12:28:12:41 | goto case ...; | goto.cs:13:23:13:24 | s4: | semmle.label | goto(1) |
+| goto.cs:12:28:12:41 | goto case ...; | goto.cs:13:13:13:21 | case ...: | semmle.label | goto(1) |
 | goto.cs:12:38:12:40 | "1" | goto.cs:12:28:12:41 | goto case ...; | semmle.label | successor |
 | goto.cs:13:13:13:21 | case ...: | goto.cs:13:18:13:20 | "1" | semmle.label | successor |
 | goto.cs:13:18:13:20 | "1" | goto.cs:13:23:13:24 | s4: | semmle.label | match |
 | goto.cs:13:18:13:20 | "1" | goto.cs:14:13:14:21 | case ...: | semmle.label | no-match |
 | goto.cs:13:23:13:24 | s4: | goto.cs:13:37:13:39 | "2" | semmle.label | successor |
-| goto.cs:13:27:13:40 | goto case ...; | goto.cs:14:23:14:24 | s5: | semmle.label | goto(2) |
+| goto.cs:13:27:13:40 | goto case ...; | goto.cs:14:13:14:21 | case ...: | semmle.label | goto(2) |
 | goto.cs:13:37:13:39 | "2" | goto.cs:13:27:13:40 | goto case ...; | semmle.label | successor |
 | goto.cs:14:13:14:21 | case ...: | goto.cs:14:18:14:20 | "2" | semmle.label | successor |
 | goto.cs:14:18:14:20 | "2" | goto.cs:14:23:14:24 | s5: | semmle.label | match |
@@ -30,7 +30,7 @@
 | goto.cs:15:18:15:20 | "3" | goto.cs:15:23:15:24 | s6: | semmle.label | match |
 | goto.cs:15:18:15:20 | "3" | goto.cs:16:13:16:21 | case ...: | semmle.label | no-match |
 | goto.cs:15:23:15:24 | s6: | goto.cs:15:27:15:39 | goto default; | semmle.label | successor |
-| goto.cs:15:27:15:39 | goto default; | goto.cs:17:13:17:20 | default: | semmle.label | goto default |
+| goto.cs:15:27:15:39 | goto default; | goto.cs:17:13:17:20 | default: | semmle.label | goto(default) |
 | goto.cs:16:13:16:21 | case ...: | goto.cs:16:18:16:20 | "4" | semmle.label | successor |
 | goto.cs:16:18:16:20 | "4" | goto.cs:16:23:16:24 | s7: | semmle.label | match |
 | goto.cs:16:18:16:20 | "4" | goto.cs:17:13:17:20 | default: | semmle.label | no-match |
@@ -38,7 +38,7 @@
 | goto.cs:16:27:16:32 | break; | goto.cs:19:9:19:10 | s9: | semmle.label | break |
 | goto.cs:17:13:17:20 | default: | goto.cs:17:22:17:23 | s8: | semmle.label | successor |
 | goto.cs:17:22:17:23 | s8: | goto.cs:17:36:17:39 | null | semmle.label | successor |
-| goto.cs:17:26:17:40 | goto case ...; | goto.cs:12:24:12:25 | s3: | semmle.label | goto(null) |
+| goto.cs:17:26:17:40 | goto case ...; | goto.cs:12:13:12:22 | case ...: | semmle.label | goto(null) |
 | goto.cs:17:36:17:39 | null | goto.cs:17:26:17:40 | goto case ...; | semmle.label | successor |
 | goto.cs:19:9:19:10 | s9: | goto.cs:19:12:19:12 | ; | semmle.label | successor |
 | goto.cs:19:12:19:12 | ; | goto.cs:4:17:4:20 | exit Main | semmle.label | successor |

From e6c258c6bad0ee169aebc56b134ae2bd04e8bcff Mon Sep 17 00:00:00 2001
From: Tom Hvitved <tom@semmle.com>
Date: Wed, 3 Jul 2019 16:25:24 +0200
Subject: [PATCH 2/3] C#: Restructure `Completion::isValidFor()`

---
 .../controlflow/internal/Completion.qll       | 118 ++++++++++--------
 1 file changed, 64 insertions(+), 54 deletions(-)

diff --git a/csharp/ql/src/semmle/code/csharp/controlflow/internal/Completion.qll b/csharp/ql/src/semmle/code/csharp/controlflow/internal/Completion.qll
index 440d611bf341..177cb03a9c93 100644
--- a/csharp/ql/src/semmle/code/csharp/controlflow/internal/Completion.qll
+++ b/csharp/ql/src/semmle/code/csharp/controlflow/internal/Completion.qll
@@ -73,60 +73,70 @@ class Completion extends TCompletion {
     else (
       this = TThrowCompletion(cfe.(TriedControlFlowElement).getAThrownException())
       or
-      if cfe instanceof ThrowElement
-      then this = TThrowCompletion(cfe.(ThrowElement).getThrownExceptionType())
-      else
-        if mustHaveBooleanCompletion(cfe)
-        then
-          exists(boolean value | isBooleanConstant(cfe, value) | this = TBooleanCompletion(value))
-          or
-          not isBooleanConstant(cfe, _) and
-          this = TBooleanCompletion(_)
-          or
-          // Corner case: In `if (x ?? y) { ... }`, `x` must have both a `true`
-          // completion, a `false` completion, and a `null` completion (but not a
-          // non-`null` completion)
-          mustHaveNullnessCompletion(cfe) and
-          this = TNullnessCompletion(true)
-        else
-          if mustHaveNullnessCompletion(cfe)
-          then
-            exists(boolean value | isNullnessConstant(cfe, value) |
-              this = TNullnessCompletion(value)
-            )
-            or
-            not isNullnessConstant(cfe, _) and
-            this = TNullnessCompletion(_)
-          else
-            if mustHaveMatchingCompletion(cfe)
-            then
-              exists(boolean value | isMatchingConstant(cfe, value) |
-                this = TMatchingCompletion(value)
-              )
-              or
-              not isMatchingConstant(cfe, _) and
-              this = TMatchingCompletion(_)
-            else
-              if mustHaveEmptinessCompletion(cfe)
-              then this = TEmptinessCompletion(_)
-              else
-                if cfe instanceof BreakStmt
-                then this = TBreakCompletion()
-                else
-                  if cfe instanceof ContinueStmt
-                  then this = TContinueCompletion()
-                  else
-                    if cfe instanceof GotoStmt
-                    then this = TGotoCompletion(cfe.(GotoStmt).getLabel())
-                    else
-                      if cfe instanceof ReturnStmt
-                      then this = TReturnCompletion()
-                      else
-                        if cfe instanceof YieldBreakStmt
-                        then
-                          // `yield break` behaves like a return statement
-                          this = TReturnCompletion()
-                        else this = TNormalCompletion()
+      cfe instanceof ThrowElement and
+      this = TThrowCompletion(cfe.(ThrowElement).getThrownExceptionType())
+      or
+      cfe instanceof BreakStmt and
+      this = TBreakCompletion()
+      or
+      cfe instanceof ContinueStmt and
+      this = TContinueCompletion()
+      or
+      cfe instanceof GotoStmt and
+      this = TGotoCompletion(cfe.(GotoStmt).getLabel())
+      or
+      cfe instanceof ReturnStmt and
+      this = TReturnCompletion()
+      or
+      cfe instanceof YieldBreakStmt and
+      // `yield break` behaves like a return statement
+      this = TReturnCompletion()
+      or
+      mustHaveBooleanCompletion(cfe) and
+      (
+        exists(boolean value | isBooleanConstant(cfe, value) | this = TBooleanCompletion(value))
+        or
+        not isBooleanConstant(cfe, _) and
+        this = TBooleanCompletion(_)
+        or
+        // Corner case: In `if (x ?? y) { ... }`, `x` must have both a `true`
+        // completion, a `false` completion, and a `null` completion (but not a
+        // non-`null` completion)
+        mustHaveNullnessCompletion(cfe) and
+        this = TNullnessCompletion(true)
+      )
+      or
+      mustHaveNullnessCompletion(cfe) and
+      not mustHaveBooleanCompletion(cfe) and
+      (
+        exists(boolean value | isNullnessConstant(cfe, value) | this = TNullnessCompletion(value))
+        or
+        not isNullnessConstant(cfe, _) and
+        this = TNullnessCompletion(_)
+      )
+      or
+      mustHaveMatchingCompletion(cfe) and
+      (
+        exists(boolean value | isMatchingConstant(cfe, value) | this = TMatchingCompletion(value))
+        or
+        not isMatchingConstant(cfe, _) and
+        this = TMatchingCompletion(_)
+      )
+      or
+      mustHaveEmptinessCompletion(cfe) and
+      this = TEmptinessCompletion(_)
+      or
+      not cfe instanceof ThrowElement and
+      not cfe instanceof BreakStmt and
+      not cfe instanceof ContinueStmt and
+      not cfe instanceof GotoStmt and
+      not cfe instanceof ReturnStmt and
+      not cfe instanceof YieldBreakStmt and
+      not mustHaveBooleanCompletion(cfe) and
+      not mustHaveNullnessCompletion(cfe) and
+      not mustHaveMatchingCompletion(cfe) and
+      not mustHaveEmptinessCompletion(cfe) and
+      this = TNormalCompletion()
     )
   }
 

From f56c17fc7723693574e02cf027733bb38758d6aa Mon Sep 17 00:00:00 2001
From: Tom Hvitved <tom@semmle.com>
Date: Thu, 4 Jul 2019 21:17:08 +0200
Subject: [PATCH 3/3] C#: Fix bad join-orders in `lastNonRec()`

---
 .../csharp/controlflow/ControlFlowGraph.qll    | 18 +++++++++++-------
 1 file changed, 11 insertions(+), 7 deletions(-)

diff --git a/csharp/ql/src/semmle/code/csharp/controlflow/ControlFlowGraph.qll b/csharp/ql/src/semmle/code/csharp/controlflow/ControlFlowGraph.qll
index 6b9e37a14d46..f36089b2d123 100644
--- a/csharp/ql/src/semmle/code/csharp/controlflow/ControlFlowGraph.qll
+++ b/csharp/ql/src/semmle/code/csharp/controlflow/ControlFlowGraph.qll
@@ -746,6 +746,10 @@ module ControlFlow {
         result = TSelf(any(Completion c | c.isValidFor(cfe)))
       }
 
+      private TRec specificBoolean(boolean value) {
+        result = TRec(TLastRecSpecificCompletion(any(BooleanCompletion bc | bc.getValue() = value)))
+      }
+
       /**
        * Gets an element from which the last element of `cfe` can be computed
        * (recursively) based on computation specification `c`. The predicate
@@ -788,7 +792,7 @@ module ControlFlow {
         cfe = any(LogicalAndExpr lae |
             // Left operand exits with a false completion
             result = lae.getLeftOperand() and
-            c = TRec(TLastRecSpecificCompletion(any(FalseCompletion fc)))
+            c = specificBoolean(false)
             or
             // Left operand exits abnormally
             result = lae.getLeftOperand() and
@@ -802,7 +806,7 @@ module ControlFlow {
         cfe = any(LogicalOrExpr loe |
             // Left operand exits with a true completion
             result = loe.getLeftOperand() and
-            c = TRec(TLastRecSpecificCompletion(any(TrueCompletion tc)))
+            c = specificBoolean(true)
             or
             // Left operand exits abnormally
             result = loe.getLeftOperand() and
@@ -887,7 +891,7 @@ module ControlFlow {
         cfe = any(IfStmt is |
             // Condition exits with a false completion and there is no `else` branch
             result = is.getCondition() and
-            c = TRec(TLastRecSpecificCompletion(any(FalseCompletion fc))) and
+            c = specificBoolean(false) and
             not exists(is.getElse())
             or
             // Condition exits abnormally
@@ -936,7 +940,7 @@ module ControlFlow {
               c = TRec(TLastRecSpecificNegCompletion(any(MatchingCompletion mc | mc.isMatch())))
               or
               result = cs.getCondition() and
-              c = TRec(TLastRecSpecificCompletion(any(FalseCompletion fc)))
+              c = specificBoolean(false)
             )
             or
             // Last statement exits with any non-break completion
@@ -966,7 +970,7 @@ module ControlFlow {
         cfe = any(Case case |
             // Condition exists with a `false` completion
             result = case.getCondition() and
-            c = TRec(TLastRecSpecificCompletion(any(FalseCompletion fc)))
+            c = specificBoolean(false)
             or
             // Condition exists abnormally
             result = case.getCondition() and
@@ -987,7 +991,7 @@ module ControlFlow {
         |
           // Condition exits with a false completion
           result = ls.getCondition() and
-          c = TRec(TLastRecSpecificCompletion(any(FalseCompletion fc)))
+          c = specificBoolean(false)
           or
           // Condition exits abnormally
           result = ls.getCondition() and
@@ -1046,7 +1050,7 @@ module ControlFlow {
               or
               // Incompatible filter
               result = scc.getFilterClause() and
-              c = TRec(TLastRecSpecificCompletion(any(FalseCompletion fc)))
+              c = specificBoolean(false)
             )
           )
         or