From 5af999eb4f6738ffe6adeeebc387f9d0f79b53c5 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Wed, 29 Jul 2026 14:01:55 -0700 Subject: [PATCH] Load versioned libz3 soname in Python bindings on Linux (#10290) The generated Python bindings loaded `libz3.so` without a soversion, which could bind to an ABI-incompatible shared library when multiple Z3 versions are present. This change makes Linux bindings prefer the versioned soname while leaving other platforms on the existing lookup path. - **Python loader generation** - Thread a `z3py_soversion` parameter through `scripts/update_api.py`. - Generate `_lib_name` as `libz3.so..` on Linux, and keep `libz3.` elsewhere. - Reuse `_lib_name` consistently for directory probing, system fallback, and error messages. - **Build-system wiring** - Pass the current `SOVERSION` from the CMake Python bindings build on Linux. - Pass the same value through the `mk_make`/`mk_util.py` generation path so both build systems emit the same loader behavior. - **In-tree Python bindings layout** - Add the matching `libz3.so..` link in `build/python/` on Linux so the generated bindings work directly from the build tree. - **Regression coverage** - Add a focused script-level test for the generated loader preamble to check: - Linux uses the versioned soname when provided. - Non-versioned fallback remains available when no soversion is supplied. Example of the generated Linux loader behavior: ```python _sover = '5.0' _ext = 'so' _lib_name = 'libz3.%s.%s' % (_ext, _sover) if sys.platform.startswith('linux') and _sover else 'libz3.%s' % _ext _lib = ctypes.CDLL(_lib_name) ``` - Fixes #7518 --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> Co-authored-by: Nikolaj Bjorner --- scripts/mk_util.py | 1 + scripts/tests/test_update_api.py | 53 ++++++++++++++++++++++++++ scripts/update_api.py | 65 +++++++++++++++++++++----------- src/api/python/CMakeLists.txt | 19 ++++++++++ 4 files changed, 116 insertions(+), 22 deletions(-) create mode 100644 scripts/tests/test_update_api.py diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 89d82303a1..6da1090aac 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -3160,6 +3160,7 @@ def mk_bindings(api_files): update_api.generate_files(api_files=new_api_files, api_output_dir=get_component('api').src_dir, z3py_output_dir=get_z3py_dir(), + z3py_soversion=f"{VER_MAJOR}.{VER_MINOR}" if is_linux() else None, dotnet_output_dir=dotnet_output_dir, java_input_dir=java_input_dir, java_output_dir=java_output_dir, diff --git a/scripts/tests/test_update_api.py b/scripts/tests/test_update_api.py new file mode 100644 index 0000000000..eeaaa5e879 --- /dev/null +++ b/scripts/tests/test_update_api.py @@ -0,0 +1,53 @@ +############################################ +# Copyright (c) 2026 Microsoft Corporation +# +# Unit tests for z3core.py library loading generation. +############################################ +import io +import os +import sys +import unittest + +# Add the scripts directory to the path so we can import update_api +_SCRIPTS_DIR = os.path.dirname(os.path.dirname(os.path.abspath(__file__))) +if _SCRIPTS_DIR not in sys.path: + sys.path.insert(0, _SCRIPTS_DIR) + +import update_api + +class TestZ3PyLibraryLoading(unittest.TestCase): + def _render_preamble(self, soversion): + buf = io.StringIO() + update_api.write_core_py_preamble(buf, soversion) + update_api.write_core_py_post(buf) + return buf.getvalue() + + def test_linux_loader_uses_soversion_when_available(self): + text = self._render_preamble("5.0") + self.assertIn("_sover = '5.0'", text) + self.assertIn("sys.platform.startswith('linux') and _sover", text) + # Should have a fallback list with both versioned and unversioned names + self.assertIn("_lib_names", text) + self.assertIn("del _lib_names", text) + self.assertIn('raise Z3Exception("%s not found." % _lib_name)', text) + + def test_linux_loader_falls_back_to_unversioned(self): + text = self._render_preamble("5.0") + # The loader should try multiple names (versioned + unversioned fallback) + self.assertIn("for _name in _lib_names:", text) + self.assertIn("d = os.path.join(d, _name)", text) + self.assertIn("_lib = ctypes.CDLL(_name)", text) + + def test_loader_falls_back_to_unsuffixed_name_without_soversion(self): + text = self._render_preamble(None) + self.assertIn("_sover = None", text) + self.assertIn( + "_lib_name = 'libz3.%s.%s' % (_ext, _sover) if sys.platform.startswith('linux') and _sover else 'libz3.%s' % _ext", + text, + ) + self.assertIn("del _lib_name", text) + self.assertIn("del _sover", text) + + +if __name__ == '__main__': + unittest.main() diff --git a/scripts/update_api.py b/scripts/update_api.py index b539165a39..c0831e2dbe 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1849,12 +1849,15 @@ def write_core_py_post(core_py): core_py.write(""" # Clean up del _lib +del _lib_name +del _lib_names del _default_dirs del _all_dirs del _ext +del _sover """) -def write_core_py_preamble(core_py): +def write_core_py_preamble(core_py, z3py_soversion=None): core_py.write( """ # Automatically generated file @@ -1871,7 +1874,14 @@ from .z3consts import * _file_manager = contextlib.ExitStack() atexit.register(_file_manager.close) +""") + core_py.write(f"_sover = {z3py_soversion!r}\n") + core_py.write( +""" _ext = 'dll' if sys.platform in ('win32', 'cygwin') else 'dylib' if sys.platform == 'darwin' else 'so' +_lib_name = 'libz3.%s.%s' % (_ext, _sover) if sys.platform.startswith('linux') and _sover else 'libz3.%s' % _ext +# On Linux with a soversion, also try the unversioned name as a fallback (e.g. build directories) +_lib_names = ['libz3.%s.%s' % (_ext, _sover), 'libz3.%s' % _ext] if sys.platform.startswith('linux') and _sover else ['libz3.%s' % _ext] _lib = None _z3_lib_resource = importlib_resources.files('z3').joinpath('lib') _z3_lib_resource_path = _file_manager.enter_context( @@ -1902,39 +1912,44 @@ for v in ('Z3_LIBRARY_PATH', 'PATH', 'PYTHONPATH'): _all_dirs.extend(lds) _failures = [] -for d in _all_dirs: - try: - d = os.path.realpath(d) - if os.path.isdir(d): - d = os.path.join(d, 'libz3.%s' % _ext) - if os.path.isfile(d): - _lib = ctypes.CDLL(d) - break - except Exception as e: - _failures += [e] - pass +for _name in _lib_names: + for d in _all_dirs: + try: + d = os.path.realpath(d) + if os.path.isdir(d): + d = os.path.join(d, _name) + if os.path.isfile(d): + _lib = ctypes.CDLL(d) + break + except Exception as e: + _failures += [e] + pass + if _lib is not None: + break if _lib is None: # If all else failed, ask the system to find it. - try: - _lib = ctypes.CDLL('libz3.%s' % _ext) - except Exception as e: - _failures += [e] - pass + for _name in _lib_names: + try: + _lib = ctypes.CDLL(_name) + break + except Exception as e: + _failures += [e] + pass if _lib is None: - print("Could not find libz3.%s; consider adding the directory containing it to" % _ext) + print("Could not find %s; consider adding the directory containing it to" % ' or '.join(_lib_names)) print(" - your system's PATH environment variable,") print(" - the Z3_LIBRARY_PATH environment variable, or ") print(" - to the custom Z3_LIB_DIRS Python-builtin before importing the z3 module, e.g. via") if sys.version < '3': print(" import __builtin__") - print(" __builtin__.Z3_LIB_DIRS = [ '/path/to/z3/lib/dir' ] # directory containing libz3.%s" % _ext) + print(" __builtin__.Z3_LIB_DIRS = [ '/path/to/z3/lib/dir' ] # directory containing %s" % _lib_name) else: print(" import builtins") - print(" builtins.Z3_LIB_DIRS = [ '/path/to/z3/lib/dir' ] # directory containing libz3.%s" % _ext) + print(" builtins.Z3_LIB_DIRS = [ '/path/to/z3/lib/dir' ] # directory containing %s" % _lib_name) print(_failures) - raise Z3Exception("libz3.%s not found." % _ext) + raise Z3Exception("%s not found." % _lib_name) if sys.version < '3': @@ -2000,6 +2015,7 @@ core_py = None def generate_files(api_files, api_output_dir=None, z3py_output_dir=None, + z3py_soversion=None, dotnet_output_dir=None, java_input_dir=None, java_output_dir=None, @@ -2057,7 +2073,7 @@ def generate_files(api_files, write_log_h_preamble(log_h) write_log_c_preamble(log_c) write_exe_c_preamble(exe_c) - write_core_py_preamble(core_py) + write_core_py_preamble(core_py, z3py_soversion) # FIXME: these functions are awful apiTypes.def_Types(api_files) @@ -2100,6 +2116,10 @@ def main(args): dest="z3py_output_dir", default=None, help="Directory to emit z3py files. If not specified no files are emitted.") + parser.add_argument("--z3py-soversion", + dest="z3py_soversion", + default=None, + help="SOVERSION for loading libz3 on supported platforms.") parser.add_argument("--dotnet-output-dir", dest="dotnet_output_dir", default=None, @@ -2147,6 +2167,7 @@ def main(args): generate_files(api_files=pargs.api_files, api_output_dir=pargs.api_output_dir, z3py_output_dir=pargs.z3py_output_dir, + z3py_soversion=pargs.z3py_soversion, dotnet_output_dir=pargs.dotnet_output_dir, java_input_dir=pargs.java_input_dir, java_output_dir=pargs.java_output_dir, diff --git a/src/api/python/CMakeLists.txt b/src/api/python/CMakeLists.txt index 2d08d2cd61..2dc30fa8ba 100644 --- a/src/api/python/CMakeLists.txt +++ b/src/api/python/CMakeLists.txt @@ -20,6 +20,13 @@ set(z3py_bindings_build_dest "${PROJECT_BINARY_DIR}/python") file(MAKE_DIRECTORY "${z3py_bindings_build_dest}") file(MAKE_DIRECTORY "${z3py_bindings_build_dest}/z3") +set(z3py_soversion_args "") +if (CMAKE_SYSTEM_NAME STREQUAL "Linux") + set(z3py_soversion_args + "--z3py-soversion" + "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}") +endif() + set(build_z3_python_bindings_target_depends "") foreach (z3py_file ${z3py_files}) add_custom_command(OUTPUT "${z3py_bindings_build_dest}/${z3py_file}" @@ -37,6 +44,7 @@ add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3/z3core.py" COMMAND "${Python3_EXECUTABLE}" "${PROJECT_SOURCE_DIR}/scripts/update_api.py" ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} + ${z3py_soversion_args} "--z3py-output-dir" "${z3py_bindings_build_dest}" DEPENDS @@ -93,6 +101,17 @@ if (TARGET libz3) DEPENDS ${LIBZ3_DEPENDS} COMMENT "Linking libz3 into python directory" ) + if (CMAKE_SYSTEM_NAME STREQUAL "Linux") + add_custom_command(OUTPUT "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}.${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}" + COMMAND "${CMAKE_COMMAND}" "-E" "${LINK_COMMAND}" + "${LIBZ3_SOURCE_PATH}" + "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}.${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}" + DEPENDS ${LIBZ3_DEPENDS} + COMMENT "Linking versioned libz3 into python directory" + ) + list(APPEND build_z3_python_bindings_target_depends + "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}.${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}") + endif() else() message(FATAL_ERROR "libz3 target not found. Cannot build Python bindings.") endif()