From 0a3219b90e1611d074abe935c5f05dab097e116d Mon Sep 17 00:00:00 2001 From: Adriaan Moors Date: Fri, 22 Feb 2013 16:45:45 -0800 Subject: move sat solving to separate file --- .../scala/tools/nsc/transform/patmat/Logic.scala | 232 -------------------- .../nsc/transform/patmat/PatternMatching.scala | 2 +- .../scala/tools/nsc/transform/patmat/Solving.scala | 242 +++++++++++++++++++++ 3 files changed, 243 insertions(+), 233 deletions(-) create mode 100644 src/compiler/scala/tools/nsc/transform/patmat/Solving.scala diff --git a/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala b/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala index a726a230ac..22eabb6d6f 100644 --- a/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala +++ b/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala @@ -289,238 +289,6 @@ trait Logic extends Debugging { } } -// naive CNF translation and simple DPLL solver -trait SimpleSolver extends Logic { - import PatternMatchingStats._ - trait CNF extends PropositionalLogic { - - /** Override Array creation for efficiency (to not go through reflection). */ - private implicit val clauseTag: scala.reflect.ClassTag[Clause] = new scala.reflect.ClassTag[Clause] { - def runtimeClass: java.lang.Class[Clause] = classOf[Clause] - final override def newArray(len: Int): Array[Clause] = new Array[Clause](len) - } - - import scala.collection.mutable.ArrayBuffer - type FormulaBuilder = ArrayBuffer[Clause] - def formulaBuilder = ArrayBuffer[Clause]() - def formulaBuilderSized(init: Int) = new ArrayBuffer[Clause](init) - def addFormula(buff: FormulaBuilder, f: Formula): Unit = buff ++= f - def toFormula(buff: FormulaBuilder): Formula = buff - - // CNF: a formula is a conjunction of clauses - type Formula = FormulaBuilder - def formula(c: Clause*): Formula = ArrayBuffer(c: _*) - - type Clause = Set[Lit] - // a clause is a disjunction of distinct literals - def clause(l: Lit*): Clause = l.toSet - - type Lit - def Lit(sym: Sym, pos: Boolean = true): Lit - - def andFormula(a: Formula, b: Formula): Formula = a ++ b - def simplifyFormula(a: Formula): Formula = a.distinct - - private def merge(a: Clause, b: Clause) = a ++ b - - // throws an AnalysisBudget.Exception when the prop results in a CNF that's too big - // TODO: be smarter/more efficient about this (http://lara.epfl.ch/w/sav09:tseitin_s_encoding) - def eqFreePropToSolvable(p: Prop): Formula = { - def negationNormalFormNot(p: Prop, budget: Int): Prop = - if (budget <= 0) throw AnalysisBudget.exceeded - else p match { - case And(a, b) => Or(negationNormalFormNot(a, budget - 1), negationNormalFormNot(b, budget - 1)) - case Or(a, b) => And(negationNormalFormNot(a, budget - 1), negationNormalFormNot(b, budget - 1)) - case Not(p) => negationNormalForm(p, budget - 1) - case True => False - case False => True - case s: Sym => Not(s) - } - - def negationNormalForm(p: Prop, budget: Int = AnalysisBudget.max): Prop = - if (budget <= 0) throw AnalysisBudget.exceeded - else p match { - case And(a, b) => And(negationNormalForm(a, budget - 1), negationNormalForm(b, budget - 1)) - case Or(a, b) => Or(negationNormalForm(a, budget - 1), negationNormalForm(b, budget - 1)) - case Not(negated) => negationNormalFormNot(negated, budget - 1) - case True - | False - | (_ : 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 = AnalysisBudget.max): Formula = { - def distribute(a: Formula, b: Formula, budget: Int): Formula = - if (budget <= 0) throw AnalysisBudget.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))) - } - - if (budget <= 0) throw AnalysisBudget.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 = if (Statistics.canEnable) Statistics.startTimer(patmatCNF) else null - val res = conjunctiveNormalForm(negationNormalForm(p)) - - 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)) - res - } - } - - // simple solver using DPLL - trait Solver 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 eq sym) && (o.pos == pos) - case _ => false - } - override def hashCode = sym.hashCode + pos.hashCode - - def unary_- = Lit(sym, !pos) - } - - 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 = 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] = { - 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)) - 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, true)) ++ force(Lit(s, false)) - } - debug.patmat("forced "+ forced) - val negated = negateModel(model) - findAllModels(f :+ negated, model :: (forced ++ models), recursionDepthAllowed - 1) - } - else models - } - - findAllModels(f, Nil) - } - - private def withLit(res: Model, l: Lit): Model = if (res eq NoModel) NoModel else res + (l.sym -> l.pos) - private def dropUnit(f: Formula, unitLit: Lit): Formula = { - 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 dropped = formulaBuilderSized(f.size) - for { - clause <- f - if !(clause contains unitLit) - } dropped += (clause - negated) - dropped - } - - def findModelFor(f: Formula): Model = { - @inline def orElse(a: Model, b: => Model) = if (a ne NoModel) a else b - - debug.patmat("DPLL\n"+ cnfString(f)) - - val start = if (Statistics.canEnable) Statistics.startTimer(patmatAnaDPLL) else null - - 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 - // debug.patmat("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 mutable.HashSet[Sym]() - val neg = new mutable.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)) - // debug.patmat("pure: "+ pureLit +" pures: "+ pures +" impures: "+ impures) - val simplified = f.filterNot(_.contains(pureLit)) - withLit(findModelFor(simplified), pureLit) - } else { - val split = f.head.head - // debug.patmat("split: "+ split) - orElse(findModelFor(f :+ clause(split)), findModelFor(f :+ clause(-split))) - } - } - - if (Statistics.canEnable) Statistics.stopTimer(patmatAnaDPLL, start) - - satisfiableWithModel - } - } -} - trait ScalaLogic extends Interface with Logic with TreeAndTypeAnalysis { trait TreesAndTypesDomain extends PropositionalLogic with CheckableTreeAndTypeAnalysis { type Type = global.Type diff --git a/src/compiler/scala/tools/nsc/transform/patmat/PatternMatching.scala b/src/compiler/scala/tools/nsc/transform/patmat/PatternMatching.scala index 946b0b0714..6d6774cf20 100644 --- a/src/compiler/scala/tools/nsc/transform/patmat/PatternMatching.scala +++ b/src/compiler/scala/tools/nsc/transform/patmat/PatternMatching.scala @@ -41,7 +41,7 @@ trait PatternMatching extends Transform with TypingTransformers with MatchTreeMaking with MatchCodeGen with ScalaLogic - with SimpleSolver + with Solving with MatchAnalysis with MatchOptimization { import global._ diff --git a/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala b/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala new file mode 100644 index 0000000000..843f831ea1 --- /dev/null +++ b/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala @@ -0,0 +1,242 @@ +/* NSC -- new Scala compiler + * + * Copyright 2011-2013 LAMP/EPFL + * @author Adriaan Moors + */ + +package scala.tools.nsc.transform.patmat + +import scala.collection.mutable +import scala.reflect.internal.util.Statistics + +// naive CNF translation and simple DPLL solver +trait Solving extends Logic { + import PatternMatchingStats._ + trait CNF extends PropositionalLogic { + + /** Override Array creation for efficiency (to not go through reflection). */ + private implicit val clauseTag: scala.reflect.ClassTag[Clause] = new scala.reflect.ClassTag[Clause] { + def runtimeClass: java.lang.Class[Clause] = classOf[Clause] + final override def newArray(len: Int): Array[Clause] = new Array[Clause](len) + } + + import scala.collection.mutable.ArrayBuffer + type FormulaBuilder = ArrayBuffer[Clause] + def formulaBuilder = ArrayBuffer[Clause]() + def formulaBuilderSized(init: Int) = new ArrayBuffer[Clause](init) + def addFormula(buff: FormulaBuilder, f: Formula): Unit = buff ++= f + def toFormula(buff: FormulaBuilder): Formula = buff + + // CNF: a formula is a conjunction of clauses + type Formula = FormulaBuilder + def formula(c: Clause*): Formula = ArrayBuffer(c: _*) + + type Clause = Set[Lit] + // a clause is a disjunction of distinct literals + def clause(l: Lit*): Clause = l.toSet + + type Lit + def Lit(sym: Sym, pos: Boolean = true): Lit + + def andFormula(a: Formula, b: Formula): Formula = a ++ b + def simplifyFormula(a: Formula): Formula = a.distinct + + private def merge(a: Clause, b: Clause) = a ++ b + + // throws an AnalysisBudget.Exception when the prop results in a CNF that's too big + // TODO: be smarter/more efficient about this (http://lara.epfl.ch/w/sav09:tseitin_s_encoding) + def eqFreePropToSolvable(p: Prop): Formula = { + def negationNormalFormNot(p: Prop, budget: Int): Prop = + if (budget <= 0) throw AnalysisBudget.exceeded + else p match { + case And(a, b) => Or(negationNormalFormNot(a, budget - 1), negationNormalFormNot(b, budget - 1)) + case Or(a, b) => And(negationNormalFormNot(a, budget - 1), negationNormalFormNot(b, budget - 1)) + case Not(p) => negationNormalForm(p, budget - 1) + case True => False + case False => True + case s: Sym => Not(s) + } + + def negationNormalForm(p: Prop, budget: Int = AnalysisBudget.max): Prop = + if (budget <= 0) throw AnalysisBudget.exceeded + else p match { + case And(a, b) => And(negationNormalForm(a, budget - 1), negationNormalForm(b, budget - 1)) + case Or(a, b) => Or(negationNormalForm(a, budget - 1), negationNormalForm(b, budget - 1)) + case Not(negated) => negationNormalFormNot(negated, budget - 1) + case True + | False + | (_ : 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 = AnalysisBudget.max): Formula = { + def distribute(a: Formula, b: Formula, budget: Int): Formula = + if (budget <= 0) throw AnalysisBudget.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))) + } + + if (budget <= 0) throw AnalysisBudget.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 = if (Statistics.canEnable) Statistics.startTimer(patmatCNF) else null + val res = conjunctiveNormalForm(negationNormalForm(p)) + + 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)) + res + } + } + + // simple solver using DPLL + trait Solver 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 eq sym) && (o.pos == pos) + case _ => false + } + override def hashCode = sym.hashCode + pos.hashCode + + def unary_- = Lit(sym, !pos) + } + + 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 = 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] = { + 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)) + 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, true)) ++ force(Lit(s, false)) + } + debug.patmat("forced "+ forced) + val negated = negateModel(model) + findAllModels(f :+ negated, model :: (forced ++ models), recursionDepthAllowed - 1) + } + else models + } + + findAllModels(f, Nil) + } + + private def withLit(res: Model, l: Lit): Model = if (res eq NoModel) NoModel else res + (l.sym -> l.pos) + private def dropUnit(f: Formula, unitLit: Lit): Formula = { + 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 dropped = formulaBuilderSized(f.size) + for { + clause <- f + if !(clause contains unitLit) + } dropped += (clause - negated) + dropped + } + + def findModelFor(f: Formula): Model = { + @inline def orElse(a: Model, b: => Model) = if (a ne NoModel) a else b + + debug.patmat("DPLL\n"+ cnfString(f)) + + val start = if (Statistics.canEnable) Statistics.startTimer(patmatAnaDPLL) else null + + 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 + // debug.patmat("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 mutable.HashSet[Sym]() + val neg = new mutable.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)) + // debug.patmat("pure: "+ pureLit +" pures: "+ pures +" impures: "+ impures) + val simplified = f.filterNot(_.contains(pureLit)) + withLit(findModelFor(simplified), pureLit) + } else { + val split = f.head.head + // debug.patmat("split: "+ split) + orElse(findModelFor(f :+ clause(split)), findModelFor(f :+ clause(-split))) + } + } + + if (Statistics.canEnable) Statistics.stopTimer(patmatAnaDPLL, start) + + satisfiableWithModel + } + } +} -- cgit v1.2.3 From 5b7cfe3c63c15488ed7d8a9bb3b8d7f2043874d8 Mon Sep 17 00:00:00 2001 From: Adriaan Moors Date: Fri, 22 Feb 2013 16:46:21 -0800 Subject: better names for components of MatchTranslator --- .../tools/nsc/transform/patmat/MatchAnalysis.scala | 31 ++++++++++----------- .../nsc/transform/patmat/MatchOptimization.scala | 32 +++++++++++----------- .../nsc/transform/patmat/PatternMatching.scala | 4 +-- 3 files changed, 33 insertions(+), 34 deletions(-) diff --git a/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala b/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala index 95c3744ca1..74b932e173 100644 --- a/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala +++ b/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala @@ -125,23 +125,15 @@ trait TreeAndTypeAnalysis extends Debugging { } } -trait MatchAnalysis extends TreeAndTypeAnalysis with ScalaLogic with MatchTreeMaking { - import PatternMatchingStats._ - import global.{Tree, Type, Symbol, CaseDef, atPos, - Select, Block, ThisType, SingleType, NoPrefix, NoType, definitions, needsOuterTest, - ConstantType, Literal, Constant, gen, This, analyzer, EmptyTree, map2, NoSymbol, Traverser, - Function, Typed, treeInfo, DefTree, ValDef, nme, appliedType, Name, WildcardType, Ident, TypeRef, - UniqueType, RefinedType, currentUnit, SingletonType, singleType, ModuleClassSymbol, - nestedMemberType, TypeMap, EmptyScope, Apply, If, Bind, lub, Alternative, deriveCaseDef, Match, MethodType, LabelDef, TypeTree, Throw, newTermName} - - import definitions._ - import analyzer.{Typer, ErrorUtils, formalTypes} +trait MatchApproximation extends TreeAndTypeAnalysis with ScalaLogic with MatchTreeMaking { + import global.{Tree, Type, NoType, Symbol, NoSymbol, ConstantType, Literal, Constant, Ident, UniqueType, RefinedType, EmptyScope} + import global.definitions.{ListClass, NilModule} /** * Represent a match as a formula in propositional logic that encodes whether the match matches (abstractly: we only consider types) * */ - trait TreeMakerApproximation extends TreeMakers with TreesAndTypesDomain { + trait MatchApproximator extends TreeMakers with TreesAndTypesDomain { object Test { var currId = 0 } @@ -348,7 +340,14 @@ trait MatchAnalysis extends TreeAndTypeAnalysis with ScalaLogic with MatchTreeMa } } - trait MatchAnalyses extends TreeMakerApproximation { +} + +trait MatchAnalysis extends MatchApproximation { + import PatternMatchingStats._ + import global.{Tree, Type, Symbol, NoSymbol, Ident, Select} + import global.definitions.{isPrimitiveValueClass, ConsClass, isTupleSymbol} + + trait MatchAnalyzer extends MatchApproximator { def uncheckedWarning(pos: Position, msg: String) = global.currentUnit.uncheckedWarning(pos, msg) def warn(pos: Position, ex: AnalysisBudget.Exception, kind: String) = uncheckedWarning(pos, s"Cannot check match for $kind.\n${ex.advice}") @@ -498,7 +497,7 @@ trait MatchAnalysis extends TreeAndTypeAnalysis with ScalaLogic with MatchTreeMa // a way to construct a value that will make the match fail: a constructor invocation, a constant, an object of some type) class CounterExample { - protected[MatchAnalyses] def flattenConsArgs: List[CounterExample] = Nil + protected[MatchAnalyzer] def flattenConsArgs: List[CounterExample] = Nil def coveredBy(other: CounterExample): Boolean = this == other || other == WildcardExample } case class ValueExample(c: ValueConst) extends CounterExample { override def toString = c.toString } @@ -513,11 +512,11 @@ trait MatchAnalysis extends TreeAndTypeAnalysis with ScalaLogic with MatchTreeMa } } case class ListExample(ctorArgs: List[CounterExample]) extends CounterExample { - protected[MatchAnalyses] override def flattenConsArgs: List[CounterExample] = ctorArgs match { + protected[MatchAnalyzer] override def flattenConsArgs: List[CounterExample] = ctorArgs match { case hd :: tl :: Nil => hd :: tl.flattenConsArgs case _ => Nil } - protected[MatchAnalyses] lazy val elems = flattenConsArgs + protected[MatchAnalyzer] lazy val elems = flattenConsArgs override def coveredBy(other: CounterExample): Boolean = other match { diff --git a/src/compiler/scala/tools/nsc/transform/patmat/MatchOptimization.scala b/src/compiler/scala/tools/nsc/transform/patmat/MatchOptimization.scala index ebc2750a4d..dcf2413b15 100644 --- a/src/compiler/scala/tools/nsc/transform/patmat/MatchOptimization.scala +++ b/src/compiler/scala/tools/nsc/transform/patmat/MatchOptimization.scala @@ -30,7 +30,7 @@ trait MatchOptimization extends MatchTreeMaking with MatchAnalysis { //// - trait CommonSubconditionElimination extends TreeMakerApproximation { self: OptimizedCodegen => + trait CommonSubconditionElimination extends OptimizedCodegen with MatchApproximator { /** a flow-sensitive, generalised, common sub-expression elimination * reuse knowledge from performed tests * the only sub-expressions we consider are the conditions and results of the three tests (type, type&equality, equality) @@ -205,16 +205,16 @@ trait MatchOptimization extends MatchTreeMaking with MatchAnalysis { //// DCE - trait DeadCodeElimination extends TreeMakers { - // TODO: non-trivial dead-code elimination - // e.g., the following match should compile to a simple instanceof: - // case class Ident(name: String) - // for (Ident(name) <- ts) println(name) - def doDCE(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type): List[List[TreeMaker]] = { - // do minimal DCE - cases - } - } +// trait DeadCodeElimination extends TreeMakers { +// // TODO: non-trivial dead-code elimination +// // e.g., the following match should compile to a simple instanceof: +// // case class Ident(name: String) +// // for (Ident(name) <- ts) println(name) +// def doDCE(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type): List[List[TreeMaker]] = { +// // do minimal DCE +// cases +// } +// } //// SWITCHES -- TODO: operate on Tests rather than TreeMakers trait SwitchEmission extends TreeMakers with OptimizedMatchMonadInterface { @@ -589,12 +589,12 @@ trait MatchOptimization extends MatchTreeMaking with MatchAnalysis { } } - trait MatchOptimizations extends CommonSubconditionElimination - with DeadCodeElimination - with SwitchEmission - with OptimizedCodegen { + trait MatchOptimizer extends OptimizedCodegen + with SwitchEmission + with CommonSubconditionElimination { override def optimizeCases(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type): (List[List[TreeMaker]], List[Tree]) = { - val optCases = doCSE(prevBinder, doDCE(prevBinder, cases, pt), pt) + // TODO: do CSE on result of doDCE(prevBinder, cases, pt) + val optCases = doCSE(prevBinder, cases, pt) val toHoist = ( for (treeMakers <- optCases) yield treeMakers.collect{case tm: ReusedCondTreeMaker => tm.treesToHoist} diff --git a/src/compiler/scala/tools/nsc/transform/patmat/PatternMatching.scala b/src/compiler/scala/tools/nsc/transform/patmat/PatternMatching.scala index 6d6774cf20..f8d8044bdb 100644 --- a/src/compiler/scala/tools/nsc/transform/patmat/PatternMatching.scala +++ b/src/compiler/scala/tools/nsc/transform/patmat/PatternMatching.scala @@ -85,8 +85,8 @@ trait PatternMatching extends Transform with TypingTransformers } class OptimizingMatchTranslator(val typer: analyzer.Typer) extends MatchTranslator - with MatchOptimizations - with MatchAnalyses + with MatchOptimizer + with MatchAnalyzer with Solver } -- cgit v1.2.3 From 2cf6c5d7e5cfbd60958eac0a545f5c2978a8e5cd Mon Sep 17 00:00:00 2001 From: Adriaan Moors Date: Fri, 1 Mar 2013 18:23:57 -0800 Subject: [port] SI-7183 Disable unreachability for withFilter matches. This is a forward port of #2168 (originally for 2.10.1, but the pattern matcher has since been refactored in 2.10.x.) --- .../tools/nsc/transform/patmat/MatchAnalysis.scala | 10 ++++--- .../nsc/transform/patmat/MatchTreeMaking.scala | 33 ++++++++++++++-------- .../nsc/transform/patmat/PatternMatching.scala | 2 +- test/files/pos/t7183.flags | 1 + test/files/pos/t7183.scala | 13 +++++++++ 5 files changed, 43 insertions(+), 16 deletions(-) create mode 100644 test/files/pos/t7183.flags create mode 100644 test/files/pos/t7183.scala diff --git a/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala b/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala index 74b932e173..d9f93f27b6 100644 --- a/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala +++ b/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala @@ -691,11 +691,13 @@ trait MatchAnalysis extends MatchApproximation { VariableAssignment(scrutVar).toCounterExample() } - def analyzeCases(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type, unchecked: Boolean): Unit = { - unreachableCase(prevBinder, cases, pt) foreach { caseIndex => - reportUnreachable(cases(caseIndex).last.pos) + def analyzeCases(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type, suppression: Suppression): Unit = { + if (!suppression.unreachable) { + unreachableCase(prevBinder, cases, pt) foreach { caseIndex => + reportUnreachable(cases(caseIndex).last.pos) + } } - if (!unchecked) { + if (!suppression.exhaustive) { val counterExamples = exhaustive(prevBinder, cases, pt) if (counterExamples.nonEmpty) reportMissingCases(prevBinder.pos, counterExamples) diff --git a/src/compiler/scala/tools/nsc/transform/patmat/MatchTreeMaking.scala b/src/compiler/scala/tools/nsc/transform/patmat/MatchTreeMaking.scala index 51f21780b5..202f3444f8 100644 --- a/src/compiler/scala/tools/nsc/transform/patmat/MatchTreeMaking.scala +++ b/src/compiler/scala/tools/nsc/transform/patmat/MatchTreeMaking.scala @@ -23,16 +23,21 @@ trait MatchTreeMaking extends MatchCodeGen with Debugging { import global.{Tree, Type, Symbol, CaseDef, atPos, settings, Select, Block, ThisType, SingleType, NoPrefix, NoType, needsOuterTest, ConstantType, Literal, Constant, gen, This, EmptyTree, map2, NoSymbol, Traverser, - Function, Typed, treeInfo, TypeRef, DefTree} + Function, Typed, treeInfo, TypeRef, DefTree, Ident, nme} import global.definitions.{SomeClass, AnyRefClass, UncheckedClass, BooleanClass} + final case class Suppression(exhaustive: Boolean, unreachable: Boolean) + object Suppression { + val NoSuppression = Suppression(false, false) + } + /////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// // the making of the trees /////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// trait TreeMakers extends TypedSubstitution with CodegenCore { def optimizeCases(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type): (List[List[TreeMaker]], List[Tree]) - def analyzeCases(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type, unchecked: Boolean): Unit + def analyzeCases(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type, suppression: Suppression): Unit def emitSwitch(scrut: Tree, scrutSym: Symbol, cases: List[List[TreeMaker]], pt: Type, matchFailGenOverride: Option[Tree => Tree], unchecked: Boolean): Option[Tree] = None @@ -522,18 +527,24 @@ trait MatchTreeMaking extends MatchCodeGen with Debugging { def matchFailGen = (matchFailGenOverride orElse Some(CODE.MATCHERROR(_: Tree))) debug.patmat("combining cases: "+ (casesNoSubstOnly.map(_.mkString(" >> ")).mkString("{", "\n", "}"))) - val (unchecked, requireSwitch) = - if (settings.XnoPatmatAnalysis.value) (true, false) + val (suppression, requireSwitch): (Suppression, Boolean) = + if (settings.XnoPatmatAnalysis.value) (Suppression.NoSuppression, false) else scrut match { - case Typed(_, tpt) => - (tpt.tpe hasAnnotation UncheckedClass, - // matches with two or fewer cases need not apply for switchiness (if-then-else will do) - treeInfo.isSwitchAnnotation(tpt.tpe) && casesNoSubstOnly.lengthCompare(2) > 0) + case Typed(tree, tpt) => + val suppressExhaustive = tpt.tpe hasAnnotation UncheckedClass + val supressUnreachable = tree match { + case Ident(name) if name startsWith nme.CHECK_IF_REFUTABLE_STRING => true // SI-7183 don't warn for withFilter's that turn out to be irrefutable. + case _ => false + } + val suppression = Suppression(suppressExhaustive, supressUnreachable) + // matches with two or fewer cases need not apply for switchiness (if-then-else will do) + val requireSwitch = treeInfo.isSwitchAnnotation(tpt.tpe) && casesNoSubstOnly.lengthCompare(2) > 0 + (suppression, requireSwitch) case _ => - (false, false) + (Suppression.NoSuppression, false) } - emitSwitch(scrut, scrutSym, casesNoSubstOnly, pt, matchFailGenOverride, unchecked).getOrElse{ + emitSwitch(scrut, scrutSym, casesNoSubstOnly, pt, matchFailGenOverride, suppression.exhaustive).getOrElse{ if (requireSwitch) typer.context.unit.warning(scrut.pos, "could not emit switch for @switch annotated match") if (casesNoSubstOnly nonEmpty) { @@ -550,7 +561,7 @@ trait MatchTreeMaking extends MatchCodeGen with Debugging { }) None else matchFailGen - analyzeCases(scrutSym, casesNoSubstOnly, pt, unchecked) + analyzeCases(scrutSym, casesNoSubstOnly, pt, suppression) val (cases, toHoist) = optimizeCases(scrutSym, casesNoSubstOnly, pt) diff --git a/src/compiler/scala/tools/nsc/transform/patmat/PatternMatching.scala b/src/compiler/scala/tools/nsc/transform/patmat/PatternMatching.scala index f8d8044bdb..df4e699620 100644 --- a/src/compiler/scala/tools/nsc/transform/patmat/PatternMatching.scala +++ b/src/compiler/scala/tools/nsc/transform/patmat/PatternMatching.scala @@ -81,7 +81,7 @@ trait PatternMatching extends Transform with TypingTransformers class PureMatchTranslator(val typer: analyzer.Typer, val matchStrategy: Tree) extends MatchTranslator with PureCodegen { def optimizeCases(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type) = (cases, Nil) - def analyzeCases(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type, unchecked: Boolean): Unit = {} + def analyzeCases(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type, suppression: Suppression): Unit = {} } class OptimizingMatchTranslator(val typer: analyzer.Typer) extends MatchTranslator diff --git a/test/files/pos/t7183.flags b/test/files/pos/t7183.flags new file mode 100644 index 0000000000..e8fb65d50c --- /dev/null +++ b/test/files/pos/t7183.flags @@ -0,0 +1 @@ +-Xfatal-warnings \ No newline at end of file diff --git a/test/files/pos/t7183.scala b/test/files/pos/t7183.scala new file mode 100644 index 0000000000..7647c1634b --- /dev/null +++ b/test/files/pos/t7183.scala @@ -0,0 +1,13 @@ +class A +object A { + def unapply(a: A): Some[A] = Some(a) // Change return type to Option[A] and the warning is gone +} + +object Test { + for (A(a) <- List(new A)) yield a // spurious dead code warning. +} + +// List(new A()).withFilter(((check$ifrefutable$2) => check$ifrefutable$2: @scala.unchecked match { +// case A((a @ _)) => true +// case _ => false // this is dead code, but it's compiler generated. +// })) -- cgit v1.2.3