[Proposal]: Require await to apply nullable postconditions to task-returning calls

[RikkiGibson]

• Speclet: inline
• Discussion: Require await to apply nullable postconditions to task-returning calls #8678

Summary

Assume that nullable postcondition attributes such as MemberNotNull only apply when Task-returning calls are directly awaited. Adjust analysis of implementations to permit postconditions to be fulfilled after an await boundary.

var c = new C();
await c.M();
c.F.ToString(); // ok

class C
{
    public string? F;

    [MemberNotNull(nameof(F))]
    public async Task M()
    {
        var result = await WebServiceCall(); // ok
        F = result.Value;
    }
}

Motivation

Users are requesting the ability to specify postconditions which are only fulfilled after a task-returning method is awaited. We're seeing a relatively high amount of engagement (upvotes and thumbs up) on this compared to many other issues in the nullable space.

A community member observed that there are very few usages of [MemberNotNull] on async methods in open source code, which bodes well for the possibility of breaking the existing behavior if we think it's the right thing for our users. We also think that the existing behavior on async methods is just broken. Currently, when an async method throws an exception, we treat it as fulfilling the postcondition, much like for a non-async method. This is because we think the caller won't actually be able to use whatever variable was expected to be not-null after the call--thus, nothing to warn about.

However, in reality, when an async method throws an exception, it is packaged up into a Task and returned to the caller. It is not thrown until the task is awaited. Because pretty much any code can throw an exception, no async method is able to reliably fulfill nullability postconditions as currently designed. This is similar to an issue we recently fixed in definite assignment.

SharpLab

public class C
{
    string? item;
    
    [MemberNotNull(nameof(item))]
    public async Task MAsync()
    {
        Helper();
        item = "a";
        await Task.Yield(); // no warnings
    }

    public static void Helper() => throw new Exception();
    
    public static void Main()
    {
        C c = new C();
        var t = c.MAsync(); // exception is thrown indirectly through Helper and included in the returned Task
        c.item.ToString(); // no warning, NRE at runtime
    }
}

Detailed design

We think the most viable option to fix the issue here is to change the existing meaning of [MemberNotNull], as well as other postconditions like [NotNull], on Task-returning methods (methods which return await-able things), such that the postconditions are only applied if the call is immediately awaited. The only safe alternative would be to warn if a nullable postcondition attribute is used at all on an async method, which would be unfortunate.

The requirement to change behavior at call sites for any "awaitable" method call is because async is treated as an implementation detail, and it's not possible to determine whether a method from metadata is async or not. We'd prefer to have uniformity in usage across both source and metadata.

The requirement to immediately await rather than being able to store the task in a variable and await it later, for example, is because we won't be able to be sure about the ordering of effects in such cases:

var task = c.MAsync();
c.item = null;
await task;
c.item.ToString(); // ok?

Although we're not sure such methods would occur in real code, we also considered the behavior of an API like the following:

namespace System
{
    public static class File
    {
        public static async Task<bool> ExistsAsync([NotNull] string? path); // throws an exception if path is null
    }
}

public class C
{
    public static async Task M(string? path)
    {
        if (await File.ExistsAsync(path))
        {
            path.ToString(); // ok
        }
    }
}

We could strictly define the behavior such that postconditions which "worsen" the current state such as [MaybeNull] are applied whether the method is awaited or not, to represent the possibility that the state change has occurred. However, this is less relevant for async code, where by-ref parameters are not permitted. In this case, the only use case for such postcondition attributes on parameters is for "assert" scenarios, learning information about the input without changing it, such as the ExistsAsync example above.

MemberNotNullWhen

This may also be an opportunity to define a useful relationship between Task<bool> and MemberNotNullWhen(bool), where we understand the attribute to be applying to the underlying value of the Task, rather than the Task itself, which is generally invalid/useless. There may be some additional complexity here relating to the different ways a value can be extracted out of a task-like object, so we may not be able to do it, or it may be on a best-effort basis.

var c = new C();
if (await c.M())
    c.F.ToString(); // ok
else
    c.F.ToString(); // warning

class C
{
    public string? F;

    [MemberNotNullWhen(true, nameof(F))]
    public async Task<bool> M()
    {
        var result = await WebServiceCall(); // ok
        F = result.Value;
        return result.HasValue;
    }
}

If we do this, we might also want to treat ConfigureAwait specially, in order to do the same thing for both if (await c.M()) { ...} and if (await c.M().ConfigureAwait(false)) { ... }.

LDM Discussions

• https://github.com/dotnet/csharplang/blob/main/meetings/2023/LDM-2023-01-18.md#nullable-post-conditions-and-asyncawait
• https://github.com/dotnet/csharplang/blob/main/meetings/2023/LDM-2023-10-09.md#require-await-to-apply-nullable-postconditions-to-task-returning-calls