hohn/codeql
1
0
Fork 0
mirror of https://github.com/github/codeql.git synced 2025-12-17 01:03:14 +01:00
Code Issues Packages Projects Releases Wiki Activity

Rangeanalysis: Bugfix division with float representation.

Browse Source
This commit is contained in:
Anders Schack-Mulligen
2023-10-12 12:59:34 +02:00
parent 7b214a24df
commit 06fe10bbe9
2 changed files with 10 additions and 6 deletions
Download Patch File Download Diff File Expand all files Collapse all files

10
cpp/ql/test/library-tests/ir/range-analysis/test.cpp
View File

@@ -120,13 +120,13 @@ void test_sub(int x, int y, int n) {
void test_div(int x) { void test_div(int x) {
if (3 <= x && x <= 7) { if (3 <= x && x <= 7) {
range(x / 2); // $ SPURIOUS: range=>=1.5 SPURIOUS: range=<=3.5 range(x / 2); // $ range=>=1 range=<=3
range(x / 3); // $ range=>=1 SPURIOUS: range=<=2.333333 range(x / 3); // $ range=>=1 range=<=2
range(x >> 2); // $ SPURIOUS: range=>=0.75 SPURIOUS: range=<=1.75 range(x >> 2); // $ range=>=0 range=<=1
} }
if (2 <= x && x <= 8) { if (2 <= x && x <= 8) {
range(x / 2); // $ range=>=1 range=<=4 range(x / 2); // $ range=>=1 range=<=4
range(x / 3); // $ SPURIOUS: range=>=0.666667 SPURIOUS: range=<=2.666667 range(x / 3); // $ range=>=0 range=<=2
range(x >> 2); // $ SPURIOUS: range=>=0.5 range=<=2 range(x >> 2); // $ range=>=0 range=<=2
} }
} }

6
shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll
View File

@@ -793,6 +793,7 @@ module RangeStage<
* therefore only valid for non-negative numbers. * therefore only valid for non-negative numbers.
*/ */
private predicate boundFlowStepDiv(Sem::Expr e2, Sem::Expr e1, D::Delta factor) { 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 | exists(Sem::ConstantIntegerExpr c, D::Delta k |
k = D::fromInt(c.getIntValue()) and D::toFloat(k) > 0 k = D::fromInt(c.getIntValue()) and D::toFloat(k) > 0
| |
@@ -1165,6 +1166,9 @@ module RangeStage<
bindingset[x] bindingset[x]
private float normalizeFloatUp(float x) { result = x + 0.0 } 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`. * Holds if `b + delta` is a valid bound for `e`.
* - `upper = true` : `e <= b + delta` * - `upper = true` : `e <= b + delta`
@@ -1223,7 +1227,7 @@ module RangeStage<
bounded(mid, b, d, upper, fromBackEdge, origdelta, reason) and bounded(mid, b, d, upper, fromBackEdge, origdelta, reason) and
b instanceof SemZeroBound and b instanceof SemZeroBound and
D::toFloat(d) >= 0 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 or
exists(NarrowingCastExpr cast | exists(NarrowingCastExpr cast |