C++: Improve bounds from inequalities on integers

Author: paldepind

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

@@ -1709,6 +1709,22 @@ predicate nonNanGuardedVariable(Expr guard, VariableAccess v, boolean branch) {
   nanExcludingComparison(guard, branch)
 }
 
+/**
+ * Adjusts a lower bound to its meaning for integral types.
+ *
+ * Examples:
+ * `>= 3.0` becomes `3.0`
+ * ` > 3.0` becomes `4.0`
+ * `>= 3.5` becomes `4.0`
+ * ` > 3.5` becomes `4.0`
+ */
+bindingset[strictness, lb]
+private float adjustLowerBoundIntegral(RelationStrictness strictness, float lb) {
+  if strictness = Nonstrict() and lb.floorFloat() = lb
+  then result = lb
+  else result = lb.floorFloat() + 1
+}
+
 /**
  * If the guard is a comparison of the form `p*v + q <CMP> r`, then this
  * predicate uses the bounds information for `r` to compute a lower bound
@@ -1720,15 +1736,29 @@ private predicate lowerBoundFromGuard(Expr guard, VariableAccess v, float lb, bo
   |
     if nonNanGuardedVariable(guard, v, branch)
     then
-      if
-        strictness = Nonstrict() or
-        not getVariableRangeType(v.getTarget()) instanceof IntegralType
-      then lb = childLB
-      else lb = childLB + 1
+      if getVariableRangeType(v.getTarget()) instanceof IntegralType
+      then lb = adjustLowerBoundIntegral(strictness, childLB)
+      else lb = childLB
     else lb = varMinVal(v.getTarget())
   )
 }
 
+/**
+ * Adjusts an upper bound to its meaning for integral types.
+ *
+ * Examples:
+ * `<= 3.0` becomes `3.0`
+ * ` < 3.0` becomes `2.0`
+ * `<= 3.5` becomes `3.0`
+ * ` < 3.5` becomes `3.0`
+ */
+bindingset[strictness, ub]
+private float adjustUpperBoundIntegral(RelationStrictness strictness, float ub) {
+  if strictness = Nonstrict() and ub.ceilFloat() = ub
+  then result = ub
+  else result = ub.ceilFloat() - 1
+}
+
 /**
  * If the guard is a comparison of the form `p*v + q <CMP> r`, then this
  * predicate uses the bounds information for `r` to compute a upper bound
@@ -1740,11 +1770,9 @@ private predicate upperBoundFromGuard(Expr guard, VariableAccess v, float ub, bo
   |
     if nonNanGuardedVariable(guard, v, branch)
     then
-      if
-        strictness = Nonstrict() or
-        not getVariableRangeType(v.getTarget()) instanceof IntegralType
-      then ub = childUB
-      else ub = childUB - 1
+      if getVariableRangeType(v.getTarget()) instanceof IntegralType
+      then ub = adjustUpperBoundIntegral(strictness, childUB)
+      else ub = childUB
     else ub = varMaxVal(v.getTarget())
   )
 }

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

@@ -353,19 +353,19 @@
 | test.c:341:32:341:34 | odd | 9007199254740991 |
 | test.c:343:10:343:16 | shifted | 4503599627370495 |
 | test.c:348:27:348:27 | e | 0 |
-| test.c:348:40:348:40 | e | 0.5 |
+| test.c:348:40:348:40 | e | 0 |
 | test.c:349:25:349:25 | e | 0 |
 | test.c:349:39:349:39 | e | 0 |
 | test.c:350:27:350:27 | e | 0 |
-| test.c:350:40:350:40 | e | 0.333333 |
+| test.c:350:40:350:40 | e | 0 |
 | test.c:351:27:351:27 | e | 0 |
-| test.c:351:40:351:40 | e | 0.5 |
+| test.c:351:40:351:40 | e | 0 |
 | test.c:352:27:352:27 | e | 0 |
-| test.c:352:41:352:41 | e | 8.5 |
-| test.c:354:10:354:12 | bi1 | 0.5 |
+| test.c:352:41:352:41 | e | 8 |
+| test.c:354:10:354:12 | bi1 | 0 |
 | test.c:354:16:354:18 | bi2 | 0 |
-| test.c:354:22:354:24 | bi3 | 0.333333 |
-| test.c:354:28:354:30 | bi4 | 0.5 |
+| test.c:354:22:354:24 | bi3 | 0 |
+| test.c:354:28:354:30 | bi4 | 0 |
 | test.c:354:34:354:36 | bi5 | 2 |
 | test.c:359:7:359:7 | x | -2147483648 |
 | test.c:363:10:363:10 | i | 0 |

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

@@ -1,9 +1,9 @@
 | test.c:154:10:154:40 | ... ? ... : ... | -1.0 | 1.0 | -1.0 |
-| test.c:348:22:348:44 | ... ? ... : ... | 0.5 | 0.5 | 2.0 |
+| test.c:348:22:348:44 | ... ? ... : ... | 0.0 | 0.0 | 2.0 |
 | test.c:349:20:349:43 | ... ? ... : ... | 0.0 | 0.0 | 2.0 |
-| test.c:350:22:350:44 | ... ? ... : ... | 0.33333333333333337 | 0.33333333333333337 | 2.0 |
-| test.c:351:22:351:44 | ... ? ... : ... | 0.5 | 0.5 | 2.0 |
-| test.c:352:22:352:45 | ... ? ... : ... | 2.0 | 8.5 | 2.0 |
+| test.c:350:22:350:44 | ... ? ... : ... | 0.0 | 0.0 | 2.0 |
+| test.c:351:22:351:44 | ... ? ... : ... | 0.0 | 0.0 | 2.0 |
+| test.c:352:22:352:45 | ... ? ... : ... | 2.0 | 8.0 | 2.0 |
 | test.c:378:8:378:23 | ... ? ... : ... | 0.0 | 0.0 | 10.0 |
 | test.c:379:8:379:24 | ... ? ... : ... | 0.0 | 10.0 | 0.0 |
 | test.c:387:10:387:15 | ... ? ... : ... | 0.0 | 0.0 | 5.0 |

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

@@ -1,7 +1,7 @@
 | test.c:154:10:154:40 | ... ? ... : ... | 2.147483647E9 | 2.147483647E9 | -1.0 |
 | test.c:348:22:348:44 | ... ? ... : ... | 2.147483647E9 | 2.147483647E9 | 2.0 |
 | test.c:349:20:349:43 | ... ? ... : ... | 2.147483647E9 | 2.147483647E9 | 2.0 |
-| test.c:350:22:350:44 | ... ? ... : ... | 1.4316557643333333E9 | 1.4316557643333333E9 | 2.0 |
+| test.c:350:22:350:44 | ... ? ... : ... | 1.431655764E9 | 1.431655764E9 | 2.0 |
 | test.c:351:22:351:44 | ... ? ... : ... | 2.147483647E9 | 2.147483647E9 | 2.0 |
 | test.c:352:22:352:45 | ... ? ... : ... | 2.147483647E9 | 2.147483647E9 | 2.0 |
 | test.c:378:8:378:23 | ... ? ... : ... | 99.0 | 99.0 | 10.0 |

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

@@ -357,14 +357,14 @@
 | test.c:349:25:349:25 | e | 4294967295 |
 | test.c:349:39:349:39 | e | 2147483647 |
 | test.c:350:27:350:27 | e | 4294967295 |
-| test.c:350:40:350:40 | e | 1431655764.333333 |
+| test.c:350:40:350:40 | e | 1431655764 |
 | test.c:351:27:351:27 | e | 4294967295 |
 | test.c:351:40:351:40 | e | 2147483647 |
 | test.c:352:27:352:27 | e | 4294967295 |
 | test.c:352:41:352:41 | e | 2147483647 |
 | test.c:354:10:354:12 | bi1 | 2147483647 |
 | test.c:354:16:354:18 | bi2 | 2147483647 |
-| test.c:354:22:354:24 | bi3 | 1431655764.333333 |
+| test.c:354:22:354:24 | bi3 | 1431655764 |
 | test.c:354:28:354:30 | bi4 | 2147483647 |
 | test.c:354:34:354:36 | bi5 | 2147483647 |
 | test.c:359:7:359:7 | x | 2147483647 |