co19/LanguageFeatures/nnbd/flow-analysis/reachability_break_* fail

[scheglov]

I see new co19 tests that exercise functionality for which I cannot find specification. @leafpetersen Is it in the flow analysis spec and I don't look well?

co19/LanguageFeatures/nnbd/flow-analysis/reachability_break_A01_t01
co19/LanguageFeatures/nnbd/flow-analysis/reachability_break_A01_t03
co19/LanguageFeatures/nnbd/flow-analysis/reachability_break_A01_t07
co19/LanguageFeatures/nnbd/flow-analysis/reachability_break_A02_t01
co19/LanguageFeatures/nnbd/flow-analysis/reachability_break_A02_t02
co19/LanguageFeatures/nnbd/flow-analysis/reachability_break_A02_t04
co19/LanguageFeatures/nnbd/flow-analysis/reachability_break_A03_t03
co19/LanguageFeatures/nnbd/flow-analysis/reachability_break_A03_t04

co19/LanguageFeatures/nnbd/flow-analysis/reachability_continue_A01_t07
co19/LanguageFeatures/nnbd/flow-analysis/reachability_continue_A02_t01
co19/LanguageFeatures/nnbd/flow-analysis/reachability_continue_A02_t02
co19/LanguageFeatures/nnbd/flow-analysis/reachability_continue_A03_t03

An example of break in the test:

main() {
  late int i;
  for (;;) {
    break;
    i = 42; // Variable is initialized in a dead code. This leaves it definitely unassigned
  }
  i; // It is an error to read a local late variable when it is definitely unassigned.
//^
// [analyzer] unspecified
// [cfe] unspecified
}

An example of continue in the test:

main() {
  late int i;
  int j = 0;
  while (j++ < 3) {
    continue;
    i = 42; // Variable is initialized in a dead code. This leaves it definitely unassigned
  }
  i; // It is an error to read a local late variable when it is definitely unassigned.
//^
// [analyzer] unspecified
// [cfe] unspecified
}

[leafpetersen]

The errors around definitely assigned/unassigned late variables were landed here .

[scheglov]

@leafpetersen Oh, sorry, I did not describe the issue fully. I know that we should report late definitely unassigned variables. But I don't see where reachability of an assignment should be takes into account.

It might be also that we just don't have all specification for definitely unassigned variables, and we implemented it wider than the spec says. For while statement we have after(N) = join(false(E), unsplit(break(S)), but in implementation we also do joinUnassigned(after(N), afterBody), and mark anything potentially assigned in the body, even after break, as not definitely unassigned. Because break might be conditional. So, this code is OK:

void f(bool c) {
  late v;
  while (c) {
    if (c) break;
    v = 0;
  }
  v;
}

But these co19 test check that if break is unconditional, and there is an assignment after it, we keep variables as definitely unassigned.

[leafpetersen]

But I don't see where reachability of an assignment should be takes into account.

@scheglov I think there are two questions here. The first is whether reachability of an assignment should be taken into account, and my expectation was certainly that it would. If I have:

void foo() {
  var x;
  if (b) {
    x = 3;
    return;
  } 
  //use(x);
}

then my initial expectation would be that x is treated as definitely unassigned after the conditional. It doesn't have to be that way, but it feels weird not to use this obviously true information. Are you saying that we don't treat x as definitely unassigned there?

The second question is around what assignments we treat as being reachable. Since we do single pass flow analysis, we have to make lots of approximations. I have less of an opinion there.

So is this issue about whether we take reachability into account at all, or about what assignments are considered reachable?

[scheglov]

The issue is what assignments make a variable not definitely unassigned.

We definitely take reachability into account.
For if statement we do merge and discard the branch that is not reachable.
So, this code has an error.

void foo(bool b) {
  late x;
  if (b) {
    x = 3;
    return;
  }
  x;
}

The following code, with my understanding of the flow analysis spec, would keep v definitely unassigned. But we implemented marking any variables not definitely unassigned at the end of the body, as not definitely unassigned after the loop (while, for). This is an issue_1 in the spec by itself.

void f(bool c) {
  late v;
  while (c) {
    if (c) break;
    v = 0;
  }
  v;
}

This leads to failures with co19, where an unconditional break or continue is tested as making all subsequent assignment not existing. Which is not unreasonable, but is not specified. This is an issue_2 that depends on issue_1.

[leafpetersen]

Sorry, I'm just paging this back in, but I'm still not entirely sure I understand where we are. I think what you are saying is that in your last example, v is assigned in the loop, and so on entry to the loop we mark it as potentially assigned in the conservative join, and hence it is potentially assigned after the loop, is that correct? If so that seems reasonable and I agree the tests should be changed. Is there a spec change required to match this?

cc @stereotype441 @eernstg

[eernstg]

@scheglov wrote:

This leads to failures with co19, where an unconditional break
or continue is tested as making all subsequent assignment not
existing.

The flow analysis spec sets after(N) = unreachable(before(N)) for a break and a continue statement, which I would expect allows the analysis to conclude that the code following the break/continue is dead (and we do get the expected 'dead code' hint). I don't see a need to update the spec in this respect.

But the issue seems to arise because the analysis is

marking any variables not definitely unassigned at the end of the
body, as not definitely unassigned after the loop (while, for).

This basically implies, in spite of whatever is already known, that the end of the body is potentially reachable.

@stereotype441, I think the spec might need to be updated to have the following for while statements:

Let after(N) = join(false(E), unsplit(join(break(S), after(S)))

such that it includes the possible normal completion of S, rather than only breaking completions. A similar change would be needed for do-while statements, and for statements (though not yet in the spec) should be treated similarly. I'm not sure why while has an unsplit and do-while doesn't, but that's a separate issue. WDYT?

[stereotype441]

@eernstg

@scheglov wrote:

This leads to failures with co19, where an unconditional break
or continue is tested as making all subsequent assignment not
existing.

The flow analysis spec sets after(N) = unreachable(before(N)) for a break and a continue statement, which I would expect allows the analysis to conclude that the code following the break/continue is dead (and we do get the expected 'dead code' hint). I don't see a need to update the spec in this respect.

Agreed

But the issue seems to arise because the analysis is

marking any variables not definitely unassigned at the end of the
body, as not definitely unassigned after the loop (while, for).

This basically implies, in spite of whatever is already known, that the end of the body is potentially reachable.

This is no longer the case. This logic was removed in a1fc2ea, as part of fixing #42301.

@stereotype441, I think the spec might need to be updated to have the following for while statements:

Let after(N) = join(false(E), unsplit(join(break(S), after(S)))

such that it includes the possible normal completion of S, rather than only breaking completions. A similar change would be needed for do-while statements, and for statements (though not yet in the spec) should be treated similarly.

@eernstg I don't think this is necessary. There is no control flow path directly from the bottom of the "while" loop to the code after the while loop; rather, the's an unconditional jump from the bottom of the while loop back up to the top, and this is already modeled by the conservativeJoin we do when analyzing before(E); this is what marks i as possibly assigned, and that state carries through to after(N). Walking through it for the example:

main() {
  late int i;
  int j = 0;
  while (j++ < 3) {
    continue;
    i = 42;
  }
  i;
}

The rules are:

• while statement: If N is a while statement of the form while (E) S then:
  • Let before(E) = conservativeJoin(before(N), assignedIn(N), capturedIn(N)).
  • Let before(S) = split(true(E)).
  • Let after(N) = join(false(E), unsplit(break(S))

So the analysis (considering just i) is:

• before(N) = {i: definitely unassigned}
• before(E) = conservativeJoin({i: definitely unassigned}, {i}, {}) = {i: possibly assigned}
• true(E) = {i: possibly assigned}
• false(E) = {i: possibly assigned}
• before(S) = split({i: possibly assigned}) = {i: possibly assigned}
• after(S) = {unreachable, i: definitely assigned}
• after(N) = join({i: possibly assigned}, unsplit({unreachable})) = {i: possibly assigned}

Another way to state this would be: we don't want the algorithm to have to use multiple passes or backtracking, therefore when we reach the top of the loop, and we have a backwards flow control edge coming from the bottom of the loop, we have to make a conservative guess about what might be assigned within the loop (this is the job of conservativeJoin). So we conservatively guess that any assignment statement inside the loop might or might not get executed on that control path; hence we assume that the state coming in on that backwards edge is that i is possibly assigned. Later, we figure out that the assignment to i is unreachable, but by then it is too late. We can't un-do our previous wrong assumption without backtracking or a second pass. Fortunately the conservative assumption was a sound one, so we just have the minor annoyance of failing to notice that the loop can't assign to i.

I'm not sure why while has an unsplit and do-while doesn't, but that's a separate issue. WDYT?

The reason while has unsplit(break(S)) in after(N) is because in a while loop, there is a flow control split prior to entry into the loop body (because the test happens before entry to the loop, so the loop body might not get executed at all); we need to un-split any flow control that exits the loop body via break before merging it into the final post-loop control flow. Whereas do while's after(N) just has break(S) because in a do while loop, there is no control flow split before the loop body, so there is no need to un-split the control flow afterwards.

[eernstg]

Great explanation, @stereotype441, thanks! But this means that there is no reason to assume that the flow analysis will change in such a way that it will produce the more precise result. Also, I believe that the spec doesn't have to change.

@sgrekhov, this means that the tests need to take this approximation in the flow analysis into account for code in loops.