Skip to content

Commit 06fe10b

Browse files
committed
Rangeanalysis: Bugfix division with float representation.
1 parent 7b214a2 commit 06fe10b

File tree

2 files changed

+10
-6
lines changed

2 files changed

+10
-6
lines changed

cpp/ql/test/library-tests/ir/range-analysis/test.cpp

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -120,13 +120,13 @@ void test_sub(int x, int y, int n) {
120120

121121
void test_div(int x) {
122122
if (3 <= x && x <= 7) {
123-
range(x / 2); // $ SPURIOUS: range=>=1.5 SPURIOUS: range=<=3.5
124-
range(x / 3); // $ range=>=1 SPURIOUS: range=<=2.333333
125-
range(x >> 2); // $ SPURIOUS: range=>=0.75 SPURIOUS: range=<=1.75
123+
range(x / 2); // $ range=>=1 range=<=3
124+
range(x / 3); // $ range=>=1 range=<=2
125+
range(x >> 2); // $ range=>=0 range=<=1
126126
}
127127
if (2 <= x && x <= 8) {
128128
range(x / 2); // $ range=>=1 range=<=4
129-
range(x / 3); // $ SPURIOUS: range=>=0.666667 SPURIOUS: range=<=2.666667
130-
range(x >> 2); // $ SPURIOUS: range=>=0.5 range=<=2
129+
range(x / 3); // $ range=>=0 range=<=2
130+
range(x >> 2); // $ range=>=0 range=<=2
131131
}
132132
}

shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -793,6 +793,7 @@ module RangeStage<
793793
* therefore only valid for non-negative numbers.
794794
*/
795795
private predicate boundFlowStepDiv(Sem::Expr e2, Sem::Expr e1, D::Delta factor) {
796+
getTrackedType(e2) instanceof Sem::IntegerType and
796797
exists(Sem::ConstantIntegerExpr c, D::Delta k |
797798
k = D::fromInt(c.getIntValue()) and D::toFloat(k) > 0
798799
|
@@ -1165,6 +1166,9 @@ module RangeStage<
11651166
bindingset[x]
11661167
private float normalizeFloatUp(float x) { result = x + 0.0 }
11671168

1169+
bindingset[x, y]
1170+
private float truncatingDiv(float x, float y) { result = (x - (x % y)) / y }
1171+
11681172
/**
11691173
* Holds if `b + delta` is a valid bound for `e`.
11701174
* - `upper = true` : `e <= b + delta`
@@ -1223,7 +1227,7 @@ module RangeStage<
12231227
bounded(mid, b, d, upper, fromBackEdge, origdelta, reason) and
12241228
b instanceof SemZeroBound and
12251229
D::toFloat(d) >= 0 and
1226-
delta = D::fromFloat(D::toFloat(d) / D::toFloat(factor))
1230+
delta = D::fromFloat(truncatingDiv(D::toFloat(d), D::toFloat(factor)))
12271231
)
12281232
or
12291233
exists(NarrowingCastExpr cast |

0 commit comments

Comments
 (0)