Merge pull request #301 from aschackmull/java/modulus-analysis

Approved by yh-semmle

Author: semmle-qlci

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.
+

java/ql/src/filters/ImportAdditionalLibraries.ql

@@ -9,6 +9,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

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)
+  }
+}