CheckContracts: false violation when the return null is reached by a control-flow merge #1731

Version

NullAway 0.14.0, and current master (21f02dd). Error Prone 2.50.0, JDK 21.

Flags: -XepOpt:NullAway:CheckContracts=true -XepOpt:NullAway:JSpecifyMode=true -XDaddTypeAnnotationsToSymbol=true.

Summary

CheckContracts reports a violation for a return null that is reachable only when the contract's preconditions are false, whenever that return is reached by a control-flow merge whose incoming edges each contradict a different argument.

The merge is what matters, not the operator. if (a == null || b == null) reports, and if (a == null || a == null) — same operator, one argument — does not.

Reproducer

package foo;

import org.jetbrains.annotations.Contract;
import org.jspecify.annotations.NullMarked;
import org.jspecify.annotations.Nullable;

@NullMarked
class Test {
  @Contract("!null, !null -> !null")
  static @Nullable Double or(@Nullable Double a, @Nullable Double b) {
    // BUG: Diagnostic contains: Method or has @Contract(!null, !null -> !null), but this appears to be violated
    if (a == null || b == null) { return null; }
    return a + b;
  }

  @Contract("!null, !null -> !null")
  static @Nullable Double and(@Nullable Double a, @Nullable Double b) {
    if (a != null && b != null) { return a + b; }
    // BUG: Diagnostic contains: Method and has @Contract(!null, !null -> !null), but this appears to be violated
    return null;
  }

  @Contract("!null, !null -> !null")
  static @Nullable Double ternary(@Nullable Double a, @Nullable Double b) {
    // BUG: Diagnostic contains: Method ternary has @Contract(!null, !null -> !null), but this appears to be violated
    return (a == null || b == null) ? null : a + b;
  }

  // no merge before the return: clean
  @Contract("!null, !null -> !null")
  static @Nullable Double twoIfs(@Nullable Double a, @Nullable Double b) {
    if (a == null) { return null; }
    if (b == null) { return null; }
    return a + b;
  }

  // a merge, but both edges contradict the same argument: clean
  @Contract("!null, _ -> !null")
  static @Nullable Double sameVar(@Nullable Double a, @Nullable Double b) {
    if (a == null || a == null) { return null; }
    return a + 1;
  }
}

All five bodies satisfy their contracts. and contains no disjunction at all, and sameVar contains one and is accepted, so neither || nor the number of arguments in the antecedent is the discriminator.

What does and does not report

What appears to be going on

ContractCheckHandler.visitReturn skips a return when hasBottomAccessPathForContractDataflow finds an access path mapped to BOTTOM in the store before the expression. Nullness.leastUpperBound documents BOTTOM as losing at a merge:

// Bottom loses.
if (this == BOTTOM) {
  return other;
}

Seed the contract dataflow with a = NONNULL, b = NONNULL and take or. The return null has two incoming edges: a == null leaves a at BOTTOM, and a != null && b == null leaves b at BOTTOM. Each edge is individually infeasible, but each is infeasible for a different variable, so the merged store is a = NONNULL, b = NONNULL with no BOTTOM anywhere, and the return is analysed as reachable.

sameVar isolates this: both edges leave the same variable at BOTTOM, BOTTOM ⊔ BOTTOM = BOTTOM survives the merge, and the return is correctly skipped. twoIfs avoids the merge entirely — each return null sits on its own branch.

Expected

A return reachable only when the contract's antecedent is false should not be reported, however the control flow arrives there. Tracking infeasibility so it survives a merge would cover all four rows above.

Workaround

Write one if per argument.

Where we hit it

NumberUtil.add and RelMdPercentageOriginalRows.quotientForPercentage. 108 other contracts in the same codebase verify without complaint; these two are the ones whose return null sits after a merge. Found while replacing the Checker Framework with NullAway in Apache Calcite (apache/calcite#5213).