1#ifndef ROSE_BinaryAnalysis_ModelChecker_ExecutionUnit_H
2#define ROSE_BinaryAnalysis_ModelChecker_ExecutionUnit_H
3#include <featureTests.h>
4#ifdef ROSE_ENABLE_MODEL_CHECKER
6#include <Rose/BinaryAnalysis/Address.h>
7#include <Rose/BinaryAnalysis/InstructionSemantics/BaseSemantics/BasicTypes.h>
8#include <Rose/BinaryAnalysis/ModelChecker/BasicTypes.h>
9#include <Rose/SourceLocation.h>
14namespace BinaryAnalysis {
15namespace ModelChecker {
24 using Ptr = ExecutionUnitPtr;
27 const SourceLocation sourceLocation_;
30 ExecutionUnit() =
delete;
31 explicit ExecutionUnit(
const SourceLocation&);
32 virtual ~ExecutionUnit();
40 virtual std::string printableName()
const = 0;
50 virtual void printSteps(
const SettingsPtr&, std::ostream&,
const std::string &prefix,
51 size_t stepOrigin,
size_t maxSteps)
const = 0;
54 virtual void toYamlHeader(
const SettingsPtr&, std::ostream&,
const std::string &prefix)
const = 0;
63 virtual void toYamlSteps(
const SettingsPtr&, std::ostream&,
const std::string &prefix,
64 size_t stepOrigin,
size_t maxSteps)
const = 0;
69 virtual std::vector<Sarif::LocationPtr> toSarif(
size_t maxSteps)
const = 0;
79 void printSource(
const SettingsPtr&, std::ostream&,
const std::string &prefix)
const;
80 void printSource(
const SettingsPtr&, std::ostream&,
const std::string &prefix,
const SourceLocation&)
const;
91 virtual size_t nSteps()
const = 0;
107 SourceLocation sourceLocation()
const;
117 virtual bool containsUnknownInsn()
const;
127 virtual std::vector<TagPtr>
128 execute(
const SettingsPtr&,
const SemanticCallbacksPtr&,
129 const InstructionSemantics::BaseSemantics::RiscOperatorsPtr &riscOperators) = 0;
160 TagPtr executeInstruction(
const SettingsPtr&,
SgAsmInstruction*,
const InstructionSemantics::BaseSemantics::DispatcherPtr&,
Holds a value or nothing.
Base class for machine instructions.
Sawyer::SharedPointer< Node > Ptr
Reference counting pointer.