Overview

The purpose of the PCG Analysis is to provide clients with the following:

• The PCG data structure representing the state of ownership and borrowing of Rust places at arbitrary program points within a Rust function
• For any pair $p{p}_i,p{p}_j$ of consecutive program points, an ordered list of actions that describe the transformation of the PCG of $p{p}_i$ to the PCG of $p{p}_j$.

PCG Analysis Algorithm

Key Concepts:

• The PCG Analysis Algorithm operates on the MIR Body of a Rust function and returns a PCG Analysis of the function.
• A PCG Analysis contains PCG Data for every reachable¹ MIR location in the Body².
• The PCG Data is a tuple of PCG States and PCG Action Data.

The PCG States of a MIR location is a list of the PCGs computed at that location, concretely:

• An Initial PCG, followed by
• One PCG for every PCG evaluation phase

The PCG Action Data of a MIR location contains a list of PCG Actions for each evaluation phase in the location (i.e. the actions performed at that phase).

The PCG Dataflow Analysis

The PCG Analysis Algorithm is implemented as a MIR dataflow analysis using PcgDomainData as the domain. PcgDomainData contains a PCGData value and other relevant metadata (e.g the associated basic block). Notably, the analysis only analyzes the statements in each basic block one time. Conceptually, this property is ensured because the final state at a loop head is computed upon entering it in the analysis (without having first seen the body).

We note that the behaviour of the join operation on PCGDomainData requires tracking of what blocks have been previously joined (this is basically a consequence of the interface of the MIR dataflow analysis). The PCGDomainData join operation joins the PCG ${\mathcal{G}}^{\prime }$ of block $b^{\prime }$ into the PCG $\mathcal{G}$ at block $b$ as follows:

1. If no block has ever been joined into $b$, then set $\mathcal{G}$ = ${\mathcal{G}}^{\prime }$
2. If the edge from $b^{\prime }$ to $b$ is not a back edge³ of a loop, then ${\mathcal{G}}^{\prime }$ is joined into $\mathcal{G}$ using the algorithm defined here

Because the join does not modify the PCG for back edges, the analysis can be completed without ever having to re-analyse the statements within a block.

PCG Data Structure

The PCG data structure represents the state of ownership and borrowing of Rust places at an arbitrary program point.

It consists of three components:

• The Owned PCG, which describes the state of owned places
• The Borrow State, which describes borrowed memory (borrowed places and lifetime projections) and borrow relations, and also some auxillary data structures
• The Place Capabilities which is a map from places to capabilities

Owned PCG

The Owned PCG is a forest, where the root of each tree in the forest is a MIR Local.

Each tree in the forest is defined by a set of place expansions, which describe how unpacked all of the owned places are. For each expansion $\overline{p}$ in the set, the base $p$ is a node in the forest and $\overline{p}$ are its children. We note that each expansion can be similarly interpreted as a hyperedge $\{p\}\to \overline{p}$

Each local in the body of a MIR function is either unallocated or allocated in the Owned PCG. A local is allocated iff there exists a corresponding root node in the Owned PCG, otherwise it is unallocated.

The operation allocate $v$ in the Owned PCG requires that $v$ is not allocated, and adds a new root for $v$. The deallocate $v$ operation removes the forest rooted at $v$.

Borrow State

The Borrow State is a tuple containing a set of Validity Conditions that describes the set of paths leading to the current block and a Borrows Graph, a directed acyclic hypergraph which describes borrowed places, sets of borrows, and their relation to one another.

Because a borrow created within a block exists only for executions that visit that block, we label new borrows using the validity conditions of the block in which they were created.

Place Capabilities

Place capabilities $\mathcal{C}$ is a partial map from places to capabilities.

1. A MIR location $l$ reachable iff its basic block $b_l$ is reachable from the start block in the CFG without traversing unwind or fake edges (the latter kind do not correspond to the actual control flow of the function). The original reason for only considering reachable edges was to improve performance; removing this constraint (and instead considering all locations) would be simple to change in the implementation. ↩

2. The PCG analysis algorithm is implemented as a MIR dataflow analysis defined by the rust compiler crate. In the implementation, the PCG Data is computed for every reachable MIR location during the algorithm execution itself, but only the PCG Data for the entry state of each basic block is stored. The PCG Data for an arbitrary location within a block is re-computed by applying the dataflow analysis transfer function from the entry state. ↩

3. In the join implementation, we an edge from $b^{\prime }$ to $b$ is a back edge if $b$ dominates $b^{\prime }$ in the CFG ↩

Definitions

Types

Type Contains

A type $\tau$ contains a type ${\tau }^{\prime }$, iff:

1. $\tau ={\tau }^{\prime }$, or
2. $\tau$ is an ADT and contains a field $\mathtt{f}:{\tau }_{\mathtt{f}}$ and ${\tau }_{\mathtt{f}}$ contains ${\tau }^{\prime }$
3. $\tau ={\&}^{\prime }\mathtt{r}\mathtt{mut}{\tau }_{\text{tgt}}$ and ${\tau }_{\text{tgt}}$ contains ${\tau }^{\prime }$

Types Containing Lifetimes

A type $\tau$ contains a lifetime $r$ iff $\tau$ contains the type $\&{}^{\prime }\mathtt{r}\mathtt{mut}{\tau }^{\prime }$ for some type ${\tau }^{\prime }$. A lifetime $r$ is nested in a type $\tau$ iff $\tau$ contains a type ${\&}^{\prime }\mathtt{r}\mathtt{mut}{\tau }^{\prime }$ and ${\tau }^{\prime }$ contains $r$. We extend these concept to places: a place $p:\tau$ contains a lifetime $r$ iff $\tau$ contains $r$; $r$ is nested in $p:\tau$ iff $r$ is nested in $\tau$. A lifetime projection $p\downarrow r$ is nested if $r$ is nested in $p$.

PCG Evaluation Phase

The PCG Evaluation Phases are:

• PreOperands
• PostOperands
• PreMain
• PostMain

For every MIR location, a seperate PCG is generated for each phase. They represent the following:

• PreOperands - A reorganization of the initial state¹ to prepare to apply the effects of evaluating the operands in the statement
• PostOperands - The result of applying the operand effects on the PreOperands state
• PreMain - A reorganization of the PostOperands state to prepare to apply any other effects of the statement
• PostMain - The result of applying any other effects of the statement to the PreMain state.

Program Point

A program point represents a point within the execution of a Rust function in a way that is more fine-grained than a MIR location (each MIR location has multiple program points which to different stages of evaluation of a statement). Concretely, a program point is either:

• The start of a basic block
• A pair of a MIR location and a PCG evaluation phase

Borrows and Blocking

Blocking

A place $p_{blocker}$ blocks a place $p_{blocked}$ at a location $l$ if a usage of $p_{blocked}$ at $l$ would invalidate a live borrow $b$ contained in the origins of $p_{blocker}$ at $l$.

Borrow Liveness

A borrow $p=\&\text{mut}{p}^{\prime }$ is live at location $l$ if a usage of $p^{\prime }$ at $l$ would invalidate the borrow.

Directly Borrowed

A place $p$ is directly borrowed by a borrow $b$ if $p$ is exactly the borrowed place (not e.g. a pre- or postfix of the place).

1. The initial state is either the PostMain of the previous location within the basic block. Or if this is the first statement within the block, it is the entry state of the block (i.e. the result from joining the final states of incoming basic blocks). ↩

Capabilities

A capability describes the actions that the program is permitted to perform on a place at a particular program point. There are three main capabilities:

Exclusive (E)

Places with this capability can be read from, written to, or mutably borrowed.

We do not differentiate between locals bound with let bindings and let mut bindings: a variable bound with let would still have this capability if it could be written to if it was mutably borrowed.

Read (R)

Places with this capability can be read from. Shared borrows can also be created to this place. Shared references with this capability can be dereferenced.

A place $p$ with capability E is downgraded to R if a shared borrow is created to a place that is a pre- or postfix of $p$.

When a shared reference $p$ is dereferenced, the capability to $p$ is downgraded to R. Any place projecting from a shared references will have capability R.

Write (W)

The place can be written to.

When an exclusive reference $p$ is dereferenced, the capability to $p$ is downgraded to W.

PCG Nodes

$$\begin{array}{llr}i& & \text{(Integer)}\\ v& & \text{(MIR Local)}\\ c& & \text{(MIR Constant)}\\ b& & \text{(MIR Basic Block Index)}\\ l& ::=b[i]& \text{(MIR Location)}\\ p& & \text{(MIR Place)}\\ \ell & ::=& \text{(Label)}\\ & \mid \text{start}b& \\ & \mid \text{loop}b& \\ & \mid \text{prepare}l& \\ & \mid \text{before-collapse}l& \\ & \mid \text{before-ref-assignment}l& \\ & \mid \text{mid}l& \\ & \mid \text{after}l& \\ \tilde{p}& ::=& \text{(Maybe-Labelled Place)}\\ & \mid p& \text{(Current Place)}\\ & \mid p\mathtt{at}\ell & \text{(Labelled Place)}\\ \hat{p}& ::=& \text{(PCG Place)}\\ & \mid \tilde{p}& \text{(Maybe-Labelled Place)}\\ & \mid remote(v)& \text{(Remote Place)}\\ rp& ::=& \text{(Lifetime Projection)}\\ & \mid \hat{p}\downarrow r& \text{(Place Projection)}\\ & \mid \hat{p}\downarrow r\text{at}\ell & \text{(Snapshot of Place Projection)}\\ & \mid \hat{p}\downarrow r\text{at}\text{FUTURE}& \text{(Placeholder Projection)}\\ & \mid c\downarrow r& \text{(Constant Projection)}\\ n& ::=\hat{p}|rp& \text{(PCG Node)}\end{array}$$

Associated Place

The associated place of a PCG node $n$ is defined by the partial function $p(n)$ :

• $p(p)=p$
• $p(p\text{at}\ell )=p$
• $p(rp)=p(base(rp))$

Where $base(rp)$ is the base of the lifetime projection $rp$ as defined here.

Local PCG Nodes

A PCG node $n$ is a local node if it has an associated place $p(n)$.

PCG Hyperedges

A PCG Hyperedge is a directed edge of the form $\overline{n_s}\to \overline{n_t}$, where elements of $\overline{n_s}$ and $\overline{n_t}$ are PCG nodes. The set $\overline{n_s}$ are referred to as the source nodes of the edge, and $\overline{n_t}$ are the target nodes. Hyperedges in the PCG are labelled with validity conditions¹.

We represent a PCG hyperedge as a tuple of an edge kind and validity conditions.

Edge Kinds

An edge kind is a description an edge, including its source and target nodes, as well as other associated metadata. The metadata is described by the type of the edge, the various types are presented below:

Unpack Edges

Unpack edges are used to represent the unpack of an owned place in order to access one of its fields. For example, writing to a field x.f requires expanding x.

An unpack edge connects an owned place $p$ to one of it's expansions $\overline{p}$. Each place in $\overline{p}$ is guaranteed to be owned.

For example, if x is an owned place with fields x.f and x.g, the edge {x} -> {x.f, x.g} is a valid unpack edge.

Unpack edges are not generated for dereferences of reference-typed places. Borrow PCG Expansion Edges are used in such cases. Unpack edges are used in derefences of Box-typed places.

Borrow PCG Expansion Edge

Borrow PCG Expansion Edges conceptually take one of three forms:

• Dereference Expansion: The dereference of a reference-typed place
• Place Expansion: The expansion of a borrowed place to access one of its fields
• Lifetime Projection Expansion: The expansion of the lifetime projections of an owned or borrowed place

Dereference Expansion

The source nodes of a dereference expansion consist of:

• A maybe-labelled place ${\tilde{p}}_s$, and:
• A lifetime projection ${rp}_s$

Where ${\tilde{p}}_s$ and ${rp}_s$ have the same associated place $p_s$.

The target node ${\tilde{p}}_t$ of a dereference expansion is a maybe-labelled place with associated place $\ast p_s$.

Place Expansion

The source node of a place expansion is a maybe-labelled place ${\tilde{p}}_s$ with associated place $p_s$, where $p_s$ is a borrowed place and $p_s$ is not a reference.

The target nodes of a place expansion is a set of maybe-labelled places $\overline{{\tilde{p}}_t}$ where the associated places of $\overline{{\tilde{p}}_t}$ are an expansion of $p_s$.

Lifetime Projection Expansion

The source node of a lifetime projection expansion is a lifetime projection ${rp}_s$ where $base({rp}_s)$ is a maybe-labelled place ${\tilde{p}}_s$ with associated place of $p_s$.

The target nodes of a lifetime projection expansion is a set of lifetime projections $\overline{{rp}_t}$ where the base of each place is a maybe-labelled place. The associated places of the bases of $\overline{{rp}_t}$ are an expansion of $p_s$.

Borrow Edges

Borrow edges are used to represent direct borrows in the program. We define two types:

• Local Borrow Edges: A borrow created in the MIR Body, e.g. from a statement let y = &mut x;
• Remote Borrow Edges: A borrow created by the caller of this function where the assigned place of the borrow is an input to this function.

Remote Borrows are named as such because (unlike local borrows), the borrowed place does not have a name in the MIR body (since it was created by the caller).

Local Borrows

The source node of a local borrow is a maybe-labelled place $\tilde{p}$. The target node of a local borrow is a lifetime projection $rp$ where $base(rp)$ is a maybe-labelled place.

Remote Borrows

The source node of a remote borrow is a remote place $remote(v)$. The target node of a remote borrow is a lifetime projection $rp$ where $base(rp)$ is a maybe-labelled place.

Abstraction Edge

An abstraction edge represents the flow of borrows introduced due to a function call or loop.

Function Call Abstraction Edge

The source node of a function call abstraction edge is a lifetime projection $rp$ where $base(rp)$ is a maybe-labelled place.

The target node of a function call abstraction edge is a lifetime projection $rp$ where $base(rp)$ is a maybe-labelled place.

Loop Abstraction Edge

The source node of a loop abstraction edge is a PCG node.

The target node of a loop abstraction edge is a local PCG node.

Borrow-Flow Edge

A borrow-flow edge represents the flow of borrows between a lifetime projection ${rp}_s$ and a local lifetime projection ${rp}_t$. This edge is used when the relationship between the blocked and target node is known concretely, but does not correspond to an expansion or a borrow.

Borrow-Flow Edges are labelled with a Borrow-Flow Edge Kind with associated metadata, enumerated as follows:

Aggregate

Metadata:

• $i_f$: Field Index
• $i_{rp}$: Lifetime Projection Index

An aggregate kind is used for borrows flowing into an aggregate type (i.e. struct, tuple). The metadata indicates that the blocked lifetime projection flows into the ${i_{rp}}^{th}$ lifetime projection of the ${i_f}^{th}$ field of the blocking lifetime projection.

Introduced in the following two cases:

1. Collapsing an owned place:
   • edges flow from the lifetime projections of the labelled places of the base to the lifetime projections of the current base
2. Assigning an aggregate (e.g. x = Aggregate(a, b)):
   • edges flow from the lifetime projections of the labelled places in the rvalue to the lifetime projections of x

Reference to Constant

Connects a region projection from a constant to some PCG node. For example let x: &'x C = c; where c is a constant of type &'c C, then an edge {c↓'c} -> {x↓'x} of this kind is created. This is called ConstRef in the implementation.

Borrow Outlives

For a borrow e.g. let x: &mut y;, the PCG analysis inserts edges of this kind to connect the (potentially snapshotted) lifetime projections of y to the lifetime projections of x.

Initial Borrows

To construct the initial PCG state, the PCG analysis adds an edge of this kind between every lifetime projection in each remote place to the corresponding lifetime projection of its corresponding argument.

For example, if $v$ is the local corresponding to a function argument and contains a lifetime projection $v\downarrow r$, an edge $\{remote(v)\downarrow r\}\to \{v\downarrow r\}$ will appear in the graph.

Connects the lifetime projections of remote places to the lifetime projections of

Copy

For a copy let x = y;, the PCG analysis inserts edges of this kind to connect the lifetime projections of y to the lifetime projections of x.

In the implementation this is currently called CopyRef.

Move

For a move let x = move y;, the PCG analysis inserts edges of this kind to connect the (potentially snapshotted) lifetime projections of y to the lifetime projections of x.

Future

These edges are introduced to describe the flow of borrows to the lifetime projections of a place that is currently blocked. When they are created, the target node is a placeholder lifetime projection of a blocked place.

1. Currently not in the owned portion of the PCG, but this should happen eventually. ↩

Types

A type $\tau$ is either:

• A type parameter of the form $\text{param}i$
• An alias type of the form $\tau ::T⟨\overline{\tau }⟩$
• A type constructor application of the form $T⟨\overline{\tau }⟩$
• A box type of the form $\text{Box}⟨\tau ⟩$

Corresponding Regions

If $r$ is a region in $\tau$, the corresponding region $r_c$ in a type ${\tau }_c$ is:

If $\tau =\text{\&}rm{\tau }^{\prime }$ and ${\tau }_c=\text{\&}{r}_c^{\prime }m{\tau }_c^{\prime }$ then $r_c=r_c^{\prime }$

If $\tau =T⟨{\tau }_1,\dots ,t_n⟩$ and ${\tau }_c=T⟨{\tau }_{c_1},\dots ,t_{c_n}⟩$, iterate $i$ over $1,\dots ,n$, and if there exists an $r_c^{\prime }$ where $r_c^{\prime }$ in ${\tau }_{c_i}$ is the corresponding region of $r$ in $t_i$, then $r_c=r_c^{\prime }$.

Places

A place $p$ is a tuple of a local $v$ and a projection.

Place Expansion

A set of places $\overline{p}$ is a place expansion iff there exists a base $p$ such that:

• $p$ is an enum type and $\overline{p}=\{p@V\}$ and $V$ is a variant of $p$
• $p$ is a struct or tuple type and $\overline{p}$ is the set of places obtained by projecting $p$ with each of the fields in the type of $p$
• $p$ is a reference-typed field and $\overline{p}=\{\ast p\}$
• $p$ is an array or slice and $\overline{p}=p[i]$ (TODO: more cases)

If there is such a $p$, then that $p$ is unique, and $\overline{p}$ is an expansion of $p$.

Owned Places

A place is owned iff it does not project from the dereference of a reference-typed place.

Place Liveness

A place $p$ is live at a location $l$ iff there exists a location $l^{\prime }$ and a control flow-path $c$ from $l$ to $l^{\prime }$ where a place conflicting with $p$ is used at $l^{\prime }$ and there are no assignments of any places conflicting with $p$ along c.

Place Prefix

A place $p$ is a prefix of a place $p^{\prime }$ iff:

• $p$ and $p^{\prime }$ have the same local, and
• The projection of $p$ is a prefix of the projection of $p^{\prime }$

Note that $p$ is a prefix of itself.

A place $p$ is a strict prefix of $p^{\prime }$ iff $p$ is a prefix of $p^{\prime }$ and $p\ne p^{\prime }$.

Regions

A region $r$ is one of:

• A RegionVid (a region variable identifier)
• The static region 'static
• An early-bound region

Lifetime Projections

Generalized Lifetimes

A generalized lifetime $gr$ is either a region $r$ or $\text{RegionsIn}(\tau )$, where $\tau$ is either:

1. a type parameter, or
2. a type alias that cannot be normalized

Generalized Lifetime Projections

A generalized lifetime projection $grp$ takes the form $b\downarrow gr$ where $b$ is a base having an associated type $\tau$. The index $\text{index}(grp)$ of a lifetime projection is the index of the occurence of $gr$ in the generalized lifetime list $GR(\tau )$ (the list of generalized lifetimes in $\tau$, occurring in the order they appear in $\tau$, and with duplicates removed).

A lifetime projection is a generalized lifetime projection of the form $b\downarrow r$ (that is, a generalized lifetime projection where the associated generalized lifetime is a region).

PCG Lifetime Projections

PCG lifetime projections take the following form

$$\begin{array}{llr}rp& ::=& \text{(Lifetime Projection)}\\ & \mid \hat{p}\downarrow r& \text{(Place Projection)}\\ & \mid \hat{p}\downarrow r\text{at}\ell & \text{(Snapshot of Place Projection)}\\ & \mid \hat{p}\downarrow r\text{at}\text{FUTURE}& \text{(Placeholder Projection)}\\ & \mid c\downarrow r& \text{(Constant Projection)}\end{array}$$

Lifetime Projection Lifetime

The lifetime $r(rp)$ of a lifetime projection $rp$ is conceptually the lifetime $r$ on the right of the $\downarrow$, i.e:

• $r(\hat{p}\downarrow r)=r$
• $r(\hat{p}\downarrow r\text{at}\ell )=r$
• $r(\hat{p}\downarrow r\text{at}\text{FUTURE})=r$
• $r(c\downarrow r)=r$

Lifetime Projection Base

The base $base(rp)$ of a lifetime projection $rp$ is conceptually the part on the left of the $\downarrow$, i.e. defined as follows:

• $base(\hat{p}\downarrow r)=\hat{p}$
• $base(\hat{p}\downarrow r\text{at}\ell )=\hat{p}$
• $base(\hat{p}\downarrow r\text{at}\text{FUTURE})=\hat{p}$
• $base(c\downarrow r)=c$

Validity Conditions

We associate borrow PCG edges with validity conditions to identify the control-flow conditions under which they are valid. Consider the following program:

fn main(){
    // BB0
    let mut x = 1;
    let mut y = 2;
    let mut z = 3;
    let mut r = &mut x;
    if rand() {
        // BB1
        r = &mut y;
    }
    // BB2
    if rand2() {
        // BB3
        r = &mut z;
    }
    // BB4
    *r = 5;
}

We represent control flow using a primitive called a branch choice $d\in D$ of the form $b_i\to b_j$. A branch choice represents the flow of control from one basic block to another. In the above code there are two possible branch choices from bb0: $\text{bb0}\to \text{bb1}$ and $\text{bb0}\to \text{bb2}$ and one branch choice from bb1 (to bb2).

For any given basic block $b$ in the program, an execution path leading to $b$ is an ordered list of blocks ending in $b$. For example, one path of execution to bb4 can be described by: $\text{bb0}\to \text{bb2}\to \text{bb3}\to \text{bb4}$.

Validity conditions $pc$ conceptually define a predicate on execution paths. For example, the validity conditions ${pc}_{x\to r}$ describing the control flow where r borrows from z at bb3 require that the path contain $\text{bb2}\to \text{bb3}$.

We represent validity conditions $pc$ as a partial function $B\to \mathcal{P}(B)$ mapping relevant blocks to sets of allowed target blocks.

An execution path $\overline{d}$ is valid for validity conditions $pc$ iff, for each $b_s\to b_t\in \overline{d}$, either:

• $b_s$ is not a relevant block in $pc$, or
• $b_t$ is in the set of allowed target blocks of $b_s$ in $pc$

Formal Definition

The representation of validity conditions in our implementations corresponds closely to the following description:

Validity conditions $pc\in I$ is a map $B\to \mathcal{P}(B)$ describing control-flow conditions. For each block $b\in \text{dom}(pc)$, $pc[b]$ is a subset of the real successors of $b$.

The join of validity conditions ${pc}_i$ and ${pc}_j$ is defined as:

$$({pc}_i\cup {pc}_j)[b]=p{c}_i[b]\cup p{c}_j[b]$$

Validity conditions $pc$ are valid for a path $b_0,\dots ,b_n$ iff:

$$\forall i\in \{0,\dots ,n-1\}:pc[b_i]=\varnothing \vee b_{i+1}\in pc[b_i]$$

Correctness Theorem (Sketch)

For every borrow edge $e$ in the PCG at location $l$ and execution path $\overline{d}$ to $l$, the corresponding borrow is live at $l$ iff $\overline{d}$ satisfies the validity conditions of $e$.

Proof

We prove this for each location in the MIR by induction on the basic blocks of the graph via a reverse-postorder traversal. The inductive hypothesis is that the property holds for each ancestor block.

Having proved for the 1st location in a basic block, it is trivial to show for the remaining locations in the block, therefore we only concern ourselves with the basic blocks.

The case of bb0 is trivial.

We now concern ourselves with the validity conditions $p{c}_n^e$ of an arbitrary edge $e$ at block $b_n$, assuming via IH that it holds for all $b_n^{\prime }$ where $n^{\prime }<n$. Let $\overline{b_{in}}$ be the set of incoming nodes. We define our $p{c}_n^e$ as the repeated join: ${\bigcup }_{p{c}_e^f\in \overline{b_{in}}}p{c}_f^e\cup \{b_f\to b_n\}$.

We first show that the if direction holds: For every borrow edge $e$ in the PCG at location $l$ and execution path $\overline{d}$ to $l$, if the corresponding borrow is live at $l$, then $\overline{d}$ satisfies the validity conditions of $e$.

Every $\overline{d}$ has a prefix $\overline{d_f}$ and ends with $b_f\to b_n$, by our IH we have $\overline{d_f}$ satisfies $p{c}_e^f$. We need to then show that $\overline{d}=\overline{d_f}++[b_n]$ satisfies $p{c}_e^n$. Our proof is by contradiction.

Suppose $\overline{d}$ did not satisfy $p{c}_e^n$; then there must be a pair $(b\to b^{\prime })\in \overline{d}$ where $p{c}_e^n[b]\ne \varnothing \wedge b^{\prime }\notin p{c}_e^n[b]$. We know that the pair cannot be the final pair in $\overline{d}$ (i.e. $b_f\to b_n$) by the definition of join we have $p{c}_e^n[b_f]=\varnothing \vee b_n\in p{c}_e^f[b]$. Therefore the edge $b\to b^{\prime }$ must exist in some strict prefix ${\overline{d}}^{\prime }$ of $\overline{d}$. Then, there must be a nonempty set ${\overline{b_f}}^{\prime }\subseteq \overline{b_{in}}$ where $p{c}_e^{f^{\prime }}[b]\ne \varnothing \wedge b^{\prime }\notin p{c}_e^{f^{\prime }}[b]$ (otherwise, the joined $p{c}_e^n[b]$ would be either $\varnothing$ or contain $b^{\prime }$). But then, because ${\overline{d}}^{\prime }$ must contain $b\to b^{\prime }$, it would not satisfy the validity conditions of $p{c}_e^{f^{\prime }}$ for any $f^{\prime }$ .

We now show the reverse: For every borrow live at $l$ for an execution path $\overline{d}$, its corresponding edge satisfies the validity conditions of $e$.

Our proof relies on the monotonicity of joins: if $b^{\prime }\in pc[b]$ then $b^{\prime }\in (pc\cup p{c}^{\prime })[b]$ for any $p{c}^{\prime }$.

The borrow is created at a unique block $b_c$. Then $b_c$ is definitely in $\overline{d}$ at some index $i$ and the borrow is not killed in any block $b_i$ for all $c<i⩽|\overline{d}|$.

Our proof works by building longer prefixes of $\overline{d}$. The base case is when the borrow is created (and therefore becomes live) at $b_c=d_i$, where the property holds trivially. Then, when going from $d_i,\dots ,d_j$ to $d_i,\dots ,d_{j+1}$, we add to the validity conditions $d_j\to d_{j+1}$ and join other incoming blocks. Because the prefix satisfies the prior conditions by induction, satisfies the additional condition, and monotonicity of join, the longer prefix also satisfies conditions. QED.

Functions

Generalized Types and Parameter Environments

A generalized type ${\tau }^{\ast }$ is either a type $\tau$ or a region $r$

A param env $E$ is a list of constraints; where a constraint takes the form:

• $r:r^{\prime }$ ($r$ outlives $r^{\prime }$)
• $\tau :r$ (All regions in $\tau$ outlive $r$)
• $\tau :\text{Tr}$ ($\tau$ implements $\text{Tr}$)

Outlives Judgments

The base outlives relation $E{⊢}_0{\tau }^{\ast }:r$ holds iff it can be derived from the following rules:

1. Direct: $({\tau }^{\ast }:r)\in E$
2. Reflexivity: $E{⊢}_{0}r:r$
3. Transitivity: $E{⊢}_0{\tau }^{\ast }:r$ and $E{⊢}_{0}r:r^{\prime }$ implies $E{⊢}_0{\tau }^{\ast }:r^{\prime }$

That is, the base outlives relation is the transitive closure of the region-outlives and type-outlives facts in $E$.

There also exists an outlives relation $E⊢{\tau }^{\ast }:r$ such that $E{⊢}_0{\tau }^{\ast }:r$ implies $E⊢{\tau }^{\ast }:r$. This relation is computed by Rust's type system and additionally accounts for outlives constraints implied by trait membership constraints in $E$.

Function Signatures

A function signature is a pair $⟨\overline{{\tau }^{\text{in}}},{\tau }^{\text{out}}⟩$.

A defined function signature $f$ is a tuple $⟨\text{defid},\overline{{\tau }^{\text{in}}},{\tau }^{\text{out}},E⟩$.

An instantiation $\hat{f}$ of $f$ is the tuple $⟨f,\overline{{\tau }^{\ast }}⟩$; where $\overline{{\tau }^{\ast }}$ is a list of early-bound parameters.

The identity instantiation $f_I$ of $f$ is obtained by applying the identity substitution $I_{{\tau }^{\ast }}$. Defined function calls are applied to instantiations of a function.

The generalized lifetime projections $GRP(\hat{f})$ of a function instantiation $\hat{f}$ is defined as the set:

$\{\text{arg}i\downarrow gr|i⩽|\overline{{\tau }^{\text{in}}}|,gr\in GR({\tau }_i^{\text{in}})|\}\cup$ $\{\text{result}\downarrow gr|gr\in GR({\tau }^{\text{out}})\}$

Function Calls

A function call target $\tilde{f}$ is either an instantiation $\hat{f}$ or a closure / function pointer $ct$.

A function call $FC$ takes the form $p=\tilde{f}(\overline{op})\text{at}l$, where $p$ is a MIR place, and $\overline{op}$ is a sequence of MIR operands.

$E(FC)$ is the parameter environment of the function with respect to the call site.

The lifetime projections $RP(FC)$ of a function call is the union of the lifetime projections in $p$ and the lifetime projections in $\overline{op}$.

A function call $FC$ is valid iff it satisfies the unique region property: each region in the lifetime projections of $FC$ is unique.

MIR Definitions

Here we describe definitions of MIR concepts that are relevant to the PCG.

MIR Dataflow Analysis

At a high level, a MIR dataflow analysis is defined by the following elements:

• A domain $\mathcal{D}$
• A join operation $join:(\mathcal{D}\times \mathcal{D})\to \mathcal{D}$
• An empty state $d_{ϵ}\in \mathcal{D}$
• A transfer function $transfer:(\mathcal{D}\times Location)\to \mathcal{D}$

Performing the dataflow analysis on a MIR body $B$ computes a value of type $\mathcal{D}$ for every location in $B$. The analysis is performed (conceptually) as follows¹:

• The analysis defines a map $S$ that maps locations in $B$ to elements of $\mathcal{D}$.
• Each location in $S$ is initialized to $d_{ϵ}$
• The operation analyze(b) updates $S$ as follows:
  • $s[b[0]]\leftarrow transfer(s[b[0]],b[0])$
  • For $0<i⩽|b|:s[b[i]]\leftarrow transfer(s[b[i-1]],b[i])$
• The analysis defines a worklist $W=[b_0]$
• While $W$ is not empty:
  • Pop $b$ from $W$
  • Perform $analyze(b)$
  • Let $s_b^{exit}$ be the entry of the last location in $b$ in $s$
  • For each successor $b^{\prime }$ of $b$:
    • Let $s_{b^{\prime }}^{entry}=s[b^{\prime }[0]]$
    • Let $s_{b^{\prime }}^{join}=join(s_{b^{\prime }}^{entry},s_b^{exit})$
    • If $s_{b^{\prime }}^{join}\ne s_{b^{\prime }}^{entry}$:
      • $s[b^{\prime }[0]]\leftarrow s_{b^{\prime }}^{join}$
      • Add $b^{\prime }$ to $W$
• $S$ is the result

1. The current analysis implementation (defined in the rust compiler) is more efficient than what we describe because it tracks state per basic block rather than per-location, as the states for any location in a block can be computed by repeated application of the transfer function to the entry state. ↩

Borrow-Checker Interface

The PCG Analysis requires an implementation of the borrow-checker interface providing the following:

• A predicate $live(n,l)$, which holds iff the borrow extents in PCG node $n$ are all in scope at MIR location $l$
• A predicate $directly\_blocked(p,l)$, which holds iff place $p$ is directly blocked at MIR location $l$
• A predicate $blocks(p,p^{\prime },l)$ which holds iff mutating $p^{\prime }$ at $l$ would cause $p$ to be dead
• A predicate $outlives(r,r^{\prime },l)$ which holds iff $r$ must outlive $r^{\prime }$ at $l$
• A function $borrows\_blocking(p,l)$ which returns the set of borrows that would be invalidated if $p$ was modified at $l$
• A function $twophase\_borrow\_activations(l)$ which returns the set of two-phase borrows that are activated at $l$.

Analysing Statements

The PCG Analysis computes four states for each MIR statement, corresponding to the PCG evaluation phases:

• PreOperands
• PostOperands
• PreMain
• PostMain

The analysis for each statement proceeds in two steps:

• Step 1: Place Conditions are computed for each statement phase
• Step 2: PCG Actions are performed for each statement phase

Determining Place Conditions

A place condition is a predicate on the PCG related to a particular MIR place.

We define the following place conditions:

• Capability: Place $p$ must have capability $c$
• RemoveCapability: Capability for place $p$ should be removed¹
• AllocateOrDeallocate: Storage for local $v$ is allocated (e.g. via the StorageLive instruction)
• Unalloc: Storage for local $v$ is not allocated (e.g. via the StorageDead instruction)
• ExpandTwoPhase: Place $p$ is the borrowed place of a two-phase borrow
• Return: The RETURN place has Exclusive capability

During this step of the analysis, place conditions are computed for each phase. The determination of place conditions is based on the MIR statement; the state of the PCG is not relevant.

The conditions computed for each phase are as follows:

• PreOperands: Pre-conditions on the PCG for the operands in the statement to be evaluated
• PostOperands: Post-conditions on the PCG after the operands in the statement has been evaluated
• PreMain: Pre-conditions on the PCG for the main effect of the statement to be applied
• PostMain: Post-conditions on the PCG after the main effect of the statement has been applied

As an example, the MIR statement: let y = move x would have the following place conditions:

• PreOperands: {x: E}
• PostOperands: {x: W}
• PreMain: {y: W}
• PostMain: {y: E}

The rules describing how these place conditions are generated for a statement are described here.

Performing PCG Actions

After the place conditions for each phase are computed, the analyses proceeds by performing the actions for each phase. At a high-level, this proceeds as follows:

PreOperands

1. The Borrow PCG graph is minimized by repeatedly removing every effective leaf edge² $e$ for which their target PCG nodes of $e$ are not live at the current MIR location. A Borrow PCG RemoveEdge action is generated for each removed edge. See more details here.

2. The place capabilities required by the PreOperand place conditions are obtained.

PostOperands

No actions occur at this stage. Capabilities for every moved-out operand are set to Write.

PreMain

The place capabilities required by the PreMain place conditions are obtained.

Then, the behaviour depends on the type of statement:

1. StorageDead(v)
   1. The analysis performs the MakePlaceOld(v, StorageDead) action.
2. Assign(p r)
   1. If p is a reference-typed value and contained in the borrows graph and the capability for p is R:
      1. The analysis performs the RestoreCapability(p, E) action
   2. If $\mathcal{C}[p]\ne \text{W}$:
      1. The analysis performs the $\text{Weaken}(p,\mathcal{C}[p],\text{W})$ action
   3. All edges in the borrow PCG blocked by any of the lifetime projections in p are removed

PostMain

1. For every operand move p in the statement:
   1. The analysis performs the MakePlaceOld(p, MoveOut) action.
2. If the statement is a function call p = call f(..):
   1. Function call abstraction edges are inserted using the rules defined here
3. If the statement takes the form Assign(p, r):
   1. p is given exclusive permission
   2. If $r$ takes the form Aggregate(o_1, ..., o_n):
      1. For every $i\in \{i|0⩽i<n\wedge (o_i=\text{move p}\vee o_i=\text{copy p})\}$
         1. Let $p_i$ be the associated place of $o_i$
         2. For all $j.k.0⩽j<|rp(p)|,0⩽k<|rp(p_i)|$
            1. If $p_i\downarrow r_k$ outlives $p\downarrow r_j$:
               1. Add an Aggregate BorrowFlow edge $\{p_i\downarrow r_k\}\to \{p\downarrow r_j\}$, with associated field index $i$ and lifetime projection index $k$.
   3. If $r$ takes the form use c, c is a reference-typed constant with lifetime $r_c$, and $p$ is a reference-typed place with lifetime $r_p$, then:
      1. Create a new ConstRef borrowedge of the form $\{c\downarrow r_c\}\to \{p\downarrow r_p\}$
   4. If $r$ takes the form move p_f or cast(_, move p_f):
      1. For all $i,0⩽i<|rp(p)|$:
         1. Let $p\downarrow r$ be the i'th lifetime projection in p
         2. Let $p_f\downarrow r_f$ be the i'th lifetime projection in p_f
         3. Let $\ell$ be the snapshot location $\text{before}l:PostOperands$
         4. Add a Move edge $\{p_f\text{at}\ell \downarrow r_f\}\to \{p\downarrow r\}$
   5. If $r$ takes the form copy p_f or cast(_, copy p_f):
      1. For all $i,0⩽i<|rp(p)|$:
         1. Let $p\downarrow r$ be the i'th lifetime projection in p
         2. Let $p_f\downarrow r_f$ be the i'th lifetime projection in p_f
         3. Add a CopyRef edge $\{p_f\downarrow r_f\}\to \{p\downarrow r\}$
   6. If $r$ takes the form &p or &mut p:
      1. Handle the borrow as described here

1. This is only used for mutably borrowed places ↩

2. The set of effective leaf edges are the leaf edges in the graph obtained by removing all edges to placeholder lifetime projections. ↩

Removing Edges for out-of-scope Borrow Extents

At the beginning of each statement

Rules for Determining Place Conditions

Place conditions are computed in terms of triples, where a triple is a pair (pre, post) where pre is a place condition and post is either a place condition or None.

The place conditions for each phase are determined by two sets of triples: the operand triples and the main triples. The place conditions for the PreOperands phase is the set of conditions in the pres of the operand triples. The PostOperands phase is the set of conditions in the posts of the operand triples. PreMain and PostMain are defined accordingly.

Determining Operand Triples for a Statement

1. For each operand $o$ in the statement:
   1. If $o$ takes the form copy p:
      • Add (p: R, None) to the operand triples
   2. If $o$ takes the form move p:
      • Add (p: E, p: W) to the operand triples
2. For each rvalue $r$ in the statement:
   1. If $r$ takes the form &p:
      • Add (p: R, p: R) to the operand triples
   2. If $r$ takes the form &mut p:
      • If the borrow is a two-phase borrow:
        • Add (ExpandTwoPhase p, p: R) to the operand triples
      • Otherwise, add (p: E, RemoveCapability p) to the operand triples
   3. If $r$ takes the form *mut p:
      • Add (p: E, None) to the operand triples
   4. If $r$ takes the form *const p:
      • Add (p: R, None) to the operand triples
   5. If $r$ takes the form len(p), discriminant(p) or CopyForDeref(p):
      • Add (p: R, None) to the operand triples

Determining Main Triples for a Statement

The rule depends on the statement type:

1. Assign(p, r)
   1. If r takes the form &fake q:
      • Add (p: W, None) to the main triples
   2. If r takes the form ShallowInitBox o t
      • Add (p: W, p: e) to the main triples
   3. Otherwise, add (p: W, p: E) to the main triples
2. FakeRead(_, p)
   1. Add (p: R, None) to the main triples
3. SetDiscriminant(p, ..)
   1. Add (p: E, None) to the main triples
4. Deinit(p)
   1. Add (p: E, p: w) to the main triples
5. StorageLive(v)
   1. Add (Unalloc v, AllocateOrDeallocate v) to the main triples
6. StorageDead(v)
   1. Add (AllocateOrDeallocate v, Unalloc v) to the main triples
7. Retag(_, p)
   1. Add (p: E, None) to the main triples

Determining Main Triples for a Terminator

The rule depends on the terminator type:

1. Return
   1. Add (Return, _0: w) to the main triples
2. Drop(p)
   1. Add (p: W, None) to the main triples
3. Call(p, _)
   1. Add (p: W, p: E) to the main triples
4. Yield(p, _)
   1. Add (p: W, p: E) to the main triples

Rules for the Creation of Borrows

Mutable Borrows

Consider the stmt p = &mut q, at a program point $l$, where $p$ has type $\&r_0\mathtt{mut}\tau$, and $q$ has type $\tau$, and $\tau$ is a type containing lifetimes $r_1,\dots r_n$.

At the end of the PreOperands phase, the PCG is guaranteed to be in a state where, for each $r_i\in \{r_1,\dots ,r_n\}$ the lifetime projection $q\downarrow r_i$ is in the graph. During the Operands phase, each lifetime projection $q\downarrow r_i$ is labelled with the current program point to become $q\downarrow r_i\mathtt{at}l$. At the end of the PreMain phase, for each $r_i\in \{r_0,\dots ,r_n\}$, the lifetime projection $p\downarrow r_i$ is guaranteed not to be in the graph. During the Main phase, these projections are added.

Subsequently, the labelled lifetime projections under $p$ are connected with BorrowFlow edges to the new lifetime projections under $q$. Namely, for each $i\in \{1,\dots n\},j\in \{0,\dots ,n\}$ if $r_i$ outlives $r_j$, then a BorrowFlow edge $\{q\downarrow r_i\mathtt{at}l\}\to \{p\downarrow r_j\}$ is added.

Subsequently, we introduce Future nodes and edges to account for nested references as follows. For each $i\in \{1,\dots n\}$:

1. Insert the node $q\downarrow r_i\mathtt{atFuture}$ into the graph
2. If any Future edges originate from the labelled projection $q\downarrow r_i\mathtt{at}l$, redirect them such that they originate from $q\downarrow r_i\mathtt{atFuture}$.
3. Insert a Future edge $\{q\downarrow r_i\mathtt{at}l\}\to \{q\downarrow r_i\mathtt{atFuture}\}$
4. Insert a Future edge $\{p\downarrow r_i\}\to \{q\downarrow r_i\mathtt{atFuture}\}$

Owned PCG Operations

Collapse

The operation $collapse(p,\mathcal{E},\mathcal{C})$ modifies place expansions $\mathcal{E}$ and set of place capabilities $\mathcal{C}$ such that $p$ becomes a leaf in the forest corresponding to $\mathcal{E}$. Stated more formally it modifies $\mathcal{E}$ to ensure that $\mathcal{E}$ contains an expansion $\overline{p}$ containing $p$, and $p$ is not the base of any expansion in $\mathcal{E}$. Capabilities in $\mathcal{C}$ are updated to account for the removal of expansions from $\mathcal{E}$.

collapse returns the set of Owned PCG Actions corresponding to the removed expansions.

The algorithm is implemented as follows:

1. Let ${\mathcal{E}}^{\prime }$ be the subset of place expansions in $\mathcal{E}$ such that for each $\overline{p^{\prime }}$ in ${\mathcal{E}}^{\prime }$, the base place $p^{\prime }$ is a prefix of $p$.
2. Let ${\mathcal{E}}^{\prime \prime }$ be an ordered list of the expansions in ${\mathcal{E}}^{\prime }$ sorted in order of descending length of the projections of their base place
3. Let $R$ be the list of operations to return
4. For each $\overline{p^{\prime }}$ in ${\mathcal{E}}^{\prime \prime }$
   1. Let $\overline{c^{\prime }}$ be the capabilities of $p^{\prime }$ in $\mathcal{C}$
   2. Let $c$ be the minimum common capabiility of $\overline{c^{\prime }}$.
   3. Let $p^{\prime }$ be the base of $\overline{p^{\prime }}$
   4. Remove capabilities to the places in $\overline{p^{\prime }}$ from $\mathcal{C}$
   5. Assign capability $c$ to $p^{\prime }$ in $\mathcal{C}$
   6. Remove $\overline{p^{\prime }}$ from $\mathcal{E}$
   7. Add $\text{collapse}(p^{\prime },\overline{p^{\prime }},c)$ to $R$
5. return $R$

Join Operation

The join algorithm on PCGs takes as input PCGs $\mathcal{G}$ and ${\mathcal{G}}^{\prime }$ and mutates $\mathcal{G}$ to join in ${\mathcal{G}}^{\prime }$.

The algorithm proceeds in the follow steps:

1. The Owned PCG of ${\mathcal{G}}^{\prime }$ is joined into the Owned PCG of $\mathcal{G}$ (this may also change the capabilities of $\mathcal{G}$)
2. The capabilities of ${\mathcal{G}}^{\prime }$ are joined into the capabilities of $\mathcal{G}$.
3. The Borrow State of ${\mathcal{G}}^{\prime }$ is joined into the Borrow State of $\mathcal{G}$

We now describe each step in detail:

Owned PCG Join

Let $\mathcal{O}$ be the owned PCG of $\mathcal{G}$ and ${\mathcal{O}}^{\prime }$ the PCG of ${\mathcal{G}}^{\prime }$.

1. For each local $v$ in the MIR body:
   1. If $v$ is allocated in both $\mathcal{O}$ and ${\mathcal{O}}^{\prime }$:
      1. Join the place expansions rooted at ${\mathcal{O}}^{\prime }[v]$ into $\mathcal{O}[v]$
   2. Otherwise, if $v$ is allocated in $\mathcal{O}$, it should be deallocated in $\mathcal{O}$

Joining Local Expansions (Algorithm Overview)

The algorithm for joining local expansions also involves modifying capabilities (including to borrowed places), and also may cause some places to be labelled. We "emulate" a modification of the block to be joined in, so that we can use the resulting modified capabilities and borrows graph in the remainder of the join. We implement the join by defining a "one-way" join operation ${\bigsqcup }^{\leftarrow }$, and then performing a join $(\mathcal{G},{\mathcal{G}}^{\prime })\leftarrow \mathcal{G}{\bigsqcup }^{\leftarrow }{\mathcal{G}}^{\prime }$ and subsequently $({\mathcal{G}}^{\prime },\mathcal{G})\to {\mathcal{G}}^{\prime }{\bigsqcup }^{\leftarrow }\mathcal{G}$. The owned PCGs of $\mathcal{G}$ and ${\mathcal{G}}^{\prime }$ (including the associated capabilities) should be the same after the join. Formally, we could imagine a partial order ${<}_{\mathcal{O}}$ where ${\mathcal{G}}_1{<}_{\mathcal{G}}{\mathcal{G}}_2$ iff the owned PCG of ${\mathcal{G}}_1$ can be transformed to the owned PCG of ${\mathcal{G}}_2$ by a sequence of repack operations on its owned PCG. The join identifies the maximum graph ${\mathcal{G}}^{\prime }$ (w.r.t ${<}_{\mathcal{O}}$) where ${\mathcal{G}}^{\prime }{<}_{\mathcal{O}}{\mathcal{G}}_1$ and ${\mathcal{G}}^{\prime }{<}_{\mathcal{O}}{\mathcal{G}}_2$.

Before we present the full algorithm (that takes into account borrows), we first describe a version that would work in the absence of borrows and therefore only considers capabilities W and E. The key point of the join is that all places/capabilities in the resulting joined PCGs should be obtainable from the originals (i.e. via a sequence of PCG repacks). The join starts from the root of both trees, and navigate downwards. For expansions that are the same in both, nothing needs to happen. If the other tree is expanded more than us, we continue expanding ours: the only reason it would be expanded is that part of it is moved out, so we can expand and weaken the LHS to match the RHS. For example, if the LHS is {x: E}, and the RHS is {x.f: E, x.g: W}, we'd want to expand x in the LHS (note that the subsequent capability join will properly account for capabilities).

If we're at a place where the expansions differ in both trees (e.g. x -> {x@Some} vs x -> {x@None}), we collapse both to the place (e.g x) and set capability to the place to W. Neither of the expansion places are accessible by both, so the "most" capability we could obtain is the W permission to the base.

More formally, we define the one-way join $joi{n}_{\leftarrow }(\mathcal{G},{\mathcal{G}}^{\prime })$ as the traversal where:

1. If we're at a leaf $p$ in $\mathcal{G}$ that is not a leaf in ${\mathcal{G}}^{\prime }$ (having children $\overline{p}$), then:
   1. Expand $p$ to $\overline{p}$ in $\mathcal{G}$
2. If were at a node $p$ in $\mathcal{G}$ where the expansion $e$ is not the same as the expansion $e^{\prime }$ in ${\mathcal{G}}^{\prime }$:
   1. Collapse both $\mathcal{G}$ and ${\mathcal{G}}^{\prime }$ to $p$ for capability $W$

Now, we extend the join to work with borrows and the read capability $R$. Borrows complicate the story because it enables mutually exclusive (at runtime) places to appear in the PCG. For example:

#![allow(unused)]
fn main() {
fn f(x: Either<String, String>) -> &String; {
    let result = match x {
        Left(l) => &l,
        Right(r) => &r
    };
    result
}
}

After the assignment, we should have $R$ capability to both x@Left and x@Right because they are borrowed into result. In the case of exclusive borrows, such places would not have capability but still present in the owned PCG (again, to reflect the target of result). Therefore, the collapse and expand rule previously shown are no longer sufficient.

1. If we're at a place $p$ that's a leaf in both $\mathcal{G}$ and ${\mathcal{G}}^{\prime }$:
   1. If $p$ has capability of at least $R$ in $\mathcal{G}$ and has capability exactly $R$ in ${\mathcal{G}}^{\prime }$:
      1. Then, after the join, the place $p$ can have at most capability $R$. Its also possible that we can now have incompatible different owned expansions of $p$ in the joined PCG, that have been borrowed under mutually exclusive paths.

Local Expansions Join: $joi{n}_{\mathcal{E}}$

The algorithm $joi{n}_{\mathcal{E}}(⟨\mathcal{E},\mathcal{B},\mathcal{C}⟩,⟨{\mathcal{E}}^{\prime },{\mathcal{B}}^{\prime },{\mathcal{C}}^{\prime }⟩)$ joins a set of place expansions ${\mathcal{E}}^{\prime }$ into a set of place expansions $\mathcal{E}$, and makes corresponding changes to borrows $\mathcal{B}$ and capabilities $\mathcal{C}$.

1. If either $\mathcal{E}$ or ${\mathcal{E}}^{\prime }$ have any expansions:
   1. Perform $joi{n}_{\mathcal{E}}^{\leftarrow }(⟨\mathcal{E},\mathcal{B},\mathcal{C}⟩,⟨{\mathcal{E}}^{\prime },{\mathcal{B}}^{\prime },{\mathcal{C}}^{\prime }⟩)$
   2. Perform $joi{n}_{\mathcal{E}}^{\leftarrow }(⟨{\mathcal{E}}^{\prime },{\mathcal{B}}^{\prime },{\mathcal{C}}^{\prime }⟩,⟨\mathcal{E},\mathcal{B},\mathcal{C}⟩)$
2. Otherwise:
   1. Let $v$ be the local
   2. Perform $joi{n}_v^{\leftarrow }(⟨\mathcal{B},\mathcal{C}⟩,⟨{\mathcal{B}}^{\prime },{\mathcal{C}}^{\prime }⟩)$
   3. Perform $joi{n}_v^{\leftarrow }(⟨{\mathcal{B}}^{\prime },{\mathcal{C}}^{\prime }⟩,⟨\mathcal{B},\mathcal{C}⟩)$

We define $joi{n}_{\mathcal{E}}^{\leftarrow }(⟨\mathcal{E},\mathcal{B},\mathcal{C}⟩,⟨{\mathcal{E}}^{\prime },{\mathcal{B}}^{\prime },{\mathcal{C}}^{\prime }⟩)$ as:

1. Let $\overline{p_{collapsed}}=\varnothing$
2. For each expansion $e^{\prime }\in {\mathcal{E}}^{\prime }$ (shortest first):
   1. Let $p^{\prime }$ be the base of $e^{\prime }$
   2. If there exists a $p\in \overline{p_{collapsed}}$ where $p$ is a prefix of $p^{\prime }$, then ignore this expansion
   3. Otherwise, let $\overline{e}$ by the set of (direct) expansions from $e^{\prime }$ in $\mathcal{E}$
   4. If $e^{\prime }\in \overline{e}$:
      1. Perform $joi{n}_{e^{\prime }}^{\leftarrow }(⟨\mathcal{E},\mathcal{B},\mathcal{C}⟩,⟨{\mathcal{E}}^{\prime },{\mathcal{B}}^{\prime },{\mathcal{C}}^{\prime }⟩)$
   5. Otherwise, if $\overline{e}$ is empty and $\mathcal{C}[p^{\prime }]=c$:
      1. If ${\mathcal{C}}^{\prime }[p^{\prime }]=c^{\prime }$:
         1. Perform $expan{d}^{\leftarrow }(e^{\prime },⟨c,\mathcal{B},\mathcal{C}⟩,⟨c^{\prime },{\mathcal{B}}^{\prime },{\mathcal{C}}^{\prime }⟩)$
      2. Otherwise, perform a normal expansion operation of $e^{\prime }$ in $\mathcal{E}$
   6. Otherwise, perform $joi{n}_{e^{\prime }}^{\leftrightarrow }(⟨\mathcal{E},\mathcal{B},\mathcal{C}⟩,⟨{\mathcal{E}}^{\prime },{\mathcal{B}}^{\prime },{\mathcal{C}}^{\prime }⟩)$
      1. If the result of the join is to collapse to $p^{\prime }$, then add $p^{\prime }$ to $\overline{p_{collapsed}}$

We define $expan{d}^{\leftarrow }(e,⟨c,\mathcal{B},\mathcal{C}⟩,⟨c^{\prime },{\mathcal{B}}^{\prime },{\mathcal{C}}^{\prime }⟩)$ as:

1. If $c\bigsqcup c^{\prime }=c^{\prime \prime }$
   1. Add expansion $e$ to $\mathcal{E}$
   2. Perform $joi{n}_{e^{\prime }}^{\leftarrow }(⟨\mathcal{E},\mathcal{B},\mathcal{C}⟩,⟨{\mathcal{E}}^{\prime },{\mathcal{B}}^{\prime },{\mathcal{C}}^{\prime }⟩)$
2. Otherwise, if $c=R$:
   1. Let $p$ be the base of $e$
   2. Perform $joi{n}_{p_{RW}}^{\leftarrow }(p,\mathcal{B},\mathcal{C})$
3. Otherwise do nothing

Expansion Edge One-Way Join $joi{n}_e^{\leftarrow }$

We define $joi{n}_e^{\leftarrow }(⟨\mathcal{E},\mathcal{B},\mathcal{C}⟩,⟨{\mathcal{E}}^{\prime },{\mathcal{B}}^{\prime },{\mathcal{C}}^{\prime }⟩)$ as:

1. For each place $p$ in the expansion of $e$:
   1. Perform $joi{n}_p^{\leftarrow }(⟨\mathcal{E},\mathcal{B},\mathcal{C}⟩,⟨{\mathcal{E}}^{\prime },{\mathcal{B}}^{\prime },{\mathcal{C}}^{\prime }⟩)$

Expansion Edge Two-Way Join $joi{n}_e^{\leftrightarrow }$

We define $joi{n}_e^{\leftrightarrow }(⟨\mathcal{E},\mathcal{B},\mathcal{C}⟩,⟨{\mathcal{E}}^{\prime },{\mathcal{B}}^{\prime },{\mathcal{C}}^{\prime }⟩)$ as:

1. Let $p$ be the base of $e$
2. If $\mathcal{C}[p]=R$ and ${\mathcal{C}}^{\prime }[p]=R$:
   1. Perform a regular expand of $e$
3. Otherwise, if there exists a descendant of $p$ in ${\mathcal{E}}^{\prime }$ that does not have a capability:
   1. Insert $e$ into $\mathcal{E}$ (do not change capabilities)
4. Otherwise:
   1. Collapse $\mathcal{E},\mathcal{C}$ and ${\mathcal{E}}^{\prime },{\mathcal{C}}^{\prime }$ to $p$

Place Join $joi{n}_p^{\leftarrow }$

We define $joi{n}_p^{\leftarrow }(⟨\mathcal{E},\mathcal{B},\mathcal{C}⟩,⟨{\mathcal{E}}^{\prime },{\mathcal{B}}^{\prime },{\mathcal{C}}^{\prime }⟩)$ as:

1. If $p$ is not a leaf in $\mathcal{E}$ or $p$ is not a leaf in ${\mathcal{E}}^{\prime }$ or $p\notin \mathcal{C}$ or $p\notin {\mathcal{C}}^{\prime }$:
   1. Abort
2. Otherwise, let $c=\mathcal{C}[p]$, $c^{\prime }={\mathcal{C}}^{\prime }[p]$
3. If $c⩾R$ and $c^{\prime }=R$:
   1. Perform $cop{y}_R^{\leftarrow }(p,C,C^{\prime })$
4. If $c=R$ and $c^{\prime }=W$:
   1. Perform $joi{n}_{p_{RW}}^{\leftarrow }(p,\mathcal{B},\mathcal{C})$
5. If $c=E$ and $c^{\prime }=W$:
   1. Perform $cop{y}^{\leftarrow }(p.+,C,C^{\prime })$

Leaf RW Join $joi{n}_{p_{RW}}^{\leftarrow }$

We define $joi{n}_{p_{RW}}^{\leftarrow }(p,\mathcal{B},\mathcal{C})$ as:

1. Label all postfixes places of $p$ in $\mathcal{B}$
2. $\mathcal{C}[p]=W$

Place Capabilitiies Join

The algorithm join($\mathcal{C},{\mathcal{C}}^{\prime }$) is defined as:

1. For each p: c in $\mathcal{C}$:
   1. If $p\notin {\mathcal{C}}^{\prime }$:
      1. Remove capability to $p$ in $\mathcal{C}$
   2. Otherwise:
      1. If $min(c,{\mathcal{C}}^{\prime }[p])$ is defined:
         1. Assign capability $min(c,{\mathcal{C}}^{\prime }[p])$ to $p$ in $\mathcal{C}$
      2. Otherwise, remove capability to $p$ in $\mathcal{C}$

Borrow State Join

1. The borrow graphs are joined
2. The validity conditions are joined

Borrow PCG Join

Joining ${\mathcal{B}}^{\prime }$ into $\mathcal{B}$, where $b$ is the block for $\mathcal{B}$ and $b^{\prime }$ is the block for ${\mathcal{B}}^{\prime }$.

Update the validity conditions for each edge $e$ in ${\mathcal{B}}^{\prime }$ to require the branch condition $b^{\prime }\to b$.

Update the validity

1. If $b$ is a loop head perform the loop join algorithm as described here.
2. Otherwise:
   1. For each edge $e^{\prime }$ in ${\mathcal{B}}^{\prime }$:
      1. If there exists an edge $e$ of the same kind in $\mathcal{B}$
         1. Join the validity conditions associated with $e$ in ${\mathcal{B}}^{\prime }$ to the validity conditions associated with $e$ in $\mathcal{B}$
      2. Otherwise, add $e$ to $\mathcal{B}$
   2. For all placeholder lifetime projections $\hat{p}\downarrow r\text{at}\text{FUTURE}$ in $\mathcal{B}$:
      1. Label all lifetime projection nodes of the form $\hat{p}\downarrow r$ in $\mathcal{B}$ with $\text{FUTURE}$

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 Places

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 - Obtain Relevant Loop Nodes in Pre-state Graph

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 performing the obtain operation on each place 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}$