Pex Usage Corner

Using Pex4Fun to explore Pex behavior

• The tip here can allow you to easily explore Pex behavior without even installing Pex but just rely on a browser.
• Step 1. Click http://pex4fun.com/default.aspx?language=CSharp&sample=_Template (or keep clicking the "New" menu as the last one near the top to get to the mode of "The code is a puzzle.", not the mode of "This puzzle is an interactive Coding Duel.", as indicated by the line above the code editing box)
• Step 2. Make sure that you include the following code snippet in the code editting box:

using System;

using Microsoft.Pex.Framework;

using Microsoft.Pex.Framework.Settings;

[PexClass]

public class Program

{

[PexMethod(TestEmissionFilter=PexTestEmissionFilter.All)]

public static string testMethod(int x, int y)

{

PexAssume.IsTrue(y >= 0);//replace here with your assumption

//... enter your code under test here

//if (x == 10000) throw new Exception();

PexAssert.IsTrue(y >= 0);//replace here with your assertion

return PexSymbolicValue.GetPathConditionString();

}

}

• Step 3. Observe the ordered list of test inputs being generated (i.e., the x and y columns) and the path condition corresponding to the generated test inputs (the "result" column) in the table displayed near the bottom.
  • Adding "[PexMethod(TestEmissionFilter=PexTestEmissionFilter.All)]" allows you not to filter out any test inputs generated/explored by Pex; without this annotation, Pex displays in the table ONLY the test inputs that achieve new block coverage. For more filtering/constraint options, see here.
  • Adding "return PexSymbolicValue.GetPathConditionString();" allows you to observe the path condition in the table as the "result" column.

Note: You can replace the API call of PexSymbolicValue.GetPathConditionString() with another API call defined on the PexSymbolicValue class. Please refer the MSDN documentation for this class. For excample, you can use PexSymbolicValue.ToRawString<T>(T) or PexSymbolicValue.ToString<T>(T) to turn a value into a string that represents the symbolic value. For example, you can turn the Puzzle method below

using System;

using Microsoft.Pex.Framework;

using Microsoft.Pex.Framework.Settings;

[PexClass]

public class Program

{

[PexMethod(TestEmissionFilter=PexTestEmissionFilter.All)]

public static int Puzzle(int x, int y)

{

//... the original puzzle code here

ret = ...;

return ret;

}

}

into the rewritten Puzzle method below with its return type replaced with string, and its return value of the method to be the combination of the path condition and the return value's symbolic expression:

using System;

using Microsoft.Pex.Framework;

using Microsoft.Pex.Framework.Settings;

[PexClass]

public class Program

{

[PexMethod(TestEmissionFilter=PexTestEmissionFilter.All)]

public static string Puzzle(int x, int y)

{

//... the original puzzle code here

ret = ...;

return "PC: " + PexSymbolicValue.GetPathConditionString() + " RET: " + PexSymbolicValue.ToString<int>(ret);

}

}

Even better, you can print the PUT name, PUT argument values, path condition, and return values' symbolic expression into a file with an example as below. First, you apply Pex on the the original PUT to generate CUTs from the PUT. Second, you replace the original PUT with the following revised PUT and run the generated CUTs (which invokes the new revised PUT). In this case, you don't need to change the return type of the PUT. In addition, you may use the same trick to construct a original PUT that includes comparing the return of the student solution puzzle and the return of the secret puzzle (see Section 4.3 of the ICSE 2016 SEET paper), and then replace such PUT with the revised one below.

using System;

using System.IO;

using Microsoft.Pex.Framework;

using Microsoft.Pex.Framework.Settings;

[PexClass]

public class Program

{

[PexMethod(TestEmissionFilter=PexTestEmissionFilter.All)]

public static int Puzzle(int x, int y)

{

//... the original puzzle code here

ret = ...;

string path = @"c:\temp\MyTest.txt"; //please make sure this file exists in your file system

using (StreamWriter sw = File.AppendText(path))

{ sw.WriteLine("Puzzle(" + x + "," + y + ") PC:" + PexSymbolicValue.GetPathConditionString() + " RET =" + PexSymbolicValue.ToString<int>(ret));

}

return ret;

}

}

=======

General debugging tips

• When you see that Pex doesn't cover a branch that you expect it to cover, you start your debugging process and try to create a micro-benchmark for this difficult branch
• It is good to see how Pex explores various paths. So you shall allow Pex to output all the tests (not filtering out any tests), each of which corresponds to one run/path
  • To do that, add [PexMethod(TestEmissionFilter=PexTestEmissionFilter.All)] for the PUT (replacing the original [PexMethod] or add the enclosed attribute value assignment to be within the existing [PexMethod])
  • When you include the above option, remember to add "using Microsoft.Pex.Framework.Settings;" in the beginning of the code.
• Look at coverage report generated by Pex
• Take a look at what these bounds mean
• For the reported un-instrumented methods, walk through them
  • All un-instrumented method issues should be dealt with as follows:
  • If the method is related to multi-threading, or an environment interaction that Pex can clearly not symbolically analyze anyway, then "Ignore Uninstrumented method"
    • Examples: Thread.Enter, Thread.Exit, Registry.GetKey, Network.Send
  • When you ignore uninstrumented methods, then it's important that Pex doesn't have to explore their argument validation code, which means that you might have to create object factories that supply concrete values, or mimic the argument validation
    • Example: the MailMessage constructor takes an email string. If MailMessage is not instrumented, Pex cannot get around the email-validation logic, and method always throws an exception. You will have to make sure that valid email strings are provided.
• Look at statements at the same block where some earlier statements are covered but later ones are not
  • Cause: exceptions are thrown by the last covered statement in the block
  • Look into the callee body of the last statement (if it contains a method call) to further investigate the coverage info in the callee method body
  • Put a break point on the last statement and rerun all the generated tests and start debugging
• Then look at all the tests and their associated information to debug
  • Especially look for the first (or many) tests that correspond to path bounds exceeded or duplicate paths
  • Put a break point in one such test
  • Click Tests-> Debug -> Tests in current context
  • The test execution will stop on the break point and then you walk through the path by F11/F10
  • Try to understand why Pex is not successful
• Creat a self-contained micro-benchmark to characterize the feature of the code related to the un-covered branch to cause difficulties for Pex
• Share your micro-benchmark with other students, Tao Xie, and/or Pex developers.

Useful tips

• Use PexSymbolicValue.IgnoreComputation to avoid exploration of a certain API. More details are here. It wraps a method into another method that won’t get monitored by Pex
  • For A a = b.f(x);, you can put "A a = PexSymbolicValue.IgnoreComputation( () => b.f(x))();"

Known issues (not resolved in Pex) and ways to get around

• Interfaces
  • when an argument type is an interface, if Pex cannt find any class in the references or the project code base under test to implement this interface, Pex will generate no objects. Such situations can happen inside a factory method
  • Solutions:
    • Option 1: add the classes implementing the interface to the references of the project under test
    • Additional guidance: add [PexUseType(typeof(C))] where C is the class implementing the interface for the PUT

Fitnex

Fitnex usage can be found at:

http://social.msdn.microsoft.com/Forums/en-US/pex/thread/e523461a-9372-46b9-af45-faa26690cedc/

http://go4answers.webhost4life.com/Example/achieve-certain-branch-node-asap-48849.aspx

Let's consider the following example to see when Fitnex won't work.

void int m(int[] a)

{

int count = 0;

for (int i = 0; i < a.length; i++)

{

if (a[i] > 0}

count ++;

}

if (count > 1000)

return -1;

return count;

}

Fitnex will NOT help cover the branch "if (count > 1000)". The reason is that count is not symbolic but a constant. Therefore, this branch is not flippable. Fitnex or any other Pex strategies would prioritize only the flippable branching nodes.

To fix this issue, you could replace the line of "int count = 0;" as

int count = PexChoose.Value<int>("count");

PexAssume.IsTrue(count == 0);

In this way, count is turned symbolic and then "if (count > 1000)" is flippable.

It seems that the latest version of Pex doesn't allow us to specify to use only Fitnex strategy. So the default Pex search strategy would be a combination of the Fitnex strategy and other strategies. So in the example below, you don't see that Pex would solely aggressively increase the loop bound or flip to the true branch in the loop body. In addition, when Pex flips the loop bound, it is not increment by 1 but by some increasing integer values.

Making constant inputs symbolic:

I found an API call, PexSymbolicValue.Internal.LoopVar<T>(string,T);

This method makes a variable of type T symbolic.

See the adjusted test case:

[PexMethod]

public void PuzzleTestThrowsPexAssertFailedException321(){

int input = PexSymbolicValue.Internal.LoopVar<int>("xPut", 4);

this.PuzzleTest(input); }

The output is as expected, a sequence of predicates for the PCs