z3: dynamic loading, dual copies, and wheel-vs-editable divergence

[Marco-Christiani]

z3: dynamic loading, dual copies, and wheel-vs-editable divergence

Companion to the broader dependency audit in issue #2; this one zooms in on z3 because its situation is load-bearing at runtime.

For wheel installs of mirage-project, I believe two different libz3.so files end up loaded in the same Python process:

1. the user's site-packages copy from z3-solver, loaded by python/mirage/__init__.py via ctypes.CDLL(lib_path), which uses the default RTLD_LOCAL mode on POSIX;
2. a hash-suffixed copy bundled into mirage_project.libs/ by auditwheel, loaded by the Cython extension via its RPATH.

Both are on disk, both are loaded into memory, they are not guaranteed to be the same version, and the wheel build does not fail if they differ.

Editable installs (pip install -e .) do not go through auditwheel, so in dev the Cython extension links against the user's z3-solver directly via the path setup.py pulled from z3.__file__ at build time. This is a different code path than what end users get from the wheel, meaning developers do not exercise the bundled-plus-preloaded configuration they ship to users.

Four roles z3-solver plays in one build

The dual-loading above is a consequence of how z3-solver is used at every stage. In one build it is simultaneously:

• a build dependency: setup.py does import z3; z3_path = path.dirname(z3.__file__) and passes that path to CMake (-DZ3_LIBRARIES=.../libz3.so) and to the Cython extension's library_dirs + libraries=["z3"];
• a runtime dependency: listed in requirements.txt as z3-solver==4.16, installed into the user's environment by pip;
• a dynamic link target: the C++ code and the Cython extension both link against libz3.so at build time, producing a DT_NEEDED entry in the resulting shared object;
• bundled retroactively by auditwheel: the repaired wheel contains mirage_project.libs/libz3-<hash>.so.4.16, with the Cython extension's RPATH rewritten to $ORIGIN/../mirage_project.libs.

A bare pip install mirage-project does not enforce that the runtime z3-solver is byte-identical to the one the wheel was built against, and no PyPI metadata mechanism enforces this.

Runtime behavior

Load order. python/mirage/__init__.py runs ctypes.CDLL("<site-packages>/z3/lib/libz3.so") with the default mode, which is RTLD_LOCAL on POSIX. The symbols from this load are not visible to the dynamic linker's global lookup. Then from .core import ... triggers dlopen of core.cpython-<tag>.so, whose DT_NEEDED list contains libz3-<hash>.so.4.16. The extension resolves that through RPATH $ORIGIN/../mirage_project.libs, which is the auditwheel-bundled copy. Both libz3 files are now resident in the same process, different inodes, different hash suffixes, potentially different versions of z3.

What currently keeps this safe. RTLD_LOCAL isolates the two namespaces, so the extension cannot accidentally call into a mismatched z3 via global symbol resolution. No state is crossed between the Python z3 module and the C++ extension at runtime; the extension uses its own linked z3 for all C++-side work, and the Python module is not consulted for anything the extension does. Version drift between build-time and runtime z3 is silent rather than fatal.

Failure modes. A future change that shares state across the boundary (for example, passing a Z3_solver handle across the Python/C++ FFI) would immediately hit version-mismatch UB. A future auditwheel or manylinux policy change could alter how the bundled copy is found, and the preload would not compensate. The wheel-vs-editable divergence means bugs that only manifest in the wheel path do not appear in dev; "works on main, broken in the published wheel" is a likely failure mode. And the number of places a z3 version has to be edited in lockstep (see issue #678) makes drift the default outcome of any version bump.

Also observed: because the ctypes preload is RTLD_LOCAL, it does not make libz3 symbols available to the extension. The extension resolves its symbols entirely through its own RPATH against the bundled copy. The preload is effectively just an early file-existence check against the runtime dependency, and would raise ImportError only if z3-solver is uninstalled.

Proposed fix

z3. Static-link z3 into the C++/Cython extension. Consequences:

• No libz3.so in the wheel bundle. auditwheel stops copying it.
• DT_NEEDED no longer names libz3. The extension's symbol resolution is self-contained.
• The ctypes.CDLL preload in __init__.py becomes a no-op and can be removed.
• z3-solver can stay as a runtime Python dependency for callers that want the Python module; the C++ side is independent of that install.
• No more version mismatch between build-time and runtime z3, because there is no runtime z3 from the C++ side's perspective.

This is the shortest path to eliminating every symptom in this issue.

libcudart. Same class of issue. setup.py passes libraries=["cudart_static", "cudart", ...] to the Cython extension, causing it to dual-link static and dynamic cudart. The dynamic DT_NEEDED is (I believe) what causes auditwheel to bundle libcudart into the wheel. The Cython extension is not the only site that links cudart dynamically: CMakeLists.txt also appends the shared CUDA_CUDART_LIBRARY (resolved via find_library to libcudart.so) to MIRAGE_LINK_LIBS in cmake/cuda.cmake and CMakeLists.txt, so the main C++ library also carries a cudart DT_NEEDED entry. Any static-link fix therefore needs to cover both the setup.py dual-link and the CMake link, not just the Python-visible side. I believe the fix remains small but I need to check it is not load-bearing elsewhere (for example, other CMake targets or examples that assume a shared cudart is present).

Open questions for maintainers

• Was the ctypes.CDLL preload load-bearing at some point, or did it accrete as a workaround for something that has since been fixed? If there is an original reason for its existence, the static-link proposal may need to accommodate it.
• Is there any plan or active use that requires libz3.so to be dynamically shareable between the C++ extension and the Python z3 module (for example, passing handles across the FFI)? If so, static linking is the wrong fix and we need a different approach (likely: bundle z3, drop the preload, fix RPATH to point at z3-solver's copy).
• Any licensing constraint that would make static-linking z3 or cudart preferable or non-preferable? I believe z3's MIT license is permissive here and CUDA toolkit components permit static linking in the context of redistributable wheels, but I would want that confirmed by whoever owns the release licensing decision before acting on this proposal.

Scope. This issue asks for the architectural fix. The pin-management symptoms (many places z3 appears, version drift between them) are tracked in the broader audit issue #2 and can be cleaned up independently.