Monday, April 29, 2013

Microsoft Pex: Understanding Assumptions, Assertions, and Test-Case Failures

In a previous post we started using Microsoft Pex and showed how it helped exploring all possible code paths, and how that helped discovering a defect in our program logic. In that example, even our program logic is defective, all test cases succeeded. A test case fails if there is an un-caught exception or a failed assertion.

To see an example of a failed test case and how Pex could help in fixing it, let’s add the following basic function to our code:

public void Add(ArrayList a, object o)
{
a.Add(o);
}

when you run Pex for that simple method, you get the following results:


ConsoleApplication2 - Microsoft Visual Studio_2013-04-24_15-46-30


As you might expected, the ArrayList object might be NULL. In situations similar to this one, when a higher-level component (the code that called Add() method) passes malformed data to a lower-level component(that Add() method), which the lower-level component rejects, then the higher-level component should be prevented from doing so in the first place.


One way to achieve this is to promote the failure condition of the lower-level component to the abstraction level of the higher-level component. This is what the Add Precondition feature of Pex does: It expresses a low-level failure condition at the abstraction level of the code under test. When added to the code-under-test as argument validation code—also called a precondition—then this effectively prevents the code under test from causing a failure somewhere in its execution. In other words, the Add Precondition feature doesn’t completely fix an error, but it promotes the failure condition to a higher, more appropriate abstraction level.


To add a precondition to your code, click the failed test case row, then on the details section (right) click Add Precondition, as in picture below


002 - 200 - Exploring Code with Microsoft Pex.docx [Compatibility Mode] - Word_2013-04-25_08-56-05


Pex will open Preview and Apply updates dialog box to show you the proposed code modifications that Pex will do.


Preview and Apply updates_2013-04-25_09-00-24


Review and Click Apply. The modified method will look like:

        
public void Add(ArrayList a, object o)
{
//
Debug.Assert(a != (ArrayList)null, "a");
//

a.Add(o);
}

When you run Pex for our method now, we will not find a failed test case.


The concept of assertions is well known in unit test frameworks. Pex understands the built-in Assert classes provided by each supported test framework. However, most frameworks do not provide a corresponding Assume class as Pex did. PexAssume is a class to express assumptions, i.e. a precondition. The methods of this class can be used to filter out undesirable test inputs. If you do not want to use an existing test framework, Pex also has the PexAssert class. Some functionalities can be achieved using attributes instead of PexAssume methods, like PexAssumeNotNullAttribute and PexAssumeUnderTestAttribute.

 
[PexMethod]
public void Test1(object o) //precondition: o should not be null
{
PexAssume.IsNotNull(o);
...
}

[PexMethod]
public void Test2([PexAssumeNotNull]object o) //precondition: o should not be null
{
...
}

When you write an assertion, Pex will not only passively detect assertion violations, but Pex will in fact actively try to compute test inputs that will cause the assertion to fail (just as an assertion might throw a PexAssertFailedException). Pes uses these exceptions internally to stop a test case when an assumption fails.


Expected Exceptions


You can annotate the test—or the test class, or the test assembly—with one of the following attributes to indicate which exception types can or must be thrown by the test in order to be considered successful:


  • PexAllowedExceptionAttribute indicates that a test method, or any other method that it calls directly or indirectly, can throw a particular type of exception for some test inputs.
    using System;
    using Microsoft.Pex.Framework;
    using Microsoft.Pex.Framework.Validation;

    namespace ConsoleApplication3
    {
    class Stack
    {
    int[] _elements;
    int _count;
    public Stack(int capacity)
    {
    if (capacity < 0) throw new ArgumentOutOfRangeException();
    _elements = new int[capacity];
    _count = 0;
    }
    }

    [PexClass]
    public partial class StackTest
    {
    [PexMethod]
    [PexAllowedException(typeof(ArgumentOutOfRangeException))]
    public void CtorTest(int capacity) // will not fail
    {
    Stack s = new Stack(capacity); // may throw ArgumentOutOfRangeException
    }
    }
    }

  • PexAllowedExceptionFromTypeAttribute indicates that any method of a specified type can throw a particular type of exception for some test inputs.
    using System;
    using System.Collections;
    using Microsoft.Pex.Framework;
    using Microsoft.Pex.Framework.Validation;

    namespace ConsoleApplication3
    {
    [PexClass]
    public partial class ArrayListTest
    {
    [PexMethod]
    [PexAllowedExceptionFromType(typeof(NullReferenceException), typeof(ArrayListTest))]
    public void Add1(ArrayList a, object o) //will not fail
    {
    a.Add(o);
    }
    }
    }

  • PexAllowedExceptionFromTypeUnderTestAttribute indicates that any method of the designated type under test can throw a particular type of exception for some test inputs.
  • PexAllowedExceptionFromAssemblyAttribute indicates that any method located in a specified assembly can throw a particular type of exception for some test inputs.

When Does Pex Emit a Test Case?


Pex supports different filters that decide when generated test inputs will be emitted as a test case. You can configure these filters with the TestEmissionFilter property that you can set for example in the PexMethod attribute. Possible values are the following:



  • All Emit every generated test input as a test case, including those that cause assumption violations.
  • FailuresAndIncreasedBranchHits (default) Emit tests for all unique failures, and whenever a test case increases coverage, as controlled by the TestEmissionBranchHits property (take values 1 or 2).
  • FailuresAndUniquePaths Emit tests for all failures Pex finds, and also for each test input that causes a unique execution path.
  • Failures Emit tests for failures only.

Regarding increased branch coverage, the TestEmissionBranchHits property controls how a branch is covered. For example:


  • TestEmissionBranchHits=1: Whether Pex should just consider whether a branch was covered at all. This gives a very small test suite that covers all branches Pex could reach. In particular, this test suite also covers all reached basic blocks and statements.
  • TestEmissionBranchHits=2: Whether a test covered it either once or twice.

The default is TestEmissionBranchHits=2, which generates a more expressive test suite that is also better suited to detect future regression errors.

using System;
using Microsoft.Pex.Framework;
using Microsoft.Pex.Framework.Settings;

namespace ConsoleApplication3
{
[PexClass]
partial class TestEmission
{
int max(int x, int y)
{
if (x > y)
return x;
else
return y;
}

[PexMethod(TestEmissionFilter=Microsoft.Pex.Framework.Settings.PexTestEmissionFilter.All)]
public void MaxTest1(int a, int b, int c, int d) // 1 test case generated
{
int e = max(a, b);
PexObserve.ValueForViewing("max", e);
}

[PexMethod(TestEmissionFilter = Microsoft.Pex.Framework.Settings.PexTestEmissionFilter.Failures)]
public void MaxTest2(int a, int b, int c, int d) // No test cases generated
{
int e = max(a, b);
PexObserve.ValueForViewing("max", e);
}
}
}

When Does Pex Stop ?


If the code under test does not contain loops or unbounded recursion, Pex will typically stop quickly because there is only a (small) finite number of execution paths to analyze. However, most interesting programs contain loops and/or unbounded recursion. In such cases the number of execution paths is (practically) infinite, and it is in general undecidable whether a statement is reachable. In other words, Pex would take forever to analyze all execution paths of the program.

In order to make sure that Pex terminates after a reasonable amount of time, there are several exploration bounds. All bounds have predefined default values, which you can override to let Pex analyze more and longer execution paths. The bounds are parameters of the PexMethod, PexClass, and PexAssemblySettings attributes. There are different kinds of bounds:


  • Constraint Solving Bounds: apply to each attempt of Pex to determine whether an execution path is feasible or not. Pex might need several constraint solving attempts to compute the next test inputs.

    • ConstraintSolverTimeOut Seconds the constraint solver has to figure out inputs that will cause a different execution path to be taken.
    • ConstraintSolverMemoryLimit Megabytes the constraint solver can use to figure out inputs.

  • Exploration Path Bounds: apply to each execution path that Pex executes and monitors. These bounds make sure that the program does not get stuck in an infinite loop, or recursive method.

    • MaxBranches Maximum number of branches that can be taken along a single execution path.
    • MaxCalls Maximum number of calls that can be taken during a single execution path.
    • MaxStack Maximum size of the stack at any time during a single execution path, measured in number of active call frames.
    • MaxConditions Maximum number of conditions over the inputs that can be checked during a single execution path.

  • Exploration Bounds apply to the exploration of each parameterized unit test.

    • MaxRuns Maximum number of runs that will be tried during an exploration (each run uses different test inputs; not every run will result in the emission of a new test case).
    • MaxRunsWithoutNewTests Maximum number of consecutive runs without a new test being emitted.
    • MaxRunsWithUniquePaths Maximum number of runs with unique execution paths that will be tried during an exploration.
    • MaxExceptions Maximum number of exceptions that can be found over all discovered execution paths combined.
    • MaxExecutionTreeNodes Maximum number of conditions over the inputs that can be checked during all discovered execution paths combined.
    • MaxWorkingSet Maximum size of working set in megabytes.
    • TimeOut Seconds after which exploration stops.

The following example shows a parameterized test that involves a loop. The loop bound depends on the test inputs, and the exception can only be triggered if the loop is executed a certain number of times. Here, we used an explicit bound of 10 runs MaxRuns=10 to let Pex finish quickly. However, with this bound, Pex will most likely not be able to trigger the exception, as Pex will not unroll the loop sufficiently many times:

 [PexMethod(MaxRuns = 10)]
public void TestWithLoop(int n)
{
var sum = 0;
for (int i = 0; i < n; i++)
sum++;
if (sum > 20) throw new Exception();
}

In the Pex Exploration Results you may see the Exception statement reached, but you will see on the Pex tool bar that there is 1 boundry reached. ConsoleApplication2 - Microsoft Visual Studio_2013-04-28_15-01-11 If you click on it, you will see more details:
ConsoleApplication2 - Microsoft Visual Studio_2013-04-28_15-04-15
on the right, you could click Set MaxRuns=20 to increase the MaxRuns boundry. You could do the same from the Pex tool bar ConsoleApplication2 - Microsoft Visual Studio_2013-04-28_15-15-32 and also setting boundary to infinity. Both actions will open a dialog to review and approve the code changes.

The following example shows another parameterized test that involves a loop, but this loop does not depend on the test inputs. Here, we used an explicit bound of 10 branches MaxBranches=10 to let Pex finish quickly. However, with this bound, Pex cannot even once execute the code from beginning to end, as executing the embedded loop will cause more than 10 branches to be executed.

 [PexMethod(MaxBranches = 10)]
public void TestWithFixedLoop(int j)
{
var sum = 0;
for (int i = 0; i < 15; i++)
sum++;
if (j == 10) throw new Exception();
}

In those cases, where a particular run exceeded some path-specific bounds, we get a special row in the results. ConsoleApplication2 - Microsoft Visual Studio_2013-04-28_15-28-43 The Set MaxBranches= button on the results tool can be used to increase the bounds.ConsoleApplication2 - Microsoft Visual Studio_2013-04-28_15-31-57 If you increased the boundary to 20, you will get all you branched executed and the exception statement reached.

In this post we talked about how and when a test case fail, how to use precondition and assumptions to differentiate between failures from your unit code and failures from malformed input, how to allow specific exception to be raised from your tests without causing it to fail, how to control which test inputs should Pex use as a test case, and finally how to control the Pex stop criteria whether through  bounding the constraint solver, or bounding the exploration paths, or bounding the exploration runs.

Friday, April 26, 2013

Getting started with Microsoft Code Digger

Microsoft Code Digger is Visual Studio 2012 extension that have been released few days ago by RiSE team at Microsoft Research (the same team who developed Pex). You can download the it from the Visual Studio Gallery here.

Microsoft Code Digger uses the same engine that Pex uses, and the same techniques under the hood (dynamic symbolic execution and constraint solvers). The only constrain that Code Digger have is that it only works on public .NET code in Portable Class Libraries.

Let’s try it

After installing the Code Digger extension for Visual Studio 2012, create a Portable Class Library. Let’s use the Triang() method we used in previous posts as an example here. Your code should look like:

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

namespace PortableClassLibrary1
{
public class Class1
{
public static int Triang(int Side1, int Side2, int Side3)
{
int triOut;

// triOut is output from the routine:
// Triang = 1 if triangle is scalene
// Triang = 2 if triangle is isosceles
// Triang = 3 if triangle is equilateral
// Triang = 4 if not a triangle

// A quick confirmation that it's a valid triangle
if (Side1 <= 0 || Side2 <= 0 || Side3 <= 0)
{
triOut = 4;
return (triOut);
}

// Detect any sides of equal sides
triOut = 0;
if (Side1 == Side2)
triOut = triOut + 1;
if (Side1 == Side3)
triOut = triOut + 2;
if (Side2 == Side3)
triOut = triOut + 3;
if (triOut == 0)
{
if ((Side1 + Side2 <= Side3) || (Side2 + Side3 <= Side1) || (Side1 + Side3 <= Side2)) // confirm that it is a valid triangle
triOut = 4;
else
triOut = 1;
return (triOut);
}

if (triOut > 3)
triOut = 3;
else if ((triOut == 1) && (Side1 + Side2 > Side3))
triOut = 2;
else if ((triOut == 2) && (Side1 + Side3 > Side2))
triOut = 2;
else if ((triOut == 3) && (Side2 + Side3 > Side1))
triOut = 2;
else
triOut = 4;
return (triOut);
}
}
}

Right click inside Triang() method and wait for few seconds. You will see the below Inputs / Outputs pane.


PortableClassLibrary1 - Microsoft Visual Studio_2013-04-24_14-17-51 


It’s the same set we got before from Pex and for the same reasons. No surprises, both tools use the same engine under hood.

Thursday, April 25, 2013

Why Pex Choose These Inputs

In the example we gave in the previous post, it may seem that Pex chose random numbers as inputs for the Triang() method but it is not. But also its not all possible values for the inputs.

Actually, Pex generates test inputs by analyzing your program code, so it is called whitebox test generation (as opposed to blackbox test generation). For every statement in the code, Pex will eventually try to create a test input that will reach that statement. Pex will do a case analysis for every conditional branch in the code—for example, if statements, assertions, and all operations that can throw exceptions.

In other words, the number of test inputs that Pex generates depends on the number and possible combinations of conditional branches in the code (if interested to know more about that, search for symbolic execution). Pex operates in a feedback loop: it executes the code multiple times and learns about the program behavior by monitoring the control and data flow.

After each run, Pex does the following:

  • Chooses a branch that was not covered previously.
  • Builds a constraint system that describes how to reach that branch.
  • Uses a constraint solver to determine new test inputs that fulfill the constraints, if any exist.

The test is executed again with the new inputs, and the process repeats. On each run, Pex might discover new code and dig deeper into the implementation. In this way, Pex explores the behavior of the code. 

Because our code doesn’t have any conditions that test zero length sides, Pex generated zero an input and also shows that our program is defective (because it considers a triangle with (0,0,0) as equilateral and (1,0,1) as isosceles). If we added the following lines of code after declaring triOut and before doing anything.

            
// A quick confirmation that it's a valid triangle
if (Side1 <= 0 || Side2 <= 0 || Side3 <= 0)
{
triOut = 4;
return (triOut);
}

You will get a different set of test inputs from Pex that reveal more code path combinations.


ConsoleApplication2 - Microsoft Visual Studio_2013-04-24_13-06-48


We mentioned before that pex generates test input by performing a symoblic analysis of the code under test. You can use the method GetPathConditionString of the PexSymbolicValue class to obtain a textual representation of the current path condition, a predicate (condition) that characterizes an execution path. The ToString method of PexSymbolicValue class gives you a textual representation of how a value was derived from the test input provided. To do so, add reference to Pex Framework dll (located at "C:\Program Files\Microsoft Moles\PublicAssemblies\Microsoft.Pex.Framework.dll"). Add using Microsoft.Pex.Framework; to your code then add the following code anywhere in your code to get details about the code path at that point.


PexObserve.ValueForViewing("Condition", PexSymbolicValue.GetPathConditionString());
PexObserve.ValueForViewing("Return Value", PexSymbolicValue.ToString(Triang(1, 1, 1)) );

Here I added it into the Triang() method we used before. Run Pex and you will see the new columns added to the results populated with conditions that led to .


ConsoleApplication2 - Microsoft Visual Studio_2013-04-25_11-49-50


ToRawString method and GetRawPathConditionString method return expressions representing symbolic values and the path condition, formatted as S-expressions.


Method PexObserve.ValueForViewing can also be used to display the value picked by Pex for any variable at any point in your code.


The same engine Pex uses is now available as part of Code Digger, a Visual Studio 2012 extension. We will talk about it in a future post.

Wednesday, April 24, 2013

Getting started with Microsoft Pex

Microsoft Pex is a white box test generation for .NET that came out of Microsoft Research and have been successfully integrated into Visual Studio 2010. It have been a result of collaborative work between Microsoft Research and the Automated Software Engineering Research Group at North Carolina State University led by  Dr. Tao Xie.

You can download and install Microsoft Pex for Visual Studio 2010 from here. We have talked in a previous post about parameterized unit tests and the possibilities it brings. In this post and the following we will explore Microsoft Pex and how it can help you in understanding the input/output behavior of your code, finding inputs that cause the code-under-test to crash, and exploring parameterized unit tests to check whether your code implements the desired functionality for all inputs.

Running Pex for the First Time

In Visual Studio click File > New > Project. In the left pane of the New Project dialog box, click Visual C#. In the center pane, click Console Application, pick a Name for it and click OK. Replace your class Program with the following class. It just the classic triangle classification program :

class Program
{
public static String[] triTypes = { "", // Ignore 0.
"scalene", "isoscelese", "equilateral", "not a valid triangle"};
public static String instructions = "This is the ancient TriType program.\nEnter three integers that represent the lengths of the sides of a triangle.\nThe triangle will be categorized as either scalene, isosceles, equilateral\n or invalid.\n";

public static void Main()
{
int A, B, C;
int T;

Console.WriteLine(instructions);
Console.WriteLine("Enter side 1: ");
A = getN();
Console.WriteLine("Enter side 2: ");
B = getN();
Console.WriteLine("Enter side 3: ");
C = getN();
T = Triang(A, B, C);

Console.WriteLine("Result is: " + triTypes[T]);
Console.ReadLine();
}

public static int Triang(int Side1, int Side2, int Side3)
{
int triOut;

// triOut is output from the routine:
// Triang = 1 if triangle is scalene
// Triang = 2 if triangle is isosceles
// Triang = 3 if triangle is equilateral
// Triang = 4 if not a triangle

// A quick confirmation that it's a valid triangle
if (Side1 <= 0 || Side2 <= 0 || Side3 <= 0)
{
triOut = 4;
return (triOut);
}

// Detect any sides of equal sides
triOut = 0;
if (Side1 == Side2)
triOut = triOut + 1;
if (Side1 == Side3)
triOut = triOut + 2;
if (Side2 == Side3)
triOut = triOut + 3;
if (triOut == 0)
{
if ((Side1 + Side2 <= Side3) || (Side2 + Side3 <= Side1) || (Side1 + Side3 <= Side2)) // confirm that it is a valid triangle
triOut = 4;
else
triOut = 1;
return (triOut);
}

if (triOut > 3)
triOut = 3;
else if ((triOut == 1) && (Side1 + Side2 > Side3))
triOut = 2;
else if ((triOut == 2) && (Side1 + Side3 > Side2))
triOut = 2;
else if ((triOut == 3) && (Side2 + Side3 > Side1))
triOut = 2;
else
triOut = 4;
return (triOut);
}

In the Build menu, click Build Solution.


To run Pex on your code, right-click in the body of the Triang method, and click Run Pex. If this is your first time running Pex, the Pex: Select a Test Framework dialog box appears. You could select your preferred test frame (Visual Studio Unit test, or NUnit)  and provide the installation path for its, then click OK. This dialog box will not appear again after you select the test framework. After a brief pause, Pex shows the results of its analysis in the Pex Exploration Results window. When you run Microsoft Pex on your .NET code, Pex generates test cases by analyzing the code-under-test. For every statement in the code, Pex will eventually try to create a test input that will reach that statement. Pex will do a case analysis for every conditional branch in the code—for example, if statements, assertions, and all operations that can throw exceptions. Each row in the table contains input/output values for the method under consideration(Traing). In the Pex Exploration Results window, click one row in the table on the left to see details in the right pane. You could select these rows and save them as unit tests. These details also displayed on the right in the Pex Explorer pane as test cases. ConsoleApplication2 - Microsoft Visual Studio_2013-04-23_16-45-40


On the next post we will explain why Pex chose these values, and other Pex stuff :)

Monday, April 22, 2013

Unit Tests vs Parametrized Unit Tests

Unit Tests

Using the conventions of NUnit unit tests as test methods contained in test classes. A parameterless method decorated with a custom attribute like [TestMethod] is a test method. Usually, each unit test explores a particular aspect of the behavior of the class-under-test.

Here is a unit test written in C# that adds an element to a .NET ArrayList instance. The test first creates a new array list, where the parameter to the constructor is the initial capacity, then adds a new object to the array list, and finally checks that the addition was correctly performed by verifying that a subsequent index lookup operation returns the new object.

[TestMethod] 
void TestAdd() 
{ 
 ArrayList a = new ArrayList(0); 
 object o = new object(); 
 a.Add(o); 
 Assert.IsTrue(a[0] == o); 
}

It is important to note that unit tests include a test oracle that compares observed behavior with expected results. By convention, the test oracle of a unit test is encoded using assertions. The test fails if any assertion fails or an exception is thrown. Unit test frame- works can also deal with expected exceptions. For a quick introduction about NUnit refer previous posts.

A test suite produced by unit testing with high code coverage gives confidence in the correctness of the tested code. However, writing unit tests to achieve high coverage can be time-consuming and tedious given that test execution frameworks only automate the test executions. You still have to write your test cases !

To address this problem, several automatic unit test generation tools such as Parasoft JTest or jCUTE can automatically generate conventional unit tests. These tools, nevertheless, cannot guarantee high code coverage, unless testers manually write some tests.

 


Parametrized Unit Tests


The unit test above specifies the behavior of the array list by example. Strictly speaking, this unit test only says that by adding a new object to an empty array list, this object becomes the first element of the list. What about other array lists and other objects?

[TestAxiom]
void TestAdd(ArrayList a, object o) 
{
 Assume.IsTrue(a!=null);
 int i = a.Count;
 a.Add(o);
 Assert.IsTrue(a[i] == o);
}

By adding parameters we can turn a closed unit test into a universally quantified conditional axiom that must hold for all inputs under specified assumptions.

Adding parameters to a unit test improves its expressiveness as a specification of intended behavior, but we lose concrete test cases. We can no longer execute this test axiom by itself. We need actual parameters. But which values must be provided to ensure sufficient and comprehensive testing? Which values can be chosen at all?

In the ArrayList example, if we study the internal structure of the .NET Framework implementation, we observe that there are two cases of interest. One occurs when adding an element to an array list that already has enough room for the new element (i.e. the array list’s capacity is greater than the current number of elements in the array list). The other occurs when the internal capacity of the array list must be increased before adding the element.

If we assume that library methods invoked by the ArrayList implementation are themselves correctly implemented, we can deduce that running exactly two test cases is sufficient to guarantee that the parametrized TestAdd(...) succeeds for all array lists and all objects.

[TestMethod]
void TestAddNoOverflow() 
{
 TestAdd(new ArrayList(1), new object());
}

[TestMethod]
void TestAddWithOverflow() 
{
 TestAdd(new ArrayList(0), new object());
}

Splitting axioms and test cases in this way is a separation of concerns:


  • First, we describe expected behavior as parametrized unit tests.
  • Then we study the case distinctions made by the code paths of the program under test to determine which inputs make sense for testing.

So, parametrized unit tests are more general specifications than conventional unit tests because it specifies the behavior for the whole input classes other than for a single concrete value of the input. But it needs concrete parameter values to be executed.


The good news is, Given a parametrized unit test, a test-generation tool, such as Microsoft Pex, can automatically generate tests with concrete inputs for the parameters to achieve high coverage. Pex explores the behaviors of a parametrized unit test using a technique called dynamic symbolic execution. Dynamic Symbolic Execution (DSE) is a variation of symbolic execution, which systematically explores feasible paths of the program under test by running the program with different test inputs to achieve high structural coverage. It collects the symbolic constraints on inputs obtained from predicates (condition statements like if else, switch,…) in branch statements along the execution and relies on a constraint solver [like Zap or Simplify] to solve the constraints and generate new test input for exploring new path. For each set of concrete test input that leads to a new path that achieves new coverage, Pex generates a corresponding conventional unit test. So, all what you have to do is write your parametrized unit test.


In this post we gave a brief overview about parametrized unit tests and its related research areas. It’s a very important concept to understand before start learning Microsoft Pex, which we will start . In later posts, we will explore Microsoft Pex in detail.