Z3 на архитектурах не x86

Question

Я проверял переносимость инструмента, используя Z3 (git-версия 2012-12-21, последняя "основная" версия), и, таким образом, пытался скомпилировать Z3 на Sparc64. Мне пришлось возиться с src/util/hwf.cpp так что он будет относиться к Sparc64, а не только к IA64, как к недостатку SIMD и emmintrin.h, Компиляция удалась.

К сожалению, в результате происходит сбой исполняемого файла при запуске с ошибкой шины в prime_generator::prime_generator(), Понятия не имею почему.

Program received signal SIGBUS, Bus error.
0x009b1dac in global constructors keyed to _ZN15prime_generatorC2Ev ()
(gdb) bt
#0  0x009b1dac in global constructors keyed to _ZN15prime_generatorC2Ev ()

Это не очень важно для меня (наши машины x86 или x86-64), но может быть актуально для некоторых встроенных приложений.

Answer 1

Я не думаю, что был какой-либо интерес к запуску Z3 на машинах, отличных от x86, поэтому весьма вероятно, что вы найдете несколько проблем.

В частности, SPARC не разрешает доступ к памяти без выравнивания, как это делает x86. При быстром взгляде я увидел несколько точек, откуда могут прийти неприсоединившиеся. Например, memory::allocate() обрабатывает указатель, возвращаемый malloc с помощью sizeof(size_t). Если это не 64 бита, то произойдет сбой (из-за данных svector). Затем, распределение svector, также резервирует 2*sizeof(без знака) перед данными. Если 2*sizeof(unsigned) не кратен sizeof(uint64), вы получите сбой.

И так далее. Дело в том, что без дополнительной информации вам невозможно помочь. Вам нужно скомпилировать с помощью -g и, если необходимо, распечатать код сборки, где он падает, чтобы точно определить точное местоположение.

Кроме того, не используйте основную ветку, пожалуйста. Это очень старый. Пожалуйста, рассмотрите возможность использования нестабильной ветки (это не так плохо, как может показаться название:)