C++: Prepatory simplification.

Author: MathiasVP

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,52 @@ 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
+  result = sub.getLeftOperand()
+}
+
 /**
  * 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) {