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 17fade16..b5fb5b07 100644 --- a/src/main/java/org/checkerframework/specimin/UnsolvedClassOrInterface.java +++ b/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 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 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 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) { 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 c829082e..bdd3cb2a 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,87 @@ public Visitable visit(SwitchEntry node, Void p) { public Visitable visit(TryStmt node, Void p) { HashSet currentLocalVariables = new HashSet<>(); localVariables.addFirst(currentLocalVariables); + List 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 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 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..469da25f --- /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(OtherResource)"}); + } +} 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..d3ebc5a7 --- /dev/null +++ b/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) { + } + } +} 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 new file mode 100644 index 00000000..b4af2ac5 --- /dev/null +++ b/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(); + } +} 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(); + } +} 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..95d45edf --- /dev/null +++ b/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) { + + } + } +}