ModulusAnalysis shared between C# and Java

2025-12-16 16:53:25 +01:00 · 2020-10-06 09:36:42 +02:00
parent d2d8d009eb
commit 4df6a41616
10 changed files with 879 additions and 52 deletions
--- a/config/identical-files.json
+++ b/config/identical-files.json
@@ -66,6 +66,10 @@
    "java/ql/src/semmle/code/java/dataflow/Bound.qll",
    "csharp/ql/src/semmle/code/csharp/dataflow/Bound.qll"
  ],
+  "ModulusAnalysis Java/C#": [
+    "java/ql/src/semmle/code/java/dataflow/ModulusAnalysis.qll",
+    "csharp/ql/src/semmle/code/csharp/dataflow/ModulusAnalysis.qll"
+  ],
  "C++ SubBasicBlocks": [
    "cpp/ql/src/semmle/code/cpp/controlflow/SubBasicBlocks.qll",
    "cpp/ql/src/semmle/code/cpp/dataflow/internal/SubBasicBlocks.qll"
--- a/csharp/ql/src/semmle/code/csharp/dataflow/ModulusAnalysis.qll
+++ b/csharp/ql/src/semmle/code/csharp/dataflow/ModulusAnalysis.qll
@@ -0,0 +1,302 @@
+/**
+ * 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]`.
+ */
+
+private import internal.rangeanalysis.ModulusAnalysisSpecific::Private
+private import Bound
+private import internal.rangeanalysis.SsaReadPositionCommon
+
+/**
+ * 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.getLhs() 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.getLhs() 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().(ConstantIntegerExpr).getIntValue() = mod and
+    mod >= 2
+  )
+  or
+  exists(ConstantIntegerExpr c |
+    mod = 2.pow([1 .. 30]) and
+    c.getIntValue() = mod - 1 and
+    result.(BitwiseAndExpr).hasOperands(arg, c)
+  )
+}
+
+/**
+ * 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, ConstantIntegerExpr 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.(LShiftExpr).getRhs() = c and factor = 2.pow(k) and k > 0
+    or
+    e.(BitwiseAndExpr).getAnOperand() = c and factor = max(int f | andmaskFactor(k, f))
+  )
+}
+
+/**
+ * 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))
+}
+
+/**
+ * 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 = m.gcd(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 = m1.gcd(m2).gcd(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 = m1.gcd(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
+    getABasicBlockExpr(bb.getBlock()) = e
+  )
+  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 = m1.gcd(m2).gcd(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 = m1.gcd(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 = m1.gcd(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
+  )
+}
--- a/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll
+++ b/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll
@@ -0,0 +1,110 @@
+module Private {
+  private import csharp as CS
+  private import ConstantUtils as CU
+  private import semmle.code.csharp.controlflow.Guards as G
+  private import semmle.code.csharp.dataflow.internal.rangeanalysis.RangeUtils as RU
+  private import SsaUtils as SU
+  private import SignAnalysisSpecific::Private as SA
+
+  class BasicBlock = CS::Ssa::BasicBlock;
+
+  class SsaVariable extends CS::Ssa::Definition {
+    CS::AssignableRead getAUse() { result = this.getARead() }
+  }
+
+  class SsaPhiNode = CS::Ssa::PhiNode;
+
+  class Expr = CS::Expr;
+
+  class Guard = G::Guard;
+
+  class ConstantIntegerExpr = CU::ConstantIntegerExpr;
+
+  class ConditionalExpr extends CS::ConditionalExpr {
+    /** Gets the "then" expression of this conditional expression. */
+    Expr getTrueExpr() { result = this.getThen() }
+
+    /** Gets the "else" expression of this conditional expression. */
+    Expr getFalseExpr() { result = this.getElse() }
+  }
+
+  /** Represent an addition expression. */
+  class AddExpr extends CS::AddExpr {
+    /** Gets the LHS operand of this add expression. */
+    Expr getLhs() { result = this.getLeftOperand() }
+
+    /** Gets the RHS operand of this add expression. */
+    Expr getRhs() { result = this.getRightOperand() }
+  }
+
+  /** Represent a subtraction expression. */
+  class SubExpr extends CS::SubExpr {
+    /** Gets the LHS operand of this subtraction expression. */
+    Expr getLhs() { result = this.getLeftOperand() }
+
+    /** Gets the RHS operand of this subtraction expression. */
+    Expr getRhs() { result = this.getRightOperand() }
+  }
+
+  class RemExpr = CS::RemExpr;
+
+  /** Represent a bitwise and or an assign-and expression. */
+  class BitwiseAndExpr extends CS::Expr {
+    BitwiseAndExpr() { this instanceof CS::BitwiseAndExpr or this instanceof CS::AssignAndExpr }
+
+    /** Gets an operand of this bitwise and operation. */
+    Expr getAnOperand() {
+      result = this.(CS::BitwiseAndExpr).getAnOperand() or
+      result = this.(CS::AssignAndExpr).getRValue() or
+      result = this.(CS::AssignAndExpr).getLValue()
+    }
+
+    /** 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
+    }
+  }
+
+  /** Represent a multiplication or an assign-mul expression. */
+  class MulExpr extends CS::Expr {
+    MulExpr() { this instanceof CS::MulExpr or this instanceof CS::AssignMulExpr }
+
+    /** Gets an operand of this multiplication. */
+    Expr getAnOperand() {
+      result = this.(CS::MulExpr).getAnOperand() or
+      result = this.(CS::AssignMulExpr).getRValue() or
+      result = this.(CS::AssignMulExpr).getLValue()
+    }
+  }
+
+  /** Represent a left shift or an assign-lshift expression. */
+  class LShiftExpr extends CS::Expr {
+    LShiftExpr() { this instanceof CS::LShiftExpr or this instanceof CS::AssignLShiftExpr }
+
+    /** Gets the RHS operand of this shift. */
+    Expr getRhs() {
+      result = this.(CS::LShiftExpr).getRightOperand() or
+      result = this.(CS::AssignLShiftExpr).getRValue()
+    }
+  }
+
+  predicate guardDirectlyControlsSsaRead = SA::guardControlsSsaRead/3;
+
+  predicate guardControlsSsaRead = SA::guardControlsSsaRead/3;
+
+  predicate valueFlowStep = RU::valueFlowStep/3;
+
+  predicate eqFlowCond = RU::eqFlowCond/5;
+
+  predicate ssaUpdateStep = RU::ssaUpdateStep/3;
+
+  Expr getABasicBlockExpr(BasicBlock bb) { result = bb.getANode().getElement() }
+
+  private predicate id(CS::ControlFlowElement x, CS::ControlFlowElement y) { x = y }
+
+  private predicate idOf(CS::ControlFlowElement x, int y) = equivalenceRelation(id/2)(x, y)
+
+  int getId(BasicBlock bb) { idOf(bb.getFirstNode().getElement(), result) }
+}
--- a/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/RangeUtils.qll
+++ b/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/RangeUtils.qll
@@ -0,0 +1,98 @@
+/**
+ * Provides predicates for range and modulus analysis.
+ */
+
+private import csharp
+private import Ssa
+private import SsaUtils
+private import ConstantUtils
+private import SsaReadPositionCommon
+private import semmle.code.csharp.controlflow.Guards as G
+
+private class BooleanValue = G::AbstractValues::BooleanValue;
+
+/**
+ * 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
+}
+
+private G::Guard eqFlowCondAbs(Definition def, Expr e, int delta, boolean isEq, G::AbstractValue v) {
+  exists(boolean eqpolarity |
+    result.isEquality(ssaRead(def, delta), e, eqpolarity) and
+    eqpolarity.booleanXor(v.(BooleanValue).getValue()).booleanNot() = isEq
+  )
+  or
+  exists(G::AbstractValue v0 |
+    G::Internal::impliesSteps(result, v, eqFlowCondAbs(def, e, delta, isEq, v0), v0)
+  )
+}
+
+/**
+ * Gets a condition that tests whether `def` equals `e + delta`.
+ *
+ * If the condition evaluates to `testIsTrue`:
+ * - `isEq = true`  : `def == e + delta`
+ * - `isEq = false` : `def != e + delta`
+ */
+G::Guard eqFlowCond(Definition def, Expr e, int delta, boolean isEq, boolean testIsTrue) {
+  exists(BooleanValue v |
+    result = eqFlowCondAbs(def, e, delta, isEq, v) and
+    testIsTrue = v.getValue()
+  )
+}
+
+/**
+ * Holds if `e1 + delta` equals `e2`.
+ */
+predicate valueFlowStep(Expr e2, Expr e1, int delta) {
+  valueFlowStep(e2.(AssignOperation).getExpandedAssignment(), e1, delta)
+  or
+  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(ConstantIntegerExpr x |
+    e2.(AddExpr).getAnOperand() = e1 and
+    e2.(AddExpr).getAnOperand() = x and
+    not e1 = x
+  |
+    x.getIntValue() = delta
+  )
+  or
+  exists(ConstantIntegerExpr x |
+    exists(SubExpr sub |
+      e2 = sub and
+      sub.getLeftOperand() = e1 and
+      sub.getRightOperand() = x
+    )
+  |
+    x.getIntValue() = -delta
+  )
+}
+
+/**
+ * Holds if `guard` controls the position `controlled` with the value `testIsTrue`.
+ */
+predicate guardControlsSsaRead(G::Guard guard, SsaReadPosition controlled, boolean testIsTrue) {
+  exists(BooleanValue b | b.getValue() = testIsTrue |
+    guard.controlsBasicBlock(controlled.(SsaReadPositionBlock).getBlock(), b)
+  )
+}
--- a/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll
+++ b/csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll
@@ -2,9 +2,10 @@
 * Provides C#-specific definitions for use in sign analysis.
 */
 module Private {
-  private import SsaUtils as SU
  private import csharp as CS
+  private import SsaUtils as SU
  private import ConstantUtils as CU
+  private import RangeUtils as RU
  private import semmle.code.csharp.controlflow.Guards as G
  import Impl

@@ -33,6 +34,8 @@ module Private {
  class Expr = CS::Expr;

  predicate ssaRead = SU::ssaRead/2;
+
+  predicate guardControlsSsaRead = RU::guardControlsSsaRead/3;
 }

 private module Impl {
@@ -254,15 +257,6 @@ private module Impl {

  Guard getComparisonGuard(ComparisonExpr ce) { result = ce.getExpr() }

-  /**
-   * Holds if `guard` controls the position `controlled` with the value `testIsTrue`.
-   */
-  predicate guardControlsSsaRead(Guard guard, SsaReadPosition controlled, boolean testIsTrue) {
-    exists(BooleanValue b | b.getValue() = testIsTrue |
-      guard.controlsBasicBlock(controlled.(SsaReadPositionBlock).getBlock(), b)
-    )
-  }
-
  /** A relational comparison */
  class ComparisonExpr extends ComparisonTest {
    private boolean strict;
--- a/csharp/ql/test/library-tests/dataflow/modulusanalysis/ModulusAnalysis.cs
+++ b/csharp/ql/test/library-tests/dataflow/modulusanalysis/ModulusAnalysis.cs
@@ -0,0 +1,84 @@
+using System;
+using System.Linq;
+
+class ModulusAnalysis
+{
+    const int c1 = 42;
+    const int c2 = 43;
+
+    void M(int i, bool cond, int x, int y, int[] arr, int otherSeven)
+    {
+        var eq = i + 3;
+
+        var mul = eq * c1 + 3; // congruent 3 mod 42
+
+        int seven = 7;
+        if (mul % c2 == seven)
+        {
+            System.Console.WriteLine(mul); // congruent 7 mod 43, 3 mod 42
+        }
+
+        if (otherSeven == 7)
+        {
+            if (mul % c2 == otherSeven)
+            {
+                System.Console.WriteLine(mul); // congruent 3 mod 42, 7 mod 43 missing
+            }
+        }
+
+        var j = cond
+            ? i * 4 + 3
+            : i * 8 + 7;
+        System.Console.WriteLine(j); // congruent 3 mod 4
+
+        if (x % c1 == 3 && y % c1 == 7)
+        {
+            System.Console.WriteLine(x + y); // congruent 10 mod 42
+        }
+
+        if (x % c1 == 3 && y % c1 == 7)
+        {
+            System.Console.WriteLine(x - y); // congruent 38 mod 42
+        }
+
+        var l = arr.Length * 4 - 11; // congruent 1 mod 4
+        System.Console.WriteLine(l);
+
+        l = GetArray().Length * 4 - 11;
+        System.Console.WriteLine(l); // congruent 1 mod 4
+
+        if (cond)
+        {
+            j = i * 4 + 3;
+        }
+        else
+        {
+            j = i * 8 + 7;
+        }
+        System.Console.WriteLine(j); // congruent 3 mod 4 or 7 mod 8
+
+        if (cond)
+        {
+            System.Console.WriteLine(j); // congruent 3 mod 4
+        }
+        else
+        {
+            System.Console.WriteLine(j); // congruent 7 mod 8
+        }
+
+        var t = 64;
+        System.Console.WriteLine(t & 32); // congruent 0 mod 32
+        System.Console.WriteLine(t & 16); // congruent 0 mod 16
+        t = 1;
+        System.Console.WriteLine(t << 2); // congruent 0 mod 4
+
+        if ((x & 15) == 3)
+        {
+            System.Console.WriteLine(x); // congruent 3 mod 16
+        }
+    }
+
+
+
+    int[] GetArray(){ return new int[42]; }
+}
--- a/csharp/ql/test/library-tests/dataflow/modulusanalysis/ModulusAnalysis.expected
+++ b/csharp/ql/test/library-tests/dataflow/modulusanalysis/ModulusAnalysis.expected
@@ -0,0 +1,138 @@
+| ModulusAnalysis.cs:6:15:6:21 | ... = ... | 0 | 42 | 0 |
+| ModulusAnalysis.cs:6:20:6:21 | 42 | 0 | 42 | 0 |
+| ModulusAnalysis.cs:7:15:7:21 | ... = ... | 0 | 43 | 0 |
+| ModulusAnalysis.cs:7:20:7:21 | 43 | 0 | 43 | 0 |
+| ModulusAnalysis.cs:11:18:11:18 | access to parameter i | SSA param(i) | 0 | 0 |
+| ModulusAnalysis.cs:11:18:11:22 | ... + ... | SSA param(i) | 3 | 0 |
+| ModulusAnalysis.cs:11:22:11:22 | 3 | 0 | 3 | 0 |
+| ModulusAnalysis.cs:13:19:13:20 | access to local variable eq | SSA def(eq) | 0 | 0 |
+| ModulusAnalysis.cs:13:19:13:20 | access to local variable eq | SSA param(i) | 3 | 0 |
+| ModulusAnalysis.cs:13:19:13:25 | ... * ... | 0 | 0 | 42 |
+| ModulusAnalysis.cs:13:19:13:29 | ... + ... | 0 | 3 | 42 |
+| ModulusAnalysis.cs:13:24:13:25 | access to constant c1 | 0 | 42 | 0 |
+| ModulusAnalysis.cs:13:24:13:25 | access to constant c1 | SSA entry def(ModulusAnalysis.c1) | 0 | 0 |
+| ModulusAnalysis.cs:13:29:13:29 | 3 | 0 | 3 | 0 |
+| ModulusAnalysis.cs:15:21:15:21 | 7 | 0 | 7 | 0 |
+| ModulusAnalysis.cs:16:13:16:15 | access to local variable mul | 0 | 3 | 42 |
+| ModulusAnalysis.cs:16:13:16:15 | access to local variable mul | SSA def(mul) | 0 | 0 |
+| ModulusAnalysis.cs:16:19:16:20 | access to constant c2 | 0 | 43 | 0 |
+| ModulusAnalysis.cs:16:19:16:20 | access to constant c2 | SSA entry def(ModulusAnalysis.c2) | 0 | 0 |
+| ModulusAnalysis.cs:16:25:16:29 | access to local variable seven | 0 | 7 | 0 |
+| ModulusAnalysis.cs:16:25:16:29 | access to local variable seven | SSA def(seven) | 0 | 0 |
+| ModulusAnalysis.cs:18:38:18:40 | access to local variable mul | 0 | 3 | 42 |
+| ModulusAnalysis.cs:18:38:18:40 | access to local variable mul | 0 | 7 | 43 |
+| ModulusAnalysis.cs:18:38:18:40 | access to local variable mul | SSA def(mul) | 0 | 0 |
+| ModulusAnalysis.cs:21:13:21:22 | access to parameter otherSeven | SSA param(otherSeven) | 0 | 0 |
+| ModulusAnalysis.cs:21:27:21:27 | 7 | 0 | 7 | 0 |
+| ModulusAnalysis.cs:23:17:23:19 | access to local variable mul | 0 | 3 | 42 |
+| ModulusAnalysis.cs:23:17:23:19 | access to local variable mul | SSA def(mul) | 0 | 0 |
+| ModulusAnalysis.cs:23:23:23:24 | access to constant c2 | 0 | 43 | 0 |
+| ModulusAnalysis.cs:23:23:23:24 | access to constant c2 | SSA entry def(ModulusAnalysis.c2) | 0 | 0 |
+| ModulusAnalysis.cs:23:29:23:38 | access to parameter otherSeven | 0 | 7 | 0 |
+| ModulusAnalysis.cs:23:29:23:38 | access to parameter otherSeven | SSA param(otherSeven) | 0 | 0 |
+| ModulusAnalysis.cs:25:42:25:44 | access to local variable mul | 0 | 3 | 42 |
+| ModulusAnalysis.cs:25:42:25:44 | access to local variable mul | SSA def(mul) | 0 | 0 |
+| ModulusAnalysis.cs:29:17:31:23 | ... ? ... : ... | 0 | 3 | 4 |
+| ModulusAnalysis.cs:30:15:30:15 | access to parameter i | SSA param(i) | 0 | 0 |
+| ModulusAnalysis.cs:30:15:30:19 | ... * ... | 0 | 0 | 4 |
+| ModulusAnalysis.cs:30:15:30:23 | ... + ... | 0 | 3 | 4 |
+| ModulusAnalysis.cs:30:19:30:19 | 4 | 0 | 4 | 0 |
+| ModulusAnalysis.cs:30:23:30:23 | 3 | 0 | 3 | 0 |
+| ModulusAnalysis.cs:31:15:31:15 | access to parameter i | SSA param(i) | 0 | 0 |
+| ModulusAnalysis.cs:31:15:31:19 | ... * ... | 0 | 0 | 8 |
+| ModulusAnalysis.cs:31:15:31:23 | ... + ... | 0 | 7 | 8 |
+| ModulusAnalysis.cs:31:19:31:19 | 8 | 0 | 8 | 0 |
+| ModulusAnalysis.cs:31:23:31:23 | 7 | 0 | 7 | 0 |
+| ModulusAnalysis.cs:32:34:32:34 | access to local variable j | 0 | 3 | 4 |
+| ModulusAnalysis.cs:32:34:32:34 | access to local variable j | [cond (line 9): false] SSA def(j) | 0 | 0 |
+| ModulusAnalysis.cs:32:34:32:34 | access to local variable j | [cond (line 9): true] SSA def(j) | 0 | 0 |
+| ModulusAnalysis.cs:34:13:34:13 | access to parameter x | SSA param(x) | 0 | 0 |
+| ModulusAnalysis.cs:34:17:34:18 | access to constant c1 | 0 | 42 | 0 |
+| ModulusAnalysis.cs:34:17:34:18 | access to constant c1 | SSA entry def(ModulusAnalysis.c1) | 0 | 0 |
+| ModulusAnalysis.cs:34:23:34:23 | 3 | 0 | 3 | 0 |
+| ModulusAnalysis.cs:34:28:34:28 | access to parameter y | SSA param(y) | 0 | 0 |
+| ModulusAnalysis.cs:34:32:34:33 | access to constant c1 | 0 | 42 | 0 |
+| ModulusAnalysis.cs:34:32:34:33 | access to constant c1 | SSA entry def(ModulusAnalysis.c1) | 0 | 0 |
+| ModulusAnalysis.cs:34:38:34:38 | 7 | 0 | 7 | 0 |
+| ModulusAnalysis.cs:36:38:36:38 | access to parameter x | 0 | 3 | 42 |
+| ModulusAnalysis.cs:36:38:36:38 | access to parameter x | SSA param(x) | 0 | 0 |
+| ModulusAnalysis.cs:36:38:36:42 | ... + ... | 0 | 10 | 42 |
+| ModulusAnalysis.cs:36:38:36:42 | ... + ... | SSA param(x) | 7 | 42 |
+| ModulusAnalysis.cs:36:38:36:42 | ... + ... | SSA param(y) | 3 | 42 |
+| ModulusAnalysis.cs:36:42:36:42 | access to parameter y | 0 | 7 | 42 |
+| ModulusAnalysis.cs:36:42:36:42 | access to parameter y | SSA param(y) | 0 | 0 |
+| ModulusAnalysis.cs:39:13:39:13 | access to parameter x | SSA param(x) | 0 | 0 |
+| ModulusAnalysis.cs:39:17:39:18 | access to constant c1 | 0 | 42 | 0 |
+| ModulusAnalysis.cs:39:17:39:18 | access to constant c1 | SSA entry def(ModulusAnalysis.c1) | 0 | 0 |
+| ModulusAnalysis.cs:39:23:39:23 | 3 | 0 | 3 | 0 |
+| ModulusAnalysis.cs:39:28:39:28 | access to parameter y | SSA param(y) | 0 | 0 |
+| ModulusAnalysis.cs:39:32:39:33 | access to constant c1 | 0 | 42 | 0 |
+| ModulusAnalysis.cs:39:32:39:33 | access to constant c1 | SSA entry def(ModulusAnalysis.c1) | 0 | 0 |
+| ModulusAnalysis.cs:39:38:39:38 | 7 | 0 | 7 | 0 |
+| ModulusAnalysis.cs:41:38:41:38 | access to parameter x | 0 | 3 | 42 |
+| ModulusAnalysis.cs:41:38:41:38 | access to parameter x | SSA param(x) | 0 | 0 |
+| ModulusAnalysis.cs:41:38:41:42 | ... - ... | 0 | 38 | 42 |
+| ModulusAnalysis.cs:41:38:41:42 | ... - ... | SSA param(x) | 35 | 42 |
+| ModulusAnalysis.cs:41:42:41:42 | access to parameter y | 0 | 7 | 42 |
+| ModulusAnalysis.cs:41:42:41:42 | access to parameter y | SSA param(y) | 0 | 0 |
+| ModulusAnalysis.cs:44:17:44:26 | access to property Length | [cond (line 9): false] SSA untracked def(arr.Length) | 0 | 0 |
+| ModulusAnalysis.cs:44:17:44:26 | access to property Length | [cond (line 9): true] SSA untracked def(arr.Length) | 0 | 0 |
+| ModulusAnalysis.cs:44:17:44:30 | ... * ... | 0 | 0 | 4 |
+| ModulusAnalysis.cs:44:17:44:35 | ... - ... | 0 | 1 | 4 |
+| ModulusAnalysis.cs:44:30:44:30 | 4 | 0 | 4 | 0 |
+| ModulusAnalysis.cs:44:34:44:35 | 11 | 0 | 11 | 0 |
+| ModulusAnalysis.cs:45:34:45:34 | access to local variable l | 0 | 1 | 4 |
+| ModulusAnalysis.cs:45:34:45:34 | access to local variable l | [cond (line 9): false] SSA def(l) | 0 | 0 |
+| ModulusAnalysis.cs:45:34:45:34 | access to local variable l | [cond (line 9): true] SSA def(l) | 0 | 0 |
+| ModulusAnalysis.cs:47:9:47:38 | ... = ... | 0 | 1 | 4 |
+| ModulusAnalysis.cs:47:13:47:29 | access to property Length | access to property Length | 0 | 0 |
+| ModulusAnalysis.cs:47:13:47:33 | ... * ... | 0 | 0 | 4 |
+| ModulusAnalysis.cs:47:13:47:38 | ... - ... | 0 | 1 | 4 |
+| ModulusAnalysis.cs:47:33:47:33 | 4 | 0 | 4 | 0 |
+| ModulusAnalysis.cs:47:37:47:38 | 11 | 0 | 11 | 0 |
+| ModulusAnalysis.cs:48:34:48:34 | access to local variable l | 0 | 1 | 4 |
+| ModulusAnalysis.cs:48:34:48:34 | access to local variable l | [cond (line 9): false] SSA def(l) | 0 | 0 |
+| ModulusAnalysis.cs:48:34:48:34 | access to local variable l | [cond (line 9): true] SSA def(l) | 0 | 0 |
+| ModulusAnalysis.cs:52:13:52:25 | ... = ... | 0 | 3 | 4 |
+| ModulusAnalysis.cs:52:17:52:17 | access to parameter i | SSA param(i) | 0 | 0 |
+| ModulusAnalysis.cs:52:17:52:21 | ... * ... | 0 | 0 | 4 |
+| ModulusAnalysis.cs:52:17:52:25 | ... + ... | 0 | 3 | 4 |
+| ModulusAnalysis.cs:52:21:52:21 | 4 | 0 | 4 | 0 |
+| ModulusAnalysis.cs:52:25:52:25 | 3 | 0 | 3 | 0 |
+| ModulusAnalysis.cs:56:13:56:25 | ... = ... | 0 | 7 | 8 |
+| ModulusAnalysis.cs:56:17:56:17 | access to parameter i | SSA param(i) | 0 | 0 |
+| ModulusAnalysis.cs:56:17:56:21 | ... * ... | 0 | 0 | 8 |
+| ModulusAnalysis.cs:56:17:56:25 | ... + ... | 0 | 7 | 8 |
+| ModulusAnalysis.cs:56:21:56:21 | 8 | 0 | 8 | 0 |
+| ModulusAnalysis.cs:56:25:56:25 | 7 | 0 | 7 | 0 |
+| ModulusAnalysis.cs:58:34:58:34 | access to local variable j | 0 | 3 | 4 |
+| ModulusAnalysis.cs:58:34:58:34 | access to local variable j | 0 | 7 | 8 |
+| ModulusAnalysis.cs:58:34:58:34 | access to local variable j | [cond (line 9): false] SSA def(j) | 0 | 0 |
+| ModulusAnalysis.cs:58:34:58:34 | access to local variable j | [cond (line 9): true] SSA def(j) | 0 | 0 |
+| ModulusAnalysis.cs:62:38:62:38 | access to local variable j | 0 | 3 | 4 |
+| ModulusAnalysis.cs:62:38:62:38 | access to local variable j | [cond (line 9): true] SSA def(j) | 0 | 0 |
+| ModulusAnalysis.cs:66:38:66:38 | access to local variable j | 0 | 7 | 8 |
+| ModulusAnalysis.cs:66:38:66:38 | access to local variable j | [cond (line 9): false] SSA def(j) | 0 | 0 |
+| ModulusAnalysis.cs:69:17:69:18 | 64 | 0 | 64 | 0 |
+| ModulusAnalysis.cs:70:34:70:34 | access to local variable t | 0 | 64 | 0 |
+| ModulusAnalysis.cs:70:34:70:34 | access to local variable t | SSA def(t) | 0 | 0 |
+| ModulusAnalysis.cs:70:34:70:39 | ... & ... | 0 | 0 | 32 |
+| ModulusAnalysis.cs:70:34:70:39 | ... & ... | 0 | 0 | 64 |
+| ModulusAnalysis.cs:70:38:70:39 | 32 | 0 | 32 | 0 |
+| ModulusAnalysis.cs:71:34:71:34 | access to local variable t | 0 | 64 | 0 |
+| ModulusAnalysis.cs:71:34:71:34 | access to local variable t | SSA def(t) | 0 | 0 |
+| ModulusAnalysis.cs:71:34:71:39 | ... & ... | 0 | 0 | 16 |
+| ModulusAnalysis.cs:71:34:71:39 | ... & ... | 0 | 0 | 64 |
+| ModulusAnalysis.cs:71:38:71:39 | 16 | 0 | 16 | 0 |
+| ModulusAnalysis.cs:72:9:72:13 | ... = ... | 0 | 1 | 0 |
+| ModulusAnalysis.cs:72:13:72:13 | 1 | 0 | 1 | 0 |
+| ModulusAnalysis.cs:73:34:73:34 | access to local variable t | 0 | 1 | 0 |
+| ModulusAnalysis.cs:73:34:73:34 | access to local variable t | SSA def(t) | 0 | 0 |
+| ModulusAnalysis.cs:73:34:73:39 | ... << ... | 0 | 0 | 4 |
+| ModulusAnalysis.cs:73:39:73:39 | 2 | 0 | 2 | 0 |
+| ModulusAnalysis.cs:75:14:75:14 | access to parameter x | SSA param(x) | 0 | 0 |
+| ModulusAnalysis.cs:75:18:75:19 | 15 | 0 | 15 | 0 |
+| ModulusAnalysis.cs:75:25:75:25 | 3 | 0 | 3 | 0 |
+| ModulusAnalysis.cs:77:38:77:38 | access to parameter x | 0 | 3 | 16 |
+| ModulusAnalysis.cs:77:38:77:38 | access to parameter x | SSA param(x) | 0 | 0 |
+| ModulusAnalysis.cs:83:38:83:39 | 42 | 0 | 42 | 0 |
--- a/csharp/ql/test/library-tests/dataflow/modulusanalysis/ModulusAnalysis.ql
+++ b/csharp/ql/test/library-tests/dataflow/modulusanalysis/ModulusAnalysis.ql
@@ -0,0 +1,7 @@
+import csharp
+import semmle.code.csharp.dataflow.ModulusAnalysis
+import semmle.code.csharp.dataflow.Bound
+
+from Expr e, Bound b, int delta, int mod
+where exprModulus(e, b, delta, mod)
+select e, b.toString(), delta, mod
--- a/java/ql/src/semmle/code/java/dataflow/ModulusAnalysis.qll
+++ b/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
 }
@@ -75,7 +58,7 @@ private Expr modExpr(Expr arg, int mod) {
  exists(ConstantIntegerExpr c |
    mod = 2.pow([1 .. 30]) and
    c.getIntValue() = mod - 1 and
-    result.(AndBitwiseExpr).hasOperands(arg, c)
+    result.(BitwiseAndExpr).hasOperands(arg, c)
  )
 }

@@ -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 |
--- a/java/ql/src/semmle/code/java/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll
+++ b/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) }
+}