JonathanSalwan / Triton

Triton is a dynamic binary analysis library. Build your own program analysis tools, automate your reverse engineering, perform software verification or just emulate code.
https://triton-library.github.io
Apache License 2.0
3.39k stars 524 forks source link

Cannot build using lastest Bitwuzla version #1320

Closed h49nakxs closed 1 month ago

h49nakxs commented 2 months ago

Hello there,

I got several errors when trying to build Triton using the latest Bitwuzla version (0.4.0) built from sources :

/usr/include/c++/13/bits/stl_map.h:920:7: note:   candidate expects 2 arguments, 1 provided
/home/user/Triton/src/libtriton/ast/bitwuzla/tritonToBitwuzla.cpp:287:56: error: cannot convert ‘bitwuzla_sort_t*’ to ‘BitwuzlaTermManager*’
  287 |               return bitwuzla_mk_bv_value_uint64(sort->second, static_cast<uint64_t>(value));
      |                                                  ~~~~~~^~~~~~
      |                                                        |
      |                                                        bitwuzla_sort_t*
/usr/local/include/bitwuzla/c/bitwuzla.h:1821:63: note:   initializing argument 1 of ‘bitwuzla_term_t* bitwuzla_mk_bv_value_uint64(BitwuzlaTermManager*, BitwuzlaSort, uint64_t)’
 1821 | BitwuzlaTerm bitwuzla_mk_bv_value_uint64(BitwuzlaTermManager *tm,
      |                                          ~~~~~~~~~~~~~~~~~~~~~^~
/usr/local/include/bitwuzla/c/bitwuzla.h:288:16: note: class type ‘bitwuzla_sort_t’ is incomplete
  288 | typedef struct bitwuzla_sort_t *BitwuzlaSort;
      |                ^~~~~~~~~~~~~~~
/home/user/Triton/src/libtriton/ast/bitwuzla/tritonToBitwuzla.cpp:289:47: error: cannot convert ‘bitwuzla_sort_t*’ to ‘BitwuzlaTermManager*’
  289 |             return bitwuzla_mk_bv_value(sort->second, triton::utils::toString(value).c_str(), 10);
      |                                         ~~~~~~^~~~~~
      |                                               |
      |                                               bitwuzla_sort_t*
/usr/local/include/bitwuzla/c/bitwuzla.h:1801:56: note:   initializing argument 1 of ‘bitwuzla_term_t* bitwuzla_mk_bv_value(BitwuzlaTermManager*, BitwuzlaSort, const char*, uint8_t)’
 1801 | BitwuzlaTerm bitwuzla_mk_bv_value(BitwuzlaTermManager *tm,
      |                                   ~~~~~~~~~~~~~~~~~~~~~^~
/usr/local/include/bitwuzla/c/bitwuzla.h:288:16: note: class type ‘bitwuzla_sort_t’ is incomplete
  288 | typedef struct bitwuzla_sort_t *BitwuzlaSort;
      |                ^~~~~~~~~~~~~~~
/home/user/Triton/src/libtriton/ast/bitwuzla/tritonToBitwuzla.cpp:302:41: error: cannot convert ‘bitwuzla_sort_t*’ to ‘BitwuzlaTermManager*’
  302 |             n = bitwuzla_mk_const(sort->second, symVar->getName().c_str());
      |                                   ~~~~~~^~~~~~
      |                                         |
      |                                         bitwuzla_sort_t*
/usr/local/include/bitwuzla/c/bitwuzla.h:2120:53: note:   initializing argument 1 of ‘bitwuzla_term_t* bitwuzla_mk_const(BitwuzlaTermManager*, BitwuzlaSort, const char*)’
 2120 | BitwuzlaTerm bitwuzla_mk_const(BitwuzlaTermManager *tm,
      |                                ~~~~~~~~~~~~~~~~~~~~~^~
/usr/local/include/bitwuzla/c/bitwuzla.h:288:16: note: class type ‘bitwuzla_sort_t’ is incomplete
  288 | typedef struct bitwuzla_sort_t *BitwuzlaSort;
      |                ^~~~~~~~~~~~~~~
/home/user/Triton/src/libtriton/ast/bitwuzla/tritonToBitwuzla.cpp:312:45: error: cannot convert ‘BitwuzlaKind’ to ‘BitwuzlaTermManager*’
  312 |           return bitwuzla_mk_term1_indexed1(BITWUZLA_KIND_BV_ZERO_EXTEND,children[1], ext);
      |                                             ^~~~~~~~~~~~~~~~~~~~~~~~~~~~
      |                                             |
      |                                             BitwuzlaKind
/usr/local/include/bitwuzla/c/bitwuzla.h:2013:62: note:   initializing argument 1 of ‘bitwuzla_term_t* bitwuzla_mk_term1_indexed1(BitwuzlaTermManager*, BitwuzlaKind, BitwuzlaTerm, uint64_t)’
 2013 | BitwuzlaTerm bitwuzla_mk_term1_indexed1(BitwuzlaTermManager *tm,
      |                                         ~~~~~~~~~~~~~~~~~~~~~^~
/home/user/Triton/src/libtriton/engines/solver/bitwuzla/bitwuzlaSolver.cpp: In member function ‘virtual std::vector<std::unordered_map<long unsigned int, triton::engines::solver::SolverModel> > triton::engines::solver::BitwuzlaSolver::getModels(const triton::ast::SharedAbstractNode&, triton::uint32, triton::engines::solver::status_e*, triton::uint32, triton::uint32*) const’:
/home/user/Triton/src/libtriton/engines/solver/bitwuzla/bitwuzlaSolver.cpp:104:34: error: cannot convert ‘BitwuzlaOptions*’ to ‘BitwuzlaTermManager*’
  104 |         auto bzla = bitwuzla_new(bzlaOptions);
      |                                  ^~~~~~~~~~~
      |                                  |
      |                                  BitwuzlaOptions*
In file included from /home/user/Triton/src/libtriton/includes/triton/bitwuzlaSolver.hpp:17,
                 from /home/user/Triton/src/libtriton/engines/solver/bitwuzla/bitwuzlaSolver.cpp:13:
/usr/local/include/bitwuzla/c/bitwuzla.h:1168:45: note:   initializing argument 1 of ‘Bitwuzla* bitwuzla_new(BitwuzlaTermManager*, const BitwuzlaOptions*)’
 1168 | Bitwuzla *bitwuzla_new(BitwuzlaTermManager *tm, const BitwuzlaOptions *options);
      |                        ~~~~~~~~~~~~~~~~~~~~~^~
/usr/local/include/bitwuzla/c/bitwuzla.h:112:16: note: class type ‘BitwuzlaOptions’ is incomplete
  112 | typedef struct BitwuzlaOptions BitwuzlaOptions;
      |                ^~~~~~~~~~~~~~~
/home/user/Triton/src/libtriton/engines/solver/bitwuzla/bitwuzlaSolver.cpp:152:49: error: cannot convert ‘bitwuzla_sort_t* const’ to ‘BitwuzlaTermManager*’
  152 |             auto cur_val = bitwuzla_mk_bv_value(symvar_sort, svalue, 2);
      |                                                 ^~~~~~~~~~~
      |                                                 |
      |                                                 bitwuzla_sort_t* const
/usr/local/include/bitwuzla/c/bitwuzla.h:1801:56: note:   initializing argument 1 of ‘bitwuzla_term_t* bitwuzla_mk_bv_value(BitwuzlaTermManager*, BitwuzlaSort, const char*, uint8_t)’
 1801 | BitwuzlaTerm bitwuzla_mk_bv_value(BitwuzlaTermManager *tm,
      |                                   ~~~~~~~~~~~~~~~~~~~~~^~
/usr/local/include/bitwuzla/c/bitwuzla.h:288:16: note: class type ‘bitwuzla_sort_t’ is incomplete
  288 | typedef struct bitwuzla_sort_t *BitwuzlaSort;
      |                ^~~~~~~~~~~~~~~
/home/user/Triton/src/libtriton/engines/solver/bitwuzla/bitwuzlaSolver.cpp:168:54: error: cannot convert ‘BitwuzlaKind’ to ‘BitwuzlaTermManager*’
  168 |               bitwuzla_assert(bzla, bitwuzla_mk_term(BITWUZLA_KIND_OR, solution.size(), solution.data()));
      |                                                      ^~~~~~~~~~~~~~~~
      |                                                      |
      |                                                      BitwuzlaKind
/usr/local/include/bitwuzla/c/bitwuzla.h:1995:52: note:   initializing argument 1 of ‘bitwuzla_term_t* bitwuzla_mk_term(BitwuzlaTermManager*, BitwuzlaKind, uint32_t, bitwuzla_term_t**)’
 1995 | BitwuzlaTerm bitwuzla_mk_term(BitwuzlaTermManager *tm,
      |                               ~~~~~~~~~~~~~~~~~~~~~^~
/home/user/Triton/src/libtriton/engines/solver/bitwuzla/bitwuzlaSolver.cpp: In member function ‘triton::uint512 triton::engines::solver::BitwuzlaSolver::evaluate(const triton::ast::SharedAbstractNode&) const’:
/home/user/Triton/src/libtriton/engines/solver/bitwuzla/bitwuzlaSolver.cpp:217:34: error: cannot convert ‘BitwuzlaOptions*’ to ‘BitwuzlaTermManager*’
  217 |         auto bzla = bitwuzla_new(bzlaOptions);
      |                                  ^~~~~~~~~~~
      |                                  |
      |                                  BitwuzlaOptions*
/usr/local/include/bitwuzla/c/bitwuzla.h:1168:45: note:   initializing argument 1 of ‘Bitwuzla* bitwuzla_new(BitwuzlaTermManager*, const BitwuzlaOptions*)’
 1168 | Bitwuzla *bitwuzla_new(BitwuzlaTermManager *tm, const BitwuzlaOptions *options);
      |                        ~~~~~~~~~~~~~~~~~~~~~^~
make[2]: *** [src/libtriton/CMakeFiles/triton.dir/build.make:804: src/libtriton/CMakeFiles/triton.dir/ast/bitwuzla/tritonToBitwuzla.cpp.o] Error 1
/usr/local/include/bitwuzla/c/bitwuzla.h:112:16: note: class type ‘BitwuzlaOptions’ is incomplete
  112 | typedef struct BitwuzlaOptions BitwuzlaOptions;
      |                ^~~~~~~~~~~~~~~
make[2]: *** Waiting for unfinished jobs....
/home/user/Triton/src/libtriton/engines/solver/bitwuzla/bitwuzlaSolver.cpp:234:80: error: no matching function for call to ‘boost::multiprecision::number<boost::multiprecision::backends::cpp_int_backend<512, 512, boost::multiprecision::unsigned_magnitude, boost::multiprecision::unchecked, void> >::number(<brace-enclosed initializer list>)’
  234 |           res = triton::uint512{bitwuzla_term_value_get_str_fmt(term_value, 10)};

In the meantime. building without Bitwuzla works fine.

Also, as a side note, latest capstone version pulled from Github is not compatible with Triton (because they renamed arm64 into aarch64) and you have to build capstone using the "v4" branch.

JonathanSalwan commented 2 months ago

I think it has been fixed in dev-v0.1?