False nullability errors in 3.42.0

[kennknowles]

Reproduce:

git clone https://github.com/kennknowles/beam --branch checkerframework-StructuralEqualityComparer
cd beam
./gradlew :sdks:java:core:compileJava

Output:

> Task :sdks:java:core:compileJava
./beam/sdks/java/core/src/main/java/org/apache/beam/sdk/io/Read.java:359: error: [dereference.of.nullable] dereference of possibly-null reference currentReader
                currentReader.close();
                ^
./beam/sdks/java/core/src/main/java/org/apache/beam/sdk/io/Read.java:367: error: [dereference.of.nullable] dereference of possibly-null reference currentReader
                    currentReader.getCurrent(), currentReader.getCurrentTimestamp());
                    ^
./beam/sdks/java/core/src/main/java/org/apache/beam/sdk/io/Read.java:367: error: [dereference.of.nullable] dereference of possibly-null reference currentReader
                    currentReader.getCurrent(), currentReader.getCurrentTimestamp());
                                                ^
./beam/sdks/java/core/src/main/java/org/apache/beam/sdk/io/Read.java:373: error: [dereference.of.nullable] dereference of possibly-null reference currentReader
              currentReader.close();
              ^

etc.

Expectation: these are not errors. This field currentReader was set to a non-nullable value with no intervening method calls.

[kennknowles]

While bisecting for a good checker version for Beam, confirmed that this (and many others) also occurs in checker 3.40.0

[kennknowles]

I don't know if it is the same, but most of the issues I see are consistent with the following hypothesis: Given an object o with field x with a non-null value, the algorithm seems to believe that calling o.x.m() can now cause o.x to become null. I suppose this is true if there is a circular dependency where o.x.m() eventually has a handle on o and sets o.x to null? I have never seen this but makes sense - is this the case? Is there a way to elide this? Otherwise literally every method call in the language has the potential to set the receiver to null, basically.

I also saw some cases even if x.m() is declared @Pure and checked against null but a repeat call did not maintain the nullness of the result.

[mernst]

Kenn, your hypothesis is correct: the Nullness Checker reasons that it is conceivable that a method has a reference to a field and sets the field. Because its aim is an iron-clad guarantee, it issues a warning in this case. In many cases this is a false positive warning, as you point out.

The manual gives ways to specify your program so that the Nullness Checker can reason about (lack of) re-assignment, in section "Side effects, determinism, purity, and type refinement". Maybe one of these can work for you. In general, the solution to a false positive is often writing a specification (that is, annotations) to provide more information to the checker.

I also saw some cases even if x.m() is declared @Pure and checked against null but a repeat call did not maintain the nullness of the result.

This sounds like a bug. Could you please report it? But, a question first: is it possible that x was side-effected between the two calls x.m()? If so, the warning is a correct one.

More generally, if you have specific cases, please let us know about them individually and we can help you reason through them.

[kennknowles]

Got it. Yes I will see if I can find a good way to manage these particular errors. If I reproduce the tangentially mentioned case, I will file a new issue.