Skip to content
Merged
Show file tree
Hide file tree
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
55 changes: 42 additions & 13 deletions compiler/src/dotty/tools/dotc/typer/Typer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Copy link
Contributor

Choose a reason for hiding this comment

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

Suggested change
/** Graphic explaination of NotNullInfo logic:
/** Graphic explanation 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(δ).
*/
Copy link
Contributor

Choose a reason for hiding this comment

The 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
suggesting it.)

It is misleading because the nnInfo represents the effect of a piece of code, not the nullness information at a particular program point. The Greek letters on the diagram suggest program points.

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
\lambda = \alpha.retractedInfo seq ((effects of catches).reduce(alt))
\beta = \alpha alt \lambda
context for typing finally = (\alpha.retractedInfo) alt (\lambda.retractedInfo) = \beta.retractedInfo
\delta = effect of finally
\theta = (\beta seq \delta) alt (\beta.retractedInfo seq \delta seq empty.terminatedInfo)

Possible English names:
\alpha -> effectOfTry
\delta -> effectOfFinally
\theta is just the final nnInfo that we compute for the whole try-catch-finally, so maybe it doesn't need a name
\lambda and \beta I'm not sure of good names
contextForFinally would be a good name, or finallyCtx
\beta means try/catch has completed normally (possibly with an exception that was handled by the catch)
The code below uses normalNNInfo for \beta and exceptionalResolveNNInfo for finallyCtx

Copy link
Contributor

Choose a reason for hiding this comment

The 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:
\theta = (\alpha seq \delta) alt (\lambda seq \delta) alt (\beta.retractedInfo seq \delta seq empty.terminatedInfo)
But since \beta = \alpha alt \lambda, I think the first two cases are equivalent to \beta seq \delta.

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

Copy link
Contributor Author

Choose a reason for hiding this comment

The 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.
Expand All @@ -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
Copy link
Member

@noti0na1 noti0na1 Nov 3, 2025

Choose a reason for hiding this comment

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

The names of tryNNInfo and catchNNInfo variables are confusing.

  • We should rename tryNNInfo to exprNNInfo to indicate the info from expr.
  • According to the logic, if cases is not empty, catchNNInfo contains the nninfo not only from cases but also from the expr?

Copy link
Contributor

Choose a reason for hiding this comment

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

We need to distinguish \beta (from my comment above) from finallyCtx. Here catchNNInfo is computing \beta. But I agree it needs to use the retracted form of tryNNInfo.

// 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(_)))
Copy link
Member

Choose a reason for hiding this comment

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

As the comment mentioned, it is possible to have non-exhaustive cases, so we can only use the retractedInfo from the cases and combine

Copy link
Contributor

Choose a reason for hiding this comment

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

If the cases are non-exhaustive, then not matching any of the cases causes an exception to propagate outwards. It is equivalent to adding a default case case e => thow e.

In this case, the finally block does get executed but the code after the try-catch-finally does not execute.

Therefore, \beta should have the non-retracted info from the cases for finallyCtx needs to have the retracted info.

Copy link
Contributor

Choose a reason for hiding this comment

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

Suggested change
tryNNInfo.seq(cases2.map(_.notNullInfo).reduce(_.alt(_)))
tryNNInfo.retractedInfo.seq(cases2.map(_.notNullInfo).reduce(_.alt(_)))

else
NotNullInfo.empty
Copy link
Member

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?

Copy link
Contributor

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() // OK

Copy link
Contributor

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.

Copy link
Contributor

Choose a reason for hiding this comment

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

Suggested change
NotNullInfo.empty
NotNullInfo.empty.terminatedInfo

val normalResolveNNInfo = tryNNInfo.alt(catchNNInfo)
val exceptionalResolveNNInfo = catchNNInfo.retractedInfo
Copy link
Contributor

Choose a reason for hiding this comment

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

Suggested change
val exceptionalResolveNNInfo = catchNNInfo.retractedInfo
val exceptionalResolveNNInfo = normalResolveNNInfo.retractedInfo // tryNNInfo.retractedInfo.alt(catchNNInfo.retractedInfo)


val finalizer1 = typed(tree.finalizer, defn.UnitType)(using ctx.addNotNullInfo(exceptionalResolveNNInfo))
val normalFinalNNInfo = normalResolveNNInfo.seq(finalizer1.notNullInfo)
val exceptionalFinalNNInfo = exceptionalResolveNNInfo.seq(finalizer1.notNullInfo)
val resNNInfo =
if (cases2.forall(_.tpe == defn.NothingType)) then
Copy link
Member

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.

Copy link
Contributor

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.

normalFinalNNInfo
Copy link
Member

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

else
exceptionalFinalNNInfo
Copy link
Member

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.

Copy link
Contributor

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:

  1. If the t-c-f block completes normally, the resNNInfo soundly overapproximates the state for the code after the t-c-f block.
  2. 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.

assignType(cpy.Try(tree)(expr2, cases2, finalizer1), expr2, cases2).withNotNullInfo(resNNInfo)

def typedTry(tree: untpd.ParsedTry, pt: Type)(using Context): Try =
val cases: List[untpd.CaseDef] = tree.handler match
Expand Down
76 changes: 75 additions & 1 deletion tests/explicit-nulls/neg/i21619.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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 _ =>
}
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
Copy link
Contributor

Choose a reason for hiding this comment

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

Add a variant of test12 without the x = "" in the finally clause. That should still be // ok because the finally clause cannot terminate normally, so the x.trim() is unreachable.

Loading