Async postconditions wraps original exception into additional AE

[SergeyTeplyakov]

Current implementation of the asynchronous postconditions is wrong. Consider following code:

static async Task<int> WillThrow()
{
    Contract.Ensures(Contract.Result<int>() == 42);

    await Task.Delay(42);
    throw new InvalidOperationException();
}

static async Task Run()
{
    try
    {
        await WillThrow();
    }
    catch (InvalidOperationException)
    {
        Console.WriteLine("Expected!");
    }
    catch (AggregateException ae)
    {
        Console.WriteLine("NOT EXPECTED!");
    }
}

In this case Expected! should be printed with or without any postconditions in the WillThrow method. Unfortunately, right now NOT EXPECTED! would be printed.

Here is a reason for this. ccrewrite uses following approach: AsyncClosure class is generated with int CheckPost(Task<int> task) method:

public int CheckPost(Task<int> task)
{
        int result = task.Result;
        if (__ContractsRuntime.insideContractEvaluation <= 4)
        {
            try
            {
                __ContractsRuntime.insideContractEvaluation++;
                __ContractsRuntime.Ensures(task.Result == 42, null, "Contract.Result<int>() == 42");
            }
            finally
            {
                __ContractsRuntime.insideContractEvaluation--;
            }
        }
        return result;
}

And following transformation are made for original async method:

public Task<int> WillThrow(string str)
{
    ThrowsWithAsyncPostconditionMixed.<WillThrow>AsyncContractClosure_0 @object = new ThrowsWithAsyncPostconditionMixed.<WillThrow>AsyncContractClosure_0();
    __ContractsRuntime.Requires(str != null, null, "str != null");
    ThrowsWithAsyncPostconditionMixed.<WillThrow>d__0 <WillThrow>d__;
    <WillThrow>d__.<>4__this = this;
    <WillThrow>d__.str = str;
    <WillThrow>d__.<>t__builder = AsyncTaskMethodBuilder<int>.Create();
    <WillThrow>d__.<>1__state = -1;
    AsyncTaskMethodBuilder<int> <>t__builder = <WillThrow>d__.<>t__builder;
    <>t__builder.Start<ThrowsWithAsyncPostconditionMixed.<WillThrow>d__0>(ref <WillThrow>d__);
    Task<int> task = <WillThrow>d__.<>t__builder.Task;
    Func<Task<int>, int> continuationFunction = new Func<Task<int>, int>(@object.CheckPost);
    return task.ContinueWith<int>(continuationFunction);
}

The problem here, that async method was changed to return new task that is result of the continuation task. But if original task fails, continuation function will try to get result via Result property. This will lead to AggregateException.

Basically, when the task faults original error would be wrapped into another AggregateException object that will break any clients that will try to handle them.

[sharwell]

The solution to this is given in a comment in #111. Note that the semantics given in the comment are C# code (referencing an open source library which behaves in the desired manner). Equivalent semantics will need to be implemented directly in IL to resolve the rewriter issue.

[SergeyTeplyakov]

Actually, I've implemented slightly different solution:)

Here is a comment from my implementatation:

    /// Current class generate AsyncClosure with CheckMethod and CheckException methods.
    /// 
    /// Following transformation are applied to the original async method:
    /// 
    /// // This is oroginal task, generated by the AsyncTaskMethodBuilder
    /// var originalTask = t_builder.Task;
    /// 
    /// var closure = new AsyncClosure();
    /// var task2 = originalTask.ContinueWith(closure.CheckPost).Unwrap();
    /// return task2;
    /// 
    /// There are 2 cases:
    /// 1) Task has no return value.
    /// In this case only EnsuresOnThrow could be used, and we emit:
    /// Task CheckMethod(Task t)
    /// {
    ///   if (t.Status == TaskStatus.Faulted)
    ///   {
    ///     // CheckException will throw if EnsuresOnThrow is not held
    ///     CheckException(t.Exception);
    ///   }
    /// 
    ///   return t;
    /// }
    /// 
    /// 2) Task(T) reutrns a T value.
    /// In this case both EnsuresOnThrow and Contract.Ensures(Contract.Result) could be used.
    /// We emit:
    /// 
    /// Task<int> CheckMethod(Task<int> t)
    /// {
    ///   if (t.Status == TaskStatus.Faulted)
    ///   {
    ///     // CheckException will throw if EnsuresOnThrow is not held
    ///     CheckException(t.Exception);
    ///   }
    ///   
    ///   if (t.Status == TaskStatus.RanToCompletion)
    ///   {
    ///      // Check ensures
    ///   }
    /// }

This is much easier solution that was proposed in the #111 and much easier than original implementation. I'll create a pull request shortly.

[Lukazoid]

I think I reported this issue back on the forums in 2013, it's nice to see it's finally getting fixed! See here for the original report.