FeasiblePath.h

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

#include <Rose/BinaryAnalysis/BasicTypes.h>
#include <Rose/BinaryAnalysis/InstructionSemantics/SymbolicSemantics.h>
#include <Rose/BinaryAnalysis/SmtSolver.h>
#include <Rose/BinaryAnalysis/SymbolicExpressionParser.h>
#include <Rose/BinaryAnalysis/Partitioner2/CfgPath.h>
#include <Rose/Exception.h>
#include <Sawyer/CommandLine.h>
#include <Sawyer/Message.h>
#include <boost/filesystem/path.hpp>
#include <boost/logic/tribool.hpp>

namespace Rose {
namespace BinaryAnalysis {

class FeasiblePath {
    //                                  Types and public data members
public:
    class Exception: public Rose::Exception {
    public:
        Exception(const std::string &what)
            : Rose::Exception(what) {}
        ~Exception() throw () {}
    };

    enum SearchMode {
        SEARCH_SINGLE_DFS,                              
        SEARCH_SINGLE_BFS,                              
        SEARCH_MULTI                                    
    };

    enum SemanticMemoryParadigm {
        LIST_BASED_MEMORY,                              
        MAP_BASED_MEMORY                                
    };

    enum EdgeVisitOrder {
        VISIT_NATURAL,                                  
        VISIT_REVERSE,                                  
        VISIT_RANDOM,                                   
    };

    enum IoMode { READ, WRITE };

    enum MayOrMust { MAY, MUST };

    typedef std::set<rose_addr_t> AddressSet;

    struct Expression {
        AddressIntervalSet location;                    
        std::string parsable;                           
        SymbolicExpressionPtr expr;                     
        Expression() {}
        /*implicit*/ Expression(const std::string &parsable): parsable(parsable) {}
        /*implicit*/ Expression(const SymbolicExpressionPtr &expr): expr(expr) {}

        void print(std::ostream&) const;
    };

    struct Settings {
        // Path feasibility
        SearchMode searchMode;                          
        Sawyer::Optional<rose_addr_t> initialStackPtr;  
        size_t maxVertexVisit;                          
        size_t maxPathLength;                           
        size_t maxCallDepth;                            
        size_t maxRecursionDepth;                       
        std::vector<Expression> assertions;             
        std::vector<std::string> assertionLocations;    
        std::vector<rose_addr_t> summarizeFunctions;    
        bool nonAddressIsFeasible;                      
        std::string solverName;                         
        SemanticMemoryParadigm memoryParadigm;          
        bool processFinalVertex;                        
        bool ignoreSemanticFailure;                     
        double kCycleCoefficient;                       
        EdgeVisitOrder edgeVisitOrder;                  
        bool trackingCodeCoverage;                      
        std::vector<rose_addr_t> ipRewrite;             
        Sawyer::Optional<boost::chrono::duration<double> > smtTimeout; 
        size_t maxExprSize;                             
        bool traceSemantics;                            
        // Null dereferences
        struct NullDeref {
            bool check;                                 
            MayOrMust mode;                             
            bool constOnly;                             
            rose_addr_t minValid;                       
            NullDeref()
                : check(false), mode(MUST), constOnly(false), minValid(1024) {}
        } nullDeref;                                    
        std::string exprParserDoc;                      
        Settings()
            : searchMode(SEARCH_SINGLE_DFS), maxVertexVisit((size_t)-1), maxPathLength(200), maxCallDepth((size_t)-1),
              maxRecursionDepth((size_t)-1), nonAddressIsFeasible(true), solverName("best"),
              memoryParadigm(LIST_BASED_MEMORY), processFinalVertex(false), ignoreSemanticFailure(false),
              kCycleCoefficient(0.0), edgeVisitOrder(VISIT_NATURAL), trackingCodeCoverage(true), maxExprSize(UNLIMITED),
              traceSemantics(false) {}
    };

    struct Statistics {
        size_t nPathsExplored;                          
        size_t maxVertexVisitHits;                      
        size_t maxPathLengthHits;                       
        size_t maxCallDepthHits;                        
        size_t maxRecursionDepthHits;                   
        Sawyer::Container::Map<rose_addr_t, size_t> reachedBlockVas; 
        Statistics()
            : nPathsExplored(0), maxVertexVisitHits(0), maxPathLengthHits(0), maxCallDepthHits(0), maxRecursionDepthHits(0) {}

        Statistics& operator+=(const Statistics&);
    };

    static Sawyer::Message::Facility mlog;

     RegisterDescriptor REG_PATH;

    struct VarDetail {
        std::string registerName;
        std::string firstAccessMode;                    
        SgAsmInstruction *firstAccessInsn;              
        Sawyer::Optional<size_t> firstAccessIdx;        
        SymbolicExpressionPtr memAddress;               
        size_t memSize;                                 
        size_t memByteNumber;                           
        Sawyer::Optional<rose_addr_t> returnFrom;       
        VarDetail(): firstAccessInsn(NULL), memSize(0), memByteNumber(0) {}
        std::string toString() const;
    };

    typedef Sawyer::Container::Map<std::string /*name*/, FeasiblePath::VarDetail> VarDetails;

    class PathProcessor {
    public:
        enum Action {
            BREAK,                                      
            CONTINUE                                    
        };

        virtual ~PathProcessor() {}

        virtual Action found(const FeasiblePath &analyzer, const Partitioner2::CfgPath &path,
                             const InstructionSemantics::BaseSemantics::DispatcherPtr &cpu,
                             const SmtSolverPtr &solver);

        virtual Action nullDeref(const FeasiblePath &analyzer, const Partitioner2::CfgPath &path, SgAsmInstruction *insn,
                                 const InstructionSemantics::BaseSemantics::RiscOperatorsPtr &cpu, const SmtSolverPtr &solver,
                                 IoMode ioMode, const InstructionSemantics::BaseSemantics::SValuePtr &addr);

        virtual Action memoryIo(const FeasiblePath &analyzer, const Partitioner2::CfgPath &path, SgAsmInstruction *insn,
                                const InstructionSemantics::BaseSemantics::RiscOperatorsPtr &cpu, const SmtSolverPtr &solver,
                                IoMode ioMode, const InstructionSemantics::BaseSemantics::SValuePtr &addr,
                                const InstructionSemantics::BaseSemantics::SValuePtr &value);
    };

    struct FunctionSummary {
        rose_addr_t address = 0;                            
        int64_t stackDelta = SgAsmInstruction::INVALID_STACK_DELTA; 
        std::string name;                               
        FunctionSummary();

        FunctionSummary(const Partitioner2::ControlFlowGraph::ConstVertexIterator &cfgFuncVertex, uint64_t stackDelta);
    };

    typedef Sawyer::Container::Map<rose_addr_t, FunctionSummary> FunctionSummaries;

    class FunctionSummarizer: public Sawyer::SharedObject {
    public:
        typedef Sawyer::SharedPointer<FunctionSummarizer> Ptr;
    protected:
        FunctionSummarizer() {}
    public:
        virtual void init(const FeasiblePath &analysis, FunctionSummary &summary /*in,out*/,
                          const Partitioner2::FunctionPtr &function,
                          Partitioner2::ControlFlowGraph::ConstVertexIterator cfgCallTarget) = 0;

        virtual bool process(const FeasiblePath &analysis, const FunctionSummary &summary,
                             const InstructionSemantics::SymbolicSemantics::RiscOperatorsPtr &ops) = 0;

        virtual InstructionSemantics::SymbolicSemantics::SValuePtr
        returnValue(const FeasiblePath &analysis, const FunctionSummary &summary,
                    const InstructionSemantics::SymbolicSemantics::RiscOperatorsPtr &ops) = 0;
    };

    //                                  Private data members
private:
    Partitioner2::PartitionerConstPtr partitioner_;     // binary analysis context, might be null
    RegisterDictionaryPtr registers_;                   // registers augmented with "path" pseudo-register
    RegisterDescriptor REG_RETURN_;                     // FIXME[Robb P Matzke 2016-10-11]: see source
    Settings settings_;
    FunctionSummaries functionSummaries_;
    Partitioner2::CfgVertexMap vmap_;                   // relates CFG vertices to path vertices
    Partitioner2::ControlFlowGraph paths_;              // all possible paths, feasible or otherwise
    Partitioner2::CfgConstVertexSet pathsBeginVertices_;// vertices of paths_ where searching starts
    Partitioner2::CfgConstVertexSet pathsEndVertices_;  // vertices of paths_ where searching stops
    bool isDirectedSearch_ = true;                      // use pathsEndVertices_?
    Partitioner2::CfgConstEdgeSet cfgAvoidEdges_;       // CFG edges to avoid
    Partitioner2::CfgConstVertexSet cfgEndAvoidVertices_;// CFG end-of-path and other avoidance vertices
    FunctionSummarizer::Ptr functionSummarizer_;        // user-defined function for handling function summaries
    InstructionSemantics::BaseSemantics::StatePtr initialState_; // set by setInitialState.
    static Sawyer::Attribute::Id POST_STATE;            // stores semantic state after executing the insns for a vertex
    static Sawyer::Attribute::Id POST_INSN_LENGTH;      // path length in instructions at end of vertex
    static Sawyer::Attribute::Id EFFECTIVE_K;           // (double) effective maximimum path length

    mutable SAWYER_THREAD_TRAITS::Mutex statsMutex_;    // protects the following data member
    Statistics stats_;                                  // statistical results of the analysis

    //                                  Construction, destruction
public:
    FeasiblePath();
    virtual ~FeasiblePath();

    void reset();

    void resetStatistics() {
        SAWYER_THREAD_TRAITS::LockGuard lock(statsMutex_);
        stats_ = Statistics();
    }

    static void initDiagnostics();


    //                                  Settings affecting behavior
public:
    const Settings& settings() const { return settings_; }
    Settings& settings() { return settings_; }
    void settings(const Settings &s) { settings_ = s; }
    static Sawyer::CommandLine::SwitchGroup commandLineSwitches(Settings &settings);

    static std::string expressionDocumentation();


    //                                  Overridable processing functions
public:
    virtual InstructionSemantics::BaseSemantics::DispatcherPtr
    buildVirtualCpu(const Partitioner2::PartitionerConstPtr&, const Partitioner2::CfgPath*, PathProcessor*, const SmtSolverPtr&);

    virtual void
    setInitialState(const InstructionSemantics::BaseSemantics::DispatcherPtr &cpu,
                    const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathsBeginVertex);

    virtual void
    processBasicBlock(const Partitioner2::BasicBlockPtr &bblock,
                      const InstructionSemantics::BaseSemantics::DispatcherPtr &cpu, size_t pathInsnIndex);

    virtual void
    processIndeterminateBlock(const Partitioner2::ControlFlowGraph::ConstVertexIterator &vertex,
                              const InstructionSemantics::BaseSemantics::DispatcherPtr &cpu,
                              size_t pathInsnIndex);

    virtual void
    processFunctionSummary(const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathsVertex,
                           const InstructionSemantics::BaseSemantics::DispatcherPtr &cpu,
                           size_t pathInsnIndex);

    virtual void
    processVertex(const InstructionSemantics::BaseSemantics::DispatcherPtr &cpu,
                  const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathsVertex,
                  size_t pathInsnIndex);

    virtual bool
    shouldSummarizeCall(const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathVertex,
                        const Partitioner2::ControlFlowGraph &cfg,
                        const Partitioner2::ControlFlowGraph::ConstVertexIterator &cfgCallTarget);

    virtual bool
    shouldInline(const Partitioner2::CfgPath &path, const Partitioner2::ControlFlowGraph::ConstVertexIterator &cfgCallTarget);

    FunctionSummarizer::Ptr functionSummarizer() const { return functionSummarizer_; }
    void functionSummarizer(const FunctionSummarizer::Ptr &f) { functionSummarizer_ = f; }
    //                                  Utilities
public:
    Partitioner2::ControlFlowGraph::ConstVertexIterator
    pathToCfg(const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathVertex) const;

    Partitioner2::CfgConstVertexSet
    cfgToPaths(const Partitioner2::CfgConstVertexSet&) const;

    Partitioner2::CfgConstEdgeSet
    cfgToPaths(const Partitioner2::CfgConstEdgeSet&) const;

    bool pathEndsWithFunctionCall(const Partitioner2::CfgPath&) const;

    bool isFunctionCall(const Partitioner2::ControlFlowGraph::ConstVertexIterator&) const;

    void printPathVertex(std::ostream &out, const Partitioner2::ControlFlowGraph::Vertex &pathVertex,
                         size_t &insnIdx /*in,out*/) const;

    void printPath(std::ostream &out, const Partitioner2::CfgPath&) const;

    bool isAnyEndpointReachable(const Partitioner2::ControlFlowGraph &cfg,
                                const Partitioner2::ControlFlowGraph::ConstVertexIterator &beginVertex,
                                const Partitioner2::CfgConstVertexSet &endVertices);

    //                                  Functions for describing the search space
public:

    void
    setSearchBoundary(const Partitioner2::PartitionerConstPtr &partitioner,
                      const Partitioner2::CfgConstVertexSet &cfgBeginVertices,
                      const Partitioner2::CfgConstVertexSet &cfgEndVertices,
                      const Partitioner2::CfgConstVertexSet &cfgAvoidVertices = Partitioner2::CfgConstVertexSet(),
                      const Partitioner2::CfgConstEdgeSet &cfgAvoidEdges = Partitioner2::CfgConstEdgeSet());
    void
    setSearchBoundary(const Partitioner2::PartitionerConstPtr &partitioner,
                      const Partitioner2::ControlFlowGraph::ConstVertexIterator &cfgBeginVertex,
                      const Partitioner2::ControlFlowGraph::ConstVertexIterator &cfgEndVertex,
                      const Partitioner2::CfgConstVertexSet &cfgAvoidVertices = Partitioner2::CfgConstVertexSet(),
                      const Partitioner2::CfgConstEdgeSet &cfgAvoidEdges = Partitioner2::CfgConstEdgeSet());
    void
    setSearchBoundary(const Partitioner2::PartitionerConstPtr &partitioner,
                      const Partitioner2::CfgConstVertexSet &cfgBeginVertices,
                      const Partitioner2::CfgConstVertexSet &cfgAvoidVertices = Partitioner2::CfgConstVertexSet(),
                      const Partitioner2::CfgConstEdgeSet &cfgAvoidEdges = Partitioner2::CfgConstEdgeSet());
    void
    setSearchBoundary(const Partitioner2::PartitionerConstPtr &partitioner,
                      const Partitioner2::ControlFlowGraph::ConstVertexIterator &cfgBeginVertex,
                      const Partitioner2::CfgConstVertexSet &cfgAvoidVertices = Partitioner2::CfgConstVertexSet(),
                      const Partitioner2::CfgConstEdgeSet &cfgAvoidEdges = Partitioner2::CfgConstEdgeSet());
    bool isDirectedSearch() const {
        return isDirectedSearch_;
    }

    //                                  Functions for searching for paths
public:
    void depthFirstSearch(PathProcessor &pathProcessor);


    //                                  Functions for getting the results
public:
    Partitioner2::PartitionerConstPtr partitioner() const;

    const FunctionSummaries& functionSummaries() const {
        return functionSummaries_;
    }

    const FunctionSummary& functionSummary(rose_addr_t entryVa) const;

    const VarDetail& varDetail(const InstructionSemantics::BaseSemantics::StatePtr&, const std::string &varName) const;

    const VarDetails& varDetails(const InstructionSemantics::BaseSemantics::StatePtr&) const;

    InstructionSemantics::BaseSemantics::StatePtr initialState() const;

    static InstructionSemantics::BaseSemantics::StatePtr pathPostState(const Partitioner2::CfgPath&, size_t vertexIdx);

    double pathEffectiveK(const Partitioner2::CfgPath&) const;

    static size_t pathLength(const Partitioner2::CfgPath&, int position = -1);

    Statistics statistics() const {
        SAWYER_THREAD_TRAITS::LockGuard lock(statsMutex_);
        return stats_;
    }

    //                                  Private supporting functions
private:
    // Check that analysis settings are valid, or throw an exception.
    void checkSettings() const;

    static rose_addr_t virtualAddress(const Partitioner2::ControlFlowGraph::ConstVertexIterator &vertex);

    void insertCallSummary(const Partitioner2::ControlFlowGraph::ConstVertexIterator &pathsCallSite,
                           const Partitioner2::ControlFlowGraph &cfg,
                           const Partitioner2::ControlFlowGraph::ConstEdgeIterator &cfgCallEdge);

    boost::filesystem::path emitPathGraph(size_t callId, size_t graphId);  // emit paths graph to "rose-debug" directory

    // Pop an edge (or more) from the path and follow some other edge.  Also, adjust the SMT solver's stack in a similar
    // way. The SMT solver will have an initial state, plus one pushed state per edge of the path.
    void backtrack(Partitioner2::CfgPath &path /*in,out*/, const SmtSolverPtr&);

    // Process one edge of a path to find any path constraints. When called, the cpu's current state should be the virtual
    // machine state at it exists just prior to executing the target vertex of the specified edge.
    //
    // Returns a null pointer if the edge's assertion is trivially unsatisfiable, such as when the edge points to a basic block
    // whose address doesn't match the contents of the instruction pointer register after executing the edge's source
    // block. Otherwise, returns a symbolic expression which must be tree if the edge is feasible. For trivially feasible
    // edges, the return value is the constant 1 (one bit wide; i.e., true).
    SymbolicExpressionPtr pathEdgeConstraint(const Partitioner2::ControlFlowGraph::ConstEdgeIterator &pathEdge,
                                             const InstructionSemantics::BaseSemantics::DispatcherPtr &cpu);

    // Parse the expression if it's a parsable string, otherwise return the expression as is. */
    Expression parseExpression(Expression, const std::string &where, SymbolicExpressionParser&) const;

    SymbolicExpressionPtr expandExpression(const Expression&, const SymbolicExpressionParser&);

    // Based on the last vertex of the path, insert user-specified assertions into the SMT solver.
    void insertAssertions(const SmtSolverPtr&, const Partitioner2::CfgPath&,
                          const std::vector<Expression> &assertions, bool atEndOfPath, const SymbolicExpressionParser&);

    // Size of vertex. How much of "k" does this vertex consume?
    static size_t vertexSize(const Partitioner2::ControlFlowGraph::ConstVertexIterator&);

    // Information needed for adding user-supplied assertions to the solver.
    struct Substitutions {
        SymbolicExpressionParser exprParser;
        std::vector<Expression> assertions;
        SymbolicExpressionParser::RegisterSubstituter::Ptr regSubber;
        SymbolicExpressionParser::MemorySubstituter::Ptr memSubber;
    };

    // Insert the edge assertion and any applicable user assertions (after delayed expansion of the expressions' register
    // and memory references), and run the solver, returning its result.
    SmtSolver::Satisfiable
    solvePathConstraints(const SmtSolverPtr&, const Partitioner2::CfgPath&, const SymbolicExpressionPtr &edgeAssertion,
                         const Substitutions&, bool atEndOfPath);

    // Mark vertex as being reached
    void markAsReached(const Partitioner2::ControlFlowGraph::ConstVertexIterator&);

    // Top-level info for debugging
    void dfsDebugHeader(Sawyer::Message::Stream &trace, Sawyer::Message::Stream &debug, size_t callId, size_t graphId);

    // Top-level info for debugging a path.
    void dfsDebugCurrentPath(Sawyer::Message::Stream&, const Partitioner2::CfgPath&, const SmtSolverPtr&, size_t effectiveK);

    // Prepare substitutions for registers and memory based on user-supplied symbolic expressions.
    Substitutions parseSubstitutions();

    // Substitute registers and memory values into user-supplied symbolic expressions.
    void makeSubstitutions(const Substitutions&, const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&);

    // Create an SMT solver. It will have an initial state plus, eventually, a transaction for each path edge.
    SmtSolverPtr createSmtSolver();

    // The parts of the instruction semantics framework
    struct Semantics {
        InstructionSemantics::BaseSemantics::DispatcherPtr cpu;
        InstructionSemantics::BaseSemantics::RiscOperatorsPtr ops;
        InstructionSemantics::BaseSemantics::StatePtr originalState;
    };

    // Create the parts of the instruction semantics framework.
    Semantics createSemantics(const Partitioner2::CfgPath&, PathProcessor&, const SmtSolverPtr&);

    // Convert a position to an index. Negative positions measure from the end of the sequence so that -1 refers to the last
    // element, -2 to the second-to-last element, etc. Non-negative positions are the same thing as an index.  Returns nothing
    // if the position is out of range.
    static Sawyer::Optional<size_t> positionToIndex(int position, size_t nElmts);

    // Obtain the incoming state for the specified path vertex. This is a pointer to the state, so copy it if you make changes.
    // The incoming state for the first vertex is the specified initial state.
    InstructionSemantics::BaseSemantics::StatePtr
    incomingState(const Partitioner2::CfgPath&, int position, const InstructionSemantics::BaseSemantics::StatePtr &initialState);

    // Number of steps (e.g., instructions) up to but not including the specified path vertex.
    size_t incomingStepCount(const Partitioner2::CfgPath&, int position);

    // Number of steps (e.g., instructions) up to and including the specified path vertex.
    size_t outgoingStepCount(const Partitioner2::CfgPath&, int position);

    // Evaluate semantics up to and including the specified path vertex, returning the outgoing state for that vertex. If
    // semantics fails, then returns a null state pointer.
    InstructionSemantics::BaseSemantics::StatePtr evaluate(Partitioner2::CfgPath&, int position, const Semantics&);

    // Check whether the last vertex of the path is feasible. Returns true if provably feasible, false if provably infeasible,
    // or indeterminate if not provable one way or the other.
    boost::logic::tribool isFeasible(Partitioner2::CfgPath&, const Substitutions&, const Semantics&, const SmtSolverPtr&);

    // Safely call the path processor's "found" action for the path's final vertex and return its value.
    PathProcessor::Action callPathProcessorFound(PathProcessor&, Partitioner2::CfgPath&, const Semantics&, const SmtSolverPtr&);

    // Given an effective K value, adjust it based on how often the last vertex of the path has been visited.  Returns a new
    // effective K. As a special case, the new K is zero if the last vertex has been visited too often.
    double adjustEffectiveK(Partitioner2::CfgPath&, double oldK);

    // Given a path that ends with a function call, inline the function or a summary of the function, adjusting the paths_
    // control flow graph.
    void summarizeOrInline(Partitioner2::CfgPath&, const Semantics&);
};

} // namespace
} // namespace

std::ostream& operator<<(std::ostream&, const Rose::BinaryAnalysis::FeasiblePath::Expression&);

// Convert string to feasible path expression during command-line parsing
namespace Sawyer {
    namespace CommandLine {
        template<>
        struct LexicalCast<Rose::BinaryAnalysis::FeasiblePath::Expression> {
            static Rose::BinaryAnalysis::FeasiblePath::Expression convert(const std::string &src) {
                return Rose::BinaryAnalysis::FeasiblePath::Expression(src);
            }
        };
    }
}

#endif
#endif