ROSE 0.11.145.189
SemanticCallbacks.h
1#ifndef ROSE_BinaryAnalysis_ModelChecker_SemanticCallbacks_H
2#define ROSE_BinaryAnalysis_ModelChecker_SemanticCallbacks_H
3#include <featureTests.h>
4#ifdef ROSE_ENABLE_MODEL_CHECKER
5
6#include <Rose/BinaryAnalysis/ModelChecker/BasicTypes.h>
7
8#include <Rose/BinaryAnalysis/InstructionSemantics/BaseSemantics/BasicTypes.h>
9#include <Rose/BinaryAnalysis/SmtSolver.h>
10#include <Rose/Yaml.h>
11
12#ifdef ROSE_HAVE_YAMLCPP
13#include <yaml-cpp/yaml.h>
14#endif
15
16namespace Rose {
17namespace BinaryAnalysis {
18namespace ModelChecker {
19
25class SemanticCallbacks {
26public:
28 using Ptr = SemanticCallbacksPtr;
29
30private:
31 const SettingsPtr mcSettings_; // model checker settings
32
33protected:
34 SemanticCallbacks() = delete;
35 explicit SemanticCallbacks(const SettingsPtr&);
36public:
37 virtual ~SemanticCallbacks();
38
39public:
41 // Functions for creating the semantics framework
43
50 virtual void reset() {}
51
57 SettingsPtr mcSettings() const;
58
68 virtual InstructionSemantics::BaseSemantics::SValuePtr protoval();
69
76 virtual InstructionSemantics::BaseSemantics::RegisterStatePtr createInitialRegisters() = 0;
77
84 virtual InstructionSemantics::BaseSemantics::MemoryStatePtr createInitialMemory() = 0;
85
93 virtual InstructionSemantics::BaseSemantics::StatePtr createInitialState();
94
112 virtual InstructionSemantics::BaseSemantics::RiscOperatorsPtr createRiscOperators() = 0;
113
124 virtual SmtSolverPtr createSolver() = 0;
125
138 virtual void attachModelCheckerSolver(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&,
139 const SmtSolverPtr&) {}
140
149 virtual void initializeState(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&);
150
157 virtual InstructionSemantics::BaseSemantics::DispatcherPtr
158 createDispatcher(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&) = 0;
159
161 // State query functions
163
170 virtual InstructionSemantics::BaseSemantics::SValuePtr
171 instructionPointer(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&) = 0;
172
176 struct CodeAddresses {
177 InstructionSemantics::BaseSemantics::SValuePtr ip;
178 std::set<rose_addr_t> addresses;
179 bool isComplete = true;
180 };
181
188 virtual CodeAddresses nextCodeAddresses(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&);
189
191 // Execution tree functions
193
203 virtual std::vector<TagPtr>
204 preExecute(const ExecutionUnitPtr&, const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&);
205
215 virtual std::vector<TagPtr>
216 postExecute(const ExecutionUnitPtr&, const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&);
217
219 struct NextUnit {
220 ExecutionUnitPtr unit;
221 SymbolicExpression::Ptr assertion;
222 SmtSolver::Evidence evidence;
223 };
224
240 virtual std::vector<NextUnit>
241 nextUnits(const PathPtr&, const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&, const SmtSolverPtr&) = 0;
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
Sawyer::SharedPointer< Node > Ptr
Reference counting pointer.
std::shared_ptr< SmtSolver > SmtSolverPtr
Reference counting pointer.
The ROSE library.