mirror of
https://github.com/Z3Prover/z3
synced 2026-08-02 12:13:25 +00:00
5af999eb4f
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>
53 lines
2 KiB
Python
53 lines
2 KiB
Python
############################################
|
|
# 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()
|