ROSE  0.11.83.2
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 #include <Rose/Yaml.h>
11 
12 #ifdef ROSE_HAVE_YAMLCPP
13 #include <yaml-cpp/yaml.h>
14 #endif
15 
16 namespace Rose {
17 namespace BinaryAnalysis {
18 namespace ModelChecker {
19 
26 public:
28  using Ptr = SemanticCallbacksPtr;
29 
30 private:
31  const SettingsPtr mcSettings_; // model checker settings
32 
33 protected:
34  SemanticCallbacks() = delete;
35  explicit SemanticCallbacks(const SettingsPtr&);
36 public:
37  virtual ~SemanticCallbacks();
38 
39 public:
41  // Functions for creating the semantics framework
43 
50  virtual void reset() {}
51 
57  SettingsPtr mcSettings() const;
58 
69 
77 
85 
94 
113 
124  virtual SmtSolver::Ptr createSolver() = 0;
125 
139  const SmtSolver::Ptr&) {}
140 
150 
159 
161  // State query functions
163 
172 
176  struct CodeAddresses {
178  std::set<rose_addr_t> addresses;
179  bool isComplete = true;
180  };
181 
189 
191  // Execution tree functions
193 
203  virtual std::vector<TagPtr>
205 
215  virtual std::vector<TagPtr>
217 
219  struct NextUnit {
220  ExecutionUnitPtr unit;
223  };
224 
240  virtual std::vector<NextUnit>
242 
244  // Path creation functions.
246 
257 #ifdef ROSE_HAVE_YAMLCPP
258  virtual std::list<ExecutionUnitPtr>
259  parsePath(const YAML::Node&, const std::string &sourceName) = 0;
260 #endif
261  virtual std::list<ExecutionUnitPtr>
262  parsePath(const Yaml::Node&, const std::string &sourceName) = 0;
264 };
265 
266 } // namespace
267 } // namespace
268 } // namespace
269 
270 #endif
271 #endif
SmtSolverPtr Ptr
Reference counting pointer for SMT solvers.
Definition: SmtSolver.h:48
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.
YAML node.
Definition: Yaml.h:328
virtual InstructionSemantics2::BaseSemantics::StatePtr createInitialState()
Create an initial state.
User-defined functions for model checking semantics.
virtual std::list< ExecutionUnitPtr > parsePath(const Yaml::Node &, const std::string &sourceName)=0
Construct a path from a YAML document.
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.