ROSE  0.11.51.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 
76 protected:
78  RiscOperators(const Settings&, const DatabasePtr&, const TestCasePtr&, const Partitioner2::Partitioner&,
79  const ArchitecturePtr&, const InstructionSemantics2::BaseSemantics::StatePtr&, const SmtSolverPtr&);
80 
81 public:
83  static RiscOperatorsPtr instance(const Settings &settings, const DatabasePtr&, const TestCasePtr&,
84  const Partitioner2::Partitioner&, const ArchitecturePtr &process,
86  const SmtSolverPtr &solver = SmtSolverPtr());
87 
90 
91  // Overrides documented in base class
94  const SmtSolverPtr &solver = SmtSolverPtr()) const ROSE_OVERRIDE {
95  ASSERT_not_implemented("[Robb Matzke 2019-09-24]");
96  }
99  const SmtSolverPtr &solver = SmtSolverPtr()) const ROSE_OVERRIDE {
100  ASSERT_not_implemented("[Robb Matzke 2019-09-24]");
101  }
102 
103 public:
107  const Settings& settings() const {
108  return settings_;
109  }
110 
112  const Partitioner2::Partitioner& partitioner() const {
113  return partitioner_;
114  }
115 
117  TestCasePtr testCase() const;
118 
120  DatabasePtr database() const;
121 
123  ArchitecturePtr process() const {
124  return process_;
125  }
126 
132  InputVariablesPtr inputVariables() const;
142  bool hadSystemCall() const {
143  return hadSystemCall_;
144  }
145  void hadSystemCall(bool b) {
146  hadSystemCall_ = b;
147  }
156  ExecutionEventPtr hadSharedMemoryAccess() const {
157  return hadSharedMemoryAccess_;
158  }
159  void hadSharedMemoryAccess(const ExecutionEventPtr &e) {
160  hadSharedMemoryAccess_ = e;
161  }
168  size_t wordSizeBits() const;
169 
171  const RegisterDictionary* registerDictionary() const;
172 
178  void createInputVariables(const SmtSolver::Ptr&);
179 
183  void restoreInputVariables(const SmtSolver::Ptr&);
184 
188  void printInputVariables(std::ostream&) const;
189 
191  void printAssertions(std::ostream&) const;
192 
193 public:
194  // Base class overrides -- the acutal RISC operations
195 
196  virtual void startInstruction(SgAsmInstruction*) override;
197 
198  virtual void interrupt(int majr, int minr) ROSE_OVERRIDE;
199 
201  readRegister(RegisterDescriptor reg, const InstructionSemantics2::BaseSemantics::SValuePtr &dflt) ROSE_OVERRIDE;
202 
204  readRegister(RegisterDescriptor reg) ROSE_OVERRIDE {
205  return readRegister(reg, undefined_(reg.nBits()));
206  }
207 
209  peekRegister(RegisterDescriptor reg, const InstructionSemantics2::BaseSemantics::SValuePtr &dflt) ROSE_OVERRIDE;
210 
211  virtual void
212  writeRegister(RegisterDescriptor, const InstructionSemantics2::BaseSemantics::SValuePtr&) override;
213 
215  readMemory(RegisterDescriptor segreg, const InstructionSemantics2::BaseSemantics::SValuePtr &addr,
217  const InstructionSemantics2::BaseSemantics::SValuePtr &cond) ROSE_OVERRIDE;
218 
220  peekMemory(RegisterDescriptor segreg, const InstructionSemantics2::BaseSemantics::SValuePtr &addr,
221  const InstructionSemantics2::BaseSemantics::SValuePtr &dflt) ROSE_OVERRIDE;
222 
223  // Call this when the concrete simulation exits.
224  void doExit(uint64_t);
225 };
226 
228 typedef boost::shared_ptr<class Dispatcher> DispatcherPtr;
229 
231 class Dispatcher: public InstructionSemantics2::DispatcherX86 {
232  typedef InstructionSemantics2::DispatcherX86 Super;
233 public:
234  using Ptr = boost::shared_ptr<Dispatcher>;
235 
236 protected:
238  explicit Dispatcher(const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &ops)
239  : Super(ops, unwrapEmulationOperators(ops)->wordSizeBits(), unwrapEmulationOperators(ops)->registerDictionary()) {}
240 
241 public:
243  static DispatcherPtr instance(const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &ops) {
244  return DispatcherPtr(new Dispatcher(ops));
245  }
246 
247 public:
249  rose_addr_t concreteInstructionPointer() const;
250 
255  bool isTerminated() const;
256 
261  RiscOperatorsPtr emulationOperators() const;
262 
264  static RiscOperatorsPtr unwrapEmulationOperators(const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr&);
265 
267  void processConcreteInstruction(SgAsmInstruction*);
268 
269 public:
270  // overrides
271  virtual void processInstruction(SgAsmInstruction*) ROSE_OVERRIDE;
272 };
273 
274 } // namespace
275 
277 // Concolic executor.
279 
283 class ConcolicExecutor: public Sawyer::SharedObject {
284 public:
287 
289  struct Settings {
290  Partitioner2::EngineSettings partitionerEngine;
291  Partitioner2::LoaderSettings loader;
292  Partitioner2::DisassemblerSettings disassembler;
293  Partitioner2::PartitionerSettings partitioner;
294  Emulation::RiscOperators::Settings emulationSettings;
295 
296  bool traceSemantics;
297  AddressIntervalSet showingStates;
299  Settings()
300  : traceSemantics(false) {}
301  };
302 
304  struct FunctionCall {
305  std::string printableName;
306  rose_addr_t sourceVa;
307  rose_addr_t targetVa;
308  rose_addr_t stackVa;
310  FunctionCall()
311  : sourceVa(0), targetVa(0), stackVa(0) {}
312 
313  FunctionCall(const std::string &printableName, rose_addr_t sourceVa, rose_addr_t targetVa, rose_addr_t stackVa)
314  : printableName(printableName), sourceVa(sourceVa), targetVa(targetVa), stackVa(stackVa) {}
315  };
316 
317 private:
318  Settings settings_;
319  std::vector<FunctionCall> functionCallStack_;
321 
322  // These can be configured by the user before calling configureExecution.
323  SmtSolverPtr solver_; // solver used during execution
324 
325  // These are initialized by configureExecution
326  TestCasePtr testCase_; // currently executing test case
327  TestCaseId testCaseId_; // database ID for currently executing test case
328  DatabasePtr db_; // database for all this stuff
329  Partitioner2::Partitioner partitioner_; // used during execution
330  ArchitecturePtr process_; // the concrete half of the execution
331  Emulation::DispatcherPtr cpu_; // the symbolic half of the execution
332 
333 protected:
334  ConcolicExecutor();
335 
336 public:
337  ~ConcolicExecutor();
338 
339 public:
341  static Ptr instance();
342 
351  const Settings& settings() const { return settings_; }
352  Settings& settings() { return settings_; }
364  SmtSolverPtr solver() const;
365  void solver(const SmtSolverPtr&);
373  DatabasePtr database() const;
374 
380  TestCasePtr testCase() const;
381 
387  TestCaseId testCaseId() const;
388 
394  const Partitioner2::Partitioner& partitioner() const;
395 
401  ArchitecturePtr process() const;
402 
408  Emulation::DispatcherPtr cpu() const;
409 
417  static std::vector<Sawyer::CommandLine::SwitchGroup> commandLineSwitches(Settings &settings /*in,out*/);
418 
423  void configureExecution(const DatabasePtr&, const TestCasePtr&);
424 
431  std::vector<TestCasePtr> execute();
432  std::vector<TestCasePtr> execute(const DatabasePtr&, const TestCasePtr&);
435 private:
436  // Disassemble the specimen and cache the result in the database. If the specimen has previously been disassembled
437  // then reconstitute the analysis results from the database.
438  Partitioner2::Partitioner partition(const SpecimenPtr&);
439 
440  // Create the dispatcher, operators, and memory and register state for the symbolic execution.
441  Emulation::DispatcherPtr makeDispatcher(const ArchitecturePtr&);
442 
443  // Create the underlying process and possibly fast forward it to the state at which it was when the test case was created.
444  void startProcess();
445 
446  // Start up the symbolic part of the testing. This must happen after startProcess.
447  void startDispatcher();
448 
449  // Run the execution
450  void run();
451 
452  // Handle function calls. This is mainly for debugging so we have some idea where we are in the execution when an error
453  // occurs. Returns true if the call stack changed.
454  bool updateCallStack(SgAsmInstruction*);
455 
456  // Print function call stack on multiple lines
457  void printCallStack(std::ostream&);
458 
459  // Handle conditional branches
460  void handleBranch(SgAsmInstruction*);
461 
462  // Generae a new test case. This must be called only after the SMT solver's assertions have been checked and found
463  // to be satisfiable.
464  void generateTestCase(const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr&, const SymbolicExpr::Ptr &childIp);
465 
466  // Save the specified symbolic state to the specified test case.
467  void saveSymbolicState(const Emulation::RiscOperatorsPtr&, const TestCaseId&);
468 
469  // True if the two test cases are close enough that we only need to run one of them.
470  bool areSimilar(const TestCasePtr&, const TestCasePtr&) const;
471 
472 public:
473  // TODO: Lots of properties to control the finer aspects of executing a test case!
474 };
475 
476 } // namespace
477 } // namespace
478 } // namespace
479 
480 #endif
481 #endif
SmtSolverPtr Ptr
Reference counting pointer for SMT solvers.
Definition: SmtSolver.h:39
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:156
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
Name space for the entire library.
Definition: FeasiblePath.h:787
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.
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:25
State
Decoder state.
Definition: String.h:198