How I added Code Contracts support for VS2015

    Over the past few weeks, I have been actively working on finalizing Code Contracts , fixing some nasty bugs, and adding support for VS2015. And since VS2015 just saw the light of day, such support will be very helpful. Now about everything about it in order, and even with a number of technical details.

    So, the first thing you need to know about Code Contracts is that this thing is alive. The code is in the public domain on the github (https://github.com/Microsoft/CodeContracts) and there are a number of people who are actively involved in restoring order there. I am the owner of the repository, but I do this in my free time. In addition to me, there are several more people who clean up the Code Contracts Editor Extensions ( @sharwell ) and some other areas.

    Code Contracts can be divided into several components:
    • ccrewrite - a tool that is engaged in “rewriting” ILs, extracting assertions (Contract.Requires / Ensures / Assert / Assume / if-throw) and replacing them with the necessary calls to contract methods, depending on the configuration.
    • cccheck - a tool that deals with static analysis and formal proof at compile time that the program is correct.
    • Code Contracts Editor Extensions - extension to VS, which allows you to "see" the contracts directly in the IDE.

    There are a number of tools, for example, to generate documentation, as well as a ReSharper plugin that simplifies adding preconditions / postconditions and shows ccrewrite errors directly in the IDE.

    I deal with two components - ccrewrite and the plugin, but now I want to dwell on ccrewrite and on the difficulties that I will encounter when adding support for VS2015.



    Breaking changes in VS2015


    The C # / VB compiler team did an amazing job of developing new compilers from scratch. They added a bunch of extension points and now they do not need a PhD degree to write a fairly functional analyzer for the studio. But not without breaking changes.

    For normal operation, ccrewrite must clearly know how the C # / VB language compiler works, and what this or that code is transformed into. Blocks of iterators, asynchronous methods, and closures are especially delivered, for which the C # / VB compilers do all sorts of different tricks. It becomes especially sad when the behavior of the compilers begins to change and the generated code becomes somewhat different.

    The developers of the C # 6.0 compiler (aka Roslyn) introduced a number of optimizations in the generated IL code, which led to breakdowns of decompilers and ccrewrite.

    Caching lambda expressions



    You may have noticed strange static fields in the decompiled code that start with CS $ <> 9__ . These are soul caches of lambda expressions that do not capture the external context (lambda expressions that capture the external context lead to the generation of closures , and classes like <> c__DisplayClass1 are generated for them ).

    static void Foo()
    {
        Action action = () => Console.WriteLine("Hello, lambda!");
        action();
    }
    


    In this case, the “old” compiler will generate the CS $ <> 9__CachedAnonymousMethodDelegatef field and initialize it in a lazy way:

    private static void b__e()
    {
          Console.WriteLine("Hello, lambda!");      
    }
    private static Action CS$<>9__CachedAnonymousMethodDelegatef;
    static void Foo()
    {
        if (CS$<>9__CachedAnonymousMethodDelegatef == null)
        {
            CS$<>9__CachedAnonymousMethodDelegatef = new Action(b__e);
        }
        Action CS$<>9__CachedAnonymousMethodDelegatef = 
            CS$<>9__CachedAnonymousMethodDelegatef;
        CS$<>9__CachedAnonymousMethodDelegatef();
    }
    


    The C # 6.0 compiler takes a different approach. The developers of the experimental OS - Midori found that calling an instance method through a delegate is more efficient than calling a static method. Therefore, the Roslyn compiler generates different code for the same lambda expression:

    private sealed class StaticClosure
    {
        public static readonly StaticClosure Instance = new StaticClosure();
        public static Action CachedDelegate;
        // Анонимный метод стал экземплярным методом
        internal void FooAnonymousMethodBody()
        {
            Console.WriteLine("Hello, lambda!");
        }
    }
    static void Foo()
    {
        Action actionTmp;
        if ((actionTmp = StaticClosure.CachedDelegate) == null)
        {
            StaticClosure.CachedDelegate = new Action(
                StaticClosure.Instance.FooAnonymousMethodBody)
            actionTmp = StaticClosure.CachedDelegate;
        }
        Action action = actionTmp;
        action();
    }
    


    Now a "closure" is created - the StaticClosure class (real name <> c ) with a static field for storing the delegate - CachedDelegate ( <> 9__8_0 ) and "singleton". But now, the body of the anonymous method is in the instance method FooAnonymousMethodBody (b__8_0)

    A simple test showed that calling a delegate through an instance method is really 10 percent faster, although in absolute units the difference is very, very small.

    Now let's see when this change leads to problems in ccrewrite.
    Statements in Code Contracts are defined as calls to methods of the Contract class , which makes it difficult to specify contracts for interfaces and abstract classes. To get around this limitation, you need to create a special class of contracts marked with the attribute ContractClassFor . But this causes a number of additional difficulties.

    [ContractClass(typeof (IFooContract))]
    interface IFoo
    {
        void Boo(int[] data);
    }
    [ExcludeFromCodeCoverage,ContractClassFor(typeof (IFoo))]
    abstract class IFooContract : IFoo
    {
        void IFoo.Boo(int[] data)
        {
            Contract.Requires(Contract.ForAll(data, n => n == 42));
        }
    }
    class Foo : IFoo
    {
        public void Boo(int[] data)
        {
            Console.WriteLine("Foo.Boo was called!");
        }
    }
    


    In this case, the Foo.Boo method does not contain preconditions at all and ccrewrite must first find the contract class ( IFooContracts ), “tear out” the contract from the IFooContracts.Boo method and transfer it to the Foo.Boo method . In the case of simple preconditions, it is not difficult to do this, but in the presence of closures, everything becomes more interesting.

    Now, you need to find the inner class IFooContracts. <> C , copy it to the Foo class , copy the call to Contract.Requires from the IFooContracts.Foo methodand update the IL so that it works with the new copy, and not with the original closure. In some cases, things are even more fun: the presence of nested closures (several scopes, each of which has an exciting anonymous method) will require updating the nested classes in the correct order - from the most nested to the topmost (which is why this logic is here ).

    Asynchronous method with two await



    Another change in the new compiler is related to the generated code for asynchronous methods. The old compiler generated different code for the asynchronous method with one await statement and with several await statements . The new compiler has a new optimization for asynchronous methods with two await , which also caused a lot of trouble.

    Let's look at the following simple example:

    public async Task FooAsync(string str)
    {
        Contract.Ensures(str != null);
        await Task.Delay(42);
        return 42;
    }
    


    The C # language compiler (pre-Roslyn) converts this code as follows:

    1. A structure is created that implements I AsyncStateMachine and all the logic of the method moves to the MoveNext method .
    2. The “facade” logic remained in the FooAsync method : creating an AsyncTaskMethodBuilder instance and initializing the state machine instance.

    Here's what the generated code looks like:

    private struct FooAsync_StatemMachine : IAsyncStateMachine
    {
        // Аргумент метода FooAsync(string str)
        public string str;
        // Состояние конечного автомата
        public int l__state;
        // Библиотечный класс для создания асинхронных операций.
        // Очень напоминает TaskCompletionSource.
        public AsyncTaskMethodBuilder t__builder;
        // "ожидатель" результатов запущенной задачи
        private TaskAwaiter u__taskAwaiter;
        public void MoveNext()
        {
            int num = this.l__state;
            int result;
            try
            {
                TaskAwaiter taskAwaiter = default(TaskAwaiter);
                if (num != 0)
                {
                    // Начало метода
                    // Именно сюда перекочевала проверка предусловий
                    Contract.Requires(this.str != null);
                    taskAwaiter = Task.Delay(42).GetAwaiter();
                    // Стандартный паттерн: возвращаем управление и используем
                    // этот же метод в качестве "продолжения": нас позовут,
                    // когда запущенная задача будет завершена
                    if (!taskAwaiter.IsCompleted)
                    {
                        // l__state равный 0 означает, что текущая операция
                        // запущена и мы ждем результатов.
                        this.l__state = 0;
                        // Передаем this AsyncTaskBuilder-у, чтобы он вызвал 
                        // этот же метод, когда текущая запущенная задача завершится
                        // t__bulder.AwaitUnsafeOnCompleted(..., this);
                        return;
                    }
                }
                // Сюда мы попадем только когда текущая задача, сохраненная
                // на предыдущем этапе, будет завершена.
                // Вызов GetResult приведет к генерацию исключения, если 
                // задача завершилась с ошибкой
                taskAwaiter.GetResult();
                // Устанавливаем результат исполнения
                result = 42;
            }
            catch (Exception exception)
            {
                // Метод завершился с ошибкой
                this.l__state = -2;
                this.t__builder.SetException(exception);
                return;
            }
            // Метод завершился успешно
            this.l__state = -2;
            this.t__builder.SetResult(result);
        }
    }
    public Task FooAsync(string str)
    {
        var stateMachine = new FooAsync_StatemMachine
        {
            l__state = -1,
            t__builder = AsyncTaskMethodBuilder.Create(),
            str = str,
        };
        stateMachine.t__builder.Start(ref stateMachine);
        return stateMachine.t__builder.Task;
    }
    


    There are quite a few letters, but the main idea is this:

    1. The precondition of the asynchronous method is inside the state machine. That is why ccrewrite must pull it and transfer it to the FooAsync method . Otherwise, violation of the precondition will lead to a faulted task, and not to a "synchronous exception".
    2. There is a specific pattern for how ccrewrite determines where a precondition is. In the case of an asynchronous method with one await operator , the original beginning of the method, and therefore the preconditions, are immediately inside the if (num! = 0) condition . It is important!
    3. The generated code depends on the number of await statements inside the asynchronous method. With two or more await statements, the old compiler generates a state machine based on the switch, and ccrewrite handled this pattern correctly.

    The C # 6.0 compiler generates the same code for the asynchronous method with one await, but completely different code, if there are two await.

    NOTE
    Another change to the C # 6.0 compiler: in Debug mode, a class, not a structure, is generated for the state machine. This is done to support Edit and Continue.

    If the FooAsync method is changed as follows:

    public async Task FooAsyncOrig(string str)
    {
        Contract.Ensures(str != null);
        await Task.Delay(42);
        await Task.Delay(43);
        return 42;
    }
    


    That C # 6.0 compiler, instead of generating a switch that is understandable to any decompiler and ccrewrite, will generate code very similar to code with one await statement , but with minor modifications:

    // Начало метода MoveNext
    if (num != 0)
    {
        // ccrewrite считал, что здесь находится предусловие!
        if (num == 1)
        {
              taskAwaiter = this.u__taskAwaiter;
              this.u__taskAwaiter = default(TaskAwaiter);
              this.l__state = -1;
              goto OperationCompleted;
        }
        // А оно находится здесь!
        Contract.Requires(this.str != null);
        taskAwaiter = Task.Delay(42).GetAwaiter();
    


    Since this is a new pattern, ccrewrite naively searched for contracts immediately inside the if condition (num! = 0) and considered the nested if as preconditions / postconditions. I had to teach him new tricks in order to process this option correctly.

    In conclusion



    Work at the IL level is walking on thin ice. The search for patterns is quite complicated, modifying the IL code is not intuitive, and even a simple task like checking postconditions in asynchronous methods can be very demanding. In addition, many things are parts of the compiler implementation and may vary from version to version. Here we examined only a few examples, but this is far from all of the changes on the part of the C # 6.0 compiler. At least the IL code generated when using expression trees, which also broke several test cases, has changed a little .

    There are still a couple of unpleasant bugs that are being worked on. There is a problem with Error List in VS2015 , and postconditions in asynchronous methodsApparently, they never worked normally. But, most importantly, the project is alive and, most likely, will develop. So if you have any wishes, especially in the field of ccrewrite, write about it or start bugs on github !

    References


    1. Code Contracts on GitHub
    2. Code Contracts Editor Extensions on github
    3. Latest release on github
    4. Code Contracts at Visual Studio Gallery
    5. Code Contracts Editor Extensions at Visual Studio Gallery
    6. A series of articles on contract programming in .NET

    Also popular now: