@@ -102,6 +102,22 @@ private PatternCase getClosestPrecedingPatternCase(SwitchCase case) {
102
102
case = getACaseUpToNextPattern ( result , _)
103
103
}
104
104
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
+
105
121
/**
106
122
* A condition that can be evaluated to either true or false. This can either
107
123
* 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 {
215
231
branch = true and
216
232
bb2 .getFirstNode ( ) = sc .getControlFlowNode ( ) and
217
233
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
227
236
bb1 = pred .getBasicBlock ( )
228
237
)
229
238
or
@@ -264,14 +273,7 @@ private predicate switchCaseControls(SwitchCase sc, BasicBlock bb) {
264
273
caseblock .bbDominates ( bb ) and
265
274
// Check we can't fall through from a previous block:
266
275
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 )
275
277
)
276
278
)
277
279
}
0 commit comments