C++: Always normalize bounds after a computation

This stops some cases of `-0.0` from propagating through the range
analysis, fixing a false positive on arvidn/libtorrent.

There seems to be no need for a corresponding change in the caller of
`getDefLowerBoundsImpl` since that predicate only contains computations
that cannot introduce negative zero.
This commit is contained in:
Jonas Jensen
2020-09-11 11:56:53 +02:00
parent 0c8e06ba68
commit ad11f76ec6
5 changed files with 8 additions and 11 deletions

View File

@@ -570,7 +570,7 @@ private float getTruncatedLowerBounds(Expr expr) {
else (
// Some of the bounds computed by getLowerBoundsImpl might
// overflow, so we replace invalid bounds with exprMinVal.
exists(float newLB | newLB = getLowerBoundsImpl(expr) |
exists(float newLB | newLB = normalizeFloatUp(getLowerBoundsImpl(expr)) |
if exprMinVal(expr) <= newLB and newLB <= exprMaxVal(expr)
then result = newLB
else result = exprMinVal(expr)
@@ -617,7 +617,7 @@ private float getTruncatedUpperBounds(Expr expr) {
// Some of the bounds computed by `getUpperBoundsImpl`
// might overflow, so we replace invalid bounds with
// `exprMaxVal`.
exists(float newUB | newUB = getUpperBoundsImpl(expr) |
exists(float newUB | newUB = normalizeFloatUp(getUpperBoundsImpl(expr)) |
if exprMinVal(expr) <= newUB and newUB <= exprMaxVal(expr)
then result = newUB
else result = exprMaxVal(expr)

View File

@@ -136,7 +136,7 @@
| test.c:183:14:183:14 | a | -7 |
| test.c:184:5:184:9 | total | -45 |
| test.c:184:14:184:14 | b | -7 |
| test.c:184:16:184:16 | c | -0 |
| test.c:184:16:184:16 | c | 0 |
| test.c:186:13:186:13 | a | -2147483648 |
| test.c:186:18:186:18 | a | -7 |
| test.c:187:14:187:14 | a | -7 |

View File

@@ -115,7 +115,7 @@
| test.c:168:14:168:14 | a | 11 |
| test.c:169:5:169:9 | total | 8 |
| test.c:169:14:169:14 | b | 11 |
| test.c:169:16:169:16 | c | -0 |
| test.c:169:16:169:16 | c | 0 |
| test.c:171:13:171:13 | a | 2147483647 |
| test.c:171:18:171:18 | a | 2147483647 |
| test.c:172:14:172:14 | a | 11 |

View File

@@ -31,7 +31,7 @@
| PointlessComparison.c:126:12:126:18 | ... >= ... | Comparison is always true because a >= 20. |
| PointlessComparison.c:129:12:129:16 | ... > ... | Comparison is always false because a <= 3. |
| PointlessComparison.c:197:7:197:11 | ... < ... | Comparison is always false because x >= 0. |
| PointlessComparison.c:264:12:264:22 | ... >= ... | Comparison is always true because dbl >= 0 and -0 >= - .... |
| PointlessComparison.c:264:12:264:22 | ... >= ... | Comparison is always true because dbl >= 0 and 0 >= - .... |
| PointlessComparison.c:273:9:273:18 | ... > ... | Comparison is always false because c <= 0. |
| PointlessComparison.c:283:13:283:19 | ... >= ... | Comparison is always true because c >= 11. |
| PointlessComparison.c:294:9:294:16 | ... >= ... | Comparison is always false because ui1 <= 0. |
@@ -50,7 +50,4 @@
| PointlessComparison.cpp:43:6:43:29 | ... >= ... | Comparison is always true because ... >> ... >= 140737488355327.5. |
| PointlessComparison.cpp:44:6:44:28 | ... >= ... | Comparison is always true because ... >> ... >= 140737488355327.5. |
| RegressionTests.cpp:57:7:57:22 | ... <= ... | Comparison is always true because * ... <= 4294967295. |
| RegressionTests.cpp:89:7:89:14 | ... == ... | Comparison is always false because val <= -0. |
| RegressionTests.cpp:107:7:107:14 | ... == ... | Comparison is always false because val <= -0. |
| RegressionTests.cpp:116:7:116:14 | ... == ... | Comparison is always false because val <= -0. |
| Templates.cpp:9:10:9:24 | ... <= ... | Comparison is always true because local <= 32767. |

View File

@@ -86,7 +86,7 @@ void negativeZero1(int val) {
{
val = -val;
}
if (val == 0) // GOOD [FALSE POSITIVE]
if (val == 0) // GOOD [NO LONGER REPORTED]
;
}
@@ -104,7 +104,7 @@ void negativeZero3(int val) {
{
val *= -1;
}
if (val == 0) // GOOD [FALSE POSITIVE]
if (val == 0) // GOOD [NO LONGER REPORTED]
;
}
@@ -113,6 +113,6 @@ void negativeZero4(int val) {
{
val = val * -1;
}
if (val == 0) // GOOD [FALSE POSITIVE]
if (val == 0) // GOOD [NO LONGER REPORTED]
;
}