RangeAnalysis: Improve bounds that rely on relative modulus.

This commit is contained in:
Anders Schack-Mulligen 2023-11-02 11:36:46 +01:00
Родитель 484d0fe4cd
Коммит 7bf271fb6c
2 изменённых файлов: 11 добавлений и 6 удалений

Просмотреть файл

@ -1077,9 +1077,8 @@ void mask_at_start(int len) {
}
// Do something with leftOver
for (int index = leftOver; index < len; index+=64) {
range(index); // $ range="<=InitializeParameter: len-1"
// This should be in bounds
range(index + 16); // $ range="<=InitializeParameter: len+15" range="==Phi: index+16" MISSING: range="<=InitializeParameter: len-1"
range(index); // $ range="<=InitializeParameter: len-64" range=">=Store: ... & ... | Store: leftOver+0"
range(index + 63); // $ range="<=InitializeParameter: len-1" range="==Phi: index+63" range=">=Store: ... & ... | Store: leftOver+63"
}
}
@ -1095,8 +1094,7 @@ void mod_at_start(int len) {
}
// Do something with leftOver
for (int index = leftOver; index < len; index+=64) {
range(index); // $ range="<=InitializeParameter: len-1"
// This should be in bounds
range(index + 16); // $ range="<=InitializeParameter: len+15" range="==Phi: index+16" MISSING: range="<=InitializeParameter: len-49"
range(index); // $ range="<=InitializeParameter: len-64" range=">=Store: ... % ... | Store: leftOver+0"
range(index + 63); // $ range="<=InitializeParameter: len-1" range="==Phi: index+63" range=">=Store: ... % ... | Store: leftOver+63"
}
}

Просмотреть файл

@ -264,6 +264,13 @@ module ModulusAnalysis<
val = remainder(val0 + delta, mod)
)
or
exists(Sem::Expr mid, int v, int m1, int m2 |
exprModulus(mid, b, v, m1) and
e = modExpr(mid, m2) and
mod = m1.gcd(m2) and
val = remainder(v, mod)
)
or
exists(Sem::ConditionalExpr cond, int v1, int v2, int m1, int m2 |
cond = e and
condExprBranchModulus(cond, true, b, v1, m1) and