 |
|
 |
|
| Files: |
1 |
|
Branches Taken: |
36.4% |
4 / 11 |
| Generated: |
2009-05-17 22:47 |
|
Branches Executed: |
18.2% |
2 / 11 |
| |
|
Line Coverage: |
100.0% |
6 / 6 |
| |
 |
|
 |
1 : //===- Interpreter.h - Abstract Execution Engine Interface --*- C++ -*-===//
2 : //
3 : // Klee
4 : //
5 : //===------------------------------------------------------------------===//
6 : //
7 : // Base interpreter class.
8 : //
9 : //===------------------------------------------------------------------===//
10 :
11 : #ifndef KLEE_INTERPRETER_H
12 : #define KLEE_INTERPRETER_H
13 :
14 : #include <vector>
15 : #include <string>
16 : #include <map>
17 : #include <set>
18 :
19 : struct BOut;
20 :
21 : namespace llvm {
22 : class Function;
23 : class Module;
24 : }
25 :
26 : namespace klee {
27 : class ExecutionState;
28 : class Interpreter;
29 : class TreeStreamWriter;
30 :
31 : class InterpreterHandler {
32 : public:
33 103: InterpreterHandler() {}
103: branch 0 taken
103: branch 1 taken
0: branch 3 not taken
0: branch 4 not taken
0: branch 6 not taken
103: branch 7 taken
0: branch 9 not taken
0: branch 10 not taken
0: branch 12 not taken
0: branch 13 not taken
34 103: virtual ~InterpreterHandler() {};
35 :
36 : virtual std::string getOutputFilename(const std::string &filename) = 0;
37 : virtual std::ostream *openOutputFile(const std::string &filename) = 0;
38 :
39 : virtual unsigned getNumTestCases() = 0;
40 : virtual unsigned getNumPathsExplored() = 0;
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:
50 : /// ModuleOptions - Module level options which can be set when
51 : /// registering a module with the interpreter.
52 : struct ModuleOptions {
53 : bool Optimize;
54 : bool CheckDivZero;
55 :
56 : ModuleOptions(bool _Optimize, bool _CheckDivZero)
57 103: : Optimize(_Optimize), CheckDivZero(_CheckDivZero) {}
58 : };
59 :
60 : /// InterpreterOptions - Options varying the runtime behavior during
61 : /// interpretation.
62 : struct InterpreterOptions {
63 : /// A frequency at which to make concrete reads return constrained
64 : /// symbolic values. This is used to test the correctness of the
65 : /// symbolic execution on concrete programs.
66 : unsigned MakeConcreteSymbolic;
67 :
68 : InterpreterOptions()
69 103: : MakeConcreteSymbolic(false)
70 : {}
71 : };
72 :
73 : protected:
74 : const InterpreterOptions interpreterOpts;
75 :
76 : Interpreter(const InterpreterOptions &_interpreterOpts)
77 103: : interpreterOpts(_interpreterOpts)
78 : {};
79 :
80 : public:
103: branch 0 taken
81 103: virtual ~Interpreter() {};
82 :
83 : static Interpreter *create(const InterpreterOptions &_interpreterOpts,
84 : InterpreterHandler *ih);
85 :
86 : /// Register the module to be executed.
87 : ///
88 : /// \return The final module after it has been optimized, checks
89 : /// inserted, and modified for interpretation.
90 : virtual const llvm::Module *
91 : setModule(llvm::Module *module,
92 : const ModuleOptions &opts,
93 : const std::vector<std::string> &excludeCovFiles) = 0;
94 :
95 : // supply a tree stream writer which the interpreter will use
96 : // to record the concrete path (as a stream of '0' and '1' bytes).
97 : virtual void setPathWriter(TreeStreamWriter *tsw) = 0;
98 :
99 : // supply a tree stream writer which the interpreter will use
100 : // to record the symbolic path (as a stream of '0' and '1' bytes).
101 : virtual void setSymbolicPathWriter(TreeStreamWriter *tsw) = 0;
102 :
103 : // supply a test case to replay from. this can be used to drive the
104 : // interpretation down a user specified path. use null to reset.
105 : virtual void setReplayOut(const struct BOut *out) = 0;
106 :
107 : // supply a list of branch decisions specifying which direction to
108 : // take on forks. this can be used to drive the interpretation down
109 : // a user specified path. use null to reset.
110 : virtual void setReplayPath(const std::vector<bool> *path) = 0;
111 :
112 : // supply a set of symbolic bindings that will be used as "seeds"
113 : // for the search. use null to reset.
114 : virtual void useSeeds(const std::vector<struct BOut *> *seeds) = 0;
115 :
116 : virtual void runFunctionAsMain(llvm::Function *f,
117 : int argc,
118 : char **argv,
119 : char **envp) = 0;
120 :
121 : /*** Runtime options ***/
122 :
123 : virtual void setHaltExecution(bool value) = 0;
124 :
125 : virtual void setInhibitForking(bool value) = 0;
126 :
127 : /*** State accessor methods ***/
128 :
129 : virtual unsigned getPathStreamID(const ExecutionState &state) = 0;
130 :
131 : virtual unsigned getSymbolicPathStreamID(const ExecutionState &state) = 0;
132 :
133 : virtual void getConstraintLog(const ExecutionState &state,
134 : std::string &res,
135 : bool asCVC = false) = 0;
136 :
137 : virtual bool getSymbolicSolution(const ExecutionState &state,
138 : std::vector<
139 : std::pair<std::string,
140 : std::vector<unsigned char> > >
141 : &res) = 0;
142 :
143 : virtual void getCoveredLines(const ExecutionState &state,
144 : std::map<const std::string*, std::set<unsigned> > &res) = 0;
145 : };
146 :
147 : } // End klee namespace
148 :
149 : #endif
Generated: 2009-05-17 22:47 by zcov