From 9f435099c106c7c26a9b9ed2007b4a7a0ea9c708 Mon Sep 17 00:00:00 2001 From: Mark Mansi Date: Thu, 8 Nov 2018 21:34:17 -0600 Subject: [PATCH] fill out the borrowck chapter a bit more --- src/borrow_check/region_inference.md | 109 ++++++++++++++++++++++----- 1 file changed, 92 insertions(+), 17 deletions(-) diff --git a/src/borrow_check/region_inference.md b/src/borrow_check/region_inference.md index e35849ef..d08e06a8 100644 --- a/src/borrow_check/region_inference.md +++ b/src/borrow_check/region_inference.md @@ -24,7 +24,7 @@ The MIR-based region analysis consists of two major functions: - [`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 checker will however create **outlives constraints** between @@ -44,29 +44,26 @@ The MIR-based region analysis consists of two major functions: [`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 +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 +## Region variables -*to be written* - - - -## 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 +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, @@ -90,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. +- `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? + +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. + ## 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? + ## Placeholders and universes @@ -541,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.