Merge pull request #234 from mark-i-m/mir_borrowck
Fill out the borrowck chapter a bit more
This commit is contained in:
commit
2e56207594
|
|
@ -51,13 +51,14 @@ the [`mir_borrowck`] query.
|
||||||
the purpose of this type check is to determine all of the constraints between
|
the purpose of this type check is to determine all of the constraints between
|
||||||
different regions.
|
different regions.
|
||||||
- Next, we do [region inference](borrow_check/region_inference.html), which computes
|
- Next, we do [region inference](borrow_check/region_inference.html), which computes
|
||||||
the values of each region — basically, points in the control-flow graph.
|
the values of each region — basically, the points in the control-flow graph where
|
||||||
|
each lifetime must be valid according to the constraints we collected.
|
||||||
- At this point, we can compute the "borrows in scope" at each point.
|
- At this point, we can compute the "borrows in scope" at each point.
|
||||||
- Finally, we do a second walk over the MIR, looking at the actions it
|
- Finally, we do a second walk over the MIR, looking at the actions it
|
||||||
does and reporting errors. For example, if we see a statement like
|
does and reporting errors. For example, if we see a statement like
|
||||||
`*a + 1`, then we would check that the variable `a` is initialized
|
`*a + 1`, then we would check that the variable `a` is initialized
|
||||||
and that it is not mutably borrowed, as either of those would
|
and that it is not mutably borrowed, as either of those would
|
||||||
require an error to be reported.
|
require an error to be reported. Doing this check requires the results of all
|
||||||
- Doing this check requires the results of all the previous analyses.
|
the previous analyses.
|
||||||
|
|
||||||
[`replace_regions_in_mir`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/fn.replace_regions_in_mir.html
|
[`replace_regions_in_mir`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/fn.replace_regions_in_mir.html
|
||||||
|
|
|
||||||
|
|
@ -9,7 +9,7 @@ deprecated once they become the standard kind of lifetime.)
|
||||||
|
|
||||||
The MIR-based region analysis consists of two major functions:
|
The MIR-based region analysis consists of two major functions:
|
||||||
|
|
||||||
- `replace_regions_in_mir`, invoked first, has two jobs:
|
- [`replace_regions_in_mir`], invoked first, has two jobs:
|
||||||
- First, it finds the set of regions that appear within the
|
- First, it finds the set of regions that appear within the
|
||||||
signature of the function (e.g., `'a` in `fn foo<'a>(&'a u32) {
|
signature of the function (e.g., `'a` in `fn foo<'a>(&'a u32) {
|
||||||
... }`). These are called the "universal" or "free" regions – in
|
... }`). These are called the "universal" or "free" regions – in
|
||||||
|
|
@ -21,49 +21,67 @@ The MIR-based region analysis consists of two major functions:
|
||||||
not of much interest. The intention is that – eventually – they
|
not of much interest. The intention is that – eventually – they
|
||||||
will be "erased regions" (i.e., no information at all), since we
|
will be "erased regions" (i.e., no information at all), since we
|
||||||
won't be doing lexical region inference at all.
|
won't be doing lexical region inference at all.
|
||||||
- `compute_regions`, invoked second: this is given as argument the
|
- [`compute_regions`], invoked second: this is given as argument the
|
||||||
results of move analysis. It has the job of computing values for all
|
results of move analysis. It has the job of computing values for all
|
||||||
the inference variables that `replace_regions_in_mir` introduced.
|
the inference variables that `replace_regions_in_mir` introduced.
|
||||||
- To do that, it first runs the [MIR type checker](#mirtypeck). This
|
- To do that, it first runs the [MIR type checker]. This
|
||||||
is basically a normal type-checker but specialized to MIR, which
|
is basically a normal type-checker but specialized to MIR, which
|
||||||
is much simpler than full Rust of course. Running the MIR type
|
is much simpler than full Rust, of course. Running the MIR type
|
||||||
checker will however create **outlives constraints** between
|
checker will however create **outlives constraints** between
|
||||||
region variables (e.g., that one variable must outlive another
|
region variables (e.g., that one variable must outlive another
|
||||||
one) to reflect the subtyping relationships that arise.
|
one) to reflect the subtyping relationships that arise.
|
||||||
- It also adds **liveness constraints** that arise from where variables
|
- It also adds **liveness constraints** that arise from where variables
|
||||||
are used.
|
are used.
|
||||||
- More details to come, though the [NLL RFC] also includes fairly thorough
|
- After this, we create a [`RegionInferenceContext`] with the constraints we
|
||||||
(and hopefully readable) coverage.
|
have computed and the inference variables we introduced and use the
|
||||||
|
[`solve`] method to infer values for all region inference varaibles.
|
||||||
|
- The [NLL RFC] also includes fairly thorough (and hopefully readable)
|
||||||
|
coverage.
|
||||||
|
|
||||||
[fvb]: ../appendix/background.html#free-vs-bound
|
[fvb]: ../appendix/background.html#free-vs-bound
|
||||||
|
[`replace_regions_in_mir`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/fn.replace_regions_in_mir.html
|
||||||
|
[`compute_regions`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/fn.compute_regions.html
|
||||||
|
[`RegionInferenceContext`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/region_infer/struct.RegionInferenceContext.html
|
||||||
|
[`solve`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/region_infer/struct.RegionInferenceContext.html#method.solve
|
||||||
[NLL RFC]: http://rust-lang.github.io/rfcs/2094-nll.html
|
[NLL RFC]: http://rust-lang.github.io/rfcs/2094-nll.html
|
||||||
|
[MIR type checker]: ./type_check.md
|
||||||
|
|
||||||
## Universal regions
|
## Universal regions
|
||||||
|
|
||||||
*to be written* – explain the `UniversalRegions` type
|
The [`UnversalRegions`] type represents a collection of _universal_ regions
|
||||||
|
corresponding to some MIR `DefId`. It is constructed in
|
||||||
|
[`replace_regions_in_mir`] when we replace all regions with fresh inference
|
||||||
|
variables. [`UniversalRegions`] contains indices for all the free regions in
|
||||||
|
the given MIR along with any relationships that are _known_ to hold between
|
||||||
|
them (e.g. implied bounds, where clauses, etc.).
|
||||||
|
|
||||||
## Region variables and constraints
|
For example, given the MIR for the following function:
|
||||||
|
|
||||||
*to be written* – describe the `RegionInferenceContext` and
|
```rust
|
||||||
the role of `liveness_constraints` vs other `constraints`, plus
|
fn foo<'a>(x: &'a u32) {
|
||||||
|
// ...
|
||||||
|
}
|
||||||
|
```
|
||||||
|
|
||||||
## Closures
|
we would create a universal region for `'a` and one for `'static`. There may
|
||||||
|
also be some complications for handling closures, but we will ignore those for
|
||||||
|
the moment.
|
||||||
|
|
||||||
*to be written*
|
TODO: write about _how_ these regions are computed.
|
||||||
|
|
||||||
<a name="mirtypeck"></a>
|
[`UniversalRegions`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/universal_regions/struct.UniversalRegions.html
|
||||||
|
|
||||||
## The MIR type-check
|
## Region variables
|
||||||
|
|
||||||
## Representing the "values" of a region variable
|
The value of a region can be thought of as a **set**. This set contains all
|
||||||
|
points in the MIR where the region is valid along with any regions that are
|
||||||
The value of a region can be thought of as a **set**; we call the
|
outlived by this region (e.g. if `'a: 'b`, then `end('b)` is in the set for
|
||||||
domain of this set a `RegionElement`. In the code, the value for all
|
`'a`); we call the domain of this set a `RegionElement`. In the code, the value
|
||||||
regions is maintained in
|
for all regions is maintained in [the
|
||||||
[the `rustc_mir::borrow_check::nll::region_infer` module][ri]. For
|
`rustc_mir::borrow_check::nll::region_infer` module][ri]. For each region we
|
||||||
each region we maintain a set storing what elements are present in its
|
maintain a set storing what elements are present in its value (to make this
|
||||||
value (to make this efficient, we give each kind of element an index,
|
efficient, we give each kind of element an index, the `RegionElementIndex`, and
|
||||||
the `RegionElementIndex`, and use sparse bitsets).
|
use sparse bitsets).
|
||||||
|
|
||||||
[ri]: https://github.com/rust-lang/rust/tree/master/src/librustc_mir/borrow_check/nll/region_infer/
|
[ri]: https://github.com/rust-lang/rust/tree/master/src/librustc_mir/borrow_check/nll/region_infer/
|
||||||
|
|
||||||
|
|
@ -83,12 +101,148 @@ The kinds of region elements are as follows:
|
||||||
for details on placeholders, see the section
|
for details on placeholders, see the section
|
||||||
[placeholders and universes](#placeholder).
|
[placeholders and universes](#placeholder).
|
||||||
|
|
||||||
## Causal tracking
|
## Constraints
|
||||||
|
|
||||||
*to be written* – describe how we can extend the values of a variable
|
Before we can infer the value of regions, we need to collect constraints on the
|
||||||
with causal tracking etc
|
regions. There are two primary types of constraints.
|
||||||
|
|
||||||
<a name="placeholder"></a>
|
1. Outlives constraints. These are constraints that one region outlives another
|
||||||
|
(e.g. `'a: 'b`). Outlives constraints are generated by the [MIR type
|
||||||
|
checker].
|
||||||
|
2. Liveness constraints. Each region needs to be live at points where it can be
|
||||||
|
used. These constraints are collected by [`generate_constraints`].
|
||||||
|
|
||||||
|
[`generate_constraints`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/constraint_generation/fn.generate_constraints.html
|
||||||
|
|
||||||
|
## Inference Overview
|
||||||
|
|
||||||
|
So how do we compute the contents of a region? This process is called _region
|
||||||
|
inference_. The high-level idea is pretty simple, but there are some details we
|
||||||
|
need to take care of.
|
||||||
|
|
||||||
|
Here is the high-level idea: we start off each region with the MIR locations we
|
||||||
|
know must be in it from the liveness constraints. From there, we use all of the
|
||||||
|
outlives constraints computed from the type checker to _propagate_ the
|
||||||
|
constraints: for each region `'a`, if `'a: 'b`, then we add all elements of
|
||||||
|
`'b` to `'a`, including `end('b)`. This all happens in
|
||||||
|
[`propagate_constraints`].
|
||||||
|
|
||||||
|
Then, we will check for errors. We first check that type tests are satisfied by
|
||||||
|
calling [`check_type_tests`]. This checks constraints like `T: 'a`. Second, we
|
||||||
|
check that universal regions are not "too big". This is done by calling
|
||||||
|
[`check_universal_regions`]. This checks that for each region `'a` if `'a`
|
||||||
|
contains the element `end('b)`, then we must already know that `'a: 'b` holds
|
||||||
|
(e.g. from a where clause). If we don't already know this, that is an error...
|
||||||
|
well, almost. There is some special handling for closures that we will discuss
|
||||||
|
later.
|
||||||
|
|
||||||
|
### Example
|
||||||
|
|
||||||
|
Consider the following example:
|
||||||
|
|
||||||
|
```rust,ignore
|
||||||
|
fn foo<'a, 'b>(x: &'a usize) -> &'b usize {
|
||||||
|
x
|
||||||
|
}
|
||||||
|
```
|
||||||
|
|
||||||
|
Clearly, this should not compile because we don't know if `'a` outlives `'b`
|
||||||
|
(if it doesn't then the return value could be a dangling reference).
|
||||||
|
|
||||||
|
Let's back up a bit. We need to introduce some free inference variables (as is
|
||||||
|
done in [`replace_regions_in_mir`]). This example doesn't use the exact regions
|
||||||
|
produced, but it (hopefully) is enough to get the idea across.
|
||||||
|
|
||||||
|
```rust,ignore
|
||||||
|
fn foo<'a, 'b>(x: &'a /* '#1 */ usize) -> &'b /* '#3 */ usize {
|
||||||
|
x // '#2, location L1
|
||||||
|
}
|
||||||
|
```
|
||||||
|
|
||||||
|
Some notation: `'#1`, `'#3`, and `'#2` represent the universal regions for the
|
||||||
|
argument, return value, and the expression `x`, respectively. Additionally, I
|
||||||
|
will call the location of the expression `x` `L1`.
|
||||||
|
|
||||||
|
So now we can use the liveness constraints to get the following starting points:
|
||||||
|
|
||||||
|
Region | Contents
|
||||||
|
--------|----------
|
||||||
|
'#1 |
|
||||||
|
'#2 | `L1`
|
||||||
|
'#3 | `L1`
|
||||||
|
|
||||||
|
Now we use the outlives constraints to expand each region. Specifically, we
|
||||||
|
know that `'#2: '#3` ...
|
||||||
|
|
||||||
|
Region | Contents
|
||||||
|
--------|----------
|
||||||
|
'#1 | `L1`
|
||||||
|
'#2 | `L1, end('#3) // add contents of '#3 and end('#3)`
|
||||||
|
'#3 | `L1`
|
||||||
|
|
||||||
|
... and `'#1: '#2`, so ...
|
||||||
|
|
||||||
|
Region | Contents
|
||||||
|
--------|----------
|
||||||
|
'#1 | `L1, end('#2), end('#3) // add contents of '#2 and end('#2)`
|
||||||
|
'#2 | `L1, end('#3)`
|
||||||
|
'#3 | `L1`
|
||||||
|
|
||||||
|
Now, we need to check that no regions were too big (we don't have any type
|
||||||
|
tests to check in this case). Notice that `'#1` now contains `end('#3)`, but
|
||||||
|
we have no `where` clause or implied bound to say that `'a: 'b`... that's an
|
||||||
|
error!
|
||||||
|
|
||||||
|
### Some details
|
||||||
|
|
||||||
|
The [`RegionInferenceContext`] type contains all of the information needed to
|
||||||
|
do inference, including the universal regions from [`replace_regions_in_mir`] and
|
||||||
|
the constraints computed for each region. It is constructed just after we
|
||||||
|
compute the liveness constraints.
|
||||||
|
|
||||||
|
Here are some of the fields of the struct:
|
||||||
|
|
||||||
|
- [`constraints`]: contains all the outlives constraints.
|
||||||
|
- [`liveness_constraints`]: contains all the liveness constraints.
|
||||||
|
- [`universal_regions`]: contains the `UniversalRegions` returned by
|
||||||
|
[`replace_regions_in_mir`].
|
||||||
|
- [`universal_region_relations`]: contains relations known to be true about
|
||||||
|
universal regions. For example, if we have a where clause that `'a: 'b`, that
|
||||||
|
relation is assumed to be true while borrow checking the implementation (it
|
||||||
|
is checked at the caller), so `universal_region_relations` would contain `'a:
|
||||||
|
'b`.
|
||||||
|
- [`type_tests`]: contains some constraints on types that we must check after
|
||||||
|
inference (e.g. `T: 'a`).
|
||||||
|
- [`closure_bounds_mapping`]: used for propagating region constraints from
|
||||||
|
closures back out to the creater of the closure.
|
||||||
|
|
||||||
|
[`constraints`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/region_infer/struct.RegionInferenceContext.html#structfield.constraints
|
||||||
|
[`liveness_constraints`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/region_infer/struct.RegionInferenceContext.html#structfield.liveness_constraints
|
||||||
|
[`universal_regions`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/region_infer/struct.RegionInferenceContext.html#structfield.universal_regions
|
||||||
|
[`universal_region_relations`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/region_infer/struct.RegionInferenceContext.html#structfield.universal_region_relations
|
||||||
|
[`type_tests`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/region_infer/struct.RegionInferenceContext.html#structfield.type_tests
|
||||||
|
[`closure_bounds_mapping`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/region_infer/struct.RegionInferenceContext.html#structfield.closure_bounds_mapping
|
||||||
|
|
||||||
|
TODO: should we discuss any of the others fields? What about the SCCs?
|
||||||
|
|
||||||
|
Ok, now that we have constructed a `RegionInferenceContext`, we can do
|
||||||
|
inference. This is done by calling the [`solve`] method on the context. This
|
||||||
|
is where we call [`propagate_constraints`] and then check the resulting type
|
||||||
|
tests and universal regions, as discussed above.
|
||||||
|
|
||||||
|
[`propagate_constraints`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/region_infer/struct.RegionInferenceContext.html#method.propagate_constraints
|
||||||
|
[`check_type_tests`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/region_infer/struct.RegionInferenceContext.html#method.check_type_tests
|
||||||
|
[`check_universal_regions`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/region_infer/struct.RegionInferenceContext.html#method.check_universal_regions
|
||||||
|
|
||||||
|
## Closures
|
||||||
|
|
||||||
|
When we are checking the type tests and universal regions, we may come across a
|
||||||
|
constraint that we can't prove yet if we are in a closure body! However, the
|
||||||
|
necessary constraints may actually hold (we just don't know it yet). Thus, if
|
||||||
|
we are inside a closure, we just collect all the constraints we can't prove yet
|
||||||
|
and return them. Later, when we are borrow check the MIR node that created the
|
||||||
|
closure, we can also check that these constraints hold. At that time, if we
|
||||||
|
can't prove they hold, we report an error.
|
||||||
|
|
||||||
## Placeholders and universes
|
## Placeholders and universes
|
||||||
|
|
||||||
|
|
@ -534,3 +688,6 @@ Now constraint propagation is done, but when we check the outlives
|
||||||
relationships, we find that `V2` includes this new element `placeholder(1)`,
|
relationships, we find that `V2` includes this new element `placeholder(1)`,
|
||||||
so we report an error.
|
so we report an error.
|
||||||
|
|
||||||
|
## Borrow Checker Errors
|
||||||
|
|
||||||
|
TODO: we should discuss how to generate errors from the results of these analyses.
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue