Improve documentation on how NullAway analyzes complex `if` conditions

[bannmann]

NullAway: 0.12.9 and earlier Java: 21.0.8_12

With the reproducer source file below, NullAway reports the following warnings:

1. [28,40] [NullAway] passing @Nullable parameter 'a' where @NonNull is required (see http://t.uber.com/nullaway )
[28,54] [NullAway] passing @Nullable parameter 'b' where @NonNull is required (see http://t.uber.com/nullaway )
   • NullAway does not infer that at this point, neither a nor b can be null.
2. [44,33] [NullAway] passing @Nullable parameter 'start' where @NonNull is required (see http://t.uber.com/nullaway )
   • NullAway does not infer that at this point, start cannot be null.

package com.example;

import java.time.LocalTime;
import java.util.Objects;

import lombok.AccessLevel;
import lombok.NoArgsConstructor;

import org.jspecify.annotations.Nullable;

import com.google.common.collect.Range;

@NoArgsConstructor(access = AccessLevel.PRIVATE)
public final class Reproducer
{
    public static boolean areEquivalent(@Nullable String a, @Nullable String b)
    {
        if (a == null && b == null)
        {
            return true;
        }

        if (a == null ^ b == null)
        {
            return false;
        }

        return Objects.equals(normalize(a), normalize(b)); // Case ⚠️1
    }

    private static Object normalize(String input)
    {
        return input.replace("_", "-");
    }

    public static Range<LocalTime> makeRange(@Nullable LocalTime start, @Nullable LocalTime end)
    {
        if (start == null && end == null)
        {
            return Range.all();
        }
        else if (end == null)
        {
            return Range.atLeast(start); // Case ⚠️2
        }
        else if (start == null)
        {
            return Range.lessThan(end);
        }
        else if (start.isAfter(end))
        {
            throw new IllegalArgumentException("Times are reversed");
        }
        else if (start.equals(end))
        {
            return Range.closed(start, end);
        }
        else
        {
            return Range.closedOpen(start, end);
        }
    }
}

[jeffrey-easyesi]

Other tools report the same errors (tested Checker Framework, Eclipse, and the JSpecify reference implementation). It's just not practical to try to compute the implications of arbitrary boolean expressions since that would take exponential time.

For the sake of both tools and humans reading your code, better to keep the logic simple, checking one variable at a time:

public static boolean areEquivalent(@Nullable String a, @Nullable String b) {
    return a == null
            ? b == null
            : b != null && normalize(a).equals(normalize(b));
}

public static Range<LocalTime> makeRange(@Nullable LocalTime start, @Nullable LocalTime end) {
    if (end == null) {
        return start == null ? Range.all() : Range.atLeast(start);
    } else if (start == null) {
        return Range.lessThan(end);
    } else if ...
}

[bannmann]

While not everybody may agree that the original version above is readable and/or good code, it is valid Java. So one could argue that tools should be able to figure this out.

Other tools report the same errors (tested Checker Framework, Eclipse, and the JSpecify reference implementation). It's just not practical to try to compute the implications of arbitrary boolean expressions since that would take exponential time.

As a counter example, at least in this case, IntelliJ IDEA seems to be able to compute the implications just fine:

• It does not complain about the "Case ⚠️1" line, but when I remove the if (a == null ^ b == null) branch above it, it does.
• It also does not complain about the "Case ⚠️2" line, but does when I change the else if (end == null) to else if (true).

Obviously, it's still up to the maintainers whether they see merit in implementing this. With NullAway being an annotation processor and not a full-blown IDE, maybe the runtime and/or memory implications of such an analysis result in a different tradeoff. If NullAway decides to not implement this analysis, it would certainly be in good company, given the behavior of the tools that you looked into. (Thanks for doing that, by the way!)

For the sake of both tools and humans reading your code, better to keep the logic simple, checking one variable at a time

Sure, I might do that. Another alternative I thought of is to simply have a normalize overload that is null safe (i.e. "null in ➞ null out"). That way, the areEquivalent() method is reduced to return Objects.equals(normalize(a), normalize(b);.

In any case, I wanted to make sure the NullAway developers know about this problem, just in case they want to fix it.

[msridhar]

Thanks for the report, @bannmann. @jeffrey-easyesi is correct that we deliberately don't do this checking as we want to keep our dataflow analysis fast to minimize NullAway's build-time overhead. We've gotten reports like this one before, and we really should add a documentation page about it. The one enhancement we are considering implementing support for is #98, tracking relationships between (some) boolean local variables and nullness facts. But even that we've had a hard time prioritizing / getting resources to do.

IntelliJ does do more sophisticated analysis than most other tools when it comes to reasoning about boolean conditions. At times I've heard discussion amongst tool developers to ask IntelliJ to provide a setting to turn that off, for better consistency between the tools 🙂 I understand it can be annoying to have inconsistent behaviors between IntelliJ in the IDE and something like NullAway on CI.

In any case, we do appreciate the report. I'm going to leave this issue open but rename it to be about improving our documentation.

[jeffrey-easyesi]

That's interesting about IntelliJ - didn't know it could do that.

For me one of the big attractions of NullAway is its speed, so I wouldn't want it becoming 'smarter' if it became significantly slower in the process. (Or less sound: I know I've seen IntelliJ's dataflow analysis just giving up on some methods, saying they're "too complex" to check.)