C++: Pull rounding functions out to new predicates

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

@@ -293,6 +293,50 @@ predicate analyzableDef(RangeSsaDefinition def, LocalScopeVariable v) {
   assignmentDef(def, v, _) or defDependsOnDef(def, v, _, _)
 }
 
+/**
+ * Computes `x + y`, rounded towards +Inf. This is the general case where both
+ * `x` and `y` may be large numbers.
+ */
+bindingset[x, y]
+private float addRoundingUp(float x, float y) {
+  if (x + y) - x < y or (x + y) - y < x
+  then result = (x + y).nextUp()
+  else result = (x + y)
+}
+
+/**
+ * Computes `x + y`, rounded towards -Inf. This is the general case where both
+ * `x` and `y` may be large numbers.
+ */
+bindingset[x, y]
+private float addRoundingDown(float x, float y) {
+  if (x + y) - x > y or (x + y) - y > x
+  then result = (x + y).nextDown()
+  else result = (x + y)
+}
+
+/**
+ * Computes `x + small`, rounded towards +Inf, where `small` is a small
+ * constant.
+ */
+bindingset[x, small]
+private float addRoundingUpSmall(float x, float small) {
+  if (x + small) - x < small
+  then result = (x + small).nextUp()
+  else result = (x + small)
+}
+
+/**
+ * Computes `x + small`, rounded towards -Inf, where `small` is a small
+ * constant.
+ */
+bindingset[x, small]
+private float addRoundingDownSmall(float x, float small) {
+  if (x + small) - x > small
+  then result = (x + small).nextDown()
+  else result = (x + small)
+}
+
 /**
  * Gets the truncated lower bounds of the fully converted expression.
  */
@@ -469,20 +513,14 @@ float getLowerBoundsImpl(Expr expr) {
   exists (AddExpr addExpr, float xLow, float yLow
   | expr = addExpr and
     xLow = getFullyConvertedLowerBounds(addExpr.getLeftOperand()) and
-    yLow = getFullyConvertedLowerBounds(addExpr.getRightOperand())
-  | // Make sure that we round towards -Inf, not to nearest.
-    if (xLow+yLow)-xLow > yLow or (xLow+yLow)-yLow > xLow
-      then result = (xLow+yLow).nextDown()
-      else result = xLow+yLow)
+    yLow = getFullyConvertedLowerBounds(addExpr.getRightOperand()) and
+    result = addRoundingDown(xLow, yLow))
   or
   exists (SubExpr subExpr, float xLow, float yHigh
   | expr = subExpr and
     xLow = getFullyConvertedLowerBounds(subExpr.getLeftOperand()) and
-    yHigh = getFullyConvertedUpperBounds(subExpr.getRightOperand())
-  | // Make sure that we round towards -Inf, not to nearest.
-    if (xLow-yHigh)-xLow > -yHigh or (xLow-yHigh)+yHigh > xLow
-      then result = (xLow-yHigh).nextDown()
-      else result = xLow-yHigh)
+    yHigh = getFullyConvertedUpperBounds(subExpr.getRightOperand()) and
+    result = addRoundingDown(xLow, -yHigh))
   or
   exists (PrefixIncrExpr incrExpr, float xLow
   | expr = incrExpr and
@@ -491,11 +529,8 @@ float getLowerBoundsImpl(Expr expr) {
   or
   exists (PrefixDecrExpr decrExpr, float xLow
   | expr = decrExpr and
-    xLow = getFullyConvertedLowerBounds(decrExpr.getOperand())
-  | // Make sure that we round towards -Inf, not to nearest.
-    if (xLow-1)-xLow > -1
-      then result = (xLow-1).nextDown()
-      else result = xLow-1)
+    xLow = getFullyConvertedLowerBounds(decrExpr.getOperand()) and
+    result = addRoundingDownSmall(xLow, -1))
   or
   // `PostfixIncrExpr` and `PostfixDecrExpr` return the value of their
   // operand. The incrementing/decrementing behavior is handled in
@@ -600,28 +635,19 @@ float getUpperBoundsImpl(Expr expr) {
   exists (AddExpr addExpr, float xHigh, float yHigh
   | expr = addExpr and
     xHigh = getFullyConvertedUpperBounds(addExpr.getLeftOperand()) and
-    yHigh = getFullyConvertedUpperBounds(addExpr.getRightOperand())
-  | // Make sure that we round towards +Inf, not to nearest.
-    if (xHigh+yHigh)-xHigh < yHigh or (xHigh+yHigh)-yHigh < xHigh
-      then result = (xHigh+yHigh).nextUp()
-      else result = xHigh+yHigh)
+    yHigh = getFullyConvertedUpperBounds(addExpr.getRightOperand()) and
+    result = addRoundingUp(xHigh, yHigh))
   or
   exists (SubExpr subExpr, float xHigh, float yLow
   | expr = subExpr and
     xHigh = getFullyConvertedUpperBounds(subExpr.getLeftOperand()) and
-    yLow = getFullyConvertedLowerBounds(subExpr.getRightOperand())
-  | // Make sure that we round towards +Inf, not to nearest.
-    if (xHigh-yLow)-xHigh < -yLow or (xHigh-yLow)+yLow < xHigh
-      then result = (xHigh-yLow).nextUp()
-      else result = xHigh-yLow)
+    yLow = getFullyConvertedLowerBounds(subExpr.getRightOperand()) and
+    result = addRoundingUp(xHigh, -yLow))
   or
   exists (PrefixIncrExpr incrExpr, float xHigh
   | expr = incrExpr and
-    xHigh = getFullyConvertedUpperBounds(incrExpr.getOperand())
-  | // Make sure that we round towards +Inf, not to nearest.
-    if (xHigh+1)-xHigh < 1
-      then result = (xHigh+1).nextUp()
-      else result = xHigh+1)
+    xHigh = getFullyConvertedUpperBounds(incrExpr.getOperand()) and
+    result = addRoundingUpSmall(xHigh, 1))
   or
   exists (PrefixDecrExpr decrExpr, float xHigh
   | expr = decrExpr and
@@ -813,22 +839,16 @@ float getDefLowerBoundsImpl(RangeSsaDefinition def, LocalScopeVariable v) {
   | def = assignAdd and
     assignAdd.getLValue() = nextDef.getAUse(v) and
     lhsLB = getDefLowerBounds(nextDef, v) and
-    rhsLB = getFullyConvertedLowerBounds(assignAdd.getRValue())
-  | // Make sure that we round towards -Inf, not to nearest.
-    if (lhsLB+rhsLB)-lhsLB > rhsLB or (lhsLB+rhsLB)-rhsLB > lhsLB
-      then result = (lhsLB+rhsLB).nextDown()
-      else result = lhsLB+rhsLB)
+    rhsLB = getFullyConvertedLowerBounds(assignAdd.getRValue()) and
+    result = addRoundingDown(lhsLB, rhsLB))
   or
   exists (
     AssignSubExpr assignSub, RangeSsaDefinition nextDef, float lhsLB, float rhsUB
   | def = assignSub and
     assignSub.getLValue() = nextDef.getAUse(v) and
     lhsLB = getDefLowerBounds(nextDef, v) and
-    rhsUB = getFullyConvertedUpperBounds(assignSub.getRValue())
-  | // Make sure that we round towards -Inf, not to nearest.
-    if (lhsLB-rhsUB)-lhsLB > -rhsUB or (lhsLB-rhsUB)+rhsUB > lhsLB
-      then result = (lhsLB-rhsUB).nextDown()
-      else result = lhsLB-rhsUB)
+    rhsUB = getFullyConvertedUpperBounds(assignSub.getRValue()) and
+    result = addRoundingDown(lhsLB, -rhsUB))
   or
   exists (IncrementOperation incr, float newLB
   | def = incr and
@@ -839,11 +859,8 @@ float getDefLowerBoundsImpl(RangeSsaDefinition def, LocalScopeVariable v) {
   exists (DecrementOperation decr, float newLB
   | def = decr and
     decr.getOperand() = v.getAnAccess() and
-    newLB = getFullyConvertedLowerBounds(decr.getOperand())
-  | // Make sure that we round towards -Inf, not to nearest.
-    if (newLB-1)-newLB > -1
-      then result = (newLB-1).nextDown()
-      else result = newLB-1)
+    newLB = getFullyConvertedLowerBounds(decr.getOperand()) and
+    result = addRoundingDownSmall(newLB, -1))
   or
   // Phi nodes.
   result = getPhiLowerBounds(v, def)
@@ -865,31 +882,22 @@ float getDefUpperBoundsImpl(RangeSsaDefinition def, LocalScopeVariable v) {
   | def = assignAdd and
     assignAdd.getLValue() = nextDef.getAUse(v) and
     lhsUB = getDefUpperBounds(nextDef, v) and
-    rhsUB = getFullyConvertedUpperBounds(assignAdd.getRValue())
-  | // Make sure that we round towards +Inf, not to nearest.
-    if (lhsUB+rhsUB)-lhsUB < rhsUB or (lhsUB+rhsUB)-rhsUB < lhsUB
-      then result = (lhsUB+rhsUB).nextUp()
-      else result = lhsUB+rhsUB)
+    rhsUB = getFullyConvertedUpperBounds(assignAdd.getRValue()) and
+    result = addRoundingUp(lhsUB, rhsUB))
   or
   exists (
     AssignSubExpr assignSub, RangeSsaDefinition nextDef, float lhsUB, float rhsLB
   | def = assignSub and
     assignSub.getLValue() = nextDef.getAUse(v) and
     lhsUB = getDefUpperBounds(nextDef, v) and
-    rhsLB = getFullyConvertedLowerBounds(assignSub.getRValue())
-  | // Make sure that we round towards +Inf, not to nearest.
-    if (lhsUB-rhsLB)-lhsUB < -rhsLB or (lhsUB-rhsLB)+rhsLB < lhsUB
-      then result = (lhsUB-rhsLB).nextUp()
-      else result = lhsUB-rhsLB)
+    rhsLB = getFullyConvertedLowerBounds(assignSub.getRValue()) and
+    result = addRoundingUp(lhsUB, -rhsLB))
   or
   exists (IncrementOperation incr, float newUB
   | def = incr and
     incr.getOperand() = v.getAnAccess() and
-    newUB = getFullyConvertedUpperBounds(incr.getOperand())
-  | // Make sure that we round towards +Inf, not to nearest.
-    if (newUB+1)-newUB < 1
-      then result = (newUB+1).nextUp()
-      else result = newUB+1)
+    newUB = getFullyConvertedUpperBounds(incr.getOperand()) and
+    result = addRoundingUpSmall(newUB, 1))
   or
   exists (DecrementOperation decr, float newUB
   | def = decr and