diff --git a/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsAnnotatedTypeFactory.java index 312d902974b..3aa1c3da044 100644 --- a/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsAnnotatedTypeFactory.java @@ -11,6 +11,7 @@ import javax.lang.model.element.Element; import javax.lang.model.element.ExecutableElement; import javax.lang.model.element.TypeElement; +import javax.lang.model.type.DeclaredType; import javax.lang.model.type.TypeKind; import javax.lang.model.type.TypeMirror; import org.checkerframework.checker.calledmethods.builder.AutoValueSupport; @@ -39,6 +40,7 @@ import org.checkerframework.javacutil.AnnotationUtils; import org.checkerframework.javacutil.ElementUtils; import org.checkerframework.javacutil.TreeUtils; +import org.checkerframework.javacutil.TypesUtils; import org.checkerframework.javacutil.UserError; /** The annotated type factory for the Called Methods Checker. */ @@ -428,4 +430,21 @@ private AnnotationMirror ensuresCMAnno(String[] expressions, List called AnnotationMirror am = builder.build(); return am; } + + /** + * Returns true if the checker should ignore exceptional control flow due to the given exception + * type. + * + * @param exceptionType exception type + * @return {@code true} if {@code exceptionType} is a member of {@link + * CalledMethodsAnalysis#ignoredExceptionTypes}, {@code false} otherwise + */ + @Override + public boolean isIgnoredExceptionType(TypeMirror exceptionType) { + if (exceptionType.getKind() == TypeKind.DECLARED) { + return CalledMethodsAnalysis.ignoredExceptionTypes.contains( + TypesUtils.getQualifiedName((DeclaredType) exceptionType)); + } + return false; + } } diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessVisitor.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessVisitor.java index 5c8ce1447b3..4a3c971a619 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessVisitor.java @@ -253,6 +253,9 @@ protected boolean commonAssignmentCheck( /** Case 1: Check for null dereferencing. */ @Override public Void visitMemberSelect(MemberSelectTree tree, Void p) { + if (atypeFactory.isUnreachable(tree)) { + return super.visitMemberSelect(tree, p); + } Element e = TreeUtils.elementFromUse(tree); if (e.getKind() == ElementKind.CLASS) { if (atypeFactory.containsNullnessAnnotation(null, tree.getExpression())) { diff --git a/checker/tests/nullness/Exceptions.java b/checker/tests/nullness/Exceptions.java index 571a5781e59..c5175034aa1 100644 --- a/checker/tests/nullness/Exceptions.java +++ b/checker/tests/nullness/Exceptions.java @@ -12,9 +12,8 @@ void nonnullExceptionParam(@NonNull Exception m) { void exception(@Nullable Exception m) { try { - + throwException(); } catch (Exception e) { - // Note that this code is dead. e.getClass(); // :: error: (dereference.of.nullable) m.getClass(); // should emit error @@ -38,8 +37,8 @@ void throwException() { void reassignException() { try { + throwException(); } catch (RuntimeException e) { - // Note that this code is dead. // :: error: (assignment) e = null; throw e; diff --git a/checker/tests/nullness/TryCatch.java b/checker/tests/nullness/TryCatch.java index e6ddbb6362c..8411ddcd1e1 100644 --- a/checker/tests/nullness/TryCatch.java +++ b/checker/tests/nullness/TryCatch.java @@ -23,7 +23,6 @@ void unreachableCatch(String[] xs) { try { } catch (Throwable e) { // Note that this code is dead. - // :: error: (dereference.of.nullable) t.toString(); } } diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/ControlFlowGraph.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/ControlFlowGraph.java index b94b657044a..d122d1a7dc7 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/ControlFlowGraph.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/ControlFlowGraph.java @@ -20,6 +20,8 @@ import java.util.Set; import java.util.StringJoiner; import java.util.concurrent.atomic.AtomicLong; +import java.util.function.Function; +import javax.lang.model.type.TypeMirror; import org.checkerframework.checker.initialization.qual.UnknownInitialization; import org.checkerframework.checker.nullness.qual.Nullable; import org.checkerframework.dataflow.analysis.AnalysisResult; @@ -28,6 +30,7 @@ import org.checkerframework.dataflow.cfg.block.ExceptionBlock; import org.checkerframework.dataflow.cfg.block.RegularBlock; import org.checkerframework.dataflow.cfg.block.SingleSuccessorBlock; +import org.checkerframework.dataflow.cfg.block.SingleSuccessorBlockImpl; import org.checkerframework.dataflow.cfg.block.SpecialBlock; import org.checkerframework.dataflow.cfg.block.SpecialBlockImpl; import org.checkerframework.dataflow.cfg.node.Node; @@ -276,6 +279,74 @@ public List getAllNodes( return result; } + /** + * Returns the set of all basic blocks in this control flow graph, except those that are + * only reachable via an exception whose type is ignored by parameter {@code + * shouldIgnoreException}. + * + * @param shouldIgnoreException returns true if it is passed a {@code TypeMirror} that should be + * ignored + * @return the set of all basic blocks in this control flow graph, except those that are + * only reachable via an exception whose type is ignored by {@code shouldIgnoreException} + */ + public Set getAllBlocks( + @UnknownInitialization(ControlFlowGraph.class) ControlFlowGraph this, + Function shouldIgnoreException) { + // This is the return value of the method. + Set visited = new LinkedHashSet<>(); + // `worklist` is always a subset of `visited`; any block in `worklist` is also in `visited`. + Queue worklist = new ArrayDeque<>(); + Block cur = entryBlock; + visited.add(entryBlock); + + // Traverse the whole control flow graph. + while (cur != null) { + if (cur instanceof ExceptionBlock) { + for (Map.Entry> entry : + ((ExceptionBlock) cur).getExceptionalSuccessors().entrySet()) { + if (!shouldIgnoreException.apply(entry.getKey())) { + for (Block b : entry.getValue()) { + if (visited.add(b)) { + worklist.add(b); + } + } + } + } + Block b = ((SingleSuccessorBlockImpl) cur).getSuccessor(); + if (b != null && visited.add(b)) { + worklist.add(b); + } + + } else { + for (Block b : cur.getSuccessors()) { + if (visited.add(b)) { + worklist.add(b); + } + } + } + cur = worklist.poll(); + } + + return visited; + } + + /** + * Returns the list of all nodes in this control flow graph, except those that are only + * reachable via an exception whose type is ignored by parameter {@code shouldIgnoreException}. + * + * @param shouldIgnoreException returns true if it is passed a {@code TypeMirror} that should be + * ignored + * @return the list of all nodes in this control flow graph, except those that are only + * reachable via an exception whose type is ignored by {@code shouldIgnoreException} + */ + public List getAllNodes( + @UnknownInitialization(ControlFlowGraph.class) ControlFlowGraph this, + Function shouldIgnoreException) { + List result = new ArrayList<>(); + getAllBlocks(shouldIgnoreException).forEach(b -> result.addAll(b.getNodes())); + return result; + } + /** * Returns all basic blocks in this control flow graph, in reversed depth-first postorder. Blocks * may appear more than once in the sequence. diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java index 6f900e062d1..f790dfe171d 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -4815,7 +4815,9 @@ protected TypeValidator createTypeValidator() { */ protected final boolean shouldSkipUses(ExpressionTree exprTree) { // System.out.printf("shouldSkipUses: %s: %s%n", exprTree.getClass(), exprTree); - + if (atypeFactory.isUnreachable(exprTree)) { + return true; + } Element elm = TreeUtils.elementFromTree(exprTree); return checker.shouldSkipUses(elm); } diff --git a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java index e5e3bd55076..e930656e3ba 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java @@ -445,6 +445,7 @@ public void setRoot(@Nullable CompilationUnitTree root) { super.setRoot(root); this.scannedClasses.clear(); + this.reachableNodes.clear(); this.flowResult = null; this.regularExitStores.clear(); this.exceptionalExitStores.clear(); @@ -1056,6 +1057,32 @@ public IPair getExpressionAndOffsetFromJavaExpressionStr return value != null ? value.getAnnotations().iterator().next() : null; } + /** + * Returns true if the {@code exprTree} is unreachable. This is a conservative estimate and may + * return {@code false} even though the {@code exprTree} is unreachable. + * + * @param exprTree an expression tree + * @return true if the {@code exprTree} is unreachable + */ + public boolean isUnreachable(ExpressionTree exprTree) { + if (!everUseFlow) { + return false; + } + Set nodes = getNodesForTree(exprTree); + if (nodes == null) { + // Dataflow has no any information about the tree, so conservatively consider the tree + // reachable. + return false; + } + for (Node n : nodes) { + if (n.getTree() != null && reachableNodes.contains(n.getTree())) { + return false; + } + } + // None of the corresponding nodes is reachable, so this tree is dead. + return true; + } + /** * Track the state of org.checkerframework.dataflow analysis scanning for each class tree in the * compilation unit. @@ -1070,6 +1097,16 @@ protected enum ScanState { /** Map from ClassTree to their dataflow analysis state. */ protected final Map scannedClasses = new HashMap<>(); + /** + * A set of trees whose corresponding nodes are reachable. This is not an exhaustive set of + * reachable trees. Use {@link #isUnreachable(ExpressionTree)} instead of this set directly. + * + *

This cannot be a set of Nodes, because two LocalVariableNodes are equal if they have the + * same name but represent different uses of the variable. So instead of storing Nodes, it stores + * the result of {@code Node#getTree}. + */ + private final Set reachableNodes = new HashSet<>(); + /** * The result of the flow analysis. Invariant: * @@ -1264,10 +1301,11 @@ public Store getStoreAfter(Node node) { /** * See {@link org.checkerframework.dataflow.analysis.AnalysisResult#getNodesForTree(Tree)}. * + * @param tree a tree * @return the {@link Node}s for a given {@link Tree} * @see org.checkerframework.dataflow.analysis.AnalysisResult#getNodesForTree(Tree) */ - public Set getNodesForTree(Tree tree) { + public @Nullable Set getNodesForTree(Tree tree) { return flowResult.getNodesForTree(tree); } @@ -1531,7 +1569,13 @@ protected void analyze( boolean isStatic, @Nullable Store capturedStore) { ControlFlowGraph cfg = CFCFGBuilder.build(root, ast, checker, this, processingEnv); - + cfg.getAllNodes(this::isIgnoredExceptionType) + .forEach( + node -> { + if (node.getTree() != null) { + reachableNodes.add(node.getTree()); + } + }); if (isInitializationCode) { Store initStore = !isStatic ? initializationStore : initializationStaticStore; if (initStore != null) { @@ -1610,6 +1654,16 @@ protected void analyze( postAnalyze(cfg); } + /** + * Returns true if {@code typeMirror} is an exception type that should be ignored. + * + * @param typeMirror an exception type + * @return true if {@code typeMirror} is an exception type that should be ignored + */ + public boolean isIgnoredExceptionType(TypeMirror typeMirror) { + return false; + } + /** * Perform any additional operations on a CFG. Called once per CFG, after the CFG has been * analyzed by {@link #analyze(Queue, Queue, UnderlyingAST, List, ClassTree, boolean, boolean,