@@ -13,6 +13,7 @@ import semmle.code.cpp.ir.IR
13
13
* has the AST for the `Function` itself, which tends to confuse mapping between the AST `BasicBlock`
14
14
* and the `IRBlock`.
15
15
*/
16
+ pragma [ noinline]
16
17
private predicate isUnreachedBlock ( IRBlock block ) {
17
18
block .getFirstInstruction ( ) instanceof UnreachedInstruction
18
19
}
@@ -304,13 +305,13 @@ class IRGuardCondition extends Instruction {
304
305
pred .getASuccessor ( ) = succ and
305
306
controls ( pred , testIsTrue )
306
307
or
307
- hasBranchEdge ( succ , testIsTrue ) and
308
+ succ = getBranchSuccessor ( testIsTrue ) and
308
309
branch .getCondition ( ) = this and
309
310
branch .getBlock ( ) = pred
310
311
}
311
312
312
313
/**
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`.
314
315
*
315
316
* This predicate is intended to help with situations in which an inference can only be made
316
317
* based on an edge between a block with multiple successors and a block with multiple
@@ -324,14 +325,14 @@ class IRGuardCondition extends Instruction {
324
325
* return x;
325
326
* ```
326
327
*/
327
- private predicate hasBranchEdge ( IRBlock succ , boolean testIsTrue ) {
328
+ private IRBlock getBranchSuccessor ( boolean testIsTrue ) {
328
329
branch .getCondition ( ) = this and
329
330
(
330
331
testIsTrue = true and
331
- succ .getFirstInstruction ( ) = branch .getTrueSuccessor ( )
332
+ result .getFirstInstruction ( ) = branch .getTrueSuccessor ( )
332
333
or
333
334
testIsTrue = false and
334
- succ .getFirstInstruction ( ) = branch .getFalseSuccessor ( )
335
+ result .getFirstInstruction ( ) = branch .getFalseSuccessor ( )
335
336
)
336
337
}
337
338
@@ -405,20 +406,78 @@ class IRGuardCondition extends Instruction {
405
406
*/
406
407
private predicate controlsBlock ( IRBlock controlled , boolean testIsTrue ) {
407
408
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 )
411
469
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 ( )
419
475
)
420
476
)
421
477
}
478
+
479
+ pragma [ noinline]
480
+ private IRBlock getBranchBlock ( ) { result = branch .getBlock ( ) }
422
481
}
423
482
424
483
private ConditionalBranchInstruction get_branch_for_condition ( Instruction guard ) {
0 commit comments