Async postconditions are broken when task is cancelled

[SergeyTeplyakov]

As I mentioned in #155, async postconditions are implemented incorrectly right now.

Here is two additional examples.

class Foo
{
    private static bool _exceptionWasThrown;
    private static async Task FooAsync(CancellationToken token)
    {
        Contract.EnsuresOnThrow<InvalidOperationException>(_exceptionWasThrown);

        await Task.Delay(4200, token);

        //return 42;
    }

    public static async Task HandleFooAsync()
    {
        try
        {
            var cts = new CancellationTokenSource();
            cts.Cancel();
            // If async postcondition are implemented properly
            // they should not affect exception handling when the method throws.
            await FooAsync(cts.Token);

            throw new Exception("This should never happen!!");
        }
        catch (TaskCanceledException)
        {
            Console.WriteLine("Task was cancelled!");
        }
        catch (Exception e)
        {
            Console.WriteLine("UNEXPECTED: " + e);
        }
    }
}

To deal with EnsuresOnThrow ccrewrite generates bool CheckException(Exception) method that will throw if the assertion specified in a Contract.EnsuresOnThrow is not held. This method implemented correctly, but the call-site is wrong.

ccrewrite generates two different code patterns for generic and non-generic tasks and both of them lead to undesired behavior.

In the previous example non-generic tas was used, so ccrewrite will generate following code:

    public void CheckPost(Task task)
    {
        AggregateException ex = task.Exception as AggregateException;
        if (ex != null)
        {
            Func<Exception, bool> predicate = new Func<Exception, bool>(this.CheckException);
            ex.Handle(predicate);
            throw ex;
        }
    }

ccrewrite also mde following changes to the original async method:

private static Task FooAsync(CancellationToken token)
{
    Program.Foo.<FooAsync>AsyncContractClosure_0 @object = new Program.Foo.<FooAsync>AsyncContractClosure_0();
    Task task;
    try
    {
        Program.Foo.<FooAsync>d__9 <FooAsync>d__;
        <FooAsync>d__.token = token;
        <FooAsync>d__.<>t__builder = AsyncTaskMethodBuilder.Create();
        <FooAsync>d__.<>1__state = -1;
        AsyncTaskMethodBuilder <>t__builder = <FooAsync>d__.<>t__builder;
        <>t__builder.Start<Program.Foo.<FooAsync>d__9>(ref <FooAsync>d__);
        task = <FooAsync>d__.<>t__builder.Task;
    }
    catch (InvalidOperationException originalException)
    {
        __ContractsRuntime.EnsuresOnThrow(Program.Foo._exceptionWasThrown, null, "_exceptionWasThrown", originalException);
        throw;
    }
    Action<Task> continuationAction = new Action<Task>(@object.CheckPost);
    task = task.ContinueWith(continuationAction);
    return task;
}

Obviously, this code is not tollerant for cancellation. If the task was cancelled, CheckPost will swallow it. That's why running original code we'll get an exception with This should never happen!! message.

P.S. Changing FooAsync return type to Task<int> will change the picture. In this case original TaskCancelledException would be wrapped into another AggregateException and overall behavior would be invalid as well.