Using external libraries in native peer class

90 views
Skip to first unread message

LauraPanizo

unread,
Apr 11, 2011, 4:03:41 AM4/11/11
to Java™ Pathfinder
Dear all,
I want to use a external user library (libppl_java.so) in my java
program.
I have implemented a native peer that uses the methods of the external
library, but when I execute the JPF it fails.
I have executed the program without calling the methods of the user
library to ensure that the native peers and the model class works
correctly. I have also tested that the library works correctly.
That is part of the code:

/***Model class:***/
package zero.example;

public class TestClass {
public native int enabled();
}

/***Peer Class***/
package gov.nasa.jpf.jvm;

public class JPF_zero_example_TestClass {

//Esta clase sera la que llame a PPL

public static void $init____V (MJIEnv env, int rcls) {
System.out.println("native classpath works");

}
public static int enabled____I(MJIEnv env, int objRef){
String ver= null;
try{
System.load("/usr/local/lib/ppl/libppl_java.so");

parma_polyhedra_library.Parma_Polyhedra_Library.initialize_library();
ver = parma_polyhedra_library.Parma_Polyhedra_Library.version();
System.out.println("Library version "+ver);
}catch(Exception e){
System.out.println("error");
}
return 1;
}

If I included the user library in the classpath of run-JPF (eclipse)
and execute it, the following errors are thrown:

native classpath works
[SEVERE] JPF exception, terminating: exception in native method
zero.example.TestClass.enabled
java.lang.UnsatisfiedLinkError:
parma_polyhedra_library.Parma_Polyhedra_Library.initialize_library()V
at
parma_polyhedra_library.Parma_Polyhedra_Library.initialize_library(Native
Method)
at
gov.nasa.jpf.jvm.JPF_zero_example_TestClass.enabled____I(JPF_zero_example_TestClass.java:
34)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at
sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:
39)
at
sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:
25)
at java.lang.reflect.Method.invoke(Method.java:597)
at
gov.nasa.jpf.jvm.NativeMethodInfo.executeNative(NativeMethodInfo.java:
151)
at gov.nasa.jpf.jvm.bytecode.EXECUTENATIVE.execute(EXECUTENATIVE.java:
65)
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(NativeMethodAccessorImpl.java:
39)
at
sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:
25)
at java.lang.reflect.Method.invoke(Method.java:597)
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.JPFNativePeerException: exception in native method
zero.example.TestClass.enabled
at
gov.nasa.jpf.jvm.NativeMethodInfo.executeNative(NativeMethodInfo.java:
202)
at gov.nasa.jpf.jvm.bytecode.EXECUTENATIVE.execute(EXECUTENATIVE.java:
65)
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(NativeMethodAccessorImpl.java:
39)
at
sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:
25)
at java.lang.reflect.Method.invoke(Method.java:597)
at gov.nasa.jpf.tool.Run.call(Run.java:76)
at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:86)
Caused by: java.lang.UnsatisfiedLinkError:
parma_polyhedra_library.Parma_Polyhedra_Library.initialize_library()V
at
parma_polyhedra_library.Parma_Polyhedra_Library.initialize_library(Native
Method)
at
gov.nasa.jpf.jvm.JPF_zero_example_TestClass.enabled____I(JPF_zero_example_TestClass.java:
34)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at
sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:
39)
at
sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:
25)
at java.lang.reflect.Method.invoke(Method.java:597)
at
gov.nasa.jpf.jvm.NativeMethodInfo.executeNative(NativeMethodInfo.java:
151)
... 15 more

Any idea of what I missed to configure?
Thanks

Peter Mehlitz

unread,
Apr 11, 2011, 12:51:15 PM4/11/11
to java-pa...@googlegroups.com
if you use System.load(pathName) there is not much JPF configuration involved (as opposed to System.loadLibrary(fileName), which uses the JPFClassLoader and '<project>.native_libraries' settings).

You actually get the exception not for loading your native lib, but for calling initialize_library(), so you have to check if the signature is right. Look at parma_polyhedra_library.Parma_Polyhedra_Library and see if it matches the sources of libppl_java.so

-- Peter

Message has been deleted

LauraPanizo

unread,
Apr 12, 2011, 4:12:27 AM4/12/11
to Java™ Pathfinder
Hi,
I have solved the problem, I have add the path of ppl_java.jar to the
native_class_path of my project
and I have removed from the class_path of the run configuration. It
seems that works fine.

Thank you very much,
Laura

On 12 abr, 09:38, LauraPanizo <panizo.ja...@gmail.com> wrote:
> Thanks Peter,
> I have used thislibraryin a normal Java program and to use it, I
> added it to the built path of the Java project and also to the
> classpath of the run configuration.
> I have used jpf-template to generate my project. Where do I have to
> include the userlibrary? Do I hace to include anything in the
> jpf.properties of my project?
>
> Thanks,
> Laura
>
> On 11 abr, 18:51, Peter Mehlitz <pcmehl...@gmail.com> wrote:
>
> > if you use System.load(pathName) there is not much JPF configuration involved (as opposed to System.loadLibrary(fileName), which uses the JPFClassLoader and  '<project>.native_libraries' settings).
>
> > You actually get the exception not for loading your native lib, but for calling initialize_library(), so you have to check if the signature is right. Look at parma_polyhedra_library.Parma_Polyhedra_Library and see if it matches the sources of libppl_java.so
>
> > -- Peter
>
> > On Apr 11, 2011, at 1:03 AM, LauraPanizo wrote:
>
> > > Dear all,
> > > I want to use a external userlibrary(libppl_java.so) in my java
> > > program.
> > > I have implemented a native peer that uses the methods of the external
> > >library, but when I execute the JPF it fails.
> > > I have executed the program without calling the methods of the user
> > >libraryto ensure that the native peers and the model class works
> > > correctly.  I have also tested that thelibraryworks correctly.
> > > That is part of the code:
>
> > > /***Model class:***/
> > > package zero.example;
>
> > > public class TestClass {
> > >    public native int enabled();
> > > }
>
> > > /***Peer Class***/
> > > package gov.nasa.jpf.jvm;
>
> > > public class JPF_zero_example_TestClass {
>
> > >    //Esta clase sera la que llame a PPL
>
> > >    public static void $init____V (MJIEnv env, int rcls) {
> > >        System.out.println("native classpath works");
>
> > >    }
> > > public static int enabled____I(MJIEnv env, int objRef){
> > >            String ver= null;
> > >            try{
> > >                    System.load("/usr/local/lib/ppl/libppl_java.so");
>
> > > parma_polyhedra_library.Parma_Polyhedra_Library.initialize_library();
> > >                    ver = parma_polyhedra_library.Parma_Polyhedra_Library.version();
> > >                    System.out.println("Libraryversion "+ver);
> > >            }catch(Exception e){
> > >                   System.out.println("error");
> > >            }
> > >            return 1;
> > >    }
>
> > > If  I included the userlibraryin the classpath of run-JPF (eclipse)

LauraPanizo

unread,
Apr 12, 2011, 8:46:54 AM4/12/11
to Java™ Pathfinder
Dear Peter,
I have a new question relative to my native peer.
After doing some operations with the user library I would like to
force a state matching but I cannot find a choice generator that
adjust to what I want to do.
The idea is executing the function "enabled" of the peer class, inside
there are callings to user library functions.
If those callings returns certain results, jpf should do state
matching to check if the program is in a previously visited state.
It is possible to force state matching from my native peer? and
outside the peer?
What are the basic calls I need to do ? There is any example code to
see how it can be used?

Thanks in advance,
Laura


On 11 abr, 18:51, Peter Mehlitz <pcmehl...@gmail.com> wrote:

Mateusz Ujma

unread,
Apr 12, 2011, 8:59:50 AM4/12/11
to java-pa...@googlegroups.com
State matching happens after each new state. If your native peer does
not create a new state you can force it by calling:

ThreadInfo ti = env.getThreadInfo();
ti.breakTransition();

--
Best regards
    Mateusz Ujma

Reply all
Reply to author
Forward
0 new messages