| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| |\
| |
| | |
virtpatmat: treemaker approximation refactorings and exhaustivity
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
We check exhaustivity by representing a match as a formula in
finite-domain propositional logic (FDPL) that is false when
the match may fail. The variables in the formula represent
tested trees in the match (type tests/value equality tests).
The approximation uses the same framework as the CSE analysis.
A matrix of tree makers is turned into a DAG, where sharing
represents the same value/type being tested.
We reduce FDPL to Boolean PL as follows.
For all assignments, V_i = c_i_j, we introduce a proposition
P_i_j that is true iff V_i is equal to the constant c_i_j,
for a given i, and all j, P_i_j are mutually exclusive
(a variable cannot have multiple values).
If the variable's domain is closed, we assert that one of P_i_j
must be true for each i and some j. The conjunction of these
propositions constitutes the equality axioms.
After going through negational normal form to conjunctive normal
form, we use a small SAT solver (the DPLL algorithm) to find
a model under which the equational axioms hold but the match fails.
The formula: EqAxioms /\ -MatchSucceeds.
Note that match failure expresses nicely in CNF: the
negation of each case (which yields a disjunction) is anded.
We then turn this model into variable assignments
(what's the variable (not) equal to, along with recursive
assignments for its fields). Valid assignments (no ill-typed
field assignments) are then presented to the user as counter examples.
A counter example is a value, a type test, a constructor call
or a wildcard. We prune the example set and only report the
most general examples. (Finally, we sort the output to yield stable,
i.e. testable, warning messages.)
A match is only checked for exhaustivity when the type of the
selector is "checkable" (has a sealed type or is a tuple
with at least one component of sealed type).
We consider statically known guard outcomes, but generally back
off (don't check exhaustivity) when a match has guards
or user-defined extractor calls. (Sometimes constant folding
lets us statically decide a guard.)
We ignore possibly failing null checks (which are performed
before calling extractors, for example), though this could
be done easily in the current framework. The problem is false
positives. People don't usually put nulls in tuples or lists.
To improve the exhaustivity checks, we rewrite `List()` to Nil.
TODO: more general rewrite of List(a, b, ..., z) to `a :: b :: ... :: z`.
When presenting counter examples, we represent lists in the
user-friendly List(a,...,z) format. (Similarly for tuples.)
There are no exhaustivity checks for a match-defined PartialFunction.
misc notes:
- fix pure case of dpll solver
impure set (symbol that occurs both as a positive and negative literal)
was always empty since I was looking for literals (which are not equal if positivity is not equal)
but should have been looking for symbols
- FDPL -> BoolPL translation collects all syms in props
since propForEqualsTo generates an Or, must traverse the prop
rather than assuming only top-level Syms are relevant...
also, propForEqualsTo will not assume Or'ing a whole domain is equivalent to True
(which it isn't, since the type test may fail in general)
- improve counter example description
- treat as constructor call when we either have definite type information about a real class,
or we have no equality information at all, but the variable's type is a class
and we gathered constraints about its fields (typically when selector is a tuple)
- flatten a :: b :: ... :: Nil to List(a, b, ...)
- don't print tuple constructor names, so instead of "Tuple2(a, b)", say "(a, b)"
- filter out more statically impossible subtypes
the static types convey more information than is actually checkable at run time
this is good, as it allows us to narrow down the subtypes of a sealed type,
however, when modeling the corresponding run-time checks we need to "erase" the
uncheckable parts (using existentials so that the types are still well-kinded),
so that we can use static subtyping as a sound model for dynamic type checks
- experimental java enum handling seals enum class
before, we created a refinement class as the placeholder for the sealed children
it seems more direct to use the enum class for that
this way, the new pattern matcher's exhaustiveness checker just works for java enums
|
| |\ \
| | |
| | | |
fix for SI-5672
|
| | |/ |
|
| |\ \
| |/
|/| |
Fixes SI-5804.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
The hash table initialSize method is now within
the the hashset and hashmap classes, and not in the companion.
Overriding this method now yields hashmaps and hashsets
of the proper initial capacity.
Review by @phaller.
|
| | |
| |
| |
| | |
Uncomment a line, as was the intent.
|
| | |
| |
| |
| |
| |
| | |
Makes `newMembers` a Map[Symbol, Buffer[Tree]] to ensure we add the forwarders to the right template.
Closes SI-5125.
|
| |\ \
| | |
| | | |
Fix SI-2488: allow named arg, in original position, before positionals
|
| | | | |
|
| |\ \ \
| | | |
| | | | |
Fixes SI-4461.
|
| | | |/
| |/|
| | |
| | | |
No review.
|
| |\ \ \
| | | |
| | | | |
Fix SI-5544
|
| | | |/
| |/|
| | |
| | | |
Type-check annotations in a context with a localDummy owner
|
| |\ \ \
| |_|/
|/| | |
Fix 4138
|
| | |/ |
|
| |\ \
| |/
|/| |
Test case for SI-3844 - fixed by #virtpatmat @adriaanm
|
| | | |
|
| |/ |
|
| |\
| |
| | |
Fix for SI-5610
|
| | | |
|
| | | |
|
| | | |
|
| |/
|
|
| |
Culling accumulated unnecessary code.
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
'refs/pull/549/head'; commit 'refs/pull/550/head'; commit 'refs/pull/551/head' into develop
|
| | | | |/ |
|
| |/ / / |
|
| |\ \ \
| | | |
| | | |
| | | | |
'refs/pull/546/head' into develop
|
| | |\| | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Don't print trees under -Xprint:all if they're identical to the
tree printed at the previous phase. It only works for a single
compilation unit but that is a huge step forward for us debuggers.
For instance this file:
trait Foo { def f = 5 }
used to produce 332 lines of output and now produces 92, with
zero loss of information. It ends with:
[[syntax trees at end of cleanup]] // a.scala: tree is unchanged since mixin
[[syntax trees at end of icode]] // a.scala: tree is unchanged since mixin
[[syntax trees at end of inliner]] // a.scala: tree is unchanged since mixin
[[syntax trees at end of inlineExceptionHandlers]] // a.scala: tree is unchanged since mixin
[[syntax trees at end of closelim]] // a.scala: tree is unchanged since mixin
[[syntax trees at end of dce]] // a.scala: tree is unchanged since mixin
[[syntax trees at end of jvm]] // a.scala: tree is unchanged since mixin
|
| | | | | | |
| | | \ \ | |
| | | \ \ | |
| | | \ \ | |
| | | \ \ | |
| | | \ \ | |
| | | \ \ | |
| | | \ \ | |
| | |\ \ \ \ \ \ \
| | |_|_|_|_|/ /
| |/| | | | | |
| | | | | | | | |
'scalamacros/topic/macrocherrypick', 'lrytz/t5626', 'lrytz/t5009', 'retronym/ticket/5029', 'retronym/ticket/4025', 'retronym/topic/quieter-nsdhnao' and 'retronym/ticket/1133' into develop
|
| | | | | | |/ /
| | | | |/| |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
Not due to virtpatmat, mind you; it passes with -Xoldpatmat.
Closes SI-4025.
|
| | | | | |/ /
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | |
| | | | | | |
Example: Given
case class C(a: Int)(b: Int)
if you call (new C(1)(2)).copy(a = 10)), you get a function (f: Int => C) such
that (f.apply(20)) yields a (new C(10)(20)).
|
| | | | |/ /
| | |/| |
| | | | |
| | | | | |
It still breaks as described in the ticket under -Xoldpatmat.
|
| |/ / / / |
|
| | | | | | |
| | \ \ \ | |
| | \ \ \ | |
| | \ \ \ | |
| |\ \ \ \ \ \
| | | |/ / /
| | |/| | |
| | | | | | |
'refs/pull/532/head'; commit 'refs/pull/533/head'; commit 'refs/pull/534/head' into develop
|
| | | |/ / /
| | | | |
| | | | |
| | | | | |
This looks like a job for... virtpatmat!
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | | |
Wonder if we should have a special area for high-turnover checkfiles.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Closes SI-4482, SI-4651, SI-3702.
Pending tests for SI-1832, SI-3439, SI-5091, SI-5231, SI-5265.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This reverts commit 58bb2d1bd2000ac3aa2c64b6c5dc56c91e911860.
I guess this must be what's failing the nightly.
|
| | |/ / /
|/| | | |
|
| |/ / / |
|
| | | | |
|
| | | |
| | |
| | |
| | | |
No boxing, no MODULE$ indirection.
|
| | | |
| | |
| | |
| | |
| | | |
This reverts commit 9b6f51d3ae6ddc6571d3101ea715e25a05aa8adb.
This reverts commit b5919100e785df58bde35bb24abe9d60b4da08a2.
|
| | | | | |
| | \ \ | |
| | \ \ | |
| | \ \ | |
| |\ \ \ \ \
| | | | | |
| | | | | |
| | | | | | |
'refs/pull/519/head'; commit 'refs/pull/520/head' into develop
|
| | | | | | | |
|
| | | | | | |
| | | | | |
| | | | | |
| | | | | | |
Hopefully without slowing things down overmuch. Closes SI-5640.
|
