Unsound promotion for async functions and assignment outside a closure

[lrhn]

The code:

FutureOr<void> foo(void Function(void Function(Object?)) callback) {
  Completer<void>? completer;
  var wasSync = false;
  callback((value) {
    if (completer != null) {
      completer.complete(value);
    } else {
      wasSync = true;
  });
  if (wasSync) return;   
  completer = Completer();
  return completer.future;
}

analyses and compiles with no errors. The completer != null check inside the closure promotes completer even though it's assigned outside of the closure.

I think that's actually sound, because the assignments outside of the closure cannot occur while the closure is running, not unless they're inside another closure, and that would disable promotion.

However, this promotion is also applied to asynchronous functions, across asynchronous gaps, and that is not sound.

Example:

import "dart:async";

void main() {
  void Function(Object) f = (_) {};

  foo((void Function(Object) c) => f = c, () => f(42));
}

void foo(
  void Function(void Function(Object o)) callback,
  void trigger(),
) {
  Completer<Object>? completer;
  print("unset");
  callback((Object value) async {
    if (completer != null) {
      print("checked");
      await 0;
      print("uses");
      completer.complete(value);
      print("used");
    }
  });
  completer = Completer();
  print("set");
  completer.future.then(print); // Sanity check.
  trigger();
  completer = null;
  print("unset");
}

This code runs and prints:

unset
set
checked
unset
uses

and then fails when it tries to call complete on null.

Assuming the synchronous promotion is deliberate, and we believe it's sound, then that promotion needs to be disabled if there is any asynchronous gap between the check and the use.

The only thing that makes the promotion sound is that the code in the surrounding function cannot run while the inner function does, and that's only true if the inner function is synchronous from check to use.

[stereotype441]

Wow, @lrhn! congratulations on finding a soundness violation that's existed in flow analysis since its inception! I'm amazed how long this bug has existed without anyone realizing it.

I consider soundness issues like this one to be quite high in priority. I'll give it my full attention ASAP.

[lrhn]

I mentioned that for soundness, it's also a problem if the outer function is asynchronous, not only if the inner one is.
It's not well-behaved code, it misuses synchronous completion of a future, but it's possible to be unsound.

import "dart:async";

void main() async { // Outer function is async.
  Completer<void> cheating = Completer.sync();
  int? value;
  print("unset");
  scheduleMicrotask(() { // Inner function is not async.
    if (value != null) {
      print("checked");
      cheating.complete(null);
      print("uses");
      try {
        print("used: ${value.toRadixString(16)}");
      } catch (e) {
        print(e);
      }
    }
  });
  value = 42;
  print("set");
  print("outer paused");
  await cheating.future;
  print("outer resumed");
  value = null;
  print("unset");
}

Any await is a re-entrancy point that can happen at any time.

It's probably sound if the outer function is synchronous (has no async gap anywhere, and probably not any yields either) and the inner function has no async gap between check and use, because then it's impossible to run code from the outer function between the two.

[stereotype441]

Ok, I spent a bunch of time thinking through this and I have a design for a fix. Let me see if I can explain it, and then we'll see if @lrhn can poke holes in it 😃

Terminology

First, in thinking about this issue I’ve found myself wanting to use two new pieces of terminology that I haven’t previously used in the flow analysis spec or implementation:

• An order block is any of the following:

  • The body of the whole top level function or method for which type inference is being performed,

  • The body of a function expression,

  • The body of a local function declaration,

  • Or the initializer of a late local variable.

  Note that order blocks are always properly nested, so we can use tree terminology to refer to their relationships (e.g., an order block's descendants are all the order blocks that are textually contained within it).

  (The flow analysis spec and implementation refer to order blocks as function expressions, but I no longer like that, because it makes it too easy to forget about late variable initializers.)

• Each local variable has a notion of promotion safety that varies with control flow. When a local variable is in the promotion-safe state, the set of expressions whose execution might mutate it is easy to recognize (e.g., v = ..., v++, etc). When a local variable is promotion-unsafe, we assume that execution of any expression might mutate it. All local variables are initially promotion-safe, but various events can cause them to become promotion-unsafe. For example, creating a closure that write-captures a local variable causes it to become promotion-unsafe, because once the closure has been created, it might at any point get called, causing the variable’s value to change.

  (The flow analysis spec calls promotion-unsafe local variables “write-captured”, but I no longer like that, because it makes it too easy to forget that there are other ways a local variable can become unsafe to promote, other than write-capturing it).

Current (buggy) behavior

Ok, to set the stage, here is how flow analysis currently handles local variables that are read or written in a different order block than the one they're declared in:

• When flow analysis’s depth-first traversal of the AST enters an order block:

  • Any local variables that are written anywhere within the order block or one of its descendants, and declared in an ancestor, are placed into the promotion-unsafe state (these variables are immediately demoted to their declared types, and can never be promoted again), and have their “unassigned” bit cleared (they can thereafter be “possibly assigned” or “definitely assigned”, but never again “definitely unassigned”).

  • Then a snapshot of the state of flow analysis is pushed onto a stack.

  • Then, any local variables that are write-captured anywhere (meaning they are written within an order block that doesn’t also contain their declaration site) are placed into the promotion-unsafe state.

  • And any non-final variables that are written anywhere (other than at their initialization site, if any) are demoted to their declared types and have their “unassigned” bit cleared.

• When flow analysis’s depth-first traversal of the AST exits an order block:

  • The state of flow analysis is restored based on the snapshot that was pushed when entering the order block.

Expanding on Lasse's examples

Example A (from the initial bug report):

import "dart:async";

void main() {
  void Function(Object) f = (_) {};

  foo((void Function(Object) c) => f = c, () => f(42));
}

void foo(
  void Function(void Function(Object o)) callback,
  void trigger(),
) {
  Completer<Object>? completer;
  print("unset");
  callback((Object value) async {                 // (A1)
    if (completer != null) {
      print("checked");
      await 0;                                    // (A2)
      print("uses");
      completer.complete(value);
      print("used");
    }
  });
  completer = Completer();
  print("set");
  completer.future.then(print); // Sanity check.
  trigger();                                      // (A3)
  completer = null;
  print("unset");
}

In this example, flow analysis thinks that completer is promotion-safe inside the function expression that starts at (A1). But it isn’t, because the await expression at (A2) causes execution of foo to resume at (A3), whereupon it sets completer to null.

Example B (from #61698 (comment))

import "dart:async";

void main() async { // Outer function is async.
  Completer<void> cheating = Completer.sync();
  int? value;
  print("unset");
  scheduleMicrotask(() {                          // (B1)
    if (value != null) {
      print("checked");
      cheating.complete(null);                    // (B2)
      print("uses");
      try {
        print("used: ${value.toRadixString(16)}");
      } catch (e) {
        print(e);
      }
    }
  });
  value = 42;
  print("set");
  print("outer paused");
  await cheating.future;                          // (B3)
  print("outer resumed");
  value = null;
  print("unset");
}

In this example, flow analysis thinks that value is promotion-safe inside the function expression that starts at (B1). But it isn’t, because the call to Completer.complete at (B2) causes execution of main to resume at (B3), whereupon it sets value to null.

General fix strategy

Both examples contain three crucial ingredients:

• A function expression F.

• A local variable V that’s declared in the outer function and read-captured by F.

• An expression E inside F that doesn’t textually contain a write to V, but whose execution mutates V (demonstrating that at this point in the code, even though flow analysis considers V to be promotion-safe, it’s actually promotion-unsafe).

All the fixes I’ve been able to think of involve either:

• Teaching flow analysis to recognize E as a kind of expression that might mutate V. (Hence, it’s sound for flow analysis to continue considering V to be promotion-safe inside F.)

• Teaching flow analysis to consider V to be promotion-unsafe inside F.

Note that for example B, our only choice is to consider V to be promotion-unsafe inside F, because there’s no reliable way to recognize E as potentially mutating (e.g., cheating could be a global variable and E could then be an invocation of any function, getter, or method that executes cheating.complete(null)). But for example A, I believe we can make a more targeted fix.

Detailed fix proposal

When flow analysis’s depth-first traversal of the AST leaves an await expression:

• Considering all local variables that are read captured by the current order block (meaning local variables that are read within it or one of its descendants¹, but declared outside of it): any of them that are written anywhere (other than at their initialization site, if any) are demoted to their declared types and have their “unassigned” bit cleared.

  This addresses example A by causing flow analysis to recognize an await expression as a kind of expression that might mutate local variables that are read-captured by the current closure. So it is sound to continue considering those variables promotion-safe even in the presence of await expressions.

When flow analysis’s depth-first traversal of the AST enters an order block, after a snapshot of the state of flow analysis is pushed onto a stack:

• Any non-final async-unsafe variables (defined below) that are read-captured by the order block are placed into the promotion-unsafe state, and have their “unassigned” bit cleared.

• An async-unsafe variable is any local variable for which there exists a flow control path containing the declaration of that variable, followed by an await expression, followed by a write to that variable.²

  This addresses example B by causing flow analysis to consider V to be promotion-unsafe inside F.

The only question that remains is, how do we compute the set of async-unsafe variables? I believe we can do so as part of the “assigned variables” phase of flow analysis (a pre-traversal of the entire AST of the top level function or method that recognizes the nesting of writes to local variables within loops and order blocks). When this pre-traversal leaves an await expression:

• Any variables that have been declared so far in the current order block are marked as potentially async-unsafe. Thereafter, when a write to a local variable is encountered, if that variable is in the async-unsafe state, it is marked as async-unsafe.

  This recognizes patterns like var x; await ...; x = ...;.

• Considering each loop in the current order block that encloses the await expression, if a write to a local variable has already been seen inside the loop, and the variable’s declaration is inside the current order block but outside the loop, the variable is marked as async-unsafe.

  This recognizes patterns like var x; while (...) { x = ...; await ...; }.

Note: since the front end does the assigned variables phase during parsing, some special care may have to be taken with for-loops, because they are parsed in an order that doesn’t match flow control order (the updates are parsed before the loop body). I will investigate this.

What do you think?

Ok, @lrhn (or anyone else on @dart-lang/language-team who is interested), let me know what you think. Do you agree that this addresses the problem? Does it seem like a reasonable approach?

Since the issue has gone undected for so many years, I'm not going to consider this super-urgent. I'll try to wait at least a week for comments before I start coding up a solution.

Footnotes

1. Implementation note: it’s not strictly necessary to check whether the variable is read within the current order block or one of its descendants; this is purely a performance optimization. The reason is that since the flow analysis state is restored at the end of the order block, the only flow analysis state changes that matter within the order block are changes to variables that are read within it or one of its descendants. ↩

2. Implementation note: if a variable is write-captured anywhere, it’s not necessary to consider it, because logic already exists to place those variables into the promotion-unsafe state on entry to an order block. Therefore, we only need to consider non-write-captured variables, and we only need to think about flow control paths within the order block that declares the variable. ↩