Precondition check on field from superclass

[wmdietl]

Take the following example:

import org.checkerframework.checker.nullness.qual.EnsuresNonNull;
import org.checkerframework.checker.nullness.qual.RequiresNonNull;
import org.checkerframework.checker.initialization.qual.UnknownInitialization;

class Parent {
  protected Integer foo;

  public Parent() {
    initFields();
  }

  @EnsuresNonNull("foo")
  private void initFields(@UnknownInitialization Parent this) {
    foo = 42;
  }
}

class Child extends Parent {
  private String bar;

  public Child() {
    // super constructor implicitly called, foo initialized
    initFields();
  }

  @RequiresNonNull("foo")
  @EnsuresNonNull("bar")
  private void initFields(@UnknownInitialization Child this) {
    bar = String.valueOf(foo);
  }

  private void foom() {
    // assert foo != null : "@AssumeAssertion(nullness)"; // SHOULDN'T BE NECESSARY!
    initFields();
  }
}

Running the Nullness Checker produces:

Parent.java:34: error: [contracts.precondition.not.satisfied] initFields's precondition about 'this.foo' is not satisfied
    initFields();
              ^

Which seems like a false positive: the receiver of method foom is fully initialized, so the pre-condition is established.

I first thought it might have to do with the receiver of initFields being @UnknownInitialization, but the following simpler example type checks without error:

import org.checkerframework.checker.nullness.qual.EnsuresNonNull;
import org.checkerframework.checker.nullness.qual.RequiresNonNull;
import org.checkerframework.checker.initialization.qual.UnknownInitialization;

class One {
  private Integer foo;
  private String bar;

  public One() {
    foo = 42;
    initFields();
  }

  @RequiresNonNull("foo")
  @EnsuresNonNull("bar")
  private void initFields(@UnknownInitialization(Object.class) One this) {
    bar = String.valueOf(foo);
  }

  private void foom() {
    initFields();
  }
}

So it seems to be related to the field being from the superclass.

This example is a minimized version of the issue reported in https://groups.google.com/d/msg/checker-framework-discuss/Vauq_jzUFyE/cFBPp6tYCQAJ

[wmdietl]

@Sadaf91 will look into this issue.

[olegshtch]

I got some maybe related issue. It is possible to declare that some super method calls child method initializes fields?

import org.checkerframework.checker.initialization.qual.UnderInitialization;
import org.checkerframework.checker.nullness.qual.EnsuresNonNull;

abstract class Parent {
  public final void reload(@UnderInitialization(Parent.class) Parent this) {
    reloadExt();
  }

  protected abstract void reloadExt(@UnderInitialization(Parent.class) Parent this);
}

class Child extends Parent {
  private Object field;

  // error: [initialization.fields.uninitialized] the constructor does not initialize fields: field
  Child() {
    reload();
  }

  @Override
  @EnsuresNonNull("field")
  protected void reloadExt(@UnderInitialization(Parent.class) Child this) {
    field = new Object();
  }
}

[mernst]

@olegshtch Your issue is related, but isn't exactly the same as the previous examples. So it's nice to have this example as well. In your example, the Parent class knows nothing about the Child class, so it cannot have specifications that refer to Child class fields. It cannot even say "is fully initialized up for Child, because it doesn't know about Child and some other subclass could violate the property. Because some other subclass could violate the property, your code really is unsafe.

As a matter of style, it's best to do initialization in the constructor. That can be made safe, and the Initialization Checker can verify its safety. The Nullness Checker can verify this code:

import org.checkerframework.checker.initialization.qual.UnderInitialization;
import org.checkerframework.checker.nullness.qual.EnsuresNonNull;

abstract class Parent {

  Parent() {
    reloadParent();
  }

  public final void reloadParent(@UnderInitialization(Parent.class) Parent this) {
  }
}

class Child extends Parent {
  private Object field;

  // error: [initialization.fields.uninitialized] the constructor does not initialize fields: field
  Child() {
    super();
    reloadChild();
  }

  @EnsuresNonNull("field")
  protected void reloadChild(@UnderInitialization(Parent.class) Child this) {
    field = new Object();
  }
}