Unsoundness escalation with patterns

[stereotype441]

Back in 2020, we put a bunch of effort into making sure that it the fundamentally unsound nature of programs running in weak mode is limited: in a weak mode program, an expression whose static type is the non-nullable type T might actually be null (due to the null coming from a legacy library), but if it's not null, it will definitely be an instance of type T. Similarly, an expression whose static type is the potentially nullable type T might be null even if the actual instatiated type of T at runtime is a non-nullable type. That is to say, the unsoundness around nulls in weak mode can't be "escalated" to unsoundness involving non-null values. See #1143 for background.

I've just realised that with the introduction of patterns, there are now new loopholes for unsoundness escalation that we haven't closed. For example:

// lib1.dart
// @dart=2.11

int secretNull() => null; // OK because this is a legacy library

// lib2.dart
// @dart=3.0

import 'lib1.dart';

T unsafeCast<T>(Object? o) {
  int i = secretNull(); // OK because static type is `int`, but secretly it's `null`!
  switch (i) {
    case int():
      o as T; // Promotes `o` to `T`
    default:
      // Flow analysis thinks this codepath is unreachable so it disregards it
  }
  // `o` still has type `T` because it's promoted in the "only" reachable code path.
  // So this `return` statement is allowed.
  return o;
}

Under the VM, this unsafeCast can be used to reinterpret any value of any type as a value of any other type. It's maximally unsound.

This technique can be used to escalate unsoundness using any construct that causes flow analysis to think a code path is unreachable when it's actually reachable due to a value unexpectedly being null, e.g. the switch statement above could be replaced with an if-case statement:

  if (i case int()) o as t;

or an if-case collection element:

  var _ = [if (i case int()) o as t];

or a switch expression:

  var _ = switch (i) { int() => o as t };

Ideas for what to do about this:

1. Ostrich algorithm. We could just decide that this situation is ok, because (a) the problematic scenario is probably very rare, and (b) we are actively discouraging people from running non-null-safe code in Dart 3.0.
2. Throw if unreachable codepaths are reached. Flow analysis could send signals to the CFE to indicate when it believes a code path is unreachable due to potentially unsound analysis; then, in weak mode builds, the CFE would then insert synthetic code that throws an exception. This would address the unsoundness by ensuring that the "unreachable" code paths really are unreachable. (This is similar to what we did to fix Flow analysis can be used to escalate mixed mode unsoundness #1143). I believe the complete set of necessary signals would be:
   • When a case in a switch statement is believed to match all possible values of the scrutinee that were not matched by previous cases (and hence the rest of the switch is considered unreachable); same for switch expressions. Note that this can happen even if the switch case has guards, because for better or worse, flow analysis understands that when true always matches.
   • When the case in an if-case is believed to match all possible values of the scrutinee (and hence the else codepath is considered unreachable).
   • When flow analysis presumes a switch statement to be exhaustive (because the scrutinee has an always-exhaustive type), and none of the switch cases contains a reachable break (and hence the code after the switch statement is considered unreachable).
   • When a top level pattern in a switch statement is believed to match no possible scrutinees (and hence the guard (if any) and case body are considered unreachable); same for switch expressions.
   • When the top level pattern in an if-case is believed to match no possible scrutinees (and hence the guard (if any) and then codepath are considered unreachable).
   • Additionally, the CFE would have to ensure that if all of the cases of a switch expression fail to match, an exception is thrown. (It's not sufficient to just let the switch expression evaluate to null, because there might be side effects on other variables that could be used for unsoundness escalation).
3. Elide "unnecessary" type tests, and add throws to cover the remaining soundness holes. This is the same as option 2, except that instead of the first two bullets, we'd have flow analysis signal to the CFE when it believes a pattern's required type is guaranteed to match; in this case, the CFE would ensure that no type test is performed. A null value might still slip through, but only in a code path that flow analysis believes to be reachable, so there would be no opportunity for unsoundness escalation. The remaining bullets would still be addressed in the same way as in option 2.
4. Weaken the flow analysis of patterns to match weak mode semantics. This would mean, for example, that flow analysis no longer believes that a scrutinee of type int is guaranteed to match the pattern int().

Option 1 obviously has the disadvantage that it's unsound. But it has the advantage that it behaves in a way that's intuitive to users (who won't be thinking about this unsoundness escalation issue). And, as a bonus, it doesn't require any additional coding work (or cherry picks), because it's what we accidentally already did!

Option 2 probably gives the best user experience; it allows the user to assume full soundness, and see that assumption reflected in static analysis; there may be occasional runtime exceptions due to nulls being injected by legacy libraries, but hopefully this won't be too surprising to users, since they know that this is a risk if they're running a mix of null-safe and legacy code. Unfortunately it's a nontrivial amount of work. However, it may bloat the size of the compiled executable due to all the synthetic throws.

Option 3 also gives a good user experience. It's possibly slightly worse in that e.g. int() can now sometimes match null. The advantage over option 2 is that it would bloat the code less. In fact, for fully sound programs, we could consider it an optimisation, since all the type tests that would be dropped are provably unnecessary in fully sound programs. Unfortunately it has similar implementation difficulty to option 2.

Option 4 is kind a the nuclear option and I don't like it. It's nontrivial to implement and it would result in a substantially worse user experience, because flow analysis would start considering code paths to be reachable that the user doesn't intend to be reachable (and that the user likely knows to be unreachable due to non-local analysis). But it has the advantage that it could be implemented entirely inside flow analysis, without any corresponding changes to the CFE.

Personally I favor option 1, because I think it's very unlikely that the situation will ever arise for real-world users. And the loophole will automatically close when we drop support for legacy code. But since option 1 is unsound I don't want to do it without a consensus that it's a level of unsoundness we're willing to accept.

CC @dart-lang/language-team @johnniwinther

[leafpetersen]

Amusingly, the VM seems to be optimizing that code based on an assumption of completely sound types, so it actually enters the case int() branch and throws an exception, thereby restoring soundness.... :). Probably not something we should be relying on though.

I believe we have specified for exhaustive switches that a default case is inserted to handle null when running in unsound null safe mode, so that should eliminate some of these cases as well.

In general, unless we see this actually cropping up (unlikely) I don't think we should spend time fixing this. Unsound mode is no longer fully supported, and will be removed entirely as soon as the last bits of internal code have been ported or deleted.

[johnniwinther]

The CFE already almost does Option 2: In weak/agnostic mode it inserts a throw in all switch expressions and in switch statements with an always-exhaustive type without a default case. Nothing is currently done for if-case statements.

[stereotype441]

Amusingly, the VM seems to be optimizing that code based on an assumption of completely sound types, so it actually enters the case int() branch and throws an exception, thereby restoring soundness.... :). Probably not something we should be relying on though.

Ah, so in effect the implementation does most of option 3. So I guess the question is whether we should cover the remaining soundness gaps (and add tests to make sure the functionality doesn't regress) or just leave things as they are.

[munificent]

I believe the proposal already specifies option 3. See Pointless type tests and legacy types. That change was made to the spec because of this related issue: #2619.

Personally, I'm fine with any blend of options 1 and 3. I don't think it makes sense to spend engineering time or increase code size because of a pair of features that almost no user will ever be able to combine.

[stereotype441]

I believe the proposal already specifies option 3. See Pointless type tests and legacy types. That change was made to the spec because of this related issue: #2619.

Aha, I'd forgotten about that! Thanks, Bob.

Personally, I'm fine with any blend of options 1 and 3. I don't think it makes sense to spend engineering time or increase code size because of a pair of features that almost no user will ever be able to combine.

Sounds good. Based on the discussion in Wednesday's language team meeting, it sounds like we are all on board with accepting the current situation, and not worrying about it further, so I'll close this issue.