From 3c29de44081382d3957ecba71d6c2ae206968251 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 6 Oct 2026 20:26:44 +0100 Subject: [PATCH] Model the implicit close() of try-with-resources Check `r.close()` for each resource when the try body ends, in reverse declaration order and before catch/finally, so typestate errors from the implicit close (double close, use after the block) are reported. Java 9 resource references (`try (r)`) are modelled by Spoon 10.4.2 as an implicit copy of r's declaration (initializer included), repeated once per earlier local with the same name; these are not scanned and closed once. Fixes #334 Co-Authored-By: Claude Opus 5.5 --- .../try_with_resources_correct/Res.java | 16 +++++ .../try_with_resources_correct/ResTest.java | 36 ++++++++++++ .../classes/try_with_resources_error/Res.java | 16 +++++ .../try_with_resources_error/ResTest.java | 39 +++++++++++++ .../RefinementTypeChecker.java | 58 +++++++++++++++++++ 5 files changed, 165 insertions(+) create mode 100644 liquidjava-example/src/main/java/testSuite/classes/try_with_resources_correct/Res.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/try_with_resources_correct/ResTest.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/try_with_resources_error/Res.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/try_with_resources_error/ResTest.java diff --git a/liquidjava-example/src/main/java/testSuite/classes/try_with_resources_correct/Res.java b/liquidjava-example/src/main/java/testSuite/classes/try_with_resources_correct/Res.java new file mode 100644 index 00000000..ebe042d1 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/try_with_resources_correct/Res.java @@ -0,0 +1,16 @@ +package testSuite.classes.try_with_resources_correct; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"open", "closed"}) +public class Res implements AutoCloseable { + @StateRefinement(to = "open(this)") + public Res() {} + + @StateRefinement(from = "open(this)") + public void read() {} + + @StateRefinement(from = "open(this)", to = "closed(this)") + public void close() {} +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/try_with_resources_correct/ResTest.java b/liquidjava-example/src/main/java/testSuite/classes/try_with_resources_correct/ResTest.java new file mode 100644 index 00000000..9b47acf0 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/try_with_resources_correct/ResTest.java @@ -0,0 +1,36 @@ +package testSuite.classes.try_with_resources_correct; + +public class ResTest { + static void useInside() { + try (Res r = new Res()) { + r.read(); + r.read(); + } + } + + static void multipleResources() { + try (Res a = new Res(); Res b = new Res()) { + a.read(); + b.read(); + } + } + + static void resourceReference() { + Res r = new Res(); + r.read(); + try (r) { + r.read(); + } + } + + static void withCatchAndFinally() { + try (Res r = new Res()) { + r.read(); + } catch (RuntimeException e) { + e.getMessage(); + } finally { + Res s = new Res(); + s.read(); + } + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/try_with_resources_error/Res.java b/liquidjava-example/src/main/java/testSuite/classes/try_with_resources_error/Res.java new file mode 100644 index 00000000..69e5352c --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/try_with_resources_error/Res.java @@ -0,0 +1,16 @@ +package testSuite.classes.try_with_resources_error; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"open", "closed"}) +public class Res implements AutoCloseable { + @StateRefinement(to = "open(this)") + public Res() {} + + @StateRefinement(from = "open(this)") + public void read() {} + + @StateRefinement(from = "open(this)", to = "closed(this)") + public void close() {} +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/try_with_resources_error/ResTest.java b/liquidjava-example/src/main/java/testSuite/classes/try_with_resources_error/ResTest.java new file mode 100644 index 00000000..cc91de26 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/try_with_resources_error/ResTest.java @@ -0,0 +1,39 @@ +package testSuite.classes.try_with_resources_error; + +public class ResTest { + // the implicit close() at the end of the block is a second close() + static void closeTwice() { + try (Res r = new Res()) { // Expect: State Refinement Error + r.read(); + r.close(); + } + } + + // the resource is closed after the block + static void useAfter() { + Res r = new Res(); + try (r) { + r.read(); + } + r.read(); // Expect: State Refinement Error + } + + // resources are closed before the catch block runs + static void useInCatch() { + Res r = new Res(); + try (r) { + r.read(); + } catch (RuntimeException e) { + r.read(); // Expect: State Refinement Error + } + } + + // the implicit close() of an already closed resource reference + static void closedBefore() { + Res r = new Res(); + r.close(); + try (r) { // Expect: State Refinement Error + r.hashCode(); + } + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index 4543bfa6..92001d7d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -3,8 +3,11 @@ import java.lang.annotation.Annotation; import java.util.ArrayList; import java.util.Arrays; +import java.util.Collections; +import java.util.LinkedHashMap; import java.util.LinkedHashSet; import java.util.List; +import java.util.Map; import java.util.Optional; import java.util.Set; @@ -49,17 +52,22 @@ import spoon.reflect.code.CtNewArray; import spoon.reflect.code.CtNewClass; import spoon.reflect.code.CtOperatorAssignment; +import spoon.reflect.code.CtResource; import spoon.reflect.code.CtReturn; import spoon.reflect.code.CtStatement; import spoon.reflect.code.CtThisAccess; import spoon.reflect.code.CtThrow; +import spoon.reflect.code.CtTryWithResource; import spoon.reflect.code.CtUnaryOperator; import spoon.reflect.code.CtVariableAccess; import spoon.reflect.code.CtVariableRead; import spoon.reflect.code.CtVariableWrite; import spoon.reflect.code.CtWhile; +import spoon.reflect.cu.CompilationUnit; +import spoon.reflect.cu.SourcePosition; import spoon.reflect.declaration.*; import spoon.reflect.factory.Factory; +import spoon.reflect.reference.CtExecutableReference; import spoon.reflect.reference.CtFieldReference; import spoon.reflect.reference.CtTypeReference; import spoon.reflect.reference.CtVariableReference; @@ -515,6 +523,56 @@ private boolean canCompleteNormally(CtStatement statement) { return true; } + @Override + public void visitCtTryWithResource(CtTryWithResource tryWithResource) { + // A resource reference (Java 9 `try (r)`) is modelled by Spoon as an implicit copy of r's declaration, + // initializer included, and repeated once per earlier local with the same name, so it is not scanned (that + // would re-run the initializer) and is only closed once + Map> resources = new LinkedHashMap<>(); + for (CtResource resource : tryWithResource.getResources()) { + if (!resource.isImplicit()) + scan(resource); + resources.put(resource.getSimpleName(), resource); + } + scan(tryWithResource.getBody()); + + // the resources are closed when the body ends, in reverse order, before any catch or finally block runs + List> toClose = new ArrayList<>(resources.values()); + Collections.reverse(toClose); + for (CtResource resource : toClose) { + SourcePosition position = resource.isImplicit() ? getHeaderPosition(tryWithResource) + : resource.getPosition(); + scan(createImplicitClose(resource, tryWithResource, position)); + } + scan(tryWithResource.getCatchers()); + scan(tryWithResource.getFinalizer()); + } + + /** Position of {@code try (...)}, without the blocks */ + private SourcePosition getHeaderPosition(CtTryWithResource tryWithResource) { + SourcePosition position = tryWithResource.getPosition(); + CompilationUnit cu = position.getCompilationUnit(); + int end = cu.getOriginalSourceCode().lastIndexOf(')', tryWithResource.getBody().getPosition().getSourceStart()); + if (end < position.getSourceStart()) + return position; + return factory.Core().createSourcePosition(cu, position.getSourceStart(), end, cu.getLineSeparatorPositions()); + } + + /** Builds the {@code resource.close()} that Java inserts at the end of a try-with-resources block */ + private CtInvocation createImplicitClose(CtResource resource, CtTryWithResource tryWithResource, + SourcePosition position) { + CtTypeReference type = resource.getType(); + CtExecutableReference close = type.getAllExecutables().stream() + .filter(e -> e.getSimpleName().equals("close") && e.getParameters().isEmpty()).findFirst() + .orElseGet(() -> factory.Executable().createReference(type, factory.Type().VOID_PRIMITIVE, "close")); + CtExpression target = factory.Code().createVariableRead(resource.getReference(), false); + CtInvocation invocation = factory.Code().createInvocation(target, close); + invocation.setParent(tryWithResource); + invocation.setPosition(position); + target.setPosition(position); + return invocation; + } + @Override public void visitCtWhile(CtWhile whileLoop) { visitLoop(whileLoop, () -> {