C++: Change all the 'ensures' predicates to be inlined to prevent explosions. Also remove the caching on 'compares' since this is't necessary now that the main recursion is cached.

Author: MathiasVP

cpp/ql/lib/semmle/code/cpp/controlflow/IRGuards.qll

@@ -98,7 +98,6 @@ abstract private class GuardConditionImpl extends Expr {
    * being short-circuited) then it will only control blocks dominated by the
    * true (for `&&`) or false (for `||`) branch.
    */
-  cached
   final predicate controls(BasicBlock controlled, boolean testIsTrue) {
     this.valueControls(controlled, any(BooleanValue bv | bv.getValue() = testIsTrue))
   }
@@ -110,43 +109,40 @@ abstract private class GuardConditionImpl extends Expr {
    * Holds if (determined by this guard) `left < right + k` must be `isLessThan` in `block`.
    *   If `isLessThan = false` then this implies `left >= right + k`.
    */
-  cached
+  pragma[inline]
   abstract predicate ensuresLt(Expr left, Expr right, int k, BasicBlock block, boolean isLessThan);
 
   /**
    * Holds if (determined by this guard) `e < k` evaluates to `isLessThan` if
    * this expression evaluates to `value`.
    */
-  cached
   abstract predicate comparesLt(Expr e, int k, boolean isLessThan, AbstractValue value);
 
   /**
    * Holds if (determined by this guard) `e < k` must be `isLessThan` in `block`.
    * If `isLessThan = false` then this implies `e >= k`.
    */
-  cached
+  pragma[inline]
   abstract predicate ensuresLt(Expr e, int k, BasicBlock block, boolean isLessThan);
 
   /** Holds if (determined by this guard) `left == right + k` evaluates to `areEqual` if this expression evaluates to `testIsTrue`. */
-  cached
   abstract predicate comparesEq(Expr left, Expr right, int k, boolean areEqual, boolean testIsTrue);
 
   /**
    * Holds if (determined by this guard) `left == right + k` must be `areEqual` in `block`.
    * If `areEqual = false` then this implies `left != right + k`.
    */
-  cached
+  pragma[inline]
   abstract predicate ensuresEq(Expr left, Expr right, int k, BasicBlock block, boolean areEqual);
 
   /** Holds if (determined by this guard) `e == k` evaluates to `areEqual` if this expression evaluates to `value`. */
-  cached
   abstract predicate comparesEq(Expr e, int k, boolean areEqual, AbstractValue value);
 
   /**
    * Holds if (determined by this guard) `e == k` must be `areEqual` in `block`.
    * If `areEqual = false` then this implies `e != k`.
    */
-  cached
+  pragma[inline]
   abstract predicate ensuresEq(Expr e, int k, BasicBlock block, boolean areEqual);
 }
 
@@ -187,12 +183,14 @@ private class GuardConditionFromBinaryLogicalOperator extends GuardConditionImpl
     )
   }
 
+  pragma[inline]
   override predicate ensuresLt(Expr left, Expr right, int k, BasicBlock block, boolean isLessThan) {
     exists(boolean testIsTrue |
       this.comparesLt(left, right, k, isLessThan, testIsTrue) and this.controls(block, testIsTrue)
     )
   }
 
+  pragma[inline]
   override predicate ensuresLt(Expr e, int k, BasicBlock block, boolean isLessThan) {
     exists(AbstractValue value |
       this.comparesLt(e, k, isLessThan, value) and this.valueControls(block, value)
@@ -207,6 +205,7 @@ private class GuardConditionFromBinaryLogicalOperator extends GuardConditionImpl
     )
   }
 
+  pragma[inline]
   override predicate ensuresEq(Expr left, Expr right, int k, BasicBlock block, boolean areEqual) {
     exists(boolean testIsTrue |
       this.comparesEq(left, right, k, areEqual, testIsTrue) and this.controls(block, testIsTrue)
@@ -222,6 +221,7 @@ private class GuardConditionFromBinaryLogicalOperator extends GuardConditionImpl
     )
   }
 
+  pragma[inline]
   override predicate ensuresEq(Expr e, int k, BasicBlock block, boolean areEqual) {
     exists(AbstractValue value |
       this.comparesEq(e, k, areEqual, value) and this.valueControls(block, value)
@@ -259,6 +259,7 @@ private class GuardConditionFromIR extends GuardConditionImpl {
     )
   }
 
+  pragma[inline]
   override predicate ensuresLt(Expr left, Expr right, int k, BasicBlock block, boolean isLessThan) {
     exists(Instruction li, Instruction ri, boolean testIsTrue |
       li.getUnconvertedResultExpression() = left and
@@ -268,6 +269,7 @@ private class GuardConditionFromIR extends GuardConditionImpl {
     )
   }
 
+  pragma[inline]
   override predicate ensuresLt(Expr e, int k, BasicBlock block, boolean isLessThan) {
     exists(Instruction i, AbstractValue value |
       i.getUnconvertedResultExpression() = e and
@@ -284,6 +286,7 @@ private class GuardConditionFromIR extends GuardConditionImpl {
     )
   }
 
+  pragma[inline]
   override predicate ensuresEq(Expr left, Expr right, int k, BasicBlock block, boolean areEqual) {
     exists(Instruction li, Instruction ri, boolean testIsTrue |
       li.getUnconvertedResultExpression() = left and
@@ -300,6 +303,7 @@ private class GuardConditionFromIR extends GuardConditionImpl {
     )
   }
 
+  pragma[inline]
   override predicate ensuresEq(Expr e, int k, BasicBlock block, boolean areEqual) {
     exists(Instruction i, AbstractValue value |
       i.getUnconvertedResultExpression() = e and
@@ -362,7 +366,6 @@ private predicate nonExcludedIRAndBasicBlock(IRBlock irb, BasicBlock controlled)
  * For performance reasons conditions inside static local initializers or
  * global initializers are not considered `IRGuardCondition`s.
  */
-cached
 class IRGuardCondition extends Instruction {
   Instruction branch;
 
@@ -383,7 +386,7 @@ class IRGuardCondition extends Instruction {
    * gcc extension.
    *
    * The implementation of all four follows the same structure: Each relation
-   * has a cached user-facing predicate that. For example,
+   * has a user-facing predicate that. For example,
    * `GuardCondition::comparesEq` calls `compares_eq`. This predicate has
    * several cases that recursively decompose the relation to bring it to a
    * canonical form (i.e., a relation of the form `e1 == e2 + k`). The base
@@ -393,7 +396,6 @@ class IRGuardCondition extends Instruction {
    * `e1 + k1 == e2 + k2` into canonical the form `e1 == e2 + (k2 - k1)`.
    */
 
-  cached
   IRGuardCondition() { branch = getBranchForCondition(this) }
 
   /**
@@ -402,7 +404,6 @@ class IRGuardCondition extends Instruction {
    *
    * For details on what "controls" mean, see the QLDoc for `controls`.
    */
-  cached
   predicate valueControls(IRBlock controlled, AbstractValue v) {
     // This condition must determine the flow of control; that is, this
     // node must be a top-level condition.
@@ -440,7 +441,6 @@ class IRGuardCondition extends Instruction {
    * being short-circuited) then it will only control blocks dominated by the
    * true (for `&&`) or false (for `||`) branch.
    */
-  cached
   predicate controls(IRBlock controlled, boolean testIsTrue) {
     this.valueControls(controlled, any(BooleanValue bv | bv.getValue() = testIsTrue))
   }
@@ -449,7 +449,6 @@ class IRGuardCondition extends Instruction {
    * Holds if the control-flow edge `(pred, succ)` may be taken only if
    * the value of this condition is `v`.
    */
-  cached
   predicate valueControlsEdge(IRBlock pred, IRBlock succ, AbstractValue v) {
     pred.getASuccessor() = succ and
     this.valueControls(pred, v)
@@ -468,7 +467,6 @@ class IRGuardCondition extends Instruction {
    * Holds if the control-flow edge `(pred, succ)` may be taken only if
    * the value of this condition is `testIsTrue`.
    */
-  cached
   final predicate controlsEdge(IRBlock pred, IRBlock succ, boolean testIsTrue) {
     this.valueControlsEdge(pred, succ, any(BooleanValue bv | bv.getValue() = testIsTrue))
   }
@@ -506,7 +504,6 @@ class IRGuardCondition extends Instruction {
   }
 
   /** Holds if (determined by this guard) `left < right + k` evaluates to `isLessThan` if this expression evaluates to `testIsTrue`. */
-  cached
   predicate comparesLt(Operand left, Operand right, int k, boolean isLessThan, boolean testIsTrue) {
     exists(BooleanValue value |
       compares_lt(valueNumber(this), left, right, k, isLessThan, value) and
@@ -518,7 +515,6 @@ class IRGuardCondition extends Instruction {
    * Holds if (determined by this guard) `op < k` evaluates to `isLessThan` if
    * this expression evaluates to `value`.
    */
-  cached
   predicate comparesLt(Operand op, int k, boolean isLessThan, AbstractValue value) {
     compares_lt(valueNumber(this), op, k, isLessThan, value)
   }
@@ -527,7 +523,7 @@ class IRGuardCondition extends Instruction {
    * Holds if (determined by this guard) `left < right + k` must be `isLessThan` in `block`.
    * If `isLessThan = false` then this implies `left >= right + k`.
    */
-  cached
+  pragma[inline]
   predicate ensuresLt(Operand left, Operand right, int k, IRBlock block, boolean isLessThan) {
     exists(AbstractValue value |
       compares_lt(valueNumber(this), left, right, k, isLessThan, value) and
@@ -539,7 +535,7 @@ class IRGuardCondition extends Instruction {
    * Holds if (determined by this guard) `op < k` must be `isLessThan` in `block`.
    * If `isLessThan = false` then this implies `op >= k`.
    */
-  cached
+  pragma[inline]
   predicate ensuresLt(Operand op, int k, IRBlock block, boolean isLessThan) {
     exists(AbstractValue value |
       compares_lt(valueNumber(this), op, k, isLessThan, value) and
@@ -551,7 +547,7 @@ class IRGuardCondition extends Instruction {
    * Holds if (determined by this guard) `left < right + k` must be `isLessThan` on the edge from
    * `pred` to `succ`. If `isLessThan = false` then this implies `left >= right + k`.
    */
-  cached
+  pragma[inline]
   predicate ensuresLtEdge(
     Operand left, Operand right, int k, IRBlock pred, IRBlock succ, boolean isLessThan
   ) {
@@ -565,7 +561,7 @@ class IRGuardCondition extends Instruction {
    * Holds if (determined by this guard) `op < k` must be `isLessThan` on the edge from
    * `pred` to `succ`. If `isLessThan = false` then this implies `op >= k`.
    */
-  cached
+  pragma[inline]
   predicate ensuresLtEdge(Operand left, int k, IRBlock pred, IRBlock succ, boolean isLessThan) {
     exists(AbstractValue value |
       compares_lt(valueNumber(this), left, k, isLessThan, value) and
@@ -574,7 +570,6 @@ class IRGuardCondition extends Instruction {
   }
 
   /** Holds if (determined by this guard) `left == right + k` evaluates to `areEqual` if this expression evaluates to `testIsTrue`. */
-  cached
   predicate comparesEq(Operand left, Operand right, int k, boolean areEqual, boolean testIsTrue) {
     exists(BooleanValue value |
       compares_eq(valueNumber(this), left, right, k, areEqual, value) and
@@ -583,7 +578,6 @@ class IRGuardCondition extends Instruction {
   }
 
   /** Holds if (determined by this guard) `op == k` evaluates to `areEqual` if this expression evaluates to `value`. */
-  cached
   predicate comparesEq(Operand op, int k, boolean areEqual, AbstractValue value) {
     unary_compares_eq(valueNumber(this), op, k, areEqual, false, value)
   }
@@ -592,7 +586,7 @@ class IRGuardCondition extends Instruction {
    * Holds if (determined by this guard) `left == right + k` must be `areEqual` in `block`.
    * If `areEqual = false` then this implies `left != right + k`.
    */
-  cached
+  pragma[inline]
   predicate ensuresEq(Operand left, Operand right, int k, IRBlock block, boolean areEqual) {
     exists(AbstractValue value |
       compares_eq(valueNumber(this), left, right, k, areEqual, value) and
@@ -604,7 +598,7 @@ class IRGuardCondition extends Instruction {
    * Holds if (determined by this guard) `op == k` must be `areEqual` in `block`.
    * If `areEqual = false` then this implies `op != k`.
    */
-  cached
+  pragma[inline]
   predicate ensuresEq(Operand op, int k, IRBlock block, boolean areEqual) {
     exists(AbstractValue value |
       unary_compares_eq(valueNumber(this), op, k, areEqual, false, value) and
@@ -616,7 +610,7 @@ class IRGuardCondition extends Instruction {
    * Holds if (determined by this guard) `left == right + k` must be `areEqual` on the edge from
    * `pred` to `succ`. If `areEqual = false` then this implies `left != right + k`.
    */
-  cached
+  pragma[inline]
   predicate ensuresEqEdge(
     Operand left, Operand right, int k, IRBlock pred, IRBlock succ, boolean areEqual
   ) {
@@ -630,7 +624,7 @@ class IRGuardCondition extends Instruction {
    * Holds if (determined by this guard) `op == k` must be `areEqual` on the edge from
    * `pred` to `succ`. If `areEqual = false` then this implies `op != k`.
    */
-  cached
+  pragma[inline]
   predicate ensuresEqEdge(Operand op, int k, IRBlock pred, IRBlock succ, boolean areEqual) {
     exists(AbstractValue value |
       unary_compares_eq(valueNumber(this), op, k, areEqual, false, value) and