hohn/codeql
1
0
Fork 0
mirror of https://github.com/github/codeql.git synced 2026-04-26 09:15:12 +02:00
Code Issues Packages Projects Releases Wiki Activity

Remove fall-through CFG edge for exhaustive switch statements

Browse Source
This commit is contained in:
Chris Smowton
2023-11-22 20:21:39 +00:00
parent 1047a89613
commit aa5f7352e2
4 changed files with 85 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

5
java/ql/lib/semmle/code/java/ControlFlowGraph.qll
View File

@@ -936,7 +936,12 @@ private module ControlFlowGraphImpl {
completion = NormalCompletion()
or
// if no default case exists, then normal completion of the expression may terminate the switch
// Note this can't happen if there are pattern cases or a null literal, as
// https://docs.oracle.com/javase/specs/jls/se21/html/jls-14.html#jls-14.11.2 requires that such
// an enhanced switch block is exhaustive.
not exists(switch.getDefaultCase()) and
not exists(switch.getAPatternCase()) and
not switch.hasNullCase() and
last(switch.getExpr(), last, completion) and
completion = NormalCompletion()
)

31
java/ql/test/library-tests/pattern-switch/cfg/Exhaustive.java Normal file
View File

@@ -0,0 +1,31 @@
public class Exhaustive {
enum E { A, B, C };
sealed interface I permits X, Y { }
final class X implements I { }
final class Y implements I { }
public static void test(E e, I i, Object o) {
// Check the CFGs of three different ways to be exhaustive -- in particular there shouldn't be a fall-through nothing-matched edge.
switch (o) {
case String s -> { }
case Object o2 -> { }
}
// Exhaustiveness not yet detected by CodeQL, because it is legal to omit some enum entries without a `default` case,
// so we'd need to check every enum entry in the type of E occurs in some case.
switch (e) {
case A -> { }
case B -> { }
case C -> { }
}
switch (i) {
case X x -> { }
case Y y -> { }
}
}
}

48
java/ql/test/library-tests/pattern-switch/cfg/test.expected
View File

@@ -1,3 +1,51 @@
| Exhaustive.java:1:14:1:23 | super(...) | Exhaustive.java:1:14:1:23 | Exhaustive |
| Exhaustive.java:1:14:1:23 | { ... } | Exhaustive.java:1:14:1:23 | super(...) |
| Exhaustive.java:3:8:3:8 | super(...) | Exhaustive.java:3:8:3:8 | E |
| Exhaustive.java:3:8:3:8 | { ... } | Exhaustive.java:3:8:3:8 | super(...) |
| Exhaustive.java:3:8:3:8 | { ... } | Exhaustive.java:3:12:3:12 | <Expr>; |
| Exhaustive.java:3:12:3:12 | ...=... | Exhaustive.java:3:15:3:15 | <Expr>; |
| Exhaustive.java:3:12:3:12 | <Expr>; | Exhaustive.java:3:12:3:12 | new E(...) |
| Exhaustive.java:3:12:3:12 | new E(...) | Exhaustive.java:3:12:3:12 | ...=... |
| Exhaustive.java:3:15:3:15 | ...=... | Exhaustive.java:3:18:3:18 | <Expr>; |
| Exhaustive.java:3:15:3:15 | <Expr>; | Exhaustive.java:3:15:3:15 | new E(...) |
| Exhaustive.java:3:15:3:15 | new E(...) | Exhaustive.java:3:15:3:15 | ...=... |
| Exhaustive.java:3:18:3:18 | ...=... | Exhaustive.java:3:8:3:8 | <clinit> |
| Exhaustive.java:3:18:3:18 | <Expr>; | Exhaustive.java:3:18:3:18 | new E(...) |
| Exhaustive.java:3:18:3:18 | new E(...) | Exhaustive.java:3:18:3:18 | ...=... |
| Exhaustive.java:5:15:5:15 | super(...) | Exhaustive.java:5:15:5:15 | X |
| Exhaustive.java:5:15:5:15 | { ... } | Exhaustive.java:5:15:5:15 | super(...) |
| Exhaustive.java:6:15:6:15 | super(...) | Exhaustive.java:6:15:6:15 | Y |
| Exhaustive.java:6:15:6:15 | { ... } | Exhaustive.java:6:15:6:15 | super(...) |
| Exhaustive.java:8:47:29:3 | { ... } | Exhaustive.java:11:5:11:14 | switch (...) |
| Exhaustive.java:11:5:11:14 | switch (...) | Exhaustive.java:11:13:11:13 | o |
| Exhaustive.java:11:13:11:13 | o | Exhaustive.java:12:7:12:22 | case <Pattern> |
| Exhaustive.java:12:7:12:22 | case <Pattern> | Exhaustive.java:12:19:12:19 | s |
| Exhaustive.java:12:7:12:22 | case <Pattern> | Exhaustive.java:13:7:13:23 | case <Pattern> |
| Exhaustive.java:12:19:12:19 | s | Exhaustive.java:12:24:12:26 | { ... } |
| Exhaustive.java:12:24:12:26 | { ... } | Exhaustive.java:18:5:18:14 | switch (...) |
| Exhaustive.java:13:7:13:23 | case <Pattern> | Exhaustive.java:13:19:13:20 | o2 |
| Exhaustive.java:13:19:13:20 | o2 | Exhaustive.java:13:25:13:27 | { ... } |
| Exhaustive.java:13:25:13:27 | { ... } | Exhaustive.java:18:5:18:14 | switch (...) |
| Exhaustive.java:18:5:18:14 | switch (...) | Exhaustive.java:18:13:18:13 | e |
| Exhaustive.java:18:13:18:13 | e | Exhaustive.java:19:7:19:15 | case ... |
| Exhaustive.java:18:13:18:13 | e | Exhaustive.java:20:7:20:15 | case ... |
| Exhaustive.java:18:13:18:13 | e | Exhaustive.java:21:7:21:15 | case ... |
| Exhaustive.java:18:13:18:13 | e | Exhaustive.java:24:5:24:14 | switch (...) |
| Exhaustive.java:19:7:19:15 | case ... | Exhaustive.java:19:17:19:19 | { ... } |
| Exhaustive.java:19:17:19:19 | { ... } | Exhaustive.java:24:5:24:14 | switch (...) |
| Exhaustive.java:20:7:20:15 | case ... | Exhaustive.java:20:17:20:19 | { ... } |
| Exhaustive.java:20:17:20:19 | { ... } | Exhaustive.java:24:5:24:14 | switch (...) |
| Exhaustive.java:21:7:21:15 | case ... | Exhaustive.java:21:17:21:19 | { ... } |
| Exhaustive.java:21:17:21:19 | { ... } | Exhaustive.java:24:5:24:14 | switch (...) |
| Exhaustive.java:24:5:24:14 | switch (...) | Exhaustive.java:24:13:24:13 | i |
| Exhaustive.java:24:13:24:13 | i | Exhaustive.java:25:7:25:17 | case <Pattern> |
| Exhaustive.java:25:7:25:17 | case <Pattern> | Exhaustive.java:25:14:25:14 | x |
| Exhaustive.java:25:7:25:17 | case <Pattern> | Exhaustive.java:26:7:26:17 | case <Pattern> |
| Exhaustive.java:25:14:25:14 | x | Exhaustive.java:25:19:25:21 | { ... } |
| Exhaustive.java:25:19:25:21 | { ... } | Exhaustive.java:8:22:8:25 | test |
| Exhaustive.java:26:7:26:17 | case <Pattern> | Exhaustive.java:26:14:26:14 | y |
| Exhaustive.java:26:14:26:14 | y | Exhaustive.java:26:19:26:21 | { ... } |
| Exhaustive.java:26:19:26:21 | { ... } | Exhaustive.java:8:22:8:25 | test |
| Test.java:1:14:1:17 | super(...) | Test.java:1:14:1:17 | Test |
| Test.java:1:14:1:17 | { ... } | Test.java:1:14:1:17 | super(...) |
| Test.java:3:41:101:3 | { ... } | Test.java:5:6:5:19 | switch (...) |

2
java/ql/test/library-tests/pattern-switch/cfg/test.ql
View File

@@ -1,5 +1,5 @@
import java
from ControlFlowNode cn
where cn.getFile().getBaseName() = "Test.java"
where cn.getFile().getBaseName() = ["Test.java", "Exhaustive.java"]
select cn, cn.getASuccessor()