Feature Request: tracking boolean logic to compute nullability

[gafter]

See also dotnet/roslyn#34665 reported by @stephentoub

Consider the following program

#nullable enable
using System;
using System.Diagnostics;

class Program
{
    static void Main() { }

    static void Foo(object? first, object? second)
    {
        Debug.Assert(first != null || second != null);

        if (first != null)
        {
            Console.WriteLine(first.GetHashCode());
        }
        else
        {
            Console.WriteLine(second.GetHashCode());
        }
    }
}

This warns on the last line that second might be null ("Possible dereference of a null reference"), but it is possible to infer that's not possible, given the Assert that at least one of first or second is non-null and then that first is null.

Implementing a compiler that is smart enough to avoid the warning may require some theorem-prover-style analysis, which might be useful for many other things.

See also dotnet/roslyn#31893 dotnet/roslyn#34976

[AartBluestoke]

Why is this a language issue vs just a compiler issue?

The language says "you must not use an unassigned variable"; does it actually say that the following snippet should not compile? (or throw a null ref warning if s is assigned null):

using System;
public class C {
    // readonly bool theBool= true; also fails for readonly vars here

    public void M() {
        bool theBool= true; //local so the compiler knows nothing else can touch it
        string s;  // or s = null; //if you want a potential null de-reff warning below
        if(theBool)
            s="some only sometimes relevent";
        //later ...  or even straight away
        if(theBool)
            Console.WriteLine(s); // error CS0165: Use of unassigned local variable 's' in writeline
    }
}

dotnet/roslyn#31893 says "we don't trace values"; which implies that if the compiler did do some logic tracing then it could be happy to compile it.

I don't think a langauge feature that states "a compiler must consider all permutations of boolean conditions before warning/erroring a potential use of a null/unassigned variable" could be written, as that opens the door to forcing the compiler to do arbitrarily complicated calculations (what if you have 4 if clauses in the function, with 4 variables; is the compiler expected to search all 32 conditional code branches for accidential miss-use if a potential Null warning or unassigned use error is detected?

I think that reduced statement like "an object may be safely used if it used under the same conditions it is assigned" -- it doesn't solve the larger problem posed in the original question, but it would allow a subset of these to compile without issues.

-- (this comment may be edited if i've missed something and the language itself says that my fragment must not compile)

[yaakov-h]

This is with regards to flow analysis for C# 8.0's Nullable Reference Types feature, not unassigned variables.

[gafter]

an object may be safely used if it used under the same conditions it is assigned

Neither the language nor the compiler have a concept of "the same condition".

[YairHalberstadt]

In the given example, would it still avoid the warning if first and second were fields, not locals?

I.e. Would the theorem prover err on the side of being conservative, or would it make the assumption that the code is well behaved?

Currently nullability analysis makes the assumption code is well behaved, whereas definite assignment analysis is conservative.

[gafter]

@YairHalberstadt The hypothetical theorem prover hasn't been designed, so we don't know.