mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-01 19:54:04 +00:00
Code Activity

Load versioned libz3 soname in Python bindings on Linux (#10290)

Browse source 
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.<major>.<minor>` on Linux, and keep
`libz3.<ext>` 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.<major>.<minor>` 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)
```

<!-- START COPILOT CODING AGENT SUFFIX -->

- 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 <nikolaj@cs.stanford.edu>
This commit is contained in:
Copilot 2026-07-29 14:01:55 -07:00 • committed by GitHub
parent 3631d1b85c
commit 5af999eb4f
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 116 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

1
scripts/mk_util.py
View file

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

53
scripts/tests/test_update_api.py Normal file
View file

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

65
scripts/update_api.py
View file

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

19
src/api/python/CMakeLists.txt
View file

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