Closed commonquail closed 1 week ago
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>
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?
Hmm, what might resolve this would be to generate:
@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)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
dynamically detect the appropriate Nullable annotation to use
Sounds cool, how would one go about this?
EDIT: nvm I figured something out
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].
Just to say that the annotations in
org.jspecify
should ultimately replace the ones inio.avaje.lang
.
So do you want me to use the jspecify ones now?
@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
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...
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.
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.
Better late than never I guess, the changes are in 1.1-RC1
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
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 https://github.com/uber/NullAway/issues/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:
Given a record
avaje-record-builder-1.0 generates the moral equivalent of
When compiled (POM below), Checker Framework produces three errors:
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).
assignment
: Although theNullityBuilder b(@Nullable String b)
receiver correctly hadorg.jspecify.annotations.Nullable
propagated from theNullity.b
component the annotation was not propagated to theNullityBuilder.b
field, which Checker Framework consequently resolves to@NonNull
.@Nullable
should have been propagated all the way to the field.initialization.fields.uninitialized
: Thebuilder()
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 thatNullityBuilder.[@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 ofNullityBuilder.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 rejectingObjects.requireNonNull
.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 becauseNullityBuilder.a
cannot practically be@NonNull
.NullityBuilder.a
and all other@NonNull
record components could be promoted to parameters on thebuilder()
method. This would undermine the utility of the resulting builder, however.POM: