CLIMB-to-top and annotated libraries

[GoogleCodeExporter]

This code

  List<@Nullable String> lns = Arrays.asList("foo", null, "bar");

should type-check because of the annotated JDK, which contains:

  class Arrays {
    public static <T> List<T> asList(T... a);
  }

That JDK annotation should be equivalent to

   public static <T extends @Nullable Object> List<T> asList(T... a);

because of the CLIMB-to-top defaulting rule.

A test case appears at 
checker-framework/checker/tests/nullness/AnnotatedJdkTest.java

Original issue reported on code.google.com by michael.ernst@gmail.com on 30 Sep 2014 at 7:16

[GoogleCodeExporter]

From bytecode it's impossible to tell if <T> is extends bounded or not since 
they all appear as <T extends Object> if they were not.  Therefore, 
QualifierDefaults assumes that any type parameter from bytecode is an EXPLICIT 
bound.  Therefore, without explicitly placing a nullable on the bound, it will 
not typecheck.   

Original comment by jbu...@cs.washington.edu on 30 Sep 2014 at 5:22

[GoogleCodeExporter]

I agree there is no way to tell from the bytecode.  I was thinking that when 
the classfile/.jar version of the annotated JDK is constructed from the source 
code, different annotations could be inserted in the classfile based on whether 
the bound was explicit or implicit in the annotated JDK source code.  That is, 
I was proposing a change to the construction of the annotated JDK, not a change 
in the way that classfile/.jar libraries are read at type-checking time.

Original comment by michael.ernst@gmail.com on 30 Sep 2014 at 6:32

[GoogleCodeExporter]

I've mentioned this before, but this is an issue we've noticed frequently. I 
just got a question today about:

private static <T> Iterable<T> foo() {
  return Collections.<T>emptyList();
}

Is there any chance you'd consider the second option, i.e. changing the way 
classfile/.jar libraries are read?

We have a large amount of code that declares type parameters with implicit 
bounds (<T>) and gets compiled to <T extends Object>, and very very little code 
that uses <T extends Object> in source. Having to write <T extends @NonNull 
Object> in the cases where it's desired would be an improvement for us.

Original comment by cus...@google.com on 6 Oct 2014 at 2:57

[GoogleCodeExporter]

I believe that you are proposing the following:

  When reading from classfiles (but not in other circumstances), if an upper bound is of Java type Object and has no annotation, then treat the upper bound as having the top annotation.  For the nullness type system, this would be @Nullable.  Make no changes in other situations, including those where the upper bound is not Object and those where the upper bound is Object but has an annotation.

This seems fine to me.  The fix to put the correct annotation (@NonNull or 
@Nullable, depending on whether the upper bound was explicit) in the classfile 
would be better, but also might be more work to implement.  Once the better fix 
is in place, this rule will not have any effect, which will be fine.  This rule 
will only affect legacy libraries for which there are no annotations available.

Original comment by michael.ernst@gmail.com on 7 Oct 2014 at 9:02

[GoogleCodeExporter]

Yes, thanks - that's what I was trying to describe.

Original comment by cus...@google.com on 7 Oct 2014 at 3:19

[GoogleCodeExporter]

We do know whether the T is explicit or implicit in source.
We started storing annotations in bytecode to support exactly this distinction: 
if we compiled the code, we can choose the explicit/implicit default and then 
store that in the bytecode.

I think at the moment the annotated JDK creation doesn't actually run the type 
checkers - we neither verify that the annotations are well-formed, nor do we 
apply defaulting.
We should change the creation process to implement both.

Also see:
https://groups.google.com/d/msg/checker-framework-dev/fVpVQyeInJw/-UVyDeiULdsJ

Original comment by wdi...@gmail.com on 14 Oct 2014 at 4:20

[GoogleCodeExporter]

This issue has grown into two separate parts, and I propose to split them in 
order to keep the issue manageable.

1. How to put better annotations into annotated libraries.  That's what is 
referred to by the title of the issue, and we'll keep that part here.

2. How to deal with *un*annotated libraries.  That belongs with issue #12.  
I'll move my comment #4, above, to issue #12.

Original comment by michael.ernst@gmail.com on 16 Oct 2014 at 3:46