@@ -30,7 +30,7 @@ private module Cached {
3030 TFinallySplitKind ( int nestLevel ) { nestLevel = FinallySplitting:: nestLevel ( _) } or
3131 TExceptionHandlerSplitKind ( ) or
3232 TBooleanSplitKind ( BooleanSplitting:: BooleanSplitSubKind kind ) { kind .startsSplit ( _) } or
33- TLoopUnrollingSplitKind ( LoopUnrollingSplitting :: UnrollableLoopStmt loop )
33+ TLoopSplitKind ( LoopSplitting :: AnalyzableLoopStmt loop )
3434
3535 cached
3636 newtype TSplit =
@@ -43,7 +43,7 @@ private module Cached {
4343 kind .startsSplit ( _) and
4444 ( branch = true or branch = false )
4545 } or
46- TLoopUnrollingSplit ( LoopUnrollingSplitting :: UnrollableLoopStmt loop )
46+ TLoopSplit ( LoopSplitting :: AnalyzableLoopStmt loop )
4747
4848 cached
4949 newtype TSplits =
@@ -1109,7 +1109,7 @@ module BooleanSplitting {
11091109 }
11101110}
11111111
1112- module LoopUnrollingSplitting {
1112+ module LoopSplitting {
11131113 private import semmle.code.csharp.controlflow.Guards as Guards
11141114 private import PreBasicBlocks
11151115 private import PreSsa
@@ -1125,51 +1125,78 @@ module LoopUnrollingSplitting {
11251125 }
11261126
11271127 /**
1128- * A loop where the body is guaranteed to be executed at least once, and
1129- * can therefore be unrolled in the control flow graph.
1128+ * A loop where the body is guaranteed to be executed at least once, and hence
1129+ * can be unrolled in the control flow graph, or where the body is guaranteed
1130+ * to never be executed, and hence can be removed from the control flow graph.
11301131 */
1131- abstract class UnrollableLoopStmt extends LoopStmt {
1132- /** Holds if the step `pred --c--> succ` should start loop unrolling . */
1133- abstract predicate startUnroll ( ControlFlowElement pred , ControlFlowElement succ , Completion c ) ;
1132+ abstract class AnalyzableLoopStmt extends LoopStmt {
1133+ /** Holds if the step `pred --c--> succ` should start the split . */
1134+ abstract predicate start ( ControlFlowElement pred , ControlFlowElement succ , Completion c ) ;
11341135
1135- /** Holds if the step `pred --c--> succ` should stop loop unrolling . */
1136- abstract predicate stopUnroll ( ControlFlowElement pred , ControlFlowElement succ , Completion c ) ;
1136+ /** Holds if the step `pred --c--> succ` should stop the split . */
1137+ abstract predicate stop ( ControlFlowElement pred , ControlFlowElement succ , Completion c ) ;
11371138
11381139 /**
1139- * Holds if any step `pred --c--> _` should be pruned from the unrolled loop
1140- * (the loop condition evaluating to `false`).
1140+ * Holds if any step `pred --c--> _` should be pruned from the control flow graph.
11411141 */
11421142 abstract predicate pruneLoopCondition ( ControlFlowElement pred , ConditionalCompletion c ) ;
1143+
1144+ /**
1145+ * Holds if the body is guaranteed to be executed at least once. If not, the
1146+ * body is guaranteed to never be executed.
1147+ */
1148+ abstract predicate isUnroll ( ) ;
11431149 }
11441150
1145- private class UnrollableForeachStmt extends UnrollableLoopStmt , ForeachStmt {
1146- UnrollableForeachStmt ( ) {
1147- exists ( Guards:: AbstractValues:: EmptyCollectionValue v | v .isNonEmpty ( ) |
1148- emptinessGuarded ( _, this .getIterableExpr ( ) , v )
1149- or
1150- this .getIterableExpr ( ) = v .getAnExpr ( )
1151- )
1151+ private class AnalyzableForeachStmt extends AnalyzableLoopStmt , ForeachStmt {
1152+ Guards:: AbstractValues:: EmptyCollectionValue v ;
1153+
1154+ AnalyzableForeachStmt ( ) {
1155+ /*
1156+ * We use `unique` to avoid degenerate cases like
1157+ * ```csharp
1158+ * if (xs.Length == 0)
1159+ * return;
1160+ * if (xs.Length > 0)
1161+ * return;
1162+ * foreach (var x in xs)
1163+ * ....
1164+ * ```
1165+ * where the iterator expression `xs` is guarded by both an emptiness check
1166+ * and a non-emptiness check.
1167+ */
1168+
1169+ v =
1170+ unique( Guards:: AbstractValues:: EmptyCollectionValue v0 |
1171+ emptinessGuarded ( _, this .getIterableExpr ( ) , v0 )
1172+ or
1173+ this .getIterableExpr ( ) = v0 .getAnExpr ( )
1174+ |
1175+ v0
1176+ )
11521177 }
11531178
1154- override predicate startUnroll ( ControlFlowElement pred , ControlFlowElement succ , Completion c ) {
1179+ override predicate start ( ControlFlowElement pred , ControlFlowElement succ , Completion c ) {
11551180 pred = last ( this .getIterableExpr ( ) , c ) and
11561181 succ = this
11571182 }
11581183
1159- override predicate stopUnroll ( ControlFlowElement pred , ControlFlowElement succ , Completion c ) {
1184+ override predicate stop ( ControlFlowElement pred , ControlFlowElement succ , Completion c ) {
11601185 pred = this and
11611186 succ = succ ( pred , c )
11621187 }
11631188
11641189 override predicate pruneLoopCondition ( ControlFlowElement pred , ConditionalCompletion c ) {
11651190 pred = this and
1166- c . ( EmptinessCompletion ) .isEmpty ( )
1191+ c = any ( EmptinessCompletion ec | if v . isEmpty ( ) then not ec .isEmpty ( ) else ec . isEmpty ( ) )
11671192 }
1193+
1194+ override predicate isUnroll ( ) { v .isNonEmpty ( ) }
11681195 }
11691196
11701197 /**
1171- * A split for loops where the body is guaranteed to be executed at least once, and
1172- * can therefore be unrolled in the control flow graph . For example, in
1198+ * A split for loops where the body is guaranteed to be executed at least once, or
1199+ * guaranteed to never be executed . For example, in
11731200 *
11741201 * ```csharp
11751202 * void M(string[] args)
@@ -1184,21 +1211,23 @@ module LoopUnrollingSplitting {
11841211 * the `foreach` loop is guaranteed to be executed at least once, as a result of the
11851212 * `args.Length == 0` check.
11861213 */
1187- class LoopUnrollingSplitImpl extends SplitImpl , TLoopUnrollingSplit {
1188- UnrollableLoopStmt loop ;
1214+ class LoopSplitImpl extends SplitImpl , TLoopSplit {
1215+ AnalyzableLoopStmt loop ;
11891216
1190- LoopUnrollingSplitImpl ( ) { this = TLoopUnrollingSplit ( loop ) }
1217+ LoopSplitImpl ( ) { this = TLoopSplit ( loop ) }
11911218
11921219 override string toString ( ) {
1193- result = "unroll (line " + loop .getLocation ( ) .getStartLine ( ) + ")"
1220+ if loop .isUnroll ( )
1221+ then result = "unroll (line " + loop .getLocation ( ) .getStartLine ( ) + ")"
1222+ else result = "skip (line " + loop .getLocation ( ) .getStartLine ( ) + ")"
11941223 }
11951224 }
11961225
1197- private int getListOrder ( UnrollableLoopStmt loop ) {
1226+ private int getListOrder ( AnalyzableLoopStmt loop ) {
11981227 exists ( Callable c , int r | c = loop .getEnclosingCallable ( ) |
11991228 result = r + BooleanSplitting:: getNextListOrder ( ) - 1 and
12001229 loop =
1201- rank [ r ] ( UnrollableLoopStmt loop0 |
1230+ rank [ r ] ( AnalyzableLoopStmt loop0 |
12021231 loop0 .getEnclosingCallable ( ) = c
12031232 |
12041233 loop0 order by loop0 .getLocation ( ) .getStartLine ( ) , loop0 .getLocation ( ) .getStartColumn ( )
@@ -1210,21 +1239,21 @@ module LoopUnrollingSplitting {
12101239 result = max ( int i | i = getListOrder ( _) + 1 or i = BooleanSplitting:: getNextListOrder ( ) )
12111240 }
12121241
1213- private class LoopUnrollingSplitKind extends SplitKind , TLoopUnrollingSplitKind {
1214- private UnrollableLoopStmt loop ;
1242+ private class LoopSplitKind extends SplitKind , TLoopSplitKind {
1243+ private AnalyzableLoopStmt loop ;
12151244
1216- LoopUnrollingSplitKind ( ) { this = TLoopUnrollingSplitKind ( loop ) }
1245+ LoopSplitKind ( ) { this = TLoopSplitKind ( loop ) }
12171246
12181247 override int getListOrder ( ) { result = getListOrder ( loop ) }
12191248
12201249 override string toString ( ) { result = "Unroll" }
12211250 }
12221251
1223- private class LoopUnrollingSplitInternal extends SplitInternal , LoopUnrollingSplitImpl {
1224- override LoopUnrollingSplitKind getKind ( ) { result = TLoopUnrollingSplitKind ( loop ) }
1252+ private class LoopUnrollingSplitInternal extends SplitInternal , LoopSplitImpl {
1253+ override LoopSplitKind getKind ( ) { result = TLoopSplitKind ( loop ) }
12251254
12261255 override predicate hasEntry ( ControlFlowElement pred , ControlFlowElement succ , Completion c ) {
1227- loop .startUnroll ( pred , succ , c )
1256+ loop .start ( pred , succ , c )
12281257 }
12291258
12301259 override predicate hasEntry ( Callable pred , ControlFlowElement succ ) { none ( ) }
@@ -1241,7 +1270,7 @@ module LoopUnrollingSplitting {
12411270
12421271 override predicate hasExit ( ControlFlowElement pred , ControlFlowElement succ , Completion c ) {
12431272 this .appliesToPredecessor ( pred , c ) and
1244- loop .stopUnroll ( pred , succ , c )
1273+ loop .stop ( pred , succ , c )
12451274 }
12461275
12471276 override Callable hasExit ( ControlFlowElement pred , Completion c ) {
@@ -1252,7 +1281,7 @@ module LoopUnrollingSplitting {
12521281 override predicate hasSuccessor ( ControlFlowElement pred , ControlFlowElement succ , Completion c ) {
12531282 this .appliesToPredecessor ( pred , c ) and
12541283 succ = succ ( pred , c ) and
1255- not loop .stopUnroll ( pred , succ , c )
1284+ not loop .stop ( pred , succ , c )
12561285 }
12571286 }
12581287}
0 commit comments