Rangeanalysis: Simplify Guards integration.

java/ql/lib/semmle/code/java/controlflow/Guards.qll

@@ -145,7 +145,7 @@ private predicate isNonFallThroughPredecessor(SwitchCase sc, ControlFlowNode pre
  * Evaluating a switch case to true corresponds to taking that switch case, and
  * evaluating it to false corresponds to taking some other branch.
  */
-class Guard extends ExprParent {
+final class Guard extends ExprParent {
   Guard() {
     this.(Expr).getType() instanceof BooleanType and not this instanceof BooleanLiteral
     or
@@ -360,6 +360,18 @@ private predicate guardControls_v3(Guard guard, BasicBlock controlled, boolean b
   )
 }
 
+pragma[nomagic]
+private predicate guardControlsBranchEdge_v2(
+  Guard guard, BasicBlock bb1, BasicBlock bb2, boolean branch
+) {
+  guard.hasBranchEdge(bb1, bb2, branch)
+  or
+  exists(Guard g, boolean b |
+    guardControlsBranchEdge_v2(g, bb1, bb2, b) and
+    implies_v2(g, b, guard, branch)
+  )
+}
+
 pragma[nomagic]
 private predicate guardControlsBranchEdge_v3(
   Guard guard, BasicBlock bb1, BasicBlock bb2, boolean branch
@@ -372,6 +384,27 @@ private predicate guardControlsBranchEdge_v3(
   )
 }
 
+/** INTERNAL: Use `Guard` instead. */
+final class Guard_v2 extends Guard {
+  /**
+   * Holds if this guard evaluating to `branch` controls the control-flow
+   * branch edge from `bb1` to `bb2`. That is, following the edge from
+   * `bb1` to `bb2` implies that this guard evaluated to `branch`.
+   */
+  predicate controlsBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) {
+    guardControlsBranchEdge_v2(this, bb1, bb2, branch)
+  }
+
+  /**
+   * Holds if this guard evaluating to `branch` directly or indirectly controls
+   * the block `controlled`. That is, the evaluation of `controlled` is
+   * dominated by this guard evaluating to `branch`.
+   */
+  predicate controls(BasicBlock controlled, boolean branch) {
+    guardControls_v2(this, controlled, branch)
+  }
+}
+
 private predicate equalityGuard(Guard g, Expr e1, Expr e2, boolean polarity) {
   exists(EqualityTest eqtest |
     eqtest = g and

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

@@ -17,7 +17,7 @@ private predicate valueFlowStepSsa(SsaVariable v, SsaReadPosition pos, Expr e, i
   exists(Guard guard, boolean testIsTrue |
     pos.hasReadOfVar(v) and
     guard = eqFlowCond(v, e, delta, true, testIsTrue) and
-    guardDirectlyControlsSsaRead(guard, pos, testIsTrue)
+    guardControlsSsaRead(guard, pos, testIsTrue)
   )
 }
 

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

@@ -219,16 +219,10 @@ module Sem implements Semantic<Location> {
 
   int getBlockId1(BasicBlock bb) { idOf(bb, result) }
 
-  final private class FinalGuard = GL::Guard;
-
-  class Guard extends FinalGuard {
+  class Guard extends GL::Guard_v2 {
     Expr asExpr() { result = this }
   }
 
-  predicate implies_v2(Guard g1, boolean b1, Guard g2, boolean b2) {
-    GL::implies_v2(g1, b1, g2, b2)
-  }
-
   class Type = J::Type;
 
   class IntegerType extends J::IntegralType {

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

@@ -19,8 +19,6 @@ predicate ssaUpdateStep = U::ssaUpdateStep/3;
 
 predicate valueFlowStep = U::valueFlowStep/3;
 
-predicate guardDirectlyControlsSsaRead = U::guardDirectlyControlsSsaRead/3;
-
 predicate guardControlsSsaRead = U::guardControlsSsaRead/3;
 
 predicate eqFlowCond = U::eqFlowCond/5;

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

@@ -4,7 +4,6 @@ module Private {
   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
-  private import semmle.code.java.controlflow.internal.GuardsLogic as GL
   private import SsaReadPositionCommon
 
   class BasicBlock = BB::BasicBlock;
@@ -15,7 +14,7 @@ module Private {
 
   class Expr = J::Expr;
 
-  class Guard = G::Guard;
+  class Guard = G::Guard_v2;
 
   class ConstantIntegerExpr = RU::ConstantIntegerExpr;
 
@@ -101,29 +100,17 @@ module Private {
     }
   }
 
-  /**
-   * Holds if `guard` directly controls the position `controlled` with the
-   * value `testIsTrue`.
-   */
-  pragma[nomagic]
-  predicate guardDirectlyControlsSsaRead(Guard guard, SsaReadPosition controlled, boolean testIsTrue) {
-    guard.directlyControls(controlled.(SsaReadPositionBlock).getBlock(), testIsTrue)
-    or
-    exists(SsaReadPositionPhiInputEdge controlledEdge | controlledEdge = controlled |
-      guard.directlyControls(controlledEdge.getOrigBlock(), testIsTrue) or
-      guard.hasBranchEdge(controlledEdge.getOrigBlock(), controlledEdge.getPhiBlock(), testIsTrue)
-    )
-  }
-
   /**
    * Holds if `guard` controls the position `controlled` with the value `testIsTrue`.
    */
   predicate guardControlsSsaRead(Guard guard, SsaReadPosition controlled, boolean testIsTrue) {
-    guardDirectlyControlsSsaRead(guard, controlled, testIsTrue)
+    guard.controls(controlled.(SsaReadPositionBlock).getBlock(), testIsTrue)
     or
-    exists(Guard guard0, boolean testIsTrue0 |
-      GL::implies_v2(guard0, testIsTrue0, guard, testIsTrue) and
-      guardControlsSsaRead(guard0, controlled, testIsTrue0)
+    exists(SsaReadPositionPhiInputEdge controlledEdge | controlledEdge = controlled |
+      guard.controls(controlledEdge.getOrigBlock(), testIsTrue) or
+      guard
+          .controlsBranchEdge(controlledEdge.getOrigBlock(), controlledEdge.getPhiBlock(),
+            testIsTrue)
     )
   }
 

java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll

@@ -7,13 +7,12 @@ module Private {
   private import semmle.code.java.dataflow.SSA as Ssa
   private import semmle.code.java.controlflow.Guards as G
   private import SsaReadPositionCommon
-  private import semmle.code.java.controlflow.internal.GuardsLogic as GL
   private import Sign
   import Impl
 
   class ConstantIntegerExpr = RU::ConstantIntegerExpr;
 
-  class Guard = G::Guard;
+  class Guard = G::Guard_v2;
 
   class SsaVariable = Ssa::SsaVariable;
 
@@ -170,31 +169,17 @@ module Private {
 
   predicate ssaRead = RU::ssaRead/2;
 
-  /**
-   * Holds if `guard` directly controls the position `controlled` with the
-   * value `testIsTrue`.
-   */
-  pragma[nomagic]
-  private predicate guardDirectlyControlsSsaRead(
-    Guard guard, SsaReadPosition controlled, boolean testIsTrue
-  ) {
-    guard.directlyControls(controlled.(SsaReadPositionBlock).getBlock(), testIsTrue)
-    or
-    exists(SsaReadPositionPhiInputEdge controlledEdge | controlledEdge = controlled |
-      guard.directlyControls(controlledEdge.getOrigBlock(), testIsTrue) or
-      guard.hasBranchEdge(controlledEdge.getOrigBlock(), controlledEdge.getPhiBlock(), testIsTrue)
-    )
-  }
-
   /**
    * Holds if `guard` controls the position `controlled` with the value `testIsTrue`.
    */
   predicate guardControlsSsaRead(Guard guard, SsaReadPosition controlled, boolean testIsTrue) {
-    guardDirectlyControlsSsaRead(guard, controlled, testIsTrue)
+    guard.controls(controlled.(SsaReadPositionBlock).getBlock(), testIsTrue)
     or
-    exists(Guard guard0, boolean testIsTrue0 |
-      GL::implies_v2(guard0, testIsTrue0, guard, testIsTrue) and
-      guardControlsSsaRead(guard0, controlled, testIsTrue0)
+    exists(SsaReadPositionPhiInputEdge controlledEdge | controlledEdge = controlled |
+      guard.controls(controlledEdge.getOrigBlock(), testIsTrue) or
+      guard
+          .controlsBranchEdge(controlledEdge.getOrigBlock(), controlledEdge.getPhiBlock(),
+            testIsTrue)
     )
   }
 }