Pex 0.6 Released

We just released another milestone for Pex: version 0.6, still under the Microsoft Research License. Ideally you have Visual Studio 2008 Professional to get the full experience, but all you really need is .NET 2.0. Take a look at exercise 3 in the tutorial to get started in Visual Studio 2008 Professional, and exercise 4 shows you how to use the command-line.

There have been a bunch of changes that we documented in the release notes, most notably some UI polishing, and finally, the ability to install Pex under a 64-bit Windows operating system!

64-bit support: Pex 0.6 installs on 64-bit Windows (but cannot analyze 64-bit-only code)

We have taken some precautions that all processes that Pex launches are 32-bit processes. Since Pex actually runs your code during the analysis to generate test inputs, this will only work when the code that you want to analyze is marked as "Any CPU" or "x86", but not "X64" (or "Itanium"). This is normally not an issue.

And you can run the generated tests on any platform (assuming your test framework supports other platforms; note that MSTest only supports 32-bit as well).

Why Pex cares about 32-bit vs. 64-bit

Pex analyzes .NET code, and you would think that it shouldn't matter for such a tool whether it runs in a 32-bit or 64-bit environment. The only difference should be how many bytes a pointer/object reference occupies, and a .NET program cannot observe such implementation details, right?

Indeed, it is true that most safe .NET applications couldn't care less about the different pointer sizes.

But Pex can not only analyze safe .NET code, but also unsafe .NET code. (In fact, many of the methods of the .NET framework are implemented using unsafe code, such as string.Equals.) In unsafe .NET code, conversions between integers and pointers happen all the time. Some conversions are explicit, and many more are implicit in the code generated by the C#.

To keep things simple, let me show you an example with an explicit conversion. The following is a parameterized unit test that has quite different behaviors depending on whether it is running in 32-bit or 64-bit mode. Can you guess in which mode the "bug" can occur?

    1: [PexMethod]

    2: public unsafe void TestX86(long x)

    3: {

    4:     void* p = (void*)x;

    5:     if (p == null && x == (1L<<32))

    6:         throw new Exception("bug!");

    7: }

Answer: Only in 32-bit mode. There, the conversion from long to (void*) ignores the upper 32-bits, which can then be freely assigned in any way. Pex finds the following in 32-bit mode:

In words: When calling TestX86 with the value 4294967296, the exception is thrown. In 32-bit mode, that is. In 64-bit mode, the exception cannot be thrown for any value.

Does the difference in behavior between 32-bit and 64-bit really matter in practice?

For most purposes, probably not. (Unless you are writing unsafe code, and you are concerned about buffer-overflows and such.) In any case, you can just take the generated test suite and run it on any platform you wish. 

Why don't you just recompile Pex for 64-bit then?

We were asked on our mailing list why we couldn't just recompile Pex for 64-bit. As you have seen above, it is not that simple, since Pex and its constraint solver needs to reason about different constraints depending on the bitness. All the explicit and implicit conversions in the .NET instruction have different meanings.

But a true 64-bit version of Pex is not that distant: My main development machine runs 64-bit Vista, and I implemented all relevant conversion for 64-bit as well. The main problem is that our automated testing process for Pex runs on a 32-bit Vista machine. Testing Pex itself for both 32-bit and 64-bit environments would double our testing matrix.

Comments

• Anonymous
  August 06, 2008
  PingBack from http://blog.a-foton.ru/2008/08/pex-06-released/

• Anonymous
  August 08, 2008
  Das Microsoft Research Team rund um Pex hat eine neue Version von Pex released wie Nikolai Tillmann in

• Anonymous
  August 08, 2008
  I’m a bit late with the news, but the guys at Microsoft Research has released a new version of Pex . 

• Anonymous
  August 16, 2008
  I've not looked at Pex (Program EXploration) yet but it seems pretty interesting. The previous version