C++: Add support for bounded modulus operations

cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/RangeAnalysisStage.qll

@@ -1039,6 +1039,28 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
         or
         b = bRight and origdelta = odRight and reason = rRight and bLeft instanceof SemZeroBound
       )
+      or
+      exists(
+        SemRemExpr rem, SemZeroBound b1, SemZeroBound b2, D::Delta d_max, D::Delta d1, D::Delta d2,
+        boolean fbe1, boolean fbe2, D::Delta od1, D::Delta od2, SemReason r1, SemReason r2
+      |
+        rem = e and
+        boundedRemExpr(rem, b1, true, d1, fbe1, od1, r1) and
+        boundedRemExpr(rem, b2, false, d2, fbe2, od2, r2) and
+        (
+          if D::toFloat(d1).abs() > D::toFloat(d2).abs()
+          then (
+            b = b1 and d_max = d1 and fromBackEdge = fbe1 and origdelta = od1 and reason = r1
+          ) else (
+            b = b2 and d_max = d2 and fromBackEdge = fbe2 and origdelta = od2 and reason = r2
+          )
+        ) and
+        (
+          upper = true and delta = D::fromFloat(D::toFloat(d_max).abs() - 1)
+          or
+          upper = false and delta = D::fromFloat(-D::toFloat(d_max).abs() + 1)
+        )
+      )
     )
   }
 
@@ -1065,4 +1087,11 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
       bounded(add.getRightOperand(), b, delta, upper, fromBackEdge, origdelta, reason)
     )
   }
+
+  private predicate boundedRemExpr(
+    SemRemExpr rem, SemZeroBound b, boolean upper, D::Delta delta, boolean fromBackEdge,
+    D::Delta origdelta, SemReason reason
+  ) {
+    bounded(rem.getRightOperand(), b, delta, upper, fromBackEdge, origdelta, reason)
+  }
 }