Skip to content
This repository has been archived by the owner on Jul 15, 2023. It is now read-only.

Static checker can't prove ForAll on Roslyn-compiled inline arrays #204

Closed
yaakov-h opened this issue Aug 12, 2015 · 0 comments · Fixed by #220
Closed

Static checker can't prove ForAll on Roslyn-compiled inline arrays #204

yaakov-h opened this issue Aug 12, 2015 · 0 comments · Fixed by #220

Comments

@yaakov-h
Copy link
Contributor

The static checker can't prove that ForAll in `new object[] { 1, 2, 3, 4}', the object is not null.

Code:

using System;
using System.Collections.Generic;
using System.Diagnostics.Contracts;

namespace ContractForAll
{
    public class Program
    {
        public static void Main(string[] args)
        {
            var objects = new object[] { 1, 2, 3, 4 };
            WriteObjects(objects);

            Console.ReadKey();
        }

        static void WriteObjects(IEnumerable<object> objects)
        {
            Contract.Requires(objects != null);
            Contract.Requires(Contract.ForAll(objects, o => o != null));

            foreach (var obj in objects)
            {
                Console.WriteLine(obj);
            }
        }
    }
}

VS2013 output:

1>------ Rebuild All started: Project: ContractForAll, Configuration: Debug Any CPU ------
CodeContracts: ContractForAll: Schedule static contract analysis.
CodeContracts: ContractForAll: Background contract analysis started.
1>  elapsed time: 147.8448ms
1>  ContractForAll -> C:\Temp\ContractForAll\ContractForAll\bin\Debug\ContractForAll.exe
========== Rebuild All: 1 succeeded, 0 failed, 0 skipped ==========
CodeContracts: ContractForAll: Time spent connecting to the cache: 00:00:01.0910416
CodeContracts: ContractForAll: Cache used: (LocalDb)\MSSQLLocalDB
CodeContracts: ContractForAll: Validated: 100.0%
CodeContracts: ContractForAll: Checked 21 assertions: 21 correct
CodeContracts: ContractForAll: Contract density: 1.57
CodeContracts: ContractForAll: Total methods analyzed 4
CodeContracts: ContractForAll: Methods analyzed with a faster abstract domain 0
CodeContracts: ContractForAll: Method analyses read from the cache 2
CodeContracts: ContractForAll: Methods not found in the cache 2
CodeContracts: ContractForAll: Methods with 0 warnings 4
CodeContracts: ContractForAll: Time spent in internal, potentially costly, operations
CodeContracts: ContractForAll: Overall time spent performing action #KarrPutIntoRowEchelonForm: 00:00:00.0190207 (invoked 3441 times)
Overall time spent performing action #KarrIsBottom: 00:00:00.0109988 (invoked 3279 times)
Overall time spent performing action #CheckIfEqual: 00:00:00.0170017 (invoked 20 times)
Overall time spent performing action #ArraysAssignInParallel: 00:00:00.1069932 (invoked 83 times)
Overall time spent performing action #ArraysJoin: 00:00:00.0709862 (invoked 42 times)
Overall time spent performing action #Simplex: 00:00:00.0709878 (invoked 302 times)
Overall time spent performing action #SubPolyJoin: 00:00:00.1390107 (invoked 41 times)
Overall time spent performing action #WP: 00:00:00.0490001 (invoked 2 times)
CodeContracts: ContractForAll: Total time 4.448sec. 1112ms/method
CodeContracts: ContractForAll: Retained 0 preconditions after filtering
CodeContracts: ContractForAll: Inferred 0 object invariants
CodeContracts: ContractForAll: Retained 0 object invariants after filtering
CodeContracts: ContractForAll: Discovered 1 postconditions to suggest
CodeContracts: ContractForAll: Retained 0 postconditions after filtering
CodeContracts: ContractForAll: Detected 0 code fixes
CodeContracts: ContractForAll: Proof obligations with a code fix: 0
C:\Program Files (x86)\Microsoft Visual Studio 12.0\Common7\IDE\ContractForAll.exe(1,1): message : CodeContracts: Checked 21 assertions: 21 correct
CodeContracts: ContractForAll: 
CodeContracts: ContractForAll: Background contract analysis done.

VS2015 output:

1>------ Rebuild All started: Project: ContractForAll, Configuration: Debug Any CPU ------
CodeContracts: ContractForAll: Schedule static contract analysis.
CodeContracts: ContractForAll: Background contract analysis started.
1>  elapsed time: 144.8568ms
1>  ContractForAll -> C:\Temp\ContractForAll\ContractForAll\bin\Debug\ContractForAll.exe
========== Rebuild All: 1 succeeded, 0 failed, 0 skipped ==========
CodeContracts: ContractForAll: Time spent connecting to the cache: 00:00:01.1950455
CodeContracts: ContractForAll: Cache used: (LocalDb)\MSSQLLocalDB
CodeContracts: ContractForAll: Validated:  95.2%
CodeContracts: ContractForAll: Checked 21 assertions: 20 correct 1 unknown
CodeContracts: ContractForAll: Contract density: 1.74
CodeContracts: ContractForAll: Total methods analyzed 4
CodeContracts: ContractForAll: Methods analyzed with a faster abstract domain 0
CodeContracts: ContractForAll: Method analyses read from the cache 2
CodeContracts: ContractForAll: Methods not found in the cache 2
CodeContracts: ContractForAll: Methods with 0 warnings 3
CodeContracts: ContractForAll: Time spent in internal, potentially costly, operations
CodeContracts: ContractForAll: Overall time spent performing action #KarrPutIntoRowEchelonForm: 00:00:00.0249749 (invoked 3743 times)
Overall time spent performing action #KarrIsBottom: 00:00:00.0139951 (invoked 3552 times)
Overall time spent performing action #CheckIfEqual: 00:00:00.0170028 (invoked 23 times)
Overall time spent performing action #ArraysAssignInParallel: 00:00:00.1080109 (invoked 71 times)
Overall time spent performing action #ArraysJoin: 00:00:00.0699943 (invoked 42 times)
Overall time spent performing action #Simplex: 00:00:00.0810813 (invoked 303 times)
Overall time spent performing action #SubPolyJoin: 00:00:00.1450139 (invoked 41 times)
Overall time spent performing action #WP: 00:00:00.0610050 (invoked 3 times)
CodeContracts: ContractForAll: Total time 5.017sec. 1254ms/method
CodeContracts: ContractForAll: Retained 0 preconditions after filtering
CodeContracts: ContractForAll: Inferred 0 object invariants
CodeContracts: ContractForAll: Retained 0 object invariants after filtering
CodeContracts: ContractForAll: Discovered 1 postconditions to suggest
CodeContracts: ContractForAll: Retained 0 postconditions after filtering
CodeContracts: ContractForAll: Detected 0 code fixes
CodeContracts: ContractForAll: Proof obligations with a code fix: 0
C:\Temp\ContractForAll\ContractForAll\Class1.cs(12,13): warning : CodeContracts: requires unproven: Contract.ForAll(objects, o => o != null)
C:\Temp\ContractForAll\ContractForAll\Class1.cs(20,13): warning :   + location related to previous warning
C:\Program Files (x86)\Microsoft Visual Studio 14.0\Common7\IDE\ContractForAll.exe(1,1): message : CodeContracts: Checked 21 assertions: 20 correct 1 unknown
CodeContracts: ContractForAll: 
CodeContracts: ContractForAll: Background contract analysis done.

IL of Main, VS2013, according to ILSpy:

.method public hidebysig static 
    void Main (
        string[] args
    ) cil managed 
{
    // Method begins at RVA 0x2048
    // Code size 60 (0x3c)
    .maxstack 3
    .entrypoint
    .locals init (
        [0] object[] objects,
        [1] object[] CS$0$0000
    )

    IL_0000: nop
    IL_0001: ldc.i4.4
    IL_0002: newarr [mscorlib]System.Object
    IL_0007: stloc.1
    IL_0008: ldloc.1
    IL_0009: ldc.i4.0
    IL_000a: ldc.i4.1
    IL_000b: box [mscorlib]System.Int32
    IL_0010: stelem.ref
    IL_0011: ldloc.1
    IL_0012: ldc.i4.1
    IL_0013: ldc.i4.2
    IL_0014: box [mscorlib]System.Int32
    IL_0019: stelem.ref
    IL_001a: ldloc.1
    IL_001b: ldc.i4.2
    IL_001c: ldc.i4.3
    IL_001d: box [mscorlib]System.Int32
    IL_0022: stelem.ref
    IL_0023: ldloc.1
    IL_0024: ldc.i4.3
    IL_0025: ldc.i4.4
    IL_0026: box [mscorlib]System.Int32
    IL_002b: stelem.ref
    IL_002c: ldloc.1
    IL_002d: stloc.0
    IL_002e: ldloc.0
    IL_002f: call void ContractForAll.Program::WriteObjects(class [mscorlib]System.Collections.Generic.IEnumerable`1<object>)
    IL_0034: nop
    IL_0035: call valuetype [mscorlib]System.ConsoleKeyInfo [mscorlib]System.Console::ReadKey()
    IL_003a: pop
    IL_003b: ret
} // end of method Program::Main

IL of Main, VS2015, according to ILSpy:

.method public hidebysig static 
    void Main (
        string[] args
    ) cil managed 
{
    // Method begins at RVA 0x2048
    // Code size 58 (0x3a)
    .maxstack 4
    .entrypoint
    .locals init (
        [0] object[] objects
    )

    IL_0000: nop
    IL_0001: ldc.i4.4
    IL_0002: newarr [mscorlib]System.Object
    IL_0007: dup
    IL_0008: ldc.i4.0
    IL_0009: ldc.i4.1
    IL_000a: box [mscorlib]System.Int32
    IL_000f: stelem.ref
    IL_0010: dup
    IL_0011: ldc.i4.1
    IL_0012: ldc.i4.2
    IL_0013: box [mscorlib]System.Int32
    IL_0018: stelem.ref
    IL_0019: dup
    IL_001a: ldc.i4.2
    IL_001b: ldc.i4.3
    IL_001c: box [mscorlib]System.Int32
    IL_0021: stelem.ref
    IL_0022: dup
    IL_0023: ldc.i4.3
    IL_0024: ldc.i4.4
    IL_0025: box [mscorlib]System.Int32
    IL_002a: stelem.ref
    IL_002b: stloc.0
    IL_002c: ldloc.0
    IL_002d: call void ContractForAll.Program::WriteObjects(class [mscorlib]System.Collections.Generic.IEnumerable`1<object>)
    IL_0032: nop
    IL_0033: call valuetype [mscorlib]System.ConsoleKeyInfo [mscorlib]System.Console::ReadKey()
    IL_0038: pop
    IL_0039: ret
} // end of method Program::Main
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Fix for #204
1 participant
@yaakov-h