---
# System prepended metadata

title: '2022-06-16: Polonius notes'
tags: [notes]

---

---
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)

### 

