Skip to content

Add @IfNullThrows parameter annotation and unify with AssertMethod in CFG#1566

Draft
HenryXi1 wants to merge 3 commits intoeisop:masterfrom
HenryXi1:add-if-null-throws-contract
Draft

Add @IfNullThrows parameter annotation and unify with AssertMethod in CFG#1566
HenryXi1 wants to merge 3 commits intoeisop:masterfrom
HenryXi1:add-if-null-throws-contract

Conversation

@HenryXi1
Copy link
Copy Markdown

@HenryXi1 HenryXi1 commented Mar 2, 2026

Goal

Support expressing "if this parameter is null, the method throws" by annotating the parameter with @IfNullThrows (e.g. requireNonNull(@IfNullThrows @Nullable T obj)), so the Nullness Checker can refine the argument to non-null on the normal-return path. This branch also unifies CFG handling of parameter-triggered throws with @AssertMethod via a single spec and shared emission logic.

Changes

checker-qual

  • Moved @IfNullThrows from org.checkerframework.dataflow.qual to org.checkerframework.checker.nullness.qual.
  • Removed dataflow/qual/IfNullThrows.java; added checker/nullness/qual/IfNullThrows.java (same semantics and Javadoc).

dataflow – CFG translation

  • Unified representation: CompareValue enum (TRUE, FALSE, NULL) and ParameterConditionalThrowSpec (parameterIndex, compareValue, exceptionType). One spec list for both @AssertMethod and @IfNullThrows.
  • getParameterConditionalThrowSpecs(executable): One spec from @AssertMethod (if present) plus one per parameter with @IfNullThrows; returns a single list.
  • Single emission path: For each argument index, for each matching spec: buildConditionNodeForParameterThrow (NULL → (arg == null), TRUE/FALSE → argument node) then emitConditionalThrow (branch + AssertionErrorNode + ThrowNode + continue label).
  • Removed: AssertMethodTuple, getAssertMethodTuple, getIfNullThrowsParameterIndices, treatMethodAsAssert, treatMethodAsIfNullThrows.
  • Safety: In all three argument loops, the actualVal == null check runs before any conditional-throw logic.
  • Docs: Javadoc for the conditional-throw logic and for AssertionErrorNode updated (condition-triggered throw for assert / AssertMethod / IfNullThrows; semantics from CFG edges; name is historical).

checker – Nullness

  • Enforcement: In NullnessNoInitVisitor, checkIfNullThrowsEnforced(tree) runs from processMethodTree. If the method has any @IfNullThrows parameter and a body, the body must contain a throw; otherwise report if.null.throws.must.throw.
  • Message: Added if.null.throws.must.throw in nullness messages.properties.
  • Imports: NullnessNoInitVisitor and IfNullThrowsTest use org.checkerframework.checker.nullness.qual.IfNullThrows.

Caching hook discovery

  • Add a framework hook to provide extra parameter throw specs during CFG phase 1.
  • Keep base dataflow specs in CFGTranslationPhaseOne; merge framework specs in CFCFGTranslationPhaseOne.
  • Introduce shared spec types: ConditionalThrowCompareValue and ParameterConditionalThrowSpec.
  • Cache merged specs in GenericAnnotatedTypeFactory per ExecutableElement.
  • Add weak cross-factory cache for @IfNullThrows parameter indexes.
  • Clear per-factory cache in setRoot(...) to keep compilation-unit correctness.

Tests

  • IfNullThrowsTest: Import updated to nullness qual. Enforcement: Added badNoThrow and badJustReturn (no throw in body) with expected // :: error: (if.null.throws.must.throw). Existing tests still check refinement after requireNonNull / requireBothNonNull.

@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target(ElementType.PARAMETER)
public @interface IfNullThrows {}
Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This qualifier should be in checker/.../nullness, not in the framework.


// requireNonNull-style: if param is null, throws; so when returns, param is non-null
public static <T> T requireNonNull(@IfNullThrows @Nullable T obj) {
if (obj == null) {
Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Also in these tests, ensure that the qualifier is actually enforced - add an incorrect implementation and ensure we raise an error.

(MethodInvocationTree) tree, assertMethodTuple, actualVal);
}
if (ifNullThrowsParams.contains(i)) {
treatMethodAsIfNullThrows((MethodInvocationTree) tree, actualVal);
Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

First perform the actualVal == null check from the line below, before using the value here.

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Probably would have made sense for the treatMethodAsAssert already... Think whether this change would make sense for both.

extendWithExtendedNode(cjump);

addLabelForNextNode(throwLabel);
AssertionErrorNode assertNode =
Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Does Assertion error code make sense for our use?
At the beginning, can you write down what the transformation is? Are you adding an if/else or are you adding an "assert"?


ArrayList<Node> convertedNodes = new ArrayList<>(numFormals);
AssertMethodTuple assertMethodTuple = getAssertMethodTuple(executable);
Set<Integer> ifNullThrowsParams = getIfNullThrowsParameterIndices(executable);
Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Think whether you can generalize and merge this with AssertMethodTuple. Instead of just a boolean condition, you'll have a parameter that you want to compare and a value you want to compare against.

AssertMethod is on the whole method declaration and needs to carry which parameter has the effect. The per-parameter annotations don't need that and get the parameter from where the annotation is. That can be unified into one common datastructure.

For AssertMethod, the parameter in the condition is a boolean. For IfNullThrows it's a reference type. Does this difference matter for the CFG you build? Or does it only matter whether you compare against true, false, or null?

@HenryXi1 HenryXi1 force-pushed the add-if-null-throws-contract branch from edfd922 to 1c4a676 Compare March 11, 2026 04:27
@HenryXi1 HenryXi1 changed the title Add @IfNullThrows parameter annotation Add @IfNullThrows parameter annotation and unify with AssertMethod in CFG Mar 11, 2026
@azure-pipelines
Copy link
Copy Markdown

Azure Pipelines:
1 pipeline(s) were filtered out due to trigger conditions.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants