@@ -102,6 +102,22 @@ private PatternCase getClosestPrecedingPatternCase(SwitchCase case) {
102102 case = getACaseUpToNextPattern ( result , _)
103103}
104104
105+ /**
106+ * Holds if `pred` is a control-flow predecessor of switch case `sc` that is not a
107+ * fall-through from a previous case.
108+ *
109+ * For classic switches that means flow from the selector expression; for switches
110+ * involving pattern cases it can also mean flow from a previous pattern case's type
111+ * test or guard failing and proceeding to then consider subsequent cases.
112+ */
113+ private predicate isNonFallThroughPredecessor ( SwitchCase sc , ControlFlowNode pred ) {
114+ pred .( Expr ) .getParent * ( ) = sc .getSelectorExpr ( )
115+ or
116+ pred .( Expr ) .getParent * ( ) = getClosestPrecedingPatternCase ( sc ) .getGuard ( )
117+ or
118+ pred = getClosestPrecedingPatternCase ( sc )
119+ }
120+
105121/**
106122 * A condition that can be evaluated to either true or false. This can either
107123 * be an `Expr` of boolean type that isn't a boolean literal, or a case of a
@@ -215,15 +231,8 @@ class Guard extends ExprParent {
215231 branch = true and
216232 bb2 .getFirstNode ( ) = sc .getControlFlowNode ( ) and
217233 pred = sc .getControlFlowNode ( ) .getAPredecessor ( ) and
218- // This is either the top of the switch block, or a preceding pattern case
219- // if one exists (in which case the edge might come from the case itself or its guard)
220- (
221- pred .( Expr ) .getParent * ( ) = sc .getSelectorExpr ( )
222- or
223- pred .( Expr ) .getParent * ( ) = getClosestPrecedingPatternCase ( sc ) .getGuard ( )
224- or
225- pred = getClosestPrecedingPatternCase ( sc )
226- ) and
234+ isNonFallThroughPredecessor ( sc , pred )
235+ and
227236 bb1 = pred .getBasicBlock ( )
228237 )
229238 or
@@ -264,14 +273,7 @@ private predicate switchCaseControls(SwitchCase sc, BasicBlock bb) {
264273 caseblock .bbDominates ( bb ) and
265274 // Check we can't fall through from a previous block:
266275 forall ( ControlFlowNode pred | pred = sc .getControlFlowNode ( ) .getAPredecessor ( ) |
267- // Branch straight from the switch selector:
268- pred .( Expr ) .getParent * ( ) = sc .getSelectorExpr ( )
269- or
270- // Branch from a predecessor pattern case (note pattern cases cannot ever fall through)
271- pred = sc .getSiblingCase ( _) .( PatternCase )
272- or
273- // Branch from a predecessor pattern case's guard test, which also can't be a fallthrough edge
274- pred .( Expr ) .getParent * ( ) = sc .getSiblingCase ( _) .( PatternCase ) .getGuard ( )
276+ isNonFallThroughPredecessor ( sc , pred )
275277 )
276278 )
277279}
0 commit comments