Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Use the new TypeUseLocation default locations #165

Merged
merged 30 commits into from
Apr 11, 2024
Merged

Use the new TypeUseLocation default locations #165

merged 30 commits into from
Apr 11, 2024

Conversation

wmdietl
Copy link
Collaborator

@wmdietl wmdietl commented Feb 8, 2024

Depends on eisop/checker-framework#708.

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

Fixes #159, #161, #163.

@wmdietl wmdietl changed the title Use the new TypeUseLocation.IMPLICIT_WILDCARD_UPPER_BOUND Use the new TypeUseLocation default locations Feb 26, 2024
@@ -70,11 +70,11 @@ FAIL: CaptureConvertedUnspecToOther.java: no unexpected facts
FAIL: CaptureConvertedUnspecToOtherUnionNull.java: no unexpected facts
FAIL: CaptureConvertedUnspecToOtherUnspec.java: no unexpected facts
PASS: CastOfCaptureOfNotNullMarkedUnboundedWildcardForObjectBoundedTypeParameter.java: no unexpected facts
PASS: CastOfCaptureOfUnboundedWildcardForNotNullMarkedObjectBoundedTypeParameter.java: no unexpected facts
FAIL: CastOfCaptureOfUnboundedWildcardForNotNullMarkedObjectBoundedTypeParameter.java: no unexpected facts
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The unexpected error for this test case is:

build/conformanceTests/samples/CastOfCaptureOfUnboundedWildcardForNotNullMarkedObjectBoundedTypeParameter.java:26: error: [type.argument.type.incompatible] incompatible type argument for type parameter T of Supplier.
    void x(Supplier<?> supplier) {
                    ^
  found   : capture#576 of ? extends Object*
  required: Object*

I think the defaults work correctly: the IMPLICIT_WILDCARD_UPPER_BOUND_NO_SUPER default is @Nullable, which gets combined with the declared upper bound, resulting in capture of ? extends Object*.

However, that is not a subtype of Object*. @cpovirk does this look like some problem with the type hierarchy?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It is correct for the checker to produce an error here. The reason that it's showing up as FAIL is that the conformance-test framework doesn't support jspecify_nullness_not_enough_information yet, only jspecify_nullness_mismatch.

(Object* is not a subtype of Object* so as to indicate that, if you don't know what you have and you don't know what you need, we can't prove that it's safe. Our expectation is that few checkers (if any) will produce even a warning in this case—or even in a more-likely-to-be-unsafe case in which you have an Object? and need an Object*. Still, the tests label such cases accordingly. This labeling may help tools like the Checker Framework that make specific assumptions about unannotated code: If a line is labeled with jspecify_nullness_mismatch, a tool like the Checker Framework can consider itself to "pass" whether it produces an error there or not. This is in contrast to cases in which it should always produce an error and cases in which it never should.)

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks, so I did remember correctly that that is how unspecified nullness is supposed to work.

I've opened jspecify/jspecify#487 to add the optional error.

(In your penultimate sentence: If a line is labeled with jspecify_nullness_mismatch, a tool like the Checker Framework can consider itself to "pass" whether it produces an error there or not. Here you meant jspecify_nullness_not_enough_information, right?)

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oops, yes, sorry.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The error here (which we add as expected in jspecify/jspecify#487) feels wrong to me.
The captured wildcard is for that type parameter of Supplier. So while in general, two unspecified nullness can't be subtypes, here, the type argument is a capture of that unspecified nullness, so it will always match.
Even more fundamentally, when checking Supplier<?> the wildcard isn't captured at all - a capture only happens at a call/field access. So the found type is not what it should be.
What do you think?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I am still not sure where the code that makes the main branch avoid this error is :\

I thought maybe 89d9b72#diff-ce82a59b06d0d82bfc6d06835d1b06ac15619bc3a71617d32189d041f02ca9c0R270, but then I found that I'd removed that cocde in 8ba39b0

I thought maybe jspecify/checker-framework@00cc056, but then I found that I'd removed that code in jspecify/checker-framework@72c5c16.

Maybe 9348e76#diff-ce82a59b06d0d82bfc6d06835d1b06ac15619bc3a71617d32189d041f02ca9c0R894 is somehow related?

I also have open 74f564f, 7e662e3, and 824113a, but I'm not convinced that any of that is relevant.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

OK, I started just diffing checker-framework against upstream, and the code jumped right out to me. At least, I assume this is the right code:

https://github.com/jspecify/checker-framework/blob/b84882d9b2f77c99081118cc7ad095dfcc3484f5/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeValidator.java#L562

(That code was a small part of the large merge commit jspecify/checker-framework@2e588e7.)

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks a lot for tracking this down!
I'll look into fixing this in the reference checker or the framework.
Besides the error here, these incorrect captures are also the cause for #164.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, do you think that it's possible that #164 is related to https://github.com/jspecify/checker-framework/blob/b84882d9b2f77c99081118cc7ad095dfcc3484f5/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java#L5017 (jspecify/checker-framework#47)?

That is, could there be two issues here?

  1. The upstream checker performs a check that the wildcard bound (or capture thereof?) is in bounds (of the type-parameter bound? of the wildcard bound?). That leads to failures for JSpecify because Object* is not a subtype of Object*. My "fix" for that was to remove the possibly unnecessary check entirely. (cause of Capture of Object* is not compatible with Object*. jspecify#487)?)
  2. When we do perform capture conversion, we get it wrong. (cause of main-eisop: x(Foo<? super T>) cannot override identical signature #164?)

The reason that it seems strange for #164 to be related to this issue is that #164 doesn't involve unspecified nullness.

But I guess that, if the tests of #164 start passing with this change, then it's a fix :) Still, maybe it's more that we're hiding the failure (by no longer checking the incorrect capture against anything) than fixing it (by making the results of capture correct)? I don't know :\

I should also write up something about type parameters in general that I've been thinking about recently. It might end up saving us some work... maybe....

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

9ee2796 uses hasEffectiveAnnotation instead of hasAnnotation. #164 has ? super T and when the code asked whether the wildcard had a particular annotation in the lower bound, it got "none", because the type variable T isn't annotated. hasEffectiveAnnotation follows bounds to find the first declared type.

I replaced all hasAnnotation with hasEffectiveAnnotation in the NullSpecAnnotatedTypeFactory. I should probably have that done more incrementally, as two more conformance tests fail now... let me see why that is. I should also look at uses of hasAnnotation in other files.

@@ -0,0 +1,12 @@
// Test case for Issue 161:
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've added this test case to show that the issue #161 is fixed.
I didn't find a file with this name in the samples.
@cpovirk Should I keep this file here or add it somewhere else?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe it can live under conformance-tests/src/assertions? netdpb@ will be back Thursday :)

Nullable.class,
NullnessUnspecified.class,
MinusNull.class,
ParametricTypeVariableUse.class));
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'll refactor how I do this in EISOP separately and add an explicit qualifier here. This is just a first hack.

@wmdietl
Copy link
Collaborator Author

wmdietl commented Feb 27, 2024

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
Copy link
Collaborator Author

wmdietl commented Mar 22, 2024

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

@wmdietl
Copy link
Collaborator Author

wmdietl commented Mar 23, 2024

I opened jspecify/jspecify#498 to fix the compilation error. While doing that I ran into google/error-prone#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.

Copy link
Collaborator Author

@wmdietl wmdietl left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There is some mismatch in running the conformance tests between my local setup and CI... not sure what's going on.
Once that is done, I suggest we finally merge this. Conformance test scores improve and #159, #161, and #163 are fixed.
Some of the sample tests produce slightly worse results, but I rather look at those separately.
@cpovirk Could you have a look at this PR and let me know what you think?

@wmdietl
Copy link
Collaborator Author

wmdietl commented Mar 26, 2024

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.

@@ -861,8 +894,8 @@ protected AnnotatedTypeMirror substituteTypeVariable(
substitute.replaceAnnotation(minusNull);
} else if (argument.hasAnnotation(unionNull) || use.hasAnnotation(unionNull)) {
substitute.replaceAnnotation(unionNull);
} else if (argument.hasAnnotation(nullnessOperatorUnspecified)
|| use.hasAnnotation(nullnessOperatorUnspecified)) {
} else if (argument.hasEffectiveAnnotation(nullnessOperatorUnspecified)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm going to just not think about this part for now, given the chance that our substitution behavior will change in one or more ways (jspecify/jspecify#248 (comment), jspecify/jspecify#91 (comment)) and given my lack of deep understanding of the Checker Framework model :)

@cpovirk
Copy link
Collaborator

cpovirk commented Mar 26, 2024

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:

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
Copy link
Collaborator Author

wmdietl commented Mar 28, 2024

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...

Copy link
Collaborator

@cpovirk cpovirk left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good info, thanks.

I'm still somewhat confused about the errors: If the problem were merely that we're seeing accidentally unspecified types, then I'd expect not to see errors, since we're running in lenient mode inside Google. But it's possible that we're seeing accidentally unspecified types and that we're not handling subtyping (and/or "same-type" checking?) correctly in the presence of unspecified types: As you say, we already have seen a similar-looking problem in #164.

As for workarounds: We certainly do have our own separate defaulting system. There seem to have been multiple reasons that led me down that path. I don't specifically remember being aware of the problem that you mentioned, but it's been a long time, so maybe I've just forgotten. (I could dig into the commit history, but it's probably academic.)

The rule of "look for defaults only in source code" probably also explains why I had to hack up the stub-file code so badly in order to recognize @NullMarked in the JDK stubs. Fortunately, I think we can get away without worrying about stub files for now. But it is good to have a deeper understanding of why that was hard to get working.

I'm fine with merging to lock in the progress so far.

@cpovirk
Copy link
Collaborator

cpovirk commented Apr 1, 2024

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
Copy link
Collaborator

cpovirk commented Apr 2, 2024

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 #165 (comment), 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

cpovirk added a commit that referenced this pull request Apr 2, 2024
While the order of the input files _shouldn't_ affect behavior, it
sometimes does. Let's use a consistent order so that we at least don't
see behavior differences between local and CI runs:

#165 (comment)
cpovirk added a commit that referenced this pull request Apr 2, 2024
While the order of the input files _shouldn't_ affect behavior, it
sometimes does. Let's use a consistent order so that we at least don't
see behavior differences between local and CI runs:

#165 (comment)
@@ -0,0 +1,26 @@
// Copyright 2024 The JSpecify Authors
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@cpovirk @netdpb Let's re-start the discussion from #165 (comment)

I've added tests for the three fixed issues and the override test from one of the last comments. I could either remove them before we merge this or maybe move them from minimal to issues or some other sub-directory?

We can then merge this and I'll work on #164 in a new PR.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We discussed this today and settled on moving the tests. Done in 2588340
A future cleanup can move some of them to conformance tests and keep others.

@wmdietl wmdietl merged commit 76b33c9 into main-eisop Apr 11, 2024
3 of 5 checks passed
@wmdietl wmdietl deleted the issue-161 branch April 11, 2024 21:38
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

main-eisop: Unbounded wildcards default to non-nullable main-eisop crash in TernaryUnspecVsNoQualifier
2 participants