Implement @ThrowsException annotation

checker/tests/nullness/flow/Issue2076.java

@@ -0,0 +1,31 @@
+// 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() {}
+
+    @ThrowsException
+    public void buildAndThrow() {}
+
+    public @NonNull Object m1() {
+        if (mObj == null) {
+            buildAndThrowNPE();
+        }
+        return mObj;
+    }
+
+    public void m2(@Nullable Object obj) {
+        int n;
+        if (obj == null) {
+            buildAndThrow();
+        }
+        n = obj.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,17 +2603,55 @@ public MethodInvocationNode visitMethodInvocation(MethodInvocationTree tree, Voi
                     new MethodInvocationNode(tree, target, arguments, getCurrentPath());
 
             Set<TypeMirror> thrownSet = new HashSet<>();
+
+            Element methodElement = TreeUtils.elementFromTree(tree);
+            // Detect the existence of @ThrowsException
+            AnnotationMirror throwAnno =
+                    annotationProvider.getDeclAnnotation(methodElement, ThrowsException.class);
+            if (throwAnno != null) {
+                // If the method is annotated with @ThrowsException, it unconditionally throws the
+                // exception specified by the value of the annotation. Then the excecution
+                // terminates.
+                TypeMirror thrown;
+                // get type of thrown exception
+                String cls =
+                        AnnotationUtils.getElementValueClassName(throwAnno, "value", true)
+                                .toString();
+                thrown = elements.getTypeElement(cls).asType();
+                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);
+                exNode.setTerminatesExecution(true);
+
+                return node;
+            }
+
             // Add exceptions explicitly mentioned in the throws clause.
             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)
                             != null;
@@ -4211,9 +4252,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,52 @@
+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 ThrowException} is a method annotation that indicates that a method always throws an
+ * exception.
+ *
+ * <p>The annotation enables flow-sensitive type refinement to be more precise. For example, after
+ *
+ * <pre>
+ * if (x == null) {
+ *   buildAndThrowNullPointerException();
+ * }
+ * </pre>
+ *
+ * where method {@code buildAndThrowNullPointerException()} is defined as
+ *
+ * <pre>
+ * public buildAndThrowNullPointerException() {
+ *     throw new NullPointerException();
+ * }
+ * </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 throws ({@code
+ * RuntimeException} by default). The type of the exception thrown is restricted to be a subtype of
+ * RuntimeException. Otherwise any checked exception should either be declared in the method
+ * signature or handled within the method.
+ *
+ * <p>According to the semantic "unconditionally throws exception", @ThrowsException annotation
+ * overrides the unchecked exception in the method signature.
+ *
+ * <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 RuntimeException> value() default RuntimeException.class;
+}