BadImageFormatException when using Contract.Ensures in async method, that returns task without any await

[Dennis-Petrov]

Hi. This code:

class Program
{
    static Task<T> Foo<T>(T source)
        where T : class
    {
        Contract.Ensures(Contract.Result<T>() != null);

        return Task.FromResult(source);
    }

    static void Main(string[] args)
    {
        Foo(new object()).Wait();
    }
}

leads to BadImageFormatException, while this one - does not:

    static async Task<T> Foo<T>(T source)
        where T : class
    {
        Contract.Ensures(Contract.Result<T>() != null);

        return await Task.FromResult(source);
    }

The only difference is awaiting the task in the second sample, which is totally unnecessary here.

It seems to me, that using Contract.Result<T>() in Foo is logically incorrect too .We're not awaiting a task result, we're just returning a task. Though, BadImageFormatException shouldn't be thrown, and I need a way to point CC to check task result here.

Is there any workarounds instead of await?

[yaakov-h]

I believe Contract.Result<T>() on a method returning Task<T> is only valid on async methods, but I'd expect a rewriter error, not a runtime error.

[SergeyTeplyakov]

@yaakov-h Contract.Result<T>() is valid for both: async and non-async methods.

I've check whether my fix (#159) helps this, but I'm not sure that it will.

BTW, please note, that this code fails on both: VS2015 and VS2013.

[SergeyTeplyakov]

BTW, please note, that switching to "async" does not help either: in this case there is no BadImageFormatException but resulting code is not valid.

For this code:

class Program
{
    public static async Task<T> Foo<T>(T source)
    where T : class
    {
        Contract.Ensures(Contract.Result<T>() != null);
        await Task.Yield();
        return source;
        //return Task.FromResult(source);
    }

    static void Main(string[] args)
    {
        Foo("foo").Wait();
    }
}

ccrewrite generates following code:

public static Task<T> Foo<T>(T source) where T : class
{
    Program.<Foo>d__0<T> <Foo>d__;
    <Foo>d__.source = source;
    <Foo>d__.<>t__builder = AsyncTaskMethodBuilder<T>.Create();
    <Foo>d__.<>1__state = -1;
    AsyncTaskMethodBuilder<T> <>t__builder = <Foo>d__.<>t__builder;
    <>t__builder.Start<Program.<Foo>d__0<T>>(ref <Foo>d__);
    Task<T> task = <Foo>d__.<>t__builder.Task;
    Task<T> task2 = task;
    if (__ContractsRuntime.insideContractEvaluation <= 4)
    {
        try
        {
            __ContractsRuntime.insideContractEvaluation++;
            __ContractsRuntime.Ensures(task2.Result != null, null, "Contract.Result<T>() != null");
        }
        finally
        {
            __ContractsRuntime.insideContractEvaluation--;
        }
    }
    return task2;
}

I.e. the postcondition is synchronous and not asynchronous!

[SergeyTeplyakov]

@Dennis-Petrov I've posted PR (#278) with a fix. Will appreciate some feedback:)

[Dennis-Petrov]

@SergeyTeplyakov, sorry, I've lost sight of this issue.
This particular case is fixed in RC, but code below still raises BadImageFormat:

class Program
{
    static void Main(string[] args)
    {
        new Foo().GetBarsAsync<object>().Wait();
    }
}

[ContractClass(typeof(FooContract))]
interface IFoo
{
    Task<IEnumerable<T>> GetBarsAsync<T>();
}

[ContractClassFor(typeof(IFoo))]
abstract class FooContract : IFoo
{
    public Task<IEnumerable<T>> GetBarsAsync<T>()
    {
        Contract.Ensures(Contract.Result<IEnumerable<T>>() != null);

        throw new NotImplementedException();
    }
}

class Foo : IFoo
{
    public Task<IEnumerable<T>> GetBarsAsync<T>()
    {
        return Task.FromResult(Enumerable.Empty<T>());
    }
}

P.S. I've installed fresh build from master branch (built using VS2013) - the problem still persists.

[DzheiZee]

Using 1.10.20606.1
Still encountering such defect.
Is fix for this defect included into given version (afaik it is the latest released version)