Skip to content

Commit aa5f735

Browse files
smowtonsmowton
committed
Remove fall-through CFG edge for exhaustive switch statements
1 parent 1047a89 commit aa5f735

File tree

4 files changed

+85
-1
lines changed

4 files changed

+85
-1
lines changed

‎java/ql/lib/semmle/code/java/ControlFlowGraph.qll

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -936,7 +936,12 @@ private module ControlFlowGraphImpl {
936936
completion = NormalCompletion()
937937
or
938938
// if no default case exists, then normal completion of the expression may terminate the switch
939+
// Note this can't happen if there are pattern cases or a null literal, as
940+
// https://docs.oracle.com/javase/specs/jls/se21/html/jls-14.html#jls-14.11.2 requires that such
941+
// an enhanced switch block is exhaustive.
939942
not exists(switch.getDefaultCase()) and
943+
not exists(switch.getAPatternCase()) and
944+
not switch.hasNullCase() and
940945
last(switch.getExpr(), last, completion) and
941946
completion = NormalCompletion()
942947
)

‎java/ql/test/library-tests/pattern-switch/cfg/Exhaustive.java

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
public class Exhaustive {
2+
3+
enum E { A, B, C };
4+
sealed interface I permits X, Y { }
5+
final class X implements I { }
6+
final class Y implements I { }
7+
8+
public static void test(E e, I i, Object o) {
9+
10+
// Check the CFGs of three different ways to be exhaustive -- in particular there shouldn't be a fall-through nothing-matched edge.
11+
switch (o) {
12+
case String s -> { }
13+
case Object o2 -> { }
14+
}
15+
16+
// Exhaustiveness not yet detected by CodeQL, because it is legal to omit some enum entries without a `default` case,
17+
// so we'd need to check every enum entry in the type of E occurs in some case.
18+
switch (e) {
19+
case A -> { }
20+
case B -> { }
21+
case C -> { }
22+
}
23+
24+
switch (i) {
25+
case X x -> { }
26+
case Y y -> { }
27+
}
28+
29+
}
30+
31+
}

‎java/ql/test/library-tests/pattern-switch/cfg/test.expected

Lines changed: 48 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,51 @@
1+
| Exhaustive.java:1:14:1:23 | super(...) | Exhaustive.java:1:14:1:23 | Exhaustive |
2+
| Exhaustive.java:1:14:1:23 | { ... } | Exhaustive.java:1:14:1:23 | super(...) |
3+
| Exhaustive.java:3:8:3:8 | super(...) | Exhaustive.java:3:8:3:8 | E |
4+
| Exhaustive.java:3:8:3:8 | { ... } | Exhaustive.java:3:8:3:8 | super(...) |
5+
| Exhaustive.java:3:8:3:8 | { ... } | Exhaustive.java:3:12:3:12 | <Expr>; |
6+
| Exhaustive.java:3:12:3:12 | ...=... | Exhaustive.java:3:15:3:15 | <Expr>; |
7+
| Exhaustive.java:3:12:3:12 | <Expr>; | Exhaustive.java:3:12:3:12 | new E(...) |
8+
| Exhaustive.java:3:12:3:12 | new E(...) | Exhaustive.java:3:12:3:12 | ...=... |
9+
| Exhaustive.java:3:15:3:15 | ...=... | Exhaustive.java:3:18:3:18 | <Expr>; |
10+
| Exhaustive.java:3:15:3:15 | <Expr>; | Exhaustive.java:3:15:3:15 | new E(...) |
11+
| Exhaustive.java:3:15:3:15 | new E(...) | Exhaustive.java:3:15:3:15 | ...=... |
12+
| Exhaustive.java:3:18:3:18 | ...=... | Exhaustive.java:3:8:3:8 | <clinit> |
13+
| Exhaustive.java:3:18:3:18 | <Expr>; | Exhaustive.java:3:18:3:18 | new E(...) |
14+
| Exhaustive.java:3:18:3:18 | new E(...) | Exhaustive.java:3:18:3:18 | ...=... |
15+
| Exhaustive.java:5:15:5:15 | super(...) | Exhaustive.java:5:15:5:15 | X |
16+
| Exhaustive.java:5:15:5:15 | { ... } | Exhaustive.java:5:15:5:15 | super(...) |
17+
| Exhaustive.java:6:15:6:15 | super(...) | Exhaustive.java:6:15:6:15 | Y |
18+
| Exhaustive.java:6:15:6:15 | { ... } | Exhaustive.java:6:15:6:15 | super(...) |
19+
| Exhaustive.java:8:47:29:3 | { ... } | Exhaustive.java:11:5:11:14 | switch (...) |
20+
| Exhaustive.java:11:5:11:14 | switch (...) | Exhaustive.java:11:13:11:13 | o |
21+
| Exhaustive.java:11:13:11:13 | o | Exhaustive.java:12:7:12:22 | case <Pattern> |
22+
| Exhaustive.java:12:7:12:22 | case <Pattern> | Exhaustive.java:12:19:12:19 | s |
23+
| Exhaustive.java:12:7:12:22 | case <Pattern> | Exhaustive.java:13:7:13:23 | case <Pattern> |
24+
| Exhaustive.java:12:19:12:19 | s | Exhaustive.java:12:24:12:26 | { ... } |
25+
| Exhaustive.java:12:24:12:26 | { ... } | Exhaustive.java:18:5:18:14 | switch (...) |
26+
| Exhaustive.java:13:7:13:23 | case <Pattern> | Exhaustive.java:13:19:13:20 | o2 |
27+
| Exhaustive.java:13:19:13:20 | o2 | Exhaustive.java:13:25:13:27 | { ... } |
28+
| Exhaustive.java:13:25:13:27 | { ... } | Exhaustive.java:18:5:18:14 | switch (...) |
29+
| Exhaustive.java:18:5:18:14 | switch (...) | Exhaustive.java:18:13:18:13 | e |
30+
| Exhaustive.java:18:13:18:13 | e | Exhaustive.java:19:7:19:15 | case ... |
31+
| Exhaustive.java:18:13:18:13 | e | Exhaustive.java:20:7:20:15 | case ... |
32+
| Exhaustive.java:18:13:18:13 | e | Exhaustive.java:21:7:21:15 | case ... |
33+
| Exhaustive.java:18:13:18:13 | e | Exhaustive.java:24:5:24:14 | switch (...) |
34+
| Exhaustive.java:19:7:19:15 | case ... | Exhaustive.java:19:17:19:19 | { ... } |
35+
| Exhaustive.java:19:17:19:19 | { ... } | Exhaustive.java:24:5:24:14 | switch (...) |
36+
| Exhaustive.java:20:7:20:15 | case ... | Exhaustive.java:20:17:20:19 | { ... } |
37+
| Exhaustive.java:20:17:20:19 | { ... } | Exhaustive.java:24:5:24:14 | switch (...) |
38+
| Exhaustive.java:21:7:21:15 | case ... | Exhaustive.java:21:17:21:19 | { ... } |
39+
| Exhaustive.java:21:17:21:19 | { ... } | Exhaustive.java:24:5:24:14 | switch (...) |
40+
| Exhaustive.java:24:5:24:14 | switch (...) | Exhaustive.java:24:13:24:13 | i |
41+
| Exhaustive.java:24:13:24:13 | i | Exhaustive.java:25:7:25:17 | case <Pattern> |
42+
| Exhaustive.java:25:7:25:17 | case <Pattern> | Exhaustive.java:25:14:25:14 | x |
43+
| Exhaustive.java:25:7:25:17 | case <Pattern> | Exhaustive.java:26:7:26:17 | case <Pattern> |
44+
| Exhaustive.java:25:14:25:14 | x | Exhaustive.java:25:19:25:21 | { ... } |
45+
| Exhaustive.java:25:19:25:21 | { ... } | Exhaustive.java:8:22:8:25 | test |
46+
| Exhaustive.java:26:7:26:17 | case <Pattern> | Exhaustive.java:26:14:26:14 | y |
47+
| Exhaustive.java:26:14:26:14 | y | Exhaustive.java:26:19:26:21 | { ... } |
48+
| Exhaustive.java:26:19:26:21 | { ... } | Exhaustive.java:8:22:8:25 | test |
149
| Test.java:1:14:1:17 | super(...) | Test.java:1:14:1:17 | Test |
250
| Test.java:1:14:1:17 | { ... } | Test.java:1:14:1:17 | super(...) |
351
| Test.java:3:41:101:3 | { ... } | Test.java:5:6:5:19 | switch (...) |

‎java/ql/test/library-tests/pattern-switch/cfg/test.ql

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
import java
22

33
from ControlFlowNode cn
4-
where cn.getFile().getBaseName() = "Test.java"
4+
where cn.getFile().getBaseName() = ["Test.java", "Exhaustive.java"]
55
select cn, cn.getASuccessor()

0 commit comments

Comments
 (0)