Skip to content

Commit 42cb870

Browse files
paldepindpaldepind
authored
Merge pull request #23026 from github/unified/match-all
Share: Handle exhaustive `switch`es in the shared CFG library
2 parents fd83822 + 8459473 commit 42cb870

7 files changed

Lines changed: 87 additions & 21 deletions

File tree

‎csharp/ql/lib/semmle/code/csharp/controlflow/ControlFlowGraph.qll‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -135,7 +135,7 @@ private module Input implements InputSig1, InputSig2 {
135135

136136
predicate catchAll(Ast::CatchClause catch) { catch instanceof GeneralCatchClause }
137137

138-
predicate matchAll(Ast::Case c) { c instanceof DefaultCase or c.(SwitchCaseExpr).matchesAll() }
138+
predicate matchAll(Ast::Case c) { c.(SwitchCaseExpr).matchesAll() }
139139

140140
private newtype TLabel =
141141
TLblGoto(string label) { any(GotoLabelStmt goto).getLabel() = label } or

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

Lines changed: 10 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -513,23 +513,18 @@ private module Input implements InputSig1, InputSig2 {
513513
)
514514
}
515515

516-
/** Holds if this case matches all possible values. */
517-
predicate matchAll(Ast::Case c) {
518-
c instanceof DefaultCase
519-
or
516+
/** Holds if this switch must be exhaustive. */
517+
predicate isExhaustive(Ast::Switch switch) {
520518
// Switch expressions and enhanced switch blocks (those that use pattern
521-
// cases or match null) must be exhaustive, so the last case matches all
522-
// remaining values.
519+
// cases or match null) must be exhaustive.
523520
// See https://docs.oracle.com/javase/specs/jls/se21/html/jls-14.html#jls-14.11.2
524-
exists(Ast::Switch switch, int last |
525-
switch instanceof SwitchExpr or
526-
exists(switch.(SwitchStmt).getAPatternCase()) or
527-
switch.(SwitchStmt).hasNullCase()
528-
|
529-
switch.getCase(last) = c and
530-
not exists(switch.getCase(last + 1))
531-
)
532-
or
521+
switch instanceof SwitchExpr or
522+
exists(switch.(SwitchStmt).getAPatternCase()) or
523+
switch.(SwitchStmt).hasNullCase()
524+
}
525+
526+
/** Holds if this case matches all possible values. */
527+
predicate matchAll(Ast::Case c) {
533528
c.(J::PatternCase).getAPattern().getType() instanceof TypeObject
534529
}
535530

‎shared/controlflow/codeql/controlflow/ControlFlowGraph.qll‎

Lines changed: 25 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -538,14 +538,19 @@ module Make0<LocationSig Location, AstSig<Location> Ast> {
538538
/** Holds if catch clause `catch` catches all exceptions. */
539539
default predicate catchAll(CatchClause catch) { not exists(catch.getPattern()) }
540540

541+
/** Holds if `switch` is exhaustive, so one of its cases must match. */
542+
default predicate isExhaustive(Switch switch) { none() }
543+
541544
/**
542545
* Holds if case `c` matches all possible values, for example, if it is a
543-
* `default` case or a match-all pattern like `Object o` or if it is the
544-
* final case in a switch that is known to be exhaustive.
546+
* match-all pattern like `Object o`.
545547
*
546548
* A match-all case can still ultimately fail to match if it has a guard.
549+
*
550+
* Default cases are handled automatically. The final case in an exhaustive
551+
* switch should not be handled here but through `isExhaustive`.
547552
*/
548-
default predicate matchAll(Case c) { c instanceof DefaultCase }
553+
default predicate matchAll(Case c) { none() }
549554
}
550555

551556
/**
@@ -847,11 +852,27 @@ module Make0<LocationSig Location, AstSig<Location> Ast> {
847852
result = DenseRank2<ParameterCtxDenseRankInput>::denseRank(c, ctx.asSome(), rnk)
848853
}
849854

855+
private predicate matchAll(Case c) {
856+
c instanceof DefaultCase
857+
or
858+
Input1::matchAll(c)
859+
or
860+
exists(Switch switch, int last |
861+
Input1::isExhaustive(switch) and
862+
// Default cases are always considered last in control flow order, so
863+
// exhaustiveness does not apply to the last case if a default case
864+
// exists.
865+
not switch.getCase(_) instanceof DefaultCase and
866+
switch.getCase(last) = c and
867+
not exists(switch.getCase(last + 1))
868+
)
869+
}
870+
850871
private predicate constantCondition(AstNode n, ConditionalSuccessor t) {
851872
n.(BooleanLiteral).getValue() = t.(BooleanSuccessor).getValue()
852873
or
853874
exists(Case c, int i |
854-
Input1::matchAll(c) and
875+
matchAll(c) and
855876
c.getPattern(i) = n and
856877
not exists(c.getPattern(i + 1)) and
857878
t.(MatchingSuccessor).getValue() = true

‎unified/ql/lib/codeql/unified/internal/ControlFlowGraph.qll‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -325,6 +325,9 @@ private module Input implements InputSig1, InputSig2 {
325325

326326
class CallableContext = Void;
327327

328+
// Swift switches are exhaustive.
329+
predicate isExhaustive(Ast::Switch switch) { any() }
330+
328331
predicate beginAbruptCompletion(
329332
AstNode ast, PreControlFlowNode n, AbruptCompletion c, boolean always
330333
) {

‎unified/ql/test/library-tests/controlflow/basicblock-slices.expected‎

Lines changed: 17 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
| 1 | cfg.swift:1:1:613:1 | Block | 'Block -V var topLevelDecl -V topLevelDecl -> Int -> 0' |
1+
| 1 | cfg.swift:1:1:635:1 | Block | 'Block -V var topLevelDecl -V topLevelDecl -> Int -> 0' |
22
| 2 | cfg.swift:2:1:2:1 | 0 | '0' |
33
| 3 | cfg.swift:3:1:3:12 | topLevelDecl | 'topLevelDecl -> 1 -^ ... + ...' |
44
| 5 | cfg.swift:5:1:5:37 | func returnZero | 'func returnZero -V returnZero' |
@@ -494,3 +494,19 @@
494494
| 610 | cfg.swift:610:5:610:13 | var x | 'var x -V x -> N' |
495495
| 611 | cfg.swift:611:5:611:9 | print | 'print -> Argument -V x -^ print(...)' |
496496
| 612 | cfg.swift:612:5:612:5 | _ | '_ -> value -^ ... = ...' |
497+
| 615 | cfg.swift:615:1:623:1 | func exhaustiveBoolSwitch | 'func exhaustiveBoolSwitch -V exhaustiveBoolSwitch' |
498+
| 615 | cfg.swift:615:29:615:33 | value | 'value -> Block' |
499+
| 616 | cfg.swift:616:3:621:3 | SwitchExpr | 'SwitchExpr -V value' |
500+
| 617 | cfg.swift:617:5:618:14 | SwitchCase | 'SwitchCase -V true' |
501+
| 618 | cfg.swift:618:7:618:14 | Block | 'Block -V 1 -^ ReturnExpr' |
502+
| 619 | cfg.swift:619:5:620:14 | SwitchCase | 'SwitchCase -V false' |
503+
| 620 | cfg.swift:620:7:620:14 | Block | 'Block -V 0 -^ ReturnExpr' |
504+
| 625 | cfg.swift:625:1:635:1 | func exhaustiveEnumSwitch | 'func exhaustiveEnumSwitch -V exhaustiveEnumSwitch' |
505+
| 625 | cfg.swift:625:29:625:33 | value | 'value -> flag -> Block' |
506+
| 626 | cfg.swift:626:3:633:3 | SwitchExpr | 'SwitchExpr -V value' |
507+
| 627 | cfg.swift:627:5:628:14 | SwitchCase | 'SwitchCase -V flag -? . -^ ... .error1 -^ ConditionalPattern' |
508+
| 628 | cfg.swift:628:7:628:14 | Block | 'Block -V 1 -^ ReturnExpr' |
509+
| 629 | cfg.swift:629:5:630:14 | SwitchCase | 'SwitchCase -V . -^ ... .error1' |
510+
| 630 | cfg.swift:630:7:630:14 | Block | 'Block -V 2 -^ ReturnExpr' |
511+
| 631 | cfg.swift:631:5:632:14 | SwitchCase | 'SwitchCase -V . -^ ... .error2 -> . -^ ... .error3 -^ OrPattern' |
512+
| 632 | cfg.swift:632:7:632:14 | Block | 'Block -V 3 -^ ReturnExpr' |

‎unified/ql/test/library-tests/controlflow/cfg.expected‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -150,6 +150,12 @@ bbStep
150150
| cfg.swift:597:14:597:14 | 2 | '2 : successor -> let b(+2)' |
151151
| cfg.swift:600:13:600:18 | ... < ... | '... < ... : false -> Block(+1)' |
152152
| cfg.swift:600:13:600:18 | ... < ... | '... < ... : true -> Block(+0)' |
153+
| cfg.swift:617:10:617:13 | true | 'true : match -> Block(+1)' |
154+
| cfg.swift:617:10:617:13 | true | 'true : no-match -> SwitchCase(+2)' |
155+
| cfg.swift:627:10:627:27 | ConditionalPattern | 'ConditionalPattern : match -> Block(+1)' |
156+
| cfg.swift:627:10:627:27 | ConditionalPattern | 'ConditionalPattern : no-match -> SwitchCase(+2)' |
157+
| cfg.swift:629:10:629:16 | ... .error1 | '... .error1 : match -> Block(+1)' |
158+
| cfg.swift:629:10:629:16 | ... .error1 | '... .error1 : no-match -> SwitchCase(+2)' |
153159
noCfg
154160
| cfg.swift:47:42:47:47 | String |
155161
| cfg.swift:53:34:53:34 | _ |
@@ -169,6 +175,9 @@ noCfg
169175
| cfg.swift:440:5:440:8 | init |
170176
| cfg.swift:506:25:506:27 | Int |
171177
| cfg.swift:564:49:564:51 | Int |
178+
| cfg.swift:622:3:622:11 | ReturnExpr |
179+
| cfg.swift:634:3:634:11 | ReturnExpr |
172180
nonSimple
173181
| cfg.swift:12:17:12:25 | withParam | 'withParam -? Block' |
174182
| cfg.swift:35:5:35:5 | CatchClause | 'CatchClause -V MyError -^ ... .error1 -> isZero -> Argument -V x -^ isZero(...) -? MyError -^ ... .error2 -^ ConditionalPattern -^ OrPattern' |
183+
| cfg.swift:627:5:627:5 | SwitchCase | 'SwitchCase -V flag -? . -^ ... .error1 -^ ConditionalPattern' |

‎unified/ql/test/library-tests/controlflow/cfg.swift‎

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -611,3 +611,25 @@ func valueGenericsFn<let N: Int>(_ value: ValueGenericsStruct<N>) {
611611
print(x);
612612
_ = value;
613613
}
614+
615+
func exhaustiveBoolSwitch(_ value: Bool) -> Int {
616+
switch value {
617+
case true: // $ bbStep='true : match -> Block(+1)' bbStep='true : no-match -> SwitchCase(+2)'
618+
return 1
619+
case false:
620+
return 0
621+
}
622+
return -1 // $ noCfg
623+
}
624+
625+
func exhaustiveEnumSwitch(_ value: MyError, _ flag: Bool) -> Int {
626+
switch value {
627+
case .error1 where flag: // $ bbStep='ConditionalPattern : match -> Block(+1)' bbStep='ConditionalPattern : no-match -> SwitchCase(+2)' nonSimple='SwitchCase -V flag -? . -^ ... .error1 -^ ConditionalPattern'
628+
return 1
629+
case .error1: // $ bbStep='... .error1 : match -> Block(+1)' bbStep='... .error1 : no-match -> SwitchCase(+2)'
630+
return 2
631+
case .error2, .error3:
632+
return 3
633+
}
634+
return -1 // $ noCfg
635+
}

0 commit comments

Comments
 (0)