Nullness checker false negative related to capture conversion

[cushon]

The nullness checker doesn't report any diagnostics for the following program, which fails at runtime with an NPE:

import org.checkerframework.checker.nullness.qual.Nullable;

interface C<T> {
  T get();
}

interface X {
  C<? extends Object> get();
}

interface Y extends X {
  @Override
  C<? super Object> get(); // should be an error
}

class A {
  public static void main(String[] args) {
    C<@Nullable Object> c = () -> null;
    Y y = () -> c;
    X x = y;
    x.get().get().toString(); // NPE
  }
}

$ ./checker-framework-3.21.1/checker/bin/javac -processor org.checkerframework.checker.nullness.NullnessChecker A.java
$ java A
Exception in thread "main" java.lang.NullPointerException
        at A.main(A.java:21)

[smillst]

Thanks for reporting!

The problem is that javac "captures" C<? super Object> to C<Object>. (I think this is a javac bug, that I thought we reported, but I can't find it.) This happens when the super bound of a wildcard is the same as the upper bound of the type parameter for which it is an argument. I noticed this problem when implementing capture conversion. (We have some tests in checker/tests/tainting/SameTypeBounds.java.)

The Checker Framework works around this by using the the super bound as the annotation on the new type argument. So C< @Nullable ? super @NonNull Object> becomes C<@NonNull Object>. This is unsound as demonstrated in this example. The Checker Framework should also require that super bounds that are captured in this way have the same annotations on the super and extends bounds. So, in this example, the Checker Framework should issue an invalid type error on C< @Nullable ? super @NonNull Object>.

(The TODOs in checker/tests/tainting/SameTypeBounds.java mention adding this error, but I could find an issue for them.)

[smillst]

I found a javac bug report with this problem: https://bugs.openjdk.java.net/browse/JDK-8054309.