ExecutionUnit.h

#ifndef ROSE_BinaryAnalysis_ModelChecker_ExecutionUnit_H
#define ROSE_BinaryAnalysis_ModelChecker_ExecutionUnit_H
#include <featureTests.h>
#ifdef ROSE_ENABLE_MODEL_CHECKER
 
#include <Rose/BinaryAnalysis/Address.h>
#include <Rose/BinaryAnalysis/InstructionSemantics/BaseSemantics/BasicTypes.h>
#include <Rose/BinaryAnalysis/ModelChecker/BasicTypes.h>
#include <Rose/SourceLocation.h>
 
class SgAsmInstruction;
 
namespace Rose {
namespace BinaryAnalysis {
namespace ModelChecker {
 
class ExecutionUnit {
public:
    using Ptr = ExecutionUnitPtr;
 
private:
    const SourceLocation sourceLocation_;
 
public:
    ExecutionUnit() = delete;
    explicit ExecutionUnit(const SourceLocation&);
    virtual ~ExecutionUnit();
 
public:
    virtual std::string printableName() const = 0;
 
    virtual void printSteps(const SettingsPtr&, std::ostream&, const std::string &prefix,
                            size_t stepOrigin, size_t maxSteps) const = 0;
 
    virtual void toYamlHeader(const SettingsPtr&, std::ostream&, const std::string &prefix) const = 0;
 
    virtual void toYamlSteps(const SettingsPtr&, std::ostream&, const std::string &prefix,
                             size_t stepOrigin, size_t maxSteps) const = 0;
 
    virtual std::vector<Sarif::LocationPtr> toSarif(size_t maxSteps) const = 0;
 
    void printSource(const SettingsPtr&, std::ostream&, const std::string &prefix) const;
    void printSource(const SettingsPtr&, std::ostream&, const std::string &prefix, const SourceLocation&) const;
    virtual size_t nSteps() const = 0;
 
    virtual Sawyer::Optional<Address> address() const;
 
    SourceLocation sourceLocation() const;
 
    virtual bool containsUnknownInsn() const;
 
    virtual std::vector<TagPtr>
    execute(const SettingsPtr&, const SemanticCallbacksPtr&,
            const InstructionSemantics::BaseSemantics::RiscOperatorsPtr &riscOperators) = 0;
 
    TagPtr executeInstruction(const SettingsPtr&, SgAsmInstruction*, const InstructionSemantics::BaseSemantics::DispatcherPtr&,
                              size_t nodeStep);
};
 
} // namespace
} // namespace
} // namespace
 
#endif
#endif