Skip to content

Fix #4225: always do reachability check #4253

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 11 commits into from
Apr 6, 2018
1 change: 0 additions & 1 deletion compiler/src/dotty/tools/dotc/ast/Desugar.scala
Original file line number Diff line number Diff line change
Expand Up @@ -429,7 +429,6 @@ object desugar {
}
val hasRepeatedParam = constrVparamss.exists(_.exists {
case ValDef(_, tpt, _) => isRepeated(tpt)
case _ => false
})
if (mods.is(Abstract) || hasRepeatedParam) Nil // cannot have default arguments for repeated parameters, hence copy method is not issued
else {
Expand Down
33 changes: 14 additions & 19 deletions compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
Original file line number Diff line number Diff line change
Expand Up @@ -473,26 +473,21 @@ class PlainPrinter(_ctx: Context) extends Printer {
("Scope{" ~ dclsText(sc.toList) ~ "}").close

def toText[T >: Untyped](tree: Tree[T]): Text = {
tree match {
case node: Positioned =>
def toTextElem(elem: Any): Text = elem match {
case elem: Showable => elem.toText(this)
case elem: List[_] => "List(" ~ Text(elem map toTextElem, ",") ~ ")"
case elem => elem.toString
}
val nodeName = node.productPrefix
val elems =
Text(node.productIterator.map(toTextElem).toList, ", ")
val tpSuffix =
if (ctx.settings.XprintTypes.value && tree.hasType)
" | " ~ toText(tree.typeOpt)
else
Text()

nodeName ~ "(" ~ elems ~ tpSuffix ~ ")" ~ (Str(node.pos.toString) provided ctx.settings.YprintPos.value)
case _ =>
tree.fallbackToText(this)
def toTextElem(elem: Any): Text = elem match {
case elem: Showable => elem.toText(this)
case elem: List[_] => "List(" ~ Text(elem map toTextElem, ",") ~ ")"
case elem => elem.toString
}
val nodeName = tree.productPrefix
val elems =
Text(tree.productIterator.map(toTextElem).toList, ", ")
val tpSuffix =
if (ctx.settings.XprintTypes.value && tree.hasType)
" | " ~ toText(tree.typeOpt)
else
Text()

nodeName ~ "(" ~ elems ~ tpSuffix ~ ")" ~ (Str(tree.pos.toString) provided ctx.settings.YprintPos.value)
}.close // todo: override in refined printer

def toText(result: SearchResult): Text = result match {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -128,6 +128,7 @@ public enum ErrorMessageID {
ParamsNoInlineID,
JavaSymbolIsNotAValueID,
DoubleDeclarationID,
MatchCaseOnlyNullWarningID,
;

public int errorNumber() {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -909,8 +909,15 @@ object messages {

case class MatchCaseUnreachable()(implicit ctx: Context)
extends Message(MatchCaseUnreachableID) {
val kind = s"""Match ${hl"case"} Unreachable"""
val msg = "unreachable code"
val kind = "Match case Unreachable"
val msg = "unreachable case"
val explanation = ""
}

case class MatchCaseOnlyNullWarning()(implicit ctx: Context)
extends Message(MatchCaseOnlyNullWarningID) {
val kind = "Only null matched"
val msg = s"Only ${hl"null"} is matched. Consider using `case null =>` instead."
val explanation = ""
}

Expand Down
7 changes: 2 additions & 5 deletions compiler/src/dotty/tools/dotc/transform/PatternMatcher.scala
Original file line number Diff line number Diff line change
Expand Up @@ -33,11 +33,8 @@ class PatternMatcher extends MiniPhase {

// check exhaustivity and unreachability
val engine = new patmat.SpaceEngine

if (engine.checkable(tree)) {
engine.checkExhaustivity(tree)
engine.checkRedundancy(tree)
}
engine.checkExhaustivity(tree)
engine.checkRedundancy(tree)

translated.ensureConforms(tree.tpe)
}
Expand Down
1 change: 0 additions & 1 deletion compiler/src/dotty/tools/dotc/transform/Splicer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -86,7 +86,6 @@ object Splicer {
""".stripMargin
ctx.error(msg, pos)
None
case ex: Throwable => throw ex
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks wrong to me, a try/catch can always catch a Throwable.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, we could keep it, and no warning will be reported. I removed it because the compiler will generate a default case anyway.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

OK.

}
}

Expand Down
114 changes: 77 additions & 37 deletions compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
Original file line number Diff line number Diff line change
Expand Up @@ -63,7 +63,7 @@ case object Empty extends Space
* @param decomposed: does the space result from decomposition? Used for pretty print
*
*/
case class Typ(tp: Type, decomposed: Boolean) extends Space
case class Typ(tp: Type, decomposed: Boolean = true) extends Space

/** Space representing an extractor pattern */
case class Prod(tp: Type, unappTp: Type, unappSym: Symbol, params: List[Space], full: Boolean) extends Space
Expand Down Expand Up @@ -288,6 +288,9 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
private val scalaNilType = ctx.requiredModuleRef("scala.collection.immutable.Nil")
private val scalaConsType = ctx.requiredClassRef("scala.collection.immutable.::")

private val nullType = ConstantType(Constant(null))
private val nullSpace = Typ(nullType)

override def intersectUnrelatedAtomicTypes(tp1: Type, tp2: Type) = {
val and = AndType(tp1, tp2)
// Precondition: !(tp1 <:< tp2) && !(tp2 <:< tp1)
Expand All @@ -296,7 +299,10 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {

debug.println(s"atomic intersection: ${and.show} = ${res}")

if (res) Typ(and, true) else Empty
if (!res) Empty
else if (tp1.isSingleton) Typ(tp1, true)
else if (tp2.isSingleton) Typ(tp2, true)
else Typ(and, true)
}

/** Whether the extractor is irrefutable */
Expand All @@ -315,6 +321,8 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
else
Typ(ConstantType(c), false)
case _: BackquotedIdent => Typ(pat.tpe, false)
case Ident(nme.WILDCARD) =>
Or(Typ(pat.tpe.stripAnnots, false) :: nullSpace :: Nil)
case Ident(_) | Select(_, _) =>
Typ(pat.tpe.stripAnnots, false)
case Alternative(trees) => Or(trees.map(project(_)))
Expand All @@ -331,6 +339,10 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
case Typed(pat @ UnApply(_, _, _), _) => project(pat)
case Typed(expr, tpt) =>
Typ(erase(expr.tpe.stripAnnots), true)
case This(_) =>
Typ(pat.tpe.stripAnnots, false)
case EmptyTree => // default rethrow clause of try/catch, check tests/patmat/try2.scala
Typ(WildcardType, false)
case _ =>
debug.println(s"unknown pattern: $pat")
Empty
Expand All @@ -345,8 +357,8 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
OrType(erase(tp1), erase(tp2))
case AndType(tp1, tp2) =>
AndType(erase(tp1), erase(tp2))
case tp: RefinedType =>
tp.derivedRefinedType(erase(tp.parent), tp.refinedName, WildcardType)
case tp @ RefinedType(parent, refinedName, _) if refinedName.isTermName => // see pos/dependent-extractors.scala
tp.derivedRefinedType(erase(parent), refinedName, WildcardType)
case _ => tp
}

Expand All @@ -370,7 +382,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {

/** Is `tp1` a subtype of `tp2`? */
def isSubType(tp1: Type, tp2: Type): Boolean = {
val res = tp1 <:< tp2
val res = (tp1 != nullType || tp2 == nullType) && tp1 <:< tp2
debug.println(s"${tp1.show} <:< ${tp2.show} = $res")
res
}
Expand Down Expand Up @@ -543,13 +555,6 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
case tp => tp.isSingleton
}

def superType(tp: Type): Type = tp match {
case tp: TypeProxy => tp.superType
case OrType(tp1, tp2) => OrType(superType(tp1), superType(tp2))
case AndType(tp1, tp2) => AndType(superType(tp1), superType(tp2))
case _ => tp
}

def recur(tp: Type): Boolean = tp.dealias match {
case AndType(tp1, tp2) =>
recur(tp1) && recur(tp2) && {
Expand All @@ -570,8 +575,8 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
noClassConflict &&
(!isSingleton(tp1) || tp1 <:< tp2) &&
(!isSingleton(tp2) || tp2 <:< tp1) &&
(!bases1.exists(_ is Final) || tp1 <:< superType(tp2)) &&
(!bases2.exists(_ is Final) || tp2 <:< superType(tp1))
(!bases1.exists(_ is Final) || tp1 <:< tp2) &&
(!bases2.exists(_ is Final) || tp2 <:< tp1)
}
case OrType(tp1, tp2) =>
recur(tp1) || recur(tp2)
Expand Down Expand Up @@ -842,7 +847,7 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
flatten(s).map(doShow(_, false)).distinct.mkString(", ")
}

def checkable(tree: Match): Boolean = {
private def exhaustivityCheckable(sel: Tree): Boolean = {
// Possible to check everything, but be compatible with scalac by default
def isCheckable(tp: Type): Boolean =
!tp.hasAnnotation(defn.UncheckedAnnot) && {
Expand All @@ -860,26 +865,25 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
(defn.isTupleType(tpw) && tpw.argInfos.exists(isCheckable(_)))
}

val Match(sel, cases) = tree
val res = isCheckable(sel.tpe)
debug.println(s"checkable: ${sel.show} = $res")
debug.println(s"exhaustivity checkable: ${sel.show} = $res")
res
}

/** Whehter counter-examples should be further checked? True for GADTs. */
def shouldCheckExamples(tp: Type): Boolean = {
private def shouldCheckExamples(tp: Type): Boolean =
new TypeAccumulator[Boolean] {
override def apply(b: Boolean, tp: Type): Boolean = tp match {
case tref: TypeRef if tref.symbol.is(TypeParam) && variance != 1 => true
case tp => b || foldOver(b, tp)
}
}.apply(false, tp)
}

def checkExhaustivity(_match: Match): Unit = {
val Match(sel, cases) = _match
val selTyp = sel.tpe.widen.dealias

if (!exhaustivityCheckable(sel)) return

val patternSpace = cases.map({ x =>
val space = project(x.pat)
Expand All @@ -890,36 +894,72 @@ class SpaceEngine(implicit ctx: Context) extends SpaceLogic {
val checkGADTSAT = shouldCheckExamples(selTyp)

val uncovered =
flatten(simplify(minus(Typ(selTyp, true), patternSpace), aggressive = true))
.filter(s => s != Empty && (!checkGADTSAT || satisfiable(s)))
flatten(simplify(minus(Typ(selTyp, true), patternSpace), aggressive = true)).filter { s =>
s != Empty && (!checkGADTSAT || satisfiable(s))
}

if (uncovered.nonEmpty)
ctx.warning(PatternMatchExhaustivity(show(Or(uncovered))), sel.pos)
}

private def redundancyCheckable(sel: Tree): Boolean =
!sel.tpe.hasAnnotation(defn.UncheckedAnnot)

def checkRedundancy(_match: Match): Unit = {
val Match(sel, cases) = _match
// ignore selector type for now
val selTyp = sel.tpe.widen.dealias

(0 until cases.length).foreach { i =>
// in redundancy check, take guard as false in order to soundly approximate
val prevs =
if (i == 0)
Empty
else
cases.take(i).map { x =>
if (x.guard.isEmpty) project(x.pat)
else Empty
}.reduce((a, b) => Or(List(a, b)))
if (!redundancyCheckable(sel)) return

val targetSpace =
if (selTyp.classSymbol.isPrimitiveValueClass)
Typ(selTyp, true)
else
Or(Typ(selTyp, true) :: nullSpace :: Nil)

val curr = project(cases(i).pat)
// in redundancy check, take guard as false in order to soundly approximate
def projectPrevCases(cases: List[CaseDef]): Space =
cases.map { x =>
if (x.guard.isEmpty) project(x.pat)
else Empty
}.reduce((a, b) => Or(List(a, b)))

debug.println(s"---------------reachable? ${show(curr)}")
debug.println(s"prev: ${show(prevs)}")
def isNull(tree: Tree): Boolean = tree match {
case Literal(Constant(null)) => true
case _ => false
}

if (isSubspace(intersect(curr, Typ(selTyp, false)), prevs)) {
ctx.warning(MatchCaseUnreachable(), cases(i).body.pos)
(1 until cases.length).foreach { i =>
val prevs = projectPrevCases(cases.take(i))

val pat = cases(i).pat

if (pat != EmptyTree) { // rethrow case of catch uses EmptyTree
val curr = project(pat)

debug.println(s"---------------reachable? ${show(curr)}")
debug.println(s"prev: ${show(prevs)}")

var covered = simplify(intersect(curr, targetSpace))
debug.println(s"covered: $covered")

// `covered == Empty` may happen for primitive types with auto-conversion
// see tests/patmat/reader.scala tests/patmat/byte.scala
if (covered == Empty) covered = curr

if (isSubspace(covered, prevs)) {
ctx.warning(MatchCaseUnreachable(), pat.pos)
}

// if last case is `_` and only matches `null`, produce a warning
if (i == cases.length - 1 && !isNull(pat) ) {
simplify(minus(covered, prevs)) match {
case Typ(`nullType`, _) =>
ctx.warning(MatchCaseOnlyNullWarning(), pat.pos)
case _ =>
}

}
}
}
}
Expand Down
1 change: 0 additions & 1 deletion tests/patmat/andtype-opentype-interaction.check
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,5 @@
27: Pattern Match Exhaustivity: _: SealedAbstractClass & OpenTrait & OpenTrait2, _: SealedClass & OpenTrait & OpenTrait2, _: SealedTrait & OpenTrait & OpenTrait2, _: AbstractClass & OpenTrait & OpenTrait2, _: Clazz & OpenTrait & OpenTrait2, _: Trait & OpenTrait & OpenTrait2
31: Pattern Match Exhaustivity: _: SealedTrait & OpenClass, _: Trait & OpenClass
35: Pattern Match Exhaustivity: _: SealedTrait & OpenTrait & OpenClass, _: Trait & OpenTrait & OpenClass
40: Match case Unreachable
43: Pattern Match Exhaustivity: _: SealedTrait & OpenAbstractClass, _: Trait & OpenAbstractClass
47: Pattern Match Exhaustivity: _: SealedTrait & OpenClass & OpenTrait & OpenClassSubclass, _: Trait & OpenClass & OpenTrait & OpenClassSubclass
3 changes: 0 additions & 3 deletions tests/patmat/andtype-refinedtype-interaction.check
Original file line number Diff line number Diff line change
@@ -1,9 +1,6 @@
32: Pattern Match Exhaustivity: _: Trait & C1{x: Int}
37: Match case Unreachable
43: Match case Unreachable
48: Pattern Match Exhaustivity: _: Clazz & (C1 | C2 | T1){x: Int} & (C3 | C4 | T2){x: Int}, _: Trait & (C1 | C2 | T1){x: Int} & (C3 | C4 | T2){x: Int}
54: Pattern Match Exhaustivity: _: Trait & (C1 | C2 | T1){x: Int} & C3{x: Int}
60: Match case Unreachable
65: Pattern Match Exhaustivity: _: Trait & (C1 | C2){x: Int} & (C3 | SubC1){x: Int}
72: Pattern Match Exhaustivity: _: Trait & (T1 & (C1 | SubC2)){x: Int} & (T2 & (C2 | C3 | SubC1)){x: Int} &
SubSubC1{x: Int}
Expand Down
1 change: 1 addition & 0 deletions tests/patmat/byte.check
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
5: Match case Unreachable
8 changes: 8 additions & 0 deletions tests/patmat/byte.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
class Test {
def foo(x: Byte) = x match {
case 23 =>
case 33 =>
case 33 =>
case _ =>
}
}
15 changes: 15 additions & 0 deletions tests/patmat/file.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
abstract class AbstractFile
class PlainFile(path: String) extends AbstractFile
class VirtualFile(name: String) extends AbstractFile
abstract class ZipArchive(path: String) extends AbstractFile {
sealed abstract class Entry(name: String) extends VirtualFile(name)
class DirEntry(path: String) extends Entry(path)
}

object Test {
def foo(file: AbstractFile) = file match {
case ze: ZipArchive#Entry =>
case pf: PlainFile =>
case _ =>
}
}
2 changes: 0 additions & 2 deletions tests/patmat/i2253.check
Original file line number Diff line number Diff line change
@@ -1,5 +1,3 @@
28: Pattern Match Exhaustivity: HasIntXIntM, HasIntXStringM
29: Pattern Match Exhaustivity: HasIntXIntM
29: Match case Unreachable
30: Pattern Match Exhaustivity: HasIntXIntM
30: Match case Unreachable
1 change: 1 addition & 0 deletions tests/patmat/i4225.check
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
10: Match case Unreachable
12 changes: 12 additions & 0 deletions tests/patmat/i4225.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
object Bar {
def unapply(x: Int): Some[Int] =
Some(0)
}

object Test {
def test(x: Int) =
x match {
case Bar(a) => a
case _ => x // should be unreachable
}
}
1 change: 1 addition & 0 deletions tests/patmat/i4225b.check
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
10: Only null matched
Loading