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 "")