Flow analysis. Assignment in the third operand of for(;;) loop is not detected

[sgrekhov]

The code below produces an error in both CFE and the analyzer.

main() {
  int i;
  for (;; i = 42) {  }
  i; // Error: Non-nullable variable 'i' must be assigned before it can be used.
}

i is definitely assigned here. Yes, it is in dead code, but definitely assigned.

Dart SDK version: 3.8.0-174.0.dev (dev) (Mon Mar 10 21:06:07 2025 -0700) on "windows_x64"

[eernstg]

@stereotype441, @johnniwinther, what do you think about the analysis of dead code? Should we try to come up with a well-specified treatment, or should we just stop writing tests about dead code?

[sgrekhov]

UPD. The below is not an issue it is expected. See https://github.com/dart-lang/sdk/issues/42232#issuecomment-690681385. The flow analysis after the break statement can be not intuitive.

I believe the below is the same issue (something is wrong with the flow analysis of the third operand of for-statement.

  late int i;
  for (; ; i = 0) {  // Dead code warning
    break;
  }
  i; // No error in either CFE ot the analyzer

Here i is initialized in dead code therefoe it is definitely unassigned but no error.

[sgrekhov]

@stereotype441 please confirm that the above is not an issue.

[stereotype441]

@stereotype441, @johnniwinther, what do you think about the analysis of dead code? Should we try to come up with a well-specified treatment, or should we just stop writing tests about dead code?

I don't think we should give up on having a well-specified treatment of analysis of dead code. I think the current flow analysis spec already does have a mostly well-specified treatment of analysis of dead code, but there are some bugs in the spec which I'll note below. Here's what the flow analysis spec says about how a for loop is analyzed:

• for statement: If N is a for statement of the form for (D; C; U) S, then:
  • Let before(D) = before(N).
  • Let before(C) = conservativeJoin(after(D), assignedIn(N), capturedIn(N)).
  • Let before(S) = split(true(C)).
  • Let before(U) = merge(after(S), continue(S)).
  • Let after(N) = inheritTested(join(false(C), unsplit(break(S))), after(U)).

Ok, so the first bug in the spec that I want to call out is: this is not exactly what was implemented. What was implemented was:

• for statement: If N is a for statement of the form for (D; C; U) S, then:
  • Let before(D) = before(N).
  • Let before(C) = split(conservativeJoin(after(D), assignedIn(N), capturedIn(N))).
  • Let before(S) = true(C).
  • Let before(U) = join(after(S), continue(S)).
  • Let after(N) = unsplit(inheritTested(join(false(C), break(S)), after(U))).

The difference that join is used instead of merge, and the splits are simpler: we have a single split at the top of the loop (right after the conservativeJoin) and a single unsplit at the bottom of the loop (after inheritTested).

I dug back through source control history, and the difference isn't due to a bug fix or anything; It looks like what happened was, Leaf specified it one way, and I implemented it a different way. I'm not sure why. In any case, I'll make a PR to bring the spec into alignment with the implementation.

Considering the first example:

main() {
  int i;
  for (;; i = 42) {  }
  i; // Error: Non-nullable variable 'i' must be assigned before it can be used.
}

Here's the behavior we expect from flow analysis:

• In before(D), i is definitely unassigned.
• In before(C), i is potentially assigned (since the conservative join can't tell whether the assignment will execute or not).
• In before(S), i is potentially assigned.
• In before(U), i is potentially assigned.
• Now we get to the evaluation of after(N) = unsplit(inheritTested(join(false(C), break(S)), after(U))):
  • In false(C), i is potentially assigned, but this code path is considered unreachable.
  • For join(false(C), break(S)), we run into another spec bug, because break(S) isn't well-defined when there are no break statements (see https://github.com/dart-lang/language/issues/4316). I'll make a PR to fix this too, but in brief, what happens is that the join just turns into a no-op, so we get false(C), which is an unreachable code path in which i is potentially assigned.
  • inheritTested and unsplit don't affect the notion of whether i is potentially assigned, so in after(N), i is considered potentially assigned.
• Therefore, an error is issued at i;, because i is not marked late, and thus i must be definitely assigned to avoid an error.

Considering the second example (from https://github.com/dart-lang/language/issues/4413):

  late int i;
  for (; ; i = 0) {  // Dead code warning
    break;
  }
  i; // No error in either CFE ot the analyzer

Most of the analysis is the same. I've highlighted differences in bold:

• In before(D), i is definitely unassigned.
• In before(C), i is potentially assigned (since the conservative join can't tell whether the assignment will execute or not).
• In before(S), i is potentially assigned.
• In before(U), i is potentially assigned, but this control flow path is unreachable due to the unconditional break.
• Now we get to the evaluation of after(N) = unsplit(inheritTested(join(false(C), break(S)), after(U))):
  • In false(C), i is potentially assigned, but this code path is considered unreachable.
  • In break(S), i is potentially assigned.
  • For join(false(C), break(S)), we keep the flow model from break(S), because it's reachable and the flow model from false(C) isn't. So i is potentially assigned here.
  • inheritTested and unsplit don't affect the notion of whether i is potentially assigned, so in after(N), i is considered potentially assigned.
• Therefore, no error is issued at i;, because i is marked late, and thus i merely has to be potentially assigned to avoid an error.

In short, I think flow analysis is behaving as specified, modulo some minor errors in the spec that I need to fix.

I hope that clears things up. I'll leave this issue open until I've made the PRs to fix the spec bugs I mentioned above.

[eernstg]

Thanks for a great analysis!

I don't think we should give up on having a well-specified treatment of analysis of dead code.

Right! I have a better understanding of the approach today than when I wrote that comment, and I can see that we do have an approach which is consistent and meaningful. Basically, unreachable code is treated as if every predecessor in the flow graph could be the path we had taken when we arrived at that unreachable code.

I think this can give rise to a somewhat confusing change if the code is edited such that at least one path is open (so the code is now reachable), because all the other paths are still unreachable, and now they will be ignored. So, for instance, certain late variables could go from being possibly assigned to definitely not assigned, which could introduce some errors in subsequent code. The developer may not immediately understand how such a thing could happen.

I think the main point is that developers should be aware of the fact that the code is dead (dimmed text is good!). It will be a common experience that switching some code from dead to live makes a real difference, and then it's probably not a big problem that the changes can be somewhat complex or confusing.

[eernstg]

@stereotype441, is it fair to say that this issue can now be considered to be a request for adjustments to the feature specification, as mentioned here?

If so, should it then be transferred to the language repository?

[stereotype441]

@stereotype441, is it fair to say that this issue can now be considered to be a request for adjustments to the feature specification, as mentioned here?

If so, should it then be transferred to the language repository?

Yes, that makes sense. Thanks for noticing this! I'll transfer it.