Skip to content
This repository
Browse code

[refactor] move PatternMatching.scala to transform.patmat

  • Loading branch information...
commit e14846ba029418723689fdacc668cd56a8165368 1 parent f5ed914
Adriaan Moors authored
1  src/compiler/scala/tools/nsc/Global.scala
@@ -23,6 +23,7 @@ import plugins.Plugins
23 23
 import ast._
24 24
 import ast.parser._
25 25
 import typechecker._
  26
+import transform.patmat.PatternMatching
26 27
 import transform._
27 28
 import backend.icode.{ ICodes, GenICode, ICodeCheckers }
28 29
 import backend.{ ScalaPrimitives, Platform, MSILPlatform, JavaPlatform }
513  src/compiler/scala/tools/nsc/transform/patmat/Logic.scala
... ...
@@ -0,0 +1,513 @@
  1
+/* NSC -- new Scala compiler
  2
+ *
  3
+ * Copyright 2011-2013 LAMP/EPFL
  4
+ * @author Adriaan Moors
  5
+ */
  6
+
  7
+package scala.tools.nsc.transform.patmat
  8
+
  9
+import scala.tools.nsc.{ast, symtab, typechecker, transform, Global}
  10
+import transform._
  11
+import typechecker._
  12
+import symtab._
  13
+import Flags.{MUTABLE, METHOD, LABEL, SYNTHETIC, ARTIFACT}
  14
+import scala.language.postfixOps
  15
+import scala.tools.nsc.transform.TypingTransformers
  16
+import scala.tools.nsc.transform.Transform
  17
+import scala.collection.mutable
  18
+import scala.reflect.internal.util.Statistics
  19
+import scala.reflect.internal.Types
  20
+import scala.reflect.internal.util.HashSet
  21
+
  22
+
  23
+trait Logic { self: PatternMatching =>
  24
+  import PatternMatchingStats._
  25
+  val global: Global
  26
+  import global.{Type, currentUnit, Position}
  27
+
  28
+  import debugging.patmatDebug
  29
+
  30
+  private def max(xs: Seq[Int]) = if (xs isEmpty) 0 else xs max
  31
+  private def alignedColumns(cols: Seq[AnyRef]): Seq[String] = {
  32
+    def toString(x: AnyRef) = if (x eq null) "" else x.toString
  33
+    if (cols.isEmpty || cols.tails.isEmpty) cols map toString
  34
+    else {
  35
+      val colLens = cols map (c => toString(c).length)
  36
+      val maxLen = max(colLens)
  37
+      val avgLen = colLens.sum/colLens.length
  38
+      val goalLen = maxLen min avgLen*2
  39
+      def pad(s: String) = {
  40
+        val toAdd = ((goalLen - s.length) max 0) + 2
  41
+        (" " * (toAdd/2)) + s + (" " * (toAdd/2 + (toAdd%2)))
  42
+      }
  43
+      cols map (x => pad(toString(x)))
  44
+    }
  45
+  }
  46
+
  47
+  def alignAcrossRows(xss: List[List[AnyRef]], sep: String, lineSep: String = "\n"): String = {
  48
+    val maxLen = max(xss map (_.length))
  49
+    val padded = xss map (xs => xs ++ List.fill(maxLen - xs.length)(null))
  50
+    padded.transpose.map(alignedColumns).transpose map (_.mkString(sep)) mkString(lineSep)
  51
+  }
  52
+
  53
+  // http://www.cis.upenn.edu/~cis510/tcl/chap3.pdf
  54
+  // http://users.encs.concordia.ca/~ta_ahmed/ms_thesis.pdf
  55
+  trait FirstOrderLogic {
  56
+    class Prop
  57
+    case class Eq(p: Var, q: Const) extends Prop
  58
+
  59
+    type Const
  60
+
  61
+    type TypeConst <: Const
  62
+    def TypeConst: TypeConstExtractor
  63
+    trait TypeConstExtractor {
  64
+      def apply(tp: Type): Const
  65
+    }
  66
+
  67
+    def NullConst: Const
  68
+
  69
+    type Var <: AbsVar
  70
+
  71
+    trait AbsVar {
  72
+      // indicate we may later require a prop for V = C
  73
+      def registerEquality(c: Const): Unit
  74
+
  75
+      // call this to indicate null is part of the domain
  76
+      def registerNull(): Unit
  77
+
  78
+      // can this variable be null?
  79
+      def mayBeNull: Boolean
  80
+
  81
+      // compute the domain and return it (call registerNull first!)
  82
+      def domainSyms: Option[Set[Sym]]
  83
+
  84
+      // the symbol for this variable being equal to its statically known type
  85
+      // (only available if registerEquality has been called for that type before)
  86
+      def symForStaticTp: Option[Sym]
  87
+
  88
+      // for this var, call it V, turn V = C into the equivalent proposition in boolean logic
  89
+      // registerEquality(c) must have been called prior to this call
  90
+      // in fact, all equalities relevant to this variable must have been registered
  91
+      def propForEqualsTo(c: Const): Prop
  92
+
  93
+      // populated by registerEquality
  94
+      // once implications has been called, must not call registerEquality anymore
  95
+      def implications: List[(Sym, List[Sym], List[Sym])]
  96
+    }
  97
+
  98
+    // would be nice to statically check whether a prop is equational or pure,
  99
+    // but that requires typing relations like And(x: Tx, y: Ty) : (if(Tx == PureProp && Ty == PureProp) PureProp else Prop)
  100
+    case class And(a: Prop, b: Prop) extends Prop
  101
+    case class Or(a: Prop, b: Prop) extends Prop
  102
+    case class Not(a: Prop) extends Prop
  103
+
  104
+    case object True extends Prop
  105
+    case object False extends Prop
  106
+
  107
+    // symbols are propositions
  108
+    abstract case class Sym(val variable: Var, val const: Const) extends Prop {
  109
+      private[this] val id = Sym.nextSymId
  110
+
  111
+      override def toString = variable +"="+ const +"#"+ id
  112
+    }
  113
+    class UniqueSym(variable: Var, const: Const) extends Sym(variable, const)
  114
+    object Sym {
  115
+      private val uniques: HashSet[Sym] = new HashSet("uniques", 512)
  116
+      def apply(variable: Var, const: Const): Sym = {
  117
+        val newSym = new UniqueSym(variable, const)
  118
+        (uniques findEntryOrUpdate newSym)
  119
+      }
  120
+      private def nextSymId = {_symId += 1; _symId}; private var _symId = 0
  121
+    }
  122
+
  123
+    def /\(props: Iterable[Prop]) = if (props.isEmpty) True else props.reduceLeft(And(_, _))
  124
+    def \/(props: Iterable[Prop]) = if (props.isEmpty) False else props.reduceLeft(Or(_, _))
  125
+
  126
+    trait PropTraverser {
  127
+      def apply(x: Prop): Unit = x match {
  128
+        case And(a, b) => apply(a); apply(b)
  129
+        case Or(a, b) => apply(a); apply(b)
  130
+        case Not(a) => apply(a)
  131
+        case Eq(a, b) => applyVar(a); applyConst(b)
  132
+        case _ =>
  133
+      }
  134
+      def applyVar(x: Var): Unit = {}
  135
+      def applyConst(x: Const): Unit = {}
  136
+    }
  137
+
  138
+    def gatherVariables(p: Prop): Set[Var] = {
  139
+      val vars = new mutable.HashSet[Var]()
  140
+      (new PropTraverser {
  141
+        override def applyVar(v: Var) = vars += v
  142
+      })(p)
  143
+      vars.toSet
  144
+    }
  145
+
  146
+    trait PropMap {
  147
+      def apply(x: Prop): Prop = x match { // TODO: mapConserve
  148
+        case And(a, b) => And(apply(a), apply(b))
  149
+        case Or(a, b) => Or(apply(a), apply(b))
  150
+        case Not(a) => Not(apply(a))
  151
+        case p => p
  152
+      }
  153
+    }
  154
+
  155
+    // to govern how much time we spend analyzing matches for unreachability/exhaustivity
  156
+    object AnalysisBudget {
  157
+      import scala.tools.cmd.FromString.IntFromString
  158
+      val max = sys.props.get("scalac.patmat.analysisBudget").collect(IntFromString.orElse{case "off" => Integer.MAX_VALUE}).getOrElse(256)
  159
+
  160
+      abstract class Exception extends RuntimeException("CNF budget exceeded") {
  161
+        val advice: String
  162
+        def warn(pos: Position, kind: String) = currentUnit.uncheckedWarning(pos, s"Cannot check match for $kind.\n$advice")
  163
+      }
  164
+
  165
+      object exceeded extends Exception {
  166
+        val advice = s"(The analysis required more space than allowed. Please try with scalac -Dscalac.patmat.analysisBudget=${AnalysisBudget.max*2} or -Dscalac.patmat.analysisBudget=off.)"
  167
+      }
  168
+    }
  169
+
  170
+    // convert finite domain propositional logic with subtyping to pure boolean propositional logic
  171
+    // a type test or a value equality test are modelled as a variable being equal to some constant
  172
+    // a variable V may be assigned multiple constants, as long as they do not contradict each other
  173
+    // according to subtyping, e.g., V = ConstantType(1) and V = Int are valid assignments
  174
+    // we rewrite V = C to a fresh boolean symbol, and model what we know about the variable's domain
  175
+    // in a prelude (the equality axioms)
  176
+    //   1. a variable with a closed domain (of a sealed type) must be assigned one of the instantiatable types in its domain
  177
+    //   2. for each variable V in props, and each constant C it is compared to,
  178
+    //      compute which assignments imply each other (as in the example above: V = 1 implies V = Int)
  179
+    //      and which assignments are mutually exclusive (V = String implies -(V = Int))
  180
+    //
  181
+    // note that this is a conservative approximation: V = Constant(A) and V = Constant(B)
  182
+    // are considered mutually exclusive (and thus both cases are considered reachable in {case A => case B =>}),
  183
+    // even though A may be equal to B   (and thus the second case is not "dynamically reachable")
  184
+    //
  185
+    // TODO: for V1 representing x1 and V2 standing for x1.head, encode that
  186
+    //       V1 = Nil implies -(V2 = Ci) for all Ci in V2's domain (i.e., it is unassignable)
  187
+    // may throw an AnalysisBudget.Exception
  188
+    def removeVarEq(props: List[Prop], modelNull: Boolean = false): (Formula, List[Formula]) = {
  189
+      val start = if (Statistics.canEnable) Statistics.startTimer(patmatAnaVarEq) else null
  190
+
  191
+      val vars = new scala.collection.mutable.HashSet[Var]
  192
+
  193
+      object gatherEqualities extends PropTraverser {
  194
+        override def apply(p: Prop) = p match {
  195
+          case Eq(v, c) =>
  196
+            vars += v
  197
+            v.registerEquality(c)
  198
+          case _ => super.apply(p)
  199
+        }
  200
+      }
  201
+
  202
+      object rewriteEqualsToProp extends PropMap {
  203
+        override def apply(p: Prop) = p match {
  204
+          case Eq(v, c) => v.propForEqualsTo(c)
  205
+          case _ => super.apply(p)
  206
+        }
  207
+      }
  208
+
  209
+      props foreach gatherEqualities.apply
  210
+      if (modelNull) vars foreach (_.registerNull)
  211
+
  212
+      val pure = props map (p => eqFreePropToSolvable(rewriteEqualsToProp(p)))
  213
+
  214
+      val eqAxioms = formulaBuilder
  215
+      @inline def addAxiom(p: Prop) = addFormula(eqAxioms, eqFreePropToSolvable(p))
  216
+
  217
+      patmatDebug("removeVarEq vars: "+ vars)
  218
+      vars.foreach { v =>
  219
+        // if v.domainSyms.isEmpty, we must consider the domain to be infinite
  220
+        // otherwise, since the domain fully partitions the type of the value,
  221
+        // exactly one of the types (and whatever it implies, imposed separately) must be chosen
  222
+        // consider X ::= A | B | C, and A => B
  223
+        // coverage is formulated as: A \/ B \/ C and the implications are
  224
+        v.domainSyms foreach { dsyms => addAxiom(\/(dsyms)) }
  225
+
  226
+        // when this variable cannot be null the equality corresponding to the type test `(x: T)`, where T is x's static type,
  227
+        // is always true; when the variable may be null we use the implication `(x != null) => (x: T)` for the axiom
  228
+        v.symForStaticTp foreach { symForStaticTp =>
  229
+          if (v.mayBeNull) addAxiom(Or(v.propForEqualsTo(NullConst), symForStaticTp))
  230
+          else addAxiom(symForStaticTp)
  231
+        }
  232
+
  233
+        v.implications foreach { case (sym, implied, excluded) =>
  234
+          // when sym is true, what must hold...
  235
+          implied  foreach (impliedSym  => addAxiom(Or(Not(sym), impliedSym)))
  236
+          // ... and what must not?
  237
+          excluded foreach (excludedSym => addAxiom(Or(Not(sym), Not(excludedSym))))
  238
+        }
  239
+      }
  240
+
  241
+      patmatDebug("eqAxioms:\n"+ cnfString(toFormula(eqAxioms)))
  242
+      patmatDebug("pure:"+ pure.map(p => cnfString(p)).mkString("\n"))
  243
+
  244
+      if (Statistics.canEnable) Statistics.stopTimer(patmatAnaVarEq, start)
  245
+
  246
+      (toFormula(eqAxioms), pure)
  247
+    }
  248
+
  249
+
  250
+    // an interface that should be suitable for feeding a SAT solver when the time comes
  251
+    type Formula
  252
+    type FormulaBuilder
  253
+
  254
+    // creates an empty formula builder to which more formulae can be added
  255
+    def formulaBuilder: FormulaBuilder
  256
+
  257
+    // val f = formulaBuilder; addFormula(f, f1); ... addFormula(f, fN)
  258
+    // toFormula(f) == andFormula(f1, andFormula(..., fN))
  259
+    def addFormula(buff: FormulaBuilder, f: Formula): Unit
  260
+    def toFormula(buff: FormulaBuilder): Formula
  261
+
  262
+    // the conjunction of formulae `a` and `b`
  263
+    def andFormula(a: Formula, b: Formula): Formula
  264
+
  265
+    // equivalent formula to `a`, but simplified in a lightweight way (drop duplicate clauses)
  266
+    def simplifyFormula(a: Formula): Formula
  267
+
  268
+    // may throw an AnalysisBudget.Exception
  269
+    def propToSolvable(p: Prop): Formula = {
  270
+      val (eqAxioms, pure :: Nil) = removeVarEq(List(p), modelNull = false)
  271
+      andFormula(eqAxioms, pure)
  272
+    }
  273
+
  274
+    // may throw an AnalysisBudget.Exception
  275
+    def eqFreePropToSolvable(p: Prop): Formula
  276
+    def cnfString(f: Formula): String
  277
+
  278
+    type Model = Map[Sym, Boolean]
  279
+    val EmptyModel: Model
  280
+    val NoModel: Model
  281
+
  282
+    def findModelFor(f: Formula): Model
  283
+    def findAllModelsFor(f: Formula): List[Model]
  284
+  }
  285
+
  286
+  trait CNF extends FirstOrderLogic {
  287
+
  288
+    /** Override Array creation for efficiency (to not go through reflection). */
  289
+    private implicit val clauseTag: scala.reflect.ClassTag[Clause] = new scala.reflect.ClassTag[Clause] {
  290
+      def runtimeClass: java.lang.Class[Clause] = classOf[Clause]
  291
+      final override def newArray(len: Int): Array[Clause] = new Array[Clause](len)
  292
+    }
  293
+
  294
+    import scala.collection.mutable.ArrayBuffer
  295
+    type FormulaBuilder = ArrayBuffer[Clause]
  296
+    def formulaBuilder  = ArrayBuffer[Clause]()
  297
+    def formulaBuilderSized(init: Int)  = new ArrayBuffer[Clause](init)
  298
+    def addFormula(buff: FormulaBuilder, f: Formula): Unit = buff ++= f
  299
+    def toFormula(buff: FormulaBuilder): Formula = buff
  300
+
  301
+    // CNF: a formula is a conjunction of clauses
  302
+    type Formula = FormulaBuilder
  303
+    def formula(c: Clause*): Formula = ArrayBuffer(c: _*)
  304
+
  305
+    type Clause  = Set[Lit]
  306
+    // a clause is a disjunction of distinct literals
  307
+    def clause(l: Lit*): Clause = l.toSet
  308
+
  309
+    type Lit
  310
+    def Lit(sym: Sym, pos: Boolean = true): Lit
  311
+
  312
+    def andFormula(a: Formula, b: Formula): Formula = a ++ b
  313
+    def simplifyFormula(a: Formula): Formula = a.distinct
  314
+
  315
+    private def merge(a: Clause, b: Clause) = a ++ b
  316
+
  317
+    // throws an AnalysisBudget.Exception when the prop results in a CNF that's too big
  318
+    // TODO: be smarter/more efficient about this (http://lara.epfl.ch/w/sav09:tseitin_s_encoding)
  319
+    def eqFreePropToSolvable(p: Prop): Formula = {
  320
+      def negationNormalFormNot(p: Prop, budget: Int): Prop =
  321
+        if (budget <= 0) throw AnalysisBudget.exceeded
  322
+        else p match {
  323
+          case And(a, b) =>  Or(negationNormalFormNot(a, budget - 1), negationNormalFormNot(b, budget - 1))
  324
+          case Or(a, b)  => And(negationNormalFormNot(a, budget - 1), negationNormalFormNot(b, budget - 1))
  325
+          case Not(p)    => negationNormalForm(p, budget - 1)
  326
+          case True      => False
  327
+          case False     => True
  328
+          case s: Sym    => Not(s)
  329
+        }
  330
+
  331
+      def negationNormalForm(p: Prop, budget: Int = AnalysisBudget.max): Prop =
  332
+        if (budget <= 0) throw AnalysisBudget.exceeded
  333
+        else p match {
  334
+          case And(a, b)      => And(negationNormalForm(a, budget - 1), negationNormalForm(b, budget - 1))
  335
+          case Or(a, b)       =>  Or(negationNormalForm(a, budget - 1), negationNormalForm(b, budget - 1))
  336
+          case Not(negated)   => negationNormalFormNot(negated, budget - 1)
  337
+          case True
  338
+             | False
  339
+             | (_ : Sym)      => p
  340
+        }
  341
+
  342
+      val TrueF          = formula()
  343
+      val FalseF         = formula(clause())
  344
+      def lit(s: Sym)    = formula(clause(Lit(s)))
  345
+      def negLit(s: Sym) = formula(clause(Lit(s, false)))
  346
+
  347
+      def conjunctiveNormalForm(p: Prop, budget: Int = AnalysisBudget.max): Formula = {
  348
+        def distribute(a: Formula, b: Formula, budget: Int): Formula =
  349
+          if (budget <= 0) throw AnalysisBudget.exceeded
  350
+          else
  351
+            (a, b) match {
  352
+              // true \/ _ = true
  353
+              // _ \/ true = true
  354
+              case (trueA, trueB) if trueA.size == 0 || trueB.size == 0 => TrueF
  355
+              // lit \/ lit
  356
+              case (a, b) if a.size == 1 && b.size == 1 => formula(merge(a(0), b(0)))
  357
+              // (c1 /\ ... /\ cn) \/ d = ((c1 \/ d) /\ ... /\ (cn \/ d))
  358
+              // d \/ (c1 /\ ... /\ cn) = ((d \/ c1) /\ ... /\ (d \/ cn))
  359
+              case (cs, ds) =>
  360
+                val (big, small) = if (cs.size > ds.size) (cs, ds) else (ds, cs)
  361
+                big flatMap (c => distribute(formula(c), small, budget - (big.size*small.size)))
  362
+            }
  363
+
  364
+        if (budget <= 0) throw AnalysisBudget.exceeded
  365
+
  366
+        p match {
  367
+          case True        => TrueF
  368
+          case False       => FalseF
  369
+          case s: Sym      => lit(s)
  370
+          case Not(s: Sym) => negLit(s)
  371
+          case And(a, b)   =>
  372
+            val cnfA = conjunctiveNormalForm(a, budget - 1)
  373
+            val cnfB = conjunctiveNormalForm(b, budget - cnfA.size)
  374
+            cnfA ++ cnfB
  375
+          case Or(a, b)    =>
  376
+            val cnfA = conjunctiveNormalForm(a)
  377
+            val cnfB = conjunctiveNormalForm(b)
  378
+            distribute(cnfA, cnfB, budget - (cnfA.size + cnfB.size))
  379
+        }
  380
+      }
  381
+
  382
+      val start = if (Statistics.canEnable) Statistics.startTimer(patmatCNF) else null
  383
+      val res   = conjunctiveNormalForm(negationNormalForm(p))
  384
+
  385
+      if (Statistics.canEnable) Statistics.stopTimer(patmatCNF, start)
  386
+
  387
+      //
  388
+      if (Statistics.canEnable) patmatCNFSizes(res.size).value += 1
  389
+
  390
+//      patmatDebug("cnf for\n"+ p +"\nis:\n"+cnfString(res))
  391
+      res
  392
+    }
  393
+
  394
+  }
  395
+
  396
+  trait DPLLSolver extends CNF {
  397
+    // a literal is a (possibly negated) variable
  398
+    def Lit(sym: Sym, pos: Boolean = true) = new Lit(sym, pos)
  399
+    class Lit(val sym: Sym, val pos: Boolean) {
  400
+      override def toString = if (!pos) "-"+ sym.toString else sym.toString
  401
+      override def equals(o: Any) = o match {
  402
+        case o: Lit => (o.sym eq sym) && (o.pos == pos)
  403
+        case _ => false
  404
+      }
  405
+      override def hashCode = sym.hashCode + pos.hashCode
  406
+
  407
+      def unary_- = Lit(sym, !pos)
  408
+    }
  409
+
  410
+    def cnfString(f: Formula) = alignAcrossRows(f map (_.toList) toList, "\\/", " /\\\n")
  411
+
  412
+    // adapted from http://lara.epfl.ch/w/sav10:simple_sat_solver (original by Hossein Hojjat)
  413
+    val EmptyModel = Map.empty[Sym, Boolean]
  414
+    val NoModel: Model = null
  415
+
  416
+    // returns all solutions, if any (TODO: better infinite recursion backstop -- detect fixpoint??)
  417
+    def findAllModelsFor(f: Formula): List[Model] = {
  418
+      val vars: Set[Sym] = f.flatMap(_ collect {case l: Lit => l.sym}).toSet
  419
+      // patmatDebug("vars "+ vars)
  420
+      // the negation of a model -(S1=True/False /\ ... /\ SN=True/False) = clause(S1=False/True, ...., SN=False/True)
  421
+      def negateModel(m: Model) = clause(m.toSeq.map{ case (sym, pos) => Lit(sym, !pos) } : _*)
  422
+
  423
+      def findAllModels(f: Formula, models: List[Model], recursionDepthAllowed: Int = 10): List[Model]=
  424
+        if (recursionDepthAllowed == 0) models
  425
+        else {
  426
+          patmatDebug("find all models for\n"+ cnfString(f))
  427
+          val model = findModelFor(f)
  428
+          // if we found a solution, conjunct the formula with the model's negation and recurse
  429
+          if (model ne NoModel) {
  430
+            val unassigned = (vars -- model.keySet).toList
  431
+            patmatDebug("unassigned "+ unassigned +" in "+ model)
  432
+            def force(lit: Lit) = {
  433
+              val model = withLit(findModelFor(dropUnit(f, lit)), lit)
  434
+              if (model ne NoModel) List(model)
  435
+              else Nil
  436
+            }
  437
+            val forced = unassigned flatMap { s =>
  438
+              force(Lit(s, true)) ++ force(Lit(s, false))
  439
+            }
  440
+            patmatDebug("forced "+ forced)
  441
+            val negated = negateModel(model)
  442
+            findAllModels(f :+ negated, model :: (forced ++ models), recursionDepthAllowed - 1)
  443
+          }
  444
+          else models
  445
+        }
  446
+
  447
+      findAllModels(f, Nil)
  448
+    }
  449
+
  450
+    private def withLit(res: Model, l: Lit): Model = if (res eq NoModel) NoModel else res + (l.sym -> l.pos)
  451
+    private def dropUnit(f: Formula, unitLit: Lit): Formula = {
  452
+      val negated = -unitLit
  453
+      // drop entire clauses that are trivially true
  454
+      // (i.e., disjunctions that contain the literal we're making true in the returned model),
  455
+      // and simplify clauses by dropping the negation of the literal we're making true
  456
+      // (since False \/ X == X)
  457
+      val dropped = formulaBuilderSized(f.size)
  458
+      for {
  459
+        clause <- f
  460
+        if !(clause contains unitLit)
  461
+      } dropped += (clause - negated)
  462
+      dropped
  463
+    }
  464
+
  465
+    def findModelFor(f: Formula): Model = {
  466
+      @inline def orElse(a: Model, b: => Model) = if (a ne NoModel) a else b
  467
+
  468
+      patmatDebug("DPLL\n"+ cnfString(f))
  469
+
  470
+      val start = if (Statistics.canEnable) Statistics.startTimer(patmatAnaDPLL) else null
  471
+
  472
+      val satisfiableWithModel: Model =
  473
+        if (f isEmpty) EmptyModel
  474
+        else if(f exists (_.isEmpty)) NoModel
  475
+        else f.find(_.size == 1) match {
  476
+          case Some(unitClause) =>
  477
+            val unitLit = unitClause.head
  478
+            // patmatDebug("unit: "+ unitLit)
  479
+            withLit(findModelFor(dropUnit(f, unitLit)), unitLit)
  480
+          case _ =>
  481
+            // partition symbols according to whether they appear in positive and/or negative literals
  482
+            val pos = new mutable.HashSet[Sym]()
  483
+            val neg = new mutable.HashSet[Sym]()
  484
+            f.foreach{_.foreach{ lit =>
  485
+              if (lit.pos) pos += lit.sym else neg += lit.sym
  486
+            }}
  487
+            // appearing in both positive and negative
  488
+            val impures = pos intersect neg
  489
+            // appearing only in either positive/negative positions
  490
+            val pures = (pos ++ neg) -- impures
  491
+
  492
+            if (pures nonEmpty) {
  493
+              val pureSym = pures.head
  494
+              // turn it back into a literal
  495
+              // (since equality on literals is in terms of equality
  496
+              //  of the underlying symbol and its positivity, simply construct a new Lit)
  497
+              val pureLit = Lit(pureSym, pos(pureSym))
  498
+              // patmatDebug("pure: "+ pureLit +" pures: "+ pures +" impures: "+ impures)
  499
+              val simplified = f.filterNot(_.contains(pureLit))
  500
+              withLit(findModelFor(simplified), pureLit)
  501
+            } else {
  502
+              val split = f.head.head
  503
+              // patmatDebug("split: "+ split)
  504
+              orElse(findModelFor(f :+ clause(split)), findModelFor(f :+ clause(-split)))
  505
+            }
  506
+        }
  507
+
  508
+        if (Statistics.canEnable) Statistics.stopTimer(patmatAnaDPLL, start)
  509
+
  510
+        satisfiableWithModel
  511
+    }
  512
+  }
  513
+}
1,090  src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala
... ...
@@ -0,0 +1,1090 @@
  1
+/* NSC -- new Scala compiler
  2
+ *
  3
+ * Copyright 2011-2013 LAMP/EPFL
  4
+ * @author Adriaan Moors
  5
+ */
  6
+
  7
+package scala.tools.nsc.transform.patmat
  8
+
  9
+import scala.tools.nsc.{ast, symtab, typechecker, transform, Global}
  10
+import transform._
  11
+import typechecker._
  12
+import symtab._
  13
+import Flags.{MUTABLE, METHOD, LABEL, SYNTHETIC, ARTIFACT}
  14
+import scala.language.postfixOps
  15
+import scala.tools.nsc.transform.TypingTransformers
  16
+import scala.tools.nsc.transform.Transform
  17
+import scala.collection.mutable
  18
+import scala.reflect.internal.util.Statistics
  19
+import scala.reflect.internal.Types
  20
+import scala.reflect.internal.util.HashSet
  21
+
  22
+trait TypeAnalysis extends Debugging {
  23
+  val global: Global
  24
+  import global.{Type, Symbol, definitions, analyzer,
  25
+    ConstantType, Literal, Constant,  appliedType, WildcardType, TypeRef, ModuleClassSymbol,
  26
+    nestedMemberType, TypeMap}
  27
+
  28
+  import definitions._
  29
+  import analyzer.Typer
  30
+
  31
+  import debugging.patmatDebug
  32
+
  33
+  trait CheckableTypeAnalysis {
  34
+    val typer: Typer
  35
+
  36
+    // TODO: domain of other feasibly enumerable built-in types (char?)
  37
+    def enumerateSubtypes(tp: Type): Option[List[Type]] =
  38
+      tp.typeSymbol match {
  39
+        // TODO case _ if tp.isTupleType => // recurse into component types?
  40
+        case UnitClass =>
  41
+          Some(List(UnitClass.tpe))
  42
+        case BooleanClass =>
  43
+          Some((List(ConstantType(Constant(true)), ConstantType(Constant(false)))))
  44
+        // TODO case _ if tp.isTupleType => // recurse into component types
  45
+        case modSym: ModuleClassSymbol =>
  46
+          Some(List(tp))
  47
+        // make sure it's not a primitive, else (5: Byte) match { case 5 => ... } sees no Byte
  48
+        case sym if !sym.isSealed || isPrimitiveValueClass(sym) =>
  49
+          patmatDebug("enum unsealed "+ (tp, sym, sym.isSealed, isPrimitiveValueClass(sym)))
  50
+          None
  51
+        case sym =>
  52
+          val subclasses = (
  53
+            sym.sealedDescendants.toList sortBy (_.sealedSortName)
  54
+            // symbols which are both sealed and abstract need not be covered themselves, because
  55
+            // all of their children must be and they cannot otherwise be created.
  56
+            filterNot (x => x.isSealed && x.isAbstractClass && !isPrimitiveValueClass(x)))
  57
+          patmatDebug("enum sealed -- subclasses: "+ (sym, subclasses))
  58
+
  59
+          val tpApprox = typer.infer.approximateAbstracts(tp)
  60
+          val pre = tpApprox.prefix
  61
+          // valid subtypes are turned into checkable types, as we are entering the realm of the dynamic
  62
+          val validSubTypes = (subclasses flatMap {sym =>
  63
+              // have to filter out children which cannot match: see ticket #3683 for an example
  64
+              // compare to the fully known type `tp` (modulo abstract types),
  65
+              // so that we can rule out stuff like: sealed trait X[T]; class XInt extends X[Int] --> XInt not valid when enumerating X[String]
  66
+              // however, must approximate abstract types in
  67
+
  68
+              val memberType  = nestedMemberType(sym, pre, tpApprox.typeSymbol.owner)
  69
+              val subTp       = appliedType(memberType, sym.typeParams.map(_ => WildcardType))
  70
+              val subTpApprox = typer.infer.approximateAbstracts(subTp) // TODO: needed?
  71
+              // patmatDebug("subtp"+(subTpApprox <:< tpApprox, subTpApprox, tpApprox))
  72
+              if (subTpApprox <:< tpApprox) Some(checkableType(subTp))
  73
+              else None
  74
+            })
  75
+          patmatDebug("enum sealed "+ (tp, tpApprox) + " as "+ validSubTypes)
  76
+          Some(validSubTypes)
  77
+      }
  78
+
  79
+    // approximate a type to the static type that is fully checkable at run time,
  80
+    // hiding statically known but dynamically uncheckable information using existential quantification
  81
+    // TODO: this is subject to the availability of TypeTags (since an abstract type with a type tag is checkable at run time)
  82
+    def checkableType(tp: Type): Type = {
  83
+      // TODO: this is extremely rough...
  84
+      // replace type args by wildcards, since they can't be checked (don't use existentials: overkill)
  85
+      // TODO: when type tags are available, we will check -- when this is implemented, can we take that into account here?
  86
+      // similar to typer.infer.approximateAbstracts
  87
+      object typeArgsToWildcardsExceptArray extends TypeMap {
  88
+        def apply(tp: Type): Type = tp match {
  89
+          case TypeRef(pre, sym, args) if args.nonEmpty && (sym ne ArrayClass) =>
  90
+            TypeRef(pre, sym, args map (_ => WildcardType))
  91
+          case _ =>
  92
+            mapOver(tp)
  93
+        }
  94
+      }
  95
+
  96
+      val res = typeArgsToWildcardsExceptArray(tp)
  97
+      patmatDebug("checkable "+(tp, res))
  98
+      res
  99
+    }
  100
+
  101
+    // a type is "uncheckable" (for exhaustivity) if we don't statically know its subtypes (i.e., it's unsealed)
  102
+    // we consider tuple types with at least one component of a checkable type as a checkable type
  103
+    def uncheckableType(tp: Type): Boolean = {
  104
+      def tupleComponents(tp: Type) = tp.normalize.typeArgs
  105
+      val checkable = (
  106
+           (isTupleType(tp) && tupleComponents(tp).exists(tp => !uncheckableType(tp)))
  107
+        || enumerateSubtypes(tp).nonEmpty)
  108
+      // if (!checkable) patmatDebug("deemed uncheckable: "+ tp)
  109
+      !checkable
  110
+    }
  111
+  }
  112
+}
  113
+
  114
+trait Analysis extends TypeAnalysis { self: PatternMatching =>
  115
+  import PatternMatchingStats._
  116
+  val global: Global
  117
+  import global.{Tree, Type, Symbol, CaseDef, Position, atPos, NoPosition,
  118
+    Select, Block, ThisType, SingleType, NoPrefix, NoType, definitions, needsOuterTest,
  119
+    ConstantType, Literal, Constant, gen, This, analyzer, EmptyTree, map2, NoSymbol, Traverser,
  120
+    Function, Typed, treeInfo, DefTree, ValDef, nme, appliedType, Name, WildcardType, Ident, TypeRef,
  121
+    UniqueType, RefinedType, currentUnit, SingletonType, singleType, ModuleClassSymbol,
  122
+    nestedMemberType, TypeMap, EmptyScope, Apply, If, Bind, lub, Alternative, deriveCaseDef, Match, MethodType, LabelDef, TypeTree, Throw, newTermName}
  123
+
  124
+  import definitions._
  125
+  import analyzer.{Typer, ErrorUtils, formalTypes}
  126
+
  127
+  import debugging.patmatDebug
  128
+
  129
+  /**
  130
+   * Represent a match as a formula in propositional logic that encodes whether the match matches (abstractly: we only consider types)
  131
+   *
  132
+   * TODO: remove duplication between Cond and Prop
  133
+   */
  134
+  trait TreeMakerApproximation extends TreeMakers with FirstOrderLogic with CheckableTypeAnalysis { self: CodegenCore =>
  135
+    object Test {
  136
+      var currId = 0
  137
+    }
  138
+    case class Test(cond: Cond, treeMaker: TreeMaker) {
  139
+      // private val reusedBy = new scala.collection.mutable.HashSet[Test]
  140
+      var reuses: Option[Test] = None
  141
+      def registerReuseBy(later: Test): Unit = {
  142
+        assert(later.reuses.isEmpty, later.reuses)
  143
+        // reusedBy += later
  144
+        later.reuses = Some(this)
  145
+      }
  146
+
  147
+      val id = { Test.currId += 1; Test.currId}
  148
+      override def toString =
  149
+        "T"+ id + "C("+ cond +")"  //+ (reuses map ("== T"+_.id) getOrElse (if(reusedBy.isEmpty) treeMaker else reusedBy mkString (treeMaker+ " -->(", ", ",")")))
  150
+    }
  151
+
  152
+    // TODO: remove Cond, replace by Prop from Logic
  153
+    object Cond {
  154
+      var currId = 0
  155
+    }
  156
+
  157
+    abstract class Cond {
  158
+      val id = { Cond.currId += 1; Cond.currId}
  159
+    }
  160
+
  161
+    case object TrueCond extends Cond  {override def toString = "T"}
  162
+    case object FalseCond extends Cond {override def toString = "F"}
  163
+
  164
+    case class AndCond(a: Cond, b: Cond) extends Cond {override def toString = a +"/\\"+ b}
  165
+    case class OrCond(a: Cond, b: Cond)  extends Cond {override def toString = "("+a+") \\/ ("+ b +")"}
  166
+
  167
+    object EqualityCond {
  168
+      private val uniques = new mutable.HashMap[(Tree, Tree), EqualityCond]
  169
+      def apply(testedPath: Tree, rhs: Tree): EqualityCond = uniques getOrElseUpdate((testedPath, rhs), new EqualityCond(testedPath, rhs))
  170
+      def unapply(c: EqualityCond) = Some((c.testedPath, c.rhs))
  171
+    }
  172
+    class EqualityCond(val testedPath: Tree, val rhs: Tree) extends Cond {
  173
+      override def toString = testedPath +" == "+ rhs +"#"+ id
  174
+    }
  175
+
  176
+    object NonNullCond {
  177
+      private val uniques = new mutable.HashMap[Tree, NonNullCond]
  178
+      def apply(testedPath: Tree): NonNullCond = uniques getOrElseUpdate(testedPath, new NonNullCond(testedPath))
  179
+      def unapply(c: NonNullCond) = Some(c.testedPath)
  180
+    }
  181
+    class NonNullCond(val testedPath: Tree) extends Cond {
  182
+      override def toString = testedPath +" ne null " +"#"+ id
  183
+    }
  184
+
  185
+    object TypeCond {
  186
+      private val uniques = new mutable.HashMap[(Tree, Type), TypeCond]
  187
+      def apply(testedPath: Tree, pt: Type): TypeCond = uniques getOrElseUpdate((testedPath, pt), new TypeCond(testedPath, pt))
  188
+      def unapply(c: TypeCond) = Some((c.testedPath, c.pt))
  189
+    }
  190
+    class TypeCond(val testedPath: Tree, val pt: Type) extends Cond {
  191
+      override def toString = testedPath +" : "+ pt +"#"+ id
  192
+    }
  193
+
  194
+//    class OuterEqCond(val testedPath: Tree, val expectedType: Type) extends Cond {
  195
+//      val expectedOuter = expectedTp.prefix match {
  196
+//        case ThisType(clazz)  => THIS(clazz)
  197
+//        case pre              => REF(pre.prefix, pre.termSymbol)
  198
+//      }
  199
+//
  200
+//      // ExplicitOuter replaces `Select(q, outerSym) OBJ_EQ expectedPrefix` by `Select(q, outerAccessor(outerSym.owner)) OBJ_EQ expectedPrefix`
  201
+//      // if there's an outer accessor, otherwise the condition becomes `true` -- TODO: can we improve needsOuterTest so there's always an outerAccessor?
  202
+//      val outer = expectedTp.typeSymbol.newMethod(vpmName.outer) setInfo expectedTp.prefix setFlag SYNTHETIC
  203
+//
  204
+//      (Select(codegen._asInstanceOf(testedBinder, expectedTp), outer)) OBJ_EQ expectedOuter
  205
+//    }
  206
+
  207
+    // TODO: improve, e.g., for constants
  208
+    def sameValue(a: Tree, b: Tree): Boolean = (a eq b) || ((a, b) match {
  209
+      case (_ : Ident, _ : Ident) => a.symbol eq b.symbol
  210
+      case _                      => false
  211
+    })
  212
+
  213
+    object IrrefutableExtractorTreeMaker {
  214
+      // will an extractor with unapply method of methodtype `tp` always succeed?
  215
+      // note: this assumes the other side-conditions implied by the extractor are met
  216
+      // (argument of the right type, length check succeeds for unapplySeq,...)
  217
+      def irrefutableExtractorType(tp: Type): Boolean = tp.resultType.dealias match {
  218
+        case TypeRef(_, SomeClass, _) => true
  219
+        // probably not useful since this type won't be inferred nor can it be written down (yet)
  220
+        case ConstantType(Constant(true)) => true
  221
+        case _ => false
  222
+      }
  223
+
  224
+      def unapply(xtm: ExtractorTreeMaker): Option[(Tree, Symbol)] = xtm match {
  225
+        case ExtractorTreeMaker(extractor, None, nextBinder) if irrefutableExtractorType(extractor.tpe) =>
  226
+          Some((extractor, nextBinder))
  227
+        case _ =>
  228
+          None
  229
+      }
  230
+    }
  231
+
  232
+    // returns (tree, tests), where `tree` will be used to refer to `root` in `tests`
  233
+    class TreeMakersToConds(val root: Symbol) {
  234
+      // 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)
  235
+      private val pointsToBound = scala.collection.mutable.HashSet(root)
  236
+      private val trees         = scala.collection.mutable.HashSet.empty[Tree]
  237
+
  238
+      // the substitution that renames variables to variables in pointsToBound
  239
+      private var normalize: Substitution  = EmptySubstitution
  240
+      private var substitutionComputed = false
  241
+
  242
+      // replaces a variable (in pointsToBound) by a selection on another variable in pointsToBound
  243
+      // in the end, instead of having x1, x1.hd, x2, x2.hd, ... flying around,
  244
+      // we want something like x1, x1.hd, x1.hd.tl, x1.hd.tl.hd, so that we can easily recognize when
  245
+      // we're testing the same variable
  246
+      // TODO check:
  247
+      //   pointsToBound -- accumSubst.from == Set(root) && (accumSubst.from.toSet -- pointsToBound) isEmpty
  248
+      private var accumSubst: Substitution = EmptySubstitution
  249
+
  250
+      // hashconsing trees (modulo value-equality)
  251
+      def unique(t: Tree, tpOverride: Type = NoType): Tree =
  252
+        trees find (a => a.correspondsStructure(t)(sameValue)) match {
  253
+          case Some(orig) =>
  254
+            // patmatDebug("unique: "+ (t eq orig, orig))
  255
+            orig
  256
+          case _ =>
  257
+            trees += t
  258
+            if (tpOverride != NoType) t setType tpOverride
  259
+            else t
  260
+        }
  261
+
  262
+      def uniqueTp(tp: Type): Type = tp match {
  263
+        // typerefs etc are already hashconsed
  264
+        case _ : UniqueType                      => tp
  265
+        case tp@RefinedType(parents, EmptyScope) => tp.memo(tp: Type)(identity) // TODO: does this help?
  266
+        case _                                   => tp
  267
+      }
  268
+
  269
+      // produce the unique tree used to refer to this binder
  270
+      // the type of the binder passed to the first invocation
  271
+      // determines the type of the tree that'll be returned for that binder as of then
  272
+      final def binderToUniqueTree(b: Symbol) =
  273
+        unique(accumSubst(normalize(CODE.REF(b))), b.tpe)
  274
+
  275
+      def /\(conds: Iterable[Cond]) = if (conds.isEmpty) TrueCond else conds.reduceLeft(AndCond(_, _))
  276
+      def \/(conds: Iterable[Cond]) = if (conds.isEmpty) FalseCond else conds.reduceLeft(OrCond(_, _))
  277
+
  278
+      // note that the sequencing of operations is important: must visit in same order as match execution
  279
+      // binderToUniqueTree uses the type of the first symbol that was encountered as the type for all future binders
  280
+      abstract class TreeMakerToCond extends (TreeMaker => Cond) {
  281
+        // requires(if (!substitutionComputed))
  282
+        def updateSubstitution(subst: Substitution): Unit = {
  283
+          // find part of substitution that replaces bound symbols by new symbols, and reverse that part
  284
+          // so that we don't introduce new aliases for existing symbols, thus keeping the set of bound symbols minimal
  285
+          val (boundSubst, unboundSubst) = (subst.from zip subst.to) partition {
  286
+            case (f, t) =>
  287
+              t.isInstanceOf[Ident] && (t.symbol ne NoSymbol) && pointsToBound(f)
  288
+          }
  289
+          val (boundFrom, boundTo) = boundSubst.unzip
  290
+          val (unboundFrom, unboundTo) = unboundSubst.unzip
  291
+
  292
+          // reverse substitution that would otherwise replace a variable we already encountered by a new variable
  293
+          // NOTE: this forgets the more precise type we have for these later variables, but that's probably okay
  294
+          normalize >>= Substitution(boundTo map (_.symbol), boundFrom map (CODE.REF(_)))
  295
+          // patmatDebug ("normalize subst: "+ normalize)
  296
+
  297
+          val okSubst = Substitution(unboundFrom, unboundTo map (normalize(_))) // it's important substitution does not duplicate trees here -- it helps to keep hash consing simple, anyway
  298
+          pointsToBound ++= ((okSubst.from, okSubst.to).zipped filter { (f, t) => pointsToBound exists (sym => t.exists(_.symbol == sym)) })._1
  299
+          // patmatDebug("pointsToBound: "+ pointsToBound)
  300
+
  301
+          accumSubst >>= okSubst
  302
+          // patmatDebug("accumSubst: "+ accumSubst)
  303
+        }
  304
+
  305
+        def handleUnknown(tm: TreeMaker): Cond
  306
+
  307
+        /** apply itself must render a faithful representation of the TreeMaker
  308
+         *
  309
+         * Concretely, TrueCond must only be used to represent a TreeMaker that is sure to match and that does not do any computation at all
  310
+         * e.g., doCSE relies on apply itself being sound in this sense (since it drops TreeMakers that are approximated to TrueCond -- SI-6077)
  311
+         *
  312
+         * handleUnknown may be customized by the caller to approximate further
  313
+         *
  314
+         * TODO: don't ignore outer-checks
  315
+         */
  316
+        def apply(tm: TreeMaker): Cond = {
  317
+          if (!substitutionComputed) updateSubstitution(tm.subPatternsAsSubstitution)
  318
+
  319
+          tm match {
  320
+            case ttm@TypeTestTreeMaker(prevBinder, testedBinder, pt, _)   =>
  321
+              object condStrategy extends TypeTestTreeMaker.TypeTestCondStrategy {
  322
+                type Result                                           = Cond
  323
+                def and(a: Result, b: Result)                         = AndCond(a, b)
  324
+                def outerTest(testedBinder: Symbol, expectedTp: Type) = TrueCond // TODO OuterEqCond(testedBinder, expectedType)
  325
+                def typeTest(b: Symbol, pt: Type) = { // a type test implies the tested path is non-null (null.isInstanceOf[T] is false for all T)
  326
+                  val p = binderToUniqueTree(b);                        AndCond(NonNullCond(p), TypeCond(p, uniqueTp(pt)))
  327
+                }
  328
+                def nonNullTest(testedBinder: Symbol)                 = NonNullCond(binderToUniqueTree(testedBinder))
  329
+                def equalsTest(pat: Tree, testedBinder: Symbol)       = EqualityCond(binderToUniqueTree(testedBinder), unique(pat))
  330
+                def eqTest(pat: Tree, testedBinder: Symbol)           = EqualityCond(binderToUniqueTree(testedBinder), unique(pat)) // TODO: eq, not ==
  331
+                def tru                                               = TrueCond
  332
+              }
  333
+              ttm.renderCondition(condStrategy)
  334
+            case EqualityTestTreeMaker(prevBinder, patTree, _)        => EqualityCond(binderToUniqueTree(prevBinder), unique(patTree))
  335
+            case AlternativesTreeMaker(_, altss, _)                   => \/(altss map (alts => /\(alts map this)))
  336
+            case ProductExtractorTreeMaker(testedBinder, None)        => NonNullCond(binderToUniqueTree(testedBinder))
  337
+            case SubstOnlyTreeMaker(_, _)                             => TrueCond
  338
+            case GuardTreeMaker(guard) =>
  339
+              guard.tpe match {
  340
+                case ConstantType(Constant(true))  => TrueCond
  341
+                case ConstantType(Constant(false)) => FalseCond
  342
+                case _                             => handleUnknown(tm)
  343
+              }
  344
+            case ExtractorTreeMaker(_, _, _) |
  345
+                 ProductExtractorTreeMaker(_, _) |
  346
+                 BodyTreeMaker(_, _)               => handleUnknown(tm)
  347
+          }
  348
+        }
  349
+      }
  350
+
  351
+
  352
+      private val irrefutableExtractor: PartialFunction[TreeMaker, Cond] = {
  353
+        // the extra condition is None, the extractor's result indicates it always succeeds,
  354
+        // (the potential type-test for the argument is represented by a separate TypeTestTreeMaker)
  355
+        case IrrefutableExtractorTreeMaker(_, _) => TrueCond
  356
+      }
  357
+
  358
+      // special-case: interpret pattern `List()` as `Nil`
  359
+      // TODO: make it more general List(1, 2) => 1 :: 2 :: Nil  -- not sure this is a good idea...
  360
+      private val rewriteListPattern: PartialFunction[TreeMaker, Cond] = {
  361
+        case p @ ExtractorTreeMaker(_, _, testedBinder)
  362
+          if testedBinder.tpe.typeSymbol == ListClass && p.checkedLength == Some(0) =>
  363
+            EqualityCond(binderToUniqueTree(p.prevBinder), unique(Ident(NilModule) setType NilModule.tpe))
  364
+      }
  365
+      val fullRewrite      = (irrefutableExtractor orElse rewriteListPattern)
  366
+      val refutableRewrite = irrefutableExtractor
  367
+
  368
+      @inline def onUnknown(handler: TreeMaker => Cond) = new TreeMakerToCond {
  369
+        def handleUnknown(tm: TreeMaker) = handler(tm)
  370
+      }
  371
+
  372
+      // used for CSE -- rewrite all unknowns to False (the most conserative option)
  373
+      object conservative extends TreeMakerToCond {
  374
+        def handleUnknown(tm: TreeMaker) = FalseCond
  375
+      }
  376
+
  377
+      final def approximateMatch(cases: List[List[TreeMaker]], treeMakerToCond: TreeMakerToCond = conservative) ={
  378
+        val testss = cases.map { _ map (tm => Test(treeMakerToCond(tm), tm)) }
  379
+        substitutionComputed = true // a second call to approximateMatch should not re-compute the substitution (would be wrong)
  380
+        testss
  381
+      }
  382
+    }
  383
+
  384
+    def approximateMatchConservative(root: Symbol, cases: List[List[TreeMaker]]): List[List[Test]] =
  385
+      (new TreeMakersToConds(root)).approximateMatch(cases)
  386
+
  387
+    def prepareNewAnalysis() = { Var.resetUniques(); Const.resetUniques() }
  388
+
  389
+    object Var {
  390
+      private var _nextId = 0
  391
+      def nextId = {_nextId += 1; _nextId}
  392
+
  393
+      def resetUniques() = {_nextId = 0; uniques.clear()}
  394
+      private val uniques = new mutable.HashMap[Tree, Var]
  395
+      def apply(x: Tree): Var = uniques getOrElseUpdate(x, new Var(x, x.tpe))
  396
+    }
  397
+    class Var(val path: Tree, staticTp: Type) extends AbsVar {
  398
+      private[this] val id: Int = Var.nextId
  399
+
  400
+      // private[this] var canModify: Option[Array[StackTraceElement]] = None
  401
+      private[this] def ensureCanModify() = {} //if (canModify.nonEmpty) patmatDebug("BUG!"+ this +" modified after having been observed: "+ canModify.get.mkString("\n"))
  402
+
  403
+      private[this] def observed() = {} //canModify = Some(Thread.currentThread.getStackTrace)
  404
+
  405
+      // don't access until all potential equalities have been registered using registerEquality
  406
+      private[this] val symForEqualsTo = new mutable.HashMap[Const, Sym]
  407
+
  408
+      // when looking at the domain, we only care about types we can check at run time
  409
+      val staticTpCheckable: Type = checkableType(staticTp)
  410
+
  411
+      private[this] var _mayBeNull = false
  412
+      def registerNull(): Unit = { ensureCanModify; if (NullTp <:< staticTpCheckable) _mayBeNull = true }
  413
+      def mayBeNull: Boolean = _mayBeNull
  414
+
  415
+      // case None => domain is unknown,
  416
+      // case Some(List(tps: _*)) => domain is exactly tps
  417
+      // we enumerate the subtypes of the full type, as that allows us to filter out more types statically,
  418
+      // once we go to run-time checks (on Const's), convert them to checkable types
  419
+      // TODO: there seems to be bug for singleton domains (variable does not show up in model)
  420
+      lazy val domain: Option[Set[Const]] = {
  421
+        val subConsts = enumerateSubtypes(staticTp).map{ tps =>
  422
+          tps.toSet[Type].map{ tp =>
  423
+            val domainC = TypeConst(tp)
  424
+            registerEquality(domainC)
  425
+            domainC
  426
+          }
  427
+        }
  428
+
  429
+        val allConsts =
  430
+          if (mayBeNull) {
  431
+            registerEquality(NullConst)
  432
+            subConsts map (_ + NullConst)
  433
+          } else
  434
+            subConsts
  435
+
  436
+        observed; allConsts
  437
+      }
  438
+
  439
+      // populate equalitySyms
  440
+      // don't care about the result, but want only one fresh symbol per distinct constant c
  441
+      def registerEquality(c: Const): Unit = {ensureCanModify; symForEqualsTo getOrElseUpdate(c, Sym(this, c))}
  442
+
  443
+      // return the symbol that represents this variable being equal to the constant `c`, if it exists, otherwise False (for robustness)
  444
+      // (registerEquality(c) must have been called prior, either when constructing the domain or from outside)
  445
+      def propForEqualsTo(c: Const): Prop = {observed; symForEqualsTo.getOrElse(c, False)}
  446
+
  447
+      // [implementation NOTE: don't access until all potential equalities have been registered using registerEquality]p
  448
+      /** the information needed to construct the boolean proposition that encods the equality proposition (V = C)
  449
+       *
  450
+       * that models a type test pattern `_: C` or constant pattern `C`, where the type test gives rise to a TypeConst C,
  451
+       * and the constant pattern yields a ValueConst C
  452
+       *
  453
+       * for exhaustivity, we really only need implication (e.g., V = 1 implies that V = 1 /\ V = Int, if both tests occur in the match,
  454
+       * and thus in this variable's equality symbols), but reachability also requires us to model things like V = 1 precluding V = "1"
  455
+       */
  456
+      lazy val implications = {
  457
+        /** when we know V = C, which other equalities must hold
  458
+         *
  459
+         * in general, equality to some type implies equality to its supertypes
  460
+         * (this multi-valued kind of equality is necessary for unreachability)
  461
+         * note that we use subtyping as a model for implication between instanceof tests
  462
+         * i.e., when S <:< T we assume x.isInstanceOf[S] implies x.isInstanceOf[T]
  463
+         * unfortunately this is not true in general (see e.g. SI-6022)
  464
+         */
  465
+        def implies(lower: Const, upper: Const): Boolean =
  466
+          // values and null
  467
+            lower == upper ||
  468
+          // type implication
  469
+            (lower != NullConst && !upper.isValue &&
  470
+             instanceOfTpImplies(if (lower.isValue) lower.wideTp else lower.tp, upper.tp))
  471
+
  472
+          // if(r) patmatDebug("implies    : "+(lower, lower.tp, upper, upper.tp))
  473
+          // else  patmatDebug("NOT implies: "+(lower, upper))
  474
+
  475
+
  476
+        /** does V = C preclude V having value `other`?
  477
+         (1) V = null is an exclusive assignment,
  478
+         (2) V = A and V = B, for A and B value constants, are mutually exclusive unless A == B
  479
+             we err on the safe side, for example:
  480
+               - assume `val X = 1; val Y = 1`, then
  481
+                 (2: Int) match { case X => case Y =>  <falsely considered reachable>  }
  482
+               - V = 1 does not preclude V = Int, or V = Any, it could be said to preclude V = String, but we don't model that
  483
+
  484
+         (3) for types we could try to do something fancy, but be conservative and just say no
  485
+         */
  486
+        def excludes(a: Const, b: Const): Boolean =
  487
+          a != b && ((a == NullConst || b == NullConst) || (a.isValue && b.isValue))
  488
+
  489
+          // if(r) patmatDebug("excludes    : "+(a, a.tp, b, b.tp))
  490
+          // else  patmatDebug("NOT excludes: "+(a, b))
  491
+
  492
+/*
  493
+[ HALF BAKED FANCINESS: //!equalitySyms.exists(common => implies(common.const, a) && implies(common.const, b)))
  494
+ when type tests are involved, we reason (conservatively) under a closed world assumption,
  495
+ since we are really only trying to counter the effects of the symbols that we introduce to model type tests
  496
+ we don't aim to model the whole subtyping hierarchy, simply to encode enough about subtyping to do unreachability properly
  497
+
  498
+ consider the following hierarchy:
  499
+
  500
+    trait A
  501
+    trait B
  502
+    trait C
  503
+    trait AB extends B with A
  504
+
  505
+  // two types are mutually exclusive if there is no equality symbol whose constant implies both
  506
+  object Test extends App {
  507
+    def foo(x: Any) = x match {
  508
+      case _ : C  => println("C")
  509
+      case _ : AB => println("AB")
  510
+      case _ : (A with B) => println("AB'")