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