Figure 4: Eclipse Output for MyClass1
In the above output the path conditions (marked with brown arrows) show you the test cases:
Test Case 1: y = -9999999, x = 10000000
Test Case 2: y = -10000000, x = 10000000
Test Case 1 corresponds to the z>0 branch of myMethod's if statement.
Test Case 2 corresponds to the z≤0 branch of the if statement.
Extending the Example: Filtering the Test Cases
Let's modify the MyClass1.myMethod() example a bit. Suppose you have another class with a slightly different method:
public class MyClass2 {
... etc ...
private int myMethod2(int x, int y) {
int z = x + y;
if (z > 0) {
z = 1;
}
if (x < 5) {
z = -z;
}
return z;
}
... etc ...
}
To generate test cases for this method you create a new Eclipse run configuration and add a main() method to MyClass2, as before:
+vm.insn_factory.class=gov.nasa.jpf.symbc.SymbolicInstructionFactory
+vm.classpath=.
+vm.storage.class=
+symbolic.method=myMethod2(sym#sym)
+search.multiple_errors=true
+jpf.report.console.finished=
MyClass2
The parts that have changed are in bold. Here is the code with the new driver:
import gov.nasa.jpf.symbc.Debug;
... etc ...
public class MyClass2 {
... etc ...
private int myMethod2(int x, int y) {
int z = x + y;
if (z > 0) {
z = 1;
}
if (x < 5) {
z = -z;
}
return z;
}
... etc ...
// The test driver
public static void main(String[] args) {
MyClass2 mc = new MyClass2();
int x = mc.myMethod2(1, 2);
Debug.printPC("\nMyClass2.myMethod2 Path Condition: ");
}
}
If you run this as in the previous example, you will get four test cases which test the four possible paths through the method:
Test Case 1: y = 10000000, x = -9999999
Test Case 2: y = -4, x = 5
Test Case 3: y = -10000000, x = -10000000
Test Case 4: y = -10000000, x = 5
However, suppose that you are only interested in the test cases where exactly one of the if statements is executed.
That is, you only care about Test Case 2 and Test Case 3.
You could, of course, just run JPF as above and filter these out by hand.
But that would be both tedious and inefficient if your myMethod2() had fifty consecutive if statements.
If you are allowed to annotate your method's code, there is another approach: use Verify.ignoreIf() to force JPF to backtrack when more than one if statement fires.
For example, you can annotate myMethod2() as follows:
import gov.nasa.jpf.jvm.Verify;
import gov.nasa.jpf.symbc.Debug;
... etc ...
public class MyClass2 {
... etc ...
private int myMethod2(int x, int y) {
int jpfIfCounter = 0;
int z = x + y;
if (z > 0) {
jpfIfCounter++;
z = 1;
}
if (x < 5) {
jpfIfCounter++;
Verify.ignoreIf(jpfIfCounter > 1);
z = -z;
}
Verify.ignoreIf(jpfIfCounter == 0);
return z;
}
... etc ...
// The test driver
public static void main(String[] args) {
MyClass2 mc = new MyClass2();
int x = mc.myMethod2(1, 2);
Debug.printPC("\nMyClass2.myMethod2 Path Condition: ");
}
}
The added annotations are shown in bold.
This code is in extensions/symbc/examples/MyClass2.java.
Now you can execute this symbolically and you will only get the two test cases you need:
Test Case 1: y = -4, x = 5
Test Case 2: y = -10000000, x = -10000000
Extending the Example: Adding Preconditions
Suppose again that you want to restrict the test cases generated, but now the problem is that you believe that your method will only be called with certain ranges of parameters.
For example, in MyClass1.myMethod() you believe that x and y are restricted to the ranges -100 ≤ x ≤ 100 and 1 ≤ y ≤ 3.
Enforcing these requirements during symbolic execution is easy — you do not even need to modify myMethod()'s original code.
Instead you can use preconditions implemented in the driver.
For the sake of variety we will use a separate class to implement the driver, MyDriver1.
import gov.nasa.jpf.symbc.Debug;
public class MyDriver1 {
// The method whose parameters are marked as symbolic.
private static void imposePreconditions(int x, int y) {
MyClass1 mc = new MyClass1();
if (-100 <= x && x <= 100 && 1 <= y && y <= 3) {
mc.myMethod(x, y);
Debug.printPC("\nMyClass1.myMethod Path Condition: ");
}
}
// The test driver
public static void main(String[] args) {
// Actual arguments are ignored when doing symbolic execution.
imposePreconditions(1,2);
}
}
Because you need preconditions and because you do not want to modify MyClass1,
the method you call symbolically is MyDriver1.imposePreconditions(), not MyClass1.myMethod().
Note that imposePreconditions()'s parameters are x and y, the parameters to myMethod() that you want to be symbolic.
This code is in extensions/symbc/examples/MyDriver1.java.
Create an Eclipse run configuration for MyDriver1, pasting the following into the Program Arguments box on the Arguments config page:
+vm.insn_factory.class=gov.nasa.jpf.symbc.SymbolicInstructionFactory
+vm.classpath=.
+vm.storage.class=
+symbolic.method=imposePreconditions(sym#sym)
+search.multiple_errors=true
+jpf.report.console.finished=
MyDriver1
Running MyDriver1 produces the test cases with the desired range restrictions:
Test Case 1: y = 1, x = 0
Test Case 2: y = 1, x = -100
Floating Point Arguments
Methods with float and double parameters are handled exactly the same as ones with int parameters, though the output is slightly different.
Here is a quick illustration.
import gov.nasa.jpf.symbc.Debug;
public class MyClassFP {
public double myMethodFP(double x, double y) {
double z = x + y;
if (z > 0.0) {
z = 1.0;
} else {
z = z - x;
}
z = 2.0 * z;
return z;
}
// The test driver
public static void main(String[] args) {
MyClassFP mc = new MyClassFP();
double x = mc.myMethodFP(1.0, 22.0);
Debug.printPC("\nMyClassFP.myMethodFP Path Condition: ");
}
}
MyClassFP.myMethodFP() is the same as MyClass1.myMethod() except that everything is a double, not an int:
Its code is in extensions/symbc/examples/MyClassFP.java.
The Eclipse run config parameters are:
+vm.insn_factory.class=gov.nasa.jpf.symbc.SymbolicInstructionFactory
+vm.classpath=.
+vm.storage.class=
+symbolic.method=myMethodFP(sym#sym)
+search.multiple_errors=true
+jpf.report.console.finished=
MyClassFP
And the resulting test cases are:
Test Case 1: y = -4.99999991632194E-7, x = -50.00000025000001
Test Case 2: y = 0.0, x = 0.0
Test Case 3: y = -4.99999991632194E-7, x = 50.00000025000001
At this point you might wonder why there are three test cases instead of the two you got when the parameters were integers.
The answer is that JPF operates on the JVM bytecodes, not the Java source code. When z is a floating point variable, the code
if (z > 0.0) {
z = 1.0;
} else {
z = z - x;
}
is compiled as though it were (conceptually, at least) something like
if (z > 0.0) {
z = 1.0;
} else if (z == 0.0 || z < 0.0) {
z = z - x;
}
So you get one test case for z > 0.0, one for z == 0.0, and one for z < 0.0.
Object Fields
Instead of doing symbolic evaluation of method parameters, you might need to do it with fields of objects.
One way to do this is to have your driver assign symbolic method parameters to the object's fields:
public class MyClassWithFields {
public int field1;
public int field2;
public void myMethod1() {
...etc...
}
}
public class MyDriverForFields {
private static void makeFieldsSymbolic(int x, int y) {
MyClassWithFields mc = new MyClassWithFields();
mc.field1 = x;
mc.field2 = y;
mc.myMethod1();
Debug.printPC("\nMyClassWithFields.myMethod1 Path Condition: ");
}
// The test driver
public static void main(String[] args) {
makeFieldsSymbolic(1,2);
}
}
This, along with these Eclipse run config parameters:
+vm.insn_factory.class=gov.nasa.jpf.symbc.SymbolicInstructionFactory
+vm.classpath=.
+vm.storage.class=
+symbolic.method=makeFieldsSymbolic(sym#sym)
+search.multiple_errors=true
+jpf.report.console.finished=
MyDriverForFields
will do the trick.
The other way to do this is with the @Symbolic() annotation:
public class MyClassWithFields {
@Symbolic("true")
public int field1;
@Symbolic("true")
public int field2;
public void myMethod1() {
int z = field1 + field2;
if (z > 0) {
z = 1;
} else {
z = z - field1;
}
z = field1 * z;
return z;
}
}
public class MyDriverForFields {
// The test driver
public static void main(String[] args) {
MyClassWithFields mc = new MyClassWithFields();
mc.myMethod1();
Debug.printPC("\nMyClassWithFields.myMethod1 Path Condition: ");
}
}
and with these Eclipse run config parameters:
+vm.insn_factory.class=gov.nasa.jpf.symbc.SymbolicInstructionFactory
+vm.classpath=.
+vm.storage.class=
+symbolic.method=myMethod1()
+search.multiple_errors=true
+jpf.report.console.finished=
MyDriverForFields
will produce the same results as above, namely:
Test Case 1: field2 = -9999999, field2 = 10000000
Test Case 2: field2 = -10000000, field2 = -10000000
(as usual, these classes are in extensions/symbc/examples/MyClassWithFields.java and
extensions/symbc/examples/MyDriverForFields.java).
A Larger Example: Code Coverage and Validation
Suppose you not only need test cases for each path through your code, but for each test case you also need to know which path it covers.
This can be done easily enough by annotating your code.
However, whenever you annotate your code (i.e. change it) you run the risk of introducing bugs.
(We skipped over this problem in the earlier annotation example.)
So we need a way of verifying that the test cases we generate have the same effect on the original code as they do on the annotated code.
To make all this happen we will do the following:
- Annotate each "path segment" in the code (typically, each clause of an
if statement) with an identifier for that segment.
- Run the test case on the original code and verify that we get the same results
Our original code consists of a bunch of if statements.
We will keep track of the path by assigning an ID to each branch of each if statement and appending that ID to a string variable when the segment is executed.
To verify that each test case produces the same result in both versions of the code we will extract the symbolic variable values from the path condition and run them through both versions, comparing the results.
Finally, we will print the path taken by each test case along with the input values.
This is the original code, in the package coverage:
package coverage;
public class MyClassOriginal {
public int myMethod(int x, int y) {
int z = x + y;
if (z > 0) {
z = 1;
} else {
z = z - x;
}
if (x < 0) {
z = z * 2;
} else if (x < 10) {
z = z + 2;
} else {
z = -z;
}
if (y < 5) {
z = z - 12;
} else {
z = z - 30;
}
return z;
}
}
Now for the code with the annotations to identify the path taken.
The variable path holds the string describing the path taken.
For the "path segment" IDs, we use human-readable descriptions like "z>0 ".
At the end of myMethod() we have also added a call that validates and prints the test case: CheckCoverage.processTestCase().
CheckCoverage is discussed in more detail later.
package coverage;
public class MyClassWithPathAnnotations {
public int myMethod(int x, int y) {
StringBuilder path = new StringBuilder();
int z = x + y;
if (z > 0) {
path.append("z>0 ");
z = 1;
} else {
path.append("z<=0 ");
z = z - x;
}
if (x < 0) {
path.append("x<0 ");
z = z * 2;
} else if (x < 10) {
path.append("0<=x<10 ");
z = z + 2;
} else {
path.append("x>=10 ");
z = -z;
}
if (y < 5) {
path.append("y<5 ");
z = z - 12;
} else {
path.append("y>=5 ");
z = z - 30;
}
CheckCoverage.processTestCase(path.toString());
return z;
}
}
And this is the driver:
package coverage;
public class MyDriverForPathAnnotations {
// The test driver
public static void main(String[] args) {
MyClassWithPathAnnotations mca = new MyClassWithPathAnnotations();
mca.myMethod(1, 2);
}
}
The trickiest part here is CheckCoverage.processTestCase().
To understand this part, you will have to recall that when you run your programs under JPF, there are actually two VMs involved.
Your code runs under JPF's VM, but JPF runs under a native JVM.
You use JPF's "native interface", JMI, to comunicate between the two VMs.
You need to know this because we will need to get the current path condition, extract from it the current variables and their values, validate those values, and print the test cases.
But the current path condition and its class (gov.nasa.jpf.symbc.numeric.PathCondition) do not exist in the JVM your code is running in.
Your code runs in the JPF VM, but path conditions exist only in the base JVM, i.e. the Sun JVM in which JPF itself runs.
With that in mind, here is the code for CheckCoverage.
As always with JMI, there are two parts: a declaration on the JPF VM side for class CheckCoverage and an implementation on the base JVM side for the peer class JPF_coverage_CheckCoverage.
package coverage;
public class CheckCoverage {
public static void processTestCase(String path) {}
}
package coverage;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Map;
import java.util.Set;
import gov.nasa.jpf.jvm.MJIEnv;
import gov.nasa.jpf.symbc.JPF_gov_nasa_jpf_symbc_Debug;
import gov.nasa.jpf.symbc.numeric.PathCondition;
public class JPF_coverage_CheckCoverage {
private static Set paths = new HashSet();
private static int caseNum = 0;
public static void processTestCase(MJIEnv env, int objRef, int pathRef) {
String path = env.getStringObject(pathRef);
if (! paths.contains(path)) {
paths.add(path);
Map varsVals = getPcVarsVals(env);
int x = (Integer)varsVals.get("x");
int y = (Integer)varsVals.get("y");
int origZ = new MyClassOriginal().myMethod(x, y);
int annoZ = new MyClassWithPathAnnotations().myMethod(x, y);
caseNum++;
if (origZ == annoZ) {
System.out.format("TestCase %s: x = %s y = %s\nPath: %s\n\n",
caseNum, x, y, path);
} else {
System.out.format("Error for TestCase %s: x = %s y = %s\nPath: %s\n\n",
caseNum, x, y, path);
System.out.format("The annotated and original code got different results.\n" +
"Annotated Result: %s\n" +
"Original Result: %s\n\n",
annoZ, origZ);
}
} else {
System.out.println("Already saw '" + path + "'");
}
}
private static Map getPcVarsVals(MJIEnv env) {
Map varsVals = new HashMap();
PathCondition pc = JPF_gov_nasa_jpf_symbc_Debug.getPC(env);
if (pc != null) {
pc.solve();
pc.header.getVarVals(varsVals);
}
return varsVals;
}
}
All of this code is in extensions/symbc/examples/coverage.
Here is the Eclipse run config data needed to run it:
+vm.insn_factory.class=gov.nasa.jpf.symbc.SymbolicInstructionFactory
+vm.classpath=.
+vm.storage.class=
+symbolic.method=myMethod(sym#sym)
+search.multiple_errors=true
+jpf.report.console.finished=
coverage.MyDriverForPathAnnotations
And here is what you get for output when you run it:
Figure 5: Eclipse Output With Annotations
One thing you might notice here is that there are only ten test cases, but if you do the math, there should be 2*3*2=12.
The missing two test cases would have the paths z<=0 0<=x<10 y>=5 and z<=0 x>=10 y>=5.
It turns out these cannot happen: at the first if statement, z = x + y, so if you work out the inequalities, you will find there are no values for x and x that will generate these paths.
The cool thing is that JPF and Choco figure this out automatically.
Other Examples
The test directory, extensions/symbc/test/gov/nasa/jpf/symbc, has lots of examples but they cover pretty much the same ground as the ones above.
Common Problems
If you do not see a line at the start of your output similar to the one labeled myMethod() is called symbolically in
