Skip to content

Region inference member constraints #344

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.

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
Show file tree
Hide file tree
Changes from 5 commits
Commits
Show all changes
30 commits
Select commit Hold shift + click to select a range
20347ca
fix typo
nikomatsakis Jun 18, 2019
f2c8574
break out parts of the region inference chapter into sub-chapters
nikomatsakis Jun 18, 2019
7ec2b86
start filling out the constraint propagation chapter in more detail
nikomatsakis Jun 18, 2019
9e62f21
describe region inference and member constraints in some detail
nikomatsakis Jun 20, 2019
b8ff361
adjust overview slightly
nikomatsakis Jun 20, 2019
8f2f27f
Update src/borrow_check/region_inference/constraint_propagation.md
nikomatsakis Jun 24, 2019
1f8181c
Update src/borrow_check/region_inference/lifetime_parameters.md
nikomatsakis Jun 24, 2019
addc52b
Update src/borrow_check/region_inference/lifetime_parameters.md
nikomatsakis Jun 24, 2019
bfd8e66
Update src/borrow_check/region_inference/lifetime_parameters.md
nikomatsakis Jun 24, 2019
78834e5
Update src/borrow_check/region_inference/constraint_propagation.md
nikomatsakis Jun 24, 2019
8c6e8ae
Update src/borrow_check/region_inference/constraint_propagation.md
nikomatsakis Jun 24, 2019
0863713
Update src/borrow_check/region_inference/constraint_propagation.md
nikomatsakis Jun 24, 2019
c6b4f83
Update src/borrow_check/region_inference/constraint_propagation.md
nikomatsakis Jun 24, 2019
3ea4723
Update src/borrow_check/region_inference/constraint_propagation.md
nikomatsakis Jun 24, 2019
2563350
Update src/borrow_check/region_inference/constraint_propagation.md
nikomatsakis Jun 24, 2019
5f2af11
Update src/borrow_check/region_inference/constraint_propagation.md
nikomatsakis Jun 24, 2019
3273d19
Update src/borrow_check/region_inference/member_constraints.md
nikomatsakis Jun 24, 2019
7e51cd3
Update src/borrow_check/region_inference/lifetime_parameters.md
nikomatsakis Jun 24, 2019
d7e2823
Update src/borrow_check/region_inference/member_constraints.md
nikomatsakis Jun 24, 2019
35ff1f5
Update src/borrow_check/region_inference/member_constraints.md
nikomatsakis Jun 24, 2019
7d54887
Update src/borrow_check/region_inference/constraint_propagation.md
nikomatsakis Jun 24, 2019
88f13cb
Update src/borrow_check/region_inference/member_constraints.md
nikomatsakis Jun 24, 2019
c12a025
Update src/borrow_check/region_inference/constraint_propagation.md
nikomatsakis Jun 24, 2019
06548ae
Update src/borrow_check/region_inference/member_constraints.md
nikomatsakis Jun 24, 2019
c44f66f
Update src/borrow_check/region_inference/placeholders_and_universes.md
nikomatsakis Jun 24, 2019
1cd4efb
Update src/borrow_check/region_inference/placeholders_and_universes.md
nikomatsakis Jun 24, 2019
348e2be
Update src/borrow_check/region_inference/placeholders_and_universes.md
nikomatsakis Jun 24, 2019
3ecff8c
fix indentation
nikomatsakis Jun 24, 2019
564b1b3
add `point` to the glossary and link a use of it
nikomatsakis Jun 24, 2019
425c1cb
fix long line
mark-i-m Jun 26, 2019
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
6 changes: 6 additions & 0 deletions src/SUMMARY.md
Original file line number Diff line number Diff line change
Expand Up @@ -76,6 +76,12 @@
- [Move paths](./borrow_check/moves_and_initialization/move_paths.md)
- [MIR type checker](./borrow_check/type_check.md)
- [Region inference](./borrow_check/region_inference.md)
- [Constraint propagation](./borrow_check/region_inference/constraint_propagation.md)
- [Lifetime parameters](./borrow_check/region_inference/lifetime_parameters.md)
- [Member constraints](./borrow_check/region_inference/member_constraints.md)
- [Placeholders and universes](./borrow_check/region_inference/placeholders_and_universes.md)
- [Closure constraints](./borrow_check/region_inference/closure_constraints.md)
- [Errror reporting](./borrow_check/region_inference/error_reporting.md)
- [Two-phase-borrows](./borrow_check/two_phase_borrows.md)
- [Constant evaluation](./const-eval.md)
- [miri const evaluator](./miri.md)
Expand Down
488 changes: 17 additions & 471 deletions src/borrow_check/region_inference.md

Large diffs are not rendered by default.

10 changes: 10 additions & 0 deletions src/borrow_check/region_inference/closure_constraints.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
# Propagating closure constraints

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.
222 changes: 222 additions & 0 deletions src/borrow_check/region_inference/constraint_propagation.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,222 @@
# Constraint propagation

The main work of the region inference is **constraint propagation**,
which is done in the [`propagate_constraints`] function. There are
three sorts of constraints that are used in NLL, and we'll explain how
`propagate_constraints` works by "layering" those sorts of constraints
on one at a time (each of them is fairly independent from the others):

- liveness constraints (`R live at E`), which arise from liveness;
- outlives constraints (`R1: R2`), which arise from subtyping;
- [member constraints][m_c] (`member R_m of [R_c...]`), which arise from impl Trait.

[`propagate_constraints`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/region_infer/struct.RegionInferenceContext.html#method.propagate_constraints
[m_c]: ./member_constraints.html

In this chapter, we'll explain the "heart" of constraint propagation,
covering both liveness and outlives constraints.

## Notation and high-level concepts

Conceptually, region inference is a "fixed-point" computation. It is
given some set of constraints `{C}` and it computes a set of values
`Values: R -> {E}` that maps each region `R` to a set of elements
`{E}` (see [here][riv] for more notes on region elements):

- Initially, each region is mapped to an empty set, so `Values(R) =
{}` for all regions `R`.
- Next, we process the constraints repeatedly until a fixed-point is reached:
- For each constraint C:
- Update `Values` as needed to satisfy the constraint

[riv]: ../region-inference.html#region-variables

As a simple example, if we have a liveness constraint `R live at E`,
then we can apply `Values(R) = Values(R) union {E}` to make the
constraint be satisfied. Similarly, if we have an outlives constraints
`R1: R2`, we can apply `Values(R1) = Values(R1) union Values(R2)`.
(Member constraints are more complex and we discuss them below.)

In practice, however, we are a bit more clever. Instead of applying
the constraints in a loop, we can analyze the constraints and figure
out the correct order to apply them, so that we only have to apply
each constraint once in order to find the final result.

Similarly, in the implementation, the `Values` set is stored in the
`scc_values` field, but they are indexed not by a *region* but by a
*strongly connected component* (SCC). SCCs are an optimization that
avoids a lot of redundant storage and computation. They are explained
in the section on outlives constraints.

## Liveness constraints

A **liveness constraint** arises when some variable whose type
includes a region R is live at some point P. This simply means that
the value of R must include the point P. Liveness constraints are
computed by the MIR type checker.

A liveness constraint `R live at E` is satisfied if `E` is a member of
`Values(R)`. So to "apply" such a constraint to `Values`, we just have
to compute `Values(R) = Values(R) union {E}`.

The liveness values are computed in the type-check and passes to the
region inference upon creation in the `liveness_constraints` argument.
These are not represented as individual constraints like `R live at E`
though; instead, we store a (sparse) bitset per region variable (of
type [`LivenessValues`]). This way we only need a single bit for each
liveness constraint.

[`liveness_constraints`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/region_infer/struct.RegionInferenceContext.html#structfield.liveness_constraints
[`LivenessValues`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/region_infer/values/struct.LivenessValues.html

One thing that is worth mentioning: All lifetime parameters are always
considered to be live over the entire function body. This is because
they correspond to some portion of the *caller's* execution, and that
execution clearly includes the time spent in this function, since the
caller is waiting for us to return.

## Outlives constraints

An outlives constraint `'a: 'b` indicates that the value of `'a` must
be a **superset** of the value of `'b`. That is, an outlives
constraint `R1: R2` is satisfied if `Values(R1)` is a superset of
`Values(R2)`. So to "apply" such a constraint to `Values`, we just
have to compute `Values(R1) = Values(R1) union Values(R2)`.

One observation that follows from this is that if you have `R1: R2`
and `R2: R1`, then `R1 = R2` must be true. Similarly, if you have:

```
R1: R2
R2: R3
R3: R4
R4: R1
```

then `R1 = R2 = R3 = R4` follows. We take advantage of this to make things
much faster, as described shortly.

In the code, the set of outlives constraints is given to the region
inference context on creation in a parameter of type
[`ConstraintSet`]. The constraint set is basically just a list of `'a:
'b` constraints.

### The outlives constraint graph and SCCs

In order to work more efficiently with outlives constraints, they are
[converted into the form of a graph][graph-fn], where the nodes of the
graph are region variables (`'a`, `'b`) and each constraint `'a: 'b`
induces an edge `'a -> 'b`. This conversion happens in the
[`RegionInferenceContext::new`] function that creates the inference
context.

[`ConstraintSet`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/constraints/struct.ConstraintSet.html
[graph-fn]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/constraints/struct.ConstraintSet.html#method.graph
[`RegionInferenceContext::new`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/region_infer/struct.RegionInferenceContext.html#method.new

When using a graph representation, we can detect regions that must be equal
by looking for cycles. That is, if you have a constraint like

```
'a: 'b
'b: 'c
'c: 'd
'd: 'a
```

then this will correspond to a cycle in the graph containing the
elements `'a...'d`.

Therefore, one of the first things that we do in propagating region
values is to compute the **strongly connected components** (SCCs) in
the constraint graph. The result is stored in the [`constraint_sccs`]
field. You can then easily find the SCC that a region `r` is a part of
by invoking `constraint_sccs.scc(r)`.

Working in terms of SCCs allows us to be more efficient: if we have a
set of regions `'a...'d` that are part of a single SCC, we don't have
to compute/store their values separarely. We can just store one value
**for the SCC**, since they must all be equal.

If you look over the region inference code, you will see that a number
of fields are defined in terms of SCCs. For example, the
[`scc_values`] field stores the values of each SCC. To get the value
of a specific region `'a` then, we first figure out the SCC that the
region is a part of, and then find the value of that SCC.

[`constraint_sccs`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/region_infer/struct.RegionInferenceContext.html#structfield.constraint_sccs
[`scc_values`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/region_infer/struct.RegionInferenceContext.html#structfield.scc_values

When we compute SCCs, we not only figure out which regions are a
member of each SCC, we also figure out the edges between them. So for example
consider this set of outlives constraints:

```
'a: 'b
'b: 'a

'a: 'c

'c: 'd
'd: 'c
```

Here we have two SCCs: S0 contains `'a` and `'b`, and S1 contains `'c`
Copy link
Member

Choose a reason for hiding this comment

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

Suggested change
Here we have two SCCs: S0 contains `'a` and `'b`, and S1 contains `'c`
Here we have two SCCs: `S0` contains `'a` and `'b`, and S1 contains `'c`

and `'d`. But these SCCs are not independent: because `'a: 'c`, that
means that `S0: S1` as well. That is -- the value of `S0` must be a
superset of the value of `S1`. One crucial thing is that this graph of
SCCs is always a DAG -- that is, it never has cycles. This is because
all the cycles have been removed to form the SCCs themselves.

### Applying liveness constraints to SCCs

The liveness constraints that come in from the type-checker are
expressed in terms of regions -- that is, we have a map like
`Liveness: R -> {E}`. But we want our final result to be expressed
in terms of SCCs -- we can integrate these liveness constraints very
easily just by taking the union:

```
for each region R:
let S by the SCC that contains R
Values(S) = Values(S) union Liveness(R)
```

In the region inferencer, this step is done in [`RegionInferenceContext::new`].

### Applying outlives constraints

Once we have computed the DAG of SCCs, we use that to structure out
entire computation. If we have an edge `S1 -> S2` between two SCCs,
that means that `Values(S1) >= Values(S2)` must hold. So, to compute
the value of `S1`, we first compute the values of each successor `S2`.
Then we simply union all of those values together. To use a
quasi-iterator-like notation:

```
Values(S1) =
s1.successors()
.map(|s2| Values(s2))
.union()
```

In the code, this work starts in the [`propagate_constraints`]
function, which iterates over all the SCCs. For each SCC S1, we
compute its value by first computing the value of its
successors. Since SCCs form a DAG, we don't have to be conecrned about
cycles, though we do need to keep a set around to track whether we
have already processed a given SCC or not. For each successor S2, once
we have computed S2's value, we can union those elements into the
value for S1. (Although we have to be careful in this process to
properly handle [higher-ranked
placeholders](./placeholders_and_universes.html). Note that the value
for S1 already contains the liveness constraints, since they were
added in [`RegionInferenceContext::new`].

Once that process is done, we now have the "minimal value" for S1,
taking into account all of the liveness and outlives
constraints. However, in order to complete the process, we must also
consider [member constraints][m_c], which are described in [a later
section][m_c].


3 changes: 3 additions & 0 deletions src/borrow_check/region_inference/error_reporting.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
# Reporting region errors

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

Choose a reason for hiding this comment

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

I can actually write a bit here from working on rust-lang/rust#58281

125 changes: 125 additions & 0 deletions src/borrow_check/region_inference/lifetime_parameters.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,125 @@
# Universal regions

"Universal regions" is the name that the code uses to refer to "named
lifetimes" -- e.g., lifetime parameters and `'static`. The name
derives from the fact that such lifetimes are "universally quantified"
(i.e., we must make sure the code is true for all values of those
lifetimes). It is worth spending a bit of discussing how lifetime
parameters are handled during region inference. Consider this example:

```rust
fn foo<'a, 'b>(x: &'a u32, y: &'b u32) -> &'b u32 {
x
}
```

This example is intended not to compile, because we are returning `x`,
which has type `&'a u32`, but our signature promises that we will
return a `&'b u32` value. But how are lifetimes like `'a` and `'b
integrated into region inference, and how this error wind up being
detected?

## Universal regions and their relationships to one another

Early on in region inference, one of the first things we do is to
construct a [`UniversalRegions`] struct. This struct tracks the
various universal regions in scope on a particular function. We also
create a [`UniversalRegionRelations`] struct, which tracks their
relationships to one another. So if you have e.g. `where 'a: 'b`, then
the [`UniversalRegionRelations`] struct would track that `'a: 'b` is
known to hold (which could be tested with the [`outlives`] function.

[`UniversalRegions`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/universal_regions/struct.UniversalRegions.html
[`UniversalRegionsRelations`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/type_check/free_region_relations/struct.UniversalRegionRelations.html
[`outlives`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/type_check/free_region_relations/struct.UniversalRegionRelations.html#method.outlives

## Everything is a region variable

One important aspect of how NLL region inference works is that **all
lifetimes** are represented as numbered variables. This means that the
only variant of [`ty::RegionKind`] that we use is the [`ReVar`]
variant. These region variables are broken into two major categories,
based on their index:

[`ty::RegionKind`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc/ty/enum.RegionKind.html
[`ReVar`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc/ty/enum.RegionKind.html#variant.ReVar

- 0..N: universal regions -- the ones we are discussing here. In this
case, the code must be correct with respect to any value of those
variables that meets the declared relationships.
- N..M: existential regions -- inference variables where the region
inferencer is tasked with finding *some* suitable value.

In fact, the universal regions can be further subdivided based on
where they were brought into scope (see the [`RegionClassification`]
type). These subdivions are not important for the topics discussed
here, but become important when we consider [closure constraint
propagation](./closure_constraints.html), so we discuss them there.

[`RegionClassification`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/universal_regions/enum.RegionClassification.html#variant.Local

## Universal lifetimes as the elements of a region's value

As noted previously, the value that we infer for each region is a set
`{E}`. The elements of this set can be points in the control-flow
graph, but they can also be an element `end('a)` corresponding to each
universal lifetime `'a`. If the value for some region `R0` includes
`end('a`), then this implies that R0 must extend until the end of `'a`
in the caller.

## The "value" of a universal region

During region inference, we compute a value for each universal region
in the same way as we compute values for other regions. This value
represents, effectively, the **lower bound** on that universal region
-- the things that it must outlive. We now describe how we use this
value to check for errors.

## Liveness and universal regions

All universal regions have an initial liveness constraint that
includes the entire function body. This is because lifetime parameters
are defined in the caller and must include the entirety of the
function call that invokes this particular function. In addition, each
universal region `'a` includes itself (that is, `end('a)`) in its
liveness constraint (i.e., `'a` must extend until the end of
itself). In the code, these liveness constraints are setup in
[`init_free_and_bound_regions`].

[`init_free_and_bound_regions`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/nll/region_infer/struct.RegionInferenceContext.html#method.init_free_and_bound_regions

## Propagating outlives constraints for universal regions

So, consider the first example of this section:

```rust
fn foo<'a, 'b>(x: &'a u32, y: &'b u32) -> &'b u32 {
x
}
```

Here, returning `x` requires that `&'a u32 <: &'b u32`, which gives
rise to an outlives constraint `'a: 'b`. Combined with our default liveness
constraints we get:

```
'a live at {B, end('a)} // B represents the "bunction body"
'b live at {B, end('b)}
'a: 'b
```

When we process the `'a: 'b` constraint, therefore, we will add
`end('b)` into the value for `'a`, resulting in a final value of `{B,
end('a), end('b)}`.

## Detecting errors

Once we have finished constraint propagation, we then enforce a
constraint that if some universal region `'a` includes an element
`end('b)`, then `'a: 'b` must be declared in the function's bounds. If
not, as in our example, that is an error. This check is done in the
[`check_universal_regions`] function, which simply iterates over all
universal regions, inspects their final value, and tests against the
declared [`UniversalRegionRelations`].

[`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
Loading