NullAway interprets type parameters differently from the checker framework (TCF)

[chengniansun]

In TCF, a type parameter that has no annotations is assumed to have a nullable upper bound. For example,

interface List<T> { T add(T t); }

I think T is assumed to be nullable.

Based on my experience with NullAway, the method parameter of add(T) is assumed to be @NonNull.

Please correct me if I am wrong.

[msridhar]

This is correct. Currently NullAway has no special support for generic types. See #54 for some initial ideas for how we could add some support for checking clients of generic types. Checking implementations of generic types would require further work.

[chengniansun]

Thanks, Manu, for the clarification.

If allowed, can I ask how your team manages false positives given this feature not implemented?

I am trying to annotate guava. However as the majority of guava is collection classes which extensively use generics, it is somehow difficult to annotate the code in a right way to pass NullAway.

[msridhar]

I don't think we've run into a situation where we had to annotate a library like Guava, with so many generic collection classes. We do have some internal generic collection classes, but we generally don't want to allow null values in them, so the default of @NonNull is fine.

I'd love to help find a good solution for Guava. Thinking out loud, maybe we can add a way to annotate a class such that NullAway uses @Nullable as the default annotation for that class rather than @NonNull? Maybe even just for generic type parameters? I don't think this would affect NullAway performance too much, though we'd have to test it out. The right solution here would be proper generics support, but that'll be a significant amount of work.

[chengniansun]

Thank you, Manu. Let me dig into that further, and get back to you.

I believe the right solution is also the support for generics. How much work is it going to be?

[msridhar]

Proper support for generics in the presence of subtyping is fairly non-trivial. Plus I really do not want to compromise the performance of NullAway on non-generic code, so some care is required. If I had to guess, I'd say that design + implementation + testing would take 4-6 weeks. I'd be very happy to help out if someone is willing to take this on, but I can't promise to do this personally anytime soon.

[chengniansun]

I also tried TCF, and it is indeed slow. Can you shed some lights on why TCF is slow? I know that NullAway supports a subset. Is it the Java generics that makes TCF slow?

[msridhar]

TCF's nullness checker is far more powerful (and sound) than NullAway. The framework is also general and not specialized to nullness checking, which probably has a performance cost. I think generics could be handled in NullAway without a significant performance cost. We would just want to be very careful about performance while implementing, as NullAway runs on every build of our code.

[kageiit]

@msridhar would it be possible to turn on expensive nullaway features on demand via some flags? We could make it possible for projects that use generics heavily to opt in to it as long as they understand some build time impact would be there.

[msridhar]

@kageiit my concern is that users of an annotated generic library get sensible behavior from NullAway no matter the configuration. Users may be confused if they need to opt in to more expensive checking to get safety when using the library. But yes, you could imagine ways that we could do this if we are careful.

@chengniansun to clarify, would an intermediate step of allowing for type parameters to be @Nullable by default (via opt in) be useful to you? Or is some kind of proper generics support required to handle Guava? I'm still thinking of whether we can do some kind of basic generics support that wouldn't be too much work.

Another question: are type use annotations allowed with D8, as long as they are CLASS retention and not RUNTIME? @kageiit?

[msridhar]

In TCF, a type parameter that has no annotations is assumed to have a nullable upper bound. For example, interface List { T add(T t); } I think T is assumed to be nullable.

@chengniansun are you sure about this? Look at TCF model for ArrayDeque. There is no annotation on the type parameter, but TCF gives a compile error when trying to stick null in an ArrayDeque (as it should). OTOH LinkedList, which does allow nulls, is written as class LinkedList<E extends @Nullable Object>.

[Stephan202]

From the documentation:

The most important annotations supported by the Nullness Checker are @NonNull and @Nullable. @NonNull is rarely written, because it is the default.

[chengniansun]

Thank you for your reply. Let me get back to you this afternoon.

[chengniansun]

@msridhar

I write the following code with ArrayDeque, and TCF emits no warnings.

public static void main(String[] args) { ArrayDeque<@Nullable String> q = new ArrayDeque<>(); q.add(null); q.offer(null); }

[chengniansun]

Hi Manu,

Please refer to $23.1.2 in the manual (https://checkerframework.org/manual/#polymorphism)

"Defaults If the extends clause is omitted, then the upper bound defaults to @TopType Object. If no type annotation is written on the type parameter name, then the lower bound defaults to @BottomType void. If the extends clause is written but contains no type qualifier, then the normal defaulting rules apply to the type in the extends clause (see Section 24.3.2).

These rules mean that even though in Java the following two declarations are equivalent:

class MyClass<T> class MyClass<T extends Object> they may specify different type qualifiers on the upper bound, depending on the type system’s defaulting rules."

[msridhar]

@chengniansun ok, the CF nullness type system is a bit complex :smile: I think a brief summary is that if you just have class Foo<T>, then a client can write Foo<@Nullable String> and CF allows it and type checks the client code appropriately. So I think your original statement is correct.

When NullAway supports generics, this might be a reasonable default. On the one hand, it'd be good to match what CF does. On the other hand, it might be safer to block client code from writing Foo<@Nullable String> unless there is some specific opt-in in class Foo. At the least, there should be a way to explicitly prohibit writing Foo<@Nullable String> (e.g., ArrayDeque<@Nullable String> should be prohibited).

Is your work on annotating Guava for NullAway still blocked without proper generics support? As I mentioned, adding that support will take us some time, but if there's any intermediate step you think we could take, please let us know.

[chengniansun]

Regarding ArrayDeque, I filed a bug at https://github.com/typetools/checker-framework/issues/1714#issuecomment-353184393

[chengniansun]

Thank you, Manu. I would vote to match CF's behavior, just for the sake of consistency, after all CF is also used here.

Yes, I am blocked, but it is okay. Currently, I am just evaluating NullAway and CF to see whether we can enable them by default. If we decide to use NullAway, I can contribute code too.