Java/C++: Share eqFlowCond.

Author: aschackmull

cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeUtils.qll

@@ -9,56 +9,6 @@ private import RangeAnalysisImpl
 private import ConstantAnalysis
 
 module RangeUtil<DeltaSig D, LangSig<Sem, D> Lang> implements UtilSig<Sem, D> {
-  /**
-   * Gets an expression that equals `v - d`.
-   */
-  private SemExpr semSsaRead(SemSsaVariable v, D::Delta delta) {
-    // There are various language-specific extension points that can be removed once we no longer
-    // expect to match the original Java implementation's results exactly.
-    result = v.getAUse() and delta = D::fromInt(0)
-    or
-    exists(D::Delta d1, SemConstantIntegerExpr c |
-      result.(SemAddExpr).hasOperands(semSsaRead(v, d1), c) and
-      delta = D::fromFloat(D::toFloat(d1) - c.getIntValue())
-    )
-    or
-    exists(SemSubExpr sub, D::Delta d1, SemConstantIntegerExpr c |
-      result = sub and
-      sub.getLeftOperand() = semSsaRead(v, d1) and
-      sub.getRightOperand() = c and
-      delta = D::fromFloat(D::toFloat(d1) + c.getIntValue())
-    )
-    or
-    result = v.(SemSsaExplicitUpdate).getSourceExpr() and
-    delta = D::fromFloat(0)
-    or
-    result.(SemCopyValueExpr).getOperand() = semSsaRead(v, delta)
-    or
-    result.(SemStoreExpr).getOperand() = semSsaRead(v, delta)
-  }
-
-  /**
-   * 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`
-   */
-  pragma[nomagic]
-  SemGuard semEqFlowCond(
-    SemSsaVariable v, SemExpr e, D::Delta delta, boolean isEq, boolean testIsTrue
-  ) {
-    exists(boolean eqpolarity |
-      result.isEquality(semSsaRead(v, delta), e, eqpolarity) and
-      (testIsTrue = true or testIsTrue = false) and
-      eqpolarity.booleanXor(testIsTrue).booleanNot() = isEq
-    )
-    or
-    exists(boolean testIsTrue0 |
-      semImplies_v2(result, testIsTrue, semEqFlowCond(v, e, delta, isEq, testIsTrue0), testIsTrue0)
-    )
-  }
-
   /**
    * Holds if `v` is an `SsaExplicitUpdate` that equals `e + delta`.
    */

java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll

@@ -372,12 +372,6 @@ module JavaLangImpl implements LangSig<Sem, IntDelta> {
 module Utils implements UtilSig<Sem, IntDelta> {
   private import RangeUtils as RU
 
-  Sem::Guard semEqFlowCond(
-    Sem::SsaVariable v, Sem::Expr e, int delta, boolean isEq, boolean testIsTrue
-  ) {
-    result = RU::eqFlowCond(v, e, delta, isEq, testIsTrue)
-  }
-
   predicate semSsaUpdateStep(Sem::SsaExplicitUpdate v, Sem::Expr e, int delta) {
     RU::ssaUpdateStep(v, e, delta)
   }

java/ql/lib/semmle/code/java/dataflow/RangeUtils.qll

@@ -19,6 +19,8 @@ predicate guardDirectlyControlsSsaRead = U::guardDirectlyControlsSsaRead/3;
 
 predicate guardControlsSsaRead = U::guardControlsSsaRead/3;
 
+predicate eqFlowCond = U::eqFlowCond/5;
+
 /**
  * Holds if `v` is an input to `phi` that is not along a back edge, and the
  * only other input to `phi` is a `null` value.
@@ -156,25 +158,6 @@ class ConstantStringExpr extends Expr {
   string getStringValue() { constantStringExpr(this, result) }
 }
 
-/**
- * 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`
- */
-Guard eqFlowCond(SsaVariable 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 |
-    implies_v2(result, testIsTrue, eqFlowCond(v, e, delta, isEq, testIsTrue0), testIsTrue0)
-  )
-}
-
 /**
  * Holds if `v` is an `SsaExplicitUpdate` that equals `e + delta`.
  */

shared/rangeanalysis/codeql/rangeanalysis/ModulusAnalysis.qll

@@ -34,7 +34,7 @@ module ModulusAnalysis<
     or
     exists(Sem::Guard guard, boolean testIsTrue |
       hasReadOfVarInlineLate(pos, v) and
-      guard = U::semEqFlowCond(v, e, D::fromInt(delta), true, testIsTrue) and
+      guard = eqFlowCond(v, e, D::fromInt(delta), true, testIsTrue) and
       guardDirectlyControlsSsaRead(guard, pos, testIsTrue)
     )
   }

shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll

@@ -304,10 +304,6 @@ signature module LangSig<Semantic Sem, DeltaSig D> {
 }
 
 signature module UtilSig<Semantic Sem, DeltaSig DeltaParam> {
-  Sem::Guard semEqFlowCond(
-    Sem::SsaVariable v, Sem::Expr e, DeltaParam::Delta delta, boolean isEq, boolean testIsTrue
-  );
-
   predicate semSsaUpdateStep(Sem::SsaExplicitUpdate v, Sem::Expr e, DeltaParam::Delta delta);
 
   predicate semValueFlowStep(Sem::Expr e2, Sem::Expr e1, DeltaParam::Delta delta);
@@ -447,7 +443,7 @@ module RangeStage<
      */
     cached
     predicate possibleReason(Sem::Guard guard) {
-      guard = boundFlowCond(_, _, _, _, _) or guard = semEqFlowCond(_, _, _, _, _)
+      guard = boundFlowCond(_, _, _, _, _) or guard = eqFlowCond(_, _, _, _, _)
     }
   }
 
@@ -609,7 +605,7 @@ module RangeStage<
         testIsTrue0)
     )
     or
-    result = semEqFlowCond(v, e, delta, true, testIsTrue) and
+    result = eqFlowCond(v, e, delta, true, testIsTrue) and
     (upper = true or upper = false)
     or
     // guard that tests whether `v2` is bounded by `e + delta + d1 - d2` and
@@ -630,7 +626,7 @@ module RangeStage<
     Sem::SsaVariable v1, Sem::SsaVariable v2, float delta
   ) {
     exists(Sem::Guard guardEq, D::Delta d1, D::Delta d2, boolean eqIsTrue |
-      guardEq = semEqFlowCond(v1, ssaRead(v2, d1), d2, true, eqIsTrue) and
+      guardEq = eqFlowCond(v1, ssaRead(v2, d1), d2, true, eqIsTrue) and
       delta = D::toFloat(d2) - D::toFloat(d1) and
       guardEq.directlyControls(result, eqIsTrue)
     )
@@ -695,7 +691,7 @@ module RangeStage<
     getTrackedTypeForSsaVariable(v) instanceof Sem::IntegerType and
     exists(Sem::Guard guard, boolean testIsTrue |
       pos.hasReadOfVar(v) and
-      guard = semEqFlowCond(v, e, delta, false, testIsTrue) and
+      guard = eqFlowCond(v, e, delta, false, testIsTrue) and
       guardDirectlyControlsSsaRead(guard, pos, testIsTrue) and
       reason = TSemCondReason(guard)
     )

shared/rangeanalysis/codeql/rangeanalysis/internal/RangeUtils.qll

@@ -37,6 +37,26 @@ module MakeUtils<Semantic Lang, DeltaSig D> {
     result.(CopyValueExpr).getOperand() = ssaRead(v, delta)
   }
 
+  /**
+   * 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`
+   */
+  pragma[nomagic]
+  Guard eqFlowCond(SsaVariable v, Expr e, D::Delta 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 |
+      implies_v2(result, testIsTrue, eqFlowCond(v, e, delta, isEq, testIsTrue0), testIsTrue0)
+    )
+  }
+
   private newtype TSsaReadPosition =
     TSsaReadPositionBlock(BasicBlock bb) {
       exists(SsaVariable v | v.getAUse().getBasicBlock() = bb)