运行 64 位 linux 系统上的 32 位 z3

Question

我正在尝试在 64 位 linux 系统上构建 32 位 z3。我需要这样做才能获得 32 位 libz3.so，我可以将其用于我的 32 位应用程序。我更改了 python 文件 scripts/mk_util.py 以将 -m32 标志添加到各种编译器和链接器标志。我可以使用 z3 文件夹中的这些步骤构建 z3：
python scripts/mk_make.py; cd build; make

然后，我调用make examples来构建c和cpp_examples。但是，当我运行 cpp_example 时，出现分段错误。以下是分段错误的回溯：

#0  0x00c95463 in goal::quick_process(bool, expr*&, dependency_manager<ast_manager::expr_dependency_config>::dependency*) () from ./libz3.so
#1  0x00c97b04 in goal::update(unsigned int, expr*, app*, dependency_manager<ast_manager::expr_dependency_config>::dependency*) () from ./libz3.so
#2  0x00c0e3c8 in simplify_tactic::imp::operator()(goal&) () from ./libz3.so
#3  0x00c0d55f in simplify_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) ()
   from ./libz3.so
#4  0x00c88eeb in cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) ()
   from ./libz3.so
#5  0x00c8ed02 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) ()
   from ./libz3.so
#6  0x00c88d7a in unary_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) ()
   from ./libz3.so
#7  0x00c8ed02 in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) ()
   from ./libz3.so
#8  0x00c88f83 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) ()
   from ./libz3.so
#9  0x00c88f83 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) ()
   from ./libz3.so
#10 0x00c88f83 in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) ()
   from ./libz3.so
#11 0x00c8f40d in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) ()
   from ./libz3.so
#12 0x00c88d7a in unary_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) ()
   from ./libz3.so
#13 0x00c81b8a in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) () from ./libz3.so
#14 0x00c8240a in check_sat(tactic&, ref<goal>&, ref<model>&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::basic_string<char, std::char_traits<char>, std::allocator<char> >&) () from ./libz3.so
#15 0x00b3b5af in tactic2solver::check_sat_core(unsigned int, expr* const*) () from ./libz3.so
#16 0x00b3cddc in solver_na2as::check_sat(unsigned int, expr* const*) () from ./libz3.so
#17 0x00b3a40d in combined_solver::check_sat(unsigned int, expr* const*) () from ./libz3.so
#18 0x00448808 in _solver_check () from ./libz3.so
#19 0x00448e2f in Z3_solver_check () from ./libz3.so
#20 0x0805a32a in z3::solver::check() ()
#21 0x0804b542 in find_model_example1() ()
#22 0x08056638 in main ()

我正在使用 Linux 版本 2.6.32-504.1.3.el6.x86_64、g++ 4.4.7、python 2.7 和 z3 的最新不稳定提交 48c72d2（2015- 01-23 | FPA API：命名一致性（HEAD，origin/unstable，不稳定）[Christoph M. Wintersteiger]）。这是 scripts/mk_util.py 文件的差异。

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 4641a7b..e6decc0 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -27,10 +27,10 @@ def getenv(name, default):

 CXX=getenv("CXX", None)
 CC=getenv("CC", None)
-CPPFLAGS=getenv("CPPFLAGS", "")
-CXXFLAGS=getenv("CXXFLAGS", "")
+CPPFLAGS=getenv("CPPFLAGS", "-m32")
+CXXFLAGS=getenv("CXXFLAGS", "-m32")
 EXAMP_DEBUG_FLAG=''
-LDFLAGS=getenv("LDFLAGS", "")
+LDFLAGS=getenv("LDFLAGS", "-m32")
 JNI_HOME=getenv("JNI_HOME", None)

 CXX_COMPILERS=['g++', 'clang++']
@@ -1523,7 +1523,7 @@ def mk_config():
         check_ar()
         CXX = find_cxx_compiler()
         CC  = find_c_compiler()
-        SLIBEXTRAFLAGS = ''
+        SLIBEXTRAFLAGS = '-m32'
         if GPROF:
             CXXFLAGS = '%s -pg' % CXXFLAGS
             LDFLAGS  = '%s -pg' % LDFLAGS
@@ -1572,7 +1572,7 @@ def mk_config():
             OS_DEFINES     = '-D_LINUX'
             SO_EXT         = '.so'
             LDFLAGS        = '%s -lrt' % LDFLAGS
-            SLIBFLAGS      = '-shared'
+            SLIBFLAGS      = '-shared -m32'
             SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS
         elif sysname == 'FreeBSD':
             CXXFLAGS       = '%s -fno-strict-aliasing -D_FREEBSD_' % CXXFLAGS

Answer 1

对构建系统的那些更改是正确的，但是要获得正确的 32 位二进制文件所需的一切，例如 AMD64 宏都需要删除。我现在已经将选项 --x86 添加到 mk_make.py（在不稳定的分支中），我希望它能正确设置所有设置。

运行 64 位 linux 系统上的 32 位 z3

Running 32-bit z3 on 64-bit linux systems

64-bit

z3