Umbrella: Borrow checker completeness

[nikomatsakis]

The borrow checker is functional but incomplete relative to rustc. This is a tracking issue for the work needed to reach full NLL parity and beyond.

Sub-issues

• Add back limitations to more accurately model NLLs #253 — Add back limitations to more accurately model NLLs
• Add mut declarations and mutable-place checks #419 — Add mut declarations and mutable-place checks
• Support 2-phase borrows #211 — Support 2-phase borrows
• Track initialization and moves in the borrow checker #296 — Track initialization and moves
• Umbrella: Model the Drop trait #420 — Model the Drop trait (umbrella)
• cycle detection in borrow check is more precise than real Rust #230 — Cycle detection is more precise than real Rust
• Extend type/borrow-check to guarantee values are returned #209 — Extend type/borrow-check to guarantee values are returned
• outlives and type-tests #234 — Outlives and type-tests
• higher-ranked where-clauses, outlives #233 — Higher-ranked where-clauses, outlives

Context

The progression we want to model:

1. NLL (current rustc) — global outlives, per-point loans
2. Polonius alpha — while traversing outlives graph, don't think about kills
3. Full Polonius — full precision

Currently formality is more precise than NLL in some areas (per-point outlives, independent path checking) and less complete in others (no init/move tracking, no mut checks, no Drop modeling).