Unexpected BadImageFormatException in a GroupBy poscondition using CodeContract in VS2010 Beta1

Question

The attempt to run a custom GroupBy with the second of the following contract poscondition produces an unexpected bad image format error

static class ContractedQueryMethods {

 

  public static IEnumerable<IGrouping<K, T>> GroupBy<T, K>(this IEnumerable<T> source,

                                                           Func<T, K> selector) {

 

      //This poscondition is correctly verified in runtime

      Contract.Ensures(Contract.Result<IEnumerable<IGrouping<K, T>>>().

         Select(x => x.Count()).Sum() == source.Count(),

         "The total items of all groups is equal to the total items in the source");

     

      //The following poscondition produces an unexpected error during injection of the code!

      Contract.Ensures(Contract.ForAll<T>(

           source,

           (x => Contract.Result<IEnumerable<IGrouping<K, T>>>().Any(y => y.Contains(x)))),

           "Each item from the source belongs to some group");

 

      //...

 

      return Enumerable.GroupBy(source, selector);

     

  }

  //...

}

Message:

BadImageFormatException was unhandled

An attempt was made to load a program with an incorrect format (Exceptipn from HRESULT: 0x80070008

 

Answer 1

I was unable to reproduce it (using Beta 2), but I'm not sure I have the exact repro. Can you please send me (or post) a full program that shows the problem? You're seeing the error when the rewritten code is executed, right? So please also include a Main() that calls the method with the values that cause the error to appear.

Thanks! (And sorry for the error...)

Answer 2

Thanks Mike
Unfortunately the problem persist using Beta 2 and the Microsoft Code Contracts (devlabs_STD) 1.2.21023.14 for .NET Installer.
The following code reproduces the error
If you give me an email I will send the full code project

 

using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Diagnostics.Contracts;

namespace Weboo.Examples {

  #region Class definitions of Movie related types

  public class Film {
    public string Title;
    public string Genre;
    public string Director;
    public bool Oscar;
    public int Rating;
    public int Year;
    public Film(string title, string genre, string director, bool oscar, int rating, int year) {
      Title = title; Genre = genre; Director = director; Oscar = oscar; Rating = rating; Year = year;
    }
  }

  public class MovieDB {
    
     public static List<Film> Films;
     static MovieDB (){
        Films = new List<Film>();
        Films.Add(new Film("Titanic", "Drama", "James Cameron", true, 5, 1997));
        Films.Add(new Film("Dancing with Wolves", "Western", "Kevin Costner", true, 5, 1990));
        Films.Add(new Film("Jurassic Park", "Science Fiction", "Steven Spielberg", true, 4, 1993));
        Films.Add(new Film("Godfather", "____", "Francis Ford Coppola", true, 5, 1976));
        Films.Add(new Film("Godfather II", "____", "Francis Ford Coppola", true, 5, 1979));
        Films.Add(new Film("Unforgiven", "Western", "Clint Eastwood", true, 5, 1992));
        Films.Add(new Film("Taxi Driver", "Drama", "Martin Scorcese", true, 5, 1976));
        Films.Add(new Film("Madison Bridges", "Drama", "Clint Eastwood", false, 5, 1995));
        Films.Add(new Film("Goodfellas", "____", "Martin Scorcese", true, 4, 1990));
        Films.Add(new Film("Gangs of New York", "____", "Martin Scorcese", false, 4, 2002));
        Films.Add(new Film("Mistic River", "Drama", "Clint Eastwood", false, 4, 2004));
        Films.Add(new Film("Alien The Return", "Science Fiction", "James Cameron", false, 2, 1985));
        Films.Add(new Film("Schindler List", "Drama", "Steven Spielberg", true, 5, 1993));
        Films.Add(new Film("The Purple Color", "Drama", "Steven Spielberg", false, 5, 1985));
        Films.Add(new Film("Psycho", "Suspense", "Alfred Hichtcock", false, 5, 1960));
        Films.Add(new Film("Vertigo", "Suspense", "Alfred Hichtcock", true, 5, 1958));
        Films.Add(new Film("The Birds", "Suspense", "Alfred Hichtcock", true, 5, 1963));
        Films.Add(new Film("Cape Fear", "Suspense", "Martin Scorcese", false, 5, 1991));
      }
   }
 
  #endregion

  #region Putting contract to LINQ methods

  static class ContractedLINQMethods {

    #region GroupBy with posconditions
    //The following code shows how to put some posconditions to GroupBy method
    public static IEnumerable<IGrouping<K, T>> GroupBy<T, K>(this IEnumerable<T> source, Func<T, K> selector) {

      //This poscondition produces an unexpected error during injection of the code in the assembly (see attached image)
      Contract.Ensures(Contract.ForAll<T>(source, (x => Contract.Result<IEnumerable<IGrouping<K, T>>>().Any(y => y.Contains(x)))),
                       "Ensures that each item from the source belongs to some group");

      //GroupBy implementation
      return Enumerable.GroupBy(source, selector);

    }
    #endregion

  }
  #endregion

  
  //NOTE: Before execution check "Perfom Runtime Contract Checking" in the Code Contract property window
  class Program {
    static void Main(string[] args) {
      Console.WriteLine("\nGROUP BY");
      var byGenre = from f in MovieDB.Films group f by f.Genre;
      foreach (var g in byGenre) {
        Console.WriteLine("\n{0}", g.Key);
        Console.WriteLine("--------------------------");
        foreach (var f in g)
          Console.WriteLine(f.Title);
      }
      Console.ReadLine();
    }
  }
}

 

 

 

Answer 3

Thanks. Actually, we've been able to reproduce it and are working on it. The problem is that the anonymous delegate in the problematic contract doesn't capture any method-local state (i.e., the parameters) so the compiler creates a static generic method for it. (Otherwise the compiler generates a generic class with fields to hold the method-local state.) But we need to introduce a field to hold the return value of the method so it can be set by the method body and then accessed from that method. But the class is not generic, just the method. So we don't have anywhere to hang the field. We're not sure there is a good workaround at this point. It may have to wait until we have moved our tools onto the new infrastructure (which would allow us to support this).