Make synthetic classes used in a try with resources statement implement AutoCloseable

src/main/java/org/checkerframework/specimin/PrunerVisitor.java

@@ -223,6 +223,12 @@ private void removeUnusedInterfacesHelper(
         String typeFullName =
             JavaParserUtil.classOrInterfaceTypeToResolvedReferenceType(interfaceType)
                 .getQualifiedName();
+
+        // Never remove java.lang.AutoCloseable, because it will create compilation
+        // errors at try-with-resources statements.
+        if (typeFullName.equals("java.lang.AutoCloseable")) {
+          continue;
+        }
         if (!usedTypeElements.contains(typeFullName)) {
           iterator.remove();
         }

src/main/java/org/checkerframework/specimin/UnsolvedClassOrInterface.java

@@ -43,9 +43,12 @@ public class UnsolvedClassOrInterface {
   /** This field records the name of type variables that we prefer this class to have. */
   private Set<String> preferredTypeVariables = new HashSet<>();
 
-  /** The field records the extends/implements clauses, if one exists. */
+  /** This field records the extends clause, if one exists. */
   private @Nullable String extendsClause;
 
+  /** The implements clauses, if they exist. */
+  private Set<String> implementsClauses = new LinkedHashSet<>(0);
+
   /** This field records if the class is an interface */
   private boolean isAnInterface;
 
@@ -283,6 +286,15 @@ public int getNumberOfTypeVariables() {
     return this.numberOfTypeVariables;
   }
 
+  /**
+   * Adds a new interface to the list of implemented interfaces.
+   *
+   * @param interfaceName the fqn of the interface
+   */
+  public void implement(String interfaceName) {
+    implementsClauses.add(interfaceName);
+  }
+
   /**
    * Adds an extends clause to this class.
    *
@@ -499,6 +511,19 @@ public String toString() {
     if (extendsClause != null) {
       sb.append(" ").append(extendsClause);
     }
+    if (implementsClauses.size() > 0) {
+      if (extendsClause != null) {
+        sb.append(", ");
+      }
+      sb.append(" implements ");
+      Iterator<String> interfaces = implementsClauses.iterator();
+      while (interfaces.hasNext()) {
+        sb.append(interfaces.next());
+        if (interfaces.hasNext()) {
+          sb.append(", ");
+        }
+      }
+    }
     sb.append(" {\n");
     if (innerClasses != null) {
       for (UnsolvedClassOrInterface innerClass : innerClasses) {

src/main/java/org/checkerframework/specimin/UnsolvedMethod.java

@@ -10,6 +10,17 @@
  * SymbolSolver. The reason is that the class file of that method is not in the root directory.
  */
 public class UnsolvedMethod {
+
+  /** The close() method from java.lang.AutoCloseable. */
+  public static final UnsolvedMethod CLOSE =
+      new UnsolvedMethod(
+          "close",
+          "void",
+          Collections.emptyList(),
+          false,
+          "public",
+          List.of("java.lang.Exception"));
+
   /** The name of the method */
   private final String name;
 

src/main/java/org/checkerframework/specimin/UnsolvedSymbolVisitor.java

@@ -32,6 +32,7 @@
 import com.github.javaparser.ast.expr.SingleMemberAnnotationExpr;
 import com.github.javaparser.ast.expr.SwitchExpr;
 import com.github.javaparser.ast.expr.ThisExpr;
+import com.github.javaparser.ast.expr.VariableDeclarationExpr;
 import com.github.javaparser.ast.stmt.BlockStmt;
 import com.github.javaparser.ast.stmt.CatchClause;
 import com.github.javaparser.ast.stmt.ExplicitConstructorInvocationStmt;
@@ -640,11 +641,87 @@ public Visitable visit(SwitchEntry node, Void p) {
   public Visitable visit(TryStmt node, Void p) {
     HashSet<String> currentLocalVariables = new HashSet<>();
     localVariables.addFirst(currentLocalVariables);
+    List<Expression> resources = node.getResources();
+    if (resources.size() != 0) {
+      handleSyntheticResources(resources);
+    }
     Visitable result = super.visit(node, p);
     localVariables.removeFirst();
     return result;
   }
 
+  /**
+   * Ensures that every type used by a try-with-resources statement extends java.lang.AutoCloseable.
+   *
+   * @param resources a list of resource expressions
+   */
+  private void handleSyntheticResources(List<Expression> resources) {
+    // Resource expressions can be:
+    // * names
+    // * field accesses
+    // * a new local variable declaration
+    // In the former two cases, we have to wait to handle the synthetic resources
+    // until the expression can be solved. For the latter, we have to wait until the
+    // declared type is solvable.
+    for (Expression resource : resources) {
+      if (resource.isVariableDeclarationExpr()) {
+        VariableDeclarationExpr asVar = resource.asVariableDeclarationExpr();
+        String fqn;
+        try {
+          fqn = asVar.calculateResolvedType().describe();
+        } catch (UnsolvedSymbolException e) {
+          gotException();
+          continue;
+        }
+        makeClassAutoCloseable(fqn);
+      } else if (resource.isNameExpr()) {
+        NameExpr asName = resource.asNameExpr();
+        String fqn;
+        try {
+          fqn = asName.resolve().getType().describe();
+        } catch (UnsolvedSymbolException e) {
+          gotException();
+          continue;
+        }
+        makeClassAutoCloseable(fqn);
+      } else if (resource.isFieldAccessExpr()) {
+        FieldAccessExpr asField = resource.asFieldAccessExpr();
+        String fqn;
+        try {
+          fqn = asField.resolve().getType().describe();
+        } catch (UnsolvedSymbolException e) {
+          gotException();
+          continue;
+        }
+        makeClassAutoCloseable(fqn);
+      } else {
+        throw new RuntimeException(
+            "unexpected type of node in a try-with-resources expression: "
+                + resource.getClass()
+                + "\nresouce was "
+                + resource);
+      }
+    }
+  }
+
+  /**
+   * Makes the synthetic class with the given name implement AutoCloseable, if such a synthetic
+   * class exists. If not, silently does nothing, since that should only happen when encounting a
+   * non-synthetic class, which must already implement AutoCloseable if it is used in a
+   * try-with-resources that compiles (i.e., this method relies on the assumption that the input
+   * compiles).
+   *
+   * @param fqn a fully-qualified name
+   */
+  private void makeClassAutoCloseable(String fqn) {
+    for (UnsolvedClassOrInterface sytheticClass : missingClass) {
+      if (sytheticClass.getQualifiedClassName().equals(fqn)) {
+        sytheticClass.implement("java.lang.AutoCloseable");
+        sytheticClass.addMethod(UnsolvedMethod.CLOSE);
+      }
+    }
+  }
+
   @Override
   @SuppressWarnings("nullness")
   // This method returns a nullable result, and "comment" can be null for the phrase

src/test/java/org/checkerframework/specimin/TryWithResourcesTest.java

@@ -0,0 +1,18 @@
+package org.checkerframework.specimin;
+
+import java.io.IOException;
+import org.junit.Test;
+
+/**
+ * This test checks that an unsolved type that's used in a try-with-resources context correctly
+ * implements AutoCloseable.
+ */
+public class TryWithResourcesTest {
+  @Test
+  public void runTest() throws IOException {
+    SpeciminTestExecutor.runTestWithoutJarPaths(
+        "trywithresources",
+        new String[] {"com/example/Simple.java"},
+        new String[] {"com.example.Simple#bar(OtherResource)"});
+  }
+}

src/test/resources/trywithresources/expected/com/example/Simple.java

@@ -0,0 +1,19 @@
+package com.example;
+
+import org.example.Resource;
+import org.example.OtherResource;
+import org.example.ThirdResource;
+
+class Simple {
+
+    private final ThirdResource r = null;
+
+    void bar(final OtherResource o) throws Exception {
+        try (Resource r = new Resource()) {
+        }
+        try (o) {
+        }
+        try (r) {
+        }
+    }
+}

src/test/resources/trywithresources/expected/org/example/OtherResource.java

@@ -0,0 +1,8 @@
+package org.example;
+
+public class OtherResource implements java.lang.AutoCloseable {
+
+    public void close() throws java.lang.Exception {
+        throw new Error();
+    }
+}

src/test/resources/trywithresources/expected/org/example/Resource.java

@@ -0,0 +1,12 @@
+package org.example;
+
+public class Resource implements java.lang.AutoCloseable {
+
+    public Resource() {
+        throw new Error();
+    }
+
+    public void close() throws java.lang.Exception {
+        throw new Error();
+    }
+}

src/test/resources/trywithresources/expected/org/example/ThirdResource.java

@@ -0,0 +1,8 @@
+package org.example;
+
+public class ThirdResource implements java.lang.AutoCloseable {
+
+    public void close() throws java.lang.Exception {
+        throw new Error();
+    }
+}

src/test/resources/trywithresources/input/com/example/Simple.java

@@ -0,0 +1,23 @@
+package com.example;
+
+import org.example.Resource;
+import org.example.OtherResource;
+import org.example.ThirdResource;
+
+class Simple {
+
+    private final ThirdResource r = null;
+
+    // Target method.
+    void bar(final OtherResource o) throws Exception {
+        try (Resource r = new Resource()) {
+            // do something
+        }
+        try (o) {
+            // do something else
+        }
+        try (r) {
+
+        }
+    }
+}