Skip to content

Commit 540db82

Browse files
CatarinaGamboaclaude
CatarinaGamboa
and
claude
committed
Combine try and catch blocks like if branches (#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. Visit them as an if-else-if chain with unknown conditions and combine each variable after the join with the existing if machinery. A catch block may start after any statement of the try block, so the variables changed in the try block are unknown at its start. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 parent ad083df commit 540db82

5 files changed

Lines changed: 300 additions & 0 deletions

File tree

‎liquidjava-example/src/main/java/testSuite/classes/try_catch_correct/Test.java‎

Lines changed: 98 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,98 @@
1+
package testSuite.classes.try_catch_correct;
2+
3+
import java.io.StringReader;
4+
5+
import liquidjava.specification.Refinement;
6+
7+
public class Test {
8+
static void load() throws Exception {
9+
throw new Exception("x");
10+
}
11+
12+
static void sameValueInBothBranches() {
13+
int y = 1;
14+
try {
15+
load();
16+
y = 5;
17+
} catch (Exception e) {
18+
y = 7;
19+
}
20+
@Refinement("_ > 0")
21+
int z = y;
22+
}
23+
24+
static void catchDoesNotComplete() {
25+
Throwable t = new Throwable("start");
26+
try {
27+
load();
28+
} catch (Exception e) {
29+
t = new Throwable("catch", e);
30+
return;
31+
}
32+
t.initCause(new RuntimeException());
33+
}
34+
35+
static void multipleCatches() {
36+
int y = 1;
37+
try {
38+
load();
39+
y = 2;
40+
} catch (RuntimeException e) {
41+
y = 3;
42+
} catch (Exception e) {
43+
y = 4;
44+
}
45+
@Refinement("_ > 0")
46+
int z = y;
47+
}
48+
49+
static void finallyOverridesBranches() {
50+
int y = 1;
51+
try {
52+
load();
53+
y = -2;
54+
} catch (Exception e) {
55+
y = -3;
56+
} finally {
57+
y = 4;
58+
}
59+
@Refinement("_ > 0")
60+
int z = y;
61+
}
62+
63+
static void nestedTry() {
64+
int y = 1;
65+
try {
66+
try {
67+
load();
68+
y = 2;
69+
} catch (RuntimeException e) {
70+
y = 3;
71+
}
72+
} catch (Exception e) {
73+
y = 4;
74+
}
75+
@Refinement("_ > 0")
76+
int z = y;
77+
}
78+
79+
static void tryWithResources() throws Exception {
80+
int y = 1;
81+
try (StringReader r = new StringReader("x")) {
82+
y = 2;
83+
} catch (RuntimeException e) {
84+
y = 3;
85+
}
86+
@Refinement("_ > 0")
87+
int z = y;
88+
}
89+
90+
static void unchangedInTry() {
91+
Throwable t = new Throwable("start");
92+
try {
93+
load();
94+
} catch (Exception e) {
95+
t.initCause(e);
96+
}
97+
}
98+
}

‎liquidjava-example/src/main/java/testSuite/classes/try_catch_correct/ThrowableRefinements.java‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
package testSuite.classes.try_catch_correct;
2+
3+
import liquidjava.specification.ExternalRefinementsFor;
4+
import liquidjava.specification.StateRefinement;
5+
import liquidjava.specification.StateSet;
6+
7+
@ExternalRefinementsFor("java.lang.Throwable")
8+
@StateSet({"withThrowable", "noThrowable"})
9+
public interface ThrowableRefinements {
10+
@StateRefinement(to = "noThrowable(this)")
11+
void Throwable(String message);
12+
13+
@StateRefinement(to = "withThrowable(this)")
14+
void Throwable(String message, Throwable cause);
15+
16+
@StateRefinement(from = "noThrowable(this)", to = "withThrowable(this)")
17+
Throwable initCause(Throwable cause);
18+
}

‎liquidjava-example/src/main/java/testSuite/classes/try_catch_error/Test.java‎

Lines changed: 72 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,72 @@
1+
package testSuite.classes.try_catch_error;
2+
3+
import liquidjava.specification.Refinement;
4+
5+
public class Test {
6+
static void load() throws Exception {
7+
throw new Exception("x");
8+
}
9+
10+
// the try may complete normally, so t may be withThrowable
11+
static void stateOfTryPathKept() {
12+
Throwable t = new Throwable("start");
13+
try {
14+
load();
15+
t = new Throwable("try", new RuntimeException());
16+
} catch (Exception e) {
17+
t = new Throwable("catch");
18+
}
19+
t.initCause(new RuntimeException()); // Expect: State Refinement Error
20+
}
21+
22+
// the catch may not run, so y may be negative
23+
static void valueOfTryPathKept() {
24+
int y = 0;
25+
try {
26+
load();
27+
y = -5;
28+
} catch (Exception e) {
29+
y = 7;
30+
}
31+
@Refinement("_ > 0")
32+
int z = y; // Expect: Refinement Error
33+
}
34+
35+
// the catch may run, so y may be negative
36+
static void valueOfCatchPathKept() {
37+
int y = 0;
38+
try {
39+
load();
40+
y = 5;
41+
} catch (Exception e) {
42+
y = -5;
43+
}
44+
@Refinement("_ > 0")
45+
int z = y; // Expect: Refinement Error
46+
}
47+
48+
// the exception may be thrown after t changed, so its state in the catch is unknown
49+
static void changedBeforeException() {
50+
Throwable t = new Throwable("start");
51+
try {
52+
t.initCause(new RuntimeException());
53+
load();
54+
} catch (Exception e) {
55+
t.initCause(new RuntimeException()); // Expect: State Refinement Error
56+
}
57+
}
58+
59+
// only the second of several catches assigns a negative value
60+
static void multipleCatches() {
61+
int y = 1;
62+
try {
63+
load();
64+
} catch (RuntimeException e) {
65+
y = 3;
66+
} catch (Exception e) {
67+
y = -4;
68+
}
69+
@Refinement("_ > 0")
70+
int z = y; // Expect: Refinement Error
71+
}
72+
}

‎liquidjava-example/src/main/java/testSuite/classes/try_catch_error/ThrowableRefinements.java‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
package testSuite.classes.try_catch_error;
2+
3+
import liquidjava.specification.ExternalRefinementsFor;
4+
import liquidjava.specification.StateRefinement;
5+
import liquidjava.specification.StateSet;
6+
7+
@ExternalRefinementsFor("java.lang.Throwable")
8+
@StateSet({"withThrowable", "noThrowable"})
9+
public interface ThrowableRefinements {
10+
@StateRefinement(to = "noThrowable(this)")
11+
void Throwable(String message);
12+
13+
@StateRefinement(to = "withThrowable(this)")
14+
void Throwable(String message, Throwable cause);
15+
16+
@StateRefinement(from = "noThrowable(this)", to = "withThrowable(this)")
17+
Throwable initCause(Throwable cause);
18+
}

‎liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java‎

Lines changed: 94 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,10 @@
33
import java.lang.annotation.Annotation;
44
import java.util.ArrayList;
55
import java.util.Arrays;
6+
import java.util.IdentityHashMap;
67
import java.util.LinkedHashSet;
78
import java.util.List;
9+
import java.util.Map;
810
import java.util.Optional;
911
import java.util.Set;
1012

@@ -31,6 +33,7 @@
3133
import spoon.reflect.code.CtBinaryOperator;
3234
import spoon.reflect.code.CtBlock;
3335
import spoon.reflect.code.CtBreak;
36+
import spoon.reflect.code.CtCatch;
3437
import spoon.reflect.code.CtConditional;
3538
import spoon.reflect.code.CtContinue;
3639
import spoon.reflect.code.CtDo;
@@ -53,6 +56,8 @@
5356
import spoon.reflect.code.CtStatement;
5457
import spoon.reflect.code.CtThisAccess;
5558
import spoon.reflect.code.CtThrow;
59+
import spoon.reflect.code.CtTry;
60+
import spoon.reflect.code.CtTryWithResource;
5661
import spoon.reflect.code.CtUnaryOperator;
5762
import spoon.reflect.code.CtVariableAccess;
5863
import spoon.reflect.code.CtVariableRead;
@@ -474,6 +479,95 @@ public void visitCtIf(CtIf ifElement) {
474479
context.variablesFinishIfCombination();
475480
}
476481

482+
@Override
483+
public void visitCtTry(CtTry tryBlock) {
484+
Map<Variable, Optional<VariableInstance>> before = new IdentityHashMap<>();
485+
for (RefinedVariable rv : context.getCtxVars())
486+
if (rv instanceof Variable v)
487+
before.put(v, v.getLastInstance());
488+
visitTryBranches(tryBlock, 0, before, new ArrayList<>());
489+
scan(tryBlock.getFinalizer());
490+
}
491+
492+
@Override
493+
public void visitCtTryWithResource(CtTryWithResource tryWithResource) {
494+
scan(tryWithResource.getResources());
495+
visitCtTry(tryWithResource);
496+
}
497+
498+
/**
499+
* Visits the try block (branch 0) and its catch blocks (branches 1..n) from branch {@code i} like an if-else-if
500+
* chain with unknown conditions, so that after them each variable is combined from all the branches that can
501+
* complete normally
502+
*
503+
* @return whether some branch from {@code i} can complete normally
504+
*/
505+
private boolean visitTryBranches(CtTry tryBlock, int i, Map<Variable, Optional<VariableInstance>> before,
506+
List<Variable> changed) {
507+
if (i == tryBlock.getCatchers().size())
508+
return visitTryBranch(tryBlock, i, before, changed);
509+
510+
String pathVarName = String.format(Formats.FRESH, context.getCounter());
511+
Predicate cond = Predicate.createVar(pathVarName);
512+
RefinedVariable freshRV = context.addInstanceToContext(pathVarName, factory.Type().BOOLEAN_PRIMITIVE,
513+
new Predicate(), tryBlock);
514+
vcChecker.addPathVariable(freshRV);
515+
516+
context.variablesNewIfCombination();
517+
context.variablesSetBeforeIf();
518+
context.enterContext();
519+
520+
context.enterContext();
521+
boolean thenCompletes = visitTryBranch(tryBlock, i, before, changed);
522+
if (thenCompletes)
523+
context.variablesSetThenIf();
524+
context.exitContext();
525+
526+
context.newRefinementToVariableInContext(pathVarName, cond.negate());
527+
context.enterContext();
528+
boolean elseCompletes = visitTryBranches(tryBlock, i + 1, before, changed);
529+
if (elseCompletes)
530+
context.variablesSetElseIf();
531+
context.exitContext();
532+
533+
if (thenCompletes == elseCompletes) {
534+
// after the join either branch may have run
535+
context.newRefinementToVariableInContext(pathVarName, new Predicate());
536+
vcChecker.removePathVariable(freshRV);
537+
} else {
538+
context.newRefinementToVariableInContext(pathVarName, thenCompletes ? cond : cond.negate());
539+
}
540+
context.exitContext();
541+
context.variablesCombineFromIf(cond);
542+
context.variablesFinishIfCombination();
543+
return thenCompletes || elseCompletes;
544+
}
545+
546+
/**
547+
* Visits branch {@code i} of a try. A catch block may start after any statement of the try block, so the variables
548+
* changed in the try block are unknown at its start
549+
*
550+
* @return whether the branch can complete normally
551+
*/
552+
private boolean visitTryBranch(CtTry tryBlock, int i, Map<Variable, Optional<VariableInstance>> before,
553+
List<Variable> changed) {
554+
if (i == 0) {
555+
scan(tryBlock.getBody());
556+
for (Map.Entry<Variable, Optional<VariableInstance>> e : before.entrySet())
557+
if (e.getKey().getLastInstance().orElse(null) != e.getValue().orElse(null))
558+
changed.add(e.getKey());
559+
return canCompleteNormally(tryBlock.getBody());
560+
}
561+
CtCatch catcher = tryBlock.getCatchers().get(i - 1);
562+
for (Variable v : changed) {
563+
String name = String.format(Formats.INSTANCE, v.getName(), context.getCounter());
564+
context.addInstanceToContext(name, v.getType(), new Predicate(), catcher);
565+
context.addRefinementInstanceToVariable(v.getName(), name);
566+
}
567+
scan(catcher);
568+
return canCompleteNormally(catcher.getBody());
569+
}
570+
477571
/**
478572
* A condition is uninformative when its refinement is the trivial {@code true} predicate yet the expression itself
479573
* is not a boolean literal — i.e. the verifier has no symbolic information to relate the branch to. Treating such a

0 commit comments

Comments
 (0)