@@ -470,17 +470,17 @@ private module ControlFlowGraphImpl {
470
470
private predicate isNthCaseOf ( StmtParent switch , SwitchCase c , int i ) { c .isNthCaseOf ( switch , i ) }
471
471
472
472
/**
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` .
474
474
*
475
475
* This means any switch case that comes after `pred` up to the next pattern case, if any, except for `case null`.
476
476
*
477
477
* 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
478
478
* that any default case comes after the last pattern case.
479
479
*/
480
- private SwitchCase getASuccessorSwitchCase ( PatternCase pred ) {
480
+ private SwitchCase getASuccessorSwitchCase ( PatternCase pred , StmtParent switch ) {
481
481
// Note we do include `case null, default` (as well as plain old `default`) here.
482
482
not result .( ConstCase ) .getValue ( _) instanceof NullLiteral and
483
- exists ( int maxCaseIndex , StmtParent switch |
483
+ exists ( int maxCaseIndex |
484
484
switch = pred .getParent ( ) and
485
485
if exists ( getNextPatternCase ( pred ) )
486
486
then maxCaseIndex = getNextPatternCase ( pred ) .getCaseIndex ( )
@@ -511,6 +511,24 @@ private module ControlFlowGraphImpl {
511
511
)
512
512
}
513
513
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
+
514
532
/**
515
533
* Expressions and statements with CFG edges in post-order AST traversal.
516
534
*
@@ -808,7 +826,10 @@ private module ControlFlowGraphImpl {
808
826
or
809
827
last ( n , last , BooleanCompletion ( _, _) ) and
810
828
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
812
833
or
813
834
// Logic expressions and conditional expressions are executed in AST pre-order to facilitate
814
835
// proper short-circuit representation. All other expressions are executed in post-order.
@@ -957,6 +978,9 @@ private module ControlFlowGraphImpl {
957
978
not completion instanceof NormalOrBooleanCompletion
958
979
)
959
980
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.
960
984
exists ( Completion caseCompletion , SwitchCase case |
961
985
case = n and
962
986
(
@@ -973,18 +997,24 @@ private module ControlFlowGraphImpl {
973
997
else completion = caseCompletion
974
998
)
975
999
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)
980
1007
exists ( PatternCase pc | n = pc |
1008
+ last = pc and completion = basicBooleanCompletion ( false )
1009
+ or
1010
+ last ( pc .getGuard ( ) , last , completion ) and
981
1011
(
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
986
1016
not pc .isRule ( ) and
987
- completion = NormalCompletion ( )
1017
+ lastPatternCaseMatchingOp ( pc , last , completion )
988
1018
)
989
1019
or
990
1020
// the last statement of a synchronized statement is the last statement of its body
@@ -1296,90 +1326,66 @@ private module ControlFlowGraphImpl {
1296
1326
last ( cc .getVariable ( ) , n , completion ) and result = first ( cc .getBlock ( ) )
1297
1327
)
1298
1328
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
+ )
1306
1342
or
1307
1343
// Statements within a switch body execute sequentially.
1308
1344
// Note this includes non-rule case statements and the successful pattern match successor
1309
1345
// 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).
1312
1347
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 , _) )
1314
1351
)
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 ( ) )
1321
1352
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 )
1332
1356
)
1333
1357
)
1334
1358
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 ( ) )
1353
1368
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
1360
1374
(
1361
- completion = basicBooleanCompletion ( false ) and
1362
- result = getASuccessorSwitchCase ( case )
1375
+ result = first ( pc .getRuleExpression ( ) )
1363
1376
or
1364
- completion = basicBooleanCompletion ( true ) and
1365
- result = first ( case .getPattern ( ) )
1377
+ result = first ( pc .getRuleStatement ( ) )
1366
1378
)
1367
1379
)
1368
1380
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
1375
1385
(
1376
- last ( case .getPattern ( ) , n , NormalCompletion ( ) ) and
1377
- result = first ( guard ) and
1378
- completion = NormalCompletion ( )
1386
+ result = first ( case .getRuleExpression ( ) )
1379
1387
or
1380
- last ( guard , n , completion ) and
1381
- completion = basicBooleanCompletion ( false ) and
1382
- result = getASuccessorSwitchCase ( case )
1388
+ result = first ( case .getRuleStatement ( ) )
1383
1389
)
1384
1390
)
1385
1391
or
0 commit comments