SI-7020 Deterministic warnings for pattern matcher, take 2

The previous swing at determinism, ebb01e0, made decent
contact but apparently didn't hit it out of the park. The test
wavered every hundred or so runs, as witnessed occasionally in
nightly builds or pull request validation.

I setup a test to run neg/7020.scala a few hundred times, and
could trigger the failure reliably.

I then swept through the pattern matcher in search of HashMap and
HashSet creation, and changed them all to the Linked variety.
The results of that are published in retronym#ticket/7020-3 [1].

This commit represents the careful whittling down of that patch
to the minimal change required to exhibit determinism.

[1] https://github.com/retronym/scala/compare/ticket/7020-3

src/compiler/scala/tools/nsc/transform/patmat/Logic.scala

@@ -113,7 +113,7 @@ trait Logic extends Debugging  {
 
     // symbols are propositions
     abstract case class Sym(variable: Var, const: Const) extends Prop {
-      private[this] val id = Sym.nextSymId
+      private val id: Int = Sym.nextSymId
 
       override def toString = variable +"="+ const +"#"+ id
     }
@@ -125,6 +125,7 @@ trait Logic extends Debugging  {
         (uniques findEntryOrUpdate newSym)
       }
       private def nextSymId = {_symId += 1; _symId}; private var _symId = 0
+      implicit val SymOrdering: Ordering[Sym] = Ordering.by(_.id)
     }
 
     def /\(props: Iterable[Prop]) = if (props.isEmpty) True else props.reduceLeft(And(_, _))
@@ -279,7 +280,7 @@ trait Logic extends Debugging  {
     def eqFreePropToSolvable(p: Prop): Formula
     def cnfString(f: Formula): String
 
-    type Model = Map[Sym, Boolean]
+    type Model = collection.immutable.SortedMap[Sym, Boolean]
     val EmptyModel: Model
     val NoModel: Model
 

src/compiler/scala/tools/nsc/transform/patmat/Solving.scala

@@ -26,9 +26,12 @@ trait Solving extends Logic {
     type Formula = FormulaBuilder
     def formula(c: Clause*): Formula = ArrayBuffer(c: _*)
 
-    type Clause  = Set[Lit]
+    type Clause  = collection.Set[Lit]
     // a clause is a disjunction of distinct literals
-    def clause(l: Lit*): Clause = l.toSet
+    def clause(l: Lit*): Clause = (
+      // neg/t7020.scala changes output 1% of the time, the non-determinism is quelled with this linked set
+      mutable.LinkedHashSet(l: _*)
+    )
 
     type Lit
     def Lit(sym: Sym, pos: Boolean = true): Lit
@@ -134,7 +137,7 @@ trait Solving extends Logic {
     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)
-    val EmptyModel = Map.empty[Sym, Boolean]
+    val EmptyModel = collection.immutable.SortedMap.empty[Sym, Boolean]
     val NoModel: Model = null
 
     // returns all solutions, if any (TODO: better infinite recursion backstop -- detect fixpoint??)
@@ -229,9 +232,8 @@ trait Solving extends Logic {
             }
         }
 
-        if (Statistics.canEnable) Statistics.stopTimer(patmatAnaDPLL, start)
-
-        satisfiableWithModel
+      if (Statistics.canEnable) Statistics.stopTimer(patmatAnaDPLL, start)
+      satisfiableWithModel
     }
   }
 }

test/disabled/neg/t7020.check → test/files/neg/t7020.check

@@ -1,17 +1,17 @@
 t7020.scala:3: warning: match may not be exhaustive.
-It would fail on the following inputs: List((x: Int forSome x not in (1, 2, 4, 5, 6, 7))), List((x: Int forSome x not in (1, 2, 4, 5, 6, 7)), _), List(1, _), List(2, _), List(4, _), List(5, _), List(6, _), List(7, _), List(??, _), List(_, _)
+It would fail on the following inputs: List((x: Int forSome x not in (1, 2, 4, 5, 6, 7))), List((x: Int forSome x not in (1, 2, 4, 5, 6, 7)), _), List(1, _), List(2, _), List(4, _), List(5, _), List(6, _), List(7, _), List(_, _)
   List(5) match {
       ^
 t7020.scala:10: warning: match may not be exhaustive.
-It would fail on the following inputs: List((x: Int forSome x not in (1, 2, 4, 5, 6, 7))), List((x: Int forSome x not in (1, 2, 4, 5, 6, 7)), _), List(1, _), List(2, _), List(4, _), List(5, _), List(6, _), List(7, _), List(??, _), List(_, _)
+It would fail on the following inputs: List((x: Int forSome x not in (1, 2, 4, 5, 6, 7))), List((x: Int forSome x not in (1, 2, 4, 5, 6, 7)), _), List(1, _), List(2, _), List(4, _), List(5, _), List(6, _), List(7, _), List(_, _)
   List(5) match {
       ^
 t7020.scala:17: warning: match may not be exhaustive.
-It would fail on the following inputs: List((x: Int forSome x not in (1, 2, 4, 5, 6, 7))), List((x: Int forSome x not in (1, 2, 4, 5, 6, 7)), _), List(1, _), List(2, _), List(4, _), List(5, _), List(6, _), List(7, _), List(??, _), List(_, _)
+It would fail on the following inputs: List((x: Int forSome x not in (1, 2, 4, 5, 6, 7))), List((x: Int forSome x not in (1, 2, 4, 5, 6, 7)), _), List(1, _), List(2, _), List(4, _), List(5, _), List(6, _), List(7, _), List(_, _)
   List(5) match {
       ^
 t7020.scala:24: warning: match may not be exhaustive.
-It would fail on the following inputs: List((x: Int forSome x not in (1, 2, 4, 5, 6, 7))), List((x: Int forSome x not in (1, 2, 4, 5, 6, 7)), _), List(1, _), List(2, _), List(4, _), List(5, _), List(6, _), List(7, _), List(??, _), List(_, _)
+It would fail on the following inputs: List((x: Int forSome x not in (1, 2, 4, 5, 6, 7))), List((x: Int forSome x not in (1, 2, 4, 5, 6, 7)), _), List(1, _), List(2, _), List(4, _), List(5, _), List(6, _), List(7, _), List(_, _)
   List(5) match {
       ^
 error: No warnings can be incurred under -Xfatal-warnings.