csharplang/meetings/2018/LDM-2018-06-04.md

C# Language Design Notes for Jun 4, 2018

Warning: These are raw notes, and still need to be cleaned up. Read at your own peril!

Nullable flow analysis

static void F(object? x)
    {
        object y = null;
        Action f = () => y = x; // warning?
        if (x == null) return;
        f();
        y.ToString(); // warning?
    }

A proposal is to take the most nullable the variable can be and use that state in a lambda that captures it.

(This is only relevant for top-level nullability, as nested nullability is not tracked through flow.)

There's a slight concern that we could run into cycles, where "the most nullable state" depends on "the most nullable state". We think that it is not going to be an issue.

M(string? x, string? y)
{
    Action f = () => y = x;
    x = null;
    //M1(f);
    x = "";
    M2(f);
    y.Length;
}

It seems a shame that optimizing like this, by caching the delegate, could lead to more nullable warnings. We could imagine tracking delegates through locals and basing the analysis on where they are used (called or passed).

Envisioned safe tightenings:

• Only care about null assignments that happen after the lambda becomes "effective"
• If a lambda goes into a local variable, then it is only "effective" when that local variable is used
• Such a local, when invoked directly, does not depend on future null states

Another option is to just be more loose about the whole thing, and allow there to be holes. Specifically we could assume that the lambda is executed either when it appears or not at all. The hole is that this does not accurately account for deferred execution.

Thinking about the effect of the lambda above on y, it can happen at any time after the lambda. So at any point after that, the null state of y would be a "superposition" of null states. So if a lambda makes a variable MayBeNull, it would be irreversibly MayBeNull for the remainder of the method. Even right after a null check! It's on perpetual lockdown!

This seems draconian. It feels stronger than our position on dotted names, which lets us assume that the null state remains stable between observing and using. That suggests we should be at least somewhat loose. We could maybe just assume that the lambda is conditionally executed at the point of capture, and we assume that mutations don't happen later.

Aside: lambdas that assign captured variables aren't as esoteric as they may seem. For instance, our whole ecosystem around analyzers relies on a recommended pattern that does that.

Conclusion

We analyze a lambda as if it is conditionally executed only at the point of capture into a delegate. It does rely on order of execution to an uncomfortable degree. Some of the refinements we've considered could be introduced later.

For instance, these two examples would behave differently if y comes in non-null and x comes in maybe-null:

void M1(Action, ref string s);
M1(() => y = x, ref y);

void M2(ref string s, Action);
M2(ref y, () => y = x);

Side note: There's a similar granularity issue with the nullability attributes, whether they should apply to parameters as soon as that parameter is encountered, or only after the whole argument list.

Local functions

When a local function is captured into a delegate, we just do the same as for lambdas: assume a conditional execution at the point of capture.

When local functions are called, abstractly speaking we should do the same as for definite assignment, where the requirements and the effect are inferred for each local function, and then applied in place where the function is called. The difficulty of course comes in when functions are recursive. For definite assignment, we can prove that a recursive analysis terminates, because of the monotony of definite assignment (you never become unassigned). Can we make a similar argument/proof for nullability?

Conditional attributes and special annotations

Let's change EnsuresTrueAttribute to AssertsTrueAttribute, and always take them into account, even when the condition is false.