From 6dfbb72fc88e95432c2736d5905e085d04b82868 Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <schack@semmle.com>
Date: Tue, 9 Oct 2018 12:04:37 +0200
Subject: [PATCH 1/9] Java: Add constant array lengths to ConstantIntegerExpr.

---
 java/ql/src/semmle/code/java/dataflow/RangeUtils.qll | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/java/ql/src/semmle/code/java/dataflow/RangeUtils.qll b/java/ql/src/semmle/code/java/dataflow/RangeUtils.qll
index 9b5e9a257a2..bec801248d7 100644
--- a/java/ql/src/semmle/code/java/dataflow/RangeUtils.qll
+++ b/java/ql/src/semmle/code/java/dataflow/RangeUtils.qll
@@ -15,6 +15,13 @@ private predicate constantIntegerExpr(Expr e, int val) {
     src = v.getDefiningExpr().(VariableAssign).getSource() and
     constantIntegerExpr(src, val)
   )
+  or
+  exists(SsaExplicitUpdate v, FieldRead arrlen |
+    e = arrlen and
+    arrlen.getField() instanceof ArrayLengthField and
+    arrlen.getQualifier() = v.getAUse() and
+    v.getDefiningExpr().(VariableAssign).getSource().(ArrayCreationExpr).getFirstDimensionSize() = val
+  )
 }
 
 /** An expression that always has the same integer value. */

From 8659bedbd914674b8ea3af6746729c9662966937 Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <schack@semmle.com>
Date: Tue, 9 Oct 2018 16:16:22 +0200
Subject: [PATCH 2/9] Java: Extract Bound class to its own file.

---
 .../src/semmle/code/java/dataflow/Bound.qll   | 58 +++++++++++++++++++
 .../code/java/dataflow/RangeAnalysis.qll      | 58 +------------------
 2 files changed, 60 insertions(+), 56 deletions(-)
 create mode 100644 java/ql/src/semmle/code/java/dataflow/Bound.qll

diff --git a/java/ql/src/semmle/code/java/dataflow/Bound.qll b/java/ql/src/semmle/code/java/dataflow/Bound.qll
new file mode 100644
index 00000000000..f607444908a
--- /dev/null
+++ b/java/ql/src/semmle/code/java/dataflow/Bound.qll
@@ -0,0 +1,58 @@
+import java
+private import SSA
+private import RangeUtils
+
+private newtype TBound =
+  TBoundZero() or
+  TBoundSsa(SsaVariable v) { v.getSourceVariable().getType() instanceof IntegralType } or
+  TBoundExpr(Expr e) { e.(FieldRead).getField() instanceof ArrayLengthField and not exists(SsaVariable v | e = v.getAUse()) }
+
+/**
+ * A bound that may be inferred for an expression plus/minus an integer delta.
+ */
+abstract class Bound extends TBound {
+  abstract string toString();
+  /** Gets an expression that equals this bound plus `delta`. */
+  abstract Expr getExpr(int delta);
+  /** Gets an expression that equals this bound. */
+  Expr getExpr() {
+    result = getExpr(0)
+  }
+  predicate hasLocationInfo(string path, int sl, int sc, int el, int ec) {
+    path = "" and sl = 0 and sc = 0 and el = 0 and ec = 0
+  }
+}
+
+/**
+ * The bound that corresponds to the integer 0. This is used to represent all
+ * integer bounds as bounds are always accompanied by an added integer delta.
+ */
+class ZeroBound extends Bound, TBoundZero {
+  override string toString() { result = "0" }
+  override Expr getExpr(int delta) { result.(ConstantIntegerExpr).getIntValue() = delta }
+}
+
+/**
+ * A bound corresponding to the value of an SSA variable.
+ */
+class SsaBound extends Bound, TBoundSsa {
+  /** Gets the SSA variable that equals this bound. */
+  SsaVariable getSsa() { this = TBoundSsa(result) }
+  override string toString() { result = getSsa().toString() }
+  override Expr getExpr(int delta) { result = getSsa().getAUse() and delta = 0 }
+  override predicate hasLocationInfo(string path, int sl, int sc, int el, int ec) {
+    getSsa().getLocation().hasLocationInfo(path, sl, sc, el, ec)
+  }
+}
+
+/**
+ * A bound that corresponds to the value of a specific expression that might be
+ * interesting, but isn't otherwise represented by the value of an SSA variable.
+ */
+class ExprBound extends Bound, TBoundExpr {
+  override string toString() { result = getExpr().toString() }
+  override Expr getExpr(int delta) { this = TBoundExpr(result) and delta = 0 }
+  override predicate hasLocationInfo(string path, int sl, int sc, int el, int ec) {
+    getExpr().hasLocationInfo(path, sl, sc, el, ec)
+  }
+}
diff --git a/java/ql/src/semmle/code/java/dataflow/RangeAnalysis.qll b/java/ql/src/semmle/code/java/dataflow/RangeAnalysis.qll
index d6d396e8c6a..d588da9e2dd 100644
--- a/java/ql/src/semmle/code/java/dataflow/RangeAnalysis.qll
+++ b/java/ql/src/semmle/code/java/dataflow/RangeAnalysis.qll
@@ -72,6 +72,7 @@ private import ParityAnalysis
 private import semmle.code.java.Reflection
 private import semmle.code.java.Collections
 private import semmle.code.java.Maps
+import Bound
 
 cached private module RangeAnalysisCache {
 
@@ -409,61 +410,6 @@ private predicate boundFlowStepDiv(Expr e2, Expr e1, int factor) {
   )
 }
 
-private newtype TBound =
-  TBoundZero() or
-  TBoundSsa(SsaVariable v) { v.getSourceVariable().getType() instanceof IntegralType } or
-  TBoundExpr(Expr e) { e.(FieldRead).getField() instanceof ArrayLengthField and not exists(SsaVariable v | e = v.getAUse()) }
-
-/**
- * A bound that may be inferred for an expression plus/minus an integer delta.
- */
-abstract class Bound extends TBound {
-  abstract string toString();
-  /** Gets an expression that equals this bound plus `delta`. */
-  abstract Expr getExpr(int delta);
-  /** Gets an expression that equals this bound. */
-  Expr getExpr() {
-    result = getExpr(0)
-  }
-  predicate hasLocationInfo(string path, int sl, int sc, int el, int ec) {
-    path = "" and sl = 0 and sc = 0 and el = 0 and ec = 0
-  }
-}
-
-/**
- * The bound that corresponds to the integer 0. This is used to represent all
- * integer bounds as bounds are always accompanied by an added integer delta.
- */
-class ZeroBound extends Bound, TBoundZero {
-  override string toString() { result = "0" }
-  override Expr getExpr(int delta) { result.(ConstantIntegerExpr).getIntValue() = delta }
-}
-
-/**
- * A bound corresponding to the value of an SSA variable.
- */
-class SsaBound extends Bound, TBoundSsa {
-  /** Gets the SSA variable that equals this bound. */
-  SsaVariable getSsa() { this = TBoundSsa(result) }
-  override string toString() { result = getSsa().toString() }
-  override Expr getExpr(int delta) { result = getSsa().getAUse() and delta = 0 }
-  override predicate hasLocationInfo(string path, int sl, int sc, int el, int ec) {
-    getSsa().getLocation().hasLocationInfo(path, sl, sc, el, ec)
-  }
-}
-
-/**
- * A bound that corresponds to the value of a specific expression that might be
- * interesting, but isn't otherwise represented by the value of an SSA variable.
- */
-class ExprBound extends Bound, TBoundExpr {
-  override string toString() { result = getExpr().toString() }
-  override Expr getExpr(int delta) { this = TBoundExpr(result) and delta = 0 }
-  override predicate hasLocationInfo(string path, int sl, int sc, int el, int ec) {
-    getExpr().hasLocationInfo(path, sl, sc, el, ec)
-  }
-}
-
 /**
  * Holds if `b + delta` is a valid bound for `v` at `pos`.
  * - `upper = true`  : `v <= b + delta`
@@ -632,7 +578,7 @@ private predicate baseBound(Expr e, int b, boolean upper) {
  */
 private predicate safeNarrowingCast(NarrowingCastExpr cast, boolean upper) {
   exists(int bound |
-    bounded(cast.getExpr(), TBoundZero(), bound, upper, _, _, _)
+    bounded(cast.getExpr(), any(ZeroBound zb), bound, upper, _, _, _)
     |
     upper = true and bound <= cast.getUpperBound() or
     upper = false and bound >= cast.getLowerBound()

From a78a0b52ec9142bb7d1b79a6ec5ef6f1eb8017ca Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <schack@semmle.com>
Date: Tue, 9 Oct 2018 16:24:25 +0200
Subject: [PATCH 3/9] Java: Add test.

---
 java/ql/test/query-tests/RangeAnalysis/A.java | 154 ++++++++++++++++++
 .../ArrayIndexOutOfBounds.expected            |  15 ++
 .../RangeAnalysis/ArrayIndexOutOfBounds.qlref |   1 +
 3 files changed, 170 insertions(+)
 create mode 100644 java/ql/test/query-tests/RangeAnalysis/A.java
 create mode 100644 java/ql/test/query-tests/RangeAnalysis/ArrayIndexOutOfBounds.expected
 create mode 100644 java/ql/test/query-tests/RangeAnalysis/ArrayIndexOutOfBounds.qlref

diff --git a/java/ql/test/query-tests/RangeAnalysis/A.java b/java/ql/test/query-tests/RangeAnalysis/A.java
new file mode 100644
index 00000000000..abe2b3d4aed
--- /dev/null
+++ b/java/ql/test/query-tests/RangeAnalysis/A.java
@@ -0,0 +1,154 @@
+public class A {
+  private static final int[] arr1 = new int[] { 1, 2, 3, 4, 5, 6, 7, 8 };
+  private final int[] arr2;
+  private final int[] arr3;
+
+  public A(int[] arr2, int n) {
+    if (arr2.length % 2 != 0)
+      throw new Exception();
+    this.arr2 = arr2;
+    this.arr3 = new int[n << 1];
+  }
+
+  void m1(int[] a) {
+    int sum = 0;
+    for (int i = 0; i <= a.length; i++) {
+      sum += a[i]; // Out of bounds
+    }
+  }
+
+  void m2(int[] a) {
+    int sum = 0;
+    for (int i = 0; i < a.length; i += 2) {
+      sum += a[i] + a[i + 1]; // Out of bounds (unless len%2==0)
+    }
+  }
+
+  void m3(int[] a) {
+    if (a.length % 2 != 0)
+      return;
+    int sum = 0;
+    for (int i = 0; i < a.length; ) {
+      sum += a[i++]; // OK
+      sum += a[i++]; // OK
+    }
+    for (int i = 0; i < arr1.length; ) {
+      sum += arr1[i++]; // OK
+      sum += arr1[i++]; // OK - FP
+      i += 2;
+    }
+    for (int i = 0; i < arr2.length; ) {
+      sum += arr2[i++]; // OK
+      sum += arr2[i++]; // OK - FP
+    }
+    for (int i = 0; i < arr3.length; ) {
+      sum += arr3[i++]; // OK
+      sum += arr3[i++]; // OK - FP
+    }
+    int[] b;
+    if (sum > 3)
+      b = a;
+    else
+      b = arr1;
+    for (int i = 0; i < b.length; i++) {
+      sum += b[i]; // OK
+      sum += b[++i]; // OK - FP
+    }
+  }
+
+  void m4(int[] a, int[] b) {
+    assert a.length % 2 == 0;
+    int sum = 0;
+    for (int i = 0; i < a.length; ) {
+      sum += a[i++]; // OK
+      sum += a[i++]; // OK - FP
+    }
+    int len = b.length;
+    if ((len & 1) != 0)
+      return;
+    for (int i = 0; i < len; ) {
+      sum += b[i++]; // OK
+      sum += b[i++]; // OK
+    }
+  }
+
+  void m5(int n) {
+    int[] a = new int[3 * n];
+    int sum = 0;
+    for (int i = 0; i < a.length; i += 3) {
+      sum += a[i] + a[i + 1] + a[i + 2]; // OK - FP
+    }
+  }
+
+  int m6(int[] a, int ix) {
+    if (ix < 0 || ix > a.length)
+      return 0;
+    return a[ix]; // Out of bounds
+  }
+
+  void m7() {
+    int[] xs = new int[11];
+    int sum = 0;
+    for (int i = 0; i < 11; i++) {
+      for (int j = 0; j < 11; j++) {
+        sum += xs[i]; // OK
+        sum += xs[j]; // OK
+        if (i < j)
+          sum += xs[i + 11 - j]; // OK - FP
+        else
+          sum += xs[i - j]; // OK
+      }
+    }
+  }
+
+  void m8(int[] a) {
+    if ((a.length - 4) % 3 != 0)
+      return;
+    int sum = 0;
+    for (int i = 4; i < a.length; i += 3) {
+      sum += a[i]; // OK
+      sum += a[i + 1]; // OK - FP
+      sum += a[i + 2]; // OK - FP
+    }
+  }
+
+  void m9() {
+    int[] a = new int[] { 1, 2, 3, 4, 5 };
+    int sum = 0;
+    for (int i = 0; i < 10; i++) {
+      if (i < 5)
+        sum += a[i]; // OK
+      else
+        sum += a[9 - i]; // OK - FP
+    }
+  }
+
+  void m10(int n, int m) {
+    int len = Math.min(n, m);
+    int[] a = new int[n];
+    int sum = 0;
+    for (int i = n - 1; i >= 0; i--) {
+      sum += a[i]; // OK
+      for (int j = i + 1; j < len; j++) {
+        sum += a[j]; // OK
+        sum += a[i + 1]; // OK - FP
+      }
+    }
+  }
+
+  void m11(int n) {
+    int len = n*2;
+    int[] a = new int[len];
+    int sum = 0;
+    for (int i = 0; i < len; i = i + 2) {
+      sum += a[i+1]; // OK
+      for (int j = i; j < len - 2; j = j + 2) {
+        sum += a[j]; // OK
+        sum += a[j+1]; // OK
+        sum += a[j+2]; // OK
+        sum += a[j+3]; // OK
+      }
+    }
+  }
+
+}
diff --git a/java/ql/test/query-tests/RangeAnalysis/ArrayIndexOutOfBounds.expected b/java/ql/test/query-tests/RangeAnalysis/ArrayIndexOutOfBounds.expected
new file mode 100644
index 00000000000..eb59dd6d262
--- /dev/null
+++ b/java/ql/test/query-tests/RangeAnalysis/ArrayIndexOutOfBounds.expected
@@ -0,0 +1,15 @@
+| A.java:16:14:16:17 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length. |
+| A.java:23:21:23:28 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length. |
+| A.java:37:14:37:22 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length. |
+| A.java:42:14:42:22 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length. |
+| A.java:46:14:46:22 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length. |
+| A.java:55:14:55:19 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length. |
+| A.java:64:14:64:19 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length. |
+| A.java:79:21:79:28 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length. |
+| A.java:79:32:79:39 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length + 1. |
+| A.java:86:12:86:16 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length. |
+| A.java:97:18:97:31 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length + 8. |
+| A.java:110:14:110:21 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length. |
+| A.java:111:14:111:21 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length + 1. |
+| A.java:122:16:122:23 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length + 3. |
+| A.java:134:16:134:23 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length. |
diff --git a/java/ql/test/query-tests/RangeAnalysis/ArrayIndexOutOfBounds.qlref b/java/ql/test/query-tests/RangeAnalysis/ArrayIndexOutOfBounds.qlref
new file mode 100644
index 00000000000..439f2fd18de
--- /dev/null
+++ b/java/ql/test/query-tests/RangeAnalysis/ArrayIndexOutOfBounds.qlref
@@ -0,0 +1 @@
+Likely Bugs/Collections/ArrayIndexOutOfBounds.ql

From e7b0d399d14b4e398afc528fd4db682050c4377d Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <schack@semmle.com>
Date: Tue, 9 Oct 2018 16:31:11 +0200
Subject: [PATCH 4/9] Java: Refactor parts of RangeAnalysis needed for
 ModulusAnalysis.

---
 .../code/java/dataflow/RangeAnalysis.qll      | 49 ++-----------
 .../semmle/code/java/dataflow/RangeUtils.qll  | 72 +++++++++++++++++++
 2 files changed, 77 insertions(+), 44 deletions(-)

diff --git a/java/ql/src/semmle/code/java/dataflow/RangeAnalysis.qll b/java/ql/src/semmle/code/java/dataflow/RangeAnalysis.qll
index d588da9e2dd..09a47566f08 100644
--- a/java/ql/src/semmle/code/java/dataflow/RangeAnalysis.qll
+++ b/java/ql/src/semmle/code/java/dataflow/RangeAnalysis.qll
@@ -100,23 +100,6 @@ cached private module RangeAnalysisCache {
 private import RangeAnalysisCache
 import RangeAnalysisPublic
 
-/**
- * Gets a condition that tests whether `v` equals `e + delta`.
- *
- * If the condition evaluates to `testIsTrue`:
- * - `isEq = true`  : `v == e + delta`
- * - `isEq = false` : `v != e + delta`
- */
-private Guard eqFlowCond(SsaVariable v, Expr e, int delta, boolean isEq, boolean testIsTrue) {
-  exists(boolean eqpolarity |
-    result.isEquality(ssaRead(v, delta), e, eqpolarity) and
-    (testIsTrue = true or testIsTrue = false) and
-    eqpolarity.booleanXor(testIsTrue).booleanNot() = isEq
-  )
-  or
-  exists(boolean testIsTrue0 | implies_v2(result, testIsTrue, eqFlowCond(v, e, delta, isEq, testIsTrue0), testIsTrue0))
-}
-
 /**
  * Holds if `comp` corresponds to:
  * - `upper = true`  : `v <= e + delta` or `v < e + delta`
@@ -207,14 +190,8 @@ class CondReason extends Reason, TCondReason {
  * - `upper = false` : `v >= e + delta`
  */
 private predicate boundFlowStepSsa(SsaVariable v, SsaReadPosition pos, Expr e, int delta, boolean upper, Reason reason) {
-  exists(SsaExplicitUpdate upd | v = upd and pos.hasReadOfVar(v) and reason = TNoReason() |
-    upd.getDefiningExpr().(VariableAssign).getSource() = e and delta = 0 and (upper = true or upper = false) or
-    upd.getDefiningExpr().(PostIncExpr).getExpr() = e and delta = 1 and (upper = true or upper = false) or
-    upd.getDefiningExpr().(PreIncExpr).getExpr() = e and delta = 1 and (upper = true or upper = false) or
-    upd.getDefiningExpr().(PostDecExpr).getExpr() = e and delta = -1 and (upper = true or upper = false) or
-    upd.getDefiningExpr().(PreDecExpr).getExpr() = e and delta = -1 and (upper = true or upper = false) or
-    upd.getDefiningExpr().(AssignOp) = e and delta = 0 and (upper = true or upper = false)
-  ) or
+  ssaUpdateStep(v, e, delta) and pos.hasReadOfVar(v) and (upper = true or upper = false) and reason = TNoReason()
+  or
   exists(Guard guard, boolean testIsTrue |
     pos.hasReadOfVar(v) and
     guard = boundFlowCond(v, e, delta, upper, testIsTrue) and
@@ -291,22 +268,8 @@ private class NarrowingCastExpr extends CastExpr {
  * - `upper = false` : `e2 >= e1 + delta`
  */
 private predicate boundFlowStep(Expr e2, Expr e1, int delta, boolean upper) {
-  e2.(ParExpr).getExpr() = e1 and delta = 0 and (upper = true or upper = false) or
-  e2.(AssignExpr).getSource() = e1 and delta = 0 and (upper = true or upper = false) or
-  e2.(PlusExpr).getExpr() = e1 and delta = 0 and (upper = true or upper = false) or
-  e2.(PostIncExpr).getExpr() = e1 and delta = 0 and (upper = true or upper = false) or
-  e2.(PostDecExpr).getExpr() = e1 and delta = 0 and (upper = true or upper = false) or
-  e2.(PreIncExpr).getExpr() = e1 and delta = 1 and (upper = true or upper = false) or
-  e2.(PreDecExpr).getExpr() = e1 and delta = -1 and (upper = true or upper = false) or
+  valueFlowStep(e2, e1, delta) and (upper = true or upper = false) or
   e2.(SafeCastExpr).getExpr() = e1 and delta = 0 and (upper = true or upper = false) or
-  exists(SsaExplicitUpdate v, FieldRead arrlen |
-    e2 = arrlen and
-    arrlen.getField() instanceof ArrayLengthField and
-    arrlen.getQualifier() = v.getAUse() and
-    v.getDefiningExpr().(VariableAssign).getSource().(ArrayCreationExpr).getDimension(0) = e1 and
-    delta = 0 and
-    (upper = true or upper = false)
-  ) or
   exists(Expr x |
     e2.(AddExpr).hasOperands(e1, x) or
     exists(AssignAddExpr add | add = e2 |
@@ -314,8 +277,7 @@ private predicate boundFlowStep(Expr e2, Expr e1, int delta, boolean upper) {
       add.getDest() = x and add.getRhs() = e1
     )
     |
-    x.(ConstantIntegerExpr).getIntValue() = delta and (upper = true or upper = false)
-    or
+    // `x instanceof ConstantIntegerExpr` is covered by valueFlowStep
     not x instanceof ConstantIntegerExpr and
     not e1 instanceof ConstantIntegerExpr and
     if strictlyPositive(x) then
@@ -341,8 +303,7 @@ private predicate boundFlowStep(Expr e2, Expr e1, int delta, boolean upper) {
       sub.getRhs() = x
     )
     |
-    x.(ConstantIntegerExpr).getIntValue() = -delta and (upper = true or upper = false)
-    or
+    // `x instanceof ConstantIntegerExpr` is covered by valueFlowStep
     not x instanceof ConstantIntegerExpr and
     if strictlyPositive(x) then
       (upper = true and delta = -1)
diff --git a/java/ql/src/semmle/code/java/dataflow/RangeUtils.qll b/java/ql/src/semmle/code/java/dataflow/RangeUtils.qll
index bec801248d7..131d62ccdaf 100644
--- a/java/ql/src/semmle/code/java/dataflow/RangeUtils.qll
+++ b/java/ql/src/semmle/code/java/dataflow/RangeUtils.qll
@@ -138,3 +138,75 @@ predicate guardControlsSsaRead(Guard guard, SsaReadPosition controlled, boolean
     guardControlsSsaRead(guard0, controlled, testIsTrue0)
   )
 }
+
+/**
+ * Gets a condition that tests whether `v` equals `e + delta`.
+ *
+ * If the condition evaluates to `testIsTrue`:
+ * - `isEq = true`  : `v == e + delta`
+ * - `isEq = false` : `v != e + delta`
+ */
+Guard eqFlowCond(SsaVariable v, Expr e, int delta, boolean isEq, boolean testIsTrue) {
+  exists(boolean eqpolarity |
+    result.isEquality(ssaRead(v, delta), e, eqpolarity) and
+    (testIsTrue = true or testIsTrue = false) and
+    eqpolarity.booleanXor(testIsTrue).booleanNot() = isEq
+  )
+  or
+  exists(boolean testIsTrue0 | implies_v2(result, testIsTrue, eqFlowCond(v, e, delta, isEq, testIsTrue0), testIsTrue0))
+}
+
+/**
+ * Holds if `v` is an `SsaExplicitUpdate` that equals `e + delta`.
+ */
+predicate ssaUpdateStep(SsaExplicitUpdate v, Expr e, int delta) {
+  v.getDefiningExpr().(VariableAssign).getSource() = e and delta = 0 or
+  v.getDefiningExpr().(PostIncExpr).getExpr() = e and delta = 1 or
+  v.getDefiningExpr().(PreIncExpr).getExpr() = e and delta = 1 or
+  v.getDefiningExpr().(PostDecExpr).getExpr() = e and delta = -1 or
+  v.getDefiningExpr().(PreDecExpr).getExpr() = e and delta = -1 or
+  v.getDefiningExpr().(AssignOp) = e and delta = 0
+}
+
+/**
+ * Holds if `e1 + delta` equals `e2`.
+ */
+predicate valueFlowStep(Expr e2, Expr e1, int delta) {
+  e2.(ParExpr).getExpr() = e1 and delta = 0 or
+  e2.(AssignExpr).getSource() = e1 and delta = 0 or
+  e2.(PlusExpr).getExpr() = e1 and delta = 0 or
+  e2.(PostIncExpr).getExpr() = e1 and delta = 0 or
+  e2.(PostDecExpr).getExpr() = e1 and delta = 0 or
+  e2.(PreIncExpr).getExpr() = e1 and delta = 1 or
+  e2.(PreDecExpr).getExpr() = e1 and delta = -1 or
+  exists(SsaExplicitUpdate v, FieldRead arrlen |
+    e2 = arrlen and
+    arrlen.getField() instanceof ArrayLengthField and
+    arrlen.getQualifier() = v.getAUse() and
+    v.getDefiningExpr().(VariableAssign).getSource().(ArrayCreationExpr).getDimension(0) = e1 and
+    delta = 0
+  ) or
+  exists(Expr x |
+    e2.(AddExpr).hasOperands(e1, x) or
+    exists(AssignAddExpr add | add = e2 |
+      add.getDest() = e1 and add.getRhs() = x or
+      add.getDest() = x and add.getRhs() = e1
+    )
+    |
+    x.(ConstantIntegerExpr).getIntValue() = delta
+  ) or
+  exists(Expr x |
+    exists(SubExpr sub |
+      e2 = sub and
+      sub.getLeftOperand() = e1 and
+      sub.getRightOperand() = x
+    ) or
+    exists(AssignSubExpr sub |
+      e2 = sub and
+      sub.getDest() = e1 and
+      sub.getRhs() = x
+    )
+    |
+    x.(ConstantIntegerExpr).getIntValue() = -delta
+  )
+}

From 5c5324961279804d2a1f622fa49479d93a096fc9 Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <schack@semmle.com>
Date: Wed, 10 Oct 2018 14:02:51 +0200
Subject: [PATCH 5/9] Java: Add ModulusAnalysis.

---
 .../code/java/dataflow/ModulusAnalysis.qll    | 322 ++++++++++++++++++
 .../code/java/dataflow/RangeAnalysis.qll      |  33 +-
 java/ql/test/query-tests/RangeAnalysis/A.java |   2 +-
 .../ArrayIndexOutOfBounds.expected            |   2 -
 4 files changed, 351 insertions(+), 8 deletions(-)
 create mode 100644 java/ql/src/semmle/code/java/dataflow/ModulusAnalysis.qll

diff --git a/java/ql/src/semmle/code/java/dataflow/ModulusAnalysis.qll b/java/ql/src/semmle/code/java/dataflow/ModulusAnalysis.qll
new file mode 100644
index 00000000000..32133d785ff
--- /dev/null
+++ b/java/ql/src/semmle/code/java/dataflow/ModulusAnalysis.qll
@@ -0,0 +1,322 @@
+/**
+ * Provides inferences of the form: `e` equals `b + v` modulo `m` where `e` is
+ * an expression, `b` is a `Bound` (typically zero or the value of an SSA
+ * variable), and `v` is an integer in the range `[0 .. m-1]`.
+ */
+
+import java
+private import SSA
+private import RangeUtils
+private import semmle.code.java.controlflow.Guards
+import Bound
+
+/**
+ * Holds if `e + delta` equals `v` at `pos`.
+ */
+private predicate valueFlowStepSsa(SsaVariable v, SsaReadPosition pos, Expr e, int delta) {
+  ssaUpdateStep(v, e, delta) and pos.hasReadOfVar(v)
+  or
+  exists(Guard guard, boolean testIsTrue |
+    pos.hasReadOfVar(v) and
+    guard = eqFlowCond(v, e, delta, true, testIsTrue) and
+    guardDirectlyControlsSsaRead(guard, pos, testIsTrue)
+  )
+}
+
+/**
+ * Holds if `add` is the addition of `larg` and `rarg`, neither of which are
+ * `ConstantIntegerExpr`s.
+ */
+private predicate nonConstAddition(Expr add, Expr larg, Expr rarg) {
+  (
+    exists(AddExpr a | a = add |
+      larg = a.getLeftOperand() and
+      rarg = a.getRightOperand()
+    ) or
+    exists(AssignAddExpr a | a = add |
+      larg = a.getDest() and
+      rarg = a.getRhs()
+    )
+  ) and
+  not larg instanceof ConstantIntegerExpr and
+  not rarg instanceof ConstantIntegerExpr
+}
+
+/**
+ * Holds if `sub` is the subtraction of `larg` and `rarg`, where `rarg` is not
+ * a `ConstantIntegerExpr`.
+ */
+private predicate nonConstSubtraction(Expr sub, Expr larg, Expr rarg) {
+  (
+    exists(SubExpr s | s = sub |
+      larg = s.getLeftOperand() and
+      rarg = s.getRightOperand()
+    ) or
+    exists(AssignSubExpr s | s = sub |
+      larg = s.getDest() and
+      rarg = s.getRhs()
+    )
+  ) and
+  not rarg instanceof ConstantIntegerExpr
+}
+
+/** Gets an expression that is the remainder modulo `mod` of `arg`. */
+private Expr modExpr(Expr arg, int mod) {
+  exists(RemExpr rem |
+    result = rem and
+    arg = rem.getLeftOperand() and
+    rem.getRightOperand().(CompileTimeConstantExpr).getIntValue() = mod and
+    mod >= 2
+  ) or
+  exists(CompileTimeConstantExpr c |
+    mod = 2.pow([1..30]) and
+    c.getIntValue() = mod - 1 and
+    result.(AndBitwiseExpr).hasOperands(arg, c)
+  ) or
+  result.(ParExpr).getExpr() = modExpr(arg, mod)
+}
+
+/**
+ * Gets a guard that tests whether `v` is congruent with `val` modulo `mod` on
+ * its `testIsTrue` branch.
+ */
+private Guard moduloCheck(SsaVariable v, int val, int mod, boolean testIsTrue) {
+  exists(Expr rem, CompileTimeConstantExpr c, int r, boolean polarity |
+    result.isEquality(rem, c, polarity) and
+    c.getIntValue() = r and
+    rem = modExpr(v.getAUse(), mod) and
+    (
+      testIsTrue = polarity and val = r
+      or
+      testIsTrue = polarity.booleanNot() and mod = 2 and val = 1 - r and
+      (r = 0 or r = 1)
+    )
+  )
+}
+
+/**
+ * Holds if a guard ensures that `v` at `pos` is congruent with `val` modulo `mod`.
+ */
+private predicate moduloGuardedRead(SsaVariable v, SsaReadPosition pos, int val, int mod) {
+  exists(Guard guard, boolean testIsTrue |
+    pos.hasReadOfVar(v) and
+    guard = moduloCheck(v, val, mod, testIsTrue) and
+    guardControlsSsaRead(guard, pos, testIsTrue)
+  )
+}
+
+/** Holds if `factor` is a power of 2 that divides `mask`. */
+bindingset[mask]
+private predicate andmaskFactor(int mask, int factor) {
+  mask % factor = 0 and
+  factor = 2.pow([1..30])
+}
+
+/** Holds if `e` is evenly divisible by `factor`. */
+private predicate evenlyDivisibleExpr(Expr e, int factor) {
+  exists(ConstantIntegerExpr c, int k | k = c.getIntValue() |
+    e.(MulExpr).getAnOperand() = c and factor = k.abs() and factor >= 2 or
+    e.(AssignMulExpr).getSource() = c and factor = k.abs() and factor >= 2 or
+    e.(LShiftExpr).getRightOperand() = c and factor = 2.pow(k) and k > 0 or
+    e.(AssignLShiftExpr).getRhs() = c and factor = 2.pow(k) and k > 0 or
+    e.(AndBitwiseExpr).getAnOperand() = c and factor = max(int f | andmaskFactor(k, f)) or
+    e.(AssignAndExpr).getSource() = c and factor = max(int f | andmaskFactor(k, f))
+  )
+}
+
+private predicate id(BasicBlock x, BasicBlock y) { x = y }
+
+private predicate idOf(BasicBlock x, int y) = equivalenceRelation(id/2)(x, y)
+
+private int getId(BasicBlock bb) { idOf(bb, result) }
+
+/**
+ * Holds if `inp` is an input to `phi` along `edge` and this input has index `r`
+ * in an arbitrary 1-based numbering of the input edges to `phi`.
+ */
+private predicate rankedPhiInput(SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge, int r) {
+  edge.phiInput(phi, inp) and
+  edge = rank[r](SsaReadPositionPhiInputEdge e | e.phiInput(phi, _) | e order by getId(e.getOrigBlock()))
+}
+
+/**
+ * Holds if `rix` is the number of input edges to `phi`.
+ */
+private predicate maxPhiInputRank(SsaPhiNode phi, int rix) {
+  rix = max(int r | rankedPhiInput(phi, _, _, r))
+}
+
+private int gcdLim() { result = 128 }
+
+/**
+ * Gets the greatest common divisor of `x` and `y`. This is restricted to small
+ * inputs and the case when `x` and `y` are not relatively prime.
+ */
+private int gcd(int x, int y) {
+  result != 1 and
+  result = x.abs() and y = 0 and x in [-gcdLim()..gcdLim()]
+  or
+  result = gcd(y, x % y) and y != 0 and x in [-gcdLim()..gcdLim()]
+}
+
+/**
+ * Gets the remainder of `val` modulo `mod`.
+ *
+ * For `mod = 0` the result equals `val` and for `mod > 1` the result is within
+ * the range `[0 .. mod-1]`.
+ */
+bindingset[val, mod]
+private int remainder(int val, int mod) {
+  mod = 0 and result = val or
+  mod > 1 and result = ((val % mod) + mod) % mod
+}
+
+/**
+ * Holds if `inp` is an input to `phi` and equals `phi` modulo `mod` along `edge`.
+ */
+private predicate phiSelfModulus(SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge, int mod) {
+  exists(SsaBound phibound, int v, int m |
+    edge.phiInput(phi, inp) and
+    phibound.getSsa() = phi and
+    ssaModulus(inp, edge, phibound, v, m) and
+    mod = gcd(m, v) and
+    mod != 1
+  )
+}
+
+/**
+ * Holds if `b + val` modulo `mod` is a candidate congruence class for `phi`.
+ */
+private predicate phiModulusInit(SsaPhiNode phi, Bound b, int val, int mod) {
+  exists(SsaVariable inp, SsaReadPositionPhiInputEdge edge |
+    edge.phiInput(phi, inp) and
+    ssaModulus(inp, edge, b, val, mod)
+  )
+}
+
+/**
+ * Holds if all inputs to `phi` numbered `1` to `rix` are equal to `b + val` modulo `mod`.
+ */
+private predicate phiModulusRankStep(SsaPhiNode phi, Bound b, int val, int mod, int rix) {
+  rix = 0 and
+  phiModulusInit(phi, b, val, mod)
+  or
+  exists(SsaVariable inp, SsaReadPositionPhiInputEdge edge, int v1, int m1 |
+    mod != 1 and
+    val = remainder(v1, mod)
+    |
+    exists(int v2, int m2 |
+      rankedPhiInput(phi, inp, edge, rix) and
+      phiModulusRankStep(phi, b, v1, m1, rix - 1) and
+      ssaModulus(inp, edge, b, v2, m2) and
+      mod = gcd(gcd(m1, m2), v1 - v2)
+    )
+    or
+    exists(int m2 |
+      rankedPhiInput(phi, inp, edge, rix) and
+      phiModulusRankStep(phi, b, v1, m1, rix - 1) and
+      phiSelfModulus(phi, inp, edge, m2) and
+      mod = gcd(m1, m2)
+    )
+  )
+}
+
+/**
+ * Holds if `phi` is equal to `b + val` modulo `mod`.
+ */
+private predicate phiModulus(SsaPhiNode phi, Bound b, int val, int mod) {
+  exists(int r |
+    maxPhiInputRank(phi, r) and
+    phiModulusRankStep(phi, b, val, mod, r)
+  )
+}
+
+/**
+ * Holds if `v` at `pos` is equal to `b + val` modulo `mod`.
+ */
+private predicate ssaModulus(SsaVariable v, SsaReadPosition pos, Bound b, int val, int mod) {
+  phiModulus(v, b, val, mod) and pos.hasReadOfVar(v)
+  or
+  b.(SsaBound).getSsa() = v and pos.hasReadOfVar(v) and val = 0 and mod = 0
+  or
+  exists(Expr e, int val0, int delta |
+    exprModulus(e, b, val0, mod) and
+    valueFlowStepSsa(v, pos, e, delta) and
+    val = remainder(val0 + delta, mod)
+  )
+  or
+  moduloGuardedRead(v, pos, val, mod) and b instanceof ZeroBound
+}
+
+/**
+ * Holds if `e` is equal to `b + val` modulo `mod`.
+ *
+ * There are two cases for the modulus:
+ * - `mod = 0`: The equality `e = b + val` is an ordinary equality.
+ * - `mod > 1`: `val` lies within the range `[0 .. mod-1]`.
+ */
+cached
+predicate exprModulus(Expr e, Bound b, int val, int mod) {
+  e = b.getExpr(val) and mod = 0 or
+  evenlyDivisibleExpr(e, mod) and val = 0 and b instanceof ZeroBound or
+  exists(SsaVariable v, SsaReadPositionBlock bb |
+    ssaModulus(v, bb, b, val, mod) and
+    e = v.getAUse() and
+    bb.getBlock() = e.getBasicBlock()
+  ) or
+  exists(Expr mid, int val0, int delta |
+    exprModulus(mid, b, val0, mod) and
+    valueFlowStep(e, mid, delta) and
+    val = remainder(val0 + delta, mod)
+  ) or
+  exists(ConditionalExpr cond, int v1, int v2, int m1, int m2 |
+    cond = e and
+    condExprBranchModulus(cond, true, b, v1, m1) and
+    condExprBranchModulus(cond, false, b, v2, m2) and
+    mod = gcd(gcd(m1, m2), v1 - v2) and
+    mod != 1 and
+    val = remainder(v1, mod)
+  ) or
+  exists(Bound b1, Bound b2, int v1, int v2, int m1, int m2 |
+    addModulus(e, true, b1, v1, m1) and
+    addModulus(e, false, b2, v2, m2) and
+    mod = gcd(m1, m2) and
+    mod != 1 and
+    val = remainder(v1 + v2, mod)
+    |
+    b = b1 and b2 instanceof ZeroBound or
+    b = b2 and b1 instanceof ZeroBound
+  ) or
+  exists(int v1, int v2, int m1, int m2 |
+    subModulus(e, true, b, v1, m1) and
+    subModulus(e, false, any(ZeroBound zb), v2, m2) and
+    mod = gcd(m1, m2) and
+    mod != 1 and
+    val = remainder(v1 - v2, mod)
+  )
+}
+
+private predicate condExprBranchModulus(ConditionalExpr cond, boolean branch, Bound b, int val, int mod) {
+  exprModulus(cond.getTrueExpr(), b, val, mod) and branch = true or
+  exprModulus(cond.getFalseExpr(), b, val, mod) and branch = false
+}
+
+private predicate addModulus(Expr add, boolean isLeft, Bound b, int val, int mod) {
+  exists(Expr larg, Expr rarg |
+    nonConstAddition(add, larg, rarg)
+  |
+    exprModulus(larg, b, val, mod) and isLeft = true
+    or
+    exprModulus(rarg, b, val, mod) and isLeft = false
+  )
+}
+
+private predicate subModulus(Expr sub, boolean isLeft, Bound b, int val, int mod) {
+  exists(Expr larg, Expr rarg |
+    nonConstSubtraction(sub, larg, rarg)
+  |
+    exprModulus(larg, b, val, mod) and isLeft = true
+    or
+    exprModulus(rarg, b, val, mod) and isLeft = false
+  )
+}
diff --git a/java/ql/src/semmle/code/java/dataflow/RangeAnalysis.qll b/java/ql/src/semmle/code/java/dataflow/RangeAnalysis.qll
index 09a47566f08..d5acafa47ce 100644
--- a/java/ql/src/semmle/code/java/dataflow/RangeAnalysis.qll
+++ b/java/ql/src/semmle/code/java/dataflow/RangeAnalysis.qll
@@ -68,7 +68,7 @@ private import SSA
 private import RangeUtils
 private import semmle.code.java.controlflow.internal.GuardsLogic
 private import SignAnalysis
-private import ParityAnalysis
+private import ModulusAnalysis
 private import semmle.code.java.Reflection
 private import semmle.code.java.Collections
 private import semmle.code.java.Maps
@@ -133,6 +133,29 @@ private predicate boundCondition(ComparisonExpr comp, SsaVariable v, Expr e, int
   )
 }
 
+/**
+ * Holds if `comp` is a comparison between `x` and `y` for which `y - x` has a
+ * fixed value modulo some `mod > 1`, such that the comparison can be
+ * strengthened by `strengthen` when evaluating to `testIsTrue`.
+ */
+private predicate modulusComparison(ComparisonExpr comp, boolean testIsTrue, int strengthen) {
+  exists(Bound b, int v1, int v2, int mod, boolean resultIsStrict, int d, int k |
+    // If `x <= y` and `x =(mod) b + v1` and `y =(mod) b + v2` then
+    // `0 <= y - x =(mod) v2 - v1`. By choosing `k =(mod) v2 - v1` with
+    // `0 <= k < mod` we get `k <= y - x`. If the resulting comparison is
+    // strict then the strengthening amount is instead `k - 1` modulo `mod`:
+    // `x < y` means `0 <= y - x - 1 =(mod) k - 1` so `k - 1 <= y - x - 1` and
+    // thus `k - 1 < y - x` with `0 <= k - 1 < mod`.
+    exprModulus(comp.getLesserOperand(), b, v1, mod) and
+    exprModulus(comp.getGreaterOperand(), b, v2, mod) and
+    (testIsTrue = true or testIsTrue = false) and
+    (if comp.isStrict() then resultIsStrict = testIsTrue else resultIsStrict = testIsTrue.booleanNot()) and
+    (resultIsStrict = true and d = 1 or resultIsStrict = false and d = 0) and
+    (testIsTrue = true and k = v2 - v1 or testIsTrue = false and k = v1 - v2) and
+    strengthen = (((k - d) % mod) + mod) % mod
+  )
+}
+
 /**
  * Gets a condition that tests whether `v` is bounded by `e + delta`.
  *
@@ -152,10 +175,10 @@ private Guard boundFlowCond(SsaVariable v, Expr e, int delta, boolean upper, boo
       upper = false and strengthen = 1)
     else
       strengthen = 0) and
-    // A non-strict inequality `x <= y` can be strengthened to `x <= y - 1` if
-    // `x` and `y` have opposite parities, and a strict inequality `x < y` can
-    // be similarly strengthened if `x` and `y` have equal parities.
-    (if parityComparison(comp, resultIsStrict) then d2 = strengthen else d2 = 0) and
+    (
+      exists(int k | modulusComparison(comp, testIsTrue, k) and d2 = strengthen * k) or
+      not modulusComparison(comp, testIsTrue, _) and d2 = 0
+    ) and
     // A strict inequality `x < y` can be strengthened to `x <= y - 1`.
     (resultIsStrict = true and d3 = strengthen or resultIsStrict = false and d3 = 0) and
     delta = d1 + d2 + d3
diff --git a/java/ql/test/query-tests/RangeAnalysis/A.java b/java/ql/test/query-tests/RangeAnalysis/A.java
index abe2b3d4aed..d18d09d2ccd 100644
--- a/java/ql/test/query-tests/RangeAnalysis/A.java
+++ b/java/ql/test/query-tests/RangeAnalysis/A.java
@@ -76,7 +76,7 @@ public class A {
     int[] a = new int[3 * n];
     int sum = 0;
     for (int i = 0; i < a.length; i += 3) {
-      sum += a[i] + a[i + 1] + a[i + 2]; // OK - FP
+      sum += a[i] + a[i + 1] + a[i + 2]; // OK
     }
   }
 
diff --git a/java/ql/test/query-tests/RangeAnalysis/ArrayIndexOutOfBounds.expected b/java/ql/test/query-tests/RangeAnalysis/ArrayIndexOutOfBounds.expected
index eb59dd6d262..23daa615a19 100644
--- a/java/ql/test/query-tests/RangeAnalysis/ArrayIndexOutOfBounds.expected
+++ b/java/ql/test/query-tests/RangeAnalysis/ArrayIndexOutOfBounds.expected
@@ -5,8 +5,6 @@
 | A.java:46:14:46:22 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length. |
 | A.java:55:14:55:19 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length. |
 | A.java:64:14:64:19 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length. |
-| A.java:79:21:79:28 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length. |
-| A.java:79:32:79:39 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length + 1. |
 | A.java:86:12:86:16 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length. |
 | A.java:97:18:97:31 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length + 8. |
 | A.java:110:14:110:21 | ...[...] | This array access might be out of bounds, as the index might be equal to the array length. |

From ca8ca55828c49e6b72245ae9d57c1dde68d197cc Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <schack@semmle.com>
Date: Wed, 10 Oct 2018 14:09:19 +0200
Subject: [PATCH 6/9] Java: Deprecate ParityAnalysis.

---
 java/ql/src/filters/ImportAdditionalLibraries.ql |  1 +
 .../semmle/code/java/dataflow/ParityAnalysis.qll | 16 ++++++++++++++++
 2 files changed, 17 insertions(+)

diff --git a/java/ql/src/filters/ImportAdditionalLibraries.ql b/java/ql/src/filters/ImportAdditionalLibraries.ql
index d3a5f8bc52a..7fc55fbc960 100644
--- a/java/ql/src/filters/ImportAdditionalLibraries.ql
+++ b/java/ql/src/filters/ImportAdditionalLibraries.ql
@@ -10,6 +10,7 @@
 import java
 
 import semmle.code.java.dataflow.Guards
+import semmle.code.java.dataflow.ParityAnalysis
 import semmle.code.java.security.DataFlow
 
 from File f, string tag
diff --git a/java/ql/src/semmle/code/java/dataflow/ParityAnalysis.qll b/java/ql/src/semmle/code/java/dataflow/ParityAnalysis.qll
index 152f240914d..9014b08650a 100644
--- a/java/ql/src/semmle/code/java/dataflow/ParityAnalysis.qll
+++ b/java/ql/src/semmle/code/java/dataflow/ParityAnalysis.qll
@@ -1,4 +1,6 @@
 /**
+ * DEPRECATED: semmle.code.java.dataflow.ModulusAnalysis instead.
+ *
  * Parity Analysis.
  *
  * The analysis is implemented as an abstract interpretation over the
@@ -12,6 +14,7 @@ private import SignAnalysis
 private import semmle.code.java.Reflection
 
 /** Gets an expression that is the remainder modulo 2 of `arg`. */
+deprecated
 private Expr mod2(Expr arg) {
   exists(RemExpr rem |
     result = rem and
@@ -23,6 +26,7 @@ private Expr mod2(Expr arg) {
 }
 
 /** An expression that calculates remainder modulo 2. */
+deprecated
 private class Mod2 extends Expr {
   Mod2() {
     this = mod2(_)
@@ -38,6 +42,7 @@ private class Mod2 extends Expr {
  * Parity represented as booleans. Even corresponds to `false` and odd
  * corresponds to `true`.
  */
+deprecated
 class Parity extends boolean {
   Parity() { this = true or this = false }
   predicate isEven() { this = false }
@@ -48,6 +53,7 @@ class Parity extends boolean {
  * Gets a condition that performs a parity check on `v`, such that `v` has
  * the given parity if the condition evaluates to `testIsTrue`.
  */
+deprecated
 private Guard parityCheck(SsaVariable v, Parity parity, boolean testIsTrue) {
   exists(Mod2 rem, CompileTimeConstantExpr c, int r, boolean polarity |
     result.isEquality(rem, c, polarity) and
@@ -65,6 +71,7 @@ private Guard parityCheck(SsaVariable v, Parity parity, boolean testIsTrue) {
 /**
  * Gets the parity of `e` if it can be directly determined.
  */
+deprecated
 private Parity certainExprParity(Expr e) {
   exists(int i | e.(ConstantIntegerExpr).getIntValue() = i |
     if i % 2 = 0 then result.isEven() else result.isOdd()
@@ -92,6 +99,7 @@ private Parity certainExprParity(Expr e) {
 /**
  * Gets the expression that defines the array length that equals `len`, if any.
  */
+deprecated
 private Expr arrLenDef(FieldAccess len) {
   exists(SsaVariable arr |
     len.getField() instanceof ArrayLengthField and
@@ -101,6 +109,7 @@ private Expr arrLenDef(FieldAccess len) {
 }
 
 /** Gets a possible parity for `v`. */
+deprecated
 private Parity ssaParity(SsaVariable v) {
   exists(VariableUpdate def | def = v.(SsaExplicitUpdate).getDefiningExpr() |
     result = exprParity(def.(VariableAssign).getSource()) or
@@ -115,6 +124,7 @@ private Parity ssaParity(SsaVariable v) {
 }
 
 /** Gets a possible parity for `f`. */
+deprecated
 private Parity fieldParity(Field f) {
   result = exprParity(f.getAnAssignedValue()) or
   exists(UnaryAssignExpr u | u.getExpr() = f.getAnAccess() and (result = true or result = false)) or
@@ -128,6 +138,7 @@ private Parity fieldParity(Field f) {
 }
 
 /** Holds if the parity of `e` is too complicated to determine. */
+deprecated
 private predicate unknownParity(Expr e) {
   e instanceof AssignDivExpr or
   e instanceof AssignRShiftExpr or
@@ -144,6 +155,7 @@ private predicate unknownParity(Expr e) {
 }
 
 /** Gets a possible parity for `e`. */
+deprecated
 private Parity exprParity(Expr e) {
   result = certainExprParity(e) or
   not exists(certainExprParity(e)) and
@@ -207,14 +219,18 @@ private Parity exprParity(Expr e) {
 /**
  * Gets the parity of `e` if it can be uniquely determined.
  */
+deprecated
 Parity getExprParity(Expr e) {
   result = exprParity(e) and 1 = count(exprParity(e))
 }
 
 /**
+ * DEPRECATED: semmle.code.java.dataflow.ModulusAnalysis instead.
+ *
  * Holds if the parity can be determined for both sides of `comp`. The boolean
  * `eqparity` indicates whether the two sides have equal or opposite parity.
  */
+deprecated
 predicate parityComparison(ComparisonExpr comp, boolean eqparity) {
   exists(Expr left, Expr right, boolean lpar, boolean rpar |
     comp.getLeftOperand() = left and

From 1a66f7e249ce3a77ae131c51499fbf442d2be70d Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <schack@semmle.com>
Date: Wed, 10 Oct 2018 15:39:56 +0200
Subject: [PATCH 7/9] Java: Add change note.

---
 change-notes/1.19/analysis-java.md | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/change-notes/1.19/analysis-java.md b/change-notes/1.19/analysis-java.md
index becec5b9d98..3d5e09b5746 100644
--- a/change-notes/1.19/analysis-java.md
+++ b/change-notes/1.19/analysis-java.md
@@ -4,13 +4,17 @@
 
 ## New queries
 
-| **Query**                                     | **Tags**                                             | **Purpose**                                                                                                                                                                 |
-|-----------------------------------------------|------------------------------------------------------|-----------------------------------------------------------------------------------------------------------------------------------------------------------------------------|
+| **Query**                   | **Tags**  | **Purpose**                                                        |
+|-----------------------------|-----------|--------------------------------------------------------------------|
 
 ## Changes to existing queries
 
-| **Query**                      | **Expected impact**        | **Change**                                   |
-| Unreachable catch clause (`java/unreachable-catch-clause`) | Fewer false-positive results | This rule now accounts for calls to generic methods that throw generic exceptions. |
+| **Query**                  | **Expected impact**    | **Change**                                                       |
+|----------------------------|------------------------|------------------------------------------------------------------|
+| Array index out of bounds (`java/index-out-of-bounds`) | Fewer false positive results | False positives involving arrays with a length evenly divisible by 3 or some greater number and an index being increased with a similar stride length are no longer reported. |
+| Unreachable catch clause (`java/unreachable-catch-clause`) | Fewer false positive results | This rule now accounts for calls to generic methods that throw generic exceptions. |
 
 ## Changes to QL libraries
 
+* The `ParityAnalysis` library is replaced with the more general `ModulusAnalysis` library, which improves the range analysis.
+

From 26009065af84d08c105abfc9de637f5a67f4d465 Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <schack@semmle.com>
Date: Tue, 16 Oct 2018 11:29:15 +0200
Subject: [PATCH 8/9] Java: Fix regression.

---
 .../code/java/dataflow/RangeAnalysis.qll      | 26 ++++++++++++++++---
 java/ql/test/query-tests/RangeAnalysis/A.java | 11 ++++++++
 2 files changed, 34 insertions(+), 3 deletions(-)

diff --git a/java/ql/src/semmle/code/java/dataflow/RangeAnalysis.qll b/java/ql/src/semmle/code/java/dataflow/RangeAnalysis.qll
index d5acafa47ce..694989d1a8e 100644
--- a/java/ql/src/semmle/code/java/dataflow/RangeAnalysis.qll
+++ b/java/ql/src/semmle/code/java/dataflow/RangeAnalysis.qll
@@ -133,21 +133,41 @@ private predicate boundCondition(ComparisonExpr comp, SsaVariable v, Expr e, int
   )
 }
 
+private predicate gcdInput(int x, int y) {
+  exists(ComparisonExpr comp, Bound b |
+    exprModulus(comp.getLesserOperand(), b, _, x) and
+    exprModulus(comp.getGreaterOperand(), b, _, y)
+  ) or
+  exists(int x0, int y0 |
+    gcdInput(x0, y0) and
+    x = y0 and
+    y = x0 % y0
+  )
+}
+
+private int gcd(int x, int y) {
+  result = x.abs() and y = 0 and gcdInput(x, y)
+  or
+  result = gcd(y, x % y) and y != 0 and gcdInput(x, y)
+}
+
 /**
  * Holds if `comp` is a comparison between `x` and `y` for which `y - x` has a
  * fixed value modulo some `mod > 1`, such that the comparison can be
  * strengthened by `strengthen` when evaluating to `testIsTrue`.
  */
 private predicate modulusComparison(ComparisonExpr comp, boolean testIsTrue, int strengthen) {
-  exists(Bound b, int v1, int v2, int mod, boolean resultIsStrict, int d, int k |
+  exists(Bound b, int v1, int v2, int mod1, int mod2, int mod, boolean resultIsStrict, int d, int k |
     // If `x <= y` and `x =(mod) b + v1` and `y =(mod) b + v2` then
     // `0 <= y - x =(mod) v2 - v1`. By choosing `k =(mod) v2 - v1` with
     // `0 <= k < mod` we get `k <= y - x`. If the resulting comparison is
     // strict then the strengthening amount is instead `k - 1` modulo `mod`:
     // `x < y` means `0 <= y - x - 1 =(mod) k - 1` so `k - 1 <= y - x - 1` and
     // thus `k - 1 < y - x` with `0 <= k - 1 < mod`.
-    exprModulus(comp.getLesserOperand(), b, v1, mod) and
-    exprModulus(comp.getGreaterOperand(), b, v2, mod) and
+    exprModulus(comp.getLesserOperand(), b, v1, mod1) and
+    exprModulus(comp.getGreaterOperand(), b, v2, mod2) and
+    mod = gcd(mod1, mod2) and
+    mod != 1 and
     (testIsTrue = true or testIsTrue = false) and
     (if comp.isStrict() then resultIsStrict = testIsTrue else resultIsStrict = testIsTrue.booleanNot()) and
     (resultIsStrict = true and d = 1 or resultIsStrict = false and d = 0) and
diff --git a/java/ql/test/query-tests/RangeAnalysis/A.java b/java/ql/test/query-tests/RangeAnalysis/A.java
index d18d09d2ccd..1a3a3377286 100644
--- a/java/ql/test/query-tests/RangeAnalysis/A.java
+++ b/java/ql/test/query-tests/RangeAnalysis/A.java
@@ -151,4 +151,15 @@ public class A {
     }
   }
 
+  void m12() {
+    int[] a = new int[] { 1, 2, 3, 4, 5, 6 };
+    int sum = 0;
+    for (int i = 0; i < a.length; i += 2) {
+      sum += a[i] + a[i + 1]; // OK
+    }
+    int[] b = new int[8];
+    for (int i = 2; i < 8; i += 2) {
+      sum += b[i] + b[i + 1]; // OK
+    }
+  }
 }

From 3dc9071a4406908b957a358d7091513e40f69680 Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <schack@semmle.com>
Date: Wed, 17 Oct 2018 15:59:52 +0200
Subject: [PATCH 9/9] Java: Add missing word in deprecation comments.

---
 java/ql/src/semmle/code/java/dataflow/ParityAnalysis.qll | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/java/ql/src/semmle/code/java/dataflow/ParityAnalysis.qll b/java/ql/src/semmle/code/java/dataflow/ParityAnalysis.qll
index 9014b08650a..f5a28a509e5 100644
--- a/java/ql/src/semmle/code/java/dataflow/ParityAnalysis.qll
+++ b/java/ql/src/semmle/code/java/dataflow/ParityAnalysis.qll
@@ -1,5 +1,5 @@
 /**
- * DEPRECATED: semmle.code.java.dataflow.ModulusAnalysis instead.
+ * DEPRECATED: Use semmle.code.java.dataflow.ModulusAnalysis instead.
  *
  * Parity Analysis.
  *
@@ -225,7 +225,7 @@ Parity getExprParity(Expr e) {
 }
 
 /**
- * DEPRECATED: semmle.code.java.dataflow.ModulusAnalysis instead.
+ * DEPRECATED: Use semmle.code.java.dataflow.ModulusAnalysis instead.
  *
  * Holds if the parity can be determined for both sides of `comp`. The boolean
  * `eqparity` indicates whether the two sides have equal or opposite parity.