Merge pull request #4098 from jbj/SimpleRangeAnalysis-mul-constant

C++: Support multiplication by constants in range analysis
This commit is contained in:
Mathias Vorreiter Pedersen
2020-08-20 09:22:05 +02:00
committed by GitHub
7 changed files with 262 additions and 61 deletions

View File

@@ -21,4 +21,4 @@ The following changes in version 1.26 affect C/C++ analysis in all applications.
* The models library now models many more taint flows through `std::string`.
* The `SimpleRangeAnalysis` library now supports multiplications of the form
`e1 * e2` when `e1` and `e2` are unsigned.
`e1 * e2` and `x *= e2` when `e1` and `e2` are unsigned or constant.

View File

@@ -539,6 +539,17 @@ class BinaryOperation extends Operation, @bin_op_expr {
/** Gets the right operand of this binary operation. */
Expr getRightOperand() { this.hasChild(result, 1) }
/**
* Holds if `e1` and `e2` (in either order) are the two operands of this
* binary operation.
*/
predicate hasOperands(Expr e1, Expr e2) {
exists(int i | i in [0, 1] |
this.hasChild(e1, i) and
this.hasChild(e2, 1 - i)
)
}
override string toString() { result = "... " + this.getOperator() + " ..." }
override predicate mayBeImpure() {

View File

@@ -127,7 +127,7 @@ private class UnsignedBitwiseAndExpr extends BitwiseAndExpr {
UnsignedBitwiseAndExpr() {
(
getLeftOperand().getFullyConverted().getType().getUnderlyingType().(IntegralType).isUnsigned() or
getLeftOperand().getFullyConverted().getValue().toInt() >= 0
getValue(getLeftOperand().getFullyConverted()).toInt() >= 0
) and
(
getRightOperand()
@@ -136,7 +136,7 @@ private class UnsignedBitwiseAndExpr extends BitwiseAndExpr {
.getUnderlyingType()
.(IntegralType)
.isUnsigned() or
getRightOperand().getFullyConverted().getValue().toInt() >= 0
getValue(getRightOperand().getFullyConverted()).toInt() >= 0
)
}
}
@@ -157,12 +157,90 @@ float safeFloor(float v) {
result = v
}
/** A `MulExpr` where exactly one operand is constant. */
private class MulByConstantExpr extends MulExpr {
float constant;
Expr operand;
MulByConstantExpr() {
exists(Expr constantExpr |
this.hasOperands(constantExpr, operand) and
constant = getValue(constantExpr.getFullyConverted()).toFloat() and
not exists(getValue(operand.getFullyConverted()).toFloat())
)
}
/** Gets the value of the constant operand. */
float getConstant() { result = constant }
/** Gets the non-constant operand. */
Expr getOperand() { result = operand }
}
private class UnsignedMulExpr extends MulExpr {
UnsignedMulExpr() { this.getType().(IntegralType).isUnsigned() }
UnsignedMulExpr() {
this.getType().(IntegralType).isUnsigned() and
// Avoid overlap. It should be slightly cheaper to analyze
// `MulByConstantExpr`.
not this instanceof MulByConstantExpr
}
}
/**
* Holds if `expr` is effectively a multiplication of `operand` with the
* positive constant `positive`.
*/
private predicate effectivelyMultipliesByPositive(Expr expr, Expr operand, float positive) {
operand = expr.(MulByConstantExpr).getOperand() and
positive = expr.(MulByConstantExpr).getConstant() and
positive >= 0.0 // includes positive zero
or
operand = expr.(UnaryPlusExpr).getOperand() and
positive = 1.0
or
operand = expr.(CommaExpr).getRightOperand() and
positive = 1.0
or
operand = expr.(StmtExpr).getResultExpr() and
positive = 1.0
}
/**
* Holds if `expr` is effectively a multiplication of `operand` with the
* negative constant `negative`.
*/
private predicate effectivelyMultipliesByNegative(Expr expr, Expr operand, float negative) {
operand = expr.(MulByConstantExpr).getOperand() and
negative = expr.(MulByConstantExpr).getConstant() and
negative < 0.0 // includes negative zero
or
operand = expr.(UnaryMinusExpr).getOperand() and
negative = -1.0
}
private class AssignMulByConstantExpr extends AssignMulExpr {
float constant;
AssignMulByConstantExpr() { constant = getValue(this.getRValue().getFullyConverted()).toFloat() }
float getConstant() { result = constant }
}
private class AssignMulByPositiveConstantExpr extends AssignMulByConstantExpr {
AssignMulByPositiveConstantExpr() { constant >= 0.0 }
}
private class AssignMulByNegativeConstantExpr extends AssignMulByConstantExpr {
AssignMulByNegativeConstantExpr() { constant < 0.0 }
}
private class UnsignedAssignMulExpr extends AssignMulExpr {
UnsignedAssignMulExpr() { this.getType().(IntegralType).isUnsigned() }
UnsignedAssignMulExpr() {
this.getType().(IntegralType).isUnsigned() and
// Avoid overlap. It should be slightly cheaper to analyze
// `AssignMulByConstantExpr`.
not this instanceof AssignMulByConstantExpr
}
}
/** Set of expressions which we know how to analyze. */
@@ -173,9 +251,9 @@ private predicate analyzableExpr(Expr e) {
(
exists(getValue(e).toFloat())
or
e instanceof UnaryPlusExpr
effectivelyMultipliesByPositive(e, _, _)
or
e instanceof UnaryMinusExpr
effectivelyMultipliesByNegative(e, _, _)
or
e instanceof MinExpr
or
@@ -197,14 +275,12 @@ private predicate analyzableExpr(Expr e) {
or
e instanceof UnsignedAssignMulExpr
or
e instanceof AssignMulByConstantExpr
or
e instanceof CrementOperation
or
e instanceof RemExpr
or
e instanceof CommaExpr
or
e instanceof StmtExpr
or
// A conversion is analyzable, provided that its child has an arithmetic
// type. (Sometimes the child is a reference type, and so does not get
// any bounds.) Rather than checking whether the type of the child is
@@ -219,7 +295,7 @@ private predicate analyzableExpr(Expr e) {
e instanceof UnsignedBitwiseAndExpr
or
// `>>` by a constant
exists(e.(RShiftExpr).getRightOperand().getValue())
exists(getValue(e.(RShiftExpr).getRightOperand()))
or
// A modeled expression for range analysis
e instanceof SimpleRangeAnalysisExpr
@@ -261,6 +337,12 @@ private predicate defDependsOnDef(
exprDependsOnDef(assignMul.getAnOperand(), srcDef, srcVar)
)
or
exists(AssignMulByConstantExpr assignMul |
def = assignMul and
def.getAVariable() = v and
exprDependsOnDef(assignMul.getLValue(), srcDef, srcVar)
)
or
exists(CrementOperation crem |
def = crem and
def.getAVariable() = v and
@@ -276,12 +358,14 @@ private predicate defDependsOnDef(
* the structure of `getLowerBoundsImpl` and `getUpperBoundsImpl`.
*/
private predicate exprDependsOnDef(Expr e, RangeSsaDefinition srcDef, StackVariable srcVar) {
exists(UnaryMinusExpr negateExpr | e = negateExpr |
exprDependsOnDef(negateExpr.getOperand(), srcDef, srcVar)
exists(Expr operand |
effectivelyMultipliesByNegative(e, operand, _) and
exprDependsOnDef(operand, srcDef, srcVar)
)
or
exists(UnaryPlusExpr plusExpr | e = plusExpr |
exprDependsOnDef(plusExpr.getOperand(), srcDef, srcVar)
exists(Expr operand |
effectivelyMultipliesByPositive(e, operand, _) and
exprDependsOnDef(operand, srcDef, srcVar)
)
or
exists(MinExpr minExpr | e = minExpr | exprDependsOnDef(minExpr.getAnOperand(), srcDef, srcVar))
@@ -314,20 +398,16 @@ private predicate exprDependsOnDef(Expr e, RangeSsaDefinition srcDef, StackVaria
exprDependsOnDef(mulExpr.getAnOperand(), srcDef, srcVar)
)
or
exists(AssignMulByConstantExpr mulExpr | e = mulExpr |
exprDependsOnDef(mulExpr.getLValue(), srcDef, srcVar)
)
or
exists(CrementOperation crementExpr | e = crementExpr |
exprDependsOnDef(crementExpr.getOperand(), srcDef, srcVar)
)
or
exists(RemExpr remExpr | e = remExpr | exprDependsOnDef(remExpr.getAnOperand(), srcDef, srcVar))
or
exists(CommaExpr commaExpr | e = commaExpr |
exprDependsOnDef(commaExpr.getRightOperand(), srcDef, srcVar)
)
or
exists(StmtExpr stmtExpr | e = stmtExpr |
exprDependsOnDef(stmtExpr.getResultExpr(), srcDef, srcVar)
)
or
exists(Conversion convExpr | e = convExpr | exprDependsOnDef(convExpr.getExpr(), srcDef, srcVar))
or
// unsigned `&`
@@ -339,7 +419,7 @@ private predicate exprDependsOnDef(Expr e, RangeSsaDefinition srcDef, StackVaria
// `>>` by a constant
exists(RShiftExpr rs |
rs = e and
exists(rs.getRightOperand().getValue()) and
exists(getValue(rs.getRightOperand())) and
exprDependsOnDef(rs.getLeftOperand(), srcDef, srcVar)
)
or
@@ -592,15 +672,16 @@ deprecated predicate positive_overflow(Expr expr) { exprMightOverflowPositively(
/** Only to be called by `getTruncatedLowerBounds`. */
private float getLowerBoundsImpl(Expr expr) {
exists(UnaryPlusExpr plusExpr |
expr = plusExpr and
result = getFullyConvertedLowerBounds(plusExpr.getOperand())
exists(Expr operand, float operandLow, float positive |
effectivelyMultipliesByPositive(expr, operand, positive) and
operandLow = getFullyConvertedLowerBounds(operand) and
result = positive * operandLow
)
or
exists(UnaryMinusExpr negateExpr, float xHigh |
expr = negateExpr and
xHigh = getFullyConvertedUpperBounds(negateExpr.getOperand()) and
result = -xHigh
exists(Expr operand, float operandHigh, float negative |
effectivelyMultipliesByNegative(expr, operand, negative) and
operandHigh = getFullyConvertedUpperBounds(operand) and
result = negative * operandHigh
)
or
exists(MinExpr minExpr |
@@ -688,6 +769,18 @@ private float getLowerBoundsImpl(Expr expr) {
result = xLow * yLow
)
or
exists(AssignMulByPositiveConstantExpr mulExpr, float xLow |
expr = mulExpr and
xLow = getFullyConvertedLowerBounds(mulExpr.getLValue()) and
result = xLow * mulExpr.getConstant()
)
or
exists(AssignMulByNegativeConstantExpr mulExpr, float xHigh |
expr = mulExpr and
xHigh = getFullyConvertedUpperBounds(mulExpr.getLValue()) and
result = xHigh * mulExpr.getConstant()
)
or
exists(PrefixIncrExpr incrExpr, float xLow |
expr = incrExpr and
xLow = getFullyConvertedLowerBounds(incrExpr.getOperand()) and
@@ -732,16 +825,6 @@ private float getLowerBoundsImpl(Expr expr) {
)
)
or
exists(CommaExpr commaExpr |
expr = commaExpr and
result = getFullyConvertedLowerBounds(commaExpr.getRightOperand())
)
or
exists(StmtExpr stmtExpr |
expr = stmtExpr and
result = getFullyConvertedLowerBounds(stmtExpr.getResultExpr())
)
or
// If the conversion is to an arithmetic type then we just return the
// lower bound of the child. We do not need to handle truncation and
// overflow here, because that is done in `getTruncatedLowerBounds`.
@@ -770,7 +853,7 @@ private float getLowerBoundsImpl(Expr expr) {
exists(RShiftExpr rsExpr, float left, int right |
rsExpr = expr and
left = getFullyConvertedLowerBounds(rsExpr.getLeftOperand()) and
right = rsExpr.getRightOperand().getFullyConverted().getValue().toInt() and
right = getValue(rsExpr.getRightOperand().getFullyConverted()).toInt() and
result = safeFloor(left / 2.pow(right))
)
or
@@ -783,15 +866,16 @@ private float getLowerBoundsImpl(Expr expr) {
/** Only to be called by `getTruncatedUpperBounds`. */
private float getUpperBoundsImpl(Expr expr) {
exists(UnaryPlusExpr plusExpr |
expr = plusExpr and
result = getFullyConvertedUpperBounds(plusExpr.getOperand())
exists(Expr operand, float operandHigh, float positive |
effectivelyMultipliesByPositive(expr, operand, positive) and
operandHigh = getFullyConvertedUpperBounds(operand) and
result = positive * operandHigh
)
or
exists(UnaryMinusExpr negateExpr, float xLow |
expr = negateExpr and
xLow = getFullyConvertedLowerBounds(negateExpr.getOperand()) and
result = -xLow
exists(Expr operand, float operandLow, float negative |
effectivelyMultipliesByNegative(expr, operand, negative) and
operandLow = getFullyConvertedLowerBounds(operand) and
result = negative * operandLow
)
or
exists(MaxExpr maxExpr |
@@ -879,6 +963,18 @@ private float getUpperBoundsImpl(Expr expr) {
result = xHigh * yHigh
)
or
exists(AssignMulByPositiveConstantExpr mulExpr, float xHigh |
expr = mulExpr and
xHigh = getFullyConvertedUpperBounds(mulExpr.getLValue()) and
result = xHigh * mulExpr.getConstant()
)
or
exists(AssignMulByNegativeConstantExpr mulExpr, float xLow |
expr = mulExpr and
xLow = getFullyConvertedLowerBounds(mulExpr.getLValue()) and
result = xLow * mulExpr.getConstant()
)
or
exists(PrefixIncrExpr incrExpr, float xHigh |
expr = incrExpr and
xHigh = getFullyConvertedUpperBounds(incrExpr.getOperand()) and
@@ -921,16 +1017,6 @@ private float getUpperBoundsImpl(Expr expr) {
)
)
or
exists(CommaExpr commaExpr |
expr = commaExpr and
result = getFullyConvertedUpperBounds(commaExpr.getRightOperand())
)
or
exists(StmtExpr stmtExpr |
expr = stmtExpr and
result = getFullyConvertedUpperBounds(stmtExpr.getResultExpr())
)
or
// If the conversion is to an arithmetic type then we just return the
// upper bound of the child. We do not need to handle truncation and
// overflow here, because that is done in `getTruncatedUpperBounds`.
@@ -961,7 +1047,7 @@ private float getUpperBoundsImpl(Expr expr) {
exists(RShiftExpr rsExpr, float left, int right |
rsExpr = expr and
left = getFullyConvertedUpperBounds(rsExpr.getLeftOperand()) and
right = rsExpr.getRightOperand().getFullyConverted().getValue().toInt() and
right = getValue(rsExpr.getRightOperand().getFullyConverted()).toInt() and
result = safeFloor(left / 2.pow(right))
)
or
@@ -1123,6 +1209,20 @@ private float getDefLowerBoundsImpl(RangeSsaDefinition def, StackVariable v) {
result = lhsLB * rhsLB
)
or
exists(AssignMulByPositiveConstantExpr assignMul, RangeSsaDefinition nextDef, float lhsLB |
def = assignMul and
assignMul.getLValue() = nextDef.getAUse(v) and
lhsLB = getDefLowerBounds(nextDef, v) and
result = lhsLB * assignMul.getConstant()
)
or
exists(AssignMulByNegativeConstantExpr assignMul, RangeSsaDefinition nextDef, float lhsUB |
def = assignMul and
assignMul.getLValue() = nextDef.getAUse(v) and
lhsUB = getDefUpperBounds(nextDef, v) and
result = lhsUB * assignMul.getConstant()
)
or
exists(IncrementOperation incr, float newLB |
def = incr and
incr.getOperand() = v.getAnAccess() and
@@ -1173,6 +1273,20 @@ private float getDefUpperBoundsImpl(RangeSsaDefinition def, StackVariable v) {
result = lhsUB * rhsUB
)
or
exists(AssignMulByPositiveConstantExpr assignMul, RangeSsaDefinition nextDef, float lhsUB |
def = assignMul and
assignMul.getLValue() = nextDef.getAUse(v) and
lhsUB = getDefUpperBounds(nextDef, v) and
result = lhsUB * assignMul.getConstant()
)
or
exists(AssignMulByNegativeConstantExpr assignMul, RangeSsaDefinition nextDef, float lhsLB |
def = assignMul and
assignMul.getLValue() = nextDef.getAUse(v) and
lhsLB = getDefLowerBounds(nextDef, v) and
result = lhsLB * assignMul.getConstant()
)
or
exists(IncrementOperation incr, float newUB |
def = incr and
incr.getOperand() = v.getAnAccess() and

View File

@@ -510,6 +510,28 @@
| 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.c:509:7:509:7 | i | -2147483648 |
| test.c:509:18:509:18 | i | -1 |
| test.c:510:5:510:5 | i | -2147483648 |
| test.c:510:13:510:13 | i | -1 |
| test.c:511:9:511:9 | i | -5 |
| test.c:513:5:513:5 | i | -2147483648 |
| test.c:513:9:513:9 | i | -5 |
| test.c:514:9:514:9 | i | -30 |
| test.c:516:5:516:5 | i | -30 |
| test.c:517:9:517:9 | i | -210 |
| test.c:519:5:519:5 | i | -210 |
| test.c:520:9:520:9 | i | -1155 |
| test.c:522:7:522:7 | i | -2147483648 |
| test.c:523:5:523:5 | i | -2147483648 |
| test.c:523:9:523:9 | i | -1 |
| test.c:524:9:524:9 | i | 1 |
| test.c:526:3:526:3 | i | -2147483648 |
| test.c:526:7:526:7 | i | -2147483648 |
| test.c:527:10:527:10 | i | -2147483648 |
| test.c:530:3:530:3 | i | -2147483648 |
| test.c:530:10:530:11 | sc | 1 |
| test.c:532:7:532:7 | i | -128 |
| 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

@@ -504,3 +504,32 @@ unsigned long mul_assign(unsigned int ui) {
ulconst *= 4;
return uiconst + ulconst; // 40 .. 40 for both
}
int mul_by_constant(int i, int j) {
if (i >= -1 && i <= 2) {
i = 5 * i;
out(i); // -5 .. 10
i = i * -3;
out(i); // -30 .. 15
i *= 7;
out(i); // -210 .. 105
i *= -11;
out(i); // -1155 .. 2310
}
if (i == -1) {
i = i * (int)0xffFFffFF; // fully converted literal is -1
out(i); // 1 .. 1
}
i = i * -1;
out( i); // -2^31 .. 2^31-1
signed char sc = 1;
i = (*&sc *= 2);
out(sc); // demonstrate that we couldn't analyze the LHS of the `*=` above...
out(i); // -128 .. 127 // ... but we can still bound its result by its type.
return 0;
}

View File

@@ -510,6 +510,28 @@
| 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.c:509:7:509:7 | i | 2147483647 |
| test.c:509:18:509:18 | i | 2147483647 |
| test.c:510:5:510:5 | i | 2147483647 |
| test.c:510:13:510:13 | i | 2 |
| test.c:511:9:511:9 | i | 10 |
| test.c:513:5:513:5 | i | 2147483647 |
| test.c:513:9:513:9 | i | 10 |
| test.c:514:9:514:9 | i | 15 |
| test.c:516:5:516:5 | i | 15 |
| test.c:517:9:517:9 | i | 105 |
| test.c:519:5:519:5 | i | 105 |
| test.c:520:9:520:9 | i | 2310 |
| test.c:522:7:522:7 | i | 2147483647 |
| test.c:523:5:523:5 | i | 2147483647 |
| test.c:523:9:523:9 | i | -1 |
| test.c:524:9:524:9 | i | 1 |
| test.c:526:3:526:3 | i | 2147483647 |
| test.c:526:7:526:7 | i | 2147483647 |
| test.c:527:10:527:10 | i | 2147483647 |
| test.c:530:3:530:3 | i | 2147483647 |
| test.c:530:10:530:11 | sc | 1 |
| test.c:532:7:532:7 | i | 127 |
| test.cpp:10:7:10:7 | b | 2147483647 |
| test.cpp:11:5:11:5 | x | 2147483647 |
| test.cpp:13:10:13:10 | x | 2147483647 |

View File

@@ -2,5 +2,8 @@
| test3.c:13:16:13:19 | * ... | $@ flows to here and is used in an expression which might overflow negatively. | test3.c:11:15:11:18 | argv | User-provided value |
| test4.cpp:13:17:13:20 | access to array | $@ flows to here and is used in an expression which might overflow negatively. | test4.cpp:9:13:9:16 | argv | User-provided value |
| test5.cpp:10:9:10:15 | call to strtoul | $@ flows to here and is used in an expression which might overflow. | test5.cpp:9:7:9:9 | buf | User-provided value |
| test5.cpp:17:6:17:27 | ... * ... | $@ flows to here and is used in an expression which might overflow. | test5.cpp:9:7:9:9 | buf | User-provided value |
| test5.cpp:19:6:19:13 | ... * ... | $@ flows to here and is used in an expression which might overflow. | test5.cpp:9:7:9:9 | buf | User-provided value |
| test.c:14:15:14:35 | ... * ... | $@ flows to here and is used in an expression which might overflow. | test.c:11:29:11:32 | argv | User-provided value |
| test.c:44:7:44:12 | ... -- | $@ flows to here and is used in an expression which might overflow negatively. | test.c:41:17:41:20 | argv | User-provided value |
| test.c:54:7:54:12 | ... -- | $@ flows to here and is used in an expression which might overflow negatively. | test.c:51:17:51:20 | argv | User-provided value |