diff --git a/cpp/ql/test/library-tests/ir/range-analysis/test.cpp b/cpp/ql/test/library-tests/ir/range-analysis/test.cpp index df06b28e297..61d17102948 100644 --- a/cpp/ql/test/library-tests/ir/range-analysis/test.cpp +++ b/cpp/ql/test/library-tests/ir/range-analysis/test.cpp @@ -120,13 +120,13 @@ void test_sub(int x, int y, int n) { void test_div(int x) { if (3 <= x && x <= 7) { - range(x / 2); // $ SPURIOUS: range=>=1.5 SPURIOUS: range=<=3.5 - range(x / 3); // $ range=>=1 SPURIOUS: range=<=2.333333 - range(x >> 2); // $ SPURIOUS: range=>=0.75 SPURIOUS: range=<=1.75 + range(x / 2); // $ range=>=1 range=<=3 + range(x / 3); // $ range=>=1 range=<=2 + range(x >> 2); // $ range=>=0 range=<=1 } if (2 <= x && x <= 8) { range(x / 2); // $ range=>=1 range=<=4 - range(x / 3); // $ SPURIOUS: range=>=0.666667 SPURIOUS: range=<=2.666667 - range(x >> 2); // $ SPURIOUS: range=>=0.5 range=<=2 + range(x / 3); // $ range=>=0 range=<=2 + range(x >> 2); // $ range=>=0 range=<=2 } } diff --git a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll index e1f1fd4b331..ea11074ad12 100644 --- a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll +++ b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll @@ -793,6 +793,7 @@ module RangeStage< * therefore only valid for non-negative numbers. */ private predicate boundFlowStepDiv(Sem::Expr e2, Sem::Expr e1, D::Delta factor) { + getTrackedType(e2) instanceof Sem::IntegerType and exists(Sem::ConstantIntegerExpr c, D::Delta k | k = D::fromInt(c.getIntValue()) and D::toFloat(k) > 0 | @@ -1165,6 +1166,9 @@ module RangeStage< bindingset[x] private float normalizeFloatUp(float x) { result = x + 0.0 } + bindingset[x, y] + private float truncatingDiv(float x, float y) { result = (x - (x % y)) / y } + /** * Holds if `b + delta` is a valid bound for `e`. * - `upper = true` : `e <= b + delta` @@ -1223,7 +1227,7 @@ module RangeStage< bounded(mid, b, d, upper, fromBackEdge, origdelta, reason) and b instanceof SemZeroBound and D::toFloat(d) >= 0 and - delta = D::fromFloat(D::toFloat(d) / D::toFloat(factor)) + delta = D::fromFloat(truncatingDiv(D::toFloat(d), D::toFloat(factor))) ) or exists(NarrowingCastExpr cast |