Add an option to support correct positioning of type use annotations on arrays, even outside JSpecify mode

[agentgt]

I normally use Checkerframework and Eclipse for null checking so apologies on my ignorance and or if this is a known issue.

I have field like:

protected @Nullable String[] kvs;

https://github.com/jstachio/rainbowgum/blob/31c71243eef1661513516938005a064663930bf2/core/src/main/java/io/jstach/rainbowgum/KeyValues.java#L378

I get a compiler error here

https://github.com/jstachio/rainbowgum/blob/31c71243eef1661513516938005a064663930bf2/core/src/main/java/io/jstach/rainbowgum/KeyValues.java#L396

rainbowgum/core/src/main/java/io/jstach/rainbowgum/KeyValues.java:[396,26] [NullAway] dereferenced expression kvs is @Nullable

I'm using the Eclipse TYPE_USE annotations and mostly following JSpecify. It appears that Nullaway thinks that kvs is nullable and not the elements. Perhaps if I switch to the JSpecify annotations it will know that it means the elements or not?

It works with Eclipse null analysis and Checkerframework.

[agentgt]

OK apparently after looking around I think it is because I don't have JSpecifyMode turned on.

So I guess we can close this bug (I did find other issues with generics but it appears those are a work in progress).

[msridhar]

Hi @agentgt thanks for the report. I think there is a real issue here that we should fix. NullAway has traditionally not had support for "correct" placement of type use annotations like those from JSpecify or Checker Framework. As you noticed, our full support for JSpecify checking (under the JSpecifyMode flag) is not ready for prime time, and most likely it won't be fully ready for some time longer. But in the interim, since JSpecify 1.0 has been released, I think we should implement some flag that enables "strict" interpretation of type use annotation positions even with NullAway's normal checking. This would ensure, e.g., that you don't get unwanted errors for dereferences of an array itself when you annotate its elements as @Nullable. This might also impact varargs and is hence possibly related to #674. Without this "strict" mode, I'm afraid we may hold back proper use of JSpecify annotations by NullAway users. We will try to investigate, though it may be a couple of weeks before we can look.

[agentgt]

But in the interim, since JSpecify 1.0 has been released, I think we should implement some flag that enables "strict" interpretation of type use annotation positions even with NullAway's normal checking. This would ensure, e.g., that you don't get unwanted errors for dereferences of an array itself when you annotate its elements as @nullable.

@msridhar I wonder if you can just look at the annotation to see if it is TYPE_USE (and maybe only TYPE_USE to avoid ambiguity) thus avoiding the flag or at least do the correct guessing behavior when neither JSpecify or strict? Or perhaps that might just confuse folks even more.

That is I assume the original behavior is because NullAway was supporting the defunct JSR javax annotations (and friends).

Anyway thanks for the reply. I'll try to help in the future by using NullAway on my various projects in conjunction w/ checker + eclipse!

[msridhar]

@agentgt hrm, the issue is backwards compatibility. It's possible we have users who were using CF type use nullability annotations on arrays in the "wrong" place before, and it worked as they expected with NullAway. I'm not sure we want to introduce a bunch of new errors in their code when they upgrade. On the other hand, maybe it would be good to start getting people more used to the new locations? The problem with the flag approach is that folks might adopt JSpecify annotations but in the wrong way if they don't pass the flag.

@lazaroclapp @yuxincs thoughts here?

[msridhar]

Another thought here is we could add an opt-out flag rather than opt-in. So, by default, we assume type use annotations should be in the right place, but you can pass the flag to go back to "legacy" mode for backward compatibility. And eventually we remove that flag. I think I like this idea best.

[msridhar]

@agentgt FWIW this should be fixed now. I think the Eclipse @Nullable annotation is just type use, similar to JSpecify, so your original case should work as intended. If you test and see something different, please let us know.

[agentgt]

@msridhar I'll let you know next week. Thank you for all the work!