dotnet / dotnet/csharplang

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

Open
#8,679 0 comments 0 reactions 1 assignee Claimed by @RikkiGibson View on GitHub
Proposal Proposal champion
Dominant language
C#
Stars
12.7k
Forks
1.1k
Avg merge
11h 1m
Merged PRs (30d)
3

Description

* Speclet: inline
* Discussion: https://github.com/dotnet/csharplang/discussions/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.

```cs
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](https://github.com/dotnet/roslyn/issues/43697#issuecomment-1267566839).

[SharpLab](https://sharplab.io/#v2:C4LgTgrgdgPgAgJgIwFgBQcAMACOSB0AIgJYCGA5lAPYDOwxAxjfgMJUAmApgIJSkA2ATxrEaAbnRZcSAKwS0kgMy4E2FugDe6bDumYA/NmLBOAW3m7s23QG0AsmYBGnMADkqwVxH78AFH1NOKgAzX2MzAEoIgF1rHThlOAAOXAA2bDtuGkEoBl8IuOwtNEtLAAlOfgAHF3yLUp1w02wAXmwAIlJ2+oa4AE40/ABNYkr2OuwAeknsamwAd1IwKGIochpCgF90QoTpdLgAFmwK6tqI1oA+bGAACzAqednOJ4BRAA8GTir6Kig6wq7BAIQrFBo6FjYBitZ5PFgAkrggBuSxuMIY+Ey2VyE2m2E4n2+vygRhoN3ujxJq3YxDAnAYwCE5IeEHItxOlRqYGwpCg7CMuX4EC4/NW5M4uAA7Jx+XBUoVLBimvgACpUADKwDAq3IuJmc0Wyx1ABpsK4AEqvHnAbCQKD0QJbdCbIA)

```cs
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:

```cs
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:

```cs
namespace System
{
public static class File
{
public static async Task 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` 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.

```cs
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 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

Contributor guide

No contributing guide indexed for this repository

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.