New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Redo Exhaustiveness Analysis #8908

Merged
merged 3 commits into from Apr 29, 2017

Conversation

Projects
None yet
9 participants
@CodaFi
Collaborator

CodaFi commented Apr 21, 2017

Implement exhaustiveness checking in Sema with rich error messages. The
algorithm used is a variant of the one described in Fengyun Liu's paper
"A Generic Algorithm for Checking Exhaustivity of Pattern Matching"
published in the EPFL conference, and Luc Maranget's seminal paper
"Warnings for Pattern Matching"

The Space Engine views pattern matching as a problem of projecting the
scrutinee of a pattern-match into a "Space", then iteratively
constructing a Space from the cases. Taking the difference of this
master space and the covered spaces yields the "holes" left over or
reveals a completely covered space.

The algorithm also extends trivially to redundancy checks in patterns,
but that check is already implemented in SIL dataflow diagnostics and
it's not clear if this this algorithm improves upon it.

Resolves SR-483, SR-2293, SR-1313, SR-4468, SR-911, SR-4658, SR-3768 and probably a few others.

@CodaFi

This comment has been minimized.

Show comment
Hide comment
@CodaFi

CodaFi Apr 21, 2017

Collaborator

@swift-ci please smoke test

Collaborator

CodaFi commented Apr 21, 2017

@swift-ci please smoke test

@jrose-apple

This comment has been minimized.

Show comment
Hide comment
@jrose-apple
Member

jrose-apple commented Apr 21, 2017

@CodaFi

This comment has been minimized.

Show comment
Hide comment
@CodaFi

CodaFi Apr 21, 2017

Collaborator

@swift-ci please smoke test macOS platform

Collaborator

CodaFi commented Apr 21, 2017

@swift-ci please smoke test macOS platform

@CodaFi

This comment has been minimized.

Show comment
Hide comment
@CodaFi

CodaFi Apr 21, 2017

Collaborator

@swift-ci please smoke test macOS platform

Collaborator

CodaFi commented Apr 21, 2017

@swift-ci please smoke test macOS platform

@CodaFi

This comment has been minimized.

Show comment
Hide comment
@CodaFi

CodaFi Apr 21, 2017

Collaborator

@jrose-apple I'm baffled about the final failing validation test. Inserting defaults causes the driver not to skip building main.

Collaborator

CodaFi commented Apr 21, 2017

@jrose-apple I'm baffled about the final failing validation test. Inserting defaults causes the driver not to skip building main.

@CodaFi

This comment has been minimized.

Show comment
Hide comment
@CodaFi

CodaFi Apr 21, 2017

Collaborator

@swift-ci please smoke test

Collaborator

CodaFi commented Apr 21, 2017

@swift-ci please smoke test

@@ -9,6 +9,7 @@ func checkEquatablePattern(_ c: Color) {
case red: return
case green: return
case blue: return
default: return

This comment has been minimized.

@slavapestov

slavapestov Apr 21, 2017

Member

Is this a source-breaking change?

@slavapestov

slavapestov Apr 21, 2017

Member

Is this a source-breaking change?

This comment has been minimized.

@CodaFi

CodaFi Apr 21, 2017

Collaborator

I think so, but at the same time it's also something that the old check wasn't catching but should have - and there's a trivial migration path here.

@CodaFi

CodaFi Apr 21, 2017

Collaborator

I think so, but at the same time it's also something that the old check wasn't catching but should have - and there's a trivial migration path here.

@slavapestov

This comment has been minimized.

Show comment
Hide comment
@slavapestov

slavapestov Apr 21, 2017

Member

I don't know much about this problem domain, but resolving five JIRA bugs is impressive ;)

Member

slavapestov commented Apr 21, 2017

I don't know much about this problem domain, but resolving five JIRA bugs is impressive ;)

@jckarter

This comment has been minimized.

Show comment
Hide comment
@jckarter

jckarter Apr 21, 2017

Member

Thanks for looking into this! I have concerns about doing the checking in Sema though, since that means we end up with duplicated logic for understanding pattern exclusivity, reachability, and exhaustiveness across Sema, SILGen, and the mandatory passes. I had envisioned tackling this problem by improving unreachable code diagnostics' understanding of switch_enums.

Member

jckarter commented Apr 21, 2017

Thanks for looking into this! I have concerns about doing the checking in Sema though, since that means we end up with duplicated logic for understanding pattern exclusivity, reachability, and exhaustiveness across Sema, SILGen, and the mandatory passes. I had envisioned tackling this problem by improving unreachable code diagnostics' understanding of switch_enums.

@gottesmm

This comment has been minimized.

Show comment
Hide comment
@gottesmm

gottesmm Apr 21, 2017

Member

I agree 100% with @jckarter.

Member

gottesmm commented Apr 21, 2017

I agree 100% with @jckarter.

@jckarter

This comment has been minimized.

Show comment
Hide comment
@jckarter

jckarter Apr 22, 2017

Member

I'm willing to believe sema is a better home for this analysis, but it might do some good to tease out the specialization, destructuring, and other abstractions from SILGenPattern into Sema so they can be shared.

Member

jckarter commented Apr 22, 2017

I'm willing to believe sema is a better home for this analysis, but it might do some good to tease out the specialization, destructuring, and other abstractions from SILGenPattern into Sema so they can be shared.

@CodaFi

This comment has been minimized.

Show comment
Hide comment
@CodaFi

CodaFi Apr 22, 2017

Collaborator

since that means we end up with duplicated logic

I was hoping to be able to remove SIL's ability to reason about pattern completeness entirely after this patch lands. This check in Sema is both more conservative and more complete - the old check would recur into tuple patterns and yield false negatives, or ignore where clauses and report false positives, for example - but leave the dataflow checks in place as a way to diagnose redundancy and as a sanity check to back up the exhaustiveness checker.

Collaborator

CodaFi commented Apr 22, 2017

since that means we end up with duplicated logic

I was hoping to be able to remove SIL's ability to reason about pattern completeness entirely after this patch lands. This check in Sema is both more conservative and more complete - the old check would recur into tuple patterns and yield false negatives, or ignore where clauses and report false positives, for example - but leave the dataflow checks in place as a way to diagnose redundancy and as a sanity check to back up the exhaustiveness checker.

@jckarter

This comment has been minimized.

Show comment
Hide comment
@jckarter

jckarter Apr 22, 2017

Member

Aside from exhaustiveness checking, it seems to me like there's other duplicated logic shared between the exhaustiveness analysis of patterns and code generation. In both cases, you need an understanding of what patterns are mutually exclusive and how to specialize the pattern graph after applying a pattern. I'm wondering whether there are abstractions your space engine can share with the SILGenPattern algorithm, so we don't have to duplicate the work every time we introduce a new kind of pattern.

Member

jckarter commented Apr 22, 2017

Aside from exhaustiveness checking, it seems to me like there's other duplicated logic shared between the exhaustiveness analysis of patterns and code generation. In both cases, you need an understanding of what patterns are mutually exclusive and how to specialize the pattern graph after applying a pattern. I'm wondering whether there are abstractions your space engine can share with the SILGenPattern algorithm, so we don't have to duplicate the work every time we introduce a new kind of pattern.

@CodaFi

This comment has been minimized.

Show comment
Hide comment
@CodaFi

CodaFi Apr 22, 2017

Collaborator

In both of the cited papers the algorithms don't focus on decision-flows, they're just syntactico-semantic checks for exhaustiveness. Given the precondition that a pattern is complete, one can use this approach to detect overlap in patterns more easily - and I did originally plan to do that - but SIL does it far better than this currently. Compiling patterns to decision trees, unfortunately, seems like a different problem. Maranget even acknowledges difficulty with trying that approach.

Collaborator

CodaFi commented Apr 22, 2017

In both of the cited papers the algorithms don't focus on decision-flows, they're just syntactico-semantic checks for exhaustiveness. Given the precondition that a pattern is complete, one can use this approach to detect overlap in patterns more easily - and I did originally plan to do that - but SIL does it far better than this currently. Compiling patterns to decision trees, unfortunately, seems like a different problem. Maranget even acknowledges difficulty with trying that approach.

@CodaFi

This comment has been minimized.

Show comment
Hide comment
@CodaFi

CodaFi Apr 22, 2017

Collaborator

@swift-ci please smoke test macOS platform

Collaborator

CodaFi commented Apr 22, 2017

@swift-ci please smoke test macOS platform

@CodaFi

This comment has been minimized.

Show comment
Hide comment
@CodaFi

CodaFi Apr 23, 2017

Collaborator

@swift-ci please smoke test

Collaborator

CodaFi commented Apr 23, 2017

@swift-ci please smoke test

@swift-ci

This comment has been minimized.

Show comment
Hide comment
@swift-ci

swift-ci Apr 24, 2017

Contributor

Build failed
Jenkins build - Swift Test Linux Platform
Git Commit - c79b4ef
Test requested by - @CodaFi

Contributor

swift-ci commented Apr 24, 2017

Build failed
Jenkins build - Swift Test Linux Platform
Git Commit - c79b4ef
Test requested by - @CodaFi

@swift-ci

This comment has been minimized.

Show comment
Hide comment
@swift-ci

swift-ci Apr 24, 2017

Contributor

Build failed
Jenkins build - Swift Test OS X Platform
Git Commit - c79b4ef
Test requested by - @CodaFi

Contributor

swift-ci commented Apr 24, 2017

Build failed
Jenkins build - Swift Test OS X Platform
Git Commit - c79b4ef
Test requested by - @CodaFi

@CodaFi

This comment has been minimized.

Show comment
Hide comment
@CodaFi

CodaFi Apr 24, 2017

Collaborator

@swift-ci please test

Collaborator

CodaFi commented Apr 24, 2017

@swift-ci please test

@swift-ci

This comment has been minimized.

Show comment
Hide comment
@swift-ci

swift-ci Apr 24, 2017

Contributor

Build failed
Jenkins build - Swift Test OS X Platform
Git Commit - ec71640
Test requested by - @CodaFi

Contributor

swift-ci commented Apr 24, 2017

Build failed
Jenkins build - Swift Test OS X Platform
Git Commit - ec71640
Test requested by - @CodaFi

@CodaFi

This comment has been minimized.

Show comment
Hide comment
@CodaFi

CodaFi Apr 25, 2017

Collaborator

@swift-ci please smoke test

Collaborator

CodaFi commented Apr 25, 2017

@swift-ci please smoke test

@CodaFi

This comment has been minimized.

Show comment
Hide comment
@CodaFi

CodaFi Apr 25, 2017

Collaborator

Alright: @jckarter @gottesmm I don't want to merge this without convincing y'all that this is the approach we should take for this feature.

I've poked around in our implementation of Maranget's algorithm for minimal decision tree generation for the last few days and I can't really see it fitting in with the idea of iterative specialization of matrices. For one, the iterative specialization process doesn't maintain the shape of the case matrix as the user wrote it. Even if the process were perfect, if we attempted to diagnose non-exhaustive specialized rows we may wind up introducing far more patterns than needed. The benefit of this approach is it arrives at a minimal set of uncovered cases fairly efficiently and can emit diagnostics that match the actual structure the user wrote.

We can also use this check to simplify invariants in SILGen around exhaustiveness of select_enum and switch_enum and turn the existing specialization machinery around to catch redundant rows more effectively.

Collaborator

CodaFi commented Apr 25, 2017

Alright: @jckarter @gottesmm I don't want to merge this without convincing y'all that this is the approach we should take for this feature.

I've poked around in our implementation of Maranget's algorithm for minimal decision tree generation for the last few days and I can't really see it fitting in with the idea of iterative specialization of matrices. For one, the iterative specialization process doesn't maintain the shape of the case matrix as the user wrote it. Even if the process were perfect, if we attempted to diagnose non-exhaustive specialized rows we may wind up introducing far more patterns than needed. The benefit of this approach is it arrives at a minimal set of uncovered cases fairly efficiently and can emit diagnostics that match the actual structure the user wrote.

We can also use this check to simplify invariants in SILGen around exhaustiveness of select_enum and switch_enum and turn the existing specialization machinery around to catch redundant rows more effectively.

@slavapestov

This comment has been minimized.

Show comment
Hide comment
@slavapestov

slavapestov Apr 25, 2017

Member

I think having this check in Sema makes sense. I don't really see how exhaustiveness checking benefits from having a CFG around. @gottesmm @jckarter what do you think?

Member

slavapestov commented Apr 25, 2017

I think having this check in Sema makes sense. I don't really see how exhaustiveness checking benefits from having a CFG around. @gottesmm @jckarter what do you think?

@CodaFi

This comment has been minimized.

Show comment
Hide comment
@CodaFi

CodaFi Apr 27, 2017

Collaborator

Let's see what happens here too.

@swift-ci please test source compatibility

Collaborator

CodaFi commented Apr 27, 2017

Let's see what happens here too.

@swift-ci please test source compatibility

@CodaFi

This comment has been minimized.

Show comment
Hide comment
@CodaFi

CodaFi Apr 28, 2017

Collaborator

Apparently GRDB is still acting up @lplarson

Collaborator

CodaFi commented Apr 28, 2017

Apparently GRDB is still acting up @lplarson

@lplarson

This comment has been minimized.

Show comment
Hide comment
@lplarson

lplarson Apr 28, 2017

Member

Hmm, not seeing that in CI.

Member

lplarson commented Apr 28, 2017

Hmm, not seeing that in CI.

@lplarson

This comment has been minimized.

Show comment
Hide comment
@lplarson

lplarson Apr 28, 2017

Member

Let's try this one more time.

@swift-ci please test source compatibility

Member

lplarson commented Apr 28, 2017

Let's try this one more time.

@swift-ci please test source compatibility

@lplarson

This comment has been minimized.

Show comment
Hide comment

CodaFi added some commits Apr 4, 2017

Introduce the Space Engine
Implement exhaustiveness checking in Sema with rich error messages.  The
algorithm used is a variant of the one described in Fengyun Liu's paper
"A Generic Algorithm for Checking Exhaustivity of Pattern Matching"
published in the EPFL conference, and Luc Maranget's seminal paper
"Warnings for Pattern Matching"

The Space Engine views pattern matching as a problem of projecting the
scrutinee of a pattern-match into a "Space", then iteratively
constructing a Space from the cases.  Taking the difference of this
master space and the covered spaces yields the "holes" left over or
reveals a completely covered space.

The algorithm also extends trivially to redundancy checks in patterns,
but that check is already implemented in SILGen and this algorithm does
not improve upon it.
@CodaFi

This comment has been minimized.

Show comment
Hide comment
@CodaFi

CodaFi Apr 28, 2017

Collaborator

Ah, you're right. Didn't get the semantic pattern of a paren pattern (I love this CI feature).

Collaborator

CodaFi commented Apr 28, 2017

Ah, you're right. Didn't get the semantic pattern of a paren pattern (I love this CI feature).

@CodaFi

This comment has been minimized.

Show comment
Hide comment
@CodaFi

CodaFi Apr 28, 2017

Collaborator

@swift-ci please smoke test

Collaborator

CodaFi commented Apr 28, 2017

@swift-ci please smoke test

@CodaFi

This comment has been minimized.

Show comment
Hide comment
@CodaFi

CodaFi Apr 28, 2017

Collaborator

@swift-ci please clean smoke test macOS platform

Collaborator

CodaFi commented Apr 28, 2017

@swift-ci please clean smoke test macOS platform

@CodaFi

This comment has been minimized.

Show comment
Hide comment
@CodaFi

CodaFi Apr 28, 2017

Collaborator

@swift-ci please test source compatibility

Collaborator

CodaFi commented Apr 28, 2017

@swift-ci please test source compatibility

@CodaFi

This comment has been minimized.

Show comment
Hide comment
@CodaFi

CodaFi Apr 29, 2017

Collaborator

After a short conversation with Joe, I feel comfortable with this going in.

⛵️

Collaborator

CodaFi commented Apr 29, 2017

After a short conversation with Joe, I feel comfortable with this going in.

⛵️

@CodaFi CodaFi merged commit 2a7eee8 into apple:master Apr 29, 2017

3 checks passed

Swift Source Compatibility Suite on macOS Platform Build finished.
Details
Swift Test Linux Platform (smoke test)
Details
Swift Test OS X Platform (smoke test)
Details

@CodaFi CodaFi deleted the CodaFi:space-engine branch Apr 29, 2017

@nkcsgexi

This comment has been minimized.

Show comment
Hide comment
@nkcsgexi

nkcsgexi May 1, 2017

Contributor

In future, please add test if the commit is behavior-changing. You have added a new "StringRef" here.

Contributor

nkcsgexi commented on include/swift/AST/DiagnosticsSema.def in 42c5955 May 1, 2017

In future, please add test if the commit is behavior-changing. You have added a new "StringRef" here.

@lattner

This comment has been minimized.

Show comment
Hide comment
@lattner

lattner May 1, 2017

Collaborator

Awesome @CodaFi !

Collaborator

lattner commented May 1, 2017

Awesome @CodaFi !

@jpsim jpsim referenced this pull request May 1, 2017

Closed

[68] Issue #68 - May 4, 2017 #242

palimondo referenced this pull request May 7, 2017

[Foundation] Performance improvements for IndexPath bridging and comp…
…arison (#9339)

* [Foundation] Refactor the backing of IndexPath to favor stack allocations

The previous implementation of IndexPath would cause a malloc of the underlying array buffer upon bridging from ObjectiveC. This impacts graphical APIs (such as UICollectionView or AppKit equivalents) when calling delegation patterns. Since IndexPath itself can be a tagged pointer and most often just a pair of elements it can  be represented as an enum of common cases. Those common cases of empty, single, or pair can be represented respectively as no associated value, a single Int, and a tuple of Ints. These cases will be exclusively stack allocations, which is markably faster than the allocating code-path. IndexPaths that have a count greater than 2 will still fall into the array storage case. As an added performance benefit, accessing count and subscripting is now faster by aproximately 30% due to more tightly coupled inlining potential under whole module optimizations. Accessing count is also faster since it has better cache-line effeciency (lesson learned: the branch predictor is more optimized than pointer indirection chasing).

Benchmarks performed on x86_64, arm and arm64 still pending results but should be applicable across the board.

Resolves the following issues:
https://bugs.swift.org/browse/SR-3655
https://bugs.swift.org/browse/SR-2769

Resolves the following radars:
rdar://problem/28207534
rdar://problem/28209456

* [Foundation] remove temp IndexPath hashing that required bridging to ref types

* [Foundation] IndexPath does not guarentee hashing to be the same as objc
@jckarter

This comment has been minimized.

Show comment
Hide comment
@jckarter

jckarter May 11, 2017

Member

<deleted, my mistake>

Member

jckarter commented May 11, 2017

<deleted, my mistake>

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment