Unsoundness in Nullness Checker with record patterns

[msridhar]

Test:

import org.checkerframework.checker.nullness.qual.Nullable;
public class Test {
  sealed interface IntOrBool {}
  public record WrappedInt(Integer a) implements IntOrBool {}
  public record WrappedBoolean(@Nullable Boolean b) implements IntOrBool {}
  public static void test(IntOrBool i) {
    switch (i) {
      case WrappedInt(Integer x) -> {
      }
      case WrappedBoolean(Boolean y) -> {
        y.hashCode();
      }
    }
  }
  public static void main(String[] args) {
    test(new WrappedBoolean(null));
  }
}

We get an NPE at runtime but it's not detected by the nullness checker. If we write case WrappedBoolean(@Nullable Boolean y) an error is reported as expected. Record patterns were finalized in Java 21; not sure if that version is officially supported by the Checker Framework yet.

[msridhar]

Thinking more, assuming that in the above example y shows up as a local variable in the CFG, a possible fix would be to generate a synthetic assignment y = i.getB();. That should lead local type inference to figure out that y should be @Nullable. Also I like this fix because it'll probably work for NullAway too 🙂