Check safe initialization of static objects

[liufengyun]

The problem is illustrated by the example below:

class Foo(val opposite: Foo)
case object A extends Foo(B)     // A -> B
case object B extends Foo(A)     // B -> A

The check aims to be simple for programmers to understand, expressive, fast, and sound.

The check is centered around two design ideas: (1) initialization-time irrelevance; (2) partial ordering.

The check enforces the principle of initialization-time irrelevance, which means that the time when a static object is initialized should not change program semantics. For that purpose, it enforces the following rule:

The initialization of a static object should not directly or indirectly read or write mutable state owned by another static object.

This principle not only puts the initialization of static objects on a solid foundation but also avoids whole-program analysis.

Partial ordering means that the initialization dependencies of static objects form a directed-acyclic graph (DAG). No cycles with length bigger than 1 allowed --- which might lead to deadlocks in the presence of concurrency and strong coupling & subtle contracts between objects.

Related Issues:

#16152
#9176
#11262
scala/bug#9312
scala/bug#9115
scala/bug#9261
scala/bug#5366
scala/bug#9360

[olhotak]

I've seen the pattern of this if statement before. Perhaps it could be factored out. Or perhaps it's too messy to make that general enough.

[olhotak]

Consider a recursive call to initParent on the NewExpr.

[EnzeXing]

Here we begin to define the abstract domain and abstract values as listed in Section 4.4 in paper

[EnzeXing]

Ref is a parent class for both ObjectRef and OfClass, which correspond to Object and Instance locations as listed in Section 4.4. Both ObjectRef and OfClass need to store the values of immutable fields, as stored in valsMap, and the abstract heap address for mutable fields, as stored in varsMap, and the pointers and values for outer classes, as listed in outersMap.

[EnzeXing]

This corresponds with Object(O) as defined in Section 4.4. Note that the maps are mutable, and will be filled as we speculate the initialization of the object.

[olhotak]

If I have case class Foo(a: Int)(b: Int), then Foo(1)(2) == Foo(1)(3).

[EnzeXing]

This corresponds to Instance as defined in Section 4.4. Again, the maps are mutable. We also store its local environment, which stores the information of the local method it resides in. We do not need to store local environment for ObjectRef since they refer to global objects.

[EnzeXing]

This corresponds to the abstract value Cold as in Section 4.4.

[liufengyun]

We use it as a convenience so that we have fewer cases in the method call/select/assign. The convenience should work as if we define a separate Bottom --- otherwise, it's broken.

[EnzeXing]

Abstract heap addresses can refer to mutable fields or local variables. A heap address also stores other necessary information, such as its owner and the region it belongs to. The value corresponds to the address is the join of all mutations to this address.

[EnzeXing]

Comparison between the language design in paper and the actual implementation in checker: in paper, we explicitly list an abstract heap that maps a reference to an object or instance to the map that stores its field values. The checker directly stores the field value maps in ObjectRef and OfClass without using an explicit map. I believe Fengyun said that the paper design is convenient in such way that the references to objects and instances are immutable, as the explicit heap and maps handle the mutable parts, while in the checker, every reference contains mutable parts. Also it seems that in paper, only each instance stores the region it belongs to, while in code implementation, each mutable field stores the region in belongs to. Does it mean that we can define different regions during initialization of an object? This seems to be a more flexible design.

[EnzeXing]

Syntax for the data structure abstraction we use in Objects.scala:

ve ::= ObjectRef(class)
| OfClass(class, vs[outer], ctor, args, env)
| OfArray(object[owner], regions)
| Fun(..., env)
| Cold // abstract values in domain
vs ::= Set(ve) // set of abstract values

refMap = ( ObjectRef | OfClass ) -> ( valsMap, varsMap, outersMap ) // refMap stores field informations of an object or instance
valsMap = valsym -> vs // maps immutable fields to their values
varsMap = valsym -> addr // each mutable field has an abstract address
outersMap = class -> vs // maps outer objects to their values

arrayMap = OfArray -> addr // an array has one address that stores the join value of every element

heap = addr -M> vs

env = (valsMap, Option[env]) // stores local variables in the residing method, and possibly outer environments

addr ::= localVarAddr(regions, valsym, owner)
| fieldVarAddr(regions, valsym, owner) // independent of OfClass/ObjectRef
| arrayAddr(regions, owner) // independent of array element type

regions ::= List(sourcePosition)

Note: -> refers to extensible maps whose entries cannot be modified; -M> refers to extensible whose entries can be modified

[liufengyun]

@nicolasstucki We introduced new annotations to the standard library, marked with @experimental. Could you have a look and see if there are any concerns with introducing the experimental annotations?

[EnzeXing]

If klass is a top-level class, what would klass.owner be?

[liufengyun]

The owner will be the enclosing package --- the root of the name hierarchy is the _root_ package.

[EnzeXing]

If this is the case, would klass.owner.isClass return true on line 817, or it will try the find the enclosing method of the owner? I'm asking this because I'm trying to refine the type for thisV in resolveEnv.

[liufengyun]

Packages are represented as classes in the compiler --- therefore it will return true for top-level classes. It would be nice to add a comment here.

[nicolasstucki]

The @experimental annotation LGTM