Nullness checker incorrectly marking possible null on compound if/else condition

[jpschewe]

In this code, it's not possible for thisLastEdited or otherLastEdited to be null in the else block. This is a pretty common way to check for nulls in comparisons.

I didn't put this on #4872 because that one is accessing local class state, so another thread may made the class variable null between statements. Here I have stored a local reference to ensure that this can't happen.

package net.mtu.eggplant.checker;

import java.time.LocalTime;

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

public class IfElseNullable {

  private int compareLastEdited(final @Nullable LocalTime thisLastEdited, final @Nullable LocalTime otherLastEdited) {
    if (null != thisLastEdited
        && null == otherLastEdited) {
      return -1;
    } else if (null == thisLastEdited
               && null != otherLastEdited) {
      return 1;
    } else if (null == thisLastEdited
               && null == otherLastEdited) {
      return 0;
    } else {
      return thisLastEdited.compareTo(otherLastEdited);
    }
  }

}

These are the outputs of the checker framework.

/home/jpschewe/projects/checker-bugs/src/main/java/net/mtu/eggplant/checker/IfElseNullable.java:20: error: [dereference.of.nullable] dereference of possibly-null reference thisLastEdited
      return thisLastEdited.compareTo(otherLastEdited);
             ^
/home/jpschewe/projects/checker-bugs/src/main/java/net/mtu/eggplant/checker/IfElseNullable.java:20: error: [argument] incompatible argument for parameter other of compareTo.
      return thisLastEdited.compareTo(otherLastEdited);
                                      ^
  found   : @Initialized @Nullable LocalTime
  required: @Initialized @NonNull LocalTime

This output was created using checker framework version 3.21.1.

[MdSahil-oss]

/assign

[mernst]

Thanks for reporting this problem. You are right that the Nullness Checker does not track arbitrary boolean conditions (not even ones as simple as a conjunction). Thus, the code that you wrote is beyond the capabilities of its simple brain.

Here is a variant that the Nullness Checker does verify:

import java.time.LocalTime;
import org.checkerframework.checker.nullness.qual.Nullable;

public class IfElseNullable {

  private int compareLastEdited(
      final @Nullable LocalTime thisLastEdited, final @Nullable LocalTime otherLastEdited) {
    if (null == thisLastEdited) {
      if (null != otherLastEdited) {
        return 1;
      } else {
        // null == otherLastEdited
        return 0;
      }
    } else {
      // null != thisLastEdited
      if (null == otherLastEdited) {
        return -1;
      } else {
        return thisLastEdited.compareTo(otherLastEdited);
      }
    }
  }
}

It differs in that each if condition is a single boolean expression rather than a compound one with &&.

There are pros and cons of the two different ways of writing the code, and I can see why you would prefer your version.

It would be possible to change the Checker Framework to track more complex boolean conditions, which would enable it to handle your version. This would take extra code and would have a run-time cost, so unfortunately it is not high on our priority list (though we would be happy to review such a code contribution).