C++: Add range analysis for binary multiplication.

Author: MathiasVP

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

@@ -1062,6 +1062,20 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
         or
         upper = false and delta = D::fromFloat(-D::toFloat(d_max).abs() + 1)
       )
+      or
+      exists(
+        SemZeroBound bLeft, SemZeroBound bRight, D::Delta dLeft, D::Delta dRight, boolean fbeLeft,
+        boolean fbeRight, D::Delta odLeft, D::Delta odRight, SemReason rLeft, SemReason rRight
+      |
+        boundedMulOperand(e, upper, bLeft, true, dLeft, fbeLeft, odLeft, rLeft) and
+        boundedMulOperand(e, upper, bRight, false, dRight, fbeRight, odRight, rRight) and
+        delta = D::fromFloat(D::toFloat(dLeft) * D::toFloat(dRight)) and
+        fromBackEdge = fbeLeft.booleanOr(fbeRight)
+      |
+        b = bLeft and origdelta = odLeft and reason = rLeft
+        or
+        b = bRight and origdelta = odRight and reason = rRight
+      )
     )
   }
 
@@ -1095,4 +1109,100 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
   ) {
     bounded(rem.getRightOperand(), b, delta, upper, fromBackEdge, origdelta, reason)
   }
+
+  /**
+   * Define `cmp(true) = <=` and `cmp(false) >=`.
+   *
+   * Holds if `mul = left * right`, and in order to know if `mul cmp(upper) B + k` (for
+   * some `B` and `k`) we need to know that `left cmp(upperLeft) B1 + k1` and
+   * `right cmp(upperRight) B2 + k2` (for some `B1`, `B2`, `k1`, and `k2`).
+   */
+  pragma[nomagic]
+  private predicate boundedMulOperandCand(
+    SemMulExpr mul, SemExpr left, SemExpr right, boolean upper, boolean upperLeft,
+    boolean upperRight
+  ) {
+    not boundFlowStepMul(mul, _, _) and
+    mul.getLeftOperand() = left and
+    mul.getRightOperand() = right and
+    (
+      semPositive(left) and
+      (
+        // left, right >= 0
+        semPositive(right) and
+        (
+          // max(left * right) = max(left) * max(right)
+          upper = true and
+          upperLeft = true and
+          upperRight = true
+          or
+          // min(left * right) = min(left) * min(right)
+          upper = false and
+          upperLeft = false and
+          upperRight = false
+        )
+        or
+        // left >= 0, right <= 0
+        semNegative(right) and
+        (
+          // max(left * right) = min(left) * max(right)
+          upper = true and
+          upperLeft = false and
+          upperRight = true
+          or
+          // min(left * right) = max(left) * min(right)
+          upper = false and
+          upperLeft = true and
+          upperRight = false
+        )
+      )
+      or
+      semNegative(left) and
+      (
+        // left <= 0, right >= 0
+        semPositive(right) and
+        (
+          // max(left * right) = max(left) * min(right)
+          upper = true and
+          upperLeft = true and
+          upperRight = false
+          or
+          // min(left * right) = min(left) * max(right)
+          upper = false and
+          upperLeft = false and
+          upperRight = true
+        )
+        or
+        // left, right <= 0
+        semNegative(right) and
+        (
+          // max(left * right) = min(left) * min(right)
+          upper = true and
+          upperLeft = false and
+          upperRight = false
+          or
+          // min(left * right) = max(left) * max(right)
+          upper = false and
+          upperLeft = true and
+          upperRight = true
+        )
+      )
+    )
+  }
+
+  pragma[nomagic]
+  private predicate boundedMulOperand(
+    SemMulExpr mul, boolean upper, SemZeroBound b, boolean isLeft, D::Delta delta,
+    boolean fromBackEdge, D::Delta origdelta, SemReason reason
+  ) {
+    exists(boolean upperLeft, boolean upperRight, SemExpr left, SemExpr right |
+      boundedMulOperandCand(mul, left, right, upper, upperLeft, upperRight)
+    |
+      isLeft = true and
+      bounded(left, b, delta, upperLeft, fromBackEdge, origdelta, reason)
+      or
+      isLeft = false and
+      bounded(right, b, delta, upperRight, fromBackEdge, origdelta, reason)
+    )
+  }
 }