Trouble with Z3 on OCaml 4.10 on Linux and OCaml 4.x on macOS

I’m having trouble getting a project to work using Z3. The project, KMT uses the Z3 SMT solver to generate Kleene algebras with tests (KATs) and decide equivalences between them.

Some configurations work fine, others don’t.

  • On my own computer, macOS 10.13.6, my project works with OCaml 4.07 and 4.10 just fine.
  • On Travis’s Linux build, my project works with OCaml 4.07, 4.08, and 4.09 just fine.
  • On Travis’s Linux build, my project fails in 4.10 with an error related to caml_local_roots (see below).
  • On Travis’s macOS build, my project fails in 4.07 through 4.10 with a missing libz3.dylib.

I suspect these are totally different issues. There’s also a third issue, perhaps related, perhaps not: with Z3 breaking on versions higher than 4.8.1. I’m only using 4.8.1 in my project, though.

Linux and OCaml 4.10

Here’s the build error, excerpted from my CI log.

$ opam config exec -- dune build src/main.exe
(cd _build/default && /home/travis/.opam/ocaml-base-compiler.4.10.0/bin/ocamlopt.opt -thread -cclib -lstdc++ -g -o src/main.exe /home/travis/.opam/ocaml-base-compiler.4.10.0/lib/ocaml/nums.cmxa -I /home/travis/.opam/ocaml-base-compiler.4.10.0/lib/ocaml /home/travis/.opam/ocaml-base-compiler.4.10.0/lib/z3/z3ml.cmxa -I /home/travis/.opam/ocaml-base-compiler.4.10.0/lib/z3 /home/travis/.opam/ocaml-base-compiler.4.10.0/lib/ocaml/unix.cmxa -I /home/travis/.opam/ocaml-base-compiler.4.10.0/lib/ocaml /home/travis/.opam/ocaml-base-compiler.4.10.0/lib/ocaml/bigarray.cmxa -I /home/travis/.opam/ocaml-base-compiler.4.10.0/lib/ocaml /home/travis/.opam/ocaml-base-compiler.4.10.0/lib/ocaml/str.cmxa -I /home/travis/.opam/ocaml-base-compiler.4.10.0/lib/ocaml /home/travis/.opam/ocaml-base-compiler.4.10.0/lib/ocaml/threads/threads.cmxa -I /home/travis/.opam/ocaml-base-compiler.4.10.0/lib/ocaml /home/travis/.opam/ocaml-base-compiler.4.10.0/lib/batteries/batteries.cmxa /home/travis/.opam/ocaml-base-compiler.4.10.0/lib/batteries/batteriesThread.cmxa /home/travis/.opam/ocaml-base-compiler.4.10.0/lib/ANSITerminal/ANSITerminal.cmxa -I /home/travis/.opam/ocaml-base-compiler.4.10.0/lib/ANSITerminal /home/travis/.opam/ocaml-base-compiler.4.10.0/lib/stdlib-shims/stdlib_shims.cmxa /home/travis/.opam/ocaml-base-compiler.4.10.0/lib/fmt/fmt.cmxa /home/travis/.opam/ocaml-base-compiler.4.10.0/lib/cmdliner/cmdliner.cmxa /home/travis/.opam/ocaml-base-compiler.4.10.0/lib/fmt/fmt_cli.cmxa /home/travis/.opam/ocaml-base-compiler.4.10.0/lib/fmt/fmt_tty.cmxa /home/travis/.opam/ocaml-base-compiler.4.10.0/lib/astring/astring.cmxa /home/travis/.opam/ocaml-base-compiler.4.10.0/lib/uuidm/uuidm.cmxa /home/travis/.opam/ocaml-base-compiler.4.10.0/lib/re/re.cmxa /home/travis/.opam/ocaml-base-compiler.4.10.0/lib/alcotest/alcotest.cmxa /home/travis/.opam/ocaml-base-compiler.4.10.0/lib/logs/logs.cmxa /home/travis/.opam/ocaml-base-compiler.4.10.0/lib/logs/logs_fmt.cmxa /home/travis/.opam/ocaml-base-compiler.4.10.0/lib/logs/logs_cli.cmxa /home/travis/.opam/ocaml-base-compiler.4.10.0/lib/result/result.cmxa /home/travis/.opam/ocaml-base-compiler.4.10.0/lib/ppx_deriving/runtime/ppx_deriving_runtime.cmxa src/kmt.cmxa src/.main.eobjs/native/main.cmx)
/home/travis/.opam/ocaml-base-compiler.4.10.0/lib/z3/libz3ml.a(z3native_stubs.o): In function `n_context_of_ast':
z3native_stubs.c:(.text+0x133a): undefined reference to `caml_local_roots'
/home/travis/.opam/ocaml-base-compiler.4.10.0/lib/z3/libz3ml.a(z3native_stubs.o): In function `n_mk_null_ast':
z3native_stubs.c:(.text+0x142a): undefined reference to `caml_local_roots'
/home/travis/.opam/ocaml-base-compiler.4.10.0/lib/z3/libz3ml.a(z3native_stubs.o): In function `n_context_of_symbol':
z3native_stubs.c:(.text+0x153a): undefined reference to `caml_local_roots'
/home/travis/.opam/ocaml-base-compiler.4.10.0/lib/z3/libz3ml.a(z3native_stubs.o): In function `n_mk_null_symbol':
z3native_stubs.c:(.text+0x162a): undefined reference to `caml_local_roots'
/home/travis/.opam/ocaml-base-compiler.4.10.0/lib/z3/libz3ml.a(z3native_stubs.o): In function `n_context_of_constructor':
z3native_stubs.c:(.text+0x173a): undefined reference to `caml_local_roots'
/home/travis/.opam/ocaml-base-compiler.4.10.0/lib/z3/libz3ml.a(z3native_stubs.o):z3native_stubs.c:(.text+0x182a): more undefined references to `caml_local_roots' follow
collect2: error: ld returned 1 exit status

File "caml_startup", line 1:
Error: Error during linking

My understanding is that OCaml 4.10 changed caml_local_roots to be a macro referring to Caml_state_field(local_roots). My guess at what’s going wrong is that Z3 is somehow using older headers (maybe from the system ocaml?). I’m not certain how to figure this out, though, since I’m installing Z3 from OPAM. (Which, you would think, would make sure that the right headers got found.) Thoughts?

macOS and libz3.dylib (resolved, but not to my satisfaction)

On the macOS builds, libz3.dylib isn’t found. Here’s the build error, excerpted from my CI log:

$ opam config exec -- dune exec src/test_equivalence.exe
dyld: Library not loaded: libz3.dylib
  Referenced from: /Users/travis/build/mgree/kmt/_build/default/src/test_equivalence.exe
  Reason: image not found
/Users/travis/.travis/functions: line 109: 48960 Abort trap: 6           opam config exec -- dune exec src/test_equivalence.exe
The command "opam config exec -- dune exec src/test_equivalence.exe" exited with 134.

I’ve found a temporary but unsatisfactory solution: setting DYLD_LIBRARY_PATH or, preferably, DYLD_FALLBACK_LIBRARY_PATH. (Apparently the latter plays better with correctly configured executables.)

An ideal solution here wouldn’t require environment variables for my executables to run. I can see two ways forward here:

  1. Change the Z3 OPAM file to use -install_name correctly when building libz3.dylib.
  2. Change my build to use install_name_tool when generating Z3-linked executables on macOS.

The first option seems better—it should fix things for more people—but the second has the advantage of being local.

Update 1: I’ve got the basics working, though not particularly nicely. I’m not certain of the right way to accomplish executable post-processing in dune. Currently I have:

(rule
 (target kmt)
 (enabled_if (= %{ocaml-config:system} macosx))
 (deps main.exe)
 (action (progn
           (copy main.exe %{target})
           (run install_name_tool -change libz3.dylib "%{lib:z3:libz3.dylib}" %{target}))))

(rule
 (target kmt)
 (enabled_if (<> %{ocaml-config:system} macosx))
 (deps main.exe)
 (action (copy main.exe %{target})))

Doing so allows me to drop the DYLD_FALLBACK_LIBRARY_PATH variable setting, but then I have to munge every executable—including tests! (Here’s a CI log showing success for munged and failure for unmunged executables.) Is there a better way to do this? How do you postprocess an executable in dune? While I need the copy command to generate the correctly named kmt executable, it’d be great to be able to skip the copying (and verbose rules).

Maybe post an issue on their tracker on github.

So far as I can tell, there is no GitHub repo for the z3 OPAM package, which is separately maintained from Z3 itself. I’m in touch with Simon Cruanes, the maintainer. (There is a fork of opam-repository that contains the PRs for Z3, but it has many PRs for other packages, too.) Is this forum an inappropriate venue?

The current status (per CI logs) is that OCaml 4.10 doesn’t work with any version of z3 on Linux, but OCaml 4.10 works fine on z3 >= 4.8.4 for macOS.

I don’t know how long it will take to get the z3 OPAM package in deployable shape (i.e., install w/o need for environment variables), so I’m still interested in:

  • Advice for how to debug the caml_local_roots issue in the Z3 bindings.
  • Local solutions for clients of the library. I have a tentative solution (post-processing), though I’d appreciate feedback/help with a better way to post-process executables in dune.

The Z3 package seems to build fine on the opam-heallth-check CI?

Indeed! But building the library doesn’t mean you can use the library.

One of the core issues here is that OPAM only lets you test before install, but not after. I’ve submitted an issue that would allow for post-install tests, though I don’t think it’s implemented yet.

1 Like

I can finally make my project work with Z3 4.8.7 rather than 4.8.1 on OCaml 4.09.0.
For everything executables in dune file, I add (link_flags -cc g++), and then it works. I don’t need to modify ANY_PATH either compiling or executing it.

When working with z3.4.8.1 before, I need to modify LD_LIBRARY_PATH when executing a compiled binary.

p.s. for me there is just one breaking API to fix: Big_int -> Big_int_Z due to the latest z3 depends on Zarith.

Neat! I can try to adopt my canary.

Shouldn’t the Z3 package itself be setting those link flags? Isn’t that the point of META file in the first place? :confused:

Even if it will, it won’t work for project built with dune, since dune doesn’t respect these flags in META files. See this SO answer for more details, you may also find this answer relevant.

1 Like

I have read and upvoted your answers before.

For this one, the direct solution works for me

ocamlfind ocamlmktop -thread -custom -linkpkg -package z3 -o z3top

However, I cannot make the dune version answer in the post. For dune 2.5.1, utop 2.5.0 and OCaml 4.10.0,

(executable
 (name z3utop)
 (link_flags -linkall -custom -cclib -lstdc++)
 (libraries utop z3))

Building with this dune file gets error message

File "dune", line 2, characters 7-13:
2 |  (name z3utop)
           ^^^^^^
Error: File unavailable:
/home/exx/.opam/4.10.0+flambda/lib/ocaml/compiler-libs/ocamltoplevel.cmxa
File "dune", line 2, characters 7-13:
2 |  (name z3utop)
           ^^^^^^
Error: File unavailable: /home/exx/.opam/4.10.0+flambda/lib/utop/uTop.a
File "dune", line 2, characters 7-13:
2 |  (name z3utop)
           ^^^^^^
Error: File unavailable: /home/exx/.opam/4.10.0+flambda/lib/utop/uTop.cmxa
File "_none_", line 1:
Warning 58: no cmx file was found in path for module UTop_main, and its interface was not compiled with -opaque

EDIT: this works. the error message won’t show so I delete it.
If I add a (modes byte) as dune doc suggests, it works.
I don’t figure it out for some time. Then I found this dune issue on GitHub and it works magically.

1 Like

Didn’t you forget to create the z3utop.ml file? It shall have the following contents

let () = UTop_main.main ()

Oh, I do have z3utop.ml.

I re-check the experiment and find that adding (modes byte) to dune file in your answer works. Without this, the error message is showed as my previous post.

1 Like

I see. It used to work without the (modes byte) stanza. I’ve updated the answer.

I’ve proposed a PR to z3 that will fix the building process of the z3 libraries, so that it won’t require passing any additional options (like C++) and, most importantly, enable z3 in the default runtime (so there is no need anymore for building custom runtimes, and z3 could be used in utop or Jupyter Notebooks). See the PR message for the detailed information. I will also make a PR to opam-repository with the same patch so that we can benefit from correctly built bindings more or less immediately (without having to wait for z3 release, technically, we can backport this patch to all recent version of z3).

6 Likes

Thanks a lot for this! This has been a long standing issue that I wanted to fix years ago, but didn’t know how to. I’m surprised the patch is so short (even tho, as you pointed out, it’s not simple :p)

1 Like

Yep, I was also thinking about fixing it for the last six years (we used to use z3 before it became open-source), but yesterday I got really angry and finally pinned it to the wall. My next desire is to make the bindings work with the system installation of z3. A smaller wish is to at least install the z3 binary to opam’s bin folder, so that I don’t have to install the system one, if I need the z3 binary.

1 Like

OK, the PR to the upstream is merged, the PR to the opam-repository is pending (I’ve also added the installation of the z3 binary, so now after opam install z3 you can run z3 without installing the system z3. Once the PR is merged, of course.

For those who want to use it right now, just add my repo (it is currently syncronized with master but will diverge quite soon, so don’t forget to remove it once the PR to the main OCaml repository is merged).

opam repo add ivg git@github.com:ivg/opam-repository.git
3 Likes

Six years is a long time. I suffered from this just for one year. The reason that I replied 2 MONTHS LATER is I am more or less tired of the manual fix of the path problem and seeking a solution to this problem. I had never thought it could be solved with a descriptive explanation in the pull request of z3 before the post and the solution seems so simple.

2 Likes