ROSE  0.11.50.0
ExecutionUnit.h
1 #ifndef ROSE_BinaryAnalysis_ModelChecker_ExecutionUnit_H
2 #define ROSE_BinaryAnalysis_ModelChecker_ExecutionUnit_H
3 #include <featureTests.h>
4 #ifdef ROSE_ENABLE_BINARY_ANALYSIS
5 
6 #include <Rose/BinaryAnalysis/ModelChecker/Types.h>
7 
8 #include <Rose/BinaryAnalysis/InstructionSemantics2/BaseSemantics/Types.h>
9 #include <Rose/SourceLocation.h>
10 
11 namespace Rose {
12 namespace BinaryAnalysis {
13 namespace ModelChecker {
14 
20 public:
22  using Ptr = ExecutionUnitPtr;
23 
24 private:
25  const SourceLocation sourceLocation_;
26 
27 public:
28  ExecutionUnit() = delete;
29  explicit ExecutionUnit(const SourceLocation&);
30  virtual ~ExecutionUnit();
31 
32 public:
38  virtual std::string printableName() const = 0;
39 
48  virtual void printSteps(const SettingsPtr&, std::ostream&, const std::string &prefix,
49  size_t stepOrigin, size_t maxSteps) const = 0;
50 
52  virtual void toYamlHeader(const SettingsPtr&, std::ostream&, const std::string &prefix) const = 0;
53 
61  virtual void toYamlSteps(const SettingsPtr&, std::ostream&, const std::string &prefix,
62  size_t stepOrigin, size_t maxSteps) const = 0;
63 
72  void printSource(const SettingsPtr&, std::ostream&, const std::string &prefix) const;
73  void printSource(const SettingsPtr&, std::ostream&, const std::string &prefix, const SourceLocation&) const;
84  virtual size_t nSteps() const = 0;
85 
93  virtual Sawyer::Optional<rose_addr_t> address() const;
94 
101 
110  virtual bool containsUnknownInsn() const;
111 
120  virtual std::vector<TagPtr>
121  execute(const SettingsPtr&, const SemanticCallbacksPtr&, const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr&) = 0;
122 
153  size_t nodeStep);
154 };
155 
156 } // namespace
157 } // namespace
158 } // namespace
159 
160 #endif
161 #endif
boost::shared_ptr< RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to a RISC operators object.
Information about a source location.
Base class for machine instructions.
TagPtr executeInstruction(const SettingsPtr &, SgAsmInstruction *, const InstructionSemantics2::BaseSemantics::DispatcherPtr &, size_t nodeStep)
Execute a single instruction semantically.
void printSource(const SettingsPtr &, std::ostream &, const std::string &prefix) const
List source location.
Main namespace for the ROSE library.
virtual void toYamlHeader(const SettingsPtr &, std::ostream &, const std::string &prefix) const =0
Print the header information in YAML format.
boost::shared_ptr< Dispatcher > DispatcherPtr
Shared-ownership pointer to a semantics instruction dispatcher.
SourceLocation sourceLocation() const
Property: Location in source code.
virtual size_t nSteps() const =0
Property: Number of steps required to execute this unit.
virtual bool containsUnknownInsn() const
Predicate to test for unknown instructions.
virtual void toYamlSteps(const SettingsPtr &, std::ostream &, const std::string &prefix, size_t stepOrigin, size_t maxSteps) const =0
Print the steps for this execution unit in YAML format.
ExecutionUnitPtr Ptr
Shared ownership pointer for an execution unit.
Definition: ExecutionUnit.h:22
virtual Sawyer::Optional< rose_addr_t > address() const
Property: Address if it has one.
virtual std::string printableName() const =0
Property: Printable name.
virtual std::vector< TagPtr > execute(const SettingsPtr &, const SemanticCallbacksPtr &, const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &)=0
Execute the unit to create a new state.
virtual void printSteps(const SettingsPtr &, std::ostream &, const std::string &prefix, size_t stepOrigin, size_t maxSteps) const =0
Print the steps for this execution unit.