False positives on 'invariant unreached' and 'reference use unreached' with Roslyn

[yaakov-h]

Repro case:

using System.Diagnostics.Contracts;

namespace ContractInvariants
{
    public class MyThingy
    {
        public MyThingy(object value)
        {
            Contract.Requires(value != null);
            this.value = value;
            this.valueTypeFullName = GetValueTypeFullName();
        }

        readonly object value;
        readonly string valueTypeFullName;

        string GetValueTypeFullName()
        {
            return value.GetType().FullName;
        }

        [ContractInvariantMethod]
        void ObjectInvariant()
        {
            Contract.Invariant(value != null);
            Contract.Invariant(valueTypeFullName != null);
        }
    }
}

VS2013 build output with -show unreached

1>------ Build started: Project: ContractInvariants, Configuration: Debug Any CPU ------
CodeContracts: ContractInvariants: Schedule static contract analysis.
CodeContracts: ContractInvariants: Background contract analysis started.
1>  elapsed time: 175.4416ms
1>  ContractInvariants -> C:\Temp\ContractForAll\ContractInvariants\bin\Debug\ContractInvariants.dll
========== Build: 1 succeeded, 0 failed, 0 up-to-date, 0 skipped ==========
CodeContracts: ContractInvariants: Time spent connecting to the cache: 00:00:01.1090546
CodeContracts: ContractInvariants: Cache used: (LocalDb)\MSSQLLocalDB
CodeContracts: ContractInvariants: Validated: 100.0%
CodeContracts: ContractInvariants: Checked 9 assertions: 9 correct
CodeContracts: ContractInvariants: Contract density: 8.38
CodeContracts: ContractInvariants: Total methods analyzed 3
CodeContracts: ContractInvariants: Methods analyzed with a faster abstract domain 0
CodeContracts: ContractInvariants: Method analyses read from the cache 1
CodeContracts: ContractInvariants: Methods not found in the cache 2
CodeContracts: ContractInvariants: Methods with 0 warnings 3
CodeContracts: ContractInvariants: Time spent in internal, potentially costly, operations
CodeContracts: ContractInvariants: Overall time spent performing action #KarrPutIntoRowEchelonForm: 00:00:00.0080076 (invoked 399 times)
Overall time spent performing action #KarrIsBottom: 00:00:00.0060011 (invoked 1065 times)
Overall time spent performing action #ArraysAssignInParallel: 00:00:00.0710238 (invoked 18 times)
Overall time spent performing action #ArraysJoin: 00:00:00.0609960 (invoked 9 times)
Overall time spent performing action #WP: 00:00:00.0300029 (invoked 1 times)
CodeContracts: ContractInvariants: Total time 3.935sec. 1311ms/method
CodeContracts: ContractInvariants: Retained 0 preconditions after filtering
CodeContracts: ContractInvariants: Inferred 0 object invariants
CodeContracts: ContractInvariants: Retained 0 object invariants after filtering
CodeContracts: ContractInvariants: Discovered 3 postconditions to suggest
CodeContracts: ContractInvariants: Retained 3 postconditions after filtering
CodeContracts: ContractInvariants: Detected 0 code fixes
CodeContracts: ContractInvariants: Proof obligations with a code fix: 0
C:\Workspace\glow\DotNet\Service\ContractInvariants.dll(1,1): message : CodeContracts: Checked 9 assertions: 9 correct
CodeContracts: ContractInvariants: 
CodeContracts: ContractInvariants: Background contract analysis done.

VS2015 build output with -show unreached

1>------ Build started: Project: ContractInvariants, Configuration: Debug Any CPU ------
CodeContracts: ContractInvariants: Schedule static contract analysis.
CodeContracts: ContractInvariants: Background contract analysis started.
1>  elapsed time: 128.0562ms
1>  ContractInvariants -> C:\Temp\ContractForAll\ContractInvariants\bin\Debug\ContractInvariants.dll
========== Build: 1 succeeded, 0 failed, 1 up-to-date, 0 skipped ==========
CodeContracts: ContractInvariants: Time spent connecting to the cache: 00:00:01.0950366
CodeContracts: ContractInvariants: Cache used: (LocalDb)\MSSQLLocalDB
CodeContracts: ContractInvariants: Validated:  75.0%
CodeContracts: ContractInvariants: Checked 12 assertions: 9 correct 3 unreached
CodeContracts: ContractInvariants: Contract density: 7.71
CodeContracts: ContractInvariants: Total methods analyzed 3
CodeContracts: ContractInvariants: Methods analyzed with a faster abstract domain 0
CodeContracts: ContractInvariants: Method analyses read from the cache 0
CodeContracts: ContractInvariants: Methods not found in the cache 3
CodeContracts: ContractInvariants: Methods with 0 warnings 2
CodeContracts: ContractInvariants: Time spent in internal, potentially costly, operations
CodeContracts: ContractInvariants: Overall time spent performing action #KarrPutIntoRowEchelonForm: 00:00:00.0080104 (invoked 436 times)
Overall time spent performing action #KarrIsBottom: 00:00:00.0069994 (invoked 1066 times)
Overall time spent performing action #ArraysAssignInParallel: 00:00:00.0670037 (invoked 18 times)
Overall time spent performing action #ArraysJoin: 00:00:00.0670094 (invoked 9 times)
Overall time spent performing action #WP: 00:00:00.0200231 (invoked 1 times)
CodeContracts: ContractInvariants: Total time 3.918sec. 1306ms/method
CodeContracts: ContractInvariants: Retained 0 preconditions after filtering
CodeContracts: ContractInvariants: Inferred 0 object invariants
CodeContracts: ContractInvariants: Retained 0 object invariants after filtering
CodeContracts: ContractInvariants: Discovered 3 postconditions to suggest
CodeContracts: ContractInvariants: Retained 3 postconditions after filtering
CodeContracts: ContractInvariants: Detected 0 code fixes
CodeContracts: ContractInvariants: Proof obligations with a code fix: 0
C:\Temp\ContractForAll\ContractInvariants\Class1.cs(12,9): warning : CodeContracts: invariant unreachable (2 more unreached assertion(s) at the same location)
C:\Temp\ContractForAll\ContractInvariants\Class1.cs(25,13): warning :   + location related to previous warning
C:\Temp\ContractForAll\ContractInvariants\Class1.cs(11,13): warning : CodeContracts: reference use unreached
C:\Program Files (x86)\Microsoft Visual Studio 14.0\Common7\IDE\ContractInvariants.dll(1,1): message : CodeContracts: Checked 12 assertions: 9 correct 3 unreached
CodeContracts: ContractInvariants: 
CodeContracts: ContractInvariants: Background contract analysis done.

[liamzebedee]

Can also add to this. We have something like this:

        public static double GetScaledPixelIncrements(this IDiagramEntity diagramEntity)
        {
            Contract.Requires(diagramEntity != null); // Suggested By ReviewBot 
            var resolutionIncrementFactor = diagramEntity.ResolutionIncrement / (double)diagramEntity.Scale;
            var scaleSizeInPixels = diagramEntity.ScaleUnitPixelSize;

            return scaleSizeInPixels * resolutionIncrementFactor;
        }

Getting a "reference use unreached" on the scaleSizeInPixels variable as it's only used once in the return statement. The variables are introduced for readability and used once in the return statement, which I think is a fair use case.

[yaakov-h]

I encountered another similar case today with C# 6's enhancement to properties. This code will trigger an "invariant unreachable":

using System.Diagnostics.Contracts;

namespace ContractCSharp6Properties
{
    [ContractClass(typeof(FooContract))]
    public interface IFoo
    {
        object Bar { get; }
    }

    [ContractClassFor(typeof(IFoo))]
    abstract class FooContract : IFoo
    {
        public object Bar
        {
            get
            {
                Contract.Ensures(Contract.Result<object>() != null);
                return default(object);
            }
        }
    }

    public class Foo : IFoo
    {
        public Foo(object bar)
        {
            Contract.Requires(bar != null);

            Bar = bar;
        }

        public object Bar { get; }

        [ContractInvariantMethod]
        void ObjectInvariant()
        {
            Contract.Invariant(Bar != null);
        }
    }
}

Interestingly, if I strip out the interface, like so:

using System.Diagnostics.Contracts;

namespace ContractCSharp6Properties
{
    public class Foo
    {
        public Foo(object bar)
        {
            Contract.Requires(bar != null);

            Bar = bar;
        }

        public object Bar { get; }

        [ContractInvariantMethod]
        void ObjectInvariant()
        {
            Contract.Invariant(Bar != null);
        }
    }
}

I then get the following warning:

C:\Temp\ContractCSharp6Properties\ContractCSharp6Properties\Class1.cs(7,3): warning : CodeContracts: Invoking constructor 'ContractCSharp6Properties.Foo.#ctor(System.Object)' will always lead to a violation of an (inferred) object invariant
C:\Temp\ContractCSharp6Properties\ContractCSharp6Properties\Class1.cs(12,3): warning : CodeContracts: invariant is false: Bar != null
C:\Temp\ContractCSharp6Properties\ContractCSharp6Properties\Class1.cs(19,4): warning :   + location related to previous warning
C:\Program Files (x86)\Microsoft Visual Studio 14.0\Common7\IDE\ContractCSharp6Properties.dll(1,1): message : CodeContracts: Checked 5 assertions: 3 correct 1 unknown 1 false

Invoking constructor 'ContractCSharp6Properties.Foo.#ctor(System.Object)' will always lead to a violation of an (inferred) object invariant

This is false, and goes away if the interface is added and implemented.