From 2929a3977db15f247ede4f645b8d3326c81821e6 Mon Sep 17 00:00:00 2001 From: Martin Kellogg Date: Tue, 17 Aug 2021 21:14:33 +0000 Subject: [PATCH] Fix unsoundess in Resource Leak Checker related to owning fields and EnsuresCalledMethods (#4869) --- .../calledmethods/CalledMethodsAnalysis.java | 28 +++++-- .../resourceleak/ResourceLeakVisitor.java | 76 +++++++++++++++++++ .../checker/resourceleak/messages.properties | 1 + ...MultipleMethodParamsMustCallAliasTest.java | 1 + .../resourceleak/ReplicaInputStreams.java | 28 +++++++ .../resourceleak/ReplicaInputStreams2.java | 31 ++++++++ .../tests/resourceleak/TwoResourcesECM.java | 35 +++++++++ docs/manual/resource-leak-checker.tex | 7 +- 8 files changed, 198 insertions(+), 9 deletions(-) create mode 100644 checker/tests/resourceleak/ReplicaInputStreams.java create mode 100644 checker/tests/resourceleak/ReplicaInputStreams2.java create mode 100644 checker/tests/resourceleak/TwoResourcesECM.java diff --git a/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsAnalysis.java b/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsAnalysis.java index 6ac945a4b9b..7d961e85df5 100644 --- a/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsAnalysis.java +++ b/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsAnalysis.java @@ -1,6 +1,8 @@ package org.checkerframework.checker.calledmethods; import com.sun.tools.javac.code.Type; +import java.util.HashSet; +import java.util.Set; import javax.lang.model.type.TypeMirror; import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.framework.flow.CFAnalysis; @@ -20,21 +22,31 @@ public class CalledMethodsAnalysis extends CFAnalysis { protected CalledMethodsAnalysis( BaseTypeChecker checker, CalledMethodsAnnotatedTypeFactory factory) { super(checker, factory); + // Use the Nullness Checker. + ignoredExceptionTypes.add("java.lang.NullPointerException"); + // Ignore run-time errors, which cannot be predicted statically. Doing so is unsound + // in the sense that they could still occur - e.g., the program could run out of memory - + // but if they did, the checker's results would be useless anyway. + ignoredExceptionTypes.add("java.lang.Error"); + ignoredExceptionTypes.add("java.lang.RuntimeException"); } /** - * Ignore exceptional control flow due to {@code NullPointerException}s, as this checker assumes - * the Nullness Checker will be used to prevent such exceptions. + * The fully-qualified names of the exception types that are ignored by this checker when + * computing dataflow stores. + */ + private final Set ignoredExceptionTypes = new HashSet<>(); + + /** + * Ignore exceptional control flow due to ignored exception types. * * @param exceptionType exception type - * @return {@code true} if {@code exceptionType} is {@code NullPointerException}, {@code false} - * otherwise + * @return {@code true} if {@code exceptionType} is a member of {@link #ignoredExceptionTypes}, + * {@code false} otherwise */ @Override protected boolean isIgnoredExceptionType(TypeMirror exceptionType) { - return ((Type) exceptionType) - .tsym - .getQualifiedName() - .contentEquals("java.lang.NullPointerException"); + return ignoredExceptionTypes.contains( + ((Type) exceptionType).tsym.getQualifiedName().toString()); } } diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakVisitor.java b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakVisitor.java index c7c1479b2f2..e1e6adef3bb 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakVisitor.java @@ -4,10 +4,12 @@ import com.sun.source.tree.VariableTree; import java.util.ArrayList; import java.util.List; +import java.util.Set; import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.Element; import javax.lang.model.element.ElementKind; import javax.lang.model.element.ExecutableElement; +import javax.lang.model.element.TypeElement; import org.checkerframework.checker.calledmethods.CalledMethodsVisitor; import org.checkerframework.checker.calledmethods.qual.EnsuresCalledMethods; import org.checkerframework.checker.mustcall.CreatesMustCallForElementSupplier; @@ -16,6 +18,10 @@ import org.checkerframework.checker.mustcall.qual.CreatesMustCallFor; import org.checkerframework.checker.mustcall.qual.Owning; import org.checkerframework.common.basetype.BaseTypeChecker; +import org.checkerframework.dataflow.expression.JavaExpression; +import org.checkerframework.framework.flow.CFAbstractStore; +import org.checkerframework.framework.flow.CFAbstractValue; +import org.checkerframework.framework.type.QualifierHierarchy; import org.checkerframework.javacutil.AnnotationUtils; import org.checkerframework.javacutil.ElementUtils; import org.checkerframework.javacutil.TreeUtils; @@ -80,6 +86,76 @@ public Void visitMethod(MethodTree node, Void p) { return super.visitMethod(node, p); } + // Overwritten to check that destructors (i.e. methods responsible for resolving + // the must-call obligations of owning fields) enforce a stronger version of + // @EnsuresCalledMethods: that the claimed @CalledMethods annotation is true on + // both exceptional and regular exits, not just on regular exits. + @Override + protected void checkPostcondition( + MethodTree methodTree, AnnotationMirror annotation, JavaExpression expression) { + super.checkPostcondition(methodTree, annotation, expression); + // Only check if the required annotation is a CalledMethods annotation (implying + // the method was annotated with @EnsuresCalledMethods). + if (!AnnotationUtils.areSameByName( + annotation, "org.checkerframework.checker.calledmethods.qual.CalledMethods")) { + return; + } + if (!isMustCallMethod(methodTree)) { + // In this case, the method has an EnsuresCalledMethods annotation but is not a destructor, + // so no further checking is required. + return; + } + CFAbstractStore exitStore = atypeFactory.getExceptionalExitStore(methodTree); + if (exitStore == null) { + // If there is no exceptional exitStore, then the method cannot throw an exception and there + // is no need to check anything else. + } else { + CFAbstractValue value = exitStore.getValue(expression); + AnnotationMirror inferredAnno = null; + if (value != null) { + QualifierHierarchy hierarchy = atypeFactory.getQualifierHierarchy(); + Set annos = value.getAnnotations(); + inferredAnno = hierarchy.findAnnotationInSameHierarchy(annos, annotation); + } + if (!checkContract(expression, annotation, inferredAnno, exitStore)) { + String inferredAnnoStr = + inferredAnno == null + ? "no information about " + expression.toString() + : inferredAnno.toString(); + checker.reportError( + methodTree, + "destructor.exceptional.postcondition", + methodTree.getName(), + expression.toString(), + inferredAnnoStr, + annotation); + } + } + } + + /** + * Returns true iff the {@code MustCall} annotation of the class that encloses the methodTree + * names this method. + * + * @param methodTree the declaration of a method + * @return whether that method is one of the must-call methods for its enclosing class + */ + private boolean isMustCallMethod(MethodTree methodTree) { + ExecutableElement elt = TreeUtils.elementFromDeclaration(methodTree); + TypeElement containingClass = ElementUtils.enclosingTypeElement(elt); + MustCallAnnotatedTypeFactory mustCallAnnotatedTypeFactory = + rlTypeFactory.getTypeFactoryOfSubchecker(MustCallChecker.class); + AnnotationMirror mcAnno = + mustCallAnnotatedTypeFactory + .getAnnotatedType(containingClass) + .getAnnotationInHierarchy(mustCallAnnotatedTypeFactory.TOP); + List mcValues = + AnnotationUtils.getElementValueArray( + mcAnno, mustCallAnnotatedTypeFactory.getMustCallValueElement(), String.class); + String methodName = elt.getSimpleName().toString(); + return mcValues.contains(methodName); + } + /** * Returns the {@link CreatesMustCallFor#value} element/argument of the given @CreatesMustCallFor * annotation, or "this" if there is none. diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/messages.properties b/checker/src/main/java/org/checkerframework/checker/resourceleak/messages.properties index aad451f1914..3e2d625de5c 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/messages.properties +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/messages.properties @@ -3,3 +3,4 @@ missing.creates.mustcall.for=This method re-assigns the non-final, owning field incompatible.creates.mustcall.for=This method re-assigns the non-final, owning field %s.%s, but its @CreatesMustCallFor annotation targets %s. reset.not.owning=Calling this method resets the must-call obligations of the expression %s, which is non-owning. Either annotate its declaration with an @Owning annotation, extract it into a local variable, or write a corresponding @CreatesMustCallFor annotation on the method that encloses this statement. creates.mustcall.for.override.invalid=Method %s cannot override method %s, which defines fewer @CreatesMustCallFor targets.\nfound: %s\nrequired: %s +destructor.exceptional.postcondition=Method %s must resolve the must-call obligations of the owning field %s along all paths, including exceptional paths. On an exceptional path, the @EnsuresCalledMethods annotation was not satisfied.\nFound: %s\nRequired: %s diff --git a/checker/tests/resourceleak/MultipleMethodParamsMustCallAliasTest.java b/checker/tests/resourceleak/MultipleMethodParamsMustCallAliasTest.java index dd3113c7d6a..153a10698d8 100644 --- a/checker/tests/resourceleak/MultipleMethodParamsMustCallAliasTest.java +++ b/checker/tests/resourceleak/MultipleMethodParamsMustCallAliasTest.java @@ -79,6 +79,7 @@ class ReplicaInputStreams implements Closeable { @EnsuresCalledMethods( value = {"this.in1", "this.in2"}, methods = {"close"}) + // :: error: destructor.exceptional.postcondition public void close() throws IOException { in1.close(); in2.close(); diff --git a/checker/tests/resourceleak/ReplicaInputStreams.java b/checker/tests/resourceleak/ReplicaInputStreams.java new file mode 100644 index 00000000000..9e3656b582b --- /dev/null +++ b/checker/tests/resourceleak/ReplicaInputStreams.java @@ -0,0 +1,28 @@ +// A test case for https://github.com/typetools/checker-framework/issues/4838. + +import java.io.Closeable; +import java.io.IOException; +import java.io.InputStream; +import org.checkerframework.checker.calledmethods.qual.EnsuresCalledMethods; +import org.checkerframework.checker.mustcall.qual.Owning; + +class ReplicaInputStreams implements Closeable { + + private final @Owning InputStream in1; + private final @Owning InputStream in2; + + public ReplicaInputStreams(@Owning InputStream i1, @Owning InputStream i2) { + this.in1 = i1; + this.in2 = i2; + } + + @Override + @EnsuresCalledMethods( + value = {"this.in1", "this.in2"}, + methods = {"close"}) + // :: error: destructor.exceptional.postcondition + public void close() throws IOException { + in1.close(); + in2.close(); + } +} diff --git a/checker/tests/resourceleak/ReplicaInputStreams2.java b/checker/tests/resourceleak/ReplicaInputStreams2.java new file mode 100644 index 00000000000..c5df98e1ba0 --- /dev/null +++ b/checker/tests/resourceleak/ReplicaInputStreams2.java @@ -0,0 +1,31 @@ +// A test case for https://github.com/typetools/checker-framework/issues/4838. +// This variant uses a try-finally in the destructor, so it is correct. + +import java.io.Closeable; +import java.io.IOException; +import java.io.InputStream; +import org.checkerframework.checker.calledmethods.qual.EnsuresCalledMethods; +import org.checkerframework.checker.mustcall.qual.Owning; + +class ReplicaInputStreams2 implements Closeable { + + private final @Owning InputStream in1; + private final @Owning InputStream in2; + + public ReplicaInputStreams2(@Owning InputStream i1, @Owning InputStream i2) { + this.in1 = i1; + this.in2 = i2; + } + + @Override + @EnsuresCalledMethods( + value = {"this.in1", "this.in2"}, + methods = {"close"}) + public void close() throws IOException { + try { + in1.close(); + } finally { + in2.close(); + } + } +} diff --git a/checker/tests/resourceleak/TwoResourcesECM.java b/checker/tests/resourceleak/TwoResourcesECM.java new file mode 100644 index 00000000000..dad157ee1aa --- /dev/null +++ b/checker/tests/resourceleak/TwoResourcesECM.java @@ -0,0 +1,35 @@ +// A test case for https://github.com/typetools/checker-framework/issues/4838. +// +// This test that shows that no unsoundess occurs when a single close() method is responsible +// for closing two resources. + +import java.io.IOException; +import java.net.Socket; +import org.checkerframework.checker.calledmethods.qual.*; +import org.checkerframework.checker.mustcall.qual.*; + +@MustCall("dispose") class TwoResourcesECM { + @Owning Socket s1, s2; + + // The contracts.postcondition error below is thrown because s1 is not final, + // and therefore might theoretically be side-effected by the call to s2.close() + // even on the non-exceptional path. See ReplicaInputStreams.java for a variant + // of this test where such an error is not issued. Because this method can leak + // along both regular and exceptional exits, both errors are issued. + @EnsuresCalledMethods( + value = {"this.s1", "this.s2"}, + methods = {"close"}) + // :: error: contracts.postcondition :: error: destructor.exceptional.postcondition + public void dispose() throws IOException { + s1.close(); + s2.close(); + } + + static void test1(TwoResourcesECM obj) { + try { + obj.dispose(); + } catch (IOException ioe) { + + } + } +} diff --git a/docs/manual/resource-leak-checker.tex b/docs/manual/resource-leak-checker.tex index e75652eb4ee..b1d0ef006bf 100644 --- a/docs/manual/resource-leak-checker.tex +++ b/docs/manual/resource-leak-checker.tex @@ -221,7 +221,12 @@ destructor-like method \ must satisfy the field's must-call obligation (and this fact must be expressed via a \<@EnsuresCalledMethods> annotation on \), and the enclosing class must have a \<@MustCall("d")> obligation to -ensure the destructor is called. +ensure the destructor is called. In addition to the \<@EnsuresCalledMethods> annotation, +which guarantees that the field(s) it references have their must-call obligations satisfied +on non-exceptional paths, the Resource Leak Checker requires those fields to have their must-call +obligations satisfied on all paths in (only) the destructor, and will issue a \ +error if they are not satisfied. Resolve this error by ensuring that the required methods are called +on all exceptional paths. \textbf{Non-final, non-static owning fields} usually require one or more \<@CreatesMustCallFor> annotations when they might be re-assigned. See Section~\ref{resource-leak-createsmustcallfor} for