Skip to content

Commit 7bf271f

Browse files
committed
RangeAnalysis: Improve bounds that rely on relative modulus.
1 parent 484d0fe commit 7bf271f

File tree

2 files changed

+11
-6
lines changed

2 files changed

+11
-6
lines changed

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

Lines changed: 4 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1077,9 +1077,8 @@ void mask_at_start(int len) {
10771077
}
10781078
// Do something with leftOver
10791079
for (int index = leftOver; index < len; index+=64) {
1080-
range(index); // $ range="<=InitializeParameter: len-1"
1081-
// This should be in bounds
1082-
range(index + 16); // $ range="<=InitializeParameter: len+15" range="==Phi: index+16" MISSING: range="<=InitializeParameter: len-1"
1080+
range(index); // $ range="<=InitializeParameter: len-64" range=">=Store: ... & ... | Store: leftOver+0"
1081+
range(index + 63); // $ range="<=InitializeParameter: len-1" range="==Phi: index+63" range=">=Store: ... & ... | Store: leftOver+63"
10831082
}
10841083
}
10851084

@@ -1095,8 +1094,7 @@ void mod_at_start(int len) {
10951094
}
10961095
// Do something with leftOver
10971096
for (int index = leftOver; index < len; index+=64) {
1098-
range(index); // $ range="<=InitializeParameter: len-1"
1099-
// This should be in bounds
1100-
range(index + 16); // $ range="<=InitializeParameter: len+15" range="==Phi: index+16" MISSING: range="<=InitializeParameter: len-49"
1097+
range(index); // $ range="<=InitializeParameter: len-64" range=">=Store: ... % ... | Store: leftOver+0"
1098+
range(index + 63); // $ range="<=InitializeParameter: len-1" range="==Phi: index+63" range=">=Store: ... % ... | Store: leftOver+63"
11011099
}
11021100
}

shared/rangeanalysis/codeql/rangeanalysis/ModulusAnalysis.qll

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -264,6 +264,13 @@ module ModulusAnalysis<
264264
val = remainder(val0 + delta, mod)
265265
)
266266
or
267+
exists(Sem::Expr mid, int v, int m1, int m2 |
268+
exprModulus(mid, b, v, m1) and
269+
e = modExpr(mid, m2) and
270+
mod = m1.gcd(m2) and
271+
val = remainder(v, mod)
272+
)
273+
or
267274
exists(Sem::ConditionalExpr cond, int v1, int v2, int m1, int m2 |
268275
cond = e and
269276
condExprBranchModulus(cond, true, b, v1, m1) and

0 commit comments

Comments
 (0)