Merge pull request #13972 from MathiasVP/range-analysis-for-sub-expr

C++: Support subtraction in the new range analysis
2025-12-22 11:46:32 +01:00 · 2023-08-16 11:51:11 +01:00
parent c55b0982f7 49a5a39395
commit 986aa74db7
5 changed files with 88 additions and 46 deletions
--- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisStage.qll
+++ b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisStage.qll
@@ -574,16 +574,6 @@ module RangeStage<
    )
  }

-  /** Holds if `e >= 1` as determined by sign analysis. */
-  private predicate strictlyPositiveIntegralExpr(SemExpr e) {
-    semStrictlyPositive(e) and getTrackedType(e) instanceof SemIntegerType
-  }
-
-  /** Holds if `e <= -1` as determined by sign analysis. */
-  private predicate strictlyNegativeIntegralExpr(SemExpr e) {
-    semStrictlyNegative(e) and getTrackedType(e) instanceof SemIntegerType
-  }
-
  /**
   * Holds if `e1 + delta` is a valid bound for `e2`.
   * - `upper = true`  : `e2 <= e1 + delta`
@@ -597,27 +587,6 @@ module RangeStage<
    delta = D::fromInt(0) and
    (upper = true or upper = false)
    or
-    exists(SemExpr x, SemSubExpr sub |
-      e2 = sub and
-      sub.getLeftOperand() = e1 and
-      sub.getRightOperand() = x
-    |
-      // `x instanceof ConstantIntegerExpr` is covered by valueFlowStep
-      not x instanceof SemConstantIntegerExpr and
-      if strictlyPositiveIntegralExpr(x)
-      then upper = true and delta = D::fromInt(-1)
-      else
-        if semPositive(x)
-        then upper = true and delta = D::fromInt(0)
-        else
-          if strictlyNegativeIntegralExpr(x)
-          then upper = false and delta = D::fromInt(1)
-          else
-            if semNegative(x)
-            then upper = false and delta = D::fromInt(0)
-            else none()
-    )
-    or
    e2.(SemRemExpr).getRightOperand() = e1 and
    semPositive(e1) and
    delta = D::fromInt(-1) and
@@ -1137,6 +1106,30 @@ module RangeStage<
        b = bRight and origdelta = odRight and reason = rRight and bLeft instanceof SemZeroBound
      )
      or
+      exists(
+        D::Delta dLeft, D::Delta dRight, boolean fbeLeft, boolean fbeRight, D::Delta odLeft,
+        D::Delta odRight, SemReason rLeft, SemReason rRight
+      |
+        boundedSubOperandLeft(e, upper, b, dLeft, fbeLeft, odLeft, rLeft) and
+        boundedSubOperandRight(e, upper, dRight, fbeRight, odRight, rRight) and
+        // when `upper` is `true` we have:
+        // left <= b + dLeft
+        // right >= 0 + dRight
+        // left - right <= b + dLeft - (0 + dRight)
+        //               = b + (dLeft - dRight)
+        // and when `upper` is `false` we have:
+        // left >= b + dLeft
+        // right <= 0 + dRight
+        // left - right >= b + dLeft - (0 + dRight)
+        //               = b + (dLeft - dRight)
+        delta = D::fromFloat(D::toFloat(dLeft) - D::toFloat(dRight)) and
+        fromBackEdge = fbeLeft.booleanOr(fbeRight)
+      |
+        origdelta = odLeft and reason = rLeft
+        or
+        origdelta = odRight and reason = rRight
+      )
+      or
      exists(
        SemRemExpr rem, D::Delta d_max, D::Delta d1, D::Delta d2, boolean fbe1, boolean fbe2,
        D::Delta od1, D::Delta od2, SemReason r1, SemReason r2
@@ -1201,6 +1194,38 @@ module RangeStage<
    )
  }

+  /**
+   * Holds if `sub = left - right` and `left <= b + delta` if `upper` is `true`
+   * and `left >= b + delta` is `upper` is `false`.
+   */
+  pragma[nomagic]
+  private predicate boundedSubOperandLeft(
+    SemSubExpr sub, boolean upper, SemBound b, D::Delta delta, boolean fromBackEdge,
+    D::Delta origdelta, SemReason reason
+  ) {
+    // `semValueFlowStep` already handles the case where one of the operands is a constant.
+    not semValueFlowStep(sub, _, _) and
+    bounded(sub.getLeftOperand(), b, delta, upper, fromBackEdge, origdelta, reason)
+  }
+
+  /**
+   * Holds if `sub = left - right` and `right <= 0 + delta` if `upper` is `false`
+   * and `right >= 0 + delta` is `upper` is `true`.
+   *
+   * Note that the boolean value of `upper` is flipped compared to many other predicates in
+   * this file. This ensures a clean join at the call-site.
+   */
+  pragma[nomagic]
+  private predicate boundedSubOperandRight(
+    SemSubExpr sub, boolean upper, D::Delta delta, boolean fromBackEdge, D::Delta origdelta,
+    SemReason reason
+  ) {
+    // `semValueFlowStep` already handles the case where one of the operands is a constant.
+    not semValueFlowStep(sub, _, _) and
+    bounded(sub.getRightOperand(), any(SemZeroBound zb), delta, upper.booleanNot(), fromBackEdge,
+      origdelta, reason)
+  }
+
  pragma[nomagic]
  private predicate boundedRemExpr(
    SemRemExpr rem, boolean upper, D::Delta delta, boolean fromBackEdge, D::Delta origdelta,
--- a/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/constant-size/ConstantSizeArrayOffByOne.expected
+++ b/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/constant-size/ConstantSizeArrayOffByOne.expected
@@ -69,12 +69,6 @@ edges
 | test.cpp:322:19:322:27 | ... + ... | test.cpp:325:24:325:26 | end |
 | test.cpp:324:23:324:26 | temp | test.cpp:324:23:324:32 | ... + ... |
 | test.cpp:324:23:324:32 | ... + ... | test.cpp:325:15:325:19 | temp2 |
-| test.cpp:351:9:351:11 | arr | test.cpp:351:9:351:14 | access to array |
-| test.cpp:351:9:351:11 | arr | test.cpp:351:18:351:25 | access to array |
-| test.cpp:351:18:351:20 | arr | test.cpp:351:9:351:14 | access to array |
-| test.cpp:351:18:351:20 | arr | test.cpp:351:18:351:25 | access to array |
-| test.cpp:351:29:351:31 | arr | test.cpp:351:9:351:14 | access to array |
-| test.cpp:351:29:351:31 | arr | test.cpp:351:18:351:25 | access to array |
 nodes
 | test.cpp:34:5:34:24 | access to array | semmle.label | access to array |
 | test.cpp:34:10:34:12 | buf | semmle.label | buf |
@@ -167,11 +161,6 @@ nodes
 | test.cpp:325:15:325:19 | temp2 | semmle.label | temp2 |
 | test.cpp:325:24:325:26 | end | semmle.label | end |
 | test.cpp:325:24:325:26 | end | semmle.label | end |
-| test.cpp:351:9:351:11 | arr | semmle.label | arr |
-| test.cpp:351:9:351:14 | access to array | semmle.label | access to array |
-| test.cpp:351:18:351:20 | arr | semmle.label | arr |
-| test.cpp:351:18:351:25 | access to array | semmle.label | access to array |
-| test.cpp:351:29:351:31 | arr | semmle.label | arr |
 subpaths
 #select
 | test.cpp:35:5:35:22 | PointerAdd: access to array | test.cpp:35:10:35:12 | buf | test.cpp:35:5:35:22 | access to array | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:15:9:15:11 | buf | buf | test.cpp:35:5:35:26 | Store: ... = ... | write |
@@ -194,6 +183,3 @@ subpaths
 | test.cpp:322:19:322:27 | PointerAdd: ... + ... | test.cpp:322:19:322:22 | temp | test.cpp:325:24:325:26 | end | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:314:10:314:13 | temp | temp | test.cpp:330:13:330:24 | Store: ... = ... | write |
 | test.cpp:322:19:322:27 | PointerAdd: ... + ... | test.cpp:322:19:322:22 | temp | test.cpp:325:24:325:26 | end | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:314:10:314:13 | temp | temp | test.cpp:331:13:331:24 | Store: ... = ... | write |
 | test.cpp:322:19:322:27 | PointerAdd: ... + ... | test.cpp:322:19:322:22 | temp | test.cpp:325:24:325:26 | end | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:314:10:314:13 | temp | temp | test.cpp:333:13:333:24 | Store: ... = ... | write |
-| test.cpp:351:18:351:25 | PointerAdd: access to array | test.cpp:351:9:351:11 | arr | test.cpp:351:18:351:25 | access to array | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:348:9:348:11 | arr | arr | test.cpp:351:18:351:25 | Load: access to array | read |
-| test.cpp:351:18:351:25 | PointerAdd: access to array | test.cpp:351:18:351:20 | arr | test.cpp:351:18:351:25 | access to array | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:348:9:348:11 | arr | arr | test.cpp:351:18:351:25 | Load: access to array | read |
-| test.cpp:351:18:351:25 | PointerAdd: access to array | test.cpp:351:29:351:31 | arr | test.cpp:351:18:351:25 | access to array | This pointer arithmetic may have an off-by-1 error allowing it to overrun $@ at this $@. | test.cpp:348:9:348:11 | arr | arr | test.cpp:351:18:351:25 | Load: access to array | read |
--- a/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/constant-size/test.cpp
+++ b/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/constant-size/test.cpp
@@ -348,7 +348,7 @@ int positiveRange(int x) {
    int arr[128];

    for(int i=127-offset; i>= 0; i--) {
-        arr[i] = arr[i+1] + arr[i+offset]; // GOOD [FALSE POSITIVE]
+        arr[i] = arr[i+1] + arr[i+offset]; // GOOD
    }
    return arr[0];
 }
--- a/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/pointer-deref/test.cpp
+++ b/cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/pointer-deref/test.cpp
@@ -733,3 +733,12 @@ void test36(unsigned size, unsigned n) {
    *end = 0; // $ deref=L733 // BAD
  }
 }
+
+void test37(unsigned long n)
+{
+  int *p = new int[n];
+  for (unsigned long i = n; i != 0u; i--)
+  {
+    p[n - i] = 0; // GOOD
+  }
+}
--- a/cpp/ql/test/library-tests/ir/range-analysis/test.cpp
+++ b/cpp/ql/test/library-tests/ir/range-analysis/test.cpp
@@ -95,3 +95,25 @@ void gotoLoop(bool b1, bool b2)
    }
  }
 }
+
+void test_sub(int x, int y, int n) {
+  if(x > 0 && x < 500) {
+    if(y > 0 && y < 10) {
+      range(x - y); // $ range=<=498 range=>=-8
+    }
+
+    if(n > 0 && n < 100) {
+      for (int i = 0; i < n; i++)
+      {
+        range(n - i); // $ range=">=Phi: i-97" range=<=99 range=>=-97
+        range(i - n); // $ range="<=Phi: i-1" range=">=Phi: i-99" range=<=97 range=>=-99 
+      }
+
+      for (int i = n; i != 0; i--)
+      {
+        range(n - i); // $ SPURIOUS: overflow=+
+        range(i - n); // $ range=">=Phi: i-99"
+      }
+    }
+  }
+}