Unify AssertMethod and IfNullThrows in CFG, move IfNullThrows to Nullness

Author: HenryXi1

…ramework/dataflow/qual/IfNullThrows.java …/checker/nullness/qual/IfNullThrows.javachecker-qual/src/main/java/org/checkerframework/dataflow/qual/IfNullThrows.java renamed to checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/IfNullThrows.java checker-qual/src/main/java/org/checkerframework/dataflow/qual/IfNullThrows.java renamed to checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/IfNullThrows.java

@@ -1,4 +1,4 @@
-package org.checkerframework.dataflow.qual;
+package org.checkerframework.checker.nullness.qual;
 
 import java.lang.annotation.Documented;
 import java.lang.annotation.ElementType;

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

@@ -5,6 +5,7 @@
 import com.sun.source.tree.ArrayAccessTree;
 import com.sun.source.tree.ArrayTypeTree;
 import com.sun.source.tree.AssertTree;
+import com.sun.source.tree.BlockTree;
 import com.sun.source.tree.BinaryTree;
 import com.sun.source.tree.CaseTree;
 import com.sun.source.tree.CatchTree;
@@ -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,49 @@ 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

@@ -2,7 +2,7 @@
 // Nullness Checker.
 
 import org.checkerframework.checker.nullness.qual.Nullable;
-import org.checkerframework.dataflow.qual.IfNullThrows;
+import org.checkerframework.checker.nullness.qual.IfNullThrows;
 
 public class IfNullThrowsTest {
 
@@ -45,4 +45,16 @@ void useRequireBothNonNull(@Nullable Object x, @Nullable Object 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;
+    }
 }