Skip to content

Commit e8fd54d

Browse files
wadoonwadoon
committed
add MultiCatch transformation to KeY
1 parent 0a91117 commit e8fd54d

6 files changed

Lines changed: 398 additions & 1 deletion

File tree

‎key.core/src/main/java/de/uka/ilkd/key/java/transformations/pipeline/MultiCatchReducer.java‎

Lines changed: 94 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,94 @@
1+
/* This file is part of KeY - https://key-project.org
2+
* KeY is licensed under the GNU General Public License Version 2
3+
* SPDX-License-Identifier: GPL-2.0-only */
4+
package de.uka.ilkd.key.java.transformations.pipeline;
5+
6+
import com.github.javaparser.ast.body.TypeDeclaration;
7+
import com.github.javaparser.ast.stmt.CatchClause;
8+
import com.github.javaparser.ast.stmt.TryStmt;
9+
import com.github.javaparser.ast.type.UnionType;
10+
11+
/// Desugaring of Multi-Catch statements to multiple single catch statements.
12+
/// ## Transformation Rules (per JLS 14.20)
13+
/// ### Multi-Catch:
14+
/// ```java
15+
/// try {
16+
/// body
17+
/// } catch (ExceptionType1 | ExceptionType2 | ExceptionType3 e) {
18+
/// handler
19+
/// }
20+
/// ```
21+
///
22+
/// becomes:
23+
/// ```java
24+
/// try {
25+
/// body
26+
/// } catch (ExceptionType1 e) {
27+
/// handler
28+
/// } catch (ExceptionType2 e) {
29+
/// handler
30+
/// } catch (ExceptionType3 e) {
31+
/// handler
32+
/// }
33+
/// ```
34+
///
35+
/// Important notes:
36+
///
37+
/// - The exception variable `e` in a multi-catch is implicitly final.
38+
/// - Each resulting catch clause gets its own copy of the handler body.
39+
/// - The order of catch clauses follows the order of exception types in the union.
40+
/// - Catch clause ordering must respect subtype relationships (more specific exceptions first).
41+
///
42+
/// @author Alexander Weigl
43+
/// @version 1 (12.07.26)
44+
/// @see [JLS 14.20](https://docs.oracle.com/javase/specs/jls/se21/html/jls-14.html#jls-14.20)
45+
public class MultiCatchReducer implements JavaTransformer {
46+
@Override
47+
public void apply(TypeDeclaration<?> td) {
48+
td.walk(TryStmt.class, this::rewrite);
49+
}
50+
51+
/**
52+
* Rewrites a try statement with multi-catch clauses to use only single catch clauses.
53+
* Each multi-catch clause is replaced by multiple single-type catch clauses.
54+
*/
55+
private void rewrite(TryStmt tryStmt) {
56+
var catchClauses = tryStmt.getCatchClauses();
57+
58+
// Process catch clauses in reverse order to safely modify the list while iterating
59+
for (int i = catchClauses.size() - 1; i >= 0; i--) {
60+
CatchClause catchClause = catchClauses.get(i);
61+
var paramType = catchClause.getParameter().getType();
62+
63+
if (paramType instanceof UnionType) {
64+
UnionType unionType = (UnionType) paramType;
65+
66+
// Create individual catch clauses for each exception type in the union
67+
for (var elementType : unionType.getElements()) {
68+
CatchClause newCatchClause = new CatchClause();
69+
70+
// Create a new parameter with the single exception type
71+
var originalParam = catchClause.getParameter();
72+
var newParam = new com.github.javaparser.ast.body.Parameter(
73+
elementType.clone(),
74+
originalParam.getName().clone()
75+
);
76+
77+
// Copy modifiers (the parameter is implicitly final in multi-catch)
78+
newParam.addFinalModifier();
79+
80+
newCatchClause.setParameter(newParam);
81+
82+
// Clone the body for each catch clause
83+
newCatchClause.setBody(catchClause.getBody().clone());
84+
85+
// Insert after the current position (will be before due to reverse iteration)
86+
catchClauses.add(i + 1, newCatchClause);
87+
}
88+
89+
// Remove the original multi-catch clause
90+
catchClauses.remove(i);
91+
}
92+
}
93+
}
94+
}

‎key.core/src/test/java/de/uka/ilkd/key/java/transformations/pipeline/MultiCatchReducerTest.java‎

Lines changed: 238 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,238 @@
1+
/* This file is part of KeY - https://key-project.org
2+
* KeY is licensed under the GNU General Public License Version 2
3+
* SPDX-License-Identifier: GPL-2.0-only */
4+
package de.uka.ilkd.key.java.transformations.pipeline;
5+
6+
import com.github.javaparser.StaticJavaParser;
7+
import com.github.javaparser.ast.CompilationUnit;
8+
import org.junit.jupiter.api.Test;
9+
10+
import static org.assertj.core.api.Assertions.assertThat;
11+
12+
/**
13+
* Tests for the {@link MultiCatchReducer} transformer.
14+
*
15+
* @author Alexander Weigl
16+
* @version 1 (12.07.26)
17+
*/
18+
class MultiCatchReducerTest {
19+
@Test
20+
void testSimpleMultiCatch() {
21+
String source = """
22+
class Demo {
23+
void run() {
24+
try {
25+
doSomething();
26+
} catch (Exception1 | Exception2 e) {
27+
System.out.println("caught: " + e);
28+
}
29+
}
30+
void doSomething() throws Exception1, Exception2 {}
31+
}
32+
""";
33+
34+
CompilationUnit cu = StaticJavaParser.parse(source);
35+
var t = new MultiCatchReducer();
36+
t.apply(cu);
37+
var actual = cu.toString();
38+
39+
var expected = """
40+
class Demo {
41+
42+
void run() {
43+
try {
44+
doSomething();
45+
} catch (Exception1 e) {
46+
System.out.println("caught: " + e);
47+
} catch (Exception2 e) {
48+
System.out.println("caught: " + e);
49+
}
50+
}
51+
52+
void doSomething() throws Exception1, Exception2 {
53+
}
54+
}
55+
""";
56+
57+
assertThat(actual).isEqualToNormalizingWhitespace(expected);
58+
}
59+
60+
@Test
61+
void testThreeExceptionTypes() {
62+
String source = """
63+
class Demo {
64+
void run() {
65+
try {
66+
doSomething();
67+
} catch (IOException | SQLException | RuntimeException e) {
68+
handle(e);
69+
}
70+
}
71+
void doSomething() throws IOException, SQLException, RuntimeException {}
72+
void handle(Exception e) {}
73+
}
74+
""";
75+
76+
CompilationUnit cu = StaticJavaParser.parse(source);
77+
var t = new MultiCatchReducer();
78+
t.apply(cu);
79+
var actual = cu.toString();
80+
81+
var expected = """
82+
class Demo {
83+
84+
void run() {
85+
try {
86+
doSomething();
87+
} catch (IOException e) {
88+
handle(e);
89+
} catch (SQLException e) {
90+
handle(e);
91+
} catch (RuntimeException e) {
92+
handle(e);
93+
}
94+
}
95+
96+
void doSomething() throws IOException, SQLException, RuntimeException {
97+
}
98+
99+
void handle(Exception e) {
100+
}
101+
}
102+
""";
103+
104+
assertThat(actual).isEqualToNormalizingWhitespace(expected);
105+
}
106+
107+
@Test
108+
void testMixedSingleAndMultiCatch() {
109+
String source = """
110+
class Demo {
111+
void run() {
112+
try {
113+
doSomething();
114+
} catch (IllegalArgumentException e) {
115+
log("illegal arg");
116+
} catch (IOException | SQLException e) {
117+
log("io/sql error");
118+
} catch (RuntimeException e) {
119+
throw e;
120+
}
121+
}
122+
void doSomething() throws IOException, SQLException {}
123+
void log(String s) {}
124+
}
125+
""";
126+
127+
CompilationUnit cu = StaticJavaParser.parse(source);
128+
var t = new MultiCatchReducer();
129+
t.apply(cu);
130+
var actual = cu.toString();
131+
132+
var expected = """
133+
class Demo {
134+
135+
void run() {
136+
try {
137+
doSomething();
138+
} catch (IllegalArgumentException e) {
139+
log("illegal arg");
140+
} catch (IOException e) {
141+
log("io/sql error");
142+
} catch (SQLException e) {
143+
log("io/sql error");
144+
} catch (RuntimeException e) {
145+
throw e;
146+
}
147+
}
148+
149+
void doSomething() throws IOException, SQLException {
150+
}
151+
152+
void log(String s) {
153+
}
154+
}
155+
""";
156+
157+
assertThat(actual).isEqualToNormalizingWhitespace(expected);
158+
}
159+
160+
@Test
161+
void testMultiCatchWithFinally() {
162+
String source = """
163+
class Demo {
164+
void run() {
165+
try {
166+
doSomething();
167+
} catch (Exception1 | Exception2 e) {
168+
handle(e);
169+
} finally {
170+
cleanup();
171+
}
172+
}
173+
void doSomething() throws Exception1, Exception2 {}
174+
void handle(Exception e) {}
175+
void cleanup() {}
176+
}
177+
""";
178+
179+
CompilationUnit cu = StaticJavaParser.parse(source);
180+
var t = new MultiCatchReducer();
181+
t.apply(cu);
182+
var actual = cu.toString();
183+
184+
var expected = """
185+
class Demo {
186+
187+
void run() {
188+
try {
189+
doSomething();
190+
} catch (Exception1 e) {
191+
handle(e);
192+
} catch (Exception2 e) {
193+
handle(e);
194+
} finally {
195+
cleanup();
196+
}
197+
}
198+
199+
void doSomething() throws Exception1, Exception2 {
200+
}
201+
202+
void handle(Exception e) {
203+
}
204+
205+
void cleanup() {
206+
}
207+
}
208+
""";
209+
210+
assertThat(actual).isEqualToNormalizingWhitespace(expected);
211+
}
212+
213+
@Test
214+
void testNoMultiCatchUnchanged() {
215+
String source = """
216+
class Demo {
217+
void run() {
218+
try {
219+
doSomething();
220+
} catch (Exception e) {
221+
handle(e);
222+
}
223+
}
224+
void doSomething() throws Exception {}
225+
void handle(Exception e) {}
226+
}
227+
""";
228+
229+
CompilationUnit cu = StaticJavaParser.parse(source);
230+
var original = cu.toString();
231+
var t = new MultiCatchReducer();
232+
t.apply(cu);
233+
var actual = cu.toString();
234+
235+
// Should remain unchanged since there's no multi-catch
236+
assertThat(actual).isEqualToNormalizingWhitespace(original);
237+
}
238+
}

‎key.ui/examples/Java/MultiCatch/MultiCatch.java‎

Lines changed: 49 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,49 @@
1+
public final class MultiCatch {
2+
/*@ ensures true; requires true; */
3+
public void m() throws Exception {
4+
// Simple multi-catch with two exception types
5+
try {
6+
doSomethingRisky();
7+
} catch (IllegalArgumentException | IllegalStateException e) {
8+
System.out.println("Caught exception: " + e);
9+
}
10+
11+
// Multi-catch with three exception types
12+
try {
13+
doAnotherRiskyThing();
14+
} catch (java.io.IOException | java.sql.SQLException | RuntimeException e) {
15+
handleError(e);
16+
}
17+
18+
// Mixed single and multi-catch
19+
try {
20+
doComplexOperation();
21+
} catch (NullPointerException e) {
22+
System.out.println("Null pointer!");
23+
} catch (IllegalArgumentException | IllegalStateException e) {
24+
System.out.println("Illegal state or argument");
25+
} catch (Exception e) {
26+
System.out.println("Other exception");
27+
}
28+
}
29+
30+
/*@ ensures true; requires true; */
31+
private void doSomethingRisky() throws IllegalArgumentException, IllegalStateException {
32+
// might throw
33+
}
34+
35+
/*@ ensures true; requires true; */
36+
private void doAnotherRiskyThing() throws java.io.IOException, java.sql.SQLException, RuntimeException {
37+
// might throw
38+
}
39+
40+
/*@ ensures true; requires true; */
41+
private void doComplexOperation() throws NullPointerException, IllegalArgumentException, IllegalStateException, Exception {
42+
// might throw
43+
}
44+
45+
/*@ ensures true; requires true; */
46+
private void handleError(Exception e) {
47+
// handle error
48+
}
49+
}

‎key.ui/examples/Java/MultiCatch/README.txt‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
example.name = Multi Catch
2+
example.path = Java 25
3+
example.file = project.key
4+
example.additionalFile.1 = MultiCatch.java
5+
6+
Multi-Catch statements are supported in KeY. They are reduced to multiple single catch clauses.
7+
8+
The proof obligation is verifiable without user interaction.

0 commit comments

Comments
 (0)