diff options
author | Adriaan Moors <adriaan.moors@typesafe.com> | 2014-12-18 10:11:41 -0800 |
---|---|---|
committer | Adriaan Moors <adriaan.moors@typesafe.com> | 2014-12-18 10:11:41 -0800 |
commit | 1b67ced47a12b9bf85537c43f7bdf008d00e7663 (patch) | |
tree | 2718bf9da91419c6ffe253bc458afd103ce4041b | |
parent | ecc63690f11c0c72bff62c79277761b0a04f259c (diff) | |
parent | 578c3b188a4a3588e11ad9624e3922a706a36229 (diff) | |
download | scala-1b67ced47a12b9bf85537c43f7bdf008d00e7663.tar.gz scala-1b67ced47a12b9bf85537c43f7bdf008d00e7663.tar.bz2 scala-1b67ced47a12b9bf85537c43f7bdf008d00e7663.zip |
Merge pull request #4199 from adriaanm/rebase-4193
SI-8999 Reduce memory usage in exhaustivity check
-rw-r--r-- | src/compiler/scala/tools/nsc/transform/patmat/Logic.scala | 4 | ||||
-rw-r--r-- | src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala | 118 | ||||
-rw-r--r-- | src/compiler/scala/tools/nsc/transform/patmat/Solving.scala | 62 | ||||
-rw-r--r-- | test/files/pos/t8999.flags | 1 | ||||
-rw-r--r-- | test/files/pos/t8999.scala | 271 |
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 87037b7ccc..d3a5507273 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 |