Skip to content

Commit dcfc4eb

Browse files
CatarinaGamboaclaude
CatarinaGamboa
and
claude
authored
Combine try, catch and finally blocks soundly (#366)
Closes #339 and #364. `try`/`catch` was checked as straight-line code: first the `try`, then the `catch`. An exception can leave the `try` after any statement, and a `finally` also runs after `return`s and uncaught exceptions. Because of that, errors in all three places were missed. ### Example ```java int y = 1; try { y = -1; load(); // may throw y = 2; } catch (Exception e) { // (1) start of catch y = 3; } finally { // (3) start of finally } // (2) after the try statement ``` | Point | `main` assumes | This PR assumes | |---|---|---| | (1) start of catch | `y == 2` (the whole `try` ran) | `y == 1 ∨ y == -1 ∨ y == 2` | | (2) after the try statement | `y == 3` (the `catch` always ran) | `c ? y == 2 : y == 3` | | (3) start of finally | `y == 3` | any of the above | **Walkthrough** 1. **Start of the `catch`:** while checking the `try`, every new value of `y` is recorded (`-1`, `2`). The `catch` starts from "the value before the `try` or any recorded value". So `@Refinement("_ > 0") int a = y;` placed at (1) is now an error; on `main` it passed. 2. **After the `try` statement:** the `try` and the `catch` are joined like an `if`/`else` on an unknown condition `c`, reusing the `if` machinery. So `@Refinement("_ == 3") int b = y;` placed at (2) is now an error. 3. **Start of the `finally`:** it starts from any value seen in the `try` or the `catch`. After it, checking continues from the joined state (2), plus whatever the `finally` assigns. Path conditions from inside a branch (e.g. `if (x <= 0) return;` in the `try`) are also dropped before the next branch, the `finally` and the code after, since the exception may come before the check. ### Changes - **New `TryChecker`:** holds the `try`/`catch`/`finally` logic. The existing try-with-resources code moved there from `RefinementTypeChecker`, which is now smaller than on `main`. - **`Context`:** `startRecordingInstances` / `stopRecordingInstances` record the new values variables get inside a block. - **Tests:** `try_catch_error` and `try_catch_correct`, 13 cases each. ### Limitations - A `finally` that updates a variable from itself (`y = y + 1`) starts from every possible value. This is sound but imprecise. - Fields are not tracked, the same as for `if`s. - Catch and finally entries conservatively include the pre-try state even when only later operations can throw. This can reject valid code such as `x = 1; risky();` followed by a catch requiring `x == 1`. Exception-point-aware snapshots would improve precision. 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
1 parent 321a732 commit dcfc4eb

8 files changed

Lines changed: 657 additions & 30 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/StoreException.java‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
package testSuite.classes.try_catch_error;
2+
3+
// shape of Apache Derby's StandardException: the constructor may already set the cause
4+
class StoreException extends Exception {
5+
StoreException(String message, Throwable cause) {
6+
super(message, cause);
7+
}
8+
}

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

Lines changed: 189 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,189 @@
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+
172+
static void drop(int i) throws StoreException {
173+
throw new StoreException("cannot drop " + i, new RuntimeException());
174+
}
175+
176+
// a caught exception may already carry its cause (Apache Derby, DERBY-2472, fixed in 1870e8fa:
177+
// chaining with initCause threw "Can't overwrite cause")
178+
static void chainCaughtExceptions() throws StoreException {
179+
StoreException top = null;
180+
for (int i = 0; i < 2; i++) {
181+
try {
182+
drop(i);
183+
} catch (StoreException e) {
184+
e.initCause(top); // Expect: State Refinement Error
185+
top = e;
186+
}
187+
}
188+
}
189+
}

0 commit comments

Comments
 (0)