search

creusot-rs / creusot

Creusot helps you prove your code is correct in an automated fashion.
GNU Lesser General Public License v2.1
1.12k stars 50 forks source link

Better detection of available libraries #1138

Open Lysxia opened 1 day ago

Lysxia commented 1 day ago

creusot setup downloads the Z3 binary from the official release on github, which depends on glibc 2.32, 2.33, or 2.34 (see error message below). WSL by default installs Ubuntu 20.04 which is admittedly pretty old, and which only has glibc 2.31. So the Z3 binary can't run without more tweaks.

I think it's really the fault of WSL and Ubuntu for being old but there could still be a way to handle this kind of situation on our side better than downloading a binary that won't run.

$ ~/.local/share/creusot/bin/z3
/home/sam/.local/share/creusot/bin/z3: /lib/x86_64-linux-gnu/libc.so.6: version `GLIBC_2.34' not found (required by /home/sam/.local/share/creusot/bin/z3)
/home/sam/.local/share/creusot/bin/z3: /lib/x86_64-linux-gnu/libc.so.6: version `GLIBC_2.32' not found (required by /home/sam/.local/share/creusot/bin/z3)
/home/sam/.local/share/creusot/bin/z3: /lib/x86_64-linux-gnu/libc.so.6: version `GLIBC_2.33' not found (required by /home/sam/.local/share/creusot/bin/z3)
/home/sam/.local/share/creusot/bin/z3: /lib/x86_64-linux-gnu/libstdc++.so.6: version `GLIBCXX_3.4.30' not found (required by /home/sam/.local/share/creusot/bin/z3)
/home/sam/.local/share/creusot/bin/z3: /lib/x86_64-linux-gnu/libstdc++.so.6: version `GLIBCXX_3.4.29' not found (required by /home/sam/.local/share/creusot/bin/z3)
jhjourdan commented 1 day ago

Isn't Z3 Microsoft software? Isn't Windows Microsoft's operating system?

jhjourdan commented 1 day ago

I guess the solution is to ship our own Z3 version which depends on Glibc 2.31?

Armael commented 1 day ago

Building Z3 ourselves could be a solution indeed (either on an old-enough ubuntu, or statically linking everything using musl with alpine). Alternatively, as a low effort hack, I wonder if we could apply polyfill-glibc on the binaries shipped by Z3 (and host the result somewhere for creusot setup to download). But in the long run, shipping a musl static build might be better...

jhjourdan commented 1 day ago

One thing I am slightly worried about is that we need to get convinced that these linking hack do not alter the performances of Z3. That's not a big problem for Why3 or Creusot, because they are not performance critical (or are they?).