Handling List, Map and String

[srgiri]

Hi,
From the wiki what I understand is:
1- JDart doesn't support string as symbolic. It means I cannot get test case values for a string.
2- JDart supports List and Map but the configuration needs to be different in the jpf file.

Could you please tell me how can I get test case values of List and Map and what what kind of condition I have to write for List and Map in the method, so that Jdart will solve it and will generate some test case values.
If in case it supports string, how can I get the test case value of a string. what configuration I have to write in the jpf file ?

Regards,
S R Giri

[ksluckow]

Hi!

1- JDart doesn't support string as symbolic. It means I cannot get test case values for a string.

Correct. JDart supports (fixed size) symbolic arrays, so you can have constraints on the elements of char[], e.g., equality.

2- JDart supports List and Map but the configuration needs to be different in the jpf file.

You can have a look in src/examples/simple/Input.java and the associated jpf files (in particular example.jpf and test_xyz.jpf) to see the configuration for Map. For List, replace the type in the config to java.util.List. You can extract the valuations obtained with JDart for the elements, but it does not automatically build the data structures as part of test suite generation; only for primitive types.

[srgiri]

Thank you for the response.

In TestSuiteGenerator.java line # 112: Method[] ms = cls.getMethods();
It gives a list of public methods. What if user wants to test a private method ? can this line be modified to Method[] ms = cls.getDeclaredMethods(); ?
Is there any significance of testing only public methods ?

[ksluckow]

Hi!
TestSuiteGenerator will generate a test suite for the target method. It assumes that this method is public when generating the test cases (which are based on code generation with a fairly simple template).
In my opinion, testing a private method is not a good idea, but if you want to have this feature, you can extend the code template with a check for whether the target method is private. If it is, you can add code for calling it reflectively.

[srgiri]

Hi,
Thank you very much for sharing the idea behind it.

I have one more doubt.
I observed that JDart is not generating any test case for equal (==) condition in List and Map. The coverage report shows it doesn't go into that branch.

Example:
if(m1.get("a") == m2.get("b"))
System.out.println("Equal");
else if(m1.get("a") < m2.get("b"))
System.out.println("Lesser");
else
System.out.println("Greater");

Here JDart generates 2 test cases and the branch coverage shows 1/2.
But if we reorder/modify the conditions as below,

if(m1.get("a") > m2.get("b"))
System.out.println("Greater");;
else if(m1.get("a") < m2.get("b"))
System.out.println("Lesser");
else
System.out.println("Equal");

JDart is generating 3 test cases and the branch coverage shows 2/2.

The same behavior is observed for List as well.

Could you please tell me the reason behind it.

[ksluckow]

There is a good reason for what you are observing:
Remember that you have two Map<String, Integer>s. When you call get(key), you will get the object wrapper class of the primitive int type. I.e. you apply == on two reference types in this particular case. When you do that, unboxing to the primitive types is not applied, and hence you are comparing the references of the object wrappers; not the values. I know this is a quite ambiguous case. If you compare the Integer obtained from the map with a primitive int, unboxing will take place regardless of the operator used. Also when you apply a comparison operator that can only "meaningfully" be evaluated on primitive types (e.g., >, <=), unboxing is performed, hence you get the results you are seeing.

Note that this is not a limitation of JDart, but rather the semantics of the JVM.

If you explicitly cast to primitive type:

if((int)m1.get("a") == m2.get("b"))
  //....

or store the values in temporary variables:

int a = m1.get("a");
int b = m1.get("b");
if(a == b))
  //....

unboxing is performed, and thus JDart will explore both branches.

[srgiri]

Thanks a lot for such a nice explanation.

[ksluckow]

You are very welcome! Let me know if you have additional questions!

[srgiri]

Hi,
I have a Map<customObject,customObject> and the generated test cases are as in the below format:
java.lang.Integer : m[#0].vendor.vendorId = 23

Here the value part (vendor.vendorId = 23) is OK but how can I get the Key ?
After I get the Key and Value, the Map object can be constructed and would be used for the Junit test cases.

Example: m.put(new customObject(args), new Vendor(23));
P.S. equals() and hashCode() methods are overridden in the Key class.
If you could also tell me which class in Jdart proj has the key_object information. Please help me.

Regards,
S R Giri

[ksluckow]

Hi!
Can you give more details about what you are trying to do? What information is symbolic etc?

[srgiri]

I have two custom classes: 'Student' and 'Course'.

`public class Student {
private String name;
private int rollNo;

public String getName() {
	return name;
}
public void setName(String name) {
	this.name = name;
}
public int getRollNo() {
	return rollNo;
}
public void setRollNo(int rollNo) {
	this.rollNo = rollNo;
}


public Student(String name, int rollNo) {
	super();
	this.name = name;
	this.rollNo = rollNo;
}

@Override
public boolean equals(Object stud){
	if(stud != null && this.getRollNo() == ((Student)stud).getRollNo())
		return true;
	else
		return false;
}

@Override
public int hashCode(){
	return this.getRollNo() * 23 + this.getName().length();
}

}`

`public class Course {
private String courseName;
private int courseId;

public Course(String courseName, int courseId) {
	super();
	this.courseName = courseName;
	this.courseId = courseId;
}

public Course(){}

public String getCourseName() {
	return courseName;
}
public void setCourseName(String courseName) {
	this.courseName = courseName;
}
public int getCourseId() {
	return courseId;
}
public void setCourseId(int courseId) {
	this.courseId = courseId;
}

}`

The class containing main() method and the method under test is:

`public class Sample {

public static void main(String[] args) {
	Student s1 = new Student("Sam", 12);
	Course c1 = new Course("Algorithm", 100);
	Student s2 = new Student("Tom", 266);
	Course c2 = new Course("Data Structure", 200);
	
	Map<Student,Course> m1 = new HashMap<>();
	m1.put(s1,c1);
	Map<Student,Course> m2 = new HashMap<>();
	m2.put(s2,c2);
	
	testMap(m1,m2);
}


public static void testMap(Map<Student,Course> m1, Map<Student,Course> m2){
	Student s1 = new Student("Sam", 12);
	Student s2 = new Student("Tom", 266);
	if(m1.get(s1).getCourseId() < m2.get(s2).getCourseId())
		System.out.println("m1.s1.courseId < m1.s1.courseId");
	else if(m1.get(s1).getCourseId() > m2.get(s2).getCourseId())
		System.out.println("m1.s1.courseId > m1.s1.courseId");
	else
		System.out.println("m1.s1.courseId = m1.s1.courseId");
}

}`

My jpf file is as below.

shell=gov.nasa.jpf.jdart.JDart
symbolic.dp=z3
symbolic.dp.z3.bitvectors=true

log.finest=jdart
log.info=constraints

jdart.configs.all_fields_symbolic.symbolic.include=m1[*;m2[*

target=com.sam.jdart.util.Sample

concolic.method=testMap
concolic.method.testMap=com.sam.jdart.util.Sample.testMap(m1:java.util.Map,m2:java.util.Map)
concolic.method.testMap.config=all_fields_symbolic

listener=gov.nasa.jpf.listener.CoverageAnalyzer
coverage.include=com.sam.jdart.util.Sample
coverage.show_methods=true

When I run I get the below test cases:

java.lang.Integer:m1[#0].courseId=-2100273060, java.lang.Integer:m2[#0].courseId=-2100273060,

java.lang.Integer:m1[#0].courseId=0, java.lang.Integer:m2[#0].courseId=-2147483647,

java.lang.Integer:m1[#0].courseId=100, java.lang.Integer:m2[#0].courseId=200,

The test cases are correct.
Now I want to create map objects out of these test cases. And then I can use these objects in my JUnit test class.
To create and initialize the map I need to create the Key and Value. Here both the key and the value are custom objects. I can create the value object from the generated test cases.
Course c1 = new Course(); c1.setCourseId(-2100273060);

But I can't create key objects as the test cases do not have enough information about the keys.. It shows only [#0].
Student s1 = new Student(); s1.setRollNo(??);
Map<Student,Course> m1 = new HashMap<>(); m1.put(s1,c1);

`
public void test0() throws Throwable {

     // step 0    
      if (!(true)) {
        fail("Precondition not met: true");
      }
      testMap(m1,m2);
      // perform checks 
  } // end of test case 0

`

[srgiri]

Hi,
Could you please give me some idea how can I generate test cases for a method which have String in conditions.
Can somehow char array be used to achieve it.
Most of the java methods deal with string.

[ksluckow]

It depends on which string constraints you have. JDart can handle constraints that would amount to constraints on the elements of char[] such as String.equals().

However, in order to do so, you will have to make some changes to jpf-core since it has models (and peers) for the String class.

Let's assume you only have constraints on string equalities. Depending on how you model String, it could look like the following:

public static void main(String args[]) {
  char[] a = new char[] {'a', 'b', '3'};
  char[] b = new char[] {'c', 'd', 'f'};
  target(a, b);
}
  
public static void target(char[] a, char[] b) {
  String stra = new String(a);
  String strb = new String(b);
  if(stra.equals(strb)) {
    System.out.println("equals");
  } else {
    System.out.println("not equals");
  }
}

Your config would then contain something like:

concolic.method.targetMethod=StringExample.target(a:char[],b:char[])

Now, for this to work, you will have to replace equals() in the String class in jpf-core/src/classes with, e.g., how it is done in open-jdk:

public boolean equals(Object anObject) {
    if (this == anObject) {
        return true;
    }
    if (anObject instanceof String) {
        String anotherString = (String) anObject;
        int n = value.length;
        if (n == anotherString.value.length) {
            char v1[] = value;
            char v2[] = anotherString.value;
            int i = 0;
            while (n-- != 0) {
                if (v1[i] != v2[i])
                        return false;
                i++;
            }
            return true;
        }
    }
    return false;
}

In addition, remove the peer equals__Ljava_lang_Object_2__Z.equals__Ljava_lang_Object_2__Z(...) in jpf-core/src/peers.

[srgiri]

Thank you.
I observed that most of the times char arrays generate some non human-readable characters. This is creating problem when I try to generate the test cases for the char[] which is equivalent of a string.
Is there any way to generate all the characters in human-readable format ?

[ksluckow]

Yes, that is expected because characters in Java are encoded as UTF-16. The solver represents characters as 16-bit integers.
I'm not sure what you mean by human-readable, but if you want to constrain the solutions to characters in, say, ASCII, then you could add that condition to each character of the string, e.g., a[0] >= 0 && a[0] <= 128 && a[1] >= 0 && a[1] <= 128 && ...

[srgiri]

I meant the keyboard characters. Thank you for the explanation.
But adding the extra conditions a[0] >= 32 && a[0] <= 126 && a[1] >= 32 && a[1] <= 126 && ... increase the number of generated test cases. I think it is because JDart is trying to solve each condition separately.
Is there any mechanism to reduce such test cases ?

[srgiri]

I have a question in continuation of your answer "It depends on which string constraints you have. JDart can handle constraints that would amount to constraints on the elements of char[] such as String.equals()...." given above.
What would be the impact if I remove the String class from the jpf-core (assuming it will take the String class from the jdk) and removing all the corresponding methods from the peer class.

I observed it is generating test cases. But is there any other impact ?

[ksluckow]

In jpf-core equals is a native method that is handled by a peer; it is not a native method in JDK (at least OpenJDK 1.7), hence it will be explored by JDart. That's why you are getting test cases.

On the other hand, when removing those classes from jpf-core, your analysis will also become dependent on the JDK installation. Since different versions of the JDK (and different JDKs) can have different implementations of the Java classes, you may get different analysis results. In addition, jpf-core simplifies many of the jdk classes and takes care of the native calls with peers.

In fact, a better method in your case could be to rely on the String class in jpf-core, but only substitute---as needed---the methods you would like to symbolically execute.
The impact is that the analysis will then become dependent on your JDK installation.

[srgiri]

Thanks a lot.

[srgiri]

Hi,
I need one urgent help.
I am not sure which code has been modified or anything else could be the reason, I am getting some weired output.

I have a target class, which has the SUT and a main method. The SUT is called from within the main method. If I write the below code in the main method.
int i = 0;
System.out.println("Before: i = "+i);
i++;
System.out.println("After: i = "+i);
i++;
System.out.println("Another time: i = "+i);

When I right click on the .jpf file and click on 'verify', I am getting output as:
Before: i = 0
After: i = 2 //why ?
Another time: i = 3

Similar issue is happening for '--' operator.

Please tell me what could be the reason for this issue.

[ksluckow]

Should be fixed now.

[srgiri]

Hi,
I have a method under test as below.

public static float getTotalPriceForBookBank(List<Book> books){
	float totalPricePayable = 0;
	for(Book book:books){
		if(book.getPrice() > 2500)
			totalPricePayable = totalPricePayable + (book.getPrice() * 0.2f); 
		else if(book.getYearOfPublication() < 2000)
			totalPricePayable = totalPricePayable + (book.getPrice() * 0.05f); 
		else
			totalPricePayable = totalPricePayable + (book.getPrice() * 0.1f); 
	}
	return totalPricePayable;
}

As I understand JDart can work on bounded list i.e. initialized list with objects.
When the SUT is called from the main method (as below) I am getting the test cases generated correctly.

List<Book> bookList = new ArrayList<>();
bookList.add(new Book());
bookList.add(new Book());
bookList.add(new Book());
new SUT().getTotalPriceForBookBank(bookList);

But if I call the SUT like below, I am not getting any test cases.

List<Book> bookList = new ArrayList<Book>(){{
    add(new Book());
    add(new Book());
    add(new Book());
}};
new SUT().getTotalPriceForBookBank(bookList);

Why no test cases are generated when the SUT is called in the 2nd way ? Could you please help me.

[ksluckow]

This is because you are effectively initializing the list in two very different ways. The latter uses the so-called double-brace initializer which creates an anonymous class for performing initialization. You can confirm this behavior by looking in the build folder; you'll see a new class with 1$.class suffix---this is the class generated by the compiler.
I haven't tested it, but you might be able to analyze the SUT by specifying the anonymous class as your target.

However, if you can, I would highly recommend not using double-brace initializers. I consider it an anti-pattern.

[srgiri]

Hi,
Is there any plan to support String in future ? If so, could you give any idea when ?
Most of the methods deal with Strings in conditions. It would be great if JDart can generate test cases for Strings. If this is done, then I feel JDart would be a complete solution for test case generation.

[zvonimir]

FYI, a student in my class on software verification is planning to try to add support for string to JDart. We
'll see how for he'll get in the next 2 months.