A simpler implementation of init checker #12495

liufengyun · 2021-05-17T06:09:36Z

A simpler implementation of init checker

This version is based on the same insights as the previous version [1]. The analysis is written as an abstract definitional interpreter instead of a type-and-effect system. The new version is simpler, more regular, and enjoys better extensibility.

A type-and-effect system for object initialization, OOPSLA, 2020.

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

olhotak · 2021-05-18T20:13:25Z

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

@@ -57,7 +59,14 @@ class Checker extends MiniPhase {
        env = Env(ctx.withOwner(cls), cache)
      )

-      Checking.checkClassBody(tree)
+      // Checking.checkClassBody(tree)


Should we remove checkClassBody or is it too early? Also cache, summarization, etc.

Yes, we will remove the existing version in another PR.

olhotak · 2021-05-18T20:17:31Z

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

+      val tpl = tree.rhs.asInstanceOf[Template]
+      val thisRef = ThisRef(cls)
+      val heap = Objekt(cls, fields = mutable.Map.empty)
+      val res = eval(tpl, thisRef, cls)(using heap, ctx, Vector.empty)


We discussed that we could in theory call init here instead of eval. I there are tricky reasons to prefer eval, fine, but if not, then init would make the intent clearer.

Here the reason is only for consistency and tries to follow the Scala specification on initialization literally.
Inside the interpreter, beyond the cosmetical reason, another reason to reuse the cache infrastructure in early promotion of warm objects.

olhotak · 2021-05-18T20:26:07Z

tests/init/neg/early-promote.scala

@@ -24,7 +24,7 @@ class A { // checking A
    def c = new C
  }
  val b = new B()
-  List(b) // Direct promotion works here
+  List(b) // error: no promotion for objects that contain inner classes


Consider a comment to explain why that's not safe.

olhotak · 2021-05-18T20:27:13Z

tests/init/neg/features-doublelist.scala

@@ -1,6 +1,6 @@
 class DoubleList {
  class Node(var prev: Node, var next: Node, data: Int)
-  object sentinel extends Node(sentinel, sentinel, 0)
+  object sentinel extends Node(sentinel, sentinel, 0)  // error // error


Is this change related to this PR or to the global objects checker? Or point to inner-loop.scala.

According to concrete semantics, the code will run into loop.
The previous version ignores the effects in parent calls (assumimg they are hot, except super ctor calls).
The current version is more eager in check, thus report two warnings: Promote the value under initialization to fully-initialized. It's not related to the global object checker (which is not merged yet).

olhotak · 2021-05-18T20:40:48Z

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

+
+  /** Abstract values
+   *
+   * Value = Hot | Cold | Warm | ThisRef | Fun | RefSet


It would be nice to give the <= relation on the abstract domain here.

Good idea, I'll update the documentation.

olhotak · 2021-05-18T22:09:17Z

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

+
+    // parents
+    def initParent(parent: Tree) = parent match {
+      case tree @ Block(stats, NewExpr(tref, New(tpt), ctor, argss)) =>


I don't fully understand these cases of parent. Perhaps comment like // class A extends B(arg)

olhotak · 2021-05-18T22:11:15Z

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

+        case Some(parent) => initParent(parent)
+        case None =>
+          val tref = typeRefOf(klass.typeRef.baseType(mixin).typeConstructor)
+          val ctor = tref.classSymbol.primaryConstructor


Is the primary constructor always the one with zero args?

According to the language spec, if the mix trait requires arguments, then the class must provide arguments to it explicitly in the parent list. That means we will encounter it in the Some branch.

When a trait A extends a parameterized trait B, it cannot provide term arguments to B. That can only be done in a concrete class.

olhotak · 2021-05-18T22:16:34Z

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

+      case t: Tree      => t
+      case ByNameArg(t) => t
+
+  object Call {


Is there something like this extractor elsewhere in Dotty for general use? If not, should there be (should this be moved out of init where other code can use it)?

The logic here is specific to our analysis, thus it's better to keep it here. The handling of ByNameArg is also special to our purpose. In the compiler, we also do the same thing.

olhotak · 2021-05-18T22:18:43Z

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

+      // ignored as they are all hot
+
+      // follow constructor
+      if !cls.defTree.isEmpty then


Consider using hasSource instead of !defTree.isEmpty.

olhotak · 2021-05-18T22:21:17Z

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

+    else sym.matchingMember(cls.appliedRef)
+
+  def resolveSuper(cls: ClassSymbol, superType: Type, sym: Symbol)(using Context): Symbol = {
+    import annotation.tailrec


Is there something like this elsewhere in Dotty? Should there be?

There isn't anything similar, so I think it's better to keep it here -- also because they are two important helper methods in the logic of the analysis.

olhotak · 2021-05-20T15:20:08Z

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

+   *        │         │      │       │
+   *        └─────────┴──────┴───────┘
+   *                  Hot
+   */


I like the diagram but I think RefSet should be above ThisRef(C), Warm(D), and Fun (but below Cold).

Putting RefSet above ThisRef(C) is also problematic (it might not be a member). In the end, I added more text to explain the ordering with RefSet.

olhotak · 2021-05-20T15:22:02Z

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

+          Result(value2, errors)
+      }
+
+    def instantiate(klass: ClassSymbol, ctor: Symbol, source: Tree): Contextual[Result] =


OK, please add comment:
// call on prefix p of a new expression new p.C

EnzeXing · 2021-05-20T20:54:00Z

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

+          val value = Fun(ddef.rhs, obj, klass)
+          Result(value, Nil)
+        case _ =>
+          // The reason is that we never evaluate an expression if `thisV` is


Can you explain why we don't evaluate an expression when thisV is cold?

That's part of the design of the system -- when we call a method on a cold value, the system reports a warning. That's why this branch cannot be reached.

olhotak

This now LGTM. Ready to be merged.

liufengyun · 2021-05-21T15:56:17Z

This now LGTM. Ready to be merged.

Thanks @olhotak . I'll rebase and if it's green, let's merge. I'll make two following-up PRs

To remove the old checker and clean up docs
Refactor the domain to make it easier to implement escape to constructors without annotation (also implements caching of outers for warm)

This brings us closer to OOPSLA paper. The key insight to avoid cycles like the following ``` class A(b: B) { val b2 = new B(this) } class B(a: A) { val a2 = new A(this) } ``` is to use `Warm(C, outer)` to evaluate fields and methods of `C`. The evaluation results are cached uniformly. Therefore, there is no need to treat `Warm(C, outer)` as addresses.

tests/init/crash/explicitOuter.scala

liufengyun · 2021-05-21T17:20:55Z

The PR to remove the old init checker is #12561.

liufengyun changed the title ~~[WIP] A simpler implementation of init checker~~ A simpler implementation of init checker May 17, 2021

liufengyun marked this pull request as ready for review May 17, 2021 09:44

liufengyun commented May 17, 2021

View reviewed changes

compiler/src/dotty/tools/dotc/transform/init/Semantic.scala Outdated Show resolved Hide resolved

olhotak reviewed May 18, 2021

View reviewed changes

olhotak reviewed May 20, 2021

View reviewed changes

EnzeXing reviewed May 20, 2021

View reviewed changes

olhotak reviewed May 21, 2021

View reviewed changes

liufengyun added 22 commits May 21, 2021 17:56

Add Domain and Semantic

c8fe7e8

Add evaluator skeleton

006f714

Add concrete domain definitions

5373188

Define join

b31bbda

Implement this resolution

d955d26

Add utility extractors

b3ebab0

Handle Select node

ea7185f

Handle more expressions

021b58e

Handle method call

34e476a

Handle method call in abstract semantics

ab926d9

Don't thread-through heap thanks to monotonicity

21cfb0f

Refactor eval for list of expressions

237ceec

Implement case for new expressions

3058635

Handle instantiation in abstract semantics

a8c70d5

Initial implementation of object initialization

6c7f170

Refactor: use extension methods for heap operations

f8abf7e

Be faithful to initialization semantics

0a39a8f

First example works

4f298c0

Show stacktrace for errors

dd65e1a

Remove useless file

252f3e4

Only cache top-level expressions

fff6f48

liufengyun added 22 commits May 21, 2021 17:56

Implement promotion

3fccd63

Handle constructor call effects on warm objects

7717c5b

Refactor cache: don't use location as cache key

d3383f6

Add test

9831b97

Check term usage in types for type soundness

366c972

Support early promotion of warm objects

9960e5a

Handle by-name arguments

89a0845

Ignore known safe method calls

01fc3e6

Fix crash: impossible to construct super calls for leaked objects

390691e

Fix joining empty sequence of values

c6ea1a2

Fix crash: use the correct outer class

fa3d6ed

tests/init/crash/explicitOuter.scala

Reorganize tests

f4aa49b

Refactor: move heap from ThisRef for sharing more information

48f7b97

Handle cycles in early promotion

ee84531

Handle exception with super calls

d94d794

Handle package and static objects in this resolution

2f2253d

Handle poly functions

062bb98

Add test for structural types

a7af9d8

Fix test for poly functions

b978ad9

Remove unused field

3c25533

Address review

f67b3cd

Address review: Add more documentation

12bfbd2

liufengyun force-pushed the new-init branch from 2b2e98d to 12bfbd2 Compare May 21, 2021 15:57

liufengyun merged commit 450f8ac into scala:master May 21, 2021

liufengyun deleted the new-init branch May 21, 2021 17:18

liufengyun mentioned this pull request May 25, 2021

Testing unusable with -Ysafe-init #12128

Closed

griggt mentioned this pull request May 31, 2021

Fix #12128: Add test #12592

Merged

liufengyun mentioned this pull request May 31, 2021

Refactor heap and cache outers #12608

Merged

Kordyjan added this to the 3.0.1 milestone Aug 2, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

A simpler implementation of init checker #12495

A simpler implementation of init checker #12495

liufengyun commented May 17, 2021 •

edited

Loading

olhotak May 18, 2021

liufengyun May 19, 2021

olhotak May 18, 2021

liufengyun May 19, 2021

olhotak May 18, 2021

olhotak May 18, 2021

liufengyun May 19, 2021

olhotak May 18, 2021

liufengyun May 19, 2021

olhotak May 18, 2021

olhotak May 18, 2021

liufengyun May 19, 2021

olhotak May 18, 2021

liufengyun May 19, 2021

olhotak May 18, 2021

olhotak May 18, 2021

liufengyun May 19, 2021

olhotak May 20, 2021

liufengyun May 21, 2021

olhotak May 20, 2021

EnzeXing May 20, 2021

liufengyun May 21, 2021

olhotak left a comment

liufengyun commented May 21, 2021

liufengyun commented May 21, 2021

A simpler implementation of init checker #12495

A simpler implementation of init checker #12495

Conversation

liufengyun commented May 17, 2021 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

olhotak left a comment

Choose a reason for hiding this comment

liufengyun commented May 21, 2021

liufengyun commented May 21, 2021

liufengyun commented May 17, 2021 •

edited

Loading