Skip to content

Fill out the borrowck chapter a bit more #234

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 5 commits into from
Jan 11, 2019
Merged

Fill out the borrowck chapter a bit more #234

Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
97e8530
minor improvements
mark-i-m Nov 9, 2018
5194978
add a few links to rustdocs
mark-i-m Nov 9, 2018
9f43509
fill out the borrowck chapter a bit more
mark-i-m Nov 9, 2018
7acbc48
a few updates
mark-i-m Dec 11, 2018
a69982d
added example, reworked inference section
mark-i-m Dec 11, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 4 additions & 3 deletions src/borrow_check.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,13 +51,14 @@ the [`mir_borrowck`] query.
the purpose of this type check is to determine all of the constraints between
different regions.
- 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.
- 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
`*a + 1`, then we would check that the variable `a` is initialized
and that it is not mutably borrowed, as either of those would
require an error to be reported.
- Doing this check requires the results of all the previous analyses.
require an error to be reported. Doing this check requires the results of all
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
126 changes: 104 additions & 22 deletions src/borrow_check/region_inference.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ deprecated once they become the standard kind of lifetime.)

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
signature of the function (e.g., `'a` in `fn foo<'a>(&'a u32) {
... }`). These are called the "universal" or "free" regions – in
Expand All @@ -21,45 +21,49 @@ The MIR-based region analysis consists of two major functions:
not of much interest. The intention is that – eventually – they
will be "erased regions" (i.e., no information at all), since we
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
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 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
region variables (e.g., that one variable must outlive another
one) to reflect the subtyping relationships that arise.
- It also adds **liveness constraints** that arise from where variables
are used.
- More details to come, though the [NLL RFC] also includes fairly thorough
(and hopefully readable) coverage.
- After this, we create a [`RegionInferenceContext`] with the constraints we
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
[`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
[MIR type checker]: ./type_check.md

## Universal regions

*to be written* – explain the `UniversalRegions` type
The [`UnversalRegions`] type represents a collection of _unversal_ regions
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nit: "Universal" is misspelled as "unversal" in few places here. I think I would explain this through an example. Basically say something about how it computes information about the various named lifetimes in scope and their relationships to one another e.g., for the following function:

fn foo<'a>(x: &'a u32) { .. }

we would create a "universal region" 'a as well as 'static. (I really want to rename this, but anyway.)

That's probably good enough to start. The various categories of lifetimes around closures are interesting but maybe not needed here.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

TBH, I didn't dig into this part of the code, so I'm not really sure how it computes that info. I did add the other things you mentioned, though, and a note to add more.

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
TODO: is there more to write here?

*to be written* – describe the `RegionInferenceContext` and
the role of `liveness_constraints` vs other `constraints`, plus
[`UniversalRegions`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/universal_regions/struct.UniversalRegions.html

## Closures

*to be written*

<a name="mirtypeck"></a>
## Region variables

## The MIR type-check

## Representing the "values" of a region variable

The value of a region can be thought of as a **set**; we call the
domain of this set a `RegionElement`. In the code, the value for all
regions is maintained in
The value of a region can be thought of as a **set** of points in the MIR where
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This isn't really complete. It's actually a set of points + a set of universal regions.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

But adding a universal region is adding a set, no?

Also, the universal regions are the end('foo) elements, correct?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I wondered if you would call me on that. =)

Yes, it's best I think to think of universal regions as "unknown sets", but they are not sets of points in MIR -- or at least they include points from outside the fn being investigated (to me, MIR implies "the source of one function).

I think it's also valid to think of a region as a "set of elements" where an "element" is a "MIR point" or "universal regions". That's certainly how it's implemented.

I guess I'm not sure what's the best way to describe it. I'm trying to remember if there is some point where the distinction is important. I'm also more and more trying to move into the polonius mindset, which is sort of different.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I updated this sentence. Let me know what you think.

I'm trying to remember if there is some point where the distinction is important.

Perhaps something around placeholders?

I'm also more and more trying to move into the polonius mindset, which is sort of different.

Would it be better to stay in the "NLL" mindset here for consistency and add a new chapter on Polonius?

the region is valid; we call the domain of this set a `RegionElement`. In the
code, the value for all regions is maintained in
[the `rustc_mir::borrow_check::nll::region_infer` module][ri]. For
each region we maintain a set storing what elements are present in its
value (to make this efficient, we give each kind of element an index,
Expand All @@ -83,11 +87,86 @@ The kinds of region elements are as follows:
for details on placeholders, see the section
[placeholders and universes](#placeholder).

## Constraints

Before we can infer the value of regions, we need to collect constraints on the
regions. There are two primary types of constraints.

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.

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.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

can we link to the rustdoc here, or otherwise try to prevent bitrot?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

maybe not worth it, I have some thoughts on how to revisit this section

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I tried to rework this section a bit to factor out the details from the meat. I also added an example.

I am a bit fuzzy on this part, so please let me know if you spot any problems. In particular, the example is a bit hand-wavey in some places...

- `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.

TODO: should we discuss any of the others fields? What about the SCCs?
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I feel like overall this discussion is a bit too focused on the "low-level details" and not much about the high-level process, but it seems like a good start.


Ok, now that we have constructed a `RegionInferenceContext`, we can do
inference. This is done by calling the [`solve`] method on the context.

We will start off the value of each region with the liveness constraints (the
places we already know must be in the region). We will then use the outlives
constraints to widen each region until all constraints are met. This is done in
[`propagate_constraints`]. For each region, if `'a: 'b`, we add all elements of
`'b` to `'a`.

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.

[`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.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This seems fine, but really needs some examples


## Causal tracking

*to be written* – describe how we can extend the values of a variable
with causal tracking etc

TODO: is this what I described above or something else?

<a name="placeholder"></a>

## Placeholders and universes
Expand Down Expand Up @@ -534,3 +613,6 @@ Now constraint propagation is done, but when we check the outlives
relationships, we find that `V2` includes this new element `placeholder(1)`,
so we report an error.

## Borrow Checker Errors

TODO: we should discuss how to generate errors from the results of these analyses.