Skip to content

Use initialization checker for soundness #11716

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 7 commits into from
Mar 17, 2021
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 5 additions & 5 deletions compiler/src/dotty/tools/dotc/transform/init/Checking.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
12 changes: 6 additions & 6 deletions compiler/src/dotty/tools/dotc/transform/init/Effects.scala
Original file line number Diff line number Diff line change
Expand Up @@ -12,8 +12,8 @@ import core.Contexts._
import Potentials._

object Effects {
type Effects = Set[Effect]
val empty: Effects = Set.empty
type Effects = Vector[Effect]
Copy link
Contributor

Choose a reason for hiding this comment

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

Is the change from Set to Vector related to checking TypeDefs, or is it an orthogonal improvement?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

It's orthogonal. Set is bad for concatenation, and we can afford to have duplicate entries in summaries.

val empty: Effects = Vector.empty

def show(effs: Effects)(using Context): String =
effs.map(_.show).mkString(", ")
Expand All @@ -25,13 +25,15 @@ 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
/** 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
Expand All @@ -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) =>
Expand Down
8 changes: 4 additions & 4 deletions compiler/src/dotty/tools/dotc/transform/init/Potentials.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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(", ")
Expand All @@ -31,6 +31,8 @@ object Potentials {

def show(using Context): String
def source: Tree

def toPots: Potentials = Vector(this)
}

sealed trait Refinable extends Potential {
Expand Down Expand Up @@ -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
Expand Down
34 changes: 26 additions & 8 deletions compiler/src/dotty/tools/dotc/transform/init/Summarization.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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) =>
Expand All @@ -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)
Expand Down Expand Up @@ -199,8 +199,9 @@ object Summarization {
Summary(pots.promote(ddef) ++ effs)
}

case _: TypeDef =>
Summary.empty
case tdef: TypeDef =>
if tdef.isClassDef then Summary.empty
else Summary(effectsOfType(tdef.symbol.info, tdef.rhs))

case _: Import | _: Export =>
Summary.empty
Expand All @@ -213,6 +214,19 @@ object Summarization {
else summary
}

private def effectsOfType(tp: Type, source: Tree)(implicit env: Env): Effects =
Copy link
Contributor

Choose a reason for hiding this comment

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

Is this function calculating the effects of constructing an instance of type tp?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

It's calculating field access effects in types. In Scala we can have types like p.f.T, here we summarize the effects for p.f.

var summary = Summary.empty
val traverser = new TypeTraverser {
def traverse(tp: Type): Unit = tp match {
case TermRef(_: SingletonType, _) =>
Copy link
Contributor

Choose a reason for hiding this comment

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

Why do we restrict to SingletonType here as a prefix of the TermRef?

What could the prefix be other than a SingletonType and why is it OK to skip those cases?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

In the community build, the project effpi (which use compiler plugin for session protocol checking) generates types like the following:

effpi.examples.demo.audit.types.Pay#replyTo

The type looks dubious, but the compiler seems to be fine with it. For such a type, our code will simply recur on the prefix effpi.examples.demo.audit.types.Pay and look for term selections recursively.

Copy link
Contributor

Choose a reason for hiding this comment

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

I'm still confused.

That type is a TypeRef, right? And we recurse on its prefix below in case _ => traverseChildren(tp), right? What would go wrong if this case was just case _: TermRef => instead of the pattern with the SingletonType?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I didn't make it clear: it's a display problem, it's a TermRef where the prefix is a TypeRef.

If we only have _: TermRef, we will need to do more error-handling in analyze(tp) to avoid crash: currently it's pretty strict about what types it may get.

Copy link
Contributor

Choose a reason for hiding this comment

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

Oh, sorry, yes, this makes sense now.

Then I just wonder why the restriction is for the prefix to be a SingletonType rather than the prefix being something like TermRef | NoPrefix. Can a SingletonType be more things than that and are those things that we want?

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, the prefix can also be ThisType, which is usually what we care about. If the prefix is NoPrefix, the variable is a local variable --- the analysis currently enforces that all local variables are hot.

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 {
Expand Down Expand Up @@ -243,8 +257,12 @@ object Summarization {
}
Summary(pots2, effs)

case _: TermParamRef | _: RecThis =>
// possible from checking effects of types
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)
Expand Down Expand Up @@ -290,7 +308,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
Expand Down Expand Up @@ -320,7 +338,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)
}
})
}
Expand Down
14 changes: 7 additions & 7 deletions compiler/src/dotty/tools/dotc/transform/init/Summary.scala
Original file line number Diff line number Diff line change
Expand Up @@ -14,14 +14,14 @@ 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 =
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)
Expand All @@ -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.
Expand Down
17 changes: 17 additions & 0 deletions tests/init/neg/i11572.scala
Original file line number Diff line number Diff line change
@@ -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
}
10 changes: 10 additions & 0 deletions tests/init/neg/i4031.scala
Original file line number Diff line number Diff line change
@@ -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!"))
}
}
18 changes: 18 additions & 0 deletions tests/init/neg/i4042.scala
Original file line number Diff line number Diff line change
@@ -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)
}
}
5 changes: 5 additions & 0 deletions tests/init/neg/i50.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
class C[T] {
val a: T = method
def method = b
val b: T = a // error
}
5 changes: 5 additions & 0 deletions tests/init/neg/i5854.scala
Original file line number Diff line number Diff line change
@@ -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()
}
24 changes: 24 additions & 0 deletions tests/neg-strict/i5854.scala
Original file line number Diff line number Diff line change
@@ -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("...")
}
}