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.