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

Static checker: different behavior of Contract.ForAll in VS2012 vs VS2015 #177

Closed
fedotovalex opened this issue Jul 29, 2015 · 2 comments · Fixed by #182
Closed

Static checker: different behavior of Contract.ForAll in VS2012 vs VS2015 #177

fedotovalex opened this issue Jul 29, 2015 · 2 comments · Fixed by #182
Assignees

Comments

@fedotovalex
Copy link
Contributor

It appears that Contract.ForAll never validates statically in Visual Studio 2015 while the same code is validated without a problem in Visual Studio 2012 (did not test in Visual Studio 2013).

Here's a minimal application to illustrate the issue:

using System;
using System.Diagnostics.Contracts;

namespace Arrays
{
    class Program
    {
        static void Main(string[] args)
        {
            Contract.Assume(args != null);
            Contract.Assume(args.Length > 0);
            Contract.Assume(Contract.ForAll(args, a => a != null));

            Console.WriteLine(Method(args));
        }

        static int Method(string[] args)
        {
            Contract.Requires(args != null);
            Contract.Requires(args.Length > 0);
            Contract.Requires(Contract.ForAll(args, a => a != null));

            return args[0].Length;
        }
    }
}

When compiling in Visual Studio 2012, the output is as follows:

CodeContracts: Arrays: Run static contract analysis.
C:\Projects\Contracts\Arrays\Arrays\Program.cs(10,13): message : CodeContracts: Suggested assumption: Assumption can be proven: Consider changing it into an assert.
C:\Projects\Contracts\Arrays\Arrays\Program.cs(12,13): message : CodeContracts: Suggested assumption: Assumption can be proven: Consider changing it into an assert.
CodeContracts: Arrays: Validated: 100.0 %
CodeContracts: Arrays: Checked 13 assertions: 13 correct
CodeContracts: Arrays: Contract density: 1.65
CodeContracts: Arrays: Total methods analyzed 4
CodeContracts: Arrays: Methods analyzed with a faster abstract domain 0
CodeContracts: Arrays: Methods with 0 warnings 4
CodeContracts: Arrays: Time spent in internal, potentially costly, operations
CodeContracts: Arrays: Overall time spent performing action #KarrPutIntoRowEchelonForm: 00:00:00.0180010 (invoked 526 times)
Overall time spent performing action #KarrIsBottom: 00:00:00.0200009 (invoked 1255 times)
Overall time spent performing action #CheckIfEqual: 00:00:00.0200011 (invoked 15 times)
Overall time spent performing action #Simplex: 00:00:00.0910052 (invoked 35 times)
Overall time spent performing action #WP: 00:00:00.1160064 (invoked 4 times)
CodeContracts: Arrays: Total time 6.961sec. 1740ms/method
CodeContracts: Arrays: Retained 0 preconditions after filtering
CodeContracts: Arrays: Inferred 0 object invariants
CodeContracts: Arrays: Retained 0 object invariants after filtering
CodeContracts: Arrays: Detected 0 code fixes
CodeContracts: Arrays: Proof obligations with a code fix: 0
C:\Program Files (x86)\Microsoft Visual Studio 11.0\Common7\IDE\Arrays.exe(1,1): message : CodeContracts: Checked 13 assertions: 13 correct
CodeContracts: Arrays: 
CodeContracts: Arrays: Static contract analysis done.

When compiling in Visual Studio 2015, the output is different:

CodeContracts: Arrays: Run static contract analysis.
C:\Projects\Arrays\Arrays\Program.cs(10,13): message : CodeContracts: Suggested assumption: Assumption can be proven: Consider changing it into an assert.
CodeContracts: Arrays: Validated: 84.6 %
CodeContracts: Arrays: Checked 13 assertions: 11 correct 2 unknown
CodeContracts: Arrays: Contract density: 1.64
CodeContracts: Arrays: Total methods analyzed 4
CodeContracts: Arrays: Methods analyzed with a faster abstract domain 0
CodeContracts: Arrays: Methods with 0 warnings 2
CodeContracts: Arrays: Time spent in internal, potentially costly, operations
CodeContracts: Arrays: Overall time spent performing action #KarrPutIntoRowEchelonForm: 00:00:00.0210344 (invoked 666 times)
Overall time spent performing action #KarrIsBottom: 00:00:00.0180034 (invoked 1571 times)
Overall time spent performing action #CheckIfEqual: 00:00:00.0190029 (invoked 18 times)
Overall time spent performing action #ArraysAssignInParallel: 00:00:00.0860030 (invoked 3 times)
Overall time spent performing action #Simplex: 00:00:00.0510336 (invoked 50 times)
Overall time spent performing action #SubPolyJoin: 00:00:00.2000088 (invoked 3 times)
Overall time spent performing action #WP: 00:00:00.4369996 (invoked 7 times)
CodeContracts: Arrays: Total time 4.843sec. 1210ms/method
CodeContracts: Arrays: Retained 0 preconditions after filtering
CodeContracts: Arrays: Inferred 0 object invariants
CodeContracts: Arrays: Retained 0 object invariants after filtering
CodeContracts: Arrays: Detected 0 code fixes
CodeContracts: Arrays: Proof obligations with a code fix: 0
C:\Projects\Arrays\Arrays\Program.cs(23,13): warning : CodeContracts: Possibly calling a method on a null reference
C:\Projects\Arrays\Arrays\Program.cs(14,13): warning : CodeContracts: requires unproven: Contract.ForAll(args, a => a != null)
C:\Projects\Arrays\Arrays\Program.cs(21,13): warning :   + location related to previous warning
C:\Program Files (x86)\Microsoft Visual Studio 14.0\Common7\IDE\Arrays.exe(1,1): message : CodeContracts: Checked 13 assertions: 11 correct 2 unknown
CodeContracts: Arrays: 
CodeContracts: Arrays: Static contract analysis done.

Note that it behaves as if Contract.Assume(Contract.ForAll(args, a => a != null)); has no effect.

Full project source code is available at https://www.dropbox.com/s/3xbs3q819xx0l90/Arrays.zip?dl=0.

@fedotovalex
Copy link
Contributor Author

As an observation, changing the program as follows makes it validate in Visual Studio 2015:

using System;
using System.Diagnostics.Contracts;

namespace Arrays
{
    class Program
    {
        static void Main(string[] args)
        {
            Contract.Assume(args != null);
            Contract.Assume(args.Length > 0);
            Contract.Assume(Contract.ForAll(args, NotNull));

            Console.WriteLine(Method(args));
        }

        static int Method(string[] args)
        {
            Contract.Requires(args != null);
            Contract.Requires(args.Length > 0);
            Contract.Requires(Contract.ForAll(args, NotNull));

            return args[0].Length;
        }

        [Pure]
        static bool NotNull<T>(
            T value
            )
        {
            return value != null;
        }
    }
}

Perhaps the original issue has to do with how backing methods for lambdas are generated in Roslyn?

@SergeyTeplyakov
Copy link
Contributor

I've changed the logic for ccrewriter to understand new IL code pattern, but my assumption was that cccheck is using the same logic. Apparently, I was wrong. I'll take a look at this issue, because I've already fixed similar one for ccrewrite.

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants