@@ -224,17 +224,18 @@ signature module AstSig<LocationSig Location> {
224224
225225 /** Gets the case at the specified (zero-based) `index`. */
226226 Case getCase ( int index ) ;
227- }
228227
229- /**
230- * Gets an integer indicating the control flow order of a case within a switch.
231- * This is most often the same as the AST order, but can be different in some
232- * languages if the language allows a default case to appear before other
233- * cases.
234- *
235- * The values do not need to be contiguous; only the relative ordering matters.
236- */
237- default int getCaseControlFlowOrder ( Switch s , Case c ) { s .getCase ( result ) = c }
228+ /**
229+ * Gets the statement at the specified (zero-based) `index`, if any.
230+ *
231+ * Depending on the language, switches may have their case bodies nested
232+ * under the case nodes, which may or may not be statements themselves, or
233+ * the switches may have a flat structure where the cases are just labels
234+ * and the case bodies are sequences of statements between case statements.
235+ * This predicate accommodates the latter.
236+ */
237+ Stmt getStmt ( int index ) ;
238+ }
238239
239240 /** A case in a switch. */
240241 class Case extends AstNode {
@@ -245,19 +246,22 @@ signature module AstSig<LocationSig Location> {
245246 Expr getGuard ( ) ;
246247
247248 /**
248- * Gets the body element of this case at the specified (zero-based) `index` .
249+ * Gets the body of this case, if any .
249250 *
250- * This is either unique when the case has a single right-hand side, or it
251- * is the sequence of statements between this case and the next case.
251+ * A case can either have a body as a single child AST node given by this
252+ * predicate, or it can have an implicit body given by the sequence of
253+ * statements between this case and the next case.
252254 */
253- AstNode getBodyElement ( int index ) ;
255+ AstNode getBody ( ) ;
254256 }
255257
258+ class DefaultCase extends Case ;
259+
256260 /**
257261 * Holds if this case can fall through to the next case if it is not
258262 * otherwise prevented with a `break` or similar.
259263 */
260- default predicate fallsThrough ( Case c ) { none ( ) }
264+ default predicate fallsThrough ( Case c ) { not exists ( c . getBody ( ) ) }
261265
262266 /** A ternary conditional expression. */
263267 class ConditionalExpr extends Expr {
@@ -938,7 +942,7 @@ module Make0<LocationSig Location, AstSig<Location> Ast> {
938942 *
939943 * A match-all case can still ultimately fail to match if it has a guard.
940944 */
941- default predicate matchAll ( Case c ) { none ( ) }
945+ default predicate matchAll ( Case c ) { c instanceof DefaultCase }
942946
943947 /**
944948 * Holds if `ast` may result in an abrupt completion `c` originating at
@@ -1083,7 +1087,7 @@ module Make0<LocationSig Location, AstSig<Location> Ast> {
10831087 )
10841088 or
10851089 exists ( Switch switch |
1086- ast = switch .getCase ( _) . getBodyElement ( _) and
1090+ ast = getCaseBodyElement ( switch .getCase ( _) , _) and
10871091 n .isAfter ( switch ) and
10881092 c .getSuccessorType ( ) instanceof BreakSuccessor
10891093 |
@@ -1096,14 +1100,59 @@ module Make0<LocationSig Location, AstSig<Location> Ast> {
10961100 )
10971101 }
10981102
1103+ /**
1104+ * Gets an integer indicating the control flow order of a case within a
1105+ * switch. This is equal to the AST order, except that default cases are
1106+ * always last in control flow order, even if some languages allow them
1107+ * to appear before other cases in the AST.
1108+ */
1109+ private int getCaseControlFlowOrder ( Switch s , Case c ) {
1110+ exists ( int pos | s .getCase ( pos ) = c |
1111+ // if a default case is not last in the AST, move it last in the CFG order
1112+ if c instanceof DefaultCase and exists ( s .getCase ( pos + 1 ) )
1113+ then result = strictcount ( s .getCase ( _) )
1114+ else result = pos
1115+ )
1116+ }
1117+
10991118 private Case getRankedCaseCfgOrder ( Switch s , int rnk ) {
11001119 result = rank [ rnk ] ( Case c , int i | getCaseControlFlowOrder ( s , c ) = i | c order by i )
11011120 }
11021121
1122+ private int numberOfStmts ( Switch s ) { result = strictcount ( s .getStmt ( _) ) }
1123+
1124+ private predicate caseIndex ( Switch s , Case c , int caseIdx , int caseStmtPos ) {
1125+ c = s .getCase ( caseIdx ) and
1126+ c = s .getStmt ( caseStmtPos )
1127+ }
1128+
1129+ /**
1130+ * Gets the body element of `case` at the specified (zero-based) `index`.
1131+ *
1132+ * This is either unique when the case has a single right-hand side, or it
1133+ * is the sequence of statements between this case and the next case.
1134+ */
1135+ private AstNode getCaseBodyElement ( Case case , int index ) {
1136+ result = case .getBody ( ) and index = 0
1137+ or
1138+ not exists ( case .getBody ( ) ) and
1139+ exists ( Switch s , int caseIdx , int caseStmtPos , int nextCaseStmtPos |
1140+ caseIndex ( pragma [ only_bind_into ] ( s ) , case , caseIdx , caseStmtPos ) and
1141+ (
1142+ caseIndex ( pragma [ only_bind_into ] ( s ) , _, caseIdx + 1 , nextCaseStmtPos )
1143+ or
1144+ not exists ( s .getCase ( caseIdx + 1 ) ) and
1145+ nextCaseStmtPos = numberOfStmts ( s )
1146+ ) and
1147+ index = [ 0 .. nextCaseStmtPos - caseStmtPos - 2 ] and
1148+ result = pragma [ only_bind_into ] ( s ) .getStmt ( caseStmtPos + 1 + index )
1149+ )
1150+ }
1151+
11031152 private AstNode getFirstCaseBodyElement ( Case case ) {
1104- result = case . getBodyElement ( 0 )
1153+ result = getCaseBodyElement ( case , 0 )
11051154 or
1106- not exists ( case . getBodyElement ( 0 ) ) and
1155+ not exists ( getCaseBodyElement ( case , 0 ) ) and
11071156 exists ( Switch s , int i |
11081157 fallsThrough ( case ) and
11091158 // fall-through follows AST order, not case control flow order:
@@ -1113,10 +1162,10 @@ module Make0<LocationSig Location, AstSig<Location> Ast> {
11131162 }
11141163
11151164 private AstNode getNextCaseBodyElement ( AstNode bodyElement ) {
1116- exists ( Case case , int i | case . getBodyElement ( i ) = bodyElement |
1117- result = case . getBodyElement ( i + 1 )
1165+ exists ( Case case , int i | getCaseBodyElement ( case , i ) = bodyElement |
1166+ result = getCaseBodyElement ( case , i + 1 )
11181167 or
1119- not exists ( case . getBodyElement ( i + 1 ) ) and
1168+ not exists ( getCaseBodyElement ( case , i + 1 ) ) and
11201169 exists ( Switch s , int j |
11211170 fallsThrough ( case ) and
11221171 // fall-through follows AST order, not case control flow order:
@@ -1467,7 +1516,7 @@ module Make0<LocationSig Location, AstSig<Location> Ast> {
14671516 or
14681517 n1 .isAfter ( caseBodyElement ) and
14691518 not exists ( getNextCaseBodyElement ( caseBodyElement ) ) and
1470- n2 .isAfter ( any ( Switch s | s .getCase ( _) . getBodyElement ( _) = caseBodyElement ) )
1519+ n2 .isAfter ( any ( Switch s | getCaseBodyElement ( s .getCase ( _) , _) = caseBodyElement ) )
14711520 )
14721521 }
14731522
0 commit comments