Add a check to ensure that if the formulas originating from the exhaustivity /

reachability analysis are too big to be solved in reasonable time, then we skip
the analysis. I also cleaned up warnings.

Why did `t9181.scala` work fine with 2.11.4, but is now running out of memory?

In order to ensure that the scrutinee is associated only with one of the 400
derived classes we add 400*400 / 2 ~ 80k clauses to ensure mutual exclusivity.

In 2.11.4 the translation into CNF used to fail, since it would blow up already
at this point in memory. This has been fixed in 2.11.5, but now the DPLL solver
is the bottleneck.

There's a check in the search for all models (exhaustivity) that it would avoid
a blow up, but in the search for a model (reachability), such a check is
missing.

3 files changed, 111 insertions, 58 deletions

diff --git a/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala b/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala
index 0b53dc37de..4ea569c8e6 100644
--- a/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala
+++ b/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala
@@ -9,8 +9,7 @@ package tools.nsc.transform.patmat
 
 import scala.language.postfixOps
 import scala.collection.mutable
-import scala.reflect.internal.util.Statistics
-import scala.reflect.internal.util.HashSet
+import scala.reflect.internal.util.{NoPosition, Position, Statistics, HashSet}
 
 trait Logic extends Debugging  {
   import PatternMatchingStats._
@@ -71,6 +70,8 @@ trait Logic extends Debugging  {
       def unapply(v: Var): Some[Tree]
     }
 
+    def uncheckedWarning(pos: Position, msg: String): Unit
+
     def reportWarning(message: String): Unit
 
     // resets hash consing -- only supposed to be called by TreeMakersToProps
@@ -283,6 +284,23 @@ trait Logic extends Debugging  {
       }
     }
 
+    // to govern how much time we spend analyzing matches for unreachability/exhaustivity
+    object AnalysisBudget {
+      val maxDPLLdepth = global.settings.YpatmatExhaustdepth.value
+      val maxFormulaSize = 100 * math.min(Int.MaxValue / 100, maxDPLLdepth)
+
+      private def advice =
+        s"Please try with scalac -Ypatmat-exhaust-depth ${maxDPLLdepth * 2} or -Ypatmat-exhaust-depth off."
+
+      def recursionDepthReached =
+        s"Exhaustivity analysis reached max recursion depth, not all missing cases are reported.\n($advice)"
+
+      abstract class Exception(val advice: String) extends RuntimeException("CNF budget exceeded")
+
+      object formulaSizeExceeded extends Exception(s"The analysis required more space than allowed.\n$advice")
+
+    }
+
     // TODO: remove since deprecated
     val budgetProp = scala.sys.Prop[String]("scalac.patmat.analysisBudget")
     if (budgetProp.isSet) {
@@ -385,7 +403,7 @@ trait Logic extends Debugging  {
 
     def findModelFor(solvable: Solvable): Model
 
-    def findAllModelsFor(solvable: Solvable): List[Solution]
+    def findAllModelsFor(solvable: Solvable, pos: Position = NoPosition): List[Solution]
   }
 }
 
diff --git a/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala b/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala
index 34ebbc7463..cecb5c37be 100644
--- a/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala
+++ b/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala
@@ -399,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
@@ -429,44 +430,50 @@ trait MatchAnalysis extends MatchApproximation {
       val propsCasesOk   = approximate(True)  map caseWithoutBodyToProp
       val propsCasesFail = approximate(False) map (t => Not(caseWithoutBodyToProp(t)))
 
-      val (eqAxiomsFail, symbolicCasesFail) = removeVarEq(propsCasesFail, modelNull = true)
-      val (eqAxiomsOk, symbolicCasesOk)     = removeVarEq(propsCasesOk, modelNull = true)
-      val eqAxioms = simplify(And(eqAxiomsOk, eqAxiomsFail)) // I'm pretty sure eqAxiomsOk == eqAxiomsFail, but not 100% sure.
-
-      val prefix = mutable.ArrayBuffer[Prop]()
-      prefix += eqAxioms
-
-      var prefixRest = symbolicCasesFail
-      var current = symbolicCasesOk
-      var reachable = true
-      var caseIndex = 0
-
-      debug.patmat("reachability, vars:\n" + ((propsCasesFail flatMap gatherVariables).distinct map (_.describe) mkString ("\n")))
-      debug.patmat(s"equality axioms:\n$eqAxiomsOk")
-
-      // invariant (prefixRest.length == current.length) && (prefix.reverse ++ prefixRest == symbolicCasesFail)
-      // termination: prefixRest.length decreases by 1
-      while (prefixRest.nonEmpty && reachable) {
-        val prefHead = prefixRest.head
-        caseIndex += 1
-        prefixRest = prefixRest.tail
-        if (prefixRest.isEmpty) reachable = true
-        else {
-          prefix += prefHead
-          current = current.tail
+      try {
+        val (eqAxiomsFail, symbolicCasesFail) = removeVarEq(propsCasesFail, modelNull = true)
+        val (eqAxiomsOk, symbolicCasesOk) = removeVarEq(propsCasesOk, modelNull = true)
+        val eqAxioms = simplify(And(eqAxiomsOk, eqAxiomsFail)) // I'm pretty sure eqAxiomsOk == eqAxiomsFail, but not 100% sure.
+
+        val prefix = mutable.ArrayBuffer[Prop]()
+        prefix += eqAxioms
+
+        var prefixRest = symbolicCasesFail
+        var current = symbolicCasesOk
+        var reachable = true
+        var caseIndex = 0
+
+        debug.patmat("reachability, vars:\n" + ((propsCasesFail flatMap gatherVariables).distinct map (_.describe) mkString ("\n")))
+        debug.patmat(s"equality axioms:\n$eqAxiomsOk")
+
+        // invariant (prefixRest.length == current.length) && (prefix.reverse ++ prefixRest == symbolicCasesFail)
+        // termination: prefixRest.length decreases by 1
+        while (prefixRest.nonEmpty && reachable) {
+          val prefHead = prefixRest.head
+          caseIndex += 1
+          prefixRest = prefixRest.tail
+          if (prefixRest.isEmpty) reachable = true
+          else {
+            prefix += prefHead
+            current = current.tail
           val and = And((current.head +: prefix): _*)
           val model = findModelFor(eqFreePropToSolvable(and))
 
-          // debug.patmat("trying to reach:\n"+ cnfString(current.head) +"\nunder prefix:\n"+ cnfString(prefix))
-          // if (NoModel ne model) debug.patmat("reached: "+ modelString(model))
+            // debug.patmat("trying to reach:\n"+ cnfString(current.head) +"\nunder prefix:\n"+ cnfString(prefix))
+            // if (NoModel ne model) debug.patmat("reached: "+ modelString(model))
 
-          reachable = NoModel ne model
+            reachable = NoModel ne model
+          }
         }
-      }
 
-      if (Statistics.canEnable) Statistics.stopTimer(patmatAnaReach, start)
+        if (Statistics.canEnable) Statistics.stopTimer(patmatAnaReach, start)
 
-      if (reachable) None else Some(caseIndex)
+        if (reachable) None else Some(caseIndex)
+      } catch {
+        case ex: AnalysisBudget.Exception =>
+          warn(prevBinder.pos, ex, "unreachability")
+          None // CNF budget exceeded
+      }
     }
 
     // exhaustivity
@@ -507,32 +514,38 @@ trait MatchAnalysis extends MatchApproximation {
         // when does the match fail?
         val matchFails = Not(\/(symbolicCases))
 
-  // debug output:
+        // debug output:
         debug.patmat("analysing:")
         showTreeMakers(cases)
 
         // debug.patmat("\nvars:\n"+ (vars map (_.describe) mkString ("\n")))
         // debug.patmat("\nmatchFails as CNF:\n"+ cnfString(propToSolvable(matchFails)))
 
-        // find the models (under which the match fails)
-        val matchFailModels = findAllModelsFor(propToSolvable(matchFails))
+        try {
+          // find the models (under which the match fails)
+          val matchFailModels = findAllModelsFor(propToSolvable(matchFails), prevBinder.pos)
 
-        val scrutVar = Var(prevBinderTree)
-        val counterExamples = {
-          matchFailModels.flatMap {
-            model =>
-              val varAssignments = expandModel(model)
-              varAssignments.flatMap(modelToCounterExample(scrutVar) _)
+          val scrutVar = Var(prevBinderTree)
+          val counterExamples = {
+            matchFailModels.flatMap {
+              model =>
+                val varAssignments = expandModel(model)
+                varAssignments.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
+          // 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
+        } catch {
+          case ex: AnalysisBudget.Exception =>
+            warn(prevBinder.pos, ex, "exhaustivity")
+            Nil // CNF budget exceeded
+        }
       }
     }
 
diff --git a/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala b/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala
index 27217f0dc2..f071dc1077 100644
--- a/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala
+++ b/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala
@@ -11,6 +11,7 @@ import scala.reflect.internal.util.Statistics
 import scala.language.postfixOps
 import scala.collection.mutable
 import scala.reflect.internal.util.Collections._
+import scala.reflect.internal.util.Position
 
 // a literal is a (possibly negated) variable
 class Lit(val v: Int) extends AnyVal {
@@ -244,11 +245,33 @@ trait Solving extends Logic {
 
     def eqFreePropToSolvable(p: Prop): Solvable = {
 
+      def doesFormulaExceedSize(p: Prop): Boolean = {
+        p match {
+          case And(ops) =>
+            if (ops.size > AnalysisBudget.maxFormulaSize) {
+              true
+            } else {
+              ops.exists(doesFormulaExceedSize)
+            }
+          case Or(ops)  =>
+            if (ops.size > AnalysisBudget.maxFormulaSize) {
+              true
+            } else {
+              ops.exists(doesFormulaExceedSize)
+            }
+          case Not(a)   => doesFormulaExceedSize(a)
+          case _        => false
+        }
+      }
+
+      val simplified = simplify(p)
+      if (doesFormulaExceedSize(simplified)) {
+        throw AnalysisBudget.formulaSizeExceeded
+      }
+
       // collect all variables since after simplification / CNF conversion
       // they could have been removed from the formula
       val symbolMapping = new SymbolMapping(gatherSymbols(p))
-
-      val simplified = simplify(p)
       val cnfExtractor = new AlreadyInCNF(symbolMapping)
       simplified match {
         case cnfExtractor.ToCnf(solvable) =>
@@ -288,7 +311,7 @@ trait Solving extends Logic {
     val NoTseitinModel: TseitinModel = null
 
     // returns all solutions, if any (TODO: better infinite recursion backstop -- detect fixpoint??)
-    def findAllModelsFor(solvable: Solvable): List[Solution] = {
+    def findAllModelsFor(solvable: Solvable, pos: Position): List[Solution] = {
       debug.patmat("find all models for\n"+ cnfString(solvable.cnf))
 
       // we must take all vars from non simplified formula
@@ -308,13 +331,12 @@ trait Solving extends Logic {
       final case class TseitinSolution(model: TseitinModel, unassigned: List[Int]) {
         def projectToSolution(symForVar: Map[Int, Sym]) = Solution(projectToModel(model, symForVar), unassigned map symForVar)
       }
+
       def findAllModels(clauses: Array[Clause],
                         models: List[TseitinSolution],
-                        recursionDepthAllowed: Int = global.settings.YpatmatExhaustdepth.value): List[TseitinSolution]=
+                        recursionDepthAllowed: Int = AnalysisBudget.maxDPLLdepth): List[TseitinSolution]=
         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.)")
+          uncheckedWarning(pos, AnalysisBudget.recursionDepthReached)
           models
         } else {
           debug.patmat("find all models for\n" + cnfString(clauses))