Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Unreachability analysis for pattern matches
Analyze matches for unreachable cases. A case is unreachable if it implies its preceding cases. Call `C` the formula that is satisfiable if the considered case matches. Call `P` the formula that is satisfiable if the cases preceding it match. The case is reachable if there is a model for `-P /\ C`. Thus, the case is unreachable if there is no model for `-(-P /\ C)`, or, equivalently, `P \/ -C`, or `C => P`. Unreachability needs a more precise model for type and value tests than exhaustivity. Before, `{case _: Int => case 1 =>}` would be modeled as `X = Int \/ X = 1.type`, and thus, the second case would be reachable if we can satisfy `X != Int /\ X = 1.type`. Of course, the case isn't reachable, yet the formula is satisfiable, so we must augment our model to take into account that `X = 1.type => X = Int`. This is done by `removeVarEq`, which models the following axioms about equality. It does so to retain the meaning of equality after replacing `V = C` (variable = constant) by a literal (fresh symbol). For each variable: 1. a sealed type test must result in exactly one of its partitions being chosen (the core of exhaustivity) 2. when a type test is true, tests of super types must also be true, and unrelated type tests must be false For example, `V : X ::= A | B | C`, and `A => B` (since `A extends B`). Coverage (1) is formulated as: `A \/ B \/ C`, and the implications of (2) are simply `V=A => V=B /\ V=X`, `V=B => V=X`, `V=C => V=X`. Exclusion for unrelated types typically results from matches such as `{case SomeConst => case OtherConst => }`. Here, `V=SomeConst.type => !V=OtherConst.type`. This is a conservative approximation. If these constants happen to be the same value dynamically (but the types don't tell us this), the last case is actually unreachable. Of course we must err on the safe side. We simplify the equality axioms as follows (in principle this could be done by the solver, but it's easy to do before solving). If we've already excluded a pair of assignments of constants to a certain variable at some point, say `(-A \/ -B)`, then don't exclude the symmetric one `(-B \/ -A)`. (Nor the positive implications `-B \/ A`, or `-A \/ B`, which would entail the equality axioms falsifying the whole formula.) TODO: We should also model dependencies between variables: if `V1` corresponds to `x: List[_]` and `V2` is `x.hd`, `V2` cannot be assigned at all when `V1 = null` or `V1 = Nil`. Right now this is implemented hackily by pruning counter-examples in exhaustivity. Unreachability would also benefit from a more faithful representation. I had to refactor some of the framework, but most of it is shared with exhaustivity. We must allow approximating tree makers twice, sharing variables, but using different approximations for values not statically known. When considering reachability of a case, we must assume, for example, that its unknown guard succeeds (otherwise it would wrongly be considered unreachable), whereas unknown guards in the preceding cases must be considered to fail (otherwise we could never get to those case, and again, it would falsely be considered unreachable). Since this analysis is relatively expensive, you may opt-out using `-Xno-patmat-analysis` (or annotating the selector with @unchecked). We hope to improve the performance in the near future. -Ystatistics has also been extended to provide some numbers on time spent in the equality-rewrite, solving and analyzing.
- Loading branch information
Showing
10 changed files
with
807 additions
and
249 deletions.
There are no files selected for viewing
951 changes: 706 additions & 245 deletions
951
src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala
Large diffs are not rendered by default.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,4 @@ | ||
virtpatmat_reach_null.scala:13: error: unreachable code | ||
case _ => // unreachable | ||
^ | ||
one error found |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
-Xfatal-warnings |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,19 @@ | ||
sealed abstract class Const { | ||
final def excludes(other: Const) = | ||
(this, other) match { | ||
case (_, NullConst) => | ||
case (NullConst, _) => | ||
case (_: ValueConst, _: ValueConst) => | ||
case (_: ValueConst, _: TypeConst) => | ||
case (_: TypeConst, _: ValueConst) => | ||
case (_: TypeConst, _: TypeConst) => | ||
case (null, _) => | ||
case (_, null) => | ||
case null => | ||
case _ => // unreachable | ||
} | ||
} | ||
|
||
sealed class TypeConst extends Const | ||
sealed class ValueConst extends Const | ||
case object NullConst extends Const |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,14 @@ | ||
virtpatmat_reach_sealed_unsealed.scala:16: error: match may not be exhaustive. | ||
It would fail on the following input: false | ||
(true: Boolean) match { case true => } // not exhaustive, but reachable | ||
^ | ||
virtpatmat_reach_sealed_unsealed.scala:18: error: unreachable code | ||
(true: Boolean) match { case true => case false => case _ => } // exhaustive, last case is unreachable | ||
^ | ||
virtpatmat_reach_sealed_unsealed.scala:19: error: unreachable code | ||
(true: Boolean) match { case true => case false => case _: Boolean => } // exhaustive, last case is unreachable | ||
^ | ||
virtpatmat_reach_sealed_unsealed.scala:20: error: unreachable code | ||
(true: Boolean) match { case true => case false => case _: Any => } // exhaustive, last case is unreachable | ||
^ | ||
four errors found |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1 @@ | ||
-Xfatal-warnings |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,21 @@ | ||
sealed abstract class X | ||
sealed case class A(x: Int) extends X | ||
|
||
// test reachability on mixed sealed / non-sealed matches | ||
object Test extends App { | ||
val B: X = A(0) | ||
val C: X = A(1) | ||
|
||
// all cases are reachable and the match is exhaustive | ||
(C: X) match { | ||
case B => | ||
case C => | ||
case A(_) => | ||
} | ||
|
||
(true: Boolean) match { case true => } // not exhaustive, but reachable | ||
(true: Boolean) match { case true => case false => } // exhaustive, reachable | ||
(true: Boolean) match { case true => case false => case _ => } // exhaustive, last case is unreachable | ||
(true: Boolean) match { case true => case false => case _: Boolean => } // exhaustive, last case is unreachable | ||
(true: Boolean) match { case true => case false => case _: Any => } // exhaustive, last case is unreachable | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,11 @@ | ||
// check the interaction between constants and type tests in creating the equality axioms | ||
object Test { | ||
type Formula = List[String] | ||
val TrueF: Formula = List() | ||
def distribute(a: Formula, b: Formula) = (a, b) match { | ||
case (TrueF, _) => | ||
case (_, TrueF) => // bug: considered unreachable | ||
case (a :: Nil, b :: Nil) => | ||
case _ => | ||
} | ||
} |