1 #ifndef ROSE_BinaryAnalysis_Concolic_ConcolicExecutor_H
2 #define ROSE_BinaryAnalysis_Concolic_ConcolicExecutor_H
3 #include <featureTests.h>
4 #ifdef ROSE_ENABLE_CONCOLIC_TESTING
5 #include <Rose/BinaryAnalysis/Concolic/BasicTypes.h>
7 #include <Rose/BinaryAnalysis/Concolic/LinuxI386.h>
8 #include <Rose/BinaryAnalysis/Debugger.h>
9 #include <Rose/BinaryAnalysis/InstructionSemantics2/DispatcherX86.h>
10 #include <Rose/BinaryAnalysis/InstructionSemantics2/SymbolicSemantics.h>
11 #include <Rose/BinaryAnalysis/Partitioner2/Partitioner.h>
12 #include <Sawyer/FileSystem.h>
15 namespace BinaryAnalysis {
25 typedef InstructionSemantics2::SymbolicSemantics::Formatter SValueFormatter;
27 typedef InstructionSemantics2::SymbolicSemantics::SValue SValue;
28 typedef InstructionSemantics2::SymbolicSemantics::RegisterStatePtr RegisterStatePtr;
29 typedef InstructionSemantics2::SymbolicSemantics::RegisterState RegisterState;
30 typedef InstructionSemantics2::SymbolicSemantics::MemoryStatePtr
MemoryStatePtr;
31 typedef InstructionSemantics2::SymbolicSemantics::MemoryState MemoryState;
32 typedef InstructionSemantics2::SymbolicSemantics::StatePtr StatePtr;
33 typedef InstructionSemantics2::SymbolicSemantics::State
State;
36 class Exit:
public Exception {
40 explicit Exit(uint64_t status)
41 : Exception(
"subordinate exit"), status_(status) {}
46 uint64_t status()
const {
52 class RiscOperators:
public InstructionSemantics2::SymbolicSemantics::RiscOperators {
58 typedef InstructionSemantics2::SymbolicSemantics::RiscOperators Super;
61 const RegisterDescriptor REG_PATH;
70 TestCasePtr testCase_;
71 const Partitioner2::Partitioner &partitioner_;
72 ArchitecturePtr process_;
73 bool hadSystemCall_ =
false;
74 ExecutionEventPtr hadSharedMemoryAccess_;
75 bool isRecursive_ =
false;
79 RiscOperators(
const Settings&,
const DatabasePtr&,
const TestCasePtr&,
const Partitioner2::Partitioner&,
84 static RiscOperatorsPtr instance(
const Settings &settings,
const DatabasePtr&,
const TestCasePtr&,
85 const Partitioner2::Partitioner&,
const ArchitecturePtr &process,
96 ASSERT_not_implemented(
"[Robb Matzke 2019-09-24]");
101 ASSERT_not_implemented(
"[Robb Matzke 2019-09-24]");
108 const Settings& settings()
const {
113 const Partitioner2::Partitioner& partitioner()
const {
118 TestCasePtr testCase()
const;
121 DatabasePtr database()
const;
124 ArchitecturePtr process()
const {
133 InputVariablesPtr inputVariables()
const;
143 bool hadSystemCall()
const {
144 return hadSystemCall_;
146 void hadSystemCall(
bool b) {
157 ExecutionEventPtr hadSharedMemoryAccess()
const {
158 return hadSharedMemoryAccess_;
160 void hadSharedMemoryAccess(
const ExecutionEventPtr &e) {
161 hadSharedMemoryAccess_ = e;
171 bool isRecursive()
const {
174 void isRecursive(
bool b) {
183 size_t wordSizeBits()
const;
186 const RegisterDictionary* registerDictionary()
const;
203 void printInputVariables(std::ostream&)
const;
206 void printAssertions(std::ostream&)
const;
213 virtual void interrupt(
int majr,
int minr)
override;
219 readRegister(RegisterDescriptor reg)
override {
220 return readRegister(reg, undefined_(reg.nBits()));
239 void doExit(uint64_t);
246 class Dispatcher:
public InstructionSemantics2::DispatcherX86 {
247 typedef InstructionSemantics2::DispatcherX86 Super;
249 using Ptr = boost::shared_ptr<Dispatcher>;
254 : Super(ops, unwrapEmulationOperators(ops)->wordSizeBits(), unwrapEmulationOperators(ops)->registerDictionary()) {}
259 return DispatcherPtr(
new Dispatcher(ops));
264 rose_addr_t concreteInstructionPointer()
const;
270 bool isTerminated()
const;
305 Partitioner2::EngineSettings partitionerEngine;
306 Partitioner2::LoaderSettings loader;
307 Partitioner2::DisassemblerSettings disassembler;
308 Partitioner2::PartitionerSettings partitioner;
309 Emulation::RiscOperators::Settings emulationSettings;
315 : traceSemantics(false) {}
319 struct FunctionCall {
320 std::string printableName;
321 rose_addr_t sourceVa;
322 rose_addr_t targetVa;
326 : sourceVa(0), targetVa(0), stackVa(0) {}
328 FunctionCall(
const std::string &printableName, rose_addr_t sourceVa, rose_addr_t targetVa, rose_addr_t stackVa)
329 : printableName(printableName), sourceVa(sourceVa), targetVa(targetVa), stackVa(stackVa) {}
334 std::vector<FunctionCall> functionCallStack_;
341 TestCasePtr testCase_;
342 TestCaseId testCaseId_;
344 Partitioner2::Partitioner partitioner_;
345 ArchitecturePtr process_;
346 Emulation::DispatcherPtr cpu_;
356 static Ptr instance();
366 const Settings& settings()
const {
return settings_; }
367 Settings& settings() {
return settings_; }
388 DatabasePtr database()
const;
395 TestCasePtr testCase()
const;
402 TestCaseId testCaseId()
const;
409 const Partitioner2::Partitioner& partitioner()
const;
416 ArchitecturePtr process()
const;
423 Emulation::DispatcherPtr cpu()
const;
432 static std::vector<Sawyer::CommandLine::SwitchGroup>
commandLineSwitches(Settings &settings );
438 void configureExecution(
const DatabasePtr&,
const TestCasePtr&);
446 std::vector<TestCasePtr> execute();
447 std::vector<TestCasePtr> execute(
const DatabasePtr&,
const TestCasePtr&);
453 Partitioner2::Partitioner partition(
const SpecimenPtr&);
456 Emulation::DispatcherPtr makeDispatcher(
const ArchitecturePtr&);
462 void startDispatcher();
472 void printCallStack(std::ostream&);
482 void saveSymbolicState(
const Emulation::RiscOperatorsPtr&,
const TestCaseId&);
485 bool areSimilar(
const TestCasePtr&,
const TestCasePtr&)
const;
SmtSolverPtr Ptr
Reference counting pointer for SMT solvers.
boost::shared_ptr< RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to a RISC operators object.
Sawyer::SharedPointer< Node > Ptr
Shared-ownership pointer to an expression Node.
boost::shared_ptr< class RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to concrete RISC operations.
Sawyer::CommandLine::SwitchGroup commandLineSwitches(Settings &)
Command-line switches for settings.
Base class for machine instructions.
boost::shared_ptr< State > StatePtr
Shared-ownership pointer to a semantic state.
boost::shared_ptr< class Dispatcher > DispatcherPtr
Shared-ownership pointer to Dispatcher.
Main namespace for the ROSE library.
Reference-counting intrusive smart pointer.
Sawyer::SharedPointer< class SValue > SValuePtr
Smart-ownership pointer to a concrete semantic value.
boost::shared_ptr< class MemoryState > MemoryStatePtr
Shared-ownership pointer to a concrete memory state.
Sawyer::SharedPointer< class SValue > SValuePtr
Shared-ownership pointer for symbolic semantic value.
Base class for reference counted objects.
Sawyer::SharedPointer< SValue > SValuePtr
Shared-ownership pointer to a semantic value in any domain.
Create a temporary directory.
std::shared_ptr< class SmtSolver > SmtSolverPtr
Reference-counting pointer for SMT solvers.