ROSE 0.11.145.147
ExecutionUnit.h
1#ifndef ROSE_BinaryAnalysis_ModelChecker_ExecutionUnit_H
2#define ROSE_BinaryAnalysis_ModelChecker_ExecutionUnit_H
3#include <featureTests.h>
4#ifdef ROSE_ENABLE_MODEL_CHECKER
5
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>
10
12
13namespace Rose {
14namespace BinaryAnalysis {
15namespace ModelChecker {
16
21class ExecutionUnit {
22public:
24 using Ptr = ExecutionUnitPtr;
25
26private:
27 const SourceLocation sourceLocation_;
28
29public:
30 ExecutionUnit() = delete;
31 explicit ExecutionUnit(const SourceLocation&);
32 virtual ~ExecutionUnit();
33
34public:
40 virtual std::string printableName() const = 0;
41
50 virtual void printSteps(const SettingsPtr&, std::ostream&, const std::string &prefix,
51 size_t stepOrigin, size_t maxSteps) const = 0;
52
54 virtual void toYamlHeader(const SettingsPtr&, std::ostream&, const std::string &prefix) const = 0;
55
63 virtual void toYamlSteps(const SettingsPtr&, std::ostream&, const std::string &prefix,
64 size_t stepOrigin, size_t maxSteps) const = 0;
65
69 virtual std::vector<Sarif::LocationPtr> toSarif(size_t maxSteps) const = 0;
70
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;
92
100 virtual Sawyer::Optional<rose_addr_t> address() const;
101
107 SourceLocation sourceLocation() const;
108
117 virtual bool containsUnknownInsn() const;
118
127 virtual std::vector<TagPtr>
128 execute(const SettingsPtr&, const SemanticCallbacksPtr&,
129 const InstructionSemantics::BaseSemantics::RiscOperatorsPtr &riscOperators) = 0;
130
160 TagPtr executeInstruction(const SettingsPtr&, SgAsmInstruction*, const InstructionSemantics::BaseSemantics::DispatcherPtr&,
161 size_t nodeStep);
162};
163
164} // namespace
165} // namespace
166} // namespace
167
168#endif
169#endif
Holds a value or nothing.
Definition Optional.h:56
Base class for machine instructions.
Sawyer::SharedPointer< Node > Ptr
Reference counting pointer.
The ROSE library.