false negative when encountering recursive bound

[theosotr]

Command

javac \        
  -J--add-exports=jdk.compiler/com.sun.tools.javac.api=ALL-UNNAMED \
  -J--add-exports=jdk.compiler/com.sun.tools.javac.code=ALL-UNNAMED \
  -J--add-exports=jdk.compiler/com.sun.tools.javac.file=ALL-UNNAMED \
  -J--add-exports=jdk.compiler/com.sun.tools.javac.main=ALL-UNNAMED \
  -J--add-exports=jdk.compiler/com.sun.tools.javac.model=ALL-UNNAMED \
  -J--add-exports=jdk.compiler/com.sun.tools.javac.processing=ALL-UNNAMED \
  -J--add-exports=jdk.compiler/com.sun.tools.javac.tree=ALL-UNNAMED \
  -J--add-exports=jdk.compiler/com.sun.tools.javac.util=ALL-UNNAMED \
  -J--add-opens=jdk.compiler/com.sun.tools.javac.comp=ALL-UNNAMED \
-processor org.checkerframework.checker.nullness.NullnessChecker \
-cp checker-framework/checker/dist/checker.jar  Test.java

File

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


class A<T> {
    public static <T extends Comparable<? super T>> A<T> m(T k) {
        k.toString();
        return new A<T>();
    }
}

public class Test {
    public static void main(String[] args) {
        A.m(null);
    }
}

Actual behavior

The code passes the checks but there's a NPE at runtime

Exception in thread "main" java.lang.NullPointerException: Cannot invoke "java.lang.Comparable.toString()" because "<parameter1>" is null
        at A.m(Test.java:6)
        at Test.main(Test.java:13)

Expected behavior

The code should have been rejected.

[smillst]

Thanks for reporting!

The bug seems to be with the special handling of the null literal in the type argument inference algorithm:

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

class Issue6815<T> {
     static <T extends Comparable<? super T>> Issue6815<T> m(T k) {
      k.toString();
      return new Issue6815<T>();
    }
    void method1(@Nullable Integer i) {
      Issue6815.m(i);  // true positive
    }
    void method2() {
      Issue6815.m(null);  // false negative
    }
  }