@@ -87,148 +87,20 @@ class ControlFlowElement extends ExprOrStmtParent, @control_flow_element {
8787 result .getAControlFlowNode ( )
8888 }
8989
90- pragma [ noinline]
91- private predicate immediatelyControlsBlockSplit0 (
92- ConditionBlock cb , BasicBlock succ , ConditionalSuccessor s
93- ) {
94- // Only calculate dominance by explicit recursion for split nodes;
95- // all other nodes can use regular CFG dominance
96- this instanceof Impl:: SplitAstNode and
97- cb .getLastNode ( ) = this .getAControlFlowNode ( ) and
98- succ = cb .getASuccessor ( s )
99- }
100-
101- pragma [ noinline]
102- private predicate immediatelyControlsBlockSplit1 (
103- ConditionBlock cb , BasicBlock succ , ConditionalSuccessor s , BasicBlock pred , SuccessorType t
104- ) {
105- this .immediatelyControlsBlockSplit0 ( cb , succ , s ) and
106- pred = succ .getAPredecessorByType ( t ) and
107- pred != cb
108- }
109-
110- pragma [ noinline]
111- private predicate immediatelyControlsBlockSplit2 (
112- ConditionBlock cb , BasicBlock succ , ConditionalSuccessor s , BasicBlock pred , SuccessorType t
113- ) {
114- this .immediatelyControlsBlockSplit1 ( cb , succ , s , pred , t ) and
115- (
116- succ .dominates ( pred )
117- or
118- // `pred` might be another split of this element
119- pred .getLastNode ( ) .getAstNode ( ) = this and
120- t = s
121- )
122- }
123-
12490 /**
125- * Holds if basic block `succ` is immediately controlled by this control flow
126- * element with conditional value `s`. That is, `succ` can only be reached from
127- * the callable entry point by going via the `s` edge out of *some* basic block
128- * `pred` ending with this element, and `pred` is an immediate predecessor
129- * of `succ`.
130- *
131- * Moreover, this control flow element corresponds to multiple control flow nodes,
132- * which is why
133- *
134- * ```ql
135- * exists(ConditionBlock cb |
136- * cb.getLastNode() = this.getAControlFlowNode() |
137- * cb.immediatelyControls(succ, s)
138- * )
139- * ```
91+ * DEPRECATED: Use `Guard` class instead.
14092 *
141- * does not work.
142- *
143- * `cb` records all of the possible condition blocks for this control flow element
144- * that a path from the callable entry point to `succ` may go through.
145- */
146- pragma [ nomagic]
147- private predicate immediatelyControlsBlockSplit (
148- BasicBlock succ , ConditionalSuccessor s , ConditionBlock cb
149- ) {
150- this .immediatelyControlsBlockSplit0 ( cb , succ , s ) and
151- forall ( BasicBlock pred , SuccessorType t |
152- this .immediatelyControlsBlockSplit1 ( cb , succ , s , pred , t )
153- |
154- this .immediatelyControlsBlockSplit2 ( cb , succ , s , pred , t )
155- )
156- }
157-
158- pragma [ noinline]
159- private predicate controlsJoinBlockPredecessor (
160- JoinBlock controlled , ConditionalSuccessor s , int i , ConditionBlock cb
161- ) {
162- this .controlsBlockSplit ( controlled .getJoinBlockPredecessor ( i ) , s , cb )
163- }
164-
165- private predicate controlsJoinBlockSplit ( JoinBlock controlled , ConditionalSuccessor s , int i ) {
166- i = - 1 and
167- this .controlsJoinBlockPredecessor ( controlled , s , _, _)
168- or
169- this .controlsJoinBlockSplit ( controlled , s , i - 1 ) and
170- (
171- this .controlsJoinBlockPredecessor ( controlled , s , i , _)
172- or
173- controlled .dominates ( controlled .getJoinBlockPredecessor ( i ) )
174- )
175- }
176-
177- cached
178- private predicate controlsBlockSplit (
179- BasicBlock controlled , ConditionalSuccessor s , ConditionBlock cb
180- ) {
181- Stages:: GuardsStage:: forceCachingInSameStage ( ) and
182- this .immediatelyControlsBlockSplit ( controlled , s , cb )
183- or
184- // Equivalent with
185- //
186- // ```ql
187- // exists(JoinBlockPredecessor pred | pred = controlled.getAPredecessor() |
188- // this.controlsBlockSplit(pred, s)
189- // ) and
190- // forall(JoinBlockPredecessor pred | pred = controlled.getAPredecessor() |
191- // this.controlsBlockSplit(pred, s)
192- // or
193- // controlled.dominates(pred)
194- // )
195- // ```
196- //
197- // but uses no universal recursion for better performance.
198- exists ( int last |
199- last = max ( int i | exists ( controlled .( JoinBlock ) .getJoinBlockPredecessor ( i ) ) )
200- |
201- this .controlsJoinBlockSplit ( controlled , s , last )
202- ) and
203- this .controlsJoinBlockPredecessor ( controlled , s , _, cb )
204- or
205- not controlled instanceof JoinBlock and
206- this .controlsBlockSplit ( controlled .getAPredecessor ( ) , s , cb )
207- }
208-
209- /**
21093 * Holds if basic block `controlled` is controlled by this control flow element
21194 * with conditional value `s`. That is, `controlled` can only be reached from
21295 * the callable entry point by going via the `s` edge out of *some* basic block
21396 * ending with this element.
21497 *
215- * This predicate is different from
216- *
217- * ```ql
218- * exists(ConditionBlock cb |
219- * cb.getLastNode() = this.getAControlFlowNode() |
220- * cb.controls(controlled, s)
221- * )
222- * ```
223- *
224- * as control flow splitting is taken into account.
225- *
22698 * `cb` records all of the possible condition blocks for this control flow element
22799 * that a path from the callable entry point to `controlled` may go through.
228100 */
229- predicate controlsBlock ( BasicBlock controlled , ConditionalSuccessor s , ConditionBlock cb ) {
230- this . controlsBlockSplit ( controlled , s , cb )
231- or
101+ deprecated predicate controlsBlock (
102+ BasicBlock controlled , ConditionalSuccessor s , ConditionBlock cb
103+ ) {
232104 cb .getLastNode ( ) = this .getAControlFlowNode ( ) and
233105 cb .edgeDominates ( controlled , s )
234106 }
0 commit comments