Spurious [dereference.of.nullable] for object under initialization?

[DrMicrobit]

Hi,

I've made a file with minimal examples to follow along this potential issue which I tested with CheckerFramework 3.51.0.

000_nullness_spurious.tar.gz

Untar, this creates subdirectory 000_nullness_spurious, there will be two subdirectories: 01_compilesand 02_hascompileerror. In each subdirectory simply do mvn clean compile to either see the successful compile or the compile error.

In each case there are to .java files: Command.java is simply declaring a @Command annotation interface, while the file producing the spurious compiler error is SimpleCliParser.java.

Case that works (01_compiles)

(lines commented out in this file are there to keep line numbering consistent with the case that will produce the error later on).

package com.bjtrain.parser;

import java.util.Objects;
import org.checkerframework.checker.initialization.qual.UnderInitialization;
// import org.checkerframework.checker.nullness.qual.EnsuresNonNull;
import org.checkerframework.checker.nullness.qual.NonNull;

public final class SimpleCliParser<T> {
  public static <T> SimpleCliParser<T> create(final Class<T> commandClass) {
    return new SimpleCliParser<>(commandClass);
  }

  // private @NonNull Integer mmMetadata;
  private final @NonNull Class<T> mmCommandClass;

  private SimpleCliParser(final @NonNull Class<T> commandClass) {
    mmCommandClass = Objects.requireNonNull(commandClass, "Command class cannot be null");
    subScpInitMetadata();
  }

  // @EnsuresNonNull({"mmMetadata"})
  private void subScpInitMetadata(SimpleCliParser<T> this) {
    final Command commandAnnotation = mmCommandClass.getAnnotation(Command.class);
    if (commandAnnotation == null) {
      throw new IllegalArgumentException(
          "The provided class " + mmCommandClass.getName() + " is not annotated with @Command.");
    }
    // mmMetadata = 99;
  }
}

You will see that this class has no default constructor, a factory method create() returns an initialised object. create() calls the private constructor SimpleCliParser(), which in turn will call a helper function subScpInitMetadata().

Proof(?) that CompilerFramework "does the expected thing"
Any SimpleCliParser object has only one field: mmCommandClass. That field is initialised as very first step by the constructor SimpleCliParser(), and I gave three times (I think) the information that this field cannot be null by the time subScpInitMetadata() is called:

1. via a combination of finaland @NonNull in the field declaration (line 14)
2. via @NonNull added to the parameter of the constructor (line 16)
3. via an additional Objects.requireNonNull() in the assignment on line 17

Apparently, CheckerFramework picks up that information and everything compiles, including the helper function subScpInitMetadata() called from the constructor which successfully uses the field in line 23 like this final Command commandAnnotation = mmCommandClass.getAnnotation(Command.class);.

Indeed, were I to change line 22 from

private void subScpInitMetadata(SimpleCliParser<T> this) {

to

private void subScpInitMetadata(@UnderInitialization SimpleCliParser<T> this) {

then CheckerFramework would abort with the following error:

SimpleCliParser.java:[18,22] error: [method.invocation] call to subScpInitMetadata() not allowed on the given receiver.
[ERROR]   found   : @Initialized @NonNull SimpleCliParser<T extends @Initialized @Nullable Object>
[ERROR]   required: @UnderInitialization @NonNull SimpleCliParser<T extends @Initialized @Nullable Object>

Basically telling me d'oh, dear user, you claim the object is not fully initialised when calling subScpInitMetadata()? But I totally have deduced that it is as the only field mmCommandClass is final and was initialised beforehand. Silly user!

Ok, perfect, CheckerFramework does what it should do.

Case that does not work (02_hascompileerror)

Now the "spurious" error case I cannot explain:

package com.bjtrain.parser;

import java.util.Objects;
import org.checkerframework.checker.initialization.qual.UnderInitialization;
import org.checkerframework.checker.nullness.qual.EnsuresNonNull;
import org.checkerframework.checker.nullness.qual.NonNull;

public final class SimpleCliParser<T> {
  public static <T> SimpleCliParser<T> create(final Class<T> commandClass) {
    return new SimpleCliParser<>(commandClass);
  }

  private @NonNull Integer mmMetadata;
  private final @NonNull Class<T> mmCommandClass;

  private SimpleCliParser(final @NonNull Class<T> commandClass) {
    mmCommandClass = Objects.requireNonNull(commandClass, "Command class cannot be null");
    subScpInitMetadata();
  }

  @EnsuresNonNull({"mmMetadata"})
  private void subScpInitMetadata(@UnderInitialization SimpleCliParser<T> this) {
    final Command commandAnnotation = mmCommandClass.getAnnotation(Command.class);
    if (commandAnnotation == null) {
      throw new IllegalArgumentException(
          "The provided class " + mmCommandClass.getName() + " is not annotated with @Command.");
    }
    mmMetadata = 99;
  }
}

Note that in this version, there is an additional field mmMetadata in the object. Logic of the class is such that this field should be initialised by the helper function.
Additionally, declaration of the helper function (lines 21 and 22) is changed to tell CheckerFramework what is should expect: a function that ensures that mmMetadata will be initialised, and that this is still being initialised at that point in time.

However, I am now getting a compiler error for subScpInitMetadata():

SimpleCliParser.java:[23,38] error: [dereference.of.nullable] dereference of possibly-null reference mmCommandClass

This puzzles me: the successful compilation of line 23 in the previous example showed that CheckerFramework apparently had deduced that mmCommandClass cannot be null when subScpInitMetadata() is called, but now it tells me that there possibly is a null reference.

Have I done something wrong or is that a bug in CheckerFramework?

[DrMicrobit]

Addendum: workaround

Looking further into the issue, I just found out about @MonotonicNonNulland @RequiresNonNull.

So, I should have declared private final @MonotonicNonNull Class<T> mmCommandClass; instead of @NonNull. Or leave the annotation out completely, as final fields are treated to be monotonic anyway (as per manual).

However, that does not resolve the compiler error.

But what does resolve the compiler error (for me, inexplicably so) is ... adding @RequiresNonNull to the helper function like so:

  @RequiresNonNull("mmCommandClass")
  @EnsuresNonNull({"mmMetadata"})
  private void subScpInitMetadata(@UnderInitialization SimpleCliParser<T> this) {
    final Command commandAnnotation = mmCommandClass.getAnnotation(Command.class);
    if (commandAnnotation == null) {
      throw new IllegalArgumentException(
          "The provided class " + mmCommandClass.getName() + " is not annotated with @Command.");
    }
    mmMetadata = 99;
  }

At this point I would argue that this feels like a bug of the CheckerFramework? Or I am seriously missing something.