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

Question

我正在 Z3 源目录中使用以下(标准)命令从源代码中使用 OCaml 编译 Z3:

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

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

然后运行

> utop

和

> #require "z3";;

给我以下错误:

无法加载所需的共享库 dllz3ml。
原因:/home/foobar/.opam/my_opam/lib/stublibs/dllz3ml.so: undefined symbol :Z3_rcf_del。

我对如何调试此类错误感到困惑。对于识别问题以及如何解决它有什么建议吗？

Answer 1

该问题表明缺少的符号不是由构成 OCaml z3 绑定(bind)的对象提供的，并且它不是运行时的一部分。结论是，您不能在默认运行时(即使用 ocaml 或 utop 应用程序)中使用 OCaml 顶层中的 OCaml z3 绑定(bind)。嗯，至少在 z3 绑定(bind)的当前状态下是这样。

首先，既然你问了，这里有一些调试此类问题的技巧。不确定它们在一般情况下是否会有帮助，但这将是我将采取的步骤，对于初学者来说。首先，我将仔细检查该符号是否确实未定义(有时它只是被损坏，或版本化，或具有错误的 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)，它可以在运行时加载，而无需任何额外的系统依赖项)。

修复上游的一些指示

我记得原生版本也有同样的问题，我已经修复了它(所以当时我可能也应该修复字节码版本)，这里是 the patch 。我们的想法是将此补丁扩展到字节码部分 - 我们应该将 -linkall 选项添加到创建 z3ml.cma 文件的位置(可能是 here )。

简单但肮脏的解决方案

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

 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`