1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
|
/* NSC -- new Scala compiler
*
* Copyright 2011-2013 LAMP/EPFL
* @author Adriaan Moors
*/
package scala.tools.nsc.transform.patmat
import scala.language.postfixOps
import scala.collection.mutable
import scala.reflect.internal.util.Statistics
trait TreeAndTypeAnalysis extends Debugging {
import global._
import definitions._
import analyzer.Typer
/** Compute the type T implied for a value `v` matched by a pattern `pat` (with expected type `pt`).
*
* Usually, this is the pattern's type because pattern matching implies instance-of checks.
*
* However, Stable Identifier and Literal patterns are matched using `==`,
* which does not imply a type for the binder that binds the matched value.
*
* See SI-1503, SI-5024: don't cast binders to types we're not sure they have
*
* TODO: update spec as follows (deviation between `**`):
*
* A pattern binder x@p consists of a pattern variable x and a pattern p.
* The type of the variable x is the static type T **IMPLIED BY** the pattern p.
* This pattern matches any value v matched by the pattern p
* **Deleted: , provided the run-time type of v is also an instance of T, **
* and it binds the variable name to that value.
*
* Addition:
* A pattern `p` _implies_ a type `T` if the pattern matches only values of the type `T`.
*/
def binderTypeImpliedByPattern(pat: Tree, pt: Type, binder: Symbol): Type =
pat match {
// because `==` decides whether these patterns match, stable identifier patterns (ident or selection)
// do not contribute any type information (beyond the pattern's expected type)
// e.g., in case x@Nil => x --> all we know about `x` is that it satisfies Nil == x, which could be anything
case Ident(_) | Select(_, _) =>
if (settings.future) pt
else {
// TODO: don't warn unless this unsound assumption is actually used in a cast
// I tried annotating the type returned here with an internal annotation (`pat.tpe withAnnotation UnsoundAssumptionAnnotation`),
// and catching it in the patmat backend when used in a cast (because that would signal the unsound assumption was used),
// but the annotation didn't bubble up...
// This is a pretty poor approximation.
def unsoundAssumptionUsed = binder.name != nme.WILDCARD && !(pt <:< pat.tpe)
if (settings.warnUnsoundMatch && unsoundAssumptionUsed)
reporter.warning(pat.pos,
sm"""The value matched by $pat is bound to ${binder.name}, which may be used under the
|unsound assumption that it has type ${pat.tpe}, whereas we can only safely
|count on it having type $pt, as the pattern is matched using `==` (see SI-1503).""")
pat.tpe
}
// the other patterns imply type tests, so we can safely assume the binder has the pattern's type when the pattern matches
// concretely, a literal, type pattern, a case class (the constructor's result type) or extractor (the unapply's argument type) all imply type tests
// (and, inductively, an alternative)
case _ => pat.tpe
}
// we use subtyping as a model for implication between instanceof tests
// i.e., when S <:< T we assume x.isInstanceOf[S] implies x.isInstanceOf[T]
// unfortunately this is not true in general:
// SI-6022 expects instanceOfTpImplies(ProductClass.tpe, AnyRefTpe)
def instanceOfTpImplies(tp: Type, tpImplied: Type) = {
val tpValue = isPrimitiveValueType(tp)
// pretend we're comparing to Any when we're actually comparing to AnyVal or AnyRef
// (and the subtype is respectively a value type or not a value type)
// this allows us to reuse subtyping as a model for implication between instanceOf tests
// the latter don't see a difference between AnyRef, Object or Any when comparing non-value types -- SI-6022
val tpImpliedNormalizedToAny =
if (tpImplied =:= (if (tpValue) AnyValTpe else AnyRefTpe)) AnyTpe
else tpImplied
tp <:< tpImpliedNormalizedToAny
}
// TODO: improve, e.g., for constants
def sameValue(a: Tree, b: Tree): Boolean = (a eq b) || ((a, b) match {
case (_ : Ident, _ : Ident) => a.symbol eq b.symbol
case _ => false
})
trait CheckableTreeAndTypeAnalysis {
val typer: Typer
// TODO: domain of other feasibly enumerable built-in types (char?)
def enumerateSubtypes(tp: Type): Option[List[Type]] =
tp.typeSymbol match {
// TODO case _ if tp.isTupleType => // recurse into component types?
case UnitClass =>
Some(List(UnitTpe))
case BooleanClass =>
Some(ConstantTrue :: ConstantFalse :: Nil)
// TODO case _ if tp.isTupleType => // recurse into component types
case modSym: ModuleClassSymbol =>
Some(List(tp))
case sym: RefinementClassSymbol =>
val parentSubtypes: List[Option[List[Type]]] = tp.parents.map(parent => enumerateSubtypes(parent))
if (parentSubtypes exists (_.isDefined))
// If any of the parents is enumerable, then the refinement type is enumerable.
Some(
// We must only include subtypes of the parents that conform to `tp`.
// See neg/virtpatmat_exhaust_compound.scala for an example.
parentSubtypes flatMap (_.getOrElse(Nil)) filter (_ <:< tp)
)
else None
// make sure it's not a primitive, else (5: Byte) match { case 5 => ... } sees no Byte
case sym if sym.isSealed =>
val subclasses = debug.patmatResult(s"enum $sym sealed, subclasses")(
// 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.
sym.sealedDescendants.toList
sortBy (_.sealedSortName)
filterNot (x => x.isSealed && x.isAbstractClass && !isPrimitiveValueClass(x))
)
val tpApprox = typer.infer.approximateAbstracts(tp)
val pre = tpApprox.prefix
Some(debug.patmatResult(s"enum sealed tp=$tp, tpApprox=$tpApprox as") {
// valid subtypes are turned into checkable types, as we are entering the realm of the dynamic
subclasses flatMap { sym =>
// have to filter out children which cannot match: see ticket #3683 for an example
// compare to the fully known type `tp` (modulo abstract types),
// so that we can rule out stuff like: sealed trait X[T]; class XInt extends X[Int] --> XInt not valid when enumerating X[String]
// however, must approximate abstract types in
val memberType = nestedMemberType(sym, pre, tpApprox.typeSymbol.owner)
val subTp = appliedType(memberType, sym.typeParams.map(_ => WildcardType))
val subTpApprox = typer.infer.approximateAbstracts(subTp) // TODO: needed?
// debug.patmat("subtp"+(subTpApprox <:< tpApprox, subTpApprox, tpApprox))
if (subTpApprox <:< tpApprox) Some(checkableType(subTp))
else None
}
})
case sym =>
debug.patmat("enum unsealed "+ ((tp, sym, sym.isSealed, isPrimitiveValueClass(sym))))
None
}
// 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)
def checkableType(tp: Type): Type = {
// TODO: this is extremely rough...
// replace type args by wildcards, since they can't be checked (don't use existentials: overkill)
// TODO: when type tags are available, we will check -- when this is implemented, can we take that into account here?
// similar to typer.infer.approximateAbstracts
object typeArgsToWildcardsExceptArray extends TypeMap {
// SI-6771 dealias would be enough today, but future proofing with the dealiasWiden.
// See neg/t6771b.scala for elaboration
def apply(tp: Type): Type = tp.dealias match {
case TypeRef(pre, sym, args) if args.nonEmpty && (sym ne ArrayClass) =>
TypeRef(pre, sym, args map (_ => WildcardType))
case _ =>
mapOver(tp)
}
}
val result = typeArgsToWildcardsExceptArray(tp)
debug.patmatResult(s"checkableType($tp)")(result)
}
// a type is "uncheckable" (for exhaustivity) if we don't statically know its subtypes (i.e., it's unsealed)
// we consider tuple types with at least one component of a checkable type as a checkable type
def uncheckableType(tp: Type): Boolean = {
val checkable = (
(isTupleType(tp) && tupleComponents(tp).exists(tp => !uncheckableType(tp)))
|| enumerateSubtypes(tp).nonEmpty)
// if (!checkable) debug.patmat("deemed uncheckable: "+ tp)
!checkable
}
}
}
trait MatchApproximation extends TreeAndTypeAnalysis with ScalaLogic with MatchTreeMaking {
import global._
import global.definitions._
/**
* Represent a match as a formula in propositional logic that encodes whether the match matches (abstractly: we only consider types)
*
*/
trait MatchApproximator extends TreeMakers with TreesAndTypesDomain {
object Test {
var currId = 0
}
case class Test(prop: Prop, treeMaker: TreeMaker) {
// private val reusedBy = new mutable.HashSet[Test]
var reuses: Option[Test] = None
def registerReuseBy(later: Test): Unit = {
assert(later.reuses.isEmpty, later.reuses)
// reusedBy += later
later.reuses = Some(this)
}
val id = { Test.currId += 1; Test.currId}
override def toString = s"T${id}C($prop)"
}
class TreeMakersToPropsIgnoreNullChecks(root: Symbol) extends TreeMakersToProps(root) {
override def uniqueNonNullProp(p: Tree): Prop = True
}
// returns (tree, tests), where `tree` will be used to refer to `root` in `tests`
class TreeMakersToProps(val root: Symbol) {
prepareNewAnalysis() // reset hash consing for Var and Const
private[this] val uniqueEqualityProps = new mutable.HashMap[(Tree, Tree), Eq]
private[this] val uniqueNonNullProps = new mutable.HashMap[Tree, Not]
private[this] val uniqueTypeProps = new mutable.HashMap[(Tree, Type), Eq]
def uniqueEqualityProp(testedPath: Tree, rhs: Tree): Prop =
uniqueEqualityProps getOrElseUpdate((testedPath, rhs), Eq(Var(testedPath), ValueConst(rhs)))
// overridden in TreeMakersToPropsIgnoreNullChecks
def uniqueNonNullProp (testedPath: Tree): Prop =
uniqueNonNullProps getOrElseUpdate(testedPath, Not(Eq(Var(testedPath), NullConst)))
def uniqueTypeProp(testedPath: Tree, pt: Type): Prop =
uniqueTypeProps getOrElseUpdate((testedPath, pt), Eq(Var(testedPath), TypeConst(checkableType(pt))))
// 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 = mutable.HashSet(root)
private val trees = mutable.HashSet.empty[Tree]
// the substitution that renames variables to variables in pointsToBound
private var normalize: Substitution = EmptySubstitution
private var substitutionComputed = false
// 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
// hashconsing trees (modulo value-equality)
def unique(t: Tree, tpOverride: Type = NoType): Tree =
trees find (a => a.correspondsStructure(t)(sameValue)) match {
case Some(orig) =>
// debug.patmat("unique: "+ (t eq orig, orig))
orig
case _ =>
trees += t
if (tpOverride != NoType) t setType tpOverride
else t
}
def uniqueTp(tp: Type): Type = tp match {
// typerefs etc are already hashconsed
case _ : UniqueType => tp
case tp@RefinedType(parents, EmptyScope) => tp.memo(tp: Type)(identity) // TODO: does this help?
case _ => tp
}
// 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
final def binderToUniqueTree(b: Symbol) =
unique(accumSubst(normalize(gen.mkAttributedStableRef(b))), b.tpe)
// 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
abstract class TreeMakerToProp extends (TreeMaker => Prop) {
// requires(if (!substitutionComputed))
def updateSubstitution(subst: Substitution): Unit = {
// 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.exists && 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 type we have for these later variables, but that's probably okay
normalize >>= Substitution(boundTo map (_.symbol), boundFrom map (CODE.REF(_)))
// debug.patmat ("normalize subst: "+ 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
// debug.patmat("pointsToBound: "+ pointsToBound)
accumSubst >>= okSubst
// debug.patmat("accumSubst: "+ accumSubst)
}
def handleUnknown(tm: TreeMaker): Prop
/** apply itself must render a faithful representation of the TreeMaker
*
* Concretely, True must only be used to represent a TreeMaker that is sure to match and that does not do any computation at all
* e.g., doCSE relies on apply itself being sound in this sense (since it drops TreeMakers that are approximated to True -- SI-6077)
*
* handleUnknown may be customized by the caller to approximate further
*
* TODO: don't ignore outer-checks
*/
def apply(tm: TreeMaker): Prop = {
if (!substitutionComputed) updateSubstitution(tm.subPatternsAsSubstitution)
tm match {
case ttm@TypeTestTreeMaker(prevBinder, testedBinder, pt, _) =>
object condStrategy extends TypeTestTreeMaker.TypeTestCondStrategy {
type Result = Prop
def and(a: Result, b: Result) = And(a, b)
def outerTest(testedBinder: Symbol, expectedTp: Type) = True // TODO OuterEqProp(testedBinder, expectedType)
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); And(uniqueNonNullProp(p), uniqueTypeProp(p, uniqueTp(pt)))
}
def nonNullTest(testedBinder: Symbol) = uniqueNonNullProp(binderToUniqueTree(testedBinder))
def equalsTest(pat: Tree, testedBinder: Symbol) = uniqueEqualityProp(binderToUniqueTree(testedBinder), unique(pat))
// rewrite eq test to type test against the singleton type `pat.tpe`; unrelated to == (uniqueEqualityProp), could be null
def eqTest(pat: Tree, testedBinder: Symbol) = uniqueTypeProp(binderToUniqueTree(testedBinder), uniqueTp(pat.tpe))
def tru = True
}
ttm.renderCondition(condStrategy)
case EqualityTestTreeMaker(prevBinder, patTree, _) => uniqueEqualityProp(binderToUniqueTree(prevBinder), unique(patTree))
case AlternativesTreeMaker(_, altss, _) => \/(altss map (alts => /\(alts map this)))
case ProductExtractorTreeMaker(testedBinder, None) => uniqueNonNullProp(binderToUniqueTree(testedBinder))
case SubstOnlyTreeMaker(_, _) => True
case GuardTreeMaker(guard) =>
guard.tpe match {
case ConstantTrue => True
case ConstantFalse => False
case _ => handleUnknown(tm)
}
case ExtractorTreeMaker(_, _, _) |
ProductExtractorTreeMaker(_, _) |
BodyTreeMaker(_, _) => handleUnknown(tm)
}
}
}
private val irrefutableExtractor: PartialFunction[TreeMaker, Prop] = {
// the extra condition is None, the extractor's result indicates it always succeeds,
// (the potential type-test for the argument is represented by a separate TypeTestTreeMaker)
case IrrefutableExtractorTreeMaker(_, _) => True
}
// special-case: interpret pattern `List()` as `Nil`
// TODO: make it more general List(1, 2) => 1 :: 2 :: Nil -- not sure this is a good idea...
private val rewriteListPattern: PartialFunction[TreeMaker, Prop] = {
case p @ ExtractorTreeMaker(_, _, testedBinder)
if testedBinder.tpe.typeSymbol == ListClass && p.checkedLength == Some(0) =>
uniqueEqualityProp(binderToUniqueTree(p.prevBinder), unique(Ident(NilModule) setType NilModule.tpe))
}
val fullRewrite = (irrefutableExtractor orElse rewriteListPattern)
val refutableRewrite = irrefutableExtractor
@inline def onUnknown(handler: TreeMaker => Prop) = new TreeMakerToProp {
def handleUnknown(tm: TreeMaker) = handler(tm)
}
// used for CSE -- rewrite all unknowns to False (the most conserative option)
object conservative extends TreeMakerToProp {
def handleUnknown(tm: TreeMaker) = False
}
final def approximateMatch(cases: List[List[TreeMaker]], treeMakerToProp: TreeMakerToProp = conservative) ={
val testss = cases.map { _ map (tm => Test(treeMakerToProp(tm), tm)) }
substitutionComputed = true // a second call to approximateMatch should not re-compute the substitution (would be wrong)
testss
}
}
def approximateMatchConservative(root: Symbol, cases: List[List[TreeMaker]]): List[List[Test]] =
(new TreeMakersToProps(root)).approximateMatch(cases)
// turns a case (represented as a list of abstract tests)
// into a proposition that is satisfiable if the case may match
protected final def caseWithoutBodyToProp(tests: List[Test]): Prop =
/\(tests.takeWhile(t => !t.treeMaker.isInstanceOf[BodyTreeMaker]).map(t => t.prop))
def showTreeMakers(cases: List[List[TreeMaker]]) = {
debug.patmat("treeMakers:")
debug.patmat(alignAcrossRows(cases, ">>"))
}
}
}
trait MatchAnalysis extends MatchApproximation {
import PatternMatchingStats._
import global._
import global.definitions._
trait MatchAnalyzer extends MatchApproximator {
def uncheckedWarning(pos: Position, msg: String) = currentRun.reporting.uncheckedWarning(pos, msg)
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
// 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] = {
val start = if (Statistics.canEnable) Statistics.startTimer(patmatAnaReach) else null
// use the same approximator so we share variables,
// but need different conditions depending on whether we're conservatively looking for failure or success
// don't rewrite List-like patterns, as List() and Nil need to distinguished for unreachability
val approx = new TreeMakersToProps(prevBinder)
def approximate(default: Prop) = approx.approximateMatch(cases, approx.onUnknown { tm =>
approx.refutableRewrite.applyOrElse(tm, (_: TreeMaker) => default )
})
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
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))
reachable = NoModel ne model
}
}
if (Statistics.canEnable) Statistics.stopTimer(patmatAnaReach, start)
if (reachable) None else Some(caseIndex)
}
// exhaustivity
def exhaustive(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type): List[String] = if (uncheckableType(prevBinder.info)) Nil else {
// customize TreeMakersToProps (which turns a tree of tree makers into a more abstract DAG of tests)
// - approximate the pattern `List()` (unapplySeq on List with empty length) as `Nil`,
// otherwise the common (xs: List[Any]) match { case List() => case x :: xs => } is deemed unexhaustive
// - 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 = if (Statistics.canEnable) Statistics.startTimer(patmatAnaExhaust) else null
var backoff = false
val approx = new TreeMakersToPropsIgnoreNullChecks(prevBinder)
val symbolicCases = approx.approximateMatch(cases, approx.onUnknown { tm =>
approx.fullRewrite.applyOrElse[TreeMaker, Prop](tm, {
case BodyTreeMaker(_, _) => True // irrelevant -- will be discarded by symbolCase later
case _ => // debug.patmat("backing off due to "+ tm)
backoff = true
False
})
}) map caseWithoutBodyToProp
if (backoff) Nil else {
val prevBinderTree = approx.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?
// val nonNullScrutineeCond =
// assume non-null for all the components of the tuple we're matching on (if we're matching on a tuple)
// if (isTupleType(prevBinder.tpe))
// prevBinder.tpe.typeArgs.mapWithIndex{case (_, i) => NonNullProp(codegen.tupleSel(prevBinderTree)(i))}.reduceLeft(And)
// else
// NonNullProp(prevBinderTree)
// val matchFails = And(symbolic(nonNullScrutineeCond), Not(symbolicCases reduceLeft (Or(_, _))))
// when does the match fail?
val matchFails = Not(\/(symbolicCases))
// 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))
val scrutVar = Var(prevBinderTree)
val counterExamples = matchFailModels.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
}
}
object CounterExample {
def prune(examples: List[CounterExample]): List[CounterExample] = {
// SI-7669 Warning: we don't used examples.distinct here any more as
// we can have A != B && A.coveredBy(B) && B.coveredBy(A)
// with Nil and List().
val result = mutable.Buffer[CounterExample]()
for (example <- examples if (!result.exists(example coveredBy _)))
result += example
result.toList
}
}
// a way to construct a value that will make the match fail: a constructor invocation, a constant, an object of some type)
class CounterExample {
protected[MatchAnalyzer] def flattenConsArgs: List[CounterExample] = Nil
def coveredBy(other: CounterExample): Boolean = this == other || other == WildcardExample
}
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(eqTo: Const, nonTrivialNonEqualTo: List[Const]) extends CounterExample {
// require(nonTrivialNonEqualTo.nonEmpty, nonTrivialNonEqualTo)
override def toString = {
val negation =
if (nonTrivialNonEqualTo.tail.isEmpty) nonTrivialNonEqualTo.head.toString
else nonTrivialNonEqualTo.map(_.toString).sorted.mkString("(", ", ", ")")
"(x: "+ eqTo +" forSome x not in "+ negation +")"
}
}
case class ListExample(ctorArgs: List[CounterExample]) extends CounterExample {
protected[MatchAnalyzer] override def flattenConsArgs: List[CounterExample] = ctorArgs match {
case hd :: tl :: Nil => hd :: tl.flattenConsArgs
case _ => Nil
}
protected[MatchAnalyzer] lazy val elems = flattenConsArgs
override def coveredBy(other: CounterExample): Boolean =
other match {
case other@ListExample(_) =>
this == other || ((elems.length == other.elems.length) && (elems zip other.elems).forall{case (a, b) => a coveredBy b})
case _ => super.coveredBy(other)
}
override def toString = elems.mkString("List(", ", ", ")")
}
case class TupleExample(ctorArgs: List[CounterExample]) extends CounterExample {
override def toString = ctorArgs.mkString("(", ", ", ")")
override def coveredBy(other: CounterExample): Boolean =
other match {
case TupleExample(otherArgs) =>
this == other || ((ctorArgs.length == otherArgs.length) && (ctorArgs zip otherArgs).forall{case (a, b) => a coveredBy b})
case _ => super.coveredBy(other)
}
}
case class ConstructorExample(cls: Symbol, ctorArgs: List[CounterExample]) extends CounterExample {
override def toString = cls.decodedName + (if (cls.isModuleClass) "" else ctorArgs.mkString("(", ", ", ")"))
}
case object WildcardExample extends CounterExample { override def toString = "_" }
case object NoExample extends CounterExample { override def toString = "??" }
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.staticTpCheckable +") "+ assignment
}.mkString("\n")
// 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(_ :: _, _ :: _),
// since we didn't realize the tail of the outer cons was a Nil)
def modelToCounterExample(scrutVar: Var)(model: Model): Option[CounterExample] = {
// x1 = ...
// x1.hd = ...
// x1.tl = ...
// x1.hd.hd = ...
// ...
val varAssignment = modelToVarAssignment(model)
debug.patmat("var assignment for model "+ model +":\n"+ varAssignmentString(varAssignment))
// chop a path into a list of symbols
def chop(path: Tree): List[Symbol] = path match {
case Ident(_) => List(path.symbol)
case Select(pre, name) => chop(pre) :+ path.symbol
case _ =>
// debug.patmat("don't know how to chop "+ path)
Nil
}
// turn the variable assignments into a tree
// the root is the scrutinee (x1), edges are labelled by the fields that are assigned
// a node is a variable example (which is later turned into a counter example)
object VariableAssignment {
private def findVar(path: List[Symbol]) = path match {
case List(root) if root == scrutVar.path.symbol => Some(scrutVar)
case _ => varAssignment.find{case (v, a) => chop(v.path) == path}.map(_._1)
}
private val uniques = new mutable.HashMap[Var, VariableAssignment]
private def unique(variable: Var): VariableAssignment =
uniques.getOrElseUpdate(variable, {
val (eqTo, neqTo) = varAssignment.getOrElse(variable, (Nil, Nil)) // TODO
VariableAssignment(variable, eqTo.toList, neqTo.toList)
})
def apply(variable: Var): VariableAssignment = {
val path = chop(variable.path)
val pre = path.init
val field = path.last
val newCtor = unique(variable)
if (pre.isEmpty) newCtor
else {
findVar(pre) foreach { preVar =>
val outerCtor = this(preVar)
outerCtor.addField(field, newCtor)
}
newCtor
}
}
}
// node in the tree that describes how to construct a counter-example
case class VariableAssignment(variable: Var, equalTo: List[Const], notEqualTo: List[Const]) {
private val fields: mutable.Map[Symbol, VariableAssignment] = mutable.HashMap.empty
// need to prune since the model now incorporates all super types of a constant (needed for reachability)
private lazy val uniqueEqualTo = equalTo filterNot (subsumed => equalTo.exists(better => (better ne subsumed) && instanceOfTpImplies(better.tp, subsumed.tp)))
private lazy val inSameDomain = uniqueEqualTo forall (const => variable.domainSyms.exists(_.exists(_.const.tp =:= const.tp)))
private lazy val prunedEqualTo = uniqueEqualTo filterNot (subsumed => variable.staticTpCheckable <:< subsumed.tp)
private lazy val ctor = (prunedEqualTo match { case List(TypeConst(tp)) => tp case _ => variable.staticTpCheckable }).typeSymbol.primaryConstructor
private lazy val ctorParams = if (ctor.paramss.isEmpty) Nil else ctor.paramss.head
private lazy val cls = ctor.safeOwner
private lazy val caseFieldAccs = cls.caseFieldAccessors
def addField(symbol: Symbol, assign: VariableAssignment) {
// SI-7669 Only register this field if if this class contains it.
val shouldConstrainField = !symbol.isCaseAccessor || caseFieldAccs.contains(symbol)
if (shouldConstrainField) fields(symbol) = assign
}
def allFieldAssignmentsLegal: Boolean =
(fields.keySet subsetOf caseFieldAccs.toSet) && fields.values.forall(_.allFieldAssignmentsLegal)
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?)
// beBrief is used to suppress negative information nested in tuples -- it tends to get too noisy
def toCounterExample(beBrief: Boolean = false): Option[CounterExample] =
if (!allFieldAssignmentsLegal) Some(NoExample)
else {
debug.patmat("describing "+ ((variable, equalTo, notEqualTo, fields, cls, allFieldAssignmentsLegal)))
val res = prunedEqualTo match {
// a definite assignment to a value
case List(eq: ValueConst) if fields.isEmpty => Some(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 && !isPrimitiveValueClass(cls) &&
( uniqueEqualTo.nonEmpty
|| (fields.nonEmpty && prunedEqualTo.isEmpty && notEqualTo.isEmpty)) =>
def args(brevity: Boolean = beBrief) = {
// figure out the constructor arguments from the field assignment
val argLen = (caseFieldAccs.length min ctorParams.length)
val examples = (0 until argLen).map(i => fields.get(caseFieldAccs(i)).map(_.toCounterExample(brevity)) getOrElse Some(WildcardExample)).toList
sequence(examples)
}
cls match {
case ConsClass =>
args().map {
case List(NoExample, l: ListExample) =>
// special case for neg/t7020.scala:
// if we find a counter example `??::*` we report `*::*` instead
// since the `??` originates from uniqueEqualTo containing several instanced of the same type
List(WildcardExample, l)
case args => args
}.map(ListExample)
case _ if isTupleSymbol(cls) => args(brevity = true).map(TupleExample)
case _ if cls.isSealed && cls.isAbstractClass =>
// don't report sealed abstract classes, since
// 1) they can't be instantiated
// 2) we are already reporting any missing subclass (since we know the full domain)
// (see patmatexhaust.scala)
None
case _ => args().map(ConstructorExample(cls, _))
}
// a definite assignment to a type
case List(eq) if fields.isEmpty => Some(TypeExample(eq))
// negative information
case Nil if nonTrivialNonEqualTo.nonEmpty =>
// negation tends to get pretty verbose
if (beBrief) Some(WildcardExample)
else {
val eqTo = equalTo.headOption getOrElse TypeConst(variable.staticTpCheckable)
Some(NegativeExample(eqTo, nonTrivialNonEqualTo))
}
// if uniqueEqualTo contains more than one symbol of the same domain
// then we can safely ignore these counter examples since we will eventually encounter
// both counter examples separately
case _ if inSameDomain => None
// not a valid counter-example, possibly since we have a definite type but there was a field mismatch
// TODO: improve reasoning -- in the mean time, a false negative is better than an annoying false positive
case _ => Some(NoExample)
}
debug.patmatResult("described as")(res)
}
override def toString = toCounterExample().toString
}
// slurp in information from other variables
varAssignment.keys.foreach{ v => if (v != scrutVar) VariableAssignment(v) }
// this is the variable we want a counter example for
VariableAssignment(scrutVar).toCounterExample()
}
def analyzeCases(prevBinder: Symbol, cases: List[List[TreeMaker]], pt: Type, suppression: Suppression): Unit = {
if (!suppression.suppressUnreachable) {
unreachableCase(prevBinder, cases, pt) foreach { caseIndex =>
reportUnreachable(cases(caseIndex).last.pos)
}
}
if (!suppression.suppressExhaustive) {
val counterExamples = exhaustive(prevBinder, cases, pt)
if (counterExamples.nonEmpty)
reportMissingCases(prevBinder.pos, counterExamples)
}
}
}
}
|