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