1 //===-- Interpreter.h - Abstract Execution Engine Interface -----*- C++ -*-===//
2 //
3 //                     The KLEE Symbolic Virtual Machine
4 //
5 // This file is distributed under the University of Illinois Open Source
6 // License. See LICENSE.TXT for details.
7 //===----------------------------------------------------------------------===//
8 
9 #ifndef KLEE_INTERPRETER_H
10 #define KLEE_INTERPRETER_H
11 
12 #include <map>
13 #include <memory>
14 #include <set>
15 #include <string>
16 #include <vector>
17 
18 struct KTest;
19 
20 namespace llvm {
21 class Function;
22 class LLVMContext;
23 class Module;
24 class raw_ostream;
25 class raw_fd_ostream;
26 }
27 
28 namespace klee {
29 class ExecutionState;
30 class Interpreter;
31 class TreeStreamWriter;
32 
33 class InterpreterHandler {
34 public:
InterpreterHandler()35   InterpreterHandler() {}
~InterpreterHandler()36   virtual ~InterpreterHandler() {}
37 
38   virtual llvm::raw_ostream &getInfoStream() const = 0;
39 
40   virtual std::string getOutputFilename(const std::string &filename) = 0;
41   virtual std::unique_ptr<llvm::raw_fd_ostream> openOutputFile(const std::string &filename) = 0;
42 
43   virtual void incPathsExplored() = 0;
44 
45   virtual void processTestCase(const ExecutionState &state,
46                                const char *err,
47                                const char *suffix) = 0;
48 };
49 
50 class Interpreter {
51 public:
52   /// ModuleOptions - Module level options which can be set when
53   /// registering a module with the interpreter.
54   struct ModuleOptions {
55     std::string LibraryDir;
56     std::string EntryPoint;
57     std::string OptSuffix;
58     bool Optimize;
59     bool CheckDivZero;
60     bool CheckOvershift;
61 
ModuleOptionsModuleOptions62     ModuleOptions(const std::string &_LibraryDir,
63                   const std::string &_EntryPoint, const std::string &_OptSuffix,
64                   bool _Optimize, bool _CheckDivZero, bool _CheckOvershift)
65         : LibraryDir(_LibraryDir), EntryPoint(_EntryPoint),
66           OptSuffix(_OptSuffix), Optimize(_Optimize),
67           CheckDivZero(_CheckDivZero), CheckOvershift(_CheckOvershift) {}
68   };
69 
70   enum LogType
71   {
72 	  STP, //.CVC (STP's native language)
73 	  KQUERY, //.KQUERY files (kQuery native language)
74 	  SMTLIB2 //.SMT2 files (SMTLIB version 2 files)
75   };
76 
77   /// InterpreterOptions - Options varying the runtime behavior during
78   /// interpretation.
79   struct InterpreterOptions {
80     /// A frequency at which to make concrete reads return constrained
81     /// symbolic values. This is used to test the correctness of the
82     /// symbolic execution on concrete programs.
83     unsigned MakeConcreteSymbolic;
84 
InterpreterOptionsInterpreterOptions85     InterpreterOptions()
86       : MakeConcreteSymbolic(false)
87     {}
88   };
89 
90 protected:
91   const InterpreterOptions interpreterOpts;
92 
Interpreter(const InterpreterOptions & _interpreterOpts)93   Interpreter(const InterpreterOptions &_interpreterOpts)
94     : interpreterOpts(_interpreterOpts)
95   {}
96 
97 public:
~Interpreter()98   virtual ~Interpreter() {}
99 
100   static Interpreter *create(llvm::LLVMContext &ctx,
101                              const InterpreterOptions &_interpreterOpts,
102                              InterpreterHandler *ih);
103 
104   /// Register the module to be executed.
105   /// \param modules A list of modules that should form the final
106   ///                module
107   /// \return The final module after it has been optimized, checks
108   /// inserted, and modified for interpretation.
109   virtual llvm::Module *
110   setModule(std::vector<std::unique_ptr<llvm::Module>> &modules,
111             const ModuleOptions &opts) = 0;
112 
113   // supply a tree stream writer which the interpreter will use
114   // to record the concrete path (as a stream of '0' and '1' bytes).
115   virtual void setPathWriter(TreeStreamWriter *tsw) = 0;
116 
117   // supply a tree stream writer which the interpreter will use
118   // to record the symbolic path (as a stream of '0' and '1' bytes).
119   virtual void setSymbolicPathWriter(TreeStreamWriter *tsw) = 0;
120 
121   // supply a test case to replay from. this can be used to drive the
122   // interpretation down a user specified path. use null to reset.
123   virtual void setReplayKTest(const struct KTest *out) = 0;
124 
125   // supply a list of branch decisions specifying which direction to
126   // take on forks. this can be used to drive the interpretation down
127   // a user specified path. use null to reset.
128   virtual void setReplayPath(const std::vector<bool> *path) = 0;
129 
130   // supply a set of symbolic bindings that will be used as "seeds"
131   // for the search. use null to reset.
132   virtual void useSeeds(const std::vector<struct KTest *> *seeds) = 0;
133 
134   virtual void runFunctionAsMain(llvm::Function *f,
135                                  int argc,
136                                  char **argv,
137                                  char **envp) = 0;
138 
139   /*** Runtime options ***/
140 
141   virtual void setHaltExecution(bool value) = 0;
142 
143   virtual void setInhibitForking(bool value) = 0;
144 
145   virtual void prepareForEarlyExit() = 0;
146 
147   /*** State accessor methods ***/
148 
149   virtual unsigned getPathStreamID(const ExecutionState &state) = 0;
150 
151   virtual unsigned getSymbolicPathStreamID(const ExecutionState &state) = 0;
152 
153   virtual void getConstraintLog(const ExecutionState &state,
154                                 std::string &res,
155                                 LogType logFormat = STP) = 0;
156 
157   virtual bool getSymbolicSolution(const ExecutionState &state,
158                                    std::vector<
159                                    std::pair<std::string,
160                                    std::vector<unsigned char> > >
161                                    &res) = 0;
162 
163   virtual void getCoveredLines(const ExecutionState &state,
164                                std::map<const std::string*, std::set<unsigned> > &res) = 0;
165 };
166 
167 } // End klee namespace
168 
169 #endif /* KLEE_INTERPRETER_H */
170