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

Question

我正在使用 Z3 源目录中的以下（标准）命令从源代码中使用 OCaml 编译 Z3：

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

然后从build/目录中构建和安装。

然后运行

> utop

和

> #require "z3";;

给了我以下错误：

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

我对如何调试这些类型的错误感到困惑。是否有任何建议可以确定问题以及如何解决？

Answer 1

问题表明缺少的符号不是由构成 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 vanilla 顶层的方式打包 OCaml z3 库。这需要链接所有依赖项并创建一个独立的 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`