Flow analysis. Unassigned variable is treated as definitely assigned

[sgrekhov]

  int i;
  try {
    throw "throw!";
    i = 42;
  } finally {
    i; // Error: Non-nullable variable 'i' must be assigned before it can be used.
  }
  i; // No error

Why there is no error when i is read after try-finally block?

cc @stereotype441

Dart SDK version: 3.8.0-265.0.dev (dev) (Thu Apr 3 21:12:43 2025 -0700) on "windows_x64"

[eernstg]

We talked a bit about a similar example elsewhere, but I forgot a thing: When an exception is thrown in the try block, that block will immediately complete throwing that exception; next, the finally block will run. However, even if the finally block completes normally, the next thing that happens is that the exception which was being thrown when the finally block started executing is still being thrown. So if N is the try/finally statement then after(N) is unreachable, and the second i; is analyzed as such.

It's definitely counter-intuitive, but I do think the outcome is as intended. It's yet another case where the analysis of unreachable code is confusing because it considers all the unreachable predecessors as being potential predecessors. If the code is adjusted such that at least one control flow path is reachable then we'll disregard all the unreachable paths, and then i may not be definitely assigned any more.

[lrhn]

What Erik says is probably true - the second i is unreachable because the try statement cannot complete normally.
A variable being uninitialized along zero code paths isn't really surprising, so no need to also tell you that your unreachable code didn't initialize a variable "along the way". Or, to put it differently, the variable is vacuously definitely assigned along all code paths reaching it, so there is no error.

Everything is true about the control flow into dead code.
(That's not what it does, though, it does combine initializing and non-initializing branches that lead up to the dead code, as if there was a flow from the finally block into the code after it, even if it recognizes that if a try body can't complete normally, then neither can its finally block.)

On top of that, looking only at the code outside the try body, the second read of i is dominated by the first read of i, so I'd also want to quenching the second, duplicate, error.
The analyzer doesn't do that, it gives two errors for print(i + i) above.

If you write:

final int i;
// no assignment to i
print(i + i);

it's not really necessary to tell you that both reads are uninitialized, one should be sufficient, at the first where it's read that dominate all the other reads. If you fix the first read, every other read dominated by that will also be fixed.
(Analyzer does give two errors, so that isn't it.)

[stereotype441]

I dug a bit into the implementation, and this looks like another place where the specification and the implementation don't agree.

Here's what the spec currently says (see the statements section of the flow analysis spec):

• try finally: If N is a try/finally statement of the form try B1 finally B2 then:
  • Let before(B1) = split(before(N))
  • Let before(B2) = split(join(drop(after(B1)), conservativeJoin(before(N), assignedIn(B1), capturedIn(B1))))
  • Let after(N) = restrict(after(B1), after(B2), assignedIn(B2))

Here is what was actually implemented:

• try finally: If N is a try/finally statement of the form try B1 finally B2 then:
  • Let before(B1) = before(N)
  • Let before(B2) = join(after(B1), conservativeJoin(before(N), assignedIn(B1), capturedIn(B1)))
  • Let after(N) = attachFinally(after(B1), before(B2), after(B2)).

Unfortunately, I don't have enough time right now to fully specify the behavior of attachFinally. Here's what it does in a nutshell:

• If before(B2) and after(B2) are the same*, then it lets after(N) = after(B1). In other words, if nothing of consequence happened in the finally block, then the model after the try/finally statement is the same as the model after the try part.
  • *Note: one of the undocumented differences between the implementation and the specification is that instances of FlowModel have unique identities, so it's possible to meaningfully talk about whether two FlowModels are "the same". By checking whether two FlowModels are the same, it's possible to determine that a chunk of code has zero effect on flow analysis.
• Otherwise, if before(B1), after(B1), and before(B2), are the same, then it lets after(N) = after(B2). In other words, if nothing of consequence happened in the try block, then the model after the try/finally statement is the same as the model after the finally part.
• Otherwise, attachFinally compares the FlowModels before(B2) and after(B2), and applies those differences, using after(B1) as a starting point, to create the final after(N) FlowModel.

So, in your example:

  int i;
  try {
    throw "throw!";
    i = 42;
  } finally {
    i; // Error: Non-nullable variable 'i' must be assigned before it can be used.
  }
  i; // No error

Here's what happens:

• In before(B1), which is the same as before(N), the control path is considered reachable, and i is definitely unassigned.
• In after(B1), the control path is considered unreachable, and i is definitely assigned.
• To compute before(B2):
  • First conservativeJoin(before(N), assignedIn(B1), capturedIn(B1)) is computed. This FlowModel is the same as before(N), except that i is considered potentially assigned. Flow analysis isn't smart enough to see that B1 unconditionally throws before assigning to i; it just sees that B1 contains an assignment to i, and reasons that an exception might or might not get thrown before reaching the assignment, therefore it considers i to be potentially assigned.
  • Then, it joins after(B1) with the result of the conservativeJoin. Since after(B1) is unreachable and the result of the conservativeJoin is reachable, after(B1) is discarded.
  • So in before(B2), the control path is considered reachable and i is potentially assigned.
• Since B2 doesn't do anything that affects flow analysis, after(B2) is the same as before(B2).
• To compute after(N):
  • attachFinally first checks whether before(B2) and after(B2) are the same. They are, so it lets after(N) = after(B1).
• Therefore, after the try/finally statement, the control path is considered unreachable, and i is definitely assigned.

I'm not sure whether it makes sense to close this issue or not. On the one hand, I believe flow analysis is behaving as intended. On the other hand, the description of try/finally in the spec is definitely out of date and could use improvement. @eernstg what do you think?

[lrhn]

A try/finally can (theoretically) jump to the finally finally from any place in the try block. (If it does so, it's because something throws, which any operation can in theory, and then this finally block would also throw.)

"Anywhere in B1" is approximated by joining before(B1) and after(B1), as well as considering every assignment in B1 as potentially executed (I think).

I don't know exactly what after(B1) includes.
If it includes all exits from B1, including state at throws, returns and breaks, then it has all the information.
If it's just flow out of the bottom, would it make sense to instead join the states at every "exit point" of B1, so any throw or rethrow (not inside a catch?), any return, and any break or continue with a target outside. It's not all the possible positions where B1 can potentially exit, but it's just before anything that would be dead code, and it would still joining with before(B1) too.
Then it could distinguish { throw "Foo"; i = 0; } from { i = 0; throw "Foo"; }. The former would join points where i is not assigned with an unreachable position where it is assigned, which means that it's unassigned on all reachable paths. The latter will join an unassigned, a definitely assigned and an unreachable assigned position, so it's potentially assigned in the finally. That would make dead code in B1 be recognized as such in B2, and still allow knowing

• Let after(N) = restrict(after(B1), after(B2), assignedIn(B2))

(I'm guessing this is to recognize that if B1 cannot complete normally, then neither can N, even though B2 is reachable.)

[eernstg]

@stereotype441, thanks for a very clear explanation, as usual! One little thing came to mind:

Since after(B1) is unreachable and the result of the conservativeJoin is reachable, after(B1) is discarded.

I thought merge would do this, but join would just keep both branches and make the result reachable if one or the other branch is reachable (top(r1) || top(r2)). However, I don't think this would make the situation in the next step different.

the description of try/finally in the spec is definitely out of date

Let's just fix that. Work is ongoing, as far as I know. ;-D

[eernstg]

@lrhn, I think it could be interesting to consider whether the conservative join could be made slightly smarter. However, we would need to be very careful in order to avoid widespread breakage. In favor of moving in this direction, one could say that the breakage would generally be caused by flow analysis coming up with analysis results which are more precise and still sound, so there would be new warnings or errors, but they would be semantically justified.

So it's a balancing act: More implementation work, some breakage — versus — more precise analysis, probably catching some additional bugs.

[stereotype441]

@lrhn

I don't know exactly what after(B1) includes. If it includes all exits from B1, including state at throws, returns and breaks, then it has all the information. If it's just flow out of the bottom, would it make sense to instead join the states at every "exit point" of B1, so any throw or rethrow (not inside a catch?), any return, and any break or continue with a target outside. It's not all the possible positions where B1 can potentially exit, but it's just before anything that would be dead code, and it would still joining with before(B1) too. Then it could distinguish { throw "Foo"; i = 0; } from { i = 0; throw "Foo"; }. The former would join points where i is not assigned with an unreachable position where it is assigned, which means that it's unassigned on all reachable paths. The latter will join an unassigned, a definitely assigned and an unreachable assigned position, so it's potentially assigned in the finally. That would make dead code in B1 be recognized as such in B2, and still allow knowing

after(B1) is just flow out of the bottom.

When you say "would it make sense to instead join the states at every "exit point" of B1", I assume you mean "instead of using conservativeJoin, right? (conservativeJoin is conservative enough that it covers every possible point already, so I don't think that joining the exit points and doing conservativeJoin would be noticably different from just doing conservativeJoin.)

Assuing you do mean "instead of using conservativeJoin", then I think what you're proposing would work, and it would change the behavior for the example at the top of this issue.

I'm not entirely convinced that it would be an improvement, though. A nice property that the current implementation has is that flow analysis always treats try S finally {} the same as S. I personally find that property pretty intuitive.

Also, it would be a lot of machinery to implement, and a lot of work to come up with test cases that exercise all that machinery. I think it would be a hard sell to convince me that the benefit is worth the cost. One of the reasons I chose the conservativeJoin approach is that conservativeJoin already exists, and is well exercised by loops, so using it as the basis for try/finally analysis had a low implementation cost.

• Let after(N) = restrict(after(B1), after(B2), assignedIn(B2))

(I'm guessing this is to recognize that if B1 cannot complete normally, then neither can N, even though B2 is reachable.)

Correct 😃

[stereotype441]

@eernstg

@stereotype441, thanks for a very clear explanation, as usual! One little thing came to mind:

Since after(B1) is unreachable and the result of the conservativeJoin is reachable, after(B1) is discarded.

I thought merge would do this, but join would just keep both branches and make the result reachable if one or the other branch is reachable (top(r1) || top(r2)). However, I don't think this would make the situation in the next step different.

Oh gosh, you're right, that is what the spec says! That's definitely not what was implemented. What was implemented was that join has the same behavior as merge if one or the other FlowModel is unreachable (it keeps just the reachable one). In fact, at some point I realized that what I implemented for join and merge was so similar that I didn't need both of them; so the current implementation just has join.

I am really going to have to go through the spec with a fine toothed comb, especially considering everything to do with merge, split, unsplit, and join. My original implementation of flow analysis just had a join operation; Leaf invented merge, split, unsplit, and added them to the spec. They were tremendously useful, and I added them to the implementation. But looking back on things, it's clear that rather than implement what he specified, I just took the core ideas and came up with my own approach.

Sorry for all the confusion. I should have been paying a lot more attention back in 2020 when I did all this implementation work.

the description of try/finally in the spec is definitely out of date

Let's just fix that. Work is ongoing, as far as I know. ;-D

👍