Model try-with-resources semantics during CFG construction

checker/src/main/java/org/checkerframework/checker/mustcall/MustCallAnnotatedTypeFactory.java

@@ -515,9 +515,6 @@ public Void visitIdentifier(IdentifierTree tree, AnnotatedTypeMirror type) {
           type.replaceAnnotation(BOTTOM);
         }
       }
-      if (ElementUtils.isResourceVariable(elt)) {
-        type.replaceAnnotation(withoutClose(type.getPrimaryAnnotationInHierarchy(TOP)));
-      }
       return super.visitIdentifier(tree, type);
     }
   }

checker/src/main/java/org/checkerframework/checker/mustcall/MustCallTransfer.java

@@ -12,13 +12,11 @@
 import javax.lang.model.element.AnnotationMirror;
 import javax.lang.model.element.Element;
 import javax.lang.model.type.TypeMirror;
-import org.checkerframework.checker.mustcall.qual.MustCall;
 import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.checkerframework.checker.resourceleak.ResourceLeakChecker;
 import org.checkerframework.dataflow.analysis.TransferInput;
 import org.checkerframework.dataflow.analysis.TransferResult;
-import org.checkerframework.dataflow.cfg.node.AssignmentNode;
 import org.checkerframework.dataflow.cfg.node.LocalVariableNode;
 import org.checkerframework.dataflow.cfg.node.MethodInvocationNode;
 import org.checkerframework.dataflow.cfg.node.Node;
@@ -31,7 +29,6 @@
 import org.checkerframework.framework.flow.CFStore;
 import org.checkerframework.framework.flow.CFTransfer;
 import org.checkerframework.framework.flow.CFValue;
-import org.checkerframework.javacutil.ElementUtils;
 import org.checkerframework.javacutil.TreePathUtil;
 import org.checkerframework.javacutil.TreeUtils;
 import org.checkerframework.javacutil.TypesUtils;
@@ -114,28 +111,6 @@ private AnnotationMirror getDefaultStringType(StringConversionNode n) {
     return this.defaultStringType;
   }
 
-  @Override
-  public TransferResult<CFValue, CFStore> visitAssignment(
-      AssignmentNode n, TransferInput<CFValue, CFStore> in) {
-    TransferResult<CFValue, CFStore> result = super.visitAssignment(n, in);
-    // Remove "close" from the type in the store for resource variables.
-    // The Resource Leak Checker relies on this code to avoid checking that
-    // resource variables are closed.
-    if (ElementUtils.isResourceVariable(TreeUtils.elementFromTree(n.getTarget().getTree()))) {
-      CFStore store = result.getRegularStore();
-      JavaExpression expr = JavaExpression.fromNode(n.getTarget());
-      CFValue value = store.getValue(expr);
-      AnnotationMirror withClose =
-          atypeFactory.getAnnotationByClass(value.getAnnotations(), MustCall.class);
-      if (withClose == null) {
-        return result;
-      }
-      AnnotationMirror withoutClose = atypeFactory.withoutClose(withClose);
-      insertIntoStores(result, expr, withoutClose);
-    }
-    return result;
-  }
-
   @Override
   public TransferResult<CFValue, CFStore> visitMethodInvocation(
       MethodInvocationNode n, TransferInput<CFValue, CFStore> in) {

checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java

@@ -17,7 +17,6 @@
 import javax.lang.model.element.ExecutableElement;
 import javax.lang.model.element.TypeElement;
 import javax.lang.model.type.TypeMirror;
-import org.checkerframework.checker.compilermsgs.qual.CompilerMessageKey;
 import org.checkerframework.checker.mustcall.qual.InheritableMustCall;
 import org.checkerframework.checker.mustcall.qual.MustCall;
 import org.checkerframework.checker.mustcall.qual.MustCallAlias;
@@ -267,75 +266,6 @@ protected boolean skipReceiverSubtypeCheck(
     return true;
   }
 
-  /**
-   * This boolean is used to communicate between different levels of the common assignment check
-   * whether a given check is being carried out on a (pseudo-)assignment to a resource variable. In
-   * those cases, close doesn't need to be considered when doing the check, since close will always
-   * be called by Java.
-   *
-   * <p>The check for whether the LHS is a resource variable can only be carried out on the element,
-   * but the effect needs to happen at the stage where the type is available (i.e. close needs to be
-   * removed from the type). Thus, this variable is used to communicate that a resource variable was
-   * detected on the LHS.
-   */
-  private boolean commonAssignmentCheckOnResourceVariable = false;
-
-  /**
-   * {@inheritDoc}
-   *
-   * <p>Mark (using the {@code #commonAssignmentCheckOnResourceVariable} field of this class) any
-   * assignments where the LHS is a resource variable, so that close doesn't need to be considered.
-   * See {@link #commonAssignmentCheck(AnnotatedTypeMirror, AnnotatedTypeMirror, Tree, String,
-   * Object...)} for the code that uses and removes the mark.
-   */
-  @Override
-  protected boolean commonAssignmentCheck(
-      Tree varTree,
-      ExpressionTree valueExp,
-      @CompilerMessageKey String errorKey,
-      Object... extraArgs) {
-    Element elt = TreeUtils.elementFromTree(varTree);
-    if (elt != null && elt.getKind() == ElementKind.RESOURCE_VARIABLE) {
-      commonAssignmentCheckOnResourceVariable = true;
-    }
-    return super.commonAssignmentCheck(varTree, valueExp, errorKey, extraArgs);
-  }
-
-  /**
-   * {@inheritDoc}
-   *
-   * <p>Iff the LHS is a resource variable, then {@code #commonAssignmentCheckOnResourceVariable}
-   * will be true. This method guarantees that {@code #commonAssignmentCheckOnResourceVariable} will
-   * be false when it returns.
-   */
-  @Override
-  protected boolean commonAssignmentCheck(
-      AnnotatedTypeMirror varType,
-      AnnotatedTypeMirror valueType,
-      Tree valueTree,
-      @CompilerMessageKey String errorKey,
-      Object... extraArgs) {
-
-    if (commonAssignmentCheckOnResourceVariable) {
-      commonAssignmentCheckOnResourceVariable = false;
-      // The LHS has been marked as a resource variable.  Skip the standard common assignment
-      // check; instead do a check that does not include "close".
-      AnnotationMirror varAnno = varType.getPrimaryAnnotationInHierarchy(atypeFactory.TOP);
-      AnnotationMirror valueAnno = valueType.getPrimaryAnnotationInHierarchy(atypeFactory.TOP);
-      if (qualHierarchy.isSubtypeShallow(
-          atypeFactory.withoutClose(valueAnno),
-          valueType.getUnderlyingType(),
-          atypeFactory.withoutClose(varAnno),
-          varType.getUnderlyingType())) {
-        return true;
-      }
-      // Note that in this case, the rest of the common assignment check should fail (barring
-      // an exception).  Control falls through here to avoid duplicating error-issuing code.
-    }
-    // commonAssignmentCheckOnResourceVariable is already false, so no need to set it.
-    return super.commonAssignmentCheck(varType, valueType, valueTree, errorKey, extraArgs);
-  }
-
   /**
    * This method typically issues a warning if the result type of the constructor is not top,
    * because in top-default type systems that indicates a potential problem. The Must Call Checker

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

@@ -74,7 +74,6 @@
 import org.checkerframework.dataflow.util.NodeUtils;
 import org.checkerframework.framework.flow.CFStore;
 import org.checkerframework.framework.flow.CFValue;
-import org.checkerframework.framework.type.AnnotatedTypeMirror;
 import org.checkerframework.framework.util.JavaExpressionParseUtil.JavaExpressionParseException;
 import org.checkerframework.framework.util.StringToJavaExpression;
 import org.checkerframework.javacutil.AnnotationUtils;
@@ -711,8 +710,7 @@ private void checkCreatesMustCallForInvocation(
    *   <li>2) the expression already has a tracked Obligation (i.e. there is already a resource
    *       alias in some Obligation's resource alias set that refers to the expression), or
    *   <li>3) the method in which the invocation occurs also has an @CreatesMustCallFor annotation,
-   *       with the same expression, or
-   *   <li>4) the expression is a resource variable.
+   *       with the same expression.
    * </ul>
    *
    * @param obligations the currently-tracked Obligations; this value is side-effected if there is
@@ -739,10 +737,6 @@ private boolean isValidCreatesMustCallForExpression(
         // formal parameters are also represented by LocalVariable in the bodies of methods.
         // This satisfies case 1.
         return true;
-      } else if (ElementUtils.isResourceVariable(elt)) {
-        // The expression is a resource variable, and therefore will be closed, so we can
-        // treat it as owning (case 4).
-        return true;
       } else {
         Obligation toRemove = null;
         Obligation toAdd = null;
@@ -1224,16 +1218,6 @@ private void updateObligationsForAssignment(
               new ResourceAlias(JavaExpression.fromNode(lhs), lhsElement, lhs.getTree()));
         }
       }
-    } else if (lhsElement.getKind() == ElementKind.RESOURCE_VARIABLE && isMustCallClose(rhs)) {
-      if (rhs instanceof FieldAccessNode) {
-        // Handling of @Owning fields is a completely separate check.
-      } else if (rhs instanceof LocalVariableNode) {
-        removeObligationsContainingVar(
-            obligations,
-            (LocalVariableNode) rhs,
-            MustCallAliasHandling.RETAIN_OBLIGATIONS_DERIVED_FROM_A_MUST_CALL_ALIAS_PARAMETER,
-            MethodExitKind.ALL);
-      }
     } else if (lhs instanceof LocalVariableNode) {
       LocalVariableNode lhsVar = (LocalVariableNode) lhs;
       updateObligationsForPseudoAssignment(obligations, assignmentNode, lhsVar, rhs);
@@ -1264,22 +1248,6 @@ private boolean hasAtMostOneOwningField(TypeElement element) {
     return true;
   }
 
-  /**
-   * Returns true if must-call type of node only contains close. This is a helper method for
-   * handling try-with-resources statements.
-   *
-   * @param node the node
-   * @return true if must-call type of node only contains close
-   */
-  /*package-private*/ boolean isMustCallClose(Node node) {
-    MustCallAnnotatedTypeFactory mcAtf =
-        typeFactory.getTypeFactoryOfSubchecker(MustCallChecker.class);
-    AnnotatedTypeMirror mustCallAnnotatedType = mcAtf.getAnnotatedType(node.getTree());
-    AnnotationMirror mustCallAnnotation =
-        mustCallAnnotatedType.getPrimaryAnnotation(MustCall.class);
-    return typeFactory.getMustCallValues(mcAtf.withoutClose(mustCallAnnotation)).isEmpty();
-  }
-
   /**
    * Add a new alias to all Obligations that have {@code var} in their resource-alias set. This
    * method should be used when {@code var} and {@code newAlias} definitively point to the same

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

@@ -369,8 +369,6 @@ private void analyzeOwnershipTransferAtAssignment(
         disposedFields.remove((VariableElement) lhsElement);
       }
       addOwningToParamsIfDisposedAtAssignment(obligations, rhsObligation, rhs);
-    } else if (lhsElement.getKind() == ElementKind.RESOURCE_VARIABLE && mcca.isMustCallClose(rhs)) {
-      addOwningToParamsIfDisposedAtAssignment(obligations, rhsObligation, rhs);
     } else if (lhs instanceof LocalVariableNode) {
       LocalVariableNode lhsVar = (LocalVariableNode) lhs;
       mcca.updateObligationsForPseudoAssignment(obligations, assignmentNode, lhsVar, rhs);

checker/tests/mustcall/TryWithResourcesSimple.java

@@ -1,4 +1,4 @@
-// A test that try-with-resources variables are always @MustCall({}).
+// A test that try-with-resources variables are always @MustCall({"close"}).
 
 import java.io.*;
 import java.net.*;
@@ -7,7 +7,7 @@
 public class TryWithResourcesSimple {
   static void test(String address, int port) {
     try (Socket socket = new Socket(address, port)) {
-      @MustCall({}) Object s = socket;
+      @MustCall({"close"}) Object s = socket;
     } catch (Exception e) {
 
     }
@@ -23,16 +23,16 @@ void test_fancy_sock(String address, int port) {
     // "close", which is the only MC method for Socket itself.
     try (Socket socket = getFancySocket()) {
       // :: error: (assignment)
-      @MustCall({}) Object s = socket;
+      @MustCall({"close"}) Object s = socket;
     } catch (Exception e) {
 
     }
   }
 
   static void test_poly(String address, int port) {
     try (Socket socket = new Socket(address, port)) {
-      // getChannel is @MustCallAlias (= poly) with the socket, so it should also be @MC({})
-      @MustCall({}) Object s = socket.getChannel();
+      // getChannel is @MustCallAlias (= poly) with the socket, so it should also be @MC({"close"})
+      @MustCall({"close"}) Object s = socket.getChannel();
     } catch (Exception e) {
 
     }
@@ -41,7 +41,7 @@ static void test_poly(String address, int port) {
   static void test_two_mca_variables(String address, int port) {
     try (Socket socket = new Socket(address, port);
         InputStream in = socket.getInputStream()) {
-      @MustCall({}) Object s = in;
+      @MustCall({"close"}) Object s = in;
     } catch (Exception e) {
 
     }

checker/tests/resourceleak/TryWithResourcesSimple.java → checker/tests/resourceleak/TryWithResourcesDeclaration.java

@@ -1,11 +1,11 @@
-// A simple test that a try-with-resources socket doesn't issue a false positive.
+// Tests for try-with-resources that declare local variables in the resource declaration.
 
 import java.io.*;
 import java.net.Socket;
 import java.nio.channels.*;
 import java.util.*;
 
-class TryWithResourcesSimple {
+class TryWithResourcesDeclaration {
   static void test(String address, int port) {
     try (Socket socket = new Socket(address, port)) {
 
@@ -31,4 +31,13 @@ public boolean isPreUpgradableLayout(File oldF) throws IOException {
       return false;
     }
   }
+
+  public void testNestedTryWithResourcesDecls(Properties prop, ClassLoader cl, String propfile)
+      throws Exception {
+    try (InputStream in = cl.getResourceAsStream(propfile)) {
+      try (InputStream fis = new FileInputStream(propfile)) {
+        prop.load(fis);
+      }
+    }
+  }
 }