search

kframework / k-legacy

The K tools (deprecated, see README)
http://kframework.org
Other
146 stars 61 forks source link

UnsatisfiedLinkError when using Z3 with K (Java 8) #977

Closed traiansf closed 9 years ago

traiansf commented 10 years ago

I was trying to help @osa1 debug an issue with #959 but I was stopped by some problems with the z3 smt libraries.

mvn package

Running org.kframework.backend.java.symbolic.UseSMTTest
c:\Program Files\Java\jdk1.8.0_05\jre\bin;C:\WINDOWS\Sun\Java\bin;C:\WINDOWS\system32;C:\WINDOWS;C:\Program Files\Java\jdk1.7.0_45\bin;c:\Program Files\Java\jdk1.8.0_05\bin;C:\WinDDK\SDV\bin;C:\Program Files (x86)\Haskell\bin;C:\Program Files (x86)\Haskell Platform\2013.2.0.0\lib\extralibs\bin;C:\Program Files (x86)\Haskell Platform\2013.2.0.0\bin;C:\Program Files (x86)\ImageMagick-6.8.7-Q16;C:\Program Files (x86)\NVIDIA Corporation\PhysX\Common;C:\WINDOWS\system32;C:\WINDOWS;C:\WINDOWS\System32\Wbem;C:\WINDOWS\System32\WindowsPowerShell\v1.0\;C:\Program Files (x86)\Git\cmd;C:\Program Files (x86)\Git\bin;C:\Program Files (x86)\Universal Extractor;C:\Program Files (x86)\Universal Extractor\bin;C:\Program Files\SlikSvn\bin;C:\Program Files (x86)\Calibre2\;C:\Program Files (x86)\Haskell Platform\2013.2.0.0\mingw\bin;C:\Program Files (x86)\scala\\bin;C:\Program Files (x86)\Windows Live\Shared;C:\Program Files (x86)\QuickTime\QTSystem\;C:\Program Files (x86)\Tesseract-OCR;C:\Program Files (x86)\sbt\\bin;C:\Users\Traian\AppData\Roaming\cabal\bin;C:\Program Files\MiKTeX 2.9\miktex\bin\x64\;c:\programs\miktex\miktex\bin\;C:\Users\Traian\AppData\Local\Pandoc\;c:\cygwin\bin;C:\Program Files (x86)\PuTTY;C:\Program Files\MiKTeX 2.9\miktex\bin\x64;C:\programs\ant\bin;c:\Users\Traian\Documents\k\bin;c:\Users\Traian\Documents\k\lib\maude\binaries;C:\programs\Python33;c:\Programs\apache-maven\bin;C:\Users\Traian\Documents\k\target/lib/native;C:\Program Files (x86)\PuTTY;C:\Program Files\MiKTeX 2.9\miktex\bin\x64;C:\programs\ant\bin;c:\Users\Traian\Documents\k\bin;c:\Users\Traian\Documents\k\lib\maude\binaries;C:\programs\Python33;.
 Tests run: 1, Failures: 0, Errors: 1, Skipped: 0, Time elapsed: 0.125 sec 
<<< FAILURE! - in org.kframework.backend.java.symbolic.UseSMTTest
testGetModel(org.kframework.backend.java.symbolic.UseSMTTest)  Time elapsed: 0.112 sec  
<<<  ERROR!
    java.lang.UnsatisfiedLinkError: C:\Users\Traian\Documents\k\target\lib\native\z3java.dll: 
        %1 is not a valid Win32 application
    at java.lang.ClassLoader$NativeLibrary.load(Native Method)
    at java.lang.ClassLoader.loadLibrary0(ClassLoader.java:1929)
    at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1847)
    at java.lang.Runtime.loadLibrary0(Runtime.java:870)
    at java.lang.System.loadLibrary(System.java:1119)
    at com.microsoft.z3.Native.<clinit>(Native.java:10)
    at com.microsoft.z3.Context.<init>(Context.java:24)
    at org.kframework.backend.java.symbolic.UseSMT.checkSat(UseSMT.java:34)
    at org.kframework.backend.java.symbolic.UseSMTTest.testGetModel(UseSMTTest.java:58)

git branch -vv |grep "^*"
* java8                           1193fac [osa1/java8] update output of one of the failing tests
dwightguth commented 10 years ago

Can I please see java -version and mvn -version both?

traiansf commented 10 years ago

Sure:

java -version
java version "1.8.0_05"
Java(TM) SE Runtime Environment (build 1.8.0_05-b13)
Java HotSpot(TM) 64-Bit Server VM (build 25.5-b02, mixed mode)

mvn -version
Apache Maven 3.2.1 (ea8b2b07643dbb1b84b6d16e1f08391b666bc1e9; 2014-02-14T19:37:52+02:00)
Maven home: c:\programs\apache-maven\bin\..
Java version: 1.8.0_05, vendor: Oracle Corporation
Java home: c:\Program Files\Java\jdk1.8.0_05\jre
Default locale: ro_RO, platform encoding: Cp1252
OS name: "windows 8.1", version: "6.3", arch: "amd64", family: "dos"
dwightguth commented 10 years ago

And just to be on the safe side, what do you see from mvn help:active-profiles?

If you see amd64 and windows as the only two active profiles, I suspect you are having some kind of dll hell. If that is the case, I suggest you modify your path by deleting absolutely everything you don't need to run this command, and let me know if that fixes the issue. If it does, I will add a note to the readme.

If on the other hand you see a different set of profiles, we have a different problem.

dwightguth commented 10 years ago

Actually, can you let me know if running mvn clean fixes the problem either?

traiansf commented 10 years ago

The following profiles are active:

mvn clean does not fix the problem

I'll try tweaking the path. Actually, I had this problem before with z3 dlls. And because I could not solve it, I decided on using the z3 executables for RV-Predict. I know this is not an option for K, though...

dwightguth commented 10 years ago

I am assigning this to Traian so he can track it. Traian, if you can trace it down to a specific dll that is causing you problems, I can make a note about it in the readme.

traiansf commented 10 years ago

The error still persists, even with using java 7 and with nothing on the path except maven. I used to have issues with the z3 dlls even before.

C:\Users\Traian\Documents\k>echo %PATH%
c:\programs\apache-maven\bin

C:\Users\Traian\Documents\k>echo %JAVA_HOME%
c:\Program Files\Java\jdk1.7.0_45

C:\Users\Traian\Documents\k>mvn package
......................
 <<< FAILURE! - in org.kframework.backend.java.symbolic.UseSMTTest
testGetModel(org.kframework.backend.java.symbolic.UseSMTTest)  Time elapsed: 0.137 sec  <<< ERROR!
java.lang.UnsatisfiedLinkError: C:\Users\Traian\Documents\k\java-backend\target\lib\native\z3java.dll: Can't find dependent libraries
    at java.lang.ClassLoader$NativeLibrary.load(Native Method)
    at java.lang.ClassLoader.loadLibrary1(ClassLoader.java:1965)
    at java.lang.ClassLoader.loadLibrary0(ClassLoader.java:1890)
    at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1880)
    at java.lang.Runtime.loadLibrary0(Runtime.java:849)
    at java.lang.System.loadLibrary(System.java:1088)
    at com.microsoft.z3.Native.<clinit>(Native.java:10)
    at com.microsoft.z3.Context.<init>(Context.java:24)
    at org.kframework.backend.java.symbolic.UseSMT.checkSat(UseSMT.java:44)
    at org.kframework.backend.java.symbolic.UseSMTTest.testGetModel(UseSMTTest.java:58)

I've tried adding the 'native' directory to the path, but it still doesn't work.

dwightguth commented 10 years ago

This is now a different error message, likely because it no longer has the visual C++ runtime on the path. Please use a dll analysis tool to look up what the needed dependencies are, add them, and let me know if it solves the issue. If it does, gradually re-add path entries until it breaks again, and then tell me which path element caused the error.

On Fri, Oct 3, 2014 at 1:56 PM, Traian Florin Șerbănuță < notifications@github.com> wrote:

The error still persists, even with using java 7 and with nothing on the path except maven. I used to have issues with the z3 dlls even before.

C:\Users\Traian\Documents\k>echo %PATH% c:\programs\apache-maven\bin

C:\Users\Traian\Documents\k>echo %JAVA_HOME% c:\Program Files\Java\jdk1.7.0_45

C:\Users\Traian\Documents\k>mvn package ...................... <<< FAILURE! - in org.kframework.backend.java.symbolic.UseSMTTest testGetModel(org.kframework.backend.java.symbolic.UseSMTTest) Time elapsed: 0.137 sec <<< ERROR! java.lang.UnsatisfiedLinkError: C:\Users\Traian\Documents\k\java-backend\target\lib\native\z3java.dll: Can't find dependent libraries at java.lang.ClassLoader$NativeLibrary.load(Native Method) at java.lang.ClassLoader.loadLibrary1(ClassLoader.java:1965) at java.lang.ClassLoader.loadLibrary0(ClassLoader.java:1890) at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1880) at java.lang.Runtime.loadLibrary0(Runtime.java:849) at java.lang.System.loadLibrary(System.java:1088) at com.microsoft.z3.Native.(Native.java:10) at com.microsoft.z3.Context.(Context.java:24) at org.kframework.backend.java.symbolic.UseSMT.checkSat(UseSMT.java:44) at org.kframework.backend.java.symbolic.UseSMTTest.testGetModel(UseSMTTest.java:58)

I've tried adding the 'native' directory to the path, but it still doesn't work.

— Reply to this email directly or view it on GitHub https://github.com/kframework/k/issues/977#issuecomment-57838473.

traiansf commented 10 years ago

ok, I think I've tracked it down.

Apparently it needs the right vcomp100.dll to be in the path

If you want to pack them with it, I have the ones I need for the windows z3 executable (both for 32 and for 64 bits)

dwightguth commented 10 years ago

sigh

I told you you needed to install the visual C++ 2010 runtime for the same architecture as your jvm. It's in the readme, too. I can make this more clear if there's something confusing, but at some point there's no fix for this problem other than just following the instructions.

On Fri, Oct 3, 2014 at 2:53 PM, Traian Florin Șerbănuță < notifications@github.com> wrote:

ok, I think I've tracked it down.

Apparently it needs the right vcomp100.dll to be in the path

If you want to pack them with it, I have the ones I need for the windows z3 executable (both for 32 and for 64 bits)

— Reply to this email directly or view it on GitHub https://github.com/kframework/k/issues/977#issuecomment-57847410.

traiansf commented 10 years ago

Maybe, but I think it's not fair to our users to ask them to install VC++ 2010 runtime, which they might not even get right, as I didn't

Why don't we better do the same as the z3 guys do on their site and package the dlls with the needed dlls to function appropriately.

grosu commented 10 years ago

This sounds right to me. I would definitely not want to spend any minutes on that; for me, that would be a good excuse to throw a system away and not look back.

Grigore

From: Traian Florin Șerbănuță [notifications@github.com] Sent: Monday, October 06, 2014 2:13 PM To: kframework/k Subject: Re: [k] UnsatisfiedLinkError when using Z3 with K (Java 8) (#977)

Maybe, but I think it's not fair to our users to ask them to install VC++ 2010 runtime, which they might not even get right, as I didn't

Why don't we better do the same as the z3 guys do on their site and package the dlls with the needed dlls to function appropriately.

— Reply to this email directly or view it on GitHubhttps://github.com/kframework/k/issues/977#issuecomment-58076175.