Add @IfNullThrows parameter annotation

Author: HenryXi1

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

@@ -0,0 +1,35 @@
+package org.checkerframework.dataflow.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/tests/nullness/IfNullThrowsTest.java

@@ -0,0 +1,48 @@
+// Test that @IfNullThrows (parameter-level postcondition: if null then throw) is respected by the
+// Nullness Checker.
+
+import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.dataflow.qual.IfNullThrows;
+
+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
+    }
+}

dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java

@@ -58,6 +58,7 @@
 import com.sun.source.util.TreeScanner;
 import com.sun.source.util.Trees;
 import com.sun.tools.javac.code.Type;
+import com.sun.tools.javac.code.TypeTag;
 
 import org.checkerframework.checker.interning.qual.FindDistinct;
 import org.checkerframework.checker.nullness.qual.Nullable;
@@ -139,6 +140,7 @@
 import org.checkerframework.dataflow.cfg.node.VariableDeclarationNode;
 import org.checkerframework.dataflow.cfg.node.WideningConversionNode;
 import org.checkerframework.dataflow.qual.AssertMethod;
+import org.checkerframework.dataflow.qual.IfNullThrows;
 import org.checkerframework.dataflow.qual.TerminatesExecution;
 import org.checkerframework.javacutil.AnnotationProvider;
 import org.checkerframework.javacutil.AnnotationUtils;
@@ -1368,6 +1370,7 @@ protected List<Node> convertCallArguments(
 
         ArrayList<Node> convertedNodes = new ArrayList<>(numFormals);
         AssertMethodTuple assertMethodTuple = getAssertMethodTuple(executable);
+        Set<Integer> ifNullThrowsParams = getIfNullThrowsParameterIndices(executable);
 
         int numActuals = actualExprs.size();
         if (executable.isVarArgs()) {
@@ -1386,6 +1389,9 @@ protected List<Node> convertCallArguments(
                         treatMethodAsAssert(
                                 (MethodInvocationTree) tree, assertMethodTuple, actualVal);
                     }
+                    if (ifNullThrowsParams.contains(i)) {
+                        treatMethodAsIfNullThrows((MethodInvocationTree) tree, actualVal);
+                    }
                     if (actualVal == null) {
                         throw new BugInCF(
                                 "CFGBuilder: scan returned null for %s [%s]",
@@ -1421,6 +1427,9 @@ protected List<Node> convertCallArguments(
                         treatMethodAsAssert(
                                 (MethodInvocationTree) tree, assertMethodTuple, actualVal);
                     }
+                    if (ifNullThrowsParams.contains(i)) {
+                        treatMethodAsIfNullThrows((MethodInvocationTree) tree, actualVal);
+                    }
                     convertedNodes.add(methodInvocationConvert(actualVal, formals.get(i)));
                 }
 
@@ -1453,6 +1462,9 @@ protected List<Node> convertCallArguments(
                 if (i == assertMethodTuple.booleanParam) {
                     treatMethodAsAssert((MethodInvocationTree) tree, assertMethodTuple, actualVal);
                 }
+                if (ifNullThrowsParams.contains(i)) {
+                    treatMethodAsIfNullThrows((MethodInvocationTree) tree, actualVal);
+                }
                 convertedNodes.add(methodInvocationConvert(actualVal, formals.get(i)));
             }
         }
@@ -1494,6 +1506,67 @@ protected AssertMethodTuple getAssertMethodTuple(ExecutableElement method) {
         return new AssertMethodTuple(booleanParam, exceptionType, isAssertFalse);
     }
 
+    /**
+     * Returns the 0-based indices of parameters annotated with {@link IfNullThrows}. Such
+     * parameters cause the method to throw when null; the CFG is modified to add an explicit
+     * branch.
+     *
+     * @param method the method or constructor
+     * @return indices of parameters with {@code @IfNullThrows}
+     */
+    protected Set<Integer> getIfNullThrowsParameterIndices(ExecutableElement method) {
+        Set<Integer> result = new HashSet<>();
+        List<? extends VariableElement> params = method.getParameters();
+        for (int i = 0; i < params.size(); i++) {
+            if (annotationProvider.getDeclAnnotation(params.get(i), IfNullThrows.class) != null) {
+                result.add(i);
+            }
+        }
+        return result;
+    }
+
+    /**
+     * Translates a method call with {@link IfNullThrows} on a parameter into CFG nodes: if the
+     * argument is null, the method throws; otherwise execution continues.
+     *
+     * @param tree the method invocation tree
+     * @param argNode the node for the argument (the parameter value)
+     */
+    protected void treatMethodAsIfNullThrows(MethodInvocationTree tree, Node argNode) {
+        // Create (arg == null) condition
+        TypeMirror booleanType = types.getPrimitiveType(TypeKind.BOOLEAN);
+        LiteralTree nullTree = TreeUtils.createLiteral(TypeTag.BOT, null, types.getNullType(), env);
+        handleArtificialTree(nullTree);
+        Node nullNode = new NullLiteralNode(nullTree);
+        extendWithNode(nullNode);
+
+        ExpressionTree argTree = (ExpressionTree) argNode.getTree();
+        BinaryTree eqTree =
+                treeBuilder.buildBinary(booleanType, Tree.Kind.EQUAL_TO, argTree, nullTree);
+        handleArtificialTree(eqTree);
+
+        Node condition = new EqualToNode(eqTree, argNode, nullNode);
+        extendWithNode(condition);
+
+        // When (arg == null) is true, throw; else continue
+        Label throwLabel = new Label();
+        Label continueLabel = new Label();
+        ConditionalJump cjump = new ConditionalJump(throwLabel, continueLabel);
+        extendWithExtendedNode(cjump);
+
+        addLabelForNextNode(throwLabel);
+        AssertionErrorNode assertNode =
+                new AssertionErrorNode(tree, condition, null, nullPointerExceptionType);
+        extendWithNode(assertNode);
+        NodeWithExceptionsHolder exNode =
+                extendWithNodeWithException(
+                        new ThrowNode(null, assertNode, env.getTypeUtils()),
+                        nullPointerExceptionType);
+        exNode.setTerminatesExecution(true);
+
+        addLabelForNextNode(continueLabel);
+    }
+
     /** Holds the elements of an {@link AssertMethod} annotation. */
     protected static class AssertMethodTuple {