From 3a135888c7f420f4477caeb7a98d45bf6b977b32 Mon Sep 17 00:00:00 2001 From: Simon Friis Vindum Date: Sat, 4 Oct 2025 16:46:50 +0200 Subject: [PATCH] C++: Improve bounds from inequalities on integers --- .../cpp/rangeanalysis/SimpleRangeAnalysis.qll | 48 +++++++++++++++---- .../SimpleRangeAnalysis/lowerBound.expected | 14 +++--- .../SimpleRangeAnalysis/ternaryLower.expected | 8 ++-- .../SimpleRangeAnalysis/ternaryUpper.expected | 2 +- .../SimpleRangeAnalysis/upperBound.expected | 4 +- 5 files changed, 52 insertions(+), 24 deletions(-) diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/SimpleRangeAnalysis.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/SimpleRangeAnalysis.qll index cc4647b54e0..c3c3c2dd3e7 100644 --- 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 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 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()) ) } diff --git a/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/lowerBound.expected b/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/lowerBound.expected index 8fe3b0ea0a1..0c520190c8b 100644 --- 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 | diff --git a/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/ternaryLower.expected b/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/ternaryLower.expected index f4e3cdb8cc2..50b65d84bf3 100644 --- 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 | diff --git a/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/ternaryUpper.expected b/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/ternaryUpper.expected index 529b6ea83f1..3b3a00df6b9 100644 --- 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 | diff --git a/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/upperBound.expected b/cpp/ql/test/library-tests/rangeanalysis/SimpleRangeAnalysis/upperBound.expected index 16181b8e238..dd7fc398f0c 100644 --- 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 |