在本地 Opam 环境中安装 Z3 OCaml 绑定时出现链接器错误
Linker error when installing Z3 OCaml bindings in local Opam environment
我在 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.
我对如何调试这些类型的错误感到困惑。对于确定问题以及如何解决问题有什么建议吗？
问题表明缺少的符号不是由构成 OCaml z3 绑定的对象提供的，它不是 运行 时间的一部分。结论是，您不能在默认的 运行 时间（即 ocaml 或 utop 应用程序）的 OCaml 顶层中使用 OCaml z3 绑定。好吧，至少在 z3 绑定的当前状态下。
首先，既然你问了，这里有一些调试此类问题的技巧。不确定它们在一般情况下是否会有所帮助，但对于初学者来说，这将是我将采取的步骤。首先，我会 double-check 这个符号确实是未定义的（有时它只是被破坏，或者版本化，或者有错误的 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 构建自定义 运行time，这将 link z3，这可能是维护者希望我们做的。
一个可能更好的解决方案是以可以加载到 OCaml 香草顶层的方式打包 OCaml z3 库。这需要 linking 所有依赖项并创建一个 self-contained z3.cma（和 z3.cmxs），它可以在 运行 时间内加载而无需任何额外的系统依赖项）。
修复上游的一些指导
我记得原生版本也有同样的问题，我已经修复了（所以当时我可能也应该修复字节码版本），这里是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）。
简单而肮脏的解决方案
正如我之前提到的，您可以创建包含所有外部原语的自定义 运行time，例如，
ocamlfind ocamlmktop -thread -custom -linkpkg -package z3 -o z3top
现在您可以从
开始
./z3top -I `ocamlfind query z3`
（是的，您仍然需要传递 -I 选项，运行 时间 link 仅执行，而不是 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`
我在 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.
我对如何调试这些类型的错误感到困惑。对于确定问题以及如何解决问题有什么建议吗？
问题表明缺少的符号不是由构成 OCaml z3 绑定的对象提供的，它不是 运行 时间的一部分。结论是，您不能在默认的 运行 时间（即 ocaml 或 utop 应用程序）的 OCaml 顶层中使用 OCaml z3 绑定。好吧，至少在 z3 绑定的当前状态下。
首先，既然你问了，这里有一些调试此类问题的技巧。不确定它们在一般情况下是否会有所帮助，但对于初学者来说，这将是我将采取的步骤。首先，我会 double-check 这个符号确实是未定义的（有时它只是被破坏，或者版本化，或者有错误的 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 构建自定义 运行time，这将 link z3，这可能是维护者希望我们做的。
一个可能更好的解决方案是以可以加载到 OCaml 香草顶层的方式打包 OCaml z3 库。这需要 linking 所有依赖项并创建一个 self-contained z3.cma（和 z3.cmxs），它可以在 运行 时间内加载而无需任何额外的系统依赖项）。
修复上游的一些指导
我记得原生版本也有同样的问题，我已经修复了（所以当时我可能也应该修复字节码版本），这里是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）。
简单而肮脏的解决方案
正如我之前提到的，您可以创建包含所有外部原语的自定义 运行time，例如，
ocamlfind ocamlmktop -thread -custom -linkpkg -package z3 -o z3top
现在您可以从
开始 ./z3top -I `ocamlfind query z3`
（是的，您仍然需要传递 -I 选项，运行 时间 link 仅执行，而不是 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`