Merge pull request #4053 from jbj/SimpleRangeAnalysis-mul

C++: SimpleRangeAnalysis: unsigned multiplication
This commit is contained in:
Geoffrey White
2020-08-13 16:59:31 +01:00
committed by GitHub
9 changed files with 1179 additions and 1053 deletions

View File

@@ -156,6 +156,10 @@ float safeFloor(float v) {
result = v
}
private class UnsignedMulExpr extends MulExpr {
UnsignedMulExpr() { this.getType().(IntegralType).isUnsigned() }
}
/** 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
@@ -178,6 +182,8 @@ private predicate analyzableExpr(Expr e) {
or
e instanceof SubExpr
or
e instanceof UnsignedMulExpr
or
e instanceof AssignExpr
or
e instanceof AssignAddExpr
@@ -278,6 +284,10 @@ private predicate exprDependsOnDef(Expr e, RangeSsaDefinition srcDef, StackVaria
or
exists(SubExpr subExpr | e = subExpr | exprDependsOnDef(subExpr.getAnOperand(), srcDef, srcVar))
or
exists(UnsignedMulExpr mulExpr | e = mulExpr |
exprDependsOnDef(mulExpr.getAnOperand(), srcDef, srcVar)
)
or
exists(AssignExpr addExpr | e = addExpr | exprDependsOnDef(addExpr.getRValue(), srcDef, srcVar))
or
exists(AssignAddExpr addExpr | e = addExpr |
@@ -625,6 +635,13 @@ private float getLowerBoundsImpl(Expr expr) {
result = addRoundingDown(xLow, -yHigh)
)
or
exists(UnsignedMulExpr mulExpr, float xLow, float yLow |
expr = mulExpr and
xLow = getFullyConvertedLowerBounds(mulExpr.getLeftOperand()) and
yLow = getFullyConvertedLowerBounds(mulExpr.getRightOperand()) and
result = xLow * yLow
)
or
exists(AssignExpr assign |
expr = assign and
result = getFullyConvertedLowerBounds(assign.getRValue())
@@ -794,6 +811,13 @@ private float getUpperBoundsImpl(Expr expr) {
result = addRoundingUp(xHigh, -yLow)
)
or
exists(UnsignedMulExpr mulExpr, float xHigh, float yHigh |
expr = mulExpr and
xHigh = getFullyConvertedUpperBounds(mulExpr.getLeftOperand()) and
yHigh = getFullyConvertedUpperBounds(mulExpr.getRightOperand()) and
result = xHigh * yHigh
)
or
exists(AssignExpr assign |
expr = assign and
result = getFullyConvertedUpperBounds(assign.getRValue())

View File

@@ -1,4 +1,4 @@
import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis
from VariableAccess expr
select expr, lowerBound(expr)
select expr, lowerBound(expr).toString()

View File

@@ -463,3 +463,30 @@ int test_unsigned_mult02(unsigned b) {
return total;
}
unsigned long mult_rounding() {
unsigned long x, y, xy;
x = y = 1000000003UL; // 1e9 + 3
xy = x * y;
return xy; // BUG: upper bound should be >= 1000000006000000009UL
}
unsigned long mult_overflow() {
unsigned long x, y, xy;
x = 274177UL;
y = 67280421310721UL;
xy = x * y;
return xy; // BUG: lower bound should be <= 18446744073709551617UL
}
unsigned long mult_lower_bound(unsigned int ui, unsigned long ul) {
if (ui >= 10) {
unsigned long result = (unsigned long)ui * ui;
return result; // BUG: upper bound should be >= 18446744065119617025 (possibly a pretty-printing bug)
}
if (ul >= 10) {
unsigned long result = ul * ul;
return result; // lower bound is correctly 0 (overflow is possible)
}
return 0;
}

View File

@@ -1,4 +1,4 @@
import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis
from VariableAccess expr
select expr, upperBound(expr)
select expr, upperBound(expr).toString()

View File

@@ -385,10 +385,39 @@ void bitwise_ands()
void unsigned_mult(unsigned int x, unsigned int y) {
if(x < 13 && y < 35) {
if(x * y > 1024) {} // always false [NOT DETECTED]
if(x * y > 1024) {} // always false
if(x * y < 204) {}
if(x >= 3 && y >= 2) {
if(x * y < 5) {} // always false [NOT DETECTED]
if(x * y < 5) {} // always false
}
}
}
}
void mult_rounding() {
unsigned long x, y, xy;
x = y = 1000000003UL; // 1e9 + 3
xy = 1000000006000000009UL; // x * y, precisely
// Even though the range analysis wrongly considers x*y to be xy - 9, there
// are no PointlessComparison false positives in these tests because alerts
// are suppressed when ulp() < 1, which roughly means that the number is
// larger than 2^53.
if (x * y < xy) {} // always false [NOT DETECTED]
if (x * y > xy) {} // always false [NOT DETECTED]
}
void mult_overflow() {
unsigned long x, y;
// The following two numbers multiply to 2^64 + 1, which is 1 when truncated
// to 64-bit unsigned.
x = 274177UL;
y = 67280421310721UL;
if (x * y == 1) {} // always true [BUG: reported as always false]
// This bug appears to be caused by
// `RangeAnalysisUtils::typeUpperBound(unsigned long)` having a result of
// 2**64 + 384, making the range analysis think that the multiplication can't
// overflow. The correct `typeUpperBound` would be 2**64 - 1, but we can't
// represent that with a QL float or int. We could make `typeUpperBound`
// exclusive instead of inclusive, but there is no exclusive upper bound for
// floats.
}

View File

@@ -41,6 +41,9 @@
| 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.c:388:10:388:21 | ... > ... | Comparison is always false because ... * ... <= 408. |
| PointlessComparison.c:391:12:391:20 | ... < ... | Comparison is always false because ... * ... >= 6. |
| PointlessComparison.c:414:7:414:16 | ... == ... | Comparison is always false because ... * ... >= 18446744073709552000. |
| 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. |
| PointlessComparison.cpp:42:6:42:29 | ... >= ... | Comparison is always false because ... >> ... <= 140737488355327.5. |