Dereference of nullable record component after checking for null

[xeals]

Given

import org.checkerframework.checker.nullness.qual.Nullable;

class Test {
  void main() {
    checkEmpty(new Foo(""));
  }

  void checkEmpty(Foo foo) {
    if (foo.bar() != null && !foo.bar().isEmpty()) {
      System.out.println("ok");
    }
  }

  record Foo(@Nullable String bar) {}
}

Using Checker Framework v3.22.2, Java 17, and the nullness checker, I get:

java: [dereference.of.nullable] dereference of possibly-null reference foo.bar()

Expectations

Record components are implicitly final, so the value of bar() is consistent across invocations. The checker should be able to infer this.

While the issue arises due to treatment of record components as methods, the typical behaviour is similar to accessing a final field, which behaves as one would expect. The exception is where components are overridden, where a developer may introduce impure or external effects.

Alternatives

Multiple workarounds already exist:

• Assigning foo.bar() to a variable:

String f = foo.bar();
if (f != null && !f.isEmpty()) {
// ...

• Overriding bar() to annotate it as @Pure:

record Foo(@Nullable String bar) {
  @Override
  @Pure
  public @Nullable String bar() {
    return bar;
  }
}