Model the implicit close() of try-with-resources

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() {}
+}

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();
+        }
+    }
+}

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() {}
+}

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();
+        }
+    }
+}

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<String, CtResource<?>> 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<CtResource<?>> 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, () -> {