Function Shapes

Background

The PCG generates a "shape" for a function call - a bipartite graph indicating where borrows could flow as a result of the call. In particular this shape represents (1) reborrows that are returned from the function (w.r.t borrows passed in the arguments), and (2) the effects of the nested borrows passed in the operands.

We model the first case by introducing abstraction edges between lifetime projections in the operands and those in the result place: each lifetime projection in the operands is connected to the corresponding lifetime projections that it outlives in the result place. The (compiler-checked) outlives constraint captures whether borrows could be assigned in this way, according to the type system.

For (2) To directly model the potentially changed sets of borrows relevant to these concerns, our analysis of function calls introduces lifetime projections to represent the post-state of each lifetime projection in the operands. Each lifetime projection in the operands is connected with abstraction edges to its corresponding post-state projection as well as the post-state nested lifetime projections that it outlives (analogously to sets of borrows explicitly returned).

Creating Function Shapes

Function Shapes

A function shape source base $B_{S}$ takes the form $arg i$ . A function shape target base $B_{T}$ is either $arg i$ or $result$ .

A function shape source node $N_{B}$ is a pair $⟨ B_{S}, i ⟩$ where $i$ is the region index of the node. Function shape target nodes $N_{T}$ are defined analogously.

A function shape edge is a pair $⟨ N_{B}, N_{T} ⟩$ , and a function shape $S$ is a set of edges.

A shape $S$ permits more borrowing than a shape $S^{'}$ iff $S^{'} \subseteq S$ ; likewise $S$ permits less borrowing than $S^{'}$ iff $S \subseteq S^{'}$ .

Signature Shape

The corresponding node $n (g r p)$ of a generalized lifetime projection $g r p \in GRP (\hat{f})$ is $⟨ base (r p), index (r p) ⟩$ .

The corresponding generalized lifetime projection $g r p (n)$ of a node $n = ⟨ b, i ⟩$ is the generalized lifetime projection $g r p \in GRP (\hat{f})$ such that $n (g r p) = n$ .

A generalized lifetime $g r$ outlives a generalized lifetime $g r^{'}$ in the signature of $\hat{f}$ (denoted $\hat{f} ⊢ g r : g r^{'}$ iff:

$g r = g r^{'}$ , or
$g r$ is a generalized type $τ^{*}$ and $g r^{'}$ is a region $r^{'}$ and $E (\hat{f}) ⊢ g r : r^{'}$

Note that $RegionsIn (τ)$ represents all regions that could occur in $τ$ . More generally, $RegionsIn (τ)$ outlives $RegionsIn (τ^{'})$ when all regions in $τ$ outlive all corresponding regions in $τ^{'}$ . The current implementation handles the case where $τ = τ^{'}$ (reflexivity); other cases may be added in the future.

The signature shape $S_{\hat{f}}^{sig}$ for a function instantiation $\hat{f}$ is defined as follows:

For each $⟨ b_{s} ↓ g r_{s}, b_{t} ↓ g r_{t} ⟩ \in GRP (\hat{f}) \times GRP (\hat{f})$ then add $⟨ n (b_{s} ↓ g r_{s}), n (b_{t} ↓ g r_{t} ⟩)⟩$ to $S_{\hat{f}}^{sig}$ if both:

$\hat{f} ⊢ g r_{s} : g r_{t}$ , and
$b_{t}$ is $result$ , or $g r_{s}$ is a region $r$ that is invariant in $b_{t}$ .

Call Shape

The corresponding node $n (r p)$ of a lifetime projection $o p ↓ r \in RP (FC)$ is $⟨ arg i, index (r p) ⟩$ .

The corresponding node $n (r p)$ of a lifetime projection $p ↓ r \in RP (FC)$ is $⟨ result, index (r p) ⟩$ .

${⟨ base (r p), index (r p) ⟩ ∣ r p \in RP (\hat{f})}$

The call shape $S_{FC}^{call}$ for a function call $FC$ is defined as follows:

For each $⟨ b_{s} ↓ r_{s}, b_{t} ↓ r_{t} ⟩ \in RP (FC) \times RP (FC)$ then add $⟨ n (b_{s} ↓ r_{s}), n (b_{t} ↓ r_{t} ⟩)⟩$ to $S_{FC}^{call}$ if both:

$r_{s} outlives r_{t}$ at $l$ according to the borrow checker, and
$b_{t}$ is $p$ , or $r_{s}$ is invariant in $b_{t}$ .

Type Aliases and Normalization

An alias type $τ_{α}$ is a type of the form $τ :: T ⟨ \overline{τ^{*}} ⟩$ where $T$ is a type constructor. The function $normalize (τ, E)$ returns a type $τ^{'}$ where alias types in $τ$ may possibly be replaced with other types. This normalisation is idempotent, e.g. $normalize (normalize (τ, E), E) = normalize (τ, E)$ .

Signature-Derived Call Shape

For a call $FC = (p = \hat{f} (\overline{o p})$ at $l$ ), the signature-derived call shape $S_{FC}^{sig}$ is obtained as follows:

Let $S_{\hat{f}}^{norm}$ be the normalized signature shape, e.g the one obtained by replacing each $τ$ in $S_{\hat{f}}^{sig}$ with $normalize (τ, E (FC))$ .

If $b$ is the $i^{'} t h$ operand in $FC$ , the corresponding normalized type $τ_{b}$ is the type of the $i^{'} t h$ argument in $S_{\hat{f}}^{norm}$ . Likewise, if $b = result$ , then $τ_{b}$ is the output type of $S_{\hat{f}}^{norm}$ . Then, the corresponding normalized region of a lifetime projection $b ↓ r$ is the region in $τ_{b}$ that corresponds to $r$ in $b$ .

For each $(n_{s}, n_{t}) \in S_{FC}^{call}$ :

Let $b_{s} ↓ r_{s} = r p (n_{s})$ , $b_{t} ↓ r_{t} = r p (n_{t})$ be the corresponding lifetime projections
Then, let $r_{s}^{'}$ and $r_{t}^{'}$ be the corresponding normalized regions of $r_{s}$ and $r_{t}$ respectively.
If $r_{s}^{'}$ outlives $r_{t}^{'}$ in $S_{\hat{f}}^{norm}$ , then add $(n_{s}, n_{t})$ to $S_{FC}^{sig}$

Using shapes for function calls in the PCG

If the call is to a defined function, then the signature-derived call shape is used. Otherwise, the call shape is used.

More Background

For a function $f$ , there are three types of shapes to consider:

Signature Shapes: The shape of an instantiation of $f$ generated from its signature
Call Shapes: A shape used to represent call to an instantiation of $f$
Implementation Shapes: A shape representing $f$ 's body, which connects remote lifetime projection nodes to the the result.

These different shape types are relevant for Prusti, as:

Signature shapes define the shape of a magic wand
Call shapes are used for magic wands that will be applied
Implementation shapes define magic wands that will be packaged

The call shape and implementation shapes are necessarily related to the signature shape; the former can contain more edges while the latter can contain less.

The shape for a function call must necessarily have corresponding edges that appear in the shape for the function signature. The reverse is not necessarily the case. For example, consider the following:

#![allow(unused)]
fn main() {
fn caller<'e, 'f: 'e>(x: T<'e>, y: U<'e>, z: T<'f>) {
    let r: W<'e> = f(x, y, z);
}
}

Using the borrow-checker to generate the shape of the call will result in an edge from z|'f to r|'e: the borrow-checker reflects that 'f: 'e. However, the definition of f do not allow borrows to flow from z to r (which is reflected in the function call shape).

Therefore, to build more precise graphs at function call sites. We want to use the shape of the function to determine the shape of the call. The procedure is as follows:

Generate the shape of the function.
Build a map $M$ from Def Projections to Call Projections by comparing the types of the arg places $T_{p}$ and formal args $T_{a}$ (analogously to the results). By construction, $M$ will contain all projections in the function def (even if they don't appear in the shape).

Here's an example of how its computed:

If the type of the $i$ 'th place $T_{p}$ is &'?1 mut U<'?2> and the type of the $i$ 'th formal arg $T_{a}$ is &'a mut U<'b>, then the visitor will first compare at the top level, add arg_i |'a -> p_i '?1 to the map and continue by comparing U<'?2> to U<'b>

Then, for each edge in the fn shape, the edge is replaced with the corresponding projections of the call. If the fn shape has an edge arg 1|'a -> result|'b for example, then for the call shape it will lookup corresponding call projections and add an edge between them.

Reasoning about Associated Types

Consider the following code:

#![allow(unused)]
fn main() {
trait MyTrait<'a> {
    type Assoc<'b> where 'a: 'b;

    fn get_assoc<'slf, 'b>(&'slf mut self) -> Self::Assoc<'b> {
      todo!()
    }
}
}

The full signature for get_assoc is:

#![allow(unused)]
fn main() {
fn(&'slf mut Self) -> <Self as MyTrait<'a>>::Assoc<'b>
}

we observe that the fn sig has the following lifetime projections:

argidx 0|'slf
result 0|'a
result 0|'b

And the shape for get_assoc contains the single edge:

argidx 0|'slf -> result|'b

For the body, self has type &'8 mut Self/#0 and result has Alias(Projection, AliasTy { args: [Self/#0, '?6, '?7], def_id: DefId(0:5 ~ input[9b88]::MyTrait::Assoc), .. }),

So we unify &'slf mut Self with &'?8 mut Self adding argidx 0|'slf -> _1|'?8 to $M$

We unify <Self as MyTrait<'a>::Assoc<'b> with <Self as MyTrait<'?6>::Assoc<'?7> adding

result|'a -> result|'?6 to $M$
result|'b -> result|'?7 to $M$

Then applying the substitutions our shape is _1|'?8 -> result|'?7

Keyboard shortcuts

PCG Documentation