Skip to content

Commit 60dd2ad

Browse files
authored
Merge pull request #11716 from dotty-staging/fix-11572
Use initialization checker for soundness
2 parents 31f3b16 + ad1aac0 commit 60dd2ad

File tree

11 files changed

+127
-30
lines changed

11 files changed

+127
-30
lines changed

compiler/src/dotty/tools/dotc/transform/init/Checking.scala

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -326,14 +326,14 @@ object Checking {
326326

327327
case Fun(pots, effs) =>
328328
val name = sym.name.toString
329-
if (name == "apply") Summary(pots, Effects.empty)
330-
else if (name == "tupled") Summary(Set(pot1), Effects.empty)
329+
if (name == "apply") Summary(pots)
330+
else if (name == "tupled") Summary(pot1)
331331
else if (name == "curried") {
332332
val arity = defn.functionArity(sym.info.finalResultType)
333-
val pots = (1 until arity).foldLeft(Set(pot1)) { (acc, i) =>
334-
Set(Fun(acc, Effects.empty)(pot1.source))
333+
val pots = (1 until arity).foldLeft(Vector(pot1)) { (acc, i) =>
334+
Vector(Fun(acc, Effects.empty)(pot1.source))
335335
}
336-
Summary(pots, Effects.empty)
336+
Summary(pots)
337337
}
338338
else Summary.empty
339339

compiler/src/dotty/tools/dotc/transform/init/Effects.scala

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -12,8 +12,8 @@ import core.Contexts._
1212
import Potentials._
1313

1414
object Effects {
15-
type Effects = Set[Effect]
16-
val empty: Effects = Set.empty
15+
type Effects = Vector[Effect]
16+
val empty: Effects = Vector.empty
1717

1818
def show(effs: Effects)(using Context): String =
1919
effs.map(_.show).mkString(", ")
@@ -25,13 +25,15 @@ object Effects {
2525
def show(using Context): String
2626

2727
def source: Tree
28+
29+
def toEffs: Effects = Vector(this)
2830
}
2931

30-
/** An effect means that a value that's possibly under initialization
32+
/** A promotion effect means that a value that's possibly under initialization
3133
* is promoted from the initializing world to the fully-initialized world.
3234
*
3335
* Essentially, this effect enforces that the object pointed to by
34-
* `potential` is fully initialized.
36+
* `potential` is transitively initialized.
3537
*
3638
* This effect is trigger in several scenarios:
3739
* - a potential is used as arguments to method calls or new-expressions
@@ -58,8 +60,6 @@ object Effects {
5860

5961
// ------------------ operations on effects ------------------
6062

61-
extension (eff: Effect) def toEffs: Effects = Effects.empty + eff
62-
6363
def asSeenFrom(eff: Effect, thisValue: Potential)(implicit env: Env): Effect =
6464
trace(eff.show + " asSeenFrom " + thisValue.show + ", current = " + currentClass.show, init, _.asInstanceOf[Effect].show) { eff match {
6565
case Promote(pot) =>

compiler/src/dotty/tools/dotc/transform/init/Potentials.scala

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -15,8 +15,8 @@ import Types._, Symbols._, Contexts._
1515
import Effects._, Summary._
1616

1717
object Potentials {
18-
type Potentials = Set[Potential]
19-
val empty: Potentials = Set.empty
18+
type Potentials = Vector[Potential]
19+
val empty: Potentials = Vector.empty
2020

2121
def show(pots: Potentials)(using Context): String =
2222
pots.map(_.show).mkString(", ")
@@ -31,6 +31,8 @@ object Potentials {
3131

3232
def show(using Context): String
3333
def source: Tree
34+
35+
def toPots: Potentials = Vector(this)
3436
}
3537

3638
sealed trait Refinable extends Potential {
@@ -153,8 +155,6 @@ object Potentials {
153155

154156
// ------------------ operations on potentials ------------------
155157

156-
extension (pot: Potential) def toPots: Potentials = Potentials.empty + pot
157-
158158
/** Selection on a set of potentials
159159
*
160160
* @param ignoreSelectEffect Where selection effects should be ignored

compiler/src/dotty/tools/dotc/transform/init/Summarization.scala

Lines changed: 26 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -107,7 +107,7 @@ object Summarization {
107107

108108
case Typed(expr, tpt) =>
109109
if (tpt.tpe.hasAnnotation(defn.UncheckedAnnot)) Summary.empty
110-
else analyze(expr)
110+
else analyze(expr) ++ effectsOfType(tpt.tpe, tpt)
111111

112112
case NamedArg(name, arg) =>
113113
analyze(arg)
@@ -140,7 +140,7 @@ object Summarization {
140140
val Summary(pots, effs) = analyze(selector)
141141
val init = Summary(Potentials.empty, pots.promote(selector) ++ effs)
142142
cases.foldLeft(init) { (acc, cas) =>
143-
acc union analyze(cas.body)
143+
acc + analyze(cas.body)
144144
}
145145

146146
// case CaseDef(pat, guard, body) =>
@@ -162,7 +162,7 @@ object Summarization {
162162

163163
case Try(block, cases, finalizer) =>
164164
val Summary(pots, effs) = cases.foldLeft(analyze(block)) { (acc, cas) =>
165-
acc union analyze(cas.body)
165+
acc + analyze(cas.body)
166166
}
167167
val Summary(_, eff2) = if (finalizer.isEmpty) Summary.empty else analyze(finalizer)
168168
Summary(pots, effs ++ eff2)
@@ -199,8 +199,9 @@ object Summarization {
199199
Summary(pots.promote(ddef) ++ effs)
200200
}
201201

202-
case _: TypeDef =>
203-
Summary.empty
202+
case tdef: TypeDef =>
203+
if tdef.isClassDef then Summary.empty
204+
else Summary(effectsOfType(tdef.symbol.info, tdef.rhs))
204205

205206
case _: Import | _: Export =>
206207
Summary.empty
@@ -213,6 +214,19 @@ object Summarization {
213214
else summary
214215
}
215216

217+
private def effectsOfType(tp: Type, source: Tree)(implicit env: Env): Effects =
218+
var summary = Summary.empty
219+
val traverser = new TypeTraverser {
220+
def traverse(tp: Type): Unit = tp match {
221+
case TermRef(_: SingletonType, _) =>
222+
summary = summary + analyze(tp, source)
223+
case _ =>
224+
traverseChildren(tp)
225+
}
226+
}
227+
traverser.traverse(tp)
228+
summary.effs
229+
216230
def analyze(tp: Type, source: Tree)(implicit env: Env): Summary =
217231
trace("summarizing " + tp.show, init, s => s.asInstanceOf[Summary].show) {
218232
val summary: Summary = tp match {
@@ -243,8 +257,12 @@ object Summarization {
243257
}
244258
Summary(pots2, effs)
245259

260+
case _: TermParamRef | _: RecThis =>
261+
// possible from checking effects of types
262+
Summary.empty
263+
246264
case _ =>
247-
throw new Exception("unexpected type: " + tp.show)
265+
throw new Exception("unexpected type: " + tp)
248266
}
249267

250268
if (env.isAlwaysInitialized(tp)) Summary(Potentials.empty, summary.effs)
@@ -290,7 +308,7 @@ object Summarization {
290308
def parentArgEffsWithInit(stats: List[Tree], ctor: Symbol, source: Tree): Effects =
291309
val init =
292310
if env.canIgnoreMethod(ctor) then Effects.empty
293-
else Effects.empty + MethodCall(ThisRef()(source), ctor)(source)
311+
else Effects.empty :+ MethodCall(ThisRef()(source), ctor)(source)
294312
stats.foldLeft(init) { (acc, stat) =>
295313
val summary = Summarization.analyze(stat)
296314
acc ++ summary.effs
@@ -320,7 +338,7 @@ object Summarization {
320338
if tref.prefix == NoPrefix then Effects.empty
321339
else Summarization.analyze(tref.prefix, ref).effs
322340

323-
prefixEff + MethodCall(ThisRef()(ref), ctor)(ref)
341+
prefixEff :+ MethodCall(ThisRef()(ref), ctor)(ref)
324342
}
325343
})
326344
}

compiler/src/dotty/tools/dotc/transform/init/Summary.scala

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -14,14 +14,14 @@ import config.Printers.init
1414
import Potentials._, Effects._, Util._
1515

1616
case class Summary(pots: Potentials, effs: Effects) {
17-
def union(summary2: Summary): Summary =
17+
def +(summary2: Summary): Summary =
1818
Summary(pots ++ summary2.pots, this.effs ++ summary2.effs)
1919

2020
def +(pot: Potential): Summary =
21-
Summary(pots + pot, effs)
21+
Summary(pots :+ pot, effs)
2222

2323
def +(eff: Effect): Summary =
24-
Summary(pots, effs + eff)
24+
Summary(pots, effs :+ eff)
2525

2626
def dropPotentials: Summary =
2727
Summary(Potentials.empty, effs)
@@ -44,14 +44,14 @@ case class Summary(pots: Potentials, effs: Effects) {
4444
object Summary {
4545
val empty: Summary = Summary(Potentials.empty, Effects.empty)
4646

47-
def apply(pots: Potentials): Summary = new Summary(pots, Effects.empty)
47+
def apply(pots: Potentials): Summary = empty ++ pots
4848

4949
@targetName("withEffects")
50-
def apply(effs: Effects): Summary = new Summary(Potentials.empty, effs)
50+
def apply(effs: Effects): Summary = empty ++ effs
5151

52-
def apply(pot: Potential): Summary = new Summary(Potentials.empty + pot, Effects.empty)
52+
def apply(pot: Potential): Summary = empty + pot
5353

54-
def apply(eff: Effect): Summary = new Summary(Potentials.empty, Effects.empty + eff)
54+
def apply(eff: Effect): Summary = empty + eff
5555
}
5656

5757
/** Summary of class.

tests/init/neg/i11572.scala

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
class A {
2+
trait Cov[+X] {
3+
def get: X
4+
}
5+
trait Bounded {
6+
type T >: Cov[Int] <: Cov[String]
7+
}
8+
val t: Bounded = new Bounded { // error
9+
// Note: using this instead of t produces an error (as expected)
10+
override type T >: t.T <: t.T
11+
}
12+
13+
val covInt = new Cov[Int] {
14+
override def get: Int = 3
15+
}
16+
val str: String = ((covInt: t.T): Cov[String]).get // ClassCastException: class Integer cannot be cast to class String
17+
}

tests/init/neg/i4031.scala

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
object App {
2+
trait A { type L >: Any}
3+
def upcast(a: A, x: Any): a.L = x
4+
val p: A { type L <: Nothing } = p // error
5+
def coerce(x: Any): Int = upcast(p, x)
6+
7+
def main(args: Array[String]): Unit = {
8+
println(coerce("Uh oh!"))
9+
}
10+
}

tests/init/neg/i4042.scala

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
object App {
2+
def coerce[U, V](u: U): V = {
3+
trait X { type R >: U }
4+
trait Y { type R = V }
5+
6+
class T[A <: X](val a: A)(val value: a.R)
7+
8+
object O { val x : Y & X = x } // error
9+
10+
val a = new T[Y & X](O.x)(u)
11+
a.value
12+
}
13+
14+
def main(args: Array[String]): Unit = {
15+
val x: Int = coerce[String, Int]("a")
16+
println(x + 1)
17+
}
18+
}

tests/init/neg/i50.scala

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
class C[T] {
2+
val a: T = method
3+
def method = b
4+
val b: T = a // error
5+
}

tests/init/neg/i5854.scala

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
class B {
2+
val a: String = (((1: Any): b.A): Nothing): String
3+
val b: { type A >: Any <: Nothing } = loop() // error
4+
def loop(): Nothing = loop()
5+
}

tests/neg-strict/i5854.scala

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
object bar {
2+
trait Sub {
3+
type M
4+
type L <: M
5+
type U >: M
6+
type M2 >: L <: U
7+
}
8+
class Box[V](val v: V)
9+
10+
class Caster[LL, UU] {
11+
trait S2 {
12+
type L = LL
13+
type U = UU
14+
}
15+
final lazy val nothing: Nothing = nothing
16+
final lazy val sub: S2 & Sub = nothing
17+
final lazy val box : Box[S2 & Sub] = new Box(nothing)
18+
def upcast(t: box.v.M2): box.v.M2 = t // error // error
19+
}
20+
def main(args : Array[String]) : Unit = {
21+
val zero : String = (new Caster[Int,String]()).upcast(0)
22+
println("...")
23+
}
24+
}

0 commit comments

Comments
 (0)