Dataflow: fall through never happens in switch rules. (#4984)

checker/tests/nullness/java17/NullnessSwitchArrows.java

@@ -36,8 +36,6 @@ void method2() {
       default -> throw new IllegalStateException("Invalid day: " + day);
     }
 
-    // TODO: this is a false positive.  It works for case: statements; see below.
-    // :: error: (dereference.of.nullable)
     o.toString();
   }
 

checker/tests/nullness/java17/NullnessSwitchStatementRules.java

@@ -0,0 +1,43 @@
+// @below-java17-jdk-skip-test
+import org.checkerframework.checker.nullness.qual.Nullable;
+
+public class NullnessSwitchStatementRules {
+  @Nullable Object field = null;
+
+  void method(int selector) {
+    field = new Object();
+    switch (selector) {
+      case 1 -> field = null;
+      case 2 -> field.toString();
+    }
+
+    field = new Object();
+    switch (selector) {
+      case 1 -> {
+        field = null;
+      }
+      case 2 -> {
+        field.toString();
+      }
+    }
+
+    field = new Object();
+    switch (selector) {
+      case 1 -> {
+        field = null;
+      }
+      case 2 -> {
+        field.toString();
+      }
+    }
+
+    field = new Object();
+    switch (selector) {
+      case 1:
+        field = null;
+      case 2:
+        // :: error: (dereference.of.nullable)
+        field.toString();
+    }
+  }
+}

dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java

@@ -2342,18 +2342,25 @@ private void buildCase(CaseTree tree, int index) {
       }
       addLabelForNextNode(thisBodyL);
       if (tree.getStatements() != null) {
+        // This is a switch labeled statement groups.
         for (StatementTree stmt : tree.getStatements()) {
           scan(stmt, null);
         }
+        // Handle possible fall through by adding jump to next body.
+        extendWithExtendedNode(new UnconditionalJump(nextBodyL));
       } else {
+        // This is a switch rule.
         Tree bodyTree = TreeUtils.caseTreeGetBody(tree);
         if (switchTree.getKind() != Tree.Kind.SWITCH && bodyTree instanceof ExpressionTree) {
           buildSwitchExpressionResult((ExpressionTree) bodyTree);
         } else {
           scan(bodyTree, null);
+          // Switch rules never fall through so add jump to the break target.
+          assert breakTargetL != null : "no target for case statement";
+          extendWithExtendedNode(new UnconditionalJump(breakTargetL.accessLabel()));
         }
       }
-      extendWithExtendedNode(new UnconditionalJump(nextBodyL));
+
       addLabelForNextNode(nextCaseL);
     }
 
@@ -2388,8 +2395,8 @@ void buildSwitchExpressionResult(ExpressionTree resultExpression) {
           new AssignmentNode(assign, switchExprVarUseNode, resultExprNode);
       assignmentNode.setInSource(false);
       extendWithNode(assignmentNode);
-
-      assert breakTargetL != null : "no target for yield statement";
+      // Switch rules never fall through so add jump to the break target.
+      assert breakTargetL != null : "no target for case statement";
       extendWithExtendedNode(new UnconditionalJump(breakTargetL.accessLabel()));
     }
   }

framework/tests/value/java17/MultiCaseConst.java

@@ -28,4 +28,18 @@ void method2(int selector) {
         @IntVal({1, 2, 3, 4, 5}) int tmp3 = selector;
     }
   }
+
+  void method3(int selector) {
+    switch (selector) {
+      case 1 -> {
+        // :: error: (assignment)
+        @IntVal(0) int o = selector;
+        @IntVal({1, 2, 3}) int tmp = selector;
+      }
+      case 4, 5 -> {
+        @IntVal({4, 5}) int tmp2 = selector;
+        @IntVal({1, 2, 3, 4, 5}) int tmp3 = selector;
+      }
+    }
+  }
 }

framework/tests/value/java17/ValueSwitchStatementRules.java

@@ -0,0 +1,29 @@
+// @below-java17-jdk-skip-test
+import org.checkerframework.common.value.qual.IntVal;
+
+public class ValueSwitchStatementRules {
+  private int field;
+
+  void method(int selector) {
+    field = 300;
+    switch (selector) {
+      case 1:
+        field = 42;
+        @IntVal(42) int copyField = field;
+      case 2:
+        // :: error: (assignment)
+        @IntVal(300) int copyField2 = field;
+    }
+
+    field = 300;
+    switch (selector) {
+      case 1 -> {
+        field = 42;
+        @IntVal(42) int copyField = field;
+      }
+      case 2 -> {
+        @IntVal(300) int copyField = field;
+      }
+    }
+  }
+}