@@ -29,7 +29,8 @@ private module Cached {
2929 TInitializerSplitKind ( ) or
3030 TFinallySplitKind ( ) or
3131 TExceptionHandlerSplitKind ( ) or
32- TBooleanSplitKind ( BooleanSplitting:: BooleanSplitSubKind kind ) { kind .startsSplit ( _) }
32+ TBooleanSplitKind ( BooleanSplitting:: BooleanSplitSubKind kind ) { kind .startsSplit ( _) } or
33+ TLoopUnrollingSplitKind ( LoopUnrollingSplitting:: UnrollableLoopStmt loop )
3334
3435 cached
3536 newtype TSplit =
@@ -39,7 +40,8 @@ private module Cached {
3940 TBooleanSplit ( BooleanSplitting:: BooleanSplitSubKind kind , boolean branch ) {
4041 kind .startsSplit ( _) and
4142 ( branch = true or branch = false )
42- }
43+ } or
44+ TLoopUnrollingSplit ( LoopUnrollingSplitting:: UnrollableLoopStmt loop )
4345
4446 cached
4547 newtype TSplits =
@@ -1023,6 +1025,165 @@ module BooleanSplitting {
10231025 }
10241026}
10251027
1028+ module LoopUnrollingSplitting {
1029+ private import semmle.code.csharp.controlflow.Guards as Guards
1030+ private import PreBasicBlocks
1031+ private import PreSsa
1032+
1033+ /** Holds if `ce` is guarded by a (non-)empty check, as specified by `v`. */
1034+ private predicate emptinessGuarded (
1035+ Guards:: Guard g , Guards:: CollectionExpr ce , Guards:: AbstractValues:: EmptyCollectionValue v
1036+ ) {
1037+ exists ( PreBasicBlock bb | Guards:: Internal:: preControls ( g , bb , v ) |
1038+ PreSsa:: adjacentReadPairSameVar ( g , ce ) and
1039+ bb .getAnElement ( ) = ce
1040+ )
1041+ }
1042+
1043+ /**
1044+ * A loop where the body is guaranteed to be executed at least once, and
1045+ * can therefore be unrolled in the control flow graph.
1046+ */
1047+ abstract class UnrollableLoopStmt extends LoopStmt {
1048+ /** Holds if the step `pred --c--> succ` should start loop unrolling. */
1049+ abstract predicate startUnroll ( ControlFlowElement pred , ControlFlowElement succ , Completion c ) ;
1050+
1051+ /** Holds if the step `pred --c--> succ` should stop loop unrolling. */
1052+ abstract predicate stopUnroll ( ControlFlowElement pred , ControlFlowElement succ , Completion c ) ;
1053+
1054+ /**
1055+ * Holds if any step `pred --c--> _` should be pruned from the unrolled loop
1056+ * (the loop condition evaluating to `false`).
1057+ */
1058+ abstract predicate pruneLoopCondition ( ControlFlowElement pred , ConditionalCompletion c ) ;
1059+
1060+ /** Gets a descendant that belongs to the body of this loop. */
1061+ ControlFlowElement getABodyDescendant ( ) {
1062+ result = this .getBody ( )
1063+ or
1064+ exists ( ControlFlowElement mid |
1065+ mid = this .getABodyDescendant ( ) and
1066+ result = getAChild ( mid , mid .getEnclosingCallable ( ) )
1067+ )
1068+ }
1069+ }
1070+
1071+ private class UnrollableForeachStmt extends UnrollableLoopStmt , ForeachStmt {
1072+ UnrollableForeachStmt ( ) {
1073+ exists ( Guards:: AbstractValues:: EmptyCollectionValue v | v .isNonEmpty ( ) |
1074+ emptinessGuarded ( _, this .getIterableExpr ( ) , v )
1075+ or
1076+ this .getIterableExpr ( ) = v .getAnExpr ( )
1077+ )
1078+ }
1079+
1080+ override predicate startUnroll ( ControlFlowElement pred , ControlFlowElement succ , Completion c ) {
1081+ pred = last ( this .getIterableExpr ( ) , c ) and
1082+ succ = this
1083+ }
1084+
1085+ override predicate stopUnroll ( ControlFlowElement pred , ControlFlowElement succ , Completion c ) {
1086+ pred = last ( this .getBody ( ) , c ) and
1087+ succ = succ ( pred , c ) and
1088+ not succ = this .getABodyDescendant ( )
1089+ }
1090+
1091+ override predicate pruneLoopCondition ( ControlFlowElement pred , ConditionalCompletion c ) {
1092+ pred = this and
1093+ c .( EmptinessCompletion ) .isEmpty ( )
1094+ }
1095+ }
1096+
1097+ /**
1098+ * A split for loops where the body is guaranteed to be executed at least once, and
1099+ * can therefore be unrolled in the control flow graph. For example, in
1100+ *
1101+ * ```
1102+ * void M(string[] args)
1103+ * {
1104+ * if (args.Length == 0)
1105+ * return;
1106+ * foreach (var arg in args)
1107+ * System.Console.WriteLine(args);
1108+ * }
1109+ * ```
1110+ *
1111+ * the `foreach` loop is guaranteed to be executed at least once, as a result of the
1112+ * `args.Length == 0` check.
1113+ */
1114+ class LoopUnrollingSplitImpl extends SplitImpl , TLoopUnrollingSplit {
1115+ UnrollableLoopStmt loop ;
1116+
1117+ LoopUnrollingSplitImpl ( ) { this = TLoopUnrollingSplit ( loop ) }
1118+
1119+ override string toString ( ) {
1120+ result = "unroll (line " + loop .getLocation ( ) .getStartLine ( ) + ")"
1121+ }
1122+ }
1123+
1124+ private int getListOrder ( UnrollableLoopStmt loop ) {
1125+ exists ( Callable c , int r | c = loop .getEnclosingCallable ( ) |
1126+ result = r + BooleanSplitting:: getNextListOrder ( ) - 1 and
1127+ loop = rank [ r ] ( UnrollableLoopStmt loop0 |
1128+ loop0 .getEnclosingCallable ( ) = c
1129+ |
1130+ loop0 order by loop0 .getLocation ( ) .getStartLine ( ) , loop0 .getLocation ( ) .getStartColumn ( )
1131+ )
1132+ )
1133+ }
1134+
1135+ int getNextListOrder ( ) {
1136+ result = max ( int i | i = getListOrder ( _) + 1 or i = BooleanSplitting:: getNextListOrder ( ) )
1137+ }
1138+
1139+ private class LoopUnrollingSplitKind extends SplitKind , TLoopUnrollingSplitKind {
1140+ private UnrollableLoopStmt loop ;
1141+
1142+ LoopUnrollingSplitKind ( ) { this = TLoopUnrollingSplitKind ( loop ) }
1143+
1144+ override int getListOrder ( ) { result = getListOrder ( loop ) }
1145+
1146+ override string toString ( ) { result = "Unroll" }
1147+ }
1148+
1149+ private class LoopUnrollingSplitInternal extends SplitInternal , LoopUnrollingSplitImpl {
1150+ override LoopUnrollingSplitKind getKind ( ) { result = TLoopUnrollingSplitKind ( loop ) }
1151+
1152+ override predicate hasEntry ( ControlFlowElement pred , ControlFlowElement succ , Completion c ) {
1153+ loop .startUnroll ( pred , succ , c )
1154+ }
1155+
1156+ override predicate hasEntry ( Callable pred , ControlFlowElement succ ) { none ( ) }
1157+
1158+ /**
1159+ * Holds if this split applies to control flow element `pred`, where `pred`
1160+ * is a valid predecessor.
1161+ */
1162+ private predicate appliesToPredecessor ( ControlFlowElement pred ) {
1163+ this .appliesTo ( pred ) and
1164+ ( exists ( succ ( pred , _) ) or exists ( succExit ( pred , _) ) )
1165+ }
1166+
1167+ override predicate hasExit ( ControlFlowElement pred , ControlFlowElement succ , Completion c ) {
1168+ this .appliesToPredecessor ( pred ) and
1169+ loop .stopUnroll ( pred , succ , c )
1170+ }
1171+
1172+ override Callable hasExit ( ControlFlowElement pred , Completion c ) {
1173+ this .appliesToPredecessor ( pred ) and
1174+ result = succExit ( pred , c ) and
1175+ not loop .pruneLoopCondition ( pred , c )
1176+ }
1177+
1178+ override predicate hasSuccessor ( ControlFlowElement pred , ControlFlowElement succ , Completion c ) {
1179+ this .appliesToPredecessor ( pred ) and
1180+ succ = succ ( pred , c ) and
1181+ not loop .pruneLoopCondition ( pred , c ) and
1182+ not loop .stopUnroll ( pred , succ , c )
1183+ }
1184+ }
1185+ }
1186+
10261187/**
10271188 * A set of control flow node splits. The set is represented by a list of splits,
10281189 * ordered by ascending rank.
0 commit comments