Merge pull request #4370 from gbasler/ticket/SI-9181

SI-9181 Exhaustivity checking does not scale (regression)

3 files changed, 141 insertions, 66 deletions

diff --git a/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala b/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala
index 0b53dc37de..4ea569c8e6 100644
--- a/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala
+++ b/src/compiler/scala/tools/nsc/transform/patmat/Logic.scala
@@ -9,8 +9,7 @@ package tools.nsc.transform.patmat
 
 import scala.language.postfixOps
 import scala.collection.mutable
-import scala.reflect.internal.util.Statistics
-import scala.reflect.internal.util.HashSet
+import scala.reflect.internal.util.{NoPosition, Position, Statistics, HashSet}
 
 trait Logic extends Debugging  {
   import PatternMatchingStats._
@@ -71,6 +70,8 @@ trait Logic extends Debugging  {
       def unapply(v: Var): Some[Tree]
     }
 
+    def uncheckedWarning(pos: Position, msg: String): Unit
+
     def reportWarning(message: String): Unit
 
     // resets hash consing -- only supposed to be called by TreeMakersToProps
@@ -283,6 +284,23 @@ trait Logic extends Debugging  {
       }
     }
 
+    // to govern how much time we spend analyzing matches for unreachability/exhaustivity
+    object AnalysisBudget {
+      val maxDPLLdepth = global.settings.YpatmatExhaustdepth.value
+      val maxFormulaSize = 100 * math.min(Int.MaxValue / 100, maxDPLLdepth)
+
+      private def advice =
+        s"Please try with scalac -Ypatmat-exhaust-depth ${maxDPLLdepth * 2} or -Ypatmat-exhaust-depth off."
+
+      def recursionDepthReached =
+        s"Exhaustivity analysis reached max recursion depth, not all missing cases are reported.\n($advice)"
+
+      abstract class Exception(val advice: String) extends RuntimeException("CNF budget exceeded")
+
+      object formulaSizeExceeded extends Exception(s"The analysis required more space than allowed.\n$advice")
+
+    }
+
     // TODO: remove since deprecated
     val budgetProp = scala.sys.Prop[String]("scalac.patmat.analysisBudget")
     if (budgetProp.isSet) {
@@ -385,7 +403,7 @@ trait Logic extends Debugging  {
 
     def findModelFor(solvable: Solvable): Model
 
-    def findAllModelsFor(solvable: Solvable): List[Solution]
+    def findAllModelsFor(solvable: Solvable, pos: Position = NoPosition): List[Solution]
   }
 }
 
diff --git a/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala b/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala
index 34ebbc7463..cecb5c37be 100644
--- a/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala
+++ b/src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala
@@ -399,6 +399,7 @@ trait MatchAnalysis extends MatchApproximation {
 
   trait MatchAnalyzer extends MatchApproximator  {
     def uncheckedWarning(pos: Position, msg: String) = currentRun.reporting.uncheckedWarning(pos, msg)
+    def warn(pos: Position, ex: AnalysisBudget.Exception, kind: String) = uncheckedWarning(pos, s"Cannot check match for $kind.\n${ex.advice}")
     def reportWarning(message: String) = global.reporter.warning(typer.context.tree.pos, message)
 
   // 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
@@ -429,44 +430,50 @@ trait MatchAnalysis extends MatchApproximation {
       val propsCasesOk   = approximate(True)  map caseWithoutBodyToProp
       val propsCasesFail = approximate(False) map (t => Not(caseWithoutBodyToProp(t)))
 
-      val (eqAxiomsFail, symbolicCasesFail) = removeVarEq(propsCasesFail, modelNull = true)
-      val (eqAxiomsOk, symbolicCasesOk)     = removeVarEq(propsCasesOk, modelNull = true)
-      val eqAxioms = simplify(And(eqAxiomsOk, eqAxiomsFail)) // I'm pretty sure eqAxiomsOk == eqAxiomsFail, but not 100% sure.
-
-      val prefix = mutable.ArrayBuffer[Prop]()
-      prefix += eqAxioms
-
-      var prefixRest = symbolicCasesFail
-      var current = symbolicCasesOk
-      var reachable = true
-      var caseIndex = 0
-
-      debug.patmat("reachability, vars:\n" + ((propsCasesFail flatMap gatherVariables).distinct map (_.describe) mkString ("\n")))
-      debug.patmat(s"equality axioms:\n$eqAxiomsOk")
-
-      // 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 += prefHead
-          current = current.tail
+      try {
+        val (eqAxiomsFail, symbolicCasesFail) = removeVarEq(propsCasesFail, modelNull = true)
+        val (eqAxiomsOk, symbolicCasesOk) = removeVarEq(propsCasesOk, modelNull = true)
+        val eqAxioms = simplify(And(eqAxiomsOk, eqAxiomsFail)) // I'm pretty sure eqAxiomsOk == eqAxiomsFail, but not 100% sure.
+
+        val prefix = mutable.ArrayBuffer[Prop]()
+        prefix += eqAxioms
+
+        var prefixRest = symbolicCasesFail
+        var current = symbolicCasesOk
+        var reachable = true
+        var caseIndex = 0
+
+        debug.patmat("reachability, vars:\n" + ((propsCasesFail flatMap gatherVariables).distinct map (_.describe) mkString ("\n")))
+        debug.patmat(s"equality axioms:\n$eqAxiomsOk")
+
+        // 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 += prefHead
+            current = current.tail
           val and = And((current.head +: prefix): _*)
           val model = findModelFor(eqFreePropToSolvable(and))
 
-          // debug.patmat("trying to reach:\n"+ cnfString(current.head) +"\nunder prefix:\n"+ cnfString(prefix))
-          // if (NoModel ne model) debug.patmat("reached: "+ modelString(model))
+            // debug.patmat("trying to reach:\n"+ cnfString(current.head) +"\nunder prefix:\n"+ cnfString(prefix))
+            // if (NoModel ne model) debug.patmat("reached: "+ modelString(model))
 
-          reachable = NoModel ne model
+            reachable = NoModel ne model
+          }
         }
-      }
 
-      if (Statistics.canEnable) Statistics.stopTimer(patmatAnaReach, start)
+        if (Statistics.canEnable) Statistics.stopTimer(patmatAnaReach, start)
 
-      if (reachable) None else Some(caseIndex)
+        if (reachable) None else Some(caseIndex)
+      } catch {
+        case ex: AnalysisBudget.Exception =>
+          warn(prevBinder.pos, ex, "unreachability")
+          None // CNF budget exceeded
+      }
     }
 
     // exhaustivity
@@ -507,32 +514,38 @@ trait MatchAnalysis extends MatchApproximation {
         // when does the match fail?
         val matchFails = Not(\/(symbolicCases))
 
-  // debug output:
+        // debug output:
         debug.patmat("analysing:")
         showTreeMakers(cases)
 
         // debug.patmat("\nvars:\n"+ (vars map (_.describe) mkString ("\n")))
         // debug.patmat("\nmatchFails as CNF:\n"+ cnfString(propToSolvable(matchFails)))
 
-        // find the models (under which the match fails)
-        val matchFailModels = findAllModelsFor(propToSolvable(matchFails))
+        try {
+          // find the models (under which the match fails)
+          val matchFailModels = findAllModelsFor(propToSolvable(matchFails), prevBinder.pos)
 
-        val scrutVar = Var(prevBinderTree)
-        val counterExamples = {
-          matchFailModels.flatMap {
-            model =>
-              val varAssignments = expandModel(model)
-              varAssignments.flatMap(modelToCounterExample(scrutVar) _)
+          val scrutVar = Var(prevBinderTree)
+          val counterExamples = {
+            matchFailModels.flatMap {
+              model =>
+                val varAssignments = expandModel(model)
+                varAssignments.flatMap(modelToCounterExample(scrutVar) _)
+            }
           }
-        }
-
-        // sorting before pruning is important here in order to
-        // keep neg/t7020.scala stable
-        // since e.g. List(_, _) would cover List(1, _)
-        val pruned = CounterExample.prune(counterExamples.sortBy(_.toString)).map(_.toString)
 
-        if (Statistics.canEnable) Statistics.stopTimer(patmatAnaExhaust, start)
-        pruned
+          // sorting before pruning is important here in order to
+          // keep neg/t7020.scala stable
+          // since e.g. List(_, _) would cover List(1, _)
+          val pruned = CounterExample.prune(counterExamples.sortBy(_.toString)).map(_.toString)
+
+          if (Statistics.canEnable) Statistics.stopTimer(patmatAnaExhaust, start)
+          pruned
+        } catch {
+          case ex: AnalysisBudget.Exception =>
+            warn(prevBinder.pos, ex, "exhaustivity")
+            Nil // CNF budget exceeded
+        }
       }
     }
 
diff --git a/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala b/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala
index 27217f0dc2..c43f1b6209 100644
--- a/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala
+++ b/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala
@@ -11,6 +11,7 @@ import scala.reflect.internal.util.Statistics
 import scala.language.postfixOps
 import scala.collection.mutable
 import scala.reflect.internal.util.Collections._
+import scala.reflect.internal.util.Position
 
 // a literal is a (possibly negated) variable
 class Lit(val v: Int) extends AnyVal {
@@ -64,7 +65,12 @@ trait Solving extends Logic {
       def size = symbols.size
     }
 
-    case class Solvable(cnf: Cnf, symbolMapping: SymbolMapping)
+    final case class Solvable(cnf: Cnf, symbolMapping: SymbolMapping) {
+      def ++(other: Solvable) = {
+        require(this.symbolMapping eq other.symbolMapping)
+        Solvable(cnf ++ other.cnf, symbolMapping)
+      }
+    }
 
     trait CnfBuilder {
       private[this] val buff = ArrayBuffer[Clause]()
@@ -95,7 +101,11 @@ trait Solving extends Logic {
         }
       }
 
-      def buildCnf: Array[Clause] = buff.toArray
+      def buildCnf: Array[Clause] = {
+        val cnf = buff.toArray
+        buff.clear()
+        cnf
+      }
 
     }
 
@@ -244,19 +254,54 @@ trait Solving extends Logic {
 
     def eqFreePropToSolvable(p: Prop): Solvable = {
 
+      def doesFormulaExceedSize(p: Prop): Boolean = {
+        p match {
+          case And(ops) =>
+            if (ops.size > AnalysisBudget.maxFormulaSize) {
+              true
+            } else {
+              ops.exists(doesFormulaExceedSize)
+            }
+          case Or(ops)  =>
+            if (ops.size > AnalysisBudget.maxFormulaSize) {
+              true
+            } else {
+              ops.exists(doesFormulaExceedSize)
+            }
+          case Not(a)   => doesFormulaExceedSize(a)
+          case _        => false
+        }
+      }
+
+      val simplified = simplify(p)
+      if (doesFormulaExceedSize(simplified)) {
+        throw AnalysisBudget.formulaSizeExceeded
+      }
+
       // collect all variables since after simplification / CNF conversion
       // they could have been removed from the formula
       val symbolMapping = new SymbolMapping(gatherSymbols(p))
-
-      val simplified = simplify(p)
       val cnfExtractor = new AlreadyInCNF(symbolMapping)
+      val cnfTransformer = new TransformToCnf(symbolMapping)
+
+      def cnfFor(prop: Prop): Solvable = {
+        prop match {
+          case cnfExtractor.ToCnf(solvable) =>
+            // this is needed because t6942 would generate too many clauses with Tseitin
+            // already in CNF, just add clauses
+            solvable
+          case p                            =>
+            cnfTransformer.apply(p)
+        }
+      }
+
       simplified match {
-        case cnfExtractor.ToCnf(solvable) =>
-          // this is needed because t6942 would generate too many clauses with Tseitin
-          // already in CNF, just add clauses
-          solvable
-        case p                           =>
-          new TransformToCnf(symbolMapping).apply(p)
+        case And(props) =>
+          // SI-6942:
+          // CNF(P1 /\ ... /\ PN) == CNF(P1) ++ CNF(...) ++ CNF(PN)
+          props.map(cnfFor).reduce(_ ++ _)
+        case p          =>
+          cnfFor(p)
       }
     }
   }
@@ -288,7 +333,7 @@ trait Solving extends Logic {
     val NoTseitinModel: TseitinModel = null
 
     // returns all solutions, if any (TODO: better infinite recursion backstop -- detect fixpoint??)
-    def findAllModelsFor(solvable: Solvable): List[Solution] = {
+    def findAllModelsFor(solvable: Solvable, pos: Position): List[Solution] = {
       debug.patmat("find all models for\n"+ cnfString(solvable.cnf))
 
       // we must take all vars from non simplified formula
@@ -308,13 +353,12 @@ trait Solving extends Logic {
       final case class TseitinSolution(model: TseitinModel, unassigned: List[Int]) {
         def projectToSolution(symForVar: Map[Int, Sym]) = Solution(projectToModel(model, symForVar), unassigned map symForVar)
       }
+
       def findAllModels(clauses: Array[Clause],
                         models: List[TseitinSolution],
-                        recursionDepthAllowed: Int = global.settings.YpatmatExhaustdepth.value): List[TseitinSolution]=
+                        recursionDepthAllowed: Int = AnalysisBudget.maxDPLLdepth): List[TseitinSolution]=
         if (recursionDepthAllowed == 0) {
-          val maxDPLLdepth = global.settings.YpatmatExhaustdepth.value
-          reportWarning("(Exhaustivity analysis reached max recursion depth, not all missing cases are reported. " +
-              s"Please try with scalac -Ypatmat-exhaust-depth ${maxDPLLdepth * 2} or -Ypatmat-exhaust-depth off.)")
+          uncheckedWarning(pos, AnalysisBudget.recursionDepthReached)
           models
         } else {
           debug.patmat("find all models for\n" + cnfString(clauses))