Experimental mechanism for loading Z3 dynamically at runtime.

[ekpyron]

Ok, so this is as close as we will get.
The "static" binary built by the b_ubu_static CI here now dynamically loads Z3 - it's available as CI artifact (https://531866-40892817-gh.circle-artifacts.com/0/solc). [Link doesn't seem to work]

The resulting binary is in fact slightly (but insignificantly) smaller than the previous static build. However, it's not entirely static anymore:

$ ldd /tmp/solc
        linux-vdso.so.1 (0x00007ffebdbf2000)
        libdl.so.2 => /usr/lib/libdl.so.2 (0x00007f0ff38c7000)
        libm.so.6 => /usr/lib/libm.so.6 (0x00007f0ff3781000)
        libc.so.6 => /usr/lib/libc.so.6 (0x00007f0ff35b8000)
        /lib64/ld-linux-x86-64.so.2 => /usr/lib64/ld-linux-x86-64.so.2 (0x00007f0ff43e3000)

I was strongly arguing for trying to achive entirely static binaries before today, but ;-)... all what remains here libdl.so, libm.so and libc.so are all part of glibc. The binary should work as is against any glibc>=2.14 (released 2011). Some further minor trickery could even make it compatible down to glibc>=2.4 (released 2006) - beyond that it might be a hassle. Newer versions of glibc released in the future can reasonably be expected to stay compatible basically forever.

So this is not entirely what we wanted, but I'm not sure it's all too bad.

The reason for entirely static linking not being possible is the fact that Z3 uses some thread-local storage variables and thread-local storage inherently depends on the dynamic linker and seems to work fundamentally different between static and dynamic linking - and to me it doesn't look like there is any workaround for that.

The PR is of course still draft, so not much sense to review the details, it's rather meant as proof-of-concept - e.g. we won't pull in the actual Z3 headers, but make them compile-time-only dependencies and also the CMake options need some refinement (e.g. errors for trying to do any of this on non-linux systems), etc.
On the other hand, note that there are hardly any changes to the existing code - the only real change is adding Z3Interface::available(), the rest is entirely transparent.

Apart from all that, all tests were passed with this kind of linking and there is no noticable performance loss.

So yeah, opinions anyone :-)?
@leonardoalt @chriseth @axic @cameel ?

[ekpyron]

By the way: IMHO these are just beautiful :-D... resp. C++17 is for allowing me to do this.

[ekpyron]

The mechanism is by the way pretty fool-proof. If any of these entry points were to result in an incompatible signature: compile-time error in the reinterpret_cast (ambiguous overloads in decltype). If any of them are missing: link-time error: undefined reference. As weird as it may look, I can't imagine what could go wrong with it :-).

[leonardoalt]

This is actually nice.
I'm wondering whether it not being entirely static anymore has any drawbacks

[ekpyron]

This is actually nice.
I'm wondering whether it not being entirely static anymore has any drawbacks

The drawbacks I can think of are:

• If anyone tries to run the binary on a more-than-a-decade-old linux distribution, they won't work. As mentioned above, without modification the binary should start working from systems ~2011 - the oldest ubuntu docker image I found is 14.10 and the binary immediately works there.
• If out of the blue glibc decided to introduce the first real forward-incompatible change since 1997 (actually I think there's even compatibility wrappers for even older ones), then the binaries will stop working.
• Exotic embedded systems that don't come with glibc, but an embedded variant may have issues. But those are used to having to rebuild everything anyways because of it.

So there are downsides, but I'm not sure they are all that horrible. Am I missing any?

[leonardoalt]

I think those are fine, especially because we would see them before releasing (well, 1 we know statically, so this is more related to 2)

[ekpyron]

The thing is rather that old historic binaries would stop working with 2 and we'd have to rebuild them. But I'd be surprised if 2 happened without any compatibility wrapper as long as x86_64 lives...

[chriseth]

The linked binary segfaults for me (when I use smt). Also I get

> ldd solc
	not a dynamic executable

[ekpyron]

The CircleCI link seems to point somewhere weird - maybe better to fetch it from the b_ubu_static CI run itself. I'll strike it out in the description.

[chriseth]

Ah nice! That one seems to work with z3, but if I move libz3.so out of the way, I get the following

> ./solc /tmp/x.sol 
Unknown exception during compilation: unknown

[leonardoalt]

Oh that's weird, without z3 I get

Unknown exception during compilation: Attempted to use dynamically loaded Z3, even though it is not available.
Segmentation fault (core dumped)

[ekpyron]

With the latest commit, Z3 being absent should work as expected.

[cameel]

Am I missing any?

Alpine, probably. Though I'm not sure - it has musl by default but maybe it's possible to install glibc there too if you need it?

I tried it in Docker and I am getting errors. Here's how to reproduce.

Get the container and executables

mkdir /tmp/alpine/
cd /tmp/alpine/
docker pull alpine
curl -OL https://github.com/ethereum/solidity/releases/download/v0.7.5/solc-static-linux
curl -L https://532552-40892817-gh.circle-artifacts.com/0/solc --output solc-dynamic
chmod +x solc-static-linux solc-dynamic

Static build of 0.7.5

docker run -it --rm --volume /tmp/alpine:/tmp/ alpine ldd /tmp/solc-static-linux
docker run -it --rm --volume /tmp/alpine:/tmp/ alpine /tmp/solc-static-linux --version

Output:

/lib/ld-musl-x86_64.so.1: /tmp/solc-static-linux: Not a valid dynamic program

solc, the solidity compiler commandline interface
Version: 0.7.5+commit.eb77ed08.Linux.g++

Dynamic builds from this PR

docker run -it --rm --volume /tmp/alpine:/tmp/ alpine /tmp/solc-dynamic --version
docker run -it --rm --volume /tmp/alpine:/tmp/ alpine ldd /tmp/solc-dynamic

Output:

standard_init_linux.go:219: exec user process caused: no such file or directory

        /lib64/ld-linux-x86-64.so.2 (0x7f75f634d000)
        libdl.so.2 => /lib64/ld-linux-x86-64.so.2 (0x7f75f634d000)
        libm.so.6 => /lib64/ld-linux-x86-64.so.2 (0x7f75f634d000)
        libc.so.6 => /lib64/ld-linux-x86-64.so.2 (0x7f75f634d000)
Error loading shared library ld-linux-x86-64.so.2: No such file or directory (needed by /tmp/solc-dynamic)
Error relocating /tmp/solc-dynamic: __vsnprintf_chk: symbol not found
Error relocating /tmp/solc-dynamic: __memcpy_chk: symbol not found
Error relocating /tmp/solc-dynamic: __memset_chk: symbol not found
Error relocating /tmp/solc-dynamic: __memmove_chk: symbol not found
Error relocating /tmp/solc-dynamic: dlmopen: symbol not found
Error relocating /tmp/solc-dynamic: __snprintf_chk: symbol not found
Error relocating /tmp/solc-dynamic: __sprintf_chk: symbol not found
Error relocating /tmp/solc-dynamic: __strftime_l: symbol not found

[ekpyron]

Of that I'm aware, that's expected - alpine linux falls under "exotic embedded systems" in #10483 (comment) ;-).

[cameel]

With the latest commit, Z3 being absent should work as expected.

The one I downloaded from most recent run of b_ubu_static (finished ~6h ago) segfaults on Arch Linux without Z3:

sudo pacman -Rsc z3 --noconfirm
./solc-dynamic test/libsolidity/smtCheckerTests/bmc_coverage/assert.sol

Segmentation fault (core dumped)

Works when Z3 is installed.

[cameel]

Is it that exotic though? We've been still using it for building not that long ago. And I generally use it for containers if I can get away with it because it's very lightweight.

[ekpyron]

Yes, it is :-). At least thinking of it as a distribution that you run, download software into and expect that to run. And it was also rather exotic that we built it in those before :-). And in general a container like that is expected to build it's own stuff and can't expect anything to just work in it. If we continue to build a docker image (do we still do that?), then that'll be a different build. So to me at least this seems to be of rather limited concern in general.

Let me look at the segfaulting thing, I probably messed something up in the force pushes...

Ah wait

[leonardoalt]

Still need to bump cmake and docs?

[ekpyron]

Still need to bump cmake and docs?

Curious - I was sure I bumped the docs as well earlier, but apparently I was imagining that or it was somehow lost again. Pushed it now.

[leonardoalt]

It would probably be good to have more approvals before merging

[cameel]

@ekpyron Sorry for not getting back to you on this today. Too many meetings + stuff happening around external repos. It's a bit late now so I'll re-review it tomorrow.

[ekpyron]

@ekpyron Sorry for not getting back to you on this today. Too many meetings + stuff happening around external repos. It's a bit late now so I'll re-review it tomorrow.

No worries ;-)!

[cameel]

A few more general things. I don't see any issues with the dynamic linking mechanism itself. If it works, it's fine and better than permanently not having Z3.

[ekpyron]

Also needed to rebase.

[ekpyron]

If you guys approve, give me a chance to squash before merging :-)!

[leonardoalt]

LGTM. Please squash and ping to reapprove

[cameel]

Looks fine to me now.

I'd still prefer to have a proper template rather than a Python-C++ hybrid (#10483 (comment)) but it's a very peripheral part of the PR so I approve anyway.

[ekpyron]

Looks fine to me now.

I'd still prefer to have a proper template rather than a Python-C++ hybrid (#10483 (comment)) but it's a very peripheral part of the PR so I approve anyway.

Alright - I also simultanously just squashed it (ping @leonardoalt).

And yeah, I see the point about the template, but to me it still seems nicer to have everything in one file - it's not like it's exceedingly complex python logic there, and this way you don't need to switch files to get an idea of what's going to be generated there... but yeah, thanks for approving it like this contrary to your preference then ;-).