jpf-symbc: get the constraint while pruning the search

[Anh Cuong]

Hi,

I am using jpf-symbc to deal with the following problem: when
symbolically searching through all the execution paths, I want to
prune the search at a certain point (that even before the last return
statement). When the search is pruned at the stop point, the search
is
backtracked and a constraint that is collected up to the stop point
is
returned.


Is there anyway to return the constraint (not the instantiation of
the
constraint) even when the constraint is not solvable?


Thanks.


Anh Cuong

[Willem Visser]

Yes. Just write a listener, or even easier, adapt one that is already there. There are a number of listeners for the symbc extension already and all you need to do is find out when the search hits the constraint on which it will backtrack and then to reconstruct the constraint by traversing the internal constraint structure and dumping it out in whatever format you would like. 

Bye,

Willem

[Anh Cuong]

Hi Willem,

Thank you very much for your answer, I will look into that. Just one
more question, can the constraints over structural data like array or
heap be kept track as well?

Thanks.

> > Anh Cuong- Hide quoted text -
>
> - Show quoted text -

[Anh Cuong]

I am toying with the SymbolicListener with structural symbolic data. I
got the following exception thrown by JPF for a program with
LinkedList. The symbolic method is : Test.test(sym)

The program is:
import java.util.LinkedList;

public class Test {

public static void main(String[] args) {
LinkedList<Integer> ll = new LinkedList<Integer>();
test(ll);
}

public static void test(LinkedList<Integer> ll) {
if (ll != null) {
int size = ll.size();
if (size > 10){
ll.get(0);
}
}
}
}

The exception is:
====================================================== error #1
gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty
java.lang.IndexOutOfBoundsException: Index: 0, Size: 0
at java.util.LinkedList.entry(LinkedList.java:365)
at java.util.LinkedList.get(LinkedList.java:315)
at NodeTest.test(NodeTest.java:21)
at NodeTest.main(NodeTest.java:14)

Is it a bug or I am getting thing wrongly?

Thanks!

On Jun 2, 9:29 pm, Willem Visser <wil...@gmail.com> wrote:

[Neha Rungta]

Anh,

In order to symbolically evaluate complex data structures you have to use the lazy initialization aspect in the symbolic execution framework. It can be invoked with the following configuration flag

symbolic.lazy=on

There are some examples in the jpf-symbc project that demonstrate how the lazy initialization works. You should be aware, however, that when you have the following code

if (size > 10){
       ll.get(0);
 }

The analysis is currently not setup to symbolically initialize the linked list to a particular size. It does allow you to symbolically intialize each element in the code. For example

if (ll.next != null)
     Element e = ll.next 

Hope this helps,

Cheers

Neha

--
-------------------------------------------------
Neha Rungta
Research Scientist
Robust Software Engineering Group
SGT/NASA Ames Research Center
Moffett Field, CA 94035
--------------------------------------------------