From 2a4cb240f31c643187687407f4f1995550d18cdf Mon Sep 17 00:00:00 2001 From: Simon Friis Vindum Date: Thu, 5 Nov 2026 11:29:54 +0100 Subject: [PATCH 1/6] Unified: Add exhaustive Swift switch CFG test fixtures Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 4a9b52f8-d07b-4692-8fb9-409f0efd64f2 --- .../controlflow/basicblock-slices.expected | 20 ++++++++++++++++- .../library-tests/controlflow/cfg.expected | 11 ++++++++++ .../test/library-tests/controlflow/cfg.swift | 22 +++++++++++++++++++ 3 files changed, 52 insertions(+), 1 deletion(-) diff --git a/unified/ql/test/library-tests/controlflow/basicblock-slices.expected b/unified/ql/test/library-tests/controlflow/basicblock-slices.expected index 75209a2d826b..dad6579918c9 100644 --- a/unified/ql/test/library-tests/controlflow/basicblock-slices.expected +++ b/unified/ql/test/library-tests/controlflow/basicblock-slices.expected @@ -1,4 +1,4 @@ -| 1 | cfg.swift:1:1:613:1 | Block | 'Block -V var topLevelDecl -V topLevelDecl -> Int -> 0' | +| 1 | cfg.swift:1:1:635:1 | Block | 'Block -V var topLevelDecl -V topLevelDecl -> Int -> 0' | | 2 | cfg.swift:2:1:2:1 | 0 | '0' | | 3 | cfg.swift:3:1:3:12 | topLevelDecl | 'topLevelDecl -> 1 -^ ... + ...' | | 5 | cfg.swift:5:1:5:37 | func returnZero | 'func returnZero -V returnZero' | @@ -494,3 +494,21 @@ | 610 | cfg.swift:610:5:610:13 | var x | 'var x -V x -> N' | | 611 | cfg.swift:611:5:611:9 | print | 'print -> Argument -V x -^ print(...)' | | 612 | cfg.swift:612:5:612:5 | _ | '_ -> value -^ ... = ...' | +| 615 | cfg.swift:615:1:623:1 | func exhaustiveBoolSwitch | 'func exhaustiveBoolSwitch -V exhaustiveBoolSwitch' | +| 615 | cfg.swift:615:29:615:33 | value | 'value -> Block' | +| 616 | cfg.swift:616:3:621:3 | SwitchExpr | 'SwitchExpr -V value' | +| 617 | cfg.swift:617:5:618:14 | SwitchCase | 'SwitchCase -V true' | +| 618 | cfg.swift:618:7:618:14 | Block | 'Block -V 1 -^ ReturnExpr' | +| 619 | cfg.swift:619:5:620:14 | SwitchCase | 'SwitchCase -V false' | +| 620 | cfg.swift:620:7:620:14 | Block | 'Block -V 0 -^ ReturnExpr' | +| 622 | cfg.swift:622:11:622:11 | 1 | '1 -^ - ... -^ ReturnExpr' | +| 625 | cfg.swift:625:1:635:1 | func exhaustiveEnumSwitch | 'func exhaustiveEnumSwitch -V exhaustiveEnumSwitch' | +| 625 | cfg.swift:625:29:625:33 | value | 'value -> flag -> Block' | +| 626 | cfg.swift:626:3:633:3 | SwitchExpr | 'SwitchExpr -V value' | +| 627 | cfg.swift:627:5:628:14 | SwitchCase | 'SwitchCase -V flag -? . -^ ... .error1 -^ ConditionalPattern' | +| 628 | cfg.swift:628:7:628:14 | Block | 'Block -V 1 -^ ReturnExpr' | +| 629 | cfg.swift:629:5:630:14 | SwitchCase | 'SwitchCase -V . -^ ... .error1' | +| 630 | cfg.swift:630:7:630:14 | Block | 'Block -V 2 -^ ReturnExpr' | +| 631 | cfg.swift:631:5:632:14 | SwitchCase | 'SwitchCase -V . -^ ... .error2 -> . -^ ... .error3 -^ OrPattern' | +| 632 | cfg.swift:632:7:632:14 | Block | 'Block -V 3 -^ ReturnExpr' | +| 634 | cfg.swift:634:11:634:11 | 1 | '1 -^ - ... -^ ReturnExpr' | diff --git a/unified/ql/test/library-tests/controlflow/cfg.expected b/unified/ql/test/library-tests/controlflow/cfg.expected index a2f876ffabff..354f2806986a 100644 --- a/unified/ql/test/library-tests/controlflow/cfg.expected +++ b/unified/ql/test/library-tests/controlflow/cfg.expected @@ -150,6 +150,16 @@ bbStep | cfg.swift:597:14:597:14 | 2 | '2 : successor -> let b(+2)' | | cfg.swift:600:13:600:18 | ... < ... | '... < ... : false -> Block(+1)' | | cfg.swift:600:13:600:18 | ... < ... | '... < ... : true -> Block(+0)' | +| cfg.swift:617:10:617:13 | true | 'true : match -> Block(+1)' | +| cfg.swift:617:10:617:13 | true | 'true : no-match -> SwitchCase(+2)' | +| cfg.swift:619:10:619:14 | false | 'false : match -> Block(+1)' | +| cfg.swift:619:10:619:14 | false | 'false : no-match -> 1(+3)' | +| cfg.swift:627:10:627:27 | ConditionalPattern | 'ConditionalPattern : match -> Block(+1)' | +| cfg.swift:627:10:627:27 | ConditionalPattern | 'ConditionalPattern : no-match -> SwitchCase(+2)' | +| cfg.swift:629:10:629:16 | ... .error1 | '... .error1 : match -> Block(+1)' | +| cfg.swift:629:10:629:16 | ... .error1 | '... .error1 : no-match -> SwitchCase(+2)' | +| cfg.swift:631:10:631:25 | OrPattern | 'OrPattern : match -> Block(+1)' | +| cfg.swift:631:10:631:25 | OrPattern | 'OrPattern : no-match -> 1(+3)' | noCfg | cfg.swift:47:42:47:47 | String | | cfg.swift:53:34:53:34 | _ | @@ -172,3 +182,4 @@ noCfg nonSimple | cfg.swift:12:17:12:25 | withParam | 'withParam -? Block' | | cfg.swift:35:5:35:5 | CatchClause | 'CatchClause -V MyError -^ ... .error1 -> isZero -> Argument -V x -^ isZero(...) -? MyError -^ ... .error2 -^ ConditionalPattern -^ OrPattern' | +| cfg.swift:627:5:627:5 | SwitchCase | 'SwitchCase -V flag -? . -^ ... .error1 -^ ConditionalPattern' | diff --git a/unified/ql/test/library-tests/controlflow/cfg.swift b/unified/ql/test/library-tests/controlflow/cfg.swift index cbd54f5bdc4f..cdda55221a51 100644 --- a/unified/ql/test/library-tests/controlflow/cfg.swift +++ b/unified/ql/test/library-tests/controlflow/cfg.swift @@ -611,3 +611,25 @@ func valueGenericsFn(_ value: ValueGenericsStruct) { print(x); _ = value; } + +func exhaustiveBoolSwitch(_ value: Bool) -> Int { + switch value { + case true: // $ bbStep='true : match -> Block(+1)' bbStep='true : no-match -> SwitchCase(+2)' + return 1 + case false: // $ bbStep='false : match -> Block(+1)' bbStep='false : no-match -> 1(+3)' + return 0 + } + return -1 +} + +func exhaustiveEnumSwitch(_ value: MyError, _ flag: Bool) -> Int { + switch value { + case .error1 where flag: // $ bbStep='ConditionalPattern : match -> Block(+1)' bbStep='ConditionalPattern : no-match -> SwitchCase(+2)' nonSimple='SwitchCase -V flag -? . -^ ... .error1 -^ ConditionalPattern' + return 1 + case .error1: // $ bbStep='... .error1 : match -> Block(+1)' bbStep='... .error1 : no-match -> SwitchCase(+2)' + return 2 + case .error2, .error3: // $ bbStep='OrPattern : match -> Block(+1)' bbStep='OrPattern : no-match -> 1(+3)' + return 3 + } + return -1 +} From b1ef63872e1400300fcf7a52a80a5a3d9f294ead Mon Sep 17 00:00:00 2001 From: Simon Friis Vindum Date: Thu, 5 Nov 2026 11:31:34 +0100 Subject: [PATCH 2/6] Shared: Support exhaustive switches in the shared control-flow graph Add an `isExhaustive` input hook and treat the final case of an exhaustive switch as match-all. Default to non-exhaustive to preserve existing behavior. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 4a9b52f8-d07b-4692-8fb9-409f0efd64f2 --- .../codeql/controlflow/ControlFlowGraph.qll | 25 ++++++++++++++++--- 1 file changed, 21 insertions(+), 4 deletions(-) diff --git a/shared/controlflow/codeql/controlflow/ControlFlowGraph.qll b/shared/controlflow/codeql/controlflow/ControlFlowGraph.qll index 395ed815ca74..859cbc874b19 100644 --- a/shared/controlflow/codeql/controlflow/ControlFlowGraph.qll +++ b/shared/controlflow/codeql/controlflow/ControlFlowGraph.qll @@ -538,14 +538,19 @@ module Make0 Ast> { /** Holds if catch clause `catch` catches all exceptions. */ default predicate catchAll(CatchClause catch) { not exists(catch.getPattern()) } + /** Holds if `switch` is exhaustive, so one of its cases must match. */ + default predicate isExhaustive(Switch switch) { none() } + /** * Holds if case `c` matches all possible values, for example, if it is a - * `default` case or a match-all pattern like `Object o` or if it is the - * final case in a switch that is known to be exhaustive. + * match-all pattern like `Object o`. * * A match-all case can still ultimately fail to match if it has a guard. + * + * Default cases are handled automatically. The final case in an exhaustive + * switch should not be handled here but through `isExhaustive`. */ - default predicate matchAll(Case c) { c instanceof DefaultCase } + default predicate matchAll(Case c) { none() } } /** @@ -847,11 +852,23 @@ module Make0 Ast> { result = DenseRank2::denseRank(c, ctx.asSome(), rnk) } + private predicate matchAll(Case c) { + c instanceof DefaultCase + or + Input1::matchAll(c) + or + exists(Switch switch, int last | + Input1::isExhaustive(switch) and + switch.getCase(last) = c and + not exists(switch.getCase(last + 1)) + ) + } + private predicate constantCondition(AstNode n, ConditionalSuccessor t) { n.(BooleanLiteral).getValue() = t.(BooleanSuccessor).getValue() or exists(Case c, int i | - Input1::matchAll(c) and + matchAll(c) and c.getPattern(i) = n and not exists(c.getPattern(i + 1)) and t.(MatchingSuccessor).getValue() = true From c4bd8fd29c43584a5b0b3981eff1556b65c526ca Mon Sep 17 00:00:00 2001 From: Simon Friis Vindum Date: Thu, 5 Nov 2026 11:31:54 +0100 Subject: [PATCH 3/6] Unified: Treat Unified Swift switches as exhaustive Use the shared exhaustive-switch handling. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 4a9b52f8-d07b-4692-8fb9-409f0efd64f2 --- .../ql/lib/codeql/unified/internal/ControlFlowGraph.qll | 3 +++ .../library-tests/controlflow/basicblock-slices.expected | 2 -- unified/ql/test/library-tests/controlflow/cfg.expected | 6 ++---- unified/ql/test/library-tests/controlflow/cfg.swift | 8 ++++---- 4 files changed, 9 insertions(+), 10 deletions(-) diff --git a/unified/ql/lib/codeql/unified/internal/ControlFlowGraph.qll b/unified/ql/lib/codeql/unified/internal/ControlFlowGraph.qll index 374afa4a6c82..26a08e1df71f 100644 --- a/unified/ql/lib/codeql/unified/internal/ControlFlowGraph.qll +++ b/unified/ql/lib/codeql/unified/internal/ControlFlowGraph.qll @@ -325,6 +325,9 @@ private module Input implements InputSig1, InputSig2 { class CallableContext = Void; + // Swift switches are exhaustive. + predicate isExhaustive(Ast::Switch switch) { any() } + predicate beginAbruptCompletion( AstNode ast, PreControlFlowNode n, AbruptCompletion c, boolean always ) { diff --git a/unified/ql/test/library-tests/controlflow/basicblock-slices.expected b/unified/ql/test/library-tests/controlflow/basicblock-slices.expected index dad6579918c9..de0738748fb9 100644 --- a/unified/ql/test/library-tests/controlflow/basicblock-slices.expected +++ b/unified/ql/test/library-tests/controlflow/basicblock-slices.expected @@ -501,7 +501,6 @@ | 618 | cfg.swift:618:7:618:14 | Block | 'Block -V 1 -^ ReturnExpr' | | 619 | cfg.swift:619:5:620:14 | SwitchCase | 'SwitchCase -V false' | | 620 | cfg.swift:620:7:620:14 | Block | 'Block -V 0 -^ ReturnExpr' | -| 622 | cfg.swift:622:11:622:11 | 1 | '1 -^ - ... -^ ReturnExpr' | | 625 | cfg.swift:625:1:635:1 | func exhaustiveEnumSwitch | 'func exhaustiveEnumSwitch -V exhaustiveEnumSwitch' | | 625 | cfg.swift:625:29:625:33 | value | 'value -> flag -> Block' | | 626 | cfg.swift:626:3:633:3 | SwitchExpr | 'SwitchExpr -V value' | @@ -511,4 +510,3 @@ | 630 | cfg.swift:630:7:630:14 | Block | 'Block -V 2 -^ ReturnExpr' | | 631 | cfg.swift:631:5:632:14 | SwitchCase | 'SwitchCase -V . -^ ... .error2 -> . -^ ... .error3 -^ OrPattern' | | 632 | cfg.swift:632:7:632:14 | Block | 'Block -V 3 -^ ReturnExpr' | -| 634 | cfg.swift:634:11:634:11 | 1 | '1 -^ - ... -^ ReturnExpr' | diff --git a/unified/ql/test/library-tests/controlflow/cfg.expected b/unified/ql/test/library-tests/controlflow/cfg.expected index 354f2806986a..46994ef52c9b 100644 --- a/unified/ql/test/library-tests/controlflow/cfg.expected +++ b/unified/ql/test/library-tests/controlflow/cfg.expected @@ -152,14 +152,10 @@ bbStep | cfg.swift:600:13:600:18 | ... < ... | '... < ... : true -> Block(+0)' | | cfg.swift:617:10:617:13 | true | 'true : match -> Block(+1)' | | cfg.swift:617:10:617:13 | true | 'true : no-match -> SwitchCase(+2)' | -| cfg.swift:619:10:619:14 | false | 'false : match -> Block(+1)' | -| cfg.swift:619:10:619:14 | false | 'false : no-match -> 1(+3)' | | cfg.swift:627:10:627:27 | ConditionalPattern | 'ConditionalPattern : match -> Block(+1)' | | cfg.swift:627:10:627:27 | ConditionalPattern | 'ConditionalPattern : no-match -> SwitchCase(+2)' | | cfg.swift:629:10:629:16 | ... .error1 | '... .error1 : match -> Block(+1)' | | cfg.swift:629:10:629:16 | ... .error1 | '... .error1 : no-match -> SwitchCase(+2)' | -| cfg.swift:631:10:631:25 | OrPattern | 'OrPattern : match -> Block(+1)' | -| cfg.swift:631:10:631:25 | OrPattern | 'OrPattern : no-match -> 1(+3)' | noCfg | cfg.swift:47:42:47:47 | String | | cfg.swift:53:34:53:34 | _ | @@ -179,6 +175,8 @@ noCfg | cfg.swift:440:5:440:8 | init | | cfg.swift:506:25:506:27 | Int | | cfg.swift:564:49:564:51 | Int | +| cfg.swift:622:3:622:11 | ReturnExpr | +| cfg.swift:634:3:634:11 | ReturnExpr | nonSimple | cfg.swift:12:17:12:25 | withParam | 'withParam -? Block' | | cfg.swift:35:5:35:5 | CatchClause | 'CatchClause -V MyError -^ ... .error1 -> isZero -> Argument -V x -^ isZero(...) -? MyError -^ ... .error2 -^ ConditionalPattern -^ OrPattern' | diff --git a/unified/ql/test/library-tests/controlflow/cfg.swift b/unified/ql/test/library-tests/controlflow/cfg.swift index cdda55221a51..f00bea336a97 100644 --- a/unified/ql/test/library-tests/controlflow/cfg.swift +++ b/unified/ql/test/library-tests/controlflow/cfg.swift @@ -616,10 +616,10 @@ func exhaustiveBoolSwitch(_ value: Bool) -> Int { switch value { case true: // $ bbStep='true : match -> Block(+1)' bbStep='true : no-match -> SwitchCase(+2)' return 1 - case false: // $ bbStep='false : match -> Block(+1)' bbStep='false : no-match -> 1(+3)' + case false: return 0 } - return -1 + return -1 // $ noCfg } func exhaustiveEnumSwitch(_ value: MyError, _ flag: Bool) -> Int { @@ -628,8 +628,8 @@ func exhaustiveEnumSwitch(_ value: MyError, _ flag: Bool) -> Int { return 1 case .error1: // $ bbStep='... .error1 : match -> Block(+1)' bbStep='... .error1 : no-match -> SwitchCase(+2)' return 2 - case .error2, .error3: // $ bbStep='OrPattern : match -> Block(+1)' bbStep='OrPattern : no-match -> 1(+3)' + case .error2, .error3: return 3 } - return -1 + return -1 // $ noCfg } From f45376c7b18071fb436010d58fb60875df8ea5e5 Mon Sep 17 00:00:00 2001 From: Simon Friis Vindum Date: Thu, 5 Nov 2026 11:44:18 +0100 Subject: [PATCH 4/6] Java: Use shared exhaustive-switch handling Declare exhaustive Java switch constructs through `isExhaustive`. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 4a9b52f8-d07b-4692-8fb9-409f0efd64f2 --- .../lib/semmle/code/java/ControlFlowGraph.qll | 25 ++++++++----------- 1 file changed, 10 insertions(+), 15 deletions(-) diff --git a/java/ql/lib/semmle/code/java/ControlFlowGraph.qll b/java/ql/lib/semmle/code/java/ControlFlowGraph.qll index dce6ba6afd03..b7fb06876905 100644 --- a/java/ql/lib/semmle/code/java/ControlFlowGraph.qll +++ b/java/ql/lib/semmle/code/java/ControlFlowGraph.qll @@ -513,23 +513,18 @@ private module Input implements InputSig1, InputSig2 { ) } - /** Holds if this case matches all possible values. */ - predicate matchAll(Ast::Case c) { - c instanceof DefaultCase - or + /** Holds if this switch must be exhaustive. */ + predicate isExhaustive(Ast::Switch switch) { // Switch expressions and enhanced switch blocks (those that use pattern - // cases or match null) must be exhaustive, so the last case matches all - // remaining values. + // cases or match null) must be exhaustive. // See https://docs.oracle.com/javase/specs/jls/se21/html/jls-14.html#jls-14.11.2 - exists(Ast::Switch switch, int last | - switch instanceof SwitchExpr or - exists(switch.(SwitchStmt).getAPatternCase()) or - switch.(SwitchStmt).hasNullCase() - | - switch.getCase(last) = c and - not exists(switch.getCase(last + 1)) - ) - or + switch instanceof SwitchExpr or + exists(switch.(SwitchStmt).getAPatternCase()) or + switch.(SwitchStmt).hasNullCase() + } + + /** Holds if this case matches all possible values. */ + predicate matchAll(Ast::Case c) { c.(J::PatternCase).getAPattern().getType() instanceof TypeObject } From d383b86496d2cb53f1b50e46b501a0daf85f894e Mon Sep 17 00:00:00 2001 From: Simon Friis Vindum Date: Thu, 5 Nov 2026 11:53:05 +0100 Subject: [PATCH 5/6] C#: Use shared default-case handling for C# Keep only language-specific switch-arm match-all logic, since the shared control-flow graph now handles default cases directly. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 4a9b52f8-d07b-4692-8fb9-409f0efd64f2 --- .../ql/lib/semmle/code/csharp/controlflow/ControlFlowGraph.qll | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/csharp/ql/lib/semmle/code/csharp/controlflow/ControlFlowGraph.qll b/csharp/ql/lib/semmle/code/csharp/controlflow/ControlFlowGraph.qll index c56d3dab420c..ee877750ff08 100644 --- a/csharp/ql/lib/semmle/code/csharp/controlflow/ControlFlowGraph.qll +++ b/csharp/ql/lib/semmle/code/csharp/controlflow/ControlFlowGraph.qll @@ -135,7 +135,7 @@ private module Input implements InputSig1, InputSig2 { predicate catchAll(Ast::CatchClause catch) { catch instanceof GeneralCatchClause } - predicate matchAll(Ast::Case c) { c instanceof DefaultCase or c.(SwitchCaseExpr).matchesAll() } + predicate matchAll(Ast::Case c) { c.(SwitchCaseExpr).matchesAll() } private newtype TLabel = TLblGoto(string label) { any(GotoLabelStmt goto).getLabel() = label } or From 84594736efe8760e5603b4b5615a772b9886c515 Mon Sep 17 00:00:00 2001 From: Simon Friis Vindum Date: Thu, 5 Nov 2026 13:20:05 +0100 Subject: [PATCH 6/6] Shared: Account for default cases when handling exhaustiveness --- shared/controlflow/codeql/controlflow/ControlFlowGraph.qll | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/shared/controlflow/codeql/controlflow/ControlFlowGraph.qll b/shared/controlflow/codeql/controlflow/ControlFlowGraph.qll index 859cbc874b19..78d894c01a36 100644 --- a/shared/controlflow/codeql/controlflow/ControlFlowGraph.qll +++ b/shared/controlflow/codeql/controlflow/ControlFlowGraph.qll @@ -859,6 +859,10 @@ module Make0 Ast> { or exists(Switch switch, int last | Input1::isExhaustive(switch) and + // Default cases are always considered last in control flow order, so + // exhaustiveness does not apply to the last case if a default case + // exists. + not switch.getCase(_) instanceof DefaultCase and switch.getCase(last) = c and not exists(switch.getCase(last + 1)) )