Annotating reentrancy with Java Checker Framework's Nullness Checker

Question

I'm trying out the Checker Framework's Nullness checker with Java 8. When I run the checker on the following code:

import java.util.HashMap;
import java.util.Map;

import org.checkerframework.checker.nullness.qual.Nullable;

class A {
    public void f() {}
}

public class Foo {
    private Map<A,Integer> map = new HashMap<>();
    private @Nullable A x;

    public void setX(@Nullable A x) {
        this.x = x;
    }

    public void call() {
        if (x != null) {
            map.put(x, 0);
            x.f();
        }
    }
}

the checker gives a warning on the x.f();: dereference of possible null-reference x. This makes sense, of course. Checker Framework doesn't know what map.put does. The map object might already have a reference to this, and then call setX(null) on it.

Now my question is the following. Is there any way to tell the Checker Framework that a method does not modify any object other than the object it's called on? Because map.put doesn't call the setX method, so the value of x will not change.

To get rid of the warning, I could change the call method to:

public void call() {
    A y = x;
    if (y != null) {
        map.put(y, 0);
        y.f();
    }
}

Now there are no warnings. This also makes sense: the local variable cannot be accessed from the outside. But I do not like to introduce this local variable with the sole purpose of getting rid of a warning.

Alternatively, I could annotate the field x by @MonotonicNonNull. But in my actual use case I would like to keep the possibility of setting the field to null.

Thanks in advance!

Answer 1

Your question already gives several excellent ways to suppress the warning, so you clearly know what you are doing.

However, you want a better way. You want to know how to make the Checker Framework never issue the warning in the first place. Your key question is:

Is there any way to tell the Checker Framework that a method does not modify any object other than the object it's called on?

Unfortunately, the Checker Framework does not currently have this functionality. Manual section 21.4.3, "Side effects, determinism, purity, and flow-sensitive analysis", discusses how the Checker Framework indicates purity or freedom from side effects. The @SideEffectFree and @Pure annotations are currently all-or-nothing.

Your suggestion of partial purity annotations would be useful: it would make the Checker Framework more expressive and would reduce the need to suppress warnings, as is currently required. (On the other hand, it would also be one more thing for users to learn; there is always an expressiveness-complexity tradeoff.) I suggest that you propose this feature to the Checker Framework developers.