Initialized state when calling super methods

[mtf90]

Consider the following code:

class Sup {

    private final int a;
    private final int b;

    public Sup(int a, int b) {
        this.a = a;
        this.b = b;
    }

    public int compute() {
        return this.a + this.b;
    }
}

class Sub extends Sup {

    private final int c;

    public Sub(int a, int b) {
        super(a, b);
        this.c = super.compute();
    }

    @Override
    public int compute() {
        return c;
    }
}

When checking this code with the default NullnessChecker, I get the following error

[ERROR] Failed to execute goal org.apache.maven.plugins:maven-compiler-plugin:3.8.1:compile (cf-compile) on project cf-test: Compilation failure
[ERROR] /media/storage/workspace/cf-test/src/main/java/com/github/mtf90/Sub.java:[9,30] error: [method.invocation.invalid] call to compute() not allowed on the given receiver.
[ERROR]   found   : @UnderInitialization(com.github.mtf90.Sub.class) @NonNull Sup
[ERROR]   required: @Initialized @NonNull Sup

According to the documentation on partial initialization (esp. case 3) Sup's constructor has completed and therefore when treated as Sup (we call Sup's version of compute) its state should be @Initialized, right?

If I refactor Sup#compute to

public int compute(@UnknownInitialization(Sup.class) Sup this) {
    return this.a + this.b;
}

I have to refactor the Sub#compute method as well. However, here I have to write

@Override
public int compute(@UnknownInitialization(Sup.class) Sub this) {
    return c;
}

which doesn't seem correct, because I need all fields of Sub to be initialized for this method to work properly. However, the check (wrongfully?) passes. Writing

@Override
public int compute(@UnknownInitialization(Sub.class) Sub this) {
    return c;
}

would be correct for the method, but then the checker (rightfully) throws an error due to parameter contra-variance.

Am I missing something or is this a bug in the detection logic? I used version 3.7.0 via Maven. If necessary I can share the project in a repo.

[mernst]

Thanks for your issue report. I'm sorry you are having trouble.
Also thanks for the clear, concise example code you provided.

First example

In your code as given, the error message is correct. This declaration:

class Sup {
    public int compute() { ... }
}

states that compute requires a fully-initialized receiver. The message states the mismatch:

Test.java:24: error: [method.invocation.invalid] call to compute() not allowed on the given receiver.
        this.c = super.compute();
                              ^
  found   : @UnderInitialization(Sub.class) @NonNull Sup
  required: @Initialized @NonNull Sup

Sup's constructor has completed and therefore when treated as Sup (we call Sup's version of compute) its state should be @Initialized, right?

No, @UnderInitialization(Sub.class) Sup cannot be used where an @Initialized Sup is required.
Permitting that would be unsound. For example, it would permit this code:

public class Test {
    public static void main(String[] args) {
        new Sub(1, 2);
    }
}

class Sup {

    final int a;
    final int b;

    public Sup(int a, int b) {
        this.a = a;
        this.b = b;
    }

    public int compute() {
        System.out.printf("called Sup.compute %s %s%n", a, b);
        return this.a + this.b + compute2();
    }

    public int compute2() {
        System.out.printf("called Sup.compute2 %s %s%n", a, b);
        return 0;
    }
}

class Sub extends Sup {

    final int c;
    final int d;

    public Sub(int a, int b) {
        super(a, b);
        this.c = super.compute();
        this.d = 1;
    }

        @Override
    public int compute() {
        System.out.printf("called Sub.compute %s %s %s %s%n", a, b, c, d);
        return c;
    }

    @Override
    public int compute2() {
        System.out.printf("called Sub.compute2 %s %s %s %s%n", a, b, c, d);
        return c / d;
    }
}

I see that the text in the manual is misleading. (It was trying to be colloquial and imprecise, but it did not convey the key ideas clearly.)

I have opened pull request #3810 to improve it and to add an example. Can you take a look to see if that addresses your concern?

Please let me know if you can suggest any other improvements to the documentation.

Second example

The Initialization Checker is focused on ensuring correct assignment of fields in constructors with respect to preventing null pointer exceptions, as opposed to other types of initialization errors. Thus, it neglected to check accesses to fields fields of primitive type outside of constructors.

I have updated the manual (in pull request #3810) to clarify the scope of the Initialization Checker, which was not clear. Again, your comments on that are welcome.

I agree with your bug report: expanding the scope of the Initialization Checker would be a good enhancement. It would then reject any fields that are currently implicitly initialized to null, 0, or false. You could open a separate issue for that feature request.

[mtf90]

Thanks @mernst for your response. Don't feel sorry, even as-is your tool already helped us a lot :).

With your version of the example, I can see that this error message would make sense, because compute() now adds a dependency to (the overridden) compute2() that depends on Sub and therefore isn't properly initialized during Sub's constructor. However, this is a crucial change compared to my example: In my situation, the usage of super.compute() looks sound to me, because it doesn't depend on any overridden functionality. I don't know the details of your analysis process, but I would have hoped that it somehow detected that Sup#compute is some kind of "pure" function that is safe to use. Maybe this goes in line with your suggestion to ramp up the Initialization Checker to support this kind of analysis? Or should I use something like the @Pure annotation for this?

After all, I am just looking for a way to make the checks pass without any errors (and preferably without using @SuppressWarnings). Maybe I am on the completely wrong track and you can suggest something entirely different?

Regarding your changes towards the documentation: I think it disarms some of the traps I fell victim to. I think what previously threw me off was the concept of "when treated as A". Since Java always uses dynamic dispatching (compared to, e.g., C++) treating an object as A (e.g., via A a = new B();) doesn't differ from treating it as B. Maybe reiterating this fact would further clarify the situation.

Come to think of it, when instantiating y as new A();, shouldn't @UnderInitialization(A.class) A y; guarantee that y.get() is always non-null? According to the documentation, a class C becomes @UnderInitialization(C) only after all non-null fields have been initialized. So in this case, get() is also guaranteed to return non-null, right?

But this would mean that you can't really rely on any declaration type of a variable but instead require a full data-flow analysis everytime. I can understand if you default to a pessimistic world assumption ("it could always be a sub type") to keep things more managable for now. (But again: stating this fact somewhere would help understanding the decision process of the checker).

Other than that, I only asked myself if return aField(); / return bField(); shouldn't be return aField; / return bField; instead? Or are these some language features I am not aware of?

[mernst]

In my situation, the usage of super.compute() looks sound to me, because it doesn't depend on any overridden functionality. I don't know the details of your analysis process, but I would have hoped that it somehow detected that Sup#compute is some kind of "pure" function that is safe to use.

The analysis doesn't detect this. The most important thing to understand about type-checking is that it is modular. While analyzing one method, the analysis only uses the signatures of other methods; it does not look into the implementation of any other method.

So, while analyzing

    public Sub(int a, int b) {
        super(a, b);
        this.c = super.compute();
    }

the type-checker only uses the signature of compute().

It would be possible to enrich the Nullness Checker's annotation language, so that the signature of compute() can be more informative.

I think you are suggesting a @NoDispatch method annotation. If written on a method m() in class C:

• The implementations of m() may not perform dynamic dispatch.
• Callers of m() may pass a receiver of type @UnderInitialization(C.class) or @UnknownInitialization(C.class).

This would be possible, but it would be necessary to more precisely define it. (I have not thought through the details.)
We only implement new features if they arise sufficiently often in practice -- is this very common for you, or an uncommon case?

If it is uncommon, you could suppress the warning with an explanation of why the code is correct despite the false positive warning that arises due to the fact that the Nullness Checker's specification language is not exhaustive.

shouldn't @UnderInitialization(A.class) A y; guarantee that y.get() is always non-null?

No. y.get() might evaluate to <null> because the run-time type of y might be B. That is, y and z might refer to the same value, just as w and x might refer to the same value.

I slightly misquoted you, because you actually asked:

when instantiating y as new A();, shouldn't @UnderInitialization(A.class) A y; guarantee that y.get() is always non-null?

The first clause of your sentence is irrelevant. Given a variable, the type-checker knows its type, but the type-checker does not re-analyze all paths through the program to determine richer facts than the type.
It would be possible to enrich the Nullness Checker by introducing a new type beyond @UnderInitialization -- for instance, it might also carry information about the run-time class.
This would require a more formal definition of the semantics; feel free to submit a proposal.

But this would mean that you can't really rely on any declaration type of a variable but instead require a full data-flow analysis everytime. I can understand if you default to a pessimistic world assumption ("it could always be a sub type") to keep things more managable for now. (But again: stating this fact somewhere would help understanding the decision process of the checker).

Yes, you are correct. Type-checking examines types, not the data flow that produced the type.
The text in the manual about "modular analysis" is intended to express this. I added it explicitly in a few more places.

Other than that, I only asked myself if return aField(); / return bField(); shouldn't be return aField; / return bField; instead? Or are these some language features I am not aware of?

That was a typo from editing the code after pasting it in from my IDE. Thanks for catching my goof.

[mtf90]

Ok, with this kind of analysis the error message makes sense then. So this issue is not so much a bug report anymore but a feature request if anything. However, this is not very pressing for us as it only affects a single instance. I was just on a bug-crusade and wondered if there was a way to work-around the report of this seemingly safe case.

Enhancing the type-checker with something like a @NoDispatch annotation could definitely help. Although, I don't know if NoDispatch is a concise term for this: It could mean the method itself should not be dispatched (dynamically) or the method (body) should not dispatch to any other methods. For the first case, I can already mark the method as final and use on-board Java language features. Maybe something like @NoDelegation fits better?

I was also thinking about, wether or not you actually need an annotation. For example, the framework already detects if constructors call (overridable) methods, so the same (or similar) check could be used for this use-case. But with constructors you probably never want to call other methods, whereas delegation is generally fine with normal methods. Also, annotated (parent) methods would make it easier to detect whether or not sub-classes break this contract.

Anyway, at this point this is just brainstorming. Feel free to tag this issue as a (low-level) feature request or close it since your changes on the documentation should address the source of confusion for this issue. And thank you for your thorough explanations.

[mernst]

I'm glad that things are clearer now. Thanks for prompting me to improve the documentation.

with constructors you probably never want to call other methods,

In practice, constructors calling methods is not uncommon. If it never happened, there would be less need for the Initialization Checker.
But I agree with you that code is easier to understand when constructors do not call methods.

I will close this issue for now, but others may find the discussion helpful.
One useful followup would be enhancing the Initialization Checker to track all fields rather than just @NonNull fields. (This may have performance implications.)
Another possible followup is adding an annotation along the lines of @NoDelegation indicating that the method implementation does no dynamic dispatch. That would eliminate the false positive warning that you encountered.

[mernst]

Version 3.8.0 of the Checker Framework contains an Initialized Fields Checker that warns when a field is not initialized by a constructor. This is more general than the Initialization Checker, which only checks that @NonNull fields are initialized. It addresses the second example in this issue.