Polonius 2022-11-02 Hackathon Master Document

# Polonius 2022-11-02 Hackathon Master Document ## Agenda * Introductions * Review and discuss goals * including those that are publishable work for Amanda * Review the polonius.next rules * compare with the original rules * (also: the claim that they are not equivalent and polonius.next's `clear_origin` would allow patterns that regular polonius wouldn't) * Possible reports: * Experience and insights from integration with a-mir-formality (nikomatsakis) ## Links * https://github.com/nikomatsakis/polonius.next/ * borrowck in a-mir-formality * https://github.com/nikomatsakis/a-mir-formality/pull/110 and https://github.com/nikomatsakis/a-mir-formality/pull/111 * more polonius-like https://github.com/nikomatsakis/a-mir-formality/pull/113 ## Goals for the day * Breakdown of tasks, clarity around who would do what * Plans for next hackathon ## architectural design ```mermaid flowchart TD MirConstruction --produces --> DefaultMir DefaultMir -- read by --> InitializationAnalysis DefaultMir[(Default MIR)] InitializationAnalysis -- produces --> DropElaboratedMir DropElaboratedMir[(Drop-elaborated MIR)] DropElaboratedMir -- read by --> MirTypeChecker MirTypeChecker -- produces --> TypeCheckConstraints TypeCheckConstraints[(Type-check constraints)] TypeCheckConstraints -- read by --> LoanAnalysis DropElaboratedMir -- read by --> LoanAnalysis TypeCheckConstraints -- read by --> SubsetAnalysis DropElaboratedMir -- read by --> SubsetAnalysis subgraph Polonius LoanAnalysis SubsetAnalysis end ``` ## task listing ```mermaid flowchart TD drop_if_refactoring[" drop-if-refactoring: use `DROP_IF` in representation of Drop-Elaborated MIR "] class drop_if_refactoring nice_to_have; shallow_subtyping[" shallow-subtyping: resolve higher-ranked outlives constraints in trait solver "] class shallow_subtyping active_development; extract_mir_to_library[" extract-mir-to-library: represent MIR as a separate library "] class extract_mir_to_library nice_to_have; loan_analysis_rules[" loan-analysis-rules: draft polonius.next and polonius into rules for loan-analysis, specify fact generation "] class loan_analysis_rules active_development; loan_analysis_code_complete[" loan-analysis-code-complete: implement loan analysis in rustc "] class loan_analysis_code_complete blocking; loan_analysis_passing_test_suite[" loan-analysis-passing-test-suite: go through every regression and fix the problems, address issues found by user testing "] class loan_analysis_passing_test_suite blocking; loan_analysis_in_mir_formality[" loan-analysis-in-mir-formality: model loan-analysis rules in mir-formality "] class loan_analysis_in_mir_formality blocking; polonius_fuzzer[" polonius-fuzzer: generate programs and check if polonius diverges from compiler "] class polonius_fuzzer nice_to_have; ship_polonius_crate[" ship-polonius-crate: polonius ships as an independent thing that can be used outside of rustc, from crates.io "] class ship_polonius_crate blocking; drop_if_refactoring -..-> loan_analysis_code_complete loan_analysis_rules --> loan_analysis_code_complete loan_analysis_rules --> loan_analysis_in_mir_formality loan_analysis_in_mir_formality --> polonius_fuzzer loan_analysis_code_complete --> loan_analysis_passing_test_suite shallow_subtyping --> loan_analysis_passing_test_suite loan_analysis_code_complete --> polonius_fuzzer polonius_fuzzer -..-> loan_analysis_passing_test_suite loan_analysis_passing_test_suite --> ship_polonius_crate extract_mir_to_library --> ship_polonius_crate classDef nice_to_have fill:#7FDBFF,color:black classDef blocking fill:#0074D9,color:white classDef active_development fill:#B10DC9,color:white ``` Cyan things are "nice to have" Blue things are "blocking a stable polonius" Purple things are "under active development" ### examples ```rust fn foo<'a>(x: &'a u32) where for<'b> 'a: 'b, // effectively the same as `'a: 'static` { /* */ } fn main() { let mut x = 22; let p: &i32 = &x; foo(p); x += 1; // error } ``` in the compiler today. Produce MIR for `main` ``` main() { let x: i32; let p: &'0 i32; BB0 { p = &'1 x; // &'1 i32 <: &'0 i32 ===> '1: '0 foo(p) returns BB1; // for<'b> '0: 'b ===> // adds a constraint `for<'b> '0: 'b` to the borrow checker } BB1 { x += 1; StorageDead(x); } } ``` * Today, the output from MIR type checking are constraints like: * `for<'v...> 'r0: 'r1` * Borrow check to take those as input and figure out what they mean * it figures out that this means `'0: 'static` * `'0` includes all points in the CFG * `'1` outlives `'0` -- so it too includes all points in the CFG * reports an error at `x += 1` is inside `'1` How nikomatsakis expects it to work when we're done: * MIR type checker (or trait solver) deals with higher-ranked stuff and only emits constraints of the form * `r0: 'r1` * So in this example: * `foo(p)` would yield a constraint like `'0: 'static` * Polonius would take that as input and, based on it, figure out that `x += 1` is an error ### examples ```rust fn foo<'a>(x: &'a u32) where for<'b> if ('a: 'b) 'a: 'b, // gets derived by for<'b> fn(&'b &'a u32) : Ord, // proving that `fn` is well-formed here { /* */ } fn main() { let mut x = 22; let p: &i32 = &x; foo(p); x += 1; // error } ``` ### reviewing the rules https://github.com/nikomatsakis/polonius.next/blob/main/src/polonius.dl https://hackmd.io/CGMNjt1hR_qYtsR9hgdGmw ### polonius.next ```rust let mut x = 1; let p = &x; // p: &{O0} i32, O0 includes x x += 1; // invalid = {x} drop(p); // error: use of reference with invalidated origin (`x`) ``` * compute live variables at each point * for each origin that appears in their type, call that origin live at that point * for each `&'0 x` expression in the MIR, create a loan L0 * and require that `'0` includes `{L0}` * propagate these using dataflow * gives rise to, each point: * origin includes some set of loans L... * set set of origins O... are live * if a live origin O includes a loan L, * and the node takes an action that contradicts L, * then you have an error * work item: * merge liveness into polonius.next to produce the preferred rules * simplify polonius to remove before/after nodes and to remove initialization, liveness computation ```rust impl LinkedList { fn get_next(&mut self) -> Option<&mut Self>; } fn foo(tmp: &mut LinkedList) { loop { match get_next(tmp) { Some(p) => { tmp = p; } None => { } } } } ``` * compiler can tell us the live origins at each point * https://github.com/domenicquirl/polonius.next/blob/subset-paths/src/polonius.dl ### location insensitive variant of polonius * loan active is a dataflow computation: * loans become active when they are issued (at the `&x` instruction) * loans are killed when the path that was borrowed is mutated * propagate till fixed point ```rust fn main() { let mut x = 3; // L0 is not active here let p = &x; // loan L0 // L0 is active here drop(p); // p goes dead here // L0 is still active here x = 5; // this mutates the path that was borrowed // loan is inactive } ``` * every origin maps to a set of loans that you are computing * MIR type check produces `'a: 'b` constraints * if some point P has an action that contradicts loan L and L is active at P: * search each live origin O at P * report an error if O contains L ``` inputs: subset(O1, O2). borrow_loan(O, L). error(P) :- contradicts(P, L), loan_active(L, P), live_origin(P, O), contains_loan(O, L). contains_loan(O, L) :- contains_loan(O1, L), subset(O1, O). contains_loan(O, L) :- borrow_loan(O, L). ``` https://github.com/rust-lang/polonius/blob/master/polonius-engine/src/output/location_insensitive.rs purely forward propagation errors and thoughts: https://hackmd.io/KpK0ICQOQLSPxIcNIlhkJQ ## Follow-up items * figuring out the spec (nikomatsakis driving to some extent :) * a-mir-formality / coordinate on types team stream? * implement MIR + MIR type checker (to some extent) on the riir branch of a-mir-formality https://github.com/nikomatsakis/a-mir-formality/tree/riir * port redex rules for NLL to that * update on current status of .next rules, and in-progress work * to compare with regular rules * check the claim that they maybe are not equivalent in expressive power * domenicquirl to look at that first * simplify existing polonius rules to remove CFG points / strip down to the loan check * lqd to pick that up next * prototyping an actual impl (lqd driving) * factor out the universe logic to simplify higher-ranked constraints * theo * prototype "polonius-style" checker in rustc * lqd could follow-up / move forward * assess current status of test suite * theo to pursue (and will look at that first) * what is working? what fails and why?