From 6559819fd3da67aea113e3fe3f408f1f6f99471a Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Wed, 7 Oct 2026 12:36:51 +0100 Subject: [PATCH 1/2] Combine try, catch and finally blocks soundly (#364) try/catch blocks were checked one after the other, so after them only the last catch path was considered and errors on the try path were missed. - The try and catch blocks are visited like an if-else-if chain with unknown conditions, and each variable is combined after the join with the existing if machinery. - An exception may leave the try block after any of its statements, so a catch block starts with each variable in any of the states it had before or during the try block (instances are recorded while visiting it). - The finally block starts with any of the states of the try and catch blocks; after it, the normal completion state continues, updated with what the finally block changed. - Path conditions from inside a branch do not leak into later branches, the finally block, or the code after the try statement. - Catch parameters get an instance so refinements referring to them outlive the catch block. Co-Authored-By: Claude Opus 5.5 --- .../classes/try_catch_correct/Test.java | 175 ++++++++++++++ .../ThrowableRefinements.java | 18 ++ .../classes/try_catch_error/Test.java | 171 ++++++++++++++ .../try_catch_error/ThrowableRefinements.java | 18 ++ .../liquidjava/processor/context/Context.java | 15 ++ .../RefinementTypeChecker.java | 44 ++-- .../refinement_checker/TryChecker.java | 220 ++++++++++++++++++ 7 files changed, 631 insertions(+), 30 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/classes/try_catch_correct/Test.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/try_catch_correct/ThrowableRefinements.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/try_catch_error/Test.java create mode 100644 liquidjava-example/src/main/java/testSuite/classes/try_catch_error/ThrowableRefinements.java create mode 100644 liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TryChecker.java 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/Test.java b/liquidjava-example/src/main/java/testSuite/classes/try_catch_error/Test.java new file mode 100644 index 00000000..32378642 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/try_catch_error/Test.java @@ -0,0 +1,171 @@ +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 + } +} 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; + } +} From 6634032adf9a35bf5d2865c7c433754caee62a12 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa <52540187+CatarinaGamboa@users.noreply.github.com> Date: Thu, 8 Oct 2026 14:03:30 +0100 Subject: [PATCH 2/2] Test chaining a caught exception that may already have its cause The Apache Derby shape behind DERBY-2472: exceptions caught in a loop are chained with initCause, but their constructor may already have set the cause, so the call can throw "Can't overwrite cause". The catch parameter's state is unknown, so the call is reported. Co-Authored-By: Claude Opus 5.5 --- .../try_catch_error/StoreException.java | 8 ++++++++ .../classes/try_catch_error/Test.java | 18 ++++++++++++++++++ 2 files changed, 26 insertions(+) create mode 100644 liquidjava-example/src/main/java/testSuite/classes/try_catch_error/StoreException.java 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 index 32378642..7883a4be 100644 --- 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 @@ -168,4 +168,22 @@ static void finallyChangesVariableCheckedInTry(int x) { @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; + } + } + } }