Make semantic modulus analysismatch Java results

Author: Dave Bartolomeo

java/ql/lib/semmle/code/java/semantic/SemanticExprSpecific.qll

@@ -337,12 +337,14 @@ module SemanticExprConfig {
       type = getSemanticType(update.getSourceVariable().getType()) and
       exists(J::Expr expr | expr = update.getDefiningExpr() |
         (
-          expr instanceof J::Assignment or
+          expr instanceof J::AssignOp or
           expr instanceof J::PreIncExpr or
           expr instanceof J::PreDecExpr
         ) and
         sourceExpr = getResultExpr(expr)
         or
+        sourceExpr = getResultExpr(expr.(J::AssignExpr).getSource())
+        or
         sourceExpr = getResultExpr(expr.(J::LocalVariableDeclExpr).getInit())
         or
         (expr instanceof J::PostIncExpr or expr instanceof J::PostDecExpr) and

java/ql/lib/semmle/code/java/semantic/analysis/ModulusAnalysis.qll

@@ -6,6 +6,7 @@
 
 private import ModulusAnalysisSpecific::Private
 private import semmle.code.java.semantic.SemanticBound
+private import semmle.code.java.semantic.SemanticCFG
 private import semmle.code.java.semantic.SemanticExpr
 private import semmle.code.java.semantic.SemanticGuard
 private import semmle.code.java.semantic.SemanticSSA
@@ -30,9 +31,9 @@ private predicate valueFlowStepSsa(SemSsaVariable v, SemSsaReadPosition pos, Sem
  * `ConstantIntegerExpr`s.
  */
 private predicate nonConstAddition(SemExpr add, SemExpr larg, SemExpr rarg) {
-  exists(AddExpr a | a = add |
-    larg = a.getLhs() and
-    rarg = a.getRhs()
+  exists(SemAddExpr a | a = add |
+    larg = a.getLeftOperand() and
+    rarg = a.getRightOperand()
   ) and
   not larg instanceof SemConstantIntegerExpr and
   not rarg instanceof SemConstantIntegerExpr
@@ -43,9 +44,9 @@ private predicate nonConstAddition(SemExpr add, SemExpr larg, SemExpr rarg) {
  * a `ConstantIntegerExpr`.
  */
 private predicate nonConstSubtraction(SemExpr sub, SemExpr larg, SemExpr rarg) {
-  exists(SubExpr s | s = sub |
-    larg = s.getLhs() and
-    rarg = s.getRhs()
+  exists(SemSubExpr s | s = sub |
+    larg = s.getLeftOperand() and
+    rarg = s.getRightOperand()
   ) and
   not rarg instanceof SemConstantIntegerExpr
 }
@@ -62,7 +63,7 @@ private SemExpr modExpr(SemExpr arg, int mod) {
   exists(SemConstantIntegerExpr c |
     mod = 2.pow([1 .. 30]) and
     c.getIntValue() = mod - 1 and
-    result.(BitwiseAndExpr).hasOperands(arg, c)
+    result.(SemBitAndExpr).hasOperands(arg, c)
   )
 }
 
@@ -107,11 +108,11 @@ private predicate andmaskFactor(int mask, int factor) {
 /** Holds if `e` is evenly divisible by `factor`. */
 private predicate evenlyDivisibleExpr(SemExpr e, int factor) {
   exists(SemConstantIntegerExpr c, int k | k = c.getIntValue() |
-    e.(MulExpr).getAnOperand() = c and factor = k.abs() and factor >= 2
+    e.(SemMulExpr).getAnOperand() = c and factor = k.abs() and factor >= 2
     or
-    e.(LShiftExpr).getRhs() = c and factor = 2.pow(k) and k > 0
+    e.(SemShiftLeftExpr).getRightOperand() = c and factor = 2.pow(k) and k > 0
     or
-    e.(BitwiseAndExpr).getAnOperand() = c and factor = max(int f | andmaskFactor(k, f))
+    e.(SemBitAndExpr).getAnOperand() = c and factor = max(int f | andmaskFactor(k, f))
   )
 }
 
@@ -223,49 +224,54 @@ private predicate ssaModulus(SemSsaVariable v, SemSsaReadPosition pos, SemBound
  */
 cached
 predicate semExprModulus(SemExpr e, SemBound b, int val, int mod) {
-  e = b.getExpr(val) and mod = 0
-  or
-  evenlyDivisibleExpr(e, mod) and val = 0 and b instanceof SemZeroBound
-  or
-  exists(SemSsaVariable v, SemSsaReadPositionBlock bb |
-    ssaModulus(v, bb, b, val, mod) and
-    e = v.getAUse() and
-    bb.getAnExpr() = e
-  )
-  or
-  exists(SemExpr mid, int val0, int delta |
-    semExprModulus(mid, b, val0, mod) and
-    semValueFlowStep(e, mid, delta) and
-    val = remainder(val0 + delta, mod)
-  )
-  or
-  exists(SemConditionalExpr 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 = m1.gcd(m2).gcd(v1 - v2) and
-    mod != 1 and
-    val = remainder(v1, mod)
-  )
-  or
-  exists(SemBound b1, SemBound b2, int v1, int v2, int m1, int m2 |
-    addModulus(e, true, b1, v1, m1) and
-    addModulus(e, false, b2, v2, m2) and
-    mod = m1.gcd(m2) and
-    mod != 1 and
-    val = remainder(v1 + v2, mod)
-  |
-    b = b1 and b2 instanceof SemZeroBound
+  not ignoreExprModulus(e) and
+  (
+    e = b.getExpr(val) and mod = 0
     or
-    b = b2 and b1 instanceof SemZeroBound
-  )
-  or
-  exists(int v1, int v2, int m1, int m2 |
-    subModulus(e, true, b, v1, m1) and
-    subModulus(e, false, any(SemZeroBound zb), v2, m2) and
-    mod = m1.gcd(m2) and
-    mod != 1 and
-    val = remainder(v1 - v2, mod)
+    evenlyDivisibleExpr(e, mod) and
+    val = 0 and
+    b instanceof SemZeroBound
+    or
+    exists(SemSsaVariable v, SemSsaReadPositionBlock bb |
+      ssaModulus(v, bb, b, val, mod) and
+      e = v.getAUse() and
+      bb.getAnExpr() = e
+    )
+    or
+    exists(SemExpr mid, int val0, int delta |
+      semExprModulus(mid, b, val0, mod) and
+      semValueFlowStep(e, mid, delta) and
+      val = remainder(val0 + delta, mod)
+    )
+    or
+    exists(SemConditionalExpr 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 = m1.gcd(m2).gcd(v1 - v2) and
+      mod != 1 and
+      val = remainder(v1, mod)
+    )
+    or
+    exists(SemBound b1, SemBound b2, int v1, int v2, int m1, int m2 |
+      addModulus(e, true, b1, v1, m1) and
+      addModulus(e, false, b2, v2, m2) and
+      mod = m1.gcd(m2) and
+      mod != 1 and
+      val = remainder(v1 + v2, mod)
+    |
+      b = b1 and b2 instanceof SemZeroBound
+      or
+      b = b2 and b1 instanceof SemZeroBound
+    )
+    or
+    exists(int v1, int v2, int m1, int m2 |
+      subModulus(e, true, b, v1, m1) and
+      subModulus(e, false, any(SemZeroBound zb), v2, m2) and
+      mod = m1.gcd(m2) and
+      mod != 1 and
+      val = remainder(v1 - v2, mod)
+    )
   )
 }
 
@@ -290,3 +296,25 @@ private predicate subModulus(SemExpr sub, boolean isLeft, SemBound b, int val, i
     semExprModulus(rarg, b, val, mod) and isLeft = false
   )
 }
+
+private predicate id(SemBasicBlock x, SemBasicBlock y) { x = y }
+
+private predicate idOf(SemBasicBlock x, int y) = equivalenceRelation(id/2)(x, y)
+
+private int getId(SemBasicBlock 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(
+  SemSsaPhiNode phi, SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge, int r
+) {
+  edge.phiInput(phi, inp) and
+  edge =
+    rank[r](SemSsaReadPositionPhiInputEdge e |
+      e.phiInput(phi, _)
+    |
+      e order by getId(e.getOrigBlock())
+    )
+}

java/ql/lib/semmle/code/java/semantic/analysis/ModulusAnalysisSpecific.qll

@@ -1,107 +1,11 @@
 module Private {
   private import java as J
-  private import semmle.code.java.controlflow.BasicBlocks as BB
-  private import semmle.code.java.semantic.SemanticCFG
   private import semmle.code.java.semantic.SemanticExpr
-  private import semmle.code.java.semantic.SemanticSSA
-
-  /** An addition or an assign-add expression. */
-  class AddExpr extends SemExpr {
-    AddExpr() { this instanceof SemAddExpr or this instanceof SemAssignAddExpr }
-
-    /** Gets the LHS operand of this add expression. */
-    SemExpr getLhs() {
-      result = this.(SemAddExpr).getLeftOperand()
-      or
-      result = this.(SemAssignAddExpr).getDest()
-    }
-
-    /** Gets the RHS operand of this add expression. */
-    SemExpr getRhs() {
-      result = this.(SemAddExpr).getRightOperand()
-      or
-      result = this.(SemAssignAddExpr).getRhs()
-    }
-  }
-
-  /** A subtraction or an assign-sub expression. */
-  class SubExpr extends SemExpr {
-    SubExpr() { this instanceof SemSubExpr or this instanceof SemAssignSubExpr }
-
-    /** Gets the LHS operand of this subtraction expression. */
-    SemExpr getLhs() {
-      result = this.(SemSubExpr).getLeftOperand()
-      or
-      result = this.(SemAssignSubExpr).getDest()
-    }
-
-    /** Gets the RHS operand of this subtraction expression. */
-    SemExpr getRhs() {
-      result = this.(SemSubExpr).getRightOperand()
-      or
-      result = this.(SemAssignSubExpr).getRhs()
-    }
-  }
-
-  /** A multiplication or an assign-mul expression. */
-  class MulExpr extends SemExpr {
-    MulExpr() { this instanceof SemMulExpr or this instanceof SemAssignMulExpr }
-
-    /** Gets an operand of this multiplication. */
-    SemExpr getAnOperand() {
-      result = this.(SemMulExpr).getAnOperand() or
-      result = this.(SemAssignMulExpr).getSource()
-    }
-  }
-
-  /** A left shift or an assign-lshift expression. */
-  class LShiftExpr extends SemExpr {
-    LShiftExpr() { this instanceof SemLShiftExpr or this instanceof SemAssignLShiftExpr }
-
-    /** Gets the RHS operand of this shift. */
-    SemExpr getRhs() {
-      result = this.(SemLShiftExpr).getRightOperand() or
-      result = this.(SemAssignLShiftExpr).getRhs()
-    }
-  }
-
-  /** A bitwise and or an assign-and expression. */
-  class BitwiseAndExpr extends SemExpr {
-    BitwiseAndExpr() { this instanceof SemAndBitwiseExpr or this instanceof SemAssignAndExpr }
-
-    /** Gets an operand of this bitwise and operation. */
-    SemExpr getAnOperand() {
-      result = this.(SemAndBitwiseExpr).getAnOperand() or
-      result = this.(SemAssignAndExpr).getSource()
-    }
-
-    /** Holds if this expression has operands `e1` and `e2`. */
-    predicate hasOperands(SemExpr e1, SemExpr e2) {
-      this.getAnOperand() = e1 and
-      this.getAnOperand() = e2 and
-      e1 != e2
-    }
-  }
-
-  private predicate id(BB::BasicBlock x, BB::BasicBlock y) { x = y }
-
-  private predicate idOf(BB::BasicBlock x, int y) = equivalenceRelation(id/2)(x, y)
-
-  private int getId(BB::BasicBlock bb) { idOf(bb, result) }
+  private import semmle.code.java.semantic.SemanticExprSpecific
 
   /**
-   * 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`.
+   * Workaround to preserve the original Java results by ignoring the modulus of
+   * certain expressions.
    */
-  predicate rankedPhiInput(
-    SemSsaPhiNode phi, SemSsaVariable inp, SemSsaReadPositionPhiInputEdge edge, int r
-  ) {
-    edge.phiInput(phi, inp) and
-    edge =
-      rank[r](SemSsaReadPositionPhiInputEdge e |
-        e.phiInput(phi, _)
-      |
-        e order by getId(getJavaBasicBlock(e.getOrigBlock()))
-      )
-  }
+  predicate ignoreExprModulus(SemExpr e) { getJavaExpr(e) instanceof J::LocalVariableDeclExpr }
 }

java/ql/test/library-tests/dataflow/modulus-analysis/diff.ql

@@ -2,16 +2,30 @@ import java
 import semmle.code.java.semantic.analysis.ModulusAnalysis
 import semmle.code.java.semantic.SemanticBound
 import semmle.code.java.semantic.SemanticExpr
+import semmle.code.java.semantic.SemanticExprSpecific
+import semmle.code.java.semantic.SemanticSSA
 import semmle.code.java.dataflow.ModulusAnalysis
 import semmle.code.java.dataflow.Bound
+import semmle.code.java.dataflow.SSA
+import semmle.code.java.dataflow.internal.rangeanalysis.SsaReadPositionCommon
+import semmle.code.java.dataflow.RangeUtils as RU
 
-from Expr e, Bound b, int delta, int mod, string message
-where
-  semExprModulus(getSemanticExpr(e), getSemanticBound(b), delta, mod) and
-  not exprModulus(e, b, delta, mod) and
-  message = "semantic only"
-  or
-  not semExprModulus(getSemanticExpr(e), getSemanticBound(b), delta, mod) and
-  exprModulus(e, b, delta, mod) and
-  message = "AST only"
-select e, b.toString(), delta, mod
+predicate interestingLocation(Location loc) {
+  //  loc.getFile().getBaseName() = "Utf8Test.java" and
+  //  loc.getStartLine() in [164 .. 164] and
+  any()
+}
+
+query predicate diff_exprModulus(Expr e, string c, Bound b, int delta, int mod, string message) {
+  interestingLocation(e.getLocation()) and
+  c = concat(e.getAQlClass(), ", ") and
+  (
+    semExprModulus(getSemanticExpr(e), getSemanticBound(b), delta, mod) and
+    not exprModulus(e, b, delta, mod) and
+    message = "semantic only"
+    or
+    not semExprModulus(getSemanticExpr(e), getSemanticBound(b), delta, mod) and
+    exprModulus(e, getJavaBound(b), delta, mod) and
+    message = "AST only"
+  )
+}