Segfault是由于与ocaml和c库的静态链接

Question

我有一个关于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一起使用，但不幸的是，由于以下未解决的问题，安装过程失败了。

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

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

源文件(检查公式"true"是否可满足(

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 "satisfiablen"
else 
print_string "unsatisfiablen"

我们使用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。

Answer 1

有人遇到过同样的问题吗

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

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

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

如何解决这个问题？

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

如果您在没有优化的情况下构建它(或它的某些部分(，请尝试使用优化构建(这可能会产生更小的二进制文件(，和/或使用-ffunction-sections-fdata-sections和-Wl,--icf=safe构建以启用链接器垃圾收集。

如果这些都不起作用，您可能会尝试用-mcmodel=large构建并链接所有内容，但这不是一个经过良好测试的配置，可能会因为不同的原因而失败。

Answer 2

我认为这可能是z3的问题。如果您这样配置z3：./configure --staticlib --single-threaded，然后编译它以获得libz3.a(我还删除了configure之前的旧build目录(，我认为它可能会工作。

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

谢谢！