@@ -80,7 +80,6 @@ module Make<LocationSig Location, InputSig<Location> Input> {
80
80
BasicBlock getAPredecessor ( SuccessorType t ) { result .getASuccessor ( t ) = this }
81
81
82
82
/** Gets the control flow node at a specific (zero-indexed) position in this basic block. */
83
- cached
84
83
Node getNode ( int pos ) { bbIndex ( this .getFirstNode ( ) , result , pos ) }
85
84
86
85
/** Gets a control flow node in this basic block. */
@@ -152,6 +151,68 @@ module Make<LocationSig Location, InputSig<Location> Input> {
152
151
*/
153
152
BasicBlock getImmediateDominator ( ) { bbIDominates ( result , this ) }
154
153
154
+ /**
155
+ * Holds if basic block `succ` is immediately controlled by this basic
156
+ * block with conditional value `s`. That is, `succ` is an immediate
157
+ * successor of this block, and `succ` can only be reached from
158
+ * the callable entry point by going via the `s` edge out of this basic block.
159
+ */
160
+ pragma [ nomagic]
161
+ predicate immediatelyControls ( BasicBlock succ , SuccessorType s ) {
162
+ succ = this .getASuccessor ( s ) and
163
+ forall ( BasicBlock pred | pred = succ .getAPredecessor ( ) and pred != this |
164
+ succ .dominates ( pred )
165
+ )
166
+ }
167
+
168
+ predicate immediatelyControls2 ( BasicBlock succ , SuccessorType s ) {
169
+ succ = this .getASuccessor ( s ) and
170
+ bbIDominates ( this , succ ) and
171
+ forall ( BasicBlock pred | pred = succ .getAPredecessor ( ) and pred != this |
172
+ succ .dominates ( pred )
173
+ )
174
+ }
175
+
176
+ /**
177
+ * Holds if basic block `controlled` is controlled by this basic block with
178
+ * conditional value `s`. That is, `controlled` can only be reached from
179
+ * the callable entry point by going via the `s` edge out of this basic block.
180
+ */
181
+ predicate controls ( BasicBlock controlled , SuccessorType s ) {
182
+ // For this block to control the block `controlled` with `s` the following must be true:
183
+ // 1/ Execution must have passed through the test i.e. `this` must strictly dominate `controlled`.
184
+ // 2/ Execution must have passed through the `s` edge leaving `this`.
185
+ //
186
+ // Although "passed through the `s` edge" implies that `this.getASuccessor(s)` dominates `controlled`,
187
+ // the reverse is not true, as flow may have passed through another edge to get to `this.getASuccessor(s)`
188
+ // so we need to assert that `this.getASuccessor(s)` dominates `controlled` *and* that
189
+ // all predecessors of `this.getASuccessor(s)` are either `this` or dominated by `this.getASuccessor(s)`.
190
+ //
191
+ // For example, in the following C# snippet:
192
+ // ```csharp
193
+ // if (x)
194
+ // controlled;
195
+ // false_successor;
196
+ // uncontrolled;
197
+ // ```
198
+ // `false_successor` dominates `uncontrolled`, but not all of its predecessors are `this` (`if (x)`)
199
+ // or dominated by itself. Whereas in the following code:
200
+ // ```csharp
201
+ // if (x)
202
+ // while (controlled)
203
+ // also_controlled;
204
+ // false_successor;
205
+ // uncontrolled;
206
+ // ```
207
+ // the block `while controlled` is controlled because all of its predecessors are `this` (`if (x)`)
208
+ // or (in the case of `also_controlled`) dominated by itself.
209
+ //
210
+ // The additional constraint on the predecessors of the test successor implies
211
+ // that `this` strictly dominates `controlled` so that isn't necessary to check
212
+ // directly.
213
+ exists ( BasicBlock succ | this .immediatelyControls ( succ , s ) | succ .dominates ( controlled ) )
214
+ }
215
+
155
216
/**
156
217
* Holds if this basic block strictly post-dominates basic block `bb`.
157
218
*
@@ -188,6 +249,52 @@ module Make<LocationSig Location, InputSig<Location> Input> {
188
249
cached
189
250
newtype TBasicBlock = TBasicBlockStart ( Node cfn ) { startsBB ( cfn ) }
190
251
252
+ /** Holds if `cfn` starts a new basic block. */
253
+ private predicate startsBB ( Node cfn ) {
254
+ not exists ( nodeGetAPredecessor ( cfn , _) ) and exists ( nodeGetASuccessor ( cfn , _) )
255
+ or
256
+ nodeIsJoin ( cfn )
257
+ or
258
+ nodeIsBranch ( nodeGetAPredecessor ( cfn , _) )
259
+ or
260
+ // In cases such as
261
+ //
262
+ // ```rb
263
+ // if x and y
264
+ // foo
265
+ // else
266
+ // bar
267
+ // ```
268
+ //
269
+ // we have a CFG that looks like
270
+ //
271
+ // x --false--> [false] x and y --false--> bar
272
+ // \ |
273
+ // --true--> y --false--
274
+ // \
275
+ // --true--> [true] x and y --true--> foo
276
+ //
277
+ // and we want to ensure that both `foo` and `bar` start a new basic block.
278
+ exists ( nodeGetAPredecessor ( cfn , any ( SuccessorType s | successorTypeIsCondition ( s ) ) ) )
279
+ }
280
+
281
+ /**
282
+ * Holds if `succ` is a control flow successor of `pred` within
283
+ * the same basic block.
284
+ */
285
+ private predicate intraBBSucc ( Node pred , Node succ ) {
286
+ succ = nodeGetASuccessor ( pred , _) and
287
+ not startsBB ( succ )
288
+ }
289
+
290
+ /**
291
+ * Holds if `bbStart` is the first node in a basic block and `cfn` is the
292
+ * `i`th node in the same basic block.
293
+ */
294
+ cached
295
+ predicate bbIndex ( Node bbStart , Node cfn , int i ) =
296
+ shortestDistances( startsBB / 1 , intraBBSucc / 2 ) ( bbStart , cfn , i )
297
+
191
298
/**
192
299
* Holds if the first node of basic block `succ` is a control flow
193
300
* successor of the last node of basic block `pred`.
@@ -213,51 +320,6 @@ module Make<LocationSig Location, InputSig<Location> Input> {
213
320
214
321
private import Cached
215
322
216
- /** Holds if `cfn` starts a new basic block. */
217
- private predicate startsBB ( Node cfn ) {
218
- not exists ( nodeGetAPredecessor ( cfn , _) ) and exists ( nodeGetASuccessor ( cfn , _) )
219
- or
220
- nodeIsJoin ( cfn )
221
- or
222
- nodeIsBranch ( nodeGetAPredecessor ( cfn , _) )
223
- or
224
- // In cases such as
225
- //
226
- // ```rb
227
- // if x and y
228
- // foo
229
- // else
230
- // bar
231
- // ```
232
- //
233
- // we have a CFG that looks like
234
- //
235
- // x --false--> [false] x or y --false--> bar
236
- // \ |
237
- // --true--> y --false--
238
- // \
239
- // --true--> [true] x or y --true--> foo
240
- //
241
- // and we want to ensure that both `foo` and `bar` start a new basic block.
242
- exists ( nodeGetAPredecessor ( cfn , any ( SuccessorType s | successorTypeIsCondition ( s ) ) ) )
243
- }
244
-
245
- /**
246
- * Holds if `succ` is a control flow successor of `pred` within
247
- * the same basic block.
248
- */
249
- predicate intraBBSucc ( Node pred , Node succ ) {
250
- succ = nodeGetASuccessor ( pred , _) and
251
- not startsBB ( succ )
252
- }
253
-
254
- /**
255
- * Holds if `bbStart` is the first node in a basic block and `cfn` is the
256
- * `i`th node in the same basic block.
257
- */
258
- private predicate bbIndex ( Node bbStart , Node cfn , int i ) =
259
- shortestDistances( startsBB / 1 , intraBBSucc / 2 ) ( bbStart , cfn , i )
260
-
261
323
/** Holds if `bb` is an entry basic block. */
262
324
private predicate entryBB ( BasicBlock bb ) { nodeIsDominanceEntry ( bb .getFirstNode ( ) ) }
263
325
}
0 commit comments