@@ -255,8 +255,8 @@ signature module AstSig<LocationSig Location> {
255255
256256 /** A case in a switch. */
257257 class Case extends AstNode {
258- /** Gets a pattern being matched by this case. */
259- AstNode getAPattern ( ) ;
258+ /** Gets the pattern being matched by this case at the specified (zero-based) `index` . */
259+ AstNode getPattern ( int index ) ;
260260
261261 /** Gets the guard expression of this case, if any. */
262262 Expr getGuard ( ) ;
@@ -489,6 +489,18 @@ module Make0<LocationSig Location, AstSig<Location> Ast> {
489489 * need to be consecutive nor start from a specific index.
490490 */
491491 default Parameter callableGetParameter ( Callable c , CallableContext ctx , int index ) { none ( ) }
492+
493+ /** Holds if this catch clause catches all exceptions. */
494+ default predicate catchAll ( CatchClause catch ) { none ( ) }
495+
496+ /**
497+ * Holds if this case matches all possible values, for example, if it is a
498+ * `default` case or a match-all pattern like `Object o` or if it is the
499+ * final case in a switch that is known to be exhaustive.
500+ *
501+ * A match-all case can still ultimately fail to match if it has a guard.
502+ */
503+ default predicate matchAll ( Case c ) { c instanceof DefaultCase }
492504 }
493505
494506 /**
@@ -612,6 +624,8 @@ module Make0<LocationSig Location, AstSig<Location> Ast> {
612624 or
613625 n instanceof Case
614626 or
627+ n = any ( Case case ) .getPattern ( _)
628+ or
615629 exists ( n .( Parameter ) .getDefaultValue ( ) )
616630 )
617631 }
@@ -772,12 +786,25 @@ module Make0<LocationSig Location, AstSig<Location> Ast> {
772786 result = DenseRank2< ParameterCtxDenseRankInput > :: denseRank ( c , ctx .asSome ( ) , rnk )
773787 }
774788
789+ private predicate constantCondition ( AstNode n , ConditionalSuccessor t ) {
790+ n .( BooleanLiteral ) .getValue ( ) = t .( BooleanSuccessor ) .getValue ( )
791+ or
792+ exists ( Case c , int i |
793+ Input1:: matchAll ( c ) and
794+ c .getPattern ( i ) = n and
795+ not exists ( c .getPattern ( i + 1 ) ) and
796+ t .( MatchingSuccessor ) .getValue ( ) = true
797+ )
798+ }
799+
775800 cached
776801 private newtype TNode =
777802 TBeforeNode ( AstNode n ) { Input1:: cfgCachedStageRef ( ) and exists ( getEnclosingCallable ( n ) ) } or
778803 TAstNode ( AstNode n ) { postOrInOrder ( n ) and exists ( getEnclosingCallable ( n ) ) } or
779804 TAfterValueNode ( AstNode n , ConditionalSuccessor t ) {
780- inConditionalContext ( n , t .getKind ( ) ) and exists ( getEnclosingCallable ( n ) )
805+ inConditionalContext ( n , t .getKind ( ) ) and
806+ exists ( getEnclosingCallable ( n ) ) and
807+ not constantCondition ( n , t .getDual ( ) )
781808 } or
782809 TAfterNode ( AstNode n ) {
783810 exists ( getEnclosingCallable ( n ) ) and
@@ -1105,18 +1132,6 @@ module Make0<LocationSig Location, AstSig<Location> Ast> {
11051132 }
11061133
11071134 signature module InputSig2 {
1108- /** Holds if this catch clause catches all exceptions. */
1109- default predicate catchAll ( CatchClause catch ) { none ( ) }
1110-
1111- /**
1112- * Holds if this case matches all possible values, for example, if it is a
1113- * `default` case or a match-all pattern like `Object o` or if it is the
1114- * final case in a switch that is known to be exhaustive.
1115- *
1116- * A match-all case can still ultimately fail to match if it has a guard.
1117- */
1118- default predicate matchAll ( Case c ) { c instanceof DefaultCase }
1119-
11201135 /**
11211136 * Holds if `ast` may result in an abrupt completion `c` originating at
11221137 * `n`. The boolean `always` indicates whether the abrupt completion
@@ -1471,12 +1486,6 @@ module Make0<LocationSig Location, AstSig<Location> Ast> {
14711486 n2 .isBefore ( condexpr .getElse ( ) )
14721487 )
14731488 or
1474- exists ( BooleanLiteral boollit |
1475- inConditionalContext ( boollit , _) and
1476- n1 .isBefore ( boollit ) and
1477- n2 .isAfterValue ( boollit , any ( BooleanSuccessor t | t .getValue ( ) = boollit .getValue ( ) ) )
1478- )
1479- or
14801489 exists ( PatternMatchExpr pme |
14811490 n1 .isBefore ( pme ) and
14821491 n2 .isBefore ( pme .getExpr ( ) )
@@ -1662,7 +1671,7 @@ module Make0<LocationSig Location, AstSig<Location> Ast> {
16621671 exists ( MatchingSuccessor t |
16631672 n1 .isBefore ( catchclause ) and
16641673 n2 .isAfterValue ( catchclause , t ) and
1665- if Input2 :: catchAll ( catchclause ) then t .getValue ( ) = true else any ( )
1674+ if Input1 :: catchAll ( catchclause ) then t .getValue ( ) = true else any ( )
16661675 )
16671676 or
16681677 exists ( PreControlFlowNode beforeVar , PreControlFlowNode beforeCond |
@@ -1720,21 +1729,22 @@ module Make0<LocationSig Location, AstSig<Location> Ast> {
17201729 )
17211730 or
17221731 exists ( Case case |
1723- exists ( MatchingSuccessor t |
1724- n1 .isBefore ( case ) and
1725- n2 .isAfterValue ( case , t ) and
1726- if Input2:: matchAll ( case ) then t .getValue ( ) = true else any ( )
1732+ n1 .isBefore ( case ) and
1733+ (
1734+ if exists ( case .getPattern ( _) )
1735+ then n2 .isBefore ( case .getPattern ( 0 ) )
1736+ else n2 .isAfterValue ( case , any ( MatchingSuccessor t | t .getValue ( ) = true ) )
17271737 )
17281738 or
1729- exists (
1730- PreControlFlowNode beforePattern , PreControlFlowNode beforeGuard ,
1731- PreControlFlowNode beforeBody
1732- |
1733- (
1734- beforePattern . isBefore ( case . getAPattern ( ) )
1735- or
1736- not exists ( case . getAPattern ( ) ) and beforePattern = beforeGuard
1737- ) and
1739+ exists ( int i , MatchingSuccessor ms | n1 . isAfterValue ( case . getPattern ( i ) , ms ) |
1740+ ms . getValue ( ) = false and
1741+ n2 . isBefore ( case . getPattern ( i + 1 ) )
1742+ or
1743+ ( ms . getValue ( ) = true or not exists ( case . getPattern ( i + 1 ) ) ) and
1744+ n2 . isAfterValue ( case , ms )
1745+ )
1746+ or
1747+ exists ( PreControlFlowNode beforeGuard , PreControlFlowNode beforeBody |
17381748 (
17391749 beforeGuard .isBefore ( case .getGuard ( ) )
17401750 or
@@ -1748,9 +1758,6 @@ module Make0<LocationSig Location, AstSig<Location> Ast> {
17481758 )
17491759 |
17501760 n1 .isAfterValue ( case , any ( MatchingSuccessor t | t .getValue ( ) = true ) ) and
1751- n2 = beforePattern
1752- or
1753- n1 .isAfter ( case .getAPattern ( ) ) and
17541761 n2 = beforeGuard
17551762 or
17561763 n1 .isAfterTrue ( case .getGuard ( ) ) and
@@ -2225,12 +2232,6 @@ module Make0<LocationSig Location, AstSig<Location> Ast> {
22252232 t instanceof DirectSuccessor and
22262233 node .isAdditional ( any ( ForeachStmt foreach ) , loopHeaderTag ( ) )
22272234 ) and
2228- // allow for disjunctive patterns (e.g. `case "foo", "bar":`)
2229- not (
2230- t instanceof DirectSuccessor and
2231- node .isAfterValue ( any ( Case c | 2 <= strictcount ( c .getAPattern ( ) ) ) ,
2232- any ( MatchingSuccessor m | m .getValue ( ) = true ) )
2233- ) and
22342235 // allow for functions with multiple bodies
22352236 not exists ( Callable c |
22362237 successor .getAstNode ( ) = getBodyEntry ( c , _) and
0 commit comments