C++: Copy and adjust Java's correctness argumnt

Instead of a vague reference to a code comment for another language, the
`controlsBlock` predicate now has the whole comment in it directly.

I've adjusted the wording so it should be reasonably correct for C/C++.
As with the other comments in this file, I don't distinguish between the
condition and its block. I think that makes the explanation clearer
without losing any detail we care about.

To make the code fit the wording of the comment, I changed the
`hasBranchEdge/2` predicate into `getBranchSuccessor/1`.

cpp/ql/src/semmle/code/cpp/controlflow/IRGuards.qll

@@ -305,13 +305,13 @@ class IRGuardCondition extends Instruction {
     pred.getASuccessor() = succ and
     controls(pred, testIsTrue)
     or
-    hasBranchEdge(succ, testIsTrue) and
+    succ = getBranchSuccessor(testIsTrue) and
     branch.getCondition() = this and
     branch.getBlock() = pred
   }
 
   /**
-   * Holds if `branch` jumps directly to `succ` when this condition is `testIsTrue`.
+   * Gets the block to which `branch` jumps directly when this condition is `testIsTrue`.
    *
    * This predicate is intended to help with situations in which an inference can only be made
    * based on an edge between a block with multiple successors and a block with multiple
@@ -325,14 +325,14 @@ class IRGuardCondition extends Instruction {
    * return x;
    * ```
    */
-  private predicate hasBranchEdge(IRBlock succ, boolean testIsTrue) {
+  private IRBlock getBranchSuccessor(boolean testIsTrue) {
     branch.getCondition() = this and
     (
       testIsTrue = true and
-      succ.getFirstInstruction() = branch.getTrueSuccessor()
+      result.getFirstInstruction() = branch.getTrueSuccessor()
       or
       testIsTrue = false and
-      succ.getFirstInstruction() = branch.getFalseSuccessor()
+      result.getFirstInstruction() = branch.getFalseSuccessor()
     )
   }
 
@@ -406,11 +406,46 @@ class IRGuardCondition extends Instruction {
    */
   private predicate controlsBlock(IRBlock controlled, boolean testIsTrue) {
     not isUnreachedBlock(controlled) and
-    // The following implementation is ported from `controls` in Java's
-    // `Guards.qll`. See that file (at 398678a28) for further explanation and
-    // correctness arguments.
+    //
+    // For this block to control the block `controlled` with `testIsTrue` the
+    // following must hold: Execution must have passed through the test; that
+    // is, `this` must strictly dominate `controlled`. Execution must have
+    // passed through the `testIsTrue` edge leaving `this`.
+    //
+    // Although "passed through the true edge" implies that
+    // `getBranchSuccessor(true)` dominates `controlled`, the reverse is not
+    // true, as flow may have passed through another edge to get to
+    // `getBranchSuccessor(true)`, so we need to assert that
+    // `getBranchSuccessor(true)` dominates `controlled` *and* that all
+    // predecessors of `getBranchSuccessor(true)` are either `this` or
+    // dominated by `getBranchSuccessor(true)`.
+    //
+    // For example, in the following snippet:
+    //
+    //     if (x)
+    //       controlled;
+    //     false_successor;
+    //     uncontrolled;
+    //
+    // `false_successor` dominates `uncontrolled`, but not all of its
+    // predecessors are `this` (`if (x)`) or dominated by itself. Whereas in
+    // the following code:
+    //
+    //     if (x)
+    //       while (controlled)
+    //         also_controlled;
+    //     false_successor;
+    //     uncontrolled;
+    //
+    // the block `while (controlled)` is controlled because all of its
+    // predecessors are `this` (`if (x)`) or (in the case of `also_controlled`)
+    // dominated by itself.
+    //
+    // The additional constraint on the predecessors of the test successor implies
+    // that `this` strictly dominates `controlled` so that isn't necessary to check
+    // directly.
     exists(IRBlock succ |
-      this.hasBranchEdge(succ, testIsTrue) and
+      succ = this.getBranchSuccessor(testIsTrue) and
       this.hasDominatingEdgeTo(succ) and
       succ.dominates(controlled)
     )