search

Z3Prover / z3

The Z3 Theorem Prover
Other
9.96k stars 1.46k forks source link

Failed to build libz3.so because of missing `LDFLAGS` in `SLIBEXTRAFLAGS` when cross compiling z3 #7225

Closed shijy16 closed 1 month ago

shijy16 commented 1 month ago

I've been trying to cross-compiling z3 for arm32 on a x64 machine with arm-linux-gnu toolchain and clang/clang++, with the following environment settings:

  export CC=clang-15
  export CXX=clang++-15
  export CFLAGS="-fno-inline -g -fno-stack-protector --target=arm-linux-gnu -march=armv8-a -mfloat-abi=soft  -O$2 -I/usr/arm-linux-gnueabi/include/"
  export CXXFLAGS="-fno-inline -g -fno-stack-protector --target=arm-linux-gnu -march=armv8-a -mfloat-abi=soft  -O$2 -I/usr/arm-linux-gnueabi/include/"
  export CPPFLAGS="-fno-inline -g -fno-stack-protector --target=arm-linux-gnu -march=armv8-a -mfloat-abi=soft  -O$2 -I/usr/arm-linux-gnueabi/include/"
  export LDFLAGS="-fuse-ld=lld-15 -mfloat-abi=soft --target=arm-linux-gnu -march=armv8-a -L/usr/arm-linux-gnueabi/lib/  -Wl,-z,notext"

It went well until generating libz3.so:

clang++-15 -static -o z3  shell/gparams_register_modules.o shell/z3_log_frontend.o shell/drat_frontend.o shell/dimacs_frontend.o shell/mem_initializer.o shell/datalog_frontend.o shell/install_tactic.o shell/smtlib_frontend.o shell/opt_frontend.o shell/main.o api/api.a cmd_context/extra_cmds/extra_cmds.a opt/opt.a tactic/portfolio/portfolio.a tactic/fpa/fpa_tactics.a tactic/ufbv/ufbv_tactic.a tactic/smtlogics/smtlogic_tactics.a muz/fp/fp.a muz/bmc/bmc.a muz/ddnf/ddnf.a muz/tab/tab.a muz/clp/clp.a muz/spacer/spacer.a muz/rel/rel.a muz/transforms/transforms.a muz/dataflow/dataflow.a muz/base/muz.a tactic/fd_solver/fd_solver.a sat/sat_solver/sat_solver.a qe/qe.a tactic/sls/sls_tactic.a smt/tactic/smt_tactic.a tactic/bv/bv_tactics.a nlsat/tactic/nlsat_tactic.a sat/tactic/sat_tactic.a sat/smt/sat_smt.a smt/smt.a smt/proto_model/proto_model.a math/subpaving/tactic/subpaving_tactic.a solver/assertions/solver_assertions.a tactic/arith/arith_tactics.a tactic/core/core_tactics.a ast/fpa/fpa.a ackermannization/ackermannization.a tactic/aig/aig_tactic.a ast/pattern/pattern.a parsers/smt2/smt2parser.a cmd_context/cmd_context.a solver/solver.a qe/lite/qe_lite.a qe/mbp/mbp.a tactic/tactic.a ast/sls/ast_sls.a ast/simplifiers/simplifiers.a ast/converters/converters.a model/model.a ast/macros/macros.a ast/proofs/proofs.a ast/substitution/substitution.a ast/normal_forms/normal_forms.a ast/rewriter/bit_blaster/bit_blaster.a ast/rewriter/rewriter.a math/lp/lp.a nlsat/nlsat.a sat/sat.a math/grobner/grobner.a ast/euf/euf.a parsers/util/parser_util.a smt/params/smt_params.a ast/ast.a math/subpaving/subpaving.a math/realclosure/realclosure.a params/params.a math/automata/automata.a math/hilbert/hilbert.a math/simplex/simplex.a math/dd/dd.a math/interval/interval.a math/polynomial/polynomial.a util/util.a -Wl,--whole-archive -lrt -lpthread -Wl,--no-whole-archive -fuse-ld=lld-15 -mfloat-abi=soft --target=arm-linux-gnu -march=armv8-a -L/usr/arm-linux-gnueabi/lib/  -Wl,-z,notext
clang++-15 -o libz3.so -shared api/dll/gparams_register_modules.o api/dll/mem_initializer.o api/dll/install_tactic.o api/dll/dll.o api/z3_replayer.o api/api_log_macros.o api/api_log.o api/api_context.o api/api_algebraic.o api/api_opt.o api/api_pb.o api/api_goal.o api/api_fpa.o api/api_config_params.o api/api_arith.o api/api_datatype.o api/api_stats.o api/api_model.o api/api_quant.o api/api_ast.o api/api_ast_map.o api/api_rcf.o api/api_special_relations.o api/api_datalog.o api/api_numeral.o api/api_params.o api/api_solver.o api/api_polynomial.o api/api_seq.o api/api_qe.o api/api_tactic.o api/api_bv.o api/api_array.o api/api_ast_vector.o api/api_parsers.o api/api_commands.o cmd_context/extra_cmds/extra_cmds.a opt/opt.a tactic/portfolio/portfolio.a tactic/fpa/fpa_tactics.a tactic/ufbv/ufbv_tactic.a tactic/smtlogics/smtlogic_tactics.a muz/fp/fp.a muz/bmc/bmc.a muz/ddnf/ddnf.a muz/tab/tab.a muz/clp/clp.a muz/spacer/spacer.a muz/rel/rel.a muz/transforms/transforms.a muz/dataflow/dataflow.a muz/base/muz.a tactic/fd_solver/fd_solver.a sat/sat_solver/sat_solver.a qe/qe.a tactic/sls/sls_tactic.a smt/tactic/smt_tactic.a tactic/bv/bv_tactics.a nlsat/tactic/nlsat_tactic.a sat/tactic/sat_tactic.a sat/smt/sat_smt.a smt/smt.a smt/proto_model/proto_model.a math/subpaving/tactic/subpaving_tactic.a solver/assertions/solver_assertions.a tactic/arith/arith_tactics.a tactic/core/core_tactics.a ast/fpa/fpa.a ackermannization/ackermannization.a tactic/aig/aig_tactic.a ast/pattern/pattern.a parsers/smt2/smt2parser.a cmd_context/cmd_context.a solver/solver.a qe/lite/qe_lite.a qe/mbp/mbp.a tactic/tactic.a ast/sls/ast_sls.a ast/simplifiers/simplifiers.a ast/converters/converters.a model/model.a ast/macros/macros.a ast/proofs/proofs.a ast/substitution/substitution.a ast/normal_forms/normal_forms.a ast/rewriter/bit_blaster/bit_blaster.a ast/rewriter/rewriter.a math/lp/lp.a nlsat/nlsat.a sat/sat.a math/grobner/grobner.a ast/euf/euf.a parsers/util/parser_util.a smt/params/smt_params.a ast/ast.a math/subpaving/subpaving.a math/realclosure/realclosure.a params/params.a math/automata/automata.a math/hilbert/hilbert.a math/simplex/simplex.a math/dd/dd.a math/interval/interval.a math/polynomial/polynomial.a util/util.a -lpthread  -Wl,-soname,libz3.so
/usr/bin/ld: api/dll/gparams_register_modules.o: relocations in generic ELF (EM: 40)
...                    <--    lots of repeated errors here)
/usr/bin/ld: api/dll/gparams_register_modules.o: error adding symbols: file in wrong format
clang: error: linker command failed with exit code 1 (use -v to see invocation)
make: *** [Makefile:5291: libz3.so] Error 1
make: *** Waiting for unfinished jobs....

I noticed that flags are missing in the command for generating libz3.so (the second line above) , e.g. -fuse-ld=lld-15 -mfloat-abi=soft --target=arm-linux-gnu -march=armv8-a -L/usr/arm-linux-gnueabi/lib/. After reading the Makefile and the python scripts for making Makefile (scripts/mk_util.py), I think the following code causes the problem:

         SLIBEXTRAFLAGS = ''
        # SLIBEXTRAFLAGS = '%s -Wl,-soname,libz3.so.0' % LDFLAGS

The commented line(L2603) adds LDFLAGS to SLIBEXTRAFLAGS, but it was commented in this commit. I fix the cross-compiling issue by simply uncommenting this line.

I wonder about the intention behind commenting out this line. If there is none, then it should be uncommented.

shijy16 commented 1 month ago

Solved in the comment of #7226 .