BinaryZ3Solver.h

#ifndef Rose_BinaryAnalysis_Z3Solver_H
#define Rose_BinaryAnalysis_Z3Solver_H
#include <featureTests.h>
#ifdef ROSE_ENABLE_BINARY_ANALYSIS

#include <BinarySmtlibSolver.h>
#ifdef ROSE_HAVE_Z3
#include <z3++.h>
#endif
#ifdef ROSE_HAVE_Z3_VERSION_H
#include <z3_version.h>
#endif

#ifndef ROSE_Z3
#define ROSE_Z3 ""
#endif

#include <boost/serialization/access.hpp>

namespace Rose {
namespace BinaryAnalysis {

class Z3Solver: public SmtlibSolver {
#ifdef ROSE_HAVE_Z3
public:
    typedef std::pair<z3::expr, Type> Z3ExprTypePair;
private:
    z3::context *ctx_;
    z3::solver *solver_;
    std::vector<std::vector<z3::expr> > z3Stack_;       // lazily parallel with parent class' "stack_" data member
    typedef Sawyer::Container::Map<SymbolicExpr::Ptr, Z3ExprTypePair> CommonSubexpressions;
    CommonSubexpressions ctxCses_; // common subexpressions
    typedef Sawyer::Container::Map<SymbolicExpr::LeafPtr, z3::func_decl, CompareLeavesByName> VariableDeclarations;
    VariableDeclarations ctxVarDecls_;
#endif

private:
#ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
    friend class boost::serialization::access;

    template<class S>
    void serialize(S &s, const unsigned /*version*/) {
        s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(SmtSolver);
        // ctx_         -- not serialized
        // solver_      -- not serialized
        // z3Stack_     -- not serialized
        // ctxCses_     -- not serialized
        // ctxVarDecls_ -- not serialized
    }
#endif

protected:
    // Reference counted object. Use instance or create instead.
    explicit Z3Solver(unsigned linkages = LM_ANY)
        : SmtlibSolver("z3", ROSE_Z3, "", linkages & availableLinkages())
#ifdef ROSE_HAVE_Z3
          , ctx_(NULL), solver_(NULL)
#endif
    {
#ifdef ROSE_HAVE_Z3
        ctx_ = new z3::context;
        solver_ = new z3::solver(*ctx_);
        z3Stack_.push_back(std::vector<z3::expr>());
#endif
    }

public:
    ~Z3Solver() {
#ifdef ROSE_HAVE_Z3
        ctxVarDecls_.clear();
        ctxCses_.clear();
        z3Stack_.clear();
        delete solver_;
        delete ctx_;
#endif
    }

public:
    static Ptr instance(unsigned linkages = LM_ANY) {
        return Ptr(new Z3Solver(linkages));
    }

    virtual Ptr create() const ROSE_OVERRIDE {
        return Ptr(instance(linkage()));
    }

    explicit Z3Solver(const boost::filesystem::path &exe, const std::string &shellArgs = "")
        : SmtlibSolver("Z3", exe, shellArgs) {}
    
    static unsigned availableLinkages();

#ifdef ROSE_HAVE_Z3

    virtual z3::context *z3Context() const;

    virtual z3::solver *z3Solver() const;

    virtual std::vector<z3::expr> z3Assertions() const;
    virtual std::vector<z3::expr> z3Assertions(size_t level) const;
#endif

    virtual void z3Update();

protected:
    SExprTypePair outputList(const std::string &name, const SymbolicExpr::InteriorPtr&, Type rettype = NO_TYPE);
    SExprTypePair outputList(const std::string &name, const std::vector<SExprTypePair>&, Type rettype = NO_TYPE);

    // Overrides
public:
    virtual Satisfiable checkLib() ROSE_OVERRIDE;
    virtual void reset() ROSE_OVERRIDE;
    virtual void clearEvidence() ROSE_OVERRIDE;
    virtual void parseEvidence() ROSE_OVERRIDE;
    virtual void pop() ROSE_OVERRIDE;
    virtual void selfTest() ROSE_OVERRIDE;
    virtual void timeout(boost::chrono::duration<double>) ROSE_OVERRIDE;
protected:
    virtual void outputBvxorFunctions(std::ostream&, const std::vector<SymbolicExpr::Ptr>&) ROSE_OVERRIDE;
    virtual void outputComparisonFunctions(std::ostream&, const std::vector<SymbolicExpr::Ptr>&) ROSE_OVERRIDE;
    virtual SExprTypePair outputExpression(const SymbolicExpr::Ptr&) ROSE_OVERRIDE;
    virtual SExprTypePair outputArithmeticShiftRight(const SymbolicExpr::InteriorPtr&) ROSE_OVERRIDE;

#ifdef ROSE_HAVE_Z3
protected:
    virtual Type mostType(const std::vector<Z3ExprTypePair>&);
    using SmtlibSolver::mostType;
    Z3ExprTypePair ctxCast(const Z3ExprTypePair&, Type toType);
    std::vector<Z3Solver::Z3ExprTypePair> ctxCast(const std::vector<Z3ExprTypePair>&, Type toType);
    Z3ExprTypePair ctxLeaf(const SymbolicExpr::LeafPtr&);
    Z3ExprTypePair ctxExpression(const SymbolicExpr::Ptr&);
    std::vector<Z3Solver::Z3ExprTypePair> ctxExpressions(const std::vector<SymbolicExpr::Ptr>&);
    void ctxVariableDeclarations(const VariableSet&);
    void ctxCommonSubexpressions(const SymbolicExpr::Ptr&);
    Z3ExprTypePair ctxArithmeticShiftRight(const SymbolicExpr::InteriorPtr&);
    Z3ExprTypePair ctxExtract(const SymbolicExpr::InteriorPtr&);
    Z3ExprTypePair ctxRead(const SymbolicExpr::InteriorPtr&);
    Z3ExprTypePair ctxRotateLeft(const SymbolicExpr::InteriorPtr&);
    Z3ExprTypePair ctxRotateRight(const SymbolicExpr::InteriorPtr&);
    Z3ExprTypePair ctxSet(const SymbolicExpr::InteriorPtr&);
    Z3ExprTypePair ctxSignExtend(const SymbolicExpr::InteriorPtr&);
    Z3ExprTypePair ctxShiftLeft(const SymbolicExpr::InteriorPtr&);
    Z3ExprTypePair ctxShiftRight(const SymbolicExpr::InteriorPtr&);
    Z3ExprTypePair ctxMultiply(const SymbolicExpr::InteriorPtr&);
    Z3ExprTypePair ctxUnsignedDivide(const SymbolicExpr::InteriorPtr&);
    Z3ExprTypePair ctxSignedDivide(const SymbolicExpr::InteriorPtr&);
    Z3ExprTypePair ctxUnsignedExtend(const SymbolicExpr::InteriorPtr&);
    Z3ExprTypePair ctxUnsignedModulo(const SymbolicExpr::InteriorPtr&);
    Z3ExprTypePair ctxSignedModulo(const SymbolicExpr::InteriorPtr&);
    Z3ExprTypePair ctxWrite(const SymbolicExpr::InteriorPtr&);
    Z3ExprTypePair ctxZerop(const SymbolicExpr::InteriorPtr&);
#endif
};

} // namespace
} // namespace

#ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
BOOST_CLASS_EXPORT_KEY(Rose::BinaryAnalysis::Z3Solver);
#endif

#endif
#endif