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 buildAndThrow() {}
+
+    public @NonNull Object m1() {
+        if (mObj == null) {
+            buildAndThrow();
+        }
+        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

@@ -74,6 +74,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;
@@ -175,9 +176,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;
@@ -300,6 +303,13 @@ protected abstract static class ExtendedNode {
         /** Does this node terminate the execution? (e.g., "System.exit()") */
         protected boolean terminatesExecution = false;
 
+        /**
+         * Provided this node terminates the execution, does the execution exit immediately? e.g.
+         * ("System.exit()" causes the entire execution to exit immediately) v.s. (A throw or assert
+         * statement does not).
+         */
+        protected boolean exitImmediately = false;
+
         /**
          * Create a new ExtendedNode.
          *
@@ -329,6 +339,27 @@ public void setTerminatesExecution(boolean terminatesExecution) {
             this.terminatesExecution = terminatesExecution;
         }
 
+        /**
+         * Return the flag that indicates whether this node causes the execution to exit
+         * immediately.
+         *
+         * @return the flag that indicates whether this node causes the execution to exit
+         *     immediately.
+         */
+        public boolean isExitImmediately() {
+            return exitImmediately;
+        }
+
+        /**
+         * Set the flag that indicates whether this node causes the execution to exit immediately.
+         *
+         * @param exitImmediately the flag that indicates whether this node causes the entire
+         *     execution to exit immediately.
+         */
+        public void setExitImmediately(boolean exitImmediately) {
+            this.exitImmediately = exitImmediately;
+        }
+
         /**
          * Returns the node contained in this extended node (only applicable if the type is {@code
          * NODE} or {@code EXCEPTION_NODE}).
@@ -1347,8 +1378,14 @@ public void setSuccessor(BlockImpl successor) {
                         // ensure linking between e and next block (normal edge)
                         // Note: do not link to the next block for throw statements
                         // (these throw exceptions for sure)
+                        // However, for method invocation that causes the entire execution to exit
+                        // immediately, like "System.exit()", directly link it to the exceptional
+                        // exit block.
                         if (!node.getTerminatesExecution()) {
                             missingEdges.add(new Tuple<>(e, i + 1));
+
+                        } else if (node.isExitImmediately()) {
+                            e.setSuccessor(exceptionalExitBlock);
                         }
 
                         // exceptional edges
@@ -2599,22 +2636,56 @@ 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 annotation
+            AnnotationMirror throwAnno =
+                    annotationProvider.getDeclAnnotation(methodElement, ThrowsException.class);
+            if (throwAnno != null) {
+                TypeMirror thrown;
+                // get type of thrown exception
+                String cls =
+                        AnnotationUtils.getElementValueClassName(throwAnno, "value", false)
+                                .toString();
+                if (cls == null) { // thrown type is Throwable by default
+                    thrown = elements.getTypeElement("java.lang.Throwable").asType();
+                } else {
+                    thrown = elements.getTypeElement(cls).asType();
+                }
+                thrownSet.add(thrown);
+                TypeElement throwableElement = elements.getTypeElement("java.lang.Throwable");
+                thrownSet.add(throwableElement.asType());
+
+                NodeWithExceptionsHolder exNode = extendWithNodeWithExceptions(node, thrownSet);
+                // in unconditional cases, the exceptional block has exactly one exceptional
+                // successor
+                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
+            // Add Throwable to account for special cases,
+            // e.g. a method is always possible to throw an OutOfMemoryError
             TypeElement throwableElement = elements.getTypeElement("java.lang.Throwable");
             thrownSet.add(throwableElement.asType());
 
             ExtendedNode extendedNode = extendWithNodeWithExceptions(node, thrownSet);
 
             /* Check for the TerminatesExecution annotation. */
-            Element methodElement = TreeUtils.elementFromTree(tree);
             boolean terminatesExecution =
                     annotationProvider.getDeclAnnotation(methodElement, TerminatesExecution.class)
                             != null;
+
+            // If the method is annotated with @TerminatesExecution, then set:
+            // (1) the flag that indicates current node terminates the execution
+            // (2) the flag tht indicates the entire execution exits immediately.
+            // (e.g. "System.exit()")
             if (terminatesExecution) {
                 extendedNode.setTerminatesExecution(true);
+                extendedNode.setExitImmediately(true);
             }
 
             return node;

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

@@ -0,0 +1,47 @@
+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. By default,
+ * the type is {@code Throwable}.
+ *
+ * <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() default Throwable.class;
+}