C++: Fix rounding for >>.

This commit is contained in:
Geoffrey White
2020-05-06 18:29:51 +01:00
parent b1c32deabc
commit a4fa4c859a
3 changed files with 23 additions and 8 deletions

View File

@@ -140,6 +140,22 @@ private class UnsignedBitwiseAndExpr extends BitwiseAndExpr {
}
}
/**
* Gets the floor of `v`, with additional logic to work around issues with
* large numbers.
*/
bindingset[v]
float safeFloor(float v) {
// return the floor of v
v.abs() < 2.pow(31) and
result = v.floor()
or
// `floor()` doesn't work correctly on large numbers (since it returns an integer),
// so fall back to unrounded numbers at this scale.
not v.abs() < 2.pow(31) and
result = v
}
/** Set of expressions which we know how to analyze. */
private predicate analyzableExpr(Expr e) {
// The type of the expression must be arithmetic. We reuse the logic in
@@ -709,7 +725,7 @@ private float getLowerBoundsImpl(Expr expr) {
rsExpr = expr and
left = getFullyConvertedLowerBounds(rsExpr.getLeftOperand()) and
right = rsExpr.getRightOperand().getValue().toInt() and
result = left / 2.pow(right)
result = safeFloor(left / 2.pow(right))
)
}
@@ -878,7 +894,7 @@ private float getUpperBoundsImpl(Expr expr) {
rsExpr = expr and
left = getFullyConvertedUpperBounds(rsExpr.getLeftOperand()) and
right = rsExpr.getRightOperand().getValue().toInt() and
result = left / 2.pow(right)
result = safeFloor(left / 2.pow(right))
)
}

View File

@@ -369,9 +369,9 @@ int shifts(void)
{
unsigned int x = 3;
if (x >> 1 >= 1) {} // always true [BAD MESSAGE]
if (x >> 1 >= 2) {} // always false [BAD MESSAGE]
if (x >> 1 == 1) {} // always true [INCORRECT MESSAGE]
if (x >> 1 >= 1) {} // always true
if (x >> 1 >= 2) {} // always false
if (x >> 1 == 1) {} // always true [NOT DETECTED]
}
int bitwise_ands()

View File

@@ -38,9 +38,8 @@
| PointlessComparison.c:303:9:303:14 | ... >= ... | Comparison is always false because c <= 0. |
| PointlessComparison.c:312:9:312:14 | ... >= ... | Comparison is always false because c <= 0. |
| PointlessComparison.c:337:14:337:21 | ... >= ... | Comparison is always true because x >= 0. |
| PointlessComparison.c:372:6:372:16 | ... >= ... | Comparison is always true because ... >> ... >= 1.5. |
| PointlessComparison.c:373:6:373:16 | ... >= ... | Comparison is always false because ... >> ... <= 1.5. |
| PointlessComparison.c:374:6:374:16 | ... == ... | Comparison is always false because ... >> ... >= 1.5. |
| PointlessComparison.c:372:6:372:16 | ... >= ... | Comparison is always true because ... >> ... >= 1. |
| PointlessComparison.c:373:6:373:16 | ... >= ... | Comparison is always false because ... >> ... <= 1. |
| PointlessComparison.c:383:6:383:17 | ... >= ... | Comparison is always false because ... & ... <= 2. |
| PointlessComparison.cpp:36:6:36:33 | ... >= ... | Comparison is always false because ... >> ... <= 9223372036854776000. |
| PointlessComparison.cpp:41:6:41:29 | ... >= ... | Comparison is always false because ... >> ... <= 140737488355327.5. |