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: $bb0 \to bb1$ and $bb0 \to 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 P (D)$ of branch choices. For example, one path of execution to bb4 can be described by: $bb0 \to bb2 \to bb3 \to 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 $bb2 \to bb3$ .

We represent validity conditions $pc$ as a partial function $B \to 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$

TODO: Explain how validity conditions are initially determined when creating a new edge at a basic block (inherent VCs). Describe the join informally.

Formal Definition

Validity conditions $pc \in I$ is a map $B \to P (B)$ describing control-flow conditions. For each block $b \in 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] = {\emptyset pc_{i} [b] \cup pc_{j} [b] if pc_{i} [b] \cup pc_{j} [b] = succ_{real} (b) otherwise$

Validity conditions $pc$ are valid for a path $b_{0}, \dots, b_{n}$ iff:

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

The intuition behind the first case of the join is that if whether a borrow is live does not depend on what successor is taken from some basic block $b$ , then it is not necessary to store a predicate about $b$ .

This is kind of an optimization, actually removing this case for the join would not have any difference on whether the resulting validity conditions are valid for any block. In the implementation this is useful so we can have a canonical representation (and also reduces the size of the data structure).

Keyboard shortcuts

PCG Documentation

Validity Conditions

Formal Definition