Skip to content

Commit 4340fb3

Browse files
CatarinaGamboaclaude
CatarinaGamboa
and
claude
committed
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 <noreply@anthropic.com>
1 parent 9045ecd commit 4340fb3

6 files changed

Lines changed: 575 additions & 2 deletions

File tree

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

Lines changed: 175 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,175 @@
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+
99+
// every state t has in the try allows initCause
100+
static void everyStateInTryAllowsCall() {
101+
Throwable t = new Throwable("start");
102+
try {
103+
t = new Throwable("try");
104+
load();
105+
} catch (Exception e) {
106+
t.initCause(e);
107+
}
108+
}
109+
110+
// the declared refinement of y holds for every value it has in the try
111+
static void everyValueInTryPositive() {
112+
@Refinement("_ > 0")
113+
int y = 1;
114+
try {
115+
y = 2;
116+
load();
117+
} catch (Exception e) {
118+
@Refinement("_ > 0")
119+
int z = y;
120+
}
121+
}
122+
123+
// every path into the finally leaves y positive
124+
static void finallyFromEveryPath() {
125+
int y = 1;
126+
try {
127+
y = 2;
128+
load();
129+
return;
130+
} catch (Exception e) {
131+
y = 3;
132+
} finally {
133+
@Refinement("_ > 0")
134+
int z = y;
135+
}
136+
}
137+
138+
// after the finally, only the states where the try statement completed normally remain
139+
static void afterTryFinally() {
140+
int y = 0;
141+
try {
142+
y = 5;
143+
} finally {
144+
}
145+
@Refinement("_ > 0")
146+
int z = y;
147+
}
148+
149+
static void afterTryCatchFinally() {
150+
int y = 0;
151+
try {
152+
load();
153+
y = 5;
154+
} catch (Exception e) {
155+
y = 6;
156+
} finally {
157+
}
158+
@Refinement("_ > 0")
159+
int z = y;
160+
}
161+
162+
// what the finally assigns holds after it
163+
static void finallyAssignmentKept() {
164+
int y = 0;
165+
try {
166+
load();
167+
} catch (Exception e) {
168+
y = -1;
169+
} finally {
170+
y = 1;
171+
}
172+
@Refinement("_ > 0")
173+
int z = y;
174+
}
175+
}

‎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: 171 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,171 @@
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+
73+
// a value assigned in a nested if of the try may reach the catch
74+
static void valueFromIfInTry(boolean b) {
75+
int y = 1;
76+
try {
77+
if (b)
78+
y = -1;
79+
load();
80+
} catch (Exception e) {
81+
@Refinement("_ > 0")
82+
int z = y; // Expect: Refinement Error
83+
}
84+
}
85+
86+
// the finally also runs after a catch that returns
87+
static void finallyAfterReturningCatch() {
88+
Throwable t = new Throwable("start");
89+
try {
90+
load();
91+
return;
92+
} catch (Exception e) {
93+
t.initCause(e);
94+
return;
95+
} finally {
96+
t.initCause(new RuntimeException()); // Expect: State Refinement Error
97+
}
98+
}
99+
100+
// the finally also runs when an exception leaves the try uncaught
101+
static void finallyAfterUncaughtException() throws Exception {
102+
Throwable t = new Throwable("start");
103+
try {
104+
t.initCause(new RuntimeException());
105+
load();
106+
t = new Throwable("again");
107+
} finally {
108+
t.initCause(new RuntimeException()); // Expect: State Refinement Error
109+
}
110+
}
111+
112+
// the exception may be thrown before the check, so the catch cannot assume it
113+
static void pathConditionInCatch(int x) {
114+
try {
115+
load();
116+
if (x <= 0)
117+
return;
118+
} catch (Exception e) {
119+
@Refinement("_ > 0")
120+
int z = x; // Expect: Refinement Error
121+
}
122+
}
123+
124+
// after the join the catch path may have run, so the check from the try does not hold
125+
static void pathConditionAfterTry(int x) {
126+
try {
127+
load();
128+
if (x <= 0)
129+
return;
130+
} catch (Exception e) {
131+
}
132+
@Refinement("_ > 0")
133+
int z = x; // Expect: Refinement Error
134+
}
135+
136+
// the finally also runs on the return, so it cannot assume the check
137+
static void pathConditionInFinally(int x) {
138+
try {
139+
if (x <= 0)
140+
return;
141+
} finally {
142+
@Refinement("_ > 0")
143+
int z = x; // Expect: Refinement Error
144+
}
145+
}
146+
147+
// the finally changes x, so the check from before the try does not hold after it
148+
static void finallyChangesCheckedVariable(int x) throws Exception {
149+
if (x <= 0)
150+
return;
151+
try {
152+
load();
153+
} finally {
154+
x = -1;
155+
}
156+
@Refinement("_ > 0")
157+
int z = x; // Expect: Refinement Error
158+
}
159+
160+
// the finally changes x, so the check from the try does not hold after it
161+
static void finallyChangesVariableCheckedInTry(int x) {
162+
try {
163+
if (x <= 0)
164+
return;
165+
} finally {
166+
x = -1;
167+
}
168+
@Refinement("_ > 0")
169+
int z = x; // Expect: Refinement Error
170+
}
171+
}

‎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+
}

0 commit comments

Comments
 (0)