C++: Fix off-by-one in range analysis for 'RemExpr'.

This commit is contained in:
Mathias Vorreiter Pedersen
2021-07-16 16:35:19 +02:00
parent 81aa115838
commit 39d9395bc3
4 changed files with 9 additions and 9 deletions

View File

@@ -863,16 +863,16 @@ private float getLowerBoundsImpl(Expr expr) {
result = 0
or
// If either input could be negative then the output could be
// negative. If so, the lower bound of `x%y` is `-abs(y)`, which is
// equal to `min(-y,y)`.
// negative. If so, the lower bound of `x%y` is `-abs(y) + 1`, which is
// equal to `min(-y + 1,y - 1)`.
exists(float childLB |
childLB = getFullyConvertedLowerBounds(remExpr.getAnOperand()) and
not childLB >= 0
|
result = getFullyConvertedLowerBounds(remExpr.getRightOperand())
result = getFullyConvertedLowerBounds(remExpr.getRightOperand()) - 1
or
exists(float rhsUB | rhsUB = getFullyConvertedUpperBounds(remExpr.getRightOperand()) |
result = -rhsUB
result = -rhsUB + 1
)
)
)
@@ -1058,7 +1058,7 @@ private float getUpperBoundsImpl(Expr expr) {
expr = remExpr and
rhsUB = getFullyConvertedUpperBounds(remExpr.getRightOperand())
|
result = rhsUB
result = rhsUB - 1
or
// If the right hand side could be negative then we need to take its
// absolute value. Since `abs(x) = max(-x,x)` this is equivalent to
@@ -1067,7 +1067,7 @@ private float getUpperBoundsImpl(Expr expr) {
rhsLB = getFullyConvertedLowerBounds(remExpr.getRightOperand()) and
not rhsLB >= 0
|
result = -rhsLB
result = -rhsLB + 1
)
)
or

View File

@@ -593,7 +593,7 @@
| test.c:658:7:658:7 | u | 0 |
| test.c:659:9:659:9 | u | 0 |
| test.c:664:12:664:12 | s | -2147483648 |
| test.c:665:7:665:8 | s2 | -5 |
| test.c:665:7:665:8 | s2 | -4 |
| test.cpp:10:7:10:7 | b | -2147483648 |
| test.cpp:11:5:11:5 | x | -2147483648 |
| test.cpp:13:10:13:10 | x | -2147483648 |

View File

@@ -662,5 +662,5 @@ void guard_bound_out_of_range(void) {
void test_mod(int s) {
int s2 = s % 5;
out(s2); // -4 .. 4 [BUG: is -5 .. 5]
out(s2); // -4 .. 4
}

View File

@@ -593,7 +593,7 @@
| test.c:658:7:658:7 | u | 0 |
| test.c:659:9:659:9 | u | 4294967295 |
| test.c:664:12:664:12 | s | 2147483647 |
| test.c:665:7:665:8 | s2 | 5 |
| test.c:665:7:665:8 | s2 | 4 |
| test.cpp:10:7:10:7 | b | 2147483647 |
| test.cpp:11:5:11:5 | x | 2147483647 |
| test.cpp:13:10:13:10 | x | 2147483647 |