search

jspecify / jspecify-reference-checker

The reference implementation for the JSpecify nullness specification (and later, its other specifications as well)
https://jspecify.org
Apache License 2.0
27 stars 7 forks source link

Use the new `TypeUseLocation` default locations #165

Closed wmdietl closed 7 months ago

wmdietl commented 9 months ago

Depends on https://github.com/eisop/checker-framework/pull/708.

Something still seems to be missing, failure in NullUnmarkedUndoesNullMarkedForWildcards.java is odd.

Fixes #159, #161, #163.

wmdietl commented 9 months ago

A bit frustratingly, this doesn't fix #163 and #164. At least #163 I had hoped should be fixed by the change to TYPE_VARIABLE_USE defaults. I'll look some more.

wmdietl commented 9 months ago

Hmm. The number of expected errors that are not found went to 411. On the other hand, the number of unexpected errors went to 3.

I can't compare against main-eisop on CI, because for some reason it fails there: https://github.com/jspecify/jspecify-reference-checker/actions/runs/8058639754/job/22094984781#step:6:177

/home/runner/work/jspecify-reference-checker/jspecify-reference-checker/jspecify-reference-checker/src/main/java/com/google/jspecify/nullness/NullSpecVisitor.java:591: error: cannot find symbol

  private static final Set<String> NULLNESS_ANNOTATIONS =
> Task :compileJava FAILED
                       ^
  symbol:   class Set
  location: class NullSpecVisitor
/home/runner/work/jspecify-reference-checker/jspecify-reference-checker/jspecify-reference-checker/src/main/java/com/google/jspecify/nullness/NullSpecVisitor.java:592: error: cannot find symbol
      Set.of(
      ^
  symbol:   variable Set
  location: class NullSpecVisitor
2 errors

What is strange about this is that there is no Set.of in that file: https://github.com/jspecify/jspecify-reference-checker/blob/main-eisop/src/main/java/com/google/jspecify/nullness/NullSpecVisitor.java

Also, this PR builds successfully and doesn't touch NullSpecVisitor.java. So I'm a bit confused what CI is doing...

wmdietl commented 9 months ago

So locally, I get in main-eisop:

tests.NullSpecTest$Lenient > run[/home/wdietl/tmp/jspecify/jspecify-reference-checker-forked/build/conformanceTests/samples] FAILED
    java.lang.AssertionError: 1203 out of 1225 expected diagnostics were found.
    21 unexpected diagnostics were found:

whereas in this branch, as it is right now:

tests.NullSpecTest$Lenient > run[/home/wdietl/tmp/jspecify/jspecify-reference-checker-forked/build/conformanceTests/samples] FAILED
    java.lang.AssertionError: 1146 out of 1225 expected diagnostics were found.
    42 unexpected diagnostics were found:

So let me see what's going wrong here.

cpovirk commented 9 months ago

What is strange about this is that there is no Set.of in that file: https://github.com/jspecify/jspecify-reference-checker/blob/main-eisop/src/main/java/com/google/jspecify/nullness/NullSpecVisitor.java

I don't know where it's picking the commit from, but the logs show that it's picking 9cfc77d1a477371bcc743b7a3604cd8dde16c2a6, which does at least have the Set.of call:

https://github.com/jspecify/jspecify-reference-checker/blob/9cfc77d1a477371bcc743b7a3604cd8dde16c2a6/src/main/java/com/google/jspecify/nullness/NullSpecVisitor.java#L592

cpovirk commented 8 months ago

Is this the PR that you were seeing the surprise CI behavior for? (Sorry, I should really remember that....)

I just created 3 local clones:

Alongside each, I ran git clone git@github.com:jspecify/jspecify.git -b samples-google-prototype. Then, in each, I ran ./gradlew jspecifySamplesTest --include-build ../jspecify.

I think that's all expected.

Here are the details in test results:

Lenient samples
- 524 unexpected diagnostics were found
+ 486 unexpected diagnostics were found

Lenient implementwithnullabletypeargument
+ 1 unexpected diagnostic was found

Lenient wildcardswithdefault
- 3 unexpected diagnostics were found

Strict samples
- 1367 unexpected diagnostics were found
+ 1495 unexpected diagnostics were found

Strict implementwithnullabletypeargument
+ 1 unexpected diagnostic was found

Strict wildcardswithdefault
- 6 unexpected diagnostics were found
+ 4 unexpected diagnostics were found

I notice that this differs from the CI results, apparently because the CI for main-eisop checks out a different branch of the jspecify repo:

https://github.com/jspecify/jspecify-reference-checker/blob/8eb4ab8280e373c6ec97914a0f1fcf1a62a9e32f/.github/workflows/build.yml#L36-L37

Does that all seem reasonable to you? (Again, I might not even be asking about the right PR/branch....)

wmdietl commented 8 months ago

Thanks for looking into this @cpovirk ! Yes, this is the branch we had been discussing earlier.

For main-eisop and this PR you need to use the samples-google-prototype-eisop branch of jspecify, because the error marker format changed.

I'll try to reproduce your numbers. Both locally and on CI, for the lenient test, I see:

tests.NullSpecTest$Lenient > run[/home/runner/work/jspecify-reference-checker/jspecify-reference-checker/jspecify-reference-checker/build/conformanceTests/samples] FAILED
    java.lang.AssertionError: 816 out of 1227 expected diagnostics were found.
    3 unexpected diagnostics were found:
...
    411 expected diagnostics were not found:

Your numbers look very different, so I'm not sure what's going on.

cpovirk commented 8 months ago

Ah, thanks, I should have tried samples-google-prototype-eisop. With that, I'm able to reproduce the 816/3/411 numbers for the lenient samples test.

With this PR, I:

It ends like this:

found   : Lib<? extends Foo?>
required: Lib<? extends Foo>
ContainmentSuper.java:38:46: compiler.err.proc.messager: (type.argument.type.incompatible) $$ 4 $$ A $$ Check $$ Lib<? super Foo> $$ Lib<? super Foo?> $$ ( 1446, 1462 ) $$ incompatible type argument for type parameter A of Check.
found   : Lib<? super Foo>
required: Lib<? super Foo?>
ContainmentSuperVsExtends.java:24:41: compiler.err.proc.messager: (type.argument.type.incompatible) $$ 4 $$ A $$ Check $$ Lib<? super Foo> $$ Lib<? extends Object> $$ ( 885, 901 ) $$ incompatible type argument for type parameter A of Check.
found   : Lib<? super Foo>
required: Lib<? extends Object>
ContainmentSuperVsExtends.java:31:26: compiler.err.proc.messager: (type.argument.type.incompatible) $$ 4 $$ A $$ Check $$ Lib<? super Foo> $$ Lib<? extends Object> $$ ( 1136, 1152 ) $$ incompatible type argument for type parameter A of Check.
found   : Lib<? super Foo>
required: Lib<? extends Object>
ContainmentSuperVsExtendsSameType.java:23:41: compiler.err.not.within.bounds: ContainmentSuperVsExtendsSameType.Lib<? super java.lang.Number>, A
133 errors
4 warnings
- compiler.note.proc.messager:
=====
The nullness checker is still early in development.
It has many rough edges.
For an introduction, see https://jspecify.dev/docs/user-guide
=====

The files are being processed in alphabetical order, so it seems that something goes wrong before we even get to ContravariantReturns (which would be the very next file)—and of course many other files.

I wondered if I'd get more information if I went back to the normal, user-facing output, so I removed -Adetailedmsgtext (and -XDrawDiagnostics, which I think was irrelevant, oops). The output still ended mysteriously after ContainmentSuperVsExtendsSameType.java.

Hmm, wait a minute: That's a javac error:

/tmp/tmp.Mrxwdt3AcN/main-eisop/jspecify-reference-checker/build/conformanceTests/samples/ContainmentSuperVsExtendsSameType.java:23: error: type argument Lib<? super Number> is not within bounds of type-variable A
    new Check<Lib<? extends Number>, Lib<? super Number>>();
                                        ^
  where A,F are type-variables:
    A extends F declared in class Check
    F extends @org.jspecify.annotations.Nullable Object declared in class Check
1 error

So I suspect that https://github.com/jspecify/jspecify/pull/485 broke this.

I guess that the runner used by jspecifySamplesTest doesn't abort on javac errors.

wmdietl commented 8 months ago

Thanks for tracking this down, @cpovirk ! I'll look into why javac errors aren't surfaced properly and into fixing the problem introduced in https://github.com/jspecify/jspecify/pull/485.

wmdietl commented 8 months ago

I opened https://github.com/jspecify/jspecify/pull/498 to fix the compilation error. While doing that I ran into https://github.com/google/error-prone/issues/4343. I ended up disabling error-prone on samples anyways, b/c there are too many warnings for the hand-crafted samples.

With that fixed, the numbers in this PR look much better. I'll still try to first track down why javac errors don't show up in test output - they do show up in stock EISOP.

wmdietl commented 8 months ago

The mismatch is

        -PASS: implementWithNullableTypeArgument/implementwithnullabletypeargument/User.java: no unexpected facts
        +FAIL: implementWithNullableTypeArgument/implementwithnullabletypeargument/User.java: no unexpected facts

I'm trying to find what is different in CI.

cpovirk commented 8 months ago

I kicked off an internal build with the current code in this PR (752ad0978019cdfdbe6675ffa807a1486e55858e). I'll have to sort through the result in more detail on another day, but the main thing that jumps out to me at the moment is a lot of messages along the lines of found: Foo<T> | required: Foo<T>. It's somewhat like https://github.com/jspecify/jspecify-reference-checker/issues/164 but not resricted to ? super:

java/com/google/common/collect/HashBiMap.java:707: error: [override.param.invalid] Incompatible parameter type for entry.
        Entry<V, K> output(BiEntry<K, V> entry) {
                                         ^
  found   : BiEntry<K, V>
  required: BiEntry<K, V>
  Consequence: method in 
    Entry<V, K> output(BiEntry<K, V>)
  cannot override method in Itr<Entry<V, K>>
    Entry<V, K> output(BiEntry<K, V>)
wmdietl commented 8 months ago

I kicked off an internal build with the current code in this PR (752ad09). I'll have to sort through the result in more detail on another day, but the main thing that jumps out to me at the moment is a lot of messages along the lines of found: Foo<T> | required: Foo<T>. It's somewhat like #164 but not resricted to ? super:

Thanks for re-running your tests! I think what is happening is that the @NullMarked is ignored when code comes from an Element, that is, a different compilation unit or bytecode. We treat @NullMarked and @NullUnmarked as changes to defaults. Defaults are however only applied when we check source code. In stock CF, we write the defaulted types back into the Element, which then allows us to directly see the annotations in bytecode. The reference checker intentionally does not store defaults back into bytecode. I think we need to change how we load bytecode and similarly look for @Null(Un)Marked on enclosing elements. Similarly, when looking at stub files, stock CF only looks at @AnnotatedFor. I'm not sure the defaults set by @Null(Un)Marked have any effect in stubs and the annotated JDK. Does either of these sound like you had work-arounds for them before? I don't see how this PR would have made that behavior different, so I think we can still merge this.

Because the @NullMarked is ignored, the upper bounds for these type variables are UnknownNullness and therefore the override check fails. But fixing the override check, ala #164, is probably not enough and we need to fix the above handling of defaults. (The error message is pretty cryptic, as it's the same type twice. The reference checker intentionally doesn't show bounds of type variables. I believe that in the bound we would see unknown nullness. Then we would still see the same type twice, but at least if one remembers that subtyping for unknown nullness is not reflexive, it might make sense.)

However, I'm still trying to figure out why the conformance test is different on CI than on my local machine...

cpovirk commented 8 months ago

Some notes:

import org.jspecify.annotations.NullMarked;
import org.jspecify.annotations.Nullable;

@NullMarked
class HashBiMapAlike<E extends @Nullable Object> {
  abstract class Super {
    abstract void accept(Entry<E> entry);
  }

  abstract class Sub extends Super {
    @Override
    abstract void accept(Entry<E> entry);
  }
}

interface Entry<E extends @Nullable Object> {}
$ ./demo HashBiMapAlike.java 
HashBiMapAlike.java:12: error: [override.param.invalid] Incompatible parameter type for entry.
    abstract void accept(Entry<E> entry);
                                  ^
  found   : Entry<E>
  required: Entry<E>
  Consequence: method in Sub
    void accept(Entry<E>)
  cannot override method in Super
    void accept(Entry<E>)
1 error
cpovirk commented 8 months ago

tl;dr I think the conformance-test runner needs to sort the input files. Not that that should matter, but I've seen it matter for my original samples integration, which I have set up to sort files.

Details:

I mentioned this part on an internal doc, but I'll say it here, too: The tests pass for me locally, as well. (That includes if I use JDK17 and if I use the ./gradlew build conformanceTests demoTest --include-build ../jspecify command line from CI.)

I wonder if we're seeing something similar to https://github.com/jspecify/jspecify-reference-checker/pull/165#issuecomment-2015364311, in which an error from javac itself stops us from checking many files. And maybe our different systems have very slight difference in how javac behaves, either because of different versions or because of environmental perturbations, perhaps the most likely of which would be filesystem iteration order?? Even if we're not seeing a javac error, I have seen cases (unfortunately) in which the order of files matters.

To test that, I just tried a run in which the conformance tests use ImmutableSortedSet instead of ImmutableList for their input files. And... that produced the failure locally!

    diff (-expected +actual):
        @@ -1,4 +1,4 @@
        -# 73 pass; 500 fail; 573 total; 12.7% score
        +# 72 pass; 501 fail; 573 total; 12.6% score
         FAIL: AnnotatedInnerOfNonParameterized.java: no unexpected facts
         FAIL: AnnotatedInnerOfParameterized.java: no unexpected facts
         FAIL: AnnotatedReceiver.java: no unexpected facts
        @@ -532,7 +532,7 @@
         FAIL: ignoreAnnotations/ignoreannotations/IgnoreAnnotations.java: no unexpected facts
         PASS: implementWithNullableTypeArgument/implementwithnullabletypeargument/MyFunction.java: no unexpected facts
         PASS: implementWithNullableTypeArgument/implementwithnullabletypeargument/SuperFunction.java: no unexpected facts
        -PASS: implementWithNullableTypeArgument/implementwithnullabletypeargument/User.java: no unexpected facts
        +FAIL: implementWithNullableTypeArgument/implementwithnullabletypeargument/User.java: no unexpected facts
         PASS: memberSelectNonExpression/memberselectnonexpression/MemberSelectNonExpressions.java: no unexpected facts
         PASS: nonPlatformTypeParameter/nonplatformtypeparameter/NonPlatformTypeParameter.java: no unexpected facts
         PASS: nullnessUnspecifiedTypeParameter/nullnessunspecifiedtypeparameter/NullnessUnspecifiedTypeParameter.java:35:jspecify_nullness_mismatch

The extra error, incidentally, appears to be this:

OOPS: implementWithNullableTypeArgument/implementwithnullabletypeargument/User.java:25:test:cannot-convert:SuperFunction!<Object!, Object!> to Object apply(Object)!
2024-03-28T14:07:45.7406117Z       /home/runner/work/jspecify-reference-checker/jspecify-reference-checker/jspecify-reference-checker/build/conformanceTests/samples/implementWithNullableTypeArgument/implementwithnullabletypeargument/User.java:25: (override.return.invalid) Incompatible return type.
2024-03-28T14:07:45.7409196Z         @Nullable Object apply(@Nullable Object f);
2024-03-28T14:07:45.7409908Z                   ^
2024-03-28T14:07:45.7410397Z       found   : Object?
2024-03-28T14:07:45.7410929Z       required: Object

That looks like a substitution problem. (Sorry, I can't seem to remember whether your existing suspicion had been a substitution problem or not.)

Since there are multiple files involved in that sample, the ordering hypothesis is relatively plausible. And sure enough:

$ ./demo ../jspecify/samples/implementWithNullableTypeArgument/implementwithnullabletypeargument/SuperFunction.java ../jspecify/samples/implementWithNullableTypeArgument/implementwithnullabletypeargument/User.java ../jspecify/samples/implementWithNullableTypeArgument/implementwithnullabletypeargument/MyFunction.java 

(no errors)

$ ./demo ../jspecify/samples/implementWithNullableTypeArgument/implementwithnullabletypeargument/MyFunction.java ../jspecify/samples/implementWithNullableTypeArgument/implementwithnullabletypeargument/SuperFunction.java ../jspecify/samples/implementWithNullableTypeArgument/implementwithnullabletypeargument/User.java 
../jspecify/samples/implementWithNullableTypeArgument/implementwithnullabletypeargument/User.java:25: error: [override.return.invalid] Incompatible return type.
    @Nullable Object apply(@Nullable Object f);
              ^
  found   : Object?
  required: Object
  Consequence: method in NullableObjectFunction
    Object? apply(Object?)
  cannot override method in SuperFunction<Object, Object>
    Object apply(Object)
1 error