SI-7746 patmat: fix non-determinism, infeasible counter examples

Fixes non-determinism within the DPLL algorithm and disallows
infeasible counter examples directly in the formula.

The function to compute all solutions was flawed and thus only
returned a subset of the solutions. The algorithm would stop too soon
and thus depending on the ordering of the symbols return more or less
solutions. I also added printing a warning when the search was stopped
because the max recursion depth was reached. This is very useful as an
explanation of spuriously failing regression tests, since less counter
examples might be reported. In such a case the recursion depth should
be set to infinite by adding `-Ypatmat-exhaust-depth off`.

The mapping of the solutions of the DPLL algorithm to counter examples
has been adapted to take the additional solutions from the
solver into account:

Consider for example `t8430.scala`:

```Scala
sealed trait CL3Literal
case object IntLit extends CL3Literal
case object CharLit extends CL3Literal
case object BooleanLit extends CL3Literal
case object UnitLit extends CL3Literal

sealed trait Tree
case class LetL(value: CL3Literal) extends Tree
case object LetP extends Tree
case object LetC extends Tree
case object LetF extends Tree

object Test {
  (tree: Tree) => tree match {case LetL(CharLit) => ??? }
}
```

This test contains 2 domains,  `IntLit, CharLit, ...` and `LetL, LetP, ...`,
the corresponding formula to check exhaustivity looks like:

```
    V1=LetC.type#13    \/ V1=LetF.type#14 \/    V1=LetL#11     \/  V1=LetP.type#15    /\
 V2=BooleanLit.type#16 \/  V2=CharLit#12  \/ V2=IntLit.type#17 \/ V2=UnitLit.type#18  /\
      -V1=LetL#11      \/ -V2=CharLit#12  \/                   \/
```

The first two lines assign a value of the domain to the scrutinee (and
the correponding member in case of `LetL`) and prohibit the counter
example `LetL(CharLit)` since it's covered by the pattern match. The
used Boolean encoding allows that scrutinee `V1` can be equal to
`LetC` and `LetF` at the same time and thus, during enumeration of all
possible solutions of the formula, such a solution will be found,
since only one literal needs to be set to true, to  satisfy that
clause. That means, if at least one of the literals of such a clause
was in the `unassigned` list of the DPLL procedure, we will get
solutions where the scrutinee is equal to more than one element of the
domain.

A remedy would be to add constraints that forbid both literals
to be true at the same time. His is infeasible for big domains (see
`pos/t8531.scala`), since we would have to add a quadratic number of
clauses (one clause for each pair in the domain). A much simpler
solution is to just filter the invalid results. Since both values for
`unassigned` literals are explored, we will eventually find a valid
counter example.

11 files changed, 115 insertions, 41 deletions

diff --git a/src/compiler/scala/tools/nsc/settings/ScalaSettings.scala b/src/compiler/scala/tools/nsc/settings/ScalaSettings.scala
index 466e397dd7..850534f2cc 100644
--- a/src/compiler/scala/tools/nsc/settings/ScalaSettings.scala
+++ b/src/compiler/scala/tools/nsc/settings/ScalaSettings.scala
@@ -262,6 +262,8 @@ trait ScalaSettings extends AbsScalaSettings
   val Yreifydebug             = BooleanSetting("-Yreify-debug", "Trace reification.")
   val Ytyperdebug             = BooleanSetting("-Ytyper-debug", "Trace all type assignments.")
   val Ypatmatdebug            = BooleanSetting("-Ypatmat-debug", "Trace pattern matching translation.")
+  val YpatmatExhaustdepth     = IntSetting("-Ypatmat-exhaust-depth", "off", 20, Some((10, Int.MaxValue)),
+    str => Some(if(str.equalsIgnoreCase("off")) Int.MaxValue else str.toInt))
   val Yquasiquotedebug        = BooleanSetting("-Yquasiquote-debug", "Trace quasiquote-related activities.")
 
   // TODO 2.12 Remove
diff --git a/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala b/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala
index 0899507bab..3331805c1b 100644
--- a/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala
+++ b/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala
@@ -10,7 +10,6 @@ package tools.nsc.transform.patmat
 import scala.language.postfixOps
 import scala.collection.mutable
 import scala.reflect.internal.util.Statistics
-import scala.reflect.internal.util.Position
 import scala.reflect.internal.util.HashSet
 
 trait Logic extends Debugging  {
@@ -72,6 +71,8 @@ trait Logic extends Debugging  {
       def unapply(v: Var): Some[Tree]
     }
 
+    def reportWarning(message: String): Unit
+
     // resets hash consing -- only supposed to be called by TreeMakersToProps
     def prepareNewAnalysis(): Unit
 
diff --git a/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala b/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala
index b2dc6e4e52..a8852a3ff3 100644
--- a/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala
+++ b/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala
@@ -9,7 +9,6 @@ package scala.tools.nsc.transform.patmat
 import scala.language.postfixOps
 import scala.collection.mutable
 import scala.reflect.internal.util.Statistics
-import scala.reflect.internal.util.Position
 
 trait TreeAndTypeAnalysis extends Debugging {
   import global._
@@ -400,6 +399,7 @@ trait MatchAnalysis extends MatchApproximation {
   trait MatchAnalyzer extends MatchApproximator  {
     def uncheckedWarning(pos: Position, msg: String) = currentRun.reporting.uncheckedWarning(pos, msg)
     def warn(pos: Position, ex: AnalysisBudget.Exception, kind: String) = uncheckedWarning(pos, s"Cannot check match for $kind.\n${ex.advice}")
+    def reportWarning(message: String) = global.reporter.warning(typer.context.tree.pos, message)
 
   // TODO: model dependencies between variables: if V1 corresponds to (x: List[_]) and V2 is (x.hd), V2 cannot be assigned when V1 = null or V1 = Nil
     // right now hackily implement this by pruning counter-examples
@@ -524,9 +524,11 @@ trait MatchAnalysis extends MatchApproximation {
           val matchFailModels = findAllModelsFor(propToSolvable(matchFails))
 
           val scrutVar = Var(prevBinderTree)
-          val counterExamples = matchFailModels.map(modelToCounterExample(scrutVar))
-
-          val pruned = CounterExample.prune(counterExamples).map(_.toString).sorted
+          val counterExamples = matchFailModels.flatMap(modelToCounterExample(scrutVar))
+          // sorting before pruning is important here in order to
+          // keep neg/t7020.scala stable
+          // since e.g. List(_, _) would cover List(1, _)
+          val pruned = CounterExample.prune(counterExamples.sortBy(_.toString)).map(_.toString)
 
           if (Statistics.canEnable) Statistics.stopTimer(patmatAnaExhaust, start)
           pruned
@@ -616,7 +618,7 @@ trait MatchAnalysis extends MatchApproximation {
     // (the variables don't take into account type information derived from other variables,
     //  so, naively, you might try to construct a counter example like _ :: Nil(_ :: _, _ :: _),
     //  since we didn't realize the tail of the outer cons was a Nil)
-    def modelToCounterExample(scrutVar: Var)(model: Model): CounterExample = {
+    def modelToCounterExample(scrutVar: Var)(model: Model): Option[CounterExample] = {
       // x1 = ...
       // x1.hd = ...
       // x1.tl = ...
@@ -674,6 +676,7 @@ trait MatchAnalysis extends MatchApproximation {
         private val fields: mutable.Map[Symbol, VariableAssignment] = mutable.HashMap.empty
         // need to prune since the model now incorporates all super types of a constant (needed for reachability)
         private lazy val uniqueEqualTo = equalTo filterNot (subsumed => equalTo.exists(better => (better ne subsumed) && instanceOfTpImplies(better.tp, subsumed.tp)))
+        private lazy val inSameDomain = uniqueEqualTo forall (const => variable.domainSyms.exists(_.exists(_.const.tp =:= const.tp)))
         private lazy val prunedEqualTo = uniqueEqualTo filterNot (subsumed => variable.staticTpCheckable <:< subsumed.tp)
         private lazy val ctor       = (prunedEqualTo match { case List(TypeConst(tp)) => tp case _ => variable.staticTpCheckable }).typeSymbol.primaryConstructor
         private lazy val ctorParams = if (ctor.paramss.isEmpty) Nil else ctor.paramss.head
@@ -694,13 +697,13 @@ trait MatchAnalysis extends MatchApproximation {
         // NoExample if the constructor call is ill-typed
         // (thus statically impossible -- can we incorporate this into the formula?)
         // beBrief is used to suppress negative information nested in tuples -- it tends to get too noisy
-        def toCounterExample(beBrief: Boolean = false): CounterExample =
-          if (!allFieldAssignmentsLegal) NoExample
+        def toCounterExample(beBrief: Boolean = false): Option[CounterExample] =
+          if (!allFieldAssignmentsLegal) Some(NoExample)
           else {
             debug.patmat("describing "+ ((variable, equalTo, notEqualTo, fields, cls, allFieldAssignmentsLegal)))
             val res = prunedEqualTo match {
               // a definite assignment to a value
-              case List(eq: ValueConst) if fields.isEmpty => ValueExample(eq)
+              case List(eq: ValueConst) if fields.isEmpty => Some(ValueExample(eq))
 
               // constructor call
               // or we did not gather any information about equality but we have information about the fields
@@ -713,30 +716,50 @@ trait MatchAnalysis extends MatchApproximation {
                   // figure out the constructor arguments from the field assignment
                   val argLen = (caseFieldAccs.length min ctorParams.length)
 
-                  (0 until argLen).map(i => fields.get(caseFieldAccs(i)).map(_.toCounterExample(brevity)) getOrElse WildcardExample).toList
+                  val examples = (0 until argLen).map(i => fields.get(caseFieldAccs(i)).map(_.toCounterExample(brevity)) getOrElse Some(WildcardExample)).toList
+                  sequence(examples)
                 }
 
                 cls match {
-                  case ConsClass               => ListExample(args())
-                  case _ if isTupleSymbol(cls) => TupleExample(args(brevity = true))
-                  case _ => ConstructorExample(cls, args())
+                  case ConsClass                                =>
+                    args().map {
+                      case List(NoExample, l: ListExample) =>
+                        // special case for neg/t7020.scala:
+                        // if we find a counter example `??::*` we report `*::*` instead
+                        // since the `??` originates from uniqueEqualTo containing several instanced of the same type
+                        List(WildcardExample, l)
+                      case args                            => args
+                    }.map(ListExample)
+                  case _ if isTupleSymbol(cls)                  => args(brevity = true).map(TupleExample)
+                  case _ if cls.isSealed && cls.isAbstractClass =>
+                    // don't report sealed abstract classes, since
+                    // 1) they can't be instantiated
+                    // 2) we are already reporting any missing subclass (since we know the full domain)
+                    // (see patmatexhaust.scala)
+                    None
+                  case _                                        => args().map(ConstructorExample(cls, _))
                 }
 
               // a definite assignment to a type
-              case List(eq) if fields.isEmpty => TypeExample(eq)
+              case List(eq) if fields.isEmpty => Some(TypeExample(eq))
 
               // negative information
               case Nil if nonTrivialNonEqualTo.nonEmpty =>
                 // negation tends to get pretty verbose
-                if (beBrief) WildcardExample
+                if (beBrief) Some(WildcardExample)
                 else {
                   val eqTo = equalTo.headOption getOrElse TypeConst(variable.staticTpCheckable)
-                  NegativeExample(eqTo, nonTrivialNonEqualTo)
+                  Some(NegativeExample(eqTo, nonTrivialNonEqualTo))
                 }
 
+              // if uniqueEqualTo contains more than one symbol of the same domain
+              // then we can safely ignore these counter examples since we will eventually encounter
+              // both counter examples separately
+              case _ if inSameDomain => None
+                
               // not a valid counter-example, possibly since we have a definite type but there was a field mismatch
               // TODO: improve reasoning -- in the mean time, a false negative is better than an annoying false positive
-              case _ => NoExample
+              case _ => Some(NoExample)
             }
             debug.patmatResult("described as")(res)
           }
diff --git a/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala b/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala
index 31b1ffa912..0d867be4b6 100644
--- a/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala
+++ b/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala
@@ -115,7 +115,6 @@ trait Solving extends Logic {
 
       if (Statistics.canEnable) Statistics.stopTimer(patmatCNF, start)
 
-      //
       if (Statistics.canEnable) patmatCNFSizes(res.size).value += 1
 
 //      debug.patmat("cnf for\n"+ p +"\nis:\n"+cnfString(res))
@@ -146,31 +145,78 @@ trait Solving extends Logic {
 
     // returns all solutions, if any (TODO: better infinite recursion backstop -- detect fixpoint??)
     def findAllModelsFor(f: Formula): List[Model] = {
+
+      debug.patmat("find all models for\n"+ cnfString(f))
+
       val vars: Set[Sym] = f.flatMap(_ collect {case l: Lit => l.sym}).toSet
       // debug.patmat("vars "+ vars)
       // the negation of a model -(S1=True/False /\ ... /\ SN=True/False) = clause(S1=False/True, ...., SN=False/True)
       def negateModel(m: Model) = clause(m.toSeq.map{ case (sym, pos) => Lit(sym, !pos) } : _*)
 
-      def findAllModels(f: Formula, models: List[Model], recursionDepthAllowed: Int = 10): List[Model]=
-        if (recursionDepthAllowed == 0) models
-        else {
-          debug.patmat("find all models for\n"+ cnfString(f))
+      /**
+       * The DPLL procedure only returns a minimal mapping from literal to value
+       * such that the CNF formula is satisfied.
+       * E.g. for:
+       * `(a \/ b)`
+       * The DPLL procedure will find either {a = true} or {b = true}
+       * as solution.
+       *
+       * The expansion step will amend both solutions with the unassigned variable
+       * i.e., {a = true} will be expanded to {a = true, b = true} and {a = true, b = false}.
+       */
+      def expandUnassigned(unassigned: List[Sym], model: Model): List[Model] = {
+        // the number of solutions is doubled for every unassigned variable
+        val expandedModels = 1 << unassigned.size
+        var current = mutable.ArrayBuffer[Model]()
+        var next = mutable.ArrayBuffer[Model]()
+        current.sizeHint(expandedModels)
+        next.sizeHint(expandedModels)
+
+        current += model
+
+        // we use double buffering:
+        // read from `current` and create a two models for each model in `next`
+        for {
+          s <- unassigned
+        } {
+          for {
+            model <- current
+          } {
+            def force(l: Lit) = model + (l.sym -> l.pos)
+
+            next += force(Lit(s, pos = true))
+            next += force(Lit(s, pos = false))
+          }
+
+          val tmp = current
+          current = next
+          next = tmp
+
+          next.clear()
+        }
+
+        current.toList
+      }
+
+      def findAllModels(f: Formula,
+                        models: List[Model],
+                        recursionDepthAllowed: Int = global.settings.YpatmatExhaustdepth.value): List[Model]=
+        if (recursionDepthAllowed == 0) {
+          val maxDPLLdepth = global.settings.YpatmatExhaustdepth.value
+          reportWarning("(Exhaustivity analysis reached max recursion depth, not all missing cases are reported. " +
+              s"Please try with scalac -Ypatmat-exhaust-depth ${maxDPLLdepth * 2} or -Ypatmat-exhaust-depth off.)")
+          models
+        } else {
           val model = findModelFor(f)
           // if we found a solution, conjunct the formula with the model's negation and recurse
           if (model ne NoModel) {
             val unassigned = (vars -- model.keySet).toList
             debug.patmat("unassigned "+ unassigned +" in "+ model)
-            def force(lit: Lit) = {
-              val model = withLit(findModelFor(dropUnit(f, lit)), lit)
-              if (model ne NoModel) List(model)
-              else Nil
-            }
-            val forced = unassigned flatMap { s =>
-              force(Lit(s, pos = true)) ++ force(Lit(s, pos = false))
-            }
+
+            val forced = expandUnassigned(unassigned, model)
             debug.patmat("forced "+ forced)
             val negated = negateModel(model)
-            findAllModels(f :+ negated, model :: (forced ++ models), recursionDepthAllowed - 1)
+            findAllModels(f :+ negated, forced ++ models, recursionDepthAllowed - 1)
           }
           else models
         }
diff --git a/test/files/neg/patmatexhaust.check b/test/files/neg/patmatexhaust.check
index 2dad608451..bbf5e9b528 100644
--- a/test/files/neg/patmatexhaust.check
+++ b/test/files/neg/patmatexhaust.check
@@ -12,7 +12,7 @@ It would fail on the following inputs: (Kult(_), Kult(_)), (Qult(), Qult())
                       ^
 patmatexhaust.scala:49: warning: match may not be exhaustive.
 It would fail on the following inputs: Gp(), Gu
-    def ma4(x:Deep) = x match { // missing cases: Gu, Gp
+    def ma4(x:Deep) = x match { // missing cases: Gu, Gp which is not abstract so must be included
                       ^
 patmatexhaust.scala:55: warning: unreachable code
       case _ if 1 == 0 =>
diff --git a/test/files/neg/patmatexhaust.flags b/test/files/neg/patmatexhaust.flags
index 85d8eb2ba2..3b01ca062c 100644
--- a/test/files/neg/patmatexhaust.flags
+++ b/test/files/neg/patmatexhaust.flags
@@ -1 +1 @@
--Xfatal-warnings
+-Xfatal-warnings -Ypatmat-exhaust-depth off
\ No newline at end of file
diff --git a/test/files/neg/patmatexhaust.scala b/test/files/neg/patmatexhaust.scala
index f937197829..26f0c12a91 100644
--- a/test/files/neg/patmatexhaust.scala
+++ b/test/files/neg/patmatexhaust.scala
@@ -46,7 +46,7 @@ class TestSealedExhaustive { // compile only
       case _ =>
     }
 
-    def ma4(x:Deep) = x match { // missing cases: Gu, Gp
+    def ma4(x:Deep) = x match { // missing cases: Gu, Gp which is not abstract so must be included
       case Ga =>
     }
 
diff --git a/test/files/neg/t8430.check b/test/files/neg/t8430.check
index 7c6a73ce53..dbc0c70bba 100644
--- a/test/files/neg/t8430.check
+++ b/test/files/neg/t8430.check
@@ -1,25 +1,25 @@
 t8430.scala:15: warning: match may not be exhaustive.
-It would fail on the following inputs: ??, LetC, LetF, LetL(IntLit), LetP
+It would fail on the following inputs: LetC, LetF, LetL(BooleanLit), LetL(IntLit), LetL(UnitLit), LetP
   (tree: Tree) => tree match {case LetL(CharLit) => ??? }
                   ^
 t8430.scala:16: warning: match may not be exhaustive.
-It would fail on the following inputs: ??, LetC, LetF, LetL(IntLit), LetP
+It would fail on the following inputs: LetC, LetF, LetL(BooleanLit), LetL(IntLit), LetL(UnitLit), LetP
   (tree: Tree) => tree match {case LetL(CharLit) => ??? }
                   ^
 t8430.scala:17: warning: match may not be exhaustive.
-It would fail on the following inputs: ??, LetC, LetF, LetL(IntLit), LetP
+It would fail on the following inputs: LetC, LetF, LetL(BooleanLit), LetL(IntLit), LetL(UnitLit), LetP
   (tree: Tree) => tree match {case LetL(CharLit) => ??? }
                   ^
 t8430.scala:18: warning: match may not be exhaustive.
-It would fail on the following inputs: ??, LetC, LetF, LetL(IntLit), LetP
+It would fail on the following inputs: LetC, LetF, LetL(BooleanLit), LetL(IntLit), LetL(UnitLit), LetP
   (tree: Tree) => tree match {case LetL(CharLit) => ??? }
                   ^
 t8430.scala:19: warning: match may not be exhaustive.
-It would fail on the following inputs: ??, LetC, LetF, LetL(IntLit), LetP
+It would fail on the following inputs: LetC, LetF, LetL(BooleanLit), LetL(IntLit), LetL(UnitLit), LetP
   (tree: Tree) => tree match {case LetL(CharLit) => ??? }
                   ^
 t8430.scala:20: warning: match may not be exhaustive.
-It would fail on the following inputs: ??, LetC, LetF, LetL(IntLit), LetP
+It would fail on the following inputs: LetC, LetF, LetL(BooleanLit), LetL(IntLit), LetL(UnitLit), LetP
   (tree: Tree) => tree match {case LetL(CharLit) => ??? }
                   ^
 error: No warnings can be incurred under -Xfatal-warnings.
diff --git a/test/files/neg/t8430.flags b/test/files/neg/t8430.flags
index 85d8eb2ba2..6f60189a8d 100644
--- a/test/files/neg/t8430.flags
+++ b/test/files/neg/t8430.flags
@@ -1 +1 @@
--Xfatal-warnings
+-Xfatal-warnings -Ypatmat-exhaust-depth off
diff --git a/test/files/run/virtpatmat_nested_lists.flags b/test/files/run/virtpatmat_nested_lists.flags
new file mode 100644
index 0000000000..ca9a4c0697
--- /dev/null
+++ b/test/files/run/virtpatmat_nested_lists.flags
@@ -0,0 +1 @@
+-Ypatmat-exhaust-depth off
\ No newline at end of file
diff --git a/test/files/run/virtpatmat_opt_sharing.flags b/test/files/run/virtpatmat_opt_sharing.flags
new file mode 100644
index 0000000000..ca9a4c0697
--- /dev/null
+++ b/test/files/run/virtpatmat_opt_sharing.flags
@@ -0,0 +1 @@
+-Ypatmat-exhaust-depth off
\ No newline at end of file