Sound behavior for array creation expressions with @NonNull element type

The Nullness Checker is unsound by default with respect to array creation expressions. When an array, whose element type is @NonNull, is constructed, the Checker Framework does not guarantee that all elements get initialized. Therefore, array indexing expressions such as a[i] may have @NonNull type but null values, leading to missed alarms (unsoundness). This behavior is because we believe that sound behavior would lead to too many false alarms, which would irritate users and lead them not to carefully examine the warnings.

The Nullness Checker can be made sound by via the -Alint=forbidnonnullarraycomponents command-line argument. This enforces that every non-empty array must be constructed with an @Nullable or @LazyNonNull element type. In other words, new @NonNull Object[10] is illegal, because the newly-constructed array does have nulls in it. The best one can do is new @LazyNonNull Object[10].

I propose that we make -Alint=forbidnonnullarraycomponents the default, via the following steps:

• We perform case studies with the -Alint=forbidnonnullarraycomponents. This will reveal how many false positive warnings the Nullness Checker issues, where the program fully initializes the array, immediately after the array creation expression.
• We add special-case checks to the Nullness Checker, to eliminate those false positive warnings. For example, one such check would pattern-match for certain varieties of for loop containing array element initialization a[i] = ... right after the array creation expression. Either flow-sensitive type refinement would change the array's element type to @NonNull, or the original declaration with a @NonNull element type would be permitted when immediately followed by such a for loop.
• We add, to the manual, advice to programmers about how to write their initialization loops in order to avoid false positive warnings (and to avoid exposing the partially-initialized array)
• We remove the forbidnonnullarraycomponents lint option from the code and the manual. Users can write -AsuppressWarnings=new.array.type.invalid to go back to the old behavior. Hopefully the false positive rate will be low enough that few programmers will do so.

Start with the Nullness Checker and the existing -Alint=forbidnonnullarraycomponents behavior, then run case studies to measure false positives from array initialization. Review the manual guidance and determine the needed special cases before making the lint the default; done means the option is removed and users can still suppress the resulting warning as described.