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

@@ -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<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;
+}
+
+/// 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<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();
+private:
+    void reset_btor();
+};
 #endif
 
 /** \} */ // doxygen groupe Solver

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<std::string> contained_vars() const; ///< Return the contained symbolic variables
+
 public:
     virtual serial::uid_t class_uid() const;
     virtual void dump(serial::Serializer& s) const;

src/solver/solver.cpp

@@ -25,7 +25,8 @@ bool Solver::did_time_out() const
 std::unique_ptr<Solver> new_solver()
 {
 #ifdef MAAT_Z3_BACKEND
-    return std::make_unique<SolverZ3>();
+    // DEBUG return std::make_unique<SolverZ3>();
+    return std::make_unique<SolverBtor>();
 #else
     return nullptr;
 #endif

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 <fstream>
+
+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<VarContext> SolverBtor::get_model()
+{
+    return std::shared_ptr<VarContext>(_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<char> data(
+        (std::istreambuf_iterator<char>(in)),
+        (std::istreambuf_iterator<char>())
+    );
+    std::vector<char> 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