typetools / checker-framework

Pluggable type-checking for Java
http://checkerframework.org/
Other
1.01k stars 353 forks source link

@NotOnlyInitialized does not support 1:N circular references #4543

Open sooniln opened 3 years ago

sooniln commented 3 years ago
public class Test {

  final ArrayList<Child> children = new ArrayList<>();

  Test() {
    // assignment.type.incompatible
    children.add(new Child(this));
  }

  static final class Child {
    final @NotOnlyInitialized Object parent;

    protected Child(@UnknownInitialization Object parent) {
      this.parent = parent;
    }
  }
}

Results in:

error: [argument.type.incompatible] incompatible argument for parameter e of add.
    children.add(new Child(this));
                 ^
  found   : @UnderInitialization(com.google.android.gms.thunderbird.worker.Test.Child.class) @NonNull Child
  required: @Initialized @NonNull Child

I don't quite understand the root cause of this, so it's difficult to say what the proper solution is... The obvious solution would be to apply @NotOnlyInitialized to the type parameter of childern, ie: ArrayList<@NotOnlyInitialized Child> children. However, NotOnlyInitialized is not currently a type-use annotation, and I'm not even sure if would be sound to apply the annotation like this or not.

More deeply however, I do not understand why the result of new Child(...) is UnderInitialization - why does the following fail?

public class Test {

  final Child child;

  Test() {
    // assignment.type.incompatible
    child = new Child(this);
  }

  static final class Child {
    final @NotOnlyInitialized Object parent;

    protected Child(@UnknownInitialization Object parent) {
      this.parent = parent;
    }
  }
}

It seems to me that after new Child(this) is invoked, the result of that expression should be Initialized. The Child class is final, there are no possible subclasses, and every NonNull field within Child has obviously been initialized. This meets the definition of Initialized as given in the documentation. Is this because Initialized also implies that all fields within the type must also be Initialized? If so, this doesn't appear to be documented anywhere I can find. The only related sentence in the manual reads, "Eventually, when all constructors complete, the type is @Initialized." However there are never any details given on how it's determined when constructors are complete, and at what point after that a type is considered initialized. In the example above, all constructors have clearly completed it seems to me, and yet the type is considered UnderInitialization instead of Initialized.

This problem is vaguely referenced in the manual section on circular references, where the parent field is annotated with NotOnlyInitialized in order to avoid the problem, but it is never explained why this is necessary, and it comes across as magic code.

jpschewe commented 3 years ago

This looks to be the same issue that I'm seeing at #4568. I have a work around referenced there, however like you I would like to understand why the object "child" isn't initialized right away.