Skip to content

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.

Sign up for GitHub

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

Open
wants to merge 2 commits into
base: main
Choose a base branch
from
+204 −14
Open

Record NotNullInfo for exceptional try-catch #24320

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
5285598
Record NotNullInfo for exceptional try-catch
HarrisL2 Nov 3, 2025
9b62f71
Address PR comments
HarrisL2 Nov 3, 2025
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
58 changes: 45 additions & 13 deletions compiler/src/dotty/tools/dotc/typer/Typer.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2436,8 +2436,38 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
val capabilityProof = caughtExceptions.reduce(OrType(_, _, true))
untpd.Block(makeCanThrow(capabilityProof), expr)

/** Graphic explanation of NotNullInfo logic:
* Leftward exit indicates exceptional case
* Downward exit indicates normal case
*
* ┌─────┐
* │ Try ├─────┬────────┬─────┐
* └──┬──┘ ▼ ▼ │
* │ ┌───────┐┌───────┐ │
* │ │ Catch ││ Catch ├─┤
* │ └───┬───┘└───┬───┘ │
* └─┬──────┴────────┘ │
* ▼ ▼
* ┌─────────┐ ┌─────────┐
* │ Finally ├──────┐ │ Finally ├──┐
* └────┬────┘ │ └────┬────┘ │
* ▼ └─────────┴───────┴─►
* α = tryEffect
* λ = α.retracted.seq.(catchEffects.reduce.alt)
* β = α.alt(λ)
* finallyCtx = β.retracted
* δ = finallyEffect
* resultNNInfo = β.seq(δ).alt(β.retracted.seq(δ).seq(empty.terminated))
*
* 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. Since the NNinfo
* 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 β (normalNNInfo) and once sequenced with β.retractedInfo but post-sequenced
* by empty.terminated (to indicate that this path does not reach the code after
* the try-catch-finally).
*/
Copy link
Contributor

@olhotak olhotak Nov 3, 2025

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

@olhotak olhotak Nov 3, 2025

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

@HarrisL2 HarrisL2 Nov 3, 2025

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 +2480,27 @@ 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 exprNNInfo = 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 casesNNInfo = if cases2.nonEmpty then
exprNNInfo.retractedInfo.seq(cases2.map(_.notNullInfo).reduce(_.alt(_)))
else
NotNullInfo.empty.terminatedInfo
val catchSuccessNNInfo = exprNNInfo.alt(casesNNInfo)
val catchFailNNInfo = catchSuccessNNInfo.retractedInfo

val finalizer1 = typed(tree.finalizer, defn.UnitType)(using ctx.addNotNullInfo(catchFailNNInfo))
val normalFinalNNInfo = catchSuccessNNInfo.seq(finalizer1.notNullInfo)
val exceptionalFinalNNInfo = catchFailNNInfo.seq(finalizer1.notNullInfo)
val resNNInfo = normalFinalNNInfo.alt(exceptionalFinalNNInfo.seq(NotNullInfo.empty.terminatedInfo))
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
160 changes: 159 additions & 1 deletion tests/explicit-nulls/neg/i21619.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,22 @@ def test1: String =
x.replace("", "") // error

def test2: String =
var x: String | Null = null
x = ""
var i: Int = 1
try
i match
case _ =>
x = null
throw new Exception()
x = ""
catch
case e: NoSuchMethodError =>
x = "e"
x.replace("", "") // ok

// From i24296
def test2_2: String =
var x: String | Null = null
x = ""
var i: Int = 1
Expand All @@ -25,8 +41,43 @@ def test2: String =
catch
case e: Exception =>
x = "e"
case _ =>
x.replace("", "") // error

def test2_3: String =
var x: String | Null = null
x = ""
var i: Int = 1
try
i match
case _ =>
x = null
throw new Exception()
x = ""
catch
case e: NoSuchMethodError =>
x = "e"
case e: AbstractMethodError =>
x = "e"
x.replace("", "") // ok

def test2_4: String =
var x: String | Null = null
x = ""
var i: Int = 1
try
i match
case _ =>
x = null
throw new Exception()
x = ""
catch
case e: NoSuchMethodError =>
x = "e"
case e: AbstractMethodError =>
throw new Exception()
x.replace("", "") // ok

def test3: String =
var x: String | Null = null
x = ""
Expand Down Expand Up @@ -89,4 +140,111 @@ 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 test9_2() =
var x: String | Null = null
try {
x = ""
} catch {
case e: AssertionError =>
throw e
}
x.trim() // ok

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

def test12_2() =
var x: String | Null = null
try {
x = ""
} catch {
case e =>
x = null
throw e
} finally {
throw new Exception
}
x.trim() // ok

def test13() =
var x: String | Null = null
try {
x = null
throw new RuntimeException
} finally {
x.trim() // error
}
x.trim() // OK
Loading