Async postconditions in generic methods

[SergeyTeplyakov]

This PR contains fixes for #235 and #275. Main change in this PR was made in EmitAsyncClosure class.

Special generic type mapping was added to correlate potentially different generic arguments from enclosing generic method to closure generic class.

[hubuk]

This delegate seems not to be used anywhere else so the calculation can be performed without it.

[SergeyTeplyakov]

You're right. I thought to extract method but left with "local" function. Will extract function.

[hubuk]

What if method is generic, but returned task uses declaring type generic parameter?
Something like this:

class DeclaringType<T> where T : class {
    public async Task<T> MethodAsync<U>() {
        Contract.Ensures(Contract.Result<T>() != null);
    }
}

or scenario with nested type:

class DeclaringType<T> where T : class {
    private class NestedType<U> where U : class {
        public async Task<T> MethodAsync<V>() {
            Contract.Ensures(Contract.Result<T>() != null);
        }
    }
}

Will this also work?

[SergeyTeplyakov]

Not sure. I'll test this code.

[SergeyTeplyakov]

Any other comments on this stuff? The change was relatively major, so I would like to get additional feedback on this...

/cc @sharwell

[hubuk]

Just out of curiosity. Why do you used CDATA here? is there any difference in just plain text in ?

[AlexanderTaeschner]

I assume, that the would be parsed as xml tag otherwise.

[SergeyTeplyakov]

@hubuk Yep, @AlexanderTaeschner is right. Otherwise we would have to encode all this < with < which is annoying...

[hubuk]

@SergeyTeplyakov I have found a few cases for which BadImageFormatException is thrown.
Some of them are reproducible before fix and some were introduced by the fix. I have prepared 192 combinations of class generic arguments and method arguments. With class and struct constraints. I will present a list of failing scenarios ASAP.

EDIT:
Async versions of some test cases did not throw an exception before fix. But as you observed in another example the generated IL was invalid anyway.

I was able to narrow down all the failing cases to the following two:

public class Outer<T> {
  public class Inner {
    public static Task<T> OuterClassTypeArgument(T obj) {
      Contract.Ensures(Contract.Result<T>() != null);
      return Task.FromResult(obj);
    }
  }
}
public static Task<T> DefaultValue<T>(T obj) {
// Does not throw when null is used instead of default(T)
  Contract.Ensures(!object.Equals(Contract.Result<T>(), default(T)));
  return Task.FromResult(obj);
}

// Constraint on Outer<T> class does not matter.
// Reproducible also before fix.
// System.BadImageFormatException thrown for:
// Program.Outer`1.Inner.OuterClassTypeArgument(T obj) method
Outer<object>.Inner.OuterClassTypeArgument(new object()).Wait();

// Constraint on method does not matter.
// Reproducible also before fix.
// Also fails (but only after the fix) when made async.
// Aggregated System.BadImageFormatException thrown for
// Program.<DefaultValue>AsyncContractClosure_0`1.CheckPost(Task`1 task)
DefaultValue(new object()).Wait();

[hubuk]

There is also some questionable behavior for closure class generation.

public class OuterClassGeneric<T0> where T0 : class {
  public class InnerGeneric<T1> {
    public static async Task<T0> AsyncTest1(T0 v0, T1 v1) {
      Contract.Ensures(Contract.Result<T0>() != null);
      return await Task.FromResult(v0);
    }
  }
}

rewriter generates the following closure class for the method above:

.class nested private auto ansi '<AsyncTest1>AsyncContractClosure_0`1'<class T0, T1, T1>
    extends [mscorlib]System.Object

Second T1 generic type parameter is probably not needed.

[hubuk]

Previously CheckPost method content was:

TaskStatus status = task.Status;
if (status == TaskStatus.RanToCompletion && __ContractsRuntime.insideContractEvaluation <= 4)
{
  try
  {
    __ContractsRuntime.insideContractEvaluation++;
    __ContractsRuntime.Ensures(task.Result != null, null, "Contract.Result<T0>() != null");
  }
  finally
  {
    __ContractsRuntime.insideContractEvaluation--;
  }
}
return task;

now it looks like:

TaskStatus status = task.Status;
if (status == TaskStatus.RanToCompletion)
{
  __ContractsRuntime.Ensures(task.Result != null, null, "Contract.Result<T0>() != null");
}
return task;

Is it intended change?

[SergeyTeplyakov]

@hubuk About last comment: the chnage is intented, because async postconditions are all about multi threading where thread static checks like __ContracatsRuntime.insideContractEvaluation just makes no sense.

[SergeyTeplyakov]

@hubuk Thanks a lot for clear test cases, I'll fix them and will update PR before pushing it to master.

[SergeyTeplyakov]

@hubuk FIxed everything that you've mentioned. Including two test cases that you've provde.

Once you'll sign off I'll move forward and will prepare new release of the CodeContracts.

[hubuk]

It seems that issue with public static Task<T> DefaultValue<T>(T obj) method is not reproducible even without the fix. Second issue is fixed by 2163f15.
LGTM 👍

[SergeyTeplyakov]

@hubuk Great. Moving forward to 1.10 release!