[−][src]Module rustc_mir_build::thir::pattern::_match
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
- 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 depend on a particular feature like or_patterns.
This file includes the logic for exhaustiveness and usefulness checking for pattern-matching. Specifically, given a list of patterns for a type, we can tell whether: (a) the patterns cover every possible constructor for the type (exhaustiveness) (b) each pattern is necessary (usefulness)
The algorithm implemented here is a modified version of the one described in: http://moscova.inria.fr/~maranget/papers/warn/index.html However, to save future implementors from reading the original paper, we summarise the algorithm here to hopefully save time and be a little clearer (without being so rigorous).
Premise
The core of the algorithm revolves about a "usefulness" check. In particular, we
are trying to compute a predicate U(P, p) where P is a list of patterns (we refer to this as
a matrix). U(P, p) represents whether, given an existing list of patterns
P_1 ..= P_m, adding a new pattern p will be "useful" (that is, cover previously-
uncovered values of the type).
If we have this predicate, then we can easily compute both exhaustiveness of an
entire set of patterns and the individual usefulness of each one.
(a) the set of patterns is exhaustive iff U(P, _) is false (i.e., adding a wildcard
match doesn't increase the number of values we're matching)
(b) a pattern P_i is not useful if U(P[0..=(i-1), P_i) is false (i.e., adding a
pattern to those that have come before it doesn't increase the number of values
we're matching).
Core concept
The idea that powers everything that is done in this file is the following: a value is made
from a constructor applied to some fields. 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). Fields are just a (possibly empty) list of values.
Some of the constructors listed above might feel weird: None and 2 don't take any
arguments. This is part of what makes constructors so general: we will consider plain values
like numbers and string literals to be constructors that take no arguments, also called "0-ary
constructors"; they are the simplest case of constructors. This allows us to see any value as
made up from a tree of constructors, each having a given number of children. For example:
(None, Ok(0)) is made from 4 different constructors.
This idea can be extended to patterns: a pattern captures a set of possible values, and we can
describe this set using constructors. For example, Err(_) captures all values of the type
Result<T, E> that start with the Err constructor (for some choice of T and E). The
wildcard _ captures all values of the given type starting with any of the constructors for
that type.
We use this to compute whether different patterns might capture a same value. Do the patterns
Ok("foo") and Err(_) capture a common value? The answer is no, because the first pattern
captures only values starting with the Ok constructor and the second only values starting
with the Err constructor. Do the patterns Some(42) and Some(1..10) intersect? They might,
since they both capture values starting with Some. To be certain, we need to dig under the
Some constructor and continue asking the question. This is the main idea behind the
exhaustiveness algorithm: by looking at patterns constructor-by-constructor, we can efficiently
figure out if some new pattern might capture a value that hadn't been captured by previous
patterns.
Constructors are represented by the Constructor enum, and its fields by the Fields enum.
Most of the complexity of this file resides in transforming between patterns and
(Constructor, Fields) pairs, handling all the special cases correctly.
Caveat: this constructors/fields distinction doesn't quite cover every Rust value. For example
a value of type Rc<u64> doesn't fit this idea very well, nor do various other things.
However, this idea covers most of the cases that are relevant to exhaustiveness checking.
Algorithm
Recall that U(P, p) represents whether, given an existing list of patterns (aka matrix) P,
adding a new pattern p will cover previously-uncovered values of the type.
During the course of the algorithm, the rows of the matrix won't just be individual patterns,
but rather partially-deconstructed patterns in the form of a list of fields. The paper
calls those pattern-vectors, and we will call them pattern-stacks. The same holds for the
new pattern p.
For example, say we have the following:
// x: (Option<bool>, Result<()>) match x { (Some(true), _) => {} (None, Err(())) => {} (None, Err(_)) => {} }
Here, the matrix P starts as:
[
[(Some(true), _)],
[(None, Err(()))],
[(None, Err(_))],
]We can tell it's not exhaustive, because U(P, _) is true (we're not covering
[(Some(false), _)], for instance). In addition, row 3 is not useful, because
all the values it covers are already covered by row 2.
A list of patterns can be thought of as a stack, because we are mainly interested in the top of the stack at any given point, and we can pop or apply constructors to get new pattern-stacks. To match the paper, the top of the stack is at the beginning / on the left.
There are two important operations on pattern-stacks necessary to understand the algorithm:
-
We can pop a given constructor off the top of a stack. This operation is called
specialize, and is denotedS(c, p)wherecis a constructor (likeSomeorNone) andpa pattern-stack. If the pattern on top of the stack can coverc, this removes the constructor and pushes its arguments onto the stack. It also expands OR-patterns into distinct patterns. Otherwise the pattern-stack is discarded. This essentially filters those pattern-stacks whose top covers the constructorcand discards the others.For example, the first pattern above initially gives a stack
[(Some(true), _)]. If we pop the tuple constructor, we are left with[Some(true), _], and if we then pop theSomeconstructor we get[true, _]. If we had poppedNoneinstead, we would get nothing back.This returns zero or more new pattern-stacks, as follows. We look at the pattern
p_1on top of the stack, and we have four cases: 1.1.p_1 = c(r_1, .., r_a), i.e. the top of the stack has constructorc. We push onto the stack the arguments of this constructor, and return the result: r_1, .., r_a, p_2, .., p_n 1.2.p_1 = c'(r_1, .., r_a')wherec ≠ c'. We discard the current stack and return nothing. 1.3.p_1 = _. We push onto the stack as many wildcards as the constructorchas arguments (its arity), and return the resulting stack: _, .., _, p_2, .., p_n 1.4.p_1 = r_1 | r_2. We expand the OR-pattern and then recurse on each resulting stack: S(c, (r_1, p_2, .., p_n)) S(c, (r_2, p_2, .., p_n)) -
We can pop a wildcard off the top of the stack. This is called
S(_, p), wherepis a pattern-stack. Note: the paper calls thisD(p). This is used when we know there are missing constructor cases, but there might be existing wildcard patterns, so to check the usefulness of the matrix, we have to check all its other components.It is computed as follows. We look at the pattern
p_1on top of the stack, and we have three cases: 2.1.p_1 = c(r_1, .., r_a). We discard the current stack and return nothing. 2.2.p_1 = _. We return the rest of the stack: p_2, .., p_n 2.3.p_1 = r_1 | r_2. We expand the OR-pattern and then recurse on each resulting stack. S(, (r_1, p_2, .., p_n)) S(, (r_2, p_2, .., p_n))
Note that the OR-patterns are not always used directly in Rust, but are used to derive the exhaustive integer matching rules, so they're written here for posterity.
Both those operations extend straightforwardly to a list or pattern-stacks, i.e. a matrix, by working row-by-row. Popping a constructor ends up keeping only the matrix rows that start with the given constructor, and popping a wildcard keeps those rows that start with a wildcard.
The algorithm for computing U
The algorithm is inductive (on the number of columns: i.e., components of tuple patterns).
That means we're going to check the components from left-to-right, so the algorithm
operates principally on the first component of the matrix and new pattern-stack p.
This algorithm is realised in the is_useful function.
Base case. (n = 0, i.e., an empty tuple pattern)
- If P already contains an empty pattern (i.e., if the number of patterns m > 0),
then U(P, p) is false.
- Otherwise, P must be empty, so U(P, p) is true.
Inductive step. (n > 0, i.e., whether there's at least one column
[which may then be expanded into further columns later])
We're going to match on the top of the new pattern-stack, p_1.
- If p_1 == c(r_1, .., r_a), i.e. we have a constructor pattern.
Then, the usefulness of p_1 can be reduced to whether it is useful when
we ignore all the patterns in the first column of P that involve other constructors.
This is where S(c, P) comes in:
U(P, p) := U(S(c, P), S(c, p))
For example, if P is:
[
[Some(true), _],
[None, 0],
]and p is [Some(false), 0], then we don't care about row 2 since we know p only
matches values that row 2 doesn't. For row 1 however, we need to dig into the
arguments of Some to know whether some new value is covered. So we compute
U([[true, _]], [false, 0]).
- If
p_1 == _, then we look at the list of constructors that appear in the first component of the rows ofP:
- If there are some constructors that aren't present, then we might think that the
wildcard
_is useful, since it covers those constructors that weren't covered before. That's almost correct, but only works if there were no wildcards in those first components. So we need to check thatpis useful with respect to the rows that start with a wildcard, if there are any. This is whereS(_, x)comes in:U(P, p) := U(S(_, P), S(_, p))
For example, if P is:
[
[_, true, _],
[None, false, 1],
]and p is [_, false, _], the Some constructor doesn't appear in P. So if we
only had row 2, we'd know that p is useful. However row 1 starts with a
wildcard, so we need to check whether U([[true, _]], [false, 1]).
- Otherwise, all possible constructors (for the relevant type) are present. In this
case we must check whether the wildcard pattern covers any unmatched value. For
that, we can think of the
_pattern as a big OR-pattern that covers all possible constructors. ForOption, that would mean_ = None | Some(_)for example. The wildcard pattern is useful in this case if it is useful when specialized to one of the possible constructors. So we compute:U(P, p) := ∃(k ϵ constructors) U(S(k, P), S(k, p))
For example, if P is:
[
[Some(true), _],
[None, false],
]and p is [_, false], both None and Some constructors appear in the first
components of P. We will therefore try popping both constructors in turn: we
compute U([[true, _]], [_, false]) for the Some constructor, and U([[false]], [false]) for the None constructor. The first case returns true, so we know that
p is useful for P. Indeed, it matches [Some(false), _] that wasn't matched
before.
- If
p_1 == r_1 | r_2, then the usefulness depends on eachr_iseparately:U(P, p) := U(P, (r_1, p_2, .., p_n)) || U(P, (r_2, p_2, .., p_n))
Modifications to the algorithm
The algorithm in the paper doesn't cover some of the special cases that arise in Rust, for example uninhabited types and variable-length slice patterns. These are drawn attention to throughout the code below. I'll make a quick note here about how exhaustive integer matching is accounted for, though.
Exhaustive integer matching
An integer type can be thought of as a (huge) sum type: 1 | 2 | 3 | ... So to support exhaustive integer matching, we can make use of the logic in the paper for OR-patterns. However, we obviously can't just treat ranges x..=y as individual sums, because they are likely gigantic. So we instead treat ranges as constructors of the integers. This means that we have a constructor of constructors (the integers themselves). We then need to work through all the inductive step rules above, deriving how the ranges would be treated as OR-patterns, and making sure that they're treated in the same way even when they're ranges. There are really only four special cases here:
- When we match on a constructor that's actually a range, we have to treat it as if we would
an OR-pattern.
- It turns out that we can simply extend the case for single-value patterns in
specializeto either be equal to a value constructor, or contained within a range constructor. - When the pattern itself is a range, you just want to tell whether any of the values in the pattern range coincide with values in the constructor range, which is precisely intersection. Since when encountering a range pattern for a value constructor, we also use inclusion, it means that whenever the constructor is a value/range and the pattern is also a value/range, we can simply use intersection to test usefulness.
- It turns out that we can simply extend the case for single-value patterns in
- When we're testing for usefulness of a pattern and the pattern's first component is a
wildcard.
- If all the constructors appear in the matrix, we have a slight complication. By default,
the behaviour (i.e., a disjunction over specialised matrices for each constructor) is
invalid, because we want a disjunction over every integer in each range, not just a
disjunction over every range. This is a bit more tricky to deal with: essentially we need
to form equivalence classes of subranges of the constructor range for which the behaviour
of the matrix
Pand new patternpare the same. This is described in more detail inConstructor::split. - If some constructors are missing from the matrix, it turns out we don't need to do anything special (because we know none of the integers are actually wildcards: i.e., we can't span wildcards using ranges).
- If all the constructors appear in the matrix, we have a slight complication. By default,
the behaviour (i.e., a disjunction over specialised matrices for each constructor) is
invalid, because we want a disjunction over every integer in each range, not just a
disjunction over every range. This is a bit more tricky to deal with: essentially we need
to form equivalence classes of subranges of the constructor range for which the behaviour
of the matrix
Structs
| IntRange | An inclusive interval, used for precise integer exhaustiveness checking.
|
| LiteralExpander | |
| MatchArm | The arm of a match expression. |
| MatchCheckCtxt | |
| Matrix | A 2D matrix. |
| MissingConstructors | |
| PatCtxt | |
| PatStack | A row of a matrix. Rows of len 1 are very common, which is why |
| Slice | A constructor for array and slice patterns. |
| UsefulnessReport | The output of checking a match for exhaustiveness and arm reachability. |
| Witness | A witness of non-exhaustiveness for error reporting, represented as a list of patterns (in reverse order of construction) with wildcards inside to represent elements that can take any inhabitant of the type as a value. |
Enums
| Constructor | A value can be decomposed into a constructor applied to some fields. This struct represents
the constructor. See also |
| Fields | A value can be decomposed into a constructor applied to some fields. This struct represents
those fields, generalized to allow patterns in each field. See also |
| FilteredField | Some fields need to be explicitly hidden away in certain cases; see the comment above the
|
| SliceKind | |
| Usefulness | |
| WitnessPreference |
Functions
| all_constructors | This determines the set of all possible constructors of a pattern matching
values of type |
| compute_match_usefulness | The entrypoint for the usefulness algorithm. Computes whether a match is exhaustive and which of its arms are reachable. |
| expand_pattern | |
| is_useful | Algorithm from http://moscova.inria.fr/~maranget/papers/warn/index.html.
The algorithm from the paper has been modified to correctly handle empty
types. The changes are:
(0) We don't exit early if the pattern matrix has zero rows. We just
continue to recurse over columns.
(1) all_constructors will only return constructors that are statically
possible. E.g., it will only return |
| pat_constructor | Determines the constructor that the given pattern can be specialized to.
Returns |