Skip to content
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

Refine error messages for early promotion #15263

Merged
merged 11 commits into from
May 25, 2022
Merged

Conversation

liufengyun
Copy link
Contributor

  • Stop early promotion on first error
  • Refine error messages for early promotion

@liufengyun
Copy link
Contributor Author

The failure comes from the tree checker, due to a limitation in subtyping checker:

dotty.tools.dotc.transform.init.Semantic.Hot.type 
| (dotty.tools.dotc.transform.init.Semantic.Hot.type 
|  dotty.tools.dotc.transform.init.Semantic.Cold.type )  

<:  

dotty.tools.dotc.transform.init.Semantic.Hot.type 
| dotty.tools.dotc.transform.init.Semantic.Cold.type 

= false

@liufengyun liufengyun force-pushed the restrict-early-promote branch from b9d3145 to cbdda5f Compare May 23, 2022 00:20
The failure comes from the tree checker, due to a limitation in subtyping checker:

```
dotty.tools.dotc.transform.init.Semantic.Hot.type
| (dotty.tools.dotc.transform.init.Semantic.Hot.type
|  dotty.tools.dotc.transform.init.Semantic.Cold.type )

<:

dotty.tools.dotc.transform.init.Semantic.Hot.type
| dotty.tools.dotc.transform.init.Semantic.Cold.type

= false
```
@liufengyun liufengyun force-pushed the restrict-early-promote branch from cbdda5f to efb9776 Compare May 23, 2022 05:50
@liufengyun liufengyun marked this pull request as ready for review May 23, 2022 07:14
@liufengyun liufengyun requested a review from olhotak May 23, 2022 07:15
|
| The unsafe promotion may cause the following problem:
| Cannot prove that the value is fully initialized. Only initialized values may be used as arguments.
| Cannot prove the argument is fully initialized.
Copy link
Contributor

Choose a reason for hiding this comment

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

I still find these messages difficult to understand. Here's how I would explain this particular failure to someone. (We can think about making the error messages closer to such an explanation.)

  1. The arguments of a method call in a constructor must be fully initialized. I could not prove that the underlined argument is fully initialized.
  2. For a closure to be considered fully initialized, its body must access only fully initialized variables. I could not prove that the underlined access is fully initialized.

One general distinction I see is between "X must be fully initialized because that is the rule (e.g. argument to a method call in a constructor)" vs. "X must be fully initialized in order to prove that Y is fully initialized (e.g. expression in body of closure)".

| ^
| -> val bAgain = toB.getBAgain [ inherit-non-hot.scala:16 ]
| ^^^
| May only assign fully initialized value. Calling trace:
Copy link
Contributor

Choose a reason for hiding this comment

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

  1. The RHS of an assignment to a field that may be called from a constructor must be fully initialized.
  2. This assignment may be called from a constructor because:
    2a. The constructor of object Foo calls new C (line 19)
    (It seems line 15 is not really relevant to the explanation.)
    2b. The constructor of C calls A.toB (line 16)
    2c. A.toB contains the assignment to the field.
  3. I could not prove that the assigned value is fully initialized for the following reason.
    3a. For the result of a constructor call to be fully initialized, all arguments of the call must be fully initialized. I could not prove that the argument this for the parameter a is fully initialized.
    3b. I could not prove that this is fully initialized because the initializer of its field c has not yet run.

| ^^^^^^^^^^^
| -> updateA() [ local-warm4.scala:21 ]
| ^^^^^^^^^
| May only assign fully initialized value. Calling trace:
Copy link
Contributor

Choose a reason for hiding this comment

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

Again, I think there are two issues here:

  • Why is line 18 called from a constructor? (Maybe say from the constructor of which class, in this case localWarm, through a stack of several other calls.)
  • Why is newA not considered fully initialized? (In this case, because it comes from new A(y), and y is not fully initialized. Why is not fully initialized? Because the tree new A(y) executes before the initializer of A.y runs. Why before? Because the constructor of B, which is a subclass of class A that contains the initializer of y, calls increment (line 23), which calls updateA (line 21), which contains the tree new A(y) (line 17). )

|
| The unsafe promotion may cause the following problem:
| Cannot prove that the value is fully initialized. Only initialized values may be used as arguments.
| Cannot prove the argument is fully initialized.
Copy link
Contributor

Choose a reason for hiding this comment

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

  1. The arguments of a method call in a constructor must be fully initialized. I could not prove that the underlined argument is fully initialized.
  2. The initializer of b instantiates class B.
  3. The constructor of B references test, the self parameter of class Test.
  4. The this of class Test is not yet initialized because the initializer of its field n has not yet run.

@olhotak
Copy link
Contributor

olhotak commented May 24, 2022

While interpreting other error messages from the initialization checker, it occurred to me that it would be useful for each error message to start with a statement of which class (constructor) is being checker. The error message starts with the location where the initialization checker failed to prove that a class is safely initialized, but often this location is far removed from the class that is not safely initialized.

@liufengyun
Copy link
Contributor Author

While interpreting other error messages from the initialization checker, it occurred to me that it would be useful for each error message to start with a statement of which class (constructor) is being checker. The error message starts with the location where the initialization checker failed to prove that a class is safely initialized, but often this location is far removed from the class that is not safely initialized.

This is a good improvement. Now we make sure that the top of the trace is always the class under check. The tracing and error reporting mechanism is overhauled and the low-hanging fruits are dealt with.

For other suggestions, we need to discuss how to tackle them. As this PR mainly focuses on overhauling the infrastructure of error reporting, can we address the remaining concerns in other PRs?

Copy link
Contributor

@olhotak olhotak left a comment

Choose a reason for hiding this comment

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

My comments here are minor. After you consider them, this can be merged.

if allArgsPromote then
Hot: Value
else if errors.nonEmpty then
for error <- errors do reporter.report(error)
Copy link
Contributor

Choose a reason for hiding this comment

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

Could be factored into a method (reportAll) in Reporter.

Hot: Value
else if errors.nonEmpty then
for error <- errors do reporter.report(error)
Hot: Value
Copy link
Contributor

Choose a reason for hiding this comment

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

Why is the ascription needed?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

This is due to a TreeChecker failure:

#15263 (comment)

I have no idea why the subtyping failed --- it shouldn't be.

val cls = target.owner.enclosingClass.asClass
val ddef = target.defTree.asInstanceOf[DefDef]
val argErrors = checkArgs
val argErrors = Reporter.errorsIn { args.foreach(_.promote) }
Copy link
Contributor

Choose a reason for hiding this comment

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

Why not Reporter.errorsIn { checkArgs } ?

def call(meth: Symbol, args: List[ArgInfo], receiver: Type, superType: Type, source: Tree, needResolve: Boolean = true): Contextual[Result] = log("call " + meth.show + ", args = " + args, printer, (_: Result).show) {
def checkArgs = args.flatMap(_.promote)
def call(meth: Symbol, args: List[ArgInfo], receiver: Type, superType: Type, needResolve: Boolean = true): Contextual[Value] = log("call " + meth.show + ", args = " + args, printer, (_: Value).show) {
def checkArgs = args.foreach(_.promote)
Copy link
Contributor

Choose a reason for hiding this comment

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

Consider renaming to promoteArgs. Also consider parentheses promoteArgs() to indicate side effect and Unit return type. But many other methods here have side effects, so maybe not.

@olhotak
Copy link
Contributor

olhotak commented May 25, 2022

While interpreting other error messages from the initialization checker, it occurred to me that it would be useful for each error message to start with a statement of which class (constructor) is being checker. The error message starts with the location where the initialization checker failed to prove that a class is safely initialized, but often this location is far removed from the class that is not safely initialized.

This is a good improvement. Now we make sure that the top of the trace is always the class under check. The tracing and error reporting mechanism is overhauled and the low-hanging fruits are dealt with.

For other suggestions, we need to discuss how to tackle them. As this PR mainly focuses on overhauling the infrastructure of error reporting, can we address the remaining concerns in other PRs?

I agree that this PR is already a good improvement - the call traces are more informative. The class being checked at the top of the trace really helps.

I also agree with a separate discussion and separate PR for further improvements.

@liufengyun liufengyun enabled auto-merge May 25, 2022 20:34
@liufengyun liufengyun merged commit 4518be0 into main May 25, 2022
@liufengyun liufengyun deleted the restrict-early-promote branch May 25, 2022 22:14
@Kordyjan Kordyjan added this to the 3.2.0 milestone Aug 1, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants