@@ -199,6 +199,8 @@ private module Internal {
199
199
/**
200
200
* Holds if the `i`th node of `bb` is a use or an SSA definition of variable `v`, with
201
201
* `k` indicating whether it is the former or the latter.
202
+ *
203
+ * Note this includes phi nodes, whereas `ref` above only includes explicit writes and captures.
202
204
*/
203
205
private predicate ssaRef ( ReachableBasicBlock bb , int i , SsaSourceVariable v , RefKind k ) {
204
206
useAt ( bb , i , v ) and k = ReadRef ( )
@@ -290,6 +292,145 @@ private module Internal {
290
292
or
291
293
rewindReads ( bb , i , v ) = 1 and result = getDefReachingEndOf ( bb .getImmediateDominator ( ) , v )
292
294
}
295
+
296
+ private module AdjacentUsesImpl {
297
+ /** Holds if `v` is defined or used in `b`. */
298
+ private predicate varOccursInBlock ( SsaSourceVariable v , ReachableBasicBlock b ) {
299
+ ssaRef ( b , _, v , _)
300
+ }
301
+
302
+ /** Holds if `v` occurs in `b` or one of `b`'s transitive successors. */
303
+ private predicate blockPrecedesVar ( SsaSourceVariable v , ReachableBasicBlock b ) {
304
+ varOccursInBlock ( v , b )
305
+ or
306
+ exists ( getDefReachingEndOf ( b , v ) )
307
+ }
308
+
309
+ /**
310
+ * Holds if `b2` is a transitive successor of `b1` and `v` occurs in `b1` and
311
+ * in `b2` or one of its transitive successors but not in any block on the path
312
+ * between `b1` and `b2`.
313
+ */
314
+ private predicate varBlockReaches (
315
+ SsaSourceVariable v , ReachableBasicBlock b1 , ReachableBasicBlock b2
316
+ ) {
317
+ varOccursInBlock ( v , b1 ) and
318
+ b2 = b1 .getASuccessor ( ) and
319
+ blockPrecedesVar ( v , b2 )
320
+ or
321
+ exists ( ReachableBasicBlock mid |
322
+ varBlockReaches ( v , b1 , mid ) and
323
+ b2 = mid .getASuccessor ( ) and
324
+ not varOccursInBlock ( v , mid ) and
325
+ blockPrecedesVar ( v , b2 )
326
+ )
327
+ }
328
+
329
+ /**
330
+ * Holds if `b2` is a transitive successor of `b1` and `v` occurs in `b1` and
331
+ * `b2` but not in any block on the path between `b1` and `b2`.
332
+ */
333
+ private predicate varBlockStep (
334
+ SsaSourceVariable v , ReachableBasicBlock b1 , ReachableBasicBlock b2
335
+ ) {
336
+ varBlockReaches ( v , b1 , b2 ) and
337
+ varOccursInBlock ( v , b2 )
338
+ }
339
+
340
+ /**
341
+ * Gets the maximum rank among all SSA references to `v` in basic block `bb`.
342
+ */
343
+ private int maxSsaRefRank ( ReachableBasicBlock bb , SsaSourceVariable v ) {
344
+ result = max ( ssaRefRank ( bb , _, v , _) )
345
+ }
346
+
347
+ /**
348
+ * Holds if `v` occurs at index `i1` in `b1` and at index `i2` in `b2` and
349
+ * there is a path between them without any occurrence of `v`.
350
+ */
351
+ pragma [ nomagic]
352
+ predicate adjacentVarRefs (
353
+ SsaSourceVariable v , ReachableBasicBlock b1 , int i1 , ReachableBasicBlock b2 , int i2
354
+ ) {
355
+ exists ( int rankix |
356
+ b1 = b2 and
357
+ ssaRefRank ( b1 , i1 , v , _) = rankix and
358
+ ssaRefRank ( b2 , i2 , v , _) = rankix + 1
359
+ )
360
+ or
361
+ maxSsaRefRank ( b1 , v ) = ssaRefRank ( b1 , i1 , v , _) and
362
+ varBlockStep ( v , b1 , b2 ) and
363
+ ssaRefRank ( b2 , i2 , v , _) = 1
364
+ }
365
+
366
+ predicate variableUse ( SsaSourceVariable v , IR:: Instruction use , ReachableBasicBlock bb , int i ) {
367
+ bb .getNode ( i ) = use and
368
+ exists ( SsaVariable sv |
369
+ sv .getSourceVariable ( ) = v and
370
+ use = sv .getAUse ( )
371
+ )
372
+ }
373
+ }
374
+
375
+ private import AdjacentUsesImpl
376
+
377
+ /**
378
+ * Holds if the value defined at `def` can reach `use` without passing through
379
+ * any other uses, but possibly through phi nodes.
380
+ */
381
+ cached
382
+ predicate firstUse ( SsaDefinition def , IR:: Instruction use ) {
383
+ exists ( SsaSourceVariable v , ReachableBasicBlock b1 , int i1 , ReachableBasicBlock b2 , int i2 |
384
+ adjacentVarRefs ( v , b1 , i1 , b2 , i2 ) and
385
+ def .definesAt ( b1 , i1 , v ) and
386
+ variableUse ( v , use , b2 , i2 )
387
+ )
388
+ or
389
+ exists (
390
+ SsaSourceVariable v , SsaPhiNode redef , ReachableBasicBlock b1 , int i1 , ReachableBasicBlock b2 ,
391
+ int i2
392
+ |
393
+ adjacentVarRefs ( v , b1 , i1 , b2 , i2 ) and
394
+ def .definesAt ( b1 , i1 , v ) and
395
+ redef .definesAt ( b2 , i2 , v ) and
396
+ firstUse ( redef , use )
397
+ )
398
+ }
399
+
400
+ /**
401
+ * Holds if `use1` and `use2` form an adjacent use-use-pair of the same SSA
402
+ * variable, that is, the value read in `use1` can reach `use2` without passing
403
+ * through any other use or any SSA definition of the variable.
404
+ */
405
+ cached
406
+ predicate adjacentUseUseSameVar ( IR:: Instruction use1 , IR:: Instruction use2 ) {
407
+ exists ( SsaSourceVariable v , ReachableBasicBlock b1 , int i1 , ReachableBasicBlock b2 , int i2 |
408
+ adjacentVarRefs ( v , b1 , i1 , b2 , i2 ) and
409
+ variableUse ( v , use1 , b1 , i1 ) and
410
+ variableUse ( v , use2 , b2 , i2 )
411
+ )
412
+ }
413
+
414
+ /**
415
+ * Holds if `use1` and `use2` form an adjacent use-use-pair of the same
416
+ * `SsaSourceVariable`, that is, the value read in `use1` can reach `use2`
417
+ * without passing through any other use or any SSA definition of the variable
418
+ * except for phi nodes and uncertain implicit updates.
419
+ */
420
+ cached
421
+ predicate adjacentUseUse ( IR:: Instruction use1 , IR:: Instruction use2 ) {
422
+ adjacentUseUseSameVar ( use1 , use2 )
423
+ or
424
+ exists (
425
+ SsaSourceVariable v , SsaPhiNode def , ReachableBasicBlock b1 , int i1 , ReachableBasicBlock b2 ,
426
+ int i2
427
+ |
428
+ adjacentVarRefs ( v , b1 , i1 , b2 , i2 ) and
429
+ variableUse ( v , use1 , b1 , i1 ) and
430
+ def .definesAt ( b2 , i2 , v ) and
431
+ firstUse ( def , use2 )
432
+ )
433
+ }
293
434
}
294
435
295
436
import Internal
0 commit comments