PEX & Code Digger

Every developer eventually faces the challenge of testing. It is tempting to say, "I'm a developer, not a tester – writing tests is not my job." Unfortunately, that is rarely how things work in practice. Writing exhaustive tests takes time, and achieving high code coverage while also handling edge cases is tedious work. You need to verify not only that the code does what it should, but also that it does not fail unexpectedly due to an overlooked case.

Fortunately, Microsoft Research has a tool to help: Pex. With Pex, you can worry a lot less about test coverage (well, maybe that is a slight exaggeration 😉). Pex analyzes compiled code, making it compatible with all .NET languages, and automatically generates tests with the highest possible coverage for each method. Its goal is not to validate business logic (it cannot guess what the developer intended), but to ensure all code paths are exercised. Pex identifies the minimal set of arguments needed to traverse every branch of a method, without generating redundant tests for the same branch.

To do this, rather than generating random arguments (fuzzing), Pex understands the code and derives precise arguments using the Z3 engine

Let's start with a rather simple example:

public static void AnswerToTheUltimateQuestionOfLifeTheUniverseAndEverything(int i)
{
    if (i > 41)
        return;

    throw new Exception("Try again...");
}

Pex finds the right answer 😃. Let's see an example of what Pex offers with a slightly more complicated mathematical example:

public static void TestMath(object o, int[] values)
{
    // Preconditions
    if (values == null)
        throw new ArgumentNullException("values");
    if (values.Length < 3)
        throw new ArgumentException("values must have at least 3 elements", "values");

    if (values[0] == values[1] / 2)
    {
        o.ToString(); // NullReferenceException
    }
    else if (values[0] + values[1] == (values[1] * 71 + values[2] + 42) / 2)
    {
        throw new Exception("Simple equation");
    }

    // Pex makes it possible to check that 2 numbers are coprime integers!
    // The proof using the Bachet-Bézout theorem (https://en.wikipedia.org/wiki/Coprime_integers)
    if (41 * values[0] + 42 * values[1] == GCD(41, 42)) // 41x+42y=1
    {
        throw new Exception("41 and 42 are coprimes");
    }
}

private static int GCD(int a, int b)
{
    return b == 0 ? a : GCD(b, a % b);
}

As you can see, exceptions thrown on arguments (ArgumentNullException, ArgumentException, ArgumentOutOfRangeException, etc.) are treated as valid (green), while others are treated as errors (red). You can tell Pex that a specific exception is expected:

Here's the result:

In addition to solving equations, Pex also understands Regex:

public static void TestString(string s)
{
    if (Regex.IsMatch(s, @"\w+\d{2}"))
        throw new Exception("Match");
}

However, there are many cases Pex cannot solve:

public void TestXml(XDocument doc)
{
    if (doc == null)
        throw new ArgumentNullException("doc");
    if (doc.Descendants("Tests").Any())
        throw new Exception(); // Pex can't create the XDocument itself
}

Finding interesting test values is useful, but Pex can also save the generated unit tests so you can replay them later. For each analyzed class, Pex generates the following files:

• One file per class: {class name}Test.cs
• One file per method of the class: {class name}Test.{method name}.g.cs

The first file contains test stubs of the type:

[PexMethod, PexAllowedException(typeof(ArgumentException)), PexAllowedException(typeof(ArgumentNullException)), PexAllowedException(typeof(Exception))]
public void TestMath(object o, int[] values)
{
    Program.TestMath(o, values);
    // TODO: add assertions to method ProgramTest.TestMath(StringBuilder, Int32[])
}

The second file contains the tests with the values found by Pex during the analysis:

[TestMethod]
[PexGeneratedBy(typeof(ProgramTest))]
[PexRaisedException(typeof(NullReferenceException))]
public void TestMathThrowsNullReferenceException543()
{
    int[] ints = new int[3];
    this.TestMath((StringBuilder)null, ints);
}

[TestMethod]
[PexGeneratedBy(typeof(ProgramTest))]
public void TestMath900()
{
    int[] ints = new int[3];
    ints[0] = 427;
    ints[1] = 8;
    ints[2] = 245;
    this.TestMath((StringBuilder)null, ints);
}

The advantage of using stubs is that you can add assertions for the expected behavior, which will then be verified against every test case Pex generates.

For those wondering whether Pex only works with MSTest: it does not. Pex can generate code for multiple test frameworks, including MSTest, xUnit.Net, NUnit, and MbUnit.

As shown, Pex integrates directly into Visual Studio 2008 and 2010, so you never need to leave your development environment. Just right-click on the method you want to test and Pex starts. The main limitation is the lack of support for Visual Studio 2012 and 2013.

For Visual Studio 2012, the team released the Microsoft Code Digger plugin, which generates interesting argument sets for a method but does not support test generation. It is equally easy to use: right-click and select Generate Inputs / Outputs Table.

Finally, Pex can also be run from the command line (see the documentation), making it easy to integrate into a nightly build.

This post is a brief overview of Pex. For a deeper look at its capabilities, I recommend reading the official PDF manual from the Pex team: http://research.microsoft.com/en-us/projects/pex/pexmanual.pdf

PS: If you are not yet convinced, try the online version: http://www.pexforfun.com/

Do you have a question or a suggestion about this post? Contact me!