SmtSolver.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 <Rose/BinaryAnalysis/SymbolicExpression.h>
#include <Rose/Exception.h>
#include <Rose/Progress.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 <inttypes.h>
#include <unordered_map>

namespace Rose {
namespace BinaryAnalysis {

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

class CompareRawLeavesByName {
public:
    bool operator()(const SymbolicExpression::Leaf*, const SymbolicExpression::Leaf*) const;
};

class SmtSolver: private boost::noncopyable {
public:
    using ExprList = std::vector<SymbolicExpression::Ptr>;

    using Ptr = SmtSolverPtr;

    using Availability = std::map<std::string, bool>;

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

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

    using StringTypePair = std::pair<std::string, Type>;
    using TermNames = Sawyer::Container::Map<SymbolicExpression::Ptr, StringTypePair>;

    using ExprExprMap = Sawyer::Container::Map<SymbolicExpression::Ptr, SymbolicExpression::Ptr>;

    struct Exception: Rose::Exception {
        Exception(const std::string &mesg): Rose::Exception(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 = 0;                              
        size_t input_size = 0;                          
        size_t output_size = 0;                         
        size_t memoizationHits = 0;                     
        size_t nSolversCreated = 0;                     
        size_t nSolversDestroyed = 0;                   
        double prepareTime = 0.0;                       
        double longestPrepareTime = 0.0;                
        double solveTime = 0.0;                         
        double longestSolveTime = 0.0;                  
        double evidenceTime = 0.0;                      
        double longestEvidenceTime = 0.0;               
        size_t nSatisfied = 0;                          
        size_t nUnsatisfied = 0;                        
        size_t nUnknown = 0;                            
        // Remember to add all data members to SmtSolver::resetStatistics() and SmtSolver::Stats::print()

        void print(std::ostream&, const std::string &prefix = "") const;
    };

    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_;
        }
    };

    using VariableSet = Sawyer::Container::Set<SymbolicExpression::LeafPtr, CompareLeavesByName>;

    using Definitions = std::set<uint64_t>;             
    class SExpr: public Sawyer::SmallObject, public Sawyer::SharedObject {
    public:
        using Ptr = Sawyer::SharedPointer<SExpr>;
    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;
    };

    using SExprTypePair = std::pair<SExpr::Ptr, Type>;

    class Memoizer: public Sawyer::SharedObject {
    public:
        using Ptr = Sawyer::SharedPointer<Memoizer>;

        /* Return value from @ref find function. */
        struct Found {
            Sawyer::Optional<Satisfiable> satisfiable;      
            ExprList sortedNormalized;                      
            SymbolicExpression::ExprExprHashMap rewriteMap; 
            ExprExprMap evidence;                           
            explicit operator bool() const {
                return satisfiable;
            }
        };

    private:
        using ExprExpr = std::pair<SymbolicExpression::Ptr, SymbolicExpression::Ptr>;

        // The thing that is memoized
        struct Record {
            ExprList assertions;                        // "find" inputs, sorted and normalized
            Satisfiable satisfiable;                    // main output of SMT solver
            ExprExprMap evidence;                       // output if satisfied: sorted and normalized
        };

        // Mapping from hash of sorted-normalized assertions to the memoization record.
        using Map = std::multimap<SymbolicExpression::Hash, Record>;

    private:
        mutable SAWYER_THREAD_TRAITS::Mutex mutex_;     // protects the following data members
        Map map_;                                       // memoization records indexed by hash of sorted-normalized assertions

    protected:
        Memoizer() {}

    public:
        static Ptr instance();

        void clear();

        Found find(const ExprList &assertions);

        ExprExprMap evidence(const Found&) const;

        void insert(const Found&, Satisfiable, const ExprExprMap &evidence);

        size_t size() const;

    public:
        // Non-synchronized search for the sorted-normalized assertions which have the specified hash.
        Map::iterator searchNS(SymbolicExpression::Hash, const ExprList &sortedNormalized);
    };

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

protected:
    LinkMode linkage_;
    std::string outputText_;                            
    std::vector<SExpr::Ptr> parsedOutput_;              // the evidence output
    ExprExprMap evidence_;                              // evidence for last check() if satisfiable
    TermNames termNames_;                               // maps ROSE exprs to SMT exprs and their basic type
    Memoizer::Ptr memoizer_;                            // cache of previously computed results
    Progress::Ptr progress_;                            // optional progress reporting

    // 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
        // memoizer_                 -- 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) {
        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);

    Memoizer::Ptr memoizer() const;
    void memoizer(const Memoizer::Ptr&);
    virtual void timeout(boost::chrono::duration<double> seconds) = 0;

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

    virtual Satisfiable triviallySatisfiable(const ExprList &exprs);

    virtual Satisfiable satisfiable(const SymbolicExpression::Ptr&);
    virtual Satisfiable satisfiable(const ExprList&);
    // 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 SymbolicExpression::Ptr&);
    virtual void insert(const ExprList&);
    virtual ExprList assertions() const;

    virtual const ExprList& assertions(size_t level) const;

    virtual Satisfiable check();

    virtual Satisfiable checkTrivial();


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

    using Evidence = Sawyer::Container::Map<std::string /*variable name*/, SymbolicExpression::Ptr /*value*/>;

    virtual std::vector<std::string> evidenceNames() const;

    virtual SymbolicExpression::Ptr evidenceForName(const std::string&) const;

    Evidence evidenceByName() const;
    ExprExprMap evidence() const;
    // Mid-level abstraction for solver results.
public:

    virtual void clearEvidence();

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


    // Statistics
public:

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

    static Stats classStatistics();

    void resetStatistics();

    static void resetClassStatistics();

    Progress::Ptr progress() const;
    void progress(const Progress::Ptr &progress);
    // Low-level API used in subclasses and sometimes for debugging
public:
    virtual void generateFile(std::ostream&, const ExprList &exprs, Definitions*) = 0;

protected:
    virtual Satisfiable checkExe();

    virtual Satisfiable checkLib();

    virtual std::string getErrorMessage(int exitStatus);

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

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

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

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

    virtual void parseEvidence() {};

    static ExprList normalizeVariables(const ExprList&, SymbolicExpression::ExprExprHashMap &index /*out*/);

    static ExprList undoNormalization(const ExprList&, const SymbolicExpression::ExprExprHashMap &index);


    // Miscellaneous
public:
    virtual void selfTest();

    static void initDiagnostics();

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

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

} // namespace
} // namespace

#endif
#endif