ROSE  0.11.145.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/Settings.h>
6 
7 #include <Rose/BinaryAnalysis/BasicTypes.h>
8 #include <Rose/Yaml.h>
9 
10 #include <Sawyer/FileSystem.h>
11 
12 namespace Rose {
13 namespace BinaryAnalysis {
14 namespace Concolic {
15 
17 // Concolic executor.
19 
23 class ConcolicExecutor: public Sawyer::SharedObject {
24 public:
27 
29  struct FunctionCall {
30  std::string printableName;
31  rose_addr_t sourceVa;
32  rose_addr_t targetVa;
33  rose_addr_t stackVa;
35  FunctionCall()
36  : sourceVa(0), targetVa(0), stackVa(0) {}
37 
38  FunctionCall(const std::string &printableName, rose_addr_t sourceVa, rose_addr_t targetVa, rose_addr_t stackVa)
39  : printableName(printableName), sourceVa(sourceVa), targetVa(targetVa), stackVa(stackVa) {}
40  };
41 
42 private:
43  ConcolicExecutorSettings settings_;
44  std::vector<FunctionCall> functionCallStack_;
46 
47  // These can be configured by the user before calling configureExecution.
48  SmtSolverPtr solver_; // solver used during execution
49 
50  // These are initialized by configureExecution
51  TestCasePtr testCase_; // currently executing test case
52  TestCaseId testCaseId_; // database ID for currently executing test case
53  DatabasePtr db_; // database for all this stuff
54  Partitioner2::PartitionerPtr partitioner_; // used during execution
55  ArchitecturePtr process_; // the concrete half of the execution
56  Emulation::DispatcherPtr cpu_; // the symbolic half of the execution
57 
58 protected:
59  ConcolicExecutor();
60 
61 public:
62  ~ConcolicExecutor();
63 
64 public:
66  static Ptr instance();
67 
76  const ConcolicExecutorSettings& settings() const;
77  ConcolicExecutorSettings& settings();
78  void settings(const ConcolicExecutorSettings&);
90  SmtSolverPtr solver() const;
91  void solver(const SmtSolverPtr&);
99  DatabasePtr database() const;
100 
106  TestCasePtr testCase() const;
107 
113  TestCaseId testCaseId() const;
114 
120  Partitioner2::PartitionerConstPtr partitioner() const;
121 
127  ArchitecturePtr process() const;
128 
134  Emulation::DispatcherPtr cpu() const;
135 
143  static std::vector<Sawyer::CommandLine::SwitchGroup> commandLineSwitches(ConcolicExecutorSettings &settings /*in,out*/);
144 
152  void configureExecution(const DatabasePtr&, const TestCasePtr&, const Yaml::Node &config);
153 
160  std::vector<TestCasePtr> execute();
161  std::vector<TestCasePtr> execute(const DatabasePtr&, const TestCasePtr&, const Yaml::Node &config);
164 private:
165  // Disassemble the specimen and cache the result in the database. If the specimen has previously been disassembled
166  // then reconstitute the analysis results from the database.
167  Partitioner2::PartitionerPtr partition(const SpecimenPtr&, const ArchitecturePtr&);
168 
169  // Create the dispatcher, operators, and memory and register state for the symbolic execution.
170  Emulation::DispatcherPtr makeDispatcher(const ArchitecturePtr&);
171 
172  // Create the underlying process and possibly fast forward it to the state at which it was when the test case was created.
173  void startProcess();
174 
175  // Start up the symbolic part of the testing. This must happen after startProcess.
176  void startDispatcher();
177 
178  // Run the execution
179  void run();
180 
181  // Handle function calls. This is mainly for debugging so we have some idea where we are in the execution when an error
182  // occurs. Returns true if the call stack changed.
183  bool updateCallStack(SgAsmInstruction*);
184 
185  // Print function call stack on multiple lines
186  void printCallStack(std::ostream&);
187 
188  // Handle conditional branches
189  void handleBranch(SgAsmInstruction*);
190 
191  // Generae a new test case. This must be called only after the SMT solver's assertions have been checked and found
192  // to be satisfiable.
193  void generateTestCase(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&, const SymbolicExpression::Ptr &childIp);
194 
195  // Save the specified symbolic state to the specified test case.
196  void saveSymbolicState(const Emulation::RiscOperatorsPtr&, const TestCaseId&);
197 
198  // True if the two test cases are close enough that we only need to run one of them.
199  bool areSimilar(const TestCasePtr&, const TestCasePtr&) const;
200 
201 public:
202  // TODO: Lots of properties to control the finer aspects of executing a test case!
203 };
204 
205 } // namespace
206 } // namespace
207 } // namespace
208 
209 #endif
210 #endif
boost::shared_ptr< RiscOperators > RiscOperatorsPtr
Shared-ownership pointer to a RISC operators object.
Base class for machine instructions.
Sawyer::CommandLine::SwitchGroup commandLineSwitches(Settings &settings)
Command-line switches for unparser settings.
Settings settings
Command-line settings for the rosebud tool.
Main namespace for the ROSE library.
Reference-counting intrusive smart pointer.
Definition: SharedPointer.h:68
Sawyer::SharedPointer< Partitioner > PartitionerPtr
Shared-ownership pointer for Partitioner.
Sawyer::SharedPointer< const Partitioner > PartitionerConstPtr
Shared-ownership pointer for Partitioner.
Base class for reference counted objects.
Definition: SharedObject.h:64
Sawyer::SharedPointer< Node > Ptr
Reference counting pointer.
std::shared_ptr< SmtSolver > SmtSolverPtr
Reference counting pointer.