Merge pull request #14664 from aschackmull/shared/modulus-step

RangeAnalysis: Improve bounds that rely on relative modulus.

Author: aschackmull

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

@@ -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"
   }
 }

shared/rangeanalysis/codeql/rangeanalysis/ModulusAnalysis.qll

@@ -264,6 +264,14 @@ 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
+      mod != 1 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