klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
Interpreter.h
Go to the documentation of this file.
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 <vector>
13 #include <string>
14 #include <map>
15 #include <set>
16 
17 struct KTest;
18 
19 namespace llvm {
20 class Function;
21 class Module;
22 class raw_ostream;
23 class raw_fd_ostream;
24 }
25 
26 namespace klee {
27 class ExecutionState;
28 class Interpreter;
29 class TreeStreamWriter;
30 
32 public:
34  virtual ~InterpreterHandler() {}
35 
36  virtual llvm::raw_ostream &getInfoStream() const = 0;
37 
38  virtual std::string getOutputFilename(const std::string &filename) = 0;
39  virtual llvm::raw_fd_ostream *openOutputFile(const std::string &filename) = 0;
40 
41  virtual void incPathsExplored() = 0;
42 
43  virtual void processTestCase(const ExecutionState &state,
44  const char *err,
45  const char *suffix) = 0;
46 };
47 
48 class Interpreter {
49 public:
52  struct ModuleOptions {
53  std::string LibraryDir;
54  bool Optimize;
57 
58  ModuleOptions(const std::string& _LibraryDir,
59  bool _Optimize, bool _CheckDivZero,
60  bool _CheckOvershift)
61  : LibraryDir(_LibraryDir), Optimize(_Optimize),
62  CheckDivZero(_CheckDivZero), CheckOvershift(_CheckOvershift) {}
63  };
64 
65  enum LogType
66  {
67  STP, //.CVC (STP's native language)
68  KQUERY, //.PC files (kQuery native language)
69  SMTLIB2 //.SMT2 files (SMTLIB version 2 files)
70  };
71 
79 
81  : MakeConcreteSymbolic(false)
82  {}
83  };
84 
85 protected:
87 
88  Interpreter(const InterpreterOptions &_interpreterOpts)
89  : interpreterOpts(_interpreterOpts)
90  {}
91 
92 public:
93  virtual ~Interpreter() {}
94 
95  static Interpreter *create(const InterpreterOptions &_interpreterOpts,
96  InterpreterHandler *ih);
97 
102  virtual const llvm::Module *
103  setModule(llvm::Module *module,
104  const ModuleOptions &opts) = 0;
105 
106  // supply a tree stream writer which the interpreter will use
107  // to record the concrete path (as a stream of '0' and '1' bytes).
108  virtual void setPathWriter(TreeStreamWriter *tsw) = 0;
109 
110  // supply a tree stream writer which the interpreter will use
111  // to record the symbolic path (as a stream of '0' and '1' bytes).
112  virtual void setSymbolicPathWriter(TreeStreamWriter *tsw) = 0;
113 
114  // supply a test case to replay from. this can be used to drive the
115  // interpretation down a user specified path. use null to reset.
116  virtual void setReplayOut(const struct KTest *out) = 0;
117 
118  // supply a list of branch decisions specifying which direction to
119  // take on forks. this can be used to drive the interpretation down
120  // a user specified path. use null to reset.
121  virtual void setReplayPath(const std::vector<bool> *path) = 0;
122 
123  // supply a set of symbolic bindings that will be used as "seeds"
124  // for the search. use null to reset.
125  virtual void useSeeds(const std::vector<struct KTest *> *seeds) = 0;
126 
127  virtual void runFunctionAsMain(llvm::Function *f,
128  int argc,
129  char **argv,
130  char **envp) = 0;
131 
132  /*** Runtime options ***/
133 
134  virtual void setHaltExecution(bool value) = 0;
135 
136  virtual void setInhibitForking(bool value) = 0;
137 
138  /*** State accessor methods ***/
139 
140  virtual unsigned getPathStreamID(const ExecutionState &state) = 0;
141 
142  virtual unsigned getSymbolicPathStreamID(const ExecutionState &state) = 0;
143 
144  virtual void getConstraintLog(const ExecutionState &state,
145  std::string &res,
146  LogType logFormat = STP) = 0;
147 
148  virtual bool getSymbolicSolution(const ExecutionState &state,
149  std::vector<
150  std::pair<std::string,
151  std::vector<unsigned char> > >
152  &res) = 0;
153 
154  virtual void getCoveredLines(const ExecutionState &state,
155  std::map<const std::string*, std::set<unsigned> > &res) = 0;
156 };
157 
158 } // End klee namespace
159 
160 #endif
virtual void getConstraintLog(const ExecutionState &state, std::string &res, LogType logFormat=STP)=0
Definition: KTest.h:26
virtual void useSeeds(const std::vector< struct KTest * > *seeds)=0
virtual const llvm::Module * setModule(llvm::Module *module, const ModuleOptions &opts)=0
int const char const char * suffix
Definition: klee.h:68
virtual void setReplayPath(const std::vector< bool > *path)=0
virtual void setInhibitForking(bool value)=0
virtual ~Interpreter()
Definition: Interpreter.h:93
virtual void incPathsExplored()=0
virtual llvm::raw_fd_ostream * openOutputFile(const std::string &filename)=0
virtual unsigned getPathStreamID(const ExecutionState &state)=0
Interpreter(const InterpreterOptions &_interpreterOpts)
Definition: Interpreter.h:88
virtual void setHaltExecution(bool value)=0
virtual void setSymbolicPathWriter(TreeStreamWriter *tsw)=0
virtual void processTestCase(const ExecutionState &state, const char *err, const char *suffix)=0
virtual llvm::raw_ostream & getInfoStream() const =0
static Interpreter * create(const InterpreterOptions &_interpreterOpts, InterpreterHandler *ih)
Definition: Executor.cpp:3573
const InterpreterOptions interpreterOpts
Definition: Interpreter.h:86
virtual void setPathWriter(TreeStreamWriter *tsw)=0
virtual bool getSymbolicSolution(const ExecutionState &state, std::vector< std::pair< std::string, std::vector< unsigned char > > > &res)=0
virtual void runFunctionAsMain(llvm::Function *f, int argc, char **argv, char **envp)=0
virtual void setReplayOut(const struct KTest *out)=0
virtual ~InterpreterHandler()
Definition: Interpreter.h:34
virtual void getCoveredLines(const ExecutionState &state, std::map< const std::string *, std::set< unsigned > > &res)=0
virtual std::string getOutputFilename(const std::string &filename)=0
ModuleOptions(const std::string &_LibraryDir, bool _Optimize, bool _CheckDivZero, bool _CheckOvershift)
Definition: Interpreter.h:58
virtual unsigned getSymbolicPathStreamID(const ExecutionState &state)=0