hohn/codeql
1
0
Fork 0
mirror of https://github.com/github/codeql.git synced 2026-04-29 10:45:15 +02:00
Code Issues Packages Projects Releases Wiki Activity

Merge pull request #12696 from MathiasVP/range-analysis-of-mul-expr

Browse Source 
C++: IR-based range analysis of multiplication
This commit is contained in:
Mathias Vorreiter Pedersen
2023-03-29 14:05:55 +01:00
committed by GitHub
parent d0fa7c7ff8 9d5c785d89
commit 6dd45b31e1
2 changed files with 159 additions and 40 deletions
Download Patch File Download Diff File Expand all files Collapse all files

119
cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/RangeAnalysisStage.qll
View File

@@ -1062,6 +1062,20 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
or
upper = false and delta = D::fromFloat(-D::toFloat(d_max).abs() + 1)
)
or
exists(
D::Delta dLeft, D::Delta dRight, boolean fbeLeft, boolean fbeRight, D::Delta odLeft,
D::Delta odRight, SemReason rLeft, SemReason rRight
|
boundedMulOperand(e, upper, true, dLeft, fbeLeft, odLeft, rLeft) and
boundedMulOperand(e, upper, false, dRight, fbeRight, odRight, rRight) and
delta = D::fromFloat(D::toFloat(dLeft) * D::toFloat(dRight)) and
fromBackEdge = fbeLeft.booleanOr(fbeRight)
|
b instanceof SemZeroBound and origdelta = odLeft and reason = rLeft
or
b instanceof SemZeroBound and origdelta = odRight and reason = rRight
)
)
}
@@ -1095,4 +1109,109 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
) {
bounded(rem.getRightOperand(), b, delta, upper, fromBackEdge, origdelta, reason)
}
/**
* Define `cmp(true) = <=` and `cmp(false) = >=`.
*
* Holds if `mul = left * right`, and in order to know if `mul cmp(upper) 0 + k` (for
* some `k`) we need to know that `left cmp(upperLeft) 0 + k1` and
* `right cmp(upperRight) 0 + k2` (for some `k1` and `k2`).
*/
pragma[nomagic]
private predicate boundedMulOperandCand(
SemMulExpr mul, SemExpr left, SemExpr right, boolean upper, boolean upperLeft,
boolean upperRight
) {
not boundFlowStepMul(mul, _, _) and
mul.getLeftOperand() = left and
mul.getRightOperand() = right and
(
semPositive(left) and
(
// left, right >= 0
semPositive(right) and
(
// max(left * right) = max(left) * max(right)
upper = true and
upperLeft = true and
upperRight = true
or
// min(left * right) = min(left) * min(right)
upper = false and
upperLeft = false and
upperRight = false
)
or
// left >= 0, right <= 0
semNegative(right) and
(
// max(left * right) = min(left) * max(right)
upper = true and
upperLeft = false and
upperRight = true
or
// min(left * right) = max(left) * min(right)
upper = false and
upperLeft = true and
upperRight = false
)
)
or
semNegative(left) and
(
// left <= 0, right >= 0
semPositive(right) and
(
// max(left * right) = max(left) * min(right)
upper = true and
upperLeft = true and
upperRight = false
or
// min(left * right) = min(left) * max(right)
upper = false and
upperLeft = false and
upperRight = true
)
or
// left, right <= 0
semNegative(right) and
(
// max(left * right) = min(left) * min(right)
upper = true and
upperLeft = false and
upperRight = false
or
// min(left * right) = max(left) * max(right)
upper = false and
upperLeft = true and
upperRight = true
)
)
)
}
/**
* Holds if `isLeft = true` and `mul`'s left operand is bounded by `delta`,
* or if `isLeft = false` and `mul`'s right operand is bounded by `delta`.
*
* If `upper = true` the computed bound contributes to an upper bound of `mul`,
* and if `upper = false` it contributes to a lower bound.
* The `fromBackEdge`, `origdelta`, `reason` triple are defined by the recursive
* call to `bounded`.
*/
pragma[nomagic]
private predicate boundedMulOperand(
SemMulExpr mul, boolean upper, boolean isLeft, D::Delta delta, boolean fromBackEdge,
D::Delta origdelta, SemReason reason
) {
exists(boolean upperLeft, boolean upperRight, SemExpr left, SemExpr right |
boundedMulOperandCand(mul, left, right, upper, upperLeft, upperRight)
|
isLeft = true and
bounded(left, any(SemZeroBound zb), delta, upperLeft, fromBackEdge, origdelta, reason)
or
isLeft = false and
bounded(right, any(SemZeroBound zb), delta, upperRight, fromBackEdge, origdelta, reason)
)
}
}

80
cpp/ql/test/library-tests/ir/range-analysis/SimpleRangeAnalysis_tests.cpp
View File

@@ -300,17 +300,17 @@ int test_mult01(int a, int b) {
range(a); // $ range=<=11 range=>=3
range(b); // $ range=<=23 range=>=5
int r = a*b; // 15 .. 253
range(r);
range(r); // $ range=<=253 range=>=15
total += r;
range(total); // $ MISSING: range=>=1
range(total); // $ range=<=253 range=>=15
}
if (3 <= a && a <= 11 && 0 <= b && b <= 23) {
range(a); // $ range=<=11 range=>=3
range(b); // $ range=<=23 range=>=0
int r = a*b; // 0 .. 253
range(r);
range(r); // $ range=<=253 range=>=0
total += r;
range(total); // $ MISSING: range=>=0 range=>=3+0
range(total); // $ range=<=3+253 range=<=506 range=>=0 range=>=3+0
}
if (3 <= a && a <= 11 && -13 <= b && b <= 23) {
range(a); // $ range=<=11 range=>=3
@@ -324,19 +324,19 @@ int test_mult01(int a, int b) {
range(a); // $ range=<=11 range=>=3
range(b); // $ range=<=0 range=>=-13
int r = a*b; // -143 .. 0
range(r);
range(r); // $ range=<=0 range=>=-143
total += r;
range(total); // $ MISSING: range=<=3+0
range(total); // $ range=<=3+0 range=>=3-143
}
if (3 <= a && a <= 11 && -13 <= b && b <= -7) {
range(a); // $ range=<=11 range=>=3
range(b); // $ range=<=-7 range=>=-13
int r = a*b; // -143 .. -21
range(r);
range(r); // $ range=<=-21 range=>=-143
total += r;
range(total); // $ MISSING: range=<=3-1
range(total); // $ range=<=3-21 range=>=3-143 range=>=3-286
}
range(total); // $ MISSING: range=<=3+0
range(total); // $ range=<=3+0 range=>=3-143 range=>=3-286
return total;
}
@@ -348,17 +348,17 @@ int test_mult02(int a, int b) {
range(a); // $ range=<=11 range=>=0
range(b); // $ range=<=23 range=>=5
int r = a*b; // 0 .. 253
range(r);
range(r); // $ range=<=253 range=>=0
total += r;
range(total); // $ MISSING: range=>=0
range(total); // $ range=>=0 range=<=253
}
if (0 <= a && a <= 11 && 0 <= b && b <= 23) {
range(a); // $ range=<=11 range=>=0
range(b); // $ range=<=23 range=>=0
int r = a*b; // 0 .. 253
range(r);
range(r); // $ range=<=253 range=>=0
total += r;
range(total); // $ MISSING: range=>=0 range=>=0+0
range(total); // $ range=>=0 range=>=0+0 range=<=0+253 range=<=506
}
if (0 <= a && a <= 11 && -13 <= b && b <= 23) {
range(a); // $ range=<=11 range=>=0
@@ -372,19 +372,19 @@ int test_mult02(int a, int b) {
range(a); // $ range=<=11 range=>=0
range(b); // $ range=<=0 range=>=-13
int r = a*b; // -143 .. 0
range(r);
range(r); // $ range=<=0 range=>=-143
total += r;
range(total); // $ MISSING: range=<=0+0
range(total); // $ range=<=0+0 range=>=0-143
}
if (0 <= a && a <= 11 && -13 <= b && b <= -7) {
range(a); // $ range=<=11 range=>=0
range(b); // $ range=<=-7 range=>=-13
int r = a*b; // -143 .. 0
range(r);
range(r); // $ range=<=0 range=>=-143
total += r;
range(total); // $ MISSING: range=<=0+0
range(total); // $ range=<=0+0 range=>=0-143 range=>=0-286
}
range(total); // $ MISSING: range=<=0+0
range(total); // $ range=<=0+0 range=>=0-143 range=>=0-286
return total;
}
@@ -445,15 +445,15 @@ int test_mult04(int a, int b) {
range(b); // $ range=<=23 range=>=5
int r = a*b; // -391 .. 0
total += r;
range(total); // $ MISSING: range=<=0
range(total); // $ range=<=0 range=>=-391
}
if (-17 <= a && a <= 0 && 0 <= b && b <= 23) {
range(a); // $ range=<=0 range=>=-17
range(b); // $ range=<=23 range=>=0
int r = a*b; // -391 .. 0
range(r);
range(r); // $ range=<=0 range=>=-391
total += r;
range(total); // $ MISSING: range="<=- ...+0" range=<=0
range(total); // $ range="<=- ...+0" range=<=0 range=">=- ...-391" range=>=-782
}
if (-17 <= a && a <= 0 && -13 <= b && b <= 23) {
range(a); // $ range=<=0 range=>=-17
@@ -467,19 +467,19 @@ int test_mult04(int a, int b) {
range(a); // $ range=<=0 range=>=-17
range(b); // $ range=<=0 range=>=-13
int r = a*b; // 0 .. 221
range(r);
range(r); // $ range=<=221 range=>=0
total += r;
range(total); // $ MISSING: range=">=- ...+0"
range(total); // $ range="<=- ...+221" range=">=- ...+0"
}
if (-17 <= a && a <= 0 && -13 <= b && b <= -7) {
range(a); // $ range=<=0 range=>=-17
range(b); // $ range=<=-7 range=>=-13
int r = a*b; // 0 .. 221
range(r);
range(r); // $ range=<=221 range=>=0
total += r;
range(total); // $ MISSING: range=">=- ...+0"
range(total); // $ range=">=- ...+0" range="<=- ...+221" range="<=- ...+442"
}
range(total); // $ MISSING: range=">=- ...+0"
range(total); // $ range=">=- ...+0" range="<=- ...+221" range="<=- ...+442"
return total;
}
@@ -491,17 +491,17 @@ int test_mult05(int a, int b) {
range(a); // $ range=<=-2 range=>=-17
range(b); // $ range=<=23 range=>=5
int r = a*b; // -391 .. -10
range(r);
range(r); // $ range=<=-10 range=>=-391
total += r;
range(total); // $ MISSING: range=<=-1
range(total); // $ range=<=-10 range=>=-391
}
if (-17 <= a && a <= -2 && 0 <= b && b <= 23) {
range(a); // $ range=<=-2 range=>=-17
range(b); // $ range=<=23 range=>=0
int r = a*b; // -391 .. 0
range(r);
range(r); // $ range=<=0 range=>=-391
total += r;
range(total); // $ MISSING: range="<=- ...+0" range=<=0
range(total); // $ range="<=- ...+0" range=<=0 range=">=- ...-391" range=>=-782
}
if (-17 <= a && a <= -2 && -13 <= b && b <= 23) {
range(a); // $ range=<=-2 range=>=-17
@@ -515,19 +515,19 @@ int test_mult05(int a, int b) {
range(a); // $ range=<=-2 range=>=-17
range(b); // $ range=<=0 range=>=-13
int r = a*b; // 0 .. 221
range(r);
range(r); // $ range=<=221 range=>=0
total += r;
range(total); // $ MISSING: range=">=- ...+0"
range(total); // $ range="<=- ...+221" range=">=- ...+0"
}
if (-17 <= a && a <= -2 && -13 <= b && b <= -7) {
range(a); // $ range=<=-2 range=>=-17
range(b); // $ range=<=-7 range=>=-13
int r = a*b; // 14 .. 221
range(r);
range(r); // $ range=<=221 range=>=14
total += r;
range(total); // $ MISSING: range=">=- ...+1"
range(total); // $ range="<=- ...+221" range="<=- ...+442" range=">=- ...+14"
}
range(total); // $ MISSING: range=">=- ...+0"
range(total); // $ range=">=- ...+0" range="<=- ...+221" range="<=- ...+442"
return total;
}
@@ -741,7 +741,7 @@ unsigned long mult_rounding() {
range(y); // $ range===1000000003
range(x); // $ range===1000000003
xy = x * y;
range(xy);
range(xy); // $ range===2147483647
return xy; // BUG: upper bound should be >= 1000000006000000009UL
}
@@ -761,13 +761,13 @@ unsigned long mult_lower_bound(unsigned int ui, unsigned long ul) {
range(ui); // $ range=>=10
range((unsigned long)ui); // $ range=>=10
unsigned long result = (unsigned long)ui * ui;
range(result);
range(result); // $ range=>=100 range=>=100
return result; // BUG: upper bound should be >= 18446744065119617025
}
if (ul >= 10) {
range(ul); // $ range=>=10
unsigned long result = ul * ul;
range(result);
range(result); // $ range=>=100
return result; // BUG: lower bound should be 0 (overflow is possible)
}
return 0;
@@ -777,7 +777,7 @@ unsigned long mul_assign(unsigned int ui) {
if (ui <= 10 && ui >= 2) {
range(ui); // $ range=<=10 range=>=2
ui *= ui + 0;
range(ui);
range(ui); // $ range=<=100 range=>=4
return ui; // 4 .. 100
}
@@ -813,7 +813,7 @@ int mul_by_constant(int i, int j) {
range(i); // $ range===-1
range((int)0xffFFffFF); // $ range===-1
i = i * (int)0xffFFffFF; // fully converted literal is -1
range(i); // 1 .. 1
range(i); // $ range===1
}
i = i * -1;
range( i); // -2^31 .. 2^31-1