C++: Support != constant in range analysis

Author: jbj

cpp/ql/src/semmle/code/cpp/rangeanalysis/SimpleRangeAnalysis.qll

@@ -1160,6 +1160,17 @@ private float getPhiLowerBounds(StackVariable v, RangeSsaDefinition phi) {
     if guardLB > defLB then result = guardLB else result = defLB
   )
   or
+  exists(VariableAccess access, float neConstant, float lower |
+    isNEPhi(v, phi, access, neConstant) and
+    lower = getFullyConvertedLowerBounds(access) and
+    if lower = neConstant then result = lower + 1 else result = lower
+  )
+  or
+  exists(VariableAccess access |
+    isUnsupportedGuardPhi(v, phi, access) and
+    result = getFullyConvertedLowerBounds(access)
+  )
+  or
   result = getDefLowerBounds(phi.getAPhiInput(v), v)
 }
 
@@ -1177,6 +1188,17 @@ private float getPhiUpperBounds(StackVariable v, RangeSsaDefinition phi) {
     if guardUB < defUB then result = guardUB else result = defUB
   )
   or
+  exists(VariableAccess access, float neConstant, float upper |
+    isNEPhi(v, phi, access, neConstant) and
+    upper = getFullyConvertedUpperBounds(access) and
+    if upper = neConstant then result = upper - 1 else result = upper
+  )
+  or
+  exists(VariableAccess access |
+    isUnsupportedGuardPhi(v, phi, access) and
+    result = getFullyConvertedUpperBounds(access)
+  )
+  or
   result = getDefUpperBounds(phi.getAPhiInput(v), v)
 }
 
@@ -1501,22 +1523,13 @@ private predicate linearBoundFromGuard(
   //   1. x <= upperbound(RHS)
   //   2. x >= lowerbound(RHS)
   //
-  // For x != RHS, we create trivial bounds:
-  //
-  //   1. x <= typeUpperBound(RHS.getUnspecifiedType())
-  //   2. x >= typeLowerBound(RHS.getUnspecifiedType())
-  //
-  exists(Expr lhs, Expr rhs, boolean isEQ |
+  exists(Expr lhs, Expr rhs |
     linearAccess(lhs, v, p, q) and
-    eqOpWithSwapAndNegate(guard, lhs, rhs, isEQ, branch) and
+    eqOpWithSwapAndNegate(guard, lhs, rhs, true, branch) and
+    getBounds(rhs, boundValue, isLowerBound) and
     strictness = Nonstrict()
-  |
-    // True branch
-    isEQ = true and getBounds(rhs, boundValue, isLowerBound)
-    or
-    // False branch: set the bounds to the min/max for the type.
-    isEQ = false and exprTypeBounds(rhs, boundValue, isLowerBound)
   )
+  // x != RHS and !x are handled elsewhere
 }
 
 /** Utility for `linearBoundFromGuard`. */
@@ -1533,6 +1546,42 @@ private predicate exprTypeBounds(Expr expr, float boundValue, boolean isLowerBou
   isLowerBound = false and boundValue = exprMaxVal(expr.getFullyConverted())
 }
 
+/**
+ * Holds if `(v, phi)` ensures that `access` is not equal to `neConstant`. For
+ * example, the condition `if (x + 1 != 3)` ensures that `x` is not equal to 2.
+ * Only integral types are supported.
+ */
+private predicate isNEPhi(
+  Variable v, RangeSsaDefinition phi, VariableAccess access, float neConstant
+) {
+  exists(
+    ComparisonOperation cmp, boolean branch, Expr linearExpr, Expr rExpr, float p, float q, float r
+  |
+    access.getTarget() = v and
+    phi.isGuardPhi(access, cmp, branch) and
+    eqOpWithSwapAndNegate(cmp, linearExpr, rExpr, false, branch) and
+    v.getUnspecifiedType() instanceof IntegralOrEnumType and // Float `!=` is too imprecise
+    r = getValue(rExpr).toFloat() and
+    linearAccess(linearExpr, access, p, q) and
+    neConstant = (r - q) / p
+  )
+}
+
+/**
+ * Holds if `(v, phi)` constrains the value of `access` but in a way that
+ * doesn't allow this library to constrain the upper or lower bounds of
+ * `access`. An example is `if (x != y)` if neither `x` nor `y` is a
+ * compile-time constant.
+ */
+private predicate isUnsupportedGuardPhi(Variable v, RangeSsaDefinition phi, VariableAccess access) {
+  exists(ComparisonOperation cmp, boolean branch |
+    access.getTarget() = v and
+    phi.isGuardPhi(access, cmp, branch) and
+    eqOpWithSwapAndNegate(cmp, _, _, false, branch) and
+    not isNEPhi(v, phi, access, _)
+  )
+}
+
 cached
 private module SimpleRangeAnalysisCached {
   /**

cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/lowerBound.expected

@@ -536,33 +536,33 @@
 | test.c:541:7:541:7 | n | 0 |
 | test.c:542:9:542:9 | n | 1 |
 | test.c:545:7:545:7 | n | 0 |
-| test.c:546:9:546:9 | n | 0 |
+| test.c:546:9:546:9 | n | 1 |
 | test.c:548:9:548:9 | n | 0 |
 | test.c:551:8:551:8 | n | 0 |
 | test.c:552:9:552:9 | n | 0 |
 | test.c:554:9:554:9 | n | 0 |
 | test.c:557:10:557:10 | n | 0 |
-| test.c:558:5:558:5 | n | 0 |
+| test.c:558:5:558:5 | n | 1 |
 | test.c:561:7:561:7 | n | 0 |
 | test.c:565:7:565:7 | n | -32768 |
 | test.c:568:7:568:7 | n | 0 |
 | test.c:569:9:569:9 | n | 0 |
-| test.c:571:9:571:9 | n | 0 |
+| test.c:571:9:571:9 | n | 1 |
 | test.c:574:7:574:7 | n | 0 |
 | test.c:575:9:575:9 | n | 0 |
 | test.c:577:9:577:9 | n | 0 |
-| test.c:580:10:580:10 | n | -32768 |
-| test.c:581:5:581:5 | n | -32768 |
+| test.c:580:10:580:10 | n | 0 |
+| test.c:581:5:581:5 | n | 1 |
 | test.c:584:7:584:7 | n | 0 |
 | test.c:588:7:588:7 | n | -32768 |
 | test.c:589:9:589:9 | n | -32768 |
 | test.c:590:11:590:11 | n | 0 |
 | test.c:594:7:594:7 | n | -32768 |
 | test.c:595:13:595:13 | n | 5 |
-| test.c:598:9:598:9 | n | 5 |
+| test.c:598:9:598:9 | n | 6 |
 | test.c:601:7:601:7 | n | -32768 |
-| test.c:601:22:601:22 | n | -32768 |
-| test.c:602:9:602:9 | n | -32768 |
+| test.c:601:22:601:22 | n | -32767 |
+| test.c:602:9:602:9 | n | -32766 |
 | test.cpp:10:7:10:7 | b | -2147483648 |
 | test.cpp:11:5:11:5 | x | -2147483648 |
 | test.cpp:13:10:13:10 | x | -2147483648 |

cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/test.c

@@ -543,7 +543,7 @@ int notequal_type_endpoint(unsigned n) {
   }
 
   if (n != 0) {
-    out(n); // 1 .. [BUG: lower bound is deduced to be 0]
+    out(n); // 1 ..
   } else {
     out(n); // 0 .. 0
   }
@@ -555,7 +555,7 @@ int notequal_type_endpoint(unsigned n) {
   }
 
   while (n != 0) {
-    n--; // 1 .. [BUG: lower bound is deduced to be 0]
+    n--; // 1 ..
   }
 
   out(n); // 0 .. 0
@@ -568,7 +568,7 @@ void notequal_refinement(short n) {
   if (n == 0) {
     out(n); // 0 .. 0
   } else {
-    out(n); // 1 .. [BUG: lower bound is deduced to be 0]
+    out(n); // 1 ..
   }
 
   if (n) {
@@ -578,7 +578,7 @@ void notequal_refinement(short n) {
   }
 
   while (n != 0) {
-    n--; // 1 .. [BUG: lower bound is deduced to be -32768]
+    n--; // 1 ..
   }
 
   out(n); // 0 .. 0
@@ -595,10 +595,10 @@ void notequal_variations(short n, float f) {
     if (2 * n - 10 == 0) { // Same as `n == 10/2` (modulo overflow)
       return;
     }
-    out(n); // 6 .. [BUG: lower bound is deduced to be 5]
+    out(n); // 6 ..
   }
 
   if (n != -32768 && n != -32767) {
-    out(n); // -32766 .. [BUG: lower bound is deduced to be -32768]
+    out(n); // -32766 ..
   }
 }