ConcolicExecutor.h

#ifndef ROSE_BinaryAnalysis_Concolic_ConcolicExecutor_H
#define ROSE_BinaryAnalysis_Concolic_ConcolicExecutor_H
#include <featureTests.h>
#ifdef ROSE_ENABLE_CONCOLIC_TESTING
#include <Rose/BinaryAnalysis/Concolic/Settings.h>
 
#include <Rose/BinaryAnalysis/BasicTypes.h>
#include <Rose/Yaml.h>
 
#include <Sawyer/CommandLine.h>
#include <Sawyer/FileSystem.h>
 
#include <ostream>
#include <string>
#include <vector>
 
namespace Rose {
namespace BinaryAnalysis {
namespace Concolic {
 
// Concolic executor.
 
class ConcolicExecutor: public Sawyer::SharedObject {
public:
    typedef Sawyer::SharedPointer<ConcolicExecutor> Ptr;
 
    struct FunctionCall {
        std::string printableName;                      
        Address sourceVa;                               
        Address targetVa;                               
        Address stackVa;                                
        FunctionCall()
            : sourceVa(0), targetVa(0), stackVa(0) {}
 
        FunctionCall(const std::string &printableName, Address sourceVa, Address targetVa, Address stackVa)
            : printableName(printableName), sourceVa(sourceVa), targetVa(targetVa), stackVa(stackVa) {}
    };
 
private:
    ConcolicExecutorSettings settings_;
    std::vector<FunctionCall> functionCallStack_;
    Sawyer::FileSystem::TemporaryDirectory tmpDir_;
 
    // These can be configured by the user before calling configureExecution.
    SmtSolverPtr solver_;                               // solver used during execution
 
    // These are initialized by configureExecution
    TestCasePtr testCase_;                              // currently executing test case
    TestCaseId testCaseId_;                             // database ID for currently executing test case
    DatabasePtr db_;                                    // database for all this stuff
    Partitioner2::PartitionerPtr partitioner_;          // used during execution
    ArchitecturePtr process_;                           // the concrete half of the execution
    Emulation::DispatcherPtr cpu_;                      // the symbolic half of the execution
 
protected:
    ConcolicExecutor();
 
public:
    ~ConcolicExecutor();
 
public:
    static Ptr instance();
 
    const ConcolicExecutorSettings& settings() const;
    ConcolicExecutorSettings& settings();
    void settings(const ConcolicExecutorSettings&);
    SmtSolverPtr solver() const;
    void solver(const SmtSolverPtr&);
    DatabasePtr database() const;
 
    TestCasePtr testCase() const;
 
    TestCaseId testCaseId() const;
 
    Partitioner2::PartitionerConstPtr partitioner() const;
 
    ArchitecturePtr process() const;
 
    Emulation::DispatcherPtr cpu() const;
 
    static std::vector<Sawyer::CommandLine::SwitchGroup> commandLineSwitches(ConcolicExecutorSettings &settings /*in,out*/);
 
    void configureExecution(const DatabasePtr&, const TestCasePtr&, const Yaml::Node &config);
 
    std::vector<TestCasePtr> execute();
    std::vector<TestCasePtr> execute(const DatabasePtr&, const TestCasePtr&, const Yaml::Node &config);
private:
    // Disassemble the specimen and cache the result in the database. If the specimen has previously been disassembled
    // then reconstitute the analysis results from the database.
    Partitioner2::PartitionerPtr partition(const SpecimenPtr&, const ArchitecturePtr&);
 
    // Create the dispatcher, operators, and memory and register state for the symbolic execution.
    Emulation::DispatcherPtr makeDispatcher(const ArchitecturePtr&);
 
    // Create the underlying process and possibly fast forward it to the state at which it was when the test case was created.
    void startProcess();
 
    // Start up the symbolic part of the testing. This must happen after startProcess.
    void startDispatcher();
 
    // Run the execution
    void run();
 
    // Handle function calls. This is mainly for debugging so we have some idea where we are in the execution when an error
    // occurs.  Returns true if the call stack changed.
    bool updateCallStack(SgAsmInstruction*);
 
    // Print function call stack on multiple lines
    void printCallStack(std::ostream&);
 
    // Handle conditional branches
    void handleBranch(SgAsmInstruction*);
 
    // Generae a new test case. This must be called only after the SMT solver's assertions have been checked and found
    // to be satisfiable.
    void generateTestCase(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&, const SymbolicExpression::Ptr &childIp);
 
    // Save the specified symbolic state to the specified test case.
    void saveSymbolicState(const Emulation::RiscOperatorsPtr&, const TestCaseId&);
 
    // True if the two test cases are close enough that we only need to run one of them.
    bool areSimilar(const TestCasePtr&, const TestCasePtr&) const;
 
public:
    // TODO: Lots of properties to control the finer aspects of executing a test case!
};
 
} // namespace
} // namespace
} // namespace
 
#endif
#endif