pip install z3-solver: bad path or elf header

[zwimer]

In the newest release of the z3 pip package, I've run into what I think is a bug on both macOS and Linux.

On Linux:

In /lib there is libz3.so; this is the shared library, not a symlink. There are no other libs.
If you run readelf -a libz3.so | grep SONAME you will fine the output is:

 0x000000000000000e (SONAME)             Library soname: [libz3.so.4.8]

When I try to link to the library the link command succeeds but it when I try to run the linked binary it looks for libz3.so.4.8, which does not exist. On macOS this same thing happens.

For more details, here is my exact linking command:

[ 83%] Linking CXX executable backend-z3-solver.test
cd /claripy/native/build/tests/unit/backend/z3 && /venv/lib/python3.8/site-packages/cmake/data/bin/cmake -E cmake_link_script CMakeFiles/backend-z3-solver.test.dir/link.txt --verbose=1
/usr/bin/c++ -O2 -g -DNDEBUG CMakeFiles/backend-z3-solver.test.dir/solver.cpp.o -o backend-z3-solver.test  -Wl,-rpath,/claripy/native/build/tests/unit/testlib:/claripy/native/build:/venv/lib/python3.8/site-packages/z3/lib ../../../../../gmp/build/.libs/libgmp.a ../../testlib/libtestlib.so ../../../../libclaricpp.so ../../../../../gmp/build/.libs/libgmp.a /venv/lib/python3.8/site-packages/z3/lib/libz3.so -ldl

Specifically, that last line; as you can see it links to /venv/lib/python3.8/site-packages/z3/lib/libz3.so; as one would expect. Then running ldd on the resulting binary gives:

root@93638fc1d8d2:/claripy/native/build# ldd libclaricpp.so
	linux-vdso.so.1 (0x0000ffff8f616000)
	libc.so.6 => /lib/aarch64-linux-gnu/libc.so.6 (0x0000ffff8f41c000)
	/lib/ld-linux-aarch64.so.1 (0x0000ffff8f5e6000)
	libdw.so.1 => /lib/aarch64-linux-gnu/libdw.so.1 (0x0000ffff8f3b8000)
	libz3.so.4.8 => not found
	libstdc++.so.6 => /lib/aarch64-linux-gnu/libstdc++.so.6 (0x0000ffff8f1d3000)
	libgcc_s.so.1 => /lib/aarch64-linux-gnu/libgcc_s.so.1 (0x0000ffff8f1af000)
	libelf.so.1 => /lib/aarch64-linux-gnu/libelf.so.1 (0x0000ffff8f182000)
	libdl.so.2 => /lib/aarch64-linux-gnu/libdl.so.2 (0x0000ffff8f16e000)
	libz.so.1 => /lib/aarch64-linux-gnu/libz.so.1 (0x0000ffff8f144000)
	liblzma.so.5 => /lib/aarch64-linux-gnu/liblzma.so.5 (0x0000ffff8f110000)
	libbz2.so.1.0 => /lib/aarch64-linux-gnu/libbz2.so.1.0 (0x0000ffff8f0ef000)
	libm.so.6 => /lib/aarch64-linux-gnu/libm.so.6 (0x0000ffff8f045000)
	libpthread.so.0 => /lib/aarch64-linux-gnu/libpthread.so.0 (0x0000ffff8f015000)

As you can see in libz3.so.4.8 => not found, it is looking for a file that does not exist.

If I had to guess, either the soname should just be libz3.so or the library path should be libz3.so.4.8.

To validate this all, I tried replacing the string "libz3.so.4.8" with libz3.so.4.7" in the shared library and relinked it; the result was indeed that ldd gave libz3.so.4.7 => not found.

Also, on macOS the names are different slightly (libz3.4.8.dylib) where the numbers come before the extension; I'm not sure that is intentional or not

[zwimer]

Alternatively a symlink could be added perhaps. (Update: If the path is meant to be changed. Below I conclude it is probably an issue with the SONAME so this is moot in that case).

[zwimer]

This is on an M1, (linux is docker on M1).

[zwimer]

When I test from an x86 machine, pip install z3-solver does not need to build and readelf gives:

(z3) zwimer@thingy ~/.v/z/l/p/s/z/lib> readelf -a libz3.so| grep SONAME
 0x000000000000000e (SONAME)             Library soname: [libz3.so]

To verify the version, the pip install command gave: Successfully installed z3-solver-4.8.15.0

[zwimer]

I'm guessing the SONAME is being set improperly when pip install z3 builds on arm then, be that natively on apple silicon or within the VM that docker on mac creates.

[NikolajBjorner]

Is this only a problem with 4.15 or is this a problem with M1?

[zwimer]

I ran some tests using after doing pip install z3-solver==4.8.14.0:

Using readelf -a libz3.so | grep SONAME:
Linux Ubuntu 20.04 x86_64: libz3.so
Linux Ubuntu 20.04 virtualized on M1 arm64: libz3.so.4.8

Using grep libz3.so.4.8.dylib libz3.dylib
M1 macOS: contained the string libz3.so.4.8

Also possibly relevant on macOS: otool -L libz3.so gives:

libz3.dylib:
	@rpath/libz3.4.8.dylib (compatibility version 4.8.0, current version 4.8.14)
	/usr/lib/libc++.1.dylib (compatibility version 1.0.0, current version 1300.23.0)
	/usr/lib/libSystem.B.dylib (compatibility version 1.0.0, current version 1311.100.3)

I tried linking my program against the mac version and indeed it failed looking for the versioned name of the library.

Both arm packages had to build wheels (that is I had to apt install make and pip install cmake wheel as dependencies before pip installing the z3-solver version).

This seems to happen on M1 hardware, however it happens both on macOS and on the linux VM mac docker uses; therefore it is quite possible that the problem is on the arm64 architecture in general.

[NikolajBjorner]

So, given the M1 wave, it sounds like we need to release for arm64 on at least the mac pipeline.
This isn't done yet and can take some trial and error. The https://github.com/Z3Prover/z3/blob/master/scripts/nightly.yaml can be used to dry-run the arm version. Do you have bandwidth in this direction? There are already Arm64 pipelines/actions of various forms, but unlikely in the format that is useful for pip. There is a related request to have native arm64 binaries for M1. So far packaging "fat" binaries hasn't worked.

[zwimer]

I would agree with your statements, but I do not. In the meantime, while this is not a fix, it might be an acceptable patch if we were to add in a symlink. That is, under /lib you would have libz3.so and a symlink to it named libz3.so.4.8. This does not fix the underlying issue and will not work for all situations, but it will work in many. It might be worth considering as a quick temporary thing. This way when things look for libz3.so.4.8 in the /lib directory, they will find it and loaders typically respect symlinks.

Likewise, perhaps a 'dumb', temporary, simple way of having native arm64 binaries is the same thing currently done to support multiple distros. If you pip install z3 on ubuntu 20.04 on x86, you'll notice the wheel contains both an .so and a .dylib; that is you ship both the mac and linux so. Perhaps you could have libz3.arm.so and libz3.x86.so then just make a symlink to the right one based on arch.

The more correct way to do it, if there is bandwidth, is to create different wheels for different OS's and architectures. I believe pip and pypy support this, but it is not something I know how to do personally. For example, the cmake pypy wheels list different versions for different OS's, architectures, and other things.

[NikolajBjorner]

ouch. This is beyond something I know how to easily do so will take some time to deal with. A pedestrian attempt to create an ARM version for macos runs into some legacy issues so it is easily some days of on-off work fiddling with which build configuration works.

[zwimer]

As a very short-term stop-gap measure, may I suggest making the symlink? In a dockerfile I have for testing things I have these lines (since you obviously cannot rely on standard pip install z3-solver or permit packages that rely on z3 as a dependency to install z3 without this fix at the moment):

RUN pip3 install cmake # CMake (apt cmake is ancient) and z3 doesn't declare this as a pip dependency
RUN pip3 install wheel # Z3 fails to declare this as a dependency; TODO: PR a fix
# TODO: remove once Z3 fixes broken ELF header thing
RUN pip3 install z3-solver
RUN python3 -c 'import os, z3; lib=os.path.dirname(z3.__file__)+"/lib/libz3.so"; os.symlink(lib,lib+".4.8")'

All this does is functionally ln -s libz3.so libz3.so.4.8; obviously, you would want to also make the same type of symlink for mac, the .dylib. This is by no means a fix, but it might be a short-term stop-gap until this is properly fixed.

At the moment if you pip install X, and X depends on and links to z3, it will fail to run; this should temporarily fix it in some instances at least.

[zwimer]

I've made a PR that I think should do the symlink patch I mentioned above. It is not a fix, but it should alleviate the problem a bit until a fix is made. #5974

[NikolajBjorner]

The issue appears to be stale now that there is an ARM64 pip out.