@@ -13,6 +13,7 @@ import semmle.code.cpp.ir.IR
1313 * has the AST for the `Function` itself, which tends to confuse mapping between the AST `BasicBlock`
1414 * and the `IRBlock`.
1515 */
16+ pragma [ noinline]
1617private predicate isUnreachedBlock ( IRBlock block ) {
1718 block .getFirstInstruction ( ) instanceof UnreachedInstruction
1819}
@@ -304,13 +305,13 @@ class IRGuardCondition extends Instruction {
304305 pred .getASuccessor ( ) = succ and
305306 controls ( pred , testIsTrue )
306307 or
307- hasBranchEdge ( succ , testIsTrue ) and
308+ succ = getBranchSuccessor ( testIsTrue ) and
308309 branch .getCondition ( ) = this and
309310 branch .getBlock ( ) = pred
310311 }
311312
312313 /**
313- * Holds if `branch` jumps directly to `succ` when this condition is `testIsTrue`.
314+ * Gets the block to which `branch` jumps directly when this condition is `testIsTrue`.
314315 *
315316 * This predicate is intended to help with situations in which an inference can only be made
316317 * based on an edge between a block with multiple successors and a block with multiple
@@ -324,14 +325,14 @@ class IRGuardCondition extends Instruction {
324325 * return x;
325326 * ```
326327 */
327- private predicate hasBranchEdge ( IRBlock succ , boolean testIsTrue ) {
328+ private IRBlock getBranchSuccessor ( boolean testIsTrue ) {
328329 branch .getCondition ( ) = this and
329330 (
330331 testIsTrue = true and
331- succ .getFirstInstruction ( ) = branch .getTrueSuccessor ( )
332+ result .getFirstInstruction ( ) = branch .getTrueSuccessor ( )
332333 or
333334 testIsTrue = false and
334- succ .getFirstInstruction ( ) = branch .getFalseSuccessor ( )
335+ result .getFirstInstruction ( ) = branch .getFalseSuccessor ( )
335336 )
336337 }
337338
@@ -405,20 +406,78 @@ class IRGuardCondition extends Instruction {
405406 */
406407 private predicate controlsBlock ( IRBlock controlled , boolean testIsTrue ) {
407408 not isUnreachedBlock ( controlled ) and
408- exists ( IRBlock branchBlock | branchBlock .getAnInstruction ( ) = branch |
409- exists ( IRBlock succ |
410- testIsTrue = true and succ .getFirstInstruction ( ) = branch .getTrueSuccessor ( )
409+ //
410+ // For this block to control the block `controlled` with `testIsTrue` the
411+ // following must hold: Execution must have passed through the test; that
412+ // is, `this` must strictly dominate `controlled`. Execution must have
413+ // passed through the `testIsTrue` edge leaving `this`.
414+ //
415+ // Although "passed through the true edge" implies that
416+ // `getBranchSuccessor(true)` dominates `controlled`, the reverse is not
417+ // true, as flow may have passed through another edge to get to
418+ // `getBranchSuccessor(true)`, so we need to assert that
419+ // `getBranchSuccessor(true)` dominates `controlled` *and* that all
420+ // predecessors of `getBranchSuccessor(true)` are either `this` or
421+ // dominated by `getBranchSuccessor(true)`.
422+ //
423+ // For example, in the following snippet:
424+ //
425+ // if (x)
426+ // controlled;
427+ // false_successor;
428+ // uncontrolled;
429+ //
430+ // `false_successor` dominates `uncontrolled`, but not all of its
431+ // predecessors are `this` (`if (x)`) or dominated by itself. Whereas in
432+ // the following code:
433+ //
434+ // if (x)
435+ // while (controlled)
436+ // also_controlled;
437+ // false_successor;
438+ // uncontrolled;
439+ //
440+ // the block `while (controlled)` is controlled because all of its
441+ // predecessors are `this` (`if (x)`) or (in the case of `also_controlled`)
442+ // dominated by itself.
443+ //
444+ // The additional constraint on the predecessors of the test successor implies
445+ // that `this` strictly dominates `controlled` so that isn't necessary to check
446+ // directly.
447+ exists ( IRBlock succ |
448+ succ = this .getBranchSuccessor ( testIsTrue ) and
449+ this .hasDominatingEdgeTo ( succ ) and
450+ succ .dominates ( controlled )
451+ )
452+ }
453+
454+ /**
455+ * Holds if `(this, succ)` is an edge that dominates `succ`, that is, all other
456+ * predecessors of `succ` are dominated by `succ`. This implies that `this` is the
457+ * immediate dominator of `succ`.
458+ *
459+ * This is a necessary and sufficient condition for an edge to dominate anything,
460+ * and in particular `bb1.hasDominatingEdgeTo(bb2) and bb2.dominates(bb3)` means
461+ * that the edge `(bb1, bb2)` dominates `bb3`.
462+ */
463+ private predicate hasDominatingEdgeTo ( IRBlock succ ) {
464+ exists ( IRBlock branchBlock | branchBlock = this .getBranchBlock ( ) |
465+ branchBlock .immediatelyDominates ( succ ) and
466+ branchBlock .getASuccessor ( ) = succ and
467+ forall ( IRBlock pred | pred = succ .getAPredecessor ( ) and pred != branchBlock |
468+ succ .dominates ( pred )
411469 or
412- testIsTrue = false and succ .getFirstInstruction ( ) = branch .getFalseSuccessor ( )
413- |
414- branch .getCondition ( ) = this and
415- succ .dominates ( controlled ) and
416- forall ( IRBlock pred | pred .getASuccessor ( ) = succ |
417- pred = branchBlock or succ .dominates ( pred ) or not pred .isReachableFromFunctionEntry ( )
418- )
470+ // An unreachable `pred` is vacuously dominated by `succ` since all
471+ // paths from the entry to `pred` go through `succ`. Such vacuous
472+ // dominance is not included in the `dominates` predicate since that
473+ // could cause quadratic blow-up.
474+ not pred .isReachableFromFunctionEntry ( )
419475 )
420476 )
421477 }
478+
479+ pragma [ noinline]
480+ private IRBlock getBranchBlock ( ) { result = branch .getBlock ( ) }
422481}
423482
424483private ConditionalBranchInstruction get_branch_for_condition ( Instruction guard ) {
0 commit comments