@@ -101,46 +101,56 @@ class ControlFlowElement extends ExprOrStmtParent, @control_flow_element {
101101 |
102102 succ .dominates ( pred )
103103 or
104- // `pred` might be another split of `cfe`
104+ // `pred` might be another split of this element
105105 pred .getLastNode ( ) .getElement ( ) = this and
106- pred .getASuccessorByType ( t ) = succ and
107106 t = s
108107 )
109108 )
110109 }
111110
112- pragma [ nomagic]
113- private JoinBlockPredecessor getAPossiblyControlledPredecessor (
114- JoinBlock controlled , ConditionalSuccessor s
115- ) {
116- exists ( BasicBlock mid | this .immediatelyControlsBlockSplit ( mid , s ) |
117- result = mid .getASuccessor * ( )
118- ) and
119- result .getASuccessor ( ) = controlled and
120- not controlled .dominates ( result )
111+ pragma [ noinline]
112+ private predicate controlsJoinBlockPredecessor ( JoinBlock controlled , ConditionalSuccessor s , int i ) {
113+ this .controlsBlockSplit ( controlled .getJoinBlockPredecessor ( i ) , s )
121114 }
122115
123- pragma [ nomagic]
124- private predicate isPossiblyControlledJoinBlock ( JoinBlock controlled , ConditionalSuccessor s ) {
125- exists ( this .getAPossiblyControlledPredecessor ( controlled , s ) ) and
126- forall ( BasicBlock pred | pred = controlled .getAPredecessor ( ) |
127- pred = this .getAPossiblyControlledPredecessor ( controlled , s )
116+ private predicate controlsJoinBlockSplit ( JoinBlock controlled , ConditionalSuccessor s , int i ) {
117+ i = - 1 and
118+ this .controlsJoinBlockPredecessor ( controlled , s , _)
119+ or
120+ this .controlsJoinBlockSplit ( controlled , s , i - 1 ) and
121+ (
122+ this .controlsJoinBlockPredecessor ( controlled , s , i )
128123 or
129- controlled .dominates ( pred )
124+ controlled .dominates ( controlled . getJoinBlockPredecessor ( i ) )
130125 )
131126 }
132127
133128 cached
134129 private predicate controlsBlockSplit ( BasicBlock controlled , ConditionalSuccessor s ) {
135130 this .immediatelyControlsBlockSplit ( controlled , s )
136131 or
137- if controlled instanceof JoinBlock
138- then
139- this .isPossiblyControlledJoinBlock ( controlled , s ) and
140- forall ( BasicBlock pred | pred = this .getAPossiblyControlledPredecessor ( controlled , s ) |
141- this .controlsBlock ( pred , s )
142- )
143- else this .controlsBlockSplit ( controlled .getAPredecessor ( ) , s )
132+ // Equivalent with
133+ //
134+ // ```
135+ // exists(JoinBlockPredecessor pred | pred = controlled.getAPredecessor() |
136+ // this.controlsBlockSplit(pred, s)
137+ // ) and
138+ // forall(JoinBlockPredecessor pred | pred = controlled.getAPredecessor() |
139+ // this.controlsBlockSplit(pred, s)
140+ // or
141+ // controlled.dominates(pred)
142+ // )
143+ // ```
144+ //
145+ // but uses no universal recursion for better performance.
146+ exists ( int last |
147+ last = max ( int i | exists ( controlled .( JoinBlock ) .getJoinBlockPredecessor ( i ) ) )
148+ |
149+ this .controlsJoinBlockSplit ( controlled , s , last )
150+ )
151+ or
152+ not controlled instanceof JoinBlock and
153+ this .controlsBlockSplit ( controlled .getAPredecessor ( ) , s )
144154 }
145155
146156 /**
0 commit comments