println destroying "knowledge" on non-nullness of unrelated field?

[Bastien Chevreux]

Hi all,

stumbled across a compilation problem where I do not understand why the nullness checker "forgets" the correct assumption of non-nullness. Here's a minimal example, the problem arises in the while loop at the bottom of the code.

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

public class Dlist {

private static class DlistNode {

protected @Nullable DlistNode mmNext = null;

protected String mmData = "Some data";

}

private @Nullable DlistNode mmHead = null;

public void checkIntegrity() {

if (mmHead == null) {

return;

}

var current = mmHead;

while (current.mmNext != null) {

System.out.println(current.mmData); // commenting out println allows compilation

current = current.mmNext;

}

}

}

If I comment out the println in the while loop, then this compiles fine.

What I do not understand is why the nullness checker "forgets" its knowledge on "current.mmNext" when the println statement uses a completely unrelated field (current.mmData).

I could understand checkerframework behaviour if I called println with either the full instance (current) or with the very specific nullness-related field (current.mmNext), but it baffles me when using an unrelated field (current.mmData).

As far as my knowledge on Java goes (which is not saying much), there is no sane way a method - which gets a field (mmData) from a larger instance (DlistNode) - is able to change a sibling (mmNext) to the field of the enclosing instance (DlistNode). I also asked this to ChatGPT, Claude, and Gemini, but what i got as answers was not convincing in terms of do-ability in any kind of normal code.

I know that as a workaround one can do

while (current.mmNext != null) {

var next = current.mmNext;

System.out.println(current.mmData); // This now works

current = next;

}

But this feels unnatural for many loops and does raise eyebrows in code reviews.

Is that an expected behaviour of the nullness checker?

Best,
  Bastien

[Manu Sridharan]

Hi Bastien,

In principle, it’s possible that the object referenced by `current` is also accessible through some public static field, so println could null out the `mmNext` field by getting access via the global variable.  That said, it seems like the Nullness Checker could/should have a better model of `System.out.println` so that it knows that won’t happen in this case.

Best,

Manu

--

---
You received this message because you are subscribed to the Google Groups "Checker Framework discussion" group.
To unsubscribe from this group and stop receiving emails from it, send an email to checker-framework-...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/checker-framework-discuss/b20d35ae-0f73-4560-8da4-1b650a6c857dn%40googlegroups.com.