@@ -309,6 +309,17 @@ private module Cached {
309
309
jbp order by JoinBlockPredecessors:: getId ( jbp ) , JoinBlockPredecessors:: getSplitString ( jbp )
310
310
)
311
311
}
312
+
313
+ cached
314
+ predicate immediatelyControls ( ConditionBlock cb , BasicBlock succ , BooleanSuccessor s ) {
315
+ succ = cb .getASuccessor ( s ) and
316
+ forall ( BasicBlock pred | pred = succ .getAPredecessor ( ) and pred != cb | succ .dominates ( pred ) )
317
+ }
318
+
319
+ cached
320
+ predicate controls ( ConditionBlock cb , BasicBlock controlled , BooleanSuccessor s ) {
321
+ exists ( BasicBlock succ | cb .immediatelyControls ( succ , s ) | succ .dominates ( controlled ) )
322
+ }
312
323
}
313
324
314
325
private import Cached
@@ -395,18 +406,14 @@ class ConditionBlock extends BasicBlock {
395
406
* successor of this block, and `succ` can only be reached from
396
407
* the callable entry point by going via the `s` edge out of this basic block.
397
408
*/
398
- pragma [ nomagic]
399
409
predicate immediatelyControls ( BasicBlock succ , BooleanSuccessor s ) {
400
- succ = this .getASuccessor ( s ) and
401
- forall ( BasicBlock pred | pred = succ .getAPredecessor ( ) and pred != this | succ .dominates ( pred ) )
410
+ immediatelyControls ( this , succ , s )
402
411
}
403
412
404
413
/**
405
414
* Holds if basic block `controlled` is controlled by this basic block with
406
415
* conditional value `s`. That is, `controlled` can only be reached from
407
416
* the callable entry point by going via the `s` edge out of this basic block.
408
417
*/
409
- predicate controls ( BasicBlock controlled , BooleanSuccessor s ) {
410
- exists ( BasicBlock succ | this .immediatelyControls ( succ , s ) | succ .dominates ( controlled ) )
411
- }
418
+ predicate controls ( BasicBlock controlled , BooleanSuccessor s ) { controls ( this , controlled , s ) }
412
419
}
0 commit comments