Record NotNullInfo for exceptional try-catch

[HarrisL2]

Fixes #24296

This PR modifies the logic for recording notNullInfo in try-catch-finally blocks, motivated by repeated pattern from community build sconfig (source):

def computeCachedConfig(
      loader: ClassLoader,
      key: String,
      updater: Callable[Config]
  ): Config = {
    var cache: LoaderCache = null
    try {
      cache = LoaderCacheHolder.cache
    } catch {
      case e: ExceptionInInitializerError =>
        throw ConfigImplUtil.extractInitializerError(e)
    }
    cache.getOrElseUpdate(loader, key, updater)
  }

Here, the cache will never be null. Because all cases of the catch block resolve exceptionally, no matter where in the try block an exception occurs, once an exception is thrown, the entire context will resolve exceptionally. Hence, we can use the notNullInfo of the try block to type what comes after the catch.

The logic of the notNullInfo is as follows (also in code):

/** 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).
   */

[noti0na1]

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.

[olhotak]

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.

[noti0na1]

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?

[olhotak]

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.

[noti0na1]

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

[olhotak]

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.

[noti0na1]

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.

[olhotak]

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.

[noti0na1]

If cases is empty, then the nninfo from expr will never be included?

[olhotak]

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

[olhotak]

However, if cases is empty, it should be empty.terminatedInfo because any exception will never be caught.

[noti0na1]

Also, I would like to name the situation where all cases terminates exceptionally as "exceptional"..

[olhotak]

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.

[olhotak]

Suggested change

	/** Graphic explaination of NotNullInfo logic:
	/** Graphic explanation of NotNullInfo logic:

[olhotak]

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

[olhotak]

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.

[HarrisL2]

I see, I realized after commenting that I mixed up some symbols and deleted my reply, sorry for the confusion.

[olhotak]

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.

[olhotak]

Suggested change

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

[olhotak]

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.

[olhotak]

However, if cases is empty, it should be empty.terminatedInfo because any exception will never be caught.

[olhotak]

Suggested change

	NotNullInfo.empty
	NotNullInfo.empty.terminatedInfo

[olhotak]

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.

[olhotak]

I see that Github reordered my comments by the chronological order of @noti0na1 's comments that they were replying to. That puts my comments in a confusing order. It's clearer to read them in code order, in the order in which they appear on the Files Changed view.