0

Microsoft.Z3.dll 在文件属性中被描述为 Z3 托管 DLL。

Java可以加载dll。它使用 System.loadLibrary 或 System.load 执行此操作,具体取决于程序员的偏好。

如果 Java 设计者还创建了 DLL,则可以使用 javah 来定义导入/导出声明。不幸的是,这不是我的情况。Microsoft 已将 DLL 创建为托管 C# DLL。

我需要一些帮助来获取 C# 声明,例如在Microsoft RISE Z3 托管 API中找到的声明,并对Java 包/类进行原型设计以使调用成功。(我确信 DLL 已加载)。

为方便起见,具体调用由 Microsoft 在 Microsoft.Z3.h 的第 03042 行定义。任何示例代码将不胜感激!

我从我的服务器得到的错误是:

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)
4

1 回答 1

1

我曾希望 DLL 的托管版本与 Java 有一些本机兼容性。看起来并非如此。因此,答案是生成一个新的 DLL,该 DLL 实现了一个与 JNI 兼容的调用协议,如盛亮的“Java™ 本地接口:程序员指南和规范”中所述。在 David Caldwell 的网站上找到了一些有用的教程: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(&cmaj, &cmin, &bn, &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 Files (x86)\Microsoft Research\Z3-3.2\include。Microsoft RISE 还提供 z3.lib,它位于 C:\Program Files (x86)\Microsoft Research\Z3-3.2\bin;您需要将其与上述代码链接到名为 Z3GetVersion_Release.dll 的 Win32 DLL 项目中。

HelloWorld.h 由 javah 生成(参见 InOnIt 示例)。要生成 HelloWorld.h,您需要在名为 HelloWorld.java 的文件中包含以下 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.2\bin 复制到您的工作目录,并且您已将 java.exe 指向已编译的 java 类所在的正确类路径. 如果一切顺利,运行命令“java example.jni.HelloWorld”将输出响应:Z3 3.2 (build 0, rev. 0)

于 2011-11-02T22:44:06.107 回答