Permalink
Browse files

Exhaustivity: TreeMakers as boolean propositions

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
  • Loading branch information...
adriaanm committed May 22, 2012
1 parent 0497c15 commit 3f7b8b58748eb70aec4269f1ef63853b5ad4af60
Showing with 882 additions and 123 deletions.
  1. +1 −0 src/compiler/scala/reflect/internal/Constants.scala
  2. +1 −0 src/compiler/scala/reflect/internal/Definitions.scala
  3. +4 −5 src/compiler/scala/tools/nsc/symtab/classfile/ClassfileParser.scala
  4. +703 −1 src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala
  5. +3 −3 src/compiler/scala/tools/nsc/typechecker/Typers.scala
  6. +15 −19 test/files/neg/exhausting.check
  7. +1 −1 test/files/neg/exhausting.flags
  8. +21 −5 test/files/neg/exhausting.scala
  9. +1 −1 test/files/neg/pat_unreachable.flags
  10. +21 −34 test/files/neg/patmatexhaust.check
  11. +1 −1 test/files/neg/patmatexhaust.flags
  12. +1 −1 test/files/neg/patmatexhaust.scala
  13. +2 −6 test/files/neg/sealed-java-enums.check
  14. +1 −1 test/files/neg/sealed-java-enums.flags
  15. +3 −3 test/files/neg/switch.check
  16. +0 −1 test/files/neg/switch.flags
  17. +2 −3 test/files/neg/t3098.check
  18. +1 −1 test/files/neg/t3098.flags
  19. +2 −3 test/files/neg/t3683a.check
  20. +1 −1 test/files/neg/t3683a.flags
  21. +1 −1 test/files/neg/t3692-new.flags
  22. +1 −1 test/files/neg/t3692-old.flags
  23. +1 −0 test/files/pos/exhaust_alternatives.flags
  24. +10 −0 test/files/pos/exhaust_alternatives.scala
  25. +16 −0 test/files/pos/exhaustive_heuristics.scala
  26. +0 −31 test/files/pos/t3097.scala
  27. +24 −0 test/files/pos/virtpatmat_exhaust.scala
  28. +1 −0 test/files/pos/virtpatmat_exhaust_unchecked.flags
  29. +24 −0 test/files/pos/virtpatmat_exhaust_unchecked.scala
  30. +1 −0 test/files/run/t3097.check
  31. +18 −0 test/files/run/t3097.scala
@@ -224,6 +224,7 @@ trait Constants extends api.Constants {
case ClazzTag => "classOf[" + signature(typeValue) + "]"
case CharTag => "'" + escapedChar(charValue) + "'"
case LongTag => longValue.toString() + "L"
case EnumTag => symbolValue.name.toString()
case _ => String.valueOf(value)
}
}
@@ -609,6 +609,7 @@ trait Definitions extends reflect.api.StandardDefinitions {
def isTupleTypeOrSubtype(tp: Type) = isTupleType(tp)
def tupleField(n: Int, j: Int) = getMember(TupleClass(n), nme.productAccessorName(j))
// NOTE: returns true for NoSymbol since it's included in the TupleClass array -- is this intensional?
def isTupleSymbol(sym: Symbol) = TupleClass contains unspecializedSymbol(sym)
def isProductNClass(sym: Symbol) = ProductClass contains sym
@@ -615,12 +615,11 @@ abstract class ClassfileParser {
// sealed java enums (experimental)
if (isEnum && opt.experimental) {
// need to give singleton type
sym setInfo info.narrow
if (!sym.superClass.isSealed)
sym.superClass setFlag SEALED
val enumClass = sym.owner.linkedClassOfClass
if (!enumClass.isSealed)
enumClass setFlag (SEALED | ABSTRACT)
sym.superClass addChild sym
enumClass addChild sym
}
}
}

Large diffs are not rendered by default.

Oops, something went wrong.
@@ -2327,7 +2327,7 @@ trait Typers extends Modes with Adaptations with Taggings {
val methodBodyTyper = newTyper(context.makeNewScope(context.tree, methodSym)) // should use the DefDef for the context's tree, but it doesn't exist yet (we need the typer we're creating to create it)
paramSyms foreach (methodBodyTyper.context.scope enter _)
val match_ = methodBodyTyper.typedMatch(selector, cases, mode, ptRes)
val match_ = methodBodyTyper.typedMatch(gen.mkUnchecked(selector), cases, mode, ptRes)
val resTp = match_.tpe
val methFormals = paramSyms map (_.tpe)
@@ -2367,7 +2367,7 @@ trait Typers extends Modes with Adaptations with Taggings {
val methodBodyTyper = newTyper(context.makeNewScope(context.tree, methodSym)) // should use the DefDef for the context's tree, but it doesn't exist yet (we need the typer we're creating to create it)
paramSyms foreach (methodBodyTyper.context.scope enter _)
val match_ = methodBodyTyper.typedMatch(selector, cases, mode, ptRes)
val match_ = methodBodyTyper.typedMatch(gen.mkUnchecked(selector), cases, mode, ptRes)
val resTp = match_.tpe
anonClass setInfo ClassInfoType(parentsPartial(List(argTp, resTp)), newScope, anonClass)
@@ -2394,7 +2394,7 @@ trait Typers extends Modes with Adaptations with Taggings {
paramSyms foreach (methodBodyTyper.context.scope enter _)
methodSym setInfoAndEnter MethodType(paramSyms, BooleanClass.tpe)
val match_ = methodBodyTyper.typedMatch(selector, casesTrue, mode, BooleanClass.tpe)
val match_ = methodBodyTyper.typedMatch(gen.mkUnchecked(selector), casesTrue, mode, BooleanClass.tpe)
val body = methodBodyTyper.virtualizedMatch(match_ withAttachment DefaultOverrideMatchAttachment(FALSE_typed), mode, BooleanClass.tpe)
DefDef(methodSym, body)
@@ -1,29 +1,25 @@
exhausting.scala:20: error: match is not exhaustive!
missing combination * Nil
exhausting.scala:21: error: match may not be exhaustive.
It would fail on the following input: List(_, _, _)
def fail1[T](xs: List[T]) = xs match {
^
exhausting.scala:24: error: match is not exhaustive!
missing combination Nil
exhausting.scala:27: error: match may not be exhaustive.
It would fail on the following input: Nil
def fail2[T](xs: List[T]) = xs match {
^
exhausting.scala:27: error: match is not exhaustive!
missing combination Bar3
exhausting.scala:32: error: match may not be exhaustive.
It would fail on the following input: List(<not in (1, 2)>)
def fail3a(xs: List[Int]) = xs match {
^
exhausting.scala:39: error: match may not be exhaustive.
It would fail on the following input: Bar3
def fail3[T](x: Foo[T]) = x match {
^
exhausting.scala:31: error: match is not exhaustive!
missing combination Bar2 Bar2
exhausting.scala:47: error: match may not be exhaustive.
It would fail on the following inputs: (Bar1, Bar2), (Bar1, Bar3), (Bar2, Bar1), (Bar2, Bar2)
def fail4[T <: AnyRef](xx: (Foo[T], Foo[T])) = xx match {
^
exhausting.scala:36: error: match is not exhaustive!
missing combination Bar1 Bar2
missing combination Bar1 Bar3
missing combination Bar2 Bar1
missing combination Bar2 Bar2
exhausting.scala:56: error: match may not be exhaustive.
It would fail on the following inputs: (Bar1, Bar2), (Bar1, Bar3), (Bar2, Bar1), (Bar2, Bar2)
def fail5[T](xx: (Foo[T], Foo[T])) = xx match {
^
5 errors found
6 errors found
@@ -1 +1 @@
-Xfatal-warnings -Xoldpatmat
-Xfatal-warnings
@@ -16,30 +16,46 @@ object Test {
def ex3[T](xx: (Foo[T], Foo[T])) = xx match {
case (_: Foo[_], _: Foo[_]) => ()
}
// fails for: ::(_, ::(_, ::(_, _)))
def fail1[T](xs: List[T]) = xs match {
case Nil => "ok"
case x :: y :: Nil => "ok"
}
// fails for: Nil
def fail2[T](xs: List[T]) = xs match {
case _ :: _ => "ok"
}
// fails for: ::(<not in (2, 1)>, _)
def fail3a(xs: List[Int]) = xs match {
case 1 :: _ =>
case 2 :: _ =>
case Nil =>
}
// fails for: Bar3
def fail3[T](x: Foo[T]) = x match {
case Bar1 => "ok"
case Bar2 => "ok"
}
// fails for: (Bar1, Bar2)
// fails for: (Bar1, Bar3)
// fails for: (Bar2, Bar2)
// fails for: (Bar2, Bar1)
def fail4[T <: AnyRef](xx: (Foo[T], Foo[T])) = xx match {
case (Bar1, Bar1) => ()
case (Bar2, Bar3) => ()
case (Bar3, _) => ()
}
// fails for: (Bar1, Bar2)
// fails for: (Bar1, Bar3)
// fails for: (Bar2, Bar1)
// fails for: (Bar2, Bar2)
def fail5[T](xx: (Foo[T], Foo[T])) = xx match {
case (Bar1, Bar1) => ()
case (Bar2, Bar3) => ()
case (Bar3, _) => ()
}
def main(args: Array[String]): Unit = {
}
}
@@ -1 +1 @@
-Xoldpatmat
-Xoldpatmat
@@ -1,54 +1,41 @@
patmatexhaust.scala:7: error: match is not exhaustive!
missing combination Baz
patmatexhaust.scala:7: error: match may not be exhaustive.
It would fail on the following input: Baz
def ma1(x:Foo) = x match {
^
patmatexhaust.scala:11: error: match is not exhaustive!
missing combination Bar
patmatexhaust.scala:11: error: match may not be exhaustive.
It would fail on the following input: Bar(_)
def ma2(x:Foo) = x match {
^
patmatexhaust.scala:23: error: match is not exhaustive!
missing combination Kult Kult
missing combination Qult Qult
patmatexhaust.scala:23: error: match may not be exhaustive.
It would fail on the following inputs: (Kult(_), Kult(_)), (Qult(), Qult())
def ma3(x:Mult) = (x,x) match { // not exhaustive
^
patmatexhaust.scala:49: error: match is not exhaustive!
missing combination Gp
missing combination Gu
patmatexhaust.scala:49: error: match may not be exhaustive.
It would fail on the following inputs: Gp(), Gu
def ma4(x:Deep) = x match { // missing cases: Gu, Gp
^
patmatexhaust.scala:53: error: match is not exhaustive!
missing combination Gp
def ma5(x:Deep) = x match { // Gp
patmatexhaust.scala:53: error: match may not be exhaustive.
It would fail on the following input: Gp()
def ma5(x:Deep) = x match {
^
patmatexhaust.scala:59: error: match is not exhaustive!
missing combination Nil
patmatexhaust.scala:59: error: match may not be exhaustive.
It would fail on the following input: Nil
def ma6() = List(1,2) match { // give up
^
patmatexhaust.scala:75: error: match is not exhaustive!
missing combination B
patmatexhaust.scala:75: error: match may not be exhaustive.
It would fail on the following input: B()
def ma9(x: B) = x match {
^
patmatexhaust.scala:100: error: match is not exhaustive!
missing combination C1
patmatexhaust.scala:100: error: match may not be exhaustive.
It would fail on the following input: C1()
def ma10(x: C) = x match { // not exhaustive: C1 is not sealed.
^
patmatexhaust.scala:114: error: match is not exhaustive!
missing combination D1
missing combination D2
patmatexhaust.scala:114: error: match may not be exhaustive.
It would fail on the following inputs: D1, D2()
def ma10(x: C) = x match { // not exhaustive: C1 has subclasses.
^
patmatexhaust.scala:126: error: match is not exhaustive!
missing combination C1
patmatexhaust.scala:126: error: match may not be exhaustive.
It would fail on the following input: C1()
def ma10(x: C) = x match { // not exhaustive: C1 is not abstract.
^
10 errors found
@@ -1 +1 @@
-Xfatal-warnings -Xoldpatmat
-Xfatal-warnings
@@ -50,7 +50,7 @@ class TestSealedExhaustive { // compile only
case Ga =>
}
def ma5(x:Deep) = x match { // Gp
def ma5(x:Deep) = x match {
case Gu =>
case _ if 1 == 0 =>
case Ga =>
@@ -1,9 +1,5 @@
sealed-java-enums.scala:5: error: match is not exhaustive!
missing combination BLOCKED
missing combination State
missing combination TERMINATED
missing combination TIMED_WAITING
sealed-java-enums.scala:5: error: match may not be exhaustive.
It would fail on the following inputs: BLOCKED, TERMINATED, TIMED_WAITING
def f(state: State) = state match {
^
one error found
@@ -1 +1 @@
-Xexperimental -Xfatal-warnings -Xoldpatmat
-Xexperimental -Xfatal-warnings
@@ -1,10 +1,10 @@
switch.scala:28: error: could not emit switch for @switch annotated match
def fail1(c: Char) = (c: @switch) match {
^
^
switch.scala:38: error: could not emit switch for @switch annotated match
def fail2(c: Char) = (c: @switch @unchecked) match {
^
^
switch.scala:45: error: could not emit switch for @switch annotated match
def fail3(c: Char) = (c: @unchecked @switch) match {
^
^
three errors found
@@ -1 +0,0 @@
-Xoldpatmat
@@ -1,6 +1,5 @@
b.scala:3: error: match is not exhaustive!
missing combination C
b.scala:3: error: match may not be exhaustive.
It would fail on the following input: (_ : C)
def f = (null: T) match {
^
one error found
@@ -1 +1 @@
-Xfatal-warnings -Xoldpatmat
-Xfatal-warnings
@@ -1,6 +1,5 @@
t3683a.scala:14: error: match is not exhaustive!
missing combination XX
t3683a.scala:14: error: match may not be exhaustive.
It would fail on the following input: XX()
w match {
^
one error found
@@ -1 +1 @@
-Xfatal-warnings -Xoldpatmat
-Xfatal-warnings
@@ -1 +1 @@
-Xoldpatmat
-Xoldpatmat
@@ -1 +1 @@
-Xoldpatmat
-Xoldpatmat
@@ -0,0 +1 @@
-Xfatal-warnings
@@ -0,0 +1,10 @@
sealed abstract class X
sealed case class A(x: Boolean) extends X
case object B extends X
object Test {
def test(x: X) = x match {
case A(true) =>
case A(false) | B =>
}
}
@@ -0,0 +1,16 @@
// tests exhaustivity doesn't give warnings (due to its heuristic rewrites kicking in or it backing off)
object Test {
// List() => Nil
List(1) match {
case List() =>
case x :: xs =>
}
// we don't look into guards
val turnOffChecks = true
List(1) match {
case _ if turnOffChecks =>
}
// TODO: we back off when there are any user-defined extractors
}
View
@@ -1,31 +0,0 @@
package seal
sealed trait ISimpleValue
sealed trait IListValue extends ISimpleValue {
def items: List[IAtomicValue[_]]
}
sealed trait IAtomicValue[O] extends ISimpleValue {
def data: O
}
sealed trait IAbstractDoubleValue[O] extends IAtomicValue[O] { }
sealed trait IDoubleValue extends IAbstractDoubleValue[Double]
case class ListValue(val items: List[IAtomicValue[_]]) extends IListValue
class DoubleValue(val data: Double) extends IDoubleValue {
def asDouble = data
}
object Test {
/**
* @param args the command line arguments
*/
def main(args: Array[String]): Unit = {
val v: ISimpleValue = new DoubleValue(1)
v match {
case m: IListValue => println("list")
case a: IAtomicValue[_] => println("atomic")
}
}
}
Oops, something went wrong.

0 comments on commit 3f7b8b5

Please sign in to comment.