Z3 Java API fails to detect libz3.dylib #294

Eipifi · 2015-11-05T13:10:33Z

This is a crosspost of an issue reported here: https://stackoverflow.com/questions/33541226/z3-java-api-fails-to-detect-libz3-dylib

When running Z3 via the Java wrapper, the libz3.dylib library is not recognised by libz3java.dylib.

Trying to load the library by hand results in the following behaviour:

package example;

public class Main {

    public static void main(String[] args) {
        System.out.println(System.getProperty("sun.arch.data.model"));
        System.out.println(exec("file /tmp/z3/build/libz3.dylib"));
        System.out.println(exec("file /tmp/z3/build/libz3java.dylib"));

        System.load("/tmp/z3/build/libz3.dylib");
        System.load("/tmp/z3/build/libz3java.dylib"); // line 14
    }

    private static String exec(String command) { (...) }

}

The output:

64
/tmp/z3/build/libz3.dylib: Mach-O 64-bit dynamically linked shared library x86_64

/tmp/z3/build/libz3java.dylib: Mach-O 64-bit dynamically linked shared library x86_64

Exception in thread "main" java.lang.UnsatisfiedLinkError:
    /private/tmp/z3/build/libz3java.dylib:
        dlopen(/private/tmp/z3/build/libz3java.dylib, 1): 
            Library not loaded: libz3.dylib
  Referenced from: /private/tmp/z3/build/libz3java.dylib
  Reason: image not found
    at java.lang.ClassLoader$NativeLibrary.load(Native Method)
    at java.lang.ClassLoader.loadLibrary0(ClassLoader.java:1929)
    at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1814)
    at java.lang.Runtime.load0(Runtime.java:809)
    at java.lang.System.load(System.java:1083)
    at example.foo.Main.main(Main.java:14)

Z3: 4.4.1 (commit 95c9ccb)
Java version: 1.8.0_25-b17
System: OS X 10.11.1 (El Capitan)

This may or may not be related to the recent OS X upgrade, but I have no evidence for it.

The text was updated successfully, but these errors were encountered:

Eipifi · 2015-11-05T13:40:25Z

Tested on 64bit Debian 8.0, same issue.

package example;

public class Main {

    public static void main(String[] args) {
        System.load("/tmp/z3/build/libz3.so");
        System.load("/tmp/z3/build/libz3java.so"); // line 8
    }

}

The output:

Exception in thread "main" java.lang.UnsatisfiedLinkError: /tmp/z3/build/libz3java.so: libz3.so: cannot open shared object file: No such file or directory
    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:1851)
    at java.lang.Runtime.load0(Runtime.java:795)
    at java.lang.System.load(System.java:1062)
    at Example.main(Example.java:8)

wintersteiger · 2015-11-09T14:04:24Z

Is /tmp/z3/build/ in your (DY)LD_LIBRARY_PATH and or java.library.path?

Note that

System.load("/tmp/z3/build/libz3java.dylib");

actually loads

/private/tmp/z3/build/libz3java.dylib

(extra /private)

wintersteiger · 2015-11-26T12:10:22Z

Bumping this. Is this still an issue or has this been resolved?

wintersteiger · 2015-12-03T13:41:15Z

Since there was no further update on this issue, I assume that it has been resolved and those I'll close it.

243698334 · 2015-12-16T09:46:42Z

Add an environment variable to your IDE's run configuration. e.g. for a mac, DYLD_LIBRARY_PATH = "path/to/z3/lib"

markusvoelter · 2015-12-25T16:14:58Z

´I still have the problem. I have defined the DYLD_LIBRARY_PATH as well as java.library.path. I still get the exception. I have added debug code that prints the java.library.path and it comes out correctly.

Here is an interesting observation: if I run the program from the directory that contains the dylib, then it works. As soon as I start from a different directory, using DYLD_LIBRARY_PATH and java.library.path to try to find the native libs, it does not work.

Here is the exception I get:

$ java -cp ./bin/com.microsoft.z3.jar:. -Djava.library.path="/Users/markusvoelter/Downloads/z3-4.4.1-x64-osx-10.11/bin" JavaExample
/Users/markusvoelter/Downloads/z3-4.4.1-x64-osx-10.11/bin
Exception in thread "main" java.lang.UnsatisfiedLinkError: no libz3java in java.library.path
at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1865)
at java.lang.Runtime.loadLibrary0(Runtime.java:870)
at java.lang.System.loadLibrary(System.java:1122)
at com.microsoft.z3.Native.(Native.java:14)
at com.microsoft.z3.Global.ToggleWarningMessages(Global.java:86)
at JavaExample.main(JavaExample.java:2268)

If I now rename libz3java.dylib to liblibz3java.dylib, it seems I get one step further. I get the following exception:

Exception in thread "main" java.lang.UnsatisfiedLinkError: /Users/markusvoelter/Downloads/z3-4.4.1-x64-osx-10.11/bin/liblibz3java.dylib: dlopen(/Users/markusvoelter/Downloads/z3-4.4.1-x64-osx-10.11/bin/liblibz3java.dylib, 1): Library not loaded: libz3.dylib
Referenced from: /Users/markusvoelter/Downloads/z3-4.4.1-x64-osx-10.11/bin/liblibz3java.dylib
Reason: image not found
at java.lang.ClassLoader$NativeLibrary.load(Native Method)
at java.lang.ClassLoader.loadLibrary0(ClassLoader.java:1937)
at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1855)
at java.lang.Runtime.loadLibrary0(Runtime.java:870)
at java.lang.System.loadLibrary(System.java:1122)
at com.microsoft.z3.Native.(Native.java:14)
at com.microsoft.z3.Global.ToggleWarningMessages(Global.java:86)
at JavaExample.main(JavaExample.java:2268)

Not it seems it can load libz3java.dylib but now misses libz3.dylib.

wintersteiger · 2015-12-25T16:37:07Z

Did you make sure that both, Java and Z3 are both 64-bit? They must be the same, otherwise the error message might just say 'can't find' or 'can't load'.

markusvoelter · 2015-12-25T16:39:40Z

Wow, thanks for your quick reply!!

I have downloaded this Z3:
https://github.com/Z3Prover/z3/releases/download/z3-4.4.1/z3-4.4.1-x64-osx-10.11.zip

And my Java outputs:
openjdk version "1.8.0_40-internal"
OpenJDK Runtime Environment (build 1.8.0_40-internal-b64)
OpenJDK 64-Bit Server VM (build 25.40-b25, mixed mode)

wintersteiger · 2015-12-25T16:39:59Z

Also, could you try a more recent nightly binary? The 4.4.1 release is already a few months old. Or even better, compile it from source.

markusvoelter · 2015-12-25T17:29:21Z

Ok, I rebuilt from sources. Same problem. If I run the JavaExample from its directory with the following command

$ java -Djava.library.path=../../build -cp ../../build/com.microsoft.z3.jar:. JavaExample

I still get the exception:

Exception in thread "main" java.lang.UnsatisfiedLinkError: no libz3java in java.library.path
at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1865)
at java.lang.Runtime.loadLibrary0(Runtime.java:870)
at java.lang.System.loadLibrary(System.java:1122)
at com.microsoft.z3.Native.(Native.java:14)
at com.microsoft.z3.Global.ToggleWarningMessages(Global.java:86)
at JavaExample.main(JavaExample.java:2287)

This happens irrespective of whether I define the LD_LIBRARY_PATH or DYLD_LIBRARY_PATH or not.

wintersteiger · 2015-12-25T19:46:45Z

Yes, the Java API is only built with --java added to python scripts/mk_make.py.

Can you confirm that there is a file called libz3java.dylib?

markusvoelter · 2015-12-25T19:48:33Z

Yes, I found out about the --java option. Did that.

Yes, the file exists; see screenshot.

markusvoelter · 2015-12-25T21:56:20Z

This seems to be a Mac-specific problem. We just ran the same tests on Windows and on a Mac: on WIndows, it works, on the Mac the tests fail with the exception I reported above.

markusvoelter · 2015-12-26T08:00:29Z

I have debugged into this a little bit futher; specifically, I have added print statements to the code that loads the library:

  static {
    System.err.println("java.library.path = " + System.getProperty("java.library.path"));
    System.err.println("trying to load lib z3java");
    try { 
        System.loadLibrary("z3java"); 
    } catch (UnsatisfiedLinkError ex1) { 
        ex1.printStackTrace();
        try { 
            System.err.println("Trying to load lib libz3java");
            System.loadLibrary("libz3java"); 
        } catch (UnsatisfiedLinkError ex2) { 
            ex2.printStackTrace();
        }
    }
  }

When I run this, I get

java.library.path = /Users/markusvoelter/Documents/mbeddr/z3/build/
trying to load lib z3java
java.lang.UnsatisfiedLinkError: /Users/markusvoelter/Documents/mbeddr/z3/build/libz3java.dylib: dlopen(/Users/markusvoelter/Documents/mbeddr/z3/build/libz3java.dylib, 1): Library not loaded: libz3.dylib
  Referenced from: /Users/markusvoelter/Documents/mbeddr/z3/build/libz3java.dylib
  Reason: image not found
    at java.lang.ClassLoader$NativeLibrary.load(Native Method)
    at java.lang.ClassLoader.loadLibrary0(ClassLoader.java:1937)
    at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1855)
    at java.lang.Runtime.loadLibrary0(Runtime.java:870)
    at java.lang.System.loadLibrary(System.java:1122)
    at com.microsoft.z3.Native.<clinit>(Native.java:16)
    at com.microsoft.z3.Global.ToggleWarningMessages(Global.java:86)
    at JavaExample.main(JavaExample.java:2287)
Trying to load lib libz3java
java.lang.UnsatisfiedLinkError: no libz3java in java.library.path
    at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1865)
    at java.lang.Runtime.loadLibrary0(Runtime.java:870)
    at java.lang.System.loadLibrary(System.java:1122)
    at com.microsoft.z3.Native.<clinit>(Native.java:21)
    at com.microsoft.z3.Global.ToggleWarningMessages(Global.java:86)
    at JavaExample.main(JavaExample.java:2287)
Exception in thread "main" java.lang.UnsatisfiedLinkError: com.microsoft.z3.Native.INTERNALtoggleWarningMessages(Z)V
    at com.microsoft.z3.Native.INTERNALtoggleWarningMessages(Native Method)
    at com.microsoft.z3.Native.toggleWarningMessages(Native.java:3082)
    at com.microsoft.z3.Global.ToggleWarningMessages(Global.java:86)
    at JavaExample.main(JavaExample.java:2287)

So it tries to load z3java, which I think initially succeeds. But then that lib tries to load libz3.dylib, which fails. At this point, the whole loadLibrary call for z3java fails, and the system tries to load libz3java (which I think triggers liblibz3java), because a "lib" is automatically prepended.

If I create a copy liblibz3java.dylib of ibz3java.dylib, then the initial loading succeeds, and I get the same

Referenced from: /Users/markusvoelter/Documents/mbeddr/z3/build/liblibz3java.dylib
Reason: image not found

as before. So we can conclude: it is not the initial loading of libz3java that fails, but rather, the subsequent loading of libz3.dylib.

markusvoelter · 2015-12-26T08:19:09Z

Ok, I have found the problem. It is (once again!!) Apple's security crap causing problems:
oracle/node-oracledb#231

If you turn of SIP, the library is loaded correctly. While I was able to do this, requiring our end users to do this is going to be essentially impossible. Any chance this can be fixed with some kind of workaround?

wintersteiger · 2015-12-29T14:54:37Z

Wow, thanks for getting to the bottom of this and reporting it back! It never even crossed my mind to check any system features like SIP, so that would have taken me ages to figure out. Definitely an opportunity to improve error messages, but I'm not sure that we can do anything about that on our end.

markusvoelter · 2015-12-29T14:56:26Z

A good error message would of course help. A workaround seems to be to put the dylib into the working dir of the process: loading still works, only the DYLIB.... path seems to be ignored.

bkolb · 2016-01-08T09:21:33Z

Here is the openJDK bug for the underlaying issue. It contains some recommendations. Not sure if any of them works here: https://bugs.openjdk.java.net/browse/JDK-8139288

harcokuppens · 2017-12-18T16:07:40Z

I did some extra investigation and found a solution which works with SIP enabled.

When java loads a dynamic library it only looks at the locations in java.library.path.
From Apple's official developer documentation at Important Java Directories on Mac OS X - Extension Libraries we find that the standard java.library.path contains :

Static            
      - ~/Library/Java/Extensions/ : for single user 
      - /Library/Java/Extensions   : for all users
      - $JAVA_HOME/lib/ext         : for specific jvm installation

Important: it seems that Java LoadLibrary first looks in

working directory
directories in java.library.path

I tested this on os x, and there it seems to look first at working directory!
Couldn't find an official source, but only some none official sources:
https://stackoverflow.com/questions/13695718/java-working-directory
https://community.oracle.com/thread/1551225?tstart=0
https://soar.eecs.umich.edu/articles/articles/building-soar/86-how-library-search-paths-work

Normally when an exectutable or library loads a dynamic library it looks at location specified by the operating system.
From Apple's official developer documentation at Using Dynamic Libraries and The Library Search Process we find that the standard locations where OS X looks are

 Dynamic
        $CWD            : current working directory of the current process
 
 Static  
        ~/lib           : for single user 
        /usr/local/lib  : for all users 
        /usr/lib        : contains system protected libraries by SIP   
                          Proof by running: /bin/ls -lOd /usr/lib

Note that above fixed locations are the locations set in the default value for DYLD_FALLBACK_LIBRARY_PATH. These locations are still used when SIP is enabled as I found by the following reference:

https://community.plm.automation.siemens.com/t5/3D-Simulation-Simcenter-3D-Forum/NX-Support-for-El-Capitan-MAC-OSX-v10-11/td-p/327539
01-11-2016 

    As it turns out, although DYLD* variables are unavailable in El Capitan,
    the default value for DYLD_FALLBACK_LIBRARY_PATH is still set internally,

So for z3 above @markusvoelter concluded that it is not the initial loading of libz3java that fails, but rather, the subsequent loading of libz3.dylib. Loading of the JNI library succeeds because @markusvoelter set the java.library.path explicitly on the commandline in its test. However subsequent loading of libz3.dylib by libz3java.dylib fails because:

java is a SIP protected executable which ignores user set DYLD_LIBRARY_PATH
Proof by running: /bin/ls -lO $(which java)
libz3.dylib is not in one the standard locations of OS X : not in ~/lib, /usr/local/lib, /usr/lib

So the quickfix is to move or link libz3.dylib in ~/lib.

Personally I'm the only user of my macbook and prefer not to put libraries in my homedir, so I prefer the solution :

put JNI dynamic link libraries in: /Library/Java/Extensions
e.g. libz3java.dylib
put none-JNI dynamic link libraries in: /usr/local/lib
e.g. libz3.dylib

Note: to preserve the original installation I prefer soft linking into the original installation locations which also works fine.

However if you would have different versions of a library then with above central installation we have a problem because we can only link one version! In that case you add the dynamic link libraries at working directory ($CWD ) of each specific program. This works because as specified above for both jni and none-jni dynamic libraries are searched first at the current working directory of the current process.

A completely alternative solution is to relink the subsequent library dependency of libz3.dylib in libz3java.dylib with an absolute path so that it doesn't need a PATH. For how to do this look at: http://thecourtsofchaos.com/2013/09/16/how-to-copy-and-relink-binaries-on-osx/

However personally I prefer to just use the standard, that is use the above standard locations!!

delcypher · 2017-12-20T16:32:20Z

@harcokuppens Have you tried to get this to work when building with the CMake build system? IIRC CMake does things a little differently (than the old build system). libz3java.dylib in the build directory should be linked to libz3.dylib using the rpath mechanism so that when linking libz3java.dylib, libz3.dylib should always be found.

harcokuppens · 2017-12-22T09:31:41Z

No, I didn't used cmake. I just downloaded a prebuild version of z3 from https://github.com/Z3Prover/bin/tree/master/releases . This already contains libz3java.dylib and libz3.dylib . I didn't use the homebrew version on os x because that build doesn't contain libz3java.dylib.

Then I just used maven or eclipse to build. But any other java build system should be fine as long you put the dynamic libraries on the right locations mentioned in my previous post.

However from your post it is not clear what exactly you are building? Are you building z3 with cmake, or are you building a java project with cmake which uses z3 as library?

Anyway what I do know is that for java builds you cannot use DYLD_LIBRARY_PATH because the java executable is a SIP protected file.

Source: conda-forge/staged-recipes#913 (comment)

To be clear, DYLD_LIBRARY_PATH and DYLD_FALLBACK_LIBRARY_PATH (and all other DYLD* environment variables) are only disabled by SIP for protected binaries--like those in /usr/bin. This means you can't pass them to things that use OSX's bash (like autotools), but they do work for passing to python (and even bash) so long as they aren't the system copies. This is one reason we use cmake to build libnetcdf.

You can see whether a binary is SIP protected by the following command :

$  /bin/ls -lO $(realpath $(which java))
-rwxr-xr-x  1 root  wheel  restricted,compressed 54624 14 jul  2015 /System/Library/Frameworks     /JavaVM.framework/Versions/A/Commands/java

where restricted means protected by SIP.
If I run the same command on the cmake installed with homebrew I get :

  $ /bin/ls -lO $(realpath $(which cmake))
  -r-xr-xr-x  1 harcok  admin  - 5223036  7 sep  2016 /usr/local/Cellar/cmake/3.6.2/bin/cmake

So cmake is not restricted and not protected by SIP. So what I understand from the apple documentation you can then use the DYLD_LIBRARY_PATH environment variable without any problems. However I must say I didn't test this with cmake, but above quote seems to say it should work with cmake.

Apple documentation about SIP

However in general I would just use the standard install locations for .dylib files and don't rely on DYLD_LIBRARY_PATH for installations anymore. However for developer builds it can be convenient to use DYLD_LIBRARY_PATH, and then it maybe convenient to use cmake from homebrew.

dhanumamidi · 2023-11-08T17:00:03Z

Facing the same issue I have tried all the solutions mentioned above. Need help to identify where I'm going wrong.

Java --version
java 17.0.8 2023-07-18 LTS
Java(TM) SE Runtime Environment (build 17.0.8+9-LTS-211)
Java HotSpot(TM) 64-Bit Server VM (build 17.0.8+9-LTS-211, mixed mode, sharing)

lrwxr-xr-x 1 root wheel 58 Nov 8 22:15 liblibz3java.dylib -> /Users/dhanu/Documents/Covlant/z3/z3/build/libz3java.dylib
lrwxr-xr-x 1 root wheel 58 Nov 8 22:14 libz3java.dylib -> /Users/dhanu/Documents/Covlant/z3/z3/build/libz3java.dylib

trying to load lib z3java
java.lang.UnsatisfiedLinkError: no z3java in java.library.path: /Library/Java/Extensions
at java.base/java.lang.ClassLoader.loadLibrary(ClassLoader.java:2429)
at java.base/java.lang.Runtime.loadLibrary0(Runtime.java:818)
at java.base/java.lang.System.loadLibrary(System.java:1989)
at org.covlant.UnitTestGeneratorApp.(UnitTestGeneratorApp.java:23)
Trying to load lib libz3java
java.lang.UnsatisfiedLinkError: no libz3java in java.library.path: /Library/Java/Extensions
at java.base/java.lang.ClassLoader.loadLibrary(ClassLoader.java:2429)
at java.base/java.lang.Runtime.loadLibrary0(Runtime.java:818)
at java.base/java.lang.System.loadLibrary(System.java:1989)
at org.covlant.UnitTestGeneratorApp.(UnitTestGeneratorApp.java:28)
Exception in thread "main" java.lang.UnsatisfiedLinkError: no libz3java in java.library.path: /Library/Java/Extensions
at java.base/java.lang.ClassLoader.loadLibrary(ClassLoader.java:2429)
at java.base/java.lang.Runtime.loadLibrary0(Runtime.java:818)

I have tried directly passing the lib location too nothing worked. Thanks in advance for the help.

wintersteiger closed this as completed Dec 3, 2015

ksluckow mentioned this issue Jun 4, 2016

Unable to install jConstraints-z3 psycopaths/jconstraints-z3#1

Closed

FibreFoX mentioned this issue Sep 7, 2016

Add option to configure environment variables FibreFoX/javafx-gradle-plugin#34

Closed

alcides mentioned this issue Feb 28, 2018

Inconsistent (check-sat) result between Java API and commandline-tool #1112

Closed

idiomaticrefactoring mentioned this issue Apr 28, 2018

Z3 fails to find libz3java on windows #1603

Closed

polgreen mentioned this issue Jan 28, 2021

z3 java API fails to detect libz3.dylib on BigSur #4979

Open

ochimo mentioned this issue Apr 22, 2022

MacOS installation error KeenSecurityLab/BinAbsInspector#12

Closed

zcai1 mentioned this issue Jun 14, 2022

Use standalone z3-turnkey dependency instead of jar files opprop/checker-framework-inference#402

Merged

YSaxon mentioned this issue Nov 9, 2022

How to get GhiHorn to find Z3 dylibs in macOS CERTCC/kaiju#30

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Z3 Java API fails to detect libz3.dylib #294

Z3 Java API fails to detect libz3.dylib #294

Eipifi commented Nov 5, 2015

Eipifi commented Nov 5, 2015

wintersteiger commented Nov 9, 2015

wintersteiger commented Nov 26, 2015

wintersteiger commented Dec 3, 2015

243698334 commented Dec 16, 2015

markusvoelter commented Dec 25, 2015

wintersteiger commented Dec 25, 2015

markusvoelter commented Dec 25, 2015

wintersteiger commented Dec 25, 2015

markusvoelter commented Dec 25, 2015

wintersteiger commented Dec 25, 2015

markusvoelter commented Dec 25, 2015

markusvoelter commented Dec 25, 2015

markusvoelter commented Dec 26, 2015

markusvoelter commented Dec 26, 2015

wintersteiger commented Dec 29, 2015

markusvoelter commented Dec 29, 2015

bkolb commented Jan 8, 2016

harcokuppens commented Dec 18, 2017 •

edited

Loading

delcypher commented Dec 20, 2017

harcokuppens commented Dec 22, 2017 •

edited

Loading

dhanumamidi commented Nov 8, 2023 •

edited

Loading

Z3 Java API fails to detect libz3.dylib #294

Z3 Java API fails to detect libz3.dylib #294

Comments

Eipifi commented Nov 5, 2015

Eipifi commented Nov 5, 2015

wintersteiger commented Nov 9, 2015

wintersteiger commented Nov 26, 2015

wintersteiger commented Dec 3, 2015

243698334 commented Dec 16, 2015

markusvoelter commented Dec 25, 2015

wintersteiger commented Dec 25, 2015

markusvoelter commented Dec 25, 2015

wintersteiger commented Dec 25, 2015

markusvoelter commented Dec 25, 2015

wintersteiger commented Dec 25, 2015

markusvoelter commented Dec 25, 2015

markusvoelter commented Dec 25, 2015

markusvoelter commented Dec 26, 2015

markusvoelter commented Dec 26, 2015

wintersteiger commented Dec 29, 2015

markusvoelter commented Dec 29, 2015

bkolb commented Jan 8, 2016

harcokuppens commented Dec 18, 2017 • edited Loading

delcypher commented Dec 20, 2017

harcokuppens commented Dec 22, 2017 • edited Loading

dhanumamidi commented Nov 8, 2023 • edited Loading

harcokuppens commented Dec 18, 2017 •

edited

Loading

harcokuppens commented Dec 22, 2017 •

edited

Loading

dhanumamidi commented Nov 8, 2023 •

edited

Loading