Search code examples
ocamllinker-errorsz3opam

Linker error when installing Z3 OCaml bindings in local Opam environment

I'm compiling Z3 with OCaml from sources using the following (standard) command from within the Z3 source directory:

> python scripts/mk_make.py --prefix=$OPAM_SWITCH_PREFIX --ml

Then building and installing from within the build/ directory.

Then running

> utop

and

> #require "z3";;

gives me the following error:

Cannot load required shared library dllz3ml. Reason: /home/foobar/.opam/my_opam/lib/stublibs/dllz3ml.so: undefined symbol: Z3_rcf_del.

I'm confused about how to debug these kinds of errors. Are there any suggestions for identifying the problem, and how to fix it?

Solution

  • The problem indicates that the missing symbol is not provided by the objects that constitute the OCaml z3 bindings and that it is not a part of the runtime. The verdict, you can't use the OCaml z3 bindings in the OCaml toplevel with the default runtime (i.e., with the ocaml or utop applications). Well, at least in the current state of the z3 bindings.

    First of all, since you've asked, here are some tips on debugging such issues. Not sure whether they will help in the general case, but this would be the steps that I will take, for starters. First of all, I will double-check that the symbol is indeed undefined (sometimes it is just mangled, or versioned, or having wrong ABI), 

    nm /home/ivg/.opam/4.07.0/lib/z3/dllz3ml.so | grep Z3_rcf_del
             U Z3_rcf_del

    Ok, so it is indeed undefined, this is an easy case. The next step requires some intuition, we have to find a library that provides this symbol. On a hunch, let's look into all the libraries in the z3 OCaml package, 

    nm /home/ivg/.opam/4.07.0/lib/z3/libz3.so |  grep Z3_rcf_del
000000000011d6d0 t _Z14log_Z3_rcf_delP11_Z3_contextP11_Z3_rcf_num
000000000009f4c0 t _Z15exec_Z3_rcf_delR11z3_replayer
00000000000e1950 T Z3_rcf_del

    Yep, here it is, sitting quietly in the text section. One more question is... why it is then unresolved is answered by ldd:

    ldd /home/ivg/.opam/4.07.0/lib/z3/dllz3ml.so
    linux-vdso.so.1 =>  (0x00007ffd96b71000)
    libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007f72a900f000)
    /lib64/ld-linux-x86-64.so.2 (0x00007f72a9640000)

    which indicates that dllz3ml.so has no dependencies beyond libc. Neither z3 itself nor even libc++ or libcxx. That's all, we can't move forward, the library is broken. Probably, it is intentional, as if we will look into the cma file, we will find the following

    ocamlobjinfo `ocamlfind query z3`/z3ml.cma  | head -n5
File /home/ivg/.opam/4.07.0/lib/z3/z3ml.cma
Force custom: no
Extra C object files: -lz3ml -lz3-static -fopenmp -lrt
Extra C options:
Extra dynamically-loaded libraries: -lz3ml

    And indeed, the Z3_rcf_del symbol is provided by z3-static. But we can't benefit from this in the toplevel, since libz3-static.a is a static archive, which we obviously can't load in runtime.

    In general, you can build a custom runtime, using ocamlmktop, which will link z3 and this is probably what maintainers expect us to do.

    A probably better solution would be to pack the OCaml z3 library in a such way that it could be loaded into the OCaml vanilla toplevel. That requires linking all dependencies and creating a self-contained z3.cma (and z3.cmxs) which could be loaded in runtime without any extra system dependencies).

    Some directions on fixing the upstream

    I remember the same problem was with the native version, which I had fixed (so probably I should also fix the bytecode version at that time), here is the patch. The idea is to extend this patch to the bytecode part - we should add the -linkall option to the place where z3ml.cma file is created (probably it is here).

    Easy and dirty solution

    As I've mentioned before you can just create your custom runtime with all external primitives included, e.g.,

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

    Now you can start it with

     ./z3top -I `ocamlfind query z3`

    (yep, you still need to pass the -I option, the runtime linked only the implementation, but not the cmi files), and now let's check that it works,

    $ ./z3top -I `ocamlfind query z3`
        OCaml version 4.07.0

# Z3.Version.full_version;;
- : string = "Z3 4.8.4.0"
#

    Building a custom utop toplevel using dune

    Building a utop enhanced toplevel with z3 is a little bit convoluted, so it is better to rely on some build system automation, so let's use dune for that. Create a dune file with the following contents

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

    then create the z3utop.ml file with the following contents

      let () = UTop_main.main ()

    Now it could be built with

      dune build z3utop.bc

    and run with

      ./_build/default/z3utop.bc -I `ocamlfind query z3`