Nullness false positive referring to a field from an inner class's method

[amalloy]

After upgrading from 3.15.0 to 3.18.0, I see a number of new failures in our source files. Many of them are clear improvements to the nullness checker: a possible NPE was not detected before, but is now. But in this case it is easy for a human to see that no NPE can occur, and I think the checker could detect this as well.

Command

../checker-framework-3.18.0/checker/bin/javac -processor nullness Outer.java 

Input

File: ./Outer.java

class Outer {
  interface Go { void go(); }
  final Go go = new Go() {
    @Override public void go() {synchronized(x) {}}
  };
  final Object x = new Object();
}

Output

Outer.java:4: error: [locking.nullable] synchronizing over a possibly-null lock (x)
    @Override public void go() {synchronized(x) {}}
                                            ^
1 error

When I use 3.15.0 instead, I do not see any diagnostic on this line.

Expectation

No finding on this line.

Based on the other (true positive) findings I have encountered, I speculate that this version of the nullness checker is more concerned about methods in inner classes being invoked by superclass constructors, at a time when not all fields have been initialized. For example, if Go were an abstract class instead of an interface, and its implementation were elsewhere, it might possibly invoke go in its constructor, before x is initialized. But in the case where Go's only superclass is Object, we know it does not invoke go in its constructor; by the time go is eventually called, we know x is non-null.

Further research

I tried changing the go and x fields to be static final instead of merely final, and I see a change in behavior. Neither 3.15.0 nor 3.18.0 report a diagnostic in that case. This doesn't seem right to me: the order of field initialization is unchanged by marking them both static, and so exactly the same possible NPE should be present (or, with more careful analysis, not present) whether or not the fields are static.

I also tried writing x.toString(); instead of synchronized(x){}; this had no material impact. The error message reported is different, of course, but it is present in exactly the same situations as with synchronized. This matches my expectations.

[Mawootad]

Ran into this as well, checker does not correctly identify that fields initialize before the constructor does and also does not recognize the order in which fields initialize. The exact order of intialization is static fields from top to bottom, then class fields from top to bottom, then the constructor, with each parent class being fully initialized before any child classes. So in this case it actually is correctly identifying that static members initialize first, but it's not then also identifying that fields initialize after that and before the constructor. Easy solution for this is to note when a method accesses fields with field initializers vs accesses fields that are intialized via the constructor and allow those methods to be accessed from anything that's not a field initializer. More complex solution would be to take into account that fields initialize in order, since you can concretely say that in

class Foo {
  int c = getA();
  int a = 1;
  int b = getA();

  int getA() {
    return a;
}

c accesses a before it's initialized while b does not. Solution would likely be to count the ordering of fields in the file, and if any field calls a method that accesses a field below it in the file that's a bad access. Eg using some sort of pseudo-annotation

@AccessesFields(fields={1})
int getA() {
  return a;
}

Then if a field calls a method that could access a field with an order number that is greater or equal to its own flag that for possible nullness.