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 3-tuple containing a Latest Map describing the latest locations of each place; 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. The Borrows Graph is represented as a set of PCG hyperedges.

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 ↩

Capabilities

There are four types of capabilites:

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.

ShallowExclusive (e)

This is used for a rather specific and uncommon situation. When converting a raw pointer *mut T into a Box<T>, there is an intermediate state where the memory for the box is allocated on the heap but the box does not yet hold a value. We use ShallowExclusive to represent this state.

Writing to a Box-typed place p via e.g. *p = 5 requires that p have capability e.

Choosing Place Labels

When the PCG analysis labels a place, all references to the current version of the place (i.e. not within already labelled places) are labelled with a label corresponding to the last time the place could have been updated.

To accomplish this, the PCG uses a data structure called the Latest Map to track, for each place, the most recent location where it could have been updated.

The Latest Map

The Latest Map $\mathcal{L}$ is a partial map from places to labels.

The function $latest(p)$ is defined as follows:

$$latest(p)=\{\begin{array}{ll}\mathcal{L}[p^{\prime }]& \text{if there exists a}{p}^{\prime }\in \mathcal{L}\text{where}{p}^{\prime }\text{is a prefix or a postfix of}p\\ \mathtt{start}bb0& \text{otherwise}\end{array}$$

We note that for each place $p$, either $\mathcal{L}$ does not contain any place that is either a prefix or postfix of $p$, or it contains exactly one such place. This is ensured by construction.

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). ↩

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. ↩

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 }$.

Lifetime Projections

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 $\overline{d}\in \mathcal{P}(D)$ of branch choices. 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

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 strict 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]=\{\begin{array}{ll}\varnothing & \text{if }{pc}_i[b]\cup {pc}_j[b]={\text{succ}}_{real}(b)\\ {pc}_i[b]\cup {pc}_j[b]& \text{otherwise}\end{array}$$

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]$$

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. ↩

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. The entry for p in the latest map is updated to the current location
   2. Function call abstraction edges are described using the rules defined here
3. If the statement takes the form Assign(p, r):
   1. The entry for p in the latest map is updated to the current location
   2. p is given exclusive permission
   3. 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$.
   4. 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\}$
   5. 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 location of p_f in the latest map
         4. Add a Move edge $\{p_f\text{at}\ell \downarrow r_f\}\to \{p\downarrow r\}$
   6. 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\}$
   7. 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. ↩

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}$

The algorithm $joi{n}_{\mathcal{E}}(\mathcal{E},{\mathcal{E}}^{\prime },\mathcal{C},{\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 capabilities $\mathcal{C}$.

1. Let ${\mathcal{E}}^{\prime \prime }$ be an ordered list of the expansions in ${\mathcal{E}}^{\prime }$ sorted in order of ascending length of the projections of their base place
2. For each $\overline{p^{\prime }}$ in ${\mathcal{E}}^{\prime \prime }$:
   1. Let $p^{\prime }$ be the base of $\overline{p^{\prime }}$.
   2. If there exists a $\overline{p}\in \mathcal{E}$ where the base of $\overline{p}$ is $p^{\prime }$:
      1. If $\overline{p}\ne \overline{p^{\prime }}$
         1. Perform collapse($p^{\prime }$, $\mathcal{E}$, $\mathcal{C}$)
         2. Otherwise do nothing (go back to the top of the loop)
   3. Otherwise, if $\mathcal{E}$ contains an expansion $\overline{p}$ and $p^{\prime }\in \overline{p}$:
      1. Add $\overline{p^{\prime }}$ to $\mathcal{E}$
      2. If $p^{\prime }\in {\mathcal{C}}^{\prime }$:
         1. Assign capability ${\mathcal{C}}^{\prime }[p^{\prime }]$ to $p^{\prime }$ in $\mathcal{C}$
         2. Otherwise, remove capability to $p^{\prime }$ in $\mathcal{C}$
      3. For each $p^{\prime \prime }\in \overline{p^{\prime }}$:
         1. If $p^{\prime \prime }\in {\mathcal{C}}^{\prime }$:
            1. Assign capability ${\mathcal{C}}^{\prime }[p^{\prime \prime }]$ to $p^{\prime \prime }$ in $\mathcal{C}$
            2. Otherwise, remove capability to $p^{\prime \prime }$ in $\mathcal{C}$

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 latest maps are joined
3. 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 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$.

Function Calls

Consider a function call $p_{result}=f(o_1,\dots ,o_n)$. Each $o_i\in \{o_1,\dots ,o_n\}$ is an operand of the form move p | copy p | const c. Let $\overline{p}$ be the set of moved operand places, and let $latest(p)$ denote the program point where $p$ was last modified.

The function call abstraction is created in the PostMain evalution stage, after all of the operands have been evaluated. Therefore, all places in $\overline{p}$ are labelled, as they have been moved-out by this point.

Creating the Function Call Abstraction Graph

The PCG constructs a function call abstraction graph $\mathcal{A}$ to reflect the effect of the call.

We begin by determining how $f$ may manipulate the borrows in $f$ by constructing the bipartite graph ${\mathcal{A}}_0$ as follows:

The function call abstraction graph $\mathcal{A}$ is constructed by adding to ${\mathcal{A}}_0$ edges such that for every lifetime $r$ in $p_{result}$, we define the set $S_r=\{p\downarrow r|p\downarrow r\text{is a leaf in}{\mathcal{G}}_0\}$, and add a BorrowFlow edge $S_r\to \{p_{result}\downarrow r\}$.

Adding the Function Call Abstraction Graph to the PCG

We add an abstraction graph $\mathcal{A}$ to a PCG ${\mathcal{G}}_0$ to create a new PCG $\mathcal{G}$ as follows.

First, we initialize $\mathcal{G}$ as $\mathcal{A}\cup {\mathcal{G}}_0$. For each projection $p\downarrow r$ in $RP$, we modify $\mathcal{G}$ as follows:

1. For each endpoint in ${\mathcal{G}}_0$ whose target is $p\downarrow r$, redirect the target to $\tilde{p}\downarrow r\mathtt{at}\mathtt{PRE}$.
2. For each Future edge $p\downarrow r\to p^{\prime }\downarrow r^{\prime }\mathtt{at}\mathtt{Future}$ in ${\mathcal{G}}_0$, remove the edge, and for each leaf $n$ in ${\mathcal{G}}_0$ with an ancestor $\tilde{p}\downarrow r\mathtt{atPRE},insertthe‘Future‘edge${n} \rightarrow p' \downarrow r' to $\mathcal{G}$.
3. Remove $p\downarrow r$ from $\mathcal{G}$.

Misc (To Update)

Unpacking Places

An unpack operation introduces an Unpack edge into the graph, and is associated with a source place $p$ and an expansion $\overline{p}$. An unpack operation can either be mutable or read-only.

An unpack operation is a dereference unpack for lifetime $r$ iff the type of the source place p is &'r mut p or &'r p.

Applying an unpack operation introduces an Unpack edge as follows:

1. If the unpack operation is a dereference operation, the edge $\{p,p\downarrow r\}\to \{\ast p\}$ is added to the graph.
2. Otherwise, the edge $\{p\}\to \{\overline{p}\}$ is added to the graph.

A mutable unpack operation for capabiliy $c\in \{W,E\}$ requires that the source place $p$ have capability $c$. When the operation is a applied, the capability for $p$ is removed and the capability of all places in $\overline{p}$ is set to $c$.

A read-only unpack operation requires that $p$ have capability $R$ and assigns capability $R$ to all places in $\overline{p}$.

Updating Lifetime Projections

Assume the source place $p$ has type $\tau$ with lifetimes $r_1,\dots ,r_n$. If the unpack operation is mutable, then we label each lifetime projection $p\downarrow r_i$ with location $l$.

The source lifetime projection for a lifetime $r$ is $p\downarrow r\mathtt{at}l$ if the unpack is mutable, and $p\downarrow r$ otherwise. The target lifetime projections is the set $\{p^{\prime }\downarrow r|p^{\prime }\in \overline{p}\text{and}r\text{is in the type of}{p}^{\prime }\}$.

For each lifetime $r\in \{r_1,\dots ,r_n\}$, if the set of target lifetime projections associated with $r$ is nonempty:

1. For each $t$ in the set of target projections, add a BorrowFlow edge $\{s\}\to \{t\}$ where $s$ is the source projection¹.

2. If the unpack is mutable and the source place of the expansion is either a reference or a borrowed place: a. Add a Future edge $\{s\}\to \{p\downarrow r\mathtt{atFuture}\}$ b. For each $t$ in the set of target projections, add a Future edge $\{t\}\to \{p\downarrow r\mathtt{atFuture}\}$ c. If any Future edges originate from the source projection $s$, redirect them such that they originate from $p\downarrow r\mathtt{atFuture}$.

Origin Containg Loan

An origin $r$ contains a loan $r_L$ created at location $l$ iff:

Polonius: Read directly from output facts

NLL: $r_L$ is live at $l$ and $r_L$ outlives $l$

1. TODO: Currently we actually introduce an unpack edge in the implementation, but we should change this. ↩

PCG Operations

Obtaining Capability to a Place

The obtain(p, o) operation reorganizes a PCG state to a new state in where the PCG node for a place $p$ is present in the graph. The parameter o is an Obtain Type which describes the reason for the expansion. The reason $o$ is either:

• To obtain a specified capability to the place
• To access the place because it is the borrowed place of a two-phase borrow

An Obtain Type is associated with a result capability $c$ which is either the specified capability (in the first case), or Read (in the case of access for two-phase borrows).

Note that a place node for $p$ is not necessarily present in the graph before this occurs.

This operation is implemented as PcgVisitor::obtain (see https://github.com/viperproject/pcg/blob/main/src/pcg/visitor/obtain.rs)

This proceeds as follows:

Step 1 - Upgrading Closest Ancestor From R to E

This step is included to handle a relatively uncommon case (see the Rationale section below).

If the obtain operation is called with permission $W$ or $E$ and the closest ancestor $p^{\prime }$ to $p$, that is, the longest prefix of $p$ for which there exists a node in the graph, has $R$ capability, we upgrade $p^{\prime }$'s capability to $E$ in exchange for removing capability to all pre- and postfix places of $p^{\prime }$ in the graph (excluding $p^{\prime }$ itself).

This is sound because if we need to obtain non-read capability to place, and there are any ancestors of place in the graph with R capability, one such ancestor originally had E capability was subsequently downgraded. This function finds such an ancestor (if one exists), and performs the capability exchange.

Rationale

It's possible that we want to obtain exclusive or write permission to a field that we currently only have read access for. For example, consider the following case:

• There is an existing shared borrow of (*c).f1
• Therefore we have read permission to *c, (*c).f1, and (*c).f2
• Then, we want to create a mutable borrow of (*c).f2
• This requires obtaining exclusive permission to (*c).f2

We can upgrade capability of (*c).f2 from R to E by downgrading all other pre-and postfix places of (*c).f2 to None (in this case c and *c). In the example, (*c).f2 is actually the closest read ancestor, but this is not always the case (e.g. if we wanted to obtain (*c).f2.f3 instead)

Step 2 - Collapse

Then, if a node for $p$ exists in the graph and $p$'s capability is not at least as strong as $c$, collapse the subgraph rooted at $p$ (and obtain capability $c$ for $p$) by performing the collapse(p, c) operation.

collapse

The collapse(p) operation is implemented as follows:

• For each $p^{\prime }$ such that $p$ is a prefix of $p^{\prime }$ (from longest to shortest) and there is a node for $p^{\prime }$ in the graph:
  • perform the Collapse Repack Operation on $p^{\prime }$.
  • For each lifetime ${}^{\prime }r$ in the type of $p^{\prime }$:
    • Create a new lifetime projection node $p^{\prime }\downarrow {}^{\prime }r$
    • For each lifetime projection node $p^{\prime \prime }\downarrow {}^{\prime }r$ where $p^{\prime \prime }$ is an expansion of $p^{\prime }$:
      • Label $p^{\prime \prime }$
      • Create a new BorrowFlow edge $\{p^{\prime \prime }\downarrow {}^{\prime }r\}\to \{p^{\prime }\downarrow {}^{\prime }r\}$

Step 3 - Labelling Lifetime Projections

At this point, if $c$ is $W$, we know that a subsequent operation will mutate $p$. As a result, if there exists a lifetime projection node for $p$ (for example, if $p$ stores a borrow that has since been reborrowed), it will no longer be tied to the current value of $p$. So, we label $p$.

Step 4 - Expand

At this point there should be a node for some prefix $p^{\prime }$ of $p$ in the graph such that $\mathcal{C}[p^{\prime }]⩾c$.

We expand the graph to $p$ (and obtain the capability for $p$) by performing the expandTo(p, o) operation.

expandTo

The expandTo operation is implemented as follows:

• For each strict prefix $p^{\prime }$ of $p$ (from shortest to longest):
  • If expanding $p^{\prime }$ one level adds new edges to the graph, then
    • We expand the lifetime projections of $p^{\prime }$ one level

The operation to expand a place one level is the expandPlaceOneLevel operation, and the operation to expand the lifetime projections one level is expandLifetimeProjectionsOneLevel.

expandLifetimeProjectionsOneLevel

expandLifetimeProjectionsOneLevel is defined with three parameters:

• $p_b$: The place to expand
• $e$: The target expansion of $p_b$
• $o$: The Obtain Type

The operation is implemented as follows:

• Let $\overline{p}$ be the expansion of $p_b$ using $e$
• For each lifetime projection $p_b\downarrow r$ of $p_b$:
  • Let ${\overline{rp}}_r$ be the set of lifetime projections in $\overline{p}$ with lifetime $r$
  • If ${\overline{rp}}_r$ is nonempty¹:
    • We identify the base lifetime projection $r{p}_b$ as follows:
      • Let $l$ be the current snapshot location
      • If $o$ is not an obtain for capability R:
        • $r{p}_b=p_b\downarrow r\text{at}l$
      • Otherwise, if $p_b$ is blocked by a two-phase borrow live at $l$:
        • Let $l^{\prime }$ be the reservation location of the conflicting borrow
        • $r{p}_b=p_b\downarrow r\text{at}{l}^{\prime }$
      • Otherwise, $r{p}_b=p_b\downarrow r$
    • Create a new Borrow PCG Expansion hyperedge $e=\{r{p}_b\}\to {\overline{rp}}_r$

Step 5 - Labelling Lifetime Projections for Projections

Finally, if we are obtaining $W$ or $E$ capability, we can again assume that the intention is to mutate $p$. If there exist any lifetime projection nodes for dereferences of $p$'s fields (or $p$'s fields' fields, and so on...), we encounter the same problem that was described in Step 3. To address this, we label any lifetime projections for dereferences of places for which $p$ is a prefix (*p.f, for example).

1. This could happen e.g. expanding an x : Option<&'a T> to a x@None ↩

Collapsing Owned Places

At the outset of each program point, the collapse_owned_places operation eagerly collapses the Owned PCG.

This operation is implemented as PcgVisitor::collapse_owned_places (see https://github.com/viperproject/pcg/blob/main/src/pcg/visitor/pack.rs

It is implemented as follows:

• For each place $p$ for which there exists a place node (from longest to shortest):
  • If no expansion of $p$ is blocked by a borrow and every expansion of $p$ has the same capability:
    • perform the collapse(p) operation
    • if $p$ has no projection and has $R$ capability, upgrade $p$'s capability to $E$

Activating Two-Phase Borrows

activateTwophaseBorrowCreatedAt

reserveLocation is a function from borrow edges to the MIR location at which the borrow edge was created.

The activateTwophaseBorrowCreatedAt operation takes a single parameter:

• $l$, a MIR location

The operation is implemented as follows:

• If there exists a borrow edge $e=\{p\}\to ps$ in the graph such that l = reserveLocation(e):
  • If there exists a place node for $\ast p$ in the graph:
    • Restore $E$ capability to $\ast p$
  • If $p$ is not owned:
    • Downgrade the capability of every ancestor of $p$ to None
• TODO Logic is bad

Packing Old and Dead Borrow Leaves

The packOldAndDeadBorrowLeaves operation removes leaf nodes in the Borrow PCG that are old or dead (according to the borrow checker).

• $l$: the current MIR location

When analysing a particular location, this operation is performed before the effect of the statement.

Note that the liveness calculation is performed based on what happened at the end of the previous statement.

For example when evaluating:

bb0[1]: let x = &mut y;
bb0[2]: *x = 2;
bb0[3]: ... // x is dead

we do not remove the *x -> y edge until bb0[3]. This ensures that the edge appears in the graph at the end of bb0[2] (rather than never at all).

This operation is implemented as PcgVisitor::pack_old_and_dead_borrow_leaves (see https://github.com/viperproject/pcg/blob/main/src/pcg/visitor/pack.rs

We must first introduce some auxiliary operations:

isDead

isDead(n, l) is true if and only if the borrow checker considers the node $n$ to be dead at MIR location $l.$

removeEdgeAndPerformAssociatedStateUpdates

removeEdgeAndPerformAssociatedStateUpdates is defined with one parameter:

• $e$: the edge to remove

It proceeds as follows:

• For each current place node $p$ that would be unblocked by removing $e$:
  • If $p$ does not have $R$ capability, and $p$ is mutable:
    • Update $\mathcal{L}$ to map $p$ to $\text{after}l$ where $l$ is the current MIR location
• Remove $e$ from the graph
• For each current place node $p$ that is unblocked by removing $e$:
  • Let $c$ be $R$ if $p$ projects a shared reference and $E$ otherwise
  • If $p$ has no capability or $\text{e}$ capability, upgrade its capability to $c$
  • Unlabel each region projection of $p$
• If $e$ is a Borrow PCG Expansion edge:
  • If $e$ is a Dereference Expansion $\{\widetilde{p_s},r{p}_s\}\to p_t$ where $p_t$ is a current place with no lifetime projections:
    • unlabel $r{p}_s$
  • If $e$ has a source node $p_s$ where $p_s$ is a current place:
    • For each place node $p_t$ in the expansion of $e$, label each region projection of $p_t$ with $\text{prepare}l$, where $l$ is the current MIR location
• If $E$ is a Borrow edge; $isDead(e,l)$ where $l$ is the current MIR location; the target of the borrow is a current place $p$; and $p$ has non-zero capability:
  • weaken $p$'s capability to $W$

Main Loop

packOldAndDeadBorrowLeaves proceeds as follows:

• Until the PCG remains unchanged across the following steps:
  • Let $E$ be be the set of edges $e=\overline{n_s}\to \overline{n_t}$ such that either:
    • $e$ is an Borrow PCG Expansion edge and either:
      • for each $n_t$, either:
        • $isDead(n_t,l)$, where $l$ is the current MIR location
        • or $n_t$ is old
      • or $n=p$, any pair of place nodes in $\overline{n_t}$ have the same capability, and for all $n_t$ such that $n_t=p_t$, $p_t$ has the same label as $p$ and $p$ is an exact prefix of $p_t$
      • or $n=p\downarrow {}^{\prime }r$ and for all $n_t$ such that $n_t=p_t\downarrow {}^{\prime }{r}_t$, $p$ is an exact prefix of $p_t$; $p$ and $p_t$ have the same label; and ${}^{\prime }r$ and ${}^{\prime }{r}_t$ have the same label.
    • or for each $n_t$, where $n_t=\hat{p}$ or $n_t=\hat{p}\downarrow ..$, either:
      • $\hat{p}$ is old
      • or $\hat{p}$'s associated place is not a function argument and either:
        • $\hat{p}$ has a non-empty projection and $n_t$ is not blocked by an edge
        • or $isDead(n_t,l)$, where $l$ is the current MIR location
  • For each $e$ in $E$:
    • perform removeEdgeAndPerformAssociatedStateUpdates(e)

Repack Operations

Repack operations describe actions on owned places.

RegainLoanedCapability

Fields:

• $p$ - Place
• $c$ - Capability

This operation is used to indicate that $p$ is no longer borrowed, and can therefore be restored to capability $c$.

Applying RegainLoanedCapability

The PCG applies this operation by setting the capability of $p$ to $c$.

DerefShallowInit

Fields:

• $p_f$ - From Place
• $p_t$ - To Place

This operation is used to indicate that a $p_f$ (which is a shallow-initialized box) was dereferenced.

Applying DerefShallowInit

Let $\overline{p}$ be the expansion of $p_f$ obtained by expanding towards $p_t$.

The PCG applies this operation by adding read capability to the places in $\overline{p}$

Collapse

Fields: