ROSE  0.11.51.0
SemanticCallbacks.h
1 #ifndef ROSE_BinaryAnalysis_ModelChecker_SemanticCallbacks_H
2 #define ROSE_BinaryAnalysis_ModelChecker_SemanticCallbacks_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/BinaryAnalysis/Partitioner2/Partitioner.h>
10 
11 #ifdef ROSE_HAVE_LIBYAML
12 #include <yaml-cpp/yaml.h>
13 #endif
14 
15 namespace Rose {
16 namespace BinaryAnalysis {
17 namespace ModelChecker {
18 
25 public:
27  using Ptr = SemanticCallbacksPtr;
28 
29 private:
30  const SettingsPtr mcSettings_; // model checker settings
31 
32 protected:
33  SemanticCallbacks() = delete;
34  explicit SemanticCallbacks(const SettingsPtr&);
35 public:
36  virtual ~SemanticCallbacks();
37 
38 public:
40  // Functions for creating the semantics framework
42 
49  virtual void reset() {}
50 
56  SettingsPtr mcSettings() const;
57 
68 
76 
84 
93 
112 
123  virtual SmtSolver::Ptr createSolver() = 0;
124 
138  const SmtSolver::Ptr&) {}
139 
149 
158 
160  // State query functions
162 
171 
175  struct CodeAddresses {
177  std::set<rose_addr_t> addresses;
178  bool isComplete = true;
179  };
180 
188 
190  // Execution tree functions
192 
202  virtual std::vector<TagPtr>
204 
214  virtual std::vector<TagPtr>
216 
218  struct NextUnit {
219  ExecutionUnitPtr unit;
222  };
223 
239  virtual std::vector<NextUnit>
241 
243  // Path creation functions.
245 
246 #ifdef ROSE_HAVE_LIBYAML
247 
255  virtual std::list<ExecutionUnitPtr>
256  parsePath(const YAML::Node&, const std::string &sourceName) = 0;
257 #endif
258 
259 };
260 
261 } // namespace
262 } // namespace
263 } // namespace
264 
265 #endif
266 #endif
SmtSolverPtr Ptr
Reference counting pointer for SMT solvers.
Definition: SmtSolver.h:39
virtual void attachModelCheckerSolver(const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &, const SmtSolver::Ptr &)
Associate solver with semantics.
virtual InstructionSemantics2::BaseSemantics::SValuePtr protoval()
Create a prototypical semantic value.
boost::shared_ptr< RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to a RISC operators object.
SmtSolver::Evidence evidence
SMT solver evidence that this is a feasible path.
virtual SmtSolver::Ptr createSolver()=0
Create model checker solver.
SymbolicExpr::Ptr assertion
Path assertion for this unit.
virtual void initializeState(const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &)
Initialize the initial state.
SettingsPtr mcSettings() const
Property: Model checker settings.
boost::shared_ptr< MemoryState > MemoryStatePtr
Shared-ownership pointer to a memory state.
virtual std::vector< TagPtr > postExecute(const ExecutionUnitPtr &, const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &)
Called after execution ends.
boost::shared_ptr< State > StatePtr
Shared-ownership pointer to a semantic state.
Main namespace for the ROSE library.
bool isComplete
Whether additional non-concrete addresses were found.
virtual CodeAddresses nextCodeAddresses(const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &)
Possible next code addresses.
boost::shared_ptr< Dispatcher > DispatcherPtr
Shared-ownership pointer to a semantics instruction dispatcher.
InstructionSemantics2::BaseSemantics::SValuePtr ip
Instruction pointer value.
virtual InstructionSemantics2::BaseSemantics::MemoryStatePtr createInitialMemory()=0
Create an initial memory state.
virtual std::vector< TagPtr > preExecute(const ExecutionUnitPtr &, const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &)
Called before execution starts.
virtual InstructionSemantics2::BaseSemantics::StatePtr createInitialState()
Create an initial state.
User-defined functions for model checking semantics.
virtual InstructionSemantics2::BaseSemantics::RiscOperatorsPtr createRiscOperators()=0
Create RISC operators.
std::set< rose_addr_t > addresses
The concrete addresses.
virtual InstructionSemantics2::BaseSemantics::SValuePtr instructionPointer(const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &)=0
Address of the next instruction.
virtual std::vector< NextUnit > nextUnits(const PathPtr &, const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &, const SmtSolver::Ptr &)=0
Discover next execution units.
virtual InstructionSemantics2::BaseSemantics::DispatcherPtr createDispatcher(const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &)=0
Create an instruction dispatcher.
virtual InstructionSemantics2::BaseSemantics::RegisterStatePtr createInitialRegisters()=0
Create an initial register state.
SemanticCallbacksPtr Ptr
Shared-ownership pointer.
boost::shared_ptr< RegisterState > RegisterStatePtr
Shared-ownership pointer to a register state.