regions.dl

.type region
.type borrow
.type point

///////////////////////////////////////////////////////////////////////////
// -- inputs --

.decl borrowRegion( r:region, b:borrow, p:point )
.input borrowRegion
.decl nextStatement( from:point, to:point )
.input nextStatement
.decl goto( from:point, to:point )
.input goto
.decl regionLiveOnEntryToStatement( r:region, p:point )
.input regionLiveOnEntryToStatement
.decl killed( b:borrow, p:point )
.input killed
.decl outlives( p:point, r_a:region, r_b:region, q:point )
.input outlives

///////////////////////////////////////////////////////////////////////////
// -- analysis --

///////////////////////////////////////////////////////////////////////////
.decl cfgEdge( p:point, q:point )

cfgEdge(P, Q) :- nextStatement(P, Q).
cfgEdge(P, Q) :- goto(P, Q).

///////////////////////////////////////////////////////////////////////////
.decl regionLiveAt( r:region, p:point )

regionLiveAt(R, P) :-
  regionLiveOnEntryToStatement(R, P).

// Propagate across basic blocks.
regionLiveAt(R, P) :-
  goto(P, Q),
  regionLiveOnEntryToStatement(R, Q).

///////////////////////////////////////////////////////////////////////////
// `restricts(R, B, P)`
//
// True if data live references with the region R, at the point P, may
// still reference data found in the path borrowed by B. This is
// different in a quite subtle way from a naive points-to analysis: in
// particular, if the path which was borrowed is modified to now refer
// to some place else, then a naive points-to would be true, but this
// relation is false. Consider this:
//
//     let cursor: &'C mut Data;
//     let x: &'X mut Data = &mut *cursor; // Point X; Borrow B
//     cursor = ...;                       // Point Y (kills B)
//     use(x);                             // Point Z
//
// Here, at the point X, a borrow B is introduced of `*cursor`. But at
// point Y, `cursor` is changed to point at something else. This is
// called "killing" the borrow `B`, because `*cursor` no longer refers
// to the same data.  Hence, at point Z, the fact that `x` is live no longer
// implies restrictions on what we can do with `cursor` -- so we say that the
// region `X` no longer restricts the borrow `B`.
.decl restricts( r:region, b:borrow, p:point )

// After a `&'R foo` executes, the borrow region `'R` points to that borrow.
restricts(R, B, P) :-
  borrowRegion(R, B, P).

// If we have `R1: R2 @ P`, this means that data with lifetime R1 is flowing
// into a place typed as R2; hence R2 points to everything that R1 points at.
restricts(R1, B, Q) :-
  outlives(P, R2, R1, Q), // P establishes R2: R1, means data from R2 flows into R1
  restricts(R2, B, P),  // R2 points at B on entry, so R1 will point at B on exit...
  !killed(B, P).       // ...unless B is killed by this statement (no more path
                       // to the data it refers to)

// Carry points to across edges, as long as region is live across that edge.
//
// Note assumption: if you have `x = ...`, then regions in `x` are dead
// on entry to that statement (P).
restricts(R1, B, Q) :-
  restricts(R1, B, P),  // On entry R1 pointed at B, so will point at B on exit...
  !killed(B, P),       // ...unless B is killed by this statement (no more path
                       // to the data it refers to)
  cfgEdge(P, Q), // P is the point before effects happen, Q is point after
  regionLiveAt(R1, Q). // Region is live at the end of the statement

///////////////////////////////////////////////////////////////////////////
.decl borrowLiveAt( b:borrow, p:point )
.output borrowLiveAt

// A borrow is live if any of the regions that may reference it
// are live at that particular point.
borrowLiveAt(B, P) :-
  regionLiveAt(R, P),
  restricts(R, B, P).