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

Fix lower bound of type variables and unspecified subtypes. #175

Merged
merged 9 commits into from
Apr 22, 2024
Merged

Fix lower bound of type variables and unspecified subtypes. #175

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
9fef70b
Adapt to changes in https://github.com/eisop/checker-framework/pull/739
wmdietl Apr 14, 2024
d3198a3
Add regression test case; adapt to API changes
wmdietl Apr 14, 2024
9c70df2
Remove accesses and assertions that are no longer needed.
wmdietl Apr 14, 2024
4011143
Run the regression tests
wmdietl Apr 14, 2024
c8a671e
Include "kind" in output; remove debugging output
wmdietl Apr 15, 2024
f44acb0
Adapt nullness annotation/comment; undo changes to hashCode/equals.
wmdietl Apr 16, 2024
651689e
Fix lower bound of type variables and unspecified subtypes.
wmdietl Apr 16, 2024
8a40027
Merge branch 'main-eisop' of github.com:jspecify/jspecify-reference-c…
wmdietl Apr 22, 2024
9e27b8f
Use suggested alternative implementation
wmdietl Apr 22, 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
16 changes: 10 additions & 6 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 @@ -14,7 +14,7 @@

package com.google.jspecify.nullness;

import static com.google.jspecify.nullness.NullSpecAnnotatedTypeFactory.IsDeclaredOrArray.IS_DECLARED_OR_ARRAY;
import static com.google.jspecify.nullness.NullSpecAnnotatedTypeFactory.IsDeclaredOrArrayOrNull.IS_DECLARED_OR_ARRAY_OR_NULL;
import static com.google.jspecify.nullness.Util.nameMatches;
import static com.sun.source.tree.Tree.Kind.IDENTIFIER;
import static com.sun.source.tree.Tree.Kind.MEMBER_SELECT;
Expand All @@ -29,6 +29,7 @@
import static javax.lang.model.element.ElementKind.ENUM_CONSTANT;
import static javax.lang.model.type.TypeKind.ARRAY;
import static javax.lang.model.type.TypeKind.DECLARED;
import static javax.lang.model.type.TypeKind.NULL;
import static javax.lang.model.type.TypeKind.TYPEVAR;
import static javax.lang.model.type.TypeKind.WILDCARD;
import static org.checkerframework.framework.util.AnnotatedTypes.asSuper;
Expand Down Expand Up @@ -139,7 +140,6 @@ final class NullSpecAnnotatedTypeFactory
new TypeUseLocation[] {
TypeUseLocation.CONSTRUCTOR_RESULT,
TypeUseLocation.EXCEPTION_PARAMETER,
TypeUseLocation.IMPLICIT_LOWER_BOUND,
TypeUseLocation.RECEIVER,
};

Expand All @@ -152,6 +152,10 @@ final class NullSpecAnnotatedTypeFactory

private static final TypeUseLocation[] defaultLocationsUnspecified =
new TypeUseLocation[] {
// Lower bounds could be MinusNull, but all uses in unmarked code would become unspecified
// anyways.
// Revisit once https://github.com/eisop/checker-framework/issues/741 is fixed.
TypeUseLocation.IMPLICIT_LOWER_BOUND,
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 order of TypeUseLocation enums matters and they are applied in declaration order.
I think what is happening is that the IMPLICIT_LOWER_BOUND default is applied first and then the TYPE_VARIABLE_USE has nothing left to do.
The inconsistency between the two constants is confusing anyways, so I think it makes sense to move this here.

I've filed eisop/checker-framework#741 to think more about this.

Copy link
Collaborator

Choose a reason for hiding this comment

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

On eisop/checker-framework#741:

Ah, I do remember issues with the ordering, now that you mention it, probably as documented here:

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

Lines 843 to 847 in fae43cf

* OTHERWISE covers anything that does not have a more specific default inherited from an
* enclosing element (or, of course, a more specific default that we set below in this
* method). If this is a @NullUnmarked element, then it might have a had a @NullMarked
* enclosing element, which would have set a default for UNBOUNDED_WILDCARD_UPPER_BOUND. So
* we make sure to override that here.

(And of course this is what the "Ensure that all locations that appear in the defaultLocations" comment above is saying, too. So I'm not saying anything new here :))

In that case, I wanted to override a specific location's value from an enclosing type with a general value at a smaller scope. As a result, I had to also override the specific location's value.

Here, I think we're talking about two values at the same scope, and the overlap is a Venn diagram: Some implicit lower bounds are type-variable uses, and some type-variable uses are implicit lower bounds. (In my case, by contrast, "every UNBOUNDED_WILDCARD_UPPER_BOUND was an OTHERWISE," so to speak.)

I say all that because a possible solution to my problem was to give priority to defaults from smaller scopes. Here, though, that wouldn't help, assuming that I've understood correctly.

On this PR more generally:

I would have guessed that there were two separate defaulting steps: one for the lower bound of E and one for the use of E itself. And my thinking is that minusNull is right for the lower bound but that unspecified is right for the use. Is the problem that, once the defaulting system defaults the lower bound, it decides not to default the use of E itself? Does the entire idea of defaulting those two things separately indicate that I'm working from a different mental model than the Checker Framework does?

That's probably it? This may get back into how substitution works differently (currently!) in the Checker Framework and JSpecify: Once the Checker Framework has an annotation for the use of a type variable, I think it applies that annotation to both of the bounds there? In contrast, JSpecify would say that "E" has a lower bound of minusNull but that "this use of E" has unspecified nullness.

(So, backing up to the eisop question for a moment: It's probably not worth trying to accommodate this case unless we decide that we want to keep the JSpecify behavior as it is—and maybe not even then.)

So this seems in line with the other hacks I've put in as part of forcing the weird JSpecify substitution behavior. It might result in slightly weird error messages by our standards (with null* instead of null)—still only when errors are triggered by some separate, real problem—but that's exactly the kind of thing that we can live with. And it may go away as we revisit substitution.

TypeUseLocation.IMPLICIT_WILDCARD_UPPER_BOUND_NO_SUPER,
TypeUseLocation.TYPE_VARIABLE_USE,
TypeUseLocation.OTHERWISE
Expand Down Expand Up @@ -699,7 +703,7 @@ && isNullInclusiveUnderEveryParameterization(
}

boolean isNullExclusiveUnderEveryParameterization(AnnotatedTypeMirror type) {
return nullnessEstablishingPathExists(type, IS_DECLARED_OR_ARRAY);
return nullnessEstablishingPathExists(type, IS_DECLARED_OR_ARRAY_OR_NULL);
}

private boolean nullnessEstablishingPathExists(
Expand Down Expand Up @@ -1852,12 +1856,12 @@ private AnnotatedDeclaredType createType(TypeElement element) {

// Avoid lambdas so that our Predicates can have a useful toString() for logging purposes.

enum IsDeclaredOrArray implements Predicate<TypeMirror> {
IS_DECLARED_OR_ARRAY;
enum IsDeclaredOrArrayOrNull implements Predicate<TypeMirror> {
IS_DECLARED_OR_ARRAY_OR_NULL;

@Override
public boolean test(TypeMirror t) {
return t.getKind() == DECLARED || t.getKind() == ARRAY;
return t.getKind() == DECLARED || t.getKind() == ARRAY || t.getKind() == NULL;
}
}

Expand Down
33 changes: 33 additions & 0 deletions tests/regression/Issue172.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
// 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 172:
// https://github.com/jspecify/jspecify-reference-checker/issues/172

import org.jspecify.annotations.NullMarked;

class Issue172<E> {
E e() {
return null;
}
}

class Issue172UnmarkedUse {
void foo(Issue172<Object> p) {}
}

@NullMarked
class Issue172MarkedUse {
void foo(Issue172<Object> p) {}
}
Loading