@@ -13,6 +13,9 @@ private import semmle.code.csharp.controlflow.Guards as Guards
1313private import ControlFlow
1414private import SuccessorTypes
1515
16+ /** The maximum number of splits allowed for a given node. */
17+ private int maxSplits ( ) { result = 7 }
18+
1619cached
1720private module Cached {
1821 cached
@@ -41,11 +44,13 @@ private module Cached {
4144 TSplitsNil ( ) or
4245 TSplitsCons ( SplitInternal head , Splits tail ) {
4346 exists (
44- ControlFlowElement pred , Splits predSplits , ControlFlowElement succ , Completion c , int rnk
45- |
46- case2aFromRank ( pred , predSplits , succ , tail , c , rnk + 1 )
47+ ControlFlowElement pred , Splits predSplits , ControlFlowElement succ , Completion c , int rnk ,
48+ int numberOfSplits
4749 |
50+ case2aFromRank ( pred , predSplits , succ , tail , c , rnk + 1 , numberOfSplits ) and
4851 head = case2aSomeAtRank ( pred , predSplits , succ , c , rnk )
52+ |
53+ numberOfSplits < maxSplits ( ) or head .getKind ( ) .isMandatory ( )
4954 )
5055 }
5156
@@ -93,6 +98,13 @@ abstract class SplitKind extends TSplitKind {
9398 */
9499 abstract int getListOrder ( ) ;
95100
101+ /**
102+ * Holds if a split of this kind is mandatory. That is, a split of this kind must
103+ * be taken into account, regardless of whether we might exceed the maximum number
104+ * of splits (`maxSplits()`).
105+ */
106+ abstract predicate isMandatory ( ) ;
107+
96108 /**
97109 * Gets the rank of this split kind among all the split kinds that apply to
98110 * control flow element `cfe`. The rank is based on the order defined by
@@ -264,6 +276,8 @@ module FinallySplitting {
264276 private class FinallySplitKind extends SplitKind , TFinallySplitKind {
265277 override int getListOrder ( ) { result = 0 }
266278
279+ override predicate isMandatory ( ) { any ( ) }
280+
267281 override string toString ( ) { result = "Finally" }
268282 }
269283
@@ -415,6 +429,8 @@ module ExceptionHandlerSplitting {
415429 private class ExceptionHandlerSplitKind extends SplitKind , TExceptionHandlerSplitKind {
416430 override int getListOrder ( ) { result = 1 }
417431
432+ override predicate isMandatory ( ) { any ( ) }
433+
418434 override string toString ( ) { result = "ExceptionHandler" }
419435 }
420436
@@ -711,6 +727,8 @@ module BooleanSplitting {
711727 )
712728 }
713729
730+ override predicate isMandatory ( ) { none ( ) }
731+
714732 override string toString ( ) { result = kind .toString ( ) }
715733 }
716734
@@ -961,19 +979,28 @@ private module SuccSplits {
961979 )
962980 }
963981
982+ pragma [ nomagic]
983+ private predicate entryOfKind (
984+ ControlFlowElement pred , ControlFlowElement succ , Completion c , SplitInternal split ,
985+ SplitKind sk
986+ ) {
987+ split .hasEntry ( pred , succ , c ) and
988+ sk = split .getKind ( )
989+ }
990+
964991 /** Holds if `succSplits` should not have a split of kind `sk`. */
965- pragma [ noinline ]
992+ pragma [ nomagic ]
966993 private predicate case2aNoneOfKind (
967994 ControlFlowElement pred , Splits predSplits , ControlFlowElement succ , Completion c , SplitKind sk
968995 ) {
969996 // None inherited from predecessor
970997 case2aNoneInheritedOfKindForall ( pred , predSplits , succ , c , sk , TSplitsNil ( ) ) and
971998 // None newly entered into
972- not exists ( SplitInternal split | split . hasEntry ( pred , succ , c ) | split . getKind ( ) = sk )
999+ not entryOfKind ( pred , succ , c , _ , sk )
9731000 }
9741001
9751002 /** Holds if `succSplits` should not have a split of kind `sk` at rank `rnk`. */
976- pragma [ noinline ]
1003+ pragma [ nomagic ]
9771004 private predicate case2aNoneAtRank (
9781005 ControlFlowElement pred , Splits predSplits , ControlFlowElement succ , Completion c , int rnk
9791006 ) {
@@ -982,27 +1009,42 @@ private module SuccSplits {
9821009 )
9831010 }
9841011
985- /** Gets a split that should be in `succSplits`. */
9861012 pragma [ nomagic]
987- private SplitInternal case2aSome (
1013+ private SplitInternal case2auxGetAPredecessorSplit (
9881014 ControlFlowElement pred , Splits predSplits , ControlFlowElement succ , Completion c
9891015 ) {
9901016 case2aux ( pred , predSplits , succ , c ) and
1017+ result = predSplits .getASplit ( )
1018+ }
1019+
1020+ /** Gets a split that should be in `succSplits`. */
1021+ pragma [ nomagic]
1022+ private SplitInternal case2aSome (
1023+ ControlFlowElement pred , Splits predSplits , ControlFlowElement succ , Completion c , SplitKind sk
1024+ ) {
9911025 (
992- result = predSplits .getASplit ( ) and
1026+ // Inherited from predecessor
1027+ result = case2auxGetAPredecessorSplit ( pred , predSplits , succ , c ) and
9931028 result .hasSuccessor ( pred , succ , c )
9941029 or
995- result .hasEntry ( pred , succ , c ) and
996- case2aNoneInheritedOfKindForall ( pred , predSplits , succ , c , result .getKind ( ) , TSplitsNil ( ) )
997- )
1030+ // Newly entered into
1031+ exists ( SplitKind sk0 |
1032+ case2aNoneInheritedOfKindForall ( pred , predSplits , succ , c , sk0 , TSplitsNil ( ) )
1033+ |
1034+ entryOfKind ( pred , succ , c , result , sk0 )
1035+ )
1036+ ) and
1037+ sk = result .getKind ( )
9981038 }
9991039
10001040 /** Gets a split that should be in `succSplits` at rank `rnk`. */
1041+ pragma [ nomagic]
10011042 SplitInternal case2aSomeAtRank (
10021043 ControlFlowElement pred , Splits predSplits , ControlFlowElement succ , Completion c , int rnk
10031044 ) {
1004- result = case2aSome ( pred , predSplits , succ , c ) and
1005- rnk = result .getKind ( ) .getListRank ( succ )
1045+ exists ( SplitKind sk | result = case2aSome ( pred , predSplits , succ , c , sk ) |
1046+ rnk = sk .getListRank ( succ )
1047+ )
10061048 }
10071049
10081050 /**
@@ -1022,28 +1064,33 @@ private module SuccSplits {
10221064 */
10231065 predicate case2aFromRank (
10241066 ControlFlowElement pred , Splits predSplits , ControlFlowElement succ , Splits succSplits ,
1025- Completion c , int rnk
1067+ Completion c , int rnk , int numberOfSplits
10261068 ) {
10271069 case2aux ( pred , predSplits , succ , c ) and
10281070 succSplits = TSplitsNil ( ) and
1029- rnk = max ( any ( SplitKind sk ) .getListRank ( succ ) ) + 1
1071+ rnk = max ( any ( SplitKind sk ) .getListRank ( succ ) ) + 1 and
1072+ numberOfSplits = 0
10301073 or
1031- case2aFromRank ( pred , predSplits , succ , succSplits , c , rnk + 1 ) and
1074+ case2aFromRank ( pred , predSplits , succ , succSplits , c , rnk + 1 , numberOfSplits ) and
10321075 case2aNoneAtRank ( pred , predSplits , succ , c , rnk )
10331076 or
1034- exists ( Splits mid , SplitInternal split |
1035- split = case2aCons ( pred , predSplits , succ , mid , c , rnk )
1077+ exists ( Splits mid , SplitInternal split , int numberOfSplitsMid |
1078+ split = case2aCons ( pred , predSplits , succ , mid , c , rnk , numberOfSplitsMid )
10361079 |
1037- succSplits = TSplitsCons ( split , mid )
1080+ if numberOfSplitsMid < maxSplits ( ) or split .getKind ( ) .isMandatory ( )
1081+ then succSplits = TSplitsCons ( split , mid ) and numberOfSplits = numberOfSplitsMid + 1
1082+ else (
1083+ succSplits = mid and numberOfSplits = numberOfSplitsMid
1084+ )
10381085 )
10391086 }
10401087
10411088 pragma [ noinline]
10421089 private SplitInternal case2aCons (
10431090 ControlFlowElement pred , Splits predSplits , ControlFlowElement succ , Splits succSplits ,
1044- Completion c , int rnk
1091+ Completion c , int rnk , int numberOfSplits
10451092 ) {
1046- case2aFromRank ( pred , predSplits , succ , succSplits , c , rnk + 1 ) and
1093+ case2aFromRank ( pred , predSplits , succ , succSplits , c , rnk + 1 , numberOfSplits ) and
10471094 result = case2aSomeAtRank ( pred , predSplits , succ , c , rnk )
10481095 }
10491096
@@ -1077,7 +1124,7 @@ private module SuccSplits {
10771124 ControlFlowElement pred , Splits predSplits , ControlFlowElement succ , Splits succSplits ,
10781125 Completion c
10791126 ) {
1080- case2aFromRank ( pred , predSplits , succ , succSplits , c , 1 )
1127+ case2aFromRank ( pred , predSplits , succ , succSplits , c , 1 , _ )
10811128 or
10821129 case2bForall ( pred , predSplits , succ , c , TSplitsNil ( ) ) and
10831130 succSplits = TSplitsNil ( )
0 commit comments