
# 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?*

```C#
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:

```C#
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:

```C#
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:

```C#
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?

```C#
#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


```C#
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
