Soundly handle must call obligations with unknown must call methods

[kelloggm]

Fixes #5908.

I'm investigating the false positive in the "correct" version of the test case separately, because I can reproduce it with just the Called Methods Checker (and it's more important to close the soundness loophole).

This PR also changes the defaulting scheme used for type variable upperbounds. See the documentation.

Merge with codespecs/daikon#492 and plume-lib/plume-util#314.

[msridhar]

I am ok with getting this change in to fix the soundness bug. However, if we can fix the false positive in the near future, that would be good too. Without that I'm not sure there is a good way to work around the new warnings other than a suppression.

[kelloggm]

@msridhar this needs to be re-reviewed, because CI failed. The failure occurred because this change introduced new typechecking errors from the RLC in the Checker Framework itself. I've removed those by writing some @MustCall({}) annotations, but they're indicative of the sort of pain this change is likely to cause users in generic-heavy code. I wrote a manual subsection about the problem with some examples, too, so that users are hopefully not too confused.

I would prefer to handle this problem by defaulting type variables to @MustCall({}) rather than @MustCallUnknown. I tried to do that in MustCallTypeAnnotator, but didn't succeed; I'm not sure what the appropriate API would be (and I'm also not sure doing so will be sound). @smillst, do you know if there is an easy way to change the defaulting rules for type variables? The current defaulting is especially painful for local variables, so I'd also appreciate a solution that just works for those.

[msridhar]

@kelloggm I'm a little concerned about these new warnings and the impacts they are going to have on users, particularly since the warnings seem to appear in code that has nothing to do with resource management. I think we should spend a bit of time trying to see if we can change defaulting of type variables to avoid these issues.

[kelloggm]

I think we should spend a bit of time trying to see if we can change defaulting of type variables to avoid these issues.

I agree. But, I figured adding them here would make the scope of the problem clear. I'd prefer a version of this PR with no new annotations but which does a better job defaulting type variables.

[smillst]

I was able to change some of the required.method.not.known errors into required.method.not.called errors.

As far as type variable defaulting, you can make the upper bound of type variables @MustCall({}) by adding TypeUseLocation.UPPER_BOUND} to @DefaultFor({TypeUseLocation.EXCEPTION_PARAMETER) to MustCall.java. You may not want to do that though. (Try it and see all the errors.)

What about changing the default of return types that are type variables to @NotOwning. It looks like most of the errors are coming from returned values. I looked at the code, but I couldn't figure out where to make that change.

For example:

public class RLTypeVarDefaulting<R, P> {
  public final R method( P p) {
    R r = other(p);
    return null;
  }

  // Add @NotOwning to the return type and the error in `method` goes away.
  private R other(P p) {
    return null;
  }
}

[kelloggm]

@smillst, thanks for your suggestions. Here are some notes on these two alternatives; I'd appreciate your (and @msridhar's) help in deciding which of them to take.

What about changing the default of return types that are type variables to @NotOwning. It looks like most of the errors are coming from returned values. I looked at the code, but I couldn't figure out where to make that change.

I looked into doing this. It's technically possible and relatively easy (the change would need to be made in MustCallConsistencyAnalyzer#shouldTrackReturnType, around line 1640 - add a case that checks if the return type is a type variable). I've implemented it on the branch issue5908-not-owning-on-typevar-returns of my fork, if you'd like to take a look.

The problem is that this causes some tests to fail, in a way that suggests to me that this change might be unsound. In particular, the following tests fail:

    3 expected diagnostics were not found:
      ACSocketTest.java:156: error: (required.method.not.called)
      ACSocketTest.java:160: error: (required.method.not.called)
      EnhancedFor.java:33: error: (required.method.not.called)

In each of these cases, we have something like List<Socket> list and then some method that produces a Socket is called, e.g., List#get. In each case, the tests expect that an error ought to be issued (we've produced a seemingly-new Socket!). Since we don't allow List<@Owning Socket>, maybe this is okay and the expected behavior, but I am surprised by it and I suspect some users will be too. I haven't been able to write a test case that actually demonstrates unsoundness based on this, though, so it might be that I'm just nervous because we'd be changing the checker's behavior.

As far as type variable defaulting, you can make the upper bound of type variables @MustCall({}) by adding TypeUseLocation.UPPER_BOUND} to @DefaultFor({TypeUseLocation.EXCEPTION_PARAMETER) to MustCall.java. You may not want to do that though. (Try it and see all the errors.)

I looked into this too, in some detail. The number of new warnings is actually not as large as your comment suggested it might be, and this change actually would remove a large number of false positives in the Checker Framework itself (i.e., would remove warning suppressions) without introducing any new false positives. So, I think we ought to seriously consider it. You can look at the changes yourself on the issue5908-change-defaults branch of my fork.

The problem with this change is that it becomes an error to write List<Socket> and any other use of a type variable where the type argument itself isn't @MustCall({}). That gives the programmer a few (bad) choices when encountering a situation where they need to do so:

• write List<@MustCall Socket>. This makes it an error to actually add a Socket to the list, since the type of the Socket is @MustCall("close") but the list requires an empty @MustCall. Obviously not great, but it matches our design philosophy that the RLC doesn't support lists of @Owning resources.
• write List<? extends Socket>. This similarly precludes calls to add or other methods that require an instance of the type variable, but it preserves some of the behavior. This is the best choice most of the time, I think.
• suppress some warnings

One thing that I do like about this option is that it limits the false positives to code that actually uses a resource, which is extremely desirable. On the other hand, though, it doesn't give the programmer any real tools to verify code that uses arbitrarily-sized collections of resources (but, as @Calvin-L discovered in #5969, this is already true of the RLC).

[msridhar]

Re-approving the changes. This is assuming nothing needs to be re-reviewed @kelloggm

[mernst]

I don't understand "and any other use of a type variable", since this paragraph has not yet used a type variable. Maybe a concrete code example would help.

[mernst]

@smillst Could you take a look at the code changes to determine the interactions with your explicit-extends-object branch?

[smillst]

@smillst Could you take a look at the code changes to determine the interactions with your explicit-extends-object branch?

This pull request makes explicit and implicit upper bounds use the same default, so nothing in this branch will need to change. In the explicit-extends-object, any extends @MustCall Object can be removed. If there are other annotations on the upper bound, @MustCall can be removed. (This changes could be made in master after this pull request is merged.)

[mernst]

@smillst Great, thanks for confirming.