WIP, snapshop

Author: paldepind

cpp/ql/lib/semmle/code/cpp/rangeanalysis/SimpleRangeAnalysis.qll

@@ -496,11 +496,20 @@ private predicate isRecursiveDef(RangeSsaDefinition def, StackVariable v) {
 }
 
 private predicate isExplosiveVar(StackVariable v) {
+  // exists(RangeSsaDefinition def, StackVariable v |
+  //   nrOfBoundsDef(def, v)
+  // )
+  // or
   none() and
   64 < count(RangeSsaDefinition def | def.getAVariable() = v and def.isPhiNode(_))
 }
 
-// private predicate isWidenedVariable
+/**
+ * Holds if `e` is an expression for which a very large number of bounds might
+ * be generated during the range analysis.
+ */
+private predicate isExplosiveExpr(Expr e) { nrOfBounds(e) > 1000000 }
+
 /**
  * Holds if the bounds of `e` depend on a recursive definition, meaning that
  * `e` is likely to have many candidate bounds during the main recursion.
@@ -512,7 +521,7 @@ private predicate isRecursiveExpr(Expr e) {
 }
 
 /** Provides an estimated measure on the number of bounds for an expression. */
-private int nrOfBounds(Expr e) {
+private float nrOfBounds(Expr e) {
   isRecursiveExpr(e) and result = 13 // FIXME: Let's not hardcode this
   or
   not isRecursiveExpr(e) and
@@ -550,8 +559,6 @@ private int nrOfBounds(Expr e) {
       exists(AssignMulByConstantExpr mulExpr |
         e = mulExpr and
         result = nrOfBounds(mulExpr.getLValue())
-        // xLow = getFullyConvertedLowerBounds(mulExpr.getLValue()) and
-        // result = xLow * mulExpr.getConstant()
       )
       or
       // Handles the `--` and `++` operators
@@ -573,7 +580,7 @@ private int nrOfBounds(Expr e) {
       or
       exists(RangeSsaDefinition def, StackVariable v |
         e = def.getAUse(v) and
-        result = defNrOfBounds(def, v) and
+        result = nrOfBoundsDef(def, v) and
         not exists(getValue(e).toFloat())
       )
       or
@@ -593,6 +600,12 @@ private int nrOfBounds(Expr e) {
         e instanceof AssignSubExpr or
         e instanceof UnsignedAssignMulExpr
       )
+      or
+      exists(RShiftExpr rsExpr |
+        e = rsExpr and
+        exists(getValue(rsExpr.getRightOperand().getFullyConverted()).toInt()) and
+        result = nrOfBounds(rsExpr.getLeftOperand())
+      )
     )
     or
     not analyzableExpr(e) and exists(exprMinVal(e)) and result = 1
@@ -608,87 +621,113 @@ int teststst(RangeSsaDefinition def, StackVariable v, VariableAccess access) {
   )
 }
 
+private predicate hasLinearBoundFromGuard2(
+  ComparisonOperation guard, VariableAccess v, float p, float q, RelationStrictness strictness,
+  boolean branch // Which control-flow branch is this bound valid on?
+) {
+  exists(Expr lhs, Expr rhs, RelationDirection dir, RelationStrictness st |
+    linearAccess(lhs, v, p, q) and
+    relOpWithSwapAndNegate(guard, lhs, rhs, dir, st, branch)
+  |
+    strictness = st
+    or
+    strictness = Nonstrict() and
+    exprTypeBounds(rhs, _, _)
+  )
+  or
+  exists(Expr lhs, Expr rhs |
+    linearAccess(lhs, v, p, q) and
+    eqOpWithSwapAndNegate(guard, lhs, rhs, true, branch) and
+    strictness = Nonstrict()
+  )
+}
+
+/**
+ * Holds if `lowerBoundFromGuard(guard, v, _, branch)` holds, but without
+ * relying on range analysis (which would cause non-monotonic recursion
+ * elsewhere).
+ */
+predicate hasLowerBoundFromGuard(Expr guard, VariableAccess v, boolean branch) {
+  hasLinearBoundFromGuard2(guard, v, _, _, _, branch)
+  or
+  // lowerBoundFromGuard(guard, v, _, branch)
+  exists(float p, float q, Expr e |
+    linearAccess(e, v, p, q) and
+    eqZeroWithNegate(guard, e, true, branch) // and
+    // boundValue = (0.0 - q) / p and
+    // isLowerBound = [false, true] and
+    // strictness = Nonstrict()
+  )
+}
+
+predicate missing(Expr guard, VariableAccess access, boolean branch) {
+  lowerBoundFromGuard(guard, access, _, branch) and
+  not hasLowerBoundFromGuard(guard, access, branch)
+}
+
+predicate tooMuch(Expr guard, VariableAccess access, boolean branch) {
+  not lowerBoundFromGuard(guard, access, _, branch) and
+  hasLowerBoundFromGuard(guard, access, branch)
+}
+
 predicate isGuardPhiWithBound(
   RangeSsaDefinition def, StackVariable v, VariableAccess access, Expr guard, boolean branch
 ) {
   def.isGuardPhi(v, access, guard, branch) and
-  lowerBoundFromGuard(guard, access, _, branch)
+  hasLowerBoundFromGuard(guard, access, branch)
 }
 
-language[monotonicAggregates]
-int defNrOfBoundsPhiGuard(RangeSsaDefinition def, StackVariable v) {
-  v = Debug::getRelevantLocatable() and
-  (
-    // NOTE: A phi node can be both a guard phi node and a normal phi node. In
-    // that case we only treat it as a normal phi node.
-    // TODO: Should we change this in `getPhiLowerBounds`?
-    // not exists(VariableAccess access, Expr guard, boolean branch |
-    //   def.isGuardPhi(v, access, guard, branch) and
-    //   lowerBoundFromGuard(guard, access, _, branch)
-    // ) and
-    not isGuardPhiWithBound(def, v, _, _, _) and
-    def.isPhiNode(v) and
-    result = 0
-    or
-    // NOTE: The differenct `access`es are the same variable and the lower
-    // bounds are the same. The guard may filter some away. Hence adding these
-    // guards make no sense (the impl will take the union but after dedup taking
-    // `max` is a better representation).
-    result =
-      max(VariableAccess access |
-        // def.isGuardPhi(v, access, guard, branch) and
-        // lowerBoundFromGuard(guard, access, _, branch)
-        isGuardPhiWithBound(def, v, access, _, _)
-      |
-        nrOfBounds(access)
-      )
-  )
+predicate debugThing(RangeSsaDefinition def, StackVariable v, VariableAccess access) {
+  def.isGuardPhi(v, access, _, _) and
+  not isGuardPhiWithBound(def, v, access, _, _)
 }
 
 language[monotonicAggregates]
-int defNrOfBoundsPhiNormal(RangeSsaDefinition def, StackVariable v) {
-  v = Debug::getRelevantLocatable() and
-  (
-    def.isGuardPhi(v, _, _, _) and
-    not exists(def.getAPhiInput(v)) and
-    result = 0
-    or
-    result =
-      strictsum(RangeSsaDefinition inputDef |
-        inputDef = def.getAPhiInput(v)
-      |
-        defNrOfBounds(inputDef, v)
-      )
-  )
+float defNrOfBoundsPhiGuard(RangeSsaDefinition def, StackVariable v) {
+  def.isPhiNode(v) and
+  not isGuardPhiWithBound(def, v, _, _, _) and
+  result = 0
+  or
+  // NOTE: The differenct `access`es are the same variable and the lower
+  // bounds are the same. The guard may filter some away. Hence adding these
+  // guards make no sense (the impl will take the union but after dedup taking
+  // `max` is a better representation).
+  result =
+    max(VariableAccess access | isGuardPhiWithBound(def, v, access, _, _) | nrOfBounds(access))
 }
 
-int nrOfBoundsNEPhi(RangeSsaDefinition def, StackVariable v) {
-  v = Debug::getRelevantLocatable() and
-  (
-    exists(VariableAccess access | isNEPhi(v, def, access, _) and result = nrOfBounds(access))
-    or
-    not isNEPhi(v, def, _, _) and result = 0
-  )
+language[monotonicAggregates]
+float defNrOfBoundsPhiNormal(RangeSsaDefinition def, StackVariable v) {
+  def.isPhiNode(v) and
+  not exists(def.getAPhiInput(v)) and
+  result = 0
+  or
+  result =
+    strictsum(RangeSsaDefinition inputDef |
+      inputDef = def.getAPhiInput(v)
+    |
+      nrOfBoundsDef(inputDef, v)
+    )
 }
 
-predicate gimmeBug(RangeSsaDefinition def, StackVariable v) {
-  nrOfBoundsNEPhi(def, v) > 0 and
-  exists(defNrOfBoundsPhiNormal(def, v)) and
-  exists(defNrOfBoundsPhiGuard(def, v))
+float nrOfBoundsNEPhi(RangeSsaDefinition def, StackVariable v) {
+  exists(VariableAccess access | isNEPhi(v, def, access, _) and result = nrOfBounds(access))
+  or
+  def.isPhiNode(v) and
+  not isNEPhi(v, def, _, _) and
+  result = 0
 }
 
-int nrOfBoundsPhi(RangeSsaDefinition def, StackVariable v) {
-  exists(int nePhi, int unsupportedGuardPhi |
+float nrOfBoundsPhi(RangeSsaDefinition def, StackVariable v) {
+  // NOTE: A phi node can be both a guard phi node and a normal phi node. In
+  // that case we only treat it as a normal phi node.
+  // TODO: Should we change this in `getPhiLowerBounds`?
+  exists(int unsupportedGuardPhi |
     result =
       // Guard phi nodes
       defNrOfBoundsPhiGuard(def, v) +
         // Normal phi nodes
-        defNrOfBoundsPhiNormal(def, v) + nePhi + unsupportedGuardPhi and
-    // (exists(VariableAccess access | isNEPhi(v, def, access, _) and nePhi = nrOfBounds(access))
-    // or
-    // not isNEPhi(v, def, _, _) and nePhi = 0.0)
-    nePhi = nrOfBoundsNEPhi(def, v) and
-    // unsupportedGuardPhi = 0 and
+        defNrOfBoundsPhiNormal(def, v) + nrOfBoundsNEPhi(def, v) + unsupportedGuardPhi and
     (
       exists(VariableAccess access |
         isUnsupportedGuardPhi(v, def, access) and
@@ -702,7 +741,7 @@ int nrOfBoundsPhi(RangeSsaDefinition def, StackVariable v) {
 }
 
 language[monotonicAggregates]
-int defNrOfBounds(RangeSsaDefinition def, StackVariable v) {
+float nrOfBoundsDef(RangeSsaDefinition def, StackVariable v) {
   v = Debug::getRelevantLocatable() and
   (
     // Definitions with a defining value
@@ -1777,27 +1816,23 @@ private predicate exprTypeBounds(Expr expr, float boundValue, boolean isLowerBou
 private predicate isNEPhi(
   Variable v, RangeSsaDefinition phi, VariableAccess access, float neConstant
 ) {
-  v = Debug::getRelevantLocatable() and
-  (
-    exists(
-      ComparisonOperation cmp, boolean branch, Expr linearExpr, Expr rExpr, float p, float q,
-      float r
-    |
-      phi.isGuardPhi(v, access, cmp, branch) and
-      eqOpWithSwapAndNegate(cmp, linearExpr, rExpr, false, branch) and
-      v.getUnspecifiedType() instanceof IntegralOrEnumType and // Float `!=` is too imprecise
-      r = getValue(rExpr).toFloat() and
-      linearAccess(linearExpr, access, p, q) and
-      neConstant = (r - q) / p
-    )
-    or
-    exists(Expr op, boolean branch, Expr linearExpr, float p, float q |
-      phi.isGuardPhi(v, access, op, branch) and
-      eqZeroWithNegate(op, linearExpr, false, branch) and
-      v.getUnspecifiedType() instanceof IntegralOrEnumType and // Float `!` is too imprecise
-      linearAccess(linearExpr, access, p, q) and
-      neConstant = (0.0 - q) / p
-    )
+  exists(
+    ComparisonOperation cmp, boolean branch, Expr linearExpr, Expr rExpr, float p, float q, float r
+  |
+    phi.isGuardPhi(v, access, cmp, branch) and
+    eqOpWithSwapAndNegate(cmp, linearExpr, rExpr, false, branch) and
+    v.getUnspecifiedType() instanceof IntegralOrEnumType and // Float `!=` is too imprecise
+    r = getValue(rExpr).toFloat() and
+    linearAccess(linearExpr, access, p, q) and
+    neConstant = (r - q) / p
+  )
+  or
+  exists(Expr op, boolean branch, Expr linearExpr, float p, float q |
+    phi.isGuardPhi(v, access, op, branch) and
+    eqZeroWithNegate(op, linearExpr, false, branch) and
+    v.getUnspecifiedType() instanceof IntegralOrEnumType and // Float `!` is too imprecise
+    linearAccess(linearExpr, access, p, q) and
+    neConstant = (0.0 - q) / p
   )
 }
 
@@ -2117,7 +2152,7 @@ private module Debug {
   Locatable getRelevantLocatable() {
     exists(string filepath, int startline |
       result.getLocation().hasLocationInfo(filepath, startline, _, _, _) and
-      // filepath.matches("%/Cmprs_RiceLayersMem.C") and
+      // filepath.matches("%/Cmprs_RiceLayersMem.C") // and
       // startline = [1452 .. 1480]
       filepath.matches("%/test.c") // and
       // startline = [845 .. 867]
@@ -2174,16 +2209,6 @@ private module Debug {
     )
   }
 
-  int debugDefNrOfBounds(RangeSsaDefinition def, StackVariable v) {
-    v = getRelevantLocatable() and
-    defNrOfBounds(def, v) = result
-  }
-
-  int debugDefNrOfBoundsPhiNormal(RangeSsaDefinition def, StackVariable v) {
-    v = getRelevantLocatable() and
-    defNrOfBoundsPhiNormal(def, v) = result
-  }
-
   int nonFunctionalNrOfBounds(Expr e) {
     // e = getRelevantLocatable() and
     strictcount(nrOfBounds(e)) > 1 and