Module rustc_mir_build::thir::pattern::usefulness

source ·
Expand description

Match exhaustiveness and reachability algorithm

This file contains the logic for exhaustiveness and reachability checking for pattern-matching. Specifically, given a list of patterns in a match, we can tell whether: (a) a given pattern is reachable (reachability) (b) the patterns cover every possible value for the type (exhaustiveness)

The algorithm implemented here is inspired from the one described in this paper. We have however changed it in various ways to accommodate the variety of patterns that Rust supports. We thus explain our version here, without being as precise.

Fun fact: computing exhaustiveness is NP-complete, because we can encode a SAT problem as an exhaustiveness problem. See here for the fun details.

Summary

The algorithm is given as input a list of patterns, one for each arm of a match, and computes the following:

  • a set of values that match none of the patterns (if any),
  • for each subpattern (taking into account or-patterns), whether it would catch any value that isn’t caught by a pattern before it, i.e. whether it is reachable.

To a first approximation, the algorithm works by exploring all possible values for the type being matched on, and determining which arm(s) catch which value. To make this tractable we cleverly group together values, as we’ll see below.

The entrypoint of this file is the compute_match_usefulness function, which computes reachability for each subpattern and exhaustiveness for the whole match.

In this page we explain the necessary concepts to understand how the algorithm works.

Usefulness

The central concept of this file is the notion of “usefulness”. Given some patterns p_1 .. p_n, a pattern q is said to be useful if there is a value that is matched by q and by none of the p_i. We write usefulness(p_1 .. p_n, q) for a function that returns a list of such values. The aim of this file is to compute it efficiently.

This is enough to compute reachability: a pattern in a match expression is reachable iff it is useful w.r.t. the patterns above it:

ⓘ
match Some(0u32) {
    Some(0..100) => {},
    Some(90..190) => {}, // reachable: `Some(150)` is matched by this but not the branch above
    Some(50..150) => {}, // unreachable: all the values this matches are already matched by
                         //   the branches above
    None => {},          // reachable: `None` is matched by this but not the branches above
}

This is also enough to compute exhaustiveness: a match is exhaustive iff the wildcard _ pattern is not useful w.r.t. the patterns in the match. The values returned by usefulness are used to tell the user which values are missing.

ⓘ
match x {
    None => {},
    Some(0) => {},
    // not exhaustive: `_` is useful because it matches `Some(1)`
}

Constructors and fields

In the value Pair(Some(0), true), Pair is called the constructor of the value, and Some(0) and true are its fields. Every matcheable value can be decomposed in this way. Examples of constructors are: Some, None, (,) (the 2-tuple constructor), Foo {..} (the constructor for a struct Foo), and 2 (the constructor for the number 2).

Each constructor takes a fixed number of fields; this is called its arity. Pair and (,) have arity 2, Some has arity 1, None and 42 have arity 0. Each type has a known set of constructors. Some types have many constructors (like u64) or even an infinitely many (like &str and &[T]).

Patterns are similar: Pair(Some(_), _) has constructor Pair and two fields. The difference is that we get some extra pattern-only constructors, namely: the wildcard _, variable bindings, integer ranges like 0..=10, and variable-length slices like [_, .., _]. We treat or-patterns separately, see the dedicated section below.

Now to check if a value v matches a pattern p, we check if v’s constructor matches p’s constructor, then recursively compare their fields if necessary. A few representative examples:

  • matches!(v, _) := true
  • matches!((v0, v1), (p0, p1)) := matches!(v0, p0) && matches!(v1, p1)
  • matches!(Foo { bar: v0, baz: v1 }, Foo { bar: p0, baz: p1 }) := matches!(v0, p0) && matches!(v1, p1)
  • matches!(Ok(v0), Ok(p0)) := matches!(v0, p0)
  • matches!(Ok(v0), Err(p0)) := false (incompatible variants)
  • matches!(v, 1..=100) := matches!(v, 1) || ... || matches!(v, 100)
  • matches!([v0], [p0, .., p1]) := false (incompatible lengths)
  • matches!([v0, v1, v2], [p0, .., p1]) := matches!(v0, p0) && matches!(v2, p1)

Constructors, fields and relevant operations are defined in the super::deconstruct_pat module. The question of whether a constructor is matched by another one is answered by Constructor::is_covered_by.

Note 1: variable bindings (like the x in Some(x)) match anything, so we treat them as wildcards. Note 2: this only applies to matcheable values. For example a value of type Rc<u64> can’t be deconstructed that way.

Specialization

The examples in the previous section motivate the operation at the heart of the algorithm: “specialization”. It captures this idea of “removing one layer of constructor”.

specialize(c, p) takes a value-only constructor c and a pattern p, and returns a pattern-tuple or nothing. It works as follows:

  • Specializing for the wrong constructor returns nothing

    • specialize(None, Some(p0)) := <nothing>
    • specialize([,,,], [p0]) := <nothing>

  • Specializing for the correct constructor returns a tuple of the fields

    • specialize(Variant1, Variant1(p0, p1, p2)) := (p0, p1, p2)
    • specialize(Foo{ bar, baz, quz }, Foo { bar: p0, baz: p1, .. }) := (p0, p1, _)
    • specialize([,,,], [p0, .., p1]) := (p0, _, _, p1)

We get the following property: for any values v_1, .., v_n of appropriate types, we have:

matches!(c(v_1, .., v_n), p)
<=> specialize(c, p) returns something
    && matches!((v_1, .., v_n), specialize(c, p))

We also extend specialization to pattern-tuples by applying it to the first pattern: specialize(c, (p_0, .., p_n)) := specialize(c, p_0) ++ (p_1, .., p_m) where ++ is concatenation of tuples.

The previous property extends to pattern-tuples:

matches!((c(v_1, .., v_n), w_1, .., w_m), (p_0, p_1, .., p_m))
<=> specialize(c, p_0) does not error
    && matches!((v_1, .., v_n, w_1, .., w_m), specialize(c, (p_0, p_1, .., p_m)))

Whether specialization returns something or not is given by Constructor::is_covered_by. Specialization of a pattern is computed in DeconstructedPat::specialize. Specialization for a pattern-tuple is computed in PatStack::pop_head_constructor. Finally, specialization for a set of pattern-tuples is computed in Matrix::specialize_constructor.

Undoing specialization

To construct witnesses we will need an inverse of specialization. If c is a constructor of arity n, we define unspecialize as: unspecialize(c, (p_1, .., p_n, q_1, .., q_m)) := (c(p_1, .., p_n), q_1, .., q_m).

This is done for a single witness-tuple in WitnessStack::apply_constructor, and for a set of witness-tuples in WitnessMatrix::apply_constructor.

Computing usefulness

We now present a naive version of the algorithm for computing usefulness. From now on we operate on pattern-tuples.

Let pt_1, .., pt_n and qt be length-m tuples of patterns for the same type (T_1, .., T_m). We compute usefulness(tp_1, .., tp_n, tq) as follows:

  • Base case: m == 0. The pattern-tuples are all empty, i.e. they’re all (). Thus tq is useful iff there are no rows above it, i.e. if n == 0. In that case we return () as a witness-tuple of usefulness of tq.

  • Inductive case: m > 0. In this naive version, we list all the possible constructors for values of type T1 (we will be more clever in the next section).

    • For each such constructor c for which specialize(c, tq) is not nothing:

      • We recursively compute usefulness(specialize(c, tp_1) ... specialize(c, tp_n), specialize(c, tq)), where we discard any specialize(c, p_i) that returns nothing.
      • For each witness-tuple w found, we apply unspecialize(c, w) to it.

    • We return the all the witnesses found, if any.

Let’s take the following example:

ⓘ
match x {
    Variant1(_) => {} // `p1`
    Variant2(None, 0) => {} // `p2`
    Variant2(Some(_), 0) => {} // `q`
}

To compute the usefulness of q, we would proceed as follows:

Start:
  `tp1 = [Variant1(_)]`
  `tp2 = [Variant2(None, 0)]`
  `tq  = [Variant2(Some(true), 0)]`

  Constructors are `Variant1` and `Variant2`. Only `Variant2` can specialize `tq`.
  Specialize with `Variant2`:
    `tp2 = [None, 0]`
    `tq  = [Some(true), 0]`

    Constructors are `None` and `Some`. Only `Some` can specialize `tq`.
    Specialize with `Some`:
      `tq  = [true, 0]`

      Constructors are `false` and `true`. Only `true` can specialize `tq`.
      Specialize with `true`:
        `tq  = [0]`

        Constructors are `0`, `1`, .. up to infinity. Only `0` can specialize `tq`.
        Specialize with `0`:
          `tq  = []`

          m == 0 and n == 0, so `tq` is useful with witness `[]`.
            `witness  = []`

        Unspecialize with `0`:
          `witness  = [0]`
      Unspecialize with `true`:
        `witness  = [true, 0]`
    Unspecialize with `Some`:
      `witness  = [Some(true), 0]`
  Unspecialize with `Variant2`:
    `witness  = [Variant2(Some(true), 0)]`

Therefore usefulness(tp_1, tp_2, tq) returns the single witness-tuple [Variant2(Some(true), 0)].

Computing the set of constructors for a type is done in ConstructorSet::for_ty. See the following sections for more accurate versions of the algorithm and corresponding links.

Computing reachability and exhaustiveness in one go

The algorithm we have described so far computes usefulness of each pattern in turn to check if it is reachable, and ends by checking if _ is useful to determine exhaustiveness of the whole match. In practice, instead of doing “for each pattern { for each constructor { … } }”, we do “for each constructor { for each pattern { … } }”. This allows us to compute everything in one go.

Matrix stores the set of pattern-tuples under consideration. We track reachability of each row mutably in the matrix as we go along. We ignore witnesses of usefulness of the match rows. We gather witnesses of the usefulness of _ in WitnessMatrix. The algorithm that computes all this is in compute_exhaustiveness_and_reachability.

See the full example at the bottom of this documentation.

Making usefulness tractable: constructor splitting

We’re missing one last detail: which constructors do we list? Naively listing all value constructors cannot work for types like u64 or &str, so we need to be more clever. The final clever idea for this algorithm is that we can group together constructors that behave the same.

Examples:

ⓘ
match (0, false) {
    (0 ..=100, true) => {}
    (50..=150, false) => {}
    (0 ..=200, _) => {}
}

In this example, trying any of 0, 1, .., 49 will give the same specialized matrix, and thus the same reachability/exhaustiveness results. We can thus accelerate the algorithm by trying them all at once. Here in fact, the only cases we need to consider are: 0..50, 50..=100, 101..=150,151..=200 and 201...

enum Direction { North, South, East, West }
match wind {
    (Direction::North, 50..) => {}
    (_, _) => {}
}

In this example, trying any of South, East, West will give the same specialized matrix. By the same reasoning, we only need to try two cases: North, and “everything else”.

We call constructor splitting the operation that computes such a minimal set of cases to try. This is done in ConstructorSet::split and explained in super::deconstruct_pat.

Or-patterns

What we have described so far works well if there are no or-patterns. To handle them, if the first pattern of a row in the matrix is an or-pattern, we expand it by duplicating the rest of the row as necessary. This is handled automatically in Matrix.

This makes reachability tracking subtle, because we also want to compute whether an alternative of an or-pattern is unreachable, e.g. in Some(_) | Some(0). We track reachability of each subpattern by interior mutability in DeconstructedPat with set_reachable/is_reachable.

It’s unfortunate that we have to use interior mutability, but believe me (Nadrieril), I have tried other solutions and nothing is remotely as simple.

Constants and opaques

There are two kinds of constants in patterns:

  • literals (1, true, "foo")
  • named or inline consts (FOO, const { 5 + 6 })

The latter are converted into the corresponding patterns by a previous phase. For example const_to_pat(const { [1, 2, 3] }) becomes an Array(vec![Const(1), Const(2), Const(3)]) pattern. This gets problematic when comparing the constant via == would behave differently from matching on the constant converted to a pattern. The situation around this is currently unclear and the lang team is working on clarifying what we want to do there. In any case, there are constants we will not turn into patterns. We capture these with Constructor::Opaque. These Opaque patterns do not participate in exhaustiveness, specialization or overlap checking.

Full example

We illustrate a full run of the algorithm on the following match.

ⓘ
match x {
    Pair(Some(0), _) => 1,
    Pair(_, false) => 2,
    Pair(Some(0), false) => 3,
}

We keep track of the original row for illustration purposes, this is not what the algorithm actually does (it tracks reachability as a boolean on each row).

 ┐ Patterns:
 │   1. `[Pair(Some(0), _)]`
 │   2. `[Pair(_, false)]`
 │   3. `[Pair(Some(0), false)]`
 │
 │ Specialize with `Pair`:
 ├─┐ Patterns:
 │ │   1. `[Some(0), _]`
 │ │   2. `[_, false]`
 │ │   3. `[Some(0), false]`
 │ │
 │ │ Specialize with `Some`:
 │ ├─┐ Patterns:
 │ │ │   1. `[0, _]`
 │ │ │   2. `[_, false]`
 │ │ │   3. `[0, false]`
 │ │ │
 │ │ │ Specialize with `0`:
 │ │ ├─┐ Patterns:
 │ │ │ │   1. `[_]`
 │ │ │ │   3. `[false]`
 │ │ │ │
 │ │ │ │ Specialize with `true`:
 │ │ │ ├─┐ Patterns:
 │ │ │ │ │   1. `[]`
 │ │ │ │ │
 │ │ │ │ │ We note arm 1 is reachable (by `Pair(Some(0), true)`).
 │ │ │ ├─┘
 │ │ │ │
 │ │ │ │ Specialize with `false`:
 │ │ │ ├─┐ Patterns:
 │ │ │ │ │   1. `[]`
 │ │ │ │ │   3. `[]`
 │ │ │ │ │
 │ │ │ │ │ We note arm 1 is reachable (by `Pair(Some(0), false)`).
 │ │ │ ├─┘
 │ │ ├─┘
 │ │ │
 │ │ │ Specialize with `1..`:
 │ │ ├─┐ Patterns:
 │ │ │ │   2. `[false]`
 │ │ │ │
 │ │ │ │ Specialize with `true`:
 │ │ │ ├─┐ Patterns:
 │ │ │ │ │   // no rows left
 │ │ │ │ │
 │ │ │ │ │ We have found an unmatched value (`Pair(Some(1..), true)`)! This gives us a witness.
 │ │ │ │ │ New witnesses:
 │ │ │ │ │   `[]`
 │ │ │ ├─┘
 │ │ │ │ Unspecialize new witnesses with `true`:
 │ │ │ │   `[true]`
 │ │ │ │
 │ │ │ │ Specialize with `false`:
 │ │ │ ├─┐ Patterns:
 │ │ │ │ │   2. `[]`
 │ │ │ │ │
 │ │ │ │ │ We note arm 2 is reachable (by `Pair(Some(1..), false)`).
 │ │ │ ├─┘
 │ │ │ │
 │ │ │ │ Total witnesses for `1..`:
 │ │ │ │   `[true]`
 │ │ ├─┘
 │ │ │ Unspecialize new witnesses with `1..`:
 │ │ │   `[1.., true]`
 │ │ │
 │ │ │ Total witnesses for `Some`:
 │ │ │   `[1.., true]`
 │ ├─┘
 │ │ Unspecialize new witnesses with `Some`:
 │ │   `[Some(1..), true]`
 │ │
 │ │ Specialize with `None`:
 │ ├─┐ Patterns:
 │ │ │   2. `[false]`
 │ │ │
 │ │ │ Specialize with `true`:
 │ │ ├─┐ Patterns:
 │ │ │ │   // no rows left
 │ │ │ │
 │ │ │ │ We have found an unmatched value (`Pair(None, true)`)! This gives us a witness.
 │ │ │ │ New witnesses:
 │ │ │ │   `[]`
 │ │ ├─┘
 │ │ │ Unspecialize new witnesses with `true`:
 │ │ │   `[true]`
 │ │ │
 │ │ │ Specialize with `false`:
 │ │ ├─┐ Patterns:
 │ │ │ │   2. `[]`
 │ │ │ │
 │ │ │ │ We note arm 2 is reachable (by `Pair(None, false)`).
 │ │ ├─┘
 │ │ │
 │ │ │ Total witnesses for `None`:
 │ │ │   `[true]`
 │ ├─┘
 │ │ Unspecialize new witnesses with `None`:
 │ │   `[None, true]`
 │ │
 │ │ Total witnesses for `Pair`:
 │ │   `[Some(1..), true]`
 │ │   `[None, true]`
 ├─┘
 │ Unspecialize new witnesses with `Pair`:
 │   `[Pair(Some(1..), true)]`
 │   `[Pair(None, true)]`
 │
 │ Final witnesses:
 │   `[Pair(Some(1..), true)]`
 │   `[Pair(None, true)]`
 ┘

We conclude:

  • Arm 3 is unreachable (it was never marked as reachable);
  • The match is not exhaustive;
  • Adding arms with Pair(Some(1..), true) and Pair(None, true) would make the match exhaustive.

Note that when we’re deep in the algorithm, we don’t know what specialization steps got us here. We can only figure out what our witnesses correspond to by unspecializing back up the stack.

Tests

Note: tests specific to this file can be found in:

  • ui/pattern/usefulness
  • ui/or-patterns
  • ui/consts/const_in_pattern
  • ui/rfc-2008-non-exhaustive
  • ui/half-open-range-patterns
  • probably many others

I (Nadrieril) prefer to put new tests in ui/pattern/usefulness unless there’s a specific reason not to, for example if they crucially depend on a particular feature like or_patterns.

Structs

  • MatchArm 🔒
    The arm of a match expression.
  • MatchCheckCtxt 🔒
  • Matrix 🔒
    A 2D matrix. Represents a list of pattern-tuples under investigation.
  • MatrixRow 🔒
    A row of the matrix.
  • PatCtxt 🔒
  • PatStack 🔒
    Represents a pattern-tuple under investigation.
  • PatternColumn 🔒
    A column of patterns in the matrix, where a column is the intuitive notion of “subpatterns that inspect the same subvalue/place”. This is used to traverse patterns column-by-column for lints. Despite similarities with compute_exhaustiveness_and_reachability, this does a different traversal. Notably this is linear in the depth of patterns, whereas compute_exhaustiveness_and_reachability is worst-case exponential (exhaustiveness is NP-complete). The core difference is that we treat sub-columns separately.
  • UsefulnessReport 🔒
    The output of checking a match for exhaustiveness and arm reachability.
  • WitnessMatrix
    Represents a set of pattern-tuples that are witnesses of non-exhaustiveness for error reporting. This has similar invariants as Matrix does.
  • WitnessStack 🔒
    A witness-tuple of non-exhaustiveness for error reporting, represented as a list of patterns (in reverse order of construction).

Enums

  • Reachability 🔒
    Indicates whether or not a given arm is reachable.

Functions