Support records

[michaelhixson]

Add support for JEP 359: Records (Preview) to the Checker Framework.

Records are a preview feature in Java 14. Java 14 is currently in early access and will be ready for general use in March 2020. The earliest that records could become a non-preview feature in a non-early-access release is in September 2020 with Java 15, but no commitment has been made to target that release yet.

What's a record?

Records are a new kind of class.

record Foo(String a, @Nullable String b) {}

That code essentially translates to this:

final class Foo extends java.lang.Record {
  private final String a;
  private final @Nullable String b;

  public Foo(String a, @Nullable String b) {
    this.a = a;
    this.b = b;
  }

  public String a() { return a; }
  public @Nullable String b() { return b; }

  // equals, hashCode, and toString based on the fields
}

They introduce one new tree kind, Tree.Kind.RECORD, which may be returned from ClassTree#getKind(). Fortunately they don't introduce a new subclass of Tree or any new methods to TreeVisitor.

They introduce two new element kinds, ElementKind.RECORD and ElementKind.RECORD_COMPONENT.

They introduce one new annotation element type, ElementType.RECORD_COMPONENT.

What's involved in supporting records?

There are a handful of switch statements in the Checker Framework that need to be modified. They do the wrong thing when encountering one of the new record-related enum constants.

That is, there's a bunch of code like this:

switch (kind) {
  case CLASS:
  case ENUM:
  case INTERFACE:
  case ANNOTATION_TYPE:
    // handle class-like constructs
    return ...
  default:
    // records currently handled by this case
    throw new BugInCF( ... );

Currently, those throw statements mean that I can't use Checker Framework or the tools that depend on it (NullAway and Error Prone) if my code contains records.

I think reasonable support can be added without breaking Java 8/11 compatibility. Locally I'm trying an approach where I modify the default case for all those switch statements.

switch (kind) {
  case CLASS:
  case ENUM:
  case INTERFACE:
  case ANNOTATION_TYPE:
    // handle class-like constructs
    return ...
  default:
    if (kind.name().equals("RECORD")) {
      // repeat the logic for class-like constructs
      return ...
    }
    throw new BugInCF( ... );

With 20 or so small changes like that, my local copy of Checker Framework + NullAway + Error Prone is giving me useful feedback about the records in my project. That is, for a record like my earlier example...

record Foo(String a, @Nullable String b) {}

...I see compile-time errors when I handle nulls incorrectly.

Foo x = new Foo(null, ""); // error because `a` is non-null
Foo y = new Foo("", null); // ok
System.out.println(y.a().length()); // ok
System.out.println(y.b().length()); // error because `b` is nullable

That's a win in my book already.

Full support for records may involve more extensive changes. Since I'm only using Checker Framework indirectly through NullAway and Error Prone, I don't have a good perspective on what "full support" really means here.

[mernst]

Thanks for this suggestion. We prioritize non-preview features in LTS versions of Java, but we try to support other features when possible. As you noted, it is important that we not break support for Java 8 or Java 11. Using kind.name().equals("RECORD") is a good idea -- we ordinarily hate string comparisons, but this is a way to avoid depending on JDK 14 features so that the Checker Framework code will still compile and run in earlier JDKs.

You said you had a set of changes that make the Checker Framework support records. Can you please prepare a pull request for the Checker Framework? Thanks!

[wmdietl]

@michaelhixson Thanks for raising this issue!

Instead of performing the string comparison, I think it would be better to rewrite the switch statements to:

if (kind.isClass() || kind.isInterface()) {

The implementation of isClass handles RECORD for us, so we wouldn't need any special version-specific handling.

I'm not sure whether this will be possible for all cases, but it would be good to try that.

In contrast to #2373 we'll hopefully be able to handle this without a preprocessor.

[michaelhixson]

You said you had a set of changes that make the Checker Framework support records. Can you please prepare a pull request for the Checker Framework? Thanks!

Ok, I opened #3017.

The implementation of isClass handles RECORD for us

Good call. I incorporated this into the PR.

[kenwang-coursera]

This looks awesome! Any updates on this by any chance? Last update was almost a year ago.

[mernst]

@kenwang-coursera #3017 added baseline support for records. It didn't add tests, though. :-(

Could you please try running the Checker Framework on code that uses records? We would appreciate it if you could open a new issue if there is specific behavior that does not work for you. Thanks!

[linusjf]

When will support for Java 14 be available?

[mernst]

When will support for Java 14 be available?

Not even Oracle supports Java 14 -- they dropped support for it in September 2020. As noted above, "we prioritize non-preview features in LTS versions of Java, but we try to support other features when possible" (especially when the community contributes pull requests).

Pull request #3017 (baseline support for records) was already merged.

Do you have a specific code example that the Checker Framework does not support?

[linusjf]

No.
My mistake. I was under the impression that LTS was available every three releases.

Apparently not.

[mernst]

Closing the issue, since records are supported since #3017 in December 2019.