Mutators cause false positives in the nullness checker

[sxlijin]

The nullness checker appears to be unable to determine that mutators do not modify a given variable. A minimal example that can be used to prove this:

import org.checkerframework.checker.nullness.qual.Nullable;
import java.util.ArrayList;

class Foo {
    static class Bar {
        Object a = new Object();
        void mutate() { a = new Object(); }
    }
    
    Bar b = new Bar();
    @Nullable Object o = null;
    
    void foo() {
        if (o == null) return;
        b.mutate();
        o.hashCode();
    }
}

The real-world example where this came up was something like:

List<Node> nodes = new ArrayList<>();
InterestingType a = null;
void loop() {
  ...
  if (a == null) {
    a = nonNullThing;
    nodes.add(buildNode());
    a.doThing();
  }
  ...
}

[mernst]

The nullness checker appears to be unable to determine that mutators do not modify a given variable.

While checking one method, the Nullness Checker does not do inference of side effects for other methods.
Rather, the Nullness Checker verifies programmer-written annotations.

If you use a fact when reasoning about your code, you need to express that fact as an annotation.

The manual section "Side effects" describes several ways to express that a mutator does not set a variable to null, including:

• @SideEffectFree
• @MonotonicNonNull
• @EnsuresNonNull

It seems that @MonotonicNonNull might be appropriate for your real-world example.
I'm closing this issue, but let us know if the manual is not clear.

[sxlijin]

That is... very surprising.

I remember that it took me a long time to track this down. Is there any way to perhaps propagate this information up to the resulting error, so that users at least know where to look?

[mernst]

Could you clarify what is the very surprising part?

Issue #982 is a proposal to give users more information about the fact that side-effecting methods may set fields. Would that have helped you?

There is also #984, but that assumes the user is thinking about side effects.