Skip to content

Commit 179419c

Browse files
gbaslergbasler
committed
SI-7746 patmat: fix non-determinism, infeasible counter examples
Fixes non-determinism within the DPLL algorithm and disallows infeasible counter examples directly in the formula. The function to compute all solutions was flawed and thus only returned a subset of the solutions. The algorithm would stop too soon and thus depending on the ordering of the symbols return more or less solutions. I also added printing a warning when the search was stopped because the max recursion depth was reached. This is very useful as an explanation of spuriously failing regression tests, since less counter examples might be reported. In such a case the recursion depth should be set to infinite by adding `-Ypatmat-exhaust-depth off`. The mapping of the solutions of the DPLL algorithm to counter examples has been adapted to take the additional solutions from the solver into account: Consider for example `t8430.scala`: ```Scala sealed trait CL3Literal case object IntLit extends CL3Literal case object CharLit extends CL3Literal case object BooleanLit extends CL3Literal case object UnitLit extends CL3Literal sealed trait Tree case class LetL(value: CL3Literal) extends Tree case object LetP extends Tree case object LetC extends Tree case object LetF extends Tree object Test { (tree: Tree) => tree match {case LetL(CharLit) => ??? } } ``` This test contains 2 domains, `IntLit, CharLit, ...` and `LetL, LetP, ...`, the corresponding formula to check exhaustivity looks like: ``` V1=LetC.type#13 \/ V1=LetF.type#14 \/ V1=LetL#11 \/ V1=LetP.type#15 /\ V2=BooleanLit.type#16 \/ V2=CharLit#12 \/ V2=IntLit.type#17 \/ V2=UnitLit.type#18 /\ -V1=LetL#11 \/ -V2=CharLit#12 \/ \/ ``` The first two lines assign a value of the domain to the scrutinee (and the correponding member in case of `LetL`) and prohibit the counter example `LetL(CharLit)` since it's covered by the pattern match. The used Boolean encoding allows that scrutinee `V1` can be equal to `LetC` and `LetF` at the same time and thus, during enumeration of all possible solutions of the formula, such a solution will be found, since only one literal needs to be set to true, to satisfy that clause. That means, if at least one of the literals of such a clause was in the `unassigned` list of the DPLL procedure, we will get solutions where the scrutinee is equal to more than one element of the domain. A remedy would be to add constraints that forbid both literals to be true at the same time. His is infeasible for big domains (see `pos/t8531.scala`), since we would have to add a quadratic number of clauses (one clause for each pair in the domain). A much simpler solution is to just filter the invalid results. Since both values for `unassigned` literals are explored, we will eventually find a valid counter example.
1 parent 223e207 commit 179419c

File tree

11 files changed

+115
-41
lines changed

11 files changed

+115
-41
lines changed

‎src/compiler/scala/tools/nsc/settings/ScalaSettings.scala

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -262,6 +262,8 @@ trait ScalaSettings extends AbsScalaSettings
262262
val Yreifydebug = BooleanSetting("-Yreify-debug", "Trace reification.")
263263
val Ytyperdebug = BooleanSetting("-Ytyper-debug", "Trace all type assignments.")
264264
val Ypatmatdebug = BooleanSetting("-Ypatmat-debug", "Trace pattern matching translation.")
265+
val YpatmatExhaustdepth = IntSetting("-Ypatmat-exhaust-depth", "off", 20, Some((10, Int.MaxValue)),
266+
str => Some(if(str.equalsIgnoreCase("off")) Int.MaxValue else str.toInt))
265267
val Yquasiquotedebug = BooleanSetting("-Yquasiquote-debug", "Trace quasiquote-related activities.")
266268

267269
// TODO 2.12 Remove

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

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,6 @@ package tools.nsc.transform.patmat
1010
import scala.language.postfixOps
1111
import scala.collection.mutable
1212
import scala.reflect.internal.util.Statistics
13-
import scala.reflect.internal.util.Position
1413
import scala.reflect.internal.util.HashSet
1514

1615
trait Logic extends Debugging {
@@ -72,6 +71,8 @@ trait Logic extends Debugging {
7271
def unapply(v: Var): Some[Tree]
7372
}
7473

74+
def reportWarning(message: String): Unit
75+
7576
// resets hash consing -- only supposed to be called by TreeMakersToProps
7677
def prepareNewAnalysis(): Unit
7778

‎src/compiler/scala/tools/nsc/transform/patmat/MatchAnalysis.scala

Lines changed: 39 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,6 @@ package scala.tools.nsc.transform.patmat
99
import scala.language.postfixOps
1010
import scala.collection.mutable
1111
import scala.reflect.internal.util.Statistics
12-
import scala.reflect.internal.util.Position
1312

1413
trait TreeAndTypeAnalysis extends Debugging {
1514
import global._
@@ -400,6 +399,7 @@ trait MatchAnalysis extends MatchApproximation {
400399
trait MatchAnalyzer extends MatchApproximator {
401400
def uncheckedWarning(pos: Position, msg: String) = currentRun.reporting.uncheckedWarning(pos, msg)
402401
def warn(pos: Position, ex: AnalysisBudget.Exception, kind: String) = uncheckedWarning(pos, s"Cannot check match for $kind.\n${ex.advice}")
402+
def reportWarning(message: String) = global.reporter.warning(typer.context.tree.pos, message)
403403

404404
// 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
405405
// right now hackily implement this by pruning counter-examples
@@ -524,9 +524,11 @@ trait MatchAnalysis extends MatchApproximation {
524524
val matchFailModels = findAllModelsFor(propToSolvable(matchFails))
525525

526526
val scrutVar = Var(prevBinderTree)
527-
val counterExamples = matchFailModels.map(modelToCounterExample(scrutVar))
528-
529-
val pruned = CounterExample.prune(counterExamples).map(_.toString).sorted
527+
val counterExamples = matchFailModels.flatMap(modelToCounterExample(scrutVar))
528+
// sorting before pruning is important here in order to
529+
// keep neg/t7020.scala stable
530+
// since e.g. List(_, _) would cover List(1, _)
531+
val pruned = CounterExample.prune(counterExamples.sortBy(_.toString)).map(_.toString)
530532

531533
if (Statistics.canEnable) Statistics.stopTimer(patmatAnaExhaust, start)
532534
pruned
@@ -616,7 +618,7 @@ trait MatchAnalysis extends MatchApproximation {
616618
// (the variables don't take into account type information derived from other variables,
617619
// so, naively, you might try to construct a counter example like _ :: Nil(_ :: _, _ :: _),
618620
// since we didn't realize the tail of the outer cons was a Nil)
619-
def modelToCounterExample(scrutVar: Var)(model: Model): CounterExample = {
621+
def modelToCounterExample(scrutVar: Var)(model: Model): Option[CounterExample] = {
620622
// x1 = ...
621623
// x1.hd = ...
622624
// x1.tl = ...
@@ -674,6 +676,7 @@ trait MatchAnalysis extends MatchApproximation {
674676
private val fields: mutable.Map[Symbol, VariableAssignment] = mutable.HashMap.empty
675677
// need to prune since the model now incorporates all super types of a constant (needed for reachability)
676678
private lazy val uniqueEqualTo = equalTo filterNot (subsumed => equalTo.exists(better => (better ne subsumed) && instanceOfTpImplies(better.tp, subsumed.tp)))
679+
private lazy val inSameDomain = uniqueEqualTo forall (const => variable.domainSyms.exists(_.exists(_.const.tp =:= const.tp)))
677680
private lazy val prunedEqualTo = uniqueEqualTo filterNot (subsumed => variable.staticTpCheckable <:< subsumed.tp)
678681
private lazy val ctor = (prunedEqualTo match { case List(TypeConst(tp)) => tp case _ => variable.staticTpCheckable }).typeSymbol.primaryConstructor
679682
private lazy val ctorParams = if (ctor.paramss.isEmpty) Nil else ctor.paramss.head
@@ -694,13 +697,13 @@ trait MatchAnalysis extends MatchApproximation {
694697
// NoExample if the constructor call is ill-typed
695698
// (thus statically impossible -- can we incorporate this into the formula?)
696699
// beBrief is used to suppress negative information nested in tuples -- it tends to get too noisy
697-
def toCounterExample(beBrief: Boolean = false): CounterExample =
698-
if (!allFieldAssignmentsLegal) NoExample
700+
def toCounterExample(beBrief: Boolean = false): Option[CounterExample] =
701+
if (!allFieldAssignmentsLegal) Some(NoExample)
699702
else {
700703
debug.patmat("describing "+ ((variable, equalTo, notEqualTo, fields, cls, allFieldAssignmentsLegal)))
701704
val res = prunedEqualTo match {
702705
// a definite assignment to a value
703-
case List(eq: ValueConst) if fields.isEmpty => ValueExample(eq)
706+
case List(eq: ValueConst) if fields.isEmpty => Some(ValueExample(eq))
704707

705708
// constructor call
706709
// or we did not gather any information about equality but we have information about the fields
@@ -713,30 +716,50 @@ trait MatchAnalysis extends MatchApproximation {
713716
// figure out the constructor arguments from the field assignment
714717
val argLen = (caseFieldAccs.length min ctorParams.length)
715718

716-
(0 until argLen).map(i => fields.get(caseFieldAccs(i)).map(_.toCounterExample(brevity)) getOrElse WildcardExample).toList
719+
val examples = (0 until argLen).map(i => fields.get(caseFieldAccs(i)).map(_.toCounterExample(brevity)) getOrElse Some(WildcardExample)).toList
720+
sequence(examples)
717721
}
718722

719723
cls match {
720-
case ConsClass => ListExample(args())
721-
case _ if isTupleSymbol(cls) => TupleExample(args(brevity = true))
722-
case _ => ConstructorExample(cls, args())
724+
case ConsClass =>
725+
args().map {
726+
case List(NoExample, l: ListExample) =>
727+
// special case for neg/t7020.scala:
728+
// if we find a counter example `??::*` we report `*::*` instead
729+
// since the `??` originates from uniqueEqualTo containing several instanced of the same type
730+
List(WildcardExample, l)
731+
case args => args
732+
}.map(ListExample)
733+
case _ if isTupleSymbol(cls) => args(brevity = true).map(TupleExample)
734+
case _ if cls.isSealed && cls.isAbstractClass =>
735+
// don't report sealed abstract classes, since
736+
// 1) they can't be instantiated
737+
// 2) we are already reporting any missing subclass (since we know the full domain)
738+
// (see patmatexhaust.scala)
739+
None
740+
case _ => args().map(ConstructorExample(cls, _))
723741
}
724742

725743
// a definite assignment to a type
726-
case List(eq) if fields.isEmpty => TypeExample(eq)
744+
case List(eq) if fields.isEmpty => Some(TypeExample(eq))
727745

728746
// negative information
729747
case Nil if nonTrivialNonEqualTo.nonEmpty =>
730748
// negation tends to get pretty verbose
731-
if (beBrief) WildcardExample
749+
if (beBrief) Some(WildcardExample)
732750
else {
733751
val eqTo = equalTo.headOption getOrElse TypeConst(variable.staticTpCheckable)
734-
NegativeExample(eqTo, nonTrivialNonEqualTo)
752+
Some(NegativeExample(eqTo, nonTrivialNonEqualTo))
735753
}
736754

755+
// if uniqueEqualTo contains more than one symbol of the same domain
756+
// then we can safely ignore these counter examples since we will eventually encounter
757+
// both counter examples separately
758+
case _ if inSameDomain => None
759+
737760
// not a valid counter-example, possibly since we have a definite type but there was a field mismatch
738761
// TODO: improve reasoning -- in the mean time, a false negative is better than an annoying false positive
739-
case _ => NoExample
762+
case _ => Some(NoExample)
740763
}
741764
debug.patmatResult("described as")(res)
742765
}

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

Lines changed: 60 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -115,7 +115,6 @@ trait Solving extends Logic {
115115

116116
if (Statistics.canEnable) Statistics.stopTimer(patmatCNF, start)
117117

118-
//
119118
if (Statistics.canEnable) patmatCNFSizes(res.size).value += 1
120119

121120
// debug.patmat("cnf for\n"+ p +"\nis:\n"+cnfString(res))
@@ -146,31 +145,78 @@ trait Solving extends Logic {
146145

147146
// returns all solutions, if any (TODO: better infinite recursion backstop -- detect fixpoint??)
148147
def findAllModelsFor(f: Formula): List[Model] = {
148+
149+
debug.patmat("find all models for\n"+ cnfString(f))
150+
149151
val vars: Set[Sym] = f.flatMap(_ collect {case l: Lit => l.sym}).toSet
150152
// debug.patmat("vars "+ vars)
151153
// the negation of a model -(S1=True/False /\ ... /\ SN=True/False) = clause(S1=False/True, ...., SN=False/True)
152154
def negateModel(m: Model) = clause(m.toSeq.map{ case (sym, pos) => Lit(sym, !pos) } : _*)
153155

154-
def findAllModels(f: Formula, models: List[Model], recursionDepthAllowed: Int = 10): List[Model]=
155-
if (recursionDepthAllowed == 0) models
156-
else {
157-
debug.patmat("find all models for\n"+ cnfString(f))
156+
/**
157+
* The DPLL procedure only returns a minimal mapping from literal to value
158+
* such that the CNF formula is satisfied.
159+
* E.g. for:
160+
* `(a \/ b)`
161+
* The DPLL procedure will find either {a = true} or {b = true}
162+
* as solution.
163+
*
164+
* The expansion step will amend both solutions with the unassigned variable
165+
* i.e., {a = true} will be expanded to {a = true, b = true} and {a = true, b = false}.
166+
*/
167+
def expandUnassigned(unassigned: List[Sym], model: Model): List[Model] = {
168+
// the number of solutions is doubled for every unassigned variable
169+
val expandedModels = 1 << unassigned.size
170+
var current = mutable.ArrayBuffer[Model]()
171+
var next = mutable.ArrayBuffer[Model]()
172+
current.sizeHint(expandedModels)
173+
next.sizeHint(expandedModels)
174+
175+
current += model
176+
177+
// we use double buffering:
178+
// read from `current` and create a two models for each model in `next`
179+
for {
180+
s <- unassigned
181+
} {
182+
for {
183+
model <- current
184+
} {
185+
def force(l: Lit) = model + (l.sym -> l.pos)
186+
187+
next += force(Lit(s, pos = true))
188+
next += force(Lit(s, pos = false))
189+
}
190+
191+
val tmp = current
192+
current = next
193+
next = tmp
194+
195+
next.clear()
196+
}
197+
198+
current.toList
199+
}
200+
201+
def findAllModels(f: Formula,
202+
models: List[Model],
203+
recursionDepthAllowed: Int = global.settings.YpatmatExhaustdepth.value): List[Model]=
204+
if (recursionDepthAllowed == 0) {
205+
val maxDPLLdepth = global.settings.YpatmatExhaustdepth.value
206+
reportWarning("(Exhaustivity analysis reached max recursion depth, not all missing cases are reported. " +
207+
s"Please try with scalac -Ypatmat-exhaust-depth ${maxDPLLdepth * 2} or -Ypatmat-exhaust-depth off.)")
208+
models
209+
} else {
158210
val model = findModelFor(f)
159211
// if we found a solution, conjunct the formula with the model's negation and recurse
160212
if (model ne NoModel) {
161213
val unassigned = (vars -- model.keySet).toList
162214
debug.patmat("unassigned "+ unassigned +" in "+ model)
163-
def force(lit: Lit) = {
164-
val model = withLit(findModelFor(dropUnit(f, lit)), lit)
165-
if (model ne NoModel) List(model)
166-
else Nil
167-
}
168-
val forced = unassigned flatMap { s =>
169-
force(Lit(s, pos = true)) ++ force(Lit(s, pos = false))
170-
}
215+
216+
val forced = expandUnassigned(unassigned, model)
171217
debug.patmat("forced "+ forced)
172218
val negated = negateModel(model)
173-
findAllModels(f :+ negated, model :: (forced ++ models), recursionDepthAllowed - 1)
219+
findAllModels(f :+ negated, forced ++ models, recursionDepthAllowed - 1)
174220
}
175221
else models
176222
}

‎test/files/neg/patmatexhaust.check

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ It would fail on the following inputs: (Kult(_), Kult(_)), (Qult(), Qult())
1212
^
1313
patmatexhaust.scala:49: warning: match may not be exhaustive.
1414
It would fail on the following inputs: Gp(), Gu
15-
def ma4(x:Deep) = x match { // missing cases: Gu, Gp
15+
def ma4(x:Deep) = x match { // missing cases: Gu, Gp which is not abstract so must be included
1616
^
1717
patmatexhaust.scala:55: warning: unreachable code
1818
case _ if 1 == 0 =>

‎test/files/neg/patmatexhaust.flags

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
-Xfatal-warnings
1+
-Xfatal-warnings -Ypatmat-exhaust-depth off

‎test/files/neg/patmatexhaust.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@ class TestSealedExhaustive { // compile only
4646
case _ =>
4747
}
4848

49-
def ma4(x:Deep) = x match { // missing cases: Gu, Gp
49+
def ma4(x:Deep) = x match { // missing cases: Gu, Gp which is not abstract so must be included
5050
case Ga =>
5151
}
5252

‎test/files/neg/t8430.check

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,25 +1,25 @@
11
t8430.scala:15: warning: match may not be exhaustive.
2-
It would fail on the following inputs: ??, LetC, LetF, LetL(IntLit), LetP
2+
It would fail on the following inputs: LetC, LetF, LetL(BooleanLit), LetL(IntLit), LetL(UnitLit), LetP
33
(tree: Tree) => tree match {case LetL(CharLit) => ??? }
44
^
55
t8430.scala:16: warning: match may not be exhaustive.
6-
It would fail on the following inputs: ??, LetC, LetF, LetL(IntLit), LetP
6+
It would fail on the following inputs: LetC, LetF, LetL(BooleanLit), LetL(IntLit), LetL(UnitLit), LetP
77
(tree: Tree) => tree match {case LetL(CharLit) => ??? }
88
^
99
t8430.scala:17: warning: match may not be exhaustive.
10-
It would fail on the following inputs: ??, LetC, LetF, LetL(IntLit), LetP
10+
It would fail on the following inputs: LetC, LetF, LetL(BooleanLit), LetL(IntLit), LetL(UnitLit), LetP
1111
(tree: Tree) => tree match {case LetL(CharLit) => ??? }
1212
^
1313
t8430.scala:18: warning: match may not be exhaustive.
14-
It would fail on the following inputs: ??, LetC, LetF, LetL(IntLit), LetP
14+
It would fail on the following inputs: LetC, LetF, LetL(BooleanLit), LetL(IntLit), LetL(UnitLit), LetP
1515
(tree: Tree) => tree match {case LetL(CharLit) => ??? }
1616
^
1717
t8430.scala:19: warning: match may not be exhaustive.
18-
It would fail on the following inputs: ??, LetC, LetF, LetL(IntLit), LetP
18+
It would fail on the following inputs: LetC, LetF, LetL(BooleanLit), LetL(IntLit), LetL(UnitLit), LetP
1919
(tree: Tree) => tree match {case LetL(CharLit) => ??? }
2020
^
2121
t8430.scala:20: warning: match may not be exhaustive.
22-
It would fail on the following inputs: ??, LetC, LetF, LetL(IntLit), LetP
22+
It would fail on the following inputs: LetC, LetF, LetL(BooleanLit), LetL(IntLit), LetL(UnitLit), LetP
2323
(tree: Tree) => tree match {case LetL(CharLit) => ??? }
2424
^
2525
error: No warnings can be incurred under -Xfatal-warnings.

‎test/files/neg/t8430.flags

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
-Xfatal-warnings
1+
-Xfatal-warnings -Ypatmat-exhaust-depth off

‎test/files/run/virtpatmat_nested_lists.flags

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
-Ypatmat-exhaust-depth off

‎test/files/run/virtpatmat_opt_sharing.flags

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
-Ypatmat-exhaust-depth off

0 commit comments

Comments
 (0)