Merge d3f5fd6825 into bed73a3f43

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

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
     # ------------------------------------------------------------------

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

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