diff --git a/liquidjava-example/src/main/java/testSuite/classes/try_catch_correct/Test.java b/liquidjava-example/src/main/java/testSuite/classes/try_catch_correct/Test.java new file mode 100644 index 00000000..d27b580f --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/try_catch_correct/Test.java @@ -0,0 +1,175 @@ +package testSuite.classes.try_catch_correct; + +import java.io.StringReader; + +import liquidjava.specification.Refinement; + +public class Test { + static void load() throws Exception { + throw new Exception("x"); + } + + static void sameValueInBothBranches() { + int y = 1; + try { + load(); + y = 5; + } catch (Exception e) { + y = 7; + } + @Refinement("_ > 0") + int z = y; + } + + static void catchDoesNotComplete() { + Throwable t = new Throwable("start"); + try { + load(); + } catch (Exception e) { + t = new Throwable("catch", e); + return; + } + t.initCause(new RuntimeException()); + } + + static void multipleCatches() { + int y = 1; + try { + load(); + y = 2; + } catch (RuntimeException e) { + y = 3; + } catch (Exception e) { + y = 4; + } + @Refinement("_ > 0") + int z = y; + } + + static void finallyOverridesBranches() { + int y = 1; + try { + load(); + y = -2; + } catch (Exception e) { + y = -3; + } finally { + y = 4; + } + @Refinement("_ > 0") + int z = y; + } + + static void nestedTry() { + int y = 1; + try { + try { + load(); + y = 2; + } catch (RuntimeException e) { + y = 3; + } + } catch (Exception e) { + y = 4; + } + @Refinement("_ > 0") + int z = y; + } + + static void tryWithResources() throws Exception { + int y = 1; + try (StringReader r = new StringReader("x")) { + y = 2; + } catch (RuntimeException e) { + y = 3; + } + @Refinement("_ > 0") + int z = y; + } + + static void unchangedInTry() { + Throwable t = new Throwable("start"); + try { + load(); + } catch (Exception e) { + t.initCause(e); + } + } + + // every state t has in the try allows initCause + static void everyStateInTryAllowsCall() { + Throwable t = new Throwable("start"); + try { + t = new Throwable("try"); + load(); + } catch (Exception e) { + t.initCause(e); + } + } + + // the declared refinement of y holds for every value it has in the try + static void everyValueInTryPositive() { + @Refinement("_ > 0") + int y = 1; + try { + y = 2; + load(); + } catch (Exception e) { + @Refinement("_ > 0") + int z = y; + } + } + + // every path into the finally leaves y positive + static void finallyFromEveryPath() { + int y = 1; + try { + y = 2; + load(); + return; + } catch (Exception e) { + y = 3; + } finally { + @Refinement("_ > 0") + int z = y; + } + } + + // after the finally, only the states where the try statement completed normally remain + static void afterTryFinally() { + int y = 0; + try { + y = 5; + } finally { + } + @Refinement("_ > 0") + int z = y; + } + + static void afterTryCatchFinally() { + int y = 0; + try { + load(); + y = 5; + } catch (Exception e) { + y = 6; + } finally { + } + @Refinement("_ > 0") + int z = y; + } + + // what the finally assigns holds after it + static void finallyAssignmentKept() { + int y = 0; + try { + load(); + } catch (Exception e) { + y = -1; + } finally { + y = 1; + } + @Refinement("_ > 0") + int z = y; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/try_catch_correct/ThrowableRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/try_catch_correct/ThrowableRefinements.java new file mode 100644 index 00000000..7968366b --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/try_catch_correct/ThrowableRefinements.java @@ -0,0 +1,18 @@ +package testSuite.classes.try_catch_correct; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@ExternalRefinementsFor("java.lang.Throwable") +@StateSet({"withThrowable", "noThrowable"}) +public interface ThrowableRefinements { + @StateRefinement(to = "noThrowable(this)") + void Throwable(String message); + + @StateRefinement(to = "withThrowable(this)") + void Throwable(String message, Throwable cause); + + @StateRefinement(from = "noThrowable(this)", to = "withThrowable(this)") + Throwable initCause(Throwable cause); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/try_catch_error/StoreException.java b/liquidjava-example/src/main/java/testSuite/classes/try_catch_error/StoreException.java new file mode 100644 index 00000000..58c7df3d --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/try_catch_error/StoreException.java @@ -0,0 +1,8 @@ +package testSuite.classes.try_catch_error; + +// shape of Apache Derby's StandardException: the constructor may already set the cause +class StoreException extends Exception { + StoreException(String message, Throwable cause) { + super(message, cause); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/try_catch_error/Test.java b/liquidjava-example/src/main/java/testSuite/classes/try_catch_error/Test.java new file mode 100644 index 00000000..7883a4be --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/try_catch_error/Test.java @@ -0,0 +1,189 @@ +package testSuite.classes.try_catch_error; + +import liquidjava.specification.Refinement; + +public class Test { + static void load() throws Exception { + throw new Exception("x"); + } + + // the try may complete normally, so t may be withThrowable + static void stateOfTryPathKept() { + Throwable t = new Throwable("start"); + try { + load(); + t = new Throwable("try", new RuntimeException()); + } catch (Exception e) { + t = new Throwable("catch"); + } + t.initCause(new RuntimeException()); // Expect: State Refinement Error + } + + // the catch may not run, so y may be negative + static void valueOfTryPathKept() { + int y = 0; + try { + load(); + y = -5; + } catch (Exception e) { + y = 7; + } + @Refinement("_ > 0") + int z = y; // Expect: Refinement Error + } + + // the catch may run, so y may be negative + static void valueOfCatchPathKept() { + int y = 0; + try { + load(); + y = 5; + } catch (Exception e) { + y = -5; + } + @Refinement("_ > 0") + int z = y; // Expect: Refinement Error + } + + // the exception may be thrown after t changed, so its state in the catch is unknown + static void changedBeforeException() { + Throwable t = new Throwable("start"); + try { + t.initCause(new RuntimeException()); + load(); + } catch (Exception e) { + t.initCause(new RuntimeException()); // Expect: State Refinement Error + } + } + + // only the second of several catches assigns a negative value + static void multipleCatches() { + int y = 1; + try { + load(); + } catch (RuntimeException e) { + y = 3; + } catch (Exception e) { + y = -4; + } + @Refinement("_ > 0") + int z = y; // Expect: Refinement Error + } + + // a value assigned in a nested if of the try may reach the catch + static void valueFromIfInTry(boolean b) { + int y = 1; + try { + if (b) + y = -1; + load(); + } catch (Exception e) { + @Refinement("_ > 0") + int z = y; // Expect: Refinement Error + } + } + + // the finally also runs after a catch that returns + static void finallyAfterReturningCatch() { + Throwable t = new Throwable("start"); + try { + load(); + return; + } catch (Exception e) { + t.initCause(e); + return; + } finally { + t.initCause(new RuntimeException()); // Expect: State Refinement Error + } + } + + // the finally also runs when an exception leaves the try uncaught + static void finallyAfterUncaughtException() throws Exception { + Throwable t = new Throwable("start"); + try { + t.initCause(new RuntimeException()); + load(); + t = new Throwable("again"); + } finally { + t.initCause(new RuntimeException()); // Expect: State Refinement Error + } + } + + // the exception may be thrown before the check, so the catch cannot assume it + static void pathConditionInCatch(int x) { + try { + load(); + if (x <= 0) + return; + } catch (Exception e) { + @Refinement("_ > 0") + int z = x; // Expect: Refinement Error + } + } + + // after the join the catch path may have run, so the check from the try does not hold + static void pathConditionAfterTry(int x) { + try { + load(); + if (x <= 0) + return; + } catch (Exception e) { + } + @Refinement("_ > 0") + int z = x; // Expect: Refinement Error + } + + // the finally also runs on the return, so it cannot assume the check + static void pathConditionInFinally(int x) { + try { + if (x <= 0) + return; + } finally { + @Refinement("_ > 0") + int z = x; // Expect: Refinement Error + } + } + + // the finally changes x, so the check from before the try does not hold after it + static void finallyChangesCheckedVariable(int x) throws Exception { + if (x <= 0) + return; + try { + load(); + } finally { + x = -1; + } + @Refinement("_ > 0") + int z = x; // Expect: Refinement Error + } + + // the finally changes x, so the check from the try does not hold after it + static void finallyChangesVariableCheckedInTry(int x) { + try { + if (x <= 0) + return; + } finally { + x = -1; + } + @Refinement("_ > 0") + int z = x; // Expect: Refinement Error + } + + static void drop(int i) throws StoreException { + throw new StoreException("cannot drop " + i, new RuntimeException()); + } + + // a caught exception may already carry its cause (Apache Derby, DERBY-2472, fixed in 1870e8fa: + // chaining with initCause threw "Can't overwrite cause") + static void chainCaughtExceptions() throws StoreException { + StoreException top = null; + for (int i = 0; i < 2; i++) { + try { + drop(i); + } catch (StoreException e) { + e.initCause(top); // Expect: State Refinement Error + top = e; + } + } + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/try_catch_error/ThrowableRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/try_catch_error/ThrowableRefinements.java new file mode 100644 index 00000000..27f031e8 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/try_catch_error/ThrowableRefinements.java @@ -0,0 +1,18 @@ +package testSuite.classes.try_catch_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@ExternalRefinementsFor("java.lang.Throwable") +@StateSet({"withThrowable", "noThrowable"}) +public interface ThrowableRefinements { + @StateRefinement(to = "noThrowable(this)") + void Throwable(String message); + + @StateRefinement(to = "withThrowable(this)") + void Throwable(String message, Throwable cause); + + @StateRefinement(from = "noThrowable(this)", to = "withThrowable(this)") + Throwable initCause(Throwable cause); +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java index 4e846b6f..e8731991 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java @@ -16,6 +16,8 @@ public class Context { private List aliases; private int counter; + // instances given to each variable while visiting the try statements being visited, innermost last + private final Deque>> instanceRecorders = new ArrayDeque<>(); private static Context instance; private Context() { @@ -236,6 +238,19 @@ public void addRefinementInstanceToVariable(String name, String instanceName) { ((Variable) vi1).addInstance((VariableInstance) vi2); ((VariableInstance) vi2).setParent((Variable) vi1); addInstanceVariable(vi2); + for (Map> recorder : instanceRecorders) + recorder.computeIfAbsent((Variable) vi1, v -> new ArrayList<>()).add((VariableInstance) vi2); + } + + /** + * Starts recording the instances given to each variable, until the matching {@link #stopRecordingInstances()} + */ + public void startRecordingInstances() { + instanceRecorders.push(new IdentityHashMap<>()); + } + + public Map> stopRecordingInstances() { + return instanceRecorders.pop(); } public Optional getLastVariableInstance(String name) { 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 565776cc..0810c24d 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 @@ -50,11 +50,11 @@ 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.CtTry; import spoon.reflect.code.CtTryWithResource; import spoon.reflect.code.CtUnaryOperator; import spoon.reflect.code.CtVariableAccess; @@ -63,7 +63,6 @@ import spoon.reflect.code.CtWhile; 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; @@ -78,6 +77,7 @@ public class RefinementTypeChecker extends TypeChecker { // Auxiliary TypeCheckers OperationsChecker otc; MethodsFunctionsChecker mfc; + TryChecker tryChecker; Diagnostics diagnostics = Diagnostics.getInstance(); ContextHistory contextHistory = ContextHistory.getInstance(); @@ -85,6 +85,7 @@ public RefinementTypeChecker(Context context, Factory factory) { super(context, factory); otc = new OperationsChecker(this); mfc = new MethodsFunctionsChecker(this); + tryChecker = new TryChecker(this, context, vcChecker, factory); } // --------------------- Visitors ----------------------------------- @@ -182,6 +183,10 @@ public void visitCtCatchVariable(CtCatchVariable catchVariable) { // name with a local in scope, so a variable with the same name in the context is an out-of-scope local context.removeVarFromContext(catchVariable.getSimpleName()); context.addVarToContext(catchVariable.getSimpleName(), catchVariable.getType(), new Predicate(), catchVariable); + // an instance lets refinements that refer to it outlive the catch block + String instanceName = String.format(Formats.INSTANCE, catchVariable.getSimpleName(), context.getCounter()); + context.addInstanceToContext(instanceName, catchVariable.getType(), new Predicate(), catchVariable); + context.addRefinementInstanceToVariable(catchVariable.getSimpleName(), instanceName); } @Override @@ -508,7 +513,7 @@ private boolean isUninformativeCondition(Predicate conditionRefinement, CtExpres * labeled {@code break}/{@code continue} targets, {@code try}/{@code catch}/{@code finally} flow, and infinite * loops such as {@code while (true)}. Extending this list only tightens precision. */ - private boolean canCompleteNormally(CtStatement statement) { + boolean canCompleteNormally(CtStatement statement) { if (statement == null) return true; if (statement instanceof CtReturn || statement instanceof CtThrow || statement instanceof CtBreak @@ -528,35 +533,14 @@ private boolean canCompleteNormally(CtStatement statement) { return true; } + @Override + public void visitCtTry(CtTry tryBlock) { + tryChecker.visitTry(tryBlock); + } + @Override public void visitCtTryWithResource(CtTryWithResource tryWithResource) { - // a resource is either a declaration (`try (R r = ...)`) or a reference to an existing variable (Java 9 `try - // (r)`) - List> resources = tryWithResource.getResources(); - scan(resources); - scan(tryWithResource.getBody()); - - // the resources are closed when the body ends, in reverse order, before any catch or finally block runs - for (int i = resources.size() - 1; i >= 0; i--) - scan(createImplicitClose(resources.get(i), tryWithResource)); - scan(tryWithResource.getCatchers()); - scan(tryWithResource.getFinalizer()); - } - - /** Builds the {@code resource.close()} that Java inserts at the end of a try-with-resources block */ - private CtInvocation createImplicitClose(CtResource resource, CtTryWithResource tryWithResource) { - CtExpression target = resource instanceof CtLocalVariable variable - ? factory.Code().createVariableRead(variable.getReference(), false) - : ((CtVariableRead) resource).clone(); - CtTypeReference type = target.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")); - CtInvocation invocation = factory.Code().createInvocation(target, close); - invocation.setParent(tryWithResource); - invocation.setPosition(resource.getPosition()); - target.setPosition(resource.getPosition()); - return invocation; + tryChecker.visitTry(tryWithResource); } @Override diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TryChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TryChecker.java new file mode 100644 index 00000000..2b6ef116 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TryChecker.java @@ -0,0 +1,220 @@ +package liquidjava.processor.refinement_checker; + +import java.util.IdentityHashMap; +import java.util.List; +import java.util.Map; + +import liquidjava.processor.context.Context; +import liquidjava.processor.context.RefinedVariable; +import liquidjava.processor.context.Variable; +import liquidjava.processor.context.VariableInstance; +import liquidjava.rj_language.Predicate; +import liquidjava.utils.constants.Formats; +import spoon.reflect.code.CtCatch; +import spoon.reflect.code.CtExpression; +import spoon.reflect.code.CtInvocation; +import spoon.reflect.code.CtLocalVariable; +import spoon.reflect.code.CtResource; +import spoon.reflect.code.CtTry; +import spoon.reflect.code.CtTryWithResource; +import spoon.reflect.code.CtVariableRead; +import spoon.reflect.declaration.CtElement; +import spoon.reflect.factory.Factory; +import spoon.reflect.reference.CtExecutableReference; +import spoon.reflect.reference.CtTypeReference; + +/** + * Checks try statements. The try block and its catch blocks are combined like an if-else-if chain with unknown + * conditions. An exception may leave the try block after any of its statements, so each catch block starts with every + * variable in any of the states it had before or during the try block. The finally block also runs after returns and + * uncaught exceptions, so it starts with any of the states from the try and catch blocks. + */ +class TryChecker { + + private final RefinementTypeChecker rtc; + private final Context context; + private final VCChecker vcChecker; + private final Factory factory; + + TryChecker(RefinementTypeChecker rtc, Context context, VCChecker vcChecker, Factory factory) { + this.rtc = rtc; + this.context = context; + this.vcChecker = vcChecker; + this.factory = factory; + } + + void visitTry(CtTry tryBlock) { + // last instance of each variable before the try statement, or null if it has none + Map before = new IdentityHashMap<>(); + for (RefinedVariable rv : context.getCtxVars()) + if (rv instanceof Variable v) + before.put(v, v.getLastInstance().orElse(null)); + List pathBefore = vcChecker.getPathVariables(); + + context.startRecordingInstances(); + Map> inTryAndCatches; + try { + visitBranches(tryBlock, 0, before, null); + } finally { + inTryAndCatches = context.stopRecordingInstances(); + } + if (tryBlock.getFinalizer() != null) + visitFinally(tryBlock, before, inTryAndCatches, pathBefore); + } + + /** + * Visits the try block (branch 0) and the catch blocks (branches 1..n) from branch {@code i} like an if-else-if + * chain, combining each variable after it from the branches that can complete normally + * + * @return whether some branch from {@code i} can complete normally + */ + private boolean visitBranches(CtTry tryBlock, int i, Map before, + Map> inTry) { + if (i == tryBlock.getCatchers().size()) + return visitBranch(tryBlock, i, before, inTry); + + String pathVarName = String.format(Formats.FRESH, context.getCounter()); + Predicate cond = Predicate.createVar(pathVarName); + RefinedVariable pathVar = context.addInstanceToContext(pathVarName, factory.Type().BOOLEAN_PRIMITIVE, + new Predicate(), tryBlock); + vcChecker.addPathVariable(pathVar); + context.variablesNewIfCombination(); + context.variablesSetBeforeIf(); + context.enterContext(); + // path conditions from a branch hold neither in the next ones, which may start before it ends, nor after them + List pathBefore = vcChecker.getPathVariables(); + + context.enterContext(); + if (i == 0) + context.startRecordingInstances(); + boolean thenCompletes; + try { + thenCompletes = visitBranch(tryBlock, i, before, inTry); + } finally { + if (i == 0) + inTry = context.stopRecordingInstances(); + } + if (thenCompletes) + context.variablesSetThenIf(); + context.exitContext(); + vcChecker.restorePathVariables(pathBefore); + + context.newRefinementToVariableInContext(pathVarName, cond.negate()); + context.enterContext(); + boolean elseCompletes = visitBranches(tryBlock, i + 1, before, inTry); + if (elseCompletes) + context.variablesSetElseIf(); + context.exitContext(); + vcChecker.restorePathVariables(pathBefore); + + if (thenCompletes == elseCompletes) { + context.newRefinementToVariableInContext(pathVarName, new Predicate()); // either branch may have run + vcChecker.removePathVariable(pathVar); + } else { + context.newRefinementToVariableInContext(pathVarName, thenCompletes ? cond : cond.negate()); + } + context.exitContext(); + context.variablesCombineFromIf(cond); + context.variablesFinishIfCombination(); + return thenCompletes || elseCompletes; + } + + /** @return whether branch {@code i} can complete normally */ + private boolean visitBranch(CtTry tryBlock, int i, Map before, + Map> inTry) { + if (i == 0) { + if (tryBlock instanceof CtTryWithResource tryWithResource) + visitResourcesAndBody(tryWithResource); + else + rtc.scan(tryBlock.getBody()); + return rtc.canCompleteNormally(tryBlock.getBody()); + } + CtCatch catcher = tryBlock.getCatchers().get(i - 1); + addAnyOfInstances(before, inTry, catcher); + rtc.scan(catcher); + return rtc.canCompleteNormally(catcher.getBody()); + } + + /** + * Visits the finally block from any of the states of the try statement, then continues from the states where the + * try statement completed normally, updated with the variables changed in the finally block + */ + private void visitFinally(CtTry tryBlock, Map before, + Map> inTryAndCatches, List pathBefore) { + List pathAfterTry = vcChecker.getPathVariables(); + vcChecker.restorePathVariables(pathBefore); + context.enterContext(); + addAnyOfInstances(before, inTryAndCatches, tryBlock.getFinalizer()); + context.startRecordingInstances(); + Map> inFinally; + try { + rtc.scan(tryBlock.getFinalizer()); + } finally { + inFinally = context.stopRecordingInstances(); + } + inFinally.keySet().retainAll(before.keySet()); + Map lastInFinally = new IdentityHashMap<>(); + inFinally.keySet().forEach(v -> v.getLastInstance().ifPresent(vi -> lastInFinally.put(v, vi))); + context.exitContext(); + + lastInFinally.forEach((v, vi) -> context.addRefinementInstanceToVariable(v.getName(), vi.getName())); + // the path conditions of the normal completion hold again, except the ones on variables changed in the finally + for (RefinedVariable rv : pathAfterTry) + if (!pathBefore.contains(rv)) + vcChecker.addPathVariable(rv); + for (Variable v : inFinally.keySet()) { + vcChecker.removePathVariableThatIncludes(v.getName()); + if (before.get(v) != null) + vcChecker.removePathVariableThatIncludes(before.get(v).getName()); + inTryAndCatches.getOrDefault(v, List.of()) + .forEach(vi -> vcChecker.removePathVariableThatIncludes(vi.getName())); + } + } + + /** Gives each variable in {@code recorded} an instance that may be its instance before or any recorded one */ + private void addAnyOfInstances(Map before, + Map> recorded, CtElement element) { + recorded.forEach((v, instances) -> { + if (!before.containsKey(v)) // declared inside the try statement + return; + String name = String.format(Formats.INSTANCE, v.getName(), context.getCounter()); + Predicate anyOf = new Predicate(); // unknown if the variable had no instance before + if (before.get(v) != null) { + anyOf = before.get(v).getRenamedRefinements(name); + for (VariableInstance vi : instances) + anyOf = Predicate.createDisjunction(anyOf, vi.getRenamedRefinements(name)); + } + context.addInstanceToContext(name, v.getType(), anyOf, element); + context.addRefinementInstanceToVariable(v.getName(), name); + }); + } + + /** Visits the resources and the body of a try-with-resources, which ends by closing the resources */ + private void visitResourcesAndBody(CtTryWithResource tryWithResource) { + // a resource is either a declaration (`try (R r = ...)`) or a reference to an existing variable (Java 9 `try + // (r)`) + List> resources = tryWithResource.getResources(); + rtc.scan(resources); + rtc.scan(tryWithResource.getBody()); + + // the resources are closed when the body ends, in reverse order, before any catch or finally block runs + for (int i = resources.size() - 1; i >= 0; i--) + rtc.scan(createImplicitClose(resources.get(i), tryWithResource)); + } + + /** Builds the {@code resource.close()} that Java inserts at the end of a try-with-resources block */ + private CtInvocation createImplicitClose(CtResource resource, CtTryWithResource tryWithResource) { + CtExpression target = resource instanceof CtLocalVariable variable + ? factory.Code().createVariableRead(variable.getReference(), false) + : ((CtVariableRead) resource).clone(); + CtTypeReference type = target.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")); + CtInvocation invocation = factory.Code().createInvocation(target, close); + invocation.setParent(tryWithResource); + invocation.setPosition(resource.getPosition()); + target.setPosition(resource.getPosition()); + return invocation; + } +}