C++: Round towards +/- Inf in range analysis

Original author: Kevin Backhouse

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

@@ -469,14 +469,20 @@ float getLowerBoundsImpl(Expr expr) {
   exists (AddExpr addExpr, float xLow, float yLow
   | expr = addExpr and
     xLow = getFullyConvertedLowerBounds(addExpr.getLeftOperand()) and
-    yLow = getFullyConvertedLowerBounds(addExpr.getRightOperand()) and
-    result = xLow+yLow)
+    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)
   or
   exists (SubExpr subExpr, float xLow, float yHigh
   | expr = subExpr and
     xLow = getFullyConvertedLowerBounds(subExpr.getLeftOperand()) and
-    yHigh = getFullyConvertedUpperBounds(subExpr.getRightOperand()) and
-    result = xLow-yHigh)
+    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)
   or
   exists (PrefixIncrExpr incrExpr, float xLow
   | expr = incrExpr and
@@ -485,8 +491,11 @@ float getLowerBoundsImpl(Expr expr) {
   or
   exists (PrefixDecrExpr decrExpr, float xLow
   | expr = decrExpr and
-    xLow = getFullyConvertedLowerBounds(decrExpr.getOperand()) and
-    result = xLow-1)
+    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)
   or
   // `PostfixIncrExpr` and `PostfixDecrExpr` return the value of their
   // operand. The incrementing/decrementing behavior is handled in
@@ -591,19 +600,28 @@ float getUpperBoundsImpl(Expr expr) {
   exists (AddExpr addExpr, float xHigh, float yHigh
   | expr = addExpr and
     xHigh = getFullyConvertedUpperBounds(addExpr.getLeftOperand()) and
-    yHigh = getFullyConvertedUpperBounds(addExpr.getRightOperand()) and
-    result = xHigh+yHigh)
+    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)
   or
   exists (SubExpr subExpr, float xHigh, float yLow
   | expr = subExpr and
     xHigh = getFullyConvertedUpperBounds(subExpr.getLeftOperand()) and
-    yLow = getFullyConvertedLowerBounds(subExpr.getRightOperand()) and
-    result = xHigh-yLow)
+    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)
   or
   exists (PrefixIncrExpr incrExpr, float xHigh
   | expr = incrExpr and
-    xHigh = getFullyConvertedUpperBounds(incrExpr.getOperand()) and
-    result = xHigh+1)
+    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)
   or
   exists (PrefixDecrExpr decrExpr, float xHigh
   | expr = decrExpr and
@@ -795,16 +813,22 @@ float getDefLowerBoundsImpl(RangeSsaDefinition def, LocalScopeVariable v) {
   | def = assignAdd and
     assignAdd.getLValue() = nextDef.getAUse(v) and
     lhsLB = getDefLowerBounds(nextDef, v) and
-    rhsLB = getFullyConvertedLowerBounds(assignAdd.getRValue()) and
-    result = lhsLB + rhsLB)
+    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)
   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()) and
-    result = lhsLB - rhsUB)
+    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)
   or
   exists (IncrementOperation incr, float newLB
   | def = incr and
@@ -815,8 +839,11 @@ float getDefLowerBoundsImpl(RangeSsaDefinition def, LocalScopeVariable v) {
   exists (DecrementOperation decr, float newLB
   | def = decr and
     decr.getOperand() = v.getAnAccess() and
-    newLB = getFullyConvertedLowerBounds(decr.getOperand()) and
-    result = newLB-1)
+    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)
   or
   // Phi nodes.
   result = getPhiLowerBounds(v, def)
@@ -838,22 +865,31 @@ float getDefUpperBoundsImpl(RangeSsaDefinition def, LocalScopeVariable v) {
   | def = assignAdd and
     assignAdd.getLValue() = nextDef.getAUse(v) and
     lhsUB = getDefUpperBounds(nextDef, v) and
-    rhsUB = getFullyConvertedUpperBounds(assignAdd.getRValue()) and
-    result = lhsUB + rhsUB)
+    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)
   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()) and
-    result = lhsUB - rhsLB)
+    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)
   or
   exists (IncrementOperation incr, float newUB
   | def = incr and
     incr.getOperand() = v.getAnAccess() and
-    newUB = getFullyConvertedUpperBounds(incr.getOperand()) and
-    result = newUB+1)
+    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)
   or
   exists (DecrementOperation decr, float newUB
   | def = decr and