csharplang/meetings/2018/LDM-2018-12-05.md

C# LDM notes for Dec 5, 2018

Agenda

Tracked nullable states, their correspondence to source and the rules they follow in flow analysis

Proposal

Since we are treating nullable analysis as a conventional lattice data flow analysis, we'd like to define the lattice.

Here are the states based on current implementation:

• Unknown
• NotAnnotated
• Annotated
• NotNullable
• Nullable

The goal is to get to a concrete specification that defines how the flow state affects the language and how flow states interact.

The first task is to decide how the annotations and the nullable context interact to define the flow state. At the moment, the context of where the variable is defined decides what the state of the variable is in, when it is used in a method. However, there is a proposal to use the context of the method to define the state the variable is in.

There are now new proposed states, which are now split between states used in flow analysis, and states used as semantic annotation.

Semantic states:

• Nullable
• Oblivious
• NotAnnotated

Flow states:

• "Can be null" (true or false)

Consequences:

When reading a field we compute the flow state as follows:

• Nullable -> true
• Oblivious -> false
• NotAnnotated -> true only if a type parameter that could be nullable, else false

When writing a field we warn as follows:

• NotAnnotated, true -> warn if the RHS can be null when the variable (or type) can't (i.e., take into account both being related type parameters)

Discussion

Q: What warnings do we produce for the following?

void M<T>(T p1) where T : class?
{
    p1 = p1; // p1 may be null, but we don't produce a warning because
             // the T could be nullable
}

The consequence is:

void M<T>(T p) where T : class?
{
    p = null; // This DOES produce a warning, because there's a conversion
              // from `null` to T and we don't know that T is nullable
}

Also:

void M<T>(T p) where T : class?
{
    if (p == null) // <- this is fine
    {
        T x = p; // <- this also doesn't give a warning because
                 // there is no conversion
    }
}

And:

void M(string p1)
{
    if (p1 == null)
    {
        string x = p1; // W warning? -> Yes
    }
}

Between the current state and the new proposal, what's the behavior of the following?

#nullable disable
var t = M(new object()); // What is T inferred as?
...
#nullable enable
t.Value = null; // warning?
...

Box<T> M<T>(T t) => new Box(t);

Current: Box<T> is inferred as Box<object!>, warning New proposal: Box<T> is inferred as Box<object~>, so no warning

void M<T>(T x) 
{
    if (x == null) throw;
    var y = x;
    var z = M(y); // What is the inferred type?
    z.Value = null; // warning?
}
...
Box<T> M<T>(T t) => new Box(t);

Current implementation: Box<T2> is Box<T!>, warning New proposal: Box<T2> is inferred as Box<T>, no warnings