Implement @ThrowsException annotation

checker/tests/nullness/flow/Issue2076.java

@@ -0,0 +1,28 @@
+// Test case for issue #2076:
+// https://github.com/typetools/checker-framework/issues/2076
+
+import org.checkerframework.checker.nullness.qual.NonNull;
+import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.dataflow.qual.ThrowsException;
+
+public class Issue2076 {
+    private @Nullable Object mObj = null;
+
+    @ThrowsException(NullPointerException.class)
+    public void buildAndThrowNPE() {}
+
+    public @NonNull Object m1() {
+        if (mObj == null) {
+            buildAndThrowNPE();
+        }
+        return mObj;
+    }
+
+    public void m2(@Nullable Object obj) {
+        int n;
+        if (obj == null) {
+            buildAndThrowNPE();
+        }
+        n = obj.hashCode();
+    }
+}

checker/tests/nullness/flow/ThrowExceptionAnnotationTest.java

@@ -0,0 +1,68 @@
+import java.io.IOException;
+import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.dataflow.qual.ThrowsException;
+
+public class ThrowExceptionAnnotationTest {
+    private @Nullable Object mObj = null;
+
+    @ThrowsException(IOException.class)
+    public void foo() throws IOException {}
+
+    @ThrowsException(NullPointerException.class)
+    public void bar() {}
+
+    public void m1(@Nullable Object obj) {
+        int n;
+        try {
+            foo();
+
+            // :: error: (dereference.of.nullable)
+            int x = obj.hashCode();
+
+        } catch (IOException e) {
+            // :: error: (dereference.of.nullable)
+            int x = obj.hashCode();
+        } finally {
+        }
+    }
+
+    public void m2(@Nullable Object obj) {
+        int n;
+        try {
+            foo();
+
+        } catch (IOException e) {
+        } finally {
+            // :: error: (dereference.of.nullable)
+            int x = obj.hashCode();
+        }
+    }
+
+    public void m3(@Nullable Object obj) {
+        int n;
+        try {
+            foo();
+
+        } catch (IOException e) {
+        } finally {
+        }
+
+        // :: error: (dereference.of.nullable)
+        int x = obj.hashCode();
+    }
+
+    public void m4(@Nullable Object obj) throws IOException {
+        int n;
+        if (obj == null) {
+            foo();
+        }
+        n = obj.hashCode();
+    }
+
+    public void m5() {
+        if (mObj == null) {
+            bar();
+        }
+        int x = mObj.hashCode();
+    }
+}

dataflow/src/main/java/org/checkerframework/dataflow/cfg/CFGBuilder.java

@@ -75,6 +75,7 @@
 import java.util.Set;
 import java.util.StringJoiner;
 import javax.annotation.processing.ProcessingEnvironment;
+import javax.lang.model.element.AnnotationMirror;
 import javax.lang.model.element.Element;
 import javax.lang.model.element.ElementKind;
 import javax.lang.model.element.ExecutableElement;
@@ -176,9 +177,11 @@
 import org.checkerframework.dataflow.cfg.node.VariableDeclarationNode;
 import org.checkerframework.dataflow.cfg.node.WideningConversionNode;
 import org.checkerframework.dataflow.qual.TerminatesExecution;
+import org.checkerframework.dataflow.qual.ThrowsException;
 import org.checkerframework.dataflow.util.IdentityMostlySingleton;
 import org.checkerframework.dataflow.util.MostlySingleton;
 import org.checkerframework.javacutil.AnnotationProvider;
+import org.checkerframework.javacutil.AnnotationUtils;
 import org.checkerframework.javacutil.BasicAnnotationProvider;
 import org.checkerframework.javacutil.BugInCF;
 import org.checkerframework.javacutil.ElementUtils;
@@ -2600,19 +2603,84 @@ public MethodInvocationNode visitMethodInvocation(MethodInvocationTree tree, Voi
                     new MethodInvocationNode(tree, target, arguments, getCurrentPath());
 
             Set<TypeMirror> thrownSet = new HashSet<>();
-            // Add exceptions explicitly mentioned in the throws clause.
+
+            AnnotationMirror throwAnno =
+                    annotationProvider.getDeclAnnotation(element, ThrowsException.class);
+            if (throwAnno != null) {
+                // If @ThrowsException exists, validate the thrown type it specifies by comparing it
+                // to the method declaration.
+                TypeMirror thrown;
+                String cls =
+                        AnnotationUtils.getElementValueClassName(throwAnno, "value", false)
+                                .toString();
+                thrown = elements.getTypeElement(cls).asType();
+
+                TypeMirror runtimeExceptionType =
+                        elements.getTypeElement("java.lang.RuntimeException").asType();
+                TypeMirror errorType = elements.getTypeElement("java.lang.Error").asType();
+                if (!types.isSubtype(thrown, runtimeExceptionType)
+                        && !types.isSubtype(thrown, errorType)) {
+                    // If @ThrowsException specifies that the method throws a checked exception,
+                    // check if the thrown exception is a subtype of one of the exceptions in the
+                    // method's throws clause.
+                    boolean isThrownInDecl = false;
+                    List<? extends TypeMirror> declaredThrownTypes = element.getThrownTypes();
+                    for (TypeMirror t : declaredThrownTypes) {
+                        if (types.isSubtype(thrown, t)) {
+                            isThrownInDecl = true;
+                            break;
+                        }
+                    }
+
+                    if (!isThrownInDecl) {
+                        // If the thrown exception specified in @ThrowsException is not a subtype of
+                        // any
+                        // of the exceptions in the method's throws clause, issue an error.
+                        throw new BugInCF(
+                                "The thrown type specified in @ThrowsException is not compatible to method declaration");
+                    }
+                }
+
+                // Only add the type of exception specified in the @ThrowsException to the thrown
+                // set, while ignoring the exceptions in the method signature.
+                thrownSet.add(thrown);
+
+                // Since a method invocation is always possible to throw a runtime error, add it to
+                // the thrown set.
+                thrownSet.add(elements.getTypeElement("java.lang.Error").asType());
+                NodeWithExceptionsHolder exNode = extendWithNodeWithExceptions(node, thrownSet);
+
+                // Terminates the normal execution
+                exNode.setTerminatesExecution(true);
+
+                return node;
+            }
+
+            // If the invoked method is not annotated with @ThrowsException, add the explicit
+            // exceptions in the method declaration if any exists.
             List<? extends TypeMirror> thrownTypes = element.getThrownTypes();
             thrownSet.addAll(thrownTypes);
-            // Add Throwable to account for unchecked exceptions
-            TypeElement throwableElement = elements.getTypeElement("java.lang.Throwable");
-            thrownSet.add(throwableElement.asType());
+
+            // Check if the above explicit exceptions contains Throwable. If so, Throwable is
+            // already added to the thrownSet of the exception node, so we do not have to add
+            // RuntimeException or Error anymore; Otherwise, add these two types.
+            boolean throwsThrowable = false;
+            for (TypeMirror t : thrownTypes) {
+                if (TypesUtils.isThrowable(t)) {
+                    throwsThrowable = true;
+                    break;
+                }
+            }
+            if (!throwsThrowable) {
+                thrownSet.add(elements.getTypeElement("java.lang.RuntimeException").asType());
+                thrownSet.add(elements.getTypeElement("java.lang.Error").asType());
+            }
 
             ExtendedNode extendedNode = extendWithNodeWithExceptions(node, thrownSet);
 
             /* Check for the TerminatesExecution annotation. */
-            Element methodElement = TreeUtils.elementFromTree(tree);
             boolean terminatesExecution =
-                    annotationProvider.getDeclAnnotation(methodElement, TerminatesExecution.class)
+                    annotationProvider.getDeclAnnotation(element, TerminatesExecution.class)
                             != null;
             if (terminatesExecution) {
                 extendedNode.setTerminatesExecution(true);
@@ -4211,9 +4279,9 @@ public Node visitNewClass(NewClassTree tree, Void p) {
             // Add exceptions explicitly mentioned in the throws clause.
             List<? extends TypeMirror> thrownTypes = constructor.getThrownTypes();
             thrownSet.addAll(thrownTypes);
-            // Add Throwable to account for unchecked exceptions
-            TypeElement throwableElement = elements.getTypeElement("java.lang.Throwable");
-            thrownSet.add(throwableElement.asType());
+            // Add RuntimeException and Error to account for unchecked exceptions
+            thrownSet.add(elements.getTypeElement("java.lang.RuntimeException").asType());
+            thrownSet.add(elements.getTypeElement("java.lang.Error").asType());
 
             extendWithNodeWithExceptions(node, thrownSet);
 

dataflow/src/main/java/org/checkerframework/dataflow/qual/ThrowsException.java

@@ -0,0 +1,56 @@
+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;
+
+/**
+ * {@code ThrowsException} is a method declaration annotation indicating that a method always throws
+ * an exception.
+ *
+ * <p>The annotation enables flow-sensitive type refinement to be more precise.
+ *
+ * <p>For example, given a method {@code throwsNullPointerException()} defined as
+ *
+ * <pre>
+ * public throwsNullPointerException() {
+ *     throw new NullPointerException();
+ * }
+ * </pre>
+ *
+ * then after the following code
+ *
+ * <pre>
+ * if (x == null) {
+ *   throwsNullPointerException();
+ * }
+ * </pre>
+ *
+ * the Nullness Checker can determine that {@code x} is non-null.
+ *
+ * <p>The annotation's value represents the type of exception that the method <b>unconditionally</b>
+ * throws. The type of the exception can be checked exception, unchecked exception and error.
+ * Whichever the case is, Checker Framework always assumes the type specified in {@code
+ * ThrowsException} annotation overrides the one specified in the method signature.
+ *
+ * <p>Note that when the method itself already declares to throw a checked exception, then the type
+ * of exception specified in {@code ThrowsException} annotation is required to be
+ * <em>compatible</em>, means the type specified in {@code ThrowsException} annotation is a subtype
+ * of the one specified in the method declaration. Otherwise Checker Framework issues an error.
+ *
+ * <p>The annotation is a <em>trusted</em> annotation, meaning that it is not checked whether the
+ * annotated method really unconditionally throws an exception.
+ *
+ * <p>This annotation is inherited by subtypes, just as if it were meta-annotated with
+ * {@code @InheritedAnnotation}.
+ */
+// @InheritedAnnotation cannot be written here, because "dataflow" project cannot depend on
+// "framework" project.
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
+public @interface ThrowsException {
+    Class<? extends Throwable> value();
+}