Loops

The loop head is the basic block with an incoming back edge. We define $l_h$ as the location of the first statement of the loop head.

The pre-loop block is the block prior to the loop head. We assume that there is always a unique pre-loop block. The pre-loop state ${\mathcal{G}}_{\text{pre}}$ is the state after evaluating the terminator of the pre-loop block.

The following operations are performed when we join the pre-loop block with the loop head. Note that at this point we've already computed ${\mathcal{G}}_{\text{pre}}$.

We construct the state ${\mathcal{G}}_h$ for the loop head as follows:

Step 1 - Identify Relevant Loop Nodes

We identify the following sets of places:

• $P_{live}$: the places used inside the loop that are live and initialized at $l_h$.

• $P_{blocked}^{loop}$: the subset of $P_{live}$ that are directly borrowed by a borrow live at $l_h$

• $P_{blockers}$: the subset of $P_{live}$ that contain lifetime projections

• $P_{loop}$: Places used in the loop that may be relevant for the invariant: $P_{blocked}^{loop}\cup P_{blockers}$

${\mathcal{N}}_{loop}$ is the union of $P_{loop}$ and the associated lifetime projections of $P_{loop}$.

$R{P}_{blockers}$ are the associated lifetime projections of $P_{blockers}$.

Step 2 - Expand Pre-State Graph to Include Relevant Loop Nodes

The nodes in ${\mathcal{N}}_{loop}$ will need to appear in ${\mathcal{G}}_h$ but may not be present in ${\mathcal{G}}_{pre}$ (for example, it's possible that the loop could borrow from a subplace that requires unpacking). We construct a graph ${\mathcal{G}}_{pre}^{\prime }$ by unpacking ${\mathcal{G}}_{pre}$ such that ${\mathcal{G}}_{pre}^{\prime }$ contains all places in $P_{loop}$.

Step 3 - Identify Borrow Roots $P_{roots}$

The borrow roots of a place $p$ are the most immediate places that $p$ could be borrowing from and later become accessible, and excluding places already in $P_{loop}$

We defined the borrow roots using the function $roots(p)$:

• Initialize a list $L$ to contain all lifetime projections in $p$
• while $L$ is not empty:
  • Pop $n$ from $L$
  • For each edge $e$ blocked by $n$ in ${\mathcal{G}}_{pre}^{\prime }$:
    • If the edge is an unpack edge, add all of its blocked nodes to $L$
    • Otherwise, for each blocked node $n^{\prime }$ in $e$:
      • If $n^{\prime }\in {\mathcal{N}}_{roots}^p$ or $n^{\prime }\in {\mathcal{N}}_{loop}$, do nothing
      • If $n^{\prime }$ is live at $l_h$, add $n^{\prime }$ to ${\mathcal{N}}_{roots}^p$
      • If $n^{\prime }$ is a root in ${\mathcal{G}}_{pre}^{\prime }$, add $n^{\prime }$ to ${\mathcal{N}}_{roots}^p$
      • Otherwise, add $n^{\prime }$ to $L$
• The resulting roots are the associated places of ${\mathcal{N}}_{roots}^p$

We then identify $P_{roots}$, the most immediate nodes that $P_{loop}$ could be borrowing from and later become accessible (excluding nodes already in ${\mathcal{P}}_{loop}$). $P_{roots}$ is the union of the roots for each place in $P_{loop}$.

Step 4 - Construct Abstraction Graph And Compute Blocked Lifetime Projections

We construct an abstraction graph $\mathcal{A}$ that describes the blocking relations potentially introduced in the loop from places in $P_{\text{roots}}$ to nodes in $P_{blockers}$ and from nodes in $P_{blocked}^{loop}$ to nodes in $P_{blockers}$.

connect() function:

We begin by define a helper function $connect(p_{blocked},p_{blocker})$ which adds edges to $\mathcal{A}$ based on $p_{blocked}$ being blocked by $p_{blocker}$ in the loop:

• Identify $p_{blocker}\downarrow r_{top}$: the top-level lifetime projection in $p_{blocker}$
  • Insert a loop abstraction edge $\{p_{blocked}\}\to \{p_{blocker}\downarrow r_{top}\}$ into $\mathcal{A}$
• For each $p_{blocked}\downarrow r\in RP(p_{blocked})$:
  • Identify the lifetime projections in $p_{blocker}$ that may mutate borrows in $p_{blocked}\downarrow r$
    • $R{P}_{mut}=\{p\downarrow r^{\prime }|p\downarrow r^{\prime }\in RP(p_{blocker}),r\approx r^{\prime }\}$
    • If $R{P}_{mut}$ is nonempty:
      • Introduce a placeholder node $p_{blocked}\downarrow r\mathtt{at}\mathtt{FUTURE}$
      • Add a borrowflow hyperedge $\{p_{blocked}\downarrow r\}\to R{P}_{mut}$
      • Add a future hyperedges:
        • $\{p_{blocked}\downarrow r\}\to \{p_{blocked}\downarrow r\mathtt{at}\mathtt{FUTURE}\}$
        • $R{P}_{mut}\to \{p_{blocked}\downarrow r\mathtt{at}\mathtt{FUTURE}\}$
  • Identify the lifetime projections in $p_{blocker}$ that borrows in $p_{blocked}\downarrow r$ may flow into
    • $R{P}_{flow}=\{p\downarrow r^{\prime }|p\downarrow r^{\prime }\in RP(p_{blocker}),r\text{outlives}{r}^{\prime }\}\setminus R{P}_{flow}$
    • If $R{P}_{flow}$ is nonempty:
      • Add a borrowflow hyperedge $\{p_{blocked}\downarrow r\}\to R{P}_{flow}$

Algorithm:

• For each blocker place $p_{blocker}\in P_{blocker}$:

  • For each $p_{blocked}\in roots(p_{blocker})$, perform $connect(p_{blocked},p_{blocker})$
  • For each $p_{blocked}\in P_{blocked}^{loop}$
    • If $p_{blocker}$ blocks $p_{blocked}$ at $l_h$, then perform $connect(p_{blocked},p_{blocker})$

• Subsequently, ensure that $\mathcal{A}$ is well-formed by adding unpack edges where appropriate. For example, if (*x).f is in the graph, there should also be an expansion edge from *x to (*x).f.

• We identify the set $R{P}_{rename}$ of lifetime projections that will need to be renamed (indicating they will be expanded in the loop and remain non-accessible at the loop head). $R{P}_{rename}$ is the set of non-leaf lifetime projection nodes in $\mathcal{A}$ (leaf nodes are accessible at the head).

• Label all lifetime projections in $R{P}_{rename}$ with location $l_h$, add connections to their Future nodes as necessary.

Step 5 - Label Blocked Lifetime Projections in Pre-State

The resulting graph for the loop head will require new labels on lifetime projections modified in the loop. We begin by constructing an intermediate graph ${\mathcal{G}}_{pre}^{\prime \prime }$ by labelling each lifetime projection in $R{P}_{rename}$ with $l_h$ and remove capabilities to all places in $P_{remove}$ in ${\mathcal{G}}_{pre}^{\prime }$.

Step 6 - Identify Pre-State Subgraph to Replace With Abstraction Graph

We then identify the subgraph ${\mathcal{G}}_{cut}\subseteq {\mathcal{G}}_{pre}^{\prime \prime }$ that will be removed from ${\mathcal{G}}_{pre}^{\prime \prime }$ and replaced with the loop abstraction $\mathcal{A}$.

• Let ${\mathcal{N}}_{cut}$ = $nodes(\mathcal{A})$.
• We construct ${\mathcal{G}}_{cut}$ by including all nodes in ${\mathcal{N}}_{cut}$ and all edges $e$ where there exists $n,n^{\prime }\in {\mathcal{N}}_{cut}$ where $e$ is on a path between $n$ and $n^{\prime }$ in ${\mathcal{G}}_{\text{pre}}^{\prime \prime }$.

Step 7 - Replace Pre-State Subgraph with Abstraction Graph

The graph ${\mathcal{G}}_h$ for the loop head is defined as ${\mathcal{G}}_h={\mathcal{G}}_{pre}^{\prime \prime }\setminus {\mathcal{G}}_{cut}\cup \mathcal{A}$

Step 8 (Optional) - Confirm Invariant is Correct

To confirm that the resulting graph is correct, for any back edge into the state at ${\mathcal{G}}_h$ with state ${\mathcal{G}}^{\prime }$, performing the loop join operation on ${\mathcal{G}}^{\prime }$ and ${\mathcal{G}}_h$ should yield ${\mathcal{G}}_h$.