C++: Improve query precision

This commit is contained in:
Mathias Vorreiter Pedersen
2020-01-02 15:17:49 +01:00
parent cfb839a8f9
commit 7dbb191531
3 changed files with 43 additions and 6 deletions

View File

@@ -64,6 +64,32 @@ int getEffectiveMulOperands(MulExpr me) {
)
}
class LeafExpr extends Expr {
LeafExpr() { not this instanceof BinaryOperation }
}
/**
* Gets the size of the largest type (in bytes) of an non-literal
* operand to a binary operation. For example, for
* ```
* unsigned char a; short b;
* (a + 1) * b;
* ```
* the result is 2 (i.e., the size of a `short`)
*/
int widenedFromLiteralFromSize(Expr e) {
exists(Literal lit |
lit = e.(BinaryOperation).getAnOperand+() and
result = max(LeafExpr other |
other = e.(BinaryOperation).getAnOperand+() and
not other instanceof Literal
|
other.getType().getSize()
) and
result < lit.getType().getSize()
)
}
from MulExpr me, Type t1, Type t2
where
t1 = me.getType().getUnderlyingType() and
@@ -101,6 +127,20 @@ where
e = other.(BinaryOperation).getAnOperand*()
) and
e.(Literal).getType().getSize() = t2.getSize()
) and
// exclude cases where the operands to the multiplication were
// small, but widened due to a literal in a subexpression.
// For instance, if the multiplication is
// ```
// int c = (a + 1) * (b + 1)
// ```
// where a and b are both unsigned chars. In this case the maximum
// value of c will be 256 * 256, even though the arguments to the
// multiplication are both typed as int.
not exists(Expr e1, Expr e2 |
e1 = me.getLeftOperand() and
e2 = me.getRightOperand() and
widenedFromLiteralFromSize(e1) + widenedFromLiteralFromSize(e2) < t1.getSize()
)
select me,
"Multiplication result may overflow '" + me.getType().toString() + "' before it is converted to '"

View File

@@ -95,10 +95,10 @@ size_t three_chars(unsigned char a, unsigned char b, unsigned char c) {
void g(unsigned char a, unsigned char b, unsigned char b2, int c) {
unsigned long d, e, f, g, h;
d = (a + 1) * (b + 1); // GOOD [FALSE POSITIVE]
d = (a + 1) * (b + 1); // GOOD
e = (c + 1) * (b + 1); // BAD
h = (a + 1) * (b + 1) * (b2 + 1); // GOOD [FALSE POSITIVE]
h = (a + 1) * (b + 1) * (b2 + 1); // GOOD
f = (a + (a + 1)) * (b + 1); // GOOD [FALSE POSITIVE]
f = (a + (a + 1)) * (b + 1); // GOOD
g = (c + (a + 1)) * (b + 1); // BAD
}

View File

@@ -7,8 +7,5 @@
| IntMultToLong.c:61:23:61:33 | ... * ... | Multiplication result may overflow 'int' before it is converted to 'long long'. |
| IntMultToLong.c:63:23:63:40 | ... * ... | Multiplication result may overflow 'int' before it is converted to 'long long'. |
| IntMultToLong.c:75:9:75:13 | ... * ... | Multiplication result may overflow 'int' before it is converted to 'size_t'. |
| IntMultToLong.c:98:9:98:25 | ... * ... | Multiplication result may overflow 'int' before it is converted to 'unsigned long'. |
| IntMultToLong.c:99:9:99:25 | ... * ... | Multiplication result may overflow 'int' before it is converted to 'unsigned long'. |
| IntMultToLong.c:100:9:100:36 | ... * ... | Multiplication result may overflow 'int' before it is converted to 'unsigned long'. |
| IntMultToLong.c:102:9:102:31 | ... * ... | Multiplication result may overflow 'int' before it is converted to 'unsigned long'. |
| IntMultToLong.c:103:9:103:31 | ... * ... | Multiplication result may overflow 'int' before it is converted to 'unsigned long'. |