ROSE  0.11.101.0
ConcolicExecutor.h
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>
6 
7 #include <Rose/BinaryAnalysis/BasicTypes.h>
8 #include <Rose/BinaryAnalysis/Concolic/LinuxI386.h>
9 #include <Rose/BinaryAnalysis/Debugger.h>
10 #include <Rose/BinaryAnalysis/InstructionSemantics/DispatcherX86.h>
11 #include <Rose/BinaryAnalysis/InstructionSemantics/SymbolicSemantics.h>
12 #include <Rose/BinaryAnalysis/Partitioner2/Partitioner.h>
13 #include <Sawyer/FileSystem.h>
14 
15 namespace Rose {
16 namespace BinaryAnalysis {
17 namespace Concolic {
18 
20 // Concolic emulation semantics.
22 
24 namespace Emulation {
25 
26 typedef InstructionSemantics::SymbolicSemantics::Formatter SValueFormatter;
28 typedef InstructionSemantics::SymbolicSemantics::SValue SValue;
29 typedef InstructionSemantics::SymbolicSemantics::RegisterStatePtr RegisterStatePtr;
30 typedef InstructionSemantics::SymbolicSemantics::RegisterState RegisterState;
31 typedef InstructionSemantics::SymbolicSemantics::MemoryStatePtr MemoryStatePtr;
32 typedef InstructionSemantics::SymbolicSemantics::MemoryState MemoryState;
33 typedef InstructionSemantics::SymbolicSemantics::StatePtr StatePtr;
34 typedef InstructionSemantics::SymbolicSemantics::State State;
37 class Exit: public Exception {
38  uint64_t status_;
39 
40 public:
41  explicit Exit(uint64_t status)
42  : Exception("subordinate exit"), status_(status) {}
43 
44  ~Exit() throw () {}
45 
47  uint64_t status() const {
48  return status_;
49  }
50 };
51 
53 class RiscOperators: public InstructionSemantics::SymbolicSemantics::RiscOperators {
54 public:
56  using Ptr = RiscOperatorsPtr;
57 
59  typedef InstructionSemantics::SymbolicSemantics::RiscOperators Super;
60 
62  const RegisterDescriptor REG_PATH;
63 
65  struct Settings {
66  };
67 
68 private:
69  Settings settings_; // emulation settings
70  DatabasePtr db_; // concolic database connection
71  TestCasePtr testCase_; // test case whose instructions are being processed
72  const Partitioner2::Partitioner &partitioner_; // ROSE disassembly info about the specimen
73  ArchitecturePtr process_; // subordinate process, concrete state
74  bool hadSystemCall_ = false; // true if we need to call process_->systemCall, cleared each insn
75  ExecutionEventPtr hadSharedMemoryAccess_; // set when shared memory is read, cleared each instruction
76  bool isRecursive_ = false; // if set, avoid calling user-defined functions
77 
78 protected:
80  RiscOperators(const Settings&, const DatabasePtr&, const TestCasePtr&, const Partitioner2::Partitioner&,
81  const ArchitecturePtr&, const InstructionSemantics::BaseSemantics::StatePtr&, const SmtSolverPtr&);
82 
83 public:
85  static RiscOperatorsPtr instance(const Settings &settings, const DatabasePtr&, const TestCasePtr&,
86  const Partitioner2::Partitioner&, const ArchitecturePtr &process,
88  const SmtSolverPtr &solver = SmtSolverPtr());
89 
92 
93  // Overrides documented in base class
96  const SmtSolverPtr &solver = SmtSolverPtr()) const override {
97  ASSERT_not_implemented("[Robb Matzke 2019-09-24]");
98  }
101  const SmtSolverPtr &solver = SmtSolverPtr()) const override {
102  ASSERT_not_implemented("[Robb Matzke 2019-09-24]");
103  }
104 
105 public:
109  const Settings& settings() const {
110  return settings_;
111  }
112 
114  const Partitioner2::Partitioner& partitioner() const {
115  return partitioner_;
116  }
117 
119  TestCasePtr testCase() const;
120 
122  DatabasePtr database() const;
123 
125  ArchitecturePtr process() const {
126  return process_;
127  }
128 
134  InputVariablesPtr inputVariables() const;
144  bool hadSystemCall() const {
145  return hadSystemCall_;
146  }
147  void hadSystemCall(bool b) {
148  hadSystemCall_ = b;
149  }
158  ExecutionEventPtr hadSharedMemoryAccess() const {
159  return hadSharedMemoryAccess_;
160  }
161  void hadSharedMemoryAccess(const ExecutionEventPtr &e) {
162  hadSharedMemoryAccess_ = e;
163  }
172  bool isRecursive() const {
173  return isRecursive_;
174  }
175  void isRecursive(bool b) {
176  isRecursive_ = b;
177  }
184  size_t wordSizeBits() const;
185 
187  RegisterDictionaryPtr registerDictionary() const;
188 
194  void createInputVariables(const SmtSolver::Ptr&);
195 
199  void restoreInputVariables(const SmtSolver::Ptr&);
200 
204  void printInputVariables(std::ostream&) const;
205 
207  void printAssertions(std::ostream&) const;
208 
209 public:
210  // Base class overrides -- the acutal RISC operations
211 
212  virtual void startInstruction(SgAsmInstruction*) override;
213 
214  virtual void interrupt(int majr, int minr) override;
215 
217  readRegister(RegisterDescriptor reg, const InstructionSemantics::BaseSemantics::SValuePtr &dflt) override;
218 
220  readRegister(RegisterDescriptor reg) override {
221  return readRegister(reg, undefined_(reg.nBits()));
222  }
223 
225  peekRegister(RegisterDescriptor reg, const InstructionSemantics::BaseSemantics::SValuePtr &dflt) override;
226 
227  virtual void
228  writeRegister(RegisterDescriptor, const InstructionSemantics::BaseSemantics::SValuePtr&) override;
229 
231  readMemory(RegisterDescriptor segreg, const InstructionSemantics::BaseSemantics::SValuePtr &addr,
234 
236  peekMemory(RegisterDescriptor segreg, const InstructionSemantics::BaseSemantics::SValuePtr &addr,
238 
239  // Call this when the concrete simulation exits.
240  void doExit(uint64_t);
241 };
242 
244 typedef boost::shared_ptr<class Dispatcher> DispatcherPtr;
245 
247 class Dispatcher: public InstructionSemantics::DispatcherX86 {
248  typedef InstructionSemantics::DispatcherX86 Super;
249 public:
250  using Ptr = boost::shared_ptr<Dispatcher>;
251 
252 protected:
254  explicit Dispatcher(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr &ops)
255  : Super(ops, unwrapEmulationOperators(ops)->wordSizeBits(), unwrapEmulationOperators(ops)->registerDictionary()) {}
256 
257 public:
259  static DispatcherPtr instance(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr &ops) {
260  return DispatcherPtr(new Dispatcher(ops));
261  }
262 
263 public:
265  rose_addr_t concreteInstructionPointer() const;
266 
271  bool isTerminated() const;
272 
277  RiscOperatorsPtr emulationOperators() const;
278 
280  static RiscOperatorsPtr unwrapEmulationOperators(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&);
281 
283  void processConcreteInstruction(SgAsmInstruction*);
284 
285 public:
286  // overrides
287  virtual void processInstruction(SgAsmInstruction*) override;
288 };
289 
290 } // namespace
291 
293 // Concolic executor.
295 
299 class ConcolicExecutor: public Sawyer::SharedObject {
300 public:
303 
305  struct Settings {
306  Partitioner2::EngineSettings partitionerEngine;
307  Partitioner2::LoaderSettings loader;
308  Partitioner2::DisassemblerSettings disassembler;
309  Partitioner2::PartitionerSettings partitioner;
310  Emulation::RiscOperators::Settings emulationSettings;
311 
312  bool traceSemantics;
313  AddressIntervalSet showingStates;
315  Settings()
316  : traceSemantics(false) {}
317  };
318 
320  struct FunctionCall {
321  std::string printableName;
322  rose_addr_t sourceVa;
323  rose_addr_t targetVa;
324  rose_addr_t stackVa;
326  FunctionCall()
327  : sourceVa(0), targetVa(0), stackVa(0) {}
328 
329  FunctionCall(const std::string &printableName, rose_addr_t sourceVa, rose_addr_t targetVa, rose_addr_t stackVa)
330  : printableName(printableName), sourceVa(sourceVa), targetVa(targetVa), stackVa(stackVa) {}
331  };
332 
333 private:
334  Settings settings_;
335  std::vector<FunctionCall> functionCallStack_;
337 
338  // These can be configured by the user before calling configureExecution.
339  SmtSolverPtr solver_; // solver used during execution
340 
341  // These are initialized by configureExecution
342  TestCasePtr testCase_; // currently executing test case
343  TestCaseId testCaseId_; // database ID for currently executing test case
344  DatabasePtr db_; // database for all this stuff
345  Partitioner2::Partitioner partitioner_; // used during execution
346  ArchitecturePtr process_; // the concrete half of the execution
347  Emulation::DispatcherPtr cpu_; // the symbolic half of the execution
348 
349 protected:
350  ConcolicExecutor();
351 
352 public:
353  ~ConcolicExecutor();
354 
355 public:
357  static Ptr instance();
358 
367  const Settings& settings() const { return settings_; }
368  Settings& settings() { return settings_; }
380  SmtSolverPtr solver() const;
381  void solver(const SmtSolverPtr&);
389  DatabasePtr database() const;
390 
396  TestCasePtr testCase() const;
397 
403  TestCaseId testCaseId() const;
404 
410  const Partitioner2::Partitioner& partitioner() const;
411 
417  ArchitecturePtr process() const;
418 
424  Emulation::DispatcherPtr cpu() const;
425 
433  static std::vector<Sawyer::CommandLine::SwitchGroup> commandLineSwitches(Settings &settings /*in,out*/);
434 
439  void configureExecution(const DatabasePtr&, const TestCasePtr&);
440 
447  std::vector<TestCasePtr> execute();
448  std::vector<TestCasePtr> execute(const DatabasePtr&, const TestCasePtr&);
451 private:
452  // Disassemble the specimen and cache the result in the database. If the specimen has previously been disassembled
453  // then reconstitute the analysis results from the database.
454  Partitioner2::Partitioner partition(const SpecimenPtr&);
455 
456  // Create the dispatcher, operators, and memory and register state for the symbolic execution.
457  Emulation::DispatcherPtr makeDispatcher(const ArchitecturePtr&);
458 
459  // Create the underlying process and possibly fast forward it to the state at which it was when the test case was created.
460  void startProcess();
461 
462  // Start up the symbolic part of the testing. This must happen after startProcess.
463  void startDispatcher();
464 
465  // Run the execution
466  void run();
467 
468  // Handle function calls. This is mainly for debugging so we have some idea where we are in the execution when an error
469  // occurs. Returns true if the call stack changed.
470  bool updateCallStack(SgAsmInstruction*);
471 
472  // Print function call stack on multiple lines
473  void printCallStack(std::ostream&);
474 
475  // Handle conditional branches
476  void handleBranch(SgAsmInstruction*);
477 
478  // Generae a new test case. This must be called only after the SMT solver's assertions have been checked and found
479  // to be satisfiable.
480  void generateTestCase(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&, const SymbolicExpression::Ptr &childIp);
481 
482  // Save the specified symbolic state to the specified test case.
483  void saveSymbolicState(const Emulation::RiscOperatorsPtr&, const TestCaseId&);
484 
485  // True if the two test cases are close enough that we only need to run one of them.
486  bool areSimilar(const TestCasePtr&, const TestCasePtr&) const;
487 
488 public:
489  // TODO: Lots of properties to control the finer aspects of executing a test case!
490 };
491 
492 } // namespace
493 } // namespace
494 } // namespace
495 
496 #endif
497 #endif
SmtSolverPtr Ptr
Reference counting pointer for SMT solvers.
Definition: SmtSolver.h:45
boost::shared_ptr< RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to a RISC operators object.
Base class for machine instructions.
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.
Main namespace for the ROSE library.
boost::shared_ptr< class Dispatcher > DispatcherPtr
Shared-ownership pointer to Dispatcher.
Sawyer::SharedPointer< class SValue > SValuePtr
Shared-ownership pointer for symbolic semantic value.
Reference-counting intrusive smart pointer.
Definition: SharedPointer.h:68
boost::shared_ptr< State > StatePtr
Shared-ownership pointer to a semantic state.
boost::shared_ptr< class RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to concrete RISC operations.
Sawyer::CommandLine::SwitchGroup commandLineSwitches(Settings &)
Command-line switches for settings.
Binary analysis.
Sawyer::SharedPointer< SValue > SValuePtr
Shared-ownership pointer to a semantic value in any domain.
Base class for reference counted objects.
Definition: SharedObject.h:64
Sawyer::SharedPointer< Node > Ptr
Reference counting pointer.
State
Decoder state.
Definition: String.h:198