Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

PCG Hyperedges

A PCG Hyperedge is a directed edge of the form , where elements of and are PCG nodes. The set are referred to as the source nodes of the edge, and are the target nodes. Hyperedges in the PCG are labelled with validity conditions1.

We represent a PCG hyperedge as a tuple of an edge kind and validity conditions.

Edge Kinds

An edge kind is a description an edge, including its source and target nodes, as well as other associated metadata. The metadata is described by the type of the edge, the various types are presented below:

Unpack Edges

Unpack edges are used to represent the unpack of an owned place in order to access one of its fields. For example, writing to a field x.f requires expanding x.

An unpack edge connects an owned place to one of it's expansions . Each place in is guaranteed to be owned.

For example, if x is an owned place with fields x.f and x.g, the edge {x} -> {x.f, x.g} is a valid unpack edge.

Unpack edges are not generated for dereferences of reference-typed places. Borrow PCG Expansion Edges are used in such cases. Unpack edges are used in derefences of Box-typed places.

In the implementation, we don't have an explicit data type representing unpack edges. Rather, the unpack edges are conceptually represented as the interior edges in the Owned PCG.

Validity conditions are not currently associated with unpack edges in the implementation.

Borrow PCG Expansion Edge

Borrow PCG Expansion Edges conceptually take one of three forms:

  • Dereference Expansion: The dereference of a reference-typed place
  • Place Expansion: The expansion of a borrowed place to access one of its fields
  • Lifetime Projection Expansion: The expansion of the lifetime projections of an owned or borrowed place

Dereference Expansion

The source nodes of a dereference expansion consist of:

  • A maybe-labelled place , and:
  • A lifetime projection

Where and have the same associated place .

The target node of a dereference expansion is a maybe-labelled place with associated place .

Place Expansion

The source node of a place expansion is a maybe-labelled place with associated place , where is a borrowed place and is not a reference.

The target nodes of a place expansion is a set of maybe-labelled places where the associated places of are an expansion of .

Lifetime Projection Expansion

The source node of a lifetime projection expansion is a lifetime projection where is a maybe-labelled place with associated place of .

The target nodes of a lifetime projection expansion is a set of lifetime projections where the base of each place is a maybe-labelled place. The associated places of the bases of are an expansion of .

It might make sense to differentiate lifetime projection expansions of owned and borrowed places, since they differ in terms of how placeholder labels should be included. Namely, for owned places there is no need to connect the expansion nodes to the placeholder of the base node (the owned place may never be repacked, or could be repacked with entirely unrelated lifetime projections)

Borrow Edges

Borrow edges are used to represent direct borrows in the program. We define two types:

  • Local Borrow Edges: A borrow created in the MIR Body, e.g. from a statement let y = &mut x;
  • Remote Borrow Edges: A borrow created by the caller of this function where the assigned place of the borrow is an input to this function.

Remote Borrows are named as such because (unlike local borrows), the borrowed place does not have a name in the MIR body (since it was created by the caller).

Local Borrows

The source node of a local borrow is a maybe-labelled place . The target node of a local borrow is a lifetime projection where is a maybe-labelled place.

Remote Borrows

The source node of a remote borrow is a remote place . The target node of a remote borrow is a lifetime projection where is a maybe-labelled place.

Abstraction Edge

An abstraction edge represents the flow of borrows introduced due to a function call or loop.

Function Call Abstraction Edge

The source node of a function call abstraction edge is a lifetime projection where is a maybe-labelled place.

The target node of a function call abstraction edge is a lifetime projection where is a maybe-labelled place.

Loop Abstraction Edge

The source node of a loop abstraction edge is a PCG node.

The target node of a loop abstraction edge is a local PCG node.

Borrow-Flow Edge

A borrow-flow edge represents the flow of borrows between a lifetime projection and a local lifetime projection . This edge is used when the relationship between the blocked and target node is known concretely, but does not correspond to an expansion or a borrow.

Borrow-Flow Edges are labelled with a Borrow-Flow Edge Kind with associated metadata, enumerated as follows:

Aggregate

Metadata:

  • : Field Index
  • : Lifetime Projection Index

An aggregate kind is used for borrows flowing into an aggregate type (i.e. struct, tuple). The metadata indicates that the blocked lifetime projection flows into the lifetime projection of the field of the blocking lifetime projection.

Introduced in the following two cases:

  1. Collapsing an owned place:
    • edges flow from the lifetime projections of the labelled places of the base to the lifetime projections of the current base
  2. Assigning an aggregate (e.g. x = Aggregate(a, b)):
    • edges flow from the lifetime projections of the labelled places in the rvalue to the lifetime projections of x

is probably not necessary. We probably don't even need for case 1 (field index can be inferred from the expansion place), so perhaps a different edge kind could be used in that case.

Reference to Constant

Connects a region projection from a constant to some PCG node. For example let x: &'x C = c; where c is a constant of type &'c C, then an edge {c↓'c} -> {x↓'x} of this kind is created. This is called ConstRef in the implementation.

This seems quite similar to "Borrow Outlives", perhaps we should merge them?

Borrow Outlives

For a borrow e.g. let x: &mut y;, the PCG analysis inserts edges of this kind to connect the (potentially snapshotted) lifetime projections of y to the lifetime projections of x.

Initial Borrows

To construct the initial PCG state, the PCG analysis adds an edge of this kind between every lifetime projection in each remote place to the corresponding lifetime projection of its corresponding argument.

For example, if is the local corresponding to a function argument and contains a lifetime projection , an edge will appear in the graph.

Connects the lifetime projections of remote places to the lifetime projections of

Copy

For a copy let x = y;, the PCG analysis inserts edges of this kind to connect the lifetime projections of y to the lifetime projections of x.

In the implementation this is currently called CopyRef.

Move

For a move let x = move y;, the PCG analysis inserts edges of this kind to connect the (potentially snapshotted) lifetime projections of y to the lifetime projections of x.

Future

These edges are introduced to describe the flow of borrows to the lifetime projections of a place that is currently blocked. When they are created, the target node is a placeholder lifetime projection of a blocked place.

Perhaps this should be its own edge type?

  1. Currently not in the owned portion of the PCG, but this should happen eventually.