在本地Opam环境中安装Z3 OCaml绑定时出现链接器错误

问题表明组成OCaml z3绑定的对象未提供缺少的符号，并且它不是运行时的一部分。结论是，您不能在具有默认运行时的OCaml顶层中使用OCaml z3绑定（即，使用ocaml或utop应用程序）。好吧，至少在z3绑定的当前状态下。

首先，按照您的要求，这里有一些调试此类问题的技巧。不确定它们在一般情况下是否会有所帮助，但是对于初学者来说，这就是我将要采取的步骤。首先，我将仔细检查该符号确实是未定义的（有时它只是被修饰，版本化或具有错误的ABI），

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

好的，这确实是不确定的，这是一个简单的例子。下一步需要一些直觉，我们必须找到一个提供此符号的库。直觉，让我们看一下z3 OCaml软件包中的所有库，

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

是的，这里是安静地坐在文本部分。另一个问题是...为什么无法解决，请回答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)

这表明dllz3ml.so除libc之外没有其他依赖项。z3本身甚至libc ++或libcxx都没有。仅此而已，我们无法前进，库已损坏。可能是有意的，好像我们要查看cma文件一样，我们将找到以下内容

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

实际上，该Z3_rcf_del符号由提供z3-static。但是我们不能从顶层受益，因为libz3-static.a它是静态存档，显然我们无法在运行时加载。

通常，您可以使用来构建自定义运行时，ocamlmktop该运行时将链接z3，这可能是维护人员期望我们执行的操作。

可能更好的解决方案是以这种方式打包OCaml z3库，以便可以将其加载到OCaml vanilla顶层。这需要链接所有依赖项，并创建一个自包含的z3.cma（和z3.cmxs），可以在运行时加载它而无需任何额外的系统依赖项。

固定上游的一些指示

我记得同样的问题是我已经修复了本机版本（因此我当时也应该修复字节码版本），这是补丁。想法是将此补丁扩展到字节码部分-我们应该将-linkall选项添加到创建z3ml.cma文件的位置（可能在此处）。

简单又脏的解决方案

如前所述，您可以创建包含所有外部原语的自定义运行时，例如，

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

现在您可以开始

 ./z3top -I `ocamlfind query z3`

（是的，您仍然需要传递该-I选项，运行时仅链接实现，而不链接cmi文件），现在让我们检查它是否有效，

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

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

使用沙丘构建自定义的utop顶层

用z3构建一个utop增强的顶层有点麻烦，因此最好依靠一些构建系统的自动化，因此让我们使用dune。创建dune具有以下内容的文件

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

然后z3utop.ml使用以下内容创建文件

  let () = UTop_main.main ()

现在可以用

  dune build z3utop.bc

并与

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