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

#include <Rose/BinaryAnalysis/Concolic/LinuxI386.h>
#include <Rose/BinaryAnalysis/Debugger.h>
#include <Rose/BinaryAnalysis/InstructionSemantics2/DispatcherX86.h>
#include <Rose/BinaryAnalysis/InstructionSemantics2/SymbolicSemantics.h>
#include <Rose/BinaryAnalysis/Partitioner2/Partitioner.h>
#include <Sawyer/FileSystem.h>

namespace Rose {
namespace BinaryAnalysis {
namespace Concolic {

// Concolic emulation semantics.

namespace Emulation {

typedef InstructionSemantics2::SymbolicSemantics::Formatter SValueFormatter; 
typedef InstructionSemantics2::SymbolicSemantics::SValuePtr SValuePtr; 
typedef InstructionSemantics2::SymbolicSemantics::SValue SValue; 
typedef InstructionSemantics2::SymbolicSemantics::RegisterStatePtr RegisterStatePtr; 
typedef InstructionSemantics2::SymbolicSemantics::RegisterState RegisterState; 
typedef InstructionSemantics2::SymbolicSemantics::MemoryStatePtr MemoryStatePtr; 
typedef InstructionSemantics2::SymbolicSemantics::MemoryState MemoryState; 
typedef InstructionSemantics2::SymbolicSemantics::StatePtr StatePtr; 
typedef InstructionSemantics2::SymbolicSemantics::State State; 
class Exit: public Exception {
    uint64_t status_;

public:
    explicit Exit(uint64_t status)
        : Exception("subordinate exit"), status_(status) {}

    ~Exit() throw () {}

    uint64_t status() const {
        return status_;
    }
};

class RiscOperators: public InstructionSemantics2::SymbolicSemantics::RiscOperators {
public:
    using Ptr = RiscOperatorsPtr;

    typedef InstructionSemantics2::SymbolicSemantics::RiscOperators Super;

    const RegisterDescriptor REG_PATH;

    struct Settings {
    };

private:
    Settings settings_;                                 // emulation settings
    DatabasePtr db_;                                    // concolic database connection
    TestCasePtr testCase_;                              // test case whose instructions are being processed
    const Partitioner2::Partitioner &partitioner_;      // ROSE disassembly info about the specimen
    ArchitecturePtr process_;                           // subordinate process, concrete state
    bool hadSystemCall_ = false;                        // true if we need to call process_->systemCall, cleared each insn
    ExecutionEventPtr hadSharedMemoryAccess_;           // set when shared memory is read, cleared each instruction

protected:
    RiscOperators(const Settings&, const DatabasePtr&, const TestCasePtr&, const Partitioner2::Partitioner&,
                  const ArchitecturePtr&, const InstructionSemantics2::BaseSemantics::StatePtr&, const SmtSolverPtr&);

public:
    static RiscOperatorsPtr instance(const Settings &settings, const DatabasePtr&, const TestCasePtr&,
                                     const Partitioner2::Partitioner&, const ArchitecturePtr &process,
                                     const InstructionSemantics2::BaseSemantics::SValuePtr &protoval,
                                     const SmtSolverPtr &solver = SmtSolverPtr());

    static RiscOperatorsPtr promote(const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr&);

    // Overrides documented in base class
    virtual InstructionSemantics2::BaseSemantics::RiscOperatorsPtr
    create(const InstructionSemantics2::BaseSemantics::SValuePtr &protoval,
           const SmtSolverPtr &solver = SmtSolverPtr()) const ROSE_OVERRIDE {
        ASSERT_not_implemented("[Robb Matzke 2019-09-24]");
    }
    virtual InstructionSemantics2::BaseSemantics::RiscOperatorsPtr
    create(const InstructionSemantics2::BaseSemantics::StatePtr &state,
           const SmtSolverPtr &solver = SmtSolverPtr()) const ROSE_OVERRIDE {
        ASSERT_not_implemented("[Robb Matzke 2019-09-24]");
    }

public:
    const Settings& settings() const {
        return settings_;
    }

    const Partitioner2::Partitioner& partitioner() const {
        return partitioner_;
    }

    TestCasePtr testCase() const;

    DatabasePtr database() const;

    ArchitecturePtr process() const {
        return process_;
    }

    InputVariablesPtr inputVariables() const;
    bool hadSystemCall() const {
        return hadSystemCall_;
    }
    void hadSystemCall(bool b) {
        hadSystemCall_ = b;
    }
    ExecutionEventPtr hadSharedMemoryAccess() const {
        return hadSharedMemoryAccess_;
    }
    void hadSharedMemoryAccess(const ExecutionEventPtr &e) {
        hadSharedMemoryAccess_ = e;
    }
    size_t wordSizeBits() const;

    const RegisterDictionary* registerDictionary() const;

    void createInputVariables(const SmtSolver::Ptr&);

    void restoreInputVariables(const SmtSolver::Ptr&);

    void printInputVariables(std::ostream&) const;

    void printAssertions(std::ostream&) const;

public:
    // Base class overrides -- the acutal RISC operations

    virtual void startInstruction(SgAsmInstruction*) override;

    virtual void interrupt(int majr, int minr) ROSE_OVERRIDE;

    virtual InstructionSemantics2::BaseSemantics::SValuePtr
    readRegister(RegisterDescriptor reg, const InstructionSemantics2::BaseSemantics::SValuePtr &dflt) ROSE_OVERRIDE;

    virtual InstructionSemantics2::BaseSemantics::SValuePtr
    readRegister(RegisterDescriptor reg) ROSE_OVERRIDE {
        return readRegister(reg, undefined_(reg.nBits()));
    }

    virtual InstructionSemantics2::BaseSemantics::SValuePtr
    peekRegister(RegisterDescriptor reg, const InstructionSemantics2::BaseSemantics::SValuePtr &dflt) ROSE_OVERRIDE;

    virtual void
    writeRegister(RegisterDescriptor, const InstructionSemantics2::BaseSemantics::SValuePtr&) override;

    virtual InstructionSemantics2::BaseSemantics::SValuePtr
    readMemory(RegisterDescriptor segreg, const InstructionSemantics2::BaseSemantics::SValuePtr &addr,
               const InstructionSemantics2::BaseSemantics::SValuePtr &dflt,
               const InstructionSemantics2::BaseSemantics::SValuePtr &cond) ROSE_OVERRIDE;

    virtual InstructionSemantics2::BaseSemantics::SValuePtr
    peekMemory(RegisterDescriptor segreg, const InstructionSemantics2::BaseSemantics::SValuePtr &addr,
               const InstructionSemantics2::BaseSemantics::SValuePtr &dflt) ROSE_OVERRIDE;

    // Call this when the concrete simulation exits.
    void doExit(uint64_t);
};

typedef boost::shared_ptr<class Dispatcher> DispatcherPtr;

class Dispatcher: public InstructionSemantics2::DispatcherX86 {
    typedef InstructionSemantics2::DispatcherX86 Super;
public:
    using Ptr = boost::shared_ptr<Dispatcher>;

protected:
    explicit Dispatcher(const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &ops)
        : Super(ops, unwrapEmulationOperators(ops)->wordSizeBits(), unwrapEmulationOperators(ops)->registerDictionary()) {}

public:
    static DispatcherPtr instance(const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &ops) {
        return DispatcherPtr(new Dispatcher(ops));
    }

public:
    rose_addr_t concreteInstructionPointer() const;

    bool isTerminated() const;

    RiscOperatorsPtr emulationOperators() const;

    static RiscOperatorsPtr unwrapEmulationOperators(const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr&);

    void processConcreteInstruction(SgAsmInstruction*);

public:
    // overrides
    virtual void processInstruction(SgAsmInstruction*) ROSE_OVERRIDE;
};

} // namespace

// Concolic executor.

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

    struct Settings {
        Partitioner2::EngineSettings partitionerEngine;
        Partitioner2::LoaderSettings loader;
        Partitioner2::DisassemblerSettings disassembler;
        Partitioner2::PartitionerSettings partitioner;
        Emulation::RiscOperators::Settings emulationSettings;

        bool traceSemantics;                            
        AddressIntervalSet showingStates;               
        Settings()
            : traceSemantics(false) {}
    };

    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:
    Settings 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::Partitioner 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 Settings& settings() const { return settings_; }
    Settings& settings() { return settings_; }
    SmtSolverPtr solver() const;
    void solver(const SmtSolverPtr&);
    DatabasePtr database() const;

    TestCasePtr testCase() const;

    TestCaseId testCaseId() const;

    const Partitioner2::Partitioner& partitioner() const;

    ArchitecturePtr process() const;

    Emulation::DispatcherPtr cpu() const;

    static std::vector<Sawyer::CommandLine::SwitchGroup> commandLineSwitches(Settings &settings /*in,out*/);

    void configureExecution(const DatabasePtr&, const TestCasePtr&);

    std::vector<TestCasePtr> execute();
    std::vector<TestCasePtr> execute(const DatabasePtr&, const TestCasePtr&);
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::Partitioner partition(const SpecimenPtr&);

    // 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 InstructionSemantics2::BaseSemantics::RiscOperatorsPtr&, const SymbolicExpr::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