如何從Java的Microsoft.Z3.dll中調用Z3_get_version（）

Question

Microsoft.Z3.dll在文件屬性中描述爲Z3 Managed DLL。

Java可以加載dll。它使用System.loadLibrary或System.load，這取決於程序員的偏好。

如果Java設計器也創建DLL，則可以使用javah來定義導入/導出聲明。不幸的是，那不是我的情況。該DLL已經由Microsoft創建爲Managed C＃DLL。

我需要一些幫助，例如在Microsoft RISE Z3 managed API上找到的C＃聲明以及原型化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) 

Answer 1

我曾希望該DLL的託管版本將具備Java一些本地的兼容性。它並非如此。因此，答案是生成一個新的DLL，它執行Sheng Liang's "The Java™ Native Interface:Programmer’s Guide and Specification"中描述的與JNI兼容的呼叫協議。一些有用的教程是關於David Caldwell's website: InOnIt

大部分的C源代碼是從斯卡拉^ 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 \ win32目錄中。 z3.h和z3_api來自Microsoft RISE Z3並安裝到C：\ Program Files（x86）\ Microsoft Research \ Z3-3.2 \ include。 Microsoft RISE還提供駐留在C：\ Program Files（x86）\ Microsoft Research \ Z3-3.2 \ bin中的z3.lib;您需要將其與上面的代碼鏈接到名爲Z3GetVersion_Release.dll的Win32 DLL項目中。

HelloWorld.h由javah生成（請參閱InOnIt for the example）。要生成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）的\微軟研究院\ Z3-3.2 \ bin添加到你的工作目錄，你已經指出的java.exe到正確的類路徑編譯的Java類所在的位置。如果一切順利，運行命令「java example.jni.HelloWorld」將輸出響應：Z3 3.2（build 0，rev。0）