diff --git a/CMakeLists.txt b/CMakeLists.txt index c7be0169..c030d30f 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -61,6 +61,7 @@ add_library(maat_maat src/serialization/serialization_helpers.cpp src/serialization/serializer.cpp src/solver/solver.cpp + src/solver/solver_btor.cpp src/solver/solver_z3.cpp src/third-party/murmur3/murmur3.c src/third-party/keccak/sha3.cpp @@ -130,6 +131,12 @@ if(maat_USE_Z3) target_compile_definitions(maat_maat PUBLIC MAAT_Z3_BACKEND=1 MAAT_HAS_SOLVER_BACKEND=1) endif() +if(maat_USE_BOOLECTOR) + find_package(Boolector) + target_link_libraries(maat_maat PUBLIC Boolector::boolector) + target_compile_definitions(maat_maat PUBLIC MAAT_BOOLECTOR_BACKEND=1) +endif() + if(maat_USE_LIEF) find_package(LIEF 0.12 REQUIRED) target_link_libraries(maat_maat PUBLIC LIEF::LIEF) diff --git a/bindings/bindings.cmake b/bindings/bindings.cmake index 522cf87c..0fa7f66f 100644 --- a/bindings/bindings.cmake +++ b/bindings/bindings.cmake @@ -81,6 +81,12 @@ if(maat_USE_Z3) target_compile_definitions(maat_python PRIVATE MAAT_Z3_BACKEND=1 MAAT_HAS_SOLVER_BACKEND=1) endif() +if(maat_USE_BOOLECTOR) + find_package(Boolector) + target_link_libraries(maat_python PRIVATE Boolector::boolector) + target_compile_definitions(maat_python PUBLIC MAAT_BOOLECTOR_BACKEND=1) +endif() + if(maat_USE_LIEF) target_link_libraries(maat_python PRIVATE LIEF::LIEF) target_compile_definitions(maat_python PRIVATE MAAT_LIEF_BACKEND=1 MAAT_HAS_LOADER_BACKEND=1) diff --git a/bindings/python/py_maat.cpp b/bindings/python/py_maat.cpp index 267ada61..faa9faab 100644 --- a/bindings/python/py_maat.cpp +++ b/bindings/python/py_maat.cpp @@ -25,6 +25,7 @@ PyMethodDef module_methods[] = { {"MaatEngine", (PyCFunction)maat_MaatEngine, METH_VARARGS, "Create a new DSE engine"}, // Solver {"Solver", (PyCFunction)maat_Solver, METH_NOARGS, "Create a constraint solver"}, + {"constraints_to_smt2", (PyCFunction)maat_constraints_to_smt2, METH_VARARGS, "Convert a list of constraints to an SMTlibv2 string"}, // Arch {"Arch", (PyCFunction)maat_Arch, METH_VARARGS, "Create a new Architecture"}, // SimpleStateManager diff --git a/bindings/python/py_solver.cpp b/bindings/python/py_solver.cpp index ece55b0d..954a5d42 100644 --- a/bindings/python/py_solver.cpp +++ b/bindings/python/py_solver.cpp @@ -164,6 +164,21 @@ PyObject* maat_Solver(PyObject* module) return PySolver_FromSolver(res); } +PyObject* maat_constraints_to_smt2(PyObject* self, PyObject* args) +{ + PyObject* py_constraints; + std::vector constraints; + if (not PyArg_ParseTuple(args, "O", &py_constraints)) + return NULL; + + PyObject* fail = py_to_native(py_constraints, constraints); + if (fail != nullptr) + return fail; + + std::string res = solver::constraints_to_smt2(constraints); + return PyUnicode_FromString(res.c_str()); +} + } // namespace py } // namespace maat diff --git a/bindings/python/python_bindings.hpp b/bindings/python/python_bindings.hpp index 806344cc..514444c3 100644 --- a/bindings/python/python_bindings.hpp +++ b/bindings/python/python_bindings.hpp @@ -272,6 +272,7 @@ typedef struct{ } Solver_Object; PyObject* get_Solver_Type(); PyObject* maat_Solver(PyObject* module); +PyObject* maat_constraints_to_smt2(PyObject* module, PyObject* args); #define as_solver_object(x) (*((Solver_Object*)x)) #endif @@ -369,7 +370,7 @@ PyObject* get_EVMTransactionResult_Type(); PyObject* PyEVMTxResult_FromTxResult(env::EVM::TransactionResult*); #define as_tx_result_object(x) (*((EVMTransactionResult_Object*)x)) -// Return the contract associated with an engine +// EVM helper functions PyObject* maat_contract(PyObject* mod, PyObject* args); PyObject* maat_new_evm_runtime(PyObject* mod, PyObject* args); PyObject* maat_increment_block_timestamp(PyObject* mod, PyObject* args); @@ -383,6 +384,10 @@ PyObject* maat_allow_symbolic_keccak(PyObject* mod, PyObject* args); PyObject* native_to_py(const std::vector&); PyObject* native_to_py(const std::unordered_set& constraints); +// Transform a list of python objects into native objects. Returns a +// python error on error, and NULL on success +PyObject* py_to_native(PyObject* list, std::vector& dest); + // Python bigint into multiprecision number // num MUST be a PyLong object (no further type checks in the function) Number bigint_to_number(size_t bits, PyObject* num); diff --git a/bindings/python/util.cpp b/bindings/python/util.cpp index a865faee..52106b3e 100644 --- a/bindings/python/util.cpp +++ b/bindings/python/util.cpp @@ -48,6 +48,23 @@ PyObject* native_to_py(const std::unordered_set& constraints) return list; } +PyObject* py_to_native(PyObject* list, std::vector& dest) +{ + if (!PyList_Check(list) ) + return PyErr_Format(PyExc_TypeError, "Expected list of constraints"); + + for (int i = 0; i < PyList_Size(list); i++) + { + PyObject* val = PyList_GetItem(list, i); + if (!PyObject_TypeCheck(val, (PyTypeObject*)get_Constraint_Type())) + { + return PyErr_Format(PyExc_TypeError, "List contains object which is not a 'Constraint'"); + } + dest.push_back(*as_constraint_object(val).constr); + } + return nullptr; // return null on success +} + Number bigint_to_number(size_t bits, PyObject* num) { if (bits <= 64) diff --git a/cmake/install-config.cmake.in b/cmake/install-config.cmake.in index 8bd52a56..4d9a0987 100644 --- a/cmake/install-config.cmake.in +++ b/cmake/install-config.cmake.in @@ -16,6 +16,11 @@ if("${maat_USE_Z3}") find_dependency(Z3) endif() +set(maat_USE_BOOLECTOR @maat_USE_BOOLECTOR@) +if("${maat_USE_BOOLECTOR}") + find_dependency(Boolector) +endif() + set(maat_USE_LIEF @maat_USE_LIEF@) if("${maat_USE_LIEF}") find_dependency(LIEF) diff --git a/cmake/variables.cmake b/cmake/variables.cmake index 87433255..d31dd1a0 100644 --- a/cmake/variables.cmake +++ b/cmake/variables.cmake @@ -18,6 +18,7 @@ endif() # technically require but are almost always desirable to find. We include # these options to let an advanced user implement their own backends option(maat_USE_Z3 "Build with Z3 solver backend" ON) +option(maat_USE_BOOLECTOR "Build with Boolector solver backend" OFF) option(maat_USE_LIEF "Build with LIEF loader backend" ON) # Optionally use vendored dependencies diff --git a/src/include/maat/solver.hpp b/src/include/maat/solver.hpp index 87906f4b..a4fc9470 100644 --- a/src/include/maat/solver.hpp +++ b/src/include/maat/solver.hpp @@ -9,12 +9,16 @@ #include "z3++.h" #endif +#ifdef MAAT_BOOLECTOR_BACKEND +#include "boolector/boolector.h" +#endif + namespace maat { namespace solver { - + /** \defgroup solver Solver * \brief The Maat's constraint solver interface */ @@ -78,6 +82,49 @@ class SolverZ3 : public Solver virtual std::shared_ptr get_model(); virtual VarContext* _get_model_raw(); }; + +// Forward decl +z3::expr constraint_to_z3(z3::context* c, const Constraint& constr); + +/// Convert a set of constraints into SMTlibv2 format +template< template< typename ELEM, typename ALLOC = std::allocator> class C> +std::string constraints_to_smt2(const C& constraints) { + auto ctx = new z3::context(); + auto sol = new z3::solver(*ctx); + for (auto c : constraints) + sol->add(constraint_to_z3(ctx, c)); + std::string res = sol->to_smt2(); + delete sol; + delete ctx; + return res; +} + +/// Create a VarContext from an smtlib2 model +VarContext* ctx_from_smt2(const char* string); +#endif + +#ifdef MAAT_BOOLECTOR_BACKEND +class SolverBtor : public Solver +{ +private: + Btor* btor; + // Set to file that holds the current computed model, or to NULL + const char * model_file; +private: + std::list constraints; + bool has_model; ///< Set to true if check() returned true +public: + SolverBtor(); + virtual ~SolverBtor(); + void reset(); + void add(const Constraint& constr); + void pop(); + bool check(); + virtual std::shared_ptr get_model(); + virtual VarContext* _get_model_raw(); +private: + void reset_btor(); +}; #endif /** \} */ // doxygen groupe Solver diff --git a/src/include/maat/varcontext.hpp b/src/include/maat/varcontext.hpp index 8dc37ac2..47eecb42 100644 --- a/src/include/maat/varcontext.hpp +++ b/src/include/maat/varcontext.hpp @@ -92,6 +92,7 @@ class VarContext: public serial::Serializable void print(std::ostream& os) const; ///< Print the context to a stream Endian endianness() const; ///< Return endianness std::set contained_vars() const; ///< Return the contained symbolic variables + public: virtual serial::uid_t class_uid() const; virtual void dump(serial::Serializer& s) const; diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index ccc6db95..79cd4dfa 100644 --- a/src/solver/solver.cpp +++ b/src/solver/solver.cpp @@ -25,7 +25,8 @@ bool Solver::did_time_out() const std::unique_ptr new_solver() { #ifdef MAAT_Z3_BACKEND - return std::make_unique(); + // DEBUG return std::make_unique(); + return std::make_unique(); #else return nullptr; #endif diff --git a/src/solver/solver_btor.cpp b/src/solver/solver_btor.cpp new file mode 100644 index 00000000..1d160ab4 --- /dev/null +++ b/src/solver/solver_btor.cpp @@ -0,0 +1,172 @@ +#ifdef MAAT_BOOLECTOR_BACKEND + +#include "maat/solver.hpp" +#include "maat/stats.hpp" +#include "maat/exception.hpp" +#include + +namespace maat +{ +namespace solver +{ + +SolverBtor::SolverBtor(): + Solver(), + has_model(false), + btor(nullptr), + model_file(nullptr) +{ + reset_btor(); +} + +SolverBtor::~SolverBtor() +{ + boolector_delete(btor); + btor = nullptr; +} + +void SolverBtor::reset_btor() +{ + if (btor != nullptr) + { + // TODO(boyan) + // DEBUG: are these calls useful ? + boolector_reset_assumptions(btor); + boolector_release_all(btor); + boolector_delete(btor); + } + btor = boolector_new(); + boolector_set_opt (btor, BTOR_OPT_MODEL_GEN, 1); + boolector_set_opt (btor, BTOR_OPT_INCREMENTAL, 1); +} + +void SolverBtor::reset() +{ + constraints.clear(); + has_model = false; + _did_time_out = false; + reset_btor(); +} + +void SolverBtor::add(const Constraint& constr) +{ + constraints.push_back(constr); + has_model = false; +} + +void SolverBtor::pop() +{ + constraints.pop_back(); +} + +bool SolverBtor::check() +{ + // If already has model, don't recompute it + if (has_model) + return true; + + reset_btor(); + + // Statistics + MaatStats::instance().start_solving(); + + // Dump constraints to temporary file + // TODO(boyan): use mkstemp instead of tmpnam + const char *smt_file = tmpnam(NULL); // Get temp name + if (smt_file == nullptr) + throw solver_exception("SolverBtor::check(): couldn't create temporary filename"); + std::ofstream f(smt_file); + if (not f.good()) + throw solver_exception("SolverBtor::check(): couldn't create temporary SMT file"); + std::string smt_string = constraints_to_smt2(constraints); + f << smt_string; + f.close(); + + std::cout << "DEBUG SMT QUERY iN " << smt_file << "\n"; + + // Load SMT in boolector + // TODO(boyan): don't reopen smt_file + // TODO(boyan): don't hardcode dev/null but make it dependent on + // the platform, and find a solution for Windows + FILE* infile = fopen(smt_file, "r"); + FILE* outfile = fopen("/dev/null", "w"); + char* error_msg; + int _status; + int status = boolector_parse_smt2( + btor, + infile, // infile + smt_file, // infile_name + outfile, // outfile + &error_msg, // error_msg + &_status // status + ); + fclose(outfile); + fclose(infile); + + // DEBUG + // if (status == BOOLECTOR_PARSE_UNKNOWN) + // status = boolector_sat(btor); + if (status == BOOLECTOR_PARSE_UNKNOWN) + throw solver_exception( + Fmt() << "SolverBtor::check(): error solving SMT file: " + << smt_file >> Fmt::to_str + ); + + has_model = (status == BOOLECTOR_SAT); + + // Remove temporary file + // DEBUG remove(smt_file); + + // Statistics + MaatStats::instance().done_solving(); + + return has_model; +} + +std::shared_ptr SolverBtor::get_model() +{ + return std::shared_ptr(_get_model_raw()); +} + +VarContext* SolverBtor::_get_model_raw() +{ + if (not has_model) + return nullptr; + + // TODO(boyan): don't hardcode + if (model_file == nullptr) + { + model_file = tmpnam(NULL); // Get temp name + if (model_file == nullptr) + throw solver_exception("SolverBtor::_get_model_raw(): couldn't create temporary filename"); + } + FILE* f = fopen(model_file, "w"); + boolector_print_model(btor, "smt2", f); + fclose(f); + + std::ifstream in(model_file, std::ios::binary); + std::vector data( + (std::istreambuf_iterator(in)), + (std::istreambuf_iterator()) + ); + std::vector clean_data{'(', 'm', 'o', 'd', 'e', 'l', '\n'}; + for (int i = 2; i < data.size(); i++) + { + // DEBUG remove false?? + if ( + false && i+2 < data.size() && data[i] == '\n' + && data[i+1] == ' ' && data[i+2] == ' ' + ){ + clean_data.push_back('\n'); + i += 2; + } + else + clean_data.push_back(data[i]); + } + remove(model_file); + ctx_from_smt2(clean_data.data()); +} + +} // namespace solver +} // namespace maat +#endif // #ifdef MAAT_BOOLECTOR_BACKEND diff --git a/src/solver/solver_z3.cpp b/src/solver/solver_z3.cpp index c42af90d..c052998e 100644 --- a/src/solver/solver_z3.cpp +++ b/src/solver/solver_z3.cpp @@ -205,16 +205,12 @@ std::shared_ptr SolverZ3::get_model() return std::shared_ptr(_get_model_raw()); } -VarContext* SolverZ3::_get_model_raw() +VarContext* z3_model_to_varcontext(z3::model& m, z3::context& ctx) { - if (not has_model) - return nullptr; - - z3::model m = sol->get_model(); - auto res = new VarContext(_model_id_cnt++); + auto res = new VarContext(); for (int i = 0; i < m.num_consts(); i++) { - size_t size = Z3_get_bv_sort_size(*ctx, m.get_const_interp(m[i]).get_sort()); + size_t size = Z3_get_bv_sort_size(ctx, m.get_const_interp(m[i]).get_sort()); Number val(size); if (size <= 64) val.set_cst(m.get_const_interp(m[i]).get_numeral_uint64()); @@ -229,6 +225,37 @@ VarContext* SolverZ3::_get_model_raw() return res; } +VarContext* SolverZ3::_get_model_raw() +{ + if (not has_model) + return nullptr; + + z3::model m = sol->get_model(); + return z3_model_to_varcontext(m, *ctx); +} + +VarContext* ctx_from_smt2(const char* string) +{ + auto ctx = new z3::context(); + auto sol = new z3::solver(*ctx); + std::cout << "DEBUG smt2 string: \n" << string << "\n"; + sol->from_string(string); + switch (sol->check()) + { + case z3::check_result::sat: + break; + default: + throw solver_exception("ctx_from_smt2: z3 failed to compute model"); + } + z3::model m = sol->get_model(); + std::cout << "DEBUG z3 model " << m << "\n"; + VarContext* res = z3_model_to_varcontext(m, *ctx); + std::cout << "DEBUG ctx " << *res << "\n"; + delete sol; + delete ctx; + return res; +} + } // namespace solver } // namespace maat #endif // #ifdef MAAT_Z3_BACKEND