Merge pull request #6315 from MathiasVP/fix-off-by-one-in-rem-expr-range-analysis

C++: Fix off–by-one in range analysis for `RemExpr`.

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

@@ -863,16 +863,16 @@ private float getLowerBoundsImpl(Expr expr) {
       result = 0
       or
       // If either input could be negative then the output could be
-      // negative. If so, the lower bound of `x%y` is `-abs(y)`, which is
-      // equal to `min(-y,y)`.
+      // negative. If so, the lower bound of `x%y` is `-abs(y) + 1`, which is
+      // equal to `min(-y + 1,y - 1)`.
       exists(float childLB |
         childLB = getFullyConvertedLowerBounds(remExpr.getAnOperand()) and
         not childLB >= 0
       |
-        result = getFullyConvertedLowerBounds(remExpr.getRightOperand())
+        result = getFullyConvertedLowerBounds(remExpr.getRightOperand()) - 1
         or
         exists(float rhsUB | rhsUB = getFullyConvertedUpperBounds(remExpr.getRightOperand()) |
-          result = -rhsUB
+          result = -rhsUB + 1
         )
       )
     )
@@ -1058,16 +1058,16 @@ private float getUpperBoundsImpl(Expr expr) {
       expr = remExpr and
       rhsUB = getFullyConvertedUpperBounds(remExpr.getRightOperand())
     |
-      result = rhsUB
+      result = rhsUB - 1
       or
       // If the right hand side could be negative then we need to take its
       // absolute value. Since `abs(x) = max(-x,x)` this is equivalent to
       // adding `-rhsLB` to the set of upper bounds.
       exists(float rhsLB |
-        rhsLB = getFullyConvertedLowerBounds(remExpr.getAnOperand()) and
+        rhsLB = getFullyConvertedLowerBounds(remExpr.getRightOperand()) and
         not rhsLB >= 0
       |
-        result = -rhsLB
+        result = -rhsLB + 1
       )
     )
     or

cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/lowerBound.expected

@@ -592,6 +592,8 @@
 | test.c:654:9:654:9 | i | -2147483648 |
 | test.c:658:7:658:7 | u | 0 |
 | test.c:659:9:659:9 | u | 0 |
+| test.c:664:12:664:12 | s | -2147483648 |
+| test.c:665:7:665:8 | s2 | -4 |
 | test.cpp:10:7:10:7 | b | -2147483648 |
 | test.cpp:11:5:11:5 | x | -2147483648 |
 | test.cpp:13:10:13:10 | x | -2147483648 |

cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/test.c

@@ -659,3 +659,8 @@ void guard_bound_out_of_range(void) {
     out(u); // unreachable [BUG: is 0 .. +max]
   }
 }
+
+void test_mod(int s) {
+  int s2 = s % 5;
+  out(s2); // -4 .. 4
+}

cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/upperBound.expected

@@ -592,6 +592,8 @@
 | test.c:654:9:654:9 | i | 2147483647 |
 | test.c:658:7:658:7 | u | 0 |
 | test.c:659:9:659:9 | u | 4294967295 |
+| test.c:664:12:664:12 | s | 2147483647 |
+| test.c:665:7:665:8 | s2 | 4 |
 | test.cpp:10:7:10:7 | b | 2147483647 |
 | test.cpp:11:5:11:5 | x | 2147483647 |
 | test.cpp:13:10:13:10 | x | 2147483647 |