JSpecify 0.3.0, Checker Framework nullness, and avaje-record-builder in Maven

[commonquail]

Or, propagating TYPE_USE annotations (#19) is insufficient.

Or, builders are really validators.

---

I've been fooling around with nullability analysis to get a sense of the state of the ecosystem primo 2024. For this experiment I'm using

• Maven, because JetBrains claims 60% of Java projects use Maven and because I hate it less than Gradle.
• Checker Framework's nullness checker, because it's well established, can run without a third-party host, and NullAway depends on it anyway.
• JSpecify, because it's ~the only general TYPE_USE nullability annotation library and it specifically lacks certain tool specific support.
• avaje-record-builder, because avaje-record-builder has some recognition of TYPE_USE annotations, and anyway, because I suspect any dialogue about the state of third-party nullability analysis in combination with a record builder generator has a better chance of being fruitful here no matter the outcome.

I'm filing this issue for posterity to record that this combination of tools presently is not workable. The essence of why is the same as the essence of uber/NullAway#121, the outcome of which is not clear to me. I am aware of the extensive history represented by #19 and Randgalt/record-builder#111.

There are variations I have not experimented with much or at all and so cannot really comment on:

• Checker Framework standalone execution, which offers flexible control of what to analyse when and possibly trivially allows for ignoring problematic elements like generated code.
• Checker Framework via Gradle, but I get the sense that Checker Framework pushes Gradle hard and that the Gradle integration is richer than the Maven integration.
• NullAway, which itself is much laxer than Checker Framework, and via Error Prone offers flexible analysis inclusion and exclusion rules even in Maven integration.
• io.soabase.record-builder:record-builder:38, which is unable to recognize TYPE_USE annotations.

Given a record

package example; // avaje/avaje-record-builder#41

@io.avaje.recordbuilder.RecordBuilder
public record Nullity(
        @org.jspecify.annotations.NonNull String a,
        @org.jspecify.annotations.Nullable String b) {}

avaje-record-builder-1.0 generates the moral equivalent of

package example;

import io.avaje.recordbuilder.Generated;
import java.util.function.Consumer;
import org.jspecify.annotations.NonNull;
import org.jspecify.annotations.Nullable;

@Generated("avaje-record-builder")
public class NullityBuilder {
  private String a;
  private String b;

  private NullityBuilder() {} // initialization.fields.uninitialized

  private NullityBuilder(@NonNull String a, @Nullable String b) {
    this.a = a;
    this.b = b; // assignment
  }

  public static NullityBuilder builder() { return new NullityBuilder(); }

  public static NullityBuilder builder(Nullity from) { return new NullityBuilder(from.a(), from.b()); }

  public Nullity build() { return new Nullity(a, b); }

  public NullityBuilder a(@NonNull String a) {
      this.a = a;
      return this;
  }

  public NullityBuilder b(@Nullable String b) {
      this.b = b; // assignment
      return this;
  }
}

When compiled (POM below), Checker Framework produces three errors:

[ERROR] /.../src/avaje-record-builder-nullity/target/generated-sources/annotations/example/NullityBuilder.java:[14,10] error: [initialization.fields.uninitialized] the constructor does not initialize fields: a, b
[ERROR] /.../src/avaje-record-builder-nullity/target/generated-sources/annotations/example/NullityBuilder.java:[19,13] error: [assignment] incompatible types in assignment.
  found   : @Initialized @Nullable String
  required: @Initialized @NonNull String
[ERROR] /.../src/avaje-record-builder-nullity/target/generated-sources/annotations/example/NullityBuilder.java:[51,15] error: [assignment] incompatible types in assignment.
  found   : @Initialized @Nullable String
  required: @Initialized @NonNull String

The line numbers refer to the canonical generated lines, not the compressed version shown above. The compressed version is annotated with the error codes.

There are two errors in the generated code, one "obvious" and one subtle. Other limitations in Checker Framework, Checker Framework's Maven integration, and avaje-record-builder combine to make those two errors somewhere between difficult and impossible to work around (I have not found a way).

1. assignment: Although the NullityBuilder b(@Nullable String b) receiver correctly had org.jspecify.annotations.Nullable propagated from the Nullity.b component the annotation was not propagated to the NullityBuilder.b field, which Checker Framework consequently resolves to @NonNull. @Nullable should have been propagated all the way to the field.
   • This is the "obvious" error as far as Checker Framework's rules go.
2. initialization.fields.uninitialized: The builder() factory instantiates a builder in its default state according to the JLS, i.e. with all fields uninitialized and implicitly null. This is valid Java but Checker Framework effectively resolves those fields to @NonNull, which is a contradiction and therefore rejected. This behaviour is consistent with the various rules in play but the rules that are in play are not representative of a builder's role. The trouble is that NullityBuilder.[@o.j.a.NonNull] String a is an incorrect declaration: NullityBuilder.a must actually be the moral equivalent of @o.j.a.Nullable @javax.validation.constraints.NotNull String, comparable to Checker Framework's @org.checkerframework.checker.nullness.qual.MonotonicNonNull. This is because the builder is stateful and cannot start out in a state of NullityBuilder.a being non-null. A knock-on consequence is that the builder must validate that the values passed to the record's @NonNull components are in fact non-null. Checker Framework makes this extra difficult by rejecting Objects.requireNonNull.
   • This is the subtle error.
   • It is reasonable, and perhaps technically necessary, but not truly important, that the NullityBuilder a(@NonNull String a) receiver had the @NonNull annotation propagated. It is reasonable because passing a @Nullable value is clearly nonsensical but it is unimportant because NullityBuilder.a cannot practically be @NonNull.
   • Arguably NullityBuilder.a and all other @NonNull record components could be promoted to parameters on the builder() method. This would undermine the utility of the resulting builder, however.
   • See also https://checkerframework.org/manual/#initialization-warnings-constructor

POM:

<?xml version="1.0" encoding="UTF-8"?>
<project xmlns="http://maven.apache.org/POM/4.0.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
  <modelVersion>4.0.0</modelVersion>
  <groupId>example</groupId>
  <artifactId>avaje-record-builder-nullity</artifactId>
  <version>1.0-SNAPSHOT</version>
  <name>avaje-record-builder-nullity</name>

  <properties>
    <checker.version>3.42.0</checker.version>
    <maven-compiler-plugin.version>3.11.0</maven-compiler-plugin.version>
    <maven.compiler.release>17</maven.compiler.release>
    <record.builder.version>1.0</record.builder.version>
    <project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>
    <maven.compiler.source>17</maven.compiler.source>
    <maven.compiler.target>17</maven.compiler.target>
  </properties>

  <dependencies>
    <dependency>
      <groupId>io.avaje</groupId>
      <artifactId>avaje-record-builder</artifactId>
      <version>${record.builder.version}</version>
      <scope>provided</scope>
    </dependency>
    <dependency>
      <groupId>org.jspecify</groupId>
      <artifactId>jspecify</artifactId>
      <version>0.3.0</version>
    </dependency>
    <dependency>
      <groupId>org.checkerframework</groupId>
      <artifactId>checker</artifactId>
      <version>${checker.version}</version>
    </dependency>
    <dependency>
      <groupId>org.checkerframework</groupId>
      <artifactId>checker-qual</artifactId>
      <version>${checker.version}</version>
    </dependency>
    <dependency>
      <groupId>org.checkerframework</groupId>
      <artifactId>checker-util</artifactId>
      <version>${checker.version}</version>
    </dependency>
  </dependencies>

  <build>
    <plugins>
      <plugin>
        <groupId>org.apache.maven.plugins</groupId>
        <artifactId>maven-compiler-plugin</artifactId>
        <version>${maven-compiler-plugin.version}</version>
        <configuration>
          <compilerArgs>
          </compilerArgs>
          <annotationProcessorPaths>
            <path>
              <groupId>io.avaje</groupId>
              <artifactId>avaje-record-builder</artifactId>
              <version>${record.builder.version}</version>
            </path>
          </annotationProcessorPaths>
          <annotationProcessors>
            <annotationProcessor>io.avaje.recordbuilder.internal.RecordProcessor</annotationProcessor>
          </annotationProcessors>
        </configuration>
      </plugin>
    </plugins>
  </build>

  <profiles>
    <profile>
      <id>checkerframework</id>
      <activation>
        <jdk>[9,)</jdk>
      </activation>
      <build>
        <plugins>
          <plugin>
            <artifactId>maven-compiler-plugin</artifactId>
            <executions>
              <execution>
                <id>default-compile</id>
                <configuration>
                  <fork>true</fork>
                  <annotationProcessorPaths combine.children="append">
                    <path>
                      <groupId>org.checkerframework</groupId>
                      <artifactId>checker</artifactId>
                      <version>${checker.version}</version>
                    </path>
                  </annotationProcessorPaths>
                  <annotationProcessors combine.children="append">
                    <annotationProcessor>org.checkerframework.checker.nullness.NullnessChecker</annotationProcessor>
                  </annotationProcessors>
                  <compilerArgs combine.children="append">
                    <arg>-Xmaxerrs</arg>
                    <arg>10000</arg>
                    <arg>-Xmaxwarns</arg>
                    <arg>10000</arg>
                    <arg>-J--add-exports=jdk.compiler/com.sun.tools.javac.api=ALL-UNNAMED</arg>
                    <arg>-J--add-exports=jdk.compiler/com.sun.tools.javac.code=ALL-UNNAMED</arg>
                    <arg>-J--add-exports=jdk.compiler/com.sun.tools.javac.file=ALL-UNNAMED</arg>
                    <arg>-J--add-exports=jdk.compiler/com.sun.tools.javac.main=ALL-UNNAMED</arg>
                    <arg>-J--add-exports=jdk.compiler/com.sun.tools.javac.model=ALL-UNNAMED</arg>
                    <arg>-J--add-exports=jdk.compiler/com.sun.tools.javac.processing=ALL-UNNAMED</arg>
                    <arg>-J--add-exports=jdk.compiler/com.sun.tools.javac.tree=ALL-UNNAMED</arg>
                    <arg>-J--add-exports=jdk.compiler/com.sun.tools.javac.util=ALL-UNNAMED</arg>
                    <arg>-J--add-opens=jdk.compiler/com.sun.tools.javac.comp=ALL-UNNAMED</arg>
                  </compilerArgs>
                </configuration>
              </execution>
            </executions>
          </plugin>
        </plugins>
      </build>
    </profile>
  </profiles>

</project>

[commonquail]

For posterity, NullAway produces the logically same warnings as Checker Framework, meaning they agree on the analysis. This is a good thing, and unsurprising.

NullAway is more flexible with respect to selecting input for analysis. It can ignore classes with specific annotations, or all @Generated classes, or an entire tree like target/. The exclusion mechanism determines how much NullAway can infer. Of these three mechanisms the first one, ExcludedClassAnnotations, is most strict, and that makes it the most interesting for avaje-record-builder: NullAway will ignore the contents of the generated class but will assume its API is correctly annotated. Consequently, because avaje-record-builder propagates TYPE_USE annotations, a configuration similar to the one below, in combination with accurately annotated records, allows NullAway to compile generated builders while still flagging null values passed to non-nullable component setters.

Neither the builder nor NullAway, nor the ErrorProne harness, presently offer protection against failing to invoke the setter of a non-nullable component. That is, assert NullityBuilder.builder().build().a() == null is tolerated.

One crucial difference between Checker Framework and NullAway is their behaviour of Objects::requireNonNull. NullAway allows @NonNull T requireNonNull(@Nullable T) whereas Checker Framework defaults to @NonNull T requireNonNull(@NonNull T) (a built-in "stub" can change the parameter to @Nullable but that stub cannot be assumed to be enabled by the user). The practical effect of this is that Objects::requireNonNull cannot be used to satisfy a @o.j.a.Nullable @javax.validation.constraints.NotNull T component -- and explicit null check must be performed instead.

Editor's note: Checker Framework's treatment of Objects::requireNonNull is consistent with Checker Framework's stated goal ("guarantees lack of null pointer exceptions [...] expressions whose type is annotated with @NonNull never evaluate to null") but it is inconsistent with the JDK specification. It is improper to reject the explicit side effect of Objects::requireNonNull just because that side effect is superficially identical to the act of dereferencing a null pointer. It also burdens the user with the cumbersome work-around of locally reimplementing Objects::requireNonNull (or enabling the stub) just so Checker Framework does not fail. NullAway is clearly in the right here.

    <profile>
      <id>errorprone</id>
      <build>
        <plugins>
          <plugin>
            <artifactId>maven-compiler-plugin</artifactId>
            <configuration>
              <fork>true</fork>
              <annotationProcessorPaths combine.children="append">
                <path>
                  <groupId>com.google.errorprone</groupId>
                  <artifactId>error_prone_core</artifactId>
                  <version>2.24.1</version>
                </path>
                <path>
                  <groupId>com.uber.nullaway</groupId>
                  <artifactId>nullaway</artifactId>
                  <version>0.10.19</version>
                </path>
              </annotationProcessorPaths>
              <compilerArgs combine.children="append">
                <arg>-XDcompilePolicy=simple</arg>
                <arg>
                  -Xplugin:ErrorProne \
                  -XepOpt:NullAway:AnnotatedPackages=example \
                  -XepOpt:NullAway:ExcludedClassAnnotations=io.avaje.recordbuilder.Generated \
                </arg>
                <arg>-J--add-exports=jdk.compiler/com.sun.tools.javac.api=ALL-UNNAMED</arg>
                <arg>-J--add-exports=jdk.compiler/com.sun.tools.javac.file=ALL-UNNAMED</arg>
                <arg>-J--add-exports=jdk.compiler/com.sun.tools.javac.main=ALL-UNNAMED</arg>
                <arg>-J--add-exports=jdk.compiler/com.sun.tools.javac.model=ALL-UNNAMED</arg>
                <arg>-J--add-exports=jdk.compiler/com.sun.tools.javac.parser=ALL-UNNAMED</arg>
                <arg>-J--add-exports=jdk.compiler/com.sun.tools.javac.processing=ALL-UNNAMED</arg>
                <arg>-J--add-exports=jdk.compiler/com.sun.tools.javac.tree=ALL-UNNAMED</arg>
                <arg>-J--add-exports=jdk.compiler/com.sun.tools.javac.util=ALL-UNNAMED</arg>
                <arg>-J--add-opens=jdk.compiler/com.sun.tools.javac.code=ALL-UNNAMED</arg>
                <arg>-J--add-opens=jdk.compiler/com.sun.tools.javac.comp=ALL-UNNAMED</arg>
              </compilerArgs>
            </configuration>
          </plugin>
        </plugins>
      </build>
    </profile>

[SentryMan]

so I've not used any of these null checking tools myself, do you happen to have an example project I can clone and take a look at?

Do you have any preferred path you'd like me to take to try and resolve this?

[rob-bygrave]

Hmm, what might resolve this would be to generate:

1. @Nullable on the fields of the builder (pretty much on all the fields in the builder regardless - could use avaje.lang.Nullable if we really wanted to or otherwise dynamically detect the appropriate Nullable annotation to use)
2. Use Objects.requiresNonNull() on the [known to be NonNull components which in this case is a ]

So instead of:
public Nullity build() { return new Nullity(a, b); }

Generate:
public Nullity build() { return new Nullity(Objects.requireNonNull(a), b); } // to perform the validation

[SentryMan]

dynamically detect the appropriate Nullable annotation to use

Sounds cool, how would one go about this?

EDIT: nvm I figured something out

[rbygrave]

the appropriate Nullable annotation

Just to say that the annotations in org.jspecify should ultimately replace the ones in io.avaje.lang. That is, the community at large has been waiting for org.jspecify to release those annotations and I see they released a 0.3.0 version in December - yay!!. When the 1.0 version is released, then my expectation is that would ultimately replace the io.avaje.lang ones [and maybe one day the org.jspecify annotations could become part of the JDK].

[SentryMan]

Just to say that the annotations in org.jspecify should ultimately replace the ones in io.avaje.lang.

So do you want me to use the jspecify ones now?

[SentryMan]

@commonquail
So I'm trying to add the checker to the PR but I'm getting an illegal access error.

java.lang.IllegalAccessError: class org.checkerframework.javacutil.AbstractTypeProcessor
(in unnamed module @0x3ab9363a)  cannot access class com.sun.tools.javac.processing.JavacProcessingEnvironment 
(in module jdk.compiler) because module jdk.compiler does not 
export com.sun.tools.javac.processing to unnamed module

here's my pom, am I missing something?

EDIT: nvm I figured it out haha

[commonquail]

do you happen to have an example project I can clone and take a look at?

Sorry for the delay. I was not in a position to easily do so so I settled for inlining hopefully-adequate samples.

Do you have any preferred path you'd like me to take to try and resolve this?

I reported this more as an observation on the current state of the ecosystem than an attempt to suggest any components are malfunctioning, in the even that either you or other potential users would find value in that.

That said, my personal preferences are the moment are for you to...

1. ... take a stance on scope (will/won't do, technical obstacles notwithstanding) so users know what they have to work with
2. ... do pretty much exactly what rob-bygrave proposed.

Note that public Nullity build() { return new Nullity(Objects.requireNonNull(a), b); } will work out of the box for NullAway but will not work by default for Checker Framework. Therefore you would have to decide the degree of compatibility with Checker Framework to pursue. On the other hand, a local if (this.a == null) { throw not-NPE } would work for both. For my own part, at this point I would not likely pursue validation with Checker Framework's nullness checker so I don't care what you do in that respect.

I believe such a change is sufficient to avoid excluding generated builders from NullAway's analysis.

[SentryMan]

Yeah went with option 2. Though due to the requiresNonNull thing I merely generated a method that will throw illegal state exceptions when nulls are where they shouldn't be. I got it working with both checker and null away, so I'm just waiting for review.

[SentryMan]

Better late than never I guess, the changes are in 1.1-RC1