Add @IfNullThrows parameter annotation and unify with AssertMethod in CFG

checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/IfNullThrows.java

@@ -0,0 +1,35 @@
+package org.checkerframework.checker.nullness.qual;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+/**
+ * A parameter annotation indicating that the method throws an exception if this parameter is null.
+ *
+ * <p>When the CFG is built, calls to methods with {@code @IfNullThrows} on a parameter are
+ * translated into an explicit branch: if the argument is null, the method throws; otherwise
+ * execution continues. This enables flow-sensitive refinement in type checkers (e.g., the Nullness
+ * Checker refines the argument to non-null on the continue path).
+ *
+ * <p><b>Semantic meaning:</b> {@code @IfNullThrows} means: <i>if this parameter is null, then the
+ * method throws</i>. Equivalently: when the method returns normally, the parameter was non-null.
+ *
+ * <p><b>Example:</b>
+ *
+ * <pre><code>
+ * public static &lt;T&gt; T requireNonNull(@IfNullThrows @Nullable T obj) {
+ *   if (obj == null) throw new NullPointerException();
+ *   return obj;
+ * }
+ * </code></pre>
+ *
+ * @checker_framework.manual #type-refinement Automatic type refinement (flow-sensitive type
+ *     qualifier inference)
+ */
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target(ElementType.PARAMETER)
+public @interface IfNullThrows {}

checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitVisitor.java

@@ -6,6 +6,7 @@
 import com.sun.source.tree.ArrayTypeTree;
 import com.sun.source.tree.AssertTree;
 import com.sun.source.tree.BinaryTree;
+import com.sun.source.tree.BlockTree;
 import com.sun.source.tree.CaseTree;
 import com.sun.source.tree.CatchTree;
 import com.sun.source.tree.ClassTree;
@@ -35,9 +36,11 @@
 import com.sun.source.tree.VariableTree;
 import com.sun.source.tree.WhileLoopTree;
 import com.sun.source.util.TreePath;
+import com.sun.source.util.TreeScanner;
 
 import org.checkerframework.checker.compilermsgs.qual.CompilerMessageKey;
 import org.checkerframework.checker.formatter.qual.FormatMethod;
+import org.checkerframework.checker.nullness.qual.IfNullThrows;
 import org.checkerframework.checker.nullness.qual.NonNull;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.checkerframework.common.basetype.BaseTypeChecker;
@@ -600,9 +603,51 @@ public void processMethodTree(String className, MethodTree tree) {
             }
         }
 
+        // @IfNullThrows well-formedness: method must throw (e.g. on null param)
+        checkIfNullThrowsEnforced(tree);
+
         super.processMethodTree(className, tree);
     }
 
+    /**
+     * Reports an error if the method has {@link IfNullThrows} on any parameter but its body does
+     * not contain a throw statement (so the contract cannot be satisfied).
+     */
+    private void checkIfNullThrowsEnforced(MethodTree tree) {
+        ExecutableElement methodElement = TreeUtils.elementFromDeclaration(tree);
+        if (methodElement.getModifiers().contains(javax.lang.model.element.Modifier.ABSTRACT)
+                || methodElement
+                        .getModifiers()
+                        .contains(javax.lang.model.element.Modifier.NATIVE)) {
+            return;
+        }
+        boolean hasIfNullThrows = false;
+        for (Element param : methodElement.getParameters()) {
+            if (atypeFactory.getDeclAnnotation(param, IfNullThrows.class) != null) {
+                hasIfNullThrows = true;
+                break;
+            }
+        }
+        if (!hasIfNullThrows) {
+            return;
+        }
+        BlockTree body = tree.getBody();
+        if (body == null) {
+            return;
+        }
+        boolean[] hasThrow = new boolean[] {false};
+        new TreeScanner<Void, Void>() {
+            @Override
+            public Void visitThrow(ThrowTree node, Void p) {
+                hasThrow[0] = true;
+                return super.visitThrow(node, p);
+            }
+        }.scan(body, null);
+        if (!hasThrow[0]) {
+            checker.reportError(tree, "if.null.throws.must.throw");
+        }
+    }
+
     @Override
     public Void visitMethodInvocation(MethodInvocationTree tree, Void p) {
         if (!permitClearProperty) {

checker/src/main/java/org/checkerframework/checker/nullness/messages.properties

@@ -22,6 +22,7 @@ nulltest.redundant=redundant test against null; "%s" is non-null
 instanceof.nullable=instanceof is only true for a non-null expression
 instanceof.nonnull.redundant=redundant @NonNull annotation on instanceof
 new.array.type.invalid=annotations %s may not be applied as component type for array "%s"
+if.null.throws.must.throw=method has @IfNullThrows on parameter but body does not throw when parameter is null
 nullness.on.constructor=do not write nullness annotations on a constructor, whose result is always non-null
 nullness.on.new.array=do not write nullness annotations on an array creation, which is always non-null
 nullness.on.new.object=do not write nullness annotations on an object creation, which is always non-null

checker/tests/nullness/IfNullThrowsTest.java

@@ -0,0 +1,60 @@
+// Test that @IfNullThrows (parameter-level postcondition: if null then throw) is respected by the
+// Nullness Checker.
+
+import org.checkerframework.checker.nullness.qual.IfNullThrows;
+import org.checkerframework.checker.nullness.qual.Nullable;
+
+public class IfNullThrowsTest {
+
+    // 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) {
+            throw new NullPointerException();
+        }
+        return obj;
+    }
+
+    void useRequireNonNull(@Nullable String s) {
+        requireNonNull(s);
+        s.toString(); // OK: s refined to non-null after requireNonNull returns
+    }
+
+    // With message parameter
+    public static <T> T requireNonNull(@IfNullThrows @Nullable T obj, String msg) {
+        if (obj == null) {
+            throw new NullPointerException(msg);
+        }
+        return obj;
+    }
+
+    void useRequireNonNullWithMsg(@Nullable String s) {
+        requireNonNull(s, "s must not be null");
+        s.toString(); // OK
+    }
+
+    // Multiple parameters with @IfNullThrows - validates both must be non-null to return
+    public static void requireBothNonNull(
+            @IfNullThrows @Nullable Object a, @IfNullThrows @Nullable Object b) {
+        if (a == null || b == null) {
+            throw new NullPointerException();
+        }
+    }
+
+    void useRequireBothNonNull(@Nullable Object x, @Nullable Object y) {
+        requireBothNonNull(x, y);
+        x.toString(); // OK
+        y.toString(); // OK
+    }
+
+    // Incorrect: has @IfNullThrows but never throws
+    // :: error: (if.null.throws.must.throw)
+    public static <T> T badNoThrow(@IfNullThrows @Nullable T obj) {
+        return obj;
+    }
+
+    // Incorrect: has @IfNullThrows but only returns, no throw
+    // :: error: (if.null.throws.must.throw)
+    public static String badJustReturn(@IfNullThrows @Nullable String s) {
+        return s == null ? "" : s;
+    }
+}