C++: Range analysis for unsigned AssignMulExpr

This is essentially a copy-paste job of `AssignAddExpr`, together with
the math from the `UnsignedMulExpr` support.
This commit is contained in:
Jonas Jensen
2020-08-13 15:10:20 +02:00
parent f90d779122
commit fe72b559d3
4 changed files with 80 additions and 0 deletions

View File

@@ -160,6 +160,10 @@ private class UnsignedMulExpr extends MulExpr {
UnsignedMulExpr() { this.getType().(IntegralType).isUnsigned() }
}
private class UnsignedAssignMulExpr extends AssignMulExpr {
UnsignedAssignMulExpr() { 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
@@ -190,6 +194,8 @@ private predicate analyzableExpr(Expr e) {
or
e instanceof AssignSubExpr
or
e instanceof UnsignedAssignMulExpr
or
e instanceof CrementOperation
or
e instanceof RemExpr
@@ -249,6 +255,14 @@ private predicate defDependsOnDef(
exprDependsOnDef(assignSub.getRValue(), srcDef, srcVar)
)
or
exists(UnsignedAssignMulExpr assignMul, RangeSsaDefinition nextDef |
def = assignMul and
assignMul.getLValue() = nextDef.getAUse(v)
|
defDependsOnDef(nextDef, v, srcDef, srcVar) or
exprDependsOnDef(assignMul.getRValue(), srcDef, srcVar)
)
or
exists(CrementOperation crem |
def = crem and
crem.getOperand() = v.getAnAccess() and
@@ -298,6 +312,10 @@ private predicate exprDependsOnDef(Expr e, RangeSsaDefinition srcDef, StackVaria
exprDependsOnDef(subExpr.getAnOperand(), srcDef, srcVar)
)
or
exists(UnsignedAssignMulExpr mulExpr | e = mulExpr |
exprDependsOnDef(mulExpr.getAnOperand(), srcDef, srcVar)
)
or
exists(CrementOperation crementExpr | e = crementExpr |
exprDependsOnDef(crementExpr.getOperand(), srcDef, srcVar)
)
@@ -669,6 +687,13 @@ private float getLowerBoundsImpl(Expr expr) {
result = addRoundingDown(xLow, -yHigh)
)
or
exists(UnsignedAssignMulExpr mulExpr, float xLow, float yLow |
expr = mulExpr and
xLow = getFullyConvertedLowerBounds(mulExpr.getLValue()) and
yLow = getFullyConvertedLowerBounds(mulExpr.getRValue()) and
result = xLow * yLow
)
or
exists(PrefixIncrExpr incrExpr, float xLow |
expr = incrExpr and
xLow = getFullyConvertedLowerBounds(incrExpr.getOperand()) and
@@ -845,6 +870,13 @@ private float getUpperBoundsImpl(Expr expr) {
result = addRoundingUp(xHigh, -yLow)
)
or
exists(UnsignedAssignMulExpr mulExpr, float xHigh, float yHigh |
expr = mulExpr and
xHigh = getFullyConvertedUpperBounds(mulExpr.getLValue()) and
yHigh = getFullyConvertedUpperBounds(mulExpr.getRValue()) and
result = xHigh * yHigh
)
or
exists(PrefixIncrExpr incrExpr, float xHigh |
expr = incrExpr and
xHigh = getFullyConvertedUpperBounds(incrExpr.getOperand()) and
@@ -1073,6 +1105,14 @@ private float getDefLowerBoundsImpl(RangeSsaDefinition def, StackVariable v) {
result = addRoundingDown(lhsLB, -rhsUB)
)
or
exists(UnsignedAssignMulExpr assignMul, RangeSsaDefinition nextDef, float lhsLB, float rhsLB |
def = assignMul and
assignMul.getLValue() = nextDef.getAUse(v) and
lhsLB = getDefLowerBounds(nextDef, v) and
rhsLB = getFullyConvertedLowerBounds(assignMul.getRValue()) and
result = lhsLB * rhsLB
)
or
exists(IncrementOperation incr, float newLB |
def = incr and
incr.getOperand() = v.getAnAccess() and
@@ -1115,6 +1155,14 @@ private float getDefUpperBoundsImpl(RangeSsaDefinition def, StackVariable v) {
result = addRoundingUp(lhsUB, -rhsLB)
)
or
exists(UnsignedAssignMulExpr assignMul, RangeSsaDefinition nextDef, float lhsUB, float rhsUB |
def = assignMul and
assignMul.getLValue() = nextDef.getAUse(v) and
lhsUB = getDefUpperBounds(nextDef, v) and
rhsUB = getFullyConvertedUpperBounds(assignMul.getRValue()) and
result = lhsUB * rhsUB
)
or
exists(IncrementOperation incr, float newUB |
def = incr and
incr.getOperand() = v.getAnAccess() and

View File

@@ -501,6 +501,15 @@
| test.c:488:28:488:29 | ul | 10 |
| test.c:488:33:488:34 | ul | 10 |
| test.c:489:12:489:17 | result | 0 |
| test.c:495:7:495:8 | ui | 0 |
| test.c:495:19:495:20 | ui | 0 |
| test.c:496:5:496:6 | ui | 2 |
| test.c:496:11:496:12 | ui | 2 |
| test.c:497:12:497:13 | ui | 4 |
| test.c:501:3:501:9 | uiconst | 10 |
| test.c:504:3:504:9 | ulconst | 10 |
| test.c:505:10:505:16 | uiconst | 40 |
| test.c:505:20:505:26 | ulconst | 40 |
| 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

@@ -490,3 +490,17 @@ unsigned long mult_lower_bound(unsigned int ui, unsigned long ul) {
}
return 0;
}
unsigned long mul_assign(unsigned int ui) {
if (ui <= 10 && ui >= 2) {
ui *= ui + 0;
return ui; // 4 .. 100
}
unsigned int uiconst = 10;
uiconst *= 4;
unsigned long ulconst = 10;
ulconst *= 4;
return uiconst + ulconst; // 40 .. 40 for both
}

View File

@@ -501,6 +501,15 @@
| test.c:488:28:488:29 | ul | 18446744073709552000 |
| test.c:488:33:488:34 | ul | 18446744073709552000 |
| test.c:489:12:489:17 | result | 18446744073709552000 |
| test.c:495:7:495:8 | ui | 4294967295 |
| test.c:495:19:495:20 | ui | 10 |
| test.c:496:5:496:6 | ui | 10 |
| test.c:496:11:496:12 | ui | 10 |
| test.c:497:12:497:13 | ui | 100 |
| test.c:501:3:501:9 | uiconst | 10 |
| test.c:504:3:504:9 | ulconst | 10 |
| test.c:505:10:505:16 | uiconst | 40 |
| test.c:505:20:505:26 | ulconst | 40 |
| test.cpp:10:7:10:7 | b | 2147483647 |
| test.cpp:11:5:11:5 | x | 2147483647 |
| test.cpp:13:10:13:10 | x | 2147483647 |