--- # System prepended metadata title: Purely forward propagation --- # Purely forward propagation ## Intuition * A *loan* is a reference to a place in memory and the conditions it was borrowed (shared, mutable) * An *origin* is a set of loans {L}, such that if a reference has origin O, then we know that: * invaliding one of the loans in {L} may invalidate the reference * actions that do not invalidate any of the loans in {L} cannot invalidate the reference * When we have an access that invalidate some loan L: * We mark any origins that contain L at that point as invalidated * Questions Niko is not sure about * Do we still have to "propagate" subset etc? * What's the best way to think about that :) ## Tentative idea ### State we compute * `subset(O1, O2, N)` -- `O1 <= O2` must hold on entry to the node `N` * `loan_in_origin(L, O1, N)` -- the origin `O` contains the loan `L` on entry to the node `N` * `origin_invalidated(O, N)` -- data with origin `O` is invalidated on entry to the node N ### End goal we are searching for * `invalidated_origin_accessed(O, N)` -- origin `O` which is invalidated was accessed; error ## Rules ### Inputs * `access(O, N)`: access data with origin `O` * `invalidate_loan(L, N)`: invalidate the loan `L` at the node `N` * `clear_loan(L, N)`: the path named in `L` changed without invalidating the underlying memory; subsequence invalidations of `L` do not affect existing references * `clear_origin(O, N)`: all references with origin `O` was overwritten * `introduce_loan(L, O, N)`: introduce the loan `L` into origin `O` at node `N` * Every borrow `&'a place` or `&'a mut place` introduces, for some unique origin `'a`: * one loan in `'a` for the borrow itself * various subset relationships between each origin `O` dereferenced by place and `'a` * `introduce_subset(O1, O2, N)`: require that `O1 <= O2` at node `N` * `cfg_edge(N1, N2)`: control-flow graph edge Note the convention: Input facts are in the imperative mood ("invalidate loan") while computed facts use the past participle ("loan invalidated"). ### Assumptions about ordering For a given node `N`... * First we perform any accesses `access(O, N)` * Then we invalidate any loans `invalidate_loan(L, N)` * Then we clear any loans or origins * Then we introduce any loans, subsets, etc * Then we remove things from scopes This corresponds to ``` place = expr ``` * Evaluating the expr accesses the origins (including potentially some in place) * Then place is overwritten, invalidating and clearing loans * Storing the value also creates subtyping relationships between the type of the value that was stored and the place it was stored into ### Computing subset The `subset(O1, O2, N)` relation indicates that `O1 <= O2` on entry to node `N` ``` subset(O1, O2, N2) :- // Introduced by predecessor cfg_edge(N1, N2), introduce_subset(O1, O2, N1) subset(O1, O2, N2) :- // Carried over from predecessor cfg_edge(N1, N2), subset(O1, O2, N1), !clear_origin(O1, N1), !clear_origin(O2, N1). subset(O1, O3, N1) :- // Transitive closure subset(O1, O2, N1), subset(O2, O3, N1). ``` ### Computing loans in an origin The `loan_in_origin(L, O, N)` relation indicates that the origin `O` contains the node `L` on entry to node `N` ``` loan_in_origin(L, O, N2) :- // Introduced by predecessor cfg_edge(N1, N2), introduce_loan(L, O, N1) loan_in_origin(L, O, N2) :- // Carried over from predecessor cfg_edge(N1, N2), loan_in_origin(L, O, N1), !clear_loan(L, N1), !clear_origin(O, N1), !invalidate_loan(L, N1). loan_in_origin(L, O2, N) :- // Transitive closure subset(O1, O2, N), loan_in_origin(L, O1, N). ``` ### Computing invalidated origins An *origin* is invalidated if it contains some *loan* that has been invalidated. Invalidating a loan is an input fact, `loan_invalidated`, and it takes effect during a node's execution. So we look for origins that (a) contained a loan `L` on entry to some node `N` and (b) the node invalidated the loan `L`. ``` origin_invalidated(O, N2) :- // Introduced by predecessor cfg_edge(N1, N2), loan_in_origin(L, O, N1), invalidate_loan(L, N1). ``` ### Error: access to invalidated origins An error occurs when some node N tries to access data with origin O, but O is invalidated on entry to N. ``` invalidated_origin_accessed(O, N) :- // Introduced by predecessor access(O, N), origin_invalidated(O, N). ``` ## Fact Generation ### Accesses Any read (or write) of a place `P` counts as an access of * any origin in the type of `P`. * For example, using a `&'outer Vec<&'inner u32>` accesses both `'outer` and `'inner`. * any origin that is dereferenced in `P`, or, more precisely, any origin in the type of any reference that is dereferenced in `P`. * For example, reading from `(*x).0`, where `x: &'x0 (&'x1 u32, &'x2 u32)` accesses * `'x0` because of `*x` * `'x1` because of the `.0`, which gives the final type `&'x1 u32` Mutably borrowing `P` counts as a write to `P` in this context, immutable borrows count as a read. ### Invalidation If a read or write violates an existing borrow `'L`, then `'L` is invalidated. * For example, reading `x` invalidates and mutable borrow `'L_mut_x` of `x`. #### Questions * Does borrowing `&'L_p mut p` always invalidate + clear `'L_p`, because `p` is written to (mutably borrowed), but the borrow is also re-created? **Answer:** Yes, because the invalidation happens conceptually *before* the clear and may be propagated across subsets. * Should writing to `*y`, where `y = &'L_*x mut *x`, `x = &'L_p mut p`, `p: u32`, invalidate `'L_*x`, `'L_p`, or both? How do we know if `x` still references `p` at the time of the write? **Answer:** usage of a path invalidates any origin whose associated path starts with the used path. So using `*y` invalidates **neither** `'L_*x` **nor** `'L_p`, but **does** invalidate any `'L_y`, `'L_*y` where they exist. ```rust let mut x = 42; let p = &mut x; let pp = &mut *p; // reborrow `p` // `p` is no longer used. How is `pp` (the reborrow) connected to `x`? x = 0; dbg!(pp); ``` * I think we would need to propagate `access` across the subset graph as well? -Dylan * How do we handle assignments that invalidate unrelated origins? Example `diamond-ref-mod` (Dylan): ```rust let mut x = 4; let mut p = &22; if maybe() { p = &x; } else { x = 0; // invalidate x } dbg!(p); // access p (or *p?) ``` * Here, there can only ever be **either** a relationship between `p` and `x`, **or** a mutation of `x`, but not both. However, both the subset relationship and the invalidation from the write reach the access of `p`. * Current idea: only invalidate origins from which the invalidation is CFG-reachable. **Answer:** this is solved by removing the transitive closure on `origin_invalidated` and `subset` in favor of propagating `invalidate_origin` across subsets in the original node. This has, however, caused problems in `issue-47680`. * How do we handle self-invalidation? Example `self-invalidation-loop` (Dylan): ```rust fn main() { let mut x = 42; let mut v: Vec<&mut i32> = vec![]; while maybe() { let tmp = &mut x; // L_x v.push(tmp); } } ``` * Here, the problem is that the lifetime of `tmp`'s `'L_x` on one iteration is **extended** into the next by storing it in `v`. This makes it not match lexical scopes anymore. However, when `tmp` is re-created, this clears `'L_x`, so neither additional subset relations nor invalidation are propagated. * Is this possible to solve without liveness (of `v` or `'tmp`)? **Answer:** this is also solved by intra-node propagation of `invalidate_origin` before any corresponding clears for that origin. ### Clearing Origins Origins are cleared * when they are created. * For example, taking a borrow `&'L_P P` of `P` clears `&'L_P`. * when expressions in the path of a loan origin change, but its target and the associated memory don't. * Consider the following code ```rust let x = 42; let y = 22; let mut temp = &x; let p = &*temp; // &'L_*temp *temp == &x temp = &y; // now `*temp != x`, but `*p == x` and `x` still exists. // Therefore, `p` and `'L_*temp` are not invalidated, but // future occurences of `*temp` are unrelated to `p`. ``` ### Subset Relations Relationships between origins arise from borrows and assignments. #### Borrows * **Immutably** borrowing `P = *Q` as `&'L_*Q *Q` where `Q` is a **shared** reference `Q: &'Q T` introduces `'L_*Q <= 'Q`, because the outer reference `'L_*Q` cannot outlive the inner reference `'Q`. * **Immutably** borrowing `P = *Q` as `&'L_*Q *Q` where `Q` is a **mutable** reference `Q: &'Q mut T` introduces `'L_*Q <= 'Q` for the same reason, but continues recursively adding borrow subset relations for `Q` (i.e., if `Q = *R`, then consider origins in `R`). * This is not necessary for shared refs because they are `Copy`, while mutable refs mean the original source cannot be used while the new borrow is live. * **Mutably** borrowing `P = *Q` as `&'L_*Q mut *Q` where `Q` is a **shared** reference `Q: &'Q T` is an error (mutable borrow of shared content). * **Mutably** borrowing `P = *Q` as `&'L_*Q mut *Q` where `Q` is a **mutable** reference `Q: &'Q mut T` has the same borrow constraints as immutable borrows of mutable content (`'L_*Q <= 'Q` and adding constraints recursively). #### Types Assignments of values whose types include origins introduces subset constraints according to **variance**. | Type | `'a` | `T` | `U` | | ------------------------ | --------- | ------------- | --------- | | `&'a T` and `*const T` | covariant | covariant | | | `&'a mut T` and `*mut T` | covariant | invariant | | | `Box` and `Vec` | | covariant | | | `[Unsafe]Cell` | | invariant | | | `fn(T) -> U` | | contravariant | covariant | For example, assigning `tmp = &'L_v mut v`, where `v: Vec<&'v mut u32>` and `tmp: &'tmp0 mut Vec<&'tmp1 mut u32>` introduces * `'L_v <= 'tmp0` because of covariance of the reference in `'a` * `'v <= 'tmp1` **and** `'tmp1 <= 'v` because of invariance of the mutable reference in `T` (even though these are again lifetimes in a reference) #### Bounds Additional constraints may arise from `where` bounds. ## Examples ### Example A ```rust= let mut x = 3; let y: &u32 = &x; x = 4; drop(y); ``` #### Input relations #### CFG ```graphviz digraph G { rankdir = "TD" node [ shape = "rectangle" ] Decls [ label = <
let x: u32
let y: &'y u32
L0: shared(x)
> ] A [ label = <
A: x = 3
invalidate_loan(L0)
> ] B [ label = <
B: y = &'0 x
introduce_loan(L0, '0)
introduce_subset('0, 'y)
> ] A -> B C [ label = <
C: x = 4
invalidate_loan(L0)
-------------------
subset('0, 'y)
loan_in_origin(L0, '0)
loan_in_origin(L0, 'y)
> ] B -> C D [ label = <
D: drop(y)
access('y)
-------------------
subset('0, 'y)
origin_invalidated('0)
origin_invalidated('y)
invalidated_origin_accessed('y)
> ] C -> D } ``` ### Example #47680 ```rust #![feature(nll)] struct Thing; impl Thing { fn maybe_next(&mut self) -> Option<&mut Self> { None } } fn main() { let mut temp = &mut Thing; loop { match temp.maybe_next() { Some(v) => { temp = v; } None => { } } } } ``` ```graphviz digraph G { rankdir = "TD" node [ shape = "rectangle" ] Decls [ label = <
let temp: &'temp mut Thing
let t0: &'t0 mut Thing
let v: &'v mut Thing
L_Thing: mutable(Thing)
L_*temp: mutable(*temp)
> ] A [ label = <
temp = &'0 mut Thing
clear_loan(L_temp)
introduce_loan(L_Thing, '0)
introduce_subset('0, 'temp)
-------------------
> ] B [ label = <
t0 = &'1 mut *temp
clear_loan('t0)
introduce_loan(L_*temp, '1)
introduce_subset('temp, '1)
introduce_subset('1, 't0)
-------------------
subset('0, 'temp)
loan_in_origin(L_Thing, '0)
loan_in_origin(L_Thing, 'temp)
> ] A -> B C [ label = <
v = MaybeNext(t0)
clear_origin('v)
introduce_subset('t0, 'v)
-------------------
subset('0, 'temp)
subset('0, '1)
subset('0, 't0)
subset('temp, '1)
subset('temp, 't0)
subset('1, 't0)
loan_in_origin(L_Thing, '0)
loan_in_origin(L_Thing, 'temp)
loan_in_origin(L_Thing, '1)
loan_in_origin(L_Thing, 't0)
loan_in_origin(L_*temp, '1)
loan_in_origin(L_*temp, 't0)
> ] B -> C D [ label = <
temp = v
clear_loan(L_*temp)
clear_origin('temp)
introduce_subset('v, 'temp)
-------------------
subset('0, 'temp)
subset('0, '1)
subset('0, 't0)
subset('0, 'v)
subset('temp, '1)
subset('temp, 't0)
subset('temp, 'v)
subset('1, 't0)
subset('1, 'v)
subset('t0, 'v)
loan_in_origin(L_Thing, '0)
loan_in_origin(L_Thing, 'temp)
loan_in_origin(L_Thing, '1)
loan_in_origin(L_Thing, 't0)
loan_in_origin(L_Thing, 'v)
loan_in_origin(L_*temp, '1)
loan_in_origin(L_*temp, 't0)
loan_in_origin(L_*temp, 'v)
> ] C -> D E [ label = <
-------------------
subset('0, 'temp)
subset('0, '1)
subset('0, 't0)
subset('0, 'v)
subset('temp, '1)
subset('temp, 't0)
subset('temp, 'v)
subset('1, 't0)
subset('1, 'v)
subset('t0, 'v)
loan_in_origin(L_Thing, '0)
loan_in_origin(L_Thing, 'temp)
loan_in_origin(L_Thing, '1)
loan_in_origin(L_Thing, 't0)
loan_in_origin(L_Thing, 'v)
loan_in_origin(L_*temp, '1)
loan_in_origin(L_*temp, 't0)
loan_in_origin(L_*temp, 'v)
> ] C -> E F [ label = <
-------------------
subset('0, '1)
subset('0, 't0)
subset('0, 'v)
subset('0, 'temp)
subset('1, 't0)
subset('1, 'v)
subset('1, 'temp)
subset('t0, 'v)
subset('v, 'temp)
loan_in_origin(L_Thing, '0)
loan_in_origin(L_Thing, '1)
loan_in_origin(L_Thing, 't0)
loan_in_origin(L_Thing, 'v)
loan_in_origin(L_Thing, 'temp)
> ] E -> F D -> F F -> C } ``` ### Example vec-temp This illustrates why we propagate subtype relations. ```rust let mut x = 22; let mut v = vec![]; let p = &x; let mut tmp = &mut v; Vec::push(tmp, p); x = 23; Vec::len(v); // ERROR ``` ```graphviz digraph G { rankdir = "TD" node [ shape = "rectangle" ] Decls [ label = <
let x: u32
let v: Vec<&'v mut u32>
let p: &'p u32
let tmp: &'tmp0 mut Vec<&'tmp1 mut u32>
L_x: shared(x)
L_v: mutable(v)
> ] A [ label = <
x = 22
invalidate_loan(L_x)
> ] B [ label = <
v = vec![]
invalidate_loan(L_v)
> ] A -> B C [ label = <
p = &x
introduce_loan(L_x, 'p)
> ] B -> C D [ label = <
tmp = &mut v
introduce_loan('tmp0, L_v)
introduce_subset('tmp1, 'v)
introduce_subset('v, 'tmp1)
-------------------
loan_in_origin(L_x, 'p)
> ] C -> D E [ label = <
Vec::push(tmp, p)
access_origin('tmp0)
access_origin('tmp1)
access_origin('p)
introduce_subset('p, 'tmp1)
-------------------
subset('tmp1, 'v)
subset('v, 'tmp1)
loan_in_origin(L_v, 'tmp0)
loan_in_origin(L_x, 'p)
> ] D -> E F [ label = <
x = 23
invalidate_loan(L_x)
-------------------
subset('tmp1, 'v)
subset('v, 'tmp1)
subset('p, 'tmp1)
loan_in_origin(L_v, 'tmp0)
loan_in_origin(L_x, 'p)
loan_in_origin(L_x, 'tmp1)
loan_in_origin(L_x, 'v)
> ] E -> F G [ label = <
Vec::len(v)
access_origin('v)
-------------------
subset('tmp1, 'v)
subset('v, 'tmp1)
subset('p, 'tmp1)
origin_invalidated('tmp1)
origin_invalidated('v)
invalidated_origin_accessed('v)
> ] F -> G } ``` ### Example killing-and-murder ```rust let p = 22; let q = 44; let x: &mut i32 = &mut p; // `x` points at `p` let y = &mut *x; // Loan L0, `y` points at `p` too // ... x = &mut q; // `x` points at `q`; clears L0 ``` ```graphviz digraph G { rankdir = "TD" node [ shape = "rectangle" ] Decls [ label = <
let p: u32
let q: u32
let x: &'x mut i32
let y: &'y mut i32
L_p: mut(p)
L_q: mut(q)
L_*x: mut(*x)
> ] A [ label = <
p = 22
invalidate_loan(L_p)
> ] B [ label = <
q = 22
invalidate_loan(L_q)
> ] A -> B C [ label = <
x = &'0 mut p
invalidate_loan(L_q)
> ] B -> C } ``` ### Example Dylan's Canonical Liveness ```rust let x = 22; let y = 44; let mut p: &'0 i32 = &'1 x; // Loan L0 p = &'3 y; // Loan L1 x += 1; // invalidates(L0) print(*p); ``` ```graphviz digraph G { rankdir = "TD" node [ shape = "rectangle" ] Decls [ label = <
let p: u32
let q: u32
let x: &'x mut i32
let y: &'y mut i32
L_p: mut(p)
L_q: mut(q)
L_*x: mut(*x)
> ] A [ label = <
p = 22
invalidate_loan(L_p)
> ] B [ label = <
q = 22
invalidate_loan(L_q)
> ] A -> B } ``` --- ### Example vec-push-ref ```rust let mut x = 22; let mut v = vec![]; let p = &x; if something() { v.push(p); x += 1; v.len(); // ERROR } else { x += 1; v.len(); // OK } v.len(); // ERROR ``` ```graphviz digraph G { rankdir = "TD" node [ shape = "rectangle" ] Decls [ label = <
let x: u32
let v: Vec<&'v mut u32>
let p: &'p u32
L_x: shared(x)
L_v: mutable(*v)
> ] } ``` ### Example eq-ftw ```rust #![feature(nll)] #![allow(unused_variables, unused_assignments)] fn random_bool() -> bool { unimplemented!() } fn main() { let mut x: (&u32,) = (&0,); let mut y: (&u32,) = (&1,); let mut z = 2; if random_bool() { y.0 = x.0; // creates `'x: 'y` subset relation } if random_bool() { x.0 = &z; // creates {L0} in 'x constraint // this point, we have `'x: 'y` and `{L0} in `'x`, so we also have `{L0} in 'y` drop(x.0); } z += 1; // polonius flags an (unnecessary) error drop(y.0); } ``` ### Example propagation required ```rust fn cfg_propagation_required(x: &mut &i32) { let y = x; *y = &g(); } ``` ## 47680 unrolled ```graphviz digraph G { rankdir = "TD" node [ shape = "rectangle" ] a [ label = <
a: temp = &'L_Thing mut Thing
-------------------
introduce_subset('L_Thing, 'temp)
> ] b [ label = <
b: t0 = &'L_*temp mut *temp
-------------------
access_origin('temp)
clear_origin('L_*temp)
clear_origin('t0)
introduce_subset('L_*temp, 't0)
introduce_subset('temp, 'L_*temp)
invalidate_origin('L_*temp)
-------------------
subset('L_Thing, 'temp)
> ] a -> b b1 [ label = <
b1: t0 = &'L_*temp mut *temp
-------------------
access_origin('temp)
clear_origin('L_*temp)
clear_origin('t0)
introduce_subset('L_*temp, 't0)
introduce_subset('temp, 'L_*temp)
invalidate_origin('L_*temp)
-------------------
subset('L_*temp, 'L_*temp)
subset('L_*temp, 't0)
subset('L_*temp, 'temp)
subset('L_*temp, 'v)
subset('L_Thing, 'L_*temp)
subset('L_Thing, 't0)
subset('L_Thing, 'temp)
subset('L_Thing, 'v)
subset('t0, 'L_*temp)
subset('t0, 't0)
subset('t0, 'temp)
subset('t0, 'v)
subset('temp, 'L_*temp)
subset('temp, 't0)
subset('temp, 'temp)
subset('temp, 'v)
subset('v, 'L_*temp)
subset('v, 't0)
subset('v, 'temp)
subset('v, 'v)
> ] f -> b1 b2 [ label = <
b2: t0 = &'L_*temp mut *temp
-------------------
access_origin('temp)
clear_origin('L_*temp)
clear_origin('t0)
introduce_subset('L_*temp, 't0)
introduce_subset('temp, 'L_*temp)
invalidate_origin('L_*temp)
-------------------
invalidated_origin_accessed('temp)
origin_invalidated('temp)
subset('L_*temp, 'L_*temp)
subset('L_*temp, 't0)
subset('L_*temp, 'temp)
subset('L_*temp, 'v)
subset('L_Thing, 'L_*temp)
subset('L_Thing, 't0)
subset('L_Thing, 'temp)
subset('L_Thing, 'v)
subset('t0, 'L_*temp)
subset('t0, 't0)
subset('t0, 'temp)
subset('t0, 'v)
subset('temp, 'L_*temp)
subset('temp, 't0)
subset('temp, 'temp)
subset('temp, 'v)
subset('v, 'L_*temp)
subset('v, 't0)
subset('v, 'temp)
subset('v, 'v)
> ] f1 -> b2 b3 [ label = <
b3: (pass)
-------------------
-------------------
origin_invalidated('temp)
subset('L_*temp, 'L_*temp)
subset('L_*temp, 't0)
subset('L_*temp, 'temp)
subset('L_*temp, 'v)
subset('L_Thing, 'L_*temp)
subset('L_Thing, 't0)
subset('L_Thing, 'temp)
subset('L_Thing, 'v)
subset('t0, 'L_*temp)
subset('t0, 't0)
subset('t0, 'temp)
subset('t0, 'v)
subset('temp, 'L_*temp)
subset('temp, 't0)
subset('temp, 'temp)
subset('temp, 'v)
subset('v, 'L_*temp)
subset('v, 't0)
subset('v, 'temp)
subset('v, 'v)
> ] f2 -> b3 c [ label = <
c: v = MaybeNext(t0)
-------------------
access_origin('t0)
clear_origin('v)
introduce_subset('t0, 'v)
-------------------
subset('L_*temp, 't0)
subset('L_Thing, 'L_*temp)
subset('L_Thing, 't0)
subset('L_Thing, 'temp)
subset('temp, 'L_*temp)
subset('temp, 't0)
> ] b -> c c1 [ label = <
c1: v = MaybeNext(t0)
-------------------
access_origin('t0)
clear_origin('v)
introduce_subset('t0, 'v)
-------------------
origin_invalidated('temp)
origin_invalidated('v)
subset('L_*temp, 't0)
subset('L_Thing, 'L_*temp)
subset('L_Thing, 't0)
subset('L_Thing, 'temp)
subset('L_Thing, 'v)
subset('temp, 'L_*temp)
subset('temp, 't0)
subset('temp, 'temp)
subset('temp, 'v)
subset('v, 'L_*temp)
subset('v, 't0)
subset('v, 'temp)
subset('v, 'v)
> ] b1 -> c1 c2 [ label = <
c2: v = MaybeNext(t0)
-------------------
access_origin('t0)
clear_origin('v)
introduce_subset('t0, 'v)
-------------------
origin_invalidated('temp)
origin_invalidated('v)
subset('L_*temp, 't0)
subset('L_Thing, 'L_*temp)
subset('L_Thing, 't0)
subset('L_Thing, 'temp)
subset('L_Thing, 'v)
subset('temp, 'L_*temp)
subset('temp, 't0)
subset('temp, 'temp)
subset('temp, 'v)
subset('v, 'L_*temp)
subset('v, 't0)
subset('v, 'temp)
subset('v, 'v)
> ] b2 -> c2 d [ label = <
d: temp = v
-------------------
access_origin('v)
clear_origin('L_*temp)
clear_origin('temp)
introduce_subset('v, 'temp)
-------------------
subset('L_*temp, 't0)
subset('L_*temp, 'v)
subset('L_Thing, 'L_*temp)
subset('L_Thing, 't0)
subset('L_Thing, 'temp)
subset('L_Thing, 'v)
subset('t0, 'v)
subset('temp, 'L_*temp)
subset('temp, 't0)
subset('temp, 'v)
> ] c -> d d1 [ label = <
d1: temp = v
-------------------
access_origin('v)
clear_origin('L_*temp)
clear_origin('temp)
introduce_subset('v, 'temp)
-------------------
origin_invalidated('temp)
subset('L_*temp, 't0)
subset('L_*temp, 'v)
subset('L_Thing, 'L_*temp)
subset('L_Thing, 't0)
subset('L_Thing, 'temp)
subset('L_Thing, 'v)
subset('t0, 'v)
subset('temp, 'L_*temp)
subset('temp, 't0)
subset('temp, 'temp)
subset('temp, 'v)
> ] c1 -> d1 d2 [ label = <
d2: temp = v
-------------------
access_origin('v)
clear_origin('L_*temp)
clear_origin('temp)
introduce_subset('v, 'temp)
-------------------
origin_invalidated('temp)
subset('L_*temp, 't0)
subset('L_*temp, 'v)
subset('L_Thing, 'L_*temp)
subset('L_Thing, 't0)
subset('L_Thing, 'temp)
subset('L_Thing, 'v)
subset('t0, 'v)
subset('temp, 'L_*temp)
subset('temp, 't0)
subset('temp, 'temp)
subset('temp, 'v)
> ] c2 -> d2 e [ label = <
e: (pass)
-------------------
-------------------
subset('L_*temp, 't0)
subset('L_*temp, 'v)
subset('L_Thing, 'L_*temp)
subset('L_Thing, 't0)
subset('L_Thing, 'temp)
subset('L_Thing, 'v)
subset('t0, 'v)
subset('temp, 'L_*temp)
subset('temp, 't0)
subset('temp, 'v)
> ] c -> e e1 [ label = <
e1: (pass)
-------------------
-------------------
origin_invalidated('temp)
subset('L_*temp, 't0)
subset('L_*temp, 'v)
subset('L_Thing, 'L_*temp)
subset('L_Thing, 't0)
subset('L_Thing, 'temp)
subset('L_Thing, 'v)
subset('t0, 'v)
subset('temp, 'L_*temp)
subset('temp, 't0)
subset('temp, 'temp)
subset('temp, 'v)
> ] c1 -> e1 e2 [ label = <
e2: (pass)
-------------------
-------------------
origin_invalidated('temp)
subset('L_*temp, 't0)
subset('L_*temp, 'v)
subset('L_Thing, 'L_*temp)
subset('L_Thing, 't0)
subset('L_Thing, 'temp)
subset('L_Thing, 'v)
subset('t0, 'v)
subset('temp, 'L_*temp)
subset('temp, 't0)
subset('temp, 'temp)
subset('temp, 'v)
> ] c2 -> e2 f [ label = <
f: (pass)
-------------------
-------------------
subset('L_*temp, 'L_*temp)
subset('L_*temp, 't0)
subset('L_*temp, 'temp)
subset('L_*temp, 'v)
subset('L_Thing, 'L_*temp)
subset('L_Thing, 't0)
subset('L_Thing, 'temp)
subset('L_Thing, 'v)
subset('t0, 'L_*temp)
subset('t0, 't0)
subset('t0, 'temp)
subset('t0, 'v)
subset('temp, 'L_*temp)
subset('temp, 't0)
subset('temp, 'temp)
subset('temp, 'v)
subset('v, 'L_*temp)
subset('v, 't0)
subset('v, 'temp)
subset('v, 'v)
> ] g -> f h -> f f1 [ label = <
f1: (pass)
-------------------
-------------------
origin_invalidated('temp)
subset('L_*temp, 'L_*temp)
subset('L_*temp, 't0)
subset('L_*temp, 'temp)
subset('L_*temp, 'v)
subset('L_Thing, 'L_*temp)
subset('L_Thing, 't0)
subset('L_Thing, 'temp)
subset('L_Thing, 'v)
subset('t0, 'L_*temp)
subset('t0, 't0)
subset('t0, 'temp)
subset('t0, 'v)
subset('temp, 'L_*temp)
subset('temp, 't0)
subset('temp, 'temp)
subset('temp, 'v)
subset('v, 'L_*temp)
subset('v, 't0)
subset('v, 'temp)
subset('v, 'v)
> ] g1 -> f1 h1 -> f1 f2 [ label = <
f2: (pass)
-------------------
-------------------
origin_invalidated('temp)
subset('L_*temp, 'L_*temp)
subset('L_*temp, 't0)
subset('L_*temp, 'temp)
subset('L_*temp, 'v)
subset('L_Thing, 'L_*temp)
subset('L_Thing, 't0)
subset('L_Thing, 'temp)
subset('L_Thing, 'v)
subset('t0, 'L_*temp)
subset('t0, 't0)
subset('t0, 'temp)
subset('t0, 'v)
subset('temp, 'L_*temp)
subset('temp, 't0)
subset('temp, 'temp)
subset('temp, 'v)
subset('v, 'L_*temp)
subset('v, 't0)
subset('v, 'temp)
subset('v, 'v)
> ] g2 -> f2 h2 -> f2 g [ label = <
g: (pass)
-------------------
-------------------
subset('L_Thing, 't0)
subset('L_Thing, 'temp)
subset('L_Thing, 'v)
subset('t0, 'temp)
subset('t0, 'v)
subset('v, 'temp)
> ] d -> g g1 [ label = <
g1: (pass)
-------------------
-------------------
subset('L_Thing, 't0)
subset('L_Thing, 'temp)
subset('L_Thing, 'v)
subset('t0, 'temp)
subset('t0, 'v)
subset('v, 'temp)
> ] d1 -> g1 g2 [ label = <
g2: (pass)
-------------------
-------------------
subset('L_Thing, 't0)
subset('L_Thing, 'temp)
subset('L_Thing, 'v)
subset('t0, 'temp)
subset('t0, 'v)
subset('v, 'temp)
> ] d2 -> g2 h [ label = <
h: (pass)
-------------------
-------------------
subset('L_*temp, 't0)
subset('L_*temp, 'v)
subset('L_Thing, 'L_*temp)
subset('L_Thing, 't0)
subset('L_Thing, 'temp)
subset('L_Thing, 'v)
subset('t0, 'v)
subset('temp, 'L_*temp)
subset('temp, 't0)
subset('temp, 'v)
> ] e -> h h1 [ label = <
h1: (pass)
-------------------
-------------------
origin_invalidated('temp)
subset('L_*temp, 't0)
subset('L_*temp, 'v)
subset('L_Thing, 'L_*temp)
subset('L_Thing, 't0)
subset('L_Thing, 'temp)
subset('L_Thing, 'v)
subset('t0, 'v)
subset('temp, 'L_*temp)
subset('temp, 't0)
subset('temp, 'temp)
subset('temp, 'v)
> ] e1 -> h1 h2 [ label = <
h2: (pass)
-------------------
-------------------
origin_invalidated('temp)
subset('L_*temp, 't0)
subset('L_*temp, 'v)
subset('L_Thing, 'L_*temp)
subset('L_Thing, 't0)
subset('L_Thing, 'temp)
subset('L_Thing, 'v)
subset('t0, 'v)
subset('temp, 'L_*temp)
subset('temp, 't0)
subset('temp, 'temp)
subset('temp, 'v)
> ] e2 -> h2 } ``` ## Niko's concern ``` A -> B A -> C where A has subsets: o0 <= o1 o2 <= o3 A introduces o1 <= o2 o1, o2 are live in B o1, o2 are dead in C ``` Shouldn't we have `o0 <= o3` in C? I don't think we will. Is another way to phrase this `subset_on_entry` vs `subset_on_exit`? I think so. In that case, it makes sense that we: * Apply kills/liveness when transitioning from entry => exit * Apply liveness when we transition exit => entry (along cfg edges) * But never apply both Or rather ``` exit = entry - cleared + introduced live ``` but we could also reduce this to *just* compute subset on entry, couldn't we? ``` subset_on_exit(O1, O2, Node) = subset_on_entry(O1, O2, Node), !clear_origin(O1, Node), !clear_origin(O2, Node). subset_on_exit(O1, O2, Node) = introduce_subset(O1, O2, Node). subset_on_exit(O1, O3, Node) = subset_on_exit(O1, O2, Node). subset_on_exit(O2, O3, Node). subset_on_entry(O1, O2, Node) = cfg_edge(Node_pred, Node), subset_on_exit(O1, O2, Node_pred), ( is_loan_origin(O1); origin_live_on_entry(O1, Node), origin_live_on_entry(O2, Node) ). origin_live_on_entry(O, Node) :- access_origin(O, Node). origin_live_on_entry(O, Node) :- cfg_edge(Node, Node_succ), origin_live_on_entry(O, Node_succ), !clear_origin(O, Node). ``` --- // * First we perform any accesses `access_origin(O, N)` // * Then we invalidate any origins `invalidate_origin(L, N)` // * Then we clear any origins `clear_origin` // * Then we introduce any subsets `introduce_subset` --- Why this matters * On entry: * O1 <= O2 * O2 <= O3 * Clear origins: * O3 * Introduced: * O3 <= O4 * Result: * O1 <= O2 * O3 <= O4 ``` // vec-temp // let mut x = 22; // let mut v = vec![]; // let p = &x; // let mut tmp = &mut v; // Vec::push(tmp, p); // x = 23; // Vec::len(v); // ERROR ```