[flow analysis] Rework control flow statements and expressions.

[stereotype441]

This change adjusts the specification of flow analysis for the following kinds of statements and expressions, to match what was actually implemented:

• conditional expressions
• if-null expressions
• logical and/or expressions
• null check operators
• break statements
• continue statements
• return statements
• if statements
• while statements
• for statements
• do while statements
• for each statements
• switch statements
• try statements

Also, the paragraphs describing "Local variable conditional assignment" and "Conditional assignment to a non local-variable" are dropped. These paragraphs were quite inaccurate, and the necessary infrastructure isn't in place yet to replace them with more accurate descriptions.

Finally, there's a minor fix: the definition of a promotion chain was backwards (types are listed in least-promoted to most-promoted order).

• Thanks for your contribution! Please replace this text with a description of what this PR is changing or adding and why, list any relevant issues, and review the contribution guidelines below.

---

• I’ve reviewed the contributor guide and applied the relevant portions to this PR.

Contribution guidelines:

• See our contributor guide for general expectations for PRs.
• Larger or significant changes should be discussed in an issue before creating a PR.
• Contributions to our repos should follow the Dart style guide and use dart format.
• Most changes should add an entry to the changelog and may need to rev the pubspec package version.
• Changes to packages require corresponding tests.

Note that many Dart repos have a weekly cadence for reviewing PRs - please allow for some latency before initial review feedback.

[eernstg]

Oh, I didn't get around to look at this one. I should be able to make progress on it on Monday.

[eernstg]

Looks great! I added a couple of questions here and there. For the last part, I couldn't come up with the rules from scratch, but I'm relying on the assumption that this basically specifies the implemented behavior which is already known to handle a huge set of cases correctly.

[eernstg]

Perhaps this could be:

Suggested change

	The `join` and `joinV` combinators are commutative and associative by
	construction.
	The `join` and `joinV` combinators are commutative and associative.

I think 'by construction' is commonly used to indicate that the given properties are satisfied because it is essentially written into the definition (that is, we look at the definition and then it's obvious that each of these properties holds). I think we have these properties for join and joinV because of a slightly more involved chain of reasoning. We basically have to look at a handful of terms (like top(r1) || top(r2)), and then we can mentally outline a proof that, for example, commutativity holds. I think it makes sense to describe this situation in those more neutral words, expecting a reader to re-do this small proof as needed.

[eernstg]

OK, so why would it be obvious that join(M1, join(M2, M3)) is equal to join(join(M1, M2), M3)? I think it is true, but I also think that it would take a bit of proof tinkering to make it explicit in detail why it is true. ;-)

Do we actually need those properties? Are they just "nice to have"?

[stereotype441]

Hmm, good question. I've tried to be explicit everywhere about the order and associativity in which join is applied, and in each case I've tried to verify that the spec matches the implementation. So I guess they're just "nice to have".

I'll make a note to talk at our meeting in a few minutes about whether to make further changes to the spec text to account for this.

[eernstg]

It looks like the purpose of this operation is to compute the longest possible type-decreasing list that begins with p2 and is followed by everything in p1 "that fits".

This is clearly asymmetric. Is that an inherent property of the places where this operation is used, or would it have been equally valid to, say, use [...p2', ...p1] where we're filtering p2 to prevent the "decreasing type" requirement from being violated?

[stereotype441]

It's an inherent property of the places where this operation is used, and I don't think there's any way around that.

Imagine, for example, that p1 is [num?, int] and p2 is [Object, num]. Under my definition, p3 = [...p2, ...p1'], p3 is [Object, num, int]. But if we instead defined p3 = [...p2', ...p1] (where T1 is the first type in p1 and p2' is the promotion chain obtained by deleting any elements T from p2 that do not satisfy T1 <: T), then p3 would be [num?, int].

In all the places that I've used rebasePromotedTypes I've tried to be careful about the order of the arguments so that the user-visible behavior is sensible. See, for instance, #4382, where I fixed a place where the order was backwards compared to what I think would be a reasonable user expectation.

[eernstg]

And the state before the finally block is the same as the state before the entire try/finally statement (because the try block can throw at any point)?

Also, the state after the finally block, does that mean at the end of the finally block? Presumably the whole point of this operation is that it computes the stat after the try/finally statement as a whole, which is also right after the finally block?

Perhaps add a bit of commentary text here, to help readers.

[stereotype441]

And the state before the finally block is the same as the state before the entire try/finally statement (because the try block can throw at any point)?

Almost but not quite:

• If there is a local variable that's promoted prior to the try/finally statement, and it's assigned in the try block, then in the state before the finally block, the promotion is removed.
• If there is a local variable that's in the "definitely unassigned" state prior to the try/finally statement, and it's assigned in the try block, then in the state before the finally block, it's in the "neither definitely assigned nor definitely unassigned" state.
• If there is a local variable that's not write captured prior to the try/finally statement, and it's write captured somewhere within the try block, then in the state before the finally block, the variable is considered write captured.

All of these are handled by the use of conservativeJoin in this text from the try finally bullet in the "Statements" section:

• Let before(B2) = join(after(B1), conservativeJoin(before(N), assignedIn(B1), capturedIn(B1))).

Also, the state after the finally block, does that mean at the end of the finally block? Presumably the whole point of this operation is that it computes the stat after the try/finally statement as a whole, which is also right after the finally block?

Perhaps add a bit of commentary text here, to help readers.

Ok, I will add commentary text, in line with what we just discussed in our meeting.

[eernstg]

Is that 'definitely assigned at the end of the try block'? (So we're using the fact that the try block did not throw.)