Merge branch 'main' into improve-insufficient-pw-hash-query

This commit is contained in:
smiddy007
2023-03-27 15:37:02 -04:00
committed by GitHub
3 changed files with 93 additions and 80 deletions

View File

@@ -591,24 +591,6 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
delta = D::fromInt(0) and
(upper = true or upper = false)
or
exists(SemExpr x | e2.(SemAddExpr).hasOperands(e1, x) |
// `x instanceof ConstantIntegerExpr` is covered by valueFlowStep
not x instanceof SemConstantIntegerExpr and
not e1 instanceof SemConstantIntegerExpr and
if strictlyPositiveIntegralExpr(x)
then upper = false and delta = D::fromInt(1)
else
if semPositive(x)
then upper = false and delta = D::fromInt(0)
else
if strictlyNegativeIntegralExpr(x)
then upper = true and delta = D::fromInt(-1)
else
if semNegative(x)
then upper = true and delta = D::fromInt(0)
else none()
)
or
exists(SemExpr x, SemSubExpr sub |
e2 = sub and
sub.getLeftOperand() = e1 and
@@ -1043,13 +1025,44 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
delta = D::fromFloat(f) and
if semPositive(e) then f >= 0 else any()
)
or
exists(
SemBound bLeft, SemBound bRight, D::Delta dLeft, D::Delta dRight, boolean fbeLeft,
boolean fbeRight, D::Delta odLeft, D::Delta odRight, SemReason rLeft, SemReason rRight
|
boundedAddOperand(e, upper, bLeft, false, dLeft, fbeLeft, odLeft, rLeft) and
boundedAddOperand(e, upper, bRight, true, dRight, fbeRight, odRight, rRight) and
delta = D::fromFloat(D::toFloat(dLeft) + D::toFloat(dRight)) and
fromBackEdge = fbeLeft.booleanOr(fbeRight)
|
b = bLeft and origdelta = odLeft and reason = rLeft and bRight instanceof SemZeroBound
or
b = bRight and origdelta = odRight and reason = rRight and bLeft instanceof SemZeroBound
)
)
}
pragma[nomagic]
private predicate boundedConditionalExpr(
SemConditionalExpr cond, SemBound b, boolean upper, boolean branch, D::Delta delta,
boolean fromBackEdge, D::Delta origdelta, SemReason reason
) {
bounded(cond.getBranchExpr(branch), b, delta, upper, fromBackEdge, origdelta, reason)
}
pragma[nomagic]
private predicate boundedAddOperand(
SemAddExpr add, boolean upper, SemBound b, boolean isLeft, D::Delta delta, boolean fromBackEdge,
D::Delta origdelta, SemReason reason
) {
// `semValueFlowStep` already handles the case where one of the operands is a constant.
not semValueFlowStep(add, _, _) and
(
isLeft = true and
bounded(add.getLeftOperand(), b, delta, upper, fromBackEdge, origdelta, reason)
or
isLeft = false and
bounded(add.getRightOperand(), b, delta, upper, fromBackEdge, origdelta, reason)
)
}
}

View File

@@ -40,13 +40,13 @@ int test4() {
int total = 0;
for (i = 0; i < 2; i = i+1) {
range(i); // $ range=<=1 range=>=0
range(total);
range(total); // $ range=>=0
total += i;
range(total);
range(total); // $ range=<=i+1 range=<=i+1 range=>=0 range=>=i+0
}
range(total);
range(total); // $ range=>=0
range(i); // $ range===2
range(total + i); // $ range=>=i+1
range(total + i); // $ range===i+2 range=>=2 range=>=i+0
return total + i;
}
@@ -55,13 +55,13 @@ int test5() {
int total = 0;
for (i = 0; i < 2; i++) {
range(i); // $ range=<=1 range=>=0
range(total);
range(total); // $ range=>=0
total += i;
range(total);
range(total); // $ range=<=i+1 range=>=0 range=>=i+0
}
range(total);
range(total); // $ range=>=0
range(i); // $ range===2
range(total + i); // $ range=>=i+1
range(total + i); // $ range===i+2 range=>=2 range=>=i+0
return total + i;
}
@@ -70,9 +70,9 @@ int test6() {
int total = 0;
for (i = 0; i+2 < 4; i = i+1) {
range(i); // $ range=<=1 range=>=0
range(total);
range(total); // $ range=>=0
total += i;
range(total);
range(total); // $ range=<=i+1 range=>=0 range=>=i+0
}
return total + i;
}
@@ -175,12 +175,12 @@ int test12() {
size_type Start = 0;
while (Start <= test12_helper()-1)
{
range(Start); // $ range=>=0
range(Start);
const size_type Length = test12_helper();
Start += Length + 1;
range(Start); // $ range=>=1 range=>=Start+1 range=">=call to test12_helper+1"
range(Start);
}
range(Start); // $ range=>=0
range(Start);
return 1;
}
@@ -194,8 +194,8 @@ int test13(char c, int i) {
range(y); // $ range===-1
int z = i+1;
range(z); // $ range===i+1
range(c + i + uc + x + y + z); // $ range=>=1 range=">=... - ...+0"
range((double)(c + i + uc + x + y + z)); // $ range=>=1 range=">=... - ...+0"
range(c + i + uc + x + y + z);
range((double)(c + i + uc + x + y + z));
return (double)(c + i + uc + x + y + z);
}
@@ -233,9 +233,9 @@ int test_unary(int a) {
range(b); // $ range=<=11 range=>=3
int c = -a;
range(c); // $ range=<=-3 range=>=-11
range(b+c); // $ range=<=10 range="<=+ ...:a-1" range=">=- ...+1" range=>=-10
range(b+c); // $ range=<=8 range=>=-8
total += b+c;
range(total);
range(total); // $ range=<=8 range=>=-8
}
if (0 <= a && a <= 11) {
range(a); // $ range=<=11 range=>=0
@@ -243,9 +243,9 @@ int test_unary(int a) {
range(b); // $ range=<=11 range=>=0
int c = -a;
range(c); // $ range=<=0 range=>=-11
range(b+c); // $ range=<=11 range="<=+ ...:a+0" range=">=- ...+0" range=>=-11
range(b+c); // $ range=<=11 range=>=-11
total += b+c;
range(total);
range(total); // $ range=<=0+11 range=<=19 range=>=0-11 range=>=-19
}
if (-7 <= a && a <= 11) {
range(a); // $ range=<=11 range=>=-7
@@ -253,9 +253,9 @@ int test_unary(int a) {
range(b); // $ range=<=11 range=>=-7
int c = -a;
range(c); // $ range=<=7 range=>=-11
range(b+c);
range(b+c); // $ range=<=18 range=>=-18
total += b+c;
range(total);
range(total); // $ range="<=- ...+18" range=">=- ...-18" range=<=0+29 range=<=37 range=>=0-29 range=>=-37
}
if (-7 <= a && a <= 1) {
range(a); // $ range=<=1 range=>=-7
@@ -263,9 +263,9 @@ int test_unary(int a) {
range(b); // $ range=<=1 range=>=-7
int c = -a;
range(c); // $ range=<=7 range=>=-1
range(b+c);
range(b+c); // $ range=<=8 range=>=-8
total += b+c;
range(total);
range(total); // $ range="<=- ...+8" range="<=- ...+26" range=">=- ...-8" range=">=- ...-26" range=<=0+37 range=<=45 range=>=0-37 range=>=-45
}
if (-7 <= a && a <= 0) {
range(a); // $ range=<=0 range=>=-7
@@ -273,9 +273,9 @@ int test_unary(int a) {
range(b); // $ range=<=0 range=>=-7
int c = -a;
range(c); // $ range=<=7 range=>=0
range(b+c); // $ range="<=- ...+0" range=">=+ ...:a+0" range=>=-7 range=<=7
range(b+c); // $ range=>=-7 range=<=7
total += b+c;
range(total);
range(total); // $ range="<=- ...+7" range="<=- ...+15" range="<=- ...+33" range=">=- ...-7" range=">=- ...-15" range=">=- ...-33" range=<=0+44 range=<=52 range=>=0-44 range=>=-52
}
if (-7 <= a && a <= -2) {
range(a); // $ range=<=-2 range=>=-7
@@ -283,11 +283,11 @@ int test_unary(int a) {
range(b); // $ range=<=-2 range=>=-7
int c = -a;
range(c); // $ range=<=7 range=>=2
range(b+c); // $ range="<=- ...-1" range=">=+ ...:a+1" range=>=-6 range=<=6
range(b+c); // $ range=<=5 range=>=-5
total += b+c;
range(total);
range(total); // $ range="<=- ...+5" range="<=- ...+12" range="<=- ...+20" range="<=- ...+38" range=">=- ...-5" range=">=- ...-12" range=">=- ...-20" range=">=- ...-38" range=<=0+49 range=<=57 range=>=0-49 range=>=-57
}
range(total);
range(total); // $ range="<=- ...+5" range="<=- ...+12" range="<=- ...+20" range="<=- ...+38" range=">=- ...-5" range=">=- ...-12" range=">=- ...-20" range=">=- ...-38" range=<=0+49 range=<=57 range=>=0-49 range=>=-57
return total;
}
@@ -302,7 +302,7 @@ int test_mult01(int a, int b) {
int r = a*b; // 15 .. 253
range(r);
total += r;
range(total); // $ range=>=1
range(total); // $ MISSING: range=>=1
}
if (3 <= a && a <= 11 && 0 <= b && b <= 23) {
range(a); // $ range=<=11 range=>=3
@@ -310,7 +310,7 @@ int test_mult01(int a, int b) {
int r = a*b; // 0 .. 253
range(r);
total += r;
range(total); // $ range=>=0 range=>=3+0
range(total); // $ MISSING: range=>=0 range=>=3+0
}
if (3 <= a && a <= 11 && -13 <= b && b <= 23) {
range(a); // $ range=<=11 range=>=3
@@ -326,7 +326,7 @@ int test_mult01(int a, int b) {
int r = a*b; // -143 .. 0
range(r);
total += r;
range(total); // $ range=<=3+0
range(total); // $ MISSING: range=<=3+0
}
if (3 <= a && a <= 11 && -13 <= b && b <= -7) {
range(a); // $ range=<=11 range=>=3
@@ -334,9 +334,9 @@ int test_mult01(int a, int b) {
int r = a*b; // -143 .. -21
range(r);
total += r;
range(total); // $ range=<=3-1
range(total); // $ MISSING: range=<=3-1
}
range(total); // $ range=<=3+0
range(total); // $ MISSING: range=<=3+0
return total;
}
@@ -350,7 +350,7 @@ int test_mult02(int a, int b) {
int r = a*b; // 0 .. 253
range(r);
total += r;
range(total); // $ range=>=0
range(total); // $ MISSING: range=>=0
}
if (0 <= a && a <= 11 && 0 <= b && b <= 23) {
range(a); // $ range=<=11 range=>=0
@@ -358,7 +358,7 @@ int test_mult02(int a, int b) {
int r = a*b; // 0 .. 253
range(r);
total += r;
range(total); // $ range=>=0 range=>=0+0
range(total); // $ MISSING: range=>=0 range=>=0+0
}
if (0 <= a && a <= 11 && -13 <= b && b <= 23) {
range(a); // $ range=<=11 range=>=0
@@ -374,7 +374,7 @@ int test_mult02(int a, int b) {
int r = a*b; // -143 .. 0
range(r);
total += r;
range(total); // $ range=<=0+0
range(total); // $ MISSING: range=<=0+0
}
if (0 <= a && a <= 11 && -13 <= b && b <= -7) {
range(a); // $ range=<=11 range=>=0
@@ -382,9 +382,9 @@ int test_mult02(int a, int b) {
int r = a*b; // -143 .. 0
range(r);
total += r;
range(total); // $ range=<=0+0
range(total); // $ MISSING: range=<=0+0
}
range(total); // $ range=<=0+0
range(total); // $ MISSING: range=<=0+0
return total;
}
@@ -445,7 +445,7 @@ int test_mult04(int a, int b) {
range(b); // $ range=<=23 range=>=5
int r = a*b; // -391 .. 0
total += r;
range(total); // $ range=<=0
range(total); // $ MISSING: range=<=0
}
if (-17 <= a && a <= 0 && 0 <= b && b <= 23) {
range(a); // $ range=<=0 range=>=-17
@@ -453,7 +453,7 @@ int test_mult04(int a, int b) {
int r = a*b; // -391 .. 0
range(r);
total += r;
range(total); // $ range="<=- ...+0" range=<=0
range(total); // $ MISSING: range="<=- ...+0" range=<=0
}
if (-17 <= a && a <= 0 && -13 <= b && b <= 23) {
range(a); // $ range=<=0 range=>=-17
@@ -469,7 +469,7 @@ int test_mult04(int a, int b) {
int r = a*b; // 0 .. 221
range(r);
total += r;
range(total); // $ range=">=- ...+0"
range(total); // $ MISSING: range=">=- ...+0"
}
if (-17 <= a && a <= 0 && -13 <= b && b <= -7) {
range(a); // $ range=<=0 range=>=-17
@@ -477,9 +477,9 @@ int test_mult04(int a, int b) {
int r = a*b; // 0 .. 221
range(r);
total += r;
range(total); // $ range=">=- ...+0"
range(total); // $ MISSING: range=">=- ...+0"
}
range(total); // $ range=">=- ...+0"
range(total); // $ MISSING: range=">=- ...+0"
return total;
}
@@ -493,7 +493,7 @@ int test_mult05(int a, int b) {
int r = a*b; // -391 .. -10
range(r);
total += r;
range(total); // $ range=<=-1
range(total); // $ MISSING: range=<=-1
}
if (-17 <= a && a <= -2 && 0 <= b && b <= 23) {
range(a); // $ range=<=-2 range=>=-17
@@ -501,7 +501,7 @@ int test_mult05(int a, int b) {
int r = a*b; // -391 .. 0
range(r);
total += r;
range(total); // $ range="<=- ...+0" range=<=0
range(total); // $ MISSING: range="<=- ...+0" range=<=0
}
if (-17 <= a && a <= -2 && -13 <= b && b <= 23) {
range(a); // $ range=<=-2 range=>=-17
@@ -517,7 +517,7 @@ int test_mult05(int a, int b) {
int r = a*b; // 0 .. 221
range(r);
total += r;
range(total); // $ range=">=- ...+0"
range(total); // $ MISSING: range=">=- ...+0"
}
if (-17 <= a && a <= -2 && -13 <= b && b <= -7) {
range(a); // $ range=<=-2 range=>=-17
@@ -525,9 +525,9 @@ int test_mult05(int a, int b) {
int r = a*b; // 14 .. 221
range(r);
total += r;
range(total); // $ range=">=- ...+1"
range(total); // $ MISSING: range=">=- ...+1"
}
range(total); // $ range=">=- ...+0"
range(total); // $ MISSING: range=">=- ...+0"
return total;
}
@@ -598,7 +598,7 @@ unsigned int test_ternary01(unsigned int x) {
(range(x), 500); // $ range=<=299
range(y8); // y8 <= 300
}
range(y1 + y2 + y3 + y4 + y5 + y6 + y7 + y8); // $ range=">=... = ...:... ? ... : ...+0" range=">=call to range+0"
range(y1 + y2 + y3 + y4 + y5 + y6 + y7 + y8); // $ MISSING: range=">=... = ...:... ? ... : ...+0" range=">=call to range+0"
return y1 + y2 + y3 + y4 + y5 + y6 + y7 + y8;
}
@@ -628,7 +628,7 @@ unsigned int test_ternary02(unsigned int x) {
(range(x), 5); // $ range=>=300
range(y5); // y6 >= 0
}
range(y1 + y2 + y3 + y4 + y5); // $ range=">=... = ...:... ? ... : ...+0" range=">=call to range+0"
range(y1 + y2 + y3 + y4 + y5); // $ MISSING: range=">=... = ...:... ? ... : ...+0" range=">=call to range+0"
return y1 + y2 + y3 + y4 + y5;
}
@@ -647,7 +647,7 @@ unsigned int test_comma01(unsigned int x) {
range(y), // $ range="==++ ...:... = ...+4" range="==... +++3" range="==... ? ... : ...+5"
y);
range(y2); // $ range="==++ ...:... = ...+4" range="==... +++3" range="==... ? ... : ...+5"
range(y1 + y2); // $ range=">=++ ...:... = ...+5" range=">=... +++4" range=">=... += ...:... = ...+1" range=">=... ? ... : ...+6"
range(y1 + y2); // $ MISSING: range=">=++ ...:... = ...+5" range=">=... +++4" range=">=... += ...:... = ...+1" range=">=... ? ... : ...+6"
return y1 + y2;
}
@@ -685,7 +685,7 @@ int test_unsigned_mult01(unsigned int a, unsigned b) {
int r = a*b; // 15 .. 253
range(r);
total += r;
range(total); // $ range=>=1
range(total); // $ MISSING: range=>=1
}
if (3 <= a && a <= 11 && 0 <= b && b <= 23) {
range(a); // $ range=<=11 range=>=3
@@ -693,7 +693,7 @@ int test_unsigned_mult01(unsigned int a, unsigned b) {
int r = a*b; // 0 .. 253
range(r);
total += r;
range(total); // $ range=">=(unsigned int)...+0" range=>=0
range(total); // $ MISSING: range=">=(unsigned int)...+0" range=>=0
}
if (3 <= a && a <= 11 && 13 <= b && b <= 23) {
range(a); // $ range=<=11 range=>=3
@@ -701,9 +701,9 @@ int test_unsigned_mult01(unsigned int a, unsigned b) {
int r = a*b; // 39 .. 253
range(r);
total += r;
range(total); // $ range=">=(unsigned int)...+1" range=>=1
range(total); // $ MISSING: range=">=(unsigned int)...+1" range=>=1
}
range(total); // $ range=">=(unsigned int)...+0" range=>=0
range(total); // $ MISSING: range=">=(unsigned int)...+0" range=>=0
return total;
}
@@ -715,23 +715,23 @@ int test_unsigned_mult02(unsigned b) {
int r = 11*b; // 55 .. 253
range(r);
total += r;
range(total); // $ range=>=1
range(total); // $ MISSING: range=>=1
}
if (0 <= b && b <= 23) {
range(b); // $ range=<=23 range=>=0
int r = 11*b; // 0 .. 253
range(r);
total += r;
range(total); // $ range=">=(unsigned int)...+0" range=>=0
range(total); // $ MISSING: range=">=(unsigned int)...+0" range=>=0
}
if (13 <= b && b <= 23) {
range(b); // $ range=<=23 range=>=13
int r = 11*b; // 143 .. 253
range(r);
total += r;
range(total); // $ range=">=(unsigned int)...+1" range=>=1
range(total); // $ MISSING: range=">=(unsigned int)...+1" range=>=1
}
range(total); // $ range=">=(unsigned int)...+0" range=>=0
range(total); // $ MISSING: range=">=(unsigned int)...+0" range=>=0
return total;
}
@@ -790,7 +790,7 @@ unsigned long mul_assign(unsigned int ui) {
range(ulconst); // $ range===10
ulconst *= 4;
range(ulconst); // $ range===40
range(uiconst + ulconst); // $ range=">=... *= ...+1" range=>=41
range(uiconst + ulconst); // $ range===80
return uiconst + ulconst; // 40 .. 40 for both
}
@@ -942,7 +942,7 @@ void widen_recursive_expr() {
for (s = 0; s < 10; s++) {
range(s); // $ range=<=9 range=>=0
int result = s + s;
range(result); // 0 .. 18
range(result); // $ range=<=18 range=<=s+9 range=>=0 range=>=s+0
}
}

View File

@@ -7,7 +7,7 @@
}
if (y - 2 == x && y > 300) {
range(x + y); // $ range=>=300 range=>=x+1 range=>=y-1
range(x + y); // $ range=<=802 range=>=600
return x + y;
}