@@ -75,6 +75,40 @@ class ControlFlowElement extends ExprOrStmtParent, @control_flow_element {
7575 getAControlFlowNode ( ) .getBasicBlock ( ) .getASuccessor + ( ) .getANode ( ) = result .getAControlFlowNode ( )
7676 }
7777
78+ pragma [ noinline]
79+ private predicate immediatelyControlsBlockSplit0 (
80+ ConditionBlock cb , BasicBlock succ , ConditionalSuccessor s
81+ ) {
82+ // Only calculate dominance by explicit recursion for split nodes;
83+ // all other nodes can use regular CFG dominance
84+ this instanceof ControlFlow:: Internal:: SplitControlFlowElement and
85+ cb .getLastNode ( ) = this .getAControlFlowNode ( ) and
86+ succ = cb .getASuccessorByType ( s )
87+ }
88+
89+ pragma [ noinline]
90+ private predicate immediatelyControlsBlockSplit1 (
91+ ConditionBlock cb , BasicBlock succ , ConditionalSuccessor s , BasicBlock pred , SuccessorType t
92+ ) {
93+ this .immediatelyControlsBlockSplit0 ( cb , succ , s ) and
94+ pred = succ .getAPredecessorByType ( t ) and
95+ pred != cb
96+ }
97+
98+ pragma [ noinline]
99+ private predicate immediatelyControlsBlockSplit2 (
100+ ConditionBlock cb , BasicBlock succ , ConditionalSuccessor s , BasicBlock pred , SuccessorType t
101+ ) {
102+ this .immediatelyControlsBlockSplit1 ( cb , succ , s , pred , t ) and
103+ (
104+ succ .dominates ( pred )
105+ or
106+ // `pred` might be another split of this element
107+ pred .getLastNode ( ) .getElement ( ) = this and
108+ t = s
109+ )
110+ }
111+
78112 /**
79113 * Holds if basic block `succ` is immediately controlled by this control flow
80114 * element with conditional value `s`. That is, `succ` can only be reached from
@@ -96,19 +130,11 @@ class ControlFlowElement extends ExprOrStmtParent, @control_flow_element {
96130 */
97131 pragma [ nomagic]
98132 private predicate immediatelyControlsBlockSplit ( BasicBlock succ , ConditionalSuccessor s ) {
99- // Only calculate dominance by explicit recursion for split nodes;
100- // all other nodes can use regular CFG dominance
101- this instanceof ControlFlow:: Internal:: SplitControlFlowElement and
102- exists ( ConditionBlock cb | cb .getLastNode ( ) = this .getAControlFlowNode ( ) |
103- succ = cb .getASuccessorByType ( s ) and
133+ exists ( ConditionBlock cb | this .immediatelyControlsBlockSplit0 ( cb , succ , s ) |
104134 forall ( BasicBlock pred , SuccessorType t |
105- pred = succ . getAPredecessorByType ( t ) and pred != cb
135+ this . immediatelyControlsBlockSplit1 ( cb , succ , s , pred , t )
106136 |
107- succ .dominates ( pred )
108- or
109- // `pred` might be another split of this element
110- pred .getLastNode ( ) .getElement ( ) = this and
111- t = s
137+ this .immediatelyControlsBlockSplit2 ( cb , succ , s , pred , t )
112138 )
113139 )
114140 }
0 commit comments