Skip to content

Commit

Permalink
Inline max_slice_length
Browse files Browse the repository at this point in the history 
Note that where we previously ran `max_slice_len` with input having not
only matrix.heads() but also v.head(). Now we run it on matrix.heads()
only, but also take into account the currently processed constructor.
This preserves behavior since `pat_constructors` returns only one
constructor in the case that is of interest for us.
  • Loading branch information
@Nadrieril
Nadrieril committed Nov 5, 2019
1 parent 149792b commit d582ed5
Showing 1 changed file with 99 additions and 106 deletions.
205 changes: 99 additions & 106 deletions src/librustc_mir/hair/pattern/_match.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -985,7 +985,6 @@ pub enum WitnessPreference {
#[derive(Copy, Clone, Debug)]
struct PatCtxt<'tcx> {
ty: Ty<'tcx>,
max_slice_length: u64,
span: Span,
}

Expand Down Expand Up @@ -1143,108 +1142,6 @@ fn all_constructors<'a, 'tcx>(
ctors
}

fn max_slice_length<'p, 'a, 'tcx, I>(cx: &mut MatchCheckCtxt<'a, 'tcx>, patterns: I) -> u64
where
I: Iterator<Item = &'p Pat<'tcx>>,
'tcx: 'p,
{
// The exhaustiveness-checking paper does not include any details on
// checking variable-length slice patterns. However, they are matched
// by an infinite collection of fixed-length array patterns.
//
// Checking the infinite set directly would take an infinite amount
// of time. However, it turns out that for each finite set of
// patterns `P`, all sufficiently large array lengths are equivalent:
//
// Each slice `s` with a "sufficiently-large" length `l ≥ L` that applies
// to exactly the subset `Pₜ` of `P` can be transformed to a slice
// `sₘ` for each sufficiently-large length `m` that applies to exactly
// the same subset of `P`.
//
// Because of that, each witness for reachability-checking from one
// of the sufficiently-large lengths can be transformed to an
// equally-valid witness from any other length, so we only have
// to check slice lengths from the "minimal sufficiently-large length"
// and below.
//
// Note that the fact that there is a *single* `sₘ` for each `m`
// not depending on the specific pattern in `P` is important: if
// you look at the pair of patterns
// `[true, ..]`
// `[.., false]`
// Then any slice of length ≥1 that matches one of these two
// patterns can be trivially turned to a slice of any
// other length ≥1 that matches them and vice-versa - for
// but the slice from length 2 `[false, true]` that matches neither
// of these patterns can't be turned to a slice from length 1 that
// matches neither of these patterns, so we have to consider
// slices from length 2 there.
//
// Now, to see that that length exists and find it, observe that slice
// patterns are either "fixed-length" patterns (`[_, _, _]`) or
// "variable-length" patterns (`[_, .., _]`).
//
// For fixed-length patterns, all slices with lengths *longer* than
// the pattern's length have the same outcome (of not matching), so
// as long as `L` is greater than the pattern's length we can pick
// any `sₘ` from that length and get the same result.
//
// For variable-length patterns, the situation is more complicated,
// because as seen above the precise value of `sₘ` matters.
//
// However, for each variable-length pattern `p` with a prefix of length
// `plₚ` and suffix of length `slₚ`, only the first `plₚ` and the last
// `slₚ` elements are examined.
//
// Therefore, as long as `L` is positive (to avoid concerns about empty
// types), all elements after the maximum prefix length and before
// the maximum suffix length are not examined by any variable-length
// pattern, and therefore can be added/removed without affecting
// them - creating equivalent patterns from any sufficiently-large
// length.
//
// Of course, if fixed-length patterns exist, we must be sure
// that our length is large enough to miss them all, so
// we can pick `L = max(FIXED_LEN+1 ∪ {max(PREFIX_LEN) + max(SUFFIX_LEN)})`
//
// for example, with the above pair of patterns, all elements
// but the first and last can be added/removed, so any
// witness of length ≥2 (say, `[false, false, true]`) can be
// turned to a witness from any other length ≥2.

let mut max_prefix_len = 0;
let mut max_suffix_len = 0;
let mut max_fixed_len = 0;

for row in patterns {
match *row.kind {
PatKind::Constant { value } => {
// extract the length of an array/slice from a constant
match (value.val, &value.ty.kind) {
(_, ty::Array(_, n)) => {
max_fixed_len = cmp::max(max_fixed_len, n.eval_usize(cx.tcx, cx.param_env))
}
(ConstValue::Slice { start, end, .. }, ty::Slice(_)) => {
max_fixed_len = cmp::max(max_fixed_len, (end - start) as u64)
}
_ => {}
}
}
PatKind::Slice { ref prefix, slice: None, ref suffix } => {
let fixed_len = prefix.len() as u64 + suffix.len() as u64;
max_fixed_len = cmp::max(max_fixed_len, fixed_len);
}
PatKind::Slice { ref prefix, slice: Some(_), ref suffix } => {
max_prefix_len = cmp::max(max_prefix_len, prefix.len() as u64);
max_suffix_len = cmp::max(max_suffix_len, suffix.len() as u64);
}
_ => {}
}
}

cmp::max(max_fixed_len + 1, max_prefix_len + max_suffix_len)
}

/// An inclusive interval, used for precise integer exhaustiveness checking.
/// `IntRange`s always store a contiguous range. This means that values are
/// encoded such that `0` encodes the minimum value for the integer,
Expand Down Expand Up @@ -1609,7 +1506,6 @@ pub fn is_useful<'p, 'a, 'tcx>(
// introducing uninhabited patterns for inaccessible fields. We
// need to figure out how to model that.
ty,
max_slice_length: max_slice_length(cx, matrix.heads().chain(Some(v.head()))),
span,
};

Expand Down Expand Up @@ -2088,8 +1984,105 @@ fn split_grouped_constructors<'p, 'tcx>(
split_ctors.push(IntRange::range_to_ctor(tcx, ty, range, span));
}
}
VarLenSlice(prefix, suffix) => {
split_ctors.extend((prefix + suffix..pcx.max_slice_length + 1).map(FixedLenSlice))
VarLenSlice(self_prefix, self_suffix) => {
// The exhaustiveness-checking paper does not include any details on
// checking variable-length slice patterns. However, they are matched
// by an infinite collection of fixed-length array patterns.
//
// Checking the infinite set directly would take an infinite amount
// of time. However, it turns out that for each finite set of
// patterns `P`, all sufficiently large array lengths are equivalent:
//
// Each slice `s` with a "sufficiently-large" length `l ≥ L` that applies
// to exactly the subset `Pₜ` of `P` can be transformed to a slice
// `sₘ` for each sufficiently-large length `m` that applies to exactly
// the same subset of `P`.
//
// Because of that, each witness for reachability-checking from one
// of the sufficiently-large lengths can be transformed to an
// equally-valid witness from any other length, so we only have
// to check slice lengths from the "minimal sufficiently-large length"
// and below.
//
// Note that the fact that there is a *single* `sₘ` for each `m`
// not depending on the specific pattern in `P` is important: if
// you look at the pair of patterns
// `[true, ..]`
// `[.., false]`
// Then any slice of length ≥1 that matches one of these two
// patterns can be trivially turned to a slice of any
// other length ≥1 that matches them and vice-versa - for
// but the slice from length 2 `[false, true]` that matches neither
// of these patterns can't be turned to a slice from length 1 that
// matches neither of these patterns, so we have to consider
// slices from length 2 there.
//
// Now, to see that that length exists and find it, observe that slice
// patterns are either "fixed-length" patterns (`[_, _, _]`) or
// "variable-length" patterns (`[_, .., _]`).
//
// For fixed-length patterns, all slices with lengths *longer* than
// the pattern's length have the same outcome (of not matching), so
// as long as `L` is greater than the pattern's length we can pick
// any `sₘ` from that length and get the same result.
//
// For variable-length patterns, the situation is more complicated,
// because as seen above the precise value of `sₘ` matters.
//
// However, for each variable-length pattern `p` with a prefix of length
// `plₚ` and suffix of length `slₚ`, only the first `plₚ` and the last
// `slₚ` elements are examined.
//
// Therefore, as long as `L` is positive (to avoid concerns about empty
// types), all elements after the maximum prefix length and before
// the maximum suffix length are not examined by any variable-length
// pattern, and therefore can be added/removed without affecting
// them - creating equivalent patterns from any sufficiently-large
// length.
//
// Of course, if fixed-length patterns exist, we must be sure
// that our length is large enough to miss them all, so
// we can pick `L = max(FIXED_LEN+1 ∪ {max(PREFIX_LEN) + max(SUFFIX_LEN)})`
//
// for example, with the above pair of patterns, all elements
// but the first and last can be added/removed, so any
// witness of length ≥2 (say, `[false, false, true]`) can be
// turned to a witness from any other length ≥2.

let mut max_prefix_len = self_prefix;
let mut max_suffix_len = self_suffix;
let mut max_fixed_len = 0;

for row in matrix.heads() {
match *row.kind {
PatKind::Constant { value } => {
// extract the length of an array/slice from a constant
match (value.val, &value.ty.kind) {
(_, ty::Array(_, n)) => {
max_fixed_len =
cmp::max(max_fixed_len, n.eval_usize(tcx, param_env))
}
(ConstValue::Slice { start, end, .. }, ty::Slice(_)) => {
max_fixed_len = cmp::max(max_fixed_len, (end - start) as u64)
}
_ => {}
}
}
PatKind::Slice { ref prefix, slice: None, ref suffix } => {
let fixed_len = prefix.len() as u64 + suffix.len() as u64;
max_fixed_len = cmp::max(max_fixed_len, fixed_len);
}
PatKind::Slice { ref prefix, slice: Some(_), ref suffix } => {
max_prefix_len = cmp::max(max_prefix_len, prefix.len() as u64);
max_suffix_len = cmp::max(max_suffix_len, suffix.len() as u64);
}
_ => {}
}
}

let max_slice_length = cmp::max(max_fixed_len + 1, max_prefix_len + max_suffix_len);
split_ctors
.extend((self_prefix + self_suffix..=max_slice_length).map(FixedLenSlice))
}
// Any other constructor can be used unchanged.
_ => split_ctors.push(ctor),
Expand Down

0 comments on commit d582ed5

Please sign in to comment.