Crash on a @Contract clause whose antecedent arity does not match the method #1726

Version

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

Summary

When a @Contract clause's antecedent has a different number of value constraints than the method has parameters, NullAway reports Invalid @Contract annotation detected ... and then keeps using the mismatched antecedent. Both users of the antecedent index into something sized by the other count, so the compile crashes:

• with CheckContracts=true, checking the declaration throws BugInCF: Problem with initial store for CFGMethod(...), parameters=[];
• at any call site whose enclosing method gets dataflow-analyzed, ContractHandler.onDataflowVisitMethodInvocation throws IndexOutOfBoundsException. This one needs no flags beyond the defaults.

The call-site crash is the worse of the two: ContractUtils.getAntecedent only reports the diagnostic on a method declaration (shouldReportInvalidContract), so when the annotated method comes from a different compilation unit the build fails with a crash and no diagnostic pointing at the bad annotation.

Reproducer, declaration side

Flags: -XepOpt:NullAway:AnnotatedPackages=com.uber -XepOpt:NullAway:CheckContracts=true

package com.uber;

import org.jetbrains.annotations.Contract;

public class Test {
  @Contract("!null -> !null")
  public Object[] toArray() {
    return new Object[0];
  }
}

Test.java:6: error: An unhandled exception was thrown by the Error Prone static analysis plugin.
org.checkerframework.nullaway.javacutil.BugInCF: Problem with initial store for CFGMethod(

@Contract(value = "!null -> !null")
public Object[] toArray() {
    return new Object[0];
}
), parameters=[]
	at org.checkerframework.nullaway.dataflow.analysis.ForwardAnalysisImpl.initInitialInputs(ForwardAnalysisImpl.java:339)
	at org.checkerframework.nullaway.dataflow.analysis.AbstractAnalysis.init(AbstractAnalysis.java:519)
	at org.checkerframework.nullaway.dataflow.analysis.ForwardAnalysisImpl.performAnalysis(ForwardAnalysisImpl.java:102)
	at com.uber.nullaway.dataflow.RunOnceForwardAnalysisImpl.performAnalysis(RunOnceForwardAnalysisImpl.java:31)
	at com.uber.nullaway.dataflow.DataFlow.dataflow(DataFlow.java:160)
	at com.uber.nullaway.dataflow.DataFlow.resultFor(DataFlow.java:326)
	at com.uber.nullaway.dataflow.DataFlow.resultForExpr(DataFlow.java:304)
	at com.uber.nullaway.dataflow.DataFlow.expressionDataflow(DataFlow.java:227)
	at com.uber.nullaway.dataflow.AccessPathNullnessAnalysis.getNullnessForContractDataflow(AccessPathNullnessAnalysis.java:143)
	at com.uber.nullaway.handlers.contract.ContractCheckHandler$1.visitReturn(ContractCheckHandler.java:171)
	at com.uber.nullaway.handlers.contract.ContractCheckHandler$1.visitReturn(ContractCheckHandler.java:140)
	at com.uber.nullaway.handlers.contract.ContractCheckHandler.onMatchMethod(ContractCheckHandler.java:200)

ContractCheckHandler.onMatchMethod validates each value constraint against allValidValueConstraints and clears checkMethodBody when one is unknown, but nothing clears it when the count is wrong, so the body is analyzed with an antecedent the CFG cannot supply parameters for.

Reproducer, call side

Flags: -XepOpt:NullAway:AnnotatedPackages=com.uber only. CheckContracts is not involved.

package com.uber;

import javax.annotation.Nullable;
import org.jetbrains.annotations.Contract;

public class Test {
  @Contract("!null -> !null")
  public @Nullable Object[] toArray() {
    return new Object[0];
  }

  public void caller(Test t) {
    Object[] a = t.toArray();
    a.hashCode();
  }
}

Test.java:13: error: An unhandled exception was thrown by the Error Prone static analysis plugin.
java.lang.IndexOutOfBoundsException: Index 0 out of bounds for length 0
	at java.base/java.util.ArrayList.get(ArrayList.java:427)
	at org.checkerframework.nullaway.dataflow.cfg.node.MethodInvocationNode.getArgument(MethodInvocationNode.java:96)
	at com.uber.nullaway.handlers.contract.ContractHandler.onDataflowVisitMethodInvocation(ContractHandler.java:400)
	at com.uber.nullaway.handlers.CompositeHandler.onDataflowVisitMethodInvocation(CompositeHandler.java:199)
	at com.uber.nullaway.dataflow.AccessPathNullnessPropagation.visitMethodInvocation(AccessPathNullnessPropagation.java:1094)
	at org.checkerframework.nullaway.dataflow.cfg.node.MethodInvocationNode.accept(MethodInvocationNode.java:154)
	at org.checkerframework.nullaway.dataflow.analysis.AbstractAnalysis.callTransferFunction(AbstractAnalysis.java:494)

The loop in onDataflowVisitMethodInvocation walks antecedent and calls node.getArgument(i) without comparing the antecedent's length to the node's argument count.

Suggested fix

Skip a clause whose antecedent arity does not match the method's parameter count, in both handlers, rather than continuing with it. On the declaration side that means clearing checkMethodBody; on the call side, a length check before the loop. ContractUtils.getAntecedent already computes both numbers, so it could return the information the callers need instead of only reporting it.

Where we hit it

Replacing the Checker Framework with NullAway in Apache Calcite (apache/calcite#5213). The Checker Framework's @PolyNull has no NullAway equivalent, so @Contract("!null -> !null") stands in for it. Some of the @PolyNull methods declare an explicit receiver parameter, for example Object[] toArray(Flat1List<@Nullable T> this), and the generated contract counted that receiver as an argument. Counting it was our mistake — javac does not, and NullAway agrees with javac: @Contract("!null -> !null") on id(Box<E> this, @Nullable Object o) is accepted and checked correctly. What the receiver parameter did was make it easy to write a contract of the wrong arity, and the wrong arity is what crashes.