From b0f69e72fe9ea83af0d4cee79983be3689193672 Mon Sep 17 00:00:00 2001 From: d367wang Date: Wed, 20 May 2020 13:48:46 +0000 Subject: [PATCH 01/10] initial implementation of ThrowsException annotation --- .../dataflow/cfg/CFGBuilder.java | 29 ++++++++++- .../dataflow/qual/ThrowsException.java | 49 +++++++++++++++++++ 2 files changed, 77 insertions(+), 1 deletion(-) create mode 100644 dataflow/src/main/java/org/checkerframework/dataflow/qual/ThrowsException.java 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 48ebdfbbb0cd..7a1cd5e9dc30 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; @@ -2579,6 +2582,31 @@ public MethodInvocationNode visitMethodInvocation(MethodInvocationTree tree, Voi new MethodInvocationNode(tree, target, arguments, getCurrentPath()); Set 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); + NodeWithExceptionsHolder exNode = extendWithNodeWithException(node, thrown); + // 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 thrownTypes = element.getThrownTypes(); thrownSet.addAll(thrownTypes); @@ -2589,7 +2617,6 @@ public MethodInvocationNode visitMethodInvocation(MethodInvocationTree tree, Voi ExtendedNode extendedNode = extendWithNodeWithExceptions(node, thrownSet); /* Check for the TerminatesExecution annotation. */ - Element methodElement = TreeUtils.elementFromTree(tree); boolean terminatesExecution = annotationProvider.getDeclAnnotation(methodElement, TerminatesExecution.class) != null; 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..a562bf51684d --- /dev/null +++ b/dataflow/src/main/java/org/checkerframework/dataflow/qual/ThrowsException.java @@ -0,0 +1,49 @@ +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. + * + *

The annotation enables flow-sensitive type refinement to be more precise. For example, after + * + * 

+ * if (x == null) {
+ *   buildAndThrowNullPointerException();
+ * }
+ *
+ * + * where method {@code buildAndThrowNullPointerException()} is defined as + * + * 
+ * public buildAndThrowNullPointerException() {
+ *     throw new NullPointerException();
+ * }
+ *
+ * + * the Nullness Checker can determine that {@code x} is non-null. + * + *

+ * + *

The annotation's value represents the type of exception that the method throws. By default, + * the type is {@code Throwable}. + * + *

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() default Throwable.class; +} From cd3eeb52b5c0b3f6fec7d731c67ba2b6706c9e6c Mon Sep 17 00:00:00 2001 From: d367wang Date: Wed, 3 Jun 2020 01:32:19 +0000 Subject: [PATCH 02/10] add test cases --- checker/tests/nullness/flow/Issue2076.java | 29 ++++++++++++++++++++++ 1 file changed, 29 insertions(+) create mode 100644 checker/tests/nullness/flow/Issue2076.java diff --git a/checker/tests/nullness/flow/Issue2076.java b/checker/tests/nullness/flow/Issue2076.java new file mode 100644 index 000000000000..536722994b88 --- /dev/null +++ b/checker/tests/nullness/flow/Issue2076.java @@ -0,0 +1,29 @@ +// 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(); + } else { + n = obj.hashCode(); + } + } +} From ae80a09f334d913c0fd0bb23abc5ac6af38541ed Mon Sep 17 00:00:00 2001 From: d367wang Date: Wed, 3 Jun 2020 16:01:47 +0000 Subject: [PATCH 03/10] remove redundant

in ThrowsException Javadoc --- .../org/checkerframework/dataflow/qual/ThrowsException.java | 2 -- 1 file changed, 2 deletions(-) diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/qual/ThrowsException.java b/dataflow/src/main/java/org/checkerframework/dataflow/qual/ThrowsException.java index a562bf51684d..f5bf757110d7 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/qual/ThrowsException.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/qual/ThrowsException.java @@ -28,8 +28,6 @@ * * the Nullness Checker can determine that {@code x} is non-null. * - *

- * *

The annotation's value represents the type of exception that the method throws. By default, * the type is {@code Throwable}. * From f256c1d092734b1c6933ac8f0d101aab63ceb9d7 Mon Sep 17 00:00:00 2001 From: d367wang Date: Wed, 3 Jun 2020 16:49:56 +0000 Subject: [PATCH 04/10] modify issue 2076 test case --- checker/tests/nullness/flow/Issue2076.java | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/checker/tests/nullness/flow/Issue2076.java b/checker/tests/nullness/flow/Issue2076.java index 536722994b88..80c3001fb99b 100644 --- a/checker/tests/nullness/flow/Issue2076.java +++ b/checker/tests/nullness/flow/Issue2076.java @@ -22,8 +22,7 @@ public void m2(@Nullable Object obj) { int n; if (obj == null) { buildAndThrow(); - } else { - n = obj.hashCode(); } + n = obj.hashCode(); } } From 6a8bde0e61253a148720bdfa65060df49779e5c3 Mon Sep 17 00:00:00 2001 From: d367wang Date: Mon, 8 Jun 2020 08:15:17 +0000 Subject: [PATCH 05/10] add edges for @ThrowsException and @TerminatesExecution method --- .../dataflow/cfg/CFGBuilder.java | 44 ++++++++++++++++++- 1 file changed, 42 insertions(+), 2 deletions(-) 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 57a3d64a550f..7680c05faa4c 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/CFGBuilder.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/CFGBuilder.java @@ -304,6 +304,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, can the execution terminates normally? e.g., + * ("System.exit()" can terminate the execution narmally) v.s. (A throw statement never + * terminates normally). + */ + protected boolean canTerminateNormally = false; + public ExtendedNode(ExtendedNodeType type) { this.type = type; } @@ -320,14 +327,31 @@ public ExtendedNodeType getType() { return type; } + /** + * @return the flag that indicates whether this node can terminate the execution normally. + */ public boolean getTerminatesExecution() { return terminatesExecution; } + /** + * Set the flag that indicates whether this node can terminate the execution normally. + * + * @param canTerminateNormally The flag that indicates whether this node can terminate the + * execution normally. + */ public void setTerminatesExecution(boolean terminatesExecution) { this.terminatesExecution = terminatesExecution; } + public boolean getCanTerminateNormally() { + return canTerminateNormally; + } + + public void setCanTerminateNormally(boolean canTerminateNormally) { + this.canTerminateNormally = canTerminateNormally; + } + /** * @return the node contained in this extended node (only applicable if the type is {@code * NODE} or {@code EXCEPTION_NODE}). @@ -1337,8 +1361,15 @@ 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 cases that are possible to terminate execution normally, + // like "System.exit()", still add normal edge to regular-exit block. if (!node.getTerminatesExecution()) { missingEdges.add(new Tuple<>(e, i + 1)); + + } else if (node.getCanTerminateNormally()) { + // target - regular-exit node is the last item of nodeList + Integer target = nodeList.size() - 1; + missingEdges.add(new Tuple<>(e, target)); } // exceptional edges @@ -2599,7 +2630,10 @@ public MethodInvocationNode visitMethodInvocation(MethodInvocationTree tree, Voi thrown = elements.getTypeElement(cls).asType(); } thrownSet.add(thrown); - NodeWithExceptionsHolder exNode = extendWithNodeWithException(node, 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); @@ -2610,7 +2644,8 @@ public MethodInvocationNode visitMethodInvocation(MethodInvocationTree tree, Voi // Add exceptions explicitly mentioned in the throws clause. List 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()); @@ -2620,8 +2655,13 @@ public MethodInvocationNode visitMethodInvocation(MethodInvocationTree tree, Voi 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 current node can terminate normally. (e.g. + // "System.exit()") if (terminatesExecution) { extendedNode.setTerminatesExecution(true); + extendedNode.setCanTerminateNormally(true); } return node; From 41ae712872b2e61ba8cc32197de292aa8030b032 Mon Sep 17 00:00:00 2001 From: d367wang Date: Wed, 10 Jun 2020 00:10:19 +0000 Subject: [PATCH 06/10] link node with @TerminatesExecution to exceptional-exit block --- .../dataflow/cfg/CFGBuilder.java | 53 ++++++++++--------- 1 file changed, 27 insertions(+), 26 deletions(-) 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 7680c05faa4c..9220fde405cd 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/CFGBuilder.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/CFGBuilder.java @@ -305,11 +305,11 @@ protected abstract static class ExtendedNode { protected boolean terminatesExecution = false; /** - * Provided this node terminates the execution, can the execution terminates normally? e.g., - * ("System.exit()" can terminate the execution narmally) v.s. (A throw statement never - * terminates normally). + * 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 canTerminateNormally = false; + protected boolean exitImmediately = false; public ExtendedNode(ExtendedNodeType type) { this.type = type; @@ -327,29 +327,30 @@ public ExtendedNodeType getType() { return type; } - /** - * @return the flag that indicates whether this node can terminate the execution normally. - */ public boolean getTerminatesExecution() { return terminatesExecution; } - /** - * Set the flag that indicates whether this node can terminate the execution normally. - * - * @param canTerminateNormally The flag that indicates whether this node can terminate the - * execution normally. - */ public void setTerminatesExecution(boolean terminatesExecution) { this.terminatesExecution = terminatesExecution; } - public boolean getCanTerminateNormally() { - return canTerminateNormally; + /** + * @return the flag that indicates whether this node causes the execution to exit + * immediately. + */ + public boolean isExitImmediately() { + return exitImmediately; } - public void setCanTerminateNormally(boolean canTerminateNormally) { - this.canTerminateNormally = canTerminateNormally; + /** + * 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; } /** @@ -1361,15 +1362,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 cases that are possible to terminate execution normally, - // like "System.exit()", still add normal edge to regular-exit block. + // 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.getCanTerminateNormally()) { - // target - regular-exit node is the last item of nodeList - Integer target = nodeList.size() - 1; - missingEdges.add(new Tuple<>(e, target)); + } else if (node.isExitImmediately()) { + e.setSuccessor(exceptionalExitBlock); } // exceptional edges @@ -2655,13 +2655,14 @@ public MethodInvocationNode visitMethodInvocation(MethodInvocationTree tree, Voi 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 current node can terminate normally. (e.g. - // "System.exit()") + // (2) the flag tht indicates the entire execution exits immediately. + // (e.g. "System.exit()") if (terminatesExecution) { extendedNode.setTerminatesExecution(true); - extendedNode.setCanTerminateNormally(true); + extendedNode.setExitImmediately(true); } return node; From 11721c16b52bc4b0a95eeda0eabe09b94891b4e3 Mon Sep 17 00:00:00 2001 From: d367wang Date: Sun, 12 Jul 2020 16:47:21 -0400 Subject: [PATCH 07/10] remove flag exitImmediately and recover the handling of @TerminatesExecution --- checker/tests/nullness/flow/Issue2076.java | 5 +- .../dataflow/cfg/CFGBuilder.java | 62 ++++--------------- 2 files changed, 15 insertions(+), 52 deletions(-) diff --git a/checker/tests/nullness/flow/Issue2076.java b/checker/tests/nullness/flow/Issue2076.java index 80c3001fb99b..5cb8938854c7 100644 --- a/checker/tests/nullness/flow/Issue2076.java +++ b/checker/tests/nullness/flow/Issue2076.java @@ -9,11 +9,14 @@ 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) { - buildAndThrow(); + buildAndThrowNPE(); } return mObj; } 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 b2e0bc4a74c8..1ef742996912 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/CFGBuilder.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/CFGBuilder.java @@ -304,13 +304,6 @@ 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. * @@ -340,27 +333,6 @@ 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}). @@ -1379,14 +1351,8 @@ 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 @@ -2639,27 +2605,28 @@ public MethodInvocationNode visitMethodInvocation(MethodInvocationTree tree, Voi Set thrownSet = new HashSet<>(); Element methodElement = TreeUtils.elementFromTree(tree); - // detect the existence of ThrowsException annotation + // 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", false) + AnnotationUtils.getElementValueClassName(throwAnno, "value", true) .toString(); - if (cls == null) { // thrown type is Throwable by default - thrown = elements.getTypeElement("java.lang.Throwable").asType(); - } else { - thrown = elements.getTypeElement(cls).asType(); - } + thrown = elements.getTypeElement(cls).asType(); thrownSet.add(thrown); + + // Even if the method unconditionally throws another type of exception, add + // Throwable to the thrownSet to account for special cases. + // e.g. a method is always possible to cause an OutOfMemoryError. 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; @@ -2668,8 +2635,7 @@ public MethodInvocationNode visitMethodInvocation(MethodInvocationTree tree, Voi // Add exceptions explicitly mentioned in the throws clause. List thrownTypes = element.getThrownTypes(); thrownSet.addAll(thrownTypes); - // Add Throwable to account for special cases, - // e.g. a method is always possible to throw an OutOfMemoryError + // Add Throwable to account for unchecked exceptions TypeElement throwableElement = elements.getTypeElement("java.lang.Throwable"); thrownSet.add(throwableElement.asType()); @@ -2679,14 +2645,8 @@ public MethodInvocationNode visitMethodInvocation(MethodInvocationTree tree, Voi 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; From 3aff59a0396e3c2af8142fa80a2344209b68af3f Mon Sep 17 00:00:00 2001 From: d367wang Date: Wed, 29 Jul 2020 01:16:01 -0400 Subject: [PATCH 08/10] restrict value of @ThrowsException to be subtype of RuntimeException --- .../dataflow/cfg/CFGBuilder.java | 32 ++++++++++++------- .../dataflow/qual/ThrowsException.java | 11 +++++-- 2 files changed, 29 insertions(+), 14 deletions(-) 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 1ef742996912..14ffea09f4f8 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/CFGBuilder.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/CFGBuilder.java @@ -2620,11 +2620,9 @@ public MethodInvocationNode visitMethodInvocation(MethodInvocationTree tree, Voi thrown = elements.getTypeElement(cls).asType(); thrownSet.add(thrown); - // Even if the method unconditionally throws another type of exception, add - // Throwable to the thrownSet to account for special cases. - // e.g. a method is always possible to cause an OutOfMemoryError. - TypeElement throwableElement = elements.getTypeElement("java.lang.Throwable"); - thrownSet.add(throwableElement.asType()); + // 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); @@ -2635,9 +2633,21 @@ public MethodInvocationNode visitMethodInvocation(MethodInvocationTree tree, Voi // Add exceptions explicitly mentioned in the throws clause. 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); @@ -4242,9 +4252,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 index f5bf757110d7..57125a5fb050 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/qual/ThrowsException.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/qual/ThrowsException.java @@ -28,8 +28,13 @@ * * the Nullness Checker can determine that {@code x} is non-null. * - *

The annotation's value represents the type of exception that the method throws. By default, - * the type is {@code Throwable}. + *

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

According to the semantic "unconditionally throws exception", @ThrowsException annotation + * overrides the unchecked exception in the method signature. * *

The annotation is a trusted annotation, meaning that it is not checked whether the * annotated method really unconditionally throws an exception. @@ -43,5 +48,5 @@ @Retention(RetentionPolicy.RUNTIME) @Target({ElementType.METHOD, ElementType.CONSTRUCTOR}) public @interface ThrowsException { - Class value() default Throwable.class; + Class value() default RuntimeException.class; } From be5df7e6d8b5ba2df5af5994a55015c2329ad311 Mon Sep 17 00:00:00 2001 From: d367wang Date: Tue, 6 Oct 2020 21:29:20 -0400 Subject: [PATCH 09/10] redefine @ThrowsException semantic --- .../flow/ThrowExceptionAnnotationTest.java | 68 +++++++++++++++++++ .../dataflow/cfg/CFGBuilder.java | 49 ++++++++++--- .../dataflow/qual/ThrowsException.java | 34 ++++++---- 3 files changed, 125 insertions(+), 26 deletions(-) create mode 100644 checker/tests/nullness/flow/ThrowExceptionAnnotationTest.java 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 14ffea09f4f8..69b1c277bbf4 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/CFGBuilder.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/CFGBuilder.java @@ -2604,33 +2604,60 @@ public MethodInvocationNode visitMethodInvocation(MethodInvocationTree tree, Voi Set thrownSet = new HashSet<>(); - Element methodElement = TreeUtils.elementFromTree(tree); - // Detect the existence of @ThrowsException AnnotationMirror throwAnno = - annotationProvider.getDeclAnnotation(methodElement, ThrowsException.class); + annotationProvider.getDeclAnnotation(element, 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. + // If @ThrowsException exists, validate the thrown type it specifies by comparing it + // to the method declaration. TypeMirror thrown; - // get type of thrown exception String cls = - AnnotationUtils.getElementValueClassName(throwAnno, "value", true) + 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; } - // Add exceptions explicitly mentioned in the throws clause. + // 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); @@ -2653,7 +2680,7 @@ public MethodInvocationNode visitMethodInvocation(MethodInvocationTree tree, Voi /* Check for the TerminatesExecution annotation. */ boolean terminatesExecution = - annotationProvider.getDeclAnnotation(methodElement, TerminatesExecution.class) + annotationProvider.getDeclAnnotation(element, TerminatesExecution.class) != null; if (terminatesExecution) { extendedNode.setTerminatesExecution(true); diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/qual/ThrowsException.java b/dataflow/src/main/java/org/checkerframework/dataflow/qual/ThrowsException.java index 57125a5fb050..fc2dc8ff3ba1 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/qual/ThrowsException.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/qual/ThrowsException.java @@ -7,34 +7,38 @@ import java.lang.annotation.Target; /** - * {@code ThrowException} is a method annotation that indicates that a method always throws an - * exception. + * {@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, after + *

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

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

- * if (x == null) {
- *   buildAndThrowNullPointerException();
+ * public throwsNullPointerException() {
+ *     throw new NullPointerException();
  * }
  *
* - * where method {@code buildAndThrowNullPointerException()} is defined as + * then after the following code * * 
- * public buildAndThrowNullPointerException() {
- *     throw new NullPointerException();
+ * 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 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. + *

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. * - *

According to the semantic "unconditionally throws exception", @ThrowsException annotation - * overrides the unchecked exception 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. @@ -48,5 +52,5 @@ @Retention(RetentionPolicy.RUNTIME) @Target({ElementType.METHOD, ElementType.CONSTRUCTOR}) public @interface ThrowsException { - Class value() default RuntimeException.class; + Class value(); } From dba393f37a8bb4b49adcf3a2aae97c492d433c05 Mon Sep 17 00:00:00 2001 From: d367wang Date: Tue, 6 Oct 2020 22:47:06 -0400 Subject: [PATCH 10/10] update test case Issue2076 --- checker/tests/nullness/flow/Issue2076.java | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/checker/tests/nullness/flow/Issue2076.java b/checker/tests/nullness/flow/Issue2076.java index 5cb8938854c7..3f0c6e16a983 100644 --- a/checker/tests/nullness/flow/Issue2076.java +++ b/checker/tests/nullness/flow/Issue2076.java @@ -11,9 +11,6 @@ public class Issue2076 { @ThrowsException(NullPointerException.class) public void buildAndThrowNPE() {} - @ThrowsException - public void buildAndThrow() {} - public @NonNull Object m1() { if (mObj == null) { buildAndThrowNPE(); @@ -24,7 +21,7 @@ public void buildAndThrow() {} public void m2(@Nullable Object obj) { int n; if (obj == null) { - buildAndThrow(); + buildAndThrowNPE(); } n = obj.hashCode(); }