Google Drive
Gist
Clipboard
One of my goals for the year is that we have a prototype of polonius working on nightly. We've made good progress, and in a recent meeting Remy, Amanda Stjerna and I were discussing how we might make the next steps. One of the ideas was to try and implement the polonius revisited analysis in a reasonably naive way just to try it out and gain experience. This blog post is me braindumping how we might do that.
In the location insensitive Polonius, there is a single set of variables associated with the current MIR, and those variables have exactly one type. We'll just write Ty(X) to mean that type.
When we talk about a loan L, we mean some borrow expression &<place> in the MIR. We typically talk about origins as a set of loans. However, in the implementation, it's convenient to say that each loan has a characteristic origin O_L, which we typically write as part of the expression &'O_L <place>. Now we know that if O_L is a subset O_L : O of some origin O, then O contains the loan L. Another way to look at this is that loans are just a designated subset of origins, and the "value" of an origin O is the set {O_L} of loan origins where O_L : O (transitively) in the subset graph.
Our existing, flow-insensitive polonius integration has roughly this shape:
flowchart TD
MIR --> TypeCheck
MIR --> Liveness
TypeCheck -- emits --> RegionConstraints
Liveness -- emits --> LiveLoans
RegionConstraints --> SubsetGraphConstruction --> SubsetGraph
SubsetGraph --> Liveness
LiveLoans --> Dataflow
Dataflow --> ActiveLoans
ActiveLoans --> DetectErrors
MIR[(MIR)]
RegionConstraints[("Region constraints:\nRC = a set {O1:O2 @ P}")]
SubsetGraph[("Subset graph:\nSG = a set {O1:O2}")]
LiveLoans[("Live loans:\nLL = a set {L @ P}")]
ActiveLoans[("Active loans:\nAL = a set {L @ P}")]
SubsetGraphConstruction["
Derive SG by removing points from region constraints.
SG = { (O1 : O2) | (O1:O2 @ P) ∈ RC }
"]
Liveness["
Liveness analysis where a loan L is live at P
if there is a live variable X at P
whose type Ty(X) contains an origin O
and (L : O) in the subset graph SG.
"]
Dataflow["
Dataflow analysis where a loan is
GEN when it is issued and
KILL when it is no longer live or
the place that was borrowed is reassigned
"]
DetectErrors["
Traverse the MIR and check the places
accessed by a statement to see if they
constrained by any active loan.
"]
This is how the new analysis will look:
flowchart TD
MIR --> TypeCheck
MIR --> Liveness
TypeCheck -- emits --> RegionConstraints
ComputeLiveVars -- emits --> LiveVariables
Liveness -- emits --> LiveLoans
RegionConstraints --> SubsetGraphConstruction --> SubsetGraph
SubsetGraph --> Liveness
LiveLoans --> Dataflow
Dataflow --> ActiveLoans
LiveVariables --> Liveness
LiveVariables --> SubsetGraphConstruction
ActiveLoans --> DetectErrors
MIR[(MIR)]
RegionConstraints[("Region constraints:\nRC = a set {r1:r2 @ P}")]
SubsetGraph[("Subset graph:\nSG = a set {r1@P : r2@P}")]
LiveLoans[("Live loans:\nLL = a set {L @ P}")]
ActiveLoans[("Active loans:\nAL = a set {L @ P}")]
LiveVariables[("Live variables:\nLV = a set {X @ P}")]
Dataflow["
Dataflow analysis where a loan is
GEN when it is issued and
KILL when it is no longer live or
the place that was borrowed is reassigned
"]
Liveness["
Liveness analysis where a loan L is live at P if
there is a live variable X at P ((X, P)∈LL)
whose type contains an origin O (X : O)
and O contains L at P ((O@P : L@P) ∈ SG)
"]
DetectErrors["
Traverse the MIR and check the places
accessed by a statement to see if they
constrained by any active loan.
"]
In the blog post, I described having a distinct type for each variable at each program point. In practice, we'll implement that a bit differently. Just as in the location insensitive analysis, there will be one environment {X:T} where each variable X has a type T that references (location-independent) origins. But when we construct the subset graph, we will consider the nodes of the graph to be a origin at a point, i.e., O@P, where a point P is either a statement or a terminator. Points can be uniquely identified by BB/N, i.e., the name of a basic block and an index.
What this means in practice is that we can reuse the existing MIR type check machinery. We can also continue to write Ty(X) to refer to the type T of X, since there is only a single environment. But whenever we add things into the subset graph, we will have to localize that type T to a particular point. We write T @ P to mean "the type T but with every origin O in that type replaced with O @ P".
Efficiency note: This does mean that the number of origins is now (in principle) a function of the number of statements. In real life, this will be the biggest source of overhead. I believe we can do a lot to reduce this, but that's not the focus of this post.
The subset graph in the location sensitive analysis is much richer. Instead of just relating two origins, it relates origins at particular points. This means that a node in the graph is effectively a 64-bit quantity, with 32 bits for the origin index and 32 bits for the point. This also means that the graph will be conceptually much larger, now being of size |O| * |CFG| rather than just |O|. I believe we can reduce the number of nodes we actually need in practice with some optimizations, but that's not the subject of this post.
Even though the graph has a lot of nodes, we never need to represent the set of nodes explicitly. We only care about the edges. So we can represent the raw graph as a set of edges O1@P1 : O2@P2 which is basically a Map<u64, Vec<u64>> (a sorted vec of tuples might even be good in practice).
In practice we don't use raw origins in the compiler. Rather, we take that naive graph and then detect strongly connected components (SCCs). This makes for a more compact graph since all cycles become a single node. The SCC code exists already and is quite generic, though it may need some slight tweaks.
Given this SG representation, given two origins O1 and O2 and two points P1 and P2, we can determine whether O1@P1 : O2@P2 by
S1 = SCC(O1@P1) for O1@P1S2 = SCC(O2@P2) for O2@P2S1 ~~> S2There are two kinds of edges we have to include in the variable graph. The first kind are the edges due to variable liveness.
Note that, in the old analysis, the subset graph constructed was based purely on the output of MIR type check. In the new analysis, it also needs to know the set {X} of live variables at each point P. If there is a control-flow edge P1 -> P2 between two points, and a variable X is live at both P1 and P2, then we need to relate Ty(X) @ P1 and Ty(X) @ P2.
In fact, because the types have the same "spine", all we really need to know is the variance of Ty(X) with respect to each contained origin O. We can then add edges into the graph between O@P1 and O@P2 based on that:
O@P1 : O@P2O@P2 : O@P1Type check emits constraints of the form O1 : O2 @ P. We can basically translate these to an edge (O1 @ P) : (O2 @ P) in the subset graph, but there is one subtlety. As discussed in the previous polonius post, when we are doing an assignment we have to relate the types on entry to the type of the place on output. Distinguishing this properly will probably require some tweaks to the compiler — ideally I think we would change the region constrains to actually track both points, so that we can represent this difference explicitly.
In MIR, there are actually two places assignments occur. One of them is in statements but the other is in terminators – the final part of a basic block, which can have multiple successors. This sounds like it might present a challenge, but in fact, for each of these terminators that do assignments, the assignments only occur on one branch (in the case of a call, the "success" branch that indicates no panic occurred). So when relating the return type of a function to its target place, we can use the type of the targt place in the "success" branch.
The ultimate representation of the graph that we use is based on the idea of a strongly connected component (SCC),
which is basically a cycle.
The idea is that you can reduce any graph to a DAG where the nodes are SCCs.
To start, I imagine building up a fairly naive representation of the full subset graph.
Note that the set of nodes in the graph does not need to be represented explicitly.
We can effectively represent a node type Node = u64 using a 64-bit integer, where 32 bits are the O and 32 bits are the P.
Then we can represent the graph as just a list of edges (Map<Node, Vec<Node>>).
The process for computing live loans is very similar to what we did before. If a variable X is live on entry to a program point P we can look at each origin O that appears in its type Ty(X). We can walk backwards through the subset graph for O@P to compute the set of loan predecessors. Those are the live loans at that point.
We can compute this set by a single walk of the SCC DAG. We track for each SCC a (bit)set of loans. We start walking at SCC node and visit each of its children, returning back a set of loans that get unioned together. We also include the loans directly contained in the SCC.
Computing active loans works the same way it did before.
-
Any changes
Be notified of any changes
-
Mention me
Be notified of mention me
-
Unsubscribe
Subscribe