How to fix an UnsatisfiedLinkError when adding a new c++ code

28 views
Skip to first unread message

Ali A. Noroozi

unread,
Aug 6, 2018, 10:00:39 AM8/6/18
to PRISM model checker developers
Hi all,

I am trying to define a new method in the PrismSparse.java class for exporting the transition matrix. I followed these steps:

1. create the file src/sparse/PS_ExportMatrix_2.cc and change the function header to
      JNIEXPORT jint JNICALL Java_sparse_PrismSparse_PS_1ExportMatrix_2 ( ...)

2. add the following line to the file include/sparse_PrismSparse.h :
      JNIEXPORT jint JNICALL Java_sparse_PrismSparse_PS_1ExportMatrix_2
           (JNIEnv *, jclass, jlong, jstring, jlong, jint, jlong, jint, jlong, jint, jstring);

3. add the following line to src/sparse/PrismSparse.java :
      private static native int PS_ExportMatrix_2(long matrix, String name, long rv, int nrv, long cv, int ncv, long odd, int exportType, String filename);

4. call PS_ExportMatrix_2(...)   from ExportMatrix(...) of PrismSparse.

5. run make to compile c++ code.

6. run prism.

But, I get the following error:

 Exception in thread "main" java.lang.UnsatisfiedLinkError: sparse.PrismSparse.PS_ExportMatrix_2(JLjava/lang/String;JIJIJILjava/lang/String;)I
    at sparse.PrismSparse.PS_ExportMatrix_2(Native Method)
    at sparse.PrismSparse.ExportMatrix(PrismSparse.java:605)
    at prism.ProbModel.exportToFile(ProbModel.java:822)
    at prism.Prism.exportTransToFile(Prism.java:2326)
    at prism.PrismCL.doExports(PrismCL.java:729)
    at prism.PrismCL.run(PrismCL.java:350)
    at prism.PrismCL.go(PrismCL.java:218)
    at prism.PrismCL.main(PrismCL.java:2614)


It seems I am missing a step. Do you know how to fix this?

Joachim Klein

unread,
Aug 6, 2018, 10:50:11 AM8/6/18
to Ali A. Noroozi, PRISM model checker developers
Hello Ali,

you're on the right track.

Generally, the procedure is as follows:

1) You add the native method to src/sparse/PrismSparse.java (your step 3)

2) You recompile once. The Java compiler generates the appropriate
method signature in include/jni/sparse_PrismSparse.h [1]

3) You then provide an implementation in some *.cc file in src/sparse
(all *.cc files in that directory are compiled and linked to the
libsparse library).

4) Then, everything should work out fine...


So, in particular, you don't have to (and should not) manually edit the
.h file, as it's autogenerated. For your native method, it generates

JNIEXPORT jint JNICALL Java_sparse_PrismSparse_PS_1ExportMatrix_12
(JNIEnv *, jclass, jlong, jstring, jlong, jint, jlong, jint, jlong,
jint, jstring);

as the signature (notice the _12 at the end of the method name, which is
due to the Java name mangling of underscores in the native method name).


Cheers,
Joachim Klein

PS: If you are basing your code on the PRISM trunk after July 12th, the
generated .h headers are in include/jni/PACKAGE_CLASS.h (see
https://github.com/prismmodelchecker/prism/commit/4de3c189a4c23587565e89580293fcded7f2f310),
before they are generated in include/CLASS.h

Ali A. Noroozi

unread,
Aug 6, 2018, 11:54:47 AM8/6/18
to PRISM model checker developers
It worked like a charm. Thank you.
Reply all
Reply to author
Forward
0 new messages