Bug#842892: java.lang.UnsatisfiedLinkError: libz3java.so: undefined symbol: Z3_solver_get_model
Followup-For: Bug #842892 Hi, I've just opened 2 PU requests to get this bug fixed in buster and stretch: https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=935576 https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=935581 Andreas
Bug#842892: java.lang.UnsatisfiedLinkError: libz3java.so: undefined symbol: Z3_solver_get_model
Followup-For: Bug #842892 Control: tag -1 patch Hi, the attached patch should fix the wrong SONAME of libz3java.so. Andreas
Bug#842892: java.lang.UnsatisfiedLinkError: libz3java.so: undefined symbol: Z3_solver_get_model
Followup-For: Bug #842892 now with patch ... >From fb80ab10200c149e9dbb9ff6c043646782111a67 Mon Sep 17 00:00:00 2001 From: Andreas Beckmann Date: Wed, 31 Jul 2019 09:53:48 +0200 Subject: [PATCH] do not set the SONAME of libz3java.so to libz3.so.4 --- debian/changelog | 6 ++ debian/rules | 5 +++-- 2 files changed, 9 insertions(+), 2 deletions(-) diff --git a/debian/changelog b/debian/changelog index 9704dca..b190092 100644 --- a/debian/changelog +++ b/debian/changelog @@ -1,3 +1,9 @@ +z3 (4.4.1-0.5~exp2) UNRELEASED; urgency=medium + + * Do not set the SONAME of libz3java.so to libz3.so.4. (Closes: #842892) + + -- Andreas Beckmann Wed, 31 Jul 2019 09:50:00 +0200 + z3 (4.4.1-0.5~exp1) experimental; urgency=medium * Package moved to salsa (Closes: #926939) diff --git a/debian/rules b/debian/rules index c951e0b..c5e9d4a 100755 --- a/debian/rules +++ b/debian/rules @@ -41,8 +41,8 @@ override_dh_auto_configure: else \ python scripts/mk_make.py --ml --prefix=$(CURDIR)/debian/tmp/usr; \ fi - sed -i 's/^SLINK_FLAGS=.*/SLINK_FLAGS=$(LDFLAGS) -Wl,-soname,libz3.so.4 -fPIC -shared/' build/config.mk - sed -i 's/^CXXFLAGS=/CXXFLAGS=-fPIC /' build/config.mk + sed -i 's/^SLINK_FLAGS=/SLINK_FLAGS=$$(LDFLAGS) -fPIC /' build/config.mk + echo 'libz3$$(SO_EXT): SLINK_FLAGS += -Wl,-soname,libz3.so.4' >> build/Makefile printf '%%:\n\t$$(MAKE) -C build $$@\n' > Makefile printf '\nall:\n\t$$(MAKE) -C build $$@\n' >> Makefile ln -s libz3.so build/libz3.dll @@ -51,6 +51,7 @@ override_dh_auto_configure: override_dh_clean: dh_clean + sed -i 's/^DOTNET_ENABLED=.*/DOTNET_ENABLED=False/' scripts/mk_util.py $(RM) Makefile scripts/*.pyc $(RM) -r build $(RM) src/api/python/*.pyc -- 2.11.0
Bug#842892: java.lang.UnsatisfiedLinkError: libz3java.so: undefined symbol: Z3_solver_get_model
Control: severity -1 grave It's frustrating to see a bug report being ignored for nearly three years. The severity is definitely release-crtical, because it renders this package (libz3-jni) unusable. PS: I tried to patchelf the .so file in question. The result, however, is ridiculous. $ sudo patchelf --set-soname "whatever" /usr/lib/x86_64-linux- gnu/jni/libz3java.so $ ldd /usr/lib/x86_64-linux-gnu/jni/libz3java.so linux-vdso.so.1 (0x7ffe4cd46000) XX => not found libstdc++.so.6 => /usr/lib/x86_64-linux-gnu/libstdc++.so.6 (0x7fb5d29ac000) libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x7fb5d2829000) libgcc_s.so.1 => /lib/x86_64-linux-gnu/libgcc_s.so.1 (0x7fb5d280f000) libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x7fb5d264e000) /lib64/ld-linux-x86-64.so.2 (0x7fb5d2bc2000) Well, at least you can turn to LD_PRELOAD instead of patchelf. If you are bit by this Debian-specific bug, stop here. Download the official binaries and simply set LD_LIBRARY_PATH, unless somebody fixes this bug, whose root cause is already known 3 years ago, thanks to Andrey. Let's hope the fix does not take another 3 years...
Bug#842892: java.lang.UnsatisfiedLinkError: libz3java.so: undefined symbol: Z3_solver_get_model
On Tue, Nov 01, 2016 at 11:00:29PM -0700, Ryan Tandy wrote: > It looks like the JNI library is not actually linked against libz3? > > $ ldd /usr/lib/x86_64-linux-gnu/jni/libz3java.so > linux-vdso.so.1 (0x7ffdc41e7000) > libstdc++.so.6 => /usr/lib/x86_64-linux-gnu/libstdc++.so.6 > (0x7fb61bcf5000) > libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x7fb61b9f1000) > libgcc_s.so.1 => /lib/x86_64-linux-gnu/libgcc_s.so.1 > (0x7fb61b7da000) > libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x7fb61b43c000) > /lib64/ld-linux-x86-64.so.2 (0x55c3b7a27000) It has "NEEDED libz3.so.4", but it also has "SONAME libz3.so.4" because of a line in rules that adds -soname,libz3.so.4 to the link commands for both libs (via SLINK_FLAGS). -- WBR, wRAR signature.asc Description: PGP signature
Bug#842892: java.lang.UnsatisfiedLinkError: libz3java.so: undefined symbol: Z3_solver_get_model
Package: libz3-jni
Version: 4.4.1-0.3
Severity: important
Dear Maintainer,
The Java example program included with z3 [1] fails to run.
With the package in unstable, the error reported is:
Exception in thread "main" java.lang.UnsatisfiedLinkError: no libz3java in
java.library.path
at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1867)
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:2286)
This is a misleading error (the correct library to load is "z3java", not
"libz3java"), caused by hiding an earlier exception [2].
I applied the following patch locally:
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -570,8 +570,9 @@
java_native.write(' public static native void
setInternalErrorHandler(long ctx);\n\n')
java_native.write(' static {\n')
-java_native.write('try { System.loadLibrary("z3java"); }\n')
-java_native.write('catch (UnsatisfiedLinkError ex) {
System.loadLibrary("libz3java"); }\n')
+java_native.write('System.loadLibrary("z3java");\n')
+#java_native.write('try { System.loadLibrary("z3java"); }\n')
+#java_native.write('catch (UnsatisfiedLinkError ex) {
System.loadLibrary("libz3java"); }\n')
java_native.write(' }\n')
java_native.write('\n')
With the try-catch removed, the actual exception is revealed:
Exception in thread "main" java.lang.UnsatisfiedLinkError:
/usr/lib/x86_64-linux-gnu/jni/libz3java.so:
/usr/lib/x86_64-linux-gnu/jni/libz3java.so: undefined symbol:
Z3_solver_get_model
at java.lang.ClassLoader$NativeLibrary.load(Native Method)
at java.lang.ClassLoader.loadLibrary0(ClassLoader.java:1941)
at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1857)
at java.lang.Runtime.loadLibrary0(Runtime.java:870)
at java.lang.System.loadLibrary(System.java:1122)
at com.microsoft.z3.Native.(Native.java:13)
at com.microsoft.z3.Global.ToggleWarningMessages(Global.java:86)
at JavaExample.main(JavaExample.java:2286)
I confirmed that libz3 does in fact export the symbol in question:
$ nm -gD /usr/lib/x86_64-linux-gnu/libz3.so | grep Z3_solver_get_model
000a6220 T Z3_solver_get_model
It looks like the JNI library is not actually linked against libz3?
$ ldd /usr/lib/x86_64-linux-gnu/jni/libz3java.so
linux-vdso.so.1 (0x7ffdc41e7000)
libstdc++.so.6 => /usr/lib/x86_64-linux-gnu/libstdc++.so.6
(0x7fb61bcf5000)
libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x7fb61b9f1000)
libgcc_s.so.1 => /lib/x86_64-linux-gnu/libgcc_s.so.1
(0x7fb61b7da000)
libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x7fb61b43c000)
/lib64/ld-linux-x86-64.so.2 (0x55c3b7a27000)
[1] http://sources.debian.net/src/z3/4.4.1-0.3/examples/java/JavaExample.java/
[2] http://sources.debian.net/src/z3/4.4.1-0.3/scripts/update_api.py/#L574
thanks,
Ryan
-- System Information:
Debian Release: 8.6
APT prefers stable-updates
APT policy: (500, 'stable-updates'), (500, 'proposed-updates'), (500,
'stable')
Architecture: amd64 (x86_64)
Foreign Architectures: i386
Kernel: Linux 4.7.0-0.bpo.1-amd64 (SMP w/2 CPU cores)
Locale: LANG=en_CA.UTF-8, LC_CTYPE=en_CA.UTF-8 (charmap=UTF-8)
Shell: /bin/sh linked to /bin/dash
Init: systemd (via /run/systemd/system)
