ModulusAnalysis shared between C# and Java

Author: tamasvajk

config/identical-files.json

@@ -66,6 +66,10 @@
     "java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/BoundCommon.qll",
     "csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/BoundCommon.qll"
   ],
+  "ModulusAnalysis Java/C#": [
+    "java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/ModulusAnalysisCommon.qll",
+    "csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/ModulusAnalysisCommon.qll"
+  ],
   "C++ SubBasicBlocks": [
     "cpp/ql/src/semmle/code/cpp/controlflow/SubBasicBlocks.qll",
     "cpp/ql/src/semmle/code/cpp/dataflow/internal/SubBasicBlocks.qll"

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

@@ -0,0 +1,7 @@
+/**
+ * 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 semmle.code.csharp.dataflow.internal.rangeanalysis.ModulusAnalysisCommon

csharp/ql/src/semmle/code/csharp/dataflow/RangeAnalysis.qll

@@ -1,11 +1,11 @@
 import csharp
 import Ssa
-import Bound
-import SignAnalysis
+import semmle.code.csharp.dataflow.internal.rangeanalysis.BoundCommon
+import semmle.code.csharp.dataflow.internal.rangeanalysis.SignAnalysisCommon
 import semmle.code.csharp.dataflow.internal.rangeanalysis.SsaReadPositionCommon
 import semmle.code.csharp.dataflow.internal.rangeanalysis.ConstantUtils
 import semmle.code.csharp.dataflow.internal.rangeanalysis.SsaUtils
-import semmle.code.csharp.dataflow.internal.rangeanalysis.SignAnalysisSpecific::Private as SignPrivate
+import semmle.code.csharp.dataflow.internal.rangeanalysis.RangeUtils
 import semmle.code.csharp.controlflow.Guards as G
 import semmle.code.csharp.commons.ComparisonTest
 
@@ -61,29 +61,6 @@ private predicate boundCondition(
   // todo: other cases: // (v - d) - e < c, ...
 }
 
-/**
- * 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`
- */
-G::Guard eqFlowCond(Definition 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, G::AbstractValues::BooleanValue b0, G::AbstractValues::BooleanValue b1
-  |
-    b1.getValue() = testIsTrue and b0.getValue() = testIsTrue0
-  |
-    G::Internal::impliesSteps(result, b1, eqFlowCond(v, e, delta, isEq, testIsTrue0), b0)
-  )
-}
-
 /**
  * Gets a condition that tests whether `v` is bounded by `e + delta`.
  *
@@ -149,27 +126,10 @@ private predicate boundFlowStepSsa(
   exists(G::Guard guard, boolean testIsTrue |
     pos.hasReadOfVar(v) and
     guard = boundFlowCond(v, e, delta, upper, testIsTrue) and
-    SignPrivate::guardControlsSsaRead(guard, pos, testIsTrue)
+    guardControlsSsaRead(guard, pos, testIsTrue)
   )
 }
 
-/**
- * Holds if `v` is an `ExplicitDefinition` that equals `e + delta`.
- */
-predicate ssaUpdateStep(ExplicitDefinition v, Expr e, int delta) {
-  v.getADefinition().getExpr().(Assignment).getRValue() = e and delta = 0
-  or
-  v.getADefinition().getExpr().(PostIncrExpr).getOperand() = e and delta = 1
-  or
-  v.getADefinition().getExpr().(PreIncrExpr).getOperand() = e and delta = 1
-  or
-  v.getADefinition().getExpr().(PostDecrExpr).getOperand() = e and delta = -1
-  or
-  v.getADefinition().getExpr().(PreDecrExpr).getOperand() = e and delta = -1
-  or
-  v.getADefinition().getExpr().(AssignOperation) = e and delta = 0
-}
-
 /**
  * Holds if `b + delta` is a valid bound for `e`.
  * - `upper = true`  : `e <= b + delta`
@@ -237,59 +197,6 @@ private predicate bounded(
   )
 }
 
-/**
- * Holds if `e1 + delta` equals `e2`.
- */
-predicate valueFlowStep(Expr e2, Expr e1, int delta) {
-  e2.(AssignExpr).getRValue() = e1 and delta = 0
-  or
-  e2.(UnaryPlusExpr).getOperand() = e1 and delta = 0
-  or
-  e2.(PostIncrExpr).getOperand() = e1 and delta = 0
-  or
-  e2.(PostDecrExpr).getOperand() = e1 and delta = 0
-  or
-  e2.(PreIncrExpr).getOperand() = e1 and delta = 1
-  or
-  e2.(PreDecrExpr).getOperand() = e1 and delta = -1
-  or
-  // exists(ArrayCreationExpr a |
-  //   arrayLengthDef(e2, a) and
-  //   a.getDimension(0) = e1 and
-  //   delta = 0
-  // )
-  // or
-  exists(Expr x |
-    e2.(AddExpr).getAnOperand() = e1 and
-    e2.(AddExpr).getAnOperand() = x and
-    not e1 = x
-    or
-    exists(AssignAddExpr add | add = e2 |
-      add.getLValue() = e1 and add.getRValue() = x
-      or
-      add.getLValue() = x and add.getRValue() = 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.getLValue() = e1 and
-      sub.getRValue() = x
-    )
-  |
-    x.(ConstantIntegerExpr).getIntValue() = -delta
-  )
-}
-
 /**
  * Holds if `e1 + delta` is a valid bound for `e2`.
  * - `upper = true`  : `e2 <= e1 + delta`
@@ -465,7 +372,7 @@ private predicate unequalFlowStepIntegralSsa(Definition v, SsaReadPosition pos,
   exists(G::Guard guard, boolean testIsTrue |
     pos.hasReadOfVar(v) and
     guard = eqFlowCond(v, e, delta, false, testIsTrue) and
-    SignPrivate::guardControlsSsaRead(guard, pos, testIsTrue)
+    guardControlsSsaRead(guard, pos, testIsTrue)
   )
 }
 

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

@@ -18,4 +18,7 @@ class IntegralType = CS::IntegralType;
 class ConstantIntegerExpr = CU::ConstantIntegerExpr;
 
 /** Holds if `e` is a bound expression and it is not an SSA variable read. */
-predicate nonSsaVariableBoundedExpr(Expr e) { CU::systemArrayLengthAccess(e.(CS::PropertyRead)) }
+predicate nonSsaVariableBoundedExpr(Expr e) {
+  CU::systemArrayLengthAccess(e.(CS::PropertyRead)) and
+  not exists(SsaVariable v | e = v.getAUse())
+}