BinarySmtSolver.h

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

#ifndef __STDC_FORMAT_MACROS
#define __STDC_FORMAT_MACROS
#endif

#include <BinarySymbolicExpr.h>
#include <boost/chrono.hpp>
#include <boost/lexical_cast.hpp>
#include <boost/noncopyable.hpp>
#include <boost/serialization/access.hpp>
#include <boost/thread/mutex.hpp>
#include <boost/unordered_map.hpp>
#include <inttypes.h>

namespace Rose {
namespace BinaryAnalysis {

using SmtSolverPtr = std::shared_ptr<class SmtSolver>;

class CompareLeavesByName {
public:
    bool operator()(const SymbolicExpr::LeafPtr&, const SymbolicExpr::LeafPtr&) const;
};

class SmtSolver: private boost::noncopyable {
public:
    using Ptr = SmtSolverPtr;

    typedef std::map<std::string, bool> Availability;

    enum LinkMode {
        LM_NONE       = 0x0000,                         
        LM_LIBRARY    = 0x0001,                         
        LM_EXECUTABLE = 0x0002,                         
        LM_ANY        = 0x0003,                         
    };

    enum Type { NO_TYPE, BOOLEAN, BIT_VECTOR, MEM_STATE };

    typedef std::pair<std::string, Type> StringTypePair;
    typedef Sawyer::Container::Map<SymbolicExpr::Ptr, StringTypePair> TermNames;

    typedef Sawyer::Container::Map<SymbolicExpr::Ptr, SymbolicExpr::Ptr> ExprExprMap;

    struct Exception: std::runtime_error {
        Exception(const std::string &mesg): std::runtime_error(mesg) {}
        ~Exception() throw () {}
    };

    struct ParseError: Exception {
        ParseError(const std::pair<size_t /*line*/, size_t /*col*/> &loc, const std::string &mesg)
            : Exception("input line " + boost::lexical_cast<std::string>(loc.first+1) +
                        " column " + boost::lexical_cast<std::string>(loc.second+1) + ": " + mesg) {}
        ~ParseError() throw () {}
    };

    enum Satisfiable { SAT_NO=0,                        
                       SAT_YES,                         
                       SAT_UNKNOWN                      
    };

    struct Stats {
        size_t ncalls;                                  
        size_t input_size;                              
        size_t output_size;                             
        size_t memoizationHits;                         
        size_t nSolversCreated;                         
        size_t nSolversDestroyed;                       
        double prepareTime;                             
        double solveTime;                               
        double evidenceTime;                            
        size_t nSatisfied;                              
        size_t nUnsatisfied;                            
        size_t nUnknown;                                
        // Remember to add all data members to resetStatistics()

        Stats()
            : ncalls(0), input_size(0), output_size(0), memoizationHits(0), nSolversCreated(0), nSolversDestroyed(0),
              prepareTime(0.0), solveTime(0.0), evidenceTime(0.0), nSatisfied(0), nUnsatisfied(0), nUnknown(0) {
        }
    };

    class Transaction {
        SmtSolver::Ptr solver_;
        size_t nLevels_;
        bool committed_;
    public:
        explicit Transaction(const SmtSolver::Ptr &solver)
            : solver_(solver), committed_(false) {
            if (solver) {
                nLevels_ = solver->nLevels();
                solver->push();
            } else {
                nLevels_ = 0;
            }
        }

        ~Transaction() {
            if (solver_ && !committed_) {
                ASSERT_require2(solver_->nLevels() > nLevels_, "something popped this transaction already");
                while (solver_->nLevels() > nLevels_) {
                    if (solver_->nLevels() > 1) {
                        solver_->pop();
                    } else {
                        solver_->reset();
                    }
                }
            }
        }

        void commit(bool b = true) {
            committed_ = b;
        }

        bool isCommitted() const {
            return committed_;
        }

        SmtSolver::Ptr solver() const {
            return solver_;
        }
    };
    
    typedef Sawyer::Container::Set<SymbolicExpr::LeafPtr, CompareLeavesByName> VariableSet;

    typedef std::set<uint64_t> Definitions;             
    class SExpr: public Sawyer::SmallObject, public Sawyer::SharedObject {
    public:
        typedef Sawyer::SharedPointer<SExpr> Ptr;
    private:
        explicit SExpr(const std::string &content): content_(content) {}
        std::string content_;
        std::vector<Ptr> children_;
    public:
        static Ptr instance(const std::string &content); // leaf node
        static Ptr instance(size_t);                    // integer leaf node
        static Ptr instance(const Ptr &a = Ptr(), const Ptr &b = Ptr(), const Ptr &c = Ptr(), const Ptr &d = Ptr());

        const std::string name() const { return content_; }
        const std::vector<Ptr>& children() const { return children_; }
        std::vector<Ptr>& children() { return children_; }
        void append(const std::vector<Ptr>&);
        void print(std::ostream&) const;
    };

    typedef std::pair<SExpr::Ptr, Type> SExprTypePair;

    typedef boost::unordered_map<SymbolicExpr::Hash, Satisfiable> Memoization;

private:
    std::string name_;
    std::vector<std::vector<SymbolicExpr::Ptr> > stack_;
    bool errorIfReset_;

protected:
    LinkMode linkage_;
    std::string outputText_;                            
    std::vector<SExpr::Ptr> parsedOutput_;              // the evidence output
    TermNames termNames_;                               // maps ROSE exprs to SMT exprs and their basic type
    Memoization memoization_;                           // cached of previously computed results
    bool doMemoization_;                                // use the memoization_ table?
    SymbolicExpr::Hash latestMemoizationId_;            // key for last found or inserted memoization, or zero
    SymbolicExpr::ExprExprHashMap latestMemoizationRewrite_; // variables rewritten, need to be undone when parsing evidence

    // Statistics
    static boost::mutex classStatsMutex;
    static Stats classStats;                            // all access must be protected by classStatsMutex
    Stats stats;

public:
    static Sawyer::Message::Facility mlog;

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_NVP(name_);
        s & BOOST_SERIALIZATION_NVP(stack_);
        // linkage_                  -- not serialized
        // termNames_                -- not serialized
        // outputText_               -- not serialized
        // parsedOutput_             -- not serialized
        // termNames_                -- not serialized
        // memoization_              -- not serialized
        // doMemoization_            -- not serialized
        // latestMemoizationId_      -- not serialized
        // latestMemoizationRewrite_ -- not serialized
        // classStatsMutex           -- not serialized
        // classStats                -- not serialized
        // stats                     -- not serialized
        // mlog                      -- not serialized
    }
#endif

protected:
    SmtSolver(const std::string &name, unsigned linkages)
        : name_(name), errorIfReset_(false), linkage_(LM_NONE), doMemoization_(true), latestMemoizationId_(0) {
        init(linkages);
    }
    
public:
    virtual Ptr create() const = 0;

    // Solvers are reference counted and should not be explicitly deleted.
    virtual ~SmtSolver();


    // Methods for creating solvers.
public:

    static Availability availability();

    static Ptr instance(const std::string &name);

    static Ptr bestAvailable();

    const std::string& name() const { return name_; }
    void name(const std::string &s) { name_ = s; }
    LinkMode linkage() const {
        return linkage_;
    }

    void requireLinkage(LinkMode) const;

    static LinkMode bestLinkage(unsigned linkages);

    bool memoization() const { return doMemoization_; }
    void memoization(bool b) {
        doMemoization_ = b;
        if (!b)
            clearMemoization();
    }
    SymbolicExpr::Hash latestMemoizationId() const {
        return latestMemoizationId_;
    }
    
    virtual void clearMemoization() {
        memoization_.clear();
    }

    virtual size_t memoizationNEntries() const {
        return memoization_.size();
    }

    virtual void timeout(boost::chrono::duration<double> seconds) = 0;

    
    // High-level abstraction for testing satisfiability.
public:

    virtual Satisfiable triviallySatisfiable(const std::vector<SymbolicExpr::Ptr> &exprs);

    virtual Satisfiable satisfiable(const SymbolicExpr::Ptr&);
    virtual Satisfiable satisfiable(const std::vector<SymbolicExpr::Ptr>&);
    // Mid-level abstractions for testing satisfiaiblity.
public:

    virtual void reset();

    bool errorIfReset() const {
        return errorIfReset_;
    }
    void errorIfReset(bool b) {
        errorIfReset_ = b;
    }
    virtual void push();

    virtual void pop();

    virtual size_t nLevels() const { return stack_.size(); }

    virtual size_t nAssertions(size_t backtrackingLevel);

    virtual size_t nAssertions() const;
    
    virtual void insert(const SymbolicExpr::Ptr&);
    virtual void insert(const std::vector<SymbolicExpr::Ptr>&);
    virtual std::vector<SymbolicExpr::Ptr> assertions() const;

    virtual std::vector<SymbolicExpr::Ptr> assertions(size_t level) const;

    virtual Satisfiable check();

    virtual Satisfiable checkTrivial();


    // High-level abstraction for solver results.
public:

    virtual std::vector<std::string> evidenceNames() {
        return std::vector<std::string>();
    }

    virtual SymbolicExpr::Ptr evidenceForName(const std::string&) {
        return SymbolicExpr::Ptr();
    }


    // Mid-level abstraction for solver results.
public:

    virtual void clearEvidence();

    virtual SymbolicExpr::Ptr evidenceForVariable(const SymbolicExpr::Ptr &var) {
        SymbolicExpr::LeafPtr ln = var->isLeafNode();
        ASSERT_require(ln && ln->isVariable2());
        return evidenceForVariable(ln->nameId());
    }
    virtual SymbolicExpr::Ptr evidenceForVariable(uint64_t varno) {
        char buf[64];
        snprintf(buf, sizeof buf, "v%" PRIu64, varno);
        return evidenceForName(buf);
    }
    virtual SymbolicExpr::Ptr evidenceForAddress(uint64_t addr);


    // Statistics
public:

    const Stats& statistics() const { return stats; }

    static Stats classStatistics();

    void resetStatistics();

    static void resetClassStatistics();


    // Low-level API used in subclasses.
protected:
    virtual Satisfiable checkExe();

    virtual Satisfiable checkLib();

    virtual std::string getErrorMessage(int exitStatus);

    virtual void findVariables(const SymbolicExpr::Ptr&, VariableSet&) {}

    static void printSExpression(std::ostream&, const SExpr::Ptr&);

    virtual void generateFile(std::ostream&, const std::vector<SymbolicExpr::Ptr> &exprs, Definitions*) = 0;

    virtual std::string getCommand(const std::string &config_name) = 0;

    std::vector<SExpr::Ptr> parseSExpressions(const std::string&);

    virtual void parseEvidence() {};

    static std::vector<SymbolicExpr::Ptr> normalizeVariables(const std::vector<SymbolicExpr::Ptr>&,
                                                             SymbolicExpr::ExprExprHashMap &index /*out*/);

    static std::vector<SymbolicExpr::Ptr> undoNormalization(const std::vector<SymbolicExpr::Ptr>&,
                                                            const SymbolicExpr::ExprExprHashMap &index);


    // Miscellaneous
public:
    virtual void selfTest();

    static void initDiagnostics();

private:
    void init(unsigned linkages);                       // Called during construction



    // Deprecated junk

    // FIXME[Robb Matzke 2017-10-17]: these are all deprecated
public:
    virtual Satisfiable trivially_satisfiable(const std::vector<SymbolicExpr::Ptr> &exprs)
        ROSE_DEPRECATED("use triviallySatisfiable");
    virtual SymbolicExpr::Ptr evidence_for_variable(uint64_t varno) ROSE_DEPRECATED("use evidenceForVariable");
    virtual SymbolicExpr::Ptr evidence_for_variable(const SymbolicExpr::Ptr &var) ROSE_DEPRECATED("use evidenceForVariable");
    virtual SymbolicExpr::Ptr evidence_for_name(const std::string&) ROSE_DEPRECATED("use evidenceForName");
    virtual SymbolicExpr::Ptr evidence_for_address(uint64_t addr) ROSE_DEPRECATED("use evidenceForAddress");
    virtual std::vector<std::string> evidence_names() ROSE_DEPRECATED("use evidenceNames");
    virtual void clear_evidence() ROSE_DEPRECATED("use clearEvidence");
    const Stats& get_stats() const ROSE_DEPRECATED("use statistics");
    static Stats get_class_stats() ROSE_DEPRECATED("use classStatistics");
    void reset_stats() ROSE_DEPRECATED("use resetStatistics");
    void reset_class_stats() ROSE_DEPRECATED("use resetClassStatistics");
protected:
    virtual void generate_file(std::ostream&, const std::vector<SymbolicExpr::Ptr> &exprs, Definitions*)
        ROSE_DEPRECATED("use generateFile");
    virtual std::string get_command(const std::string &config_name) ROSE_DEPRECATED("use getCommand");
    virtual void parse_evidence() ROSE_DEPRECATED("use parseEvidence");
};

std::ostream& operator<<(std::ostream&, const SmtSolver::SExpr&);

// FIXME[Robb Matzke 2017-10-17]: This typedef is deprecated. Use SmtSolver instead.
typedef SmtSolver SMTSolver;

} // namespace
} // namespace

#endif
#endif