1#ifndef ROSE_BinaryAnalysis_Concolic_Emulation_H
2#define ROSE_BinaryAnalysis_Concolic_Emulation_H
3#include <featureTests.h>
4#ifdef ROSE_ENABLE_CONCOLIC_TESTING
5#include <Rose/BinaryAnalysis/Concolic/BasicTypes.h>
7#include <Rose/BinaryAnalysis/BasicTypes.h>
8#include <Rose/BinaryAnalysis/InstructionSemantics/BaseSemantics/BasicTypes.h>
9#include <Rose/BinaryAnalysis/InstructionSemantics/SymbolicSemantics.h>
10#include <Sawyer/FileSystem.h>
13namespace BinaryAnalysis {
19typedef InstructionSemantics::SymbolicSemantics::Formatter SValueFormatter;
20typedef InstructionSemantics::SymbolicSemantics::SValuePtr
SValuePtr;
21typedef InstructionSemantics::SymbolicSemantics::SValue SValue;
22typedef InstructionSemantics::SymbolicSemantics::RegisterStatePtr RegisterStatePtr;
23typedef InstructionSemantics::SymbolicSemantics::RegisterState RegisterState;
24typedef InstructionSemantics::SymbolicSemantics::MemoryStatePtr
MemoryStatePtr;
25typedef InstructionSemantics::SymbolicSemantics::MemoryState MemoryState;
26typedef InstructionSemantics::SymbolicSemantics::StatePtr StatePtr;
27typedef InstructionSemantics::SymbolicSemantics::State
State;
30class Exit:
public Exception {
34 explicit Exit(uint64_t status)
35 : Exception(
"subordinate exit"), status_(status) {}
40 uint64_t status()
const {
46class RiscOperators:
public InstructionSemantics::SymbolicSemantics::RiscOperators {
52 typedef InstructionSemantics::SymbolicSemantics::RiscOperators Super;
55 const RegisterDescriptor REG_PATH;
64 TestCasePtr testCase_;
65 Partitioner2::PartitionerConstPtr partitioner_;
66 ArchitecturePtr process_;
67 bool hadSystemCall_ =
false;
68 ExecutionEventPtr hadSharedMemoryAccess_;
69 bool isRecursive_ =
false;
73 RiscOperators(
const Settings&,
const DatabasePtr&,
const TestCasePtr&,
const Partitioner2::PartitionerConstPtr&,
74 const ArchitecturePtr&,
const InstructionSemantics::BaseSemantics::StatePtr&,
const SmtSolverPtr&);
80 static RiscOperatorsPtr instance(
const Settings &settings,
const DatabasePtr&,
const TestCasePtr&,
81 const Partitioner2::PartitionerConstPtr&,
const ArchitecturePtr &process,
82 const InstructionSemantics::BaseSemantics::SValuePtr &protoval,
86 static RiscOperatorsPtr promote(
const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&);
89 virtual InstructionSemantics::BaseSemantics::RiscOperatorsPtr
90 create(
const InstructionSemantics::BaseSemantics::SValuePtr &,
92 virtual InstructionSemantics::BaseSemantics::RiscOperatorsPtr
93 create(
const InstructionSemantics::BaseSemantics::StatePtr &,
103 Partitioner2::PartitionerConstPtr partitioner()
const;
106 TestCasePtr testCase()
const;
109 DatabasePtr database()
const;
112 ArchitecturePtr process()
const;
119 InputVariablesPtr inputVariables()
const;
129 bool hadSystemCall()
const;
130 void hadSystemCall(
bool);
139 ExecutionEventPtr hadSharedMemoryAccess()
const;
140 void hadSharedMemoryAccess(
const ExecutionEventPtr&);
149 bool isRecursive()
const;
150 void isRecursive(
bool);
157 size_t wordSizeBits()
const;
167 void createInputVariables(
const SmtSolver::Ptr&);
172 void restoreInputVariables(
const SmtSolver::Ptr&);
177 void printInputVariables(std::ostream&)
const;
180 void printAssertions(std::ostream&)
const;
187 virtual void interrupt(
int majr,
int minr)
override;
189 virtual InstructionSemantics::BaseSemantics::SValuePtr
190 readRegister(RegisterDescriptor reg,
const InstructionSemantics::BaseSemantics::SValuePtr &dflt)
override;
192 virtual InstructionSemantics::BaseSemantics::SValuePtr
193 readRegister(RegisterDescriptor reg)
override;
195 virtual InstructionSemantics::BaseSemantics::SValuePtr
196 peekRegister(RegisterDescriptor reg,
const InstructionSemantics::BaseSemantics::SValuePtr &dflt)
override;
199 writeRegister(RegisterDescriptor,
const InstructionSemantics::BaseSemantics::SValuePtr&)
override;
201 virtual InstructionSemantics::BaseSemantics::SValuePtr
202 readMemory(RegisterDescriptor segreg,
const InstructionSemantics::BaseSemantics::SValuePtr &addr,
203 const InstructionSemantics::BaseSemantics::SValuePtr &dflt,
204 const InstructionSemantics::BaseSemantics::SValuePtr &cond)
override;
206 virtual InstructionSemantics::BaseSemantics::SValuePtr
207 peekMemory(RegisterDescriptor segreg,
const InstructionSemantics::BaseSemantics::SValuePtr &addr,
208 const InstructionSemantics::BaseSemantics::SValuePtr &dflt)
override;
211 writeMemory(RegisterDescriptor segreg,
const InstructionSemantics::BaseSemantics::SValuePtr &addr,
212 const InstructionSemantics::BaseSemantics::SValuePtr &value,
213 const InstructionSemantics::BaseSemantics::SValuePtr &cond)
override;
216 void doExit(uint64_t);
227 InstructionSemantics::BaseSemantics::DispatcherPtr inner_;
230 explicit Dispatcher(
const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&,
const ArchitecturePtr&);
235 static Ptr instance(
const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&,
const ArchitecturePtr&);
239 InstructionSemantics::BaseSemantics::RiscOperators::Ptr operators()
const;
243 rose_addr_t concreteInstructionPointer()
const;
249 bool isTerminated()
const;
258 static RiscOperatorsPtr unwrapEmulationOperators(
const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&);
Base class for reference counted objects.
Reference-counting intrusive smart pointer.
Base class for machine instructions.
boost::shared_ptr< Dispatcher > DispatcherPtr
Shared-ownership pointer to a semantics instruction dispatcher.
boost::shared_ptr< class MemoryState > MemoryStatePtr
Shared-ownership pointer to a concrete memory state.
boost::shared_ptr< class RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to concrete RISC operations.
Sawyer::SharedPointer< class SValue > SValuePtr
Smart-ownership pointer to a concrete semantic value.
Sawyer::SharedPointer< Node > Ptr
Reference counting pointer.
std::shared_ptr< SmtSolver > SmtSolverPtr
Reference counting pointer.
Sawyer::SharedPointer< RegisterDictionary > RegisterDictionaryPtr
Reference counting pointer.
Settings settings
Command-line settings for the rosebud tool.