From 07a2e41bbc398754b760ba6bee984d340d0f53c7 Mon Sep 17 00:00:00 2001 From: Liu Fengyun Date: Fri, 12 Mar 2021 13:58:40 +0100 Subject: [PATCH 1/7] WIP: Use initialization checker for soundness -- Warning: tests/init/neg/i11572.scala:8:6 ------------------------------------ 8 | val t: Bounded = new Bounded { | ^ | Access non-initialized value t. Calling trace: | -> } [ i11572.scala:11 ] | -> override type T >: t.T <: t.T [ i11572.scala:10 ] 1 warning found --- .../dotc/transform/init/Summarization.scala | 22 +++++++++++++++---- .../tools/dotc/transform/init/Summary.scala | 2 +- tests/init/neg/i11572.scala | 17 ++++++++++++++ 3 files changed, 36 insertions(+), 5 deletions(-) create mode 100644 tests/init/neg/i11572.scala diff --git a/compiler/src/dotty/tools/dotc/transform/init/Summarization.scala b/compiler/src/dotty/tools/dotc/transform/init/Summarization.scala index 8df4cb7f558d..5c9644c82ccd 100644 --- a/compiler/src/dotty/tools/dotc/transform/init/Summarization.scala +++ b/compiler/src/dotty/tools/dotc/transform/init/Summarization.scala @@ -140,7 +140,7 @@ object Summarization { val Summary(pots, effs) = analyze(selector) val init = Summary(Potentials.empty, pots.promote(selector) ++ effs) cases.foldLeft(init) { (acc, cas) => - acc union analyze(cas.body) + acc + analyze(cas.body) } // case CaseDef(pat, guard, body) => @@ -162,7 +162,7 @@ object Summarization { case Try(block, cases, finalizer) => val Summary(pots, effs) = cases.foldLeft(analyze(block)) { (acc, cas) => - acc union analyze(cas.body) + acc + analyze(cas.body) } val Summary(_, eff2) = if (finalizer.isEmpty) Summary.empty else analyze(finalizer) Summary(pots, effs ++ eff2) @@ -199,8 +199,22 @@ object Summarization { Summary(pots.promote(ddef) ++ effs) } - case _: TypeDef => - Summary.empty + case tdef: TypeDef => + if tdef.isClassDef then Summary.empty + else { + var summary = Summary.empty + val tp = tdef.symbol.info + val traverser = new TypeTraverser { + def traverse(tp: Type): Unit = tp match { + case tp: TermRef => + summary = summary + analyze(tp, tdef.rhs) + case _ => + traverseChildren(tp) + } + } + traverser.traverse(tp) + summary + } case _: Import | _: Export => Summary.empty diff --git a/compiler/src/dotty/tools/dotc/transform/init/Summary.scala b/compiler/src/dotty/tools/dotc/transform/init/Summary.scala index d4b72d4c0214..d0d12d0486a7 100644 --- a/compiler/src/dotty/tools/dotc/transform/init/Summary.scala +++ b/compiler/src/dotty/tools/dotc/transform/init/Summary.scala @@ -14,7 +14,7 @@ import config.Printers.init import Potentials._, Effects._, Util._ case class Summary(pots: Potentials, effs: Effects) { - def union(summary2: Summary): Summary = + def +(summary2: Summary): Summary = Summary(pots ++ summary2.pots, this.effs ++ summary2.effs) def +(pot: Potential): Summary = diff --git a/tests/init/neg/i11572.scala b/tests/init/neg/i11572.scala new file mode 100644 index 000000000000..c2ebe6fe47f9 --- /dev/null +++ b/tests/init/neg/i11572.scala @@ -0,0 +1,17 @@ +class A { + trait Cov[+X] { + def get: X + } + trait Bounded { + type T >: Cov[Int] <: Cov[String] + } + val t: Bounded = new Bounded { // error + // Note: using this instead of t produces an error (as expected) + override type T >: t.T <: t.T + } + + val covInt = new Cov[Int] { + override def get: Int = 3 + } + val str: String = ((covInt: t.T): Cov[String]).get // ClassCastException: class Integer cannot be cast to class String +} From 2cefd3e404ae8eea831518fb64317b103230d762 Mon Sep 17 00:00:00 2001 From: Liu Fengyun Date: Fri, 12 Mar 2021 15:40:00 +0100 Subject: [PATCH 2/7] Performance tweak: use vector for effects and potentials --- .../dotty/tools/dotc/transform/init/Checking.scala | 10 +++++----- .../dotty/tools/dotc/transform/init/Effects.scala | 8 ++++---- .../dotty/tools/dotc/transform/init/Potentials.scala | 8 ++++---- .../tools/dotc/transform/init/Summarization.scala | 4 ++-- .../dotty/tools/dotc/transform/init/Summary.scala | 12 ++++++------ 5 files changed, 21 insertions(+), 21 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/transform/init/Checking.scala b/compiler/src/dotty/tools/dotc/transform/init/Checking.scala index 85217501d55f..e47c3b08d264 100644 --- a/compiler/src/dotty/tools/dotc/transform/init/Checking.scala +++ b/compiler/src/dotty/tools/dotc/transform/init/Checking.scala @@ -326,14 +326,14 @@ object Checking { case Fun(pots, effs) => val name = sym.name.toString - if (name == "apply") Summary(pots, Effects.empty) - else if (name == "tupled") Summary(Set(pot1), Effects.empty) + if (name == "apply") Summary(pots) + else if (name == "tupled") Summary(pot1) else if (name == "curried") { val arity = defn.functionArity(sym.info.finalResultType) - val pots = (1 until arity).foldLeft(Set(pot1)) { (acc, i) => - Set(Fun(acc, Effects.empty)(pot1.source)) + val pots = (1 until arity).foldLeft(Vector(pot1)) { (acc, i) => + Vector(Fun(acc, Effects.empty)(pot1.source)) } - Summary(pots, Effects.empty) + Summary(pots) } else Summary.empty diff --git a/compiler/src/dotty/tools/dotc/transform/init/Effects.scala b/compiler/src/dotty/tools/dotc/transform/init/Effects.scala index 9486263a8af0..41cf873c809b 100644 --- a/compiler/src/dotty/tools/dotc/transform/init/Effects.scala +++ b/compiler/src/dotty/tools/dotc/transform/init/Effects.scala @@ -12,8 +12,8 @@ import core.Contexts._ import Potentials._ object Effects { - type Effects = Set[Effect] - val empty: Effects = Set.empty + type Effects = Vector[Effect] + val empty: Effects = Vector.empty def show(effs: Effects)(using Context): String = effs.map(_.show).mkString(", ") @@ -25,6 +25,8 @@ object Effects { def show(using Context): String def source: Tree + + def toEffs: Effects = Vector(this) } /** An effect means that a value that's possibly under initialization @@ -58,8 +60,6 @@ object Effects { // ------------------ operations on effects ------------------ - extension (eff: Effect) def toEffs: Effects = Effects.empty + eff - def asSeenFrom(eff: Effect, thisValue: Potential)(implicit env: Env): Effect = trace(eff.show + " asSeenFrom " + thisValue.show + ", current = " + currentClass.show, init, _.asInstanceOf[Effect].show) { eff match { case Promote(pot) => diff --git a/compiler/src/dotty/tools/dotc/transform/init/Potentials.scala b/compiler/src/dotty/tools/dotc/transform/init/Potentials.scala index a7b409b56d5e..39eac29a2741 100644 --- a/compiler/src/dotty/tools/dotc/transform/init/Potentials.scala +++ b/compiler/src/dotty/tools/dotc/transform/init/Potentials.scala @@ -15,8 +15,8 @@ import Types._, Symbols._, Contexts._ import Effects._, Summary._ object Potentials { - type Potentials = Set[Potential] - val empty: Potentials = Set.empty + type Potentials = Vector[Potential] + val empty: Potentials = Vector.empty def show(pots: Potentials)(using Context): String = pots.map(_.show).mkString(", ") @@ -31,6 +31,8 @@ object Potentials { def show(using Context): String def source: Tree + + def toPots: Potentials = Vector(this) } sealed trait Refinable extends Potential { @@ -153,8 +155,6 @@ object Potentials { // ------------------ operations on potentials ------------------ - extension (pot: Potential) def toPots: Potentials = Potentials.empty + pot - /** Selection on a set of potentials * * @param ignoreSelectEffect Where selection effects should be ignored diff --git a/compiler/src/dotty/tools/dotc/transform/init/Summarization.scala b/compiler/src/dotty/tools/dotc/transform/init/Summarization.scala index 5c9644c82ccd..d6d602488257 100644 --- a/compiler/src/dotty/tools/dotc/transform/init/Summarization.scala +++ b/compiler/src/dotty/tools/dotc/transform/init/Summarization.scala @@ -304,7 +304,7 @@ object Summarization { def parentArgEffsWithInit(stats: List[Tree], ctor: Symbol, source: Tree): Effects = val init = if env.canIgnoreMethod(ctor) then Effects.empty - else Effects.empty + MethodCall(ThisRef()(source), ctor)(source) + else Effects.empty :+ MethodCall(ThisRef()(source), ctor)(source) stats.foldLeft(init) { (acc, stat) => val summary = Summarization.analyze(stat) acc ++ summary.effs @@ -334,7 +334,7 @@ object Summarization { if tref.prefix == NoPrefix then Effects.empty else Summarization.analyze(tref.prefix, ref).effs - prefixEff + MethodCall(ThisRef()(ref), ctor)(ref) + prefixEff :+ MethodCall(ThisRef()(ref), ctor)(ref) } }) } diff --git a/compiler/src/dotty/tools/dotc/transform/init/Summary.scala b/compiler/src/dotty/tools/dotc/transform/init/Summary.scala index d0d12d0486a7..1c7a852d4847 100644 --- a/compiler/src/dotty/tools/dotc/transform/init/Summary.scala +++ b/compiler/src/dotty/tools/dotc/transform/init/Summary.scala @@ -18,10 +18,10 @@ case class Summary(pots: Potentials, effs: Effects) { Summary(pots ++ summary2.pots, this.effs ++ summary2.effs) def +(pot: Potential): Summary = - Summary(pots + pot, effs) + Summary(pots :+ pot, effs) def +(eff: Effect): Summary = - Summary(pots, effs + eff) + Summary(pots, effs :+ eff) def dropPotentials: Summary = Summary(Potentials.empty, effs) @@ -44,14 +44,14 @@ case class Summary(pots: Potentials, effs: Effects) { object Summary { val empty: Summary = Summary(Potentials.empty, Effects.empty) - def apply(pots: Potentials): Summary = new Summary(pots, Effects.empty) + def apply(pots: Potentials): Summary = empty ++ pots @targetName("withEffects") - def apply(effs: Effects): Summary = new Summary(Potentials.empty, effs) + def apply(effs: Effects): Summary = empty ++ effs - def apply(pot: Potential): Summary = new Summary(Potentials.empty + pot, Effects.empty) + def apply(pot: Potential): Summary = empty + pot - def apply(eff: Effect): Summary = new Summary(Potentials.empty, Effects.empty + eff) + def apply(eff: Effect): Summary = empty + eff } /** Summary of class. From aaffb1198636a31f7cf125b09e1df10d8d8cba45 Mon Sep 17 00:00:00 2001 From: Liu Fengyun Date: Fri, 12 Mar 2021 16:23:57 +0100 Subject: [PATCH 3/7] Handle types that appear in effpi We get types like the following in effpi: effpi.examples.demo.audit.types.Pay#replyTo --- .../dotty/tools/dotc/transform/init/Summarization.scala | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/transform/init/Summarization.scala b/compiler/src/dotty/tools/dotc/transform/init/Summarization.scala index d6d602488257..0bc433b3381d 100644 --- a/compiler/src/dotty/tools/dotc/transform/init/Summarization.scala +++ b/compiler/src/dotty/tools/dotc/transform/init/Summarization.scala @@ -206,7 +206,7 @@ object Summarization { val tp = tdef.symbol.info val traverser = new TypeTraverser { def traverse(tp: Type): Unit = tp match { - case tp: TermRef => + case TermRef(_: SingletonType, _) => summary = summary + analyze(tp, tdef.rhs) case _ => traverseChildren(tp) @@ -257,8 +257,12 @@ object Summarization { } Summary(pots2, effs) + case _: TermParamRef => + // possible from type definitions + Summary.empty + case _ => - throw new Exception("unexpected type: " + tp.show) + throw new Exception("unexpected type: " + tp) } if (env.isAlwaysInitialized(tp)) Summary(Potentials.empty, summary.effs) From fe38137c99b361aeae8e632fb963ed463f4fe525 Mon Sep 17 00:00:00 2001 From: Liu Fengyun Date: Fri, 12 Mar 2021 19:46:44 +0100 Subject: [PATCH 4/7] Refine documentation --- compiler/src/dotty/tools/dotc/transform/init/Effects.scala | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/transform/init/Effects.scala b/compiler/src/dotty/tools/dotc/transform/init/Effects.scala index 41cf873c809b..ce9d8d8aa497 100644 --- a/compiler/src/dotty/tools/dotc/transform/init/Effects.scala +++ b/compiler/src/dotty/tools/dotc/transform/init/Effects.scala @@ -29,11 +29,11 @@ object Effects { def toEffs: Effects = Vector(this) } - /** An effect means that a value that's possibly under initialization + /** A promotion effect means that a value that's possibly under initialization * is promoted from the initializing world to the fully-initialized world. * * Essentially, this effect enforces that the object pointed to by - * `potential` is fully initialized. + * `potential` is transitively initialized. * * This effect is trigger in several scenarios: * - a potential is used as arguments to method calls or new-expressions From 74bcfd7263b4a8708a199ebb5e342e6e4b2d92ca Mon Sep 17 00:00:00 2001 From: Liu Fengyun Date: Fri, 12 Mar 2021 21:35:34 +0100 Subject: [PATCH 5/7] Fix #5854: check type annotations for soundness --- .../dotc/transform/init/Summarization.scala | 34 +++++++++---------- tests/init/neg/i5854.scala | 5 +++ tests/neg-strict/i5854.scala | 24 +++++++++++++ 3 files changed, 46 insertions(+), 17 deletions(-) create mode 100644 tests/init/neg/i5854.scala create mode 100644 tests/neg-strict/i5854.scala diff --git a/compiler/src/dotty/tools/dotc/transform/init/Summarization.scala b/compiler/src/dotty/tools/dotc/transform/init/Summarization.scala index 0bc433b3381d..8da415bf82bb 100644 --- a/compiler/src/dotty/tools/dotc/transform/init/Summarization.scala +++ b/compiler/src/dotty/tools/dotc/transform/init/Summarization.scala @@ -107,7 +107,7 @@ object Summarization { case Typed(expr, tpt) => if (tpt.tpe.hasAnnotation(defn.UncheckedAnnot)) Summary.empty - else analyze(expr) + else analyze(expr) ++ effectsOfType(tpt.tpe, tpt) case NamedArg(name, arg) => analyze(arg) @@ -201,20 +201,7 @@ object Summarization { case tdef: TypeDef => if tdef.isClassDef then Summary.empty - else { - var summary = Summary.empty - val tp = tdef.symbol.info - val traverser = new TypeTraverser { - def traverse(tp: Type): Unit = tp match { - case TermRef(_: SingletonType, _) => - summary = summary + analyze(tp, tdef.rhs) - case _ => - traverseChildren(tp) - } - } - traverser.traverse(tp) - summary - } + else Summary(effectsOfType(tdef.symbol.info, tdef.rhs)) case _: Import | _: Export => Summary.empty @@ -227,6 +214,19 @@ object Summarization { else summary } + private def effectsOfType(tp: Type, source: Tree)(implicit env: Env): Effects = + var summary = Summary.empty + val traverser = new TypeTraverser { + def traverse(tp: Type): Unit = tp match { + case TermRef(_: SingletonType, _) => + summary = summary + analyze(tp, source) + case _ => + traverseChildren(tp) + } + } + traverser.traverse(tp) + summary.effs + def analyze(tp: Type, source: Tree)(implicit env: Env): Summary = trace("summarizing " + tp.show, init, s => s.asInstanceOf[Summary].show) { val summary: Summary = tp match { @@ -257,8 +257,8 @@ object Summarization { } Summary(pots2, effs) - case _: TermParamRef => - // possible from type definitions + case _: TermParamRef | _: RecThis => + // possible from checking effects of types Summary.empty case _ => diff --git a/tests/init/neg/i5854.scala b/tests/init/neg/i5854.scala new file mode 100644 index 000000000000..a52685f63be2 --- /dev/null +++ b/tests/init/neg/i5854.scala @@ -0,0 +1,5 @@ +class B { + val a: String = (((1: Any): b.A): Nothing): String + val b: { type A >: Any <: Nothing } = loop() // error + def loop(): Nothing = loop() +} diff --git a/tests/neg-strict/i5854.scala b/tests/neg-strict/i5854.scala new file mode 100644 index 000000000000..e8c68105bbae --- /dev/null +++ b/tests/neg-strict/i5854.scala @@ -0,0 +1,24 @@ +object bar { + trait Sub { + type M + type L <: M + type U >: M + type M2 >: L <: U + } + class Box[V](val v: V) + + class Caster[LL, UU] { + trait S2 { + type L = LL + type U = UU + } + final lazy val nothing: Nothing = nothing + final lazy val sub: S2 & Sub = nothing + final lazy val box : Box[S2 & Sub] = new Box(nothing) + def upcast(t: box.v.M2): box.v.M2 = t // error // error + } + def main(args : Array[String]) : Unit = { + val zero : String = (new Caster[Int,String]()).upcast(0) + println("...") + } +} \ No newline at end of file From d28f1475af048c1e729f4deb1484b78ff8e7649c Mon Sep 17 00:00:00 2001 From: Liu Fengyun Date: Wed, 17 Mar 2021 15:50:01 +0100 Subject: [PATCH 6/7] Add test case --- tests/init/neg/i4031.scala | 10 ++++++++++ tests/init/neg/i50.scala | 5 +++++ 2 files changed, 15 insertions(+) create mode 100644 tests/init/neg/i4031.scala create mode 100644 tests/init/neg/i50.scala diff --git a/tests/init/neg/i4031.scala b/tests/init/neg/i4031.scala new file mode 100644 index 000000000000..8340296340e7 --- /dev/null +++ b/tests/init/neg/i4031.scala @@ -0,0 +1,10 @@ +object App { + trait A { type L >: Any} + def upcast(a: A, x: Any): a.L = x + val p: A { type L <: Nothing } = p // error + def coerce(x: Any): Int = upcast(p, x) + + def main(args: Array[String]): Unit = { + println(coerce("Uh oh!")) + } +} diff --git a/tests/init/neg/i50.scala b/tests/init/neg/i50.scala new file mode 100644 index 000000000000..9131fb263f48 --- /dev/null +++ b/tests/init/neg/i50.scala @@ -0,0 +1,5 @@ +class C[T] { + val a: T = method + def method = b + val b: T = a // error +} \ No newline at end of file From ad1aac006c13f437b2941b63cf3fa42cbde4f5a6 Mon Sep 17 00:00:00 2001 From: Liu Fengyun Date: Wed, 17 Mar 2021 15:58:02 +0100 Subject: [PATCH 7/7] Fix #4042: add test --- tests/init/neg/i4042.scala | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) create mode 100644 tests/init/neg/i4042.scala diff --git a/tests/init/neg/i4042.scala b/tests/init/neg/i4042.scala new file mode 100644 index 000000000000..58c884a5690d --- /dev/null +++ b/tests/init/neg/i4042.scala @@ -0,0 +1,18 @@ +object App { + def coerce[U, V](u: U): V = { + trait X { type R >: U } + trait Y { type R = V } + + class T[A <: X](val a: A)(val value: a.R) + + object O { val x : Y & X = x } // error + + val a = new T[Y & X](O.x)(u) + a.value + } + + def main(args: Array[String]): Unit = { + val x: Int = coerce[String, Int]("a") + println(x + 1) + } +}