diff options
author | Adriaan Moors <adriaan.moors@epfl.ch> | 2012-07-20 11:45:59 +0200 |
---|---|---|
committer | Adriaan Moors <adriaan.moors@epfl.ch> | 2012-07-20 12:16:09 +0200 |
commit | 93519ab5049b085c3c13c9f438e516d5dedbfca1 (patch) | |
tree | 97393102f8463f2f794717a07a0214739bb1e4e9 /src | |
parent | 314133f98118d6d2f9f515fcc5aa7a2e7e9a4559 (diff) | |
download | scala-93519ab5049b085c3c13c9f438e516d5dedbfca1.tar.gz scala-93519ab5049b085c3c13c9f438e516d5dedbfca1.tar.bz2 scala-93519ab5049b085c3c13c9f438e516d5dedbfca1.zip |
SI-6031 customizable budget for patmat analyses
read the scalac.patmat.analysisBudget system property to decide how much time to spend on unreachability/exhaustivity
the default value is 256, and you can turn it off entirely using -Dscalac.patmat.analysisBudget=off
when the budget is exhausted, an unchecked warning is emitted
stack overflows in CNF conversion are caught and treated as analysis budget violations
Diffstat (limited to 'src')
-rw-r--r-- | src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala | 56 |
1 files changed, 41 insertions, 15 deletions
diff --git a/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala b/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala index b54f127417..943f75fec6 100644 --- a/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala +++ b/src/compiler/scala/tools/nsc/typechecker/PatternMatching.scala @@ -54,6 +54,25 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL } import debugging.patmatDebug + // to govern how much time we spend analyzing matches for unreachability/exhaustivity + object AnalysisBudget { + import scala.tools.cmd.FromString.IntFromString + val max = sys.props.get("scalac.patmat.analysisBudget").collect(IntFromString.orElse{case "off" => Integer.MAX_VALUE}).getOrElse(256) + + abstract class Exception extends RuntimeException("CNF budget exceeded") { + val advice: String + def warn(pos: Position, kind: String) = currentUnit.uncheckedWarning(pos, s"Cannot check match for $kind.\n$advice") + } + + object exceeded extends Exception { + val advice = s"(The analysis required more space than allowed. Please try with scalac -Dscalac.patmat.analysisBudget=${AnalysisBudget.max*2} or -Dscalac.patmat.analysisBudget=off.)" + } + + object stackOverflow extends Exception { + val advice = "(There was a stack overflow. Please try increasing the stack available to the compiler using e.g., -Xss2m.)" + } + } + def newTransformer(unit: CompilationUnit): Transformer = if (opt.virtPatmat) new MatchTransformer(unit) else noopTransformer @@ -1946,14 +1965,14 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL type Formula def andFormula(a: Formula, b: Formula): Formula - class CNFBudgetExceeded extends RuntimeException("CNF budget exceeded") - // may throw an CNFBudgetExceeded - def propToSolvable(p: Prop) = { + // may throw an AnalysisBudget.Exception + def propToSolvable(p: Prop): Formula = { val (eqAxioms, pure :: Nil) = removeVarEq(List(p), modelNull = false) eqFreePropToSolvable(And(eqAxioms, pure)) } + // may throw an AnalysisBudget.Exception def eqFreePropToSolvable(p: Prop): Formula def cnfString(f: Formula): String @@ -1979,7 +1998,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL type Lit def Lit(sym: Sym, pos: Boolean = true): Lit - // throws an CNFBudgetExceeded when the prop results in a CNF that's too big + // throws an AnalysisBudget.Exception 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 { @@ -2001,9 +2020,9 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL 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 conjunctiveNormalForm(p: Prop, budget: Int = AnalysisBudget.max): Formula = { def distribute(a: Formula, b: Formula, budget: Int): Formula = - if (budget <= 0) throw new CNFBudgetExceeded + if (budget <= 0) throw AnalysisBudget.exceeded else (a, b) match { // true \/ _ = true @@ -2018,7 +2037,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 CNFBudgetExceeded + if (budget <= 0) throw AnalysisBudget.exceeded p match { case True => TrueF @@ -2037,9 +2056,17 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL } val start = Statistics.startTimer(patmatCNF) - val res = conjunctiveNormalForm(negationNormalForm(p)) + val res = + try { + conjunctiveNormalForm(negationNormalForm(p)) + } catch { case ex : StackOverflowError => + throw AnalysisBudget.stackOverflow + } + Statistics.stopTimer(patmatCNF, start) - patmatCNFSizes(res.size).value += 1 + + // + if (Statistics.enabled) patmatCNFSizes(res.size).value += 1 // patmatDebug("cnf for\n"+ p +"\nis:\n"+cnfString(res)) res @@ -2440,6 +2467,7 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL // 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) @@ -2508,9 +2536,8 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL if (reachable) None else Some(caseIndex) } catch { - case e : CNFBudgetExceeded => -// debugWarn(util.Position.formatMessage(prevBinder.pos, "Cannot check match for reachability", false)) -// e.printStackTrace() + case ex: AnalysisBudget.Exception => + ex.warn(prevBinder.pos, "unreachability") None // CNF budget exceeded } } @@ -2651,9 +2678,8 @@ trait PatternMatching extends Transform with TypingTransformers with ast.TreeDSL Statistics.stopTimer(patmatAnaExhaust, start) pruned } catch { - case e : CNFBudgetExceeded => - patmatDebug(util.Position.formatMessage(prevBinder.pos, "Cannot check match for exhaustivity", false)) - // e.printStackTrace() + case ex : AnalysisBudget.Exception => + ex.warn(prevBinder.pos, "exhaustivity") Nil // CNF budget exceeded } } |