]>
Commit | Line | Data |
---|---|---|
dc9dc135 XL |
1 | # Constraint propagation |
2 | ||
6a06907d XL |
3 | <!-- toc --> |
4 | ||
dc9dc135 XL |
5 | The main work of the region inference is **constraint propagation**, |
6 | which is done in the [`propagate_constraints`] function. There are | |
7 | three sorts of constraints that are used in NLL, and we'll explain how | |
8 | `propagate_constraints` works by "layering" those sorts of constraints | |
9 | on one at a time (each of them is fairly independent from the others): | |
10 | ||
11 | - liveness constraints (`R live at E`), which arise from liveness; | |
12 | - outlives constraints (`R1: R2`), which arise from subtyping; | |
13 | - [member constraints][m_c] (`member R_m of [R_c...]`), which arise from impl Trait. | |
14 | ||
dfeec247 | 15 | [`propagate_constraints`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/region_infer/struct.RegionInferenceContext.html#method.propagate_constraints |
416331ca | 16 | [m_c]: ./member_constraints.md |
dc9dc135 XL |
17 | |
18 | In this chapter, we'll explain the "heart" of constraint propagation, | |
19 | covering both liveness and outlives constraints. | |
20 | ||
21 | ## Notation and high-level concepts | |
22 | ||
23 | Conceptually, region inference is a "fixed-point" computation. It is | |
24 | given some set of constraints `{C}` and it computes a set of values | |
25 | `Values: R -> {E}` that maps each region `R` to a set of elements | |
26 | `{E}` (see [here][riv] for more notes on region elements): | |
27 | ||
28 | - Initially, each region is mapped to an empty set, so `Values(R) = | |
29 | {}` for all regions `R`. | |
30 | - Next, we process the constraints repeatedly until a fixed-point is reached: | |
31 | - For each constraint C: | |
32 | - Update `Values` as needed to satisfy the constraint | |
33 | ||
416331ca | 34 | [riv]: ../region_inference.md#region-variables |
dc9dc135 XL |
35 | |
36 | As a simple example, if we have a liveness constraint `R live at E`, | |
37 | then we can apply `Values(R) = Values(R) union {E}` to make the | |
38 | constraint be satisfied. Similarly, if we have an outlives constraints | |
39 | `R1: R2`, we can apply `Values(R1) = Values(R1) union Values(R2)`. | |
40 | (Member constraints are more complex and we discuss them [in this section][m_c].) | |
41 | ||
42 | In practice, however, we are a bit more clever. Instead of applying | |
43 | the constraints in a loop, we can analyze the constraints and figure | |
44 | out the correct order to apply them, so that we only have to apply | |
45 | each constraint once in order to find the final result. | |
46 | ||
47 | Similarly, in the implementation, the `Values` set is stored in the | |
48 | `scc_values` field, but they are indexed not by a *region* but by a | |
49 | *strongly connected component* (SCC). SCCs are an optimization that | |
50 | avoids a lot of redundant storage and computation. They are explained | |
51 | in the section on outlives constraints. | |
52 | ||
53 | ## Liveness constraints | |
54 | ||
55 | A **liveness constraint** arises when some variable whose type | |
56 | includes a region R is live at some [point] P. This simply means that | |
57 | the value of R must include the point P. Liveness constraints are | |
58 | computed by the MIR type checker. | |
59 | ||
ba9703b0 | 60 | [point]: ../../appendix/glossary.md#point |
dc9dc135 XL |
61 | |
62 | A liveness constraint `R live at E` is satisfied if `E` is a member of | |
63 | `Values(R)`. So to "apply" such a constraint to `Values`, we just have | |
64 | to compute `Values(R) = Values(R) union {E}`. | |
65 | ||
66 | The liveness values are computed in the type-check and passed to the | |
67 | region inference upon creation in the `liveness_constraints` argument. | |
68 | These are not represented as individual constraints like `R live at E` | |
69 | though; instead, we store a (sparse) bitset per region variable (of | |
70 | type [`LivenessValues`]). This way we only need a single bit for each | |
71 | liveness constraint. | |
72 | ||
dfeec247 XL |
73 | [`liveness_constraints`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/region_infer/struct.RegionInferenceContext.html#structfield.liveness_constraints |
74 | [`LivenessValues`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/region_infer/values/struct.LivenessValues.html | |
dc9dc135 XL |
75 | |
76 | One thing that is worth mentioning: All lifetime parameters are always | |
77 | considered to be live over the entire function body. This is because | |
78 | they correspond to some portion of the *caller's* execution, and that | |
79 | execution clearly includes the time spent in this function, since the | |
80 | caller is waiting for us to return. | |
81 | ||
82 | ## Outlives constraints | |
83 | ||
84 | An outlives constraint `'a: 'b` indicates that the value of `'a` must | |
85 | be a **superset** of the value of `'b`. That is, an outlives | |
86 | constraint `R1: R2` is satisfied if `Values(R1)` is a superset of | |
87 | `Values(R2)`. So to "apply" such a constraint to `Values`, we just | |
88 | have to compute `Values(R1) = Values(R1) union Values(R2)`. | |
89 | ||
90 | One observation that follows from this is that if you have `R1: R2` | |
91 | and `R2: R1`, then `R1 = R2` must be true. Similarly, if you have: | |
92 | ||
416331ca | 93 | ```txt |
dc9dc135 XL |
94 | R1: R2 |
95 | R2: R3 | |
96 | R3: R4 | |
97 | R4: R1 | |
98 | ``` | |
99 | ||
100 | then `R1 = R2 = R3 = R4` follows. We take advantage of this to make things | |
101 | much faster, as described shortly. | |
102 | ||
103 | In the code, the set of outlives constraints is given to the region | |
104 | inference context on creation in a parameter of type | |
74b04a01 | 105 | [`OutlivesConstraintSet`]. The constraint set is basically just a list of `'a: |
dc9dc135 XL |
106 | 'b` constraints. |
107 | ||
108 | ### The outlives constraint graph and SCCs | |
109 | ||
110 | In order to work more efficiently with outlives constraints, they are | |
111 | [converted into the form of a graph][graph-fn], where the nodes of the | |
112 | graph are region variables (`'a`, `'b`) and each constraint `'a: 'b` | |
113 | induces an edge `'a -> 'b`. This conversion happens in the | |
114 | [`RegionInferenceContext::new`] function that creates the inference | |
115 | context. | |
116 | ||
74b04a01 | 117 | [`OutlivesConstraintSet`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/constraints/struct.OutlivesConstraintSet.html |
dfeec247 XL |
118 | [graph-fn]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/constraints/struct.OutlivesConstraintSet.html#method.graph |
119 | [`RegionInferenceContext::new`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/region_infer/struct.RegionInferenceContext.html#method.new | |
dc9dc135 XL |
120 | |
121 | When using a graph representation, we can detect regions that must be equal | |
122 | by looking for cycles. That is, if you have a constraint like | |
123 | ||
416331ca | 124 | ```txt |
dc9dc135 XL |
125 | 'a: 'b |
126 | 'b: 'c | |
127 | 'c: 'd | |
128 | 'd: 'a | |
129 | ``` | |
130 | ||
131 | then this will correspond to a cycle in the graph containing the | |
132 | elements `'a...'d`. | |
133 | ||
134 | Therefore, one of the first things that we do in propagating region | |
135 | values is to compute the **strongly connected components** (SCCs) in | |
136 | the constraint graph. The result is stored in the [`constraint_sccs`] | |
137 | field. You can then easily find the SCC that a region `r` is a part of | |
138 | by invoking `constraint_sccs.scc(r)`. | |
139 | ||
140 | Working in terms of SCCs allows us to be more efficient: if we have a | |
141 | set of regions `'a...'d` that are part of a single SCC, we don't have | |
416331ca | 142 | to compute/store their values separately. We can just store one value |
dc9dc135 XL |
143 | **for the SCC**, since they must all be equal. |
144 | ||
145 | If you look over the region inference code, you will see that a number | |
146 | of fields are defined in terms of SCCs. For example, the | |
147 | [`scc_values`] field stores the values of each SCC. To get the value | |
148 | of a specific region `'a` then, we first figure out the SCC that the | |
149 | region is a part of, and then find the value of that SCC. | |
150 | ||
dfeec247 XL |
151 | [`constraint_sccs`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/region_infer/struct.RegionInferenceContext.html#structfield.constraint_sccs |
152 | [`scc_values`]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir/borrow_check/region_infer/struct.RegionInferenceContext.html#structfield.scc_values | |
dc9dc135 XL |
153 | |
154 | When we compute SCCs, we not only figure out which regions are a | |
155 | member of each SCC, we also figure out the edges between them. So for example | |
156 | consider this set of outlives constraints: | |
157 | ||
416331ca | 158 | ```txt |
dc9dc135 XL |
159 | 'a: 'b |
160 | 'b: 'a | |
161 | ||
162 | 'a: 'c | |
163 | ||
164 | 'c: 'd | |
165 | 'd: 'c | |
166 | ``` | |
167 | ||
168 | Here we have two SCCs: S0 contains `'a` and `'b`, and S1 contains `'c` | |
169 | and `'d`. But these SCCs are not independent: because `'a: 'c`, that | |
170 | means that `S0: S1` as well. That is -- the value of `S0` must be a | |
171 | superset of the value of `S1`. One crucial thing is that this graph of | |
172 | SCCs is always a DAG -- that is, it never has cycles. This is because | |
173 | all the cycles have been removed to form the SCCs themselves. | |
174 | ||
175 | ### Applying liveness constraints to SCCs | |
176 | ||
177 | The liveness constraints that come in from the type-checker are | |
178 | expressed in terms of regions -- that is, we have a map like | |
179 | `Liveness: R -> {E}`. But we want our final result to be expressed | |
180 | in terms of SCCs -- we can integrate these liveness constraints very | |
181 | easily just by taking the union: | |
182 | ||
416331ca | 183 | ```txt |
dc9dc135 XL |
184 | for each region R: |
185 | let S be the SCC that contains R | |
186 | Values(S) = Values(S) union Liveness(R) | |
187 | ``` | |
188 | ||
189 | In the region inferencer, this step is done in [`RegionInferenceContext::new`]. | |
190 | ||
191 | ### Applying outlives constraints | |
192 | ||
193 | Once we have computed the DAG of SCCs, we use that to structure out | |
194 | entire computation. If we have an edge `S1 -> S2` between two SCCs, | |
195 | that means that `Values(S1) >= Values(S2)` must hold. So, to compute | |
196 | the value of `S1`, we first compute the values of each successor `S2`. | |
197 | Then we simply union all of those values together. To use a | |
198 | quasi-iterator-like notation: | |
199 | ||
416331ca | 200 | ```txt |
dc9dc135 XL |
201 | Values(S1) = |
202 | s1.successors() | |
203 | .map(|s2| Values(s2)) | |
204 | .union() | |
205 | ``` | |
206 | ||
207 | In the code, this work starts in the [`propagate_constraints`] | |
208 | function, which iterates over all the SCCs. For each SCC `S1`, we | |
209 | compute its value by first computing the value of its | |
210 | successors. Since SCCs form a DAG, we don't have to be concerned about | |
211 | cycles, though we do need to keep a set around to track whether we | |
212 | have already processed a given SCC or not. For each successor `S2`, once | |
213 | we have computed `S2`'s value, we can union those elements into the | |
214 | value for `S1`. (Although we have to be careful in this process to | |
215 | properly handle [higher-ranked | |
216 | placeholders](./placeholders_and_universes.html). Note that the value | |
217 | for `S1` already contains the liveness constraints, since they were | |
218 | added in [`RegionInferenceContext::new`]. | |
219 | ||
220 | Once that process is done, we now have the "minimal value" for `S1`, | |
221 | taking into account all of the liveness and outlives | |
222 | constraints. However, in order to complete the process, we must also | |
223 | consider [member constraints][m_c], which are described in [a later | |
224 | section][m_c]. |