From a44fbaf208a0fd36a29517c4d754704764cbbcca Mon Sep 17 00:00:00 2001
From: Martin Kellogg <martin.kellogg@njit.edu>
Date: Thu, 25 Jul 2024 15:19:48 -0400
Subject: [PATCH 1/9] test that doesn't compile (will come back to it)

---
 .../specimin/TryWithResourcesTest.java         | 18 ++++++++++++++++++
 .../expected/com/example/Simple.java           | 11 +++++++++++
 .../expected/org/example/Resource.java         |  8 ++++++++
 .../input/com/example/Simple.java              | 12 ++++++++++++
 4 files changed, 49 insertions(+)
 create mode 100644 src/test/java/org/checkerframework/specimin/TryWithResourcesTest.java
 create mode 100644 src/test/resources/trywithresources/expected/com/example/Simple.java
 create mode 100644 src/test/resources/trywithresources/expected/org/example/Resource.java
 create mode 100644 src/test/resources/trywithresources/input/com/example/Simple.java

diff --git a/src/test/java/org/checkerframework/specimin/TryWithResourcesTest.java b/src/test/java/org/checkerframework/specimin/TryWithResourcesTest.java
new file mode 100644
index 00000000..599ba4a0
--- /dev/null
+++ b/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()"});
+  }
+}
diff --git a/src/test/resources/trywithresources/expected/com/example/Simple.java b/src/test/resources/trywithresources/expected/com/example/Simple.java
new file mode 100644
index 00000000..647cd3e9
--- /dev/null
+++ b/src/test/resources/trywithresources/expected/com/example/Simple.java
@@ -0,0 +1,11 @@
+package com.example;
+
+import org.example.Resource;
+
+class Simple {
+
+    void bar() {
+        try (Resource r = new Resource()) {
+        }
+    }
+}
diff --git a/src/test/resources/trywithresources/expected/org/example/Resource.java b/src/test/resources/trywithresources/expected/org/example/Resource.java
new file mode 100644
index 00000000..81f25fba
--- /dev/null
+++ b/src/test/resources/trywithresources/expected/org/example/Resource.java
@@ -0,0 +1,8 @@
+package org.example;
+
+public class Resource implements AutoCloseable {
+
+    public void close() throws Exception {
+        throw new Error();
+    }
+}
diff --git a/src/test/resources/trywithresources/input/com/example/Simple.java b/src/test/resources/trywithresources/input/com/example/Simple.java
new file mode 100644
index 00000000..06d3330d
--- /dev/null
+++ b/src/test/resources/trywithresources/input/com/example/Simple.java
@@ -0,0 +1,12 @@
+package com.example;
+
+import org.example.Resource;
+
+class Simple {
+    // Target method.
+    void bar() {
+        try (Resource r = new Resource()) {
+            // do something
+        }
+    }
+}

From a8a234e37816fd3d9959ec322e7e7cd95fb899cd Mon Sep 17 00:00:00 2001
From: Martin Kellogg <martin.kellogg@njit.edu>
Date: Thu, 25 Jul 2024 17:12:01 -0400
Subject: [PATCH 2/9] qol improvement to run just one test

---
 build.gradle              | 12 +++++++++++-
 typecheck_one_test.sh     | 28 ++++++++++++++++++++++++++++
 typecheck_test_outputs.sh | 24 ++++++++----------------
 3 files changed, 47 insertions(+), 17 deletions(-)
 create mode 100644 typecheck_one_test.sh

diff --git a/build.gradle b/build.gradle
index 1c7108ae..b4493e83 100644
--- a/build.gradle
+++ b/build.gradle
@@ -52,7 +52,6 @@ task requireJavadoc(type: JavaExec) {
 }
 
 task expectedTestOutputsMustCompile(type: Exec) {
-    // TODO: should this task run in CI, or as part of the regular tests?
     if (System.getProperty('os.name').toLowerCase().startsWith('windows')) {
         commandLine "cmd", "/c", "typecheck_test_outputs.bat"
     } else {
@@ -60,6 +59,17 @@ task expectedTestOutputsMustCompile(type: Exec) {
     }
 }
 
+// run via e.g.: ./gradlew checkExpectedOutputCompilesFor -PtestName="onefilesimple"
+task checkExpectedOutputCompilesFor(type: Exec) {
+    workingDir("src/test/resources")
+    if (System.getProperty('os.name').toLowerCase().startsWith('windows')) {
+        // TODO: fix this
+        print "checkIfTestCompiles is not supported on Windows"
+    } else {
+        commandLine "sh", "../../../typecheck_one_test.sh", project.property("testName")
+    }
+}
+
 tasks.compileJava {
     // uncomment for testing
     // options.errorprone.enabled = false
diff --git a/typecheck_one_test.sh b/typecheck_one_test.sh
new file mode 100644
index 00000000..019ea2bd
--- /dev/null
+++ b/typecheck_one_test.sh
@@ -0,0 +1,28 @@
+#!/bin/sh
+
+## This script runs javac on a single expected test output. If the test output
+## is compilable, it exits with code 0. If not, it exits with code 1. In all other
+# cases (e.g., if a cd command fails), it exits with code 2. It includes
+## logic for skipping test cases that don't need to compile, etc. It should be
+## run in the directory src/test/resources.
+
+testcase=$1
+
+if [ "${testcase}" = "shared" ]; then exit 0; fi
+# https://bugs.openjdk.org/browse/JDK-8319461 wasn't actually fixed (this test is based on that bug)
+if [ "${testcase}" = "superinterfaceextends" ]; then exit 0; fi
+# incomplete handling of method references: https://github.com/njit-jerse/specimin/issues/291
+# this test exists to check that no crash occurs, not that Specimin produces the correct output
+if [ "${testcase}" = "methodref2" ]; then exit 0; fi
+cd "${testcase}/expected/" || exit 2
+# javac relies on word splitting
+# shellcheck disable=SC2046
+javac -classpath "../../shared/checker-qual-3.42.0.jar" $(find . -name "*.java") \
+  || { echo "Running javac on ${testcase}/expected issues one or more errors, which are printed above."; \
+  find . -name "*.class" -exec rm {} \; ; exit 1; }
+
+# clean up
+find . -name "*.class" -exec rm {} \;
+
+cd ../.. || exit 2
+exit 0
\ No newline at end of file
diff --git a/typecheck_test_outputs.sh b/typecheck_test_outputs.sh
index a76958d5..410cdea2 100755
--- a/typecheck_test_outputs.sh
+++ b/typecheck_test_outputs.sh
@@ -1,7 +1,7 @@
 #!/bin/sh
 
 # This script runs javac on all of the expected test outputs under src/test/resources.
-# It returns 2 if any of them fail to compile, 1 if there are any malformed test directories,
+# It returns 1 if any of them fail to compile, 2 if there are any malformed test directories,
 # and 0 if all of them do compile.
 #
 # It is desirable that all of the expected test outputs compile, because Specimin
@@ -11,26 +11,18 @@ returnval=0
 
 cd src/test/resources || exit 1
 for testcase in * ; do
-    if [ "${testcase}" = "shared" ]; then continue; fi
-    # https://bugs.openjdk.org/browse/JDK-8319461 wasn't actually fixed (this test is based on that bug)
-    if [ "${testcase}" = "superinterfaceextends" ]; then continue; fi
-    # incomplete handling of method references: https://github.com/njit-jerse/specimin/issues/291
-    # this test exists to check that no crash occurs, not that Specimin produces the correct output
-    if [ "${testcase}" = "methodref2" ]; then continue; fi
-    cd "${testcase}/expected/" || exit 1
-    # javac relies on word splitting
-    # shellcheck disable=SC2046
-    javac -classpath "../../shared/checker-qual-3.42.0.jar" $(find . -name "*.java") \
-      || { echo "Running javac on ${testcase}/expected issues one or more errors, which are printed above."; returnval=2; }
-    cd ../.. || exit 1
+    sh ../../../typecheck_one_test.sh "${testcase}"
+    # update overall return value
+    test_retval=$?
+    if [ ! "${test_retval}" = 0 ]; then
+      returnval=1
+    fi
 done
 
 if [ "${returnval}" = 0 ]; then
   echo "All expected test outputs compiled successfully."
-elif [ "${returnval}" = 2 ]; then
+elif [ "${returnval}" = 1 ]; then
   echo "Some expected test outputs do not compile successfully. See the above error output for details."
 fi
 
-find . -name "*.class" -exec rm {} \;
-
 exit ${returnval}

From ef80315ea2e6ec77bf9c7754e024a0f249634da7 Mon Sep 17 00:00:00 2001
From: Martin Kellogg <martin.kellogg@njit.edu>
Date: Thu, 25 Jul 2024 17:13:03 -0400
Subject: [PATCH 3/9] fix name

---
 build.gradle | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/build.gradle b/build.gradle
index b4493e83..e1cd8ed3 100644
--- a/build.gradle
+++ b/build.gradle
@@ -64,7 +64,7 @@ task checkExpectedOutputCompilesFor(type: Exec) {
     workingDir("src/test/resources")
     if (System.getProperty('os.name').toLowerCase().startsWith('windows')) {
         // TODO: fix this
-        print "checkIfTestCompiles is not supported on Windows"
+        print "checkExpectedOutputCompilesFor is not supported on Windows"
     } else {
         commandLine "sh", "../../../typecheck_one_test.sh", project.property("testName")
     }

From 4c3e57fffded94875e3e303f68060e39e82754a4 Mon Sep 17 00:00:00 2001
From: Martin Kellogg <martin.kellogg@njit.edu>
Date: Thu, 25 Jul 2024 17:14:38 -0400
Subject: [PATCH 4/9] fix test

---
 .../resources/trywithresources/expected/com/example/Simple.java | 2 +-
 .../resources/trywithresources/input/com/example/Simple.java    | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/test/resources/trywithresources/expected/com/example/Simple.java b/src/test/resources/trywithresources/expected/com/example/Simple.java
index 647cd3e9..8709f0b9 100644
--- a/src/test/resources/trywithresources/expected/com/example/Simple.java
+++ b/src/test/resources/trywithresources/expected/com/example/Simple.java
@@ -4,7 +4,7 @@
 
 class Simple {
 
-    void bar() {
+    void bar() throws Exception {
         try (Resource r = new Resource()) {
         }
     }
diff --git a/src/test/resources/trywithresources/input/com/example/Simple.java b/src/test/resources/trywithresources/input/com/example/Simple.java
index 06d3330d..0add9feb 100644
--- a/src/test/resources/trywithresources/input/com/example/Simple.java
+++ b/src/test/resources/trywithresources/input/com/example/Simple.java
@@ -4,7 +4,7 @@
 
 class Simple {
     // Target method.
-    void bar() {
+    void bar() throws Exception {
         try (Resource r = new Resource()) {
             // do something
         }

From 2c2780e94f767c096d3f63728b90ffa309017f75 Mon Sep 17 00:00:00 2001
From: Martin Kellogg <martin.kellogg@njit.edu>
Date: Thu, 25 Jul 2024 17:16:10 -0400
Subject: [PATCH 5/9] safeguard

---
 build.gradle | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/build.gradle b/build.gradle
index e1cd8ed3..6d389d91 100644
--- a/build.gradle
+++ b/build.gradle
@@ -61,12 +61,14 @@ task expectedTestOutputsMustCompile(type: Exec) {
 
 // run via e.g.: ./gradlew checkExpectedOutputCompilesFor -PtestName="onefilesimple"
 task checkExpectedOutputCompilesFor(type: Exec) {
-    workingDir("src/test/resources")
-    if (System.getProperty('os.name').toLowerCase().startsWith('windows')) {
-        // TODO: fix this
-        print "checkExpectedOutputCompilesFor is not supported on Windows"
-    } else {
-        commandLine "sh", "../../../typecheck_one_test.sh", project.property("testName")
+    if (project.hasProperty("testName")) {
+        workingDir("src/test/resources")
+        if (System.getProperty('os.name').toLowerCase().startsWith('windows')) {
+            // TODO: fix this
+            print "checkExpectedOutputCompilesFor is not supported on Windows"
+        } else {
+            commandLine "sh", "../../../typecheck_one_test.sh", project.property("testName")
+        }
     }
 }
 

From ab0ebf8e0ec0ec405fe8b6d898b8484674cb2b6c Mon Sep 17 00:00:00 2001
From: Martin Kellogg <martin.kellogg@njit.edu>
Date: Fri, 26 Jul 2024 09:55:34 -0400
Subject: [PATCH 6/9] checkpoint

---
 .../specimin/UnsolvedClassOrInterface.java    | 28 +++++++-
 .../specimin/UnsolvedSymbolVisitor.java       | 64 +++++++++++++++++++
 .../specimin/TryWithResourcesTest.java        |  2 +-
 .../expected/com/example/Simple.java          | 10 ++-
 .../input/com/example/Simple.java             | 13 +++-
 5 files changed, 113 insertions(+), 4 deletions(-)

diff --git a/src/main/java/org/checkerframework/specimin/UnsolvedClassOrInterface.java b/src/main/java/org/checkerframework/specimin/UnsolvedClassOrInterface.java
index 17fade16..a57a2d8f 100644
--- a/src/main/java/org/checkerframework/specimin/UnsolvedClassOrInterface.java
+++ b/src/main/java/org/checkerframework/specimin/UnsolvedClassOrInterface.java
@@ -1,6 +1,8 @@
 package org.checkerframework.specimin;
 
 import com.google.common.base.Splitter;
+
+import java.util.ArrayList;
 import java.util.HashSet;
 import java.util.Iterator;
 import java.util.LinkedHashSet;
@@ -43,9 +45,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 List<String> implementsClauses = new ArrayList<>(0);
+
   /** This field records if the class is an interface */
   private boolean isAnInterface;
 
@@ -283,6 +288,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 +513,18 @@ public String toString() {
     if (extendsClause != null) {
       sb.append(" ").append(extendsClause);
     }
+    if (implementsClauses.size() > 0) {
+      if (extendsClause != null) {
+        sb.append(", ");
+      }
+      sb.append(" implements ");
+      for (int i = 0; i < implementsClauses.size(); i++) {
+        sb.append(implementsClauses.get(i));
+        if (i < implementsClauses.size() - 1) {
+          sb.append(", ");
+        }
+      }
+    }
     sb.append(" {\n");
     if (innerClasses != null) {
       for (UnsolvedClassOrInterface innerClass : innerClasses) {
diff --git a/src/main/java/org/checkerframework/specimin/UnsolvedSymbolVisitor.java b/src/main/java/org/checkerframework/specimin/UnsolvedSymbolVisitor.java
index c829082e..e9a67776 100644
--- a/src/main/java/org/checkerframework/specimin/UnsolvedSymbolVisitor.java
+++ b/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,74 @@ 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;
+        }
+        System.out.println("as var type: " + fqn);
+        makeClassAutoCloseable(fqn);
+      } else if (resource.isNameExpr()) {
+        NameExpr asName = resource.asNameExpr();
+        System.out.println("as name: " + asName);
+      } else if (resource.isFieldAccessExpr()) {
+        FieldAccessExpr asField = resource.asFieldAccessExpr();
+        System.out.println("as field: " + asField);
+      } 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");
+        // TODO: add the close() method.
+      }
+    }
+  }
+
   @Override
   @SuppressWarnings("nullness")
   // This method returns a nullable result, and "comment" can be null for the phrase
diff --git a/src/test/java/org/checkerframework/specimin/TryWithResourcesTest.java b/src/test/java/org/checkerframework/specimin/TryWithResourcesTest.java
index 599ba4a0..469da25f 100644
--- a/src/test/java/org/checkerframework/specimin/TryWithResourcesTest.java
+++ b/src/test/java/org/checkerframework/specimin/TryWithResourcesTest.java
@@ -13,6 +13,6 @@ public void runTest() throws IOException {
     SpeciminTestExecutor.runTestWithoutJarPaths(
         "trywithresources",
         new String[] {"com/example/Simple.java"},
-        new String[] {"com.example.Simple#bar()"});
+        new String[] {"com.example.Simple#bar(OtherResource)"});
   }
 }
diff --git a/src/test/resources/trywithresources/expected/com/example/Simple.java b/src/test/resources/trywithresources/expected/com/example/Simple.java
index 8709f0b9..aab4cffb 100644
--- a/src/test/resources/trywithresources/expected/com/example/Simple.java
+++ b/src/test/resources/trywithresources/expected/com/example/Simple.java
@@ -1,11 +1,19 @@
 package com.example;
 
 import org.example.Resource;
+import org.example.OtherResource;
+import org.example.ThirdResource;
 
 class Simple {
 
-    void bar() throws Exception {
+    private ThirdResource r;
+
+    void bar(OtherResource o) throws Exception {
         try (Resource r = new Resource()) {
         }
+        try (o) {
+        }
+        try (r) {
+        }
     }
 }
diff --git a/src/test/resources/trywithresources/input/com/example/Simple.java b/src/test/resources/trywithresources/input/com/example/Simple.java
index 0add9feb..fb8992a1 100644
--- a/src/test/resources/trywithresources/input/com/example/Simple.java
+++ b/src/test/resources/trywithresources/input/com/example/Simple.java
@@ -1,12 +1,23 @@
 package com.example;
 
 import org.example.Resource;
+import org.example.OtherResource;
+import org.example.ThirdResource;
 
 class Simple {
+
+    private ThirdResource r;
+
     // Target method.
-    void bar() throws Exception {
+    void bar(OtherResource o) throws Exception {
         try (Resource r = new Resource()) {
             // do something
         }
+        try (o) {
+            // do something else
+        }
+        try (r) {
+
+        }
     }
 }

From e6aea6e04ee705500a100bc187f72a9aac1ff789 Mon Sep 17 00:00:00 2001
From: Martin Kellogg <martin.kellogg@njit.edu>
Date: Fri, 26 Jul 2024 10:46:34 -0400
Subject: [PATCH 7/9] works for simple case, but added more test cases that
 fail

---
 .../org/checkerframework/specimin/PrunerVisitor.java |  6 ++++++
 .../specimin/UnsolvedClassOrInterface.java           | 11 +++++------
 .../checkerframework/specimin/UnsolvedMethod.java    | 11 +++++++++++
 .../specimin/UnsolvedSymbolVisitor.java              | 12 ++++++------
 .../expected/org/example/OtherResource.java          |  8 ++++++++
 .../expected/org/example/Resource.java               |  8 ++++++--
 .../expected/org/example/ThirdResource.java          |  8 ++++++++
 7 files changed, 50 insertions(+), 14 deletions(-)
 create mode 100644 src/test/resources/trywithresources/expected/org/example/OtherResource.java
 create mode 100644 src/test/resources/trywithresources/expected/org/example/ThirdResource.java

diff --git a/src/main/java/org/checkerframework/specimin/PrunerVisitor.java b/src/main/java/org/checkerframework/specimin/PrunerVisitor.java
index 52a42390..b8469022 100644
--- a/src/main/java/org/checkerframework/specimin/PrunerVisitor.java
+++ b/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();
         }
diff --git a/src/main/java/org/checkerframework/specimin/UnsolvedClassOrInterface.java b/src/main/java/org/checkerframework/specimin/UnsolvedClassOrInterface.java
index a57a2d8f..b5fb5b07 100644
--- a/src/main/java/org/checkerframework/specimin/UnsolvedClassOrInterface.java
+++ b/src/main/java/org/checkerframework/specimin/UnsolvedClassOrInterface.java
@@ -1,8 +1,6 @@
 package org.checkerframework.specimin;
 
 import com.google.common.base.Splitter;
-
-import java.util.ArrayList;
 import java.util.HashSet;
 import java.util.Iterator;
 import java.util.LinkedHashSet;
@@ -49,7 +47,7 @@ public class UnsolvedClassOrInterface {
   private @Nullable String extendsClause;
 
   /** The implements clauses, if they exist. */
-  private List<String> implementsClauses = new ArrayList<>(0);
+  private Set<String> implementsClauses = new LinkedHashSet<>(0);
 
   /** This field records if the class is an interface */
   private boolean isAnInterface;
@@ -518,9 +516,10 @@ public String toString() {
         sb.append(", ");
       }
       sb.append(" implements ");
-      for (int i = 0; i < implementsClauses.size(); i++) {
-        sb.append(implementsClauses.get(i));
-        if (i < implementsClauses.size() - 1) {
+      Iterator<String> interfaces = implementsClauses.iterator();
+      while (interfaces.hasNext()) {
+        sb.append(interfaces.next());
+        if (interfaces.hasNext()) {
           sb.append(", ");
         }
       }
diff --git a/src/main/java/org/checkerframework/specimin/UnsolvedMethod.java b/src/main/java/org/checkerframework/specimin/UnsolvedMethod.java
index 048b6f3f..c5dcef8f 100644
--- a/src/main/java/org/checkerframework/specimin/UnsolvedMethod.java
+++ b/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;
 
diff --git a/src/main/java/org/checkerframework/specimin/UnsolvedSymbolVisitor.java b/src/main/java/org/checkerframework/specimin/UnsolvedSymbolVisitor.java
index e9a67776..7beaef94 100644
--- a/src/main/java/org/checkerframework/specimin/UnsolvedSymbolVisitor.java
+++ b/src/main/java/org/checkerframework/specimin/UnsolvedSymbolVisitor.java
@@ -692,11 +692,11 @@ private void handleSyntheticResources(List<Expression> resources) {
   }
 
   /**
-   * 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).
+   * 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
    */
@@ -704,7 +704,7 @@ private void makeClassAutoCloseable(String fqn) {
     for (UnsolvedClassOrInterface sytheticClass : missingClass) {
       if (sytheticClass.getQualifiedClassName().equals(fqn)) {
         sytheticClass.implement("java.lang.AutoCloseable");
-        // TODO: add the close() method.
+        sytheticClass.addMethod(UnsolvedMethod.CLOSE);
       }
     }
   }
diff --git a/src/test/resources/trywithresources/expected/org/example/OtherResource.java b/src/test/resources/trywithresources/expected/org/example/OtherResource.java
new file mode 100644
index 00000000..bc945966
--- /dev/null
+++ b/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();
+    }
+}
diff --git a/src/test/resources/trywithresources/expected/org/example/Resource.java b/src/test/resources/trywithresources/expected/org/example/Resource.java
index 81f25fba..b4af2ac5 100644
--- a/src/test/resources/trywithresources/expected/org/example/Resource.java
+++ b/src/test/resources/trywithresources/expected/org/example/Resource.java
@@ -1,8 +1,12 @@
 package org.example;
 
-public class Resource implements AutoCloseable {
+public class Resource implements java.lang.AutoCloseable {
 
-    public void close() throws Exception {
+    public Resource() {
+        throw new Error();
+    }
+
+    public void close() throws java.lang.Exception {
         throw new Error();
     }
 }
diff --git a/src/test/resources/trywithresources/expected/org/example/ThirdResource.java b/src/test/resources/trywithresources/expected/org/example/ThirdResource.java
new file mode 100644
index 00000000..323dead0
--- /dev/null
+++ b/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();
+    }
+}

From b526b1a1864be70d290ac971822728be15c829f0 Mon Sep 17 00:00:00 2001
From: Martin Kellogg <martin.kellogg@njit.edu>
Date: Fri, 26 Jul 2024 10:48:20 -0400
Subject: [PATCH 8/9] all tests passing

---
 .../specimin/UnsolvedSymbolVisitor.java       | 19 ++++++++++++++++---
 1 file changed, 16 insertions(+), 3 deletions(-)

diff --git a/src/main/java/org/checkerframework/specimin/UnsolvedSymbolVisitor.java b/src/main/java/org/checkerframework/specimin/UnsolvedSymbolVisitor.java
index 7beaef94..bdd3cb2a 100644
--- a/src/main/java/org/checkerframework/specimin/UnsolvedSymbolVisitor.java
+++ b/src/main/java/org/checkerframework/specimin/UnsolvedSymbolVisitor.java
@@ -673,14 +673,27 @@ private void handleSyntheticResources(List<Expression> resources) {
           gotException();
           continue;
         }
-        System.out.println("as var type: " + fqn);
         makeClassAutoCloseable(fqn);
       } else if (resource.isNameExpr()) {
         NameExpr asName = resource.asNameExpr();
-        System.out.println("as name: " + asName);
+        String fqn;
+        try {
+          fqn = asName.resolve().getType().describe();
+        } catch (UnsolvedSymbolException e) {
+          gotException();
+          continue;
+        }
+        makeClassAutoCloseable(fqn);
       } else if (resource.isFieldAccessExpr()) {
         FieldAccessExpr asField = resource.asFieldAccessExpr();
-        System.out.println("as field: " + asField);
+        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: "

From a50bf8e3cd78022e248bb0415ce74ff0bde2654a Mon Sep 17 00:00:00 2001
From: Martin Kellogg <martin.kellogg@njit.edu>
Date: Fri, 26 Jul 2024 11:56:24 -0400
Subject: [PATCH 9/9] variables need to be final

---
 .../trywithresources/expected/com/example/Simple.java         | 4 ++--
 .../resources/trywithresources/input/com/example/Simple.java  | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/test/resources/trywithresources/expected/com/example/Simple.java b/src/test/resources/trywithresources/expected/com/example/Simple.java
index aab4cffb..d3ebc5a7 100644
--- a/src/test/resources/trywithresources/expected/com/example/Simple.java
+++ b/src/test/resources/trywithresources/expected/com/example/Simple.java
@@ -6,9 +6,9 @@
 
 class Simple {
 
-    private ThirdResource r;
+    private final ThirdResource r = null;
 
-    void bar(OtherResource o) throws Exception {
+    void bar(final OtherResource o) throws Exception {
         try (Resource r = new Resource()) {
         }
         try (o) {
diff --git a/src/test/resources/trywithresources/input/com/example/Simple.java b/src/test/resources/trywithresources/input/com/example/Simple.java
index fb8992a1..95d45edf 100644
--- a/src/test/resources/trywithresources/input/com/example/Simple.java
+++ b/src/test/resources/trywithresources/input/com/example/Simple.java
@@ -6,10 +6,10 @@
 
 class Simple {
 
-    private ThirdResource r;
+    private final ThirdResource r = null;
 
     // Target method.
-    void bar(OtherResource o) throws Exception {
+    void bar(final OtherResource o) throws Exception {
         try (Resource r = new Resource()) {
             // do something
         }