SI-8999 Reduce memory usage in exhaustivity check

The OOM could occur when all models are forcibly expanded in the DPLL solver.

The simplest solution would be to limit the number of returned models but then
we are back in non-determinism land (since the subset we get back depends on
which models were found first).

A better alternative is to create only the models that have corresponding
counter examples.

If this does not ring a bell, here's a longer explanation:

TThe models we get from the DPLL solver need to be mapped back to counter
examples. However there's no precalculated mapping model -> counter example.
Even worse, not every valid model corresponds to a valid counter example.

The reason is that restricting the valid models further would for example
require a quadratic number of additional clauses. So to keep the optimistic case
fast (i.e., all cases are covered in a pattern match), the infeasible counter
examples are filtered later.

The DPLL procedure keeps the literals that do not contribute to the solution
unassigned, e.g., for  `(a \/ b)` only {a = true} or {b = true} is required and
the other variable can have any value. This function does a smart expansion of
the model and avoids models that have conflicting mappings.

For example for in case of the given set of symbols (taken from `t7020.scala`):
 "V2=2#16"
 "V2=6#19"
 "V2=5#18"
 "V2=4#17"
 "V2=7#20"

One possibility would be to group the symbols by domain but
this would only work for equality tests and would not be compatible
with type tests.

Another observation leads to a much simpler algorithm:
Only one of these symbols can be set to true,
since `V2` can at most be equal to one of {2,6,5,4,7}.

TODO: How does this fare with mixed TypeConst/ValueConst assignments?
When the assignments are e.g., V2=Int | V2=2 | V2=4, only the assignments
to value constants are mutually exclusive.

5 files changed, 394 insertions, 62 deletions

diff --git a/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala b/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala
index 75d2cfe0f2..9f24d5122a 100644
--- a/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala
+++ b/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala
@@ -370,9 +370,11 @@ trait Logic extends Debugging  {
     val EmptyModel: Model
     val NoModel: Model
 
+    final case class Solution(model: Model, unassigned: List[Sym])
+
     def findModelFor(solvable: Solvable): Model
 
-    def findAllModelsFor(solvable: Solvable): List[Model]
+    def findAllModelsFor(solvable: Solvable): 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 8650f6ef90..e8e666a8a5 100644
--- a/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala
+++ b/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala
@@ -6,6 +6,8 @@
 
 package scala.tools.nsc.transform.patmat
 
+import scala.annotation.tailrec
+import scala.collection.immutable.{IndexedSeq, Iterable}
 import scala.language.postfixOps
 import scala.collection.mutable
 import scala.reflect.internal.util.Statistics
@@ -514,8 +516,16 @@ trait MatchAnalysis extends MatchApproximation {
 
         // find the models (under which the match fails)
         val matchFailModels = findAllModelsFor(propToSolvable(matchFails))
+
         val scrutVar = Var(prevBinderTree)
-        val counterExamples = matchFailModels.flatMap(modelToCounterExample(scrutVar))
+        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, _)
@@ -587,6 +597,8 @@ trait MatchAnalysis extends MatchApproximation {
     case object WildcardExample extends CounterExample { override def toString = "_" }
     case object NoExample extends CounterExample { override def toString = "??" }
 
+    // returns a mapping from variable to
+    // equal and notEqual symbols
     def modelToVarAssignment(model: Model): Map[Var, (Seq[Const], Seq[Const])] =
       model.toSeq.groupBy{f => f match {case (sym, value) => sym.variable} }.mapValues{ xs =>
         val (trues, falses) = xs.partition(_._2)
@@ -600,20 +612,110 @@ trait MatchAnalysis extends MatchApproximation {
          v +"(="+ v.path +": "+ v.staticTpCheckable +") "+ assignment
        }.mkString("\n")
 
-    // return constructor call when the model is a true counter example
-    // (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): Option[CounterExample] = {
+    /**
+     * The models we get from the DPLL solver need to be mapped back to counter examples.
+     * However there's no precalculated mapping model -> counter example. Even worse,
+     * not every valid model corresponds to a valid counter example.
+     * The reason is that restricting the valid models further would for example require
+     * a quadratic number of additional clauses. So to keep the optimistic case fast
+     * (i.e., all cases are covered in a pattern match), the infeasible counter examples
+     * are filtered later.
+     *
+     * The DPLL procedure keeps the literals that do not contribute to the solution
+     * unassigned, e.g., for  `(a \/ b)`
+     * only {a = true} or {b = true} is required and the other variable can have any value.
+     *
+     * This function does a smart expansion of the model and avoids models that
+     * have conflicting mappings.
+     *
+     * For example for in case of the given set of symbols (taken from `t7020.scala`):
+     *  "V2=2#16"
+     *  "V2=6#19"
+     *  "V2=5#18"
+     *  "V2=4#17"
+     *  "V2=7#20"
+     *
+     * One possibility would be to group the symbols by domain but
+     * this would only work for equality tests and would not be compatible
+     * with type tests.
+     * Another observation leads to a much simpler algorithm:
+     * Only one of these symbols can be set to true,
+     * since `V2` can at most be equal to one of {2,6,5,4,7}.
+     */
+    def expandModel(solution: Solution): List[Map[Var, (Seq[Const], Seq[Const])]] = {
+
+      val model = solution.model
+
       // x1 = ...
       // x1.hd = ...
       // x1.tl = ...
       // x1.hd.hd = ...
       // ...
       val varAssignment = modelToVarAssignment(model)
+      debug.patmat("var assignment for model " + model + ":\n" + varAssignmentString(varAssignment))
+
+      // group symbols that assign values to the same variables (i.e., symbols are mutually exclusive)
+      // (thus the groups are sets of disjoint assignments to variables)
+      val groupedByVar: Map[Var, List[Sym]] = solution.unassigned.groupBy(_.variable)
+
+      val expanded = for {
+        (variable, syms) <- groupedByVar.toList
+      } yield {
+
+        val (equal, notEqual) = varAssignment.getOrElse(variable, Nil -> Nil)
+
+        def addVarAssignment(equalTo: List[Const], notEqualTo: List[Const]) = {
+          Map(variable ->(equal ++ equalTo, notEqual ++ notEqualTo))
+        }
+
+        // this assignment is needed in case that
+        // there exists already an assign
+        val allNotEqual = addVarAssignment(Nil, syms.map(_.const))
 
-      debug.patmat("var assignment for model "+ model +":\n"+ varAssignmentString(varAssignment))
+        // this assignment is conflicting on purpose:
+        // a list counter example could contain wildcards: e.g. `List(_,_)`
+        val allEqual = addVarAssignment(syms.map(_.const), Nil)
 
+        if(equal.isEmpty) {
+          val oneHot = for {
+            s <- syms
+          } yield {
+            addVarAssignment(List(s.const), syms.filterNot(_ == s).map(_.const))
+          }
+          allEqual :: allNotEqual :: oneHot
+        } else {
+          allEqual :: allNotEqual :: Nil
+        }
+      }
+
+      if (expanded.isEmpty) {
+        List(varAssignment)
+      } else {
+        // we need the cartesian product here,
+        // since we want to report all missing cases
+        // (i.e., combinations)
+        val cartesianProd = expanded.reduceLeft((xs, ys) =>
+          for {map1 <- xs
+               map2 <- ys} yield {
+            map1 ++ map2
+          })
+
+        // add expanded variables
+        // note that we can just use `++`
+        // since the Maps have disjoint keySets
+        for {
+          m <- cartesianProd
+        } yield {
+          varAssignment ++ m
+        }
+      }
+    }
+
+    // return constructor call when the model is a true counter example
+    // (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)(varAssignment: Map[Var, (Seq[Const], Seq[Const])]): Option[CounterExample] = {
       // chop a path into a list of symbols
       def chop(path: Tree): List[Symbol] = path match {
         case Ident(_) => List(path.symbol)
@@ -742,7 +844,7 @@ trait MatchAnalysis extends MatchApproximation {
               // 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 _ => Some(NoExample)
diff --git a/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala b/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala
index 1ba13c0617..27217f0dc2 100644
--- a/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala
+++ b/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala
@@ -288,7 +288,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[Model] = {
+    def findAllModelsFor(solvable: Solvable): List[Solution] = {
       debug.patmat("find all models for\n"+ cnfString(solvable.cnf))
 
       // we must take all vars from non simplified formula
@@ -305,54 +305,12 @@ trait Solving extends Logic {
         relevantLits.map(lit => -lit)
       }
 
-      /**
-       * 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[Int], model: TseitinModel): List[TseitinModel] = {
-        // the number of solutions is doubled for every unassigned variable
-        val expandedModels = 1 << unassigned.size
-        var current = mutable.ArrayBuffer[TseitinModel]()
-        var next = mutable.ArrayBuffer[TseitinModel]()
-        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
-
-            next += force(Lit(s))
-            next += force(Lit(-s))
-          }
-
-          val tmp = current
-          current = next
-          next = tmp
-
-          next.clear()
-        }
-
-        current.toList
+      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[TseitinModel],
-                        recursionDepthAllowed: Int = global.settings.YpatmatExhaustdepth.value): List[TseitinModel]=
+                        models: List[TseitinSolution],
+                        recursionDepthAllowed: Int = global.settings.YpatmatExhaustdepth.value): List[TseitinSolution]=
         if (recursionDepthAllowed == 0) {
           val maxDPLLdepth = global.settings.YpatmatExhaustdepth.value
           reportWarning("(Exhaustivity analysis reached max recursion depth, not all missing cases are reported. " +
@@ -368,17 +326,15 @@ trait Solving extends Logic {
             val unassigned: List[Int] = (relevantVars -- model.map(lit => lit.variable)).toList
             debug.patmat("unassigned "+ unassigned +" in "+ model)
 
-            val forced = expandUnassigned(unassigned, model)
-            debug.patmat("forced "+ forced)
+            val solution = TseitinSolution(model, unassigned)
             val negated = negateModel(model)
-            findAllModels(clauses :+ negated, forced ++ models, recursionDepthAllowed - 1)
+            findAllModels(clauses :+ negated, solution :: models, recursionDepthAllowed - 1)
           }
           else models
         }
 
-      val tseitinModels: List[TseitinModel] = findAllModels(solvable.cnf, Nil)
-      val models: List[Model] = tseitinModels.map(projectToModel(_, solvable.symbolMapping.symForVar))
-      models
+      val tseitinSolutions = findAllModels(solvable.cnf, Nil)
+      tseitinSolutions.map(_.projectToSolution(solvable.symbolMapping.symForVar))
     }
 
     private def withLit(res: TseitinModel, l: Lit): TseitinModel = {
diff --git a/test/files/pos/t8999.flags b/test/files/pos/t8999.flags
new file mode 100644
index 0000000000..0f96f1f872
--- /dev/null
+++ b/test/files/pos/t8999.flags
@@ -0,0 +1 @@
+-nowarn
\ No newline at end of file
diff --git a/test/files/pos/t8999.scala b/test/files/pos/t8999.scala
new file mode 100644
index 0000000000..99c4b2ad84
--- /dev/null
+++ b/test/files/pos/t8999.scala
@@ -0,0 +1,271 @@
+object Types {
+
+  abstract sealed class Type
+
+  case object AnyType extends Type
+
+  case object NothingType extends Type
+
+  case object UndefType extends Type
+
+  case object BooleanType extends Type
+
+  case object IntType extends Type
+
+  case object LongType extends Type
+
+  case object FloatType extends Type
+
+  case object DoubleType extends Type
+
+  case object StringType extends Type
+
+  case object NullType extends Type
+
+  sealed abstract class ReferenceType extends Type
+
+  final case class ClassType(className: String) extends ReferenceType
+
+  final case class ArrayType(baseClassName: String, dimensions: Int) extends ReferenceType
+
+  final case class RecordType(fields: List[RecordType.Field]) extends Type
+
+  object RecordType {
+    final case class Field(name: String, originalName: Option[String],
+        tpe: Type, mutable: Boolean)
+  }
+
+  case object NoType extends Type
+
+}
+
+
+sealed abstract class ClassKind
+
+object ClassKind {
+
+  case object Class extends ClassKind
+
+  case object ModuleClass extends ClassKind
+
+  case object Interface extends ClassKind
+
+  case object RawJSType extends ClassKind
+
+  case object HijackedClass extends ClassKind
+
+  case object TraitImpl extends ClassKind
+
+}
+
+object Trees {
+
+  import Types._
+
+  abstract sealed class Tree
+
+  case object EmptyTree extends Tree
+
+  sealed trait PropertyName
+  case class Ident(name: String, originalName: Option[String]) extends PropertyName
+  object Ident {
+    def apply(name: String): Ident =
+      new Ident(name, Some(name))
+  }
+
+  case class VarDef(name: Ident, vtpe: Type, mutable: Boolean, rhs: Tree) extends Tree
+
+  case class ParamDef(name: Ident, ptpe: Type, mutable: Boolean) extends Tree
+
+  case class Skip() extends Tree
+
+  class Block private(val stats: List[Tree]) extends Tree
+
+  object Block {
+    def unapply(block: Block): Some[List[Tree]] = Some(block.stats)
+  }
+
+  case class Labeled(label: Ident, tpe: Type, body: Tree) extends Tree
+
+  case class Assign(lhs: Tree, rhs: Tree) extends Tree
+
+  case class Return(expr: Tree, label: Option[Ident] = None) extends Tree
+
+  case class If(cond: Tree, thenp: Tree, elsep: Tree) extends Tree
+
+  case class While(cond: Tree, body: Tree, label: Option[Ident] = None) extends Tree
+
+  case class DoWhile(body: Tree, cond: Tree, label: Option[Ident] = None) extends Tree
+
+  case class Try(block: Tree, errVar: Ident, handler: Tree, finalizer: Tree) extends Tree
+
+  case class Throw(expr: Tree) extends Tree
+
+  case class Continue(label: Option[Ident] = None) extends Tree
+
+  case class Match(selector: Tree, cases: List[(List[Literal], Tree)], default: Tree) extends Tree
+
+  case class Debugger() extends Tree
+
+  case class New(cls: ClassType, ctor: Ident, args: List[Tree]) extends Tree
+
+  case class LoadModule(cls: ClassType) extends Tree
+
+  case class StoreModule(cls: ClassType, value: Tree) extends Tree
+
+  case class Select(qualifier: Tree, item: Ident, mutable: Boolean) extends Tree
+
+  case class Apply(receiver: Tree, method: Ident, args: List[Tree]) extends Tree
+
+  case class StaticApply(receiver: Tree, cls: ClassType, method: Ident, args: List[Tree]) extends Tree
+
+  case class TraitImplApply(impl: ClassType, method: Ident, args: List[Tree]) extends Tree
+
+  case class UnaryOp(op: Int, lhs: Tree) extends Tree
+
+  case class BinaryOp(op: Int, lhs: Tree, rhs: Tree) extends Tree
+
+  case class NewArray(tpe: ArrayType, lengths: List[Tree]) extends Tree
+
+  case class ArrayValue(tpe: ArrayType, elems: List[Tree]) extends Tree
+
+  case class ArrayLength(array: Tree) extends Tree
+
+  case class ArraySelect(array: Tree, index: Tree) extends Tree
+
+  case class RecordValue(tpe: RecordType, elems: List[Tree]) extends Tree
+
+  case class IsInstanceOf(expr: Tree, cls: ReferenceType) extends Tree
+
+  case class AsInstanceOf(expr: Tree, cls: ReferenceType) extends Tree
+
+  case class Unbox(expr: Tree, charCode: Char) extends Tree
+
+  case class GetClass(expr: Tree) extends Tree
+
+  case class CallHelper(helper: String, args: List[Tree]) extends Tree
+
+  case class JSNew(ctor: Tree, args: List[Tree]) extends Tree
+
+  case class JSDotSelect(qualifier: Tree, item: Ident) extends Tree
+
+  case class JSBracketSelect(qualifier: Tree, item: Tree) extends Tree
+
+  case class JSFunctionApply(fun: Tree, args: List[Tree]) extends Tree
+
+  case class JSDotMethodApply(receiver: Tree, method: Ident, args: List[Tree]) extends Tree
+
+  case class JSBracketMethodApply(receiver: Tree, method: Tree, args: List[Tree]) extends Tree
+
+  case class JSDelete(prop: Tree) extends Tree
+
+  case class JSUnaryOp(op: String, lhs: Tree) extends Tree
+
+  case class JSBinaryOp(op: String, lhs: Tree, rhs: Tree) extends Tree
+
+  case class JSArrayConstr(items: List[Tree]) extends Tree
+
+  case class JSObjectConstr(fields: List[(PropertyName, Tree)]) extends Tree
+
+  case class JSEnvInfo() extends Tree
+
+  sealed trait Literal extends Tree
+
+  case class Undefined() extends Literal
+
+  case class UndefinedParam() extends Literal
+
+  case class Null() extends Literal
+
+  case class BooleanLiteral(value: Boolean) extends Literal
+
+  case class IntLiteral(value: Int) extends Literal
+
+  case class LongLiteral(value: Long) extends Literal
+
+  case class FloatLiteral(value: Float) extends Literal
+
+  case class DoubleLiteral(value: Double) extends Literal
+
+  case class StringLiteral(value: String) extends Literal with PropertyName
+
+  case class ClassOf(cls: ReferenceType) extends Literal
+
+  case class VarRef(ident: Ident, mutable: Boolean) extends Tree
+
+  case class This() extends Tree
+
+  case class Closure(captureParams: List[ParamDef], params: List[ParamDef],
+                     body: Tree, captureValues: List[Tree]) extends Tree
+
+  case class ClassDef(name: Ident, kind: ClassKind, parent: Option[Ident], ancestors: List[Ident], defs: List[Tree]) extends Tree
+
+  case class MethodDef(name: PropertyName, args: List[ParamDef], resultType: Type, body: Tree) extends Tree
+
+  case class PropertyDef(name: PropertyName, getterBody: Tree, setterArg: ParamDef, setterBody: Tree) extends Tree
+
+  case class ConstructorExportDef(name: String, args: List[ParamDef], body: Tree) extends Tree
+
+  case class ModuleExportDef(fullName: String) extends Tree
+
+  final class TreeHash(val treeHash: Array[Byte], val posHash: Array[Byte])
+}
+
+object Main {
+  import Trees._
+  import Types._
+
+  private def transform(tree: Tree) = {
+    val ObjectClass = "O"
+    tree match {
+      case VarDef(_, _, _, rhs)                                             =>
+      case tree: Block                                                      =>
+      case Labeled(ident@Ident(label, _), tpe, body)                        =>
+      case Assign(lhs, rhs)                                                 =>
+      case Return(expr, optLabel)                                           =>
+      case If(cond, thenp, elsep)                                           =>
+      case While(cond, body, optLabel)                                      =>
+      case DoWhile(body, cond, None)                                        =>
+      case Try(block, errVar, EmptyTree, finalizer)                         =>
+      case Try(block, errVar@Ident(name, originalName), handler, finalizer) =>
+      case Throw(expr)                                                      =>
+      case Continue(optLabel)                                               =>
+      case Match(selector, cases, default)                                  =>
+      case New(cls, ctor, args)                                             =>
+      case StoreModule(cls, value)                                          =>
+      case tree: Select                                                     =>
+      case tree: Apply                                                      =>
+      case tree: StaticApply                                                =>
+      case tree: TraitImplApply                                             =>
+      case tree@UnaryOp(_, arg)                                             =>
+      case tree@BinaryOp(op, lhs, rhs)                                      =>
+      case NewArray(tpe, lengths)                                           =>
+      case ArrayValue(tpe, elems)                                           =>
+      case ArrayLength(array)                                               =>
+      case ArraySelect(array, index)                                        =>
+      case RecordValue(tpe, elems)                                          =>
+      case IsInstanceOf(expr, ClassType(ObjectClass))                       =>
+      case IsInstanceOf(expr, tpe)                                          =>
+      case AsInstanceOf(expr, ClassType(ObjectClass))                       =>
+      case AsInstanceOf(expr, cls)                                          =>
+      case Unbox(arg, charCode)                                             =>
+      case GetClass(expr)                                                   =>
+      case JSNew(ctor, args)                                                =>
+      case JSDotSelect(qualifier, item)                                     =>
+      case JSBracketSelect(qualifier, item)                                 =>
+      case tree: JSFunctionApply                                            =>
+      case JSDotMethodApply(receiver, method, args)                         =>
+      case JSBracketMethodApply(receiver, method, args)                     =>
+      case JSDelete(JSDotSelect(obj, prop))                                 =>
+      case JSDelete(JSBracketSelect(obj, prop))                             =>
+      case JSUnaryOp(op, lhs)                                               =>
+      case JSBinaryOp(op, lhs, rhs)                                         =>
+      case JSArrayConstr(items)                                             =>
+      case JSObjectConstr(fields)                                           =>
+      case _: VarRef | _: This                                              =>
+      case Closure(captureParams, params, body, captureValues)              =>
+      case _: Skip | _: Debugger | _: LoadModule |
+           _: JSEnvInfo | _: Literal | EmptyTree                            =>
+    }
+  }
+}
\ No newline at end of file