#java #scala #dll #java-native-interface #z3
#java #scala #dll #java-native-interface #z3
Вопрос:
Майкрософт.Z3.dll описывается в свойствах файла как управляемая библиотека DLL Z3.
Java может загружать библиотеки dll. Это делается с помощью System.LoadLibrary или System.load, в зависимости от предпочтений программистов.
Если разработчик Java также создает DLL, javah можно использовать для определения объявлений импорта / экспорта. К сожалению, это не мой случай. Библиотека DLL уже создана Microsoft как управляемая C # DLL.
Мне нужна помощь в принятии объявления C #, такого как объявление, найденное в Microsoft RISE Z3 managed API, и создании прототипа пакета / класса Java, чтобы обеспечить успешный вызов. (Я уверен, что DLL загружена).
Чтобы упростить задачу, конкретный вызов определяется Microsoft в строке 03042 Microsoft.Z3.h. Любой пример кода будет с благодарностью оценен!
Ошибка, которую я получаю с моего сервера:
java.lang.UnsatisfiedLinkError: Microsoft.Z3.GetVersion(
LMicrosoft/Z3$IntPtr;
LMicrosoft/Z3$IntPtr;
LMicrosoft/Z3$IntPtr;
LMicrosoft/Z3$IntPtr;)V
at Microsoft.Z3.GetVersion(Native Method)
at Microsoft.Z3.z3VersionString(Z3.java:81)
at DatabaseXml.XmlTest(DatabaseXml.java:66)
at DatabaseXml.doGet(DatabaseXml.java:124)
at javax.servlet.http.HttpServlet.service(HttpServlet.java:621)
at javax.servlet.http.HttpServlet.service(HttpServlet.java:722)
at org.apache.catalina.core.ApplicationFilterChain.internalDoFilter(ApplicationFilterChain.java:304)
at org.apache.catalina.core.ApplicationFilterChain.doFilter(ApplicationFilterChain.java:210)
at org.apache.catalina.core.StandardWrapperValve.invoke(StandardWrapperValve.java:240)
at org.apache.catalina.core.StandardContextValve.invoke(StandardContextValve.java:164)
at org.apache.catalina.authenticator.AuthenticatorBase.invoke(AuthenticatorBase.java:462)
at org.apache.catalina.core.StandardHostValve.invoke(StandardHostValve.java:164)
at org.apache.catalina.valves.ErrorReportValve.invoke(ErrorReportValve.java:100)
at org.apache.catalina.valves.AccessLogValve.invoke(AccessLogValve.java:562)
at org.apache.catalina.core.StandardEngineValve.invoke(StandardEngineValve.java:118)
at org.apache.catalina.connector.CoyoteAdapter.service(CoyoteAdapter.java:395)
at org.apache.coyote.http11.Http11Processor.process(Http11Processor.java:250)
at org.apache.coyote.http11.Http11Protocol$Http11ConnectionHandler.process(Http11Protocol.java:188)
at org.apache.tomcat.util.net.JIoEndpoint$SocketProcessor.run(JIoEndpoint.java:302)
at java.util.concurrent.ThreadPoolExecutor$Worker.runTask(Unknown Source)
at java.util.concurrent.ThreadPoolExecutor$Worker.run(Unknown Source)
at java.lang.Thread.run(Unknown Source)
Комментарии:
1. Scala^Z3 ( lara.epfl.ch/w/ScalaZ3 ) используется для интеграции Z3 в Scala. Поскольку Scala работает на JVM, я предполагаю, что использование Scala ^ Z3 является лучшей отправной точкой?
2. Спасибо… похоже, они проделали всю работу. Я добавил журнал того, что было необходимо для ответа на вопрос ниже.
Ответ №1:
Я надеялся, что управляемая версия DLL будет иметь некоторую встроенную совместимость с Java. Похоже, это не так. Итак, ответ заключается в создании новой библиотеки DLL, которая реализует JNI-совместимый протокол вызова, как описано в книге Шэн Ляна «Собственный интерфейс Java ™: руководство и спецификация программиста». Некоторые полезные учебные пособия были найдены на веб-сайте Дэвида Колдуэлла: InOnIt
Большая часть исходного кода C была извлечена из Scala ^ Z3, и окончательная версия:
#include "stdafx.h"
#include <jni.h>
#include "z3.h"
// #include "z3_api.h" (z3.h automatically includes z3_api.h)
#include "HelloWorld.h"
#ifdef __cplusplus
extern "C" {
#endif
JNIEXPORT void JNICALL Java_example_jni_HelloWorld_getVersion (
JNIEnv * env,
jclass cls,
jobject major,
jobject minor,
jobject buildNumber,
jobject revisionNumber
) {
unsigned int cmaj, cmin, bn, rv;
jclass ipc;
jfieldID fid;
Z3_get_version(amp;cmaj, amp;cmin, amp;bn, amp;rv);
ipc = (env)->GetObjectClass(major);
fid = (env)->GetFieldID(ipc, "value", "I");
(env)->SetIntField(major, fid, (jint)cmaj);
ipc = (env)->GetObjectClass(minor);
fid = (env)->GetFieldID(ipc, "value", "I");
(env)->SetIntField(minor, fid, (jint)cmin);
ipc = (env)->GetObjectClass(buildNumber);
fid = (env)->GetFieldID(ipc, "value", "I");
(env)->SetIntField(buildNumber, fid, (jint)bn);
ipc = (env)->GetObjectClass(revisionNumber);
fid = (env)->GetFieldID(ipc, "value", "I");
(env)->SetIntField(revisionNumber, fid, (jint)rv);
}
#ifdef __cplusplus
}
#endif
Файлы заголовков поступают из нескольких источников: jni.h и его зависимости поставляются с JDK и находятся в его каталогах include и include win32. z3.h и z3_api поступают из Microsoft RISE Z3 и устанавливаются в C:Program Файлы (x86) Microsoft Research Z3-3.2 включают. Microsoft RISE также предоставляет z3.lib, который находится в C:Program Files (x86) Microsoft Research Z3-3.2 bin; вам нужно будет связать это с приведенным выше кодом в проект Win32 DLL под названием Z3GetVersion_Release.dll .
HelloWorld.h генерируется javah (см. InOnIt для примера). Чтобы сгенерировать HelloWorld.h, вам нужен следующий класс Java в файле с именем HelloWorld.java .
package example.jni;
public class HelloWorld {
private static final String LIB_SEPARATOR = "\";
private static final String LIB_NAME = "Z3GetVersion_Release";
private static final String LIB_EXT = ".dll";
/** Placeholder class to ease JNI interaction. */
public static class IntPtr {
public int value;
}
// this is just to force class loading, and therefore library loading.
public static void init() { }
static {
String curDir = System.getProperty("user.dir");
try {
System.load(curDir LIB_SEPARATOR LIB_NAME LIB_EXT);
} catch (UnsatisfiedLinkError e) {
System.out.println("Library could not be found in directory:" curDir );
} catch (SecurityException e) {
System.out.println("Security permissions prevented loading library from directory:" curDir );
}
}
/*private static void getVersion(IntPtr major, IntPtr minor, IntPtr buildNumber, IntPtr revisionNumber)
{
major.value=0;
minor.value=0;
buildNumber.value=0;
revisionNumber.value=0;
}*/
private static native void getVersion(IntPtr major, IntPtr minor, IntPtr buildNumber, IntPtr revisionNumber);
public static String z3VersionString() {
IntPtr major = new IntPtr();
IntPtr minor = new IntPtr();
IntPtr buildNumber = new IntPtr();
IntPtr revisionNumber = new IntPtr();
getVersion(major, minor, buildNumber, revisionNumber);
return "Z3 " major.value "." minor.value " (build " buildNumber.value ", rev. " revisionNumber.value ")";
}
public static void main(String[] args) {
System.out.println(z3VersionString());
}
}
В примере кода предполагается, что вы скопировали все библиотеки DLL из C:Program Files (x86) Microsoft Research Z3-3.2bin в ваш рабочий каталог, и вы указали java.exe к правильному пути к классу, где расположены ваши скомпилированные классы Java. Если все пойдет хорошо, выполнение команды «java example.jni.HelloWorld» выведет ответ: Z3 3.2 (build 0, rev. 0)
Комментарии:
1. Приведенный выше пример демонстрирует механику одного вызова и поможет понять исходный код, расположенный в Scala ^Z3 . Большое спасибо Филиппу Сутеру за реализацию оставшихся вызовов.