jpf-symbc installation

[Alex O.]

Hello,

I am not very experienced with JPF or SPF but I have used them before,
managed to install and run them on my projects.

However now, when I downloaded the latest jpf-core and jpf-symbc, jpf-
symbc doesn't seem to work.

Meaning....

jpf-core[466] - installed, works and site.properties is set

jpf-symbc[305] - problems:
- first one...it seems to need the bcel.jar from the jpf-core lib dir,
but i read in a post on this group that the jar was removed from jpf-
core. I edited the build path from symbc so that the link is ok and
got rid of the errors saying there is no bcel.xx package
- next problems....now, when I try to build it I get these errors


[javac] Compiling 243 source files to E:\ProiectDiploma\Diploma\jpf-
symbc\build\main
[javac] E:\ProiectDiploma\Diploma\jpf-symbc\src\main\gov\nasa\jpf
\symbc\SymbolicInstructionFactory.java:24: cannot find symbol
[javac] symbol : class DefaultInstructionFactory
[javac] location: package gov.nasa.jpf.jvm
[javac] import gov.nasa.jpf.jvm.DefaultInstructionFactory;
[javac] ^
[javac] E:\ProiectDiploma\Diploma\jpf-symbc\src\main\gov\nasa\jpf
\symbc\SymbolicInstructionFactory.java:37: cannot find symbol
[javac] symbol: class DefaultInstructionFactory
[javac] public class SymbolicInstructionFactory extends
DefaultInstructionFactory {
[javac] ^
[javac] E:\ProiectDiploma\Diploma\jpf-symbc\src\main\gov\nasa\jpf
\symbc\SymbolicInstructionFactory.java:41: cannot find symbol
[javac] symbol : method createInsnClassArray(int)
[javac] location: class
gov.nasa.jpf.symbc.SymbolicInstructionFactory
[javac] insnClass = createInsnClassArray(260);
[javac] ^
[javac] E:\ProiectDiploma\Diploma\jpf-symbc\src\main\gov\nasa\jpf
\symbc\SymbolicInstructionFactory.java:43: cannot find symbol
[javac] symbol : variable ALOAD_0
[javac] location: class
gov.nasa.jpf.symbc.SymbolicInstructionFactory
[javac] insnClass[ALOAD_0] =
gov.nasa.jpf.symbc.bytecode.ALOAD.class;
[javac] ^
[javac] E:\ProiectDiploma\Diploma\jpf-symbc\src\main\gov\nasa\jpf
\symbc\SymbolicInstructionFactory.java:44: cannot find symbol
[javac] symbol : variable ALOAD_1
[javac] location: class
gov.nasa.jpf.symbc.SymbolicInstructionFactory
[javac] insnClass[ALOAD_1] =
gov.nasa.jpf.symbc.bytecode.ALOAD.class;
[javac] ^
[javac] E:\ProiectDiploma\Diploma\jpf-symbc\src\main\gov\nasa\jpf
\symbc\SymbolicInstructionFactory.java:45: cannot find symbol
[javac] symbol : variable ALOAD_2
[javac] location: class
gov.nasa.jpf.symbc.SymbolicInstructionFactory
[javac] insnClass[ALOAD_2] =
gov.nasa.jpf.symbc.bytecode.ALOAD.class;
[javac] ^
[javac] E:\ProiectDiploma\Diploma\jpf-symbc\src\main\gov\nasa\jpf
\symbc\SymbolicInstructionFactory.java:46: cannot find symbol
[javac] symbol : variable ALOAD_3
[javac] location: class
gov.nasa.jpf.symbc.SymbolicInstructionFactory
[javac] insnClass[ALOAD_3] =
gov.nasa.jpf.symbc.bytecode.ALOAD.class;
[javac] ^


This is only the first part of the error, if you need it all tell me
and i'll post it. If I understand right, all the errors are mainly
about 2 things
1. SymbolicInstructionFactory extends DefaultInstructionFactory and
there is no gov.nasa.jpf.jvm.DefaultInstructionFactory in jpf-core
2. For some bytecode instructions in the jpf-symbc i get a constructor
error - detailed like:
"Implicit super constructor IFLE() is undefined for default
constructor. Must define an explicit constructor"

If anyone could please tell me what am I doing wrong. Am I not getting
the right version of jpf-symbc?

Thank you,
Alex

[Willem Visser]

[I think] symbc is currently incompatible with jpf-core.  Hopefully that will be fixed shortly.

[Neha Rungta]

Until symbc is updated in order to compile please use a slightly older revision of jpf-core (437).

--
-------------------------------------------------
Neha Rungta, Ph.D
SGT/NASA Ames Research Center
http://ti.arc.nasa.gov/profile/nrungta/
--------------------------------------------------

[Alex O.]

I followed your advices, and took an older version of jpf-core as
sugested(437). Thank you for the help, I can now build and run SPF.

But now I have another problem. I wanted to use SPF to look at
polimorphism with SPF and lazy initialization.
So as I checked what was done about this through SPF, i stoped at the
uberlazy package and at its examples. And I found that some of the
examples are failing due to, in my opinion, the GETFIELD instruction
in the uberlazy.bytecode package:


Running Symbolic PathFinder ...
symbolic.dp=choco
symbolic.string_dp_timeout_ms=0
symbolic.string_dp=none
symbolic.choco_time_bound=30000
JavaPathfinder v6.0 - (C) RIACS/NASA Ames Research Center


====================================================== system under
test
application: uberlazy\TestParentFieldInit.java

====================================================== search started:
04.05.2011 14:44
coming to the TestPrimTypeFieldDiff

***Execute symbolic INVOKEVIRTUAL: run()V ( ) ( n, m )
[SEVERE] JPF exception, terminating: not a int field: m
---------------------- JPF error stack trace ---------------------
gov.nasa.jpf.JPFException: not a int field: m
at gov.nasa.jpf.jvm.ElementInfo.getIntField(ElementInfo.java:976)
at
gov.nasa.jpf.symbc.uberlazy.bytecode.GETFIELD.execute(GETFIELD.java:
208)
at gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:
1981)
at gov.nasa.jpf.jvm.ThreadInfo.executeTransition(ThreadInfo.java:
1941)
at
gov.nasa.jpf.jvm.SystemState.executeNextTransition(SystemState.java:
656)
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1717)
at gov.nasa.jpf.search.Search.forward(Search.java:500)
at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:79)
at gov.nasa.jpf.JPF.run(JPF.java:534)
at gov.nasa.jpf.JPF.start(JPF.java:166)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(Unknown Source)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(Unknown Source)
at java.lang.reflect.Method.invoke(Unknown Source)
at gov.nasa.jpf.tool.Run.call(Run.java:76)
at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:86)
---------------------- JPF error stack trace ---------------------
gov.nasa.jpf.JPFException: not a int field: m
at gov.nasa.jpf.jvm.ElementInfo.getIntField(ElementInfo.java:976)
at
gov.nasa.jpf.symbc.uberlazy.bytecode.GETFIELD.execute(GETFIELD.java:
208)
at gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:
1981)
at gov.nasa.jpf.jvm.ThreadInfo.executeTransition(ThreadInfo.java:
1941)
at
gov.nasa.jpf.jvm.SystemState.executeNextTransition(SystemState.java:
656)
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1717)
at gov.nasa.jpf.search.Search.forward(Search.java:500)
at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:79)
at gov.nasa.jpf.JPF.run(JPF.java:534)
at gov.nasa.jpf.JPF.start(JPF.java:166)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(Unknown Source)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(Unknown Source)
at java.lang.reflect.Method.invoke(Unknown Source)
at gov.nasa.jpf.tool.Run.call(Run.java:76)
at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:86)

Among the examples that fail are: TestParentFieldInit.jpf,
TestDifAliasClass.jpf, TestInstanceOfByteCode.jpf and others

I am running jpf-core[437] and jpf-symbc[305].
Is there something wrong with the uberlazy.bytecode GETFIELD
instruction or am I doing something wrong?

Thanks,
Alex

[Neha Rungta]

Hi Alex,

The uberlazy is an extension of lazy initialization and is a work in progress. I have pushed the fix for the GETFIELD instruction that was causing the examples to fail. In order to see the effects of polymorphism and lazy initialization in the configuration files comment out the Uberlazy part which is the following.

#vm.insn_factory.class=gov.nasa.jpf.symbc.uberlazy.UberLazyInstructionFactory

Neha

[Corina Pasareanu]

Hi Alex:
I am in the process of making symbc compatible with core and fix some bugs.
hopefully that will be done today.
the uberlazy bit is not properly working.
if you want to experiment with lazy initialization (as per our TACAS'03 paper) please look into GETFIELD and GETSTATIC under the bytecode dir.
But I would advise you to just wait a bit to get the latest version.
I will send you a message once that is done.
Thanks,
Corina

[Corina Pasareanu]

Hi:

I committed a version. 

thanks

Corina

[Corina Pasareanu]

the code does not work yet properly.

corina

[Corina Pasareanu]

Hey:

I submitted more fixes to the Symbolic PathFinder. Slowly but surely I'll get to a stable state :)

Mateusz will also fix the regression tests. Thanks Mateusz.

Bye,

Corina

[Alex O.]

I have another question about jpf-symbc

If I have a method "public void foo(A vA)"

and I run SPF on it with

symbolic.method = foo(sym)
symbolic.lazy = true
symbolic.lazy.subtypes = true

the method is run for all the Subtypes of A

for example if type B extends A and type C extends A, SPF will run my
method foo with vA of type A, of type B and type C if the type is
relevent for the instructions executed by foo.

Now my question is how can I find out from a Listener while runing SPF
on the foo method what is the type of vA(symbolic reference) at the
current moment?

Thank you,
Alex

[Neha Rungta]

Hi Alex,

In order to find the type of the object in a listener you first need to access the object. The objects in JPF are encompassed into ElementInfo data structures. The code in listener would be similar to something below:

                ThreadInfo current = search.getVM().getCurrentThread();

                // the objRef is the index of object in the heap you want to look up
                ElementInfo ei = current.getElementInfo(objRef);
                String type = ei.getType() // will get you the type of the object

                // if you want to look at types of fields in the object you'd do something
                // like the following
                int number = ei.getNumberOfFields();
                 for(int fieldIndex = 0; fieldIndex < number; fieldIndex++) {
                     FieldInfo fi = ei.getFieldInfo(fieldIndex);
                     String type = fi.getType();
                   ....
               
Neha

[Corina Pasareanu]

Hi Alex:
In the current version that I've just submitted I disabled the handling of sub-types until we find a cleaner way to do it.
Corina

[Alex O.]

Another question. So I am running SPF, with the handling of subtypes
on, [v305]
with
conf.setProperty("symbolic.lazy", "true");
conf.setProperty("symbolic.lazy.subtypes", "true");
conf.setProperty("symbolic.method",
"testingProgs.Test.start2(sym#sym#sym)");

I have a small test hierarchy
abstract class A { public void myClass() { System.out.println("A");} }
class B extends A { public void myClass()
{ System.out.println("B");} }
class C extends A { public void myClass()
{ System.out.println("C");} }

and the test method
class Test {
public static void start2(A a, A b, A c) {
if(a != null && b != null && c != null) {
a.myClass();
b.myClass();
c.myClass()
System.out.println("__________");
} else {
System.out.println("a b c null");
System.out.println("__________");
}
}

public static void main (String[] args) {
A a = null;
A b = null;
A c = null;
start2(a,b,c);
}
}


i get multiple (5 times)
"
B
B
B
_____
"
answers. Shouldn't i get one single answer like the one above?

Why is this? Is this regarding thread interleavings? None of my
classes are Runnable.

[Neha Rungta]

That is actually intended behavior. Here is what the algorithm does.

The execution starts on data structures with un-initialized fields and it initializes them lazily, when the  fields are first accesed. In lazy initialization,  a field of class, T, is initialized non-deterministically to (1) null, (2) a reference to a new instance of class T with uninitialized fields, or (3) a reference to an object of type T created during a prior field initialization. This can generate 3 or more choice points. In order to handle sub-types additional choices are added. Lazy initialization with sub-types, step (2) above is replaced with non-deterministically assigning new instances of class T and of all the classes that inherit from T. Similarly, step (3) is replaced with assigning previously created objects to class T and objects from classes that  inherit from T.

Since the different choices are explored to cover aliasing and subtypes the algorithm generates more paths. The points of lazy initialization are essentially points of data non-determinism. The paths you see being generated are a result of this data non-determinism and not thread interleaving.

Neha

[Alex O.]

first I want to thank you for all the quick answers:

and now another question
if I have a method m declared as symbolic

symbolic.method = ClassA.m(sym)

and in this method I have:

public void m(ClassA b) {
....
n(b);
...
}

If n is not declared as symbolic.method will the lazy intialization
continue on b acording to what happens in n - giving all choices as
Neha said in the previous message?
From what I can see when i declare n as well for beeing run as
symbolic, i get more possible ways than when n is not declared
symbolic.method - even if n is a very simple method like:
public void n(ClassA b) {
System.our.println("method n");
}

Is there a way to say method m is symbolic and run every other method
invoked from m as symbolic.methods?
and
If i have a hierarchy which contains a method p from top to bottom
classes and it may or may not be overridden in subclasses, and if I
want to run it as symbolic.method... do i need to declare all methods
as symbolic or is it enough to have the top class hierarchy declare it
as symbolic?
meaning
class A - method n(param)
class B extends A - method n(param) - override top method
class C extends A - does not override method n

do I need to write
symbolic.method = "A.n(sym),B.n(sym),C.n(sym)"
or is it enough
symbolic.method = "A.n(sym)" ?

Thanks,
Alex

[Neha Rungta]

You have to explicitly define methods as symbolic where you want lazy initialization to take place. When a method is invoked from another symbolic method it doesn't treat the callee as symbolic. As you mentioned all the methods needs to be specified as symbolic. 

Neha

[Alex O.]

And another question:

First,
is the lazy initialization algorithm located only in the ALOAD and
GETFIELD bytecode instructions? Or are there more instructions where
lazy init is dealt with.

Second,
if I want more methods to be executed symbolicaly than defined in the
symbolic.method, is it feasible to do this by writing a listener and
in it's executeInstruction() method to check if the instruction that
is going to be executed is an INVOKE instruction and if it is I modify
the symbolic.method property in conf so that when
BytecodeUtils.execute() is called it will see the method as symbolic
method?

Thank you,
Alex

[Corina Pasareanu]

Hi Alex:
This is a correction to Neha's message.
In the example:

public void m(ClassA b) {
....
n(b);
...
}

if you declare m symbolic you DO NOT need to declare n symbolic.
what happens is that if b has a symbolic value (e.g. partially initialized heap + symbolic primitive fields) at the time of calling "n", that symbolic value will flow into the execution of n. So "n" will be symbolically executed as well (where the symbolic value of "b" is the one computed in the body of "m").

Now if you declare both "m" and "n" symbolically, the value of "b" at the time of calling "n" will be replaced with a fresh NEW symbolic value (i.e. unitilaized heap node).

I hope this helps,
Corina

[Corina Pasareanu]

Hi,
In essence the lazy init is done in GETSTATIC, GETFIELD and ALOAD.
You can do more by writing a listener as you say or modifying directly the bytecodes for INVOKESPECIAL, INVOKESTATIC, INVOKEVIRTUAL. Although in principle, this should not be necessary.
Out of curiosity, what do you want to do?

I hope this helps,
Corina

[Alex O.]

I would have another question about lazy initialization in jpf-symbc
if I run a method symbolicaly and with lazy init and lazy subtypes on
method(ObjA a, ObjA b)

Assuming ObjA has subtypes, how can I check in a Listener at any point
of what type are a and b(meaning the type of the object they have been
initialized with by lazy init) and the object they point to(to see if
a and b are references for different objects or are they references
for same object - aliasing)

Thanks,
Alex