@@ -308,34 +308,121 @@ private class ConstructorTree extends ControlFlowTree instanceof Constructor {
308308 }
309309}
310310
311+ cached
312+ private module SwithStmtInternal {
313+ // Reorders default to be last if needed
314+ cached
315+ CaseStmt getCase ( SwitchStmt ss , int i ) {
316+ exists ( int index , int rankIndex |
317+ caseIndex ( ss , result , index ) and
318+ rankIndex = i + 1 and
319+ index = rank [ rankIndex ] ( int j , CaseStmt cs | caseIndex ( ss , cs , j ) | j )
320+ )
321+ }
322+
323+ /** Implicitly reorder case statements to put the default case last if needed. */
324+ private predicate caseIndex ( SwitchStmt ss , CaseStmt case , int index ) {
325+ exists ( int i | case = ss .getChildStmt ( i ) |
326+ if case instanceof DefaultCase
327+ then index = max ( int j | exists ( ss .getChildStmt ( j ) ) ) + 1
328+ else index = i
329+ )
330+ }
331+
332+ /**
333+ * Gets the `i`th statement in the body of this `switch` statement.
334+ *
335+ * Example:
336+ *
337+ * ```csharp
338+ * switch (x) {
339+ * case "abc": // i = 0
340+ * return 0;
341+ * case int i when i > 0: // i = 1
342+ * return 1;
343+ * case string s: // i = 2
344+ * Console.WriteLine(s);
345+ * return 2; // i = 3
346+ * default: // i = 4
347+ * return 3; // i = 5
348+ * }
349+ * ```
350+ *
351+ * Note that each non-`default` case is a labeled statement, so the statement
352+ * that follows is a child of the labeled statement, and not the `switch` block.
353+ */
354+ cached
355+ Stmt getStmt ( SwitchStmt ss , int i ) {
356+ exists ( int index , int rankIndex |
357+ result = ss .getChildStmt ( index ) and
358+ rankIndex = i + 1 and
359+ index =
360+ rank [ rankIndex ] ( int j , Stmt s |
361+ // `getChild` includes both labeled statements and the targeted
362+ // statements of labeled statement as separate children, but we
363+ // only want the labeled statement
364+ s = getLabeledStmt ( ss , j )
365+ |
366+ j
367+ )
368+ )
369+ }
370+
371+ private Stmt getLabeledStmt ( SwitchStmt ss , int i ) {
372+ result = ss .getChildStmt ( i ) and
373+ not result = caseStmtGetBody ( _)
374+ }
375+ }
376+
377+ private ControlFlowElement caseGetBody ( Case c ) {
378+ result = c .getBody ( ) or result = caseStmtGetBody ( c )
379+ }
380+
381+ private ControlFlowElement caseStmtGetBody ( CaseStmt c ) {
382+ exists ( int i , Stmt next |
383+ c = c .getParent ( ) .getChild ( i ) and
384+ next = c .getParent ( ) .getChild ( i + 1 )
385+ |
386+ result = next and
387+ not result instanceof CaseStmt
388+ or
389+ result = caseStmtGetBody ( next )
390+ )
391+ }
392+
393+ // Reorders default to be last if needed
394+ private Case switchGetCase ( Switch s , int i ) {
395+ result = s .( SwitchExpr ) .getCase ( i ) or result = SwithStmtInternal:: getCase ( s , i )
396+ }
397+
311398abstract private class SwitchTree extends ControlFlowTree instanceof Switch {
312399 override predicate propagatesAbnormal ( AstNode child ) { child = super .getExpr ( ) }
313400
314401 override predicate succ ( AstNode pred , AstNode succ , Completion c ) {
315402 // Flow from last element of switch expression to first element of first case
316403 last ( super .getExpr ( ) , pred , c ) and
317404 c instanceof NormalCompletion and
318- first ( super . getCase ( 0 ) , succ )
405+ first ( switchGetCase ( this , 0 ) , succ )
319406 or
320407 // Flow from last element of case pattern to next case
321- exists ( Case case , int i | case = super . getCase ( i ) |
408+ exists ( Case case , int i | case = switchGetCase ( this , i ) |
322409 last ( case .getPattern ( ) , pred , c ) and
323410 c .( MatchingCompletion ) .isNonMatch ( ) and
324- first ( super . getCase ( i + 1 ) , succ )
411+ first ( switchGetCase ( this , i + 1 ) , succ )
325412 )
326413 or
327414 // Flow from last element of condition to next case
328- exists ( Case case , int i | case = super . getCase ( i ) |
415+ exists ( Case case , int i | case = switchGetCase ( this , i ) |
329416 last ( case .getCondition ( ) , pred , c ) and
330417 c instanceof FalseCompletion and
331- first ( super . getCase ( i + 1 ) , succ )
418+ first ( switchGetCase ( this , i + 1 ) , succ )
332419 )
333420 }
334421}
335422
336423abstract private class CaseTree extends ControlFlowTree instanceof Case {
337424 final override predicate propagatesAbnormal ( AstNode child ) {
338- child in [ super .getPattern ( ) .( ControlFlowElement ) , super .getCondition ( ) , super . getBody ( ) ]
425+ child in [ super .getPattern ( ) .( ControlFlowElement ) , super .getCondition ( ) , caseGetBody ( this ) ]
339426 }
340427
341428 override predicate succ ( AstNode pred , AstNode succ , Completion c ) {
@@ -348,13 +435,13 @@ abstract private class CaseTree extends ControlFlowTree instanceof Case {
348435 first ( super .getCondition ( ) , succ )
349436 else
350437 // Flow from last element of pattern to first element of body
351- first ( super . getBody ( ) , succ )
438+ first ( caseGetBody ( this ) , succ )
352439 )
353440 or
354441 // Flow from last element of condition to first element of body
355442 last ( super .getCondition ( ) , pred , c ) and
356443 c instanceof TrueCompletion and
357- first ( super . getBody ( ) , succ )
444+ first ( caseGetBody ( this ) , succ )
358445 }
359446}
360447
@@ -1226,10 +1313,11 @@ module Statements {
12261313 c instanceof NormalCompletion
12271314 or
12281315 // A statement exits with a `break` completion
1229- last ( super .getStmt ( _) , last , c .( NestedBreakCompletion ) .getAnInnerCompatibleCompletion ( ) )
1316+ last ( SwithStmtInternal:: getStmt ( this , _) , last ,
1317+ c .( NestedBreakCompletion ) .getAnInnerCompatibleCompletion ( ) )
12301318 or
12311319 // A statement exits abnormally
1232- last ( super . getStmt ( _) , last , c ) and
1320+ last ( SwithStmtInternal :: getStmt ( this , _) , last , c ) and
12331321 not c instanceof BreakCompletion and
12341322 not c instanceof NormalCompletion and
12351323 not any ( LabeledStmtTree t |
@@ -1238,8 +1326,8 @@ module Statements {
12381326 or
12391327 // Last case exits with a non-match
12401328 exists ( CaseStmt cs , int last_ |
1241- last_ = max ( int i | exists ( super . getCase ( i ) ) ) and
1242- cs = super . getCase ( last_ )
1329+ last_ = max ( int i | exists ( SwithStmtInternal :: getCase ( this , i ) ) ) and
1330+ cs = SwithStmtInternal :: getCase ( this , last_ )
12431331 |
12441332 last ( cs .getPattern ( ) , last , c ) and
12451333 not c .( MatchingCompletion ) .isMatch ( )
@@ -1258,22 +1346,22 @@ module Statements {
12581346 c instanceof SimpleCompletion
12591347 or
12601348 // Flow from last element of non-`case` statement `i` to first element of statement `i+1`
1261- exists ( int i | last ( super . getStmt ( i ) , pred , c ) |
1262- not super . getStmt ( i ) instanceof CaseStmt and
1349+ exists ( int i | last ( SwithStmtInternal :: getStmt ( this , i ) , pred , c ) |
1350+ not SwithStmtInternal :: getStmt ( this , i ) instanceof CaseStmt and
12631351 c instanceof NormalCompletion and
1264- first ( super . getStmt ( i + 1 ) , succ )
1352+ first ( SwithStmtInternal :: getStmt ( this , i + 1 ) , succ )
12651353 )
12661354 or
12671355 // Flow from last element of `case` statement `i` to first element of statement `i+1`
12681356 exists ( int i , Stmt body |
1269- body = super . getStmt ( i ) . ( CaseStmt ) . getBody ( ) and
1357+ body = caseStmtGetBody ( SwithStmtInternal :: getStmt ( this , i ) ) and
12701358 // in case of fall-through cases, make sure to not jump from their shared body back
12711359 // to one of the fall-through cases
1272- not body = super . getStmt ( i + 1 ) . ( CaseStmt ) . getBody ( ) and
1360+ not body = caseStmtGetBody ( SwithStmtInternal :: getStmt ( this , i + 1 ) ) and
12731361 last ( body , pred , c )
12741362 |
12751363 c instanceof NormalCompletion and
1276- first ( super . getStmt ( i + 1 ) , succ )
1364+ first ( SwithStmtInternal :: getStmt ( this , i + 1 ) , succ )
12771365 )
12781366 }
12791367 }
@@ -1289,7 +1377,7 @@ module Statements {
12891377 not c .( MatchingCompletion ) .isMatch ( )
12901378 or
12911379 // Case body exits with any completion
1292- last ( super . getBody ( ) , last , c )
1380+ last ( caseStmtGetBody ( this ) , last , c )
12931381 }
12941382
12951383 final override predicate succ ( AstNode pred , AstNode succ , Completion c ) {
0 commit comments