Implement new Java 21 features in dataflow

build.gradle

@@ -201,6 +201,12 @@ allprojects {
       doNotFormat += ['**/java17/', '**/*record*/']
     }
 
+    // As of 2023-09-24, google-java-format cannot parse Java 21 language features.
+    // See https://github.com/google/google-java-format/releases.
+    if (true) {
+      doNotFormat += ['**/java21/']
+    }
+
     if (!isJava21orHigher) {
       doNotFormat += ['**/java21/']
     }

checker/src/main/java/org/checkerframework/checker/fenum/FenumAnnotatedTypeFactory.java

@@ -75,7 +75,11 @@ protected Set<Class<? extends Annotation>> createSupportedTypeQualifiers() {
       if (!Signatures.isBinaryName(qualName)) {
         throw new UserError("Malformed qualifier \"%s\" in -Aquals", qualName);
       }
-      qualSet.add(loader.loadExternalAnnotationClass(qualName));
+      Class<? extends Annotation> annoClass = loader.loadExternalAnnotationClass(qualName);
+      if (annoClass == null) {
+        throw new UserError("Cannot load qualifier \"%s\" in -Aquals", qualName);
+      }
+      qualSet.add(annoClass);
     }
 
     // load directories of qualifiers

checker/src/main/java/org/checkerframework/checker/interning/InterningVisitor.java

@@ -209,6 +209,7 @@ public Void visitBinary(BinaryTree tree, Void p) {
   public Void visitMethodInvocation(MethodInvocationTree tree, Void p) {
     if (isInvocationOfEquals(tree)) {
       AnnotatedTypeMirror receiverType = atypeFactory.getReceiverType(tree);
+      assert receiverType != null : "@AssumeAssertion(nullness)";
       AnnotatedTypeMirror comp = atypeFactory.getAnnotatedType(tree.getArguments().get(0));
 
       if (this.checker.getLintOption("dotequals", true)

checker/src/main/java/org/checkerframework/checker/nullness/NullnessVisitor.java

@@ -419,14 +419,16 @@ public Void visitIf(IfTree tree, Void p) {
   public Void visitInstanceOf(InstanceOfTree tree, Void p) {
     // The "reference type" is the type after "instanceof".
     Tree refTypeTree = tree.getType();
-    if (refTypeTree.getKind() == Tree.Kind.ANNOTATED_TYPE) {
-      List<? extends AnnotationMirror> annotations =
-          TreeUtils.annotationsFromTree((AnnotatedTypeTree) refTypeTree);
-      if (AnnotationUtils.containsSame(annotations, NULLABLE)) {
-        checker.reportError(tree, "instanceof.nullable");
-      }
-      if (AnnotationUtils.containsSame(annotations, NONNULL)) {
-        checker.reportWarning(tree, "instanceof.nonnull.redundant");
+    if (refTypeTree != null) {
+      if (refTypeTree.getKind() == Tree.Kind.ANNOTATED_TYPE) {
+        List<? extends AnnotationMirror> annotations =
+            TreeUtils.annotationsFromTree((AnnotatedTypeTree) refTypeTree);
+        if (AnnotationUtils.containsSame(annotations, NULLABLE)) {
+          checker.reportError(tree, "instanceof.nullable");
+        }
+        if (AnnotationUtils.containsSame(annotations, NONNULL)) {
+          checker.reportWarning(tree, "instanceof.nonnull.redundant");
+        }
       }
     }
     // Don't call super because it will issue an incorrect instanceof.unsafe warning.

checker/tests/nullness/java17/SwitchTestIssue5412.java

@@ -30,9 +30,9 @@ public String foo1a(MyEnum b) {
             // The default case is dead code, so it would be possible for type-checking
             // to skip it and not issue this warning.  But giving the warning is also
             // good.
-            // :: error: (switch.expression)
           default -> null;
         };
+    // :: error: (return)
     return s;
   }
 

checker/tests/nullness/java21/FlowSwitch.java

@@ -0,0 +1,83 @@
+// @below-java21-jdk-skip-test
+// @infer-jaifs-skip-test
+// @infer-ajava-skip-test
+// @infer-stubs-skip-test
+
+public class FlowSwitch {
+
+  void test1(Integer i) {
+    String msg = null;
+    switch (i) {
+      case -1, 1:
+        msg = "-1 or 1";
+        break;
+      case Integer j when j > 0:
+        msg = "pos";
+        break;
+      case Integer j:
+        msg = "everything else";
+        break;
+    }
+    msg.toString();
+  }
+
+  void test2(Integer i) {
+    String msg = null;
+    switch (i) {
+      case -1, 1:
+        msg = "-1 or 1";
+        break;
+      default:
+        msg = "everythingything else";
+        break;
+      case 2:
+        msg = "pos";
+        break;
+    }
+  }
+
+  class A {}
+
+  class B extends A {}
+
+  sealed interface I permits C, D {}
+
+  final class C implements I {}
+
+  final class D implements I {}
+
+  record Pair<T>(T x, T y) {}
+
+  void testE(Pair<A> p1) {
+    B e = switch (p1) {
+      case Pair<A>(A a, B b) -> b;
+      case Pair<A>(B b, A a) -> b;
+      default -> null;
+    };
+    B e2 = null;
+    switch (p1) {
+      case Pair<A>(A a, B b) -> e2 = b;
+      case Pair<A>(B b, A a) -> e2 = b;
+      default -> e2 = new B();
+    }
+    e2.toString();
+  }
+
+  void test3(Pair<I> p2) {
+    String s = null;
+    I e = null;
+    switch (p2) {
+      case Pair<I>(I i, C c) -> {e = c; s="";}
+      case Pair<I>(I i, D d) -> {e = d; s="";}
+    }
+    s.toString();
+    e.toString();
+
+    I e2 = null;
+    switch (p2) {
+      case Pair<I>(C c, I i) -> e2 = c;
+      case Pair<I>(D d, C c) -> e2 = d;
+      case Pair<I>(D d1, D d2) -> e2 = d2;
+    }
+  }
+}

checker/tests/nullness/java21/SimpleCaseGuard.java

@@ -0,0 +1,29 @@
+// @below-java21-jdk-skip-test
+// @infer-jaifs-skip-test
+// @infer-ajava-skip-test
+// @infer-stubs-skip-test
+
+import org.checkerframework.checker.nullness.qual.NonNull;
+import org.checkerframework.checker.nullness.qual.Nullable;
+
+public class SimpleCaseGuard {
+
+  @Nullable String field;
+
+  void test2(Object obj, boolean b) {
+    switch (obj) {
+      case String s when field != null -> {
+        @NonNull String z = field;
+      }
+      case String s -> {
+        // :: error: (assignment)
+        @NonNull String z = field;
+      }
+      default -> {
+        // :: error: (assignment)
+        @NonNull String z = field;
+      }
+    }
+  }
+
+}

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

@@ -46,6 +46,7 @@
 import com.sun.source.tree.SynchronizedTree;
 import com.sun.source.tree.ThrowTree;
 import com.sun.source.tree.Tree;
+import com.sun.source.tree.Tree.Kind;
 import com.sun.source.tree.TryTree;
 import com.sun.source.tree.TypeCastTree;
 import com.sun.source.tree.TypeParameterTree;
@@ -104,6 +105,7 @@
 import org.checkerframework.dataflow.cfg.node.ConditionalAndNode;
 import org.checkerframework.dataflow.cfg.node.ConditionalNotNode;
 import org.checkerframework.dataflow.cfg.node.ConditionalOrNode;
+import org.checkerframework.dataflow.cfg.node.DeconstructorPatternNode;
 import org.checkerframework.dataflow.cfg.node.DoubleLiteralNode;
 import org.checkerframework.dataflow.cfg.node.EqualToNode;
 import org.checkerframework.dataflow.cfg.node.ExplicitThisNode;
@@ -548,6 +550,8 @@ public Node scan(Tree tree, Void p) {
             return visitSwitchExpression17(tree, p);
           case "YIELD":
             return visitYield17(tree, p);
+          case "DECONSTRUCTION_PATTERN":
+            return visitDeconstructionPattern21(tree, p);
           default:
             // fall through to generic behavior
         }
@@ -606,6 +610,26 @@ public Node visitBindingPattern17(Tree bindingPatternTree, Void p) {
     return varNode;
   }
 
+  /**
+   * Visit a DeconstructionPatternTree.
+   *
+   * @param deconstructionPatternTree a DeconstructionPatternTree, typed as Tree so the Checker
+   *     Framework compiles under JDK < 21
+   * @param p an unused parameter
+   * @return the result of visiting the tree
+   */
+  public Node visitDeconstructionPattern21(Tree deconstructionPatternTree, Void p) {
+    List<? extends Tree> nestedPatternTrees =
+        TreeUtils.deconstructionPatternTreeGetNestedPatterns(deconstructionPatternTree);
+    List<Node> nestedPatterns = new ArrayList<>(nestedPatternTrees.size());
+    for (Tree pattern : nestedPatternTrees) {
+      nestedPatterns.add(scan(pattern, p));
+    }
+
+    return new DeconstructorPatternNode(
+        TreeUtils.typeOf(deconstructionPatternTree), deconstructionPatternTree, nestedPatterns);
+  }
+
   /* --------------------------------------------------------- */
   /* Nodes and Labels Management */
   /* --------------------------------------------------------- */
@@ -2327,6 +2351,7 @@ private SwitchBuilder(Tree switchTree) {
 
       // Build CFG for the cases.
       int defaultIndex = -1;
+      boolean exhaustiveAndNoDefault = exhaustiveAndNoDefault();
       for (int i = 0; i < numCases; ++i) {
         CaseTree caseTree = caseTrees.get(i);
         if (TreeUtils.isDefaultCaseTree(caseTree)) {
@@ -2338,10 +2363,7 @@ private SwitchBuilder(Tree switchTree) {
           boolean isLastCaseExceptDefault =
               i == numCases - 1
                   || (i == numCases - 2 && TreeUtils.isDefaultCaseTree(caseTrees.get(i + 1)));
-          // This can be extended to handle case statements as well as case rules.
-          boolean noFallthroughToHere = TreeUtils.isCaseRule(caseTree);
-          boolean isLastCaseOfExhaustive =
-              isLastCaseExceptDefault && casesAreExhaustive() && noFallthroughToHere;
+          boolean isLastCaseOfExhaustive = isLastCaseExceptDefault && exhaustiveAndNoDefault;
           buildCase(caseTree, i, isLastCaseOfExhaustive);
         }
       }
@@ -2461,10 +2483,15 @@ private void buildCase(CaseTree caseTree, int index, boolean isLastCaseOfExhaust
       if (!isTerminalCase) {
         // A case expression exists, and it needs to be tested.
         ArrayList<Node> exprs = new ArrayList<>();
-        for (ExpressionTree exprTree : TreeUtils.caseTreeGetExpressions(caseTree)) {
+        for (Tree exprTree : TreeUtils.caseTreeGetLabels(caseTree)) {
           exprs.add(scan(exprTree, null));
         }
-        CaseNode test = new CaseNode(caseTree, selectorExprAssignment, exprs, env.getTypeUtils());
+
+        ExpressionTree guardTree = TreeUtils.caseTreeGetGuard(caseTree);
+        Node guard = (guardTree == null) ? null : scan(guardTree, null);
+
+        CaseNode test =
+            new CaseNode(caseTree, selectorExprAssignment, exprs, guard, env.getTypeUtils());
         extendWithNode(test);
         extendWithExtendedNode(new ConditionalJump(thisBodyLabel, nextCaseLabel));
       }
@@ -2540,39 +2567,52 @@ private void buildCase(CaseTree caseTree, int index, boolean isLastCaseOfExhaust
     }
 
     /**
-     * Returns true if the cases are exhaustive -- exactly one is executed. There might or might not
-     * be a `default` case label; if there is, it is never used.
+     * Returns true if the switch is exhaustive and does not contain a default case.
      *
-     * @return true if the cases are exhaustive
+     * @return true if the switch is exhaustive and does not contain a default case
      */
-    private boolean casesAreExhaustive() {
-      TypeMirror selectorTypeMirror = TreeUtils.typeOf(selectorExprTree);
+    private boolean exhaustiveAndNoDefault() {
+      for (CaseTree caseTree : caseTrees) {
+        if (TreeUtils.isDefaultCaseTree(caseTree)) {
+          return false;
+        }
+      }
 
-      switch (selectorTypeMirror.getKind()) {
-        case BOOLEAN:
-          // TODO
-          break;
-        case DECLARED:
-          DeclaredType declaredType = (DeclaredType) selectorTypeMirror;
-          TypeElement declaredTypeElement = (TypeElement) declaredType.asElement();
-          if (declaredTypeElement.getKind() == ElementKind.ENUM) {
-            // It's an enumerated type.
-            List<VariableElement> enumConstants =
-                ElementUtils.getEnumConstants(declaredTypeElement);
-            List<Name> caseLabels = new ArrayList<>(enumConstants.size());
-            for (CaseTree caseTree : caseTrees) {
-              for (ExpressionTree caseEnumConstant : TreeUtils.caseTreeGetExpressions(caseTree)) {
-                caseLabels.add(((IdentifierTree) caseEnumConstant).getName());
-              }
-            }
-            // Could also check that the values match.
-            boolean result = enumConstants.size() == caseLabels.size();
-            return result;
+      // There is no default case.  Check whether the switch is exhaustive.
+
+      // Switch expressions are always exhaustive, but they might have a default case, which is why
+      // the above loop is not fused with the below loop.
+      if (!TreeUtils.isSwitchStatement(switchTree)) {
+        return true;
+      }
+
+      int enumCaseLabels = 0;
+      for (CaseTree caseTree : caseTrees) {
+        for (Tree caseLabel : TreeUtils.caseTreeGetLabels(caseTree)) {
+          // Java guarantees that if one of the cases is the null literal, the switch is exhaustive.
+          // Also if certain other constructs exist.
+          if (caseLabel.getKind() == Kind.NULL_LITERAL
+              || TreeUtils.isBindingPatternTree(caseLabel)
+              || TreeUtils.isDeconstructionPatternTree(caseLabel)) {
+            return true;
           }
-          break;
-        default:
-          break;
+          if (caseLabel.getKind() == Kind.IDENTIFIER) {
+            enumCaseLabels++;
+          }
+        }
       }
+
+      TypeMirror selectorTypeMirror = TreeUtils.typeOf(selectorExprTree);
+      if (selectorTypeMirror.getKind() == TypeKind.DECLARED) {
+        DeclaredType declaredType = (DeclaredType) selectorTypeMirror;
+        TypeElement declaredTypeElement = (TypeElement) declaredType.asElement();
+        if (declaredTypeElement.getKind() == ElementKind.ENUM) {
+          // The switch expression's type is an enumerated type.
+          List<VariableElement> enumConstants = ElementUtils.getEnumConstants(declaredTypeElement);
+          return enumConstants.size() == enumCaseLabels;
+        }
+      }
+
       return false;
     }
   }
@@ -3798,12 +3838,14 @@ public Node visitTypeParameter(TypeParameterTree tree, Void p) {
   public Node visitInstanceOf(InstanceOfTree tree, Void p) {
     InstanceOfNode instanceOfNode;
     Node operand = scan(tree.getExpression(), p);
-    TypeMirror refType = TreeUtils.typeOf(tree.getType());
-    Tree binding = TreeUtils.instanceOfTreeGetPattern(tree);
-    LocalVariableNode bindingNode =
-        (LocalVariableNode) ((binding == null) ? null : scan(binding, p));
-
-    instanceOfNode = new InstanceOfNode(tree, operand, bindingNode, refType, types);
+    Tree patternTree = TreeUtils.instanceOfTreeGetPattern(tree);
+    if (patternTree != null) {
+      Node pattern = scan(patternTree, p);
+      instanceOfNode = new InstanceOfNode(tree, operand, pattern, pattern.getType(), types);
+    } else {
+      TypeMirror refType = TreeUtils.typeOf(tree.getType());
+      instanceOfNode = new InstanceOfNode(tree, operand, refType, types);
+    }
     extendWithNode(instanceOfNode);
     return instanceOfNode;
   }

dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/AbstractNodeVisitor.java

@@ -384,4 +384,9 @@ public R visitMarker(MarkerNode n, P p) {
   public R visitExpressionStatement(ExpressionStatementNode n, P p) {
     return visitNode(n, p);
   }
+
+  @Override
+  public R visitDeconstructorPattern(DeconstructorPatternNode n, P p) {
+    return visitNode(n, p);
+  }
 }