hohn/codeql
1
0
Fork 0
mirror of https://github.com/github/codeql.git synced 2025-12-17 01:03:14 +01:00
Code Issues Packages Projects Releases Wiki Activity

Merge pull request #12436 from MathiasVP/ir-range-analysis-for-unary-minus

Browse Source 
C++: IR-based range analysis for unary minus
This commit is contained in:
Robert Marsh
2023-03-13 09:02:38 -04:00
committed by GitHub
parent 0c95ab2cdc 619266d04b
commit 64f23ebb4d
2 changed files with 41 additions and 11 deletions
Download Patch File Download Diff File Expand all files Collapse all files

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

@@ -936,6 +936,15 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
bounded(cast.getOperand(), b, delta, upper, fromBackEdge, origdelta, reason)
}
/**
* Computes a normal form of `x` where -0.0 has changed to +0.0. This can be
* needed on the lesser side of a floating-point comparison or on both sides of
* a floating point equality because QL does not follow IEEE in floating-point
* comparisons but instead defines -0.0 to be less than and distinct from 0.0.
*/
bindingset[x]
private float normalizeFloatUp(float x) { result = x + 0.0 }
/**
* Holds if `b + delta` is a valid bound for `e`.
* - `upper = true` : `e <= b + delta`
@@ -1020,6 +1029,15 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
or
upper = false and delta = D::fromFloat(D::toFloat(d1).minimum(D::toFloat(d2)))
)
or
exists(SemExpr mid, D::Delta d, float f |
e.(SemNegateExpr).getOperand() = mid and
b instanceof SemZeroBound and
bounded(mid, b, d, upper.booleanNot(), fromBackEdge, origdelta, reason) and
f = normalizeFloatUp(-D::toFloat(d)) and
delta = D::fromFloat(f) and
if semPositive(e) then f >= 0 else any()
)
)
}

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

@@ -231,8 +231,8 @@ int test_unary(int a) {
int b = +a;
range(b); // $ range=<=11 range=>=3
int c = -a;
range(c);
range(b+c); // $ range=<=10 range="<=+ ...:a-1" range=">=- ...+1"
range(c); // $ range=<=-3 range=>=-11
range(b+c); // $ range=<=10 range="<=+ ...:a-1" range=">=- ...+1" range=>=-10
total += b+c;
range(total);
}
@@ -241,8 +241,8 @@ int test_unary(int a) {
int b = +a;
range(b); // $ range=<=11 range=>=0
int c = -a;
range(c);
range(b+c); // $ range=<=11 range="<=+ ...:a+0" range=">=- ...+0"
range(c); // $ range=<=0 range=>=-11
range(b+c); // $ range=<=11 range="<=+ ...:a+0" range=">=- ...+0" range=>=-11
total += b+c;
range(total);
}
@@ -251,7 +251,7 @@ int test_unary(int a) {
int b = +a;
range(b); // $ range=<=11 range=>=-7
int c = -a;
range(c);
range(c); // $ range=<=7 range=>=-11
range(b+c);
total += b+c;
range(total);
@@ -261,7 +261,7 @@ int test_unary(int a) {
int b = +a;
range(b); // $ range=<=1 range=>=-7
int c = -a;
range(c);
range(c); // $ range=<=7 range=>=-1
range(b+c);
total += b+c;
range(total);
@@ -271,8 +271,8 @@ int test_unary(int a) {
int b = +a;
range(b); // $ range=<=0 range=>=-7
int c = -a;
range(c);
range(b+c); // $ range="<=- ...+0" range=">=+ ...:a+0" range=>=-7
range(c); // $ range=<=7 range=>=0
range(b+c); // $ range="<=- ...+0" range=">=+ ...:a+0" range=>=-7 range=<=7
total += b+c;
range(total);
}
@@ -281,8 +281,8 @@ int test_unary(int a) {
int b = +a;
range(b); // $ range=<=-2 range=>=-7
int c = -a;
range(c);
range(b+c); // $ range="<=- ...-1" range=">=+ ...:a+1" range=>=-6
range(c); // $ range=<=7 range=>=2
range(b+c); // $ range="<=- ...-1" range=">=+ ...:a+1" range=>=-6 range=<=6
total += b+c;
range(total);
}
@@ -552,7 +552,7 @@ int test16(int x) {
range(x); // $ range=<=-1 range=>=0
return 1;
}
range(d); // $ range===3
range(d); // $ range=<=0 range=>=3 // Unreachable code
range(x); // $ range=<=-1 range=>=0
}
range(x); // $ range=>=0
@@ -997,3 +997,15 @@ void test_overflow() {
range(x + y); // $ range===-2147483393
}
}
void test_negate_unsigned(unsigned u) {
if(10 < u && u < 20) {
range<unsigned>(-u); // underflows
}
}
void test_negate_signed(int s) {
if(10 < s && s < 20) {
range<int>(-s); // $ range=<=-11 range=>=-19
}
}