1 #ifndef ROSE_BinaryAnalysis_ModelChecker_SemanticCallbacks_H
2 #define ROSE_BinaryAnalysis_ModelChecker_SemanticCallbacks_H
3 #include <featureTests.h>
4 #ifdef ROSE_ENABLE_BINARY_ANALYSIS
6 #include <Rose/BinaryAnalysis/ModelChecker/Types.h>
8 #include <Rose/BinaryAnalysis/InstructionSemantics2/BaseSemantics/Types.h>
9 #include <Rose/BinaryAnalysis/Partitioner2/Partitioner.h>
10 #include <Rose/Yaml.h>
12 #ifdef ROSE_HAVE_YAMLCPP
13 #include <yaml-cpp/yaml.h>
17 namespace BinaryAnalysis {
18 namespace ModelChecker {
28 using Ptr = SemanticCallbacksPtr;
31 const SettingsPtr mcSettings_;
203 virtual std::vector<TagPtr>
215 virtual std::vector<TagPtr>
240 virtual std::vector<NextUnit>
257 #ifdef ROSE_HAVE_YAMLCPP
258 virtual std::list<ExecutionUnitPtr>
259 parsePath(
const YAML::Node&,
const std::string &sourceName) = 0;
261 virtual std::list<ExecutionUnitPtr>
SmtSolverPtr Ptr
Reference counting pointer for SMT solvers.
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.
virtual void reset()
Reset internal data.
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.
Addresses and completeness.
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.
Return value for nextUnits.
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.
ExecutionUnitPtr unit
Unit to be executed.