From 66220c91094e9d5a97d0f92780f6e934155aaa6c Mon Sep 17 00:00:00 2001 From: Adriaan Moors Date: Tue, 22 May 2012 18:38:14 +0200 Subject: all treemakers need positions for unreachable error --- .../tools/nsc/typechecker/PatternMatching.scala | 22 ++++++++++++++++------ 1 file changed, 16 insertions(+), 6 deletions(-) diff --git a/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala b/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala index b36a92a186..63547a84eb 100644 --- a/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala +++ b/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala @@ -793,6 +793,8 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL None abstract class TreeMaker { + def pos: Position + /** captures the scope and the value of the bindings in patterns * important *when* the substitution happens (can't accumulate and do at once after the full matcher has been constructed) */ @@ -820,16 +822,22 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL } case class TrivialTreeMaker(tree: Tree) extends TreeMaker with NoNewBinders { + def pos = tree.pos + def chainBefore(next: Tree)(casegen: Casegen): Tree = tree } case class BodyTreeMaker(body: Tree, matchPt: Type) extends TreeMaker with NoNewBinders { + def pos = body.pos + def chainBefore(next: Tree)(casegen: Casegen): Tree = // assert(next eq EmptyTree) atPos(body.pos)(casegen.one(substitution(body))) // since SubstOnly treemakers are dropped, need to do it here override def toString = "B"+(body, matchPt) } case class SubstOnlyTreeMaker(prevBinder: Symbol, nextBinder: Symbol) extends TreeMaker { + val pos = NoPosition + val localSubstitution = Substitution(prevBinder, CODE.REF(nextBinder)) def chainBefore(next: Tree)(casegen: Casegen): Tree = substitution(next) override def toString = "S"+ localSubstitution @@ -837,10 +845,10 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL abstract class FunTreeMaker extends TreeMaker { val nextBinder: Symbol + def pos = nextBinder.pos } abstract class CondTreeMaker extends FunTreeMaker { - val pos: Position val prevBinder: Symbol val nextBinderTp: Type val cond: Tree @@ -962,9 +970,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL - A parameterized type pattern scala.Array[T1], where T1 is a type pattern. // TODO This type pattern matches any non-null instance of type scala.Array[U1], where U1 is a type matched by T1. **/ - case class TypeTestTreeMaker(prevBinder: Symbol, testedBinder: Symbol, expectedTp: Type, nextBinderTp: Type)(_pos: Position, extractorArgTypeTest: Boolean = false) extends CondTreeMaker { - val pos = _pos - + case class TypeTestTreeMaker(prevBinder: Symbol, testedBinder: Symbol, expectedTp: Type, nextBinderTp: Type)(override val pos: Position, extractorArgTypeTest: Boolean = false) extends CondTreeMaker { import TypeTestTreeMaker._ // println("TTTM"+(prevBinder, extractorArgTypeTest, testedBinder, expectedTp, nextBinderTp)) @@ -1023,7 +1029,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL } // need to substitute to deal with existential types -- TODO: deal with existentials better, don't substitute (see RichClass during quick.comp) - case class EqualityTestTreeMaker(prevBinder: Symbol, patTree: Tree, pos: Position) extends CondTreeMaker { + case class EqualityTestTreeMaker(prevBinder: Symbol, patTree: Tree, override val pos: Position) extends CondTreeMaker { val nextBinderTp = prevBinder.info.widen // NOTE: generate `patTree == patBinder`, since the extractor must be in control of the equals method (also, patBinder may be null) @@ -1056,6 +1062,8 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL } case class GuardTreeMaker(guardTree: Tree) extends TreeMaker with NoNewBinders { + val pos = guardTree.pos + def chainBefore(next: Tree)(casegen: Casegen): Tree = casegen.flatMapGuard(substitution(guardTree), next) override def toString = "G("+ guardTree +")" } @@ -2366,7 +2374,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL object ReusedCondTreeMaker { def apply(orig: CondTreeMaker) = new ReusedCondTreeMaker(orig.prevBinder, orig.nextBinder, orig.cond, orig.res, orig.pos) } - class ReusedCondTreeMaker(prevBinder: Symbol, val nextBinder: Symbol, cond: Tree, res: Tree, pos: Position) extends TreeMaker { import CODE._ + class ReusedCondTreeMaker(prevBinder: Symbol, val nextBinder: Symbol, cond: Tree, res: Tree, val pos: Position) extends TreeMaker { import CODE._ lazy val localSubstitution = Substitution(List(prevBinder), List(CODE.REF(nextBinder))) lazy val storedCond = freshSym(pos, BooleanClass.tpe, "rc") setFlag MUTABLE lazy val treesToHoist: List[Tree] = { @@ -2382,6 +2390,8 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL } case class ReusingCondTreeMaker(sharedPrefix: List[Test], toReused: TreeMaker => TreeMaker) extends TreeMaker { import CODE._ + val pos = sharedPrefix.last.treeMaker.pos + lazy val localSubstitution = { // replace binder of each dropped treemaker by corresponding binder bound by the most recent reused treemaker var mostRecentReusedMaker: ReusedCondTreeMaker = null -- cgit v1.2.3 From bc991663fd9ac34ebc3d3ebb5a7825d478a7b2e7 Mon Sep 17 00:00:00 2001 From: Adriaan Moors Date: Wed, 23 May 2012 12:41:14 +0200 Subject: construct typed trees in TypeTestTM --- src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala b/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala index 63547a84eb..08621fabae 100644 --- a/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala +++ b/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala @@ -991,6 +991,9 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL if (outerTestNeeded) and(typeTest(testedBinder, expectedTp), outerTest(testedBinder, expectedTp)) else typeTest(testedBinder, expectedTp) + // propagate expected type + @inline def expTp(t: Tree): t.type = t setType expectedTp + // true when called to type-test the argument to an extractor // don't do any fancy equality checking, just test the type if (extractorArgTypeTest) default @@ -1000,11 +1003,11 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL case SingleType(_, sym) => and(equalsTest(CODE.REF(sym), testedBinder), typeTest(testedBinder, expectedTp.widen)) // must use == to support e.g. List() == Nil case ThisType(sym) if sym.isModule => and(equalsTest(CODE.REF(sym), testedBinder), typeTest(testedBinder, expectedTp.widen)) - case ConstantType(const) => equalsTest(Literal(const), testedBinder) + case ConstantType(const) => equalsTest(expTp(Literal(const)), testedBinder) - case ThisType(sym) => eqTest(This(sym), testedBinder) + case ThisType(sym) => eqTest(expTp(This(sym)), testedBinder) case ConstantType(Constant(null)) if testedBinder.info.widen <:< AnyRefClass.tpe - => eqTest(CODE.NULL, testedBinder) + => eqTest(expTp(CODE.NULL), testedBinder) // TODO: verify that we don't need to special-case Array // I think it's okay: -- cgit v1.2.3 From bf533ea85e62a65ce1fd2613b03928801d87795e Mon Sep 17 00:00:00 2001 From: Adriaan Moors Date: Tue, 29 May 2012 10:40:49 +0200 Subject: patmatdebug --- .../tools/nsc/typechecker/PatternMatching.scala | 117 ++++++++++----------- 1 file changed, 57 insertions(+), 60 deletions(-) diff --git a/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala b/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala index 08621fabae..83cde35cc3 100644 --- a/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala +++ b/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala @@ -45,6 +45,8 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL val phaseName: String = "patmat" + def patmatDebug(msg: String) = println(msg) + def newTransformer(unit: CompilationUnit): Transformer = if (opt.virtPatmat) new MatchTransformer(unit) else noopTransformer @@ -173,7 +175,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL // (that would require more sophistication when generating trees, // and the only place that emits Matches after typers is for exception handling anyway) if(phase.id >= currentRun.uncurryPhase.id) debugwarn("running translateMatch at "+ phase +" on "+ selector +" match "+ cases) - // println("translating "+ cases.mkString("{", "\n", "}")) + // patmatDebug("translating "+ cases.mkString("{", "\n", "}")) def repeatedToSeq(tp: Type): Type = (tp baseType RepeatedParamClass) match { case TypeRef(_, RepeatedParamClass, arg :: Nil) => seqType(arg) @@ -297,9 +299,9 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL // as b.info may be based on a Typed type ascription, which has not been taken into account yet by the translation // (it will later result in a type test when `tp` is not a subtype of `b.info`) // TODO: can we simplify this, together with the Bound case? - (extractor.subPatBinders, extractor.subPatTypes).zipped foreach { case (b, tp) => b setInfo tp } // println("changing "+ b +" : "+ b.info +" -> "+ tp); + (extractor.subPatBinders, extractor.subPatTypes).zipped foreach { case (b, tp) => b setInfo tp } // patmatDebug("changing "+ b +" : "+ b.info +" -> "+ tp); - // println("translateExtractorPattern checking parameter type: "+ (patBinder, patBinder.info.widen, extractor.paramType, patBinder.info.widen <:< extractor.paramType)) + // patmatDebug("translateExtractorPattern checking parameter type: "+ (patBinder, patBinder.info.widen, extractor.paramType, patBinder.info.widen <:< extractor.paramType)) // example check: List[Int] <:< ::[Int] // TODO: extractor.paramType may contain unbound type params (run/t2800, run/t3530) val (typeTestTreeMaker, patBinderOrCasted) = @@ -337,7 +339,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL case WildcardPattern() => noFurtherSubPats() case UnApply(unfun, args) => // TODO: check unargs == args - // println("unfun: "+ (unfun.tpe, unfun.symbol.ownerChain, unfun.symbol.info, patBinder.info)) + // patmatDebug("unfun: "+ (unfun.tpe, unfun.symbol.ownerChain, unfun.symbol.info, patBinder.info)) translateExtractorPattern(ExtractorCall(unfun, args)) /** A constructor pattern is of the form c(p1, ..., pn) where n ≥ 0. @@ -403,7 +405,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL */ case Bind(n, p) => // this happens in certain ill-formed programs, there'll be an error later - // println("WARNING: Bind tree with unbound symbol "+ patTree) + // patmatDebug("WARNING: Bind tree with unbound symbol "+ patTree) noFurtherSubPats() // there's no symbol -- something's wrong... don't fail here though (or should we?) // case Star(_) | ArrayValue | This => error("stone age pattern relics encountered!") @@ -476,13 +478,13 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL // this fails to resolve overloading properly... // Apply(typedOperator(Select(orig, extractor)), List(Ident(nme.SELECTOR_DUMMY))) // no need to set the type of the dummy arg, it will be replaced anyway - // println("funtpe after = "+ fun.tpe.finalResultType) - // println("orig: "+(orig, orig.tpe)) + // patmatDebug("funtpe after = "+ fun.tpe.finalResultType) + // patmatDebug("orig: "+(orig, orig.tpe)) val tgt = typed(orig, EXPRmode | QUALmode | POLYmode, HasMember(extractor.name)) // can't specify fun.tpe.finalResultType as the type for the extractor's arg, // as it may have been inferred incorrectly (see t602, where it's com.mosol.sl.Span[Any], instead of com.mosol.sl.Span[?K]) - // println("tgt = "+ (tgt, tgt.tpe)) + // patmatDebug("tgt = "+ (tgt, tgt.tpe)) val oper = typed(Select(tgt, extractor.name), EXPRmode | FUNmode | POLYmode | TAPPmode, WildcardType) - // println("oper: "+ (oper, oper.tpe)) + // patmatDebug("oper: "+ (oper, oper.tpe)) Apply(oper, List(Ident(nme.SELECTOR_DUMMY))) // no need to set the type of the dummy arg, it will be replaced anyway } } finally context.undetparams = savedUndets @@ -598,8 +600,8 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL // private val orig = fun match {case tpt: TypeTree => tpt.original case _ => fun} // private val origExtractorTp = unapplyMember(orig.symbol.filter(sym => reallyExists(unapplyMember(sym.tpe))).tpe).tpe // private val extractorTp = if (wellKinded(fun.tpe)) fun.tpe else existentialAbstraction(origExtractorTp.typeParams, origExtractorTp.resultType) - // println("ExtractorCallProd: "+ (fun.tpe, existentialAbstraction(origExtractorTp.typeParams, origExtractorTp.resultType))) - // println("ExtractorCallProd: "+ (fun.tpe, args map (_.tpe))) + // patmatDebug("ExtractorCallProd: "+ (fun.tpe, existentialAbstraction(origExtractorTp.typeParams, origExtractorTp.resultType))) + // patmatDebug("ExtractorCallProd: "+ (fun.tpe, args map (_.tpe))) private def constructorTp = fun.tpe def isTyped = fun.isTyped @@ -627,14 +629,14 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL def indexInCPA(acc: Symbol) = constrParamAccessors indexWhere { orig => - // println("compare: "+ (orig, acc, orig.name, acc.name, (acc.name == orig.name), (acc.name startsWith (orig.name append "$")))) + // patmatDebug("compare: "+ (orig, acc, orig.name, acc.name, (acc.name == orig.name), (acc.name startsWith (orig.name append "$")))) val origName = orig.name.toString.trim val accName = acc.name.toString.trim (accName == origName) || (accName startsWith (origName + "$")) } - // println("caseFieldAccessors: "+ (accessors, binder.caseFieldAccessors map indexInCPA)) - // println("constrParamAccessors: "+ constrParamAccessors) + // patmatDebug("caseFieldAccessors: "+ (accessors, binder.caseFieldAccessors map indexInCPA)) + // patmatDebug("constrParamAccessors: "+ constrParamAccessors) val accessorsSorted = accessors sortBy indexInCPA if (accessorsSorted isDefinedAt (i-1)) REF(binder) DOT accessorsSorted(i-1) @@ -806,7 +808,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL private[TreeMakers] def incorporateOuterSubstitution(outerSubst: Substitution): Unit = { if (currSub ne null) { - println("BUG: incorporateOuterSubstitution called more than once for "+ (this, currSub, outerSubst)) + // patmatDebug("BUG: incorporateOuterSubstitution called more than once for "+ (this, currSub, outerSubst)) Thread.dumpStack() } else currSub = outerSubst >> substitution @@ -972,7 +974,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL **/ case class TypeTestTreeMaker(prevBinder: Symbol, testedBinder: Symbol, expectedTp: Type, nextBinderTp: Type)(override val pos: Position, extractorArgTypeTest: Boolean = false) extends CondTreeMaker { import TypeTestTreeMaker._ - // println("TTTM"+(prevBinder, extractorArgTypeTest, testedBinder, expectedTp, nextBinderTp)) + // patmatDebug("TTTM"+(prevBinder, extractorArgTypeTest, testedBinder, expectedTp, nextBinderTp)) lazy val outerTestNeeded = ( !((expectedTp.prefix eq NoPrefix) || expectedTp.prefix.typeSymbol.isPackageClass) @@ -1101,7 +1103,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL fixerUpper(owner, scrut.pos){ val ptDefined = if (isFullyDefined(pt)) pt else NoType def matchFailGen = (matchFailGenOverride orElse Some(CODE.MATCHERROR(_: Tree))) - // println("combining cases: "+ (casesNoSubstOnly.map(_.mkString(" >> ")).mkString("{", "\n", "}"))) + // patmatDebug("combining cases: "+ (casesNoSubstOnly.map(_.mkString(" >> ")).mkString("{", "\n", "}"))) def isSwitchAnnotation(tpe: Type) = tpe hasAnnotation SwitchClass def isUncheckedAnnotation(tpe: Type) = tpe hasAnnotation UncheckedClass @@ -1156,12 +1158,12 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL t match { case Function(_, _) if t.symbol == NoSymbol => t.symbol = currentOwner.newAnonymousFunctionValue(t.pos) - // println("new symbol for "+ (t, t.symbol.ownerChain)) + // patmatDebug("new symbol for "+ (t, t.symbol.ownerChain)) case Function(_, _) if (t.symbol.owner == NoSymbol) || (t.symbol.owner == origOwner) => - // println("fundef: "+ (t, t.symbol.ownerChain, currentOwner.ownerChain)) + // patmatDebug("fundef: "+ (t, t.symbol.ownerChain, currentOwner.ownerChain)) t.symbol.owner = currentOwner case d : DefTree if (d.symbol != NoSymbol) && ((d.symbol.owner == NoSymbol) || (d.symbol.owner == origOwner)) => // don't indiscriminately change existing owners! (see e.g., pos/t3440, pos/t3534, pos/unapplyContexts2) - // println("def: "+ (d, d.symbol.ownerChain, currentOwner.ownerChain)) + // patmatDebug("def: "+ (d, d.symbol.ownerChain, currentOwner.ownerChain)) if(d.symbol.isLazy) { // for lazy val's accessor -- is there no tree?? assert(d.symbol.lazyAccessor != NoSymbol && d.symbol.lazyAccessor.owner == d.symbol.owner, d.symbol.lazyAccessor) d.symbol.lazyAccessor.owner = currentOwner @@ -1171,16 +1173,16 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL d.symbol.owner = currentOwner // case _ if (t.symbol != NoSymbol) && (t.symbol ne null) => - // println("untouched "+ (t, t.getClass, t.symbol.ownerChain, currentOwner.ownerChain)) + // patmatDebug("untouched "+ (t, t.getClass, t.symbol.ownerChain, currentOwner.ownerChain)) case _ => } super.traverse(t) } // override def apply - // println("before fixerupper: "+ xTree) + // patmatDebug("before fixerupper: "+ xTree) // currentRun.trackerFactory.snapshot() - // println("after fixerupper") + // patmatDebug("after fixerupper") // currentRun.trackerFactory.snapshot() } } @@ -1245,7 +1247,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL def _asInstanceOf(t: Tree, tp: Type, force: Boolean = false): Tree = if (!force && (t.tpe ne NoType) && t.isTyped && typesConform(t.tpe, tp)) t else mkCast(t, tp) def _asInstanceOf(b: Symbol, tp: Type): Tree = if (typesConform(b.info, tp)) REF(b) else mkCast(REF(b), tp) def _isInstanceOf(b: Symbol, tp: Type): Tree = gen.mkIsInstanceOf(REF(b), tp.withoutAnnotations, true, false) - // if (typesConform(b.info, tpX)) { println("warning: emitted spurious isInstanceOf: "+(b, tp)); TRUE } + // if (typesConform(b.info, tpX)) { patmatDebug("warning: emitted spurious isInstanceOf: "+(b, tp)); TRUE } // duplicated out of frustration with cast generation def mkZero(tp: Type): Tree = { @@ -1448,7 +1450,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL // hashconsing trees (modulo value-equality) def unique(t: Tree, tpOverride: Type = NoType): Tree = trees find (a => a.equalsStructure0(t)(sameValue)) match { - case Some(orig) => orig // println("unique: "+ (t eq orig, orig)); + case Some(orig) => orig // patmatDebug("unique: "+ (t eq orig, orig)); case _ => trees += t if (tpOverride != NoType) t setType tpOverride @@ -1533,13 +1535,13 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL } def showTreeMakers(cases: List[List[TreeMaker]]) = { - println("treeMakers:") - println(alignAcrossRows(cases, ">>")) + patmatDebug("treeMakers:") + patmatDebug(alignAcrossRows(cases, ">>")) } def showTests(testss: List[List[Test]]) = { - println("tests: ") - println(alignAcrossRows(testss, "&")) + patmatDebug("tests: ") + patmatDebug(alignAcrossRows(testss, "&")) } } @@ -1661,7 +1663,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL def assigned(dom: Set[Sym]) = eqAxioms = And(eqAxioms, dom.reduceLeft(Or)) - // println("vars: "+ vars) + // patmatDebug("vars: "+ vars) vars.foreach { v => // is the domain enumerable? then create equality syms for all elements in the domain and // assert at least one of them must be selected @@ -1690,8 +1692,8 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL } } - // println("eqAxioms:\n"+ cnfString(conjunctiveNormalForm(negationNormalForm(eqAxioms)))) - // println("pure:\n"+ cnfString(conjunctiveNormalForm(negationNormalForm(pure)))) + // patmatDebug("eqAxioms:\n"+ cnfString(conjunctiveNormalForm(negationNormalForm(eqAxioms)))) + // patmatDebug("pure:\n"+ cnfString(conjunctiveNormalForm(negationNormalForm(pure)))) And(eqAxioms, pure) } @@ -1781,13 +1783,13 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL @inline def withLit(res: (Boolean, Model), l: Lit) = (res._1, res._2 + (l.sym -> l.pos)) @inline def orElse(a: (Boolean, Model), b: => (Boolean, Model)) = if (a._1) a else b -// println("dpll\n"+ cnfString(f)) + // patmatDebug("dpll\n"+ cnfString(f)) if (f isEmpty) (true, EmptyModel) else if(f exists (_.isEmpty)) (false, EmptyModel) else f.find(_.size == 1) map { unitClause => val unitLit = unitClause.head -// println("unit: "+ unitLit) + // patmatDebug("unit: "+ unitLit) val negated = -unitLit // drop entire clauses that are trivially true // (i.e., disjunctions that contain the literal we're making true in the returned model), @@ -1813,12 +1815,12 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL // (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)) -// println("pure: "+ pureLit +" pures: "+ pures +" impures: "+ impures) + // patmatDebug("pure: "+ pureLit +" pures: "+ pures +" impures: "+ impures) val simplified = f.filterNot(_.contains(pureLit)) withLit(DPLL(simplified), pureLit) } else { val split = f.head.head -// println("split: "+ split) + // patmatDebug("split: "+ split) orElse(DPLL(f :+ clause(split)), DPLL(f :+ clause(-split))) } } @@ -1884,6 +1886,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL 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) @@ -1901,11 +1904,11 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL def enumerateSubtypes(tp: Type): Option[List[Type]] = tp.typeSymbol match { case BooleanClass => - // println("enum bool "+ tp) + // patmatDebug("enum bool "+ tp) Some(List(ConstantType(Constant(true)), ConstantType(Constant(false)))) // TODO case _ if tp.isTupleType => // recurse into component types case sym if !sym.isSealed || isPrimitiveValueClass(sym) => - // println("enum unsealed "+ (tp, sym, sym.isSealed, isPrimitiveValueClass(sym))) + // patmatDebug("enum unsealed "+ (tp, sym, sym.isSealed, isPrimitiveValueClass(sym))) None case sym => val subclasses = ( @@ -1913,7 +1916,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL // symbols which are both sealed and abstract need not be covered themselves, because // all of their children must be and they cannot otherwise be created. filterNot (x => x.isSealed && x.isAbstractClass && !isPrimitiveValueClass(x))) - // println("subclasses "+ (sym, subclasses)) + // patmatDebug("subclasses "+ (sym, subclasses)) val tpApprox = typer.infer.approximateAbstracts(tp) val pre = tpApprox.prefix @@ -1925,11 +1928,11 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL // however, must approximate abstract types in val subTp = appliedType(pre.memberType(sym), sym.typeParams.map(_ => WildcardType)) val subTpApprox = typer.infer.approximateAbstracts(subTp) // TODO: needed? - // println("subtp"+(subTpApprox <:< tpApprox, subTpApprox, tpApprox)) + // patmatDebug("subtp"+(subTpApprox <:< tpApprox, subTpApprox, tpApprox)) if (subTpApprox <:< tpApprox) Some(checkableType(subTp)) else None }) - // println("enum sealed "+ (tp, tpApprox) + " as "+ validSubTypes) + // patmatDebug("enum sealed "+ (tp, tpApprox) + " as "+ validSubTypes) Some(validSubTypes) } @@ -1955,7 +1958,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL } } val res = toCheckable(tp) - // println("checkable "+(tp, res)) + // patmatDebug("checkable "+(tp, res)) res } @@ -1966,7 +1969,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL val checkable = ( (isTupleType(tp) && tupleComponents(tp).exists(tp => !uncheckableType(tp))) || enumerateSubtypes(tp).nonEmpty) - // if (!checkable) println("deemed uncheckable: "+ tp) + // if (!checkable) patmatDebug("deemed uncheckable: "+ tp) !checkable } @@ -2045,21 +2048,14 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL // debug output: - // println("analysing:") + // patmatDebug("analysing:") // showTreeMakers(cases) // showTests(tests) // - // def gatherVariables(p: Prop): Set[Var] = { - // val vars = new HashSet[Var]() - // (new PropTraverser { - // override def applyVar(v: Var) = vars += v - // })(p) - // vars.toSet - // } // val vars = gatherVariables(matchFails) - // println("\nvars:\n"+ (vars map (_.describe) mkString ("\n"))) + // patmatDebug("\nvars:\n"+ (vars map (_.describe) mkString ("\n"))) // - // println("\nmatchFails as CNF:\n"+ cnfString(normalize(matchFails))) + // patmatDebug("\nmatchFails as CNF:\n"+ cnfString(normalize(matchFails))) // find the models (under which the match fails) val matchFailModels = fullDPLL(normalize(matchFails)) @@ -2142,7 +2138,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL // should never be more than one value in trues... } - // println("var assignment:\n"+ + // patmatDebug("var assignment for model "+ model +":\n"+ // varAssignment.toSeq.sortBy(_._1.toString).map { case (v, (trues, falses)) => // val assignment = "== "+ (trues mkString("(", ", ", ")")) +" != ("+ (falses mkString(", ")) +")" // v +"(="+ v.path +": "+ v.domainTp +") "+ assignment @@ -2153,7 +2149,8 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL def chop(path: Tree): List[Symbol] = path match { case Ident(_) => List(path.symbol) case Select(pre, name) => chop(pre) :+ path.symbol - case _ => println("don't know how to chop "+ path); Nil + case _ => // patmatDebug("don't know how to chop "+ path) + Nil } // turn the variable assignments into a tree @@ -2246,7 +2243,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL // TODO: improve reasoning -- in the mean time, a false negative is better than an annoying false positive case _ => NoExample } -// println("described as: "+ res) +// patmatDebug("described as: "+ res) res } @@ -2319,7 +2316,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL tested.clear() tests dropWhile storeDependencies } - // println("dependencies: "+ dependencies) + // patmatDebug("dependencies: "+ dependencies) // find longest prefix of tests that reuse a prior test, and whose dependent conditions monotonically increase // then, collapse these contiguous sequences of reusing tests @@ -2353,7 +2350,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL case _ => } - // println("sharedPrefix: "+ sharedPrefix) + // patmatDebug("sharedPrefix: "+ sharedPrefix) // if the shared prefix contains interesting conditions (!= Top) // and the last of such interesting shared conditions reuses another treemaker's test // replace the whole sharedPrefix by a ReusingCondTreeMaker @@ -2369,7 +2366,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL // replace original treemakers that are reused (as determined when computing collapsed), // by ReusedCondTreeMakers val reusedMakers = collapsed mapConserve (_ mapConserve reusedOrOrig) -// println("after CSE:") +// patmatDebug("after CSE:") // showTreeMakers(reusedMakers) reusedMakers } @@ -2484,7 +2481,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL val substedBody = btm.substitution(body) CaseDef(Alternative(patterns), EmptyTree, substedBody) } - case _ => //println("can't emit switch for "+ makers) + case _ => // patmatDebug("can't emit switch for "+ makers) None //failure (can't translate pattern to a switch) } } -- cgit v1.2.3 From 01ac32a9a2eb07832231647b3fab20e5b8d4b4ac Mon Sep 17 00:00:00 2001 From: Adriaan Moors Date: Tue, 29 May 2012 10:44:37 +0200 Subject: support for repeated approximation of treemakers --- .../tools/nsc/typechecker/PatternMatching.scala | 85 ++++++++++++---------- 1 file changed, 47 insertions(+), 38 deletions(-) diff --git a/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala b/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala index 83cde35cc3..830e7db8ca 100644 --- a/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala +++ b/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala @@ -1439,6 +1439,29 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL // pointsToBound -- accumSubst.from == Set(root) && (accumSubst.from.toSet -- pointsToBound) isEmpty private var accumSubst: Substitution = EmptySubstitution + private def updateSubstitution(subst: Substitution) = { + // find part of substitution that replaces bound symbols by new symbols, and reverse that part + // so that we don't introduce new aliases for existing symbols, thus keeping the set of bound symbols minimal + val (boundSubst, unboundSubst) = (subst.from zip subst.to) partition { + case (f, t) => + t.isInstanceOf[Ident] && (t.symbol ne NoSymbol) && pointsToBound(f) + } + val (boundFrom, boundTo) = boundSubst.unzip + val (unboundFrom, unboundTo) = unboundSubst.unzip + + // reverse substitution that would otherwise replace a variable we already encountered by a new variable + // NOTE: this forgets the more precise we have for these later variables, but that's probably okay + normalize >>= Substitution(boundTo map (_.symbol), boundFrom map (CODE.REF(_))) + // patmatDebug("normalize: "+ normalize) + + val okSubst = Substitution(unboundFrom, unboundTo map (normalize(_))) // it's important substitution does not duplicate trees here -- it helps to keep hash consing simple, anyway + pointsToBound ++= ((okSubst.from, okSubst.to).zipped filter { (f, t) => pointsToBound exists (sym => t.exists(_.symbol == sym)) })._1 + // patmatDebug("pointsToBound: "+ pointsToBound) + + accumSubst >>= okSubst + // patmatDebug("accumSubst: "+ accumSubst) + } + private val trees = new collection.mutable.HashSet[Tree] // TODO: improve, e.g., for constants @@ -1467,7 +1490,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL // produce the unique tree used to refer to this binder // the type of the binder passed to the first invocation // determines the type of the tree that'll be returned for that binder as of then - def binderToUniqueTree(b: Symbol) = + final def binderToUniqueTree(b: Symbol) = unique(accumSubst(normalize(CODE.REF(b))), b.tpe) @inline def /\(conds: Iterable[Cond]) = if (conds.isEmpty) Top else conds.reduceLeft(AndCond(_, _)) @@ -1475,23 +1498,32 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL // note that the sequencing of operations is important: must visit in same order as match execution // binderToUniqueTree uses the type of the first symbol that was encountered as the type for all future binders - def treeMakerToCond(tm: TreeMaker): Cond = { + final protected def treeMakerToCond(tm: TreeMaker, condMaker: CondMaker): Cond = { updateSubstitution(tm.substitution) + condMaker(tm)(treeMakerToCond(_, condMaker)) + } + + final protected def treeMakerToCondNoSubst(tm: TreeMaker, condMaker: CondMaker): Cond = + condMaker(tm)(treeMakerToCondNoSubst(_, condMaker)) + type CondMaker = TreeMaker => (TreeMaker => Cond) => Cond + final def makeCond(tm: TreeMaker)(recurse: TreeMaker => Cond): Cond = { tm match { case ttm@TypeTestTreeMaker(prevBinder, testedBinder, pt, _) => object condStrategy extends TypeTestTreeMaker.TypeTestCondStrategy { type Result = Cond def and(a: Result, b: Result) = AndCond(a, b) def outerTest(testedBinder: Symbol, expectedTp: Type) = Top // TODO OuterEqCond(testedBinder, expectedType) - def typeTest(b: Symbol, pt: Type) = TypeCond(binderToUniqueTree(b), uniqueTp(pt)) + def typeTest(b: Symbol, pt: Type) = { // a type test implies the tested path is non-null (null.isInstanceOf[T] is false for all T) + val p = binderToUniqueTree(b); AndCond(NonNullCond(p), TypeCond(p, uniqueTp(pt))) + } def nonNullTest(testedBinder: Symbol) = NonNullCond(binderToUniqueTree(testedBinder)) def equalsTest(pat: Tree, testedBinder: Symbol) = EqualityCond(binderToUniqueTree(testedBinder), unique(pat)) def eqTest(pat: Tree, testedBinder: Symbol) = EqualityCond(binderToUniqueTree(testedBinder), unique(pat)) // TODO: eq, not == } ttm.renderCondition(condStrategy) case EqualityTestTreeMaker(prevBinder, patTree, _) => EqualityCond(binderToUniqueTree(prevBinder), unique(patTree)) - case AlternativesTreeMaker(_, altss, _) => \/(altss map (alts => /\(alts map treeMakerToCond))) + case AlternativesTreeMaker(_, altss, _) => \/(altss map (alts => /\(alts map recurse))) case ProductExtractorTreeMaker(testedBinder, None, subst) => NonNullCond(binderToUniqueTree(testedBinder)) case ExtractorTreeMaker(_, _, _, _) | GuardTreeMaker(_) @@ -1501,37 +1533,14 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL } } - private def updateSubstitution(subst: Substitution) = { - // find part of substitution that replaces bound symbols by new symbols, and reverse that part - // so that we don't introduce new aliases for existing symbols, thus keeping the set of bound symbols minimal - val (boundSubst, unboundSubst) = (subst.from zip subst.to) partition {case (f, t) => - t.isInstanceOf[Ident] && (t.symbol ne NoSymbol) && pointsToBound(f) - } - val (boundFrom, boundTo) = boundSubst.unzip - val (unboundFrom, unboundTo) = unboundSubst.unzip - - // reverse substitution that would otherwise replace a variable we already encountered by a new variable - // NOTE: this forgets the more precise we have for these later variables, but that's probably okay - normalize >>= Substitution(boundTo map (_.symbol), boundFrom map (CODE.REF(_))) - // println("normalize: "+ normalize) - - val okSubst = Substitution(unboundFrom, unboundTo map (normalize(_))) // it's important substitution does not duplicate trees here -- it helps to keep hash consing simple, anyway - pointsToBound ++= ((okSubst.from, okSubst.to).zipped filter { (f, t) => pointsToBound exists (sym => t.exists(_.symbol == sym)) })._1 - // println("pointsToBound: "+ pointsToBound) - - accumSubst >>= okSubst - // println("accumSubst: "+ accumSubst) - } - - def approximateTreeMaker(tm: TreeMaker): Test = - Test(treeMakerToCond(tm), tm) + final def approximateMatch(condMaker: CondMaker = makeCond): List[List[Test]] = cases.map { _ map (tm => Test(treeMakerToCond(tm, condMaker), tm)) } - def approximateMatch: List[List[Test]] = cases.map { _ map approximateTreeMaker } + final def approximateMatchAgain(condMaker: CondMaker = makeCond): List[List[Test]] = cases.map { _ map (tm => Test(treeMakerToCondNoSubst(tm, condMaker), tm)) } } def approximateMatch(root: Symbol, cases: List[List[TreeMaker]]): List[List[Test]] = { object approximator extends TreeMakersToConds(root, cases) - approximator.approximateMatch + approximator.approximateMatch() } def showTreeMakers(cases: List[List[TreeMaker]]) = { @@ -1982,8 +1991,8 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL // - there are extractor calls (that we can't secretly/soundly) rewrite var backoff = false object exhaustivityApproximation extends TreeMakersToConds(prevBinder, cases) { - override def treeMakerToCond(tm: TreeMaker): Cond = tm match { - case p@ExtractorTreeMaker(extractor, Some(lenCheck), testedBinder, _) => + def makeCondExhaustivity(tm: TreeMaker)(recurse: TreeMaker => Cond): Cond = tm match { + case p @ ExtractorTreeMaker(extractor, Some(lenCheck), testedBinder, _) => p.checkedLength match { // pattern: `List()` (interpret as `Nil`) // TODO: make it more general List(1, 2) => 1 :: 2 :: Nil @@ -1991,23 +2000,23 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL EqualityCond(binderToUniqueTree(p.prevBinder), unique(Ident(NilModule) setType NilModule.tpe)) case _ => backoff = true - super.treeMakerToCond(tm) + makeCond(tm)(recurse) } case ExtractorTreeMaker(_, _, _, _) => -// println("backing off due to "+ tm) +// patmatDebug("backing off due to "+ tm) backoff = true - super.treeMakerToCond(tm) + makeCond(tm)(recurse) case GuardTreeMaker(guard) => guard.tpe match { case ConstantType(Constant(true)) => Top case ConstantType(Constant(false)) => Havoc case _ => -// println("can't statically interpret guard: "+(guard, guard.tpe)) +// patmatDebug("can't statically interpret guard: "+(guard, guard.tpe)) backoff = true Havoc } case _ => - super.treeMakerToCond(tm) + makeCond(tm)(recurse) } } @@ -2026,7 +2035,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL testsBeforeBody.map(t => symbolic(t.cond)).foldLeft(True: Prop)(And) } - val tests = exhaustivityApproximation.approximateMatch + val tests = exhaustivityApproximation.approximateMatch(exhaustivityApproximation.makeCondExhaustivity) if (backoff) Nil else { val symbolicCases = tests map symbolicCase -- cgit v1.2.3 From 379384c887b01e6e8b48de671d4b2a99b6fdf520 Mon Sep 17 00:00:00 2001 From: Adriaan Moors Date: Tue, 29 May 2012 10:51:54 +0200 Subject: Unreachability analysis for pattern matches Analyze matches for unreachable cases. A case is unreachable if it implies its preceding cases. Call `C` the formula that is satisfiable if the considered case matches. Call `P` the formula that is satisfiable if the cases preceding it match. The case is reachable if there is a model for `-P /\ C`. Thus, the case is unreachable if there is no model for `-(-P /\ C)`, or, equivalently, `P \/ -C`, or `C => P`. Unreachability needs a more precise model for type and value tests than exhaustivity. Before, `{case _: Int => case 1 =>}` would be modeled as `X = Int \/ X = 1.type`, and thus, the second case would be reachable if we can satisfy `X != Int /\ X = 1.type`. Of course, the case isn't reachable, yet the formula is satisfiable, so we must augment our model to take into account that `X = 1.type => X = Int`. This is done by `removeVarEq`, which models the following axioms about equality. It does so to retain the meaning of equality after replacing `V = C` (variable = constant) by a literal (fresh symbol). For each variable: 1. a sealed type test must result in exactly one of its partitions being chosen (the core of exhaustivity) 2. when a type test is true, tests of super types must also be true, and unrelated type tests must be false For example, `V : X ::= A | B | C`, and `A => B` (since `A extends B`). Coverage (1) is formulated as: `A \/ B \/ C`, and the implications of (2) are simply `V=A => V=B /\ V=X`, `V=B => V=X`, `V=C => V=X`. Exclusion for unrelated types typically results from matches such as `{case SomeConst => case OtherConst => }`. Here, `V=SomeConst.type => !V=OtherConst.type`. This is a conservative approximation. If these constants happen to be the same value dynamically (but the types don't tell us this), the last case is actually unreachable. Of course we must err on the safe side. We simplify the equality axioms as follows (in principle this could be done by the solver, but it's easy to do before solving). If we've already excluded a pair of assignments of constants to a certain variable at some point, say `(-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.) TODO: We should also model dependencies between variables: if `V1` corresponds to `x: List[_]` and `V2` is `x.hd`, `V2` cannot be assigned at all when `V1 = null` or `V1 = Nil`. Right now this is implemented hackily by pruning counter-examples in exhaustivity. Unreachability would also benefit from a more faithful representation. I had to refactor some of the framework, but most of it is shared with exhaustivity. We must allow approximating tree makers twice, sharing variables, but using different approximations for values not statically known. When considering reachability of a case, we must assume, for example, that its unknown guard succeeds (otherwise it would wrongly be considered unreachable), whereas unknown guards in the preceding cases must be considered to fail (otherwise we could never get to those case, and again, it would falsely be considered unreachable). Since this analysis is relatively expensive, you may opt-out using `-Xno-patmat-analysis` (or annotating the selector with @unchecked). We hope to improve the performance in the near future. -Ystatistics has also been extended to provide some numbers on time spent in the equality-rewrite, solving and analyzing. --- .../tools/nsc/typechecker/PatternMatching.scala | 951 +++++++++++++++------ src/compiler/scala/tools/nsc/util/Statistics.scala | 29 +- test/files/neg/patmatexhaust.check | 5 +- test/files/neg/virtpatmat_reach_null.check | 4 + test/files/neg/virtpatmat_reach_null.flags | 1 + test/files/neg/virtpatmat_reach_null.scala | 19 + .../neg/virtpatmat_reach_sealed_unsealed.check | 14 + .../neg/virtpatmat_reach_sealed_unsealed.flags | 1 + .../neg/virtpatmat_reach_sealed_unsealed.scala | 21 + test/files/pos/virtpatmat_reach_const.scala | 11 + 10 files changed, 807 insertions(+), 249 deletions(-) create mode 100644 test/files/neg/virtpatmat_reach_null.check create mode 100644 test/files/neg/virtpatmat_reach_null.flags create mode 100644 test/files/neg/virtpatmat_reach_null.scala create mode 100644 test/files/neg/virtpatmat_reach_sealed_unsealed.check create mode 100644 test/files/neg/virtpatmat_reach_sealed_unsealed.flags create mode 100644 test/files/neg/virtpatmat_reach_sealed_unsealed.scala create mode 100644 test/files/pos/virtpatmat_reach_const.scala diff --git a/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala b/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala index 830e7db8ca..21b80df735 100644 --- a/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala +++ b/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala @@ -14,6 +14,7 @@ import scala.tools.nsc.transform.TypingTransformers import scala.tools.nsc.transform.Transform import scala.collection.mutable.HashSet import scala.collection.mutable.HashMap +import scala.tools.nsc.util.Statistics /** Translate pattern matching. * @@ -38,6 +39,8 @@ import scala.collection.mutable.HashMap * - recover exhaustivity and unreachability checking using a variation on the type-safe builder pattern */ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL { // self: Analyzer => + import Statistics._ + val global: Global // need to repeat here because otherwise last mixin defines global as // SymbolTable. If we had DOT this would not be an issue import global._ // the global environment @@ -182,6 +185,8 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL case _ => tp } + val start = startTimer(patmatNanos) + val selectorTp = repeatedToSeq(elimAnonymousClass(selector.tpe.widen.withoutAnnotations)) val origPt = match_.tpe @@ -205,7 +210,10 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL val selectorSym = freshSym(selector.pos, pureType(selectorTp)) setFlag SYNTH_CASE // pt = Any* occurs when compiling test/files/pos/annotDepMethType.scala with -Xexperimental - combineCases(selector, selectorSym, cases map translateCase(selectorSym, pt), pt, matchOwner, matchFailGenOverride) + val combined = combineCases(selector, selectorSym, cases map translateCase(selectorSym, pt), pt, matchOwner, matchFailGenOverride) + + stopTimer(patmatNanos, start) + combined } // return list of typed CaseDefs that are supported by the backend (typed/bind/wildcard) @@ -1328,11 +1336,11 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL // def andThen_: (prev: List[Test]): List[Test] = // prev.filterNot(this <:< _) :+ this - private val reusedBy = new collection.mutable.HashSet[Test] + // private val reusedBy = new collection.mutable.HashSet[Test] var reuses: Option[Test] = None def registerReuseBy(later: Test): Unit = { assert(later.reuses.isEmpty, later.reuses) - reusedBy += later + // reusedBy += later later.reuses = Some(this) } @@ -1427,9 +1435,16 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL // returns (tree, tests), where `tree` will be used to refer to `root` in `tests` - abstract class TreeMakersToConds(val root: Symbol, val cases: List[List[TreeMaker]]) { + abstract class TreeMakersToConds(val root: Symbol) { + def discard() = { + pointsToBound.clear() + trees.clear() + normalize = EmptySubstitution + accumSubst = EmptySubstitution + } // a variable in this set should never be replaced by a tree that "does not consist of a selection on a variable in this set" (intuitively) - private val pointsToBound = collection.mutable.HashSet(root) + private val pointsToBound = collection.mutable.HashSet(root) + private val trees = collection.mutable.HashSet.empty[Tree] // the substitution that renames variables to variables in pointsToBound private var normalize: Substitution = EmptySubstitution @@ -1462,7 +1477,6 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL // patmatDebug("accumSubst: "+ accumSubst) } - private val trees = new collection.mutable.HashSet[Tree] // TODO: improve, e.g., for constants def sameValue(a: Tree, b: Tree): Boolean = (a eq b) || ((a, b) match { @@ -1533,14 +1547,14 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL } } - final def approximateMatch(condMaker: CondMaker = makeCond): List[List[Test]] = cases.map { _ map (tm => Test(treeMakerToCond(tm, condMaker), tm)) } + final def approximateMatch(cases: List[List[TreeMaker]], condMaker: CondMaker = makeCond): List[List[Test]] = cases.map { _ map (tm => Test(treeMakerToCond(tm, condMaker), tm)) } - final def approximateMatchAgain(condMaker: CondMaker = makeCond): List[List[Test]] = cases.map { _ map (tm => Test(treeMakerToCondNoSubst(tm, condMaker), tm)) } + final def approximateMatchAgain(cases: List[List[TreeMaker]], condMaker: CondMaker = makeCond): List[List[Test]] = cases.map { _ map (tm => Test(treeMakerToCondNoSubst(tm, condMaker), tm)) } } def approximateMatch(root: Symbol, cases: List[List[TreeMaker]]): List[List[Test]] = { - object approximator extends TreeMakersToConds(root, cases) - approximator.approximateMatch() + object approximator extends TreeMakersToConds(root) + approximator.approximateMatch(cases) } def showTreeMakers(cases: List[List[TreeMaker]]) = { @@ -1585,18 +1599,36 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL class Prop case class Eq(p: Var, q: Const) extends Prop - type Const + type Const <: AbsConst + + trait AbsConst { + def implies(other: Const): Boolean + def excludes(other: Const): Boolean + } + type Var <: AbsVar trait AbsVar { - // if the domain is enumerable, at least one assignment must be true - def domainEnumerable: Boolean - def domain: Option[Set[Const]] + // indicate we may later require a prop for V = C + def registerEquality(c: Const): Unit + + // indicates null is part of the domain + def considerNull: Unit + + // compute the domain and return it (call considerNull first!) + def domainSyms: Option[Set[Sym]] // for this var, call it V, turn V = C into the equivalent proposition in boolean logic + // registerEquality(c) must have been called prior to this call + // in fact, all equalities relevant to this variable must have been registered def propForEqualsTo(c: Const): Prop - def equalitySyms: Set[Sym] +// // describe the equality axioms related to this variable being equal to this constant +// def impliedProp(c: Const): Prop + + // populated by registerEquality + // once equalitySyms has been called, registerEquality has no effect + def equalitySyms: List[Sym] } // would be nice to statically check whether a prop is equational or pure, @@ -1608,12 +1640,17 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL case object True extends Prop case object False extends Prop - private def nextSymId = {_symId += 1; _symId}; private var _symId = 0 - // symbols are propositions case class Sym(val variable: Var, val const: Const) extends Prop { - override val toString = variable +"="+ const +"#"+ nextSymId + private[this] val id = nextSymId + override def toString = variable +"="+ const +"#"+ id } + private def nextSymId = {_symId += 1; _symId}; private var _symId = 0 + + + @inline def /\(props: Iterable[Prop]) = if (props.isEmpty) True else props.reduceLeft(And(_, _)) + @inline def \/(props: Iterable[Prop]) = if (props.isEmpty) False else props.reduceLeft(Or(_, _)) + trait PropTraverser { def apply(x: Prop): Unit = x match { @@ -1627,6 +1664,14 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL def applyConst(x: Const): Unit = {} } + def gatherVariables(p: Prop): Set[Var] = { + val vars = new HashSet[Var]() + (new PropTraverser { + override def applyVar(v: Var) = vars += v + })(p) + vars.toSet + } + trait PropMap { def apply(x: Prop): Prop = x match { // TODO: mapConserve case And(a, b) => And(apply(a), apply(b)) @@ -1636,278 +1681,687 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL } } - // plan: (aka TODO) - // convert finite domain propositional logic to boolean propositional logic // for all c in C, there is a corresponding (meta-indexed) proposition Qv(c) that represents V = c, // the only property of equality that is encoded is that a variable can at most be equal to one of the c in C: // thus, for each distinct c, c', c'',... in C, a clause `not (Qv(c) /\ (Qv(c') \/ ... \/ Qv(c'')))` is added - def removeVarEq(prop: Prop): Prop = { + def removeVarEq(props: List[Prop], considerNull: Boolean = false): (Prop, List[Prop]) = { + val start = startTimer(patmatAnaVarEq) + val vars = new collection.mutable.HashSet[Var] - object dropEquational extends PropMap { + object gatherEqualities extends PropTraverser { override def apply(p: Prop) = p match { - case Eq(v, c) => vars += v; v.propForEqualsTo(c) + case Eq(v, c) => + vars += v + v.registerEquality(c) case _ => super.apply(p) } } - // dropEquational populates vars, and for each var in vars. var.equalitySyms - val pure = dropEquational(prop) + object rewriteEqualsToProp extends PropMap { + override def apply(p: Prop) = p match { + case Eq(v, c) => v.propForEqualsTo(c) + case _ => super.apply(p) + } + } + + props foreach gatherEqualities.apply + if (considerNull) vars foreach (_.considerNull) - // X = C is translated to P_X=C - // X = C' is translated to P_X=C' - // need to enforce X cannot simultaneously equal C and C' - // thus, all equality syms are mutually exclusive - // X = A, B, C, D --> Not(And(A, B)) /\ Not(And(A, C)) /\ Not(And(A, D)) - // /\ Not(And(B, C)) /\ Not(And(B, D)) - // /\ Not(And(C, D)) - // equivalently Or(Not(A), Not(B)) /\ Or(...) + val pure = props map rewriteEqualsToProp.apply var eqAxioms: Prop = True - def mutex(a: Sym)(b: Sym) = - eqAxioms = And(eqAxioms, Or(Not(a), Not(b))) + @inline def addAxiom(p: Prop) = eqAxioms = And(eqAxioms, p) - // at least one assignment from the domain must be true - def assigned(dom: Set[Sym]) = - eqAxioms = And(eqAxioms, dom.reduceLeft(Or)) + case class ExcludedPair(a: Const, b: Const) { + override def equals(o: Any) = o match { + case ExcludedPair(aa, bb) => (a == aa && b == bb) || (a == bb && b == aa) + case _ => false + } + } // patmatDebug("vars: "+ vars) vars.foreach { v => - // is the domain enumerable? then create equality syms for all elements in the domain and - // assert at least one of them must be selected - // if v.domain.isEmpty, we must consider the domain to be infinite - v.domain foreach { dom => - // get the Syms for the constants in the domain (making fresh ones for those not encountered in the formula) - val domProps = dom map {c => v.propForEqualsTo(c)} - val domSyms = new collection.mutable.HashSet[Sym]() - object collectSyms extends PropTraverser { - override def apply(p: Prop) = p match { - case domSym: Sym => domSyms += domSym - case _ => super.apply(p) - } + val excludedPair = new collection.mutable.HashSet[ExcludedPair] + + // if v.domainSyms.isEmpty, we must consider the domain to be infinite + // otherwise, since the domain fully partitions the type of the value, + // exactly one of the types (and whatever it implies, imposed separately) must be chosen + // consider X ::= A | B | C, and A => B + // coverage is formulated as: A \/ B \/ C and the implications are + v.domainSyms foreach { dsyms => addAxiom(\/(dsyms)) } + + val syms = v.equalitySyms + // patmatDebug("eqSyms "+(v, syms)) + syms foreach { sym => + // don't relate V = C to V = C -- `b.const == sym.const` + // if we've already excluded the pair at some point (-A \/ -B), then don't exclude the symmetric one (-B \/ -A) + // (nor the positive implications -B \/ A, or -A \/ B, which would entail the equality axioms falsifying the whole formula) + val todo = syms filterNot (b => (b.const == sym.const) || excludedPair(ExcludedPair(b.const, sym.const))) + val (excluded, notExcluded) = todo partition (b => sym.const.excludes(b.const)) + val implied = notExcluded filter (b => sym.const.implies(b.const)) + // patmatDebug("implications: "+ (sym.const, excluded, implied, syms)) + + // when this symbol is true, what must hold... + implied foreach (impliedSym => addAxiom(Or(Not(sym), impliedSym))) + + // ... and what must not? + excluded foreach {excludedSym => + excludedPair += ExcludedPair(sym.const, excludedSym.const) + addAxiom(Or(Not(sym), Not(excludedSym))) } - domProps foreach collectSyms.apply - - // TODO: an empty domain means involved type tests can never be true --> always non-exhaustive? - if (domSyms.nonEmpty) assigned(domSyms.toSet) - } - - // recover mutual-exclusivity (a variable can never be assigned two different constants) - var syms = v.equalitySyms.toList - while (syms.nonEmpty) { - syms.tail.foreach(mutex(syms.head)) - syms = syms.tail } } - // patmatDebug("eqAxioms:\n"+ cnfString(conjunctiveNormalForm(negationNormalForm(eqAxioms)))) - // patmatDebug("pure:\n"+ cnfString(conjunctiveNormalForm(negationNormalForm(pure)))) + // patmatDebug("eqAxioms:\n"+ cnfString(eqFreePropToSolvable(eqAxioms))) + // patmatDebug("pure:\n"+ cnfString(eqFreePropToSolvable(pure))) + + stopTimer(patmatAnaVarEq, start) - And(eqAxioms, pure) + (eqAxioms, pure) } - // convert propositional logic formula to CNF - // http://www.dcs.warwick.ac.uk/people/academic/Ranko.Lazic/fsv/fsv6.pdf - def negationNormalForm(p: Prop): Prop = p match { - case And(a, b) => And(negationNormalForm(a), negationNormalForm(b)) - case Or(a, b) => Or(negationNormalForm(a), negationNormalForm(b)) - case Not(And(a, b)) => negationNormalForm(Or(Not(a), Not(b))) - case Not(Or(a, b)) => negationNormalForm(And(Not(a), Not(b))) - case Not(Not(p)) => negationNormalForm(p) - case Not(True) => False - case Not(False) => True - case True - | False - | (_ : Sym) - | Not(_ : Sym) => p + + type Formula + def andFormula(a: Formula, b: Formula): Formula + + // may throw an IllegalArgumentException + def propToSolvable(p: Prop) = { + val (eqAxioms, pure :: Nil) = removeVarEq(List(p), considerNull = false) + eqFreePropToSolvable(And(eqAxioms, pure)) } + def eqFreePropToSolvable(p: Prop): Formula + def cnfString(f: Formula): String + + type Model = Map[Sym, Boolean] + val EmptyModel: Model + val NoModel: Model + + def findModelFor(f: Formula): Model + def findAllModelsFor(f: Formula): List[Model] + } + + trait CNF extends Logic { // CNF: a formula is a conjunction of clauses - type Formula = List[Clause] ; def formula(c: Clause*): Formula = c.toList + type Formula = Array[Clause] + def formula(c: Clause*): Formula = c.toArray + def andFormula(a: Formula, b: Formula): Formula = a ++ b // a clause is a disjunction of distinct literals - type Clause = Set[Lit] ; def clause(l: Lit*): Clause = l.toSet + type Clause = Set[Lit] + def clause(l: Lit*): Clause = l.toSet + @inline private def merge(a: Clause, b: Clause) = a ++ b + + type Lit + def Lit(sym: Sym, pos: Boolean = true): Lit + + // throws an IllegalArgumentException when the prop results in a CNF that's too big + def eqFreePropToSolvable(p: Prop): Formula = { + // TODO: for now, reusing the normalization from DPLL + def negationNormalForm(p: Prop): Prop = p match { + case And(a, b) => And(negationNormalForm(a), negationNormalForm(b)) + case Or(a, b) => Or(negationNormalForm(a), negationNormalForm(b)) + case Not(And(a, b)) => negationNormalForm(Or(Not(a), Not(b))) + case Not(Or(a, b)) => negationNormalForm(And(Not(a), Not(b))) + case Not(Not(p)) => negationNormalForm(p) + case Not(True) => False + case Not(False) => True + case True + | False + | (_ : Sym) + | Not(_ : Sym) => p + } + + val TrueF = formula() + val FalseF = formula(clause()) + def lit(s: Sym) = formula(clause(Lit(s))) + def negLit(s: Sym) = formula(clause(Lit(s, false))) + + def conjunctiveNormalForm(p: Prop, budget: Int = 256): Formula = { + def distribute(a: Formula, b: Formula, budget: Int): Formula = + if (budget <= 0) throw new IllegalArgumentException("CNF budget exceeded") + else + (a, b) match { + // true \/ _ = true + // _ \/ true = true + case (trueA, trueB) if trueA.size == 0 || trueB.size == 0 => TrueF + // lit \/ lit + case (a, b) if a.size == 1 && b.size == 1 => formula(merge(a(0), b(0))) + // (c1 /\ ... /\ cn) \/ d = ((c1 \/ d) /\ ... /\ (cn \/ d)) + // d \/ (c1 /\ ... /\ cn) = ((d \/ c1) /\ ... /\ (d \/ cn)) + case (cs, ds) => + val (big, small) = if (cs.size > ds.size) (cs, ds) else (ds, cs) + big flatMap (c => distribute(formula(c), small, budget - (big.size*small.size))) + } - // a literal is a (possibly negated) variable - case class Lit(sym: Sym, pos: Boolean = true) { - override def toString = if (!pos) "-"+ sym.toString else sym.toString - def unary_- = Lit(sym, !pos) + if (budget <= 0) throw new IllegalArgumentException("CNF budget exceeded") + + p match { + case True => TrueF + case False => FalseF + case s: Sym => lit(s) + case Not(s: Sym) => negLit(s) + case And(a, b) => + val cnfA = conjunctiveNormalForm(a, budget - 1) + val cnfB = conjunctiveNormalForm(b, budget - cnfA.size) + cnfA ++ cnfB + case Or(a, b) => + val cnfA = conjunctiveNormalForm(a) + val cnfB = conjunctiveNormalForm(b) + distribute(cnfA, cnfB, budget - (cnfA.size + cnfB.size)) + } + } + + val start = startTimer(patmatCNF) + val res = conjunctiveNormalForm(negationNormalForm(p)) + stopTimer(patmatCNF, start) + patmatCNFSizes(res.size) += 1 + +// patmatDebug("cnf for\n"+ p +"\nis:\n"+cnfString(res)) + res } - val TrueF = formula() - val FalseF = formula(clause()) - def lit(s: Sym) = formula(clause(Lit(s))) - def negLit(s: Sym) = formula(clause(Lit(s, false))) + } - def conjunctiveNormalForm(p: Prop): Formula = { - def distribute(a: Formula, b: Formula): Formula = (a, b) match { - // true \/ _ = true - case (TrueF, _) => TrueF - // _ \/ true = true - case (_, TrueF) => TrueF - // lit \/ lit - case (List(a), List(b)) => formula(a ++ b) - // (c1 /\ ... /\ cn) \/ d = ((c1 \/ d) /\ ... /\ (cn \/ d)) - case (cs, d) if cs.tail nonEmpty => cs flatMap (c => distribute(formula(c), d)) - // d \/ (c1 /\ ... /\ cn) = ((d \/ c1) /\ ... /\ (d \/ cn)) - case (d, cs) if cs.tail nonEmpty => cs flatMap (c => distribute(d, formula(c))) + trait DPLLSolver extends CNF { + // a literal is a (possibly negated) variable + def Lit(sym: Sym, pos: Boolean = true) = new Lit(sym, pos) + class Lit(val sym: Sym, val pos: Boolean) { + override def toString = if (!pos) "-"+ sym.toString else sym.toString + override def equals(o: Any) = o match { + case o: Lit => (o.sym == sym) && (o.pos == pos) + case _ => false } + override def hashCode = sym.hashCode + pos.hashCode - p match { - case True => TrueF - case False => FalseF - case s: Sym => lit(s) - case Not(s: Sym) => negLit(s) - case And(a, b) => conjunctiveNormalForm(a) ++ conjunctiveNormalForm(b) - case Or(a, b) => distribute(conjunctiveNormalForm(a), conjunctiveNormalForm(b)) - } + def unary_- = Lit(sym, !pos) } - def normalize(p: Prop) = conjunctiveNormalForm(negationNormalForm(removeVarEq(p))) def cnfString(f: Formula) = alignAcrossRows(f map (_.toList) toList, "\\/", " /\\\n") // adapted from http://lara.epfl.ch/w/sav10:simple_sat_solver (original by Hossein Hojjat) - type Model = Map[Sym, Boolean] +// type Model = Map[Sym, Boolean] val EmptyModel = Map.empty[Sym, Boolean] + val NoModel: Model = null // returns all solutions, if any (TODO: better infinite recursion backstop -- detect fixpoint??) - def fullDPLL(f: Formula): List[Model] = { + def findAllModelsFor(f: Formula): List[Model] = { + val vars: Set[Sym] = f.flatMap(_ collect {case l: Lit => l.sym}).toSet + // patmatDebug("vars "+ vars) // the negation of a model -(S1=True/False /\ ... /\ SN=True/False) = clause(S1=False/True, ...., SN=False/True) def negateModel(m: Model) = clause(m.toSeq.map{ case (sym, pos) => Lit(sym, !pos) } : _*) - def findAllModels(f: Formula, models: List[Model], recursionDepthAllowed: Int = 20): List[Model]= + def findAllModels(f: Formula, models: List[Model], recursionDepthAllowed: Int = 10): List[Model]= if (recursionDepthAllowed == 0) models else { - val (ok, model) = DPLL(f) + // patmatDebug("solving\n"+ cnfString(f)) + val model = findModelFor(f) // if we found a solution, conjunct the formula with the model's negation and recurse - if (ok) findAllModels(f :+ negateModel(model), model :: models, recursionDepthAllowed - 1) + if (model ne NoModel) { + val unassigned = (vars -- model.keySet).toList + // patmatDebug("unassigned "+ unassigned +" in "+ model) + def force(lit: Lit) = { + val model = withLit(findModelFor(dropUnit(f, lit)), lit) + if (model ne NoModel) List(model) + else Nil + } + val forced = unassigned flatMap { s => + force(Lit(s, true)) ++ force(Lit(s, false)) + } + // patmatDebug("forced "+ forced) + val negated = negateModel(model) + findAllModels(f :+ negated, model :: (forced ++ models), recursionDepthAllowed - 1) + } else models } findAllModels(f, Nil) } - def DPLL(f: Formula): (Boolean, Model) = { - @inline def withLit(res: (Boolean, Model), l: Lit) = (res._1, res._2 + (l.sym -> l.pos)) - @inline def orElse(a: (Boolean, Model), b: => (Boolean, Model)) = if (a._1) a else b + @inline private def withLit(res: Model, l: Lit): Model = if (res eq NoModel) NoModel else res + (l.sym -> l.pos) + @inline private def dropUnit(f: Formula, unitLit: Lit) = { + val negated = -unitLit + // drop entire clauses that are trivially true + // (i.e., disjunctions that contain the literal we're making true in the returned model), + // and simplify clauses by dropping the negation of the literal we're making true + // (since False \/ X == X) + f.filterNot(_.contains(unitLit)).map(_ - negated) + } + + def findModelFor(f: Formula): Model = { + @inline def orElse(a: Model, b: => Model) = if (a ne NoModel) a else b // patmatDebug("dpll\n"+ cnfString(f)) - if (f isEmpty) (true, EmptyModel) - else if(f exists (_.isEmpty)) (false, EmptyModel) - else f.find(_.size == 1) map { unitClause => - val unitLit = unitClause.head - // patmatDebug("unit: "+ unitLit) - val negated = -unitLit - // drop entire clauses that are trivially true - // (i.e., disjunctions that contain the literal we're making true in the returned model), - // and simplify clauses by dropping the negation of the literal we're making true - // (since False \/ X == X) - val simplified = f.filterNot(_.contains(unitLit)).map(_ - negated) - withLit(DPLL(simplified), unitLit) - } getOrElse { - // partition symbols according to whether they appear in positive and/or negative literals - val pos = new HashSet[Sym]() - val neg = new HashSet[Sym]() - f.foreach{_.foreach{ lit => - if (lit.pos) pos += lit.sym else neg += lit.sym - }} - // appearing in both positive and negative - val impures = pos intersect neg - // appearing only in either positive/negative positions - val pures = (pos ++ neg) -- impures - - if (pures nonEmpty) { - val pureSym = pures.head - // turn it back into a literal - // (since equality on literals is in terms of equality - // of the underlying symbol and its positivity, simply construct a new Lit) - val pureLit = Lit(pureSym, pos(pureSym)) - // patmatDebug("pure: "+ pureLit +" pures: "+ pures +" impures: "+ impures) - val simplified = f.filterNot(_.contains(pureLit)) - withLit(DPLL(simplified), pureLit) - } else { - val split = f.head.head - // patmatDebug("split: "+ split) - orElse(DPLL(f :+ clause(split)), DPLL(f :+ clause(-split))) + val start = startTimer(patmatAnaDPLL) + + val satisfiableWithModel: Model = + if (f isEmpty) EmptyModel + else if(f exists (_.isEmpty)) NoModel + else f.find(_.size == 1) match { + case Some(unitClause) => + val unitLit = unitClause.head + // patmatDebug("unit: "+ unitLit) + withLit(findModelFor(dropUnit(f, unitLit)), unitLit) + case _ => + // partition symbols according to whether they appear in positive and/or negative literals + val pos = new HashSet[Sym]() + val neg = new HashSet[Sym]() + f.foreach{_.foreach{ lit => + if (lit.pos) pos += lit.sym else neg += lit.sym + }} + // appearing in both positive and negative + val impures = pos intersect neg + // appearing only in either positive/negative positions + val pures = (pos ++ neg) -- impures + + if (pures nonEmpty) { + val pureSym = pures.head + // turn it back into a literal + // (since equality on literals is in terms of equality + // of the underlying symbol and its positivity, simply construct a new Lit) + val pureLit = Lit(pureSym, pos(pureSym)) + // patmatDebug("pure: "+ pureLit +" pures: "+ pures +" impures: "+ impures) + val simplified = f.filterNot(_.contains(pureLit)) + withLit(findModelFor(simplified), pureLit) + } else { + val split = f.head.head + // patmatDebug("split: "+ split) + orElse(findModelFor(f :+ clause(split)), findModelFor(f :+ clause(-split))) + } } - } + + stopTimer(patmatAnaDPLL, start) + + satisfiableWithModel } } + /** * Represent a match as a formula in propositional logic that encodes whether the match matches (abstractly: we only consider types) * */ trait SymbolicMatchAnalysis extends TreeMakerApproximation with Logic { self: CodegenCore => + def prepareNewAnalysis() = { Var.resetUniques(); Const.resetUniques() } + object Var { private var _nextId = 0 def nextId = {_nextId += 1; _nextId} + def resetUniques() = {_nextId = 0; uniques.clear()} private val uniques = new collection.mutable.HashMap[Tree, Var] def apply(x: Tree): Var = uniques getOrElseUpdate(x, new Var(x, x.tpe)) } class Var(val path: Tree, fullTp: Type, checked: Boolean = true) extends AbsVar { + private[this] val id: Int = Var.nextId + + // private[this] var canModify: Option[Array[StackTraceElement]] = None + @inline private[this] def ensureCanModify = {} //if (canModify.nonEmpty) patmatDebug("BUG!"+ this +" modified after having been observed: "+ canModify.get.mkString("\n")) + + @inline private[this] def observed = {} //canModify = Some(Thread.currentThread.getStackTrace) + + // don't access until all potential equalities have been registered using registerEquality + private[this] val symForEqualsTo = new collection.mutable.HashMap[Const, Sym] + // when looking at the domain, we only care about types we can check at run time val domainTp: Type = checkableType(fullTp) + private[this] var _considerNull = false + def considerNull: Unit = { ensureCanModify; if (NullTp <:< domainTp) _considerNull = true } + // case None => domain is unknown, // case Some(List(tps: _*)) => domain is exactly tps // we enumerate the subtypes of the full type, as that allows us to filter out more types statically, // once we go to run-time checks (on Const's), convert them to checkable types // TODO: there seems to be bug for singleton domains (variable does not show up in model) - val domain = if (checked) enumerateSubtypes(fullTp).map(_.map(Const).toSet) else None - - def describe = toString + ": "+ fullTp + domain.map(_.map(_.tp).mkString(" ::= ", " | ", "")).getOrElse(" ::= ??") +" // = "+ path - def domainEnumerable = domain.nonEmpty + lazy val domain: Option[Set[Const]] = + if (!checked) None + else { + val subConsts = enumerateSubtypes(fullTp).map{ tps => + tps.toSet[Type].map{ tp => + val domainC = TypeConst(tp) + registerEquality(domainC) + domainC + } + } - private val domMap = new collection.mutable.HashMap[Const, Sym] - private def symForEqualsTo(c: Const) = { - domMap getOrElseUpdate(c, { - // println("creating symbol for equality "+ this +" = "+ c) - Sym(this, c) - }) - } + val allConsts = + if (! _considerNull) subConsts + else { + registerEquality(NullConst) + subConsts map (_ + NullConst) + } - // for this var, call it V, turn V = C into the equivalent proposition in boolean logic - // over all executions of this method on the same Var object, - def propForEqualsTo(c: Const): Prop = { - domain match { - case None => symForEqualsTo(c) - case Some(domainConsts) => - val domainTps = domainConsts map (_.tp) - val checkedTp = c.tp - // find all the domain types that could make the type test true - // if the checked type is a supertype of the lub of the domain, - // we'll end up \/'ing the whole domain together, - // but must not simplify to True, as the type test may also fail... - val matches = domainTps.filter(_ <:< checkedTp).map{ tp => symForEqualsTo(Const(tp)) } - // println("type-equals-prop for "+ this +" = "+ c +": "+ (checkedTp, domainTp, domainTps) +" matches: "+ matches) - - if (matches isEmpty) False else matches.reduceLeft(Or) + observed; allConsts } - } - def equalitySyms: Set[Sym] = domMap.values.toSet + // accessing after calling considerNull will result in inconsistencies + lazy val domainSyms: Option[Set[Sym]] = domain map { _ map symForEqualsTo } - private[this] val id: Int = Var.nextId + + // populate equalitySyms + // don't care about the result, but want only one fresh symbol per distinct constant c + def registerEquality(c: Const): Unit = {ensureCanModify; symForEqualsTo getOrElseUpdate(c, Sym(this, c))} + + // don't access until all potential equalities have been registered using registerEquality + lazy val equalitySyms = {observed; symForEqualsTo.values.toList} + + // return the symbol that represents this variable being equal to the constant `c`, if it exists, otherwise False (for robustness) + // (registerEquality(c) must have been called prior, either when constructing the domain or from outside) + def propForEqualsTo(c: Const): Prop = {observed; symForEqualsTo.getOrElse(c, False)} + + + // don't call until all equalities have been registered and considerNull has been called (if needed) + def describe = toString + ": " + fullTp + domain.map(_.mkString(" ::= ", " | ", "// "+ symForEqualsTo.keys)).getOrElse(symForEqualsTo.keys.mkString(" ::= ", " | ", " | ...")) + " // = " + path override def toString = "V"+ id + + + + // when V = C, which other V = Ci are implied? + // V = null is an exclusive assignment, since null precludes any type test being true + // V = Any does not imply anything (except non-nullness) + // consider: + // when V's domain is closed, say V : X ::= A | B | C, and we have some value constants, say U and V, of type X: + // (x: X) match { case U => case V => case _ : X => } + // + // V's equalityConsts (for the above match): TC(X), TC(A), TC(B), TC(C), VC(U), VC(V) + // Set(TC(X), VC(U), VC(V)).forall(c => Set(TC(A), TC(B), TC(C)).forall(_.covers(c))) + // Set(VC(U), VC(V), TC(A), TC(B), TC(C)).forall(_.implies(TC(X)) + // impliedSuper for TC(X) is empty (since it's at the top of the lattice), + // but since we have a closed domain, we know that also one of the partitions must hold + // thus, TC(X) implies TC(A) \/ TC(B) \/ TC(C), + // we only need to add this implication when impliedSuper is empty, + // since that'll eventually be the case (transitive closure & acyclic graphs ftw) +// def impliedProp(c: Const): Prop = if (c eq NullConst) True else { +// val impliedSuper = /\((equalityConsts filter { other => (c != other) && c.implies(other) && !other.implies(c) } map symForEqualsTo)) +// +// val implied = +// if (impliedSuper == True) domain match { case None => True +// case Some(domCs) => \/(domCs filter { _.covers(c) } map symForEqualsTo) +// } else impliedSuper +// +// // patmatDebug("impliedProp: "+(this, c, impliedSuper, implied)) +// implied +// } +// private lazy val equalityConsts = symForEqualsTo.keySet } // all our variables range over types // a literal constant becomes ConstantType(Constant(v)) when the type allows it (roughly, anyval + string + null) // equality between variables: SingleType(x) (note that pattern variables cannot relate to each other -- it's always patternVar == nonPatternVar) - case class Const(tp: Type) { - override def toString = tp.toString + object Const { + def resetUniques() = {_nextTypeId = 0; _nextValueId = 0; uniques.clear()} // patmatDebug("RESET") + + private var _nextTypeId = 0 + def nextTypeId = {_nextTypeId += 1; _nextTypeId} + + private var _nextValueId = 0 + def nextValueId = {_nextValueId += 1; _nextValueId} + + private val uniques = new collection.mutable.HashMap[Type, Const] + private[SymbolicMatchAnalysis] def unique(tp: Type, mkFresh: => Const): Const = + uniques.get(tp).getOrElse( + uniques.find {case (oldTp, oldC) => oldTp =:= tp} match { + case Some((_, c)) => c + case _ => + val fresh = mkFresh + uniques(tp) = fresh + fresh + }) + } - def toValueString = tp match { - case ConstantType(c) => c.escapedStringValue - case _ => tp.toString + sealed abstract class Const extends AbsConst { + protected def tp: Type + protected def wideTp: Type + + def isAny = wideTp.typeSymbol == AnyClass + +// final def covers(other: Const): Boolean = { +// val r = (this, other) match { +// case (_: ValueConst, _: ValueConst) => this == other // hashconsed +// case (TypeConst(a) , _: ValueConst) => a <:< other.wideTp +// case (_ , _: TypeConst) => tp <:< other.tp +// case _ => false +// } +// // if(r) patmatDebug("covers : "+(this, other)) +// // else patmatDebug("NOT covers: "+(this, other)) +// r +// } + + final def implies(other: Const): Boolean = { + val r = (this, other) match { + case (_: ValueConst, _: ValueConst) => this == other // hashconsed + case (_: ValueConst, _: TypeConst) => tp <:< other.tp + case (_: TypeConst, _) => tp <:< other.tp + case _ => false + } + // if(r) patmatDebug("implies : "+(this, other)) + // else patmatDebug("NOT implies: "+(this, other)) + r + } + + // does V = C preclude V having value `other`? V = null is an exclusive assignment, + // but V = 1 does not preclude V = Int, or V = Any + final def excludes(other: Const): Boolean = { + val r = (this, other) match { + case (_, NullConst) => true + case (NullConst, _) => true + // this causes false negative for unreachability, but that's ok: + // example: val X = 1; val Y = 1; (2: Int) match { case X => case Y => /* considered reachable */ } + case (_: ValueConst, _: ValueConst) => this != other + case (_: ValueConst, _: TypeConst) => !((tp <:< other.tp) || (other.tp <:< wideTp)) + case (_: TypeConst, _: ValueConst) => !((other.tp <:< tp) || (tp <:< other.wideTp)) + case (_: TypeConst, _: TypeConst) => !((tp <:< other.tp) || (other.tp <:< tp)) + case _ => false + } + // if(r) patmatDebug("excludes : "+(this, other)) + // else patmatDebug("NOT excludes: "+(this, other)) + r + } + + // the equality symbol for V = C is looked up by C + final override def equals(other: Any): Boolean = other match { case o: Const => this eq o case _ => false } + } + + + object TypeConst { + def apply(tp: Type) = { + if (tp =:= NullTp) NullConst + else if (tp.isInstanceOf[SingletonType]) ValueConst.fromType(tp) + else Const.unique(tp, new TypeConst(tp)) + } + def unapply(c: TypeConst): Some[Type] = Some(c.tp) + } + + // corresponds to a type test that does not imply any value-equality (well, except for outer checks, which we don't model yet) + sealed class TypeConst(val tp: Type) extends Const { + assert(!(tp =:= NullTp)) + private[this] val id: Int = Const.nextTypeId + + val wideTp = tp.widen + + override def toString = tp.toString //+"#"+ id + } + + // p is a unique type or a constant value + object ValueConst { + def fromType(tp: Type) = { + assert(tp.isInstanceOf[SingletonType]) + val toString = tp match { + case ConstantType(c) => c.escapedStringValue + case _ => tp.toString + } + Const.unique(tp, new ValueConst(tp, tp.widen, toString)) + } + def apply(p: Tree) = { + val tp = p.tpe.normalize + if (tp =:= NullTp) NullConst + else { + val wideTp = { + if (p.hasSymbol && p.symbol.isStable) tp.asSeenFrom(tp.prefix, p.symbol.owner).widen + else tp.widen + } + + val narrowTp = + if (tp.isInstanceOf[SingletonType]) tp + else p match { + case Literal(c) => + if (c.tpe.typeSymbol == UnitClass) c.tpe + else ConstantType(c) + case p if p.symbol.isStable => + singleType(tp.prefix, p.symbol) + case x => + // TODO: better type + x.tpe.narrow + } + + val toString = + if (p.hasSymbol && p.symbol.isStable) p.symbol.name.toString // tp.toString + else p.toString //+"#"+ id + + Const.unique(narrowTp, new ValueConst(narrowTp, checkableType(wideTp), toString)) // must make wide type checkable so that it is comparable to types from TypeConst + } + } + } + sealed class ValueConst(val tp: Type, val wideTp: Type, override val toString: String) extends Const { + // patmatDebug("VC"+(tp, wideTp, toString)) + assert(!(tp =:= NullTp)) + private[this] val id: Int = Const.nextValueId + } + + lazy val NullTp = ConstantType(Constant(null)) + case object NullConst extends Const { + protected def tp = NullTp + protected def wideTp = NullTp + + def isValue = true + override def toString = "null" + } + + + // turns a case (represented as a list of abstract tests) + // into a proposition that is satisfiable if the case may match + def symbolicCase(tests: List[Test], modelNull: Boolean = false): Prop = { + def symbolic(t: Cond): Prop = t match { + case AndCond(a, b) => And(symbolic(a), symbolic(b)) + case OrCond(a, b) => Or(symbolic(a), symbolic(b)) + case Top => True + case Havoc => False + case TypeCond(p, pt) => Eq(Var(p), TypeConst(checkableType(pt))) + case EqualityCond(p, q) => Eq(Var(p), ValueConst(q)) + case NonNullCond(p) => if (!modelNull) True else Not(Eq(Var(p), NullConst)) + } + + val testsBeforeBody = tests.takeWhile(t => !t.treeMaker.isInstanceOf[BodyTreeMaker]) + /\(testsBeforeBody.map(t => symbolic(t.cond))) + } + + // TODO: model dependencies between variables: if V1 corresponds to (x: List[_]) and V2 is (x.hd), V2 cannot be assigned when V1 = null or V1 = Nil + // right now hackily implement this by pruning counter-examples + // unreachability would also benefit from a more faithful representation + + // reachability (dead code) + + // computes the first 0-based case index that is unreachable (if any) + // a case is unreachable if it implies its preceding cases + // call C the formula that is satisfiable if the considered case matches + // call P the formula that is satisfiable if the cases preceding it match + // the case is reachable if there is a model for -P /\ C, + // thus, the case is unreachable if there is no model for -(-P /\ C), + // or, equivalently, P \/ -C, or C => P + def unreachableCase(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type): Option[Int] = { + // customize TreeMakersToConds (which turns a tree of tree makers into a more abstract DAG of tests) + // when approximating the current case (which we hope is reachable), be optimistic about the unknowns + object reachabilityApproximation extends TreeMakersToConds(prevBinder) { + def makeCondOptimistic(tm: TreeMaker)(recurse: TreeMaker => Cond): Cond = tm match { + // for unreachability, let's assume a guard always matches (unless we statically determined otherwise) + // otherwise, a guarded case would be considered unreachable + case GuardTreeMaker(guard) => + guard.tpe match { + case ConstantType(Constant(false)) => Havoc // not the best name; however, symbolically, 'Havoc' becomes 'False' + case _ => Top + } + // similar to a guard, user-defined extractors should not cause us to freak out + // if we're not 100% sure it does not match (i.e., its result type is None or Constant(false) -- TODO), + // let's stay optimistic and assume it does + case ExtractorTreeMaker(_, _, _, _) + | ProductExtractorTreeMaker(_, Some(_), _) => Top + // TODO: consider length-checks + case _ => + makeCond(tm)(recurse) + } + + // be pessimistic when approximating the prefix of the current case + // we hope the prefix fails so that we might get to the current case, which we hope is not dead + def makeCondPessimistic(tm: TreeMaker)(recurse: TreeMaker => Cond): Cond = makeCond(tm)(recurse) + } + + val start = startTimer(patmatAnaReach) + + // use the same approximator so we share variables, + // but need different conditions depending on whether we're conservatively looking for failure or success + val testCasesOk = reachabilityApproximation.approximateMatch(cases, reachabilityApproximation.makeCondOptimistic) + val testCasesFail = reachabilityApproximation.approximateMatchAgain(cases, reachabilityApproximation.makeCondPessimistic) + + reachabilityApproximation.discard() + prepareNewAnalysis() + + val propsCasesOk = testCasesOk map (t => symbolicCase(t, modelNull = true)) + val propsCasesFail = testCasesFail map (t => Not(symbolicCase(t, modelNull = true))) + val (eqAxiomsFail, symbolicCasesFail) = removeVarEq(propsCasesFail, considerNull = true) + val (eqAxiomsOk, symbolicCasesOk) = removeVarEq(propsCasesOk, considerNull = true) + + try { + // most of the time eqAxiomsFail == eqAxiomsOk, but the different approximations might cause different variables to disapper in general + val eqAxiomsCNF = + if (eqAxiomsFail == eqAxiomsOk) eqFreePropToSolvable(eqAxiomsFail) + else eqFreePropToSolvable(And(eqAxiomsFail, eqAxiomsOk)) + + var prefix = eqAxiomsCNF + var prefixRest = symbolicCasesFail + var current = symbolicCasesOk + var reachable = true + var caseIndex = 0 + + // patmatDebug("reachability, vars:\n"+ ((propsCasesFail flatMap gatherVariables) map (_.describe) mkString ("\n"))) + // patmatDebug("equality axioms:\n"+ cnfString(eqAxiomsCNF)) + + // invariant (prefixRest.length == current.length) && (prefix.reverse ++ prefixRest == symbolicCasesFail) + // termination: prefixRest.length decreases by 1 + while (prefixRest.nonEmpty && reachable) { + val prefHead = prefixRest.head + caseIndex += 1 + prefixRest = prefixRest.tail + if (prefixRest.isEmpty) reachable = true + else { + prefix = andFormula(eqFreePropToSolvable(prefHead), prefix) + current = current.tail + val model = findModelFor(andFormula(eqFreePropToSolvable(current.head), prefix)) + + // patmatDebug("trying to reach:\n"+ cnfString(current.head) +"\nunder prefix:\n"+ cnfString(prefix)) + // if (ok) patmatDebug("reached: "+ modelString(model)) + + reachable = model ne NoModel + } + } + + stopTimer(patmatAnaReach, start) + + if (reachable) None else Some(caseIndex) + } catch { + case e : IllegalArgumentException => +// patmatDebug(util.Position.formatMessage(prevBinder.pos, "Cannot check match for reachability", false)) +// e.printStackTrace() + None // CNF budget exceeded } } + // exhaustivity + // make sure it's not a primitive, else (5: Byte) match { case 5 => ... } sees no Byte // TODO: domain of feasibly enumerable built-in types (enums, char?) def enumerateSubtypes(tp: Type): Option[List[Type]] = @@ -1945,12 +2399,6 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL Some(validSubTypes) } - def narrowTypeOf(p: Tree) = p match { - case Literal(c) => ConstantType(c) - case Ident(_) if p.symbol.isStable => singleType(p.tpe.prefix, p.symbol) - case x => x.tpe.narrow - } - // approximate a type to the static type that is fully checkable at run time, // hiding statically known but dynamically uncheckable information using existential quantification // TODO: this is subject to the availability of TypeTags (since an abstract type with a type tag is checkable at run time) @@ -1989,8 +2437,9 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL // - back off (to avoid crying exhaustive too often) when: // - there are guards --> // - there are extractor calls (that we can't secretly/soundly) rewrite + val start = startTimer(patmatAnaExhaust) var backoff = false - object exhaustivityApproximation extends TreeMakersToConds(prevBinder, cases) { + object exhaustivityApproximation extends TreeMakersToConds(prevBinder) { def makeCondExhaustivity(tm: TreeMaker)(recurse: TreeMaker => Cond): Cond = tm match { case p @ ExtractorTreeMaker(extractor, Some(lenCheck), testedBinder, _) => p.checkedLength match { @@ -2020,27 +2469,16 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL } } - def symbolic(t: Cond): Prop = t match { - case AndCond(a, b) => And(symbolic(a), symbolic(b)) - case OrCond(a, b) => Or(symbolic(a), symbolic(b)) - case Top => True - case Havoc => False - case TypeCond(p, pt) => Eq(Var(p), Const(checkableType(pt))) - case EqualityCond(p, q) => Eq(Var(p), Const(narrowTypeOf(q))) - case NonNullCond(p) => True // ignoring nullness because it generates too much noise Not(Eq(Var(p), Const(NullClass.tpe))) - } + val tests = exhaustivityApproximation.approximateMatch(cases, exhaustivityApproximation.makeCondExhaustivity) - def symbolicCase(tests: List[Test]) = { - val testsBeforeBody = tests.takeWhile(t => !t.treeMaker.isInstanceOf[BodyTreeMaker]) - testsBeforeBody.map(t => symbolic(t.cond)).foldLeft(True: Prop)(And) - } + if (backoff) Nil else { + val prevBinderTree = exhaustivityApproximation.binderToUniqueTree(prevBinder) - val tests = exhaustivityApproximation.approximateMatch(exhaustivityApproximation.makeCondExhaustivity) + exhaustivityApproximation.discard() + prepareNewAnalysis() - if (backoff) Nil else { - val symbolicCases = tests map symbolicCase + val symbolicCases = tests map (symbolicCase(_, modelNull = false)) - val prevBinderTree = exhaustivityApproximation.binderToUniqueTree(prevBinder) // TODO: null tests generate too much noise, so disabled them -- is there any way to bring them back? // assuming we're matching on a non-null scrutinee (prevBinder), when does the match fail? @@ -2053,8 +2491,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL // val matchFails = And(symbolic(nonNullScrutineeCond), Not(symbolicCases reduceLeft (Or(_, _)))) // when does the match fail? - val matchFails = Not(symbolicCases reduceLeft (Or(_, _))) - + val matchFails = Not(\/(symbolicCases)) // debug output: // patmatDebug("analysing:") @@ -2064,15 +2501,25 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL // val vars = gatherVariables(matchFails) // patmatDebug("\nvars:\n"+ (vars map (_.describe) mkString ("\n"))) // - // patmatDebug("\nmatchFails as CNF:\n"+ cnfString(normalize(matchFails))) + // patmatDebug("\nmatchFails as CNF:\n"+ cnfString(propToSolvable(matchFails))) + + try { + // find the models (under which the match fails) + val matchFailModels = findAllModelsFor(propToSolvable(matchFails)) - // find the models (under which the match fails) - val matchFailModels = fullDPLL(normalize(matchFails)) + val scrutVar = Var(prevBinderTree) + val counterExamples = matchFailModels.map(modelToCounterExample(scrutVar)) - val scrutVar = Var(prevBinderTree) - val counterExamples = matchFailModels.map(modelToCounterExample(scrutVar)) + val pruned = CounterExample.prune(counterExamples).map(_.toString).sorted - CounterExample.prune(counterExamples).map(_.toString).sorted + stopTimer(patmatAnaExhaust, start) + pruned + } catch { + case e : IllegalArgumentException => + // patmatDebug(util.Position.formatMessage(prevBinder.pos, "Cannot check match for exhaustivity", false)) + // e.printStackTrace() + Nil // CNF budget exceeded + } } } @@ -2088,13 +2535,13 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL protected[SymbolicMatchAnalysis] def flattenConsArgs: List[CounterExample] = Nil def coveredBy(other: CounterExample): Boolean = this == other || other == WildcardExample } - case class ValueExample(c: Const) extends CounterExample { override def toString = c.toValueString } + case class ValueExample(c: ValueConst) extends CounterExample { override def toString = c.toString } case class TypeExample(c: Const) extends CounterExample { override def toString = "(_ : "+ c +")" } case class NegativeExample(nonTrivialNonEqualTo: List[Const]) extends CounterExample { override def toString = { val negation = - if (nonTrivialNonEqualTo.tail.isEmpty) nonTrivialNonEqualTo.head.toValueString - else nonTrivialNonEqualTo.map(_.toValueString).sorted.mkString("in (", ", ", ")") + if (nonTrivialNonEqualTo.tail.isEmpty) nonTrivialNonEqualTo.head.toString + else nonTrivialNonEqualTo.map(_.toString).sorted.mkString("in (", ", ", ")") "" } } @@ -2131,6 +2578,21 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL case object WildcardExample extends CounterExample { override def toString = "_" } case object NoExample extends CounterExample { override def toString = "??" } + @inline def modelToVarAssignment(model: Model): Map[Var, (Seq[Const], Seq[Const])] = + model.toSeq.groupBy{f => f match {case (sym, value) => sym.variable} }.mapValues{ xs => + val (trues, falses) = xs.partition(_._2) + (trues map (_._1.const), falses map (_._1.const)) + // should never be more than one value in trues... + } + + def varAssignmentString(varAssignment: Map[Var, (Seq[Const], Seq[Const])]) = + varAssignment.toSeq.sortBy(_._1.toString).map { case (v, (trues, falses)) => + val assignment = "== "+ (trues mkString("(", ", ", ")")) +" != ("+ (falses mkString(", ")) +")" + v +"(="+ v.path +": "+ v.domainTp +") "+ assignment + }.mkString("\n") + + def modelString(model: Model) = varAssignmentString(modelToVarAssignment(model)) + // return constructor call when the model is a true counter example // (the variables don't take into account type information derived from other variables, // so, naively, you might try to construct a counter example like _ :: Nil(_ :: _, _ :: _), @@ -2141,18 +2603,9 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL // x1.tl = ... // x1.hd.hd = ... // ... - val varAssignment = model.toSeq.groupBy{f => f match {case (sym, value) => sym.variable} }.mapValues{ xs => - val (trues, falses) = xs.partition(_._2) - (trues map (_._1.const), falses map (_._1.const)) - // should never be more than one value in trues... - } - - // patmatDebug("var assignment for model "+ model +":\n"+ - // varAssignment.toSeq.sortBy(_._1.toString).map { case (v, (trues, falses)) => - // val assignment = "== "+ (trues mkString("(", ", ", ")")) +" != ("+ (falses mkString(", ")) +")" - // v +"(="+ v.path +": "+ v.domainTp +") "+ assignment - // }.mkString("\n")) + val varAssignment = modelToVarAssignment(model) + // patmatDebug("var assignment for model "+ model +":\n"+ varAssignmentString(varAssignment)) // chop a path into a list of symbols def chop(path: Tree): List[Symbol] = path match { @@ -2198,7 +2651,9 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL // node in the tree that describes how to construct a counter-example case class VariableAssignment(variable: Var, equalTo: List[Const], notEqualTo: List[Const], fields: collection.mutable.Map[Symbol, VariableAssignment]) { - private lazy val ctor = (equalTo match { case List(Const(tp)) => tp case _ => variable.domainTp }).typeSymbol.primaryConstructor + // need to prune since the model now incorporates all super types of a constant (needed for reachability) + private lazy val prunedEqualTo = equalTo filterNot (subsumed => equalTo.exists(better => (better ne subsumed) && (better implies subsumed))) + private lazy val ctor = (prunedEqualTo match { case List(TypeConst(tp)) => tp case _ => variable.domainTp }).typeSymbol.primaryConstructor private lazy val ctorParams = if (ctor == NoSymbol || ctor.paramss.isEmpty) Nil else ctor.paramss.head private lazy val cls = if (ctor == NoSymbol) NoSymbol else ctor.owner private lazy val caseFieldAccs = if (cls == NoSymbol) Nil else cls.caseFieldAccessors @@ -2207,7 +2662,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL def allFieldAssignmentsLegal: Boolean = (fields.keySet subsetOf caseFieldAccs.toSet) && fields.values.forall(_.allFieldAssignmentsLegal) - private lazy val nonTrivialNonEqualTo = notEqualTo.filterNot{c => val sym = c.tp.typeSymbol; sym == AnyClass } // sym == NullClass || + private lazy val nonTrivialNonEqualTo = notEqualTo.filterNot{c => c.isAny } // NoExample if the constructor call is ill-typed // (thus statically impossible -- can we incorporate this into the formula?) @@ -2215,17 +2670,17 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL def toCounterExample(beBrief: Boolean = false): CounterExample = if (!allFieldAssignmentsLegal) NoExample else { -// println("describing "+ (variable, equalTo, notEqualTo, fields, cls, allFieldAssignmentsLegal)) - val res = equalTo match { + // patmatDebug("describing "+ (variable, equalTo, notEqualTo, fields, cls, allFieldAssignmentsLegal)) + val res = prunedEqualTo match { // a definite assignment to a value - case List(eq@Const(_: ConstantType)) if fields.isEmpty => ValueExample(eq) + case List(eq: ValueConst) if fields.isEmpty => ValueExample(eq) // constructor call // or we did not gather any information about equality but we have information about the fields // --> typical example is when the scrutinee is a tuple and all the cases first unwrap that tuple and only then test something interesting case _ if cls != NoSymbol && - ( equalTo.nonEmpty - || (fields.nonEmpty && !isPrimitiveValueClass(cls) && equalTo.isEmpty && notEqualTo.isEmpty)) => + ( prunedEqualTo.nonEmpty + || (fields.nonEmpty && !isPrimitiveValueClass(cls) && prunedEqualTo.isEmpty && notEqualTo.isEmpty)) => @inline def args(brevity: Boolean = beBrief) = { // figure out the constructor arguments from the field assignment @@ -2252,7 +2707,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL // TODO: improve reasoning -- in the mean time, a false negative is better than an annoying false positive case _ => NoExample } -// patmatDebug("described as: "+ res) + // patmatDebug("described as: "+ res) res } @@ -2715,8 +3170,14 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL with DeadCodeElimination with SwitchEmission with OptimizedCodegen - with SymbolicMatchAnalysis { self: TreeMakers => + with SymbolicMatchAnalysis + with DPLLSolver { self: TreeMakers => override def optimizeCases(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type, unchecked: Boolean): (List[List[TreeMaker]], List[Tree]) = { + if (!unchecked) { + unreachableCase(prevBinder, cases, pt) foreach { caseIndex => + typer.context.unit.warning(cases(caseIndex).last.pos, "unreachable code") + } + } val counterExamples = if (unchecked) Nil else exhaustive(prevBinder, cases, pt) if (counterExamples.nonEmpty) { val ceString = diff --git a/src/compiler/scala/tools/nsc/util/Statistics.scala b/src/compiler/scala/tools/nsc/util/Statistics.scala index 61c7695911..53ab6654ee 100644 --- a/src/compiler/scala/tools/nsc/util/Statistics.scala +++ b/src/compiler/scala/tools/nsc/util/Statistics.scala @@ -60,6 +60,14 @@ class Statistics extends scala.reflect.internal.util.Statistics { val macroExpandCount = new Counter val macroExpandNanos = new Timer + + val patmatNanos = new Timer + val patmatAnaDPLL = new Timer + val patmatAnaVarEq = new Timer + val patmatCNF = new Timer + val patmatAnaExhaust = new Timer + val patmatAnaReach = new Timer + val patmatCNFSizes = new collection.mutable.HashMap[Int, Int] withDefaultValue 0 } object Statistics extends Statistics @@ -71,7 +79,7 @@ abstract class StatisticsInfo { val global: Global import global._ - var phasesShown = List("parser", "typer", "erasure", "cleanup") + var phasesShown = List("parser", "typer", "patmat", "erasure", "cleanup") def countNodes(tree: Tree, counts: ClassCounts) { for (t <- tree) counts(t.getClass) += 1 @@ -83,10 +91,15 @@ abstract class StatisticsInfo { def showRelTyper(timer: Timer) = timer+showPercent(timer.nanos, typerNanos.nanos) - def showCounts(counts: ClassCounts) = + def showRelPatmat(timer: Timer) = + timer+showPercent(timer.nanos, patmatNanos.nanos) + + def showCounts[T](counts: scala.collection.mutable.Map[T, Int]) = counts.toSeq.sortWith(_._2 > _._2).map { - case (cls, cnt) => + case (cls: Class[_], cnt) => cls.toString.substring(cls.toString.lastIndexOf("$") + 1)+": "+cnt + case (o, cnt) => + o.toString +": "+cnt } def print(phase: Phase) = if (phasesShown contains phase.name) { @@ -169,6 +182,16 @@ abstract class StatisticsInfo { if (timer1 != null) inform("#timer1 : " + timer1) if (timer2 != null) inform("#timer2 : " + timer2) //for (t <- uniques.iterator) println("unique: "+t) + + if (phase.name == "patmat") { + inform("time spent in patmat : " + patmatNanos ) + inform(" of which DPLL : " + showRelPatmat(patmatAnaDPLL )) + inform("of which in CNF conversion : " + showRelPatmat(patmatCNF )) + inform(" CNF size counts : " + showCounts(patmatCNFSizes )) + inform("of which variable equality : " + showRelPatmat(patmatAnaVarEq )) + inform(" of which in exhaustivity : " + showRelPatmat(patmatAnaExhaust)) + inform("of which in unreachability : " + showRelPatmat(patmatAnaReach )) + } } } } diff --git a/test/files/neg/patmatexhaust.check b/test/files/neg/patmatexhaust.check index 1168f36e11..4556e6622f 100644 --- a/test/files/neg/patmatexhaust.check +++ b/test/files/neg/patmatexhaust.check @@ -14,6 +14,9 @@ patmatexhaust.scala:49: error: match may not be exhaustive. It would fail on the following inputs: Gp(), Gu def ma4(x:Deep) = x match { // missing cases: Gu, Gp ^ +patmatexhaust.scala:55: error: unreachable code + case _ if 1 == 0 => + ^ patmatexhaust.scala:53: error: match may not be exhaustive. It would fail on the following input: Gp() def ma5(x:Deep) = x match { @@ -34,4 +37,4 @@ patmatexhaust.scala:126: error: match may not be exhaustive. It would fail on the following input: C1() def ma10(x: C) = x match { // not exhaustive: C1 is not abstract. ^ -9 errors found +10 errors found diff --git a/test/files/neg/virtpatmat_reach_null.check b/test/files/neg/virtpatmat_reach_null.check new file mode 100644 index 0000000000..595c8ec889 --- /dev/null +++ b/test/files/neg/virtpatmat_reach_null.check @@ -0,0 +1,4 @@ +virtpatmat_reach_null.scala:13: error: unreachable code + case _ => // unreachable + ^ +one error found diff --git a/test/files/neg/virtpatmat_reach_null.flags b/test/files/neg/virtpatmat_reach_null.flags new file mode 100644 index 0000000000..e8fb65d50c --- /dev/null +++ b/test/files/neg/virtpatmat_reach_null.flags @@ -0,0 +1 @@ +-Xfatal-warnings \ No newline at end of file diff --git a/test/files/neg/virtpatmat_reach_null.scala b/test/files/neg/virtpatmat_reach_null.scala new file mode 100644 index 0000000000..6314a5b1d8 --- /dev/null +++ b/test/files/neg/virtpatmat_reach_null.scala @@ -0,0 +1,19 @@ +sealed abstract class Const { + final def excludes(other: Const) = + (this, other) match { + case (_, NullConst) => + case (NullConst, _) => + case (_: ValueConst, _: ValueConst) => + case (_: ValueConst, _: TypeConst) => + case (_: TypeConst, _: ValueConst) => + case (_: TypeConst, _: TypeConst) => + case (null, _) => + case (_, null) => + case null => + case _ => // unreachable + } +} + +sealed class TypeConst extends Const +sealed class ValueConst extends Const +case object NullConst extends Const diff --git a/test/files/neg/virtpatmat_reach_sealed_unsealed.check b/test/files/neg/virtpatmat_reach_sealed_unsealed.check new file mode 100644 index 0000000000..10638eff52 --- /dev/null +++ b/test/files/neg/virtpatmat_reach_sealed_unsealed.check @@ -0,0 +1,14 @@ +virtpatmat_reach_sealed_unsealed.scala:16: error: match may not be exhaustive. +It would fail on the following input: false + (true: Boolean) match { case true => } // not exhaustive, but reachable + ^ +virtpatmat_reach_sealed_unsealed.scala:18: error: unreachable code + (true: Boolean) match { case true => case false => case _ => } // exhaustive, last case is unreachable + ^ +virtpatmat_reach_sealed_unsealed.scala:19: error: unreachable code + (true: Boolean) match { case true => case false => case _: Boolean => } // exhaustive, last case is unreachable + ^ +virtpatmat_reach_sealed_unsealed.scala:20: error: unreachable code + (true: Boolean) match { case true => case false => case _: Any => } // exhaustive, last case is unreachable + ^ +four errors found diff --git a/test/files/neg/virtpatmat_reach_sealed_unsealed.flags b/test/files/neg/virtpatmat_reach_sealed_unsealed.flags new file mode 100644 index 0000000000..e8fb65d50c --- /dev/null +++ b/test/files/neg/virtpatmat_reach_sealed_unsealed.flags @@ -0,0 +1 @@ +-Xfatal-warnings \ No newline at end of file diff --git a/test/files/neg/virtpatmat_reach_sealed_unsealed.scala b/test/files/neg/virtpatmat_reach_sealed_unsealed.scala new file mode 100644 index 0000000000..13911dbd78 --- /dev/null +++ b/test/files/neg/virtpatmat_reach_sealed_unsealed.scala @@ -0,0 +1,21 @@ +sealed abstract class X +sealed case class A(x: Int) extends X + +// test reachability on mixed sealed / non-sealed matches +object Test extends App { + val B: X = A(0) + val C: X = A(1) + + // all cases are reachable and the match is exhaustive + (C: X) match { + case B => + case C => + case A(_) => + } + + (true: Boolean) match { case true => } // not exhaustive, but reachable + (true: Boolean) match { case true => case false => } // exhaustive, reachable + (true: Boolean) match { case true => case false => case _ => } // exhaustive, last case is unreachable + (true: Boolean) match { case true => case false => case _: Boolean => } // exhaustive, last case is unreachable + (true: Boolean) match { case true => case false => case _: Any => } // exhaustive, last case is unreachable +} \ No newline at end of file diff --git a/test/files/pos/virtpatmat_reach_const.scala b/test/files/pos/virtpatmat_reach_const.scala new file mode 100644 index 0000000000..b55b7cb229 --- /dev/null +++ b/test/files/pos/virtpatmat_reach_const.scala @@ -0,0 +1,11 @@ +// check the interaction between constants and type tests in creating the equality axioms +object Test { + type Formula = List[String] + val TrueF: Formula = List() + def distribute(a: Formula, b: Formula) = (a, b) match { + case (TrueF, _) => + case (_, TrueF) => // bug: considered unreachable + case (a :: Nil, b :: Nil) => + case _ => + } +} \ No newline at end of file -- cgit v1.2.3 From 9ebd4f94b5cd97f9e7cd369c0bc69e93248f8a5b Mon Sep 17 00:00:00 2001 From: Adriaan Moors Date: Sun, 27 May 2012 23:41:56 +0200 Subject: fixing bug found by unreachability --- src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala b/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala index 21b80df735..5f8ae240cc 100644 --- a/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala +++ b/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala @@ -1013,11 +1013,10 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL case SingleType(_, sym) => and(equalsTest(CODE.REF(sym), testedBinder), typeTest(testedBinder, expectedTp.widen)) // must use == to support e.g. List() == Nil case ThisType(sym) if sym.isModule => and(equalsTest(CODE.REF(sym), testedBinder), typeTest(testedBinder, expectedTp.widen)) - case ConstantType(const) => equalsTest(expTp(Literal(const)), testedBinder) - - case ThisType(sym) => eqTest(expTp(This(sym)), testedBinder) case ConstantType(Constant(null)) if testedBinder.info.widen <:< AnyRefClass.tpe => eqTest(expTp(CODE.NULL), testedBinder) + case ConstantType(const) => equalsTest(expTp(Literal(const)), testedBinder) + case ThisType(sym) => eqTest(expTp(This(sym)), testedBinder) // TODO: verify that we don't need to special-case Array // I think it's okay: -- cgit v1.2.3 From 8cab2fa15f5fbd3ee319a224cb3a8ed80158a5ee Mon Sep 17 00:00:00 2001 From: Adriaan Moors Date: Wed, 30 May 2012 18:45:24 +0200 Subject: allow disabling patmat analyses: -Xno-patmat-analysis --- .../reflect/internal/settings/MutableSettings.scala | 1 + src/compiler/scala/reflect/runtime/Settings.scala | 1 + .../scala/tools/nsc/settings/ScalaSettings.scala | 1 + .../scala/tools/nsc/typechecker/PatternMatching.scala | 18 ++++++++++-------- 4 files changed, 13 insertions(+), 8 deletions(-) diff --git a/src/compiler/scala/reflect/internal/settings/MutableSettings.scala b/src/compiler/scala/reflect/internal/settings/MutableSettings.scala index 45ba4ed3e6..8640a23aa7 100644 --- a/src/compiler/scala/reflect/internal/settings/MutableSettings.scala +++ b/src/compiler/scala/reflect/internal/settings/MutableSettings.scala @@ -44,4 +44,5 @@ abstract class MutableSettings extends AbsSettings { def maxClassfileName: IntSetting def Xexperimental: BooleanSetting def XoldPatmat: BooleanSetting + def XnoPatmatAnalysis: BooleanSetting } \ No newline at end of file diff --git a/src/compiler/scala/reflect/runtime/Settings.scala b/src/compiler/scala/reflect/runtime/Settings.scala index bbe4d60e9c..b247797c6c 100644 --- a/src/compiler/scala/reflect/runtime/Settings.scala +++ b/src/compiler/scala/reflect/runtime/Settings.scala @@ -35,4 +35,5 @@ class Settings extends internal.settings.MutableSettings { val Xexperimental = new BooleanSetting(false) val deepCloning = new BooleanSetting (false) val XoldPatmat = new BooleanSetting(false) + val XnoPatmatAnalysis = new BooleanSetting(false) } diff --git a/src/compiler/scala/tools/nsc/settings/ScalaSettings.scala b/src/compiler/scala/tools/nsc/settings/ScalaSettings.scala index efde2cee25..88a89d54eb 100644 --- a/src/compiler/scala/tools/nsc/settings/ScalaSettings.scala +++ b/src/compiler/scala/tools/nsc/settings/ScalaSettings.scala @@ -109,6 +109,7 @@ trait ScalaSettings extends AbsScalaSettings val sourceReader = StringSetting ("-Xsource-reader", "classname", "Specify a custom method for reading source files.", "") val XoldPatmat = BooleanSetting ("-Xoldpatmat", "Use the pre-2.10 pattern matcher. Otherwise, the 'virtualizing' pattern matcher is used in 2.10.") + val XnoPatmatAnalysis = BooleanSetting ("-Xno-patmat-analysis", "Don't perform exhaustivity/unreachability analysis. Also, ignore @switch annotation.") /** Compatibility stubs for options whose value name did * not previously match the option name. diff --git a/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala b/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala index 5f8ae240cc..3b2c4d06c4 100644 --- a/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala +++ b/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala @@ -1115,14 +1115,16 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL def isSwitchAnnotation(tpe: Type) = tpe hasAnnotation SwitchClass def isUncheckedAnnotation(tpe: Type) = tpe hasAnnotation UncheckedClass - val (unchecked, requireSwitch) = scrut match { - case Typed(_, tpt) => - (isUncheckedAnnotation(tpt.tpe), - // matches with two or fewer cases need not apply for switchiness (if-then-else will do) - isSwitchAnnotation(tpt.tpe) && casesNoSubstOnly.lengthCompare(2) > 0) - case _ => - (false, false) - } + val (unchecked, requireSwitch) = + if (settings.XnoPatmatAnalysis.value) (true, false) + else scrut match { + case Typed(_, tpt) => + (isUncheckedAnnotation(tpt.tpe), + // matches with two or fewer cases need not apply for switchiness (if-then-else will do) + isSwitchAnnotation(tpt.tpe) && casesNoSubstOnly.lengthCompare(2) > 0) + case _ => + (false, false) + } emitSwitch(scrut, scrutSym, casesNoSubstOnly, pt, matchFailGenOverride).getOrElse{ if (requireSwitch) typer.context.unit.warning(scrut.pos, "could not emit switch for @switch annotated match") -- cgit v1.2.3 From 3cb72faace500c14017cc163411dcac36a4ba9a4 Mon Sep 17 00:00:00 2001 From: Adriaan Moors Date: Sun, 3 Jun 2012 17:50:24 +0200 Subject: incorporate @retronym's review comments --- .../tools/nsc/typechecker/PatternMatching.scala | 108 ++++++++------------- 1 file changed, 39 insertions(+), 69 deletions(-) diff --git a/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala b/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala index 3b2c4d06c4..48985213d1 100644 --- a/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala +++ b/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala @@ -27,11 +27,9 @@ import scala.tools.nsc.util.Statistics * Cases are combined into a pattern match using the `orElse` combinator (the implicit failure case is expressed using the monad's `zero`). * * TODO: - * - exhaustivity - * - DCE (unreachability/refutability/optimization) * - use TypeTags for type testing - * - Array patterns - * - implement spec more closely (see TODO's) + * - DCE (on irrefutable patterns) + * - update spec and double check it's implemented correctly (see TODO's) * * (longer-term) TODO: * - user-defined unapplyProd @@ -1451,6 +1449,9 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL private var normalize: Substitution = EmptySubstitution // replaces a variable (in pointsToBound) by a selection on another variable in pointsToBound + // in the end, instead of having x1, x1.hd, x2, x2.hd, ... flying around, + // we want something like x1, x1.hd, x1.hd.tl, x1.hd.tl.hd, so that we can easily recognize when + // we're testing the same variable // TODO check: // pointsToBound -- accumSubst.from == Set(root) && (accumSubst.from.toSet -- pointsToBound) isEmpty private var accumSubst: Substitution = EmptySubstitution @@ -1466,7 +1467,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL val (unboundFrom, unboundTo) = unboundSubst.unzip // reverse substitution that would otherwise replace a variable we already encountered by a new variable - // NOTE: this forgets the more precise we have for these later variables, but that's probably okay + // NOTE: this forgets the more precise type we have for these later variables, but that's probably okay normalize >>= Substitution(boundTo map (_.symbol), boundFrom map (CODE.REF(_))) // patmatDebug("normalize: "+ normalize) @@ -1624,11 +1625,8 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL // in fact, all equalities relevant to this variable must have been registered def propForEqualsTo(c: Const): Prop -// // describe the equality axioms related to this variable being equal to this constant -// def impliedProp(c: Const): Prop - // populated by registerEquality - // once equalitySyms has been called, registerEquality has no effect + // once equalitySyms has been called, must not call registerEquality anymore def equalitySyms: List[Sym] } @@ -1682,10 +1680,23 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL } } - // convert finite domain propositional logic to boolean propositional logic - // for all c in C, there is a corresponding (meta-indexed) proposition Qv(c) that represents V = c, - // the only property of equality that is encoded is that a variable can at most be equal to one of the c in C: - // thus, for each distinct c, c', c'',... in C, a clause `not (Qv(c) /\ (Qv(c') \/ ... \/ Qv(c'')))` is added + // convert finite domain propositional logic with subtyping to pure boolean propositional logic + // a type test or a value equality test are modelled as a variable being equal to some constant + // a variable V may be assigned multiple constants, as long as they do not contradict each other + // according to subtyping, e.g., V = ConstantType(1) and V = Int are valid assignments + // we rewrite V = C to a fresh boolean symbol, and model what we know about the variable's domain + // in a prelude (the equality axioms) + // 1. a variable with a closed domain (of a sealed type) must be assigned one of the instantiatable types in its domain + // 2. for each variable V in props, and each constant C it is compared to, + // compute which assignments imply each other (as in the example above: V = 1 implies V = Int) + // and which assignments are mutually exclusive (V = String implies -(V = Int)) + // + // note that this is a conservative approximation: V = Constant(A) and V = Constant(B) + // are considered mutually exclusive (and thus both cases are considered reachable in {case A => case B =>}), + // even though A may be equal to B (and thus the second case is not "dynamically reachable") + // + // TODO: for V1 representing x1 and V2 standing for x1.head, encode that + // V1 = Nil implies -(V2 = Ci) for all Ci in V2's domain (i.e., it is unassignable) def removeVarEq(props: List[Prop], considerNull: Boolean = false): (Prop, List[Prop]) = { val start = startTimer(patmatAnaVarEq) @@ -1720,6 +1731,8 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL 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 } // patmatDebug("vars: "+ vars) @@ -1736,7 +1749,6 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL val syms = v.equalitySyms // patmatDebug("eqSyms "+(v, syms)) syms foreach { sym => - // don't relate V = C to V = C -- `b.const == sym.const` // if we've already excluded the pair at some point (-A \/ -B), then don't exclude the symmetric one (-B \/ -A) // (nor the positive implications -B \/ A, or -A \/ B, which would entail the equality axioms falsifying the whole formula) val todo = syms filterNot (b => (b.const == sym.const) || excludedPair(ExcludedPair(b.const, sym.const))) @@ -1767,7 +1779,9 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL type Formula def andFormula(a: Formula, b: Formula): Formula - // may throw an IllegalArgumentException + class CNFBudgetExceeded extends RuntimeException("CNF budget exceeded") + + // may throw an CNFBudgetExceeded def propToSolvable(p: Prop) = { val (eqAxioms, pure :: Nil) = removeVarEq(List(p), considerNull = false) eqFreePropToSolvable(And(eqAxioms, pure)) @@ -1798,7 +1812,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL type Lit def Lit(sym: Sym, pos: Boolean = true): Lit - // throws an IllegalArgumentException when the prop results in a CNF that's too big + // throws an CNFBudgetExceeded when the prop results in a CNF that's too big def eqFreePropToSolvable(p: Prop): Formula = { // TODO: for now, reusing the normalization from DPLL def negationNormalForm(p: Prop): Prop = p match { @@ -1822,7 +1836,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL def conjunctiveNormalForm(p: Prop, budget: Int = 256): Formula = { def distribute(a: Formula, b: Formula, budget: Int): Formula = - if (budget <= 0) throw new IllegalArgumentException("CNF budget exceeded") + if (budget <= 0) throw new CNFBudgetExceeded else (a, b) match { // true \/ _ = true @@ -1837,7 +1851,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL big flatMap (c => distribute(formula(c), small, budget - (big.size*small.size))) } - if (budget <= 0) throw new IllegalArgumentException("CNF budget exceeded") + if (budget <= 0) throw new CNFBudgetExceeded p match { case True => TrueF @@ -1883,7 +1897,6 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL def cnfString(f: Formula) = alignAcrossRows(f map (_.toList) toList, "\\/", " /\\\n") // adapted from http://lara.epfl.ch/w/sav10:simple_sat_solver (original by Hossein Hojjat) -// type Model = Map[Sym, Boolean] val EmptyModel = Map.empty[Sym, Boolean] val NoModel: Model = null @@ -2058,36 +2071,6 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL // don't call until all equalities have been registered and considerNull has been called (if needed) def describe = toString + ": " + fullTp + domain.map(_.mkString(" ::= ", " | ", "// "+ symForEqualsTo.keys)).getOrElse(symForEqualsTo.keys.mkString(" ::= ", " | ", " | ...")) + " // = " + path override def toString = "V"+ id - - - - // when V = C, which other V = Ci are implied? - // V = null is an exclusive assignment, since null precludes any type test being true - // V = Any does not imply anything (except non-nullness) - // consider: - // when V's domain is closed, say V : X ::= A | B | C, and we have some value constants, say U and V, of type X: - // (x: X) match { case U => case V => case _ : X => } - // - // V's equalityConsts (for the above match): TC(X), TC(A), TC(B), TC(C), VC(U), VC(V) - // Set(TC(X), VC(U), VC(V)).forall(c => Set(TC(A), TC(B), TC(C)).forall(_.covers(c))) - // Set(VC(U), VC(V), TC(A), TC(B), TC(C)).forall(_.implies(TC(X)) - // impliedSuper for TC(X) is empty (since it's at the top of the lattice), - // but since we have a closed domain, we know that also one of the partitions must hold - // thus, TC(X) implies TC(A) \/ TC(B) \/ TC(C), - // we only need to add this implication when impliedSuper is empty, - // since that'll eventually be the case (transitive closure & acyclic graphs ftw) -// def impliedProp(c: Const): Prop = if (c eq NullConst) True else { -// val impliedSuper = /\((equalityConsts filter { other => (c != other) && c.implies(other) && !other.implies(c) } map symForEqualsTo)) -// -// val implied = -// if (impliedSuper == True) domain match { case None => True -// case Some(domCs) => \/(domCs filter { _.covers(c) } map symForEqualsTo) -// } else impliedSuper -// -// // patmatDebug("impliedProp: "+(this, c, impliedSuper, implied)) -// implied -// } -// private lazy val equalityConsts = symForEqualsTo.keySet } @@ -2121,18 +2104,6 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL def isAny = wideTp.typeSymbol == AnyClass -// final def covers(other: Const): Boolean = { -// val r = (this, other) match { -// case (_: ValueConst, _: ValueConst) => this == other // hashconsed -// case (TypeConst(a) , _: ValueConst) => a <:< other.wideTp -// case (_ , _: TypeConst) => tp <:< other.tp -// case _ => false -// } -// // if(r) patmatDebug("covers : "+(this, other)) -// // else patmatDebug("NOT covers: "+(this, other)) -// r -// } - final def implies(other: Const): Boolean = { val r = (this, other) match { case (_: ValueConst, _: ValueConst) => this == other // hashconsed @@ -2164,8 +2135,8 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL r } - // the equality symbol for V = C is looked up by C - final override def equals(other: Any): Boolean = other match { case o: Const => this eq o case _ => false } + // 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 } @@ -2354,8 +2325,8 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL if (reachable) None else Some(caseIndex) } catch { - case e : IllegalArgumentException => -// patmatDebug(util.Position.formatMessage(prevBinder.pos, "Cannot check match for reachability", false)) + case e : CNFBudgetExceeded => +// debugWarn(util.Position.formatMessage(prevBinder.pos, "Cannot check match for reachability", false)) // e.printStackTrace() None // CNF budget exceeded } @@ -2516,7 +2487,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL stopTimer(patmatAnaExhaust, start) pruned } catch { - case e : IllegalArgumentException => + case e : CNFBudgetExceeded => // patmatDebug(util.Position.formatMessage(prevBinder.pos, "Cannot check match for exhaustivity", false)) // e.printStackTrace() Nil // CNF budget exceeded @@ -2539,6 +2510,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL case class ValueExample(c: ValueConst) extends CounterExample { override def toString = c.toString } case class TypeExample(c: Const) extends CounterExample { override def toString = "(_ : "+ c +")" } case class NegativeExample(nonTrivialNonEqualTo: List[Const]) extends CounterExample { + // require(nonTrivialNonEqualTo.nonEmpty, nonTrivialNonEqualTo) override def toString = { val negation = if (nonTrivialNonEqualTo.tail.isEmpty) nonTrivialNonEqualTo.head.toString @@ -2728,11 +2700,9 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL /** 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) - * when a sub-expression is share, it is stored in a mutable variable + * when a sub-expression is shared, it is stored in a mutable variable * the variable is floated up so that its scope includes all of the program that shares it * we generalize sharing to implication, where b reuses a if a => b and priors(a) => priors(b) (the priors of a sub expression form the path through the decision tree) - * - * intended to be generalised to exhaustivity/reachability checking */ def doCSE(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type): List[List[TreeMaker]] = { val testss = approximateMatch(prevBinder, cases) -- cgit v1.2.3