@@ -309,6 +309,17 @@ private module Cached {
309309 jbp order by JoinBlockPredecessors:: getId ( jbp ) , JoinBlockPredecessors:: getSplitString ( jbp )
310310 )
311311 }
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+ }
312323}
313324
314325private import Cached
@@ -395,18 +406,14 @@ class ConditionBlock extends BasicBlock {
395406 * successor of this block, and `succ` can only be reached from
396407 * the callable entry point by going via the `s` edge out of this basic block.
397408 */
398- pragma [ nomagic]
399409 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 )
402411 }
403412
404413 /**
405414 * Holds if basic block `controlled` is controlled by this basic block with
406415 * conditional value `s`. That is, `controlled` can only be reached from
407416 * the callable entry point by going via the `s` edge out of this basic block.
408417 */
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 ) }
412419}
0 commit comments