# 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 (`member R_m of [R_c...]`), which arise from impl Trait.

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

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 in this section.)

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

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

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

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` 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 be 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 concerned 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. 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, which are described in a later section.