Merge pull request #4349 from tamasvajk/feature/modulus-analysis

ModulusAnalysis shared between C# and Java

java/ql/src/semmle/code/java/dataflow/Bound.qll

@@ -2,15 +2,13 @@
  * Provides classes for representing abstract bounds for use in, for example, range analysis.
  */
 
-import java
-private import SSA
-private import RangeUtils
+private import internal.rangeanalysis.BoundSpecific
 
 private newtype TBound =
   TBoundZero() or
   TBoundSsa(SsaVariable v) { v.getSourceVariable().getType() instanceof IntegralType } or
   TBoundExpr(Expr e) {
-    e.(FieldRead).getField() instanceof ArrayLengthField and
+    interestingExprBound(e) and
     not exists(SsaVariable v | e = v.getAUse())
   }
 
@@ -75,6 +73,6 @@ class ExprBound extends Bound, TBoundExpr {
   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)
+    getExpr().getLocation().hasLocationInfo(path, sl, sc, el, ec)
   }
 }

java/ql/src/semmle/code/java/dataflow/ModulusAnalysis.qll

@@ -4,12 +4,9 @@
  * variable), and `v` is an integer in the range `[0 .. m-1]`.
  */
 
-import java
-private import SSA
-private import semmle.code.java.dataflow.internal.rangeanalysis.SsaReadPositionCommon
-private import RangeUtils
-private import semmle.code.java.controlflow.Guards
-import Bound
+private import internal.rangeanalysis.ModulusAnalysisSpecific::Private
+private import Bound
+private import internal.rangeanalysis.SsaReadPositionCommon
 
 /**
  * Holds if `e + delta` equals `v` at `pos`.
@@ -29,16 +26,9 @@ private predicate valueFlowStepSsa(SsaVariable v, SsaReadPosition pos, Expr e, i
  * `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()
-    )
+  exists(AddExpr a | a = add |
+    larg = a.getLhs() and
+    rarg = a.getRhs()
   ) and
   not larg instanceof ConstantIntegerExpr and
   not rarg instanceof ConstantIntegerExpr
@@ -49,16 +39,9 @@ private predicate nonConstAddition(Expr add, Expr larg, Expr rarg) {
  * 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()
-    )
+  exists(SubExpr s | s = sub |
+    larg = s.getLhs() and
+    rarg = s.getRhs()
   ) and
   not rarg instanceof ConstantIntegerExpr
 }
@@ -68,14 +51,14 @@ private Expr modExpr(Expr arg, int mod) {
   exists(RemExpr rem |
     result = rem and
     arg = rem.getLeftOperand() and
-    rem.getRightOperand().(CompileTimeConstantExpr).getIntValue() = mod and
+    rem.getRightOperand().(ConstantIntegerExpr).getIntValue() = mod and
     mod >= 2
   )
   or
-  exists(CompileTimeConstantExpr c |
+  exists(ConstantIntegerExpr c |
     mod = 2.pow([1 .. 30]) and
     c.getIntValue() = mod - 1 and
-    result.(AndBitwiseExpr).hasOperands(arg, c)
+    result.(BitwiseAndExpr).hasOperands(arg, c)
   )
 }
 
@@ -84,7 +67,7 @@ private Expr modExpr(Expr arg, int mod) {
  * its `testIsTrue` branch.
  */
 private Guard moduloCheck(SsaVariable v, int val, int mod, boolean testIsTrue) {
-  exists(Expr rem, CompileTimeConstantExpr c, int r, boolean polarity |
+  exists(Expr rem, ConstantIntegerExpr c, int r, boolean polarity |
     result.isEquality(rem, c, polarity) and
     c.getIntValue() = r and
     rem = modExpr(v.getAUse(), mod) and
@@ -122,24 +105,12 @@ 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
+    e.(LShiftExpr).getRhs() = c and factor = 2.pow(k) and k > 0
     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))
+    e.(BitwiseAndExpr).getAnOperand() = 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`.
@@ -267,7 +238,7 @@ predicate exprModulus(Expr e, Bound b, int val, int mod) {
   exists(SsaVariable v, SsaReadPositionBlock bb |
     ssaModulus(v, bb, b, val, mod) and
     e = v.getAUse() and
-    bb.getBlock() = e.getBasicBlock()
+    getABasicBlockExpr(bb.getBlock()) = e
   )
   or
   exists(Expr mid, int val0, int delta |

java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/BoundSpecific.qll

@@ -0,0 +1,20 @@
+/**
+ * Provides Java-specific definitions for bounds.
+ */
+
+private import java as J
+private import semmle.code.java.dataflow.SSA as Ssa
+private import semmle.code.java.dataflow.RangeUtils as RU
+
+class SsaVariable = Ssa::SsaVariable;
+
+class Expr = J::Expr;
+
+class IntegralType = J::IntegralType;
+
+class ConstantIntegerExpr = RU::ConstantIntegerExpr;
+
+/** Holds if `e` is a bound expression and it is not an SSA variable read. */
+predicate interestingExprBound(Expr e) {
+  e.(J::FieldRead).getField() instanceof J::ArrayLengthField
+}

java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll

@@ -0,0 +1,119 @@
+module Private {
+  private import java as J
+  private import semmle.code.java.dataflow.SSA as Ssa
+  private import semmle.code.java.dataflow.RangeUtils as RU
+  private import semmle.code.java.controlflow.Guards as G
+  private import semmle.code.java.controlflow.BasicBlocks as BB
+
+  class BasicBlock = BB::BasicBlock;
+
+  class SsaVariable = Ssa::SsaVariable;
+
+  class SsaPhiNode = Ssa::SsaPhiNode;
+
+  class Expr = J::Expr;
+
+  class Guard = G::Guard;
+
+  class ConstantIntegerExpr = RU::ConstantIntegerExpr;
+
+  class ConditionalExpr = J::ConditionalExpr;
+
+  /** An addition or an assign-add expression. */
+  class AddExpr extends J::Expr {
+    AddExpr() { this instanceof J::AddExpr or this instanceof J::AssignAddExpr }
+
+    /** Gets the LHS operand of this add expression. */
+    Expr getLhs() {
+      result = this.(J::AddExpr).getLeftOperand()
+      or
+      result = this.(J::AssignAddExpr).getDest()
+    }
+
+    /** Gets the RHS operand of this add expression. */
+    Expr getRhs() {
+      result = this.(J::AddExpr).getRightOperand()
+      or
+      result = this.(J::AssignAddExpr).getRhs()
+    }
+  }
+
+  /** A subtraction or an assign-sub expression. */
+  class SubExpr extends J::Expr {
+    SubExpr() { this instanceof J::SubExpr or this instanceof J::AssignSubExpr }
+
+    /** Gets the LHS operand of this subtraction expression. */
+    Expr getLhs() {
+      result = this.(J::SubExpr).getLeftOperand()
+      or
+      result = this.(J::AssignSubExpr).getDest()
+    }
+
+    /** Gets the RHS operand of this subtraction expression. */
+    Expr getRhs() {
+      result = this.(J::SubExpr).getRightOperand()
+      or
+      result = this.(J::AssignSubExpr).getRhs()
+    }
+  }
+
+  class RemExpr = J::RemExpr;
+
+  /** A multiplication or an assign-mul expression. */
+  class MulExpr extends J::Expr {
+    MulExpr() { this instanceof J::MulExpr or this instanceof J::AssignMulExpr }
+
+    /** Gets an operand of this multiplication. */
+    Expr getAnOperand() {
+      result = this.(J::MulExpr).getAnOperand() or
+      result = this.(J::AssignMulExpr).getSource()
+    }
+  }
+
+  /** A left shift or an assign-lshift expression. */
+  class LShiftExpr extends J::Expr {
+    LShiftExpr() { this instanceof J::LShiftExpr or this instanceof J::AssignLShiftExpr }
+
+    /** Gets the RHS operand of this shift. */
+    Expr getRhs() {
+      result = this.(J::LShiftExpr).getRightOperand() or
+      result = this.(J::AssignLShiftExpr).getRhs()
+    }
+  }
+
+  /** A bitwise and or an assign-and expression. */
+  class BitwiseAndExpr extends J::Expr {
+    BitwiseAndExpr() { this instanceof J::AndBitwiseExpr or this instanceof J::AssignAndExpr }
+
+    /** Gets an operand of this bitwise and operation. */
+    Expr getAnOperand() {
+      result = this.(J::AndBitwiseExpr).getAnOperand() or
+      result = this.(J::AssignAndExpr).getSource()
+    }
+
+    /** Holds if this expression has operands `e1` and `e2`. */
+    predicate hasOperands(Expr e1, Expr e2) {
+      this.getAnOperand() = e1 and
+      this.getAnOperand() = e2 and
+      e1 != e2
+    }
+  }
+
+  predicate guardDirectlyControlsSsaRead = RU::guardDirectlyControlsSsaRead/3;
+
+  predicate guardControlsSsaRead = RU::guardControlsSsaRead/3;
+
+  predicate valueFlowStep = RU::valueFlowStep/3;
+
+  predicate eqFlowCond = RU::eqFlowCond/5;
+
+  predicate ssaUpdateStep = RU::ssaUpdateStep/3;
+
+  Expr getABasicBlockExpr(BasicBlock bb) { result = bb.getANode() }
+
+  private predicate id(BasicBlock x, BasicBlock y) { x = y }
+
+  private predicate idOf(BasicBlock x, int y) = equivalenceRelation(id/2)(x, y)
+
+  int getId(BasicBlock bb) { idOf(bb, result) }
+}