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<T>` and `Vec<T>` | | covariant | | | `[Unsafe]Cell<T>` | | 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 = <<table border="0"> <tr><td align="left">let x:</td> <td align="left">u32</td></tr> <tr><td align="left">let y:</td> <td align="left">&'y u32</td></tr> <tr><td align="left">L0:</td> <td align="left">shared(x)</td></tr> </table>> ] A [ label = <<table border="0"> <tr><td>A: x = 3</td></tr> <tr><td>invalidate_loan(L0)</td></tr> </table>> ] B [ label = <<table border="0"> <tr><td>B: y = &'0 x</td></tr> <tr><td>introduce_loan(L0, '0)</td></tr> <tr><td>introduce_subset('0, 'y)</td></tr> </table>> ] A -> B C [ label = <<table border="0"> <tr><td>C: x = 4</td></tr> <tr><td>invalidate_loan(L0)</td></tr> <tr><td>-------------------</td></tr> <tr><td>subset('0, 'y)</td></tr> <tr><td>loan_in_origin(L0, '0)</td></tr> <tr><td>loan_in_origin(L0, 'y)</td></tr> </table>> ] B -> C D [ label = <<table border="0"> <tr><td>D: drop(y)</td></tr> <tr><td>access('y)</td></tr> <tr><td>-------------------</td></tr> <tr><td>subset('0, 'y)</td></tr> <tr><td>origin_invalidated('0)</td></tr> <tr><td>origin_invalidated('y)</td></tr> <tr><td>invalidated_origin_accessed('y)</td></tr> </table>> ] 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 = <<table border="0"> <tr><td align="left">let temp:</td> <td align="left">&'temp mut Thing</td></tr> <tr><td align="left">let t0:</td> <td align="left">&'t0 mut Thing</td></tr> <tr><td align="left">let v:</td> <td align="left">&'v mut Thing</td></tr> <tr><td align="left">L_Thing:</td> <td align="left">mutable(Thing)</td></tr> <tr><td align="left">L_*temp:</td> <td align="left">mutable(*temp)</td></tr> </table>> ] A [ label = <<table border="0"> <tr><td>temp = &'0 mut Thing</td></tr> <tr><td>clear_loan(L_temp)</td></tr> <tr><td>introduce_loan(L_Thing, '0)</td></tr> <tr><td>introduce_subset('0, 'temp)</td></tr> <tr><td>-------------------</td></tr> </table>> ] B [ label = <<table border="0"> <tr><td>t0 = &'1 mut *temp</td></tr> <tr><td>clear_loan('t0)</td></tr> <tr><td>introduce_loan(L_*temp, '1)</td></tr> <tr><td>introduce_subset('temp, '1)</td></tr> <tr><td>introduce_subset('1, 't0)</td></tr> <tr><td>-------------------</td></tr> <tr><td>subset('0, 'temp)</td></tr> <tr><td>loan_in_origin(L_Thing, '0)</td></tr> <tr><td>loan_in_origin(L_Thing, 'temp)</td></tr> </table>> ] A -> B C [ label = <<table border="0"> <tr><td>v = MaybeNext(t0)</td></tr> <tr><td>clear_origin('v)</td></tr> <tr><td>introduce_subset('t0, 'v)</td></tr> <tr><td>-------------------</td></tr> <tr><td>subset('0, 'temp)</td></tr> <tr><td>subset('0, '1)</td></tr> <tr><td>subset('0, 't0)</td></tr> <tr><td>subset('temp, '1)</td></tr> <tr><td>subset('temp, 't0)</td></tr> <tr><td>subset('1, 't0)</td></tr> <tr><td>loan_in_origin(L_Thing, '0)</td></tr> <tr><td>loan_in_origin(L_Thing, 'temp)</td></tr> <tr><td>loan_in_origin(L_Thing, '1)</td></tr> <tr><td>loan_in_origin(L_Thing, 't0)</td></tr> <tr><td>loan_in_origin(L_*temp, '1)</td></tr> <tr><td>loan_in_origin(L_*temp, 't0)</td></tr> </table>> ] B -> C D [ label = <<table border="0"> <tr><td>temp = v</td></tr> <tr><td>clear_loan(L_*temp)</td></tr> <tr><td>clear_origin('temp)</td></tr> <tr><td>introduce_subset('v, 'temp)</td></tr> <tr><td>-------------------</td></tr> <tr><td>subset('0, 'temp)</td></tr> <tr><td>subset('0, '1)</td></tr> <tr><td>subset('0, 't0)</td></tr> <tr><td>subset('0, 'v)</td></tr> <tr><td>subset('temp, '1)</td></tr> <tr><td>subset('temp, 't0)</td></tr> <tr><td>subset('temp, 'v)</td></tr> <tr><td>subset('1, 't0)</td></tr> <tr><td>subset('1, 'v)</td></tr> <tr><td>subset('t0, 'v)</td></tr> <tr><td>loan_in_origin(L_Thing, '0)</td></tr> <tr><td>loan_in_origin(L_Thing, 'temp)</td></tr> <tr><td>loan_in_origin(L_Thing, '1)</td></tr> <tr><td>loan_in_origin(L_Thing, 't0)</td></tr> <tr><td>loan_in_origin(L_Thing, 'v)</td></tr> <tr><td>loan_in_origin(L_*temp, '1)</td></tr> <tr><td>loan_in_origin(L_*temp, 't0)</td></tr> <tr><td>loan_in_origin(L_*temp, 'v)</td></tr> </table>> ] C -> D E [ label = <<table border="0"> <tr><td>-------------------</td></tr> <tr><td>subset('0, 'temp)</td></tr> <tr><td>subset('0, '1)</td></tr> <tr><td>subset('0, 't0)</td></tr> <tr><td>subset('0, 'v)</td></tr> <tr><td>subset('temp, '1)</td></tr> <tr><td>subset('temp, 't0)</td></tr> <tr><td>subset('temp, 'v)</td></tr> <tr><td>subset('1, 't0)</td></tr> <tr><td>subset('1, 'v)</td></tr> <tr><td>subset('t0, 'v)</td></tr> <tr><td>loan_in_origin(L_Thing, '0)</td></tr> <tr><td>loan_in_origin(L_Thing, 'temp)</td></tr> <tr><td>loan_in_origin(L_Thing, '1)</td></tr> <tr><td>loan_in_origin(L_Thing, 't0)</td></tr> <tr><td>loan_in_origin(L_Thing, 'v)</td></tr> <tr><td>loan_in_origin(L_*temp, '1)</td></tr> <tr><td>loan_in_origin(L_*temp, 't0)</td></tr> <tr><td>loan_in_origin(L_*temp, 'v)</td></tr> </table>> ] C -> E F [ label = <<table border="0"> <tr><td>-------------------</td></tr> <tr><td>subset('0, '1)</td></tr> <tr><td>subset('0, 't0)</td></tr> <tr><td>subset('0, 'v)</td></tr> <tr><td>subset('0, 'temp)</td></tr> <tr><td>subset('1, 't0)</td></tr> <tr><td>subset('1, 'v)</td></tr> <tr><td>subset('1, 'temp)</td></tr> <tr><td>subset('t0, 'v)</td></tr> <tr><td>subset('v, 'temp)</td></tr> <tr><td>loan_in_origin(L_Thing, '0)</td></tr> <tr><td>loan_in_origin(L_Thing, '1)</td></tr> <tr><td>loan_in_origin(L_Thing, 't0)</td></tr> <tr><td>loan_in_origin(L_Thing, 'v)</td></tr> <tr><td>loan_in_origin(L_Thing, 'temp)</td></tr> </table>> ] 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 = <<table border="0"> <tr><td align="left">let x:</td> <td align="left">u32</td></tr> <tr><td align="left">let v:</td> <td align="left">Vec<&'v mut u32></td></tr> <tr><td align="left">let p:</td> <td align="left">&'p u32</td></tr> <tr><td align="left">let tmp:</td> <td align="left">&'tmp0 mut Vec<&'tmp1 mut u32></td></tr> <tr><td align="left">L_x:</td> <td align="left">shared(x)</td></tr> <tr><td align="left">L_v:</td> <td align="left">mutable(v)</td></tr> </table>> ] A [ label = <<table border="0"> <tr><td>x = 22</td></tr> <tr><td>invalidate_loan(L_x)</td></tr> </table>> ] B [ label = <<table border="0"> <tr><td>v = vec![]</td></tr> <tr><td>invalidate_loan(L_v)</td></tr> </table>> ] A -> B C [ label = <<table border="0"> <tr><td>p = &x</td></tr> <tr><td>introduce_loan(L_x, 'p)</td></tr> </table>> ] B -> C D [ label = <<table border="0"> <tr><td>tmp = &mut v</td></tr> <tr><td>introduce_loan('tmp0, L_v)</td></tr> <tr><td>introduce_subset('tmp1, 'v)</td></tr> <tr><td>introduce_subset('v, 'tmp1)</td></tr> <tr><td>-------------------</td></tr> <tr><td>loan_in_origin(L_x, 'p)</td></tr> </table>> ] C -> D E [ label = <<table border="0"> <tr><td>Vec::push(tmp, p)</td></tr> <tr><td>access_origin('tmp0)</td></tr> <tr><td>access_origin('tmp1)</td></tr> <tr><td>access_origin('p)</td></tr> <tr><td>introduce_subset('p, 'tmp1)</td></tr> <tr><td>-------------------</td></tr> <tr><td>subset('tmp1, 'v)</td></tr> <tr><td>subset('v, 'tmp1)</td></tr> <tr><td>loan_in_origin(L_v, 'tmp0)</td></tr> <tr><td>loan_in_origin(L_x, 'p)</td></tr> </table>> ] D -> E F [ label = <<table border="0"> <tr><td>x = 23</td></tr> <tr><td>invalidate_loan(L_x)</td></tr> <tr><td>-------------------</td></tr> <tr><td>subset('tmp1, 'v)</td></tr> <tr><td>subset('v, 'tmp1)</td></tr> <tr><td>subset('p, 'tmp1)</td></tr> <tr><td>loan_in_origin(L_v, 'tmp0)</td></tr> <tr><td>loan_in_origin(L_x, 'p)</td></tr> <tr><td>loan_in_origin(L_x, 'tmp1)</td></tr> <tr><td>loan_in_origin(L_x, 'v)</td></tr> </table>> ] E -> F G [ label = <<table border="0"> <tr><td>Vec::len(v)</td></tr> <tr><td>access_origin('v)</td></tr> <tr><td>-------------------</td></tr> <tr><td>subset('tmp1, 'v)</td></tr> <tr><td>subset('v, 'tmp1)</td></tr> <tr><td>subset('p, 'tmp1)</td></tr> <tr><td>origin_invalidated('tmp1)</td></tr> <tr><td>origin_invalidated('v)</td></tr> <tr><td>invalidated_origin_accessed('v)</td></tr> </table>> ] 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 = <<table border="0"> <tr><td align="left">let p:</td> <td align="left">u32</td></tr> <tr><td align="left">let q:</td> <td align="left">u32</td></tr> <tr><td align="left">let x:</td> <td align="left">&'x mut i32</td></tr> <tr><td align="left">let y:</td> <td align="left">&'y mut i32</td></tr> <tr><td align="left">L_p:</td> <td align="left">mut(p)</td></tr> <tr><td align="left">L_q:</td> <td align="left">mut(q)</td></tr> <tr><td align="left">L_*x:</td> <td align="left">mut(*x)</td></tr> </table>> ] A [ label = <<table border="0"> <tr><td>p = 22</td></tr> <tr><td>invalidate_loan(L_p)</td></tr> </table>> ] B [ label = <<table border="0"> <tr><td>q = 22</td></tr> <tr><td>invalidate_loan(L_q)</td></tr> </table>> ] A -> B C [ label = <<table border="0"> <tr><td>x = &'0 mut p</td></tr> <tr><td>invalidate_loan(L_q)</td></tr> </table>> ] 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 = <<table border="0"> <tr><td align="left">let p:</td> <td align="left">u32</td></tr> <tr><td align="left">let q:</td> <td align="left">u32</td></tr> <tr><td align="left">let x:</td> <td align="left">&'x mut i32</td></tr> <tr><td align="left">let y:</td> <td align="left">&'y mut i32</td></tr> <tr><td align="left">L_p:</td> <td align="left">mut(p)</td></tr> <tr><td align="left">L_q:</td> <td align="left">mut(q)</td></tr> <tr><td align="left">L_*x:</td> <td align="left">mut(*x)</td></tr> </table>> ] A [ label = <<table border="0"> <tr><td>p = 22</td></tr> <tr><td>invalidate_loan(L_p)</td></tr> </table>> ] B [ label = <<table border="0"> <tr><td>q = 22</td></tr> <tr><td>invalidate_loan(L_q)</td></tr> </table>> ] 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 = <<table border="0"> <tr><td align="left">let x:</td> <td align="left">u32</td></tr> <tr><td align="left">let v:</td> <td align="left">Vec<&'v mut u32></td></tr> <tr><td align="left">let p:</td> <td align="left">&'p u32</td></tr> <tr><td align="left">L_x:</td> <td align="left">shared(x)</td></tr> <tr><td align="left">L_v:</td> <td align="left">mutable(*v)</td></tr> </table>> ] } ``` ### 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 = <<table border="0"> <tr><td>a: temp = &'L_Thing mut Thing</td></tr> <tr><td>-------------------</td></tr> <tr><td>introduce_subset('L_Thing, 'temp)</td></tr> </table>> ] b [ label = <<table border="0"> <tr><td>b: t0 = &'L_*temp mut *temp</td></tr> <tr><td>-------------------</td></tr> <tr><td>access_origin('temp)</td></tr> <tr><td>clear_origin('L_*temp)</td></tr> <tr><td>clear_origin('t0)</td></tr> <tr><td>introduce_subset('L_*temp, 't0)</td></tr> <tr><td>introduce_subset('temp, 'L_*temp)</td></tr> <tr><td>invalidate_origin('L_*temp)</td></tr> <tr><td>-------------------</td></tr> <tr><td>subset('L_Thing, 'temp)</td></tr> </table>> ] a -> b b1 [ label = <<table border="0"> <tr><td>b1: t0 = &'L_*temp mut *temp</td></tr> <tr><td>-------------------</td></tr> <tr><td>access_origin('temp)</td></tr> <tr><td>clear_origin('L_*temp)</td></tr> <tr><td>clear_origin('t0)</td></tr> <tr><td>introduce_subset('L_*temp, 't0)</td></tr> <tr><td>introduce_subset('temp, 'L_*temp)</td></tr> <tr><td>invalidate_origin('L_*temp)</td></tr> <tr><td>-------------------</td></tr> <tr><td>subset('L_*temp, 'L_*temp)</td></tr> <tr><td>subset('L_*temp, 't0)</td></tr> <tr><td>subset('L_*temp, 'temp)</td></tr> <tr><td>subset('L_*temp, 'v)</td></tr> <tr><td>subset('L_Thing, 'L_*temp)</td></tr> <tr><td>subset('L_Thing, 't0)</td></tr> <tr><td>subset('L_Thing, 'temp)</td></tr> <tr><td>subset('L_Thing, 'v)</td></tr> <tr><td>subset('t0, 'L_*temp)</td></tr> <tr><td>subset('t0, 't0)</td></tr> <tr><td>subset('t0, 'temp)</td></tr> <tr><td>subset('t0, 'v)</td></tr> <tr><td>subset('temp, 'L_*temp)</td></tr> <tr><td>subset('temp, 't0)</td></tr> <tr><td>subset('temp, 'temp)</td></tr> <tr><td>subset('temp, 'v)</td></tr> <tr><td>subset('v, 'L_*temp)</td></tr> <tr><td>subset('v, 't0)</td></tr> <tr><td>subset('v, 'temp)</td></tr> <tr><td>subset('v, 'v)</td></tr> </table>> ] f -> b1 b2 [ label = <<table border="0"> <tr><td>b2: t0 = &'L_*temp mut *temp</td></tr> <tr><td>-------------------</td></tr> <tr><td>access_origin('temp)</td></tr> <tr><td>clear_origin('L_*temp)</td></tr> <tr><td>clear_origin('t0)</td></tr> <tr><td>introduce_subset('L_*temp, 't0)</td></tr> <tr><td>introduce_subset('temp, 'L_*temp)</td></tr> <tr><td>invalidate_origin('L_*temp)</td></tr> <tr><td>-------------------</td></tr> <tr><td bgcolor= "yellow">invalidated_origin_accessed('temp)</td></tr> <tr><td>origin_invalidated('temp)</td></tr> <tr><td>subset('L_*temp, 'L_*temp)</td></tr> <tr><td>subset('L_*temp, 't0)</td></tr> <tr><td>subset('L_*temp, 'temp)</td></tr> <tr><td>subset('L_*temp, 'v)</td></tr> <tr><td>subset('L_Thing, 'L_*temp)</td></tr> <tr><td>subset('L_Thing, 't0)</td></tr> <tr><td>subset('L_Thing, 'temp)</td></tr> <tr><td>subset('L_Thing, 'v)</td></tr> <tr><td>subset('t0, 'L_*temp)</td></tr> <tr><td>subset('t0, 't0)</td></tr> <tr><td>subset('t0, 'temp)</td></tr> <tr><td>subset('t0, 'v)</td></tr> <tr><td>subset('temp, 'L_*temp)</td></tr> <tr><td>subset('temp, 't0)</td></tr> <tr><td>subset('temp, 'temp)</td></tr> <tr><td>subset('temp, 'v)</td></tr> <tr><td>subset('v, 'L_*temp)</td></tr> <tr><td>subset('v, 't0)</td></tr> <tr><td>subset('v, 'temp)</td></tr> <tr><td>subset('v, 'v)</td></tr> </table>> ] f1 -> b2 b3 [ label = <<table border="0"> <tr><td>b3: (pass)</td></tr> <tr><td>-------------------</td></tr> <tr><td>-------------------</td></tr> <tr><td>origin_invalidated('temp)</td></tr> <tr><td>subset('L_*temp, 'L_*temp)</td></tr> <tr><td>subset('L_*temp, 't0)</td></tr> <tr><td>subset('L_*temp, 'temp)</td></tr> <tr><td>subset('L_*temp, 'v)</td></tr> <tr><td>subset('L_Thing, 'L_*temp)</td></tr> <tr><td>subset('L_Thing, 't0)</td></tr> <tr><td>subset('L_Thing, 'temp)</td></tr> <tr><td>subset('L_Thing, 'v)</td></tr> <tr><td>subset('t0, 'L_*temp)</td></tr> <tr><td>subset('t0, 't0)</td></tr> <tr><td>subset('t0, 'temp)</td></tr> <tr><td>subset('t0, 'v)</td></tr> <tr><td>subset('temp, 'L_*temp)</td></tr> <tr><td>subset('temp, 't0)</td></tr> <tr><td>subset('temp, 'temp)</td></tr> <tr><td>subset('temp, 'v)</td></tr> <tr><td>subset('v, 'L_*temp)</td></tr> <tr><td>subset('v, 't0)</td></tr> <tr><td>subset('v, 'temp)</td></tr> <tr><td>subset('v, 'v)</td></tr> </table>> ] f2 -> b3 c [ label = <<table border="0"> <tr><td>c: v = MaybeNext(t0)</td></tr> <tr><td>-------------------</td></tr> <tr><td>access_origin('t0)</td></tr> <tr><td>clear_origin('v)</td></tr> <tr><td>introduce_subset('t0, 'v)</td></tr> <tr><td>-------------------</td></tr> <tr><td>subset('L_*temp, 't0)</td></tr> <tr><td>subset('L_Thing, 'L_*temp)</td></tr> <tr><td>subset('L_Thing, 't0)</td></tr> <tr><td>subset('L_Thing, 'temp)</td></tr> <tr><td>subset('temp, 'L_*temp)</td></tr> <tr><td>subset('temp, 't0)</td></tr> </table>> ] b -> c c1 [ label = <<table border="0"> <tr><td>c1: v = MaybeNext(t0)</td></tr> <tr><td>-------------------</td></tr> <tr><td>access_origin('t0)</td></tr> <tr><td>clear_origin('v)</td></tr> <tr><td>introduce_subset('t0, 'v)</td></tr> <tr><td>-------------------</td></tr> <tr><td>origin_invalidated('temp)</td></tr> <tr><td>origin_invalidated('v)</td></tr> <tr><td>subset('L_*temp, 't0)</td></tr> <tr><td>subset('L_Thing, 'L_*temp)</td></tr> <tr><td>subset('L_Thing, 't0)</td></tr> <tr><td>subset('L_Thing, 'temp)</td></tr> <tr><td>subset('L_Thing, 'v)</td></tr> <tr><td>subset('temp, 'L_*temp)</td></tr> <tr><td>subset('temp, 't0)</td></tr> <tr><td>subset('temp, 'temp)</td></tr> <tr><td>subset('temp, 'v)</td></tr> <tr><td>subset('v, 'L_*temp)</td></tr> <tr><td>subset('v, 't0)</td></tr> <tr><td>subset('v, 'temp)</td></tr> <tr><td>subset('v, 'v)</td></tr> </table>> ] b1 -> c1 c2 [ label = <<table border="0"> <tr><td>c2: v = MaybeNext(t0)</td></tr> <tr><td>-------------------</td></tr> <tr><td>access_origin('t0)</td></tr> <tr><td>clear_origin('v)</td></tr> <tr><td>introduce_subset('t0, 'v)</td></tr> <tr><td>-------------------</td></tr> <tr><td>origin_invalidated('temp)</td></tr> <tr><td>origin_invalidated('v)</td></tr> <tr><td>subset('L_*temp, 't0)</td></tr> <tr><td>subset('L_Thing, 'L_*temp)</td></tr> <tr><td>subset('L_Thing, 't0)</td></tr> <tr><td>subset('L_Thing, 'temp)</td></tr> <tr><td>subset('L_Thing, 'v)</td></tr> <tr><td>subset('temp, 'L_*temp)</td></tr> <tr><td>subset('temp, 't0)</td></tr> <tr><td>subset('temp, 'temp)</td></tr> <tr><td>subset('temp, 'v)</td></tr> <tr><td>subset('v, 'L_*temp)</td></tr> <tr><td>subset('v, 't0)</td></tr> <tr><td>subset('v, 'temp)</td></tr> <tr><td>subset('v, 'v)</td></tr> </table>> ] b2 -> c2 d [ label = <<table border="0"> <tr><td>d: temp = v</td></tr> <tr><td>-------------------</td></tr> <tr><td>access_origin('v)</td></tr> <tr><td>clear_origin('L_*temp)</td></tr> <tr><td>clear_origin('temp)</td></tr> <tr><td>introduce_subset('v, 'temp)</td></tr> <tr><td>-------------------</td></tr> <tr><td>subset('L_*temp, 't0)</td></tr> <tr><td>subset('L_*temp, 'v)</td></tr> <tr><td>subset('L_Thing, 'L_*temp)</td></tr> <tr><td>subset('L_Thing, 't0)</td></tr> <tr><td>subset('L_Thing, 'temp)</td></tr> <tr><td>subset('L_Thing, 'v)</td></tr> <tr><td>subset('t0, 'v)</td></tr> <tr><td>subset('temp, 'L_*temp)</td></tr> <tr><td>subset('temp, 't0)</td></tr> <tr><td>subset('temp, 'v)</td></tr> </table>> ] c -> d d1 [ label = <<table border="0"> <tr><td>d1: temp = v</td></tr> <tr><td>-------------------</td></tr> <tr><td>access_origin('v)</td></tr> <tr><td>clear_origin('L_*temp)</td></tr> <tr><td>clear_origin('temp)</td></tr> <tr><td>introduce_subset('v, 'temp)</td></tr> <tr><td>-------------------</td></tr> <tr><td>origin_invalidated('temp)</td></tr> <tr><td>subset('L_*temp, 't0)</td></tr> <tr><td>subset('L_*temp, 'v)</td></tr> <tr><td>subset('L_Thing, 'L_*temp)</td></tr> <tr><td>subset('L_Thing, 't0)</td></tr> <tr><td>subset('L_Thing, 'temp)</td></tr> <tr><td>subset('L_Thing, 'v)</td></tr> <tr><td>subset('t0, 'v)</td></tr> <tr><td>subset('temp, 'L_*temp)</td></tr> <tr><td>subset('temp, 't0)</td></tr> <tr><td>subset('temp, 'temp)</td></tr> <tr><td>subset('temp, 'v)</td></tr> </table>> ] c1 -> d1 d2 [ label = <<table border="0"> <tr><td>d2: temp = v</td></tr> <tr><td>-------------------</td></tr> <tr><td>access_origin('v)</td></tr> <tr><td>clear_origin('L_*temp)</td></tr> <tr><td>clear_origin('temp)</td></tr> <tr><td>introduce_subset('v, 'temp)</td></tr> <tr><td>-------------------</td></tr> <tr><td>origin_invalidated('temp)</td></tr> <tr><td>subset('L_*temp, 't0)</td></tr> <tr><td>subset('L_*temp, 'v)</td></tr> <tr><td>subset('L_Thing, 'L_*temp)</td></tr> <tr><td>subset('L_Thing, 't0)</td></tr> <tr><td>subset('L_Thing, 'temp)</td></tr> <tr><td>subset('L_Thing, 'v)</td></tr> <tr><td>subset('t0, 'v)</td></tr> <tr><td>subset('temp, 'L_*temp)</td></tr> <tr><td>subset('temp, 't0)</td></tr> <tr><td>subset('temp, 'temp)</td></tr> <tr><td>subset('temp, 'v)</td></tr> </table>> ] c2 -> d2 e [ label = <<table border="0"> <tr><td>e: (pass)</td></tr> <tr><td>-------------------</td></tr> <tr><td>-------------------</td></tr> <tr><td>subset('L_*temp, 't0)</td></tr> <tr><td>subset('L_*temp, 'v)</td></tr> <tr><td>subset('L_Thing, 'L_*temp)</td></tr> <tr><td>subset('L_Thing, 't0)</td></tr> <tr><td>subset('L_Thing, 'temp)</td></tr> <tr><td>subset('L_Thing, 'v)</td></tr> <tr><td>subset('t0, 'v)</td></tr> <tr><td>subset('temp, 'L_*temp)</td></tr> <tr><td>subset('temp, 't0)</td></tr> <tr><td>subset('temp, 'v)</td></tr> </table>> ] c -> e e1 [ label = <<table border="0"> <tr><td>e1: (pass)</td></tr> <tr><td>-------------------</td></tr> <tr><td>-------------------</td></tr> <tr><td>origin_invalidated('temp)</td></tr> <tr><td>subset('L_*temp, 't0)</td></tr> <tr><td>subset('L_*temp, 'v)</td></tr> <tr><td>subset('L_Thing, 'L_*temp)</td></tr> <tr><td>subset('L_Thing, 't0)</td></tr> <tr><td>subset('L_Thing, 'temp)</td></tr> <tr><td>subset('L_Thing, 'v)</td></tr> <tr><td>subset('t0, 'v)</td></tr> <tr><td>subset('temp, 'L_*temp)</td></tr> <tr><td>subset('temp, 't0)</td></tr> <tr><td>subset('temp, 'temp)</td></tr> <tr><td>subset('temp, 'v)</td></tr> </table>> ] c1 -> e1 e2 [ label = <<table border="0"> <tr><td>e2: (pass)</td></tr> <tr><td>-------------------</td></tr> <tr><td>-------------------</td></tr> <tr><td>origin_invalidated('temp)</td></tr> <tr><td>subset('L_*temp, 't0)</td></tr> <tr><td>subset('L_*temp, 'v)</td></tr> <tr><td>subset('L_Thing, 'L_*temp)</td></tr> <tr><td>subset('L_Thing, 't0)</td></tr> <tr><td>subset('L_Thing, 'temp)</td></tr> <tr><td>subset('L_Thing, 'v)</td></tr> <tr><td>subset('t0, 'v)</td></tr> <tr><td>subset('temp, 'L_*temp)</td></tr> <tr><td>subset('temp, 't0)</td></tr> <tr><td>subset('temp, 'temp)</td></tr> <tr><td>subset('temp, 'v)</td></tr> </table>> ] c2 -> e2 f [ label = <<table border="0"> <tr><td>f: (pass)</td></tr> <tr><td>-------------------</td></tr> <tr><td>-------------------</td></tr> <tr><td>subset('L_*temp, 'L_*temp)</td></tr> <tr><td>subset('L_*temp, 't0)</td></tr> <tr><td>subset('L_*temp, 'temp)</td></tr> <tr><td>subset('L_*temp, 'v)</td></tr> <tr><td>subset('L_Thing, 'L_*temp)</td></tr> <tr><td>subset('L_Thing, 't0)</td></tr> <tr><td>subset('L_Thing, 'temp)</td></tr> <tr><td>subset('L_Thing, 'v)</td></tr> <tr><td>subset('t0, 'L_*temp)</td></tr> <tr><td>subset('t0, 't0)</td></tr> <tr><td>subset('t0, 'temp)</td></tr> <tr><td>subset('t0, 'v)</td></tr> <tr><td>subset('temp, 'L_*temp)</td></tr> <tr><td>subset('temp, 't0)</td></tr> <tr><td>subset('temp, 'temp)</td></tr> <tr><td>subset('temp, 'v)</td></tr> <tr><td>subset('v, 'L_*temp)</td></tr> <tr><td>subset('v, 't0)</td></tr> <tr><td>subset('v, 'temp)</td></tr> <tr><td>subset('v, 'v)</td></tr> </table>> ] g -> f h -> f f1 [ label = <<table border="0"> <tr><td>f1: (pass)</td></tr> <tr><td>-------------------</td></tr> <tr><td>-------------------</td></tr> <tr><td>origin_invalidated('temp)</td></tr> <tr><td>subset('L_*temp, 'L_*temp)</td></tr> <tr><td>subset('L_*temp, 't0)</td></tr> <tr><td>subset('L_*temp, 'temp)</td></tr> <tr><td>subset('L_*temp, 'v)</td></tr> <tr><td>subset('L_Thing, 'L_*temp)</td></tr> <tr><td>subset('L_Thing, 't0)</td></tr> <tr><td>subset('L_Thing, 'temp)</td></tr> <tr><td>subset('L_Thing, 'v)</td></tr> <tr><td>subset('t0, 'L_*temp)</td></tr> <tr><td>subset('t0, 't0)</td></tr> <tr><td>subset('t0, 'temp)</td></tr> <tr><td>subset('t0, 'v)</td></tr> <tr><td>subset('temp, 'L_*temp)</td></tr> <tr><td>subset('temp, 't0)</td></tr> <tr><td>subset('temp, 'temp)</td></tr> <tr><td>subset('temp, 'v)</td></tr> <tr><td>subset('v, 'L_*temp)</td></tr> <tr><td>subset('v, 't0)</td></tr> <tr><td>subset('v, 'temp)</td></tr> <tr><td>subset('v, 'v)</td></tr> </table>> ] g1 -> f1 h1 -> f1 f2 [ label = <<table border="0"> <tr><td>f2: (pass)</td></tr> <tr><td>-------------------</td></tr> <tr><td>-------------------</td></tr> <tr><td>origin_invalidated('temp)</td></tr> <tr><td>subset('L_*temp, 'L_*temp)</td></tr> <tr><td>subset('L_*temp, 't0)</td></tr> <tr><td>subset('L_*temp, 'temp)</td></tr> <tr><td>subset('L_*temp, 'v)</td></tr> <tr><td>subset('L_Thing, 'L_*temp)</td></tr> <tr><td>subset('L_Thing, 't0)</td></tr> <tr><td>subset('L_Thing, 'temp)</td></tr> <tr><td>subset('L_Thing, 'v)</td></tr> <tr><td>subset('t0, 'L_*temp)</td></tr> <tr><td>subset('t0, 't0)</td></tr> <tr><td>subset('t0, 'temp)</td></tr> <tr><td>subset('t0, 'v)</td></tr> <tr><td>subset('temp, 'L_*temp)</td></tr> <tr><td>subset('temp, 't0)</td></tr> <tr><td>subset('temp, 'temp)</td></tr> <tr><td>subset('temp, 'v)</td></tr> <tr><td>subset('v, 'L_*temp)</td></tr> <tr><td>subset('v, 't0)</td></tr> <tr><td>subset('v, 'temp)</td></tr> <tr><td>subset('v, 'v)</td></tr> </table>> ] g2 -> f2 h2 -> f2 g [ label = <<table border="0"> <tr><td>g: (pass)</td></tr> <tr><td>-------------------</td></tr> <tr><td>-------------------</td></tr> <tr><td>subset('L_Thing, 't0)</td></tr> <tr><td>subset('L_Thing, 'temp)</td></tr> <tr><td>subset('L_Thing, 'v)</td></tr> <tr><td>subset('t0, 'temp)</td></tr> <tr><td>subset('t0, 'v)</td></tr> <tr><td>subset('v, 'temp)</td></tr> </table>> ] d -> g g1 [ label = <<table border="0"> <tr><td>g1: (pass)</td></tr> <tr><td>-------------------</td></tr> <tr><td>-------------------</td></tr> <tr><td>subset('L_Thing, 't0)</td></tr> <tr><td>subset('L_Thing, 'temp)</td></tr> <tr><td>subset('L_Thing, 'v)</td></tr> <tr><td>subset('t0, 'temp)</td></tr> <tr><td>subset('t0, 'v)</td></tr> <tr><td>subset('v, 'temp)</td></tr> </table>> ] d1 -> g1 g2 [ label = <<table border="0"> <tr><td>g2: (pass)</td></tr> <tr><td>-------------------</td></tr> <tr><td>-------------------</td></tr> <tr><td>subset('L_Thing, 't0)</td></tr> <tr><td>subset('L_Thing, 'temp)</td></tr> <tr><td>subset('L_Thing, 'v)</td></tr> <tr><td>subset('t0, 'temp)</td></tr> <tr><td>subset('t0, 'v)</td></tr> <tr><td>subset('v, 'temp)</td></tr> </table>> ] d2 -> g2 h [ label = <<table border="0"> <tr><td>h: (pass)</td></tr> <tr><td>-------------------</td></tr> <tr><td>-------------------</td></tr> <tr><td>subset('L_*temp, 't0)</td></tr> <tr><td>subset('L_*temp, 'v)</td></tr> <tr><td>subset('L_Thing, 'L_*temp)</td></tr> <tr><td>subset('L_Thing, 't0)</td></tr> <tr><td>subset('L_Thing, 'temp)</td></tr> <tr><td>subset('L_Thing, 'v)</td></tr> <tr><td>subset('t0, 'v)</td></tr> <tr><td>subset('temp, 'L_*temp)</td></tr> <tr><td>subset('temp, 't0)</td></tr> <tr><td>subset('temp, 'v)</td></tr> </table>> ] e -> h h1 [ label = <<table border="0"> <tr><td>h1: (pass)</td></tr> <tr><td>-------------------</td></tr> <tr><td>-------------------</td></tr> <tr><td>origin_invalidated('temp)</td></tr> <tr><td>subset('L_*temp, 't0)</td></tr> <tr><td>subset('L_*temp, 'v)</td></tr> <tr><td>subset('L_Thing, 'L_*temp)</td></tr> <tr><td>subset('L_Thing, 't0)</td></tr> <tr><td>subset('L_Thing, 'temp)</td></tr> <tr><td>subset('L_Thing, 'v)</td></tr> <tr><td>subset('t0, 'v)</td></tr> <tr><td>subset('temp, 'L_*temp)</td></tr> <tr><td>subset('temp, 't0)</td></tr> <tr><td>subset('temp, 'temp)</td></tr> <tr><td>subset('temp, 'v)</td></tr> </table>> ] e1 -> h1 h2 [ label = <<table border="0"> <tr><td>h2: (pass)</td></tr> <tr><td>-------------------</td></tr> <tr><td>-------------------</td></tr> <tr><td>origin_invalidated('temp)</td></tr> <tr><td>subset('L_*temp, 't0)</td></tr> <tr><td>subset('L_*temp, 'v)</td></tr> <tr><td>subset('L_Thing, 'L_*temp)</td></tr> <tr><td>subset('L_Thing, 't0)</td></tr> <tr><td>subset('L_Thing, 'temp)</td></tr> <tr><td>subset('L_Thing, 'v)</td></tr> <tr><td>subset('t0, 'v)</td></tr> <tr><td>subset('temp, 'L_*temp)</td></tr> <tr><td>subset('temp, 't0)</td></tr> <tr><td>subset('temp, 'temp)</td></tr> <tr><td>subset('temp, 'v)</td></tr> </table>> ] 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 ```

Syntax	Example	Reference
# Header	Header	基本排版
- Unordered List	Unordered List
1. Ordered List	Ordered List
- [ ] Todo List	Todo List
> Blockquote	Blockquote
Bold font	Bold font
Italics font	Italics font
~~Strikethrough~~	~~Strikethrough~~
19^th^	19^th
H~2~O	H₂O
++Inserted text++	Inserted text
==Marked text==	Marked text
[link text](https:// "title")	Link
![image alt](https:// "title")	Image
`Code`	`Code`	在筆記中貼入程式碼
```javascript var i = 0; ```	`var i = 0;`
:smile:		Emoji list
{%youtube youtube_id %}	Externals
$L^aT_eX$	L^aT_eX
:::info This is a alert area. :::	This is a alert area.