From 7fdc873c06ac4bacd8447af12495333bd30a0f3c Mon Sep 17 00:00:00 2001 From: Adriaan Moors Date: Tue, 12 Feb 2013 15:49:58 -0800 Subject: [PATCH] [refactor] move some logic-related code --- .../tools/nsc/transform/patmat/Logic.scala | 337 ++++++++++++++++- .../nsc/transform/patmat/MatchAnalysis.scala | 354 +----------------- .../transform/patmat/MatchTreeMakers.scala | 19 + 3 files changed, 358 insertions(+), 352 deletions(-) diff --git a/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala b/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala index 6a890c5bb53d..23c0272a30c1 100644 --- a/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala +++ b/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala @@ -52,7 +52,8 @@ trait Logic { self: PatternMatching => // http://www.cis.upenn.edu/~cis510/tcl/chap3.pdf // http://users.encs.concordia.ca/~ta_ahmed/ms_thesis.pdf - trait FirstOrderLogic { + // propositional logic with constants and equality + trait PropositionalLogic { class Prop case class Eq(p: Var, q: Const) extends Prop @@ -297,7 +298,7 @@ trait Logic { self: PatternMatching => def findAllModelsFor(f: Formula): List[Model] } - trait CNF extends FirstOrderLogic { + 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] { @@ -404,7 +405,6 @@ trait Logic { self: PatternMatching => // patmatDebug("cnf for\n"+ p +"\nis:\n"+cnfString(res)) res } - } trait DPLLSolver extends CNF { @@ -524,4 +524,335 @@ trait Logic { self: PatternMatching => satisfiableWithModel } } + + trait TreesAndTypesDomain extends PropositionalLogic with CheckableTreeAndTypeAnalysis { + // resets hash consing -- only supposed to be called by TreeMakersToProps + def prepareNewAnalysis(): Unit = { Var.resetUniques(); Const.resetUniques() } + + object Var extends VarExtractor { + private var _nextId = 0 + def nextId = {_nextId += 1; _nextId} + + def resetUniques() = {_nextId = 0; uniques.clear()} + private val uniques = new mutable.HashMap[Tree, Var] + def apply(x: Tree): Var = uniques getOrElseUpdate(x, new Var(x, x.tpe)) + def unapply(v: Var) = Some(v.path) + } + class Var(val path: Tree, staticTp: Type) extends AbsVar { + private[this] val id: Int = Var.nextId + + // private[this] var canModify: Option[Array[StackTraceElement]] = None + private[this] def ensureCanModify() = {} //if (canModify.nonEmpty) patmatDebug("BUG!"+ this +" modified after having been observed: "+ canModify.get.mkString("\n")) + + 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 mutable.HashMap[Const, Sym] + + // when looking at the domain, we only care about types we can check at run time + val staticTpCheckable: Type = checkableType(staticTp) + + private[this] var _mayBeNull = false + def registerNull(): Unit = { ensureCanModify; if (NullTp <:< staticTpCheckable) _mayBeNull = true } + def mayBeNull: Boolean = _mayBeNull + + // 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) + lazy val domain: Option[Set[Const]] = { + val subConsts = enumerateSubtypes(staticTp).map{ tps => + tps.toSet[Type].map{ tp => + val domainC = TypeConst(tp) + registerEquality(domainC) + domainC + } + } + + val allConsts = + if (mayBeNull) { + registerEquality(NullConst) + subConsts map (_ + NullConst) + } else + subConsts + + observed; allConsts + } + + // 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))} + + // 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)} + + // [implementation NOTE: don't access until all potential equalities have been registered using registerEquality]p + /** the information needed to construct the boolean proposition that encods the equality proposition (V = C) + * + * that models a type test pattern `_: C` or constant pattern `C`, where the type test gives rise to a TypeConst C, + * and the constant pattern yields a ValueConst C + * + * for exhaustivity, we really only need implication (e.g., V = 1 implies that V = 1 /\ V = Int, if both tests occur in the match, + * and thus in this variable's equality symbols), but reachability also requires us to model things like V = 1 precluding V = "1" + */ + lazy val implications = { + /** when we know V = C, which other equalities must hold + * + * in general, equality to some type implies equality to its supertypes + * (this multi-valued kind of equality is necessary for unreachability) + * note that we use subtyping as a model for implication between instanceof tests + * i.e., when S <:< T we assume x.isInstanceOf[S] implies x.isInstanceOf[T] + * unfortunately this is not true in general (see e.g. SI-6022) + */ + def implies(lower: Const, upper: Const): Boolean = + // values and null + lower == upper || + // type implication + (lower != NullConst && !upper.isValue && + instanceOfTpImplies(if (lower.isValue) lower.wideTp else lower.tp, upper.tp)) + + // if(r) patmatDebug("implies : "+(lower, lower.tp, upper, upper.tp)) + // else patmatDebug("NOT implies: "+(lower, upper)) + + + /** does V = C preclude V having value `other`? + (1) V = null is an exclusive assignment, + (2) V = A and V = B, for A and B value constants, are mutually exclusive unless A == B + we err on the safe side, for example: + - assume `val X = 1; val Y = 1`, then + (2: Int) match { case X => case Y => } + - V = 1 does not preclude V = Int, or V = Any, it could be said to preclude V = String, but we don't model that + + (3) for types we could try to do something fancy, but be conservative and just say no + */ + def excludes(a: Const, b: Const): Boolean = + a != b && ((a == NullConst || b == NullConst) || (a.isValue && b.isValue)) + + // if(r) patmatDebug("excludes : "+(a, a.tp, b, b.tp)) + // else patmatDebug("NOT excludes: "+(a, b)) + +/* +[ HALF BAKED FANCINESS: //!equalitySyms.exists(common => implies(common.const, a) && implies(common.const, b))) + when type tests are involved, we reason (conservatively) under a closed world assumption, + since we are really only trying to counter the effects of the symbols that we introduce to model type tests + we don't aim to model the whole subtyping hierarchy, simply to encode enough about subtyping to do unreachability properly + + consider the following hierarchy: + + trait A + trait B + trait C + trait AB extends B with A + + // two types are mutually exclusive if there is no equality symbol whose constant implies both + object Test extends App { + def foo(x: Any) = x match { + case _ : C => println("C") + case _ : AB => println("AB") + case _ : (A with B) => println("AB'") + case _ : B => println("B") + case _ : A => println("A") + } + + of course this kind of reasoning is not true in general, + but we can safely pretend types are mutually exclusive as long as there are no counter-examples in the match we're analyzing} +*/ + + val excludedPair = new mutable.HashSet[ExcludedPair] + + 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 + } + // make ExcludedPair(a, b).hashCode == ExcludedPair(b, a).hashCode + override def hashCode = a.hashCode ^ b.hashCode + } + + equalitySyms map { sym => + // 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 = equalitySyms filterNot (b => (b.const == sym.const) || excludedPair(ExcludedPair(b.const, sym.const))) + val (excluded, notExcluded) = todo partition (b => excludes(sym.const, b.const)) + val implied = notExcluded filter (b => implies(sym.const, b.const)) + + patmatDebug("eq axioms for: "+ sym.const) + patmatDebug("excluded: "+ excluded) + patmatDebug("implied: "+ implied) + + excluded foreach { excludedSym => excludedPair += ExcludedPair(sym.const, excludedSym.const)} + + (sym, implied, excluded) + } + } + + // accessing after calling registerNull will result in inconsistencies + lazy val domainSyms: Option[Set[Sym]] = domain map { _ map symForEqualsTo } + + lazy val symForStaticTp: Option[Sym] = symForEqualsTo.get(TypeConst(staticTpCheckable)) + + // don't access until all potential equalities have been registered using registerEquality + private lazy val equalitySyms = {observed; symForEqualsTo.values.toList} + + // don't call until all equalities have been registered and registerNull has been called (if needed) + def describe = { + def domain_s = domain match { + case Some(d) => d mkString (" ::= ", " | ", "// "+ symForEqualsTo.keys) + case _ => symForEqualsTo.keys mkString (" ::= ", " | ", " | ...") + } + s"$this: ${staticTp}${domain_s} // = $path" + } + override def toString = "V"+ id + } + + + import global.{ConstantType, Constant, SingletonType, Literal, Ident, singleType} + import global.definitions.{AnyClass, UnitClass} + + + // 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) + object Const { + def resetUniques() = {_nextTypeId = 0; _nextValueId = 0; uniques.clear() ; trees.clear()} + + private var _nextTypeId = 0 + def nextTypeId = {_nextTypeId += 1; _nextTypeId} + + private var _nextValueId = 0 + def nextValueId = {_nextValueId += 1; _nextValueId} + + private val uniques = new mutable.HashMap[Type, Const] + private[TreesAndTypesDomain] def unique(tp: Type, mkFresh: => Const): Const = + uniques.get(tp).getOrElse( + uniques.find {case (oldTp, oldC) => oldTp =:= tp} match { + case Some((_, c)) => + patmatDebug("unique const: "+ (tp, c)) + c + case _ => + val fresh = mkFresh + patmatDebug("uniqued const: "+ (tp, fresh)) + uniques(tp) = fresh + fresh + }) + + private val trees = mutable.HashSet.empty[Tree] + + // hashconsing trees (modulo value-equality) + private[TreesAndTypesDomain] def uniqueTpForTree(t: Tree): Type = + // a new type for every unstable symbol -- only stable value are uniqued + // technically, an unreachable value may change between cases + // thus, the failure of a case that matches on a mutable value does not exclude the next case succeeding + // (and thuuuuus, the latter case must be considered reachable) + if (!t.symbol.isStable) t.tpe.narrow + else trees find (a => a.correspondsStructure(t)(sameValue)) match { + case Some(orig) => + patmatDebug("unique tp for tree: "+ (orig, orig.tpe)) + orig.tpe + case _ => + // duplicate, don't mutate old tree (TODO: use a map tree -> type instead?) + val treeWithNarrowedType = t.duplicate setType t.tpe.narrow + patmatDebug("uniqued: "+ (t, t.tpe, treeWithNarrowedType.tpe)) + trees += treeWithNarrowedType + treeWithNarrowedType.tpe + } + } + + sealed abstract class Const { + def tp: Type + def wideTp: Type + + def isAny = wideTp.typeSymbol == AnyClass + def isValue: Boolean //= tp.isStable + + // note: use reference equality on Const since they're hash-consed (doing type equality all the time is too expensive) + // the equals inherited from AnyRef does just this + } + + // find most precise super-type of tp that is a class + // we skip non-class types (singleton types, abstract types) so that we can + // correctly compute how types relate in terms of the values they rule out + // e.g., when we know some value must be of type T, can it still be of type S? (this is the positive formulation of what `excludes` on Const computes) + // since we're talking values, there must have been a class involved in creating it, so rephrase our types in terms of classes + // (At least conceptually: `true` is an instance of class `Boolean`) + private def widenToClass(tp: Type): Type = + if (tp.typeSymbol.isClass) tp + else tp.baseType(tp.baseClasses.head) + + object TypeConst extends TypeConstExtractor { + 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 = widenToClass(tp) + def isValue = false + override def toString = tp.toString //+"#"+ id + } + + // p is a unique type or a constant value + object ValueConst extends ValueConstExtractor { + 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 = widenToClass(tp) + + val narrowTp = + if (tp.isInstanceOf[SingletonType]) tp + else p match { + case Literal(c) => + if (c.tpe.typeSymbol == UnitClass) c.tpe + else ConstantType(c) + case Ident(_) if p.symbol.isStable => + // for Idents, can encode uniqueness of symbol as uniqueness of the corresponding singleton type + // for Selects, which are handled by the next case, the prefix of the select varies independently of the symbol (see pos/virtpatmat_unreach_select.scala) + singleType(tp.prefix, p.symbol) + case _ => + Const.uniqueTpForTree(p) + } + + val toString = + if (hasStableSymbol(p)) 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)) // TODO: assert(!tp.isStable) + /*private[this] val id: Int = */Const.nextValueId + def isValue = true + } + + + lazy val NullTp = ConstantType(Constant(null)) + case object NullConst extends Const { + def tp = NullTp + def wideTp = NullTp + + def isValue = true + override def toString = "null" + } + } } \ No newline at end of file diff --git a/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala b/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala index 421207f24f26..1e12975880d5 100644 --- a/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala +++ b/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala @@ -19,7 +19,7 @@ import scala.reflect.internal.util.Statistics import scala.reflect.internal.Types import scala.reflect.internal.util.HashSet -trait TypeAnalysis extends Debugging { +trait TreeAndTypeAnalysis extends Debugging { val global: Global import global.{Tree, Type, Symbol, definitions, analyzer, ConstantType, Literal, Constant, appliedType, WildcardType, TypeRef, ModuleClassSymbol, @@ -54,7 +54,7 @@ trait TypeAnalysis extends Debugging { case _ => false }) - trait CheckableTypeAnalysis { + trait CheckableTreeAndTypeAnalysis { val typer: Typer // TODO: domain of other feasibly enumerable built-in types (char?) @@ -135,7 +135,7 @@ trait TypeAnalysis extends Debugging { } } -trait Analysis extends TypeAnalysis { self: PatternMatching => +trait Analysis extends TreeAndTypeAnalysis { self: PatternMatching => import PatternMatchingStats._ val global: Global import global.{Tree, Type, Symbol, CaseDef, Position, atPos, NoPosition, @@ -154,7 +154,7 @@ trait Analysis extends TypeAnalysis { self: PatternMatching => * 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 FirstOrderLogic with CheckableTypeAnalysis { self: CodegenCore => + trait TreeMakerApproximation extends TreeMakers with PropositionalLogic with TreesAndTypesDomain with CheckableTreeAndTypeAnalysis { self: CodegenCore => object Test { var currId = 0 } @@ -173,25 +173,6 @@ trait Analysis extends TypeAnalysis { self: PatternMatching => } - object IrrefutableExtractorTreeMaker { - // will an extractor with unapply method of methodtype `tp` always succeed? - // note: this assumes the other side-conditions implied by the extractor are met - // (argument of the right type, length check succeeds for unapplySeq,...) - def irrefutableExtractorType(tp: Type): Boolean = tp.resultType.dealias match { - case TypeRef(_, SomeClass, _) => true - // probably not useful since this type won't be inferred nor can it be written down (yet) - case ConstantType(Constant(true)) => true - case _ => false - } - - def unapply(xtm: ExtractorTreeMaker): Option[(Tree, Symbol)] = xtm match { - case ExtractorTreeMaker(extractor, None, nextBinder) if irrefutableExtractorType(extractor.tpe) => - Some((extractor, nextBinder)) - case _ => - None - } - } - class TreeMakersToPropsIgnoreNullChecks(root: Symbol) extends TreeMakersToProps(root) { override def uniqueNonNullProp(p: Tree): Prop = True } @@ -364,331 +345,6 @@ trait Analysis extends TypeAnalysis { self: PatternMatching => def approximateMatchConservative(root: Symbol, cases: List[List[TreeMaker]]): List[List[Test]] = (new TreeMakersToProps(root)).approximateMatch(cases) - // resets hash consing -- only supposed to be called by TreeMakersToProps - def prepareNewAnalysis(): Unit = { Var.resetUniques(); Const.resetUniques() } - - object Var extends VarExtractor { - private var _nextId = 0 - def nextId = {_nextId += 1; _nextId} - - def resetUniques() = {_nextId = 0; uniques.clear()} - private val uniques = new mutable.HashMap[Tree, Var] - def apply(x: Tree): Var = uniques getOrElseUpdate(x, new Var(x, x.tpe)) - def unapply(v: Var) = Some(v.path) - } - class Var(val path: Tree, staticTp: Type) extends AbsVar { - private[this] val id: Int = Var.nextId - - // private[this] var canModify: Option[Array[StackTraceElement]] = None - private[this] def ensureCanModify() = {} //if (canModify.nonEmpty) patmatDebug("BUG!"+ this +" modified after having been observed: "+ canModify.get.mkString("\n")) - - 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 mutable.HashMap[Const, Sym] - - // when looking at the domain, we only care about types we can check at run time - val staticTpCheckable: Type = checkableType(staticTp) - - private[this] var _mayBeNull = false - def registerNull(): Unit = { ensureCanModify; if (NullTp <:< staticTpCheckable) _mayBeNull = true } - def mayBeNull: Boolean = _mayBeNull - - // 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) - lazy val domain: Option[Set[Const]] = { - val subConsts = enumerateSubtypes(staticTp).map{ tps => - tps.toSet[Type].map{ tp => - val domainC = TypeConst(tp) - registerEquality(domainC) - domainC - } - } - - val allConsts = - if (mayBeNull) { - registerEquality(NullConst) - subConsts map (_ + NullConst) - } else - subConsts - - observed; allConsts - } - - // 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))} - - // 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)} - - // [implementation NOTE: don't access until all potential equalities have been registered using registerEquality]p - /** the information needed to construct the boolean proposition that encods the equality proposition (V = C) - * - * that models a type test pattern `_: C` or constant pattern `C`, where the type test gives rise to a TypeConst C, - * and the constant pattern yields a ValueConst C - * - * for exhaustivity, we really only need implication (e.g., V = 1 implies that V = 1 /\ V = Int, if both tests occur in the match, - * and thus in this variable's equality symbols), but reachability also requires us to model things like V = 1 precluding V = "1" - */ - lazy val implications = { - /** when we know V = C, which other equalities must hold - * - * in general, equality to some type implies equality to its supertypes - * (this multi-valued kind of equality is necessary for unreachability) - * note that we use subtyping as a model for implication between instanceof tests - * i.e., when S <:< T we assume x.isInstanceOf[S] implies x.isInstanceOf[T] - * unfortunately this is not true in general (see e.g. SI-6022) - */ - def implies(lower: Const, upper: Const): Boolean = - // values and null - lower == upper || - // type implication - (lower != NullConst && !upper.isValue && - instanceOfTpImplies(if (lower.isValue) lower.wideTp else lower.tp, upper.tp)) - - // if(r) patmatDebug("implies : "+(lower, lower.tp, upper, upper.tp)) - // else patmatDebug("NOT implies: "+(lower, upper)) - - - /** does V = C preclude V having value `other`? - (1) V = null is an exclusive assignment, - (2) V = A and V = B, for A and B value constants, are mutually exclusive unless A == B - we err on the safe side, for example: - - assume `val X = 1; val Y = 1`, then - (2: Int) match { case X => case Y => } - - V = 1 does not preclude V = Int, or V = Any, it could be said to preclude V = String, but we don't model that - - (3) for types we could try to do something fancy, but be conservative and just say no - */ - def excludes(a: Const, b: Const): Boolean = - a != b && ((a == NullConst || b == NullConst) || (a.isValue && b.isValue)) - - // if(r) patmatDebug("excludes : "+(a, a.tp, b, b.tp)) - // else patmatDebug("NOT excludes: "+(a, b)) - -/* -[ HALF BAKED FANCINESS: //!equalitySyms.exists(common => implies(common.const, a) && implies(common.const, b))) - when type tests are involved, we reason (conservatively) under a closed world assumption, - since we are really only trying to counter the effects of the symbols that we introduce to model type tests - we don't aim to model the whole subtyping hierarchy, simply to encode enough about subtyping to do unreachability properly - - consider the following hierarchy: - - trait A - trait B - trait C - trait AB extends B with A - - // two types are mutually exclusive if there is no equality symbol whose constant implies both - object Test extends App { - def foo(x: Any) = x match { - case _ : C => println("C") - case _ : AB => println("AB") - case _ : (A with B) => println("AB'") - case _ : B => println("B") - case _ : A => println("A") - } - - of course this kind of reasoning is not true in general, - but we can safely pretend types are mutually exclusive as long as there are no counter-examples in the match we're analyzing} -*/ - - val excludedPair = new mutable.HashSet[ExcludedPair] - - 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 - } - // make ExcludedPair(a, b).hashCode == ExcludedPair(b, a).hashCode - override def hashCode = a.hashCode ^ b.hashCode - } - - equalitySyms map { sym => - // 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 = equalitySyms filterNot (b => (b.const == sym.const) || excludedPair(ExcludedPair(b.const, sym.const))) - val (excluded, notExcluded) = todo partition (b => excludes(sym.const, b.const)) - val implied = notExcluded filter (b => implies(sym.const, b.const)) - - patmatDebug("eq axioms for: "+ sym.const) - patmatDebug("excluded: "+ excluded) - patmatDebug("implied: "+ implied) - - excluded foreach { excludedSym => excludedPair += ExcludedPair(sym.const, excludedSym.const)} - - (sym, implied, excluded) - } - } - - // accessing after calling registerNull will result in inconsistencies - lazy val domainSyms: Option[Set[Sym]] = domain map { _ map symForEqualsTo } - - lazy val symForStaticTp: Option[Sym] = symForEqualsTo.get(TypeConst(staticTpCheckable)) - - // don't access until all potential equalities have been registered using registerEquality - private lazy val equalitySyms = {observed; symForEqualsTo.values.toList} - - // don't call until all equalities have been registered and registerNull has been called (if needed) - def describe = { - def domain_s = domain match { - case Some(d) => d mkString (" ::= ", " | ", "// "+ symForEqualsTo.keys) - case _ => symForEqualsTo.keys mkString (" ::= ", " | ", " | ...") - } - s"$this: ${staticTp}${domain_s} // = $path" - } - override def toString = "V"+ id - } - - - // 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) - object Const { - def resetUniques() = {_nextTypeId = 0; _nextValueId = 0; uniques.clear() ; trees.clear()} - - private var _nextTypeId = 0 - def nextTypeId = {_nextTypeId += 1; _nextTypeId} - - private var _nextValueId = 0 - def nextValueId = {_nextValueId += 1; _nextValueId} - - private val uniques = new mutable.HashMap[Type, Const] - private[TreeMakerApproximation] def unique(tp: Type, mkFresh: => Const): Const = - uniques.get(tp).getOrElse( - uniques.find {case (oldTp, oldC) => oldTp =:= tp} match { - case Some((_, c)) => - patmatDebug("unique const: "+ (tp, c)) - c - case _ => - val fresh = mkFresh - patmatDebug("uniqued const: "+ (tp, fresh)) - uniques(tp) = fresh - fresh - }) - - private val trees = mutable.HashSet.empty[Tree] - - // hashconsing trees (modulo value-equality) - private[TreeMakerApproximation] def uniqueTpForTree(t: Tree): Type = - // a new type for every unstable symbol -- only stable value are uniqued - // technically, an unreachable value may change between cases - // thus, the failure of a case that matches on a mutable value does not exclude the next case succeeding - // (and thuuuuus, the latter case must be considered reachable) - if (!t.symbol.isStable) t.tpe.narrow - else trees find (a => a.correspondsStructure(t)(sameValue)) match { - case Some(orig) => - patmatDebug("unique tp for tree: "+ (orig, orig.tpe)) - orig.tpe - case _ => - // duplicate, don't mutate old tree (TODO: use a map tree -> type instead?) - val treeWithNarrowedType = t.duplicate setType t.tpe.narrow - patmatDebug("uniqued: "+ (t, t.tpe, treeWithNarrowedType.tpe)) - trees += treeWithNarrowedType - treeWithNarrowedType.tpe - } - } - - sealed abstract class Const { - def tp: Type - def wideTp: Type - - def isAny = wideTp.typeSymbol == AnyClass - def isValue: Boolean //= tp.isStable - - // note: use reference equality on Const since they're hash-consed (doing type equality all the time is too expensive) - // the equals inherited from AnyRef does just this - } - - // find most precise super-type of tp that is a class - // we skip non-class types (singleton types, abstract types) so that we can - // correctly compute how types relate in terms of the values they rule out - // e.g., when we know some value must be of type T, can it still be of type S? (this is the positive formulation of what `excludes` on Const computes) - // since we're talking values, there must have been a class involved in creating it, so rephrase our types in terms of classes - // (At least conceptually: `true` is an instance of class `Boolean`) - private def widenToClass(tp: Type): Type = - if (tp.typeSymbol.isClass) tp - else tp.baseType(tp.baseClasses.head) - - object TypeConst extends TypeConstExtractor { - 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 = widenToClass(tp) - def isValue = false - override def toString = tp.toString //+"#"+ id - } - - // p is a unique type or a constant value - object ValueConst extends ValueConstExtractor { - 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 = widenToClass(tp) - - val narrowTp = - if (tp.isInstanceOf[SingletonType]) tp - else p match { - case Literal(c) => - if (c.tpe.typeSymbol == UnitClass) c.tpe - else ConstantType(c) - case Ident(_) if p.symbol.isStable => - // for Idents, can encode uniqueness of symbol as uniqueness of the corresponding singleton type - // for Selects, which are handled by the next case, the prefix of the select varies independently of the symbol (see pos/virtpatmat_unreach_select.scala) - singleType(tp.prefix, p.symbol) - case _ => - Const.uniqueTpForTree(p) - } - - val toString = - if (hasStableSymbol(p)) 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)) // TODO: assert(!tp.isStable) - /*private[this] val id: Int = */Const.nextValueId - def isValue = true - } - - lazy val NullTp = ConstantType(Constant(null)) - case object NullConst extends Const { - def tp = NullTp - 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 protected final def caseWithoutBodyToProp(tests: List[Test]): Prop = @@ -706,7 +362,7 @@ trait Analysis extends TypeAnalysis { self: PatternMatching => } trait SymbolicMatchAnalysis extends TreeMakerApproximation { self: CodegenCore => - // 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 + // 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 diff --git a/src/compiler/scala/tools/nsc/transform/patmat/MatchTreeMakers.scala b/src/compiler/scala/tools/nsc/transform/patmat/MatchTreeMakers.scala index 575e53123158..b334a6b22856 100644 --- a/src/compiler/scala/tools/nsc/transform/patmat/MatchTreeMakers.scala +++ b/src/compiler/scala/tools/nsc/transform/patmat/MatchTreeMakers.scala @@ -279,6 +279,25 @@ trait TreeMaking { self: PatternMatching => override def toString = "P"+(prevBinder.name, extraCond getOrElse "", localSubstitution) } + object IrrefutableExtractorTreeMaker { + // will an extractor with unapply method of methodtype `tp` always succeed? + // note: this assumes the other side-conditions implied by the extractor are met + // (argument of the right type, length check succeeds for unapplySeq,...) + def irrefutableExtractorType(tp: Type): Boolean = tp.resultType.dealias match { + case TypeRef(_, SomeClass, _) => true + // probably not useful since this type won't be inferred nor can it be written down (yet) + case ConstantType(Constant(true)) => true + case _ => false + } + + def unapply(xtm: ExtractorTreeMaker): Option[(Tree, Symbol)] = xtm match { + case ExtractorTreeMaker(extractor, None, nextBinder) if irrefutableExtractorType(extractor.tpe) => + Some((extractor, nextBinder)) + case _ => + None + } + } + object TypeTestTreeMaker { // factored out so that we can consistently generate other representations of the tree that implements the test // (e.g. propositions for exhaustivity and friends, boolean for isPureTypeTest)