Use initialization checker for soundness #11716

liufengyun · 2021-03-12T12:59:52Z

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

-- Warning: tests/init/neg/i5854.scala:3:6 -------------------------------------
3 |  val b: { type A >: Any <: Nothing } = loop()         // error
  |      ^
  |  Access non-initialized value b. Calling trace:
  |   -> val a: String = (((1: Any): b.A): Nothing): String	[ i5854.scala:2 ]
1 warning found

-- 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

olhotak · 2021-03-12T17:44:47Z

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]


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

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

We get types like the following in effpi: effpi.examples.demo.audit.types.Pay#replyTo

natsukagami

I don't think I fully understand what effectsOfType does, but the rest looks OK!

natsukagami · 2021-03-17T10:04:51Z

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

@@ -213,6 +214,19 @@ object Summarization {
    else summary
  }

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


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

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.

liufengyun · 2021-03-17T10:13:24Z

@olhotak Could you also have a look at the changes?

olhotak · 2021-03-17T14:10:16Z

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

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


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?

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.

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?

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.

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?

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.

olhotak · 2021-03-17T14:18:46Z

I have another question above about TermRef/SingletonType.

We should check the various pieces of code in the comments of #50, scala/bug#9633, #4042, #4031, #5854. I think you have some of these already but there seem to be a lot of examples there: there are probably more that should be added as test cases.

Otherwise LGTM.

liufengyun · 2021-03-17T15:13:05Z

We should check the various pieces of code in the comments of #50, scala/bug#9633, #4042, #4031, #5854. I think you have some of these already but there seem to be a lot of examples there: there are probably more that should be added as test cases.

I added some more tests. I didn't include tests that use null as a value, as that can be easily handled by null-safety.

olhotak · 2021-03-17T15:26:33Z

We should check the various pieces of code in the comments of #50, scala/bug#9633, #4042, #4031, #5854. I think you have some of these already but there seem to be a lot of examples there: there are probably more that should be added as test cases.

I added some more tests. I didn't include tests that use null as a value, as that can be easily handled by null-safety.

Good point. I will ask @noti0na1 to look at which of the above examples are fixed by -Yexplicit-nulls and add them as tests (separately from this PR).

liufengyun added 2 commits March 12, 2021 13:58

Performance tweak: use vector for effects and potentials

2cefd3e

olhotak reviewed Mar 12, 2021

View reviewed changes

liufengyun force-pushed the fix-11572 branch from c363485 to 5c9c017 Compare March 12, 2021 17:54

liufengyun added 2 commits March 12, 2021 19:40

Handle types that appear in effpi

aaffb11

We get types like the following in effpi: effpi.examples.demo.audit.types.Pay#replyTo

Refine documentation

fe38137

liufengyun force-pushed the fix-11572 branch from 3235a0e to aaffb11 Compare March 12, 2021 18:49

liufengyun changed the title ~~WIP: Use initialization checker for soundness~~ Use initialization checker for soundness Mar 12, 2021

liufengyun marked this pull request as ready for review March 12, 2021 20:16

Fix scala#5854: check type annotations for soundness

74bcfd7

liufengyun force-pushed the fix-11572 branch from 16ca40f to 74bcfd7 Compare March 12, 2021 21:10

liufengyun requested a review from natsukagami March 15, 2021 09:40

natsukagami reviewed Mar 17, 2021

View reviewed changes

olhotak reviewed Mar 17, 2021

View reviewed changes

liufengyun added 2 commits March 17, 2021 15:54

Add test case

d28f147

Fix scala#4042: add test

ad1aac0

liufengyun linked an issue Mar 17, 2021 that may be closed by this pull request

Unsoundness due to initialization-produced null #4042

Closed

liufengyun merged commit 60dd2ad into scala:master Mar 17, 2021

liufengyun deleted the fix-11572 branch March 17, 2021 17:27

liufengyun mentioned this pull request Mar 18, 2021

Unsoundness from not-yet-initialized path without involving divergence #11572

Open

LPTK mentioned this pull request Apr 3, 2021

Add exclusion/not type lampepfl/dotty-feature-requests#177

Closed

Kordyjan added this to the 3.0.0 milestone Aug 2, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Use initialization checker for soundness #11716

Use initialization checker for soundness #11716

liufengyun commented Mar 12, 2021 •

edited

Loading

olhotak Mar 12, 2021

liufengyun Mar 12, 2021

natsukagami left a comment

natsukagami Mar 17, 2021

liufengyun Mar 17, 2021

liufengyun commented Mar 17, 2021

olhotak Mar 17, 2021

liufengyun Mar 17, 2021

olhotak Mar 17, 2021

liufengyun Mar 17, 2021

olhotak Mar 17, 2021

liufengyun Mar 17, 2021

olhotak commented Mar 17, 2021

liufengyun commented Mar 17, 2021

olhotak commented Mar 17, 2021

Use initialization checker for soundness #11716

Use initialization checker for soundness #11716

Conversation

liufengyun commented Mar 12, 2021 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

natsukagami left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

liufengyun commented Mar 17, 2021

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 commented Mar 17, 2021

liufengyun commented Mar 17, 2021

olhotak commented Mar 17, 2021

liufengyun commented Mar 12, 2021 •

edited

Loading