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.

Sign up for GitHub

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

Show file tree
Hide file tree
Changes from 29 commits
Commits
Show all changes
30 commits
Select commit Hold shift + click to select a range
33817d8
Use EISOP CF sources (#118)
wmdietl Feb 6, 2024
324d817
Document that detail messages should not be filtered out (#146)
wmdietl Feb 6, 2024
1ef0817
Update `tests/ConformanceTest-report.txt` (#157)
wmdietl Feb 7, 2024
e673ee8
Use standard error format (#154)
wmdietl Feb 8, 2024
209435e
Handle both `https` and `git@` clones (#158)
wmdietl Feb 8, 2024
d9e96d0
Use the new `TypeInformationPresenter` to output more type informatio…
wmdietl Feb 8, 2024
1362fa2
Use the new `TypeUseLocation.IMPLICIT_WILDCARD_UPPER_BOUND`
wmdietl Feb 8, 2024
4a8bd5b
Split out fields for NullMarked default locations, to make it easier
wmdietl Feb 26, 2024
cb1c7b2
Add test for issue #161
wmdietl Feb 26, 2024
cbebcf2
Check out related eisop branch
wmdietl Feb 26, 2024
a1a45fc
Remove debugging output
wmdietl Feb 26, 2024
8eb4ab8
Map `type.invalid.super.wildcard` as an expected error (#166)
wmdietl Feb 27, 2024
fad09d5
Merge branch 'main-eisop' of github.com:jspecify/jspecify-reference-c…
wmdietl Feb 27, 2024
04b8d84
Remove special handling of type variables. Fixes #159.
wmdietl Feb 27, 2024
9ee2796
Use `hasEffectiveAnnotation` to handle TVs in bounds. Fixes #164.
wmdietl Feb 27, 2024
93b50dc
Use dedicated `ParametricNull` qualifier
wmdietl Feb 28, 2024
cf2aa1d
CF branch was merged
wmdietl Feb 28, 2024
859669f
Specify hierarchy
wmdietl Feb 28, 2024
f73dfbf
Use `hasAnnotation` with `unionNull`, pending further investigation
wmdietl Feb 28, 2024
41a4ce4
Apply spotless
wmdietl Feb 28, 2024
e073d35
Adapt a few more error keys
wmdietl Mar 5, 2024
77dc086
Undo some has[Effective]Annotation changes
wmdietl Mar 26, 2024
752ad09
Rerun conformance tests
wmdietl Mar 26, 2024
88d9c88
Output details in conformance tests
wmdietl Mar 28, 2024
a4d344b
Re-instate work-around to type variable bound issue
wmdietl Apr 10, 2024
acf4230
Merge branch 'main-eisop' of github.com:jspecify/jspecify-reference-c…
wmdietl Apr 10, 2024
5c25a46
Add tests for #159, #161, and #163.
wmdietl Apr 10, 2024
ac7487f
Ensure tests are properly formatted
wmdietl Apr 10, 2024
9ba1aa8
Add test of overrides.
wmdietl Apr 10, 2024
2588340
Move regression tests to `tests/regression`.
wmdietl Apr 11, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .github/workflows/build.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,7 @@ jobs:
run: ./gradlew build conformanceTests demoTest --include-build ../jspecify
env:
SHALLOW: 1
JSPECIFY_CONFORMANCE_TEST_MODE: details
- name: Check out jspecify/samples-google-prototype-eisop
if: always()
run: |
Expand Down
1 change: 1 addition & 0 deletions build.gradle
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -235,6 +235,7 @@ if (!cfQualJar.toFile().exists()) {

spotless {
java {
target '**/*.java'
googleJavaFormat()
formatAnnotations()
}
Expand Down
93 changes: 75 additions & 18 deletions src/main/java/com/google/jspecify/nullness/NullSpecAnnotatedTypeFactory.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -115,6 +115,7 @@ final class NullSpecAnnotatedTypeFactory
private final AnnotationMirror minusNull;
private final AnnotationMirror unionNull;
private final AnnotationMirror nullnessOperatorUnspecified;
private final AnnotationMirror parametricNull;

private final boolean isLeastConvenientWorld;
private final NullSpecAnnotatedTypeFactory withLeastConvenientWorld;
Expand All @@ -128,6 +129,11 @@ final class NullSpecAnnotatedTypeFactory
final AnnotatedDeclaredType javaLangThreadLocal;
final AnnotatedDeclaredType javaUtilMap;

// Ensure that all locations that appear in the `defaultLocations` also appear somewhere in the
// `nullMarkedLocations`.
// As defaults are added and removed to the same environment, we need to ensure that all values
// are correctly changed.

private static final TypeUseLocation[] defaultLocationsMinusNull =
new TypeUseLocation[] {
TypeUseLocation.CONSTRUCTOR_RESULT,
Expand All @@ -138,14 +144,38 @@ final class NullSpecAnnotatedTypeFactory

private static final TypeUseLocation[] defaultLocationsUnionNull =
new TypeUseLocation[] {
TypeUseLocation.LOCAL_VARIABLE, TypeUseLocation.RESOURCE_VARIABLE,
TypeUseLocation.IMPLICIT_WILDCARD_UPPER_BOUND_SUPER,
TypeUseLocation.LOCAL_VARIABLE,
TypeUseLocation.RESOURCE_VARIABLE,
};

private static final TypeUseLocation[] defaultLocationsUnspecified =
new TypeUseLocation[] {
// TypeUseLocation.UNBOUNDED_WILDCARD_UPPER_BOUND, TODO
TypeUseLocation.IMPLICIT_WILDCARD_UPPER_BOUND_NO_SUPER,
TypeUseLocation.TYPE_VARIABLE_USE,
TypeUseLocation.OTHERWISE
};

private static final TypeUseLocation[] nullMarkedLocationsMinusNull =
new TypeUseLocation[] {
TypeUseLocation.CONSTRUCTOR_RESULT,
TypeUseLocation.EXCEPTION_PARAMETER,
TypeUseLocation.IMPLICIT_LOWER_BOUND,
TypeUseLocation.RECEIVER,
TypeUseLocation.OTHERWISE
};
private static final TypeUseLocation[] nullMarkedLocationsUnionNull =
new TypeUseLocation[] {
TypeUseLocation.LOCAL_VARIABLE,
TypeUseLocation.RESOURCE_VARIABLE,
TypeUseLocation.IMPLICIT_WILDCARD_UPPER_BOUND_NO_SUPER,
TypeUseLocation.IMPLICIT_WILDCARD_UPPER_BOUND_SUPER,
};

private static final TypeUseLocation[] nullMarkedLocationsParametric =
new TypeUseLocation[] {TypeUseLocation.TYPE_VARIABLE_USE};

private static final TypeUseLocation[] nullMarkedLocationsUnspecified = new TypeUseLocation[] {};

/** Constructor that takes all configuration from the provided {@code checker}. */
NullSpecAnnotatedTypeFactory(BaseTypeChecker checker, Util util) {
Expand All @@ -170,6 +200,7 @@ private NullSpecAnnotatedTypeFactory(
minusNull = util.minusNull;
unionNull = util.unionNull;
nullnessOperatorUnspecified = util.nullnessOperatorUnspecified;
parametricNull = util.parametricNull;

addAliasedTypeAnnotation(
"org.jspecify.annotations.NullnessUnspecified", nullnessOperatorUnspecified);
Expand All @@ -187,30 +218,36 @@ private NullSpecAnnotatedTypeFactory(
AnnotationMirror nullMarkedDefaultQualMinusNull =
new AnnotationBuilder(processingEnv, DefaultQualifier.class)
.setValue("value", MinusNull.class)
.setValue(
"locations",
new TypeUseLocation[] {
TypeUseLocation.EXCEPTION_PARAMETER, TypeUseLocation.OTHERWISE
})
.setValue("locations", nullMarkedLocationsMinusNull)
.setValue("applyToSubpackages", false)
.build();
AnnotationMirror nullMarkedDefaultQualUnionNull =
new AnnotationBuilder(processingEnv, DefaultQualifier.class)
.setValue("value", Nullable.class)
.setValue(
"locations",
new TypeUseLocation[] {
TypeUseLocation.LOCAL_VARIABLE, TypeUseLocation.RESOURCE_VARIABLE,
// TypeUseLocation.UNBOUNDED_WILDCARD_UPPER_BOUND TODO
})
.setValue("locations", nullMarkedLocationsUnionNull)
.setValue("applyToSubpackages", false)
.build();
AnnotationMirror nullMarkedDefaultQualParametric =
new AnnotationBuilder(processingEnv, DefaultQualifier.class)
.setValue("value", ParametricNull.class)
.setValue("locations", nullMarkedLocationsParametric)
.setValue("applyToSubpackages", false)
.build();
AnnotationMirror nullMarkedDefaultQualUnspecified =
new AnnotationBuilder(processingEnv, DefaultQualifier.class)
.setValue("value", NullnessUnspecified.class)
.setValue("locations", nullMarkedLocationsUnspecified)
.setValue("applyToSubpackages", false)
.build();
AnnotationMirror nullMarkedDefaultQual =
new AnnotationBuilder(processingEnv, DefaultQualifier.List.class)
.setValue(
"value",
new AnnotationMirror[] {
nullMarkedDefaultQualMinusNull, nullMarkedDefaultQualUnionNull
nullMarkedDefaultQualMinusNull,
nullMarkedDefaultQualUnionNull,
nullMarkedDefaultQualParametric,
nullMarkedDefaultQualUnspecified
})
.build();

Expand Down Expand Up @@ -359,7 +396,8 @@ protected void addUncheckedStandardDefaults(QualifierDefaults defs) {

@Override
protected Set<Class<? extends Annotation>> createSupportedTypeQualifiers() {
return new LinkedHashSet<>(asList(Nullable.class, NullnessUnspecified.class, MinusNull.class));
return new LinkedHashSet<>(
asList(Nullable.class, NullnessUnspecified.class, MinusNull.class, ParametricNull.class));
}

@Override
Expand Down Expand Up @@ -438,10 +476,16 @@ protected Map<DefaultQualifierKind, Set<DefaultQualifierKind>> createDirectSuper
nameToQualifierKind.get(Nullable.class.getCanonicalName());
DefaultQualifierKind nullnessOperatorUnspecified =
nameToQualifierKind.get(NullnessUnspecified.class.getCanonicalName());
DefaultQualifierKind parametricNullKind =
nameToQualifierKind.get(ParametricNull.class.getCanonicalName());

Map<DefaultQualifierKind, Set<DefaultQualifierKind>> supers = new HashMap<>();
supers.put(minusNullKind, singleton(nullnessOperatorUnspecified));
LinkedHashSet<DefaultQualifierKind> superOfMinusNull = new LinkedHashSet<>();
superOfMinusNull.add(nullnessOperatorUnspecified);
superOfMinusNull.add(parametricNullKind);
supers.put(minusNullKind, superOfMinusNull);
supers.put(nullnessOperatorUnspecified, singleton(unionNullKind));
supers.put(parametricNullKind, singleton(unionNullKind));
supers.put(unionNullKind, emptySet());
return supers;
/*
Expand All @@ -457,6 +501,16 @@ protected Map<DefaultQualifierKind, Set<DefaultQualifierKind>> createDirectSuper
}
};
}

@Override
public AnnotationMirror getParametricQualifier(AnnotationMirror qualifier) {
return parametricNull;
}

@Override
public boolean isParametricQualifier(AnnotationMirror qualifier) {
return areSame(parametricNull, qualifier);
}
}

@Override
Expand Down Expand Up @@ -706,6 +760,9 @@ private List<? extends AnnotatedTypeMirror> getUpperBounds(AnnotatedTypeMirror t
*
* My only worry is that I always worry about making calls to getAnnotatedType, as discussed in
* various comments in this file (e.g., in NullSpecTreeAnnotator.visitMethodInvocation).
*
* This is likely caused by https://github.com/eisop/checker-framework/issues/737.
* Revisit this once that issue is fixed.
*/
if (type instanceof AnnotatedTypeVariable
&& !isCapturedTypeVariable(type.getUnderlyingType())) {
Expand Down Expand Up @@ -861,8 +918,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 :)

|| use.hasEffectiveAnnotation(nullnessOperatorUnspecified)) {
substitute.replaceAnnotation(nullnessOperatorUnspecified);
}

Expand Down
27 changes: 27 additions & 0 deletions src/main/java/com/google/jspecify/nullness/ParametricNull.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
// Copyright 2024 The JSpecify Authors
//
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
// http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.

package com.google.jspecify.nullness;

import static java.lang.annotation.ElementType.TYPE_USE;

import java.lang.annotation.Target;
import org.checkerframework.framework.qual.InvisibleQualifier;
import org.checkerframework.framework.qual.ParametricTypeVariableUseQualifier;

/** Internal implementation detail; not usable in user code. */
@Target(TYPE_USE)
@InvisibleQualifier
@ParametricTypeVariableUseQualifier(Nullable.class)
@interface ParametricNull {}
2 changes: 2 additions & 0 deletions src/main/java/com/google/jspecify/nullness/Util.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,6 +51,7 @@ final class Util {
final AnnotationMirror minusNull;
final AnnotationMirror unionNull;
final AnnotationMirror nullnessOperatorUnspecified;
final AnnotationMirror parametricNull;

final TypeElement javaUtilCollectionElement;
final ExecutableElement collectionToArrayNoArgElement;
Expand Down Expand Up @@ -116,6 +117,7 @@ final class Util {
minusNull = AnnotationBuilder.fromClass(e, MinusNull.class);
unionNull = AnnotationBuilder.fromClass(e, Nullable.class);
nullnessOperatorUnspecified = AnnotationBuilder.fromClass(e, NullnessUnspecified.class);
parametricNull = AnnotationBuilder.fromClass(e, ParametricNull.class);
/*
* Note that all the above annotations must be on the *classpath*, not just the *processorpath*.
* That's because, even if we change fromClass to fromName, AnnotationBuilder ultimately calls
Expand Down
13 changes: 7 additions & 6 deletions src/test/java/tests/ConformanceTest.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -161,12 +161,13 @@ static final class DetailMessageReportedFact extends ReportedFact {
"assignment.type.incompatible",
"atomicreference.must.include.null",
"cast.unsafe",
"lambda.param",
"methodref.receiver.bound",
"methodref.receiver",
"methodref.return",
"override.param",
"override.return",
"lambda.param.type.incompatible",
"methodref.receiver.bound.invalid",
"methodref.receiver.invalid",
"methodref.return.invalid",
"override.param.invalid",
"override.receiver.invalid",
"override.return.invalid",
"return.type.incompatible",
"threadlocal.must.include.null",
"type.argument.type.incompatible");
Expand Down
22 changes: 11 additions & 11 deletions tests/ConformanceTestOnSamples-report.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
# 67 pass; 506 fail; 573 total; 11.7% score
# 73 pass; 500 fail; 573 total; 12.7% score
FAIL: AnnotatedInnerOfNonParameterized.java: no unexpected facts
FAIL: AnnotatedInnerOfParameterized.java: no unexpected facts
FAIL: AnnotatedReceiver.java: no unexpected facts
Expand All @@ -14,15 +14,15 @@ FAIL: ArraySubtype.java: no unexpected facts
PASS: AssignmentAsExpression.java: no unexpected facts
PASS: AugmentedInferenceAgreesWithBaseInference.java:35:jspecify_nullness_mismatch
PASS: AugmentedInferenceAgreesWithBaseInference.java: no unexpected facts
FAIL: BoundedTypeVariableReturn.java:27:jspecify_nullness_mismatch
FAIL: BoundedTypeVariableReturn.java:32:jspecify_nullness_mismatch
PASS: BoundedTypeVariableReturn.java:27:jspecify_nullness_mismatch
PASS: BoundedTypeVariableReturn.java:32:jspecify_nullness_mismatch
PASS: BoundedTypeVariableReturn.java: no unexpected facts
FAIL: CaptureAsInferredTypeArgument.java:51:jspecify_nullness_mismatch
FAIL: CaptureAsInferredTypeArgument.java:53:jspecify_nullness_mismatch
FAIL: CaptureAsInferredTypeArgument.java:61:jspecify_nullness_mismatch
FAIL: CaptureAsInferredTypeArgument.java:63:jspecify_nullness_mismatch
FAIL: CaptureAsInferredTypeArgument.java: no unexpected facts
FAIL: CaptureConversionForSubtyping.java: no unexpected facts
PASS: CaptureConversionForSubtyping.java: no unexpected facts
FAIL: CaptureConvertedToObject.java:71:jspecify_nullness_mismatch
FAIL: CaptureConvertedToObject.java: no unexpected facts
FAIL: CaptureConvertedToObjectUnionNull.java: no unexpected facts
Expand Down Expand Up @@ -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
PASS: CastOfCaptureOfUnboundedWildcardForObjectBoundedTypeParameter.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.

FAIL: CastToPrimitive.java:33:jspecify_nullness_mismatch
FAIL: CastToPrimitive.java: no unexpected facts
FAIL: CastWildcardToTypeVariable.java:23:jspecify_nullness_mismatch
PASS: CastWildcardToTypeVariable.java:23:jspecify_nullness_mismatch
PASS: CastWildcardToTypeVariable.java: no unexpected facts
PASS: Catch.java: no unexpected facts
PASS: ClassLiteral.java: no unexpected facts
Expand Down Expand Up @@ -116,10 +116,10 @@ FAIL: ContainmentSuperVsExtends.java:24:jspecify_nullness_mismatch
FAIL: ContainmentSuperVsExtends.java: no unexpected facts
FAIL: ContainmentSuperVsExtendsSameType.java:23:jspecify_nullness_mismatch
FAIL: ContainmentSuperVsExtendsSameType.java: no unexpected facts
FAIL: ContravariantReturns.java:30:jspecify_nullness_mismatch
FAIL: ContravariantReturns.java:34:jspecify_nullness_mismatch
FAIL: ContravariantReturns.java:38:jspecify_nullness_mismatch
FAIL: ContravariantReturns.java: no unexpected facts
PASS: ContravariantReturns.java:30:jspecify_nullness_mismatch
PASS: ContravariantReturns.java:34:jspecify_nullness_mismatch
PASS: ContravariantReturns.java:38:jspecify_nullness_mismatch
PASS: ContravariantReturns.java: no unexpected facts
PASS: CovariantReturns.java: no unexpected facts
FAIL: DereferenceClass.java:33:jspecify_nullness_mismatch
FAIL: DereferenceClass.java: no unexpected facts
Expand Down Expand Up @@ -303,7 +303,7 @@ FAIL: NullLiteralToTypeVariableUnionNull.java: no unexpected facts
FAIL: NullLiteralToTypeVariableUnspec.java: no unexpected facts
FAIL: NullMarkedDirectUseOfNotNullMarkedBoundedTypeVariable.java: no unexpected facts
PASS: NullUnmarkedUndoesNullMarked.java: no unexpected facts
PASS: NullUnmarkedUndoesNullMarkedForWildcards.java: no unexpected facts
FAIL: NullUnmarkedUndoesNullMarkedForWildcards.java: no unexpected facts
PASS: NullnessDoesNotAffectOverloadSelection.java:23:jspecify_nullness_mismatch
Copy link
Collaborator Author

Choose a reason for hiding this comment

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

This line contains a jspecify_nullness_not_enough_information marker.
I get as error:

NullUnmarkedUndoesNullMarkedForWildcards.java:25: error: [argument.type.incompatible] incompatible argument for parameter o of NullUnmarkedUndoesNullMarkedForWildcards.acceptObject.
    acceptObject(supplier.get());
                             ^
  found   : Object?
  required: Object
1 error

The Object? seems wrong, as the wildcard bound should become unspecified.
However, there is an error marker... should I change something about the test case?

Copy link
Collaborator

Choose a reason for hiding this comment

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

There appears to be a lot going on here.

First: I would have expected:

  found   : Object*
  required: Object

I think that's what you're saying, as well.

This seems familiar: I think that the reason that NullUnmarkedUndoesNullMarkedForWildcards exists is that I had wanted to define @NullMarked as something like "nullnessOperatorUnspecified for location ALL." But that turns out not to work when the enclosing scope is @NullMarked: @NullMarked configures unionNull for UNBOUNDED_WILDCARD_UPPER_BOUND, and UNBOUNDED_WILDCARD_UPPER_BOUND is more specific than ALL, even though it's on a wider scope. Or something like that? The populateNewDefaults method in NullSpecAnnotatedTypeFactory.java discusses this. Perhaps you just need to do this TODO?

Copy link
Collaborator

Choose a reason for hiding this comment

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

As for the fact that it's an error:

That much is expected. It's only the types that are wrong.

Our checker doesn't actually issue "warnings." It issues only errors. The cases that we would think of as "warnings" are cases where the checker issues an error in strict mode but no error in lenient mode. (That's in contrast to "real" errors, which are errors in both modes.)

This is what I was getting at in jspecify/jspecify#486 (comment).

As I note there, the conformance-test framework doesn't support jspecify_nullness_not_enough_information. Since IIRC the conformance-test framework current runs only in strict mode, it could be made to treat jspecify_nullness_not_enough_information exactly like jspecify_nullness_mismatch, since both of those comments indicate lines that should be errors in strict mode.

If we were to make the conformance-test framework treat jspecify_nullness_not_enough_information in that way, then the test here would begin to pass. It would still be passing for the wrong reason (since it has the types wrong), but we wouldn't notice until we also run the conformance tests in lenient mode. Once we do, it would fail: It would appear there as an unexpected error in lenient mode. Or at least I'd hope so :) (We should be able to see it fail now if we run the old-style samples integration that you'd put into place.)

Copy link
Collaborator

Choose a reason for hiding this comment

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

But things get more interesting from there....

The current head checker is likely also doing this wrong! I built it and ran ./demo -Astrict on this test, and:

NullUnmarkedUndoesNullMarkedForWildcards.java:25: error: [nullness] possible null dereference on type Supplier<? extends Object*>*
    acceptObject(supplier.get());
                 ^
1 error

That's true! Since the method is @NullUnmarked, supplier has unspecified nullness, so the call to get() itself is not provably safe, independent of what we do with the result!

(Hmm, so main-eisop should probably be producing that error, too!)

To make that accidental error go away, we should probably change the sample to:

default void apply(@NonNull Supplier<?> supplier) {

(Or we could insert a null check in the body of the method.)

But... where's the error that we actually wanted, the one about converting from Object* to Object in the return statement? It looks like that error is missing at head. I wonder if it ever worked or if we only ever had the null-dereference error, which was enough to satisfy the tests? (This is definitely one reason to like a testing approach that can be more specific about what kind of error it expects....)

Copy link
Collaborator

Choose a reason for hiding this comment

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

Perhaps you just need to do this TODO?

Sorry, I was looking at main-eisop there and not this PR.... Here's where this PR does it. It looks right to me at first blush:

jspecify-reference-checker/src/main/java/com/google/jspecify/nullness/NullSpecAnnotatedTypeFactory.java

Line 154 in 41a4ce4

TypeUseLocation.IMPLICIT_WILDCARD_UPPER_BOUND_NO_SUPER,

PASS: NullnessDoesNotAffectOverloadSelection.java: no unexpected facts
PASS: ObjectAsSuperOfTypeVariable.java:35:jspecify_nullness_mismatch
Expand Down
26 changes: 26 additions & 0 deletions tests/minimal/Issue159.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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.

//
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
// http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.

// Test case for Issue 159:
// https://github.com/jspecify/jspecify-reference-checker/issues/159

import java.util.ArrayList;
import org.jspecify.annotations.NullMarked;

@NullMarked
class Issue159<E> extends ArrayList<E> {
<F> Issue159<F> foo() {
return new Issue159<F>();
}
}
31 changes: 31 additions & 0 deletions tests/minimal/Issue163.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
// Copyright 2024 The JSpecify Authors
//
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
// http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.

// Test case for Issue 163:
// https://github.com/jspecify/jspecify-reference-checker/issues/163

import org.jspecify.annotations.NullMarked;

@NullMarked
class Issue163NullForUnspecVoid {
void x(Issue163Value val, Issue163Visitor<Void> vis) {
val.accept(vis, null);
}
}

interface Issue163Value {
<P> void accept(Issue163Visitor<P> visitor, P param);
}

interface Issue163Visitor<P> {}
Loading
Loading