diff options
author | Grzegorz Kossakowski <grzegorz.kossakowski@gmail.com> | 2014-10-06 17:17:45 +0200 |
---|---|---|
committer | Grzegorz Kossakowski <grzegorz.kossakowski@gmail.com> | 2014-10-06 17:17:45 +0200 |
commit | 8d25e84c9123fe9784ec9844b5184aa1b697b429 (patch) | |
tree | 4968b4991e0c57e5b3455114aceea03c002aba1d /src | |
parent | 830425a06ffaed5441a44edbb8018ec4e231d59d (diff) | |
parent | 34b42d850c2201d0c6dc71fa8be8b56282c7de6a (diff) | |
download | scala-8d25e84c9123fe9784ec9844b5184aa1b697b429.tar.gz scala-8d25e84c9123fe9784ec9844b5184aa1b697b429.tar.bz2 scala-8d25e84c9123fe9784ec9844b5184aa1b697b429.zip |
Merge pull request #3954 from gbasler/ticket/7746-2.11
SI-7746 fix unspecifc non-exhaustiveness warnings and non-determinism in pattern matcher (2.11)
Diffstat (limited to 'src')
4 files changed, 117 insertions, 53 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..e6ddf8b758 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 @@ -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)) 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..4330781013 100644 --- a/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala +++ b/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 |