由于与 ocaml 和 c 库的静态链接导致的段错误答案

【问题标题】：Segfault due to static linking with ocaml and c libraries由于与 ocaml 和 c 库的静态链接导致的段错误
【发布时间】：2020-02-21 10:59:39
【问题描述】：

我有一个关于 ocaml 中的静态链接的问题。将标志“-static”传递给 c 编译器时，它会编译，但在调用生成的二进制文件时，我会立即遇到分段错误。 gdb的输出如下：

#0  0x0000000000000000 in ?? ()
#1  0x000000000052268e in _GLOBAL__sub_I_util.cpp ()
#2  0x0000000001a5a00c in __libc_csu_init ()
#3  0x0000000001a597d7 in __libc_start_main ()
#4  0x000000000053505a in _start ()

当我在没有静态链接的情况下进行编译时，一切正常。但是，我需要一个静态二进制文件来在外部服务器上进行基准测试。我已经尝试过将 ocaml 与 musl 一起使用，但不幸的是，由于以下未解决的issue，安装过程失败。

有没有人遇到过同样的问题并且知道如何解决这个问题？

更新：我们花了一些时间，但我们发现问题似乎与 smt 求解器 z3 有关。 MWE 是

源文件（检查公式“真”是否可满足）

module Z3Solver =
  struct
    let context = ref (
                      Z3.mk_context [
                          ("model", "true");
                          ("proof", "false");
                        ]
                    )   
    let satis  =
      let z3_expr = Z3.Boolean.mk_true !context in
      let optimisation_goal = Z3.Optimize.mk_opt !context in
      Z3.Optimize.add optimisation_goal [z3_expr];
      let status = Z3.Optimize.check optimisation_goal in
      status == Z3.Solver.SATISFIABLE
  end

let run =
  let model = Z3Solver.satis in
  if model then
    print_string "satisfiable\n"
  else 
    print_string "unsatisfiable\n"

我们使用 OMake 将此程序编译为静态原生二进制文件。

USE_OCAMLFIND = true
OCAMLOPTFLAGS += -p -g -thread -ccopt -static -cc $(CXX)

OCAMLPACKS[] =
    z3

# Include all .ml files
FILES[] = $(removesuffix .ml, $(glob *.ml))

.PHONY: clean install

.DEFAULT: install

OCamlProgram(z3test, $(FILES))

install: z3test

clean:
    rm -f \
     *.cmi \
         *.cmx \
         *.o \
     *.omc \
     *.log \
     *.cache \
     z3test z3test.opt \

OMakeroot 文件只是标准的 OMakeroot 文件。 OCaML 版本是 4.07.1，z3 版本是 4.8.7。

【问题讨论】：

查看您的堆栈，我看到一些看起来像 C++ 初始化的东西。如果您真的只是与 C 链接，那可能需要研究一下。如果您提供一个完整的小示例来说明问题，这也会有所帮助。您对问题的描述几乎没有什么可说的。
感谢您的帮助。我包括了一个 MWE。
我遇到了同样的问题，链接 z3 静态库以制作静态链接二进制文件（用 C++ 编写）。但是，很奇怪，如果我选择制作一个动态链接的二进制文件（但仍然链接到z3静态库，libz3.a），没有问题。我仍在调查原因。

标签： segmentation-fault ocaml z3 static-linking libc

【解决方案1】：

有没有人遇到过同样的问题

一种可能的解释：你的二进制文件太大，链接器有重定位溢出，但要么没有警告，要么你忽略了警告。

要确认是这种情况，请使用ls -l 检查您的二进制文件——如果它的大小超过 2GiB，则可能会发生重定位溢出。

还要确保没有链接警告，并且您的链接器是最新的。

如何解决这个问题？

如果问题实际上是由于重定位溢出造成的，那么您无能为力——您的二进制文件太大。

如果您在构建它（或其中的某些部分）时未进行优化，请尝试使用优化构建（可以生成更小的二进制文件），和/或使用 -ffunction-sections -fdata-sections 和 -Wl,--icf=safe 构建以启用链接器垃圾回收.

如果这些都不起作用，您可以尝试使用 -mcmodel=large 构建和链接所有内容，但这不是经过充分测试的配置，并且可能由于其他原因而失败。

【讨论】：

【解决方案2】：

我认为这可能是 z3 问题。如果你这样配置z3：./configure --staticlib --single-threaded，然后编译得到libz3.a（我也把configure之前的老build目录删掉了），我觉得应该可以。

我正在向开发人员提出这个问题，另请参阅：https://github.com/Z3Prover/z3/issues/4554

谢谢！

【讨论】：