Merge pull request #19571 from aschackmull/rangeanalysis/guards

Rangeanalysis: Simplify Guards integration.

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)
     )
   }
 

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)
     )
   }

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

@@ -52,10 +52,6 @@ module MakeUtils<LocationSig Location, Semantic<Location> Lang, DeltaSig D> {
       (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)
-    )
   }
 
   /**
@@ -173,29 +169,17 @@ module MakeUtils<LocationSig Location, Semantic<Location> Lang, DeltaSig D> {
     override string toString() { result = "edge" }
   }
 
-  /**
-   * 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 |
-      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)
     )
   }