ROSE  0.11.82.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/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>
13 
14 namespace Rose {
15 namespace BinaryAnalysis {
16 namespace Concolic {
17 
19 // Concolic emulation semantics.
21 
23 namespace Emulation {
24 
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 {
37  uint64_t status_;
38 
39 public:
40  explicit Exit(uint64_t status)
41  : Exception("subordinate exit"), status_(status) {}
42 
43  ~Exit() throw () {}
44 
46  uint64_t status() const {
47  return status_;
48  }
49 };
50 
52 class RiscOperators: public InstructionSemantics2::SymbolicSemantics::RiscOperators {
53 public:
55  using Ptr = RiscOperatorsPtr;
56 
58  typedef InstructionSemantics2::SymbolicSemantics::RiscOperators Super;
59 
61  const RegisterDescriptor REG_PATH;
62 
64  struct Settings {
65  };
66 
67 private:
68  Settings settings_; // emulation settings
69  DatabasePtr db_; // concolic database connection
70  TestCasePtr testCase_; // test case whose instructions are being processed
71  const Partitioner2::Partitioner &partitioner_; // ROSE disassembly info about the specimen
72  ArchitecturePtr process_; // subordinate process, concrete state
73  bool hadSystemCall_ = false; // true if we need to call process_->systemCall, cleared each insn
74  ExecutionEventPtr hadSharedMemoryAccess_; // set when shared memory is read, cleared each instruction
75  bool isRecursive_ = false; // if set, avoid calling user-defined functions
76 
77 protected:
79  RiscOperators(const Settings&, const DatabasePtr&, const TestCasePtr&, const Partitioner2::Partitioner&,
80  const ArchitecturePtr&, const InstructionSemantics2::BaseSemantics::StatePtr&, const SmtSolverPtr&);
81 
82 public:
84  static RiscOperatorsPtr instance(const Settings &settings, const DatabasePtr&, const TestCasePtr&,
85  const Partitioner2::Partitioner&, const ArchitecturePtr &process,
87  const SmtSolverPtr &solver = SmtSolverPtr());
88 
91 
92  // Overrides documented in base class
95  const SmtSolverPtr &solver = SmtSolverPtr()) const override {
96  ASSERT_not_implemented("[Robb Matzke 2019-09-24]");
97  }
100  const SmtSolverPtr &solver = SmtSolverPtr()) const override {
101  ASSERT_not_implemented("[Robb Matzke 2019-09-24]");
102  }
103 
104 public:
108  const Settings& settings() const {
109  return settings_;
110  }
111 
113  const Partitioner2::Partitioner& partitioner() const {
114  return partitioner_;
115  }
116 
118  TestCasePtr testCase() const;
119 
121  DatabasePtr database() const;
122 
124  ArchitecturePtr process() const {
125  return process_;
126  }
127 
133  InputVariablesPtr inputVariables() const;
143  bool hadSystemCall() const {
144  return hadSystemCall_;
145  }
146  void hadSystemCall(bool b) {
147  hadSystemCall_ = b;
148  }
157  ExecutionEventPtr hadSharedMemoryAccess() const {
158  return hadSharedMemoryAccess_;
159  }
160  void hadSharedMemoryAccess(const ExecutionEventPtr &e) {
161  hadSharedMemoryAccess_ = e;
162  }
171  bool isRecursive() const {
172  return isRecursive_;
173  }
174  void isRecursive(bool b) {
175  isRecursive_ = b;
176  }
183  size_t wordSizeBits() const;
184 
186  const RegisterDictionary* registerDictionary() const;
187 
193  void createInputVariables(const SmtSolver::Ptr&);
194 
198  void restoreInputVariables(const SmtSolver::Ptr&);
199 
203  void printInputVariables(std::ostream&) const;
204 
206  void printAssertions(std::ostream&) const;
207 
208 public:
209  // Base class overrides -- the acutal RISC operations
210 
211  virtual void startInstruction(SgAsmInstruction*) override;
212 
213  virtual void interrupt(int majr, int minr) override;
214 
216  readRegister(RegisterDescriptor reg, const InstructionSemantics2::BaseSemantics::SValuePtr &dflt) override;
217 
219  readRegister(RegisterDescriptor reg) override {
220  return readRegister(reg, undefined_(reg.nBits()));
221  }
222 
224  peekRegister(RegisterDescriptor reg, const InstructionSemantics2::BaseSemantics::SValuePtr &dflt) override;
225 
226  virtual void
227  writeRegister(RegisterDescriptor, const InstructionSemantics2::BaseSemantics::SValuePtr&) override;
228 
230  readMemory(RegisterDescriptor segreg, const InstructionSemantics2::BaseSemantics::SValuePtr &addr,
233 
235  peekMemory(RegisterDescriptor segreg, const InstructionSemantics2::BaseSemantics::SValuePtr &addr,
237 
238  // Call this when the concrete simulation exits.
239  void doExit(uint64_t);
240 };
241 
243 typedef boost::shared_ptr<class Dispatcher> DispatcherPtr;
244 
246 class Dispatcher: public InstructionSemantics2::DispatcherX86 {
247  typedef InstructionSemantics2::DispatcherX86 Super;
248 public:
249  using Ptr = boost::shared_ptr<Dispatcher>;
250 
251 protected:
253  explicit Dispatcher(const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &ops)
254  : Super(ops, unwrapEmulationOperators(ops)->wordSizeBits(), unwrapEmulationOperators(ops)->registerDictionary()) {}
255 
256 public:
258  static DispatcherPtr instance(const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &ops) {
259  return DispatcherPtr(new Dispatcher(ops));
260  }
261 
262 public:
264  rose_addr_t concreteInstructionPointer() const;
265 
270  bool isTerminated() const;
271 
276  RiscOperatorsPtr emulationOperators() const;
277 
279  static RiscOperatorsPtr unwrapEmulationOperators(const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr&);
280 
282  void processConcreteInstruction(SgAsmInstruction*);
283 
284 public:
285  // overrides
286  virtual void processInstruction(SgAsmInstruction*) override;
287 };
288 
289 } // namespace
290 
292 // Concolic executor.
294 
298 class ConcolicExecutor: public Sawyer::SharedObject {
299 public:
302 
304  struct Settings {
305  Partitioner2::EngineSettings partitionerEngine;
306  Partitioner2::LoaderSettings loader;
307  Partitioner2::DisassemblerSettings disassembler;
308  Partitioner2::PartitionerSettings partitioner;
309  Emulation::RiscOperators::Settings emulationSettings;
310 
311  bool traceSemantics;
312  AddressIntervalSet showingStates;
314  Settings()
315  : traceSemantics(false) {}
316  };
317 
319  struct FunctionCall {
320  std::string printableName;
321  rose_addr_t sourceVa;
322  rose_addr_t targetVa;
323  rose_addr_t stackVa;
325  FunctionCall()
326  : sourceVa(0), targetVa(0), stackVa(0) {}
327 
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) {}
330  };
331 
332 private:
333  Settings settings_;
334  std::vector<FunctionCall> functionCallStack_;
336 
337  // These can be configured by the user before calling configureExecution.
338  SmtSolverPtr solver_; // solver used during execution
339 
340  // These are initialized by configureExecution
341  TestCasePtr testCase_; // currently executing test case
342  TestCaseId testCaseId_; // database ID for currently executing test case
343  DatabasePtr db_; // database for all this stuff
344  Partitioner2::Partitioner partitioner_; // used during execution
345  ArchitecturePtr process_; // the concrete half of the execution
346  Emulation::DispatcherPtr cpu_; // the symbolic half of the execution
347 
348 protected:
349  ConcolicExecutor();
350 
351 public:
352  ~ConcolicExecutor();
353 
354 public:
356  static Ptr instance();
357 
366  const Settings& settings() const { return settings_; }
367  Settings& settings() { return settings_; }
379  SmtSolverPtr solver() const;
380  void solver(const SmtSolverPtr&);
388  DatabasePtr database() const;
389 
395  TestCasePtr testCase() const;
396 
402  TestCaseId testCaseId() const;
403 
409  const Partitioner2::Partitioner& partitioner() const;
410 
416  ArchitecturePtr process() const;
417 
423  Emulation::DispatcherPtr cpu() const;
424 
432  static std::vector<Sawyer::CommandLine::SwitchGroup> commandLineSwitches(Settings &settings /*in,out*/);
433 
438  void configureExecution(const DatabasePtr&, const TestCasePtr&);
439 
446  std::vector<TestCasePtr> execute();
447  std::vector<TestCasePtr> execute(const DatabasePtr&, const TestCasePtr&);
450 private:
451  // Disassemble the specimen and cache the result in the database. If the specimen has previously been disassembled
452  // then reconstitute the analysis results from the database.
453  Partitioner2::Partitioner partition(const SpecimenPtr&);
454 
455  // Create the dispatcher, operators, and memory and register state for the symbolic execution.
456  Emulation::DispatcherPtr makeDispatcher(const ArchitecturePtr&);
457 
458  // Create the underlying process and possibly fast forward it to the state at which it was when the test case was created.
459  void startProcess();
460 
461  // Start up the symbolic part of the testing. This must happen after startProcess.
462  void startDispatcher();
463 
464  // Run the execution
465  void run();
466 
467  // Handle function calls. This is mainly for debugging so we have some idea where we are in the execution when an error
468  // occurs. Returns true if the call stack changed.
469  bool updateCallStack(SgAsmInstruction*);
470 
471  // Print function call stack on multiple lines
472  void printCallStack(std::ostream&);
473 
474  // Handle conditional branches
475  void handleBranch(SgAsmInstruction*);
476 
477  // Generae a new test case. This must be called only after the SMT solver's assertions have been checked and found
478  // to be satisfiable.
479  void generateTestCase(const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr&, const SymbolicExpr::Ptr &childIp);
480 
481  // Save the specified symbolic state to the specified test case.
482  void saveSymbolicState(const Emulation::RiscOperatorsPtr&, const TestCaseId&);
483 
484  // True if the two test cases are close enough that we only need to run one of them.
485  bool areSimilar(const TestCasePtr&, const TestCasePtr&) const;
486 
487 public:
488  // TODO: Lots of properties to control the finer aspects of executing a test case!
489 };
490 
491 } // namespace
492 } // namespace
493 } // namespace
494 
495 #endif
496 #endif
SmtSolverPtr Ptr
Reference counting pointer for SMT solvers.
Definition: SmtSolver.h:48
boost::shared_ptr< RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to a RISC operators object.
Sawyer::SharedPointer< Node > Ptr
Shared-ownership pointer to an expression Node.
Definition: SymbolicExpr.h:166
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.
Definition: SharedPointer.h:68
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.
Definition: SharedObject.h:64
Sawyer::SharedPointer< SValue > SValuePtr
Shared-ownership pointer to a semantic value in any domain.
std::shared_ptr< class SmtSolver > SmtSolverPtr
Reference-counting pointer for SMT solvers.
Definition: SmtSolver.h:26
State
Decoder state.
Definition: String.h:198