C#: Apply static CFG splitting limit

The predicate `maxSplits()` was previously applied dynamically to ensure that
any control flow node would keep track of at most `maxSplits()` number of splits.
However, there was no guarantee that two different copies of the same AST element
wouldn't contain different splits, so in general the number of copies for a given
AST element `e` could be on the order `$\binom{n}{k}c^k$`, where `n` is the total
number of splits that apply to `e`, `k = maxSplits()`, and `c` is a constant.

With this change, the relevant splits for `e` are instead computed statically,
meaning that the order is instead `$c^k$`.

Author: hvitved

csharp/ql/src/semmle/code/csharp/controlflow/internal/Splitting.qll

@@ -14,7 +14,7 @@ private import ControlFlow
 private import SuccessorTypes
 
 /** The maximum number of splits allowed for a given node. */
-private int maxSplits() { result = 7 }
+private int maxSplits() { result = 5 }
 
 cached
 private module Cached {
@@ -46,13 +46,10 @@ private module Cached {
     TSplitsNil() or
     TSplitsCons(SplitInternal head, Splits tail) {
       exists(
-        ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Completion c, int rnk,
-        int numberOfSplits
+        ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Completion c, int rnk
       |
-        case2aFromRank(pred, predSplits, succ, tail, c, rnk + 1, numberOfSplits) and
+        case2aFromRank(pred, predSplits, succ, tail, c, rnk + 1) and
         head = case2aSomeAtRank(pred, predSplits, succ, c, rnk)
-      |
-        numberOfSplits < maxSplits() or head.getKind().isMandatory()
       )
     }
 
@@ -86,6 +83,18 @@ class SplitImpl extends TSplit {
   string toString() { none() }
 }
 
+/**
+ * Holds if split kinds `sk1` and `sk2` may overlap. That is, they may apply
+ * to at least one common control flow element inside callable `c`.
+ */
+private predicate overlapping(Callable c, SplitKind sk1, SplitKind sk2) {
+  exists(ControlFlowElement cfe |
+    sk1.appliesTo(cfe) and
+    sk2.appliesTo(cfe) and
+    c = cfe.getEnclosingCallable()
+  )
+}
+
 /**
  * A split kind. Each control flow node can have at most one split of a
  * given kind.
@@ -103,12 +112,17 @@ abstract class SplitKind extends TSplitKind {
    */
   abstract int getListOrder();
 
+  /** Gets the rank of this split kind among all overlapping kinds for `c`. */
+  private int getRank(Callable c) {
+    this = rank[result](SplitKind sk | overlapping(c, this, sk) | sk order by sk.getListOrder())
+  }
+
   /**
-   * Holds if a split of this kind is mandatory. That is, a split of this kind must
-   * be taken into account, regardless of whether we might exceed the maximum number
-   * of splits (`maxSplits()`).
+   * Holds if this split kind should be included when constructing the control
+   * flow graph for callable `c`. For performance reasons, the number of splits
+   * is restricted by the `maxSplits()` predicate.
    */
-  abstract predicate isMandatory();
+  private predicate isEnabled(Callable c) { this.getRank(c) <= maxSplits() }
 
   /**
    * Gets the rank of this split kind among all the split kinds that apply to
@@ -117,6 +131,7 @@ abstract class SplitKind extends TSplitKind {
    */
   int getListRank(ControlFlowElement cfe) {
     this.appliesTo(cfe) and
+    this.isEnabled(cfe.getEnclosingCallable()) and
     this = rank[result](SplitKind sk | sk.appliesTo(cfe) | sk order by sk.getListOrder())
   }
 
@@ -281,8 +296,6 @@ module FinallySplitting {
   private class FinallySplitKind extends SplitKind, TFinallySplitKind {
     override int getListOrder() { result = 0 }
 
-    override predicate isMandatory() { any() }
-
     override string toString() { result = "Finally" }
   }
 
@@ -434,8 +447,6 @@ module ExceptionHandlerSplitting {
   private class ExceptionHandlerSplitKind extends SplitKind, TExceptionHandlerSplitKind {
     override int getListOrder() { result = 1 }
 
-    override predicate isMandatory() { any() }
-
     override string toString() { result = "ExceptionHandler" }
   }
 
@@ -732,8 +743,6 @@ module BooleanSplitting {
       )
     }
 
-    override predicate isMandatory() { none() }
-
     override string toString() { result = kind.toString() }
   }
 
@@ -1071,33 +1080,28 @@ private module SuccSplits {
    */
   predicate case2aFromRank(
     ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Splits succSplits,
-    Completion c, int rnk, int numberOfSplits
+    Completion c, int rnk
   ) {
     case2aux(pred, predSplits, succ, c) and
     succSplits = TSplitsNil() and
-    rnk = max(any(SplitKind sk).getListRank(succ)) + 1 and
-    numberOfSplits = 0
+    rnk = max(any(SplitKind sk).getListRank(succ)) + 1
     or
-    case2aFromRank(pred, predSplits, succ, succSplits, c, rnk + 1, numberOfSplits) and
+    case2aFromRank(pred, predSplits, succ, succSplits, c, rnk + 1) and
     case2aNoneAtRank(pred, predSplits, succ, c, rnk)
     or
-    exists(Splits mid, SplitInternal split, int numberOfSplitsMid |
-      split = case2aCons(pred, predSplits, succ, mid, c, rnk, numberOfSplitsMid)
+    exists(Splits mid, SplitInternal split |
+      split = case2aCons(pred, predSplits, succ, mid, c, rnk)
     |
-      if numberOfSplitsMid < maxSplits() or split.getKind().isMandatory()
-      then succSplits = TSplitsCons(split, mid) and numberOfSplits = numberOfSplitsMid + 1
-      else (
-        succSplits = mid and numberOfSplits = numberOfSplitsMid
-      )
+      succSplits = TSplitsCons(split, mid)
     )
   }
 
   pragma[noinline]
   private SplitInternal case2aCons(
     ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Splits succSplits,
-    Completion c, int rnk, int numberOfSplits
+    Completion c, int rnk
   ) {
-    case2aFromRank(pred, predSplits, succ, succSplits, c, rnk + 1, numberOfSplits) and
+    case2aFromRank(pred, predSplits, succ, succSplits, c, rnk + 1) and
     result = case2aSomeAtRank(pred, predSplits, succ, c, rnk)
   }
 
@@ -1131,7 +1135,7 @@ private module SuccSplits {
     ControlFlowElement pred, Splits predSplits, ControlFlowElement succ, Splits succSplits,
     Completion c
   ) {
-    case2aFromRank(pred, predSplits, succ, succSplits, c, 1, _)
+    case2aFromRank(pred, predSplits, succ, succSplits, c, 1)
     or
     case2bForall(pred, predSplits, succ, c, TSplitsNil()) and
     succSplits = TSplitsNil()

csharp/ql/test/library-tests/controlflow/splits/SplittingStressTest.cs

@@ -1,6 +1,6 @@
 class SplittingStressTest
 {
-    void M(bool b1, bool b2, bool b3, bool b4, bool b5, bool b6, bool b7, bool b8, bool b9, bool b10, bool b11, bool b12, bool b13, bool b14, bool b15, bool b16, bool b17, bool b18, bool b19, bool b20, bool b21, bool b22, bool b23, bool b24, bool b25, bool b26, bool b27, bool b28, bool b29, bool b30, bool b31, bool b32, bool b33, bool b34, bool b35, bool b36, bool b37, bool b38, bool b39, bool b40)
+    void M1(bool b1, bool b2, bool b3, bool b4, bool b5, bool b6, bool b7, bool b8, bool b9, bool b10, bool b11, bool b12, bool b13, bool b14, bool b15, bool b16, bool b17, bool b18, bool b19, bool b20, bool b21, bool b22, bool b23, bool b24, bool b25, bool b26, bool b27, bool b28, bool b29, bool b30, bool b31, bool b32, bool b33, bool b34, bool b35, bool b36, bool b37, bool b38, bool b39, bool b40)
     {
         if (b1)
             ;
@@ -166,4 +166,156 @@ void M(bool b1, bool b2, bool b3, bool b4, bool b5, bool b6, bool b7, bool b8, b
             ;
         ;
     }
+
+    void M2(int i, bool b1, bool b2, bool b3, bool b4, bool b5, bool b6, bool b7, bool b8, bool b9, bool b10, bool b11, bool b12, bool b13, bool b14, bool b15, bool b16, bool b17, bool b18, bool b19, bool b20, bool b21, bool b22, bool b23, bool b24, bool b25, bool b26, bool b27, bool b28, bool b29)
+    {
+        while (i-- > 0)
+        {
+            if (i == 1)
+            {
+                if (b1)
+                    ;
+            }
+            if (i == 2)
+            {
+                if (b2)
+                    ;
+            }
+            if (i == 3)
+            {
+                if (b3)
+                    ;
+            }
+            if (i == 4)
+            {
+                if (b4)
+                    ;
+            }
+            if (i == 5)
+            {
+                if (b5)
+                    ;
+            }
+            if (i == 6)
+            {
+                if (b6)
+                    ;
+            }
+            if (i == 7)
+            {
+                if (b7)
+                    ;
+            }
+            if (i == 8)
+            {
+                if (b8)
+                    ;
+            }
+            if (i == 9)
+            {
+                if (b9)
+                    ;
+            }
+            if (i == 10)
+            {
+                if (b10)
+                    ;
+            }
+            if (i == 11)
+            {
+                if (b11)
+                    ;
+            }
+            if (i == 12)
+            {
+                if (b12)
+                    ;
+            }
+            if (i == 13)
+            {
+                if (b13)
+                    ;
+            }
+            if (i == 14)
+            {
+                if (b14)
+                    ;
+            }
+            if (i == 15)
+            {
+                if (b15)
+                    ;
+            }
+            if (i == 16)
+            {
+                if (b16)
+                    ;
+            }
+            if (i == 17)
+            {
+                if (b17)
+                    ;
+            }
+            if (i == 18)
+            {
+                if (b18)
+                    ;
+            }
+            if (i == 19)
+            {
+                if (b19)
+                    ;
+            }
+            if (i == 20)
+            {
+                if (b20)
+                    ;
+            }
+            if (i == 21)
+            {
+                if (b21)
+                    ;
+            }
+            if (i == 22)
+            {
+                if (b22)
+                    ;
+            }
+            if (i == 23)
+            {
+                if (b23)
+                    ;
+            }
+            if (i == 24)
+            {
+                if (b24)
+                    ;
+            }
+            if (i == 25)
+            {
+                if (b25)
+                    ;
+            }
+            if (i == 26)
+            {
+                if (b26)
+                    ;
+            }
+            if (i == 27)
+            {
+                if (b27)
+                    ;
+            }
+            if (i == 28)
+            {
+                if (b28)
+                    ;
+            }
+            if (i == 29)
+            {
+                if (b29)
+                    ;
+            }
+        }
+    }
 }