Make sure Z3 binary does not depend on GLIBC >= 2.11

[cheshire]

Otherwise it does not work on Ubuntu 10.04.

[cheshire]

@kfriedberger Do you think you could expand on how our hack with versions.c is working, and how to apply it to Z3?

Also it's been a year since 10.04 official support was stopped, so should the comment really say 12.04? And does it have the same issue?

[kfriedberger]

I do not exactly know, how and why our solution with versions.c works. But I am in favor of removing this part, as Ubuntu 10.04 is quite outdated. Some computers in our VerifierCloud have used the old library of libc, but they might also have been updated last year and perhaps are working with a newer libc now.

I would suggest to remove the special handling and possibly re-add it later, if a user really complains about it.

[cheshire]

@kfriedberger Do you know the requirements for the other LTS which is still supported (namely, 12.04)?

[kfriedberger]

For Ubuntu 12.04 the libc-version 2.15 should be default. Source: http://packages.ubuntu.com/de/precise/libc-bin

[PhilippWendler]

The version of libc on all currently supported Ubuntu versions can be seen here: http://packages.ubuntu.com/search?keywords=libc6&searchon=names&exact=1&suite=all&section=all

For Debian, the link is http://packages.debian.org/search?keywords=libc6&searchon=names&exact=1&suite=all&section=all

However, we do not need to wait until "a user really complains about it" because I as a user did so already in January in a mail to @cheshire. Some machines where we want to run Z3 (HPI) do not have a current glibc, so we need the memcpy workaround.

How the workaround works and which steps are necessary to apply it to some library is documented.

[cheshire]

Hi Philipp,

We have indeed discussed this before, but from what I remember there were two reasons: old Ubuntu versions, AND an HPI cluster. Hence I've decided to re-visit it, seeing as one reason has went away.

As for the second reason, what are the upgrade timelines on HPI cluster? If it would upgrade e.g. within a year I personally would prefer to keep the "normal" Z3 rather than fidling with memcpy versions and creating technical debt. I would like to avoid a situation that our Z3 would behave differently to the official Z3. Even if two memcpy versions have same performance, using a different binary can introduce some unwanted change in behavior.

On Fri, Apr 1, 2016 at 9:20 AM, Philipp Wendler notifications@github.com wrote:

The version of libc on all currently supported Ubuntu versions can be seen here: http://packages.ubuntu.com/search?keywords=libc6&searchon=names&exact=1&suite=all&section=all

For Debian, the link is http://packages.debian.org/search?keywords=libc6&searchon=names&exact=1&suite=all&section=all

However, we do not need to wait until "a user really complains about it" because I as a user did so already in January in a mail to @cheshire https://github.com/cheshire. Some machines where we want to run Z3 (HPI) do not have a current glibc, so we need the memcpy workaround.

How the workaround works and which steps are necessary to apply it to some library is documented https://github.com/sosy-lab/java-smt/blob/master/lib/native/source/libmathsat5j/compile.sh#L36 .

— You are receiving this because you were mentioned. Reply to this email directly or view it on GitHub https://github.com/sosy-lab/java-smt/issues/31#issuecomment-204283628

[PhilippWendler]

what are the upgrade timelines on HPI cluster?

There are no upgrade timelines. They are using a version of SuSE Linux Enterprise Server that has regular support until 2019 and extended support until 2022. They might upgrade before that, but I would not hope for it (in fact, they did some major maintenance that involved upgrades a few months ago, but did not upgrade to the latest major release that would have had a newer glibc).

We have no chance of influencing their upgrade timeline for everything that influences anything else (they did not even upgrade Python for me).

The existing solution for memcpy works without maintenance effort since 2012 for MathSAT, a time where this solver was the default for CPAchecker and thus heavily used and tested. Any visible difference in behavior between old and new memcpy would be a bug in Z3, and would also occur for everybody that simply compiles Z3 on a system with older glibc.

Thus I think the effort spent for this and the potential problems are outweighed by the benefits. Note that this may not only affect us, but also other users with old Debian or other enterprise distributions.

Are there even official binaries of Z3 that we would use otherwise? I think so far we have always compiled Z3 ourselves anyway.

[cheshire]

Ok you are right, let's use that trick. On Apr 4, 2016 18:18, "Philipp Wendler" notifications@github.com wrote:

what are the upgrade timelines on HPI cluster?

There are no upgrade timelines. They are using a version of SuSE Linux Enterprise Server that has regular support until 2019 and extended support until 2022. They might upgrade before that, but I would not hope for it (in fact, they did some major maintenance that involved upgrades a few months ago, but did not upgrade to the latest major release that would have had a newer glibc).

We have no chance of influencing their upgrade timeline for everything that influences anything else (they did not even upgrade Python for me).

The existing solution for memcpy works without maintenance effort since 2012 for MathSAT, a time where this solver was the default for CPAchecker and thus heavily used and tested. Any visible difference in behavior between old and new memcpy would be a bug in Z3, and would also occur for everybody that simply compiles Z3 on a system with older glibc.

Thus I think the effort spent for this and the potential problems are outweighed by the benefits. Note that this may not only affect us, but also other users with old Debian or other enterprise distributions.

Are there even official binaries of Z3 that we would use otherwise? I think so far we have always compiled Z3 ourselves anyway.

— You are receiving this because you were mentioned. Reply to this email directly or view it on GitHub https://github.com/sosy-lab/java-smt/issues/31#issuecomment-205373419

[cheshire]

I've managed to make a trick work on the produced binary (libz3j.so) locally.

The problem with the supplied binaries remains though (libz3.so and now also libz3java.so). We can merge them into one binary, like done in Mathsat, but that loses a very nice property that a user can use their version of Z3 by just replacing the libz3.so file. @PhilippWendler Is your suggestion to merge all the files into one anyway?

[PhilippWendler]

If you can make it work for libz3j.so, why does this not work for libz3.so?

Keeping the three files separate is nice because then we do not have two copies of the rather large Z3 code. If it is not possible otherwise we could merge them, but I see no reason. If merging Z3 + memcpy_wrapper + JNI wrapper in one file works, then surely merging Z3 + memcpy_wrapper in one file should also be doable, right?

[cheshire]

@PhilippWendler Of course it should work, but I'm not sure how. For libz3j.so, I apply the wrapping to the object file, and now I can't figure out an interface to apply the wrapping to the shared object. I want a command to do versions.o + libz3.so -> wrapped_libz3.so, yet playing with LDD options haven't yielded wanted results yet.

[cheshire]

Funny enough ld -L. -lz3 -shared --wrap=memcpy --output=blah.so works, but dynamically links to libz3.so, defeating the whole point of not having files depending on certain GLIBC. For some reason adding -Bstatic kills it: ld -Bstatic -L. -lz3 -shared --wrap=memcpy --output=blah.so dies with "ld: cannot find -lz3".

[cheshire]

Right so it's worse than I've thought, shared objects cannot be linked dynamically.

The wrapping works for libz3j.so because I am creating it. It works for Mathsat as it contains a statically linked .a file. There's a tool called 'statifier' which can create "pseudo-static" libraries, but it's not even in Ubuntu repos, making automatic ANT job troublesome.

[PhilippWendler]

Why not simply compile Z3 as static library and then link it?

[cheshire]

@PhilippWendler yeah that's what I'm doing now, however for some reason the command line gcc -Wall -g -o blah2.so -shared -Wl,-soname,blah2.so versions.o -L. -Wl,-Bstatic -lz3 -Wl,-Bdynamic -lc -lm -lstdc++ -Wl,--wrap=memcpy creates nearly empty file blah2.so, which only takes 12KB.

[cheshire]

Strangely I was able to do create a shared object which combines libz3j.so and libz3.so, yet it complaints about OpenMP (should we link it statically like we do for GMP in MathSAT?).

With this approach we lose the ability to let user substitute the shared object themselves, which is IMO important.

[cheshire]

@PhilippWendler From my understanding, Java requires a shared object for JNI bindings. If we rely on a static archive file, we would require a compilation step, which would make a drag-and-drop substitution impossible. Being able to substitute a shared object without recompilation to me is considerably more important than compatibility with older systems, as it allows a JavaSMT user to use whatever Z3 version they wish. So unless you have a suggestion how to do the wrapping which would take a shared object as an input, and produce a shared object as an output, I'm tempted to close this ticket as wontfix.

Moreover, eventually I plan to switch to bindings provided by Z3Java (only the Native class as a drop-in replacement for NativeLibraries), and to drop the compilation step altogether, and if we do wrapping we would have to keep compilation just to do that.

[PhilippWendler]

Of course we cannot use a static library of Z3 for JNI, nor should we require users to supply a static library of Z3.

However, that does not mean that we cannot use a static version of Z3 during the building of our binary, just like we do it for MathSAT.

Again in full detail, what I propose is:

• Compile static Z3.
• Link static Z3 + memcpy-wrapper into dynamic libz3.so.
• Compile dynamic libz3j.so (with memcpy-wrapper if necessary).
• Compile dynamic libz3java.so (with memcpy-wrapper if necessary).

This can be easily encapsulated in a script.

Users who want to use their own Z3 still can take a dynamic libz3.so and use it with no extra compilation, I never proposed to change this.

I do not expect that we can drop compilation completely anyway. So far we have always compiled Z3 because it is necessary to get a recent version. The same is true for Princess and SMTInterpol, where we also do not rely on the official binaries because they are updated too rarely for us.

[cheshire]

@PhilippWendler OK, this is doable.

I do not expect that we can drop compilation completely anyway

I've meant the compilation step of our bindings, not the compilation of Z3 (which ANT does not do anyway).

Are we sure that only memcpy should be wrapped? Currently after repeating the steps from Mathsat5 on Z3 archive I still get a library which depends on GLIBC_2.17.

Namely:

gcc -Wall -g -o blah2.so -shared -Wl,-soname,blah2.so versions.o -L. -Wl,-Bstatic,--whole-archive -lz3 -Wl,-Bdynamic,--no-whole-archive -lc -lm -lstdc++ -Wl,--wrap=memcpy

And doing

objdump -p blah2.so | grep -A50 "required from"

gives me:

  required from libgcc_s.so.1:
    0x0b792650 0x00 14 GCC_3.0
  required from ld-linux-x86-64.so.2:
    0x0d696913 0x00 13 GLIBC_2.3
  required from libc.so.6:
    0x06969197 0x00 11 GLIBC_2.17
    0x09691972 0x00 10 GLIBC_2.3.2
    0x0d696914 0x00 09 GLIBC_2.4
    0x09691974 0x00 08 GLIBC_2.3.4
    0x09691a75 0x00 05 GLIBC_2.2.5
  required from libstdc++.so.6:
    0x0bafd171 0x00 15 CXXABI_1.3.1
    0x0297f861 0x00 12 GLIBCXX_3.4.11
    0x02297f89 0x00 07 GLIBCXX_3.4.9
    0x0297f865 0x00 06 GLIBCXX_3.4.15
    0x056bafd3 0x00 04 CXXABI_1.3
    0x08922974 0x00 03 GLIBCXX_3.4
  required from libm.so.6:
    0x09691a75 0x00 02 GLIBC_2.2.5

[PhilippWendler]

Are we sure that only memcpy should be wrapped? Currently after repeating the steps from Mathsat5 on Z3 archive I still get a library which depends on GLIBC_2.17.

This can well be. So far memcpy was the only function that we saw in practice which needs to be wrapped, but it may well happen for others, too, if new glibc versions introduce new binary incompatibilities. You can do objdump -t libz3.so |grep GLIBC_2.17 to find all respective symbols that need to be wrapped.

[cheshire]

@PhilippWendler OK so the culprit was clock_gettime, which was moved to GLIBC starting from 2.17. Simply linking with -lrt before -lc solves the problem.

Before we open champagne, what are the version requirements on libstdc++? The current shared object depends on GLIBCXX_3.4.15.

[PhilippWendler]

GLIBCXX_3.4.15 seems to be fine.

Ubuntu 12.04 has GLIBCXX_3.4.16, Debian oldstable has GLIBCXX_3.4.17, and HPI even has GLIBCXX_3.4.21.

[cheshire]

@PhilippWendler OK what about OpenMP? I would prefer to keep it. We can disable it altogether as well.

[cheshire]

Also, the current script supports Cygwin. I am not going to be able to spend effort on testing the solution under Cygwin, so I propose dropping the support unless someone else is willing to volunteer to test it (especially since MathSAT does not support Cygwin either). @stahlbauer ?

[cheshire]

Finally, why the existing commands for both MathSAT and Z3 add debugging information with -g flag just to get rid of it later using strip?