Add -ApermitInitializationLeak command-line argument (#5173)

checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java

@@ -138,6 +138,9 @@
 /* package-private */
 class MustCallConsistencyAnalyzer {
 
+  /** True if errors related to field initialization should be suppressed. */
+  private boolean permitInitializationLeak;
+
   /**
    * Aliases about which the checker has already reported about a resource leak, to avoid duplicate
    * reports.
@@ -462,6 +465,7 @@ public int hashCode() {
     this.typeFactory = typeFactory;
     this.checker = (ResourceLeakChecker) typeFactory.getChecker();
     this.analysis = analysis;
+    this.permitInitializationLeak = checker.hasOption("permitInitializationLeak");
   }
 
   /**
@@ -1241,12 +1245,19 @@ private void checkReassignmentToField(Set<Obligation> obligations, AssignmentNod
     MethodTree enclosingMethodTree = TreePathUtil.enclosingMethod(currentPath);
 
     if (enclosingMethodTree == null) {
-      // If the assignment is taking place outside of a method, the Resource Leak Checker
-      // issues an error unless it can prove that the assignment is a field initializer, which
-      // are always safe. The node's TreeKind being "VARIABLE" is a safe proxy for this requirement,
-      // because VARIABLE Trees are only used for declarations. An assignment to a field that is
-      // also a declaration must be a field initializer.
+      // The assignment is taking place outside of a method:  in a variable declaration's
+      // initializer or in an initializer block.
+      // The Resource Leak Checker issues no error if the assignment is a field initializer.
       if (node.getTree().getKind() == Tree.Kind.VARIABLE) {
+        // An assignment to a field that is also a declaration must be a field initializer (VARIABLE
+        // Trees are only used for declarations).  Assignment in a field initializer is always
+        // permitted.
+        return;
+      } else if (permitInitializationLeak
+          && TreePathUtil.isTopLevelAssignmentInInitializerBlock(currentPath)) {
+        // This is likely not reassignment; if reassignment, the number of assignments that
+        // were not warned about is limited to other initializations (is not unbounded).
+        // This behavior is unsound; see InstanceInitializer.java test case.
         return;
       } else {
         // Issue an error if the field has a non-empty must-call type.
@@ -1270,6 +1281,15 @@ private void checkReassignmentToField(Set<Obligation> obligations, AssignmentNod
             "Field assignment outside method or declaration might overwrite field's current value");
         return;
       }
+    } else if (permitInitializationLeak && TreeUtils.isConstructor(enclosingMethodTree)) {
+      Element enclosingClassElement =
+          TreeUtils.elementFromTree(enclosingMethodTree).getEnclosingElement();
+      if (ElementUtils.isTypeElement(enclosingClassElement)) {
+        Element receiverElement = TypesUtils.getTypeElement(receiver.getType());
+        if (Objects.equals(enclosingClassElement, receiverElement)) {
+          return;
+        }
+      }
     }
 
     // Check that there is a corresponding CreatesMustCallFor annotation, unless this is

checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakChecker.java

@@ -16,6 +16,7 @@
  * via the {@link org.checkerframework.checker.mustcall.MustCallChecker} have been fulfilled.
  */
 @SupportedOptions({
+  "permitInitializationLeak",
   ResourceLeakChecker.COUNT_MUST_CALL,
   MustCallChecker.NO_CREATES_MUSTCALLFOR,
   MustCallChecker.NO_LIGHTWEIGHT_OWNERSHIP,

checker/src/test/java/org/checkerframework/checker/test/junit/ResourceLeakPermitInitializationLeak.java

@@ -0,0 +1,27 @@
+package org.checkerframework.checker.test.junit;
+
+import java.io.File;
+import java.util.List;
+import org.checkerframework.checker.resourceleak.ResourceLeakChecker;
+import org.checkerframework.framework.test.CheckerFrameworkPerDirectoryTest;
+import org.junit.runners.Parameterized.Parameters;
+
+/** Tests for the Resource Leak Checker. */
+public class ResourceLeakPermitInitializationLeak extends CheckerFrameworkPerDirectoryTest {
+  public ResourceLeakPermitInitializationLeak(List<File> testFiles) {
+    super(
+        testFiles,
+        ResourceLeakChecker.class,
+        "resourceleak-permitinitializationleak",
+        "-Anomsgtext",
+        "-ApermitInitializationLeak",
+        "-AwarnUnneededSuppressions",
+        "-encoding",
+        "UTF-8");
+  }
+
+  @Parameters
+  public static String[] getTestDirs() {
+    return new String[] {"resourceleak-permitinitializationleak"};
+  }
+}

checker/tests/resourceleak-permitinitializationleak/InstanceInitializer.java

@@ -0,0 +1,53 @@
+// A test that the checker is sound in the presence of instance initializer blocks.
+// In the resourceleak-permitinitializationleak/ directory, it's a test that the
+// checker is unsound with the -ApermitInitializationLeak command-line argument.
+
+import java.net.Socket;
+import org.checkerframework.checker.mustcall.qual.*;
+
+class InstanceInitializer {
+  // :: error: required.method.not.called
+  private @Owning Socket s;
+
+  private final int DEFAULT_PORT = 5;
+  private final String DEFAULT_ADDR = "localhost";
+
+  {
+    try {
+      // This assignment is OK, because it's the first assignment.
+      s = new Socket(DEFAULT_ADDR, DEFAULT_PORT);
+    } catch (Exception e) {
+    }
+  }
+
+  {
+    try {
+      // This assignment is not OK, because it's a reassignment without satisfying the mustcall
+      // obligations of the previous value of `s`.
+      // With -ApermitInitializationLeak, the Resource Leak Checker unsoundly permits it.
+      s = new Socket(DEFAULT_ADDR, DEFAULT_PORT);
+    } catch (Exception e) {
+    }
+  }
+
+  {
+    try {
+      // :: error: required.method.not.called
+      Socket s1 = new Socket(DEFAULT_ADDR, DEFAULT_PORT);
+    } catch (Exception e) {
+    }
+  }
+
+  {
+    Socket s1 = null;
+    try {
+      s1 = new Socket(DEFAULT_ADDR, DEFAULT_PORT);
+    } catch (Exception e) {
+    }
+    s1.close();
+  }
+
+  public InstanceInitializer() throws Exception {
+    s = new Socket(DEFAULT_ADDR, DEFAULT_PORT);
+  }
+}

checker/tests/resourceleak-permitinitializationleak/SocketContainer.java

@@ -0,0 +1,25 @@
+// A simple class that has a Socket as an owning field.
+// This test exists to check that we gracefully handle assignments 1)
+// in the constructor and 2) to null.
+
+import java.io.*;
+import java.net.*;
+import org.checkerframework.checker.calledmethods.qual.*;
+import org.checkerframework.checker.mustcall.qual.*;
+
+@MustCall("close") class SocketContainer {
+  @Owning Socket sock;
+
+  public SocketContainer(String host, int port) throws Exception {
+    sock = new Socket(host, port);
+    sock = new Socket(host, port);
+  }
+
+  @EnsuresCalledMethods(value = "this.sock", methods = "close")
+  public void close() throws IOException {
+    sock.close();
+    // It's okay to assign a field to null after its obligations have been fulfilled,
+    // without inducing a reset.
+    sock = null;
+  }
+}

checker/tests/resourceleak/InstanceInitializer.java

@@ -1,4 +1,6 @@
 // A test that the checker is sound in the presence of instance initializer blocks.
+// In the resourceleak-permitinitializationleak/ directory, it's a test that the
+// checker is unsound with the -ApermitInitializationLeak command-line argument.
 
 import java.net.Socket;
 import org.checkerframework.checker.mustcall.qual.*;
@@ -12,6 +14,8 @@ class InstanceInitializer {
 
   {
     try {
+      // This assignment is OK, because it's the first assignment.
+      // However, the Resource Leak Checker issues a false positive warning.
       // :: error: required.method.not.called
       s = new Socket(DEFAULT_ADDR, DEFAULT_PORT);
     } catch (Exception e) {
@@ -20,6 +24,8 @@ class InstanceInitializer {
 
   {
     try {
+      // This assignment is not OK, because it's a reassignment without satisfying the mustcall
+      // obligations of the previous value of `s`.
       // :: error: required.method.not.called
       s = new Socket(DEFAULT_ADDR, DEFAULT_PORT);
     } catch (Exception e) {

docs/CHANGELOG.md

@@ -3,6 +3,9 @@ Version 3.22.3 (July 1, 2022)
 
 **User-visible changes:**
 
+New command-line argument `-ApermitInitializationLeak` suppresses Resource Leak
+Checker warnings related to field initialization.
+
 **Implementation details:**
 
 **Closed issues:**

docs/manual/resource-leak-checker.tex

@@ -50,8 +50,16 @@
 \end{Verbatim}
 
 The Resource Leak Checker supports all the command-line arguments
- listed in Section~\ref{called-methods-run-checker} for
-the Called Methods Checker.
+listed in Section~\ref{called-methods-run-checker} for
+the Called Methods Checker, plus two others:
+
+\begin{description}
+% \item[\<-ApermitStaticOwning>]
+%   See Section~\ref{resource-leak-owning-fields}.
+\item[\<-ApermitInitializationLeak>]
+  See Section~\ref{resource-leak-field-initialization}.
+\end{description}
+
 
 \sectionAndLabel{Resource Leak Checker annotations}{resource-leak-annotations}
 
@@ -426,6 +434,31 @@
 verification tool.
 \end{itemize}
 
+
+\sectionAndLabel{Errors about field initialization}{resource-leak-field-initialization}
+
+% Arguably, this is working around a bug in the
+% MustCallConsistencyAnalyzer, which could be improved to avoid issuing
+% these false positive warnings.
+
+The Resource Leak Checker warns about re-assignments to owning fields,
+because the value that was overwritten might not have had its obligations
+satisfied.  Such a warning is not necessary on the first assignment to a
+field, since the field had no content before the assignment.  Sometimes,
+the Resource Leak Checker is unable to determine that an assignment is the
+first one, so it conservatively assumes the assignment is a re-assignment
+and issues an error.
+
+One way to prevent this false positive warning is to declare the field as \<final>.
+
+Alternately, to suppress all warnings related to field assignments in the
+constructor and in initializer blocks, pass the
+\<-ApermitInitializationLeak> command-line argument.  This makes the
+checker unsound:  the Resoure Leak Checker will not warn if the constructor
+and initializers set a field more than once.  The amount of leakage is
+limited to how many times the field is set.
+
+
 % LocalWords:  de subchecker OutputStream MustCall MustCallUnknown RAII Un
 % LocalWords:  PolyMustCall InheritableMustCall MultiRandSelector callsite
 % LocalWords:  Partitioner CalledMethods AnoLightweightOwnership NotOwning

javacutil/src/main/java/org/checkerframework/javacutil/TreePathUtil.java

@@ -9,6 +9,7 @@
 import com.sun.source.tree.VariableTree;
 import com.sun.source.util.TreePath;
 import java.util.EnumSet;
+import java.util.Iterator;
 import java.util.Set;
 import java.util.StringJoiner;
 import javax.lang.model.element.Element;
@@ -341,6 +342,52 @@ public static boolean isTreeInStaticScope(TreePath path) {
     return false;
   }
 
+  /**
+   * Returns true if the path is to a top-level (not within a loop) assignment within an initializer
+   * block. The initializer block might be instance or static. Will return true for a re-assignment
+   * even if there is another initialization (within this initializer block, another initializer
+   * block, a constructor, or the variable declaration).
+   *
+   * @param path the path to test
+   * @return true if the path is to an initialization within an initializer block
+   */
+  public static boolean isTopLevelAssignmentInInitializerBlock(TreePath path) {
+    TreePath origPath = path;
+    if (path.getLeaf().getKind() != Tree.Kind.ASSIGNMENT) {
+      return false;
+    }
+    path = path.getParentPath();
+    if (path.getLeaf().getKind() != Tree.Kind.EXPRESSION_STATEMENT) {
+      return false;
+    }
+    Tree prevLeaf = path.getLeaf();
+    path = path.getParentPath();
+
+    for (Iterator<Tree> itor = path.iterator(); itor.hasNext(); ) {
+      Tree leaf = itor.next();
+      switch (leaf.getKind()) {
+        case CLASS:
+        case ENUM:
+        case PARAMETERIZED_TYPE:
+          return prevLeaf.getKind() == Tree.Kind.BLOCK;
+
+        case COMPILATION_UNIT:
+          throw new BugInCF("found COMPILATION_UNIT in " + toString(origPath));
+
+        case DO_WHILE_LOOP:
+        case ENHANCED_FOR_LOOP:
+        case FOR_LOOP:
+        case LAMBDA_EXPRESSION:
+        case METHOD:
+          return false;
+
+        default:
+          prevLeaf = leaf;
+      }
+    }
+    throw new BugInCF("path did not contain method or class: " + toString(origPath));
+  }
+
   ///
   /// Formatting
   ///