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/FileSystem.h>

namespace Rose {
namespace BinaryAnalysis {
namespace Concolic {

// Concolic executor.

class ConcolicExecutor: public Sawyer::SharedObject {
public:
    typedef Sawyer::SharedPointer<ConcolicExecutor> Ptr;

    struct FunctionCall {
        std::string printableName;                      
        rose_addr_t sourceVa;                           
        rose_addr_t targetVa;                           
        rose_addr_t stackVa;                            
        FunctionCall()
            : sourceVa(0), targetVa(0), stackVa(0) {}

        FunctionCall(const std::string &printableName, rose_addr_t sourceVa, rose_addr_t targetVa, rose_addr_t 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