Skip to content
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
Merged

Redo Exhaustiveness Analysis #8908

merged 3 commits into from
Apr 29, 2017

Conversation

CodaFi
Copy link
Contributor

@CodaFi 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
Copy link
Contributor Author

CodaFi commented Apr 21, 2017

@swift-ci please smoke test

@jrose-apple
Copy link
Contributor

cc @gottesmm

@CodaFi
Copy link
Contributor Author

CodaFi commented Apr 21, 2017

@swift-ci please smoke test macOS platform

@CodaFi
Copy link
Contributor Author

CodaFi commented Apr 21, 2017

@swift-ci please smoke test macOS platform

@CodaFi
Copy link
Contributor Author

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
Copy link
Contributor Author

CodaFi commented Apr 21, 2017

@swift-ci please smoke test

@@ -377,6 +306,1039 @@ class StmtChecker : public StmtVisitor<StmtChecker, Stmt*> {
/// expressions are not discarded.
bool IsREPL;

/// The SpaceEngine encapsulates an algorithm for computing the exhaustiveness
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

How about putting this in its own file?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

TypeCheckSwitchStmt.cpp?

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

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this a source-breaking change?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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
Copy link
Contributor

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

std::transform(children.begin(), children.end(),
std::back_inserter(arr), [&](EnumElementDecl *eed) {
// FIXME: This shouldn't happen.
if (!eed->hasInterfaceType()) {
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@slavapestov Can you explain this? There's one test case in our suite that causes an enum element decl to be created sans interface type but still pass typechecking.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Which test?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If you replace this return with an llvm_unreachable, then test/NameBinding/reference-dependencies.swift hits it while type-checking lookUpManyTopLevelNames.

@jckarter
Copy link
Contributor

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
Copy link
Contributor

I agree 100% with @jckarter.

@jckarter
Copy link
Contributor

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
Copy link
Contributor Author

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
Copy link
Contributor

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
Copy link
Contributor Author

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
Copy link
Contributor Author

CodaFi commented Apr 22, 2017

@swift-ci please smoke test macOS platform

@CodaFi CodaFi force-pushed the space-engine branch 5 times, most recently from d3ea4f9 to ec71640 Compare April 23, 2017 22:11
@CodaFi
Copy link
Contributor Author

CodaFi commented Apr 28, 2017

Apparently GRDB is still acting up @lplarson

@lplarson
Copy link
Contributor

Hmm, not seeing that in CI.

@lplarson
Copy link
Contributor

Let's try this one more time.

@swift-ci please test source compatibility

@lplarson
Copy link
Contributor

CodaFi added 2 commits April 28, 2017 02:06
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
Copy link
Contributor Author

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
Copy link
Contributor Author

CodaFi commented Apr 28, 2017

@swift-ci please smoke test

@CodaFi
Copy link
Contributor Author

CodaFi commented Apr 28, 2017

@swift-ci please clean smoke test macOS platform

@CodaFi
Copy link
Contributor Author

CodaFi commented Apr 28, 2017

@swift-ci please test source compatibility

@CodaFi
Copy link
Contributor Author

CodaFi commented Apr 29, 2017

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

⛵️

@CodaFi CodaFi merged commit 2a7eee8 into swiftlang:master Apr 29, 2017
@CodaFi CodaFi deleted the space-engine branch April 29, 2017 01:28
@lattner
Copy link
Contributor

lattner commented May 1, 2017

Awesome @CodaFi !

palimondo referenced this pull request May 7, 2017
…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
Copy link
Contributor

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
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

9 participants