From 5285598dc688ba82934126178ab2f4cf4ad49f3b Mon Sep 17 00:00:00 2001 From: HarrisL2 Date: Mon, 3 Nov 2025 04:33:51 -0500 Subject: [PATCH 1/2] Record NotNullInfo for exceptional try-catch --- .../src/dotty/tools/dotc/typer/Typer.scala | 55 ++++++++++---- tests/explicit-nulls/neg/i21619.scala | 76 ++++++++++++++++++- 2 files changed, 117 insertions(+), 14 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala index c5ded4e22dbf..3b7a5437ed38 100644 --- a/compiler/src/dotty/tools/dotc/typer/Typer.scala +++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala @@ -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(δ). + */ 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(_))) + else + NotNullInfo.empty + val normalResolveNNInfo = tryNNInfo.alt(catchNNInfo) + val exceptionalResolveNNInfo = 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 + normalFinalNNInfo + else + exceptionalFinalNNInfo + 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 diff --git a/tests/explicit-nulls/neg/i21619.scala b/tests/explicit-nulls/neg/i21619.scala index d7af27e3fe64..d73b5fe95e5d 100644 --- a/tests/explicit-nulls/neg/i21619.scala +++ b/tests/explicit-nulls/neg/i21619.scala @@ -89,4 +89,78 @@ def test6 = { } } x.replace("", "") // error -} \ No newline at end of file +} + +// 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 \ No newline at end of file From 9b62f71f3bf5fd0f7490ec60e65c324ee0f65ba5 Mon Sep 17 00:00:00 2001 From: HarrisL2 Date: Mon, 3 Nov 2025 15:50:23 -0500 Subject: [PATCH 2/2] Address PR comments --- .../src/dotty/tools/dotc/typer/Typer.scala | 65 +++++++------- tests/explicit-nulls/neg/i21619.scala | 86 ++++++++++++++++++- 2 files changed, 119 insertions(+), 32 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala index 3b7a5437ed38..932430c3d4e0 100644 --- a/compiler/src/dotty/tools/dotc/typer/Typer.scala +++ b/compiler/src/dotty/tools/dotc/typer/Typer.scala @@ -2436,29 +2436,36 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer val capabilityProof = caughtExceptions.reduce(OrType(_, _, true)) untpd.Block(makeCanThrow(capabilityProof), expr) - /** Graphic explaination of NotNullInfo logic: + /** Graphic explanation of NotNullInfo logic: * Leftward exit indicates exceptional case * Downward exit indicates normal case * - * ┌─────┐ α.retractedInfo + * ┌─────┐ * │ Try ├─────┬────────┬─────┐ * └──┬──┘ ▼ ▼ │ * │ ┌───────┐┌───────┐ │ - * α │ │ Catch ││ Catch ├─┤ + * │ │ 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(δ). + * └─┬──────┴────────┘ │ + * ▼ ▼ + * ┌─────────┐ ┌─────────┐ + * │ 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). */ def typedTry(tree: untpd.Try, pt: Type)(using Context): Try = val expr2 :: cases2x = harmonic(harmonize, pt) { @@ -2478,25 +2485,21 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer expr1 :: cases1 }: @unchecked val cases2 = cases2x.asInstanceOf[List[CaseDef]] - val tryNNInfo = expr2.notNullInfo + 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. - val catchNNInfo = if cases2.nonEmpty then - tryNNInfo.seq(cases2.map(_.notNullInfo).reduce(_.alt(_))) + val casesNNInfo = if cases2.nonEmpty then + exprNNInfo.retractedInfo.seq(cases2.map(_.notNullInfo).reduce(_.alt(_))) else - NotNullInfo.empty - val normalResolveNNInfo = tryNNInfo.alt(catchNNInfo) - val exceptionalResolveNNInfo = 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 - normalFinalNNInfo - else - exceptionalFinalNNInfo + 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 = diff --git a/tests/explicit-nulls/neg/i21619.scala b/tests/explicit-nulls/neg/i21619.scala index d73b5fe95e5d..014bb3639c61 100644 --- a/tests/explicit-nulls/neg/i21619.scala +++ b/tests/explicit-nulls/neg/i21619.scala @@ -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 @@ -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 = "" @@ -126,6 +177,16 @@ def test9() = } 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 { @@ -163,4 +224,27 @@ def test12() = throw new Exception x = "" } - x.trim() // ok \ No newline at end of file + 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 \ No newline at end of file