Fix unsoundess in Resource Leak Checker related to owning fields and EnsuresCalledMethods

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

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,66 @@ 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;
+    }
+    // This method might be a destructor that is responsible for resolving the must-call
+    // obligations of one or more owning fields of the containing class.
+    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<String> mcValues =
+        AnnotationUtils.getElementValueArray(
+            mcAnno, mustCallAnnotatedTypeFactory.getMustCallValueElement(), String.class);
+    String methodName = elt.getSimpleName().toString();
+    if (!mcValues.contains(methodName)) {
+      // Not a destructor, just a method with an ECM annotation. No further checking to do.
+      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<AnnotationMirror> 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 the {@link CreatesMustCallFor#value} element/argument of the given @CreatesMustCallFor
    * annotation, or "this" if there is none.

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

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();

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

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

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) {
+
+    }
+  }
+}

docs/manual/resource-leak-checker.tex

@@ -221,7 +221,12 @@
 destructor-like method \<d()> must satisfy the field's must-call obligation
 (and this fact must be expressed via a \<@EnsuresCalledMethods> annotation on \<d()>),
 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 \<destructor.exceptional.postcondition>
+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