C++: Drop the bit size restriction in typeBound and use float

This commit is contained in:
Jeroen Ketema
2023-03-30 17:22:00 +02:00
parent dec1e4dfd6
commit 8d9b96b776
2 changed files with 41 additions and 44 deletions

View File

@@ -78,18 +78,15 @@ import experimental.semmle.code.cpp.semantic.SemanticLocation
/**
* Holds if `typ` is a small integral type with the given lower and upper bounds.
*/
private predicate typeBound(SemIntegerType typ, int lowerbound, int upperbound) {
private predicate typeBound(SemIntegerType typ, float lowerbound, float upperbound) {
exists(int bitSize | bitSize = typ.getByteSize() * 8 |
bitSize < 32 and
(
if typ.isSigned()
then (
upperbound = 1.bitShiftLeft(bitSize - 1) - 1 and
upperbound = 2.pow(bitSize - 1) - 1 and
lowerbound = -upperbound - 1
) else (
lowerbound = 0 and
upperbound = 1.bitShiftLeft(bitSize) - 1
)
upperbound = 2.pow(bitSize) - 1
)
)
}
@@ -286,10 +283,10 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
}
/** Gets the lower bound of the resulting type. */
int getLowerBound() { typeBound(getTrackedType(this), result, _) }
float getLowerBound() { typeBound(getTrackedType(this), result, _) }
/** Gets the upper bound of the resulting type. */
int getUpperBound() { typeBound(getTrackedType(this), _, result) }
float getUpperBound() { typeBound(getTrackedType(this), _, result) }
}
private module SignAnalysisInstantiated = SignAnalysis<D, UtilParam>; // TODO: will this cause reevaluation if it's instantiated with the same DeltaSig and UtilParam multiple times?

View File

@@ -566,11 +566,11 @@ unsigned int test_ternary01(unsigned int x) {
y1 = x < 100 ?
(range(x), x) : // $ range=<=99
(range(x), 10); // $ range=>=100
range(y1);
range(y1); // $ range=<=99
y2 = x >= 100 ?
(range(x), 10) : // $ range=>=100
(range(x), x); // $ range=<=99
range(y2);
range(y2); // $ range=<=99
y3 = 0;
y4 = 0;
y5 = 0;
@@ -580,14 +580,14 @@ unsigned int test_ternary01(unsigned int x) {
if (x < 300) {
range(x); // $ range=<=299
y3 = x ?:
(range(x), 5); // y3 < 300
range(y3);
(range(x), 5);
range(y3); // $ range=<=299
y4 = x ?:
(range(x), 500); // y4 <= 500
range(y4);
(range(x), 500);
range(y4); // $ range=<=500
y5 = (x+1) ?:
(range(x), 500); // $ range===-1
range(y5); // y5 <= 300
range(y5); // $ range=<=500
y6 = ((unsigned char)(x+1)) ?:
(range(x), 5); // $ range=<=299
range(y6); // y6 < 256
@@ -608,11 +608,11 @@ unsigned int test_ternary02(unsigned int x) {
y1 = x > 100 ?
(range(x), x) : // $ range=>=101
(range(x), 110); // $ range=<=100
range(y1); // y1 > 100
range(y1); // $ range=>=101
y2 = x <= 100 ?
(range(x), 110) : // $ range=<=100
(range(x), x); // $ range=>=101
range(y2); // y2 > 100
range(y2); // $ range=>=101
y3 = 1000;
y4 = 1000;
y5 = 1000;
@@ -620,15 +620,15 @@ unsigned int test_ternary02(unsigned int x) {
range(x); // $ range=>=300
y3 = (x-300) ?:
(range(x), 5); // $ range===300
range(y3); // y3 >= 0
range(y3); // $ range=>=0
y4 = (x-200) ?:
(range(x), 5); // $ range=<=200 range=>=300
range(y4); // y4 >= 100
range(y4); // $ SPURIOUS: range=>=5 MISSING: range=>=100
y5 = ((unsigned char)(x-200)) ?:
(range(x), 5); // $ range=>=300
range(y5); // y6 >= 0
}
range(y1 + y2 + y3 + y4 + y5); // $ MISSING: range=">=... = ...:... ? ... : ...+0" range=">=call to range+0"
range(y1 + y2 + y3 + y4 + y5); // $ range=">=call to range+207" MISSING: range=">=... = ...:... ? ... : ...+0" range=">=call to range+0"
return y1 + y2 + y3 + y4 + y5;
}
@@ -640,14 +640,14 @@ unsigned int test_comma01(unsigned int x) {
unsigned int y1;
unsigned int y2;
y1 = (++y, y);
range(y1); // $ range="==... ? ... : ...+1"
range(y1); // $ range=<=101 range="==... ? ... : ...+1"
y2 = (y++,
range(y), // $ range="==++ ...:... = ...+1" range="==... ? ... : ...+2"
range(y), // $ range=<=102 range="==++ ...:... = ...+1" range="==... ? ... : ...+2"
y += 3,
range(y), // $ range="==++ ...:... = ...+4" range="==... +++3" range="==... ? ... : ...+5"
range(y), // $ range=<=105 range="==++ ...:... = ...+4" range="==... +++3" range="==... ? ... : ...+5"
y);
range(y2); // $ range="==++ ...:... = ...+4" range="==... +++3" range="==... ? ... : ...+5"
range(y1 + y2); // $ MISSING: range=">=++ ...:... = ...+5" range=">=... +++4" range=">=... += ...:... = ...+1" range=">=... ? ... : ...+6"
range(y2); // $ range=<=105 range="==++ ...:... = ...+4" range="==... +++3" range="==... ? ... : ...+5"
range(y1 + y2); // $ range=<=206 range="<=... ? ... : ...+106" MISSING: range=">=++ ...:... = ...+5" range=">=... +++4" range=">=... += ...:... = ...+1" range=">=... ? ... : ...+6"
return y1 + y2;
}
@@ -683,27 +683,27 @@ int test_unsigned_mult01(unsigned int a, unsigned b) {
range(a); // $ range=<=11 range=>=3
range(b); // $ range=<=23 range=>=5
int r = a*b; // 15 .. 253
range(r);
range(r); // $ range=>=15 range=<=253
total += r;
range(total); // $ MISSING: range=>=1
range(total); // $ range=>=15 range=<=253
}
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=>=0 range=<=253
total += r;
range(total); // $ MISSING: range=">=(unsigned int)...+0" range=>=0
range(total); // $ range=>=0 range=<=506 range=">=(unsigned int)...+0" range="<=(unsigned int)...+253"
}
if (3 <= a && a <= 11 && 13 <= b && b <= 23) {
range(a); // $ range=<=11 range=>=3
range(b); // $ range=<=23 range=>=13
int r = a*b; // 39 .. 253
range(r);
range(r); // $ range=>=39 range=<=253
total += r;
range(total); // $ MISSING: range=">=(unsigned int)...+1" range=>=1
range(total); // $ range=>=39 range=<=759 range=">=(unsigned int)...+39" range="<=(unsigned int)...+506" range="<=(unsigned int)...+253"
}
range(total); // $ MISSING: range=">=(unsigned int)...+0" range=>=0
range(total); // $ range=>=0 range=<=759 range=">=(unsigned int)...+0" range="<=(unsigned int)...+506" range="<=(unsigned int)...+253"
return total;
}
@@ -713,25 +713,25 @@ int test_unsigned_mult02(unsigned b) {
if (5 <= b && b <= 23) {
range(b); // $ range=<=23 range=>=5
int r = 11*b; // 55 .. 253
range(r);
range(r); // $ range=>=55 range=<=253
total += r;
range(total); // $ MISSING: range=>=1
range(total); // $ range=>=55 range=<=253
}
if (0 <= b && b <= 23) {
range(b); // $ range=<=23 range=>=0
int r = 11*b; // 0 .. 253
range(r);
range(r); // $ range=>=0 range=<=253
total += r;
range(total); // $ MISSING: range=">=(unsigned int)...+0" range=>=0
range(total); // $ range=>=0 range=<=506 range=">=(unsigned int)...+0" range="<=(unsigned int)...+253"
}
if (13 <= b && b <= 23) {
range(b); // $ range=<=23 range=>=13
int r = 11*b; // 143 .. 253
range(r);
range(r); // $ range=>=143 range=<=253
total += r;
range(total); // $ MISSING: range=">=(unsigned int)...+1" range=>=1
range(total); // $ range=>=143 range=<=759 range=">=(unsigned int)...+143" range="<=(unsigned int)...+506" range="<=(unsigned int)...+253"
}
range(total); // $ MISSING: range=">=(unsigned int)...+0" range=>=0
range(total); // $ range=>=0 range=<=759 range=">=(unsigned int)...+0" range="<=(unsigned int)...+506" range="<=(unsigned int)...+253"
return total;
}