Segfault из-за связи stati c с библиотеками ocaml и c

Question

У меня вопрос по поводу ссылки c в ocaml. При передаче флага "-stati c" компилятору 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 ()

Когда я компилирую без stati c, связывание все работает нормально. Однако мне нужен бинарный файл stati c для бенчмаркинга на внешнем сервере. Я уже пытался использовать ocaml вместе с musl, но, к сожалению, процесс установки завершился неудачно из-за следующей нерешенной проблемы .

Кто-нибудь сталкивался с такой же проблемой и знает, как решить эту проблему?

Обновление: нам потребовалось некоторое время, но мы обнаружили, что проблема, похоже, связана с smt solver 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 для компиляции этой программы в исходный двоичный файл c.

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 \

Файл OMake root является стандартным файлом OMake root. Версия OCaML - 4.07.1, версия z3 - 4.8.7.

Answer 1

Кто-нибудь сталкивался с такой же проблемой

Одно из возможных объяснений: ваш бинарный файл слишком большой, компоновщик переполнен, но либо не предупреждает об этом, либо вы проигнорировали предупреждение.

Чтобы убедиться, что это так, проверьте двоичный файл с ls -l - если его размер превышает 2 ГБ, вероятно переполнение перемещения.

Также убедитесь, что нет ссылки предупреждение, и что ваш компоновщик недавно.

как решить эту проблему?

Если проблема на самом деле из-за переполнения перемещения, вы не так уж много может сделать - ваш двоичный файл слишком велик.

Если вы собрали его (или некоторые его части) без оптимизации, попробуйте собрать с оптимизацией (которая может привести к созданию значительно меньших двоичных файлов) и / или собрать с -ffunction-sections -fdata-sections и -Wl,--icf=safe для включения сборки мусора компоновщика.

Если ничего из этого не работает, вы можете попробовать собрать и связать все с помощью -mcmodel=large, но это не является проверенной конфигурацией, и может потерпеть неудачу по другой причине.