SSA: Distinguish between has and controls branch edge.

cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowPrivate.qll

@@ -1903,6 +1903,10 @@ module IteratorFlow {
     predicate allowFlowIntoUncertainDef(IteratorSsa::UncertainWriteDefinition def) { any() }
 
     class Guard extends Void {
+      predicate hasBranchEdge(SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch) {
+        none()
+      }
+
       predicate controlsBranchEdge(
         SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch
       ) {

cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaInternals.qll

@@ -991,13 +991,17 @@ private module DataFlowIntegrationInput implements SsaImpl::DataFlowIntegrationI
   class Guard instanceof IRGuards::IRGuardCondition {
     string toString() { result = super.toString() }
 
-    predicate controlsBranchEdge(SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch) {
+    predicate hasBranchEdge(SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch) {
       exists(EdgeKind kind |
         super.getBlock() = bb1 and
         kind = getConditionalEdge(branch) and
         bb1.getSuccessor(kind) = bb2
       )
     }
+
+    predicate controlsBranchEdge(SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch) {
+      this.hasBranchEdge(bb1, bb2, branch)
+    }
   }
 
   predicate guardDirectlyControlsBlock(Guard guard, SsaInput::BasicBlock bb, boolean branch) {

csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll

@@ -1044,17 +1044,25 @@ private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInpu
 
   class Guard extends Guards::Guard {
     /**
-     * Holds if the control flow branching from `bb1` is dependent on this guard,
+     * Holds if the evaluation of this guard to `branch` corresponds to the edge
-     * and that the edge from `bb1` to `bb2` corresponds to the evaluation of this
+     * from `bb1` to `bb2`.
-     * guard to `branch`.
      */
-    predicate controlsBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) {
+    predicate hasBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) {
       exists(ControlFlow::SuccessorTypes::ConditionalSuccessor s |
         this.getAControlFlowNode() = bb1.getLastNode() and
         bb2 = bb1.getASuccessorByType(s) and
         s.getValue() = branch
       )
     }
+
+    /**
+     * 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) {
+      this.hasBranchEdge(bb1, bb2, branch)
+    }
   }
 
   /** Holds if the guard `guard` controls block `bb` upon evaluating to `branch`. */

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

@@ -272,6 +272,15 @@ class Guard extends ExprParent {
     preconditionControls(this, controlled, branch)
   }
 
+  /**
+   * 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_v3(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
@@ -351,6 +360,18 @@ private predicate guardControls_v3(Guard guard, BasicBlock controlled, boolean b
   )
 }
 
+pragma[nomagic]
+private predicate guardControlsBranchEdge_v3(
+  Guard guard, BasicBlock bb1, BasicBlock bb2, boolean branch
+) {
+  guard.hasBranchEdge(bb1, bb2, branch)
+  or
+  exists(Guard g, boolean b |
+    guardControlsBranchEdge_v3(g, bb1, bb2, b) and
+    implies_v3(g, b, guard, 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/internal/SsaImpl.qll

@@ -654,16 +654,7 @@ private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInpu
     def instanceof SsaUncertainImplicitUpdate
   }
 
-  class Guard extends Guards::Guard {
+  class Guard = Guards::Guard;
-    /**
-     * Holds if the control flow branching from `bb1` is dependent on this guard,
-     * and that the edge from `bb1` to `bb2` corresponds to the evaluation of this
-     * guard to `branch`.
-     */
-    predicate controlsBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) {
-      super.hasBranchEdge(bb1, bb2, branch)
-    }
-  }
 
   /** Holds if the guard `guard` directly controls block `bb` upon evaluating to `branch`. */
   predicate guardDirectlyControlsBlock(Guard guard, BasicBlock bb, boolean branch) {

javascript/ql/lib/semmle/javascript/dataflow/internal/sharedlib/Ssa.qll

@@ -75,11 +75,10 @@ module SsaDataflowInput implements DataFlowIntegrationInputSig {
     Guard() { this = any(js::ConditionGuardNode g).getTest() }
 
     /**
-     * Holds if the control flow branching from `bb1` is dependent on this guard,
+     * Holds if the evaluation of this guard to `branch` corresponds to the edge
-     * and that the edge from `bb1` to `bb2` corresponds to the evaluation of this
+     * from `bb1` to `bb2`.
-     * guard to `branch`.
      */
-    predicate controlsBranchEdge(js::BasicBlock bb1, js::BasicBlock bb2, boolean branch) {
+    predicate hasBranchEdge(js::BasicBlock bb1, js::BasicBlock bb2, boolean branch) {
       exists(js::ConditionGuardNode g |
         g.getTest() = this and
         bb1 = this.getBasicBlock() and
@@ -87,6 +86,15 @@ module SsaDataflowInput implements DataFlowIntegrationInputSig {
         branch = g.getOutcome()
       )
     }
+
+    /**
+     * 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(js::BasicBlock bb1, js::BasicBlock bb2, boolean branch) {
+      this.hasBranchEdge(bb1, bb2, branch)
+    }
   }
 
   pragma[inline]

ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll

@@ -484,17 +484,25 @@ private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInpu
 
   class Guard extends Cfg::CfgNodes::AstCfgNode {
     /**
-     * Holds if the control flow branching from `bb1` is dependent on this guard,
+     * Holds if the evaluation of this guard to `branch` corresponds to the edge
-     * and that the edge from `bb1` to `bb2` corresponds to the evaluation of this
+     * from `bb1` to `bb2`.
-     * guard to `branch`.
      */
-    predicate controlsBranchEdge(SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch) {
+    predicate hasBranchEdge(SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch) {
       exists(Cfg::SuccessorTypes::ConditionalSuccessor s |
         this.getBasicBlock() = bb1 and
         bb2 = bb1.getASuccessor(s) and
         s.getValue() = branch
       )
     }
+
+    /**
+     * 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(SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch) {
+      this.hasBranchEdge(bb1, bb2, branch)
+    }
   }
 
   /** Holds if the guard `guard` controls block `bb` upon evaluating to `branch`. */

rust/ql/lib/codeql/rust/dataflow/internal/SsaImpl.qll

@@ -363,17 +363,25 @@ private module DataFlowIntegrationInput implements Impl::DataFlowIntegrationInpu
 
   class Guard extends CfgNodes::AstCfgNode {
     /**
-     * Holds if the control flow branching from `bb1` is dependent on this guard,
+     * Holds if the evaluation of this guard to `branch` corresponds to the edge
-     * and that the edge from `bb1` to `bb2` corresponds to the evaluation of this
+     * from `bb1` to `bb2`.
-     * guard to `branch`.
      */
-    predicate controlsBranchEdge(SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch) {
+    predicate hasBranchEdge(SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch) {
       exists(Cfg::ConditionalSuccessor s |
         this = bb1.getANode() and
         bb2 = bb1.getASuccessor(s) and
         s.getValue() = branch
       )
     }
+
+    /**
+     * 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(SsaInput::BasicBlock bb1, SsaInput::BasicBlock bb2, boolean branch) {
+      this.hasBranchEdge(bb1, bb2, branch)
+    }
   }
 
   /** Holds if the guard `guard` controls block `bb` upon evaluating to `branch`. */

shared/dataflow/codeql/dataflow/VariableCapture.qll

@@ -732,6 +732,8 @@ module Flow<LocationSig Location, InputSig<Location> Input> implements OutputSig
     }
 
     class Guard extends Void {
+      predicate hasBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) { none() }
+
       predicate controlsBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch) { none() }
     }
 

shared/ssa/codeql/ssa/Ssa.qll

@@ -1570,9 +1570,15 @@ module Make<LocationSig Location, InputSig<Location> Input> {
       string toString();
 
       /**
-       * Holds if the control flow branching from `bb1` is dependent on this guard,
+       * Holds if the evaluation of this guard to `branch` corresponds to the edge
-       * and that the edge from `bb1` to `bb2` corresponds to the evaluation of this
+       * from `bb1` to `bb2`.
-       * guard to `branch`.
+       */
+      predicate hasBranchEdge(BasicBlock bb1, BasicBlock bb2, boolean branch);
+
+      /**
+       * 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);
     }
@@ -1667,7 +1673,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
       (
         // The input node is relevant either if it sits directly on a branch
         // edge for a guard,
-        exists(DfInput::Guard g | g.controlsBranchEdge(input, phi.getBasicBlock(), _))
+        exists(DfInput::Guard g | g.hasBranchEdge(input, phi.getBasicBlock(), _))
         or
         // or if the unique predecessor is not an equivalent substitute in
         // terms of being controlled by the same guards.