False Negative Unit Test with Pex, Contracts, and QuickGraph

Question

everyone. I have a perplexing interaction between contracts, pex, and quickgraph and would be very grateful for advice from the more knowledgeable. I have boiled it down to a repro case where commenting out one contract makes the false negative go away, but I have been unable to diagnose it with the debugger in the time allowed because the subject code (quickgraph) has side-effects in property-getters, meaning that the debugger executes the side effects when displaying the values of the properties, interfering with the actual order of execution.

First a little background, then the specifics, then a pointer to a project to download and try out, should you be so inclined as to dig in!

I installed Pex & Moles

http://research.microsoft.com/en-us/projects/pex/downloads.aspx

and CodeContracts for .NET 4.0

http://research.microsoft.com/en-us/projects/contracts/

I downloaded, via nuget, the most recent version of QuickGraph, which is all built for .NET 3.5. I pruned it to the minimum I needed, went into Project Properties for all, updated them all to .NET 4.0 from .NET 3.5 Client Profile, fixed one source breaking change (which was trivial and very, very unlikely to have any connection to my problem). I then went to the Code Contracts tab on every project page and enabled all static and dynamic options.

http://quickgraph.codeplex.com/releases/view/55262

The project has 192 unit tests, many of them Pex-generated (very nice!). To run the tests, get my project zip file from

http://dl.dropbox.com/u/1997638/QuickGraph.zip

Make sure you have Pex & Moles and Contracts from the links above. Open the solution, Rebuild everything, then, at the solution level, "Run All Tests In Solution" (control-R, A). All will pass. Then go to line 49 of IImplicitUndirectedGraphContracts.cs and uncomment the Contract under the large comment (inserted by me). One test, Prim12240WithDelegate will fail.

That test exercises a graph constructor that builds edges on-the-fly by calling a user-supplied delegate in the property-getters for Edges and EdgeCount. Cute. But something goes wrong with the Contract on line 49 of IImplicitUndirecteGraphContracts.cs.

This is a false negative, because if I comment out this contract, the test passes. In trying to follow this in the debugger, it has something to do with the timing of the creation of the Edges in the property getters. I haven't been able to disentangle this, however, because the debugger calls these getters, the subject code calls them, the contracts code calls them, maybe statically, maybe dynamically, I just plain got lost trying to follow it, and thought I'd bring the question up to those who understand the details of contract execution better than I.

Here is the offending contract; commenting it out makes the unit test succeed:

[Pure]
  IEnumerable<TEdge> IImplicitUndirectedGraph<TVertex, TEdge>.AdjacentEdges(TVertex v)
  {
    IImplicitUndirectedGraph<TVertex, TEdge> ithis = this;
    Contract.Requires(v != null);
    Contract.Requires(ithis.ContainsVertex(v));
    Contract.Ensures(Contract.Result<IEnumerable<TEdge>>() != null);
~~~~~~> Contract.Ensures(
      Enumerable.All(
        Contract.Result<IEnumerable<TEdge>>(),
        edge => 
          edge != null && 
          ithis.ContainsEdge(edge.Source, edge.Target) && 
          (edge.Source.Equals(v) || edge.Target.Equals(v))
        )
      );
    return default(IEnumerable<TEdge>);
  }

Answer 1

Pex has issues dealing with LINQ expressions in the .NET 4.0 runtime. from the first answer on this MSDN forum post for more details:

Our Linq support works for .NET 2.0/3.5 but we seem to have a regression for .NET4.0. If you are running 4.0, that would explain why Pex cannot generate interresting test cases - we don't instrument Linq correctly.

Why does Pex struggle with Linq anyway: in a nutshell, Linq uses DynamicMethod's to generate code. DynamicMethod methods are not reported to the profiler when they are jitted. Because our profiler cannot inject callbacks in the DynamicMethod, Pex cannot track the data flow through the Linq query. We have a workaround that intercepts the internals of the Linq to Object compiler and forces it to use Reflection.Emit instead.

This could have potentially made it ignore the Contract that you have commented out during its evaluation, leading to the false negative.