@@ -470,17 +470,17 @@ private module ControlFlowGraphImpl {
470470 private predicate isNthCaseOf ( StmtParent switch , SwitchCase c , int i ) { c .isNthCaseOf ( switch , i ) }
471471
472472 /**
473- * Gets a `SwitchCase` that may be `pred`'s direct successor.
473+ * Gets a `SwitchCase` that may be `pred`'s direct successor, where `pred` is declared in block `switch` .
474474 *
475475 * This means any switch case that comes after `pred` up to the next pattern case, if any, except for `case null`.
476476 *
477477 * Because we know the switch block contains at least one pattern, we know by https://docs.oracle.com/javase/specs/jls/se21/html/jls-14.html#jls-14.11
478478 * that any default case comes after the last pattern case.
479479 */
480- private SwitchCase getASuccessorSwitchCase ( PatternCase pred ) {
480+ private SwitchCase getASuccessorSwitchCase ( PatternCase pred , StmtParent switch ) {
481481 // Note we do include `case null, default` (as well as plain old `default`) here.
482482 not result .( ConstCase ) .getValue ( _) instanceof NullLiteral and
483- exists ( int maxCaseIndex , StmtParent switch |
483+ exists ( int maxCaseIndex |
484484 switch = pred .getParent ( ) and
485485 if exists ( getNextPatternCase ( pred ) )
486486 then maxCaseIndex = getNextPatternCase ( pred ) .getCaseIndex ( )
@@ -511,6 +511,24 @@ private module ControlFlowGraphImpl {
511511 )
512512 }
513513
514+ private Stmt getSwitchStatement ( StmtParent switch , int i ) { result .isNthChildOf ( switch , i ) }
515+
516+ /**
517+ * Holds if `last` is the last node in a pattern case `pc`'s succeeding bind-and-test operation,
518+ * immediately before either falling through to execute successor statements or execute a rule body
519+ * if present. `completion` is the completion kind of the last operation.
520+ */
521+ private predicate lastPatternCaseMatchingOp (
522+ PatternCase pc , ControlFlowNode last , Completion completion
523+ ) {
524+ last ( pc .getPattern ( ) , last , completion ) and
525+ completion = NormalCompletion ( ) and
526+ not exists ( pc .getGuard ( ) )
527+ or
528+ last ( pc .getGuard ( ) , last , completion ) and
529+ completion = BooleanCompletion ( true , _)
530+ }
531+
514532 /**
515533 * Expressions and statements with CFG edges in post-order AST traversal.
516534 *
@@ -808,7 +826,10 @@ private module ControlFlowGraphImpl {
808826 or
809827 last ( n , last , BooleanCompletion ( _, _) ) and
810828 not inBooleanContext ( n ) and
811- completion = NormalCompletion ( )
829+ completion = NormalCompletion ( ) and
830+ // PatternCase has both a boolean-true completion (guard success) and a normal one
831+ // (variable declaration completion, when no guard is present).
832+ not n instanceof PatternCase
812833 or
813834 // Logic expressions and conditional expressions are executed in AST pre-order to facilitate
814835 // proper short-circuit representation. All other expressions are executed in post-order.
@@ -957,6 +978,9 @@ private module ControlFlowGraphImpl {
957978 not completion instanceof NormalOrBooleanCompletion
958979 )
959980 or
981+ // If a case rule right-hand-side completes then the switch breaks or yields, depending
982+ // on whether this is a switch expression or statement. If it completes abruptly then the
983+ // switch completes the same way.
960984 exists ( Completion caseCompletion , SwitchCase case |
961985 case = n and
962986 (
@@ -973,18 +997,24 @@ private module ControlFlowGraphImpl {
973997 else completion = caseCompletion
974998 )
975999 or
976- // The normal last node in a non-rule pattern case is the last of its variable declaration(s),
977- // or the successful matching of its guard if it has one.
978- // Note that either rule or non-rule pattern cases can end with pattern match failure, whereupon
979- // they branch to the next candidate pattern. This is accounted for in the `succ` relation.
1000+ // A pattern case statement can complete:
1001+ // * On failure of its type test (boolean false)
1002+ // * On failure of its guard test if any (boolean false)
1003+ // * On any abrupt completion of its guard
1004+ // * On completion of its variable declarations, if it is not a rule and has no guard (normal completion)
1005+ // * On success of its guard test, if it is not a rule (boolean true)
1006+ // (the latter two cases are accounted for by lastPatternCaseMatchingOp)
9801007 exists ( PatternCase pc | n = pc |
1008+ last = pc and completion = basicBooleanCompletion ( false )
1009+ or
1010+ last ( pc .getGuard ( ) , last , completion ) and
9811011 (
982- if exists ( pc . getGuard ( ) )
983- then last ( pc . getGuard ( ) , last , BooleanCompletion ( true , _ ) )
984- else last ( pc . getPattern ( ) , last , NormalCompletion ( ) )
985- ) and
1012+ completion = BooleanCompletion ( false , _ ) or
1013+ not completion instanceof NormalOrBooleanCompletion
1014+ )
1015+ or
9861016 not pc .isRule ( ) and
987- completion = NormalCompletion ( )
1017+ lastPatternCaseMatchingOp ( pc , last , completion )
9881018 )
9891019 or
9901020 // the last statement of a synchronized statement is the last statement of its body
@@ -1296,90 +1326,66 @@ private module ControlFlowGraphImpl {
12961326 last ( cc .getVariable ( ) , n , completion ) and result = first ( cc .getBlock ( ) )
12971327 )
12981328 or
1299- // Switch statements
1300- exists ( SwitchStmt switch | completion = NormalCompletion ( ) |
1301- // From the entry point control is transferred first to the expression...
1302- n = switch and result = first ( switch .getExpr ( ) )
1303- or
1304- // ...and then to any case up to and including the first pattern case, if any.
1305- last ( switch .getExpr ( ) , n , completion ) and result = first ( getAFirstSwitchCase ( switch ) )
1329+ // Switch statements and expressions
1330+ exists ( StmtParent switch |
1331+ exists ( Expr switchExpr |
1332+ switchExpr = switch .( SwitchStmt ) .getExpr ( ) or switchExpr = switch .( SwitchExpr ) .getExpr ( )
1333+ |
1334+ // From the entry point control is transferred first to the expression...
1335+ n = switch and result = first ( switchExpr ) and completion = NormalCompletion ( )
1336+ or
1337+ // ...and then to any case up to and including the first pattern case, if any.
1338+ last ( switchExpr , n , completion ) and
1339+ result = first ( getAFirstSwitchCase ( switch ) ) and
1340+ completion = NormalCompletion ( )
1341+ )
13061342 or
13071343 // Statements within a switch body execute sequentially.
13081344 // Note this includes non-rule case statements and the successful pattern match successor
13091345 // of a non-rule pattern case statement. Rule case statements do not complete normally
1310- // (they always break or yield), and the case of pattern matching failure branching to the
1311- // next case is specially handled in the `PatternCase` logic below.
1346+ // (they always break or yield).
13121347 exists ( int i |
1313- last ( switch .getStmt ( i ) , n , completion ) and result = first ( switch .getStmt ( i + 1 ) )
1348+ last ( getSwitchStatement ( switch , i ) , n , completion ) and
1349+ result = first ( getSwitchStatement ( switch , i + 1 ) ) and
1350+ ( completion = NormalCompletion ( ) or completion = BooleanCompletion ( true , _) )
13141351 )
1315- )
1316- or
1317- // Switch expressions
1318- exists ( SwitchExpr switch | completion = NormalCompletion ( ) |
1319- // From the entry point control is transferred first to the expression...
1320- n = switch and result = first ( switch .getExpr ( ) )
13211352 or
1322- // ...and then to any case up to and including the first pattern case, if any.
1323- last ( switch .getExpr ( ) , n , completion ) and result = first ( getAFirstSwitchCase ( switch ) )
1324- or
1325- // Statements within a switch body execute sequentially.
1326- // Note this includes non-rule case statements and the successful pattern match successor
1327- // of a non-rule pattern case statement. Rule case statements do not complete normally
1328- // (they always break or yield), and the case of pattern matching failure branching to the
1329- // next case is specially handled in the `PatternCase` logic below.
1330- exists ( int i |
1331- last ( switch .getStmt ( i ) , n , completion ) and result = first ( switch .getStmt ( i + 1 ) )
1353+ // A pattern case that completes boolean false (type test or guard failure) continues to consider other cases:
1354+ exists ( PatternCase case | completion = BooleanCompletion ( false , _) |
1355+ last ( case , n , completion ) and result = getASuccessorSwitchCase ( case , switch )
13321356 )
13331357 )
13341358 or
1335- // Edge from rule SwitchCases to their body, after any variable assignment and/or guard test if applicable.
1336- // No edges in a non-rule SwitchCase - the constant expression in a ConstCase isn't included in the CFG.
1337- exists ( SwitchCase case , ControlFlowNode preBodyNode |
1338- if case instanceof PatternCase
1339- then (
1340- if exists ( case .( PatternCase ) .getGuard ( ) )
1341- then (
1342- last ( case .( PatternCase ) .getGuard ( ) , preBodyNode , completion ) and
1343- completion = basicBooleanCompletion ( true )
1344- ) else (
1345- last ( case .( PatternCase ) .getPattern ( ) , preBodyNode , completion ) and
1346- completion = NormalCompletion ( )
1347- )
1348- ) else (
1349- preBodyNode = case and completion = NormalCompletion ( )
1350- )
1351- |
1352- n = preBodyNode and result = first ( case .getRuleExpression ( ) )
1359+ // Pattern cases have internal edges:
1360+ // * Type test success -true-> variable declarations
1361+ // * Variable declarations -normal-> guard evaluation
1362+ // * Variable declarations -normal-> rule execution (when there is no guard)
1363+ // * Guard success -true-> rule execution
1364+ exists ( PatternCase pc |
1365+ n = pc and
1366+ completion = basicBooleanCompletion ( true ) and
1367+ result = first ( pc .getPattern ( ) )
13531368 or
1354- n = preBodyNode and result = first ( case .getRuleStatement ( ) )
1355- )
1356- or
1357- // A pattern case conducts a type test, then branches to the next case or the pattern assignment(s).
1358- exists ( PatternCase case |
1359- n = case and
1369+ last ( pc .getPattern ( ) , n , completion ) and
1370+ completion = NormalCompletion ( ) and
1371+ result = first ( pc .getGuard ( ) )
1372+ or
1373+ lastPatternCaseMatchingOp ( pc , n , completion ) and
13601374 (
1361- completion = basicBooleanCompletion ( false ) and
1362- result = getASuccessorSwitchCase ( case )
1375+ result = first ( pc .getRuleExpression ( ) )
13631376 or
1364- completion = basicBooleanCompletion ( true ) and
1365- result = first ( case .getPattern ( ) )
1377+ result = first ( pc .getRuleStatement ( ) )
13661378 )
13671379 )
13681380 or
1369- // A pattern case with a guard evaluates that guard after declaring its pattern variable(s),
1370- // and thereafter if the guard doesn't match will branch to the next case.
1371- // The case of a matching guard is accounted for in the case-with-rule logic above, or for
1372- // non-rule case statements in `last`.
1373- exists ( PatternCase case , Expr guard |
1374- guard = case .getGuard ( ) and
1381+ // Non-pattern cases have an internal edge leading to their rule body if any when the case matches.
1382+ exists ( SwitchCase case | n = case |
1383+ not case instanceof PatternCase and
1384+ completion = NormalCompletion ( ) and
13751385 (
1376- last ( case .getPattern ( ) , n , NormalCompletion ( ) ) and
1377- result = first ( guard ) and
1378- completion = NormalCompletion ( )
1386+ result = first ( case .getRuleExpression ( ) )
13791387 or
1380- last ( guard , n , completion ) and
1381- completion = basicBooleanCompletion ( false ) and
1382- result = getASuccessorSwitchCase ( case )
1388+ result = first ( case .getRuleStatement ( ) )
13831389 )
13841390 )
13851391 or
0 commit comments