C++: Improve bounds from inequalities on integers

2026-02-12 05:01:06 +01:00 · 2025-10-04 16:46:50 +02:00
parent 9af432d2f9
commit 3a135888c7
5 changed files with 52 additions and 24 deletions
--- a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/SimpleRangeAnalysis.qll
+++ b/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())
  )
 }
--- a/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/lowerBound.expected
+++ b/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 |
--- a/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/ternaryLower.expected
+++ b/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 |
--- a/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/ternaryUpper.expected
+++ b/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 |
--- a/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/upperBound.expected
+++ b/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 |