Merge pull request scala#3954 from gbasler/ticket/7746-2.11

SI-7746 fix unspecifc non-exhaustiveness warnings and non-determinism in pattern matcher (2.11)

Author: gkossakowski

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

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
 
@@ -86,7 +87,7 @@ trait Logic extends Debugging  {
       def mayBeNull: Boolean
 
       // compute the domain and return it (call registerNull first!)
-      def domainSyms: Option[mutable.LinkedHashSet[Sym]]
+      def domainSyms: Option[Set[Sym]]
 
       // the symbol for this variable being equal to its statically known type
       // (only available if registerEquality has been called for that type before)
@@ -204,7 +205,7 @@ trait Logic extends Debugging  {
     def removeVarEq(props: List[Prop], modelNull: Boolean = false): (Formula, List[Formula]) = {
       val start = if (Statistics.canEnable) Statistics.startTimer(patmatAnaVarEq) else null
 
-      val vars = mutable.LinkedHashSet[Var]()
+      val vars = new mutable.HashSet[Var]
 
       object gatherEqualities extends PropTraverser {
         override def apply(p: Prop) = p match {
@@ -291,7 +292,7 @@ trait Logic extends Debugging  {
     def eqFreePropToSolvable(p: Prop): Formula
     def cnfString(f: Formula): String
 
-    type Model = collection.immutable.SortedMap[Sym, Boolean]
+    type Model = Map[Sym, Boolean]
     val EmptyModel: Model
     val NoModel: Model
 
@@ -341,9 +342,9 @@ trait ScalaLogic extends Interface with Logic with TreeAndTypeAnalysis {
       // we enumerate the subtypes of the full type, as that allows us to filter out more types statically,
       // once we go to run-time checks (on Const's), convert them to checkable types
       // TODO: there seems to be bug for singleton domains (variable does not show up in model)
-      lazy val domain: Option[mutable.LinkedHashSet[Const]] = {
-        val subConsts: Option[mutable.LinkedHashSet[Const]] = enumerateSubtypes(staticTp).map { tps =>
-          mutable.LinkedHashSet(tps: _*).map{ tp =>
+      lazy val domain: Option[Set[Const]] = {
+        val subConsts = enumerateSubtypes(staticTp).map{ tps =>
+          tps.toSet[Type].map{ tp =>
             val domainC = TypeConst(tp)
             registerEquality(domainC)
             domainC
@@ -486,7 +487,7 @@ trait ScalaLogic extends Interface with Logic with TreeAndTypeAnalysis {
       }
 
       // accessing after calling registerNull will result in inconsistencies
-      lazy val domainSyms: Option[collection.mutable.LinkedHashSet[Sym]] = domain map { _ map symForEqualsTo }
+      lazy val domainSyms: Option[Set[Sym]] = domain map { _ map symForEqualsTo }
 
       lazy val symForStaticTp: Option[Sym]  = symForEqualsTo.get(TypeConst(staticTpCheckable))
 

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)
           }

src/compiler/scala/tools/nsc/transform/patmat/Solving.scala

@@ -26,16 +26,9 @@ trait Solving extends Logic {
     type Formula = FormulaBuilder
     def formula(c: Clause*): Formula = ArrayBuffer(c: _*)
 
-    type Clause  = collection.Set[Lit]
+    type Clause  = Set[Lit]
     // a clause is a disjunction of distinct literals
-    def clause(l: Lit*): Clause = (
-      if (l.lengthCompare(1) <= 0) {
-        l.toSet // SI-8531 Avoid LinkedHashSet's bulk for 0 and 1 element clauses
-      } else {
-        // neg/t7020.scala changes output 1% of the time, the non-determinism is quelled with this linked set
-        mutable.LinkedHashSet(l: _*)
-      }
-    )
+    def clause(l: Lit*): Clause = l.toSet
 
     type Lit
     def Lit(sym: Sym, pos: Boolean = true): Lit
@@ -115,7 +108,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))
@@ -141,36 +133,83 @@ trait Solving extends Logic {
     def cnfString(f: Formula) = alignAcrossRows(f map (_.toList) toList, "\\/", " /\\\n")
 
     // adapted from http://lara.epfl.ch/w/sav10:simple_sat_solver (original by Hossein Hojjat)
-    val EmptyModel = collection.immutable.SortedMap.empty[Sym, Boolean]
+    val EmptyModel = Map.empty[Sym, Boolean]
     val NoModel: Model = null
 
     // 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
         }
@@ -210,15 +249,14 @@ trait Solving extends Logic {
             withLit(findModelFor(dropUnit(f, unitLit)), unitLit)
           case _ =>
             // partition symbols according to whether they appear in positive and/or negative literals
-            // SI-7020 Linked- for deterministic counter examples.
-            val pos = new mutable.LinkedHashSet[Sym]()
-            val neg = new mutable.LinkedHashSet[Sym]()
+            val pos = new mutable.HashSet[Sym]()
+            val neg = new mutable.HashSet[Sym]()
             mforeach(f)(lit => if (lit.pos) pos += lit.sym else neg += lit.sym)
 
             // appearing in both positive and negative
-            val impures: mutable.LinkedHashSet[Sym] = pos intersect neg
+            val impures = pos intersect neg
             // appearing only in either positive/negative positions
-            val pures: mutable.LinkedHashSet[Sym] = (pos ++ neg) -- impures
+            val pures = (pos ++ neg) -- impures
 
             if (pures nonEmpty) {
               val pureSym = pures.head

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 =>

test/files/neg/patmatexhaust.flags

@@ -1 +1 @@
--Xfatal-warnings
+-Xfatal-warnings -Ypatmat-exhaust-depth off

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 =>
     }