Merge pull request #16988 from MathiasVP/unsigned-difference-compares-eq-zero-fp-fixes

C++: Fix FPs in `cpp/unsigned-difference-expression-compared-zero`

cpp/ql/src/Security/CWE/CWE-191/UnsignedDifferenceExpressionComparedZero.ql

@@ -17,6 +17,7 @@ import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis
 import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils
 import semmle.code.cpp.controlflow.Guards
 import semmle.code.cpp.ir.dataflow.DataFlow
+import semmle.code.cpp.valuenumbering.GlobalValueNumbering
 
 /**
  *  Holds if `sub` is guarded by a condition which ensures that
@@ -33,46 +34,109 @@ predicate isGuarded(SubExpr sub, Expr left, Expr right) {
   )
 }
 
+/**
+ * Gets an expression that is less than or equal to `sub.getLeftOperand()`.
+ * These serve as the base cases for `exprIsSubLeftOrLess`.
+ */
+Expr exprIsLeftOrLessBase(SubExpr sub) {
+  interestingSubExpr(sub, _) and // Manual magic
+  exists(Expr e | globalValueNumber(e).getAnExpr() = sub.getLeftOperand() |
+    // sub = e - x
+    // result = e
+    // so:
+    // result <= e
+    result = e
+    or
+    // sub = e - x
+    // result = e & y
+    // so:
+    // result = e & y <= e
+    result.(BitwiseAndExpr).getAnOperand() = e
+    or
+    exists(SubExpr s |
+      // sub = e - x
+      // result = s
+      // s = e - y
+      // y >= 0
+      // so:
+      // result = e - y <= e
+      result = s and
+      s.getLeftOperand() = e and
+      lowerBound(s.getRightOperand().getFullyConverted()) >= 0
+    )
+    or
+    exists(Expr other |
+      // sub = e - x
+      // result = a
+      // a = e + y
+      // y <= 0
+      // so:
+      // result = e + y <= e + 0 = e
+      result.(AddExpr).hasOperands(e, other) and
+      upperBound(other.getFullyConverted()) <= 0
+    )
+    or
+    exists(DivExpr d |
+      // sub = e - x
+      // result = d
+      // d = e / y
+      // y >= 1
+      // so:
+      // result = e / y <= e / 1 = e
+      result = d and
+      d.getLeftOperand() = e and
+      lowerBound(d.getRightOperand().getFullyConverted()) >= 1
+    )
+    or
+    exists(RShiftExpr rs |
+      // sub = e - x
+      // result = rs
+      // rs = e >> y
+      // so:
+      // result = e >> y <= e
+      result = rs and
+      rs.getLeftOperand() = e
+    )
+  )
+}
+
 /**
  * Holds if `n` is known or suspected to be less than or equal to
  * `sub.getLeftOperand()`.
  */
 predicate exprIsSubLeftOrLess(SubExpr sub, DataFlow::Node n) {
-  interestingSubExpr(sub, _) and // Manual magic
-  (
-    n.asExpr() = sub.getLeftOperand()
-    or
-    exists(DataFlow::Node other |
-      // dataflow
-      exprIsSubLeftOrLess(sub, other) and
-      (
-        DataFlow::localFlowStep(n, other) or
-        DataFlow::localFlowStep(other, n)
-      )
-    )
-    or
-    exists(DataFlow::Node other |
-      // guard constraining `sub`
-      exprIsSubLeftOrLess(sub, other) and
-      isGuarded(sub, other.asExpr(), n.asExpr()) // other >= n
-    )
-    or
-    exists(DataFlow::Node other, float p, float q |
-      // linear access of `other`
-      exprIsSubLeftOrLess(sub, other) and
-      linearAccess(n.asExpr(), other.asExpr(), p, q) and // n = p * other + q
-      p <= 1 and
-      q <= 0
-    )
-    or
-    exists(DataFlow::Node other, float p, float q |
-      // linear access of `n`
-      exprIsSubLeftOrLess(sub, other) and
-      linearAccess(other.asExpr(), n.asExpr(), p, q) and // other = p * n + q
-      p >= 1 and
-      q >= 0
+  n.asExpr() = exprIsLeftOrLessBase(sub)
+  or
+  exists(DataFlow::Node other |
+    // dataflow
+    exprIsSubLeftOrLess(sub, other) and
+    (
+      DataFlow::localFlowStep(n, other) or
+      DataFlow::localFlowStep(other, n)
     )
   )
+  or
+  exists(DataFlow::Node other |
+    // guard constraining `sub`
+    exprIsSubLeftOrLess(sub, other) and
+    isGuarded(sub, other.asExpr(), n.asExpr()) // other >= n
+  )
+  or
+  exists(DataFlow::Node other, float p, float q |
+    // linear access of `other`
+    exprIsSubLeftOrLess(sub, other) and
+    linearAccess(n.asExpr(), other.asExpr(), p, q) and // n = p * other + q
+    p <= 1 and
+    q <= 0
+  )
+  or
+  exists(DataFlow::Node other, float p, float q |
+    // linear access of `n`
+    exprIsSubLeftOrLess(sub, other) and
+    linearAccess(other.asExpr(), n.asExpr(), p, q) and // other = p * n + q
+    p >= 1 and
+    q >= 0
+  )
 }
 
 predicate interestingSubExpr(SubExpr sub, RelationalOperation ro) {

cpp/ql/src/change-notes/2024-07-16-unsigned-difference-expression-compared-zero-.md

@@ -0,0 +1,4 @@
+---
+category: minorAnalysis
+---
+* The `cpp/unsigned-difference-expression-compared-zero` ("Unsigned difference expression compared to zero") query now produces fewer false positives.

cpp/ql/test/query-tests/Security/CWE/CWE-191/UnsignedDifferenceExpressionComparedZero/UnsignedDifferenceExpressionComparedZero.expected

@@ -14,3 +14,4 @@
 | test.cpp:276:11:276:19 | ... > ... | Unsigned subtraction can never be negative. |
 | test.cpp:288:10:288:18 | ... > ... | Unsigned subtraction can never be negative. |
 | test.cpp:312:9:312:25 | ... > ... | Unsigned subtraction can never be negative. |
+| test.cpp:362:8:362:16 | ... > ... | Unsigned subtraction can never be negative. |

cpp/ql/test/query-tests/Security/CWE/CWE-191/UnsignedDifferenceExpressionComparedZero/test.cpp

@@ -321,3 +321,57 @@ void test19() {
 		total += get_data();
 	}
 }
+
+void test20(int a, bool b, unsigned long c)
+{
+  int x = 0;
+
+  if(b) {
+    x = (a - c) / 2;
+  } else {
+    x = a - c;
+  }
+
+  if (a - c - x > 0) // GOOD
+  {
+  }
+}
+
+uint32_t get_uint32();
+int64_t get_int64();
+
+void test21(unsigned long a)
+{
+  {
+    int b = a & get_int64();
+    if (a - b > 0) { } // GOOD
+  }
+
+  {
+  int b = a - get_uint32();
+  if(a - b > 0) { } // GOOD
+  }
+
+  {
+    int64_t c = get_int64();
+    if(c <= 0) {
+      int64_t b = (int64_t)a + c;
+      if(a - b > 0) { } // GOOD
+    }
+    int64_t b = (int64_t)a + c;
+    if(a - b > 0) { } // BAD
+  }
+
+  {
+    unsigned c = get_uint32();
+    if(c >= 1) {
+      int b = a / c;
+      if(a - b > 0) { } // GOOD
+    }
+  }
+
+  {
+    int b = a >> get_uint32();
+    if(a - b > 0) { } // GOOD
+  }
+}