Generating Annotations for Magic Wands

Clients like Prusti want to generate magic wands from function bodies.

The PCG facilitates this via the UnblockGraph interface. The interface takes a PCG $\mathcal{G}$ and a PCG node $n$, and returns an ordered list $L$ of annotations that describe how to unblock $n$ in $\mathcal{G}$. Prusti can consume these annotations to generate magic wands.

The annotations generated from the UnblockGraph are Borrow PCG edges.

At a high level, the resulting annotations are a topological sort of the edges in the subgraph of $\mathcal{G}$ that contains $n$ and all of its ancestors. Concretely, the procedure to generate the list $L$ of annotations is as follows:

1. Let $\mathcal{U}$ be the subgraph containing $n$ and its ancestors in $\mathcal{G}$
2. While $\mathcal{U}$ has at least one edge:
   1. Let $\overline{e}$ be the set of leaf edges in $\mathcal{U}$.
   2. If $\overline{e}$ is empty fail
   3. Append $\overline{e}$ to $L$
   4. Remove $\overline{e}$ from $\mathcal{U}$

We note that the above procedure could fail, for example, $\mathcal{U}$ could contain a cycle. We expect that in practice this is quite rare. Furthermore, we believe the following property should hold:

Therefore, it should be possible to modify the implementation to e.g. produce multiple lists for distinct paths.