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