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