Flow analysis can be used to escalate mixed mode unsoundness

[stereotype441]

For a very long time, I thought that the weakening of soundness in mixed mode was limited to nullability. That is, I thought that in mixed mode:

• within an opted out library, the result of evaluating an expression having static type T would always be a value whose runtime type is a subtype of T (because T contains the *s necessary to permit nulls in the appropriate places)
• within an opted in library, the result of evaluating an expression having static type T would always be a value whose runtime type is a subtype of T', where T' is formed from T by adding/removing *s to T in appropriate positions.

But that turns out not to be the case. The following program breaks soundness by allowing a String to be assigned to a variable of type int. Both the analyzer and CFE accept it without issuing any errors:

test.dart (opted out):

// @dart=2.6

import 'opted_in.dart';

T violateSoundness<T>(dynamic x) => accomplice<T>(x, null);

main() {
  String s = 'soudness, my old nemesis, we meet again!';
  int i = violateSoundness<int>(s);
  print(i.abs());
}

opted_in.dart:

// @dart=2.10

T accomplice<T>(Object? x, int i) {
  if (x is! T) {
    if (i is int) throw 0;
  }
  return x;
}

What's happening is that flow analysis considers the implicit "else" branch of if (i is int) to promote the type of i to Never, hence it considers it unreachable. So it considers the flow state after if (i is int) throw 0; to be unreachable, and hence it considers if (x is! T) { if (i is int) throw 0; } to promote the type of x to T. So it believes that the return x; at the end of accomplice is sound.

[stereotype441]

I believe the crux of the problem is that the inherent unsoundness of mixed mode is sufficient to cause flow analysis to incorrectly conclude that a flow control path is unreachable, and since it uses unreachability to discard control flow paths in joins, that means it can be made to conclude that any type promotion whatsoever survives beyond a join point.

I believe we could fix this by limiting the circumstances in which flow analysis concludes that code is unreachable. Flow analysis only concludes that code is unreachable when there is a clear transfer of control flow (e.g. an explicit return) or an expression has static type Never. We could change this so that it only concludes that code is unreachable when there is a clear transfer of control flow, or an expression has a type of Never and takes a form in which we are confident that null couldn't possibly leak in from an opted-out library (e.g. an explicit throw or a call to a static method declared in an opted-in library). We would also have to decide not to fix dart-lang/sdk#41985 (otherwise we would create similar loopholes with if (i != null)).

Side note: as an alternative, it is tempting to try to simply reduce the circumstances in which an expression can have a type of Never to just those circumstances where we are confident that the control flow is unreachable even in mixed mode. But I've been trying to think through this and I think there are too many holes in the mixed-mode type system to be able to do it. Beyond the possibility of the "factor" algorithm returning Never (causing a variable's type to be promoted to Never when in fact it might have a value of null), we have these circumstances, and possibly others I hvaen't thought of:

• An opted-in library might declare a variable of type Never Function(), but then an opted-out library might store a function having type Never* Function() in that variable.
• An opted-in library might declare an interface with a method having type Never Function(), but then an opted-out library might implement that interface with a method having type Never* Function().
• An opted-in library might declare a container class C<T> with a method having type T Function(), and instantiate it with a type argument of Never, but then pass it to an opted-out library that treats it as C<Never*> and stores a value of null in it; then control returns to the opted-in library, which calls the method and receives the null result.

[stereotype441]

@leafpetersen pointed out to me over IM that another possible solution would be to enforce soundness by having the compiler insert an implicit throw any time flow analysis determines that a code path is unreachable. Note that we would only have to do this in weak mode, and we wouldn't have to do it when the unreachability is due to explicit control flow, so hopefully the impact on code size could be kept reasonably low.

This would probably be a nicer experience for users than what I proposed in my comment above, because instead of saying to users "we're treating your obviously unreachable code path as 'technically reachable due to type system mumbo jumbo'", we'll just be respecting user intent by giving them a runtime check of a null safety condition that they're already asking for in their declared types. They probably won't even notice or care that the exception came from an esoteric corner of flow analysis.

[eernstg]

One main element of the soundness violation here is of course flow analysis. I agree that throwing on every occasion where an unreachable path is actually reached will safely remove any soundness issues caused by reaching it. But this may have a substantial cost in terms of the size of the generated code. Do we have an easy and safe way to eliminate most unreachable paths from this extra step, or would it apply to all unreachable paths?

Another thing is that the story currently says "dynamic type tests and type checks will behave as in legacy code", and that's no longer true because we have to add "... , and the very act of reaching certain locations will now throw (because they would be unreachable with sound null safety)". I'm not sure that's a very reassuring story for developers to work with.

But another element in the soundness violation is the fact that a declaration int i does not ensure that i is int evaluates to true in code with null safety in a mixed program (i is int can of course be false with int i in legacy code). And that is only possible because the value of i is null.

We're reserving the right to insert assertions doing dynamic null checks on parameters, and we're of course reserving the right to have a dynamic error for i.isEven in code with null safety when i is null.

This means that it is not inconsistent to throw because int i is null when we reach the type test.

So we could compile i is int to (i as int) is int. That is: In an is expression whose true or false continuation promotes a variable to Never, we perform the dynamic check which is justified by the static type of the variable at this point, thus ensuring that the computed reachability is sound.

I believe this allows for a simpler story: "An is expression may have a dynamic error because the left operand evaluates to null even though the expression has a strictly non-nullable type". It also seems easier to ensure that this approach doesn't cause program size to go up too much.

Don't you think this will catch all sources of soundness violations that have been raised here?

[stereotype441]

@eernstg

One main element of the soundness violation here is of course flow analysis. I agree that throwing on every occasion where an unreachable path is actually reached will safely remove any soundness issues caused by reaching it. But this may have a substantial cost in terms of the size of the generated code. Do we have an easy and safe way to eliminate most unreachable paths from this extra step, or would it apply to all unreachable paths?

I'm not too worried about the code size bloat issue. We would not have to apply it to all unreachable paths, only to the ones where flow analysis is imposing its own type-based notion of unreachability on top of the explicit control flow that's already present. AFAICT that only happens in four circumstances:

1. When a variable's type is promoted to Never by an is check. For practical real-world code, this should only happen if the user is deliberately trying to check for mixed mode unsoundness (e.g. by doing i is int on a variable whose static type is non-nullable int). I think this is going to be really weird and esoteric.
2. If we continue with the fix to Flow analysis should treat 's != null' as true if s is non-nullable sdk#41985, when a variable's type is promoted to Never by an == null check. Again, this should only happen in the weird and esoteric case where the user is deliberately trying to check for mixed mode unsoundness (e.g. by doing i != null on a variable whose static type is non-nullable int).
3. When there is an expression having a type of Never that isn't simply a throw expression. For practical real-world code, this should only happen if you're calling a method whose sole purpose is to throw an exception or exit the program (e.g. the fail method in package:test). I think this is rare enough outside of tests that we don't need to worry about it imposing a big code size cost.
4. When a switch statement covers all possible values of an enum except null. I suspect this is going to be the case that pops up most frequently, but it's so common to see users do an explicit throw statement in this circumstance that I can't imagine adding it automatically would be much worse in terms of code size.

...

So we could compile i is int to (i as int) is int. That is: In an is expression whose true or false continuation promotes a variable to Never, we perform the dynamic check which is justified by the static type of the variable at this point, thus ensuring that the computed reachability is sound.

I believe this allows for a simpler story: "An is expression may have a dynamic error because the left operand evaluates to null even though the expression has a strictly non-nullable type". It also seems easier to ensure that this approach doesn't cause program size to go up too much.

Don't you think this will catch all sources of soundness violations that have been raised here?

I think this is equivalent to what I said in cases 1 and 2 above, and I agree that it's unlikely to cause program size to go up too much. It doesn't catch everything, though. We still would need to cover cases 3 and 4 to close the soundness hole.

[ds84182]

Unless I'm mistaken, in mixed soundness mode shouldn't opted-in libraries do a runtime check in their entrypoints (like the covariant modifier)?

Essentially, accomplice should behave more like T accomplice<T>(Object? x, covariant int i as int?) so to opted-out code its T Function<T>(Object?, int?) and to opted-in code its T Function<T>(Object?, int)

The unsoundness certainly begins at the function entrypoint, because i is not an int.

[munificent]

4. When a switch statement covers all possible values of an enum except null. I suspect this is going to be the case that pops up most frequently, but it's so common to see users do an explicit throw statement in this circumstance that I can't imagine adding it automatically would be much worse in terms of code size.

This sparked an idle curiosity around which control flow constructs are most common. I happened to already have a scratchpad up to let me answer that easily so, going by the Dart SDK, Flutter repo, and 1,000 more recent pub packages, it's:

--- Statements (393495 total) ---
 296365 ( 75.316%): if        ****************************************************************************
  57061 ( 14.501%): if else   ***************
  19320 (  4.910%): for in    *****
  10032 (  2.549%): for ;;    ***
   6054 (  1.539%): switch    **
   4155 (  1.056%): while     **
    508 (  0.129%): do while  *
Files: 41385
Lines: 13036917

cc @pq and @bwilkerson for code-scraping example reasons. :)

[leafpetersen]

Unless I'm mistaken, in mixed soundness mode shouldn't opted-in libraries do a runtime check in their entrypoints (like the covariant modifier)?

Essentially, accomplice should behave more like T accomplice<T>(Object? x, covariant int i as int?) so to opted-out code its T Function<T>(Object?, int?) and to opted-in code its T Function<T>(Object?, int)

The unsoundness certainly begins at the function entrypoint, because i is not an int.

In this simple example, this could be caught (and we do provide an assertion mode which will stop this particular example). In general though, catching all unsoundness is both much harder, and in contradiction to our goal of making migration non-breaking to non-migrated code, and so we have chosen to make mixed mode execution unsound with respect to nullability. It is a problem though that flow analysis lets this nullability unsoundness be leveraged up to a full unsoundness, and so we will need to resolve this. My inclination at the moment is to add the appropriate unreachability assertions - I think this overall will be a positive for users anyway.

[eernstg]

@stereotype441 wrote:

We still would need to cover cases 3 and 4 to close the soundness hole.

Right, so throwing at unreachable locations is the most promising approach, and apparently not too costly.

[stereotype441]

Great! Elaborating a bit more on where throws would have to be inserted, here are some examples that illustrate what I'm thinking of. I think this covers all the soundness holes. Hopefully this can be a seed for someone (probably @munificent) to write up test cases.

promotionToNever(int i) {
  if (i is int) return; // Should throw if `i` is null
}
unnecessaryNullCheck(int f()) {
  if (f() != null) return; // Should throw if `f` returns null
}
unnecessaryIfNull(int f(), int g()) {
  return f() ?? g(); // Should throw if `f` returns null (rather than calling `g`)
}
unnecessaryIfNullAssign(List<int> x, int f()) {
  x[0] ??= f(); // Should throw if `x[0]` returns null (rather than calling `f`)
}
unnecessaryNullAwareAccess(int f()) {
  f()?.gcd(throw ...); // Should throw if `f` returns null
}
callReturningNever(Never f()) {
  f(); // Should throw if `f` completes normally
}
switchOnBool(bool b) {
  switch (b) {
    case true: return;
    case false: return;
  } // Should throw if the implicit `default` branch is taken
}
enum E { e1, e2 }
switchOnEnum(E e) {
  switch (e) {
    case E.e1: return;
    case E.e2: return;
  } // Should throw if the implicit `default` branch is taken
}

Notes:

• Test cases for promotionToNever should be sure to also cover the form i is! int.
• Test cases for unnecessaryNullCheck should be sure to also cover the forms null != f(), f() == null, and null == f().
• Technically it's not necessary for is and == null checks to throw if they don't get used for branching (e.g. bool b = i is int;), but probably we should do so anyway for consistency (and I think it's easier to implement that way anyhow).
• Test cases for unnecessaryIfNullAssign should be sure to cover various different forms that can appear on the LHS of ??=, especially those involving null shorting.
• Test cases for callReturningNever should be sure to cover instance method calls, static method calls, top level function calls, local function calls, operator invocations, and various kinds of getter invocations.
• Test cases for callReturningNever should cover cases where the call isn't a statement, e.g. List<Never> x = [f()];

Regarding how to implement this (CC @johnniwinther), I'm thinking that we make the following modifications to the FlowAnalysis API:

• For promotionToNever, isExpression should return a boolean indicating whether the implementation should throw if the "is" check is not satisfied.
• For unnecessaryNullCheck, equalityOp_end should return a boolean indicating whether the implementation should throw if the operands are equal.
• For unnecessaryIfNull and unnecessaryIfNullAssign, ifNullExpression_rightBegin should be given the type of the LHS as an additional argument, and it should return a boolean indicating whether the implementation should throw if the LHS evaluated to null. (Note: we could just let the CFE handle this all by itself, but I want to improve flow analysis so that it takes into account the type of the LHS, so this is a step in that direction).
• For unnecessaryNullAwareAccess, nullAwareAccess_rightBegin should be given the type of the target as an additional argument, and it should return a boolean indicating whether the implementation should throw if the target evaluated to null. (Note: we could just let the CFE handle this all by itself, but I want to improve flow analysis so that it takes into account the type of the target, so this is a step in that direction).
• For callReturningNever, this should be handled entirely in the CFE, in the logic where it decides whether to call handleExit based on an expression type.
• For switchOnBool and switchOnEnum, these should be handled entirely in the CFE, in the logic where it decides whether to pass isExhaustive=true to switchStatement_end.

And then it would be up to the CFE and back end teams to decide whether to implement the behaviors in the back end or by transforming the kernel. WDYT?

[stereotype441]

Side note: currently flow analysis ignores is checks where the LHS is anything other than a variable. So if i is a local variable with static type int, the "false" branch of i is int is considered unreachable; but if f is a function returning int, the "false" branch of f() is int is considered reachable. Maybe for consistency they both should be considered unreachable. If so, then the promotionToNever case above would have to be generalized to arbitrary expressions, e.g.:

promotionToNever(int f()) {
  if (f() is int) return; // Should throw if `f` returns null
}

[johnniwinther]

The plan in #1143 (comment) sounds good.

[stereotype441]

@munificent's test cases have landed; I will work on the flow analysis logic described in #1143 (comment) today.

[stereotype441]

For posterity, here's a sharp edge of the unnecessaryNullAwareAccess case that we'll need to be careful about:

T accomplice<T>(Object? x, int i) {
  i?.hashCode.remainder(x is! T ? throw 0 : 1);
  return x;
}

Since i has a non-nullable type, flow analysis will conclude that the ?. cannot null short. Therefore it will assume that x is! T ? throw 0 : 1 is always part of the control flow path, so it will promote the type of x to T, allowing the return statement without a cast. But at runtime, when a null value is passed for i, the ?. will null short, so execution will proceed directly to the return statement and we'll once again have a full soundness violation.

This case is important because it illustrates that when flow analysis believes a ?. cannot null short, we must insert an implicit null check even if the method being called (hashCode in this case) exists on Object. Similar situations could arise if there's an extension on int?.

I'll add some test cases to make sure this is covered.