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

Upstreaming: Additional configuration for substitution #4

Open
cpovirk opened this issue Oct 19, 2020 · 13 comments
Open

Upstreaming: Additional configuration for substitution #4

cpovirk opened this issue Oct 19, 2020 · 13 comments

Comments

@cpovirk
Copy link
Collaborator

cpovirk commented Oct 19, 2020

d1aba1c

CF already lets us override the TypeVariableSubstitutor, and we do so.

But our larger changes to substitution rules require changes to behavior even "before" substitution occurs. Notable, @NullnessUnspecified T (which is how we currently represent the type of a plain T when it appears in non-null-aware code) does not always have a nullness of "unspecified." That's because, if the type is instantiated with T set to a nullable type, the result must be @Nullable T. Therefore, it's not guaranteed safe to, e.g., dereference a value of type @NullnessUnspecified T, even in "lenient mode."

To upstream our current changes, we probably need to add methods to AnnotatedTypeFactory for the fixupBoundAnnotations methods in AnnotatedTypeMirror and for AsSuperVisitor to call.

Additionally, though, note that these changes do not make sense in isolation. They may invalidate assumptions in other parts of CF, so perhaps other code should be updated, too. (For example, is any of this related to jspecify/jspecify-reference-checker@89725d4#diff-ce82a59b06d0d82bfc6d06835d1b06ac15619bc3a71617d32189d041f02ca9c0R351? Or maybe that's caused by some other change I've made? Or maybe it will go away once we have dataflow implemented?) Or maybe the changes are just too weird to upstream without significantly more work, which we'd have to discuss.

Links:

@cpovirk
Copy link
Collaborator Author

cpovirk commented Oct 27, 2020

I just made another change in service of our unusual substitution rules. This one was "only" to formatting annotations, but of course that can be kind of important sometimes :)

See 5fc6c28.

@cpovirk
Copy link
Collaborator Author

cpovirk commented Nov 5, 2020

And another related change to formatting: e10a884.

@cpovirk
Copy link
Collaborator Author

cpovirk commented Nov 17, 2020

It might be that the right way to upstream this includes changing fixupBoundAnnotations() to:

  • modify the lower bound (but leave the upper bound untouched)
  • remove the annotation from the type-variable/wildcard usage itself

If we're lucky, such a change could eliminate the need for most of our existing nullness subtyping logic.

Aside: Even if we remove that logic, it's still nice to have written it:

  • It has helped validate our possible spec rules.
  • It has helped validate our sample inputs.
  • It could provide a jumping-off point for other non-GPL tools.

@cpovirk
Copy link
Collaborator Author

cpovirk commented Nov 17, 2020

(At this point, though, I am just handwaving: "Modify the lower bound" might mean "replace it with the value from the type-variable wildcard usage," or it might mean something more sophisticated with glb. Also, I've been thinking mostly in terms of ? extends wildcards (and "normal" type variables). Maybe things get more complicated in the case of ? super wildcards and their captures?)

cpovirk added a commit that referenced this issue Dec 1, 2020
…rules.

getErased() is called by getEffectiveAnnotations(), which is called by
getEffectiveAnnotationInHierarchy(), which is called by
DefaultTypeArgumentInference.clampToLowerBound().

Consequently, this commit fixes problems with inputs like the following:
jspecify/jspecify@9da93c5

This comes up in Guava. It also comes up in Truth (when compiled against
an annotated Guava).

This fix is probably the wrong thing: Ultimately, we should probably fix
the bounds themselves, as noted previously:
#4 (comment)

(So far, though, my efforts to fix that have triggered new problems.
Still, I should try more someday.)

I also note that, if I'm not mistaken, this commit *creates* an error in
Guava:

```
guava/src/com/google/common/collect/Sets.java:776: error: [nullness] incompatible parameter types for parameter 0 in lambda expression.
        return Stream.concat(set1.stream(), set2.stream().filter(e -> !set1.contains(e)));
                                                                 ^
  found   : ? extends E
  required: <captured wildcard>
```

That looks to be here:
https://github.com/google/guava/blob/7112c0339419289cf7175f304d092571c5913ec2/guava/src/com/google/common/collect/Sets.java#L778

Still, I'm seeing a net *decrease* in errors in Guava. Plus, I should be
able to remove some existing workarounds, like this one:
google/guava@189a410#diff-3ef68811fc409685d4bb4ce7c7551392290fcf9e01643b205e46b6bf97f2cce7R699
@cpovirk
Copy link
Collaborator Author

cpovirk commented Dec 1, 2020

Also ef726d7 (which notes that I should do better, as already discussed in the comments above).

@cpovirk
Copy link
Collaborator Author

cpovirk commented Dec 29, 2020

This continues to be the most concerning of our diffs from upstream. It periodically causes problems. I've made a few attempts to do things "the right way" as outlined above, but I've never quite gotten it to work. Hopefully I will someday.

Today in workarounds:

@cpovirk
Copy link
Collaborator Author

cpovirk commented Jan 14, 2021

@cpovirk
Copy link
Collaborator Author

cpovirk commented Jan 19, 2021

Possibly also jspecify/jspecify-reference-checker@559ba69, which notes that the problems there may run deeper than what I patched in that commit.

@cpovirk
Copy link
Collaborator Author

cpovirk commented Jan 19, 2021

I will likely give "the right way" another attempt after CF implements capture conversion. (They have an open PR.)

I say that after having made a few unsuccessful attempts at handling one edge case:
https://github.com/jspecify/jspecify/blob/08a36665a9d5897b7f29362091a0ac8cd5970392/samples/CastOfCaptureOfUnboundedWildcardForObjectBoundedTypeParameter.java#L24

Those attempts included jspecify/jspecify-reference-checker@9348e76 and jspecify/jspecify-reference-checker@364a2b1, both of which I reverted after finding that they caused other problems. The attempts also included a couple stabs at the wildcard handling of CFAbstractAnalysis.createAbstractValue (and, had that worked, possibly its type-variable handling, too). (I actually thought I had that working -- or at least producing a different error instead, which jspecify/jspecify-reference-checker@559ba69 was supposed to address? -- but I don't see it working now, so either I got confused, or I needed an additional part of the change. Hmm, maybe what I needed was my experimental implementation of NullSpecTransfer.visitTypeCast? That might actually have been it. Still, I've sunk way too much time into a case that I have seen only once so far in the real world -- particularly when that case might well go away if we solve the more general problem.

@cpovirk
Copy link
Collaborator Author

cpovirk commented Jan 20, 2021

Note that doing this "the right way" will likely involve reworking how we print types: Currently, we can always look up the "operator" (essentially, the "annotation") for a wildcard or type-variable usage directly on that type. Plus, we can assume that the bounds (which we print only in the case of a wildcard) are unmodified from the original bounds. But doing this "the right way" means removing the operator from the type itself (at least in the case of wildcards... I think?) and modifying the original bounds.

I'm vaguely optimistic that we will be able to (a) look up the original bounds and (b) "diff" them against the current bounds. Together, that may let us determine the operator/annotation that we actually want to print.

@cpovirk
Copy link
Collaborator Author

cpovirk commented Feb 5, 2021

I speculated yet again that we're causing ourselves issues. This time it was in jspecify/jspecify-reference-checker@31e1711#diff-1a347ba7cd35402d433b3ba1b9104e9f43add180c67b64844019b8eaccbedc8fR894 (and other comments above).

cpovirk added a commit to jspecify/jspecify that referenced this issue Jun 10, 2021
(Also, fix a type in the class name / filename of the sample that I
included with that fix.)

```java
TypeVariableMinusNullVsTypeVariable.java:53: error: [nullness] incompatible types in return.
      return cast.caching();
                         ^
  type of expression: NonnullSupplier<T!!>!!
  method return type: Supplier<T>!!
```

(This happens in both strict mode and lenient mode.)

This code is based on
https://github.com/google/guava/blob/08e8d34e304efc3040ba528337d396aaa11638be/guava/src/com/google/common/collect/Lists.java#L803

As discussed in the code comment in the new sample, I think I'm actually
OK with making this an error. It's not a useful error here, but it's
justifiable, and I expect it to be rare. If it turns out to be more
common (and still not useful), we should reconsider: The bug fixed by
the previous commit was also unlikely to be tickled by real code,
affected only code that already produced other warnings, and prevented
only warnings, not errors.

Now, Guava does see *other* new failures from the previous change.
However, they aren't enough to get me to revert it:

https://github.com/google/guava/blob/08e8d34e304efc3040ba528337d396aaa11638be/guava/src/com/google/common/collect/Iterables.java#L380
becomes an error, but that seems to be another bug, which, as usual, I
would start by blaming on
jspecify/checker-framework#4

https://github.com/google/guava/blob/08e8d34e304efc3040ba528337d396aaa11638be/guava/src/com/google/common/collect/Platform.java#L101
becomes _doubly_ an error, but again, there was already an error, and I
think that both are legitimately pointing out that I let my let the
annotations on `Arrays.copyOfRange` get out of sync with the annotations
there.

I want to at least test the previous commit more widely before backing
it out. If the problems run even deeper than I've realized, I'd like to
know.
copybara-service bot pushed a commit to google/auto that referenced this issue Jun 30, 2021
Specifically, wildcards defeat our ability to recognize that `containsKey` guarantees that `get` will return non-null.

See https://github.com/jspecify/nullness-checker-for-checker-framework/blob/a13e6921d6e23ec1349be007b5e9a6d1f279c91c/src/main/java/com/google/jspecify/nullness/NullSpecTransfer.java#L603

Without this CL, Auto-Common would break when I submit CL 382342656 to annotate the remaining immutable-map classes.

Arguably we should have a specific issue open for this problem, but:

- This may be the first time it's come up in practice.
- _Everything_ about wildcards in our checker is weird, thanks to a combination of the Checker Framework's unusual handling of them (which they are fixing by implementing capture conversion) and our hacks on top of that (which we hope can go away). (The very general project of "remove our hacks" is tracked by jspecify/checker-framework#4 (comment) and other issues there.)

RELNOTES=n/a
PiperOrigin-RevId: 382351496
copybara-service bot pushed a commit to google/auto that referenced this issue Jun 30, 2021
Specifically, wildcards defeat our ability to recognize that `containsKey` guarantees that `get` will return non-null.

See https://github.com/jspecify/nullness-checker-for-checker-framework/blob/a13e6921d6e23ec1349be007b5e9a6d1f279c91c/src/main/java/com/google/jspecify/nullness/NullSpecTransfer.java#L603

Without this CL, Auto-Common would break when I submit CL 382342656 to annotate the remaining immutable-map classes.

Arguably we should have a specific issue open for this problem, but:

- This may be the first time it's come up in practice.
- _Everything_ about wildcards in our checker is weird, thanks to a combination of the Checker Framework's unusual handling of them (which they are fixing by implementing capture conversion) and our hacks on top of that (which we hope can go away). (The very general project of "remove our hacks" is tracked by jspecify/checker-framework#4 (comment) and other issues there.)

RELNOTES=n/a
PiperOrigin-RevId: 382352859
@cpovirk
Copy link
Collaborator Author

cpovirk commented Jul 23, 2021

@cpovirk
Copy link
Collaborator Author

cpovirk commented Jan 10, 2022

Probably also 0a2de06

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

No branches or pull requests

1 participant