Skip to content

Commit 99c6111

Browse files
committed
C++: Add support for bounded modulus operations
1 parent 62d2f23 commit 99c6111

File tree

2 files changed

+50
-6
lines changed

2 files changed

+50
-6
lines changed

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

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1039,6 +1039,28 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
10391039
or
10401040
b = bRight and origdelta = odRight and reason = rRight and bLeft instanceof SemZeroBound
10411041
)
1042+
or
1043+
exists(
1044+
SemRemExpr rem, SemZeroBound b1, SemZeroBound b2, D::Delta d_max, D::Delta d1, D::Delta d2,
1045+
boolean fbe1, boolean fbe2, D::Delta od1, D::Delta od2, SemReason r1, SemReason r2
1046+
|
1047+
rem = e and
1048+
boundedRemExpr(rem, b1, true, d1, fbe1, od1, r1) and
1049+
boundedRemExpr(rem, b2, false, d2, fbe2, od2, r2) and
1050+
(
1051+
if D::toFloat(d1).abs() > D::toFloat(d2).abs()
1052+
then (
1053+
b = b1 and d_max = d1 and fromBackEdge = fbe1 and origdelta = od1 and reason = r1
1054+
) else (
1055+
b = b2 and d_max = d2 and fromBackEdge = fbe2 and origdelta = od2 and reason = r2
1056+
)
1057+
) and
1058+
(
1059+
upper = true and delta = D::fromFloat(D::toFloat(d_max).abs() - 1)
1060+
or
1061+
upper = false and delta = D::fromFloat(-D::toFloat(d_max).abs() + 1)
1062+
)
1063+
)
10421064
)
10431065
}
10441066

@@ -1065,4 +1087,11 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
10651087
bounded(add.getRightOperand(), b, delta, upper, fromBackEdge, origdelta, reason)
10661088
)
10671089
}
1090+
1091+
private predicate boundedRemExpr(
1092+
SemRemExpr rem, SemZeroBound b, boolean upper, D::Delta delta, boolean fromBackEdge,
1093+
D::Delta origdelta, SemReason reason
1094+
) {
1095+
bounded(rem.getRightOperand(), b, delta, upper, fromBackEdge, origdelta, reason)
1096+
}
10681097
}

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

Lines changed: 21 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -18,20 +18,20 @@ int test2(struct List* p) {
1818
int count = 0;
1919
for (; p; p = p->next) {
2020
count = (count+1) % 10;
21-
range(count); // $ range=<=9
21+
range(count); // $ range=>=-9 range=<=9
2222
}
23-
range(count); // $ range=<=9
23+
range(count); // $ range=>=-9 range=<=9
2424
return count;
2525
}
2626

2727
int test3(struct List* p) {
2828
int count = 0;
2929
for (; p; p = p->next) {
30-
range(count++); // $ range=<=9
30+
range(count++); // $ range=>=-9 range=<=9
3131
count = count % 10;
32-
range(count); // $ range=<=9
32+
range(count); // $ range=>=-9 range=<=9
3333
}
34-
range(count); // $ range=<=9
34+
range(count); // $ range=>=-9 range=<=9
3535
return count;
3636
}
3737

@@ -960,7 +960,22 @@ void guard_bound_out_of_range(void) {
960960

961961
void test_mod(int s) {
962962
int s2 = s % 5;
963-
range(s2); // $ range=<=4 // -4 .. 4
963+
range(s2); // $ range=>=-4 range=<=4
964+
}
965+
966+
void test_mod_neg(int s) {
967+
int s2 = s % -5;
968+
range(s2); // $ range=>=-4 range=<=4
969+
}
970+
971+
void test_mod_ternary(int s, bool b) {
972+
int s2 = s % (b ? 5 : 500);
973+
range(s2); // $ range=>=-499 range=<=499
974+
}
975+
976+
void test_mod_ternary2(int s, bool b1, bool b2) {
977+
int s2 = s % (b1 ? (b2 ? 5 : -5000) : -500000);
978+
range(s2); // $ range=>=-499999 range=<=499999
964979
}
965980

966981
void exit(int);

0 commit comments

Comments
 (0)