Strange behavior in Nullness Checker

[wadoon]

Following code only works if I use a intermediate variable to store the result.

Here is non-working code:

  @Override
    public VariableCondition build(@NonNull Object[] arguments, List<String> parameters, boolean negated) {
        if (negated && !negationSupported) {
            throw new RuntimeException(clazz.getName() + " does not support negation.");
        }

        Object[] args = Objects.requireNonNull(arguments);
        if (negationSupported) {
            args = Arrays.copyOf(arguments, arguments.length + 1);
            args[args.length - 1] = negated;
        }

Here is the working code (var a = ...):

  @Override
    public VariableCondition build(@NonNull Object[] arguments, List<String> parameters, boolean negated) {
        if (negated && !negationSupported) {
            throw new RuntimeException(clazz.getName() + " does not support negation.");
        }

        Object[] args = Objects.requireNonNull(arguments);
        if (negationSupported) {
            var a = Arrays.copyOf(arguments, arguments.length + 1);
            args = a;
            args[args.length - 1] = negated;
        }

The error message is:

/home/weigl/work/key/key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/ConstructorBasedBuilder.java:50: error: [assignment.type.incompatible] incompatible types in assignment.
            args = Arrays.copyOf(arguments, arguments.length + 1);
                                ^
  found   : @Nullable Object @NonNull []
  required: @NonNull Object @Nullable

The snippet comes form the KeY-project

Eiop used via Gradle plugin:

Note: The Checker Framework is tested with JDK 8, 11, 17, and 21. You are using version 23.
Note: Checker Framework 3.42.0-eisop5

[Ao-senXiong]

Thanks for your report!

I see the problem because the annotations are not correct in the annotated JDK.

For copyof method, we are returning a @Nullable T.
https://github.com/eisop/jdk/blob/2a5380ebe75fbfc4a26169a682f0418694aa6d50/src/java.base/share/classes/java/util/Arrays.java#L3524

When you use a local variable, it is started as @Nullable and refined to the rhs. That's why use a intermediate variable is working.

I think we should annotate copyof method's return and parameter type as @PolyNull and that will make the method return what is passed in as expeceted by a copy.

@wmdietl how do you think?

[wadoon]

The JDK describes that in Arrays.copyOf(original, length), original is non-null.

So I would say @NonNull is the way to go.

[wmdietl]

Both the original array and the returned array are already implicitly NonNull, so there is nothing to change there.

The question is about the right annotation for the array component type.
Type parameter T allows nullable and non-null component types.
The return type forces the component type of the return array to @Nullable T, always making the array components in the result nullable.

This is required, as the size of the copy could be larger than the original array. As the javadoc states @return a copy of the original array, truncated or padded with nulls to obtain the specified length.

The example in the first post is actually an example of this: in Arrays.copyOf(arguments, arguments.length + 1) even if all elements in arguments are non-null, the last element in the copy will definitely be null, because that last element is filled with a null padding.

So, the error without a local variable seems correct to me, as there is a mismatch in the array component type.
If anything, the lack of a warning when using var seems like a false negative to me.
Take this code:

import java.util.Arrays;

public class Demo {
  static void foo(Object[] args) {
     var a = Arrays.copyOf(args, args.length + 1);
     args = a;
     args[args.length - 1].toString();
  }
  
  public static void main(String[] args) {
      foo(new Object[] {""});
  }
}

This passes the Nullness Checker, but when running results in an NPE.
This seems specific to the usage of var, the correct error is raised when using an explicit type for a.

The JDK for the two Arrays.copyOf methods should have a comment about the additional logic in

checker-framework/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitAnnotatedTypeFactory.java

Line 759 in 1799158

if (TreeUtils.isArrayLengthAccess(lengthArg)) {

which tries to refine the return type when it is safe to do so.
However, that logic correctly does not refine the type in the call in these examples here.
@Ao-senXiong Can you create a PR that adds those comments?

[Ao-senXiong]

@wmdietl Thanks, see eisop/jdk#109.