hohn/codeql
1
0
Fork 0
mirror of https://github.com/github/codeql.git synced 2026-04-28 18:25:24 +02:00
Code Issues Packages Projects Releases Wiki Activity

C++: Fix range analysis rounding for negative zero

Browse Source
This commit is contained in:
Jonas Jensen
2018-10-26 12:02:00 +02:00
parent cbe16e56d7
commit a3505e008b
3 changed files with 17 additions and 6 deletions
Download Patch File Download Diff File Expand all files Collapse all files

15
cpp/ql/src/semmle/code/cpp/rangeanalysis/SimpleRangeAnalysis.qll
View File

@@ -293,13 +293,24 @@ predicate analyzableDef(RangeSsaDefinition def, LocalScopeVariable v) {
assignmentDef(def, v, _) or defDependsOnDef(def, v, _, _)
}
/**
* Computes a normal form of `x` where -0.0 has changed to +0.0. This can be
* needed on the lesser side of a floating-point comparison or on both sides of
* a floating point equality because QL does not follow IEEE in floating-point
* comparisons but instead defines -0.0 to be less than and distinct from 0.0.
*/
bindingset[x]
private float normalizeFloatUp(float x) {
result = x + 0.0
}
/**
* Computes `x + y`, rounded towards +Inf. This is the general case where both
* `x` and `y` may be large numbers.
*/
bindingset[x, y]
private float addRoundingUp(float x, float y) {
if (x + y) - x < y or (x + y) - y < x
if normalizeFloatUp((x + y) - x) < y or normalizeFloatUp((x + y) - y) < x
then result = (x + y).nextUp()
else result = (x + y)
}
@@ -310,7 +321,7 @@ private float addRoundingUp(float x, float y) {
*/
bindingset[x, y]
private float addRoundingDown(float x, float y) {
if (x + y) - x > y or (x + y) - y > x
if (x + y) - x > normalizeFloatUp(y) or (x + y) - y > normalizeFloatUp(x)
then result = (x + y).nextDown()
else result = (x + y)
}