---
tags: notes
---
# 2022-06-16: Polonius notes
## Biggest picture
```mermaid
flowchart LR
MirTypeChecker
TraitSolver
Polonius
MirTypeChecker -- invokes --> TraitSolver
TraitSolver -- schemes --> MirTypeChecker
MirTypeChecker -- first-order outlives constraints --> Polonius
```
Invokes:
* `Vec<?T>: Foo<?U>`
Scheme `(Scheme ::= (∃ KindedVarIds (implies Goals Term)))`
* `?T = ?U`
* include other inference variables and constraints
https://github.com/nikomatsakis/a-mir-formality/blob/fb940679b0b0c7e8497ed5b3d2ba78a5617634fc/src/ty/grammar.rkt#L18-L19
```rust
trait Foo<X> { }
impl<A> Foo<A> for Vec<A> { }
```
given this
```rust
trait Foo<X> { }
impl<A> Foo<A> for Vec<Box<A>> { }
```
and a goal `Vec<?T>: Foo<?U>`
the answer might be
* `∃A. ?T = Box<A> and ?U = A`
## Polonius inputs
* First-order outlives constraints like `'a: 'b`
* located at a point in the CFG
* `'a: 'b @ P`
* Maybe some `'a: 'b` that have to hold always
* maybe we can eliminate these, but maybe not
* Control-flow graph itself
* some nodes P, Q, ... and some edges P -> Q
```
C := (A : B)
| (C && C)
```
we might also want `C || C`
## Other things the borrow checker does
* checking initialization
"variables never initialized at all"
```rust
let a;
println!("{}", a); // error
```
"variables that are initialized later"
```rust
let a;
if something { a = 10; } else { a = 22; }
println!("{}", a); // OK!
```
"variables that were initialized but have been moved"
```rust
let a = vec![];
std::mem::drop(a);
a = 10; // error
```
"variables that were initialized but may be moved"
```rust
let a = vec![];
if something { std::mem::drop(a); }
a = 10; // error
```
not only variables, also fields "in some cases"
```rust
let mut tuple = (vec![], vec![]);
std::mem::drop(tuple.0);
println!("{:?}", tuple.1);
```
## Polonius inputs
* First-order outlives constraints like `'a: 'b`
* located at a point in the CFG
* `'a: 'b @ P`
* Maybe some `'a: 'b` that have to hold always
* maybe we can eliminate these, but maybe not
* Control-flow graph itself
* some nodes P, Q, ... and some edges P -> Q
* Moves that occur and what is moved
## Phasing
* initialization analysis
* checks that all data is initialized
* liveness
## Optimization potential
* flow-insensitive
* if no back-edges, don't need liveness, etc
## drop elaboration?
```rust
{
let x = Box::new(22);
...
// DROP(x);
}
```
```rust
{
let x = Box::new(22);
std::mem::drop(x);
// DROP(x); -- noop
}
```
```rust
{
let x = Box::new(22);
if something {
std::mem::drop(x);
}
// DROP(x); -- noop?
}
```
```rust
{
let x = Box::new(22);
let x_init = true;
if something {
x_init = false;
std::mem::drop(x);
}
// if x_init { DROP(x); } -- noop?
}
```
## drop-if alternative
instead of `DROP(x)` meaning
"drop x if x is initialized"
we could have `DROP_IF(condition, x)`
"if condition is true, drop x"
and a "extra" guarantee that at the time of MIR borrow check, condition is true iff x is initialized
```rust
{
let x = Box::new(22);
if something {
std::mem::drop(x);
}
// DROP_IF(true, x)
}
```
```rust
{
let x = Box::new(22);
let x_init = true;
if something {
x_init = false;
std::mem::drop(x);
}
// DROP_IF(x_init, x)
}
```
```rust
{
let tuple = (Box::new(22), Box::new(44));
if something {
std::mem::drop(tuple);
}
// DROP(tuple) -- at time of MIR build
// DROP(tuple.1) -- after elaboration
}
```
```rust
{
let tuple = (Box::new(22), Box::new(44));
if something {
std::mem::drop(tuple);
}
// DROP_IF(tuple) -- at time of MIR build
// DROP_IF(tuple.1) -- after elaboration
}
```
the upshot is:
* we can have a version of drop elaboration that produces a `DROP_IF` which the borrow checker can just treat as "always a use"
* which would be nice :)
## What exactly region analysis
```rust
{
let (x, y) = (Box::new(), Box::new());
}
```
```rust
let x = Box::new(22);
let y = &L0 x;
// y is live here
//
// therefore, loan L0 is live
//
// therefore x cannot be dropped, mutated etc
std::mem::drop(y);
```
## Pieces of work that are needed
```mermaid
flowchart LR
drop_if
move_init_formality
loan_formality
drop_if --> move_init_formality
```
* drop-if refactoring :)
* move-init / formality
* formality of the "loan" analysis
* an efficient impl of the "loan" analysis
* depends on "shallow subtyping" work that is going on
* Settle the mir-formality "fully correct" rules
* Create an efficient implementation
## overall dataflow (goal)
```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
```
<span style="background: #7FDBFF; padding: 2px 5px; border-radius: 3px">Cyan things</span> are "nice to have"
<span style="background: #0074D9; color: white; padding: 2px 5px; border-radius: 3px">Blue things</span> are "blocking a stable polonius"
<span style="background: #B10DC9; color: white; padding: 2px 5px; border-radius: 3px">Purple things</span> are "under active development"
## Detailed look at various items
### DropIfRefactoring
[discussion here](https://rust-lang.zulipchat.com/#narrow/stream/186049-t-compiler.2Fwg-polonius/topic/2022-08/near/295224824)
###
Sign in with Wallet
Connect another wallet