C++: Range analysis guard improvement

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

@@ -1,10 +1,10 @@
 import cpp
 
 /**
- * Describes whether a relation is 'strict' (that is, a `<` or `>`
+ * The strictness of a relation. Either 'strict' (that is, a `<` or `>`
  * relation) or 'non-strict' (a `<=` or `>=` relation).
  */
-newtype RelationStrictness =
+newtype TRelationStrictness =
   /**
    * Represents that a relation is 'strict' (that is, a `<` or `>` relation).
    */
@@ -14,6 +14,19 @@ newtype RelationStrictness =
    */
   Nonstrict()
 
+/**
+ * The strictness of a relation. Either 'strict' (that is, a `<` or `>`
+ * relation) or 'non-strict' (a `<=` or `>=` relation).
+ */
+class RelationStrictness extends TRelationStrictness {
+  /** Gets the string representation of this relation strictness. */
+  string toString() {
+    this = Strict() and result = "strict"
+    or
+    this = Nonstrict() and result = "non-strict"
+  }
+}
+
 /**
  * Describes whether a relation is 'greater' (that is, a `>` or `>=`
  * relation) or 'lesser' (a `<` or `<=` relation).
@@ -105,10 +118,10 @@ predicate relOpWithSwap(
  *
  * This allows for the relation to be either as written, or with its
  * arguments reversed; for example, if `rel` is `x < 5` then
- * `relOpWithSwapAndNegate(rel, x, 5, Lesser(), Strict(), true)`,
- * `relOpWithSwapAndNegate(rel, 5, x, Greater(), Strict(), true)`,
- * `relOpWithSwapAndNegate(rel, x, 5, Greater(), Nonstrict(), false)` and
- * `relOpWithSwapAndNegate(rel, 5, x, Lesser(), Nonstrict(), false)` hold.
+ * - `relOpWithSwapAndNegate(rel, x, 5, Lesser(), Strict(), true)`,
+ * - `relOpWithSwapAndNegate(rel, 5, x, Greater(), Strict(), true)`,
+ * - `relOpWithSwapAndNegate(rel, x, 5, Greater(), Nonstrict(), false)` and
+ * - `relOpWithSwapAndNegate(rel, 5, x, Lesser(), Nonstrict(), false)` hold.
  */
 predicate relOpWithSwapAndNegate(
   RelationalOperation rel, Expr a, Expr b, RelationDirection dir, RelationStrictness strict,

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

@@ -1397,6 +1397,20 @@
   nanExcludingComparison(guard, branch)
 }
 
+/**
+ * Adjusts a lower bound to its meaning for integral types.
+ *
+ * Examples:
+ * `>= 3.0` becomes `3.0`
+ * ` > 3.0` becomes `4.0`
+ * `>= 3.5` becomes `4.0`
+ * ` > 3.5` becomes `4.0`
+ */
+bindingset[strictness, lb]
+private float adjustLowerBoundIntegral(RelationStrictness strictness, float lb) {
+  if strictness = Nonstrict() and lb.floor() = lb then result = lb else result = safeFloor(lb) + 1
+}
+
 /**
  * If the guard is a comparison of the form `p*v + q <CMP> r`, then this
  * predicate uses the bounds information for `r` to compute a lower bound
@@ -1408,15 +1422,27 @@
   |
     if nonNanGuardedVariable(guard, v, branch)
     then
-      if
-        strictness = Nonstrict() or
-        not getVariableRangeType(v.getTarget()) instanceof IntegralType
-      then lb = childLB
-      else lb = childLB + 1
+      if getVariableRangeType(v.getTarget()) instanceof IntegralType
+      then lb = adjustLowerBoundIntegral(strictness, childLB)
+      else lb = childLB
     else lb = varMinVal(v.getTarget())
   )
 }
 
+/**
+ * Adjusts an upper bound to its meaning for integral types.
+ *
+ * Examples:
+ * `<= 3.0` becomes `3.0`
+ * ` < 3.0` becomes `2.0`
+ * `<= 3.5` becomes `3.0`
+ * ` < 3.5` becomes `3.0`
+ */
+bindingset[strictness, ub]
+private float adjustUpperBoundIntegral(RelationStrictness strictness, float ub) {
+  if strictness = Strict() and ub.floor() = ub then result = ub - 1 else result = safeFloor(ub)
+}
+
 /**
  * If the guard is a comparison of the form `p*v + q <CMP> r`, then this
  * predicate uses the bounds information for `r` to compute a upper bound
@@ -1428,11 +1454,9 @@
   |
     if nonNanGuardedVariable(guard, v, branch)
     then
-      if
-        strictness = Nonstrict() or
-        not getVariableRangeType(v.getTarget()) instanceof IntegralType
-      then ub = childUB
-      else ub = childUB - 1
+      if getVariableRangeType(v.getTarget()) instanceof IntegralType
+      then ub = adjustUpperBoundIntegral(strictness, childUB)
+      else ub = childUB
     else ub = varMaxVal(v.getTarget())
   )
 }
@@ -1472,7 +1496,7 @@
  * lower or upper bound for `v`.
  */
 private predicate linearBoundFromGuard(
-  ComparisonOperation guard, VariableAccess v, float p, float q, float boundValue,
+  ComparisonOperation guard, VariableAccess v, float p, float q, float r,
   boolean isLowerBound, // Is this a lower or an upper bound?
   RelationStrictness strictness, boolean branch // Which control-flow branch is this bound valid on?
 ) {
@@ -1487,11 +1511,11 @@
   |
     isLowerBound = directionIsGreater(dir) and
     strictness = st and
-    getBounds(rhs, boundValue, isLowerBound)
+    getBounds(rhs, r, isLowerBound)
     or
     isLowerBound = directionIsLesser(dir) and
     strictness = Nonstrict() and
-    exprTypeBounds(rhs, boundValue, isLowerBound)
+    exprTypeBounds(rhs, r, isLowerBound)
   )
   or
   // For x == RHS, we create the following bounds:
@@ -1502,7 +1526,7 @@
   exists(Expr lhs, Expr rhs |
     linearAccess(lhs, v, p, q) and
     eqOpWithSwapAndNegate(guard, lhs, rhs, true, branch) and
-    getBounds(rhs, boundValue, isLowerBound) and
+    getBounds(rhs, r, isLowerBound) and
     strictness = Nonstrict()
   )
   // x != RHS and !x are handled elsewhere
@@ -1860,3 +1884,34 @@
     defMightOverflowNegatively(def, v) and result = varMaxVal(v)
   }
 }
+
+/** Provides predicates for debugging the simple range analysis library. */
+private module Debug {
+  Locatable getRelevantLocatable() {
+    exists(string filepath, int startline |
+      result.getLocation().hasLocationInfo(filepath, startline, _, _, _) and
+      filepath.matches("%/test.c") and
+      startline = [464 .. 472]
+    )
+  }
+
+  float debugGetFullyConvertedLowerBounds(Expr expr) {
+    expr = getRelevantLocatable() and
+    result = getFullyConvertedLowerBounds(expr)
+  }
+
+  float debugGetLowerBoundsImpl(Expr e, string kl) {
+    e = getRelevantLocatable() and
+    result = getLowerBoundsImpl(e) and
+    kl = e.getPrimaryQlClasses()
+  }
+
+  /**
+   * Counts the number of lower bounds for a given expression. This predicate is
+   * useful for identifying performance issues in the range analysis.
+   */
+  predicate nrOfLowerBounds(Expr e, int n) {
+    e = getRelevantLocatable() and
+    n = strictcount(float lb | lb = getLowerBoundsImpl(e) | lb)
+  }
+}