Nullness status of `@MonotonicNonNull` fields is forgotten when `this` is captured by a lambda

[ghost]

Commands

checker-framework-3.42.0-eisop3/checker/bin/javac -processor nullness TestNullable.java

Inputs

// TestNullable.java

package test;

import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
import org.checkerframework.checker.nullness.qual.RequiresNonNull;

final class TestNullable {
  private @MonotonicNonNull String value = null;

  @RequiresNonNull({"value"})
  void print() {
    System.out.println(value);
  }

  void func() {
    if (value == null) {
      return;
    }

    Runnable r = () ->print();
  }
}

Outputs

TestNullable.java:19: error: [contracts.precondition.not.satisfied] precondition of print is not satisfied.
    Runnable r = () -> print();
                            ^
  found   : this.value is @MonotonicNonNull
  required: this.value is @NonNull

Expectation

Similar code with print(); instead of Runnable r = () -> print(); is allowed in current version of checker framework. Checker framework should allow both version of the code, regardless if this is captured by a lambda or not.

[wmdietl]

Thanks for the report! Yes, that looks like a false positive that we should look into removing. Note that if the field value were @Nullable, this would not be a false positive: the Runnable could be run at some later point and the field might have been re-set to null by that time. But for a @MonotonicNonNull, once it is non-null it cannot become null again, so we know that the pre-condition will be fulfilled for any future call.

[Ao-senXiong]

Interestingly, test case in here https://github.com/bazelbuild/bazel/issues/10326 also got a false positive

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

public class T {
    private final @Nullable String f;

    T(@Nullable String f) {
        this.f = f;
    }

    void test() {
        if (f == null) {
            return;
        }

        Runnable r =
                () -> {
                    System.err.println(f.toString());
                };
    }
}

checker/bin/javac -processor nullness T.java                                           
T.java:17: error: [dereference.of.nullable] dereference of possibly-null reference f
                    System.err.println(f.toString());
                                       ^
1 error