@@ -388,10 +388,17 @@ private import PhiInsertion
388388 * location and there is a use of that location reachable from that block without an intervening definition of the
389389 * location.
390390 * Within the approach outlined above, we treat a location slightly differently depending on whether or not it is a
391- * virtual variable. For a virtual variable,
392- * location into the beginning of a block
391+ * virtual variable. For a virtual variable, we will insert a `Phi` instruction on the dominance frontier if there is
392+ * a use of any member location of that virtual variable that is reachable from the `Phi` instruction. For a location
393+ * that is not a virtual variable, we insert a `Phi` instruction only if there is an exactly-overlapping use of the
394+ * location reachable from the `Phi` instruction. This ensures that we insert a `Phi` instruction for a non-virtual
395+ * variable only if doing so would allow dataflow analysis to get a more precise result than if we just used a `Phi`
396+ * instruction for the virtual variable as a whole.
393397 */
394398private module PhiInsertion {
399+ /**
400+ * Holds if a `Phi` instruction needs to be inserted for location `defLocation` at the beginning of block `phiBlock`.
401+ */
395402 predicate definitionHasPhiNode ( Alias:: MemoryLocation defLocation , OldBlock phiBlock ) {
396403 exists ( OldBlock defBlock |
397404 phiBlock = Dominance:: getDominanceFrontier ( defBlock ) and
@@ -402,8 +409,8 @@ private module PhiInsertion {
402409 }
403410
404411 /**
405- * Holds if the virtual variable `vvar ` has a definition in block `block`, either because of an existing instruction
406- * or because of a Phi node.
412+ * Holds if the memory location `defLocation ` has a definition in block `block`, either because of an existing
413+ * instruction, a `Phi` node, or a `Chi` node.
407414 */
408415 private predicate definitionHasDefinitionInBlock ( Alias:: MemoryLocation defLocation , OldBlock block ) {
409416 definitionHasPhiNode ( defLocation , block ) or
@@ -501,10 +508,10 @@ private module PhiInsertion {
501508private import DefUse
502509
503510/**
504- * Module containing the predicates that connect uses to their reaching definition. The reaching definitios are computed
505- * separately for each unique use `MemoryLocation`. An instruction is treated as a definition of a use location if the
506- * defined location overlaps the use location in any way. Thus, a single instruction may serve as a definition for
507- * multiple use locations, since a single definition location may overlap many use locations.
511+ * Module containing the predicates that connect uses to their reaching definition. The reaching definitions are
512+ * computed separately for each unique use `MemoryLocation`. An instruction is treated as a definition of a use location
513+ * if the defined location overlaps the use location in any way. Thus, a single instruction may serve as a definition
514+ * for multiple use locations, since a single definition location may overlap many use locations.
508515 *
509516 * Definitions and uses are identified by a block and an integer "offset". An offset of -1 indicates the definition
510517 * from a `Phi` instruction at the beginning of the block. An offset of 2*i indicates a definition or use on the
0 commit comments