-
Notifications
You must be signed in to change notification settings - Fork 1.1k
Record NotNullInfo for exceptional try-catch #24320
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
Changes from 1 commit
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change | ||||
|---|---|---|---|---|---|---|
|
|
@@ -2436,8 +2436,31 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer | |||||
| val capabilityProof = caughtExceptions.reduce(OrType(_, _, true)) | ||||||
| untpd.Block(makeCanThrow(capabilityProof), expr) | ||||||
|
|
||||||
| /** Graphic explaination of NotNullInfo logic: | ||||||
| * Leftward exit indicates exceptional case | ||||||
| * Downward exit indicates normal case | ||||||
| * | ||||||
| * ┌─────┐ α.retractedInfo | ||||||
| * │ Try ├─────┬────────┬─────┐ | ||||||
| * └──┬──┘ ▼ ▼ │ | ||||||
| * │ ┌───────┐┌───────┐ │ | ||||||
| * α │ │ Catch ││ Catch ├─┤ | ||||||
| * │ └───┬───┘└───┬───┘ │ | ||||||
| * │ β │ │ │ | ||||||
| * └──┬─────┴────────┘ │ | ||||||
| * │ γ = α.alt(β) │ ε = β.retractedInfo | ||||||
| * ▼ ▼ | ||||||
| * ┌─────────┐ ┌─────────┐ | ||||||
| * δ = type(ε)│ Finally ├──────┐ │ Finally ├─────────┐ | ||||||
| * └────┬────┘ │ └────┬────┘ │ | ||||||
| * │ │ ▼ ▼ | ||||||
| * │ γ.seq(δ) └──────────────────────────► | ||||||
| * ▼ ε.seq(δ) | ||||||
| * We choose to use γ.seq(δ) as the NotNullInfo of the | ||||||
| * overall tree if all the catch cases have NothingType, | ||||||
| * otherwise we use ε.seq(δ). | ||||||
| */ | ||||||
|
Contributor
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. It occurred to me that putting the Greek letters on the diagram is misleading. (I take the blame for originally It is misleading because the Instead, the Greek letters should be defined below the diagram as equations. (And we could come up with suitable descriptive English names instead of Greek letters.) \alpha = effect of try Possible English names:
Contributor
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. No, I did mean beta, not alpha. Another way of writing it would be: \alpha seq \delta corresponds to the try block completing normally, then the finally block completing normally. \lambda seq \delta corresponds to the try block throwing, the catch block catching it and completing normally, then the finally block completing normally.
Contributor
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I see, I realized after commenting that I mixed up some symbols and deleted my reply, sorry for the confusion. |
||||||
| def typedTry(tree: untpd.Try, pt: Type)(using Context): Try = | ||||||
| var nnInfo = NotNullInfo.empty | ||||||
| val expr2 :: cases2x = harmonic(harmonize, pt) { | ||||||
| // We want to type check tree.expr first to comput NotNullInfo, but `addCanThrowCapabilities` | ||||||
| // uses the types of patterns in `tree.cases` to determine the capabilities. | ||||||
|
|
@@ -2450,25 +2473,31 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer | |||||
| val casesEmptyBody2 = typedCases(casesEmptyBody1, EmptyTree, defn.ThrowableType, WildcardType) | ||||||
| val expr1 = typed(addCanThrowCapabilities(tree.expr, casesEmptyBody2), pt.dropIfProto) | ||||||
|
|
||||||
| // Since we don't know at which point the the exception is thrown in the body, | ||||||
| // we have to collect any reference that is once retracted. | ||||||
| nnInfo = expr1.notNullInfo.retractedInfo | ||||||
|
|
||||||
| val casesCtx = ctx.addNotNullInfo(nnInfo) | ||||||
| val casesCtx = ctx.addNotNullInfo(expr1.notNullInfo.retractedInfo) | ||||||
| val cases1 = typedCases(tree.cases, EmptyTree, defn.ThrowableType, pt.dropIfProto)(using casesCtx) | ||||||
| expr1 :: cases1 | ||||||
| }: @unchecked | ||||||
| val cases2 = cases2x.asInstanceOf[List[CaseDef]] | ||||||
|
|
||||||
| val tryNNInfo = expr2.notNullInfo | ||||||
|
||||||
| // It is possible to have non-exhaustive cases, and some exceptions are thrown and not caught. | ||||||
| // Therefore, the code in the finalizer and after the try block can only rely on the retracted | ||||||
| // info from the cases' body. | ||||||
| if cases2.nonEmpty then | ||||||
| nnInfo = nnInfo.seq(cases2.map(_.notNullInfo.retractedInfo).reduce(_.alt(_))) | ||||||
|
|
||||||
| val finalizer1 = typed(tree.finalizer, defn.UnitType)(using ctx.addNotNullInfo(nnInfo)) | ||||||
| nnInfo = nnInfo.seq(finalizer1.notNullInfo) | ||||||
| assignType(cpy.Try(tree)(expr2, cases2, finalizer1), expr2, cases2).withNotNullInfo(nnInfo) | ||||||
| val catchNNInfo = if cases2.nonEmpty then | ||||||
| tryNNInfo.seq(cases2.map(_.notNullInfo).reduce(_.alt(_))) | ||||||
|
||||||
| tryNNInfo.seq(cases2.map(_.notNullInfo).reduce(_.alt(_))) | |
| tryNNInfo.retractedInfo.seq(cases2.map(_.notNullInfo).reduce(_.alt(_))) |
Outdated
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
If cases is empty, then the nninfo from expr will never be included?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It need not be included in \lambda here (catchNNInfo) because we will recover it when we do \beta = \alpha alt \lambda, but it does need to be included in finallyCtx. See my suggested code change to exceptionalResolveNNInfo below.
Example (please add as a test case):
try {
x = null
throw new RuntimeException
} finally {
x.trim() // error
}
x.trim() // OKThere was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
However, if cases is empty, it should be empty.terminatedInfo because any exception will never be caught.
Outdated
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
| NotNullInfo.empty | |
| NotNullInfo.empty.terminatedInfo |
Outdated
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
| val exceptionalResolveNNInfo = catchNNInfo.retractedInfo | |
| val exceptionalResolveNNInfo = normalResolveNNInfo.retractedInfo // tryNNInfo.retractedInfo.alt(catchNNInfo.retractedInfo) |
Outdated
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
If the notNullinfo.asserted is null, then we know the program terminates in middle exceptionally, which tracks more cases than just the result type. See the comment of NotNullInfo and uses of terminatedInfo.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I agree. I think the correct thing to do here would be
val resNNInfo = normalFinalNNInfo alt (exceptionalFinalNNInfo seq NotNullInfo.empty.terminatedInfo)See \theta in my comment above.
Outdated
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Also, I would like to name the situation where all cases terminates exceptionally as "exceptional"..
Outdated
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
As discussed in #24296 (comment), if we want to consider the situation where all cases are exceptional, we should only apply the special rule if finally is empty, otherwise we need to type finally tree twice using different initial nninfos.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It is sufficient to type finally once provided that we type it in a context that considers all the paths before it that reach the finally. That condition is satisfied in the status quo and should also be satisfied in this PR with the suggested fixes.
The NN info that we get from typing finally is a summary of the effect of the finally block on the nullness state. An important distinction is that the effect is not an abstraction of the nullness state at any particular program point, such as the end of the finally block. This distinction is what makes the Greek letters in the diagram misleading.
Since the NN info that we get from typing finally summarizes the effect of the finally, we can type the finally once and use the obtained NN info twice: once sequenced with \beta (normalNNInfo) and once sequenced with \beta.retractedInfo but post-sequenced by empty.terminated (to indicate that this path does not reach the code after the try-catch-finally).
The latter alternative is necessary because the NN info represents, in one structure, both the information about normal completion of a block of code and about exceptional completion of a block of code. Specifically, for a given resNNInfo computed for a try-catch-finally block, both of the following need to be correct:
- If the t-c-f block completes normally, the resNNInfo soundly overapproximates the state for the code after the t-c-f block.
- If the t-c-f block completes exceptionally, then resNNInfo.retractedInfo soundly overapproximates the state in any exception handler that may be catching this exception.
It is easy to focus on 1. and forget about 2.
A possible alternative design would be for NNinfo to explicitly distinguish these two cases, so that .retractedInfo doesn't just manipulate these two sets. This would require a third set in NNinfo for what is retracted on an exceptional completion. (The asserted set for an exceptional completion is always empty, so we don't need to add a fourth set.) That would be a refactoring of NNinfo. It would give a small improvement in precision, perhaps too small to be valuable, and an improvement in understandability, which may be a more compelling argument for doing it.
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -89,4 +89,78 @@ def test6 = { | |
| } | ||
| } | ||
| x.replace("", "") // error | ||
| } | ||
| } | ||
|
|
||
| // From i24296 | ||
| def test7() = | ||
| var x: String | Null = null | ||
| try { | ||
| x = "" | ||
| } catch { | ||
| case e => | ||
| throw e | ||
| } | ||
| x.trim() // ok | ||
|
|
||
| def test8() = | ||
| var x: String | Null = null | ||
| try { | ||
| try { | ||
| x = "" | ||
| } catch { | ||
| case e => throw e | ||
| } | ||
| } catch { | ||
| case e => throw e | ||
| } | ||
| x.trim() // ok | ||
|
|
||
| def test9() = | ||
| var x: String | Null = null | ||
| try { | ||
| x = "" | ||
| } catch { | ||
| case e: AssertionError => | ||
| throw e | ||
| case _ => | ||
HarrisL2 marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| } | ||
| x.trim() // error | ||
|
|
||
| def test10() = | ||
| var x: String | Null = null | ||
| try { | ||
| x = "" | ||
| } catch { | ||
| case e => | ||
| throw e | ||
| } finally { | ||
| x = null | ||
| } | ||
| x.trim() // error | ||
|
|
||
| def test11() = | ||
| var x: String | Null = null | ||
| try { | ||
| x = "" | ||
| } catch { | ||
| case e => | ||
| x = null | ||
| throw e | ||
| } finally { | ||
| x = "" | ||
| } | ||
| x.trim() // ok | ||
|
|
||
| def test12() = | ||
| var x: String | Null = null | ||
| try { | ||
| x = "" | ||
| } catch { | ||
| case e => | ||
| x = null | ||
| throw e | ||
| } finally { | ||
| throw new Exception | ||
| x = "" | ||
| } | ||
| x.trim() // ok | ||
|
||
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.