Share: Handle exhaustive switches in the shared CFG library

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

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
   }
 

shared/controlflow/codeql/controlflow/ControlFlowGraph.qll

@@ -538,14 +538,19 @@ module Make0<LocationSig Location, AstSig<Location> 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,27 @@ module Make0<LocationSig Location, AstSig<Location> Ast> {
       result = DenseRank2<ParameterCtxDenseRankInput>::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
+        // 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))
+      )
+    }
+
     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

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
   ) {

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,19 @@
 | 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' |
+| 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' |

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

@@ -150,6 +150,12 @@ 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: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)' |
 noCfg
 | cfg.swift:47:42:47:47 | String |
 | cfg.swift:53:34:53:34 | _ |
@@ -169,6 +175,9 @@ 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' |
+| cfg.swift:627:5:627:5 | SwitchCase | 'SwitchCase -V flag -? . -^ ... .error1 -^ ConditionalPattern' |

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

@@ -611,3 +611,25 @@ func valueGenericsFn<let N: Int>(_ value: ValueGenericsStruct<N>) {
     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:
+      return 0
+  }
+  return -1 // $ noCfg
+}
+
+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:
+      return 3
+  }
+  return -1 // $ noCfg
+}