Introduce a NullSpecTypeValidator to ensure unspecified type variables are ok

[wmdietl]

Fixes #177.

Depends on eisop/checker-framework#746 to also correctly default type variable lower bounds.
@cpovirk If it is easy, could you see whether that EISOP PR introduces any new issues?

With both of these changes, the conformance tests should pass again.

[cpovirk]

The code change looks reasonable. Assuming that I did the testing with eisop/checker-framework#746 correctly, however, I'm now seeing at least a few dozen new errors.

It's mostly errors like this:

com/google/common/collect/Streams.java:375: error: [override.param.invalid] Incompatible parameter type for action.
              public boolean tryAdvance(Consumer<? super R> action) {
                                                            ^
  found   : Consumer<? super R>
  required: Consumer<? super R*>
  Consequence: method in 
    boolean tryAdvance(Consumer<? super R>)
  cannot override method in Spliterator<R*>
    boolean tryAdvance(Consumer<? super R*>)

And some of this similar kind of error:

com/google/common/collect/TreeMultimap.java:222: error: [assignment.type.incompatible] incompatible types in assignment.
    keyComparator = requireNonNull((Comparator<? super K>) stream.readObject());
                                  ^
  found   : Comparator<capture#845 of ? super K>
  required: Comparator<? super K>

I also see a tiny bit of this:

com/google/common/collect/Multisets.java:1137: error: [argument.type.incompatible] incompatible argument for parameter o of Collections.nCopies.
        entry -> Collections.nCopies(entry.getCount(), entry.getElement()).spliterator(),
                                                                       ^
  found   : E*
  required: E

(As usual, the line numbers there might not exactly line up with the public version.)

One small note: It looks like I had been testing past PRs with the most recent version of eisop/checker-framework that we'd imported already. That version doesn't include any changes from April. That might not matter, but I point it out to say that it's at least possible that any problems "with this PR" actually come from some recent eisop/checker-framework change that I only now imported. However, I'm not sure what that would be other than eisop/checker-framework@1d2bd6c. And when I make that change in my previous test client (which had a combination of #171 and #175), I don't see any errors. So I think that the errors really do result from this PR or the eisop/checker-framework PR.

[wmdietl]

@cpovirk Thanks for testing!

I've merged eisop/checker-framework#746 now.
Can you please let me know whether the errors in Streams.java and TreeMultimap.java are gone? I do hope so :-)

Locally, the conformance tests for this PR pass for me.

Adding the NullSpecTypeValidator only makes a difference of 4 test cases, and only in strict mode. Things are better with the more lenient validator.

On the highest level, for the jspecifySamplesTest, I now see:

tests.NullSpecTest$Lenient > run[/home/wdietl/tmp/jspecify/jspecify-reference-checker/build/conformanceTests/samples] FAILED
    java.lang.AssertionError: 1200 out of 1217 expected diagnostics were found.
    18 unexpected diagnostics were found:
....
    17 expected diagnostics were not found:
....
tests.NullSpecTest$Lenient > run[/home/wdietl/tmp/jspecify/jspecify-reference-checker/build/conformanceTests/samples/nullnessUnspecifiedTypeParameter/nullnessunspecifiedtypeparameter] FAILED
    java.lang.AssertionError: 7 out of 7 expected diagnostics were found.
    1 unexpected diagnostic was found:
....
tests.NullSpecTest$Strict > run[/home/wdietl/tmp/jspecify/jspecify-reference-checker/build/conformanceTests/samples] FAILED
    java.lang.AssertionError: 1211 out of 1217 expected diagnostics were found.
    180 unexpected diagnostics were found:
....
    6 expected diagnostics were not found:
....
tests.NullSpecTest$Strict > run[/home/wdietl/tmp/jspecify/jspecify-reference-checker/build/conformanceTests/samples/annotatedBoundsOfWildcard/annotatedboundsofwildcard] FAILED
    java.lang.AssertionError: 21 out of 21 expected diagnostics were found.
    7 unexpected diagnostics were found:
....
tests.NullSpecTest$Strict > run[/home/wdietl/tmp/jspecify/jspecify-reference-checker/build/conformanceTests/samples/wildcardsWithDefault/wildcardswithdefault] FAILED
    java.lang.AssertionError: 2 out of 2 expected diagnostics were found.
    2 unexpected diagnostics were found:
....
34 tests completed, 6 failed

The biggest blocker are the 180 unexpected diagnostics in strict mode. Do you see a pattern do those?

Picking one of the lenient failures:

jspecify-reference-checker/build/conformanceTests/samples/MultiBoundTypeVariableUnspecToObject.java:55:Error: (return.type.incompatible) incompatible types in return.
        return x;
               ^
      type of expression: T*
      method return type: Object

In lenient mode, should T* be a subtype of Object? Currently, it is not, even in lenient mode. Is that a problem with the hierarchy or the test case? I don't see a reason why the bounds of T should matter, as there is an explicit "unspecified" annotation on the use of T.

Another question:

tests.NullSpecTest$Lenient > run[/home/wdietl/tmp/jspecify/jspecify-reference-checker/build/conformanceTests/samples/nullnessUnspecifiedTypeParameter/nullnessunspecifiedtypeparameter] FAILED
    java.lang.AssertionError: 7 out of 7 expected diagnostics were found.
    1 unexpected diagnostic was found:
      /home/wdietl/tmp/jspecify/jspecify-reference-checker/build/conformanceTests/samples/nullnessUnspecifiedTypeParameter/nullnessunspecifiedtypeparameter/NullnessUnspecifiedTypeParameter.java:34:Error: (type.argument.type.incompatible) incompatible type argument for type parameter T of NullnessUnspecifiedTypeParameter.
      static final NullnessUnspecifiedTypeParameter<@Nullable Object> A2 =
                                                    ^
      found   : Object?
      required: Object

Looking at conformanceTests/samples/nullnessUnspecifiedTypeParameter/nullnessunspecifiedtypeparameter/NullnessUnspecifiedTypeParameter.java I do not understand the name of class NullnessUnspecifiedTypeParameter:

@NullMarked
public class NullnessUnspecifiedTypeParameter<T> {

Should the @NullMarked be @NullUnmarked?
As it is now, the error makes sense to me.
If it should be @NullUnmarked, it depends on whether in lenient mode it should be an error to pass @Nullable to a type parameter that is unspecified - i.e. it could be changed to non-null-bounded later.

Sorry for the long message. I made one long comment, but it might be easier to split up replies into individual comments. Or whatever works best for you :-)

[cpovirk]

Assuming that I did the testing right, I'm still seeing the errors from last time even after importing eisop/checker-framework#746 :(

More on the rest in a bit.

[cpovirk]

Oops, I replied about the Consumer<? super R> action problems in eisop/checker-framework#746 (comment) instead of here. Anyway, as noted there, they're now gone!

[cpovirk]

Correction: As I just noted in the other thread: The Consumer<? super R> action errors are still around after all.

I'll see about finally actually getting you a command to reproduce them.

[cpovirk]

OK, that wasn't actually hard at all, sorry.

$ git clone [email protected]:jspecify/jspecify-reference-checker.git

$ cd jspecify-reference-checker/

$ git checkout main-eisop # 9e4d14d4a19751a7211bf4c02e202126f59c58f3

$ JAVA_HOME=$HOME/jdk-17.0.2 ./gradlew clean assemble

$ ./demo ListSubclass.java
Note: The Checker Framework is tested with JDK 8, 11, 17, and 21. You are using version 22.
ListSubclass.java:8: error: [override.param.invalid] Incompatible parameter type for filter.
  boolean removeIf(Predicate<? super Z> filter);
                                        ^
  found   : Predicate<? super Z>
  required: Predicate<? super Z*>
  Consequence: method in ListSubclass<Z>
    boolean removeIf(Predicate<? super Z>)
  cannot override method in Collection<Z*>
    boolean removeIf(Predicate<? super Z*>)
1 error
Note: 
  =====
  The nullness checker is still early in development.
  It has many rough edges.
  For an introduction, see https://jspecify.dev/docs/user-guide
  =====

In contrast, if I create a fresh clone and build from the main branch (1a7b3ed), I get a success:

$ ./demo ListSubclass.java
warning: Use JDK 8, 11, or 17 to run the Checker Framework.  You are using version 22.
1 warning

[wmdietl]

@cpovirk Thanks for looking into this!
Can you share the code for ListSubclass.java?

You seem to be testing against main-eisop and get an unexpected error there.
What happens when you test against this PR?

[cpovirk]

🤦

I managed to notice that just before posting and then still not post it :)

import java.util.List;
import java.util.function.Predicate;
import org.jspecify.annotations.NullMarked;
import org.jspecify.annotations.Nullable;

@NullMarked
interface ListSubclass<Z extends @Nullable Object> extends List<Z> {
  boolean removeIf(Predicate<? super Z> filter);
}

[cpovirk]

I see the same error when building with this PR (f2c3679).

[cpovirk]

If you clone the guava repo and check out the newly updated jspecify-preview branch, you can also try to build it with such monstrous commands as:

CLASSPATH=$HOME/.m2/repository/com/google/guava/failureaccess/1.0.1/failureaccess-1.0.1.jar:$HOME/.m2/repository/com/google/code/findbugs/jsr305/3.0.2/jsr305-3.0.2.jar:$HOME/.m2/repository/com/google/j2objc/j2objc-annotations/3.0.0/j2objc-annotations-3.0.0.jar:$HOME/.m2/repository/org/codehaus/mojo/animal-sniffer-annotations/1.24/animal-sniffer-annotations-1.24.jar:$HOME/.m2/repository/org/checkerframework/checker-qual/3.44.0/checker-qual-3.44.0.jar:$HOME/.m2/repository/com/google/errorprone/error_prone_annotations/2.28.0/error_prone_annotations-2.28.0.jar:${CHECKER_JAR}:$HOME/.m2/repository/org/jspecify/jspecify/1.0.0/jspecify-1.0.0.jar ./demo $(find /tmp/tmp.OBavpODHqE/guava/guava/src -name '*.java')

Currently:

• With the reference checker at main, I see 2 weird errors (which we somehow aren't seeing in our internal builds... :)) that suggest we're not seeing nullness information for a couple Map methods in some situations, but let's ignore that for now.
• With main-eisop or this PR, I see 19 errors, somehow not including the 2 above but including the kind of ? super E error we've been discussing here.

I wonder we could be so lucky that the problem would go away once I enact the proposal from jspecify/jspecify#248.....

[cpovirk]

With the reference checker at main, I see 2 weird errors (which we somehow aren't seeing in our internal builds... :)) that suggest we're not seeing nullness information for a couple Map methods in some situations, but let's ignore that for now.

Somehow I ended up with a jdk repo that didn't contain any of the actual annotated source files. I don't know exactly how it happened. I see no sign that I ctrl+c'ed Git while it was running (though I did ctrl+c one build after Git had seemingly succeeded), but maybe I'm missing it, or maybe the CF build failures I got during #190 somehow automatically aborted an in-progress Git operation?

Whatever was going on, I no longer see the 2 errors in a new clone.

[wmdietl]

How about I file a new issue with the test from earlier?
It sounds like both main-eisop and this PR have that issue.
This PR should fix #177.
Is this PR the cause of this new issue or is the new issue unrelated to this PR?

[cpovirk]

Yes, that sounds good. After re-reading some things, my impression is that I was treating the problem as "caused by" this PR because this PR required eisop/checker-framework#746—which is the true cause of the problem.

[cpovirk]

Sorry, I am confused again: It turns out that some of the new errors appear with eisop/checker-framework#746 and others appear only after we also include this PR. (I probably missed the second batch (at least sometimes) because the first batch was preventing the build from continuing. I have made that mistake before....)

The ones that need this PR look like they're all similar to the SequencedCollection errors—cases in which we override a method from an unannotated JDK class with a ? super type. Sadly, some very particular kinds of our builds use an unannotated JDK, so this causes significant trouble for those builds.

As you say, this PR should be purely a fix, so something is already wrong in the checker, and this PR is probably just (correctly) producing situations that exercise that bug more. And in fact, I have a lead, which is an "unrelated" problem I had a couple weeks back when the checker wouldn't let me override Map.merge (declared with an unspecified-nullness V parameter) with a non-null-projected V in [edit: similar to KT-63676!]. I think we need for an unspecified-nullness V to be a subtype of a non-null-projected V in lenient mode. In other words, we probably are lucky enough that this problem will go away once I implement jspecify/jspecify#248.

I'm not entirely sure whether that fix will address the smaller number of problems given in my initial post in #193. But given that that's a small number of problems (and that it's possibly related to type inference), I probably won't be worried much even if that problem remains.

[cpovirk]

--- a/NullSpecAnnotatedTypeFactory.java 2024-07-26 10:56:46.000000000 -0400
+++ b/NullSpecAnnotatedTypeFactory.java 2024-07-26 11:37:39.000000000 -0400
@@ -762,6 +762,9 @@
     if (subtype.hasAnnotation(minusNull)) {
       return true;
     }
+    if (!isLeastConvenientWorld && subtype.hasAnnotation(nullnessOperatorUnspecified)) {
+      return true;
+    }
 
     if (isUnionNullOrEquivalent(subtype)) {
       return false;

[cpovirk]

Sorry, I didn't mean to post that yet :)

Anyway: The above changes fixes some of the problems but not all. That makes sense, since it merely updates one usage of minusNull and not the various others that would be required to full implement jspecify/jspecify#248. But even with some further, similar changes, I'm still seeing errors, so I must have missed something. (Could we be lucky again and find that it's just jspecify/jspecify#522 or some other possible known issue?) Even assuming that I get that worked out, I'd still want to clean the changes up (likely to use a new isMinusNullOrEquivalent helper method similar to the existing isUnionNullOrEquivalent), actually update the spec, and ideally update all the samples, too....

[cpovirk]

Also, I should be posting on #193....

[cpovirk]

I just had one thought on the original change: Perhaps we should be allowing the unspecified-unspecified bounds pair only in lenient mode.

But I have forgotten the full context here. I know there's some weirdness around combining T extends Object and ? super Object, for example (though maybe a strict-mode error would technically be more appropriate there, and it's not like people run in strict mode, anyway :)). I'm not going to worry about it right this moment, but I'll try to test that change later today. And even if I don't, I'm writing this in the hope that it will help me remember this if it comes up again later.