diff options
| -rw-r--r-- | src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala | 951 | ||||
| -rw-r--r-- | src/compiler/scala/tools/nsc/util/Statistics.scala | 29 | ||||
| -rw-r--r-- | test/files/neg/patmatexhaust.check | 5 | ||||
| -rw-r--r-- | test/files/neg/virtpatmat_reach_null.check | 4 | ||||
| -rw-r--r-- | test/files/neg/virtpatmat_reach_null.flags | 1 | ||||
| -rw-r--r-- | test/files/neg/virtpatmat_reach_null.scala | 19 | ||||
| -rw-r--r-- | test/files/neg/virtpatmat_reach_sealed_unsealed.check | 14 | ||||
| -rw-r--r-- | test/files/neg/virtpatmat_reach_sealed_unsealed.flags | 1 | ||||
| -rw-r--r-- | test/files/neg/virtpatmat_reach_sealed_unsealed.scala | 21 | ||||
| -rw-r--r-- | test/files/pos/virtpatmat_reach_const.scala | 11 |
10 files changed, 807 insertions, 249 deletions
diff --git a/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala b/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala index 830e7db8ca..21b80df735 100644 --- a/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala +++ b/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala @@ -14,6 +14,7 @@ import scala.tools.nsc.transform.TypingTransformers import scala.tools.nsc.transform.Transform import scala.collection.mutable.HashSet import scala.collection.mutable.HashMap +import scala.tools.nsc.util.Statistics /** Translate pattern matching. * @@ -38,6 +39,8 @@ import scala.collection.mutable.HashMap * - recover exhaustivity and unreachability checking using a variation on the type-safe builder pattern */ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL { // self: Analyzer => + import Statistics._ + val global: Global // need to repeat here because otherwise last mixin defines global as // SymbolTable. If we had DOT this would not be an issue import global._ // the global environment @@ -182,6 +185,8 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL case _ => tp } + val start = startTimer(patmatNanos) + val selectorTp = repeatedToSeq(elimAnonymousClass(selector.tpe.widen.withoutAnnotations)) val origPt = match_.tpe @@ -205,7 +210,10 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL val selectorSym = freshSym(selector.pos, pureType(selectorTp)) setFlag SYNTH_CASE // pt = Any* occurs when compiling test/files/pos/annotDepMethType.scala with -Xexperimental - combineCases(selector, selectorSym, cases map translateCase(selectorSym, pt), pt, matchOwner, matchFailGenOverride) + val combined = combineCases(selector, selectorSym, cases map translateCase(selectorSym, pt), pt, matchOwner, matchFailGenOverride) + + stopTimer(patmatNanos, start) + combined } // return list of typed CaseDefs that are supported by the backend (typed/bind/wildcard) @@ -1328,11 +1336,11 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL // def andThen_: (prev: List[Test]): List[Test] = // prev.filterNot(this <:< _) :+ this - private val reusedBy = new collection.mutable.HashSet[Test] + // private val reusedBy = new collection.mutable.HashSet[Test] var reuses: Option[Test] = None def registerReuseBy(later: Test): Unit = { assert(later.reuses.isEmpty, later.reuses) - reusedBy += later + // reusedBy += later later.reuses = Some(this) } @@ -1427,9 +1435,16 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL // returns (tree, tests), where `tree` will be used to refer to `root` in `tests` - abstract class TreeMakersToConds(val root: Symbol, val cases: List[List[TreeMaker]]) { + abstract class TreeMakersToConds(val root: Symbol) { + def discard() = { + pointsToBound.clear() + trees.clear() + normalize = EmptySubstitution + accumSubst = EmptySubstitution + } // a variable in this set should never be replaced by a tree that "does not consist of a selection on a variable in this set" (intuitively) - private val pointsToBound = collection.mutable.HashSet(root) + private val pointsToBound = collection.mutable.HashSet(root) + private val trees = collection.mutable.HashSet.empty[Tree] // the substitution that renames variables to variables in pointsToBound private var normalize: Substitution = EmptySubstitution @@ -1462,7 +1477,6 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL // patmatDebug("accumSubst: "+ accumSubst) } - private val trees = new collection.mutable.HashSet[Tree] // TODO: improve, e.g., for constants def sameValue(a: Tree, b: Tree): Boolean = (a eq b) || ((a, b) match { @@ -1533,14 +1547,14 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL } } - final def approximateMatch(condMaker: CondMaker = makeCond): List[List[Test]] = cases.map { _ map (tm => Test(treeMakerToCond(tm, condMaker), tm)) } + final def approximateMatch(cases: List[List[TreeMaker]], condMaker: CondMaker = makeCond): List[List[Test]] = cases.map { _ map (tm => Test(treeMakerToCond(tm, condMaker), tm)) } - final def approximateMatchAgain(condMaker: CondMaker = makeCond): List[List[Test]] = cases.map { _ map (tm => Test(treeMakerToCondNoSubst(tm, condMaker), tm)) } + final def approximateMatchAgain(cases: List[List[TreeMaker]], condMaker: CondMaker = makeCond): List[List[Test]] = cases.map { _ map (tm => Test(treeMakerToCondNoSubst(tm, condMaker), tm)) } } def approximateMatch(root: Symbol, cases: List[List[TreeMaker]]): List[List[Test]] = { - object approximator extends TreeMakersToConds(root, cases) - approximator.approximateMatch() + object approximator extends TreeMakersToConds(root) + approximator.approximateMatch(cases) } def showTreeMakers(cases: List[List[TreeMaker]]) = { @@ -1585,18 +1599,36 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL class Prop case class Eq(p: Var, q: Const) extends Prop - type Const + type Const <: AbsConst + + trait AbsConst { + def implies(other: Const): Boolean + def excludes(other: Const): Boolean + } + type Var <: AbsVar trait AbsVar { - // if the domain is enumerable, at least one assignment must be true - def domainEnumerable: Boolean - def domain: Option[Set[Const]] + // indicate we may later require a prop for V = C + def registerEquality(c: Const): Unit + + // indicates null is part of the domain + def considerNull: Unit + + // compute the domain and return it (call considerNull first!) + def domainSyms: Option[Set[Sym]] // for this var, call it V, turn V = C into the equivalent proposition in boolean logic + // registerEquality(c) must have been called prior to this call + // in fact, all equalities relevant to this variable must have been registered def propForEqualsTo(c: Const): Prop - def equalitySyms: Set[Sym] +// // describe the equality axioms related to this variable being equal to this constant +// def impliedProp(c: Const): Prop + + // populated by registerEquality + // once equalitySyms has been called, registerEquality has no effect + def equalitySyms: List[Sym] } // would be nice to statically check whether a prop is equational or pure, @@ -1608,12 +1640,17 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL case object True extends Prop case object False extends Prop - private def nextSymId = {_symId += 1; _symId}; private var _symId = 0 - // symbols are propositions case class Sym(val variable: Var, val const: Const) extends Prop { - override val toString = variable +"="+ const +"#"+ nextSymId + private[this] val id = nextSymId + override def toString = variable +"="+ const +"#"+ id } + private def nextSymId = {_symId += 1; _symId}; private var _symId = 0 + + + @inline def /\(props: Iterable[Prop]) = if (props.isEmpty) True else props.reduceLeft(And(_, _)) + @inline def \/(props: Iterable[Prop]) = if (props.isEmpty) False else props.reduceLeft(Or(_, _)) + trait PropTraverser { def apply(x: Prop): Unit = x match { @@ -1627,6 +1664,14 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL def applyConst(x: Const): Unit = {} } + def gatherVariables(p: Prop): Set[Var] = { + val vars = new HashSet[Var]() + (new PropTraverser { + override def applyVar(v: Var) = vars += v + })(p) + vars.toSet + } + trait PropMap { def apply(x: Prop): Prop = x match { // TODO: mapConserve case And(a, b) => And(apply(a), apply(b)) @@ -1636,278 +1681,687 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL } } - // plan: (aka TODO) - // convert finite domain propositional logic to boolean propositional logic // for all c in C, there is a corresponding (meta-indexed) proposition Qv(c) that represents V = c, // the only property of equality that is encoded is that a variable can at most be equal to one of the c in C: // thus, for each distinct c, c', c'',... in C, a clause `not (Qv(c) /\ (Qv(c') \/ ... \/ Qv(c'')))` is added - def removeVarEq(prop: Prop): Prop = { + def removeVarEq(props: List[Prop], considerNull: Boolean = false): (Prop, List[Prop]) = { + val start = startTimer(patmatAnaVarEq) + val vars = new collection.mutable.HashSet[Var] - object dropEquational extends PropMap { + object gatherEqualities extends PropTraverser { override def apply(p: Prop) = p match { - case Eq(v, c) => vars += v; v.propForEqualsTo(c) + case Eq(v, c) => + vars += v + v.registerEquality(c) case _ => super.apply(p) } } - // dropEquational populates vars, and for each var in vars. var.equalitySyms - val pure = dropEquational(prop) + object rewriteEqualsToProp extends PropMap { + override def apply(p: Prop) = p match { + case Eq(v, c) => v.propForEqualsTo(c) + case _ => super.apply(p) + } + } + + props foreach gatherEqualities.apply + if (considerNull) vars foreach (_.considerNull) - // X = C is translated to P_X=C - // X = C' is translated to P_X=C' - // need to enforce X cannot simultaneously equal C and C' - // thus, all equality syms are mutually exclusive - // X = A, B, C, D --> Not(And(A, B)) /\ Not(And(A, C)) /\ Not(And(A, D)) - // /\ Not(And(B, C)) /\ Not(And(B, D)) - // /\ Not(And(C, D)) - // equivalently Or(Not(A), Not(B)) /\ Or(...) + val pure = props map rewriteEqualsToProp.apply var eqAxioms: Prop = True - def mutex(a: Sym)(b: Sym) = - eqAxioms = And(eqAxioms, Or(Not(a), Not(b))) + @inline def addAxiom(p: Prop) = eqAxioms = And(eqAxioms, p) - // at least one assignment from the domain must be true - def assigned(dom: Set[Sym]) = - eqAxioms = And(eqAxioms, dom.reduceLeft(Or)) + case class ExcludedPair(a: Const, b: Const) { + override def equals(o: Any) = o match { + case ExcludedPair(aa, bb) => (a == aa && b == bb) || (a == bb && b == aa) + case _ => false + } + } // patmatDebug("vars: "+ vars) vars.foreach { v => - // is the domain enumerable? then create equality syms for all elements in the domain and - // assert at least one of them must be selected - // if v.domain.isEmpty, we must consider the domain to be infinite - v.domain foreach { dom => - // get the Syms for the constants in the domain (making fresh ones for those not encountered in the formula) - val domProps = dom map {c => v.propForEqualsTo(c)} - val domSyms = new collection.mutable.HashSet[Sym]() - object collectSyms extends PropTraverser { - override def apply(p: Prop) = p match { - case domSym: Sym => domSyms += domSym - case _ => super.apply(p) - } + val excludedPair = new collection.mutable.HashSet[ExcludedPair] + + // if v.domainSyms.isEmpty, we must consider the domain to be infinite + // otherwise, since the domain fully partitions the type of the value, + // exactly one of the types (and whatever it implies, imposed separately) must be chosen + // consider X ::= A | B | C, and A => B + // coverage is formulated as: A \/ B \/ C and the implications are + v.domainSyms foreach { dsyms => addAxiom(\/(dsyms)) } + + val syms = v.equalitySyms + // patmatDebug("eqSyms "+(v, syms)) + syms foreach { sym => + // don't relate V = C to V = C -- `b.const == sym.const` + // if we've already excluded the pair at some point (-A \/ -B), then don't exclude the symmetric one (-B \/ -A) + // (nor the positive implications -B \/ A, or -A \/ B, which would entail the equality axioms falsifying the whole formula) + val todo = syms filterNot (b => (b.const == sym.const) || excludedPair(ExcludedPair(b.const, sym.const))) + val (excluded, notExcluded) = todo partition (b => sym.const.excludes(b.const)) + val implied = notExcluded filter (b => sym.const.implies(b.const)) + // patmatDebug("implications: "+ (sym.const, excluded, implied, syms)) + + // when this symbol is true, what must hold... + implied foreach (impliedSym => addAxiom(Or(Not(sym), impliedSym))) + + // ... and what must not? + excluded foreach {excludedSym => + excludedPair += ExcludedPair(sym.const, excludedSym.const) + addAxiom(Or(Not(sym), Not(excludedSym))) } - domProps foreach collectSyms.apply - - // TODO: an empty domain means involved type tests can never be true --> always non-exhaustive? - if (domSyms.nonEmpty) assigned(domSyms.toSet) - } - - // recover mutual-exclusivity (a variable can never be assigned two different constants) - var syms = v.equalitySyms.toList - while (syms.nonEmpty) { - syms.tail.foreach(mutex(syms.head)) - syms = syms.tail } } - // patmatDebug("eqAxioms:\n"+ cnfString(conjunctiveNormalForm(negationNormalForm(eqAxioms)))) - // patmatDebug("pure:\n"+ cnfString(conjunctiveNormalForm(negationNormalForm(pure)))) + // patmatDebug("eqAxioms:\n"+ cnfString(eqFreePropToSolvable(eqAxioms))) + // patmatDebug("pure:\n"+ cnfString(eqFreePropToSolvable(pure))) + + stopTimer(patmatAnaVarEq, start) - And(eqAxioms, pure) + (eqAxioms, pure) } - // convert propositional logic formula to CNF - // http://www.dcs.warwick.ac.uk/people/academic/Ranko.Lazic/fsv/fsv6.pdf - def negationNormalForm(p: Prop): Prop = p match { - case And(a, b) => And(negationNormalForm(a), negationNormalForm(b)) - case Or(a, b) => Or(negationNormalForm(a), negationNormalForm(b)) - case Not(And(a, b)) => negationNormalForm(Or(Not(a), Not(b))) - case Not(Or(a, b)) => negationNormalForm(And(Not(a), Not(b))) - case Not(Not(p)) => negationNormalForm(p) - case Not(True) => False - case Not(False) => True - case True - | False - | (_ : Sym) - | Not(_ : Sym) => p + + type Formula + def andFormula(a: Formula, b: Formula): Formula + + // may throw an IllegalArgumentException + def propToSolvable(p: Prop) = { + val (eqAxioms, pure :: Nil) = removeVarEq(List(p), considerNull = false) + eqFreePropToSolvable(And(eqAxioms, pure)) } + def eqFreePropToSolvable(p: Prop): Formula + def cnfString(f: Formula): String + + type Model = Map[Sym, Boolean] + val EmptyModel: Model + val NoModel: Model + + def findModelFor(f: Formula): Model + def findAllModelsFor(f: Formula): List[Model] + } + + trait CNF extends Logic { // CNF: a formula is a conjunction of clauses - type Formula = List[Clause] ; def formula(c: Clause*): Formula = c.toList + type Formula = Array[Clause] + def formula(c: Clause*): Formula = c.toArray + def andFormula(a: Formula, b: Formula): Formula = a ++ b // a clause is a disjunction of distinct literals - type Clause = Set[Lit] ; def clause(l: Lit*): Clause = l.toSet + type Clause = Set[Lit] + def clause(l: Lit*): Clause = l.toSet + @inline private def merge(a: Clause, b: Clause) = a ++ b + + type Lit + def Lit(sym: Sym, pos: Boolean = true): Lit + + // throws an IllegalArgumentException when the prop results in a CNF that's too big + def eqFreePropToSolvable(p: Prop): Formula = { + // TODO: for now, reusing the normalization from DPLL + def negationNormalForm(p: Prop): Prop = p match { + case And(a, b) => And(negationNormalForm(a), negationNormalForm(b)) + case Or(a, b) => Or(negationNormalForm(a), negationNormalForm(b)) + case Not(And(a, b)) => negationNormalForm(Or(Not(a), Not(b))) + case Not(Or(a, b)) => negationNormalForm(And(Not(a), Not(b))) + case Not(Not(p)) => negationNormalForm(p) + case Not(True) => False + case Not(False) => True + case True + | False + | (_ : Sym) + | Not(_ : Sym) => p + } + + val TrueF = formula() + val FalseF = formula(clause()) + def lit(s: Sym) = formula(clause(Lit(s))) + def negLit(s: Sym) = formula(clause(Lit(s, false))) + + def conjunctiveNormalForm(p: Prop, budget: Int = 256): Formula = { + def distribute(a: Formula, b: Formula, budget: Int): Formula = + if (budget <= 0) throw new IllegalArgumentException("CNF budget exceeded") + else + (a, b) match { + // true \/ _ = true + // _ \/ true = true + case (trueA, trueB) if trueA.size == 0 || trueB.size == 0 => TrueF + // lit \/ lit + case (a, b) if a.size == 1 && b.size == 1 => formula(merge(a(0), b(0))) + // (c1 /\ ... /\ cn) \/ d = ((c1 \/ d) /\ ... /\ (cn \/ d)) + // d \/ (c1 /\ ... /\ cn) = ((d \/ c1) /\ ... /\ (d \/ cn)) + case (cs, ds) => + val (big, small) = if (cs.size > ds.size) (cs, ds) else (ds, cs) + big flatMap (c => distribute(formula(c), small, budget - (big.size*small.size))) + } - // a literal is a (possibly negated) variable - case class Lit(sym: Sym, pos: Boolean = true) { - override def toString = if (!pos) "-"+ sym.toString else sym.toString - def unary_- = Lit(sym, !pos) + if (budget <= 0) throw new IllegalArgumentException("CNF budget exceeded") + + p match { + case True => TrueF + case False => FalseF + case s: Sym => lit(s) + case Not(s: Sym) => negLit(s) + case And(a, b) => + val cnfA = conjunctiveNormalForm(a, budget - 1) + val cnfB = conjunctiveNormalForm(b, budget - cnfA.size) + cnfA ++ cnfB + case Or(a, b) => + val cnfA = conjunctiveNormalForm(a) + val cnfB = conjunctiveNormalForm(b) + distribute(cnfA, cnfB, budget - (cnfA.size + cnfB.size)) + } + } + + val start = startTimer(patmatCNF) + val res = conjunctiveNormalForm(negationNormalForm(p)) + stopTimer(patmatCNF, start) + patmatCNFSizes(res.size) += 1 + +// patmatDebug("cnf for\n"+ p +"\nis:\n"+cnfString(res)) + res } - val TrueF = formula() - val FalseF = formula(clause()) - def lit(s: Sym) = formula(clause(Lit(s))) - def negLit(s: Sym) = formula(clause(Lit(s, false))) + } - def conjunctiveNormalForm(p: Prop): Formula = { - def distribute(a: Formula, b: Formula): Formula = (a, b) match { - // true \/ _ = true - case (TrueF, _) => TrueF - // _ \/ true = true - case (_, TrueF) => TrueF - // lit \/ lit - case (List(a), List(b)) => formula(a ++ b) - // (c1 /\ ... /\ cn) \/ d = ((c1 \/ d) /\ ... /\ (cn \/ d)) - case (cs, d) if cs.tail nonEmpty => cs flatMap (c => distribute(formula(c), d)) - // d \/ (c1 /\ ... /\ cn) = ((d \/ c1) /\ ... /\ (d \/ cn)) - case (d, cs) if cs.tail nonEmpty => cs flatMap (c => distribute(d, formula(c))) + trait DPLLSolver extends CNF { + // a literal is a (possibly negated) variable + def Lit(sym: Sym, pos: Boolean = true) = new Lit(sym, pos) + class Lit(val sym: Sym, val pos: Boolean) { + override def toString = if (!pos) "-"+ sym.toString else sym.toString + override def equals(o: Any) = o match { + case o: Lit => (o.sym == sym) && (o.pos == pos) + case _ => false } + override def hashCode = sym.hashCode + pos.hashCode - p match { - case True => TrueF - case False => FalseF - case s: Sym => lit(s) - case Not(s: Sym) => negLit(s) - case And(a, b) => conjunctiveNormalForm(a) ++ conjunctiveNormalForm(b) - case Or(a, b) => distribute(conjunctiveNormalForm(a), conjunctiveNormalForm(b)) - } + def unary_- = Lit(sym, !pos) } - def normalize(p: Prop) = conjunctiveNormalForm(negationNormalForm(removeVarEq(p))) 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) - type Model = Map[Sym, Boolean] +// type Model = Map[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 fullDPLL(f: Formula): List[Model] = { + def findAllModelsFor(f: Formula): List[Model] = { + val vars: Set[Sym] = f.flatMap(_ collect {case l: Lit => l.sym}).toSet + // patmatDebug("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 = 20): List[Model]= + def findAllModels(f: Formula, models: List[Model], recursionDepthAllowed: Int = 10): List[Model]= if (recursionDepthAllowed == 0) models else { - val (ok, model) = DPLL(f) + // patmatDebug("solving\n"+ cnfString(f)) + val model = findModelFor(f) // if we found a solution, conjunct the formula with the model's negation and recurse - if (ok) findAllModels(f :+ negateModel(model), model :: models, recursionDepthAllowed - 1) + if (model ne NoModel) { + val unassigned = (vars -- model.keySet).toList + // patmatDebug("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, true)) ++ force(Lit(s, false)) + } + // patmatDebug("forced "+ forced) + val negated = negateModel(model) + findAllModels(f :+ negated, model :: (forced ++ models), recursionDepthAllowed - 1) + } else models } findAllModels(f, Nil) } - def DPLL(f: Formula): (Boolean, Model) = { - @inline def withLit(res: (Boolean, Model), l: Lit) = (res._1, res._2 + (l.sym -> l.pos)) - @inline def orElse(a: (Boolean, Model), b: => (Boolean, Model)) = if (a._1) a else b + @inline private def withLit(res: Model, l: Lit): Model = if (res eq NoModel) NoModel else res + (l.sym -> l.pos) + @inline private def dropUnit(f: Formula, unitLit: Lit) = { + val negated = -unitLit + // drop entire clauses that are trivially true + // (i.e., disjunctions that contain the literal we're making true in the returned model), + // and simplify clauses by dropping the negation of the literal we're making true + // (since False \/ X == X) + f.filterNot(_.contains(unitLit)).map(_ - negated) + } + + def findModelFor(f: Formula): Model = { + @inline def orElse(a: Model, b: => Model) = if (a ne NoModel) a else b // patmatDebug("dpll\n"+ cnfString(f)) - if (f isEmpty) (true, EmptyModel) - else if(f exists (_.isEmpty)) (false, EmptyModel) - else f.find(_.size == 1) map { unitClause => - val unitLit = unitClause.head - // patmatDebug("unit: "+ unitLit) - val negated = -unitLit - // drop entire clauses that are trivially true - // (i.e., disjunctions that contain the literal we're making true in the returned model), - // and simplify clauses by dropping the negation of the literal we're making true - // (since False \/ X == X) - val simplified = f.filterNot(_.contains(unitLit)).map(_ - negated) - withLit(DPLL(simplified), unitLit) - } getOrElse { - // partition symbols according to whether they appear in positive and/or negative literals - val pos = new HashSet[Sym]() - val neg = new HashSet[Sym]() - f.foreach{_.foreach{ lit => - if (lit.pos) pos += lit.sym else neg += lit.sym - }} - // appearing in both positive and negative - val impures = pos intersect neg - // appearing only in either positive/negative positions - val pures = (pos ++ neg) -- impures - - if (pures nonEmpty) { - val pureSym = pures.head - // turn it back into a literal - // (since equality on literals is in terms of equality - // of the underlying symbol and its positivity, simply construct a new Lit) - val pureLit = Lit(pureSym, pos(pureSym)) - // patmatDebug("pure: "+ pureLit +" pures: "+ pures +" impures: "+ impures) - val simplified = f.filterNot(_.contains(pureLit)) - withLit(DPLL(simplified), pureLit) - } else { - val split = f.head.head - // patmatDebug("split: "+ split) - orElse(DPLL(f :+ clause(split)), DPLL(f :+ clause(-split))) + val start = startTimer(patmatAnaDPLL) + + val satisfiableWithModel: Model = + if (f isEmpty) EmptyModel + else if(f exists (_.isEmpty)) NoModel + else f.find(_.size == 1) match { + case Some(unitClause) => + val unitLit = unitClause.head + // patmatDebug("unit: "+ unitLit) + withLit(findModelFor(dropUnit(f, unitLit)), unitLit) + case _ => + // partition symbols according to whether they appear in positive and/or negative literals + val pos = new HashSet[Sym]() + val neg = new HashSet[Sym]() + f.foreach{_.foreach{ lit => + if (lit.pos) pos += lit.sym else neg += lit.sym + }} + // appearing in both positive and negative + val impures = pos intersect neg + // appearing only in either positive/negative positions + val pures = (pos ++ neg) -- impures + + if (pures nonEmpty) { + val pureSym = pures.head + // turn it back into a literal + // (since equality on literals is in terms of equality + // of the underlying symbol and its positivity, simply construct a new Lit) + val pureLit = Lit(pureSym, pos(pureSym)) + // patmatDebug("pure: "+ pureLit +" pures: "+ pures +" impures: "+ impures) + val simplified = f.filterNot(_.contains(pureLit)) + withLit(findModelFor(simplified), pureLit) + } else { + val split = f.head.head + // patmatDebug("split: "+ split) + orElse(findModelFor(f :+ clause(split)), findModelFor(f :+ clause(-split))) + } } - } + + stopTimer(patmatAnaDPLL, start) + + satisfiableWithModel } } + /** * Represent a match as a formula in propositional logic that encodes whether the match matches (abstractly: we only consider types) * */ trait SymbolicMatchAnalysis extends TreeMakerApproximation with Logic { self: CodegenCore => + def prepareNewAnalysis() = { Var.resetUniques(); Const.resetUniques() } + object Var { private var _nextId = 0 def nextId = {_nextId += 1; _nextId} + def resetUniques() = {_nextId = 0; uniques.clear()} private val uniques = new collection.mutable.HashMap[Tree, Var] def apply(x: Tree): Var = uniques getOrElseUpdate(x, new Var(x, x.tpe)) } class Var(val path: Tree, fullTp: Type, checked: Boolean = true) extends AbsVar { + private[this] val id: Int = Var.nextId + + // private[this] var canModify: Option[Array[StackTraceElement]] = None + @inline private[this] def ensureCanModify = {} //if (canModify.nonEmpty) patmatDebug("BUG!"+ this +" modified after having been observed: "+ canModify.get.mkString("\n")) + + @inline private[this] def observed = {} //canModify = Some(Thread.currentThread.getStackTrace) + + // don't access until all potential equalities have been registered using registerEquality + private[this] val symForEqualsTo = new collection.mutable.HashMap[Const, Sym] + // when looking at the domain, we only care about types we can check at run time val domainTp: Type = checkableType(fullTp) + private[this] var _considerNull = false + def considerNull: Unit = { ensureCanModify; if (NullTp <:< domainTp) _considerNull = true } + // case None => domain is unknown, // case Some(List(tps: _*)) => domain is exactly tps // 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) - val domain = if (checked) enumerateSubtypes(fullTp).map(_.map(Const).toSet) else None - - def describe = toString + ": "+ fullTp + domain.map(_.map(_.tp).mkString(" ::= ", " | ", "")).getOrElse(" ::= ??") +" // = "+ path - def domainEnumerable = domain.nonEmpty + lazy val domain: Option[Set[Const]] = + if (!checked) None + else { + val subConsts = enumerateSubtypes(fullTp).map{ tps => + tps.toSet[Type].map{ tp => + val domainC = TypeConst(tp) + registerEquality(domainC) + domainC + } + } - private val domMap = new collection.mutable.HashMap[Const, Sym] - private def symForEqualsTo(c: Const) = { - domMap getOrElseUpdate(c, { - // println("creating symbol for equality "+ this +" = "+ c) - Sym(this, c) - }) - } + val allConsts = + if (! _considerNull) subConsts + else { + registerEquality(NullConst) + subConsts map (_ + NullConst) + } - // for this var, call it V, turn V = C into the equivalent proposition in boolean logic - // over all executions of this method on the same Var object, - def propForEqualsTo(c: Const): Prop = { - domain match { - case None => symForEqualsTo(c) - case Some(domainConsts) => - val domainTps = domainConsts map (_.tp) - val checkedTp = c.tp - // find all the domain types that could make the type test true - // if the checked type is a supertype of the lub of the domain, - // we'll end up \/'ing the whole domain together, - // but must not simplify to True, as the type test may also fail... - val matches = domainTps.filter(_ <:< checkedTp).map{ tp => symForEqualsTo(Const(tp)) } - // println("type-equals-prop for "+ this +" = "+ c +": "+ (checkedTp, domainTp, domainTps) +" matches: "+ matches) - - if (matches isEmpty) False else matches.reduceLeft(Or) + observed; allConsts } - } - def equalitySyms: Set[Sym] = domMap.values.toSet + // accessing after calling considerNull will result in inconsistencies + lazy val domainSyms: Option[Set[Sym]] = domain map { _ map symForEqualsTo } - private[this] val id: Int = Var.nextId + + // populate equalitySyms + // don't care about the result, but want only one fresh symbol per distinct constant c + def registerEquality(c: Const): Unit = {ensureCanModify; symForEqualsTo getOrElseUpdate(c, Sym(this, c))} + + // don't access until all potential equalities have been registered using registerEquality + lazy val equalitySyms = {observed; symForEqualsTo.values.toList} + + // return the symbol that represents this variable being equal to the constant `c`, if it exists, otherwise False (for robustness) + // (registerEquality(c) must have been called prior, either when constructing the domain or from outside) + def propForEqualsTo(c: Const): Prop = {observed; symForEqualsTo.getOrElse(c, False)} + + + // don't call until all equalities have been registered and considerNull has been called (if needed) + def describe = toString + ": " + fullTp + domain.map(_.mkString(" ::= ", " | ", "// "+ symForEqualsTo.keys)).getOrElse(symForEqualsTo.keys.mkString(" ::= ", " | ", " | ...")) + " // = " + path override def toString = "V"+ id + + + + // when V = C, which other V = Ci are implied? + // V = null is an exclusive assignment, since null precludes any type test being true + // V = Any does not imply anything (except non-nullness) + // consider: + // when V's domain is closed, say V : X ::= A | B | C, and we have some value constants, say U and V, of type X: + // (x: X) match { case U => case V => case _ : X => } + // + // V's equalityConsts (for the above match): TC(X), TC(A), TC(B), TC(C), VC(U), VC(V) + // Set(TC(X), VC(U), VC(V)).forall(c => Set(TC(A), TC(B), TC(C)).forall(_.covers(c))) + // Set(VC(U), VC(V), TC(A), TC(B), TC(C)).forall(_.implies(TC(X)) + // impliedSuper for TC(X) is empty (since it's at the top of the lattice), + // but since we have a closed domain, we know that also one of the partitions must hold + // thus, TC(X) implies TC(A) \/ TC(B) \/ TC(C), + // we only need to add this implication when impliedSuper is empty, + // since that'll eventually be the case (transitive closure & acyclic graphs ftw) +// def impliedProp(c: Const): Prop = if (c eq NullConst) True else { +// val impliedSuper = /\((equalityConsts filter { other => (c != other) && c.implies(other) && !other.implies(c) } map symForEqualsTo)) +// +// val implied = +// if (impliedSuper == True) domain match { case None => True +// case Some(domCs) => \/(domCs filter { _.covers(c) } map symForEqualsTo) +// } else impliedSuper +// +// // patmatDebug("impliedProp: "+(this, c, impliedSuper, implied)) +// implied +// } +// private lazy val equalityConsts = symForEqualsTo.keySet } // all our variables range over types // a literal constant becomes ConstantType(Constant(v)) when the type allows it (roughly, anyval + string + null) // equality between variables: SingleType(x) (note that pattern variables cannot relate to each other -- it's always patternVar == nonPatternVar) - case class Const(tp: Type) { - override def toString = tp.toString + object Const { + def resetUniques() = {_nextTypeId = 0; _nextValueId = 0; uniques.clear()} // patmatDebug("RESET") + + private var _nextTypeId = 0 + def nextTypeId = {_nextTypeId += 1; _nextTypeId} + + private var _nextValueId = 0 + def nextValueId = {_nextValueId += 1; _nextValueId} + + private val uniques = new collection.mutable.HashMap[Type, Const] + private[SymbolicMatchAnalysis] def unique(tp: Type, mkFresh: => Const): Const = + uniques.get(tp).getOrElse( + uniques.find {case (oldTp, oldC) => oldTp =:= tp} match { + case Some((_, c)) => c + case _ => + val fresh = mkFresh + uniques(tp) = fresh + fresh + }) + } - def toValueString = tp match { - case ConstantType(c) => c.escapedStringValue - case _ => tp.toString + sealed abstract class Const extends AbsConst { + protected def tp: Type + protected def wideTp: Type + + def isAny = wideTp.typeSymbol == AnyClass + +// final def covers(other: Const): Boolean = { +// val r = (this, other) match { +// case (_: ValueConst, _: ValueConst) => this == other // hashconsed +// case (TypeConst(a) , _: ValueConst) => a <:< other.wideTp +// case (_ , _: TypeConst) => tp <:< other.tp +// case _ => false +// } +// // if(r) patmatDebug("covers : "+(this, other)) +// // else patmatDebug("NOT covers: "+(this, other)) +// r +// } + + final def implies(other: Const): Boolean = { + val r = (this, other) match { + case (_: ValueConst, _: ValueConst) => this == other // hashconsed + case (_: ValueConst, _: TypeConst) => tp <:< other.tp + case (_: TypeConst, _) => tp <:< other.tp + case _ => false + } + // if(r) patmatDebug("implies : "+(this, other)) + // else patmatDebug("NOT implies: "+(this, other)) + r + } + + // does V = C preclude V having value `other`? V = null is an exclusive assignment, + // but V = 1 does not preclude V = Int, or V = Any + final def excludes(other: Const): Boolean = { + val r = (this, other) match { + case (_, NullConst) => true + case (NullConst, _) => true + // this causes false negative for unreachability, but that's ok: + // example: val X = 1; val Y = 1; (2: Int) match { case X => case Y => /* considered reachable */ } + case (_: ValueConst, _: ValueConst) => this != other + case (_: ValueConst, _: TypeConst) => !((tp <:< other.tp) || (other.tp <:< wideTp)) + case (_: TypeConst, _: ValueConst) => !((other.tp <:< tp) || (tp <:< other.wideTp)) + case (_: TypeConst, _: TypeConst) => !((tp <:< other.tp) || (other.tp <:< tp)) + case _ => false + } + // if(r) patmatDebug("excludes : "+(this, other)) + // else patmatDebug("NOT excludes: "+(this, other)) + r + } + + // the equality symbol for V = C is looked up by C + final override def equals(other: Any): Boolean = other match { case o: Const => this eq o case _ => false } + } + + + object TypeConst { + def apply(tp: Type) = { + if (tp =:= NullTp) NullConst + else if (tp.isInstanceOf[SingletonType]) ValueConst.fromType(tp) + else Const.unique(tp, new TypeConst(tp)) + } + def unapply(c: TypeConst): Some[Type] = Some(c.tp) + } + + // corresponds to a type test that does not imply any value-equality (well, except for outer checks, which we don't model yet) + sealed class TypeConst(val tp: Type) extends Const { + assert(!(tp =:= NullTp)) + private[this] val id: Int = Const.nextTypeId + + val wideTp = tp.widen + + override def toString = tp.toString //+"#"+ id + } + + // p is a unique type or a constant value + object ValueConst { + def fromType(tp: Type) = { + assert(tp.isInstanceOf[SingletonType]) + val toString = tp match { + case ConstantType(c) => c.escapedStringValue + case _ => tp.toString + } + Const.unique(tp, new ValueConst(tp, tp.widen, toString)) + } + def apply(p: Tree) = { + val tp = p.tpe.normalize + if (tp =:= NullTp) NullConst + else { + val wideTp = { + if (p.hasSymbol && p.symbol.isStable) tp.asSeenFrom(tp.prefix, p.symbol.owner).widen + else tp.widen + } + + val narrowTp = + if (tp.isInstanceOf[SingletonType]) tp + else p match { + case Literal(c) => + if (c.tpe.typeSymbol == UnitClass) c.tpe + else ConstantType(c) + case p if p.symbol.isStable => + singleType(tp.prefix, p.symbol) + case x => + // TODO: better type + x.tpe.narrow + } + + val toString = + if (p.hasSymbol && p.symbol.isStable) p.symbol.name.toString // tp.toString + else p.toString //+"#"+ id + + Const.unique(narrowTp, new ValueConst(narrowTp, checkableType(wideTp), toString)) // must make wide type checkable so that it is comparable to types from TypeConst + } + } + } + sealed class ValueConst(val tp: Type, val wideTp: Type, override val toString: String) extends Const { + // patmatDebug("VC"+(tp, wideTp, toString)) + assert(!(tp =:= NullTp)) + private[this] val id: Int = Const.nextValueId + } + + lazy val NullTp = ConstantType(Constant(null)) + case object NullConst extends Const { + protected def tp = NullTp + protected def wideTp = NullTp + + def isValue = true + override def toString = "null" + } + + + // turns a case (represented as a list of abstract tests) + // into a proposition that is satisfiable if the case may match + def symbolicCase(tests: List[Test], modelNull: Boolean = false): Prop = { + def symbolic(t: Cond): Prop = t match { + case AndCond(a, b) => And(symbolic(a), symbolic(b)) + case OrCond(a, b) => Or(symbolic(a), symbolic(b)) + case Top => True + case Havoc => False + case TypeCond(p, pt) => Eq(Var(p), TypeConst(checkableType(pt))) + case EqualityCond(p, q) => Eq(Var(p), ValueConst(q)) + case NonNullCond(p) => if (!modelNull) True else Not(Eq(Var(p), NullConst)) + } + + val testsBeforeBody = tests.takeWhile(t => !t.treeMaker.isInstanceOf[BodyTreeMaker]) + /\(testsBeforeBody.map(t => symbolic(t.cond))) + } + + // 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 + // unreachability would also benefit from a more faithful representation + + // reachability (dead code) + + // computes the first 0-based case index that is unreachable (if any) + // a case is unreachable if it implies its preceding cases + // call C the formula that is satisfiable if the considered case matches + // call P the formula that is satisfiable if the cases preceding it match + // the case is reachable if there is a model for -P /\ C, + // thus, the case is unreachable if there is no model for -(-P /\ C), + // or, equivalently, P \/ -C, or C => P + def unreachableCase(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type): Option[Int] = { + // customize TreeMakersToConds (which turns a tree of tree makers into a more abstract DAG of tests) + // when approximating the current case (which we hope is reachable), be optimistic about the unknowns + object reachabilityApproximation extends TreeMakersToConds(prevBinder) { + def makeCondOptimistic(tm: TreeMaker)(recurse: TreeMaker => Cond): Cond = tm match { + // for unreachability, let's assume a guard always matches (unless we statically determined otherwise) + // otherwise, a guarded case would be considered unreachable + case GuardTreeMaker(guard) => + guard.tpe match { + case ConstantType(Constant(false)) => Havoc // not the best name; however, symbolically, 'Havoc' becomes 'False' + case _ => Top + } + // similar to a guard, user-defined extractors should not cause us to freak out + // if we're not 100% sure it does not match (i.e., its result type is None or Constant(false) -- TODO), + // let's stay optimistic and assume it does + case ExtractorTreeMaker(_, _, _, _) + | ProductExtractorTreeMaker(_, Some(_), _) => Top + // TODO: consider length-checks + case _ => + makeCond(tm)(recurse) + } + + // be pessimistic when approximating the prefix of the current case + // we hope the prefix fails so that we might get to the current case, which we hope is not dead + def makeCondPessimistic(tm: TreeMaker)(recurse: TreeMaker => Cond): Cond = makeCond(tm)(recurse) + } + + val start = startTimer(patmatAnaReach) + + // use the same approximator so we share variables, + // but need different conditions depending on whether we're conservatively looking for failure or success + val testCasesOk = reachabilityApproximation.approximateMatch(cases, reachabilityApproximation.makeCondOptimistic) + val testCasesFail = reachabilityApproximation.approximateMatchAgain(cases, reachabilityApproximation.makeCondPessimistic) + + reachabilityApproximation.discard() + prepareNewAnalysis() + + val propsCasesOk = testCasesOk map (t => symbolicCase(t, modelNull = true)) + val propsCasesFail = testCasesFail map (t => Not(symbolicCase(t, modelNull = true))) + val (eqAxiomsFail, symbolicCasesFail) = removeVarEq(propsCasesFail, considerNull = true) + val (eqAxiomsOk, symbolicCasesOk) = removeVarEq(propsCasesOk, considerNull = true) + + try { + // most of the time eqAxiomsFail == eqAxiomsOk, but the different approximations might cause different variables to disapper in general + val eqAxiomsCNF = + if (eqAxiomsFail == eqAxiomsOk) eqFreePropToSolvable(eqAxiomsFail) + else eqFreePropToSolvable(And(eqAxiomsFail, eqAxiomsOk)) + + var prefix = eqAxiomsCNF + var prefixRest = symbolicCasesFail + var current = symbolicCasesOk + var reachable = true + var caseIndex = 0 + + // patmatDebug("reachability, vars:\n"+ ((propsCasesFail flatMap gatherVariables) map (_.describe) mkString ("\n"))) + // patmatDebug("equality axioms:\n"+ cnfString(eqAxiomsCNF)) + + // 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 = andFormula(eqFreePropToSolvable(prefHead), prefix) + current = current.tail + val model = findModelFor(andFormula(eqFreePropToSolvable(current.head), prefix)) + + // patmatDebug("trying to reach:\n"+ cnfString(current.head) +"\nunder prefix:\n"+ cnfString(prefix)) + // if (ok) patmatDebug("reached: "+ modelString(model)) + + reachable = model ne NoModel + } + } + + stopTimer(patmatAnaReach, start) + + if (reachable) None else Some(caseIndex) + } catch { + case e : IllegalArgumentException => +// patmatDebug(util.Position.formatMessage(prevBinder.pos, "Cannot check match for reachability", false)) +// e.printStackTrace() + None // CNF budget exceeded } } + // exhaustivity + // make sure it's not a primitive, else (5: Byte) match { case 5 => ... } sees no Byte // TODO: domain of feasibly enumerable built-in types (enums, char?) def enumerateSubtypes(tp: Type): Option[List[Type]] = @@ -1945,12 +2399,6 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL Some(validSubTypes) } - def narrowTypeOf(p: Tree) = p match { - case Literal(c) => ConstantType(c) - case Ident(_) if p.symbol.isStable => singleType(p.tpe.prefix, p.symbol) - case x => x.tpe.narrow - } - // approximate a type to the static type that is fully checkable at run time, // hiding statically known but dynamically uncheckable information using existential quantification // TODO: this is subject to the availability of TypeTags (since an abstract type with a type tag is checkable at run time) @@ -1989,8 +2437,9 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL // - back off (to avoid crying exhaustive too often) when: // - there are guards --> // - there are extractor calls (that we can't secretly/soundly) rewrite + val start = startTimer(patmatAnaExhaust) var backoff = false - object exhaustivityApproximation extends TreeMakersToConds(prevBinder, cases) { + object exhaustivityApproximation extends TreeMakersToConds(prevBinder) { def makeCondExhaustivity(tm: TreeMaker)(recurse: TreeMaker => Cond): Cond = tm match { case p @ ExtractorTreeMaker(extractor, Some(lenCheck), testedBinder, _) => p.checkedLength match { @@ -2020,27 +2469,16 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL } } - def symbolic(t: Cond): Prop = t match { - case AndCond(a, b) => And(symbolic(a), symbolic(b)) - case OrCond(a, b) => Or(symbolic(a), symbolic(b)) - case Top => True - case Havoc => False - case TypeCond(p, pt) => Eq(Var(p), Const(checkableType(pt))) - case EqualityCond(p, q) => Eq(Var(p), Const(narrowTypeOf(q))) - case NonNullCond(p) => True // ignoring nullness because it generates too much noise Not(Eq(Var(p), Const(NullClass.tpe))) - } + val tests = exhaustivityApproximation.approximateMatch(cases, exhaustivityApproximation.makeCondExhaustivity) - def symbolicCase(tests: List[Test]) = { - val testsBeforeBody = tests.takeWhile(t => !t.treeMaker.isInstanceOf[BodyTreeMaker]) - testsBeforeBody.map(t => symbolic(t.cond)).foldLeft(True: Prop)(And) - } + if (backoff) Nil else { + val prevBinderTree = exhaustivityApproximation.binderToUniqueTree(prevBinder) - val tests = exhaustivityApproximation.approximateMatch(exhaustivityApproximation.makeCondExhaustivity) + exhaustivityApproximation.discard() + prepareNewAnalysis() - if (backoff) Nil else { - val symbolicCases = tests map symbolicCase + val symbolicCases = tests map (symbolicCase(_, modelNull = false)) - val prevBinderTree = exhaustivityApproximation.binderToUniqueTree(prevBinder) // TODO: null tests generate too much noise, so disabled them -- is there any way to bring them back? // assuming we're matching on a non-null scrutinee (prevBinder), when does the match fail? @@ -2053,8 +2491,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL // val matchFails = And(symbolic(nonNullScrutineeCond), Not(symbolicCases reduceLeft (Or(_, _)))) // when does the match fail? - val matchFails = Not(symbolicCases reduceLeft (Or(_, _))) - + val matchFails = Not(\/(symbolicCases)) // debug output: // patmatDebug("analysing:") @@ -2064,15 +2501,25 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL // val vars = gatherVariables(matchFails) // patmatDebug("\nvars:\n"+ (vars map (_.describe) mkString ("\n"))) // - // patmatDebug("\nmatchFails as CNF:\n"+ cnfString(normalize(matchFails))) + // patmatDebug("\nmatchFails as CNF:\n"+ cnfString(propToSolvable(matchFails))) + + try { + // find the models (under which the match fails) + val matchFailModels = findAllModelsFor(propToSolvable(matchFails)) - // find the models (under which the match fails) - val matchFailModels = fullDPLL(normalize(matchFails)) + val scrutVar = Var(prevBinderTree) + val counterExamples = matchFailModels.map(modelToCounterExample(scrutVar)) - val scrutVar = Var(prevBinderTree) - val counterExamples = matchFailModels.map(modelToCounterExample(scrutVar)) + val pruned = CounterExample.prune(counterExamples).map(_.toString).sorted - CounterExample.prune(counterExamples).map(_.toString).sorted + stopTimer(patmatAnaExhaust, start) + pruned + } catch { + case e : IllegalArgumentException => + // patmatDebug(util.Position.formatMessage(prevBinder.pos, "Cannot check match for exhaustivity", false)) + // e.printStackTrace() + Nil // CNF budget exceeded + } } } @@ -2088,13 +2535,13 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL protected[SymbolicMatchAnalysis] def flattenConsArgs: List[CounterExample] = Nil def coveredBy(other: CounterExample): Boolean = this == other || other == WildcardExample } - case class ValueExample(c: Const) extends CounterExample { override def toString = c.toValueString } + case class ValueExample(c: ValueConst) extends CounterExample { override def toString = c.toString } case class TypeExample(c: Const) extends CounterExample { override def toString = "(_ : "+ c +")" } case class NegativeExample(nonTrivialNonEqualTo: List[Const]) extends CounterExample { override def toString = { val negation = - if (nonTrivialNonEqualTo.tail.isEmpty) nonTrivialNonEqualTo.head.toValueString - else nonTrivialNonEqualTo.map(_.toValueString).sorted.mkString("in (", ", ", ")") + if (nonTrivialNonEqualTo.tail.isEmpty) nonTrivialNonEqualTo.head.toString + else nonTrivialNonEqualTo.map(_.toString).sorted.mkString("in (", ", ", ")") "<not "+ negation +">" } } @@ -2131,6 +2578,21 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL case object WildcardExample extends CounterExample { override def toString = "_" } case object NoExample extends CounterExample { override def toString = "??" } + @inline 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) + (trues map (_._1.const), falses map (_._1.const)) + // should never be more than one value in trues... + } + + def varAssignmentString(varAssignment: Map[Var, (Seq[Const], Seq[Const])]) = + varAssignment.toSeq.sortBy(_._1.toString).map { case (v, (trues, falses)) => + val assignment = "== "+ (trues mkString("(", ", ", ")")) +" != ("+ (falses mkString(", ")) +")" + v +"(="+ v.path +": "+ v.domainTp +") "+ assignment + }.mkString("\n") + + def modelString(model: Model) = varAssignmentString(modelToVarAssignment(model)) + // 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(_ :: _, _ :: _), @@ -2141,18 +2603,9 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL // x1.tl = ... // x1.hd.hd = ... // ... - val varAssignment = model.toSeq.groupBy{f => f match {case (sym, value) => sym.variable} }.mapValues{ xs => - val (trues, falses) = xs.partition(_._2) - (trues map (_._1.const), falses map (_._1.const)) - // should never be more than one value in trues... - } - - // patmatDebug("var assignment for model "+ model +":\n"+ - // varAssignment.toSeq.sortBy(_._1.toString).map { case (v, (trues, falses)) => - // val assignment = "== "+ (trues mkString("(", ", ", ")")) +" != ("+ (falses mkString(", ")) +")" - // v +"(="+ v.path +": "+ v.domainTp +") "+ assignment - // }.mkString("\n")) + val varAssignment = modelToVarAssignment(model) + // patmatDebug("var assignment for model "+ model +":\n"+ varAssignmentString(varAssignment)) // chop a path into a list of symbols def chop(path: Tree): List[Symbol] = path match { @@ -2198,7 +2651,9 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL // node in the tree that describes how to construct a counter-example case class VariableAssignment(variable: Var, equalTo: List[Const], notEqualTo: List[Const], fields: collection.mutable.Map[Symbol, VariableAssignment]) { - private lazy val ctor = (equalTo match { case List(Const(tp)) => tp case _ => variable.domainTp }).typeSymbol.primaryConstructor + // need to prune since the model now incorporates all super types of a constant (needed for reachability) + private lazy val prunedEqualTo = equalTo filterNot (subsumed => equalTo.exists(better => (better ne subsumed) && (better implies subsumed))) + private lazy val ctor = (prunedEqualTo match { case List(TypeConst(tp)) => tp case _ => variable.domainTp }).typeSymbol.primaryConstructor private lazy val ctorParams = if (ctor == NoSymbol || ctor.paramss.isEmpty) Nil else ctor.paramss.head private lazy val cls = if (ctor == NoSymbol) NoSymbol else ctor.owner private lazy val caseFieldAccs = if (cls == NoSymbol) Nil else cls.caseFieldAccessors @@ -2207,7 +2662,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL def allFieldAssignmentsLegal: Boolean = (fields.keySet subsetOf caseFieldAccs.toSet) && fields.values.forall(_.allFieldAssignmentsLegal) - private lazy val nonTrivialNonEqualTo = notEqualTo.filterNot{c => val sym = c.tp.typeSymbol; sym == AnyClass } // sym == NullClass || + private lazy val nonTrivialNonEqualTo = notEqualTo.filterNot{c => c.isAny } // NoExample if the constructor call is ill-typed // (thus statically impossible -- can we incorporate this into the formula?) @@ -2215,17 +2670,17 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL def toCounterExample(beBrief: Boolean = false): CounterExample = if (!allFieldAssignmentsLegal) NoExample else { -// println("describing "+ (variable, equalTo, notEqualTo, fields, cls, allFieldAssignmentsLegal)) - val res = equalTo match { + // patmatDebug("describing "+ (variable, equalTo, notEqualTo, fields, cls, allFieldAssignmentsLegal)) + val res = prunedEqualTo match { // a definite assignment to a value - case List(eq@Const(_: ConstantType)) if fields.isEmpty => ValueExample(eq) + case List(eq: ValueConst) if fields.isEmpty => ValueExample(eq) // constructor call // or we did not gather any information about equality but we have information about the fields // --> typical example is when the scrutinee is a tuple and all the cases first unwrap that tuple and only then test something interesting case _ if cls != NoSymbol && - ( equalTo.nonEmpty - || (fields.nonEmpty && !isPrimitiveValueClass(cls) && equalTo.isEmpty && notEqualTo.isEmpty)) => + ( prunedEqualTo.nonEmpty + || (fields.nonEmpty && !isPrimitiveValueClass(cls) && prunedEqualTo.isEmpty && notEqualTo.isEmpty)) => @inline def args(brevity: Boolean = beBrief) = { // figure out the constructor arguments from the field assignment @@ -2252,7 +2707,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL // TODO: improve reasoning -- in the mean time, a false negative is better than an annoying false positive case _ => NoExample } -// patmatDebug("described as: "+ res) + // patmatDebug("described as: "+ res) res } @@ -2715,8 +3170,14 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL with DeadCodeElimination with SwitchEmission with OptimizedCodegen - with SymbolicMatchAnalysis { self: TreeMakers => + with SymbolicMatchAnalysis + with DPLLSolver { self: TreeMakers => override def optimizeCases(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type, unchecked: Boolean): (List[List[TreeMaker]], List[Tree]) = { + if (!unchecked) { + unreachableCase(prevBinder, cases, pt) foreach { caseIndex => + typer.context.unit.warning(cases(caseIndex).last.pos, "unreachable code") + } + } val counterExamples = if (unchecked) Nil else exhaustive(prevBinder, cases, pt) if (counterExamples.nonEmpty) { val ceString = diff --git a/src/compiler/scala/tools/nsc/util/Statistics.scala b/src/compiler/scala/tools/nsc/util/Statistics.scala index 61c7695911..53ab6654ee 100644 --- a/src/compiler/scala/tools/nsc/util/Statistics.scala +++ b/src/compiler/scala/tools/nsc/util/Statistics.scala @@ -60,6 +60,14 @@ class Statistics extends scala.reflect.internal.util.Statistics { val macroExpandCount = new Counter val macroExpandNanos = new Timer + + val patmatNanos = new Timer + val patmatAnaDPLL = new Timer + val patmatAnaVarEq = new Timer + val patmatCNF = new Timer + val patmatAnaExhaust = new Timer + val patmatAnaReach = new Timer + val patmatCNFSizes = new collection.mutable.HashMap[Int, Int] withDefaultValue 0 } object Statistics extends Statistics @@ -71,7 +79,7 @@ abstract class StatisticsInfo { val global: Global import global._ - var phasesShown = List("parser", "typer", "erasure", "cleanup") + var phasesShown = List("parser", "typer", "patmat", "erasure", "cleanup") def countNodes(tree: Tree, counts: ClassCounts) { for (t <- tree) counts(t.getClass) += 1 @@ -83,10 +91,15 @@ abstract class StatisticsInfo { def showRelTyper(timer: Timer) = timer+showPercent(timer.nanos, typerNanos.nanos) - def showCounts(counts: ClassCounts) = + def showRelPatmat(timer: Timer) = + timer+showPercent(timer.nanos, patmatNanos.nanos) + + def showCounts[T](counts: scala.collection.mutable.Map[T, Int]) = counts.toSeq.sortWith(_._2 > _._2).map { - case (cls, cnt) => + case (cls: Class[_], cnt) => cls.toString.substring(cls.toString.lastIndexOf("$") + 1)+": "+cnt + case (o, cnt) => + o.toString +": "+cnt } def print(phase: Phase) = if (phasesShown contains phase.name) { @@ -169,6 +182,16 @@ abstract class StatisticsInfo { if (timer1 != null) inform("#timer1 : " + timer1) if (timer2 != null) inform("#timer2 : " + timer2) //for (t <- uniques.iterator) println("unique: "+t) + + if (phase.name == "patmat") { + inform("time spent in patmat : " + patmatNanos ) + inform(" of which DPLL : " + showRelPatmat(patmatAnaDPLL )) + inform("of which in CNF conversion : " + showRelPatmat(patmatCNF )) + inform(" CNF size counts : " + showCounts(patmatCNFSizes )) + inform("of which variable equality : " + showRelPatmat(patmatAnaVarEq )) + inform(" of which in exhaustivity : " + showRelPatmat(patmatAnaExhaust)) + inform("of which in unreachability : " + showRelPatmat(patmatAnaReach )) + } } } } diff --git a/test/files/neg/patmatexhaust.check b/test/files/neg/patmatexhaust.check index 1168f36e11..4556e6622f 100644 --- a/test/files/neg/patmatexhaust.check +++ b/test/files/neg/patmatexhaust.check @@ -14,6 +14,9 @@ patmatexhaust.scala:49: error: match may not be exhaustive. It would fail on the following inputs: Gp(), Gu def ma4(x:Deep) = x match { // missing cases: Gu, Gp ^ +patmatexhaust.scala:55: error: unreachable code + case _ if 1 == 0 => + ^ patmatexhaust.scala:53: error: match may not be exhaustive. It would fail on the following input: Gp() def ma5(x:Deep) = x match { @@ -34,4 +37,4 @@ patmatexhaust.scala:126: error: match may not be exhaustive. It would fail on the following input: C1() def ma10(x: C) = x match { // not exhaustive: C1 is not abstract. ^ -9 errors found +10 errors found diff --git a/test/files/neg/virtpatmat_reach_null.check b/test/files/neg/virtpatmat_reach_null.check new file mode 100644 index 0000000000..595c8ec889 --- /dev/null +++ b/test/files/neg/virtpatmat_reach_null.check @@ -0,0 +1,4 @@ +virtpatmat_reach_null.scala:13: error: unreachable code + case _ => // unreachable + ^ +one error found diff --git a/test/files/neg/virtpatmat_reach_null.flags b/test/files/neg/virtpatmat_reach_null.flags new file mode 100644 index 0000000000..e8fb65d50c --- /dev/null +++ b/test/files/neg/virtpatmat_reach_null.flags @@ -0,0 +1 @@ +-Xfatal-warnings
\ No newline at end of file diff --git a/test/files/neg/virtpatmat_reach_null.scala b/test/files/neg/virtpatmat_reach_null.scala new file mode 100644 index 0000000000..6314a5b1d8 --- /dev/null +++ b/test/files/neg/virtpatmat_reach_null.scala @@ -0,0 +1,19 @@ +sealed abstract class Const { + final def excludes(other: Const) = + (this, other) match { + case (_, NullConst) => + case (NullConst, _) => + case (_: ValueConst, _: ValueConst) => + case (_: ValueConst, _: TypeConst) => + case (_: TypeConst, _: ValueConst) => + case (_: TypeConst, _: TypeConst) => + case (null, _) => + case (_, null) => + case null => + case _ => // unreachable + } +} + +sealed class TypeConst extends Const +sealed class ValueConst extends Const +case object NullConst extends Const diff --git a/test/files/neg/virtpatmat_reach_sealed_unsealed.check b/test/files/neg/virtpatmat_reach_sealed_unsealed.check new file mode 100644 index 0000000000..10638eff52 --- /dev/null +++ b/test/files/neg/virtpatmat_reach_sealed_unsealed.check @@ -0,0 +1,14 @@ +virtpatmat_reach_sealed_unsealed.scala:16: error: match may not be exhaustive. +It would fail on the following input: false + (true: Boolean) match { case true => } // not exhaustive, but reachable + ^ +virtpatmat_reach_sealed_unsealed.scala:18: error: unreachable code + (true: Boolean) match { case true => case false => case _ => } // exhaustive, last case is unreachable + ^ +virtpatmat_reach_sealed_unsealed.scala:19: error: unreachable code + (true: Boolean) match { case true => case false => case _: Boolean => } // exhaustive, last case is unreachable + ^ +virtpatmat_reach_sealed_unsealed.scala:20: error: unreachable code + (true: Boolean) match { case true => case false => case _: Any => } // exhaustive, last case is unreachable + ^ +four errors found diff --git a/test/files/neg/virtpatmat_reach_sealed_unsealed.flags b/test/files/neg/virtpatmat_reach_sealed_unsealed.flags new file mode 100644 index 0000000000..e8fb65d50c --- /dev/null +++ b/test/files/neg/virtpatmat_reach_sealed_unsealed.flags @@ -0,0 +1 @@ +-Xfatal-warnings
\ No newline at end of file diff --git a/test/files/neg/virtpatmat_reach_sealed_unsealed.scala b/test/files/neg/virtpatmat_reach_sealed_unsealed.scala new file mode 100644 index 0000000000..13911dbd78 --- /dev/null +++ b/test/files/neg/virtpatmat_reach_sealed_unsealed.scala @@ -0,0 +1,21 @@ +sealed abstract class X +sealed case class A(x: Int) extends X + +// test reachability on mixed sealed / non-sealed matches +object Test extends App { + val B: X = A(0) + val C: X = A(1) + + // all cases are reachable and the match is exhaustive + (C: X) match { + case B => + case C => + case A(_) => + } + + (true: Boolean) match { case true => } // not exhaustive, but reachable + (true: Boolean) match { case true => case false => } // exhaustive, reachable + (true: Boolean) match { case true => case false => case _ => } // exhaustive, last case is unreachable + (true: Boolean) match { case true => case false => case _: Boolean => } // exhaustive, last case is unreachable + (true: Boolean) match { case true => case false => case _: Any => } // exhaustive, last case is unreachable +}
\ No newline at end of file diff --git a/test/files/pos/virtpatmat_reach_const.scala b/test/files/pos/virtpatmat_reach_const.scala new file mode 100644 index 0000000000..b55b7cb229 --- /dev/null +++ b/test/files/pos/virtpatmat_reach_const.scala @@ -0,0 +1,11 @@ +// check the interaction between constants and type tests in creating the equality axioms +object Test { + type Formula = List[String] + val TrueF: Formula = List() + def distribute(a: Formula, b: Formula) = (a, b) match { + case (TrueF, _) => + case (_, TrueF) => // bug: considered unreachable + case (a :: Nil, b :: Nil) => + case _ => + } +}
\ No newline at end of file |