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.
After we released Pex recently, I came across a couple of interesting blog posts of people who tried out Pex, for example Ben Hall, Peter, and Stan. They all ran Pex on a small example. In this post, I want to run Pex on a more complicated piece of code: The .Net ResourceReader, and all the other classes which it uses under the hood.
The ResourceReader takes a stream of data, and splits it up into individual chunks that represent resources. In that sense, the ResourceReader is a big parser.
Writing a parameterized unit test
I started by creating a new C# test project in Microsoft Visual Studio, and adding a reference to Microsoft.Pex.Framework. (If you try this at home, you need to install Pex first, of course.)
Then I wrote a very simple parameterized unit test for the resource reader. It takes any (non-null) array of bytes, creates an UnmanagedMemoryStream with the bytes, and then decodes it with the ResourceReader. It's not a particular expressive test, since it doesn't contain any assertions. All this test is really saying is that, no matter what the test inputs are, the code shouldn't throw any exception. (No exception at all? I'll investigate this in more detail later.)
1: [PexClass, TestClass]
2: public partial class ResourceReaderTest
3: { 4: [PexMethod]
5: public unsafe void ReadEntries([PexAssumeNotNull]byte[] data)
6: { 7: fixed (byte* p = data)
8: using (UnmanagedMemoryStream stream =
9: new UnmanagedMemoryStream(p, data.Length))
10: { 11: ResourceReader reader = new ResourceReader(stream);
12: foreach (var entry in reader) { /* just reading */ } 13: }
14: }
15: }
Let's run Pex.
Run Pex Exploration
I can now let Pex analyze this parameterized unit test in-depth by right-clicking on the parameterized unit test, and selecting Run Pex Exploration.
(I am running our latest internal Pex bits, and we just renamed the "Pex It" menu item to "Run Pex Exploration". So if you just see a "Pex It" menu item, use that.)
Pex now generates test inputs. In a nutshell, Pex runs the code, monitors what it's doing, and uses a constraint solver to determine more relevant test inputs that will take the program along different execution paths.
That sounds great, but the result is a little bit disappointing: Pex reports only two test inputs: An empty array, and an array with one element that is zero.
(Again, I have to say that I am running our latest internal Pex bits. If you see a big black empty region in the lower right part of the Pex Results, titled with "dynamic coverage", then you can get rid of this waste of screen real-estate by pressing the button that I circled in red:
We won't show this "dynamic coverage" graph by default anymore. I might talk more about this feature in the future. And now, back to the ResourceReader.)
Pex tells us in bold letters on red ground that it encountered 3 Uninstrumented Methods.
What does that mean? Well, Pex performs a dynamic analysis, which means that it runs the code, and then Pex monitors what the code is actually doing. However, Pex doesn't monitor all code, but only code that Pex instruments. Pex doesn't instrument all code by default, since the instrumentation and the monitoring comes with a huge performance overhead. And often it is not necessary to monitor all the code that is running. For example, when you want to test your algorithm, and your algorithm happens to write its progress to the console, then you still only want to test your algorithm, but not all the supporting code that hides behind Console.WriteLine.
Configuring what Pex analyzes: Instrumentation settings
But back to the ResourceReader: Let's click on the 3 Uninstrumented Methods warning.
We see that Pex neither instrumented UnmanagedMemoryStream nor ResourceReader. No wonder that Pex' analysis didn't find any really interesting test inputs! Pex also didn't monitor what happened in a call to GC.SuppressFinalize, but this relates to the .NET garbage collector, and probably isn't so important. (In fact, Pex has a built-in list of classes which don't need to be monitored, and we might add the GC class to this list in the future.)
Let's select UnmanagedMemoryStream..ctor (".ctor" is the generic .NET name for constructors),
and click on Instrument type, and repeat for ResourceReader..ctor. For GC.SuppressFinalize, I click on Ignore uninstrumented method instead. Pex persists my choices as assembly-level attributes in a new file called PexAssembyInfo.cs in the Properties folder. It now looks like this:
1: using Microsoft.Pex.Framework.Instrumentation;
2: using System.IO;
3: using System.Resources;
4: using Microsoft.Pex.Framework.Suppression;
5: using System;
6:
7: [assembly: PexInstrumentType(typeof(UnmanagedMemoryStream))]
8: [assembly: PexInstrumentType(typeof(ResourceReader))]
9: [assembly: PexSuppressUninstrumentedMethodFromType(typeof(GC))]
I let Pex run again. You can re-run the last exploration by clicking on the Play-button:
Pex did a little bit more this time -- three test cases! And another 7 Uninstrumented Methods warnings...
What are the uninstrumented methods this time?
As you can see, Pex' analysis already proceeded much deeper into the code, and now Pex hits all kinds of other methods. Most of the methods sound relevant. So I repeat the game, and let Pex instrument all of the types. And then I let Pex run again. Boom! Pex still reports some uninstrumented methods (and lots of other things which I'll explain another time), but Pex also doesn't stop so quickly anymore. Instead, Pex is having a ball and it keeps producing more and more test cases:
(If you run this example yourself, the precise results you get will vary. There is some non-deterministic code involved in the analysis.)
Pex even managed to produce a valid resource file! (here, row 215 with the green checkmark)
When you double-click on any row, Pex shows the generated unit test code. Here is the valid resource file:
2: [PexGeneratedBy(typeof(ResourceReaderTest))]
3: public void ReadEntriesByte_20080604_134738_032()
5: byte[] bs0 = new byte[55];
16: this.ReadEntries(bs0);
The resource file is 55 bytes long, and most bytes are zero, the default value of the byte type. All values which are not zero were carefully chosen by Pex to pass all the file-validation code of the ResourceReader.
Configuring the test oracle: Allowed exceptions
All the other rows are tagged with an ugly red cross, indicating that the test failed. Did these tests really fail? Let's see. In all cases, the code either throws a ArgumentNullException, ArgumentException, BadImageFormatException, IOException, NotSupportedException, or a FormatException.
These exceptions don't sound so unreasonable, considering that Pex tried obviously ill-formed test inputs in the course of its exploration.
If you look around the documentation of the ResourceReader (here, here, and here), you will find that in fact most of these exceptions are documented somewhere (although the documentation could be more explicit, and it's missing NotSupportedException).
I can inform Pex that these exceptions are okay. The easiest way to do that is to select a failing test case in the table, and then click on Allow It. Again, my choice is persisted as attributes in PexAssemblyInfo.cs:
1: [assembly: PexAllowedExceptionFromAssembly(typeof(ArgumentNullException), "mscorlib")]
2: [assembly: PexAllowedExceptionFromAssembly(typeof(BadImageFormatException), "mscorlib")]
3: [assembly: PexAllowedExceptionFromAssembly(typeof(ArgumentException), "mscorlib")]
4: [assembly: PexAllowedExceptionFromAssembly(typeof(NotSupportedException), "mscorlib")]
5: [assembly: PexAllowedExceptionFromAssembly(typeof(IOException), "mscorlib")]
6: [assembly: PexAllowedExceptionFromAssembly(typeof(FormatException), "mscorlib")]
When you run Pex again, all the exceptions that are marked as allowed are now tagged with friendly green checkmarks, indicating that they passed.
But what is that? An OverflowException... (here, the red cross in row 98) Yet another undocumented exception...
What can we learn from this exercise?
You have seen how to configure code instrumentation settings, and how to tell Pex that certain exceptions are okay.
But I think there is a much more interesting insight: By using Pex, we discovered some unexpected ways how some complicated library code behaves. Library code that we build our applications on. Documentation will always be imperfect, and we have to test our applications to make sure that we everything works correctly together. By using a white-box testing tool like Pex, that tried many relevant test inputs and not just one exemplary test input, we discovered behaviors (here, exceptions) we were not aware of before!
Stay tuned for more
That's it for today. Another time I might talk about the constraints that Pex had to solve to create a valid resource file, how to get an idea about how much code analyzed, how to visualize that Pex makes progress, and how to write more expressive parameterized unit tests.
This posting is provided "AS IS" with no warranties, and confers no rights.
Today we released the first version of Pex under a Microsoft Research License. Ideally you have Visual Studio 2008 Professional to get the full experience, but all you really need is .NET 2.0.
We even wrote a tutorial. While it's quite long, exercise 3 helps you to get started with Visual Studio 2008 Professional, and exercise 4 shows you how to use the command-line.
What is Pex?
Pex generates test inputs that cover all, or at least many of the corner cases in your .NET code. These test inputs are plugged into parameterized unit test that you write. The result is a small unit test suite, where each unit test calls the parameterized unit test with particular test inputs. There is a great picture on our main Pex page that illustrates this process.
Pex supports other unit test frameworks since the unit tests that Pex generates can be executed by other unit test frameworks without Pex. Pex comes with support for MSTest, the unit test framework of Visual Studio, out of the box. For support for other unit test frameworks, please look at the Pex Extensions project.
Parameterized unit tests have been around for quite some time already, under several names -- row tests, data-driven tests, theories, etc.
What is really unique about Pex is that it analyzes your .NET code, instruction by instruction, to understand what your code is doing. Then, in a fully automatic way, Pex computes relevant test inputs that trigger the corner cases of the code. When you write assertions, Pex will try to come up with test inputs that cause an assertion to fail.
Is Pex a new Microsoft product?
No, it's a prototype from Microsoft Research, developed mainly by two people. I started Pex in 2005, and Peli de Halleux joined the Pex team in 2006. Pex leverages other cool Microsoft Research technology, in particular the constraint solver Z3. We know that Pex has many rough edges, its version number is 0.5 for a reason.
Pex illustrates our vision how testing can be more powerful (and fun), without the difficulties of proving programs correct.
At this point we are mainly looking for feedback, and we want to see what it can do for other people.
Final Thoughts
To ask questions, get help, or just give feedback, please take a look at our mailing lists.
While Peli has blogged about Pex before, this is my first post. Stay tuned for more in-depth information on Pex at this place. I'll also talk about its history, and the other more or less related research projects I worked on in the past (AsmL, Spec Explorer, XRT).
Hope you have some fun with Pex,
Nikolai
Disclaimer: This posting is provided "AS IS" with no warranties, and confers no rights.
