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