Merge pull request github#13226 from rdmarsh2/rdmarsh2/cpp/cobo-neq-refinement

C++: fix equality refinement in new range analysis

Author: MathiasVP

cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisStage.qll

@@ -729,7 +729,7 @@ module RangeStage<
   ) {
     exists(SemExpr e, D::Delta d1, D::Delta d2 |
       unequalFlowStepIntegralSsa(v, pos, e, d1, reason) and
-      boundedUpper(e, b, d1) and
+      boundedUpper(e, b, d2) and
       boundedLower(e, b, d2) and
       delta = D::fromFloat(D::toFloat(d1) + D::toFloat(d2))
     )

cpp/ql/test/experimental/query-tests/Security/CWE/CWE-193/constant-size/test.cpp

@@ -78,3 +78,36 @@ void testInterproc(BigArray *arr) {
 
     addToPointerAndAssign(arr->buf);
 }
+
+void testEqRefinement() {
+    int arr[MAX_SIZE];
+
+    for(int i = 0; i <= MAX_SIZE; i++) {
+        if(i != MAX_SIZE) {
+            arr[i] = 0; // GOOD
+        }
+    }
+}
+
+void testEqRefinement2() {
+    int arr[MAX_SIZE];
+
+    int n = 0;
+
+    for(int i = 0; i <= MAX_SIZE; i++) {
+        if(n == 0) {
+            if(i == MAX_SIZE) {
+                break;
+            }
+            n = arr[i]; // GOOD
+            continue;
+        }
+
+        if (i == MAX_SIZE || n != arr[i]) {
+            if (i == MAX_SIZE) {
+                break;
+            }
+            n = arr[i]; // GOOD
+        }
+    }
+}

cpp/ql/test/library-tests/ir/range-analysis/test.cpp

@@ -59,3 +59,14 @@
       range(i); // $ range=>=0 SPURIOUS: range="<=call to f3_get-1" range="<=call to f3_get-2"
     }
   }
+
+int f4(int x) {
+  for (int i = 0; i <= 100; i++) {
+    range(i); // $ range=<=100 range=>=0
+    if(i == 100) {
+      range(i); // $ range===100
+    } else {
+      range(i); // $ range=<=99 range=>=0
+    }
+  }
+}