@@ -199,6 +199,8 @@ private module Internal {
199199 /**
200200 * Holds if the `i`th node of `bb` is a use or an SSA definition of variable `v`, with
201201 * `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.
202204 */
203205 private predicate ssaRef ( ReachableBasicBlock bb , int i , SsaSourceVariable v , RefKind k ) {
204206 useAt ( bb , i , v ) and k = ReadRef ( )
@@ -290,6 +292,145 @@ private module Internal {
290292 or
291293 rewindReads ( bb , i , v ) = 1 and result = getDefReachingEndOf ( bb .getImmediateDominator ( ) , v )
292294 }
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+ }
293434}
294435
295436import Internal
0 commit comments