#3057. Add pattern assignment cases to C-style for tests

[sgrekhov]

No description provided.

[eernstg]

Looks good!

A couple of tests are somewhat tricky: The description says that something is 'reachable', but I don't think the given test would actually detect whether it is reachable or unreachable.

Come to think of it, the current version of the tests could work after all because the correct analysis will give rise to no errors (more precisely: no diagnostics), and the buggy behavior that I'm hunting would give rise to a 'dead code' warning.

Anyway, please take another look and consider the issue that I described.

[eernstg]

I think I might have overlooked a thing here in the first iteration on this test. ;-)

The false literal isn't actually affecting any observable behavior, I think.

First, there is no notion of "definitely reachable", so there's no difference between "will definitely reach this point every time this function is called" and "might reach this point if we're incredibly lucky".

This means that we can't test that any given piece of code is "definitely reachable", we will have to go for "is possibly reachable" no matter what the test is like in detail.

Next, it implies that there is no difference between the treatment of the code that may be executed after the for statement when the condition is false and when it is any boolean expression whose value might be false. This makes the reference to false in the description somewhat misleading.

Finally, the analysis of i = 42; i; is the same when those two statements are reachable (via something that we could call the "invisible else branch of the for statement") and when they are not reachable (for whatever reason). In both cases the statement i; is accepted with no errors because i = 42 is guaranteed to have been executed before we reach i;.

I think the best way to test reachability could be to remove the code which is concerned with i and change the return type of test1 to some non-void/non-dynamic type, and expect an error because there is no return e; before the end of the function.

[eernstg]

Alternatively, the for statement could simply be removed because it doesn't actually matter. But this would probably yield a test which is already included somewhere else in co19.

[eernstg]

If the i related code is removed then we probably wouldn't need the new cases in test2-3-4.

[sgrekhov]

The test is testing that after(N) = inheritTested(join(false(C), unsplit(break(S))), after(U)). Not most obvious statement for me :) As far as I understand it the meaning is that in case of false(C) then after(N) doesn't depend from what's going on in S and U. So, here I'm tryig to test that in case of for(;false;U) S; reachability of after(N) doesn't depend on U and S. What if we'll change the test to be like:

test1() {
  late int i;
  if (2 > 1) {
    for (;false;) {
      return;
    }
    i = 42;
  }
  i; // Possibly assigned.
}

In case of for (;true;) ... i become definitely unassigned in this test. WDYT will it be a valid test?

[eernstg]

Right, after(N) = inheritTested(join(false(C), unsplit(break(S))), after(U)) is convoluted.

It specifies that the flow model M after the for statement is join(false(C), unsplit(break(S)) where we have taken the 'types of interest' for each variable in after(U) and added to the types of interest for the same variable in M (and skipped variables in after(U) that aren't in M).

In other words, M is exactly join(false(C), unsplit(break(S)) as long as we ignore the types of interest. In this test U is empty, so it doesn't contribute any types of interest, anyway. So we just need to consider the join.

join combines the information in two flow models. It can only be used when the reachability stacks are identical below the top (that is, they must agree precisely on reachability except for the top of the stack), and it creates a new reachability stack which is (top1 || top2) :: commonTail, that is, it's reachable if one or the other branch is reachable.

In this case false(C) == before(N) — which is reachable, so the join is reachable, too. We basically just need to understand how unsplit(break(S)) can add information to before(N). The unsplit part manages reachability, but we already know that the join is reachable. So we just need to understand break(S). There are no break; statements in S, so we need to know how join works on the empty list of operands. This is not documented, as far as I can see. (As we can see below it's unsound if that empty join is reachable, so it must be unreachable.)

Anyway, we would clearly expect the flow analysis to consider after(N) to be a reachable flow model, which is the reason why I'm suggesting to test this as follows:

int test1() {
  for (;false;) {
    return;
  }
  // Error: reached the end of the function body with no `return anInt;`.
}

The description could then say that we're testing that after(N) is reachable when the condition is a literal false.

It would also be possible to test for (;true;) ... based on the fact that false(C) is unreachable, so join(false(C), unsplit(break(S))) would only be reachable if unsplit(break(S)) is reachable, which means that break(S) must have a reachability stack of the form true :: true :: tail.

int test1() {
  for (;true;) {
    return;
  }
  // OK to not have a `return someInt;` here.
}

About this test:

test1() {
  late int i;
  if (2 > 1) {
    for (;false;) {
      return;
    }
    i = 42;
  }
  i; // Possibly assigned.
}

Yes, this would also succeed if i = 42; is considered reachable, and fail if it is considered unreachable.

I'm thinking about this as a 'possibly assigned' test rather than a 'reachable' test, but I do recognize that it relies on reachability as well.

Also, it fixes the issue with the first version of this test where the outcome would be a success both in the case where i = 42; is considered reachable and in the case where it is considered unreachable.

Tricky stuff! ;-)

[sgrekhov]

Thank you for the detailed analysis. Updated. PTAL.

It specifies that the flow model M after the for statement is join(false(C), unsplit(break(S)) where we have taken the 'types of interest' for each variable in after(U) and added to the types of interest for the same variable in M (and skipped variables in after(U) that aren't in M).

It's an interesting about type of interest. It can be tested (in a separate PR).

class S {}
class T extends S {
  void foo() {}
}

test1() {
  S s = S();
  for (;false;) {
    if (s is T) {} // make `T` a  type of interest
  }
  s = T();
  s.foo(); // Not an error.
}

test2() {
  S s = S();
  for (;false; s is T) {
  }
  s = T();
  s.foo(); // Error. Not an issue, result of the conservativeJoin()? Same as https://github.com/dart-lang/sdk/issues/60320 ?
}

Is this an expected that there is an error in test2()?

[eernstg]

The for statement rule actually justifies that S is unreachable: before(S) = split(true(C)) and true(C) is unreachable. So after(S) would also be unreachable, and so is continue(S) (because there are no continue; statements). So before(U) is unreachable, and hence U (that is s is T) is dead code.

This justifies the error at the end, in the line with a long comment.

[sgrekhov]

The for statement rule actually justifies that S is unreachable: before(S) = split(true(C)) and true(C) is unreachable. So after(S) would also be unreachable, and so is continue(S) (because there are no continue; statements). So before(U) is unreachable, and hence U (that is s is T) is dead code.

This justifies the error at the end, in the line with a long comment.

After the testing and rereading the spec I think that there is another reason of such behavior. According to the spec:

We say that at type T is a type of interest for a variable x in a set of tested types tested if tested contains a type S such that T is S, or T is NonNull(S).

Definition of tested is:

tested is a set of types which are considered "of interest" for the purposes of promotion, generally because the variable in question has been tested against the type on some path in some way.

I think it is too general definition but the key point here is "for the purposes of promotion". So s is T itself doesn't promote anything. Therefore:

s = S();
s is T;
s = T();
s.foo(); // Error. There were no promotion above

And for the same reason we are getting an error in case of for (;false; s is T).... To get the promoution we should do something like:

  S s = S();
  int i = 0;
  for (;false; s is T ? i++ : i += 2) {}
  s = T();
  s.foo();  // Ok, now accepted

Please correct me the above is wrong. Otherwise it'd be nice to test type of interest in all of the places where we should have a promotion.

• instance check If N is an expression of the form E1 is S where the static type of E1 is T then:
  ...
  Otherwise:
• Let true(N) = promote(E1, S, after(E1))
• Let false(N) = promote(E1, factor(T, S), after(E1))

As far as I understand to get a promotion after the type check we should have true(N) or false(N) branch (in case of plain s is T; the both branches are empty that's why we have no promotion). But we have the promotion, for example, in the following case:

s = S();
s is T && 2 > 1; // `true(N)` branch added to `s is T`
s = T();
s.foo(); // Now Ok!

So to test types of interest we should check all of the places in the flow analysys spec where true(N), false(N) or promote() occurs. s = T(); s.foo(); shouldn't produce an error after it.

Please correct me if I'm wrong.

[eernstg]

So s is T itself doesn't promote anything

The flow models associated with the evaluation of the expression s is T do not agree, but both true(N) and false(N) may have a 'promoted' stack for s which reflects the newly obtained information about the run-time type of s.

I do think it's fair to say that "s is T can promote s in the true continuation or the false continuation, or both". Of course, it also adds T to the set of tested types for s.

s = S();
s is T;
s = T();
s.foo(); // Error. There were no promotion above

That's a bug! The flow model after(N) where N is the node that contains s is T should be obtained as join(true(N), false(N)), and the true(N) flow model should consider T to be a type of interest for s. The factor function might makes some other type a type of interest for s as well, but that wouldn't invalidate the fact that T is of interest in subsequent code.

Given that T is a type of interest when s = T() is reached, this assignment should promote s to T.

It has probably never been reported because it is a pointless statement: We're computing a boolean value and discarding it, and there are no side effects. In any case, I do believe that this is a bug.

To get the promoution we should do something like:

 S s = S();
 int i = 0;
 for (;false; s is T ? i++ : i += 2) {}
 s = T();
 s.foo();  // Ok, now accepted

In this case the type test s is T is again in dead code, but this is not discovered during the inheritTested stop, so T is considered to be a type of interest for s when we reach s = T();, which will then promote s to have type T.

As far as I understand to get a promotion after the type check we should have true(N) or false(N) branch (in case of plain s is T; the both branches are empty that's why we have no promotion).

No, the point is that the true and false branches are joined, it wouldn't make a difference if one or both of those branches had some code in them (as long as that code doesn't interfere with the status of s in some other way, and as long as the branches aren't unreachable).

s = S();
s is T && 2 > 1;
s = T();
s.foo(); // Now Ok!

Looks like the bug that came up above doesn't apply here, probably because the true continuation is needed for the flow analysis of the rest of the expression.

[eernstg]

@stereotype441, do you agree that the following is a bug?:

class S {}

class T extends S {
  void foo() {}
}

void main() {
  var s = S();
  s is T;
  s = T();
  s.foo(); // Error, so `T` was not a type of interest, but it should be.
}

[stereotype441]

@eernstg

@stereotype441, do you agree that the following is a bug?:

class S {}

class T extends S {
  void foo() {}
}

void main() {
  var s = S();
  s is T;
  s = T();
  s.foo(); // Error, so `T` was not a type of interest, but it should be.
}

Yes, good catch! I've filed dart-lang/sdk#60479 to track it. And nice job with the analysis above; I walked through the code in the debugger and confirmed that what's happening is exactly what you surmised.