Rangeanalysis: Simplify Guards integration.

aschackmull · aschackmull · commit 62000319fed5 · 2025-05-23T13:39:53.000+02:00
diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticExprSpecific.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticExprSpecific.qll
@@ -264,10 +264,6 @@ module SemanticExprConfig {
 
   Guard comparisonGuard(Expr e) { getSemanticExpr(result) = e }
 
-  predicate implies_v2(Guard g1, boolean b1, Guard g2, boolean b2) {
-    none() // TODO
-  }
-
   /** Gets the expression associated with `instr`. */
   SemExpr getSemanticExpr(IR::Instruction instr) { result = instr }
 }
diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticGuard.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/SemanticGuard.qll
@@ -18,11 +18,11 @@ class SemGuard instanceof Specific::Guard {
     Specific::equalityGuard(this, e1, e2, polarity)
   }
 
-  final predicate directlyControls(SemBasicBlock controlled, boolean branch) {
+  final predicate controls(SemBasicBlock controlled, boolean branch) {
     Specific::guardDirectlyControlsBlock(this, controlled, branch)
   }
 
-  final predicate hasBranchEdge(SemBasicBlock bb1, SemBasicBlock bb2, boolean branch) {
+  final predicate controlsBranchEdge(SemBasicBlock bb1, SemBasicBlock bb2, boolean branch) {
     Specific::guardHasBranchEdge(this, bb1, bb2, branch)
   }
 
@@ -31,8 +31,4 @@ class SemGuard instanceof Specific::Guard {
   final SemExpr asExpr() { result = Specific::getGuardAsExpr(this) }
 }
 
-predicate semImplies_v2(SemGuard g1, boolean b1, SemGuard g2, boolean b2) {
-  Specific::implies_v2(g1, b1, g2, b2)
-}
-
 SemGuard semGetComparisonGuard(SemRelationalExpr e) { result = Specific::comparisonGuard(e) }
diff --git a/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisImpl.qll b/cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisImpl.qll
@@ -77,8 +77,6 @@ module Sem implements Semantic<SemLocation> {
 
   class Guard = SemGuard;
 
-  predicate implies_v2 = semImplies_v2/4;
-
   class Type = SemType;
 
   class IntegerType = SemIntegerType;
diff --git a/java/ql/lib/semmle/code/java/controlflow/Guards.qll b/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
diff --git a/java/ql/lib/semmle/code/java/dataflow/ModulusAnalysis.qll b/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)
   )
 }
 
diff --git a/java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll b/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 {
diff --git a/java/ql/lib/semmle/code/java/dataflow/RangeUtils.qll b/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;
diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll b/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)
     )
   }
 
diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll b/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)
     )
   }
 }
diff --git a/shared/rangeanalysis/codeql/rangeanalysis/ModulusAnalysis.qll b/shared/rangeanalysis/codeql/rangeanalysis/ModulusAnalysis.qll
@@ -34,7 +34,7 @@ module ModulusAnalysis<
     exists(Sem::Guard guard, boolean testIsTrue |
       hasReadOfVarInlineLate(pos, v) and
       guard = eqFlowCond(v, e, D::fromInt(delta), true, testIsTrue) and
-      guardDirectlyControlsSsaRead(guard, pos, testIsTrue)
+      guardControlsSsaRead(guard, pos, testIsTrue)
     )
   }
 
diff --git a/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll b/shared/rangeanalysis/codeql/rangeanalysis/RangeAnalysis.qll
@@ -181,21 +181,6 @@ signature module Semantic<LocationSig Location> {
      */
     Expr asExpr();
 
-    /**
-     * Holds if the guard directly controls a given basic block. For example in
-     * the following code, the guard `(x > y)` directly controls the block
-     * beneath it:
-     * ```
-     * if (x > y)
-     * {
-     *   Console.WriteLine("x is greater than y");
-     * }
-     * ```
-     * `branch` indicates whether the basic block is entered when the guard
-     * evaluates to `true` or when it evaluates to `false`.
-     */
-    predicate directlyControls(BasicBlock controlled, boolean branch);
-
     /**
      * Holds if this guard is an equality test between `e1` and `e2`. If the
      * test is negated, that is `!=`, then `polarity` is false, otherwise
@@ -204,24 +189,19 @@ signature module Semantic<LocationSig Location> {
     predicate isEquality(Expr e1, Expr e2, boolean polarity);
 
     /**
-     * Holds if there is a branch edge between two basic blocks. For example
-     * in the following C code, there are two branch edges from the basic block
-     * containing the condition `(x > y)` to the beginnings of the true and
-     * false blocks that follow:
-     * ```
-     * if (x > y) {
-     *   printf("x is greater than y\n");
-     * } else {
-     *   printf("x is not greater than y\n");
-     * }
-     * ```
-     * `branch` indicates whether the second basic block is the one entered
-     * when the guard evaluates to `true` or when it evaluates to `false`.
+     * 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 hasBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch);
-  }
+    predicate controlsBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch);
 
-  predicate implies_v2(Guard g1, boolean b1, Guard g2, boolean b2);
+    /**
+     * 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);
+  }
 
   class Type;
 
@@ -670,19 +650,14 @@ module RangeStage<
       delta = D::fromFloat(D::toFloat(d1) + d2 + d3)
     )
     or
-    exists(boolean testIsTrue0 |
-      Sem::implies_v2(result, testIsTrue, boundFlowCond(v, e, delta, upper, testIsTrue0),
-        testIsTrue0)
-    )
-    or
     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
-    // exists a guard `guardEq` such that `v = v2 - d1 + d2`.
+    // guard that tests whether `v2` is bounded by `e + delta - d` and
+    // exists a guard `guardEq` such that `v = v2 + d`.
     exists(Sem::SsaVariable v2, D::Delta oldDelta, float d |
       // equality needs to control guard
-      result.getBasicBlock() = eqSsaCondDirectlyControls(v, v2, d) and
+      result.getBasicBlock() = eqSsaCondControls(v, v2, d) and
       result = boundFlowCond(v2, e, oldDelta, upper, testIsTrue) and
       delta = D::fromFloat(D::toFloat(oldDelta) + d)
     )
@@ -692,13 +667,11 @@ module RangeStage<
    * Gets a basic block in which `v1` equals `v2 + delta`.
    */
   pragma[nomagic]
-  private Sem::BasicBlock eqSsaCondDirectlyControls(
-    Sem::SsaVariable v1, Sem::SsaVariable v2, float delta
-  ) {
+  private Sem::BasicBlock eqSsaCondControls(Sem::SsaVariable v1, Sem::SsaVariable v2, float delta) {
     exists(Sem::Guard guardEq, D::Delta d1, D::Delta d2, boolean eqIsTrue |
       guardEq = eqFlowCond(v1, ssaRead(v2, d1), d2, true, eqIsTrue) and
       delta = D::toFloat(d2) - D::toFloat(d1) and
-      guardEq.directlyControls(result, eqIsTrue)
+      guardEq.controls(result, eqIsTrue)
     )
   }
 
@@ -749,7 +722,7 @@ module RangeStage<
     exists(Sem::Guard guard, boolean testIsTrue |
       pos.hasReadOfVar(v) and
       guard = boundFlowCond(v, e, delta, upper, testIsTrue) and
-      guardDirectlyControlsSsaRead(guard, pos, testIsTrue) and
+      guardControlsSsaRead(guard, pos, testIsTrue) and
       reason = TSemCondReason(guard)
     )
   }
@@ -762,7 +735,7 @@ module RangeStage<
     exists(Sem::Guard guard, boolean testIsTrue |
       pos.hasReadOfVar(v) and
       guard = eqFlowCond(v, e, delta, false, testIsTrue) and
-      guardDirectlyControlsSsaRead(guard, pos, testIsTrue) and
+      guardControlsSsaRead(guard, pos, testIsTrue) and
       reason = TSemCondReason(guard)
     )
   }
diff --git a/shared/rangeanalysis/codeql/rangeanalysis/internal/RangeUtils.qll b/shared/rangeanalysis/codeql/rangeanalysis/internal/RangeUtils.qll

Original file line number	Diff line number	Diff line change
`@@ -264,10 +264,6 @@ module SemanticExprConfig {`
`264`	`264`
`265`	`265`	`Guard comparisonGuard(Expr e) { getSemanticExpr(result) = e }`
`266`	`266`
`267`		`- predicate implies_v2(Guard g1, boolean b1, Guard g2, boolean b2) {`
`268`		`- none() // TODO`
`269`		`- }`
`270`		`-`
`271`	`267`	/** Gets the expression associated with `instr`. */
`272`	`268`	`SemExpr getSemanticExpr(IR::Instruction instr) { result = instr }`
`273`	`269`	`}`
Original file line number	Diff line number	Diff line change
`@@ -18,11 +18,11 @@ class SemGuard instanceof Specific::Guard {`
`18`	`18`	`Specific::equalityGuard(this, e1, e2, polarity)`
`19`	`19`	`}`
`20`	`20`
`21`		`- final predicate directlyControls(SemBasicBlock controlled, boolean branch) {`
	`21`	`+ final predicate controls(SemBasicBlock controlled, boolean branch) {`
`22`	`22`	`Specific::guardDirectlyControlsBlock(this, controlled, branch)`
`23`	`23`	`}`
`24`	`24`
`25`		`- final predicate hasBranchEdge(SemBasicBlock bb1, SemBasicBlock bb2, boolean branch) {`
	`25`	`+ final predicate controlsBranchEdge(SemBasicBlock bb1, SemBasicBlock bb2, boolean branch) {`
`26`	`26`	`Specific::guardHasBranchEdge(this, bb1, bb2, branch)`
`27`	`27`	`}`
`28`	`28`
`@@ -31,8 +31,4 @@ class SemGuard instanceof Specific::Guard {`
`31`	`31`	`final SemExpr asExpr() { result = Specific::getGuardAsExpr(this) }`
`32`	`32`	`}`
`33`	`33`
`34`		`-predicate semImplies_v2(SemGuard g1, boolean b1, SemGuard g2, boolean b2) {`
`35`		`- Specific::implies_v2(g1, b1, g2, b2)`
`36`		`-}`
`37`		`-`
`38`	`34`	`SemGuard semGetComparisonGuard(SemRelationalExpr e) { result = Specific::comparisonGuard(e) }`
Original file line number	Diff line number	Diff line change
`@@ -17,7 +17,7 @@ private predicate valueFlowStepSsa(SsaVariable v, SsaReadPosition pos, Expr e, i`
`17`	`17`	`exists(Guard guard, boolean testIsTrue \|`
`18`	`18`	`pos.hasReadOfVar(v) and`
`19`	`19`	`guard = eqFlowCond(v, e, delta, true, testIsTrue) and`
`20`		`- guardDirectlyControlsSsaRead(guard, pos, testIsTrue)`
	`20`	`+ guardControlsSsaRead(guard, pos, testIsTrue)`
`21`	`21`	`)`
`22`	`22`	`}`
`23`	`23`
Original file line number	Diff line number	Diff line change
`@@ -34,7 +34,7 @@ module ModulusAnalysis<`
`34`	`34`	`exists(Sem::Guard guard, boolean testIsTrue \|`
`35`	`35`	`hasReadOfVarInlineLate(pos, v) and`
`36`	`36`	`guard = eqFlowCond(v, e, D::fromInt(delta), true, testIsTrue) and`
`37`		`- guardDirectlyControlsSsaRead(guard, pos, testIsTrue)`
	`37`	`+ guardControlsSsaRead(guard, pos, testIsTrue)`
`38`	`38`	`)`
`39`	`39`	`}`
`40`	`40`