Support multiple solver backends

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)

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)

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

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<Constraint> 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
 

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<Value>&);
 PyObject* native_to_py(const std::unordered_set<Constraint>& 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<Constraint>& 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);

bindings/python/util.cpp

@@ -48,6 +48,23 @@ PyObject* native_to_py(const std::unordered_set<Constraint>& constraints)
     return list;
 }
 
+PyObject* py_to_native(PyObject* list, std::vector<Constraint>& 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)

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)

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

src/include/maat/solver.hpp

@@ -14,7 +14,7 @@ namespace maat
 
 namespace solver
 {
-    
+
 /** \defgroup solver Solver
  * \brief The Maat's constraint solver interface */
 
@@ -78,6 +78,40 @@ class SolverZ3 : public Solver
     virtual std::shared_ptr<VarContext> 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<ELEM>> class C>
+std::string constraints_to_smt2(const C<Constraint>& 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;
+}
+#endif
+
+#ifdef MAAT_BOOLECTOR_BACKEND
+class SolverBtor : public Solver
+{
+private:
+    std::list<Constraint> 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<VarContext> get_model();
+    virtual VarContext* _get_model_raw();
+};
 #endif
 
 /** \} */ // doxygen groupe Solver

src/solver/solver_btor.cpp

@@ -0,0 +1,68 @@
+#ifdef MAAT_BOOLECTOR_BACKEND
+
+#include "maat/solver.hpp"
+#include "maat/stats.hpp"
+#include "maat/exception.hpp"
+
+namespace maat
+{
+namespace solver
+{
+
+SolverBtor::SolverBtor(): Solver(), has_model(false)
+{}
+
+SolverBtor::~SolverBtor()
+{}
+
+void SolverBtor::reset()
+{
+    constraints.clear();
+    has_model = false;
+    _did_time_out = false;
+}
+
+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;
+
+    // Statistics
+    MaatStats::instance().start_solving();
+
+    // TODO 
+
+    // Statistics
+    MaatStats::instance().done_solving();
+
+    return has_model;
+}
+
+std::shared_ptr<VarContext> SolverBtor::get_model()
+{
+    return std::shared_ptr<VarContext>(_get_model_raw());
+}
+
+VarContext* SolverBtor::_get_model_raw()
+{
+    if (not has_model)
+        return nullptr;
+
+    // TODO
+}
+
+} // namespace solver
+} // namespace maat
+#endif // #ifdef MAAT_BOOLECTOR_BACKEND