@@ -294,11 +294,26 @@ module Make<LocationSig Location, InputSig<Location> Input> {
294294 variableRead ( readbb , _, v , _) and
295295 not variableWrite ( readbb , _, v , _)
296296 or
297- exists ( TPhiReadNode ( v , readbb ) ) and
297+ synthPhiRead ( readbb , v ) and
298298 not ref ( readbb , _, v , _)
299299 )
300300 }
301301
302+ /**
303+ * Holds if we should synthesize a pseudo-read of `v` at the beginning of `bb`.
304+ *
305+ * These reads are named phi-reads, since they are constructed in the same
306+ * way as ordinary phi nodes except all all reads are treated as potential
307+ * "definitions". This ensures that use-use flow has the same dominance
308+ * properties as def-use flow.
309+ */
310+ private predicate synthPhiRead ( BasicBlock bb , SourceVariable v ) {
311+ inReadDominanceFrontier ( bb , v ) and
312+ liveAtEntry ( bb , v ) and
313+ // no need to create a phi-read if there is already a normal phi
314+ not any ( PhiNode def ) .definesAt ( v , bb , _)
315+ }
316+
302317 cached
303318 private newtype TDefinitionExt =
304319 TWriteDef ( SourceVariable v , BasicBlock bb , int i ) {
@@ -309,12 +324,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
309324 inDefDominanceFrontier ( bb , v ) and
310325 liveAtEntry ( bb , v )
311326 } or
312- TPhiReadNode ( SourceVariable v , BasicBlock bb ) {
313- inReadDominanceFrontier ( bb , v ) and
314- liveAtEntry ( bb , v ) and
315- // no need to create a phi-read if there is already a normal phi
316- not any ( PhiNode def ) .definesAt ( v , bb , _)
317- }
327+ TPhiReadNode ( SourceVariable v , BasicBlock bb ) { synthPhiRead ( bb , v ) }
318328
319329 private class TDefinition = TWriteDef or TPhiNode ;
320330
0 commit comments