In Java 21, case labels can be null.

[smillst]

Fixes #6173.

[mernst]

This looks suspicious to me. One of the labels could be null, in which case I think casesAreExhaustive should return false. Could you write a test to assuage my concern? Thanks.

[smillst]

Oh good catch. I don't know how to write a test case that would have caught this bug, because I can't see how a checker would behave differently when the cases are not exhaustive.

[mernst]

Could a test be something like:

x = null;
switch (*) {
  case a: x = nonnull; break;
  case b: x = nonnull; break;
  ...
}
x.toString();

The key is to know whether fallthrough is possible.

[mernst]

On the line below, now that "null" is a possible value, I think that the cases are exhaustive only if they also include "null". Otherwise, fallthrough is possible.

[smillst]

null doesn't have to appear for the switch block to be exhaustive. If a case null does not appear and null is the value of the switch selector expressions, then a NPE is thrown.

Here's the definition of exhaustive switch blocks: https://docs.oracle.com/javase/specs/jls/se20/preview/specs/patterns-switch-record-patterns-jls.html#jls-14.11.1.1.

[smillst]

Could a test be something like:

x = null;
switch (*) {
  case a: x = nonnull; break;
  case b: x = nonnull; break;
  ...
}
x.toString();

The key is to know whether fallthrough is possible.

I read the JLS, and if case null appears then the switch must be exhaustive. (And now fall through can happen.) So no such test case exists. See:
https://docs.oracle.com/javase/specs/jls/se20/preview/specs/patterns-switch-record-patterns-jls.html#jls-14.11.2

[smillst]

We may just want to hold off on merging this pull request until we have implement support for Pattern Matching for switch and Record Patterns https://openjdk.org/jeps/440). There are more test cases that crash.

[msridhar]

We may just want to hold off on merging this pull request until we have implement support for Pattern Matching for switch and Record Patterns https://openjdk.org/jeps/440). There are more test cases that crash.

Just curious, are the crashes in the dataflow library or elsewhere? From the NullAway perspective, it'd be cool if we could test out a version of dataflow with crashes fixed before all the checkers fully support these constructs. But I agree it might be best to consolidate fixes for related issues.

[smillst]

We may just want to hold off on merging this pull request until we have implement support for Pattern Matching for switch and Record Patterns https://openjdk.org/jeps/440). There are more test cases that crash.

Just curious, are the crashes in the dataflow library or elsewhere? From the NullAway perspective, it'd be cool if we could test out a version of dataflow with crashes fixed before all the checkers fully support these constructs. But I agree it might be best to consolidate fixes for related issues.

I tried this test case (copied from https://openjdk.org/jeps/441):

  static String formatterPatternSwitch(Object obj) {
    return switch (obj) {
      case Integer i -> String.format("int %d", i);
      case Long l    -> String.format("long %d", l);
      case Double d  -> String.format("double %f", d);
      case String s  -> String.format("String %s", s);
      default        -> obj.toString();
    };
  }

The crash is not in dataflow, but the crash is because dataflow does not have a node for i in String.format("int %d", i);.

 Exception: java.lang.NullPointerException: Cannot invoke "java.util.Set.iterator()" because "nodes" is null; java.lang.NullPointerException: Cannot invoke "java.util.Set.iterator()" because "nodes" is null
  	at org.checkerframework.framework.type.GenericAnnotatedTypeFactory.getFirstNodeOfKindForTree(GenericAnnotatedTypeFactory.java:1291)
  	at org.checkerframework.framework.type.GenericAnnotatedTypeFactory.getAnnotatedTypeVarargsArray(GenericAnnotatedTypeFactory.java:1729)
  	at org.checkerframework.common.basetype.BaseTypeVisitor.checkVarargs(BaseTypeVisitor.java:1897)
  	at org.checkerframework.common.basetype.BaseTypeVisitor.visitMethodInvocation(BaseTypeVisitor.java:1782)
  	at org.checkerframework.common.basetype.BaseTypeVisitor.visitMethodInvocation(BaseTypeVisitor.java:184)

[msridhar]

Ah, makes sense. I can see how fixing that issue might be intertwined with fixing the crash.

[mernst]

@smillst CI is failing

[smillst]

From the NullAway perspective, it'd be cool if we could test out a version of dataflow with crashes fixed before all the checkers fully support these constructs.

@msridhar I'm going to close this pull request because this in not the correct implementation for case null. I'm going to work on implementing the new Java 21 language features now. The first step (and pull request) will be a version where the checkers (and therefore dataflow) don't crash on the new language features. At that point, you can use dataflow with the new features. Then, I'll work on making sure the checkers soundly handle the new features.

[msridhar]

Thanks @smillst!