From d3f5fd68253063c918e81490664f5cb95d287ba4 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 17 Mar 2026 13:59:37 -1000 Subject: [PATCH] Fix Java UnsatisfiedLinkError on macOS (#7640) On macOS, libz3java.dylib was built without an rpath to find libz3.dylib in the same directory. When Java loaded the JNI library, the dynamic linker could not resolve the libz3 dependency, causing UnsatisfiedLinkError. Three fixes: - mk_util.py: add -Wl,-rpath,@loader_path to the macOS JNI link command - CMakeLists.txt: set MACOSX_RPATH, BUILD_RPATH, INSTALL_RPATH for z3java target; remove duplicate headerpad block - update_api.py: improve Native.java error message to show the root cause from both load attempts instead of only the fallback error Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- scripts/mk_util.py | 3 +++ scripts/tests/test_jni_arch_flags.py | 39 ++++++++++++++++++++++++++++ scripts/update_api.py | 11 +++++++- src/api/java/CMakeLists.txt | 13 +++++----- 4 files changed, 59 insertions(+), 7 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 67a2fca63..63da04755 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1919,6 +1919,9 @@ class JavaDLLComponent(Component): if IS_WINDOWS: # On Windows, CL creates a .lib file to link against. out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(LIB_EXT)\n' % os.path.join('api', 'java', 'Native')) + elif IS_OSX: + out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT) -Wl,-rpath,@loader_path $(SLINK_EXTRA_FLAGS)\n' % + os.path.join('api', 'java', 'Native')) else: out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT) $(SLINK_EXTRA_FLAGS)\n' % os.path.join('api', 'java', 'Native')) diff --git a/scripts/tests/test_jni_arch_flags.py b/scripts/tests/test_jni_arch_flags.py index 2796b156d..e60285eec 100644 --- a/scripts/tests/test_jni_arch_flags.py +++ b/scripts/tests/test_jni_arch_flags.py @@ -208,6 +208,45 @@ class TestJNIArchitectureFlagsInMakefile(unittest.TestCase): "(the import library)", ) + # ------------------------------------------------------------------ + # Tests for macOS rpath, so libz3java.dylib can find libz3.dylib + # ------------------------------------------------------------------ + + def test_macos_uses_loader_path_rpath(self): + """ + On macOS, the JNI link command must include -Wl,-rpath,@loader_path + so that libz3java.dylib can find libz3.dylib in the same directory + at runtime. Without this, Java fails with UnsatisfiedLinkError. + """ + comp = self._make_java_dll_component() + text = self._generate_makefile( + comp, is_windows=False, is_osx=True, is_arch_arm64=True + ) + link_lines = self._find_jni_link_lines(text) + self.assertTrue(link_lines, "Expected at least one JNI link line") + for line in link_lines: + self.assertIn( + '-Wl,-rpath,@loader_path', line, + "macOS JNI link command must set rpath to @loader_path " + "so libz3java.dylib finds libz3.dylib at runtime", + ) + + def test_linux_does_not_use_loader_path(self): + """ + On Linux, @loader_path is a macOS concept and must not appear. + """ + comp = self._make_java_dll_component() + text = self._generate_makefile( + comp, is_windows=False, is_osx=False, is_arch_arm64=False + ) + link_lines = self._find_jni_link_lines(text) + self.assertTrue(link_lines, "Expected at least one JNI link line") + for line in link_lines: + self.assertNotIn( + '@loader_path', line, + "@loader_path is macOS-specific and must not appear on Linux", + ) + # ------------------------------------------------------------------ # Consistency check: SLINK_EXTRA_FLAGS in mk_config for cross-compile # ------------------------------------------------------------------ diff --git a/scripts/update_api.py b/scripts/update_api.py index df80da116..b539165a3 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -631,7 +631,16 @@ def mk_java(java_src, java_dir, package_name): java_native.write(' try {\n') java_native.write(' System.loadLibrary("z3java");\n') java_native.write(' } catch (UnsatisfiedLinkError ex) {\n') - java_native.write(' System.loadLibrary("libz3java");\n') + java_native.write(' try {\n') + java_native.write(' System.loadLibrary("libz3java");\n') + java_native.write(' } catch (UnsatisfiedLinkError ex2) {\n') + java_native.write(' throw new UnsatisfiedLinkError(\n') + java_native.write(' "Failed to load z3java native library. "\n') + java_native.write(' + "Tried z3java: " + ex.getMessage() + "; "\n') + java_native.write(' + "Tried libz3java: " + ex2.getMessage() + ". "\n') + java_native.write(' + "Make sure both the JNI library and libz3 are in java.library.path "\n') + java_native.write(' + "or set DYLD_LIBRARY_PATH (macOS) / LD_LIBRARY_PATH (Linux).");\n') + java_native.write(' }\n') java_native.write(' }\n') java_native.write(' }\n') java_native.write(' }\n') diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt index 194b25232..774a293bc 100644 --- a/src/api/java/CMakeLists.txt +++ b/src/api/java/CMakeLists.txt @@ -48,17 +48,18 @@ target_include_directories(z3java PRIVATE "${PROJECT_BINARY_DIR}/src/api" ${JNI_INCLUDE_DIRS} ) -# Add header padding for macOS to allow install_name_tool to modify the dylib +# On macOS, set rpath so libz3java.dylib can find libz3.dylib in the same directory, +# and add header padding to allow install_name_tool to modify the dylib. if (CMAKE_SYSTEM_NAME STREQUAL "Darwin") + set_target_properties(z3java PROPERTIES + MACOSX_RPATH TRUE + INSTALL_RPATH "@loader_path" + BUILD_RPATH "@loader_path" + ) target_link_options(z3java PRIVATE "-Wl,-headerpad_max_install_names") endif() # FIXME: Should this library have SONAME and VERSION set? -# On macOS, add headerpad for install_name_tool compatibility -if(CMAKE_SYSTEM_NAME STREQUAL "Darwin") - target_link_options(z3java PRIVATE "-Wl,-headerpad_max_install_names") -endif() - # This prevents CMake from automatically defining ``z3java_EXPORTS`` set_property(TARGET z3java PROPERTY DEFINE_SYMBOL "")