Capturing async postcondition generates invalid IL

[SergeyTeplyakov]

Yet another issue with async postconditions (see #155, #156 for other cases).

If async postcondition captures state, resulting IL is invalid. Here is an example:

    class Foo
    {
        private int _limit = 42;
        private bool _wasThrown = false;
        public async Task<int> FooAsync()
        {
            // Currently this code lead to unverifiable code!
            Contract.Ensures(Contract.Result<int>() == _limit);
            Contract.EnsuresOnThrow<InvalidOperationException>(_wasThrown);

            await Task.Delay(42);

            return 42;
        }
    }

In this case ccrewrite will generate following code for async closure CheckPost method:

private class <FooAsync>AsyncContractClosure_0
{
    public Task<int> CheckPost(Task<int> task)
    {
        TaskStatus status = task.Status;
        if (status == TaskStatus.RanToCompletion && __ContractsRuntime.insideContractEvaluation <= 4)
        {
            try
            {
                __ContractsRuntime.insideContractEvaluation++;
                Task<int> task2;
                RewriterMethods.Ensures(task2.Result == this._limit, null, "Contract.Result<int>() == _limit");
            }
            finally
            {
                __ContractsRuntime.insideContractEvaluation--;
            }
        }
        TaskStatus status2 = task.Status;
        if (status2 == TaskStatus.Faulted)
        {
            AggregateException exception = task.Exception;
            bool flag = this.CheckException(exception);
        }
        return task;
    }
    public bool CheckException(Exception e)
    {
        InvalidOperationException ex = e as InvalidOperationException;
        if (ex != null)
        {
            RewriterMethods.EnsuresOnThrow(this._wasThrown, null, "_wasThrown", ex);
        }
        else
        {
            AggregateException ex2 = e as AggregateException;
            if (ex2 != null)
            {
                Func<Exception, bool> predicate = new Func<Exception, bool>(this.CheckException);
                ex2.Handle(predicate);
            }
        }
        return true;
    }
}

So both methods: CheckPost and CheckException are using this._limit and this._wasThrown respectively. But those fields are in the parent class, there is now such fields in the closure class.

This code will not fail during runtime, but peverify will complain about type mismatch.

UPDATE: changing Foo from class to struct will lead to runtime failure: InvalidProgramException.

[sharwell]

❓ Is this a Roslyn-specific bug, or does it happen with the legacy compiler as well?

❓ Does this happen always, or only when /optimize is passed to the compiler?

[SergeyTeplyakov]

It is not Roslyn-specific. Async postconditions were never implemented properly.

[SergeyTeplyakov]

And yes, this happen always. Just because there is no logic in the EmitAsyncClosure class that will replace all the locals to the outer class fields.

[SergeyTeplyakov]

Changing Foo from class to struct changes the behavior. In that case the app will crash with InvalidProgramException.