Static checker cannot prove compiler-generated Expressions are created safely.

[yaakov-h]

Given the following case:

using System;
using System.Collections.Generic;
using System.Linq.Expressions;

namespace ContractPerformanceTesting
{
    class Program
    {
        static void Main(string[] args)
        {
            Expression<Func<IEnumerable<string>>> expr = () => new string[] { };
        }
    }
}

The static checker reports the following:

CodeContracts: ContractPerformanceTesting: 
CodeContracts: ContractPerformanceTesting: Background contract analysis done.
1>------ Build started: Project: ContractPerformanceTesting, Configuration: Debug Any CPU ------
CodeContracts: ContractPerformanceTesting: Schedule static contract analysis.
1>  elapsed time: 609.6196ms
1>  elapsed time: 498.995ms
1>  ContractPerformanceTesting -> C:\temp\ContractPerformanceTesting\ContractPerformanceTesting\bin\Debug\ContractPerformanceTestingAA.exe
CodeContracts: ContractPerformanceTesting: Background contract analysis started.
========== Build: 1 succeeded, 0 failed, 0 up-to-date, 0 skipped ==========
CodeContracts: ContractPerformanceTesting: Time spent connecting to the cache: 00:00:01.1373628
CodeContracts: ContractPerformanceTesting: Cache used: localhost
C:\temp\ContractPerformanceTesting\ContractPerformanceTesting\Program.cs(11,4): message : CodeContracts: Suggested requires: Contract.Requires((int)(0) >= 1);
CodeContracts: ContractPerformanceTesting: Validated: 55.6 %
CodeContracts: ContractPerformanceTesting: Checked 9 assertions: 5 correct 1 unknown 2 unreached 1 false
CodeContracts: ContractPerformanceTesting: Contract density: 2.21
CodeContracts: ContractPerformanceTesting: Total methods analyzed 3
CodeContracts: ContractPerformanceTesting: Methods analyzed with a faster abstract domain 0
CodeContracts: ContractPerformanceTesting: Method analyses read from the cache 3
CodeContracts: ContractPerformanceTesting: Methods not found in the cache 0
CodeContracts: ContractPerformanceTesting: Methods with 0 warnings 2
CodeContracts: ContractPerformanceTesting: Total time 1.122sec. 374ms/method
CodeContracts: ContractPerformanceTesting: Retained 0 preconditions after filtering
CodeContracts: ContractPerformanceTesting: Inferred 0 object invariants
CodeContracts: ContractPerformanceTesting: Retained 0 object invariants after filtering
CodeContracts: ContractPerformanceTesting: Detected 0 code fixes
CodeContracts: ContractPerformanceTesting: Proof obligations with a code fix: 0
C:\temp\ContractPerformanceTesting\ContractPerformanceTesting\Program.cs(11,4): warning : CodeContracts: requires is false: initializers.Length >= 1
C:\Windows\System32\ContractPerformanceTestingAA.exe(1,1): message : CodeContracts: Checked 9 assertions: 5 correct 1 unknown 2 unreached 1 false
CodeContracts: ContractPerformanceTesting: 
CodeContracts: ContractPerformanceTesting: Background contract analysis done.

The root cause is the second error (below), triggered by this contract on Expression.NewArrayInit.

Program.cs(11,4): warning : CodeContracts: requires is false: initializers.Length >= 1

The first error is a very odd side-effect, seems to be the static checker choking on the analysis.

message : CodeContracts: Suggested requires: Contract.Requires((int)(0) >= 1);

[SergeyTeplyakov]

Could you please paste decompiled IL that csc generates for this code? It will slightly help to understand the root cause of the issue.

[yaakov-h]

.method private hidebysig static 
    void Main (
        string[] args
    ) cil managed 
{
    // Method begins at RVA 0x2048
    // Code size 35 (0x23)
    .maxstack 2
    .entrypoint
    .locals init (
        [0] class [System.Core]System.Linq.Expressions.Expression`1<class [mscorlib]System.Func`1<class [mscorlib]System.Collections.Generic.IEnumerable`1<string>>> expr
    )

    IL_0000: nop
    IL_0001: ldtoken [mscorlib]System.String
    IL_0006: call class [mscorlib]System.Type [mscorlib]System.Type::GetTypeFromHandle(valuetype [mscorlib]System.RuntimeTypeHandle)
    IL_000b: ldc.i4.0
    IL_000c: newarr [System.Core]System.Linq.Expressions.Expression
    IL_0011: call class [System.Core]System.Linq.Expressions.NewArrayExpression [System.Core]System.Linq.Expressions.Expression::NewArrayInit(class [mscorlib]System.Type, class [System.Core]System.Linq.Expressions.Expression[])
    IL_0016: ldc.i4.0
    IL_0017: newarr [System.Core]System.Linq.Expressions.ParameterExpression
    IL_001c: call class [System.Core]System.Linq.Expressions.Expression`1<!!0> [System.Core]System.Linq.Expressions.Expression::Lambda<class [mscorlib]System.Func`1<class [mscorlib]System.Collections.Generic.IEnumerable`1<string>>>(class [System.Core]System.Linq.Expressions.Expression, class [System.Core]System.Linq.Expressions.ParameterExpression[])
    IL_0021: stloc.0
    IL_0022: ret
} // end of method Program::Main

[yaakov-h]

Looking at it again, judging by the Reference Source for NewArrayInit, the precondition initializers.Length >= 1 is invalid. As the IL above shows (I think), it's fine for the Expression[] to be empty.

I have a local commit that removes this precondition, I can create a PR once I'm done with a few other changes too.

I have no idea where the Contract.Requires((int)(0) >= 1); suggestion comes from, though.