diff --git a/checker/tests/nullness/flow/Issue2076.java b/checker/tests/nullness/flow/Issue2076.java new file mode 100644 index 000000000000..3f0c6e16a983 --- /dev/null +++ b/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(); + } +} diff --git a/checker/tests/nullness/flow/ThrowExceptionAnnotationTest.java b/checker/tests/nullness/flow/ThrowExceptionAnnotationTest.java new file mode 100644 index 000000000000..c04614b21c24 --- /dev/null +++ b/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(); + } +} diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/CFGBuilder.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/CFGBuilder.java index f42d5a1d4633..69b1c277bbf4 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/CFGBuilder.java +++ b/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 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 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 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 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); diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/qual/ThrowsException.java b/dataflow/src/main/java/org/checkerframework/dataflow/qual/ThrowsException.java new file mode 100644 index 000000000000..fc2dc8ff3ba1 --- /dev/null +++ b/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. + * + *

The annotation enables flow-sensitive type refinement to be more precise. + * + *

For example, given a method {@code throwsNullPointerException()} defined as + * + * 

+ * public throwsNullPointerException() {
+ *     throw new NullPointerException();
+ * }
+ *
+ * + * then after the following code + * + * 
+ * if (x == null) {
+ *   throwsNullPointerException();
+ * }
+ *
+ * + * the Nullness Checker can determine that {@code x} is non-null. + * + *

The annotation's value represents the type of exception that the method unconditionally + * 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. + * + *

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 + * compatible, 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. + * + *

The annotation is a trusted annotation, meaning that it is not checked whether the + * annotated method really unconditionally throws an exception. + * + *

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 value(); +}