mirror of
https://github.com/github/codeql.git
synced 2026-04-29 02:35:15 +02:00
Merge pull request #2577 from MathiasVP/multiplication-overflow-not-possible-due-to-type-width
Multiplication overflow not possible due to type width
This commit is contained in:
@@ -18,6 +18,8 @@
|
||||
|
||||
import cpp
|
||||
import semmle.code.cpp.controlflow.SSA
|
||||
import semmle.code.cpp.rangeanalysis.SimpleRangeAnalysis
|
||||
import semmle.code.cpp.rangeanalysis.RangeAnalysisUtils
|
||||
|
||||
/**
|
||||
* Holds if `e` is either:
|
||||
@@ -64,6 +66,110 @@ int getEffectiveMulOperands(MulExpr me) {
|
||||
)
|
||||
}
|
||||
|
||||
/**
|
||||
* As SimpleRangeAnalysis does not support reasoning about multiplication
|
||||
* we create a tiny abstract interpreter for handling multiplication, which
|
||||
* we invoke only after weeding out of all of trivial cases that we do
|
||||
* not care about. By default, the maximum and minimum values are computed
|
||||
* using SimpleRangeAnalysis.
|
||||
*/
|
||||
class AnalyzableExpr extends Expr {
|
||||
float maxValue() { result = upperBound(this.getFullyConverted()) }
|
||||
|
||||
float minValue() { result = lowerBound(this.getFullyConverted()) }
|
||||
}
|
||||
|
||||
class ParenAnalyzableExpr extends AnalyzableExpr, ParenthesisExpr {
|
||||
override float maxValue() { result = this.getExpr().(AnalyzableExpr).maxValue() }
|
||||
|
||||
override float minValue() { result = this.getExpr().(AnalyzableExpr).minValue() }
|
||||
}
|
||||
|
||||
class MulAnalyzableExpr extends AnalyzableExpr, MulExpr {
|
||||
override float maxValue() {
|
||||
exists(float x1, float y1, float x2, float y2 |
|
||||
x1 = this.getLeftOperand().getFullyConverted().(AnalyzableExpr).minValue() and
|
||||
x2 = this.getLeftOperand().getFullyConverted().(AnalyzableExpr).maxValue() and
|
||||
y1 = this.getRightOperand().getFullyConverted().(AnalyzableExpr).minValue() and
|
||||
y2 = this.getRightOperand().getFullyConverted().(AnalyzableExpr).maxValue() and
|
||||
result = (x1 * y1).maximum(x1 * y2).maximum(x2 * y1).maximum(x2 * y2)
|
||||
)
|
||||
}
|
||||
|
||||
override float minValue() {
|
||||
exists(float x1, float x2, float y1, float y2 |
|
||||
x1 = this.getLeftOperand().getFullyConverted().(AnalyzableExpr).minValue() and
|
||||
x2 = this.getLeftOperand().getFullyConverted().(AnalyzableExpr).maxValue() and
|
||||
y1 = this.getRightOperand().getFullyConverted().(AnalyzableExpr).minValue() and
|
||||
y2 = this.getRightOperand().getFullyConverted().(AnalyzableExpr).maxValue() and
|
||||
result = (x1 * y1).minimum(x1 * y2).minimum(x2 * y1).minimum(x2 * y2)
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
class AddAnalyzableExpr extends AnalyzableExpr, AddExpr {
|
||||
override float maxValue() {
|
||||
result = this.getLeftOperand().getFullyConverted().(AnalyzableExpr).maxValue() +
|
||||
this.getRightOperand().getFullyConverted().(AnalyzableExpr).maxValue()
|
||||
}
|
||||
|
||||
override float minValue() {
|
||||
result = this.getLeftOperand().getFullyConverted().(AnalyzableExpr).minValue() +
|
||||
this.getRightOperand().getFullyConverted().(AnalyzableExpr).minValue()
|
||||
}
|
||||
}
|
||||
|
||||
class SubAnalyzableExpr extends AnalyzableExpr, SubExpr {
|
||||
override float maxValue() {
|
||||
result = this.getLeftOperand().getFullyConverted().(AnalyzableExpr).maxValue() -
|
||||
this.getRightOperand().getFullyConverted().(AnalyzableExpr).minValue()
|
||||
}
|
||||
|
||||
override float minValue() {
|
||||
result = this.getLeftOperand().getFullyConverted().(AnalyzableExpr).minValue() -
|
||||
this.getRightOperand().getFullyConverted().(AnalyzableExpr).maxValue()
|
||||
}
|
||||
}
|
||||
|
||||
class VarAnalyzableExpr extends AnalyzableExpr, VariableAccess {
|
||||
VarAnalyzableExpr() { this.getTarget() instanceof StackVariable }
|
||||
|
||||
override float maxValue() {
|
||||
exists(SsaDefinition def, Variable v |
|
||||
def.getAUse(v) = this and
|
||||
// if there is a defining expression, use that for
|
||||
// computing the maximum value. Otherwise, assign the
|
||||
// variable the largest possible value it can hold
|
||||
if exists(def.getDefiningValue(v))
|
||||
then result = def.getDefiningValue(v).(AnalyzableExpr).maxValue()
|
||||
else result = upperBound(this)
|
||||
)
|
||||
}
|
||||
|
||||
override float minValue() {
|
||||
exists(SsaDefinition def, Variable v |
|
||||
def.getAUse(v) = this and
|
||||
if exists(def.getDefiningValue(v))
|
||||
then result = def.getDefiningValue(v).(AnalyzableExpr).minValue()
|
||||
else result = lowerBound(this)
|
||||
)
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* Holds if `t` is not an instance of `IntegralType`,
|
||||
* or if `me` cannot be proven to not overflow
|
||||
*/
|
||||
predicate overflows(MulExpr me, Type t) {
|
||||
t instanceof IntegralType
|
||||
implies
|
||||
(
|
||||
me.(MulAnalyzableExpr).maxValue() > exprMaxVal(me)
|
||||
or
|
||||
me.(MulAnalyzableExpr).minValue() < exprMinVal(me)
|
||||
)
|
||||
}
|
||||
|
||||
from MulExpr me, Type t1, Type t2
|
||||
where
|
||||
t1 = me.getType().getUnderlyingType() and
|
||||
@@ -101,7 +207,11 @@ where
|
||||
e = other.(BinaryOperation).getAnOperand*()
|
||||
) and
|
||||
e.(Literal).getType().getSize() = t2.getSize()
|
||||
)
|
||||
) and
|
||||
// only report if we cannot prove that the result of the
|
||||
// multiplication will be less (resp. greater) than the
|
||||
// maximum (resp. minimum) number we can compute.
|
||||
overflows(me, t1)
|
||||
select me,
|
||||
"Multiplication result may overflow '" + me.getType().toString() + "' before it is converted to '"
|
||||
+ me.getFullyConverted().getType().toString() + "'."
|
||||
|
||||
@@ -92,3 +92,37 @@ void use_printf(float f, double d)
|
||||
size_t three_chars(unsigned char a, unsigned char b, unsigned char c) {
|
||||
return a * b * c; // at most 16581375
|
||||
}
|
||||
|
||||
void g(unsigned char uchar1, unsigned char uchar2, unsigned char uchar3, int i) {
|
||||
unsigned long ulong1, ulong2, ulong3, ulong4, ulong5;
|
||||
ulong1 = (uchar1 + 1) * (uchar2 + 1); // GOOD
|
||||
ulong2 = (i + 1) * (uchar2 + 1); // BAD
|
||||
ulong3 = (uchar1 + 1) * (uchar2 + 1) * (uchar3 + 1); // GOOD
|
||||
|
||||
ulong4 = (uchar1 + (uchar1 + 1)) * (uchar2 + 1); // GOOD
|
||||
ulong5 = (i + (uchar1 + 1)) * (uchar2 + 1); // BAD
|
||||
|
||||
ulong5 = (uchar1 + 1073741824) * uchar2; // BAD [NOT DETECTED]
|
||||
ulong5 = (uchar1 + (1 << 30)) * uchar2; // BAD [NOT DETECTED]
|
||||
ulong5 = uchar1 * uchar1 * uchar1 * uchar2 * uchar2 * uchar2; // BAD [NOT DETECTED]
|
||||
ulong5 = (uchar1 + (unsigned short)(-1)) * (uchar2 + (unsigned short)(-1)); // BAD
|
||||
}
|
||||
|
||||
struct A {
|
||||
short s;
|
||||
int i;
|
||||
};
|
||||
|
||||
void g2(struct A* a, short n) {
|
||||
unsigned long ulong1, ulong2;
|
||||
ulong1 = (a->s - 1) * ((*a).s + 1); // GOOD
|
||||
ulong2 = a->i * (*a).i; // BAD
|
||||
}
|
||||
|
||||
int global_i;
|
||||
unsigned char global_uchar;
|
||||
void g3() {
|
||||
unsigned long ulong1, ulong2;
|
||||
ulong1 = global_i * global_i; // BAD
|
||||
ulong2 = (global_uchar + 1) * 2; // GOOD
|
||||
}
|
||||
@@ -7,3 +7,8 @@
|
||||
| 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:99:14:99:35 | ... * ... | Multiplication result may overflow 'int' before it is converted to 'unsigned long'. |
|
||||
| IntMultToLong.c:103:14:103:46 | ... * ... | Multiplication result may overflow 'int' before it is converted to 'unsigned long'. |
|
||||
| IntMultToLong.c:108:14:108:78 | ... * ... | Multiplication result may overflow 'int' before it is converted to 'unsigned long'. |
|
||||
| IntMultToLong.c:119:14:119:26 | ... * ... | Multiplication result may overflow 'int' before it is converted to 'unsigned long'. |
|
||||
| IntMultToLong.c:126:14:126:32 | ... * ... | Multiplication result may overflow 'int' before it is converted to 'unsigned long'. |
|
||||
|
||||
Reference in New Issue
Block a user