NullnessChecker false positive when using Comparator#nulls{First,Last}

[GoogleCodeExporter]

What steps will reproduce the problem?
Compile the attached Java class using `javac -processor 
org.checkerframework.checker.nullness.NullnessChecker -version -verbose 
-AprintErrorStack -AprintAllQualifiers NullableStringWrapper.java`

What is the expected output? What do you see instead?
I expect the class to compile successfully. Instead, the nullness analysis 
fails because the first arguments to Comparator#comparing and 
Comparator#thenComparing are functions that may return null. These errors are 
false positives because the second arguments to these methods are null-safe 
comparators.  

What version of the product are you using? On what operating system?
I built the "trunk" versions of jsr308-langtools, annotation-tools and 
checker-framework from source, as described in the manual, using jdk1.8.0_31. 
I'm running linux.

Please provide any additional information below.
I understand that the null-safety of the code depends crucially on the 
comparators used. In this case the code is safe, and it'd be great if the 
Checker Framework could detect that.

Original issue reported on code.google.com by stephan...@gmail.com on 28 Feb 2015 at 9:33

Attachments:

• NullableStringWrapper.java
• NullableStringWrapper-compiler-output.txt

[GoogleCodeExporter]

The log shows that I used version 1.8.9. Turns out this is because I used an 
old checkout of the code and performed only an `hg pull`, without an `hg 
update`. I just *properly* updated the working directory and re-ran the test 
using version 1.8.11. Can confirm the ticket is still valid.

Original comment by stephan...@gmail.com on 4 Mar 2015 at 9:51

[GoogleCodeExporter]

Thanks for the report! I can reproduce the issue.

Jonathan, I assigned this to you because type argument inference in the hacks 
repository crashes on this example. In the trunk version inference was 
imprecise, resulting in the false positive.

Original comment by wdi...@gmail.com on 17 Mar 2015 at 4:55

• Changed state: Accepted

[GoogleCodeExporter]

I'll take a look right now.

Original comment by jbu...@cs.washington.edu on 17 Mar 2015 at 9:19

[GoogleCodeExporter]

So there a couple of issues here:

1) We are missing annotations for the Java 8 Comparator in the Annotated JDK.  
I can add these no problem.
2) The crash in the type variable repo was occurring because of a failure in 
type argument inference. I have fixed the crashing issue in the type variable 
repo.  
3) However, though type argument inference will not crash, it will not lead to 
a correctly inferred type in these instances.  The issue is discussed below:

Suppose we have two methods:
<T> T getT() {}
<U> void setU(U u) {}

And a call to these methods:
setU(getT())

In this case, we would first try to infer T and we would u as the "assignedTo" 
value and create a constraint as follows:   T <: U

And then we would infer that the call to getT was actually of the form  
<U>getT()
Except U doesn't actually exist in the scope in which getT was called.  In the 
new type argument inference I was making the same mistake.  Because U is out of 
scope we encounter it in certain visitors in locations we would not expect it.  
This caused the exception in the type variables repo.

To correctly handle this, we would actually have to detect these cases and 
combine the inference of both T and U.  For instance say we had the following 
declarations:

<T> T getT(List<T> t) {}
<U> void setU(U u, List<U> u) {}

In Java (forgetting annotated types at the moment), this example would require 
us to use the type of T to determine U:
setU(getT(new ArrayList<String>()), null)

Whereas this example would require us top use the type of U to determine T:
setT(getU(null), new ArrayList<String>())

So, we need to actually solve for the two type arguments simultaneously.  The 
new type argument inference should make this much easier but the work is still 
non-trivial. 

For now, I am going to fix the crash.  In the long run I will fix type-argument 
inference to handle these cases and at that point this example should typecheck.

Original comment by jbu...@cs.washington.edu on 19 Mar 2015 at 10:38

[GoogleCodeExporter]

Thanks for taking the time to perform such an in-depth analysis. Very excited 
to hear the framework will at some point be able to handle this scenario!

Original comment by stephan...@gmail.com on 19 Mar 2015 at 10:42

[GoogleCodeExporter]

You're welcome.  Thanks for catching it.  We'll change this issue to pushed 
when this example typechecks.

Original comment by jbu...@cs.washington.edu on 19 Mar 2015 at 10:52

[GoogleCodeExporter]

Note that this is one improvement in Java 8 type argument inference. As 
discussed, rewriting the new annotated type argument inference to follow the 
Java 8 logic should solve this issue and better support lambdas as well.

Original comment by wdi...@gmail.com on 20 Mar 2015 at 2:15