mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-14 16:25:11 +00:00
Code Activity

Merge d3f5fd6825 into 477a1d817d

Browse source
This commit is contained in:
Lev Nachmanson 2026-04-06 10:29:54 +02:00 • committed by GitHub
commit 056237fd28
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 59 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

3
scripts/mk_util.py
View file

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

39
scripts/tests/test_jni_arch_flags.py
View file

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

11
scripts/update_api.py
View file

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

13
src/api/java/CMakeLists.txt
View file

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