Merge branch 'main' into skip-safe-conversions-in-range-analysis

This commit is contained in:
Mathias Vorreiter Pedersen
2023-03-28 10:32:13 +01:00
36 changed files with 994 additions and 274 deletions

View File

@@ -1039,6 +1039,29 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
or
b = bRight and origdelta = odRight and reason = rRight and bLeft instanceof SemZeroBound
)
or
exists(
SemRemExpr rem, SemZeroBound b1, SemZeroBound b2, D::Delta d_max, D::Delta d1, D::Delta d2,
boolean fbe1, boolean fbe2, D::Delta od1, D::Delta od2, SemReason r1, SemReason r2
|
rem = e and
not (upper = true and semPositive(rem.getRightOperand())) and
not (upper = true and semPositive(rem.getLeftOperand())) and
boundedRemExpr(rem, b1, true, d1, fbe1, od1, r1) and
boundedRemExpr(rem, b2, false, d2, fbe2, od2, r2) and
(
if D::toFloat(d1).abs() > D::toFloat(d2).abs()
then (
b = b1 and d_max = d1 and fromBackEdge = fbe1 and origdelta = od1 and reason = r1
) else (
b = b2 and d_max = d2 and fromBackEdge = fbe2 and origdelta = od2 and reason = r2
)
)
|
upper = true and delta = D::fromFloat(D::toFloat(d_max).abs() - 1)
or
upper = false and delta = D::fromFloat(-D::toFloat(d_max).abs() + 1)
)
)
}
@@ -1065,4 +1088,11 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
bounded(add.getRightOperand(), b, delta, upper, fromBackEdge, origdelta, reason)
)
}
private predicate boundedRemExpr(
SemRemExpr rem, SemZeroBound b, boolean upper, D::Delta delta, boolean fromBackEdge,
D::Delta origdelta, SemReason reason
) {
bounded(rem.getRightOperand(), b, delta, upper, fromBackEdge, origdelta, reason)
}
}

View File

@@ -18,20 +18,20 @@ int test2(struct List* p) {
int count = 0;
for (; p; p = p->next) {
count = (count+1) % 10;
range(count); // $ range=<=9 range=<=count:p+1
range(count); // $ range=<=9 range=>=-9 range=<=count:p+1
}
range(count); // $ range=<=9
range(count); // $ range=>=-9 range=<=9
return count;
}
int test3(struct List* p) {
int count = 0;
for (; p; p = p->next) {
range(count++); // $ range=<=9
range(count++); // $ range=>=-9 range=<=9
count = count % 10;
range(count); // $ range=<=9 range="<=... +++0" range=<=count:p+1
range(count); // $ range=<=9 range=>=-9 range="<=... +++0" range=<=count:p+1
}
range(count); // $ range=<=9
range(count); // $ range=>=-9 range=<=9
return count;
}
@@ -964,7 +964,22 @@ void guard_bound_out_of_range(void) {
void test_mod(int s) {
int s2 = s % 5;
range(s2); // $ range=<=4 // -4 .. 4
range(s2); // $ range=>=-4 range=<=4
}
void test_mod_neg(int s) {
int s2 = s % -5;
range(s2); // $ range=>=-4 range=<=4
}
void test_mod_ternary(int s, bool b) {
int s2 = s % (b ? 5 : 500);
range(s2); // $ range=>=-499 range=<=499 range="<=... ? ... : ...-1"
}
void test_mod_ternary2(int s, bool b1, bool b2) {
int s2 = s % (b1 ? (b2 ? 5 : -5000) : -500000);
range(s2); // $ range=>=-499999 range=<=499999
}
void exit(int);