epfl-lara / ScalaZ3

DSL in Scala for Constraint Solving with Z3 SMT Solver
Apache License 2.0
121 stars 33 forks source link

Native z3 library can't be loaded on Mac OS #56

Closed dragos closed 6 years ago

dragos commented 6 years ago

There are 3 native libraries that need to be loaded by ScalaZ3, with the following dependencies:

libz3java --> libz3 <-- libscalaz3

These dependencies are part of the dynamically-loaded libraries, and are resolved by the OS. Even if the JVM has the right java.library.path, Mac OS will fail to resolve the dependency from libz3java to libz3. The other dependency, from libscalaz3 to libz3 is properly resolved because the dylib list the dependency as @loaderpath:

$ otool -L /tmp/../libscalaz3.dylib 
/tmp/../libscalaz3.dylib:
    /tmp/../libscalaz3.dylib (compatibility version 0.0.0, current version 0.0.0)
    /usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1252.0.0)
!!! @loader_path/libz3.dylib (compatibility version 0.0.0, current version 0.0.0)

Somebody knew something, because this is explicitly set in the Mac part of this build. But it's not done for libz3java.

The z3 java library, instead:

$ otool -L /tmp/../libz3java.dylib
/tmp/../libz3java.dylib:
    libz3java.dylib (compatibility version 0.0.0, current version 0.0.0)
    libz3.dylib (compatibility version 0.0.0, current version 0.0.0)
    /usr/lib/libc++.1.dylib (compatibility version 1.0.0, current version 400.9.0)
    /usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1252.0.0)

The workaround seems to be to install Z3 in a place that's part of DYLD_LIBRARY_PATH, though relying on this environment variable is discouraged for security reasons.

samarion commented 6 years ago

Would it be possible to set the @loaderpath in libz3java as well? I took a look at the generated Makefile and it seems that the targets for all are: shell, api_dll and java. Would decomposing the call to make into

make shell api_dll
install_name_tool -id @loader_path/libz3.dylib z3/z3-4.5.0/build/libz3.dylib
make java

set the @loader_path correctly for the java native interface?