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
|
//===-- SpecialFunctionHandler.h --------------------------------*- 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_SPECIALFUNCTIONHANDLER_H
#define KLEE_SPECIALFUNCTIONHANDLER_H
#include <iterator>
#include <map>
#include <vector>
#include <string>
namespace llvm {
class Function;
}
namespace klee {
class Executor;
class Expr;
class ExecutionState;
struct KInstruction;
template<typename T> class ref;
class SpecialFunctionHandler {
public:
typedef void (SpecialFunctionHandler::*Handler)(ExecutionState &state,
KInstruction *target,
std::vector<ref<Expr> >
&arguments);
typedef std::map<const llvm::Function*,
std::pair<Handler,bool> > handlers_ty;
handlers_ty handlers;
class Executor &executor;
struct HandlerInfo {
const char *name;
SpecialFunctionHandler::Handler handler;
bool doesNotReturn; /// Intrinsic terminates the process
bool hasReturnValue; /// Intrinsic has a return value
bool doNotOverride; /// Intrinsic should not be used if already defined
};
// const_iterator to iterate over stored HandlerInfo
// FIXME: Implement >, >=, <=, < operators
class const_iterator : public std::iterator<std::random_access_iterator_tag, HandlerInfo>
{
private:
value_type* base;
int index;
public:
const_iterator(value_type* hi) : base(hi), index(0) {};
const_iterator& operator++(); // pre-fix
const_iterator operator++(int); // post-fix
const value_type& operator*() { return base[index];}
const value_type* operator->() { return &(base[index]);}
const value_type& operator[](int i) { return base[i];}
bool operator==(const_iterator& rhs) { return (rhs.base + rhs.index) == (this->base + this->index);}
bool operator!=(const_iterator& rhs) { return !(*this == rhs);}
};
static const_iterator begin();
static const_iterator end();
static int size();
public:
SpecialFunctionHandler(Executor &_executor);
/// Perform any modifications on the LLVM module before it is
/// prepared for execution. At the moment this involves deleting
/// unused function bodies and marking intrinsics with appropriate
/// flags for use in optimizations.
void prepare();
/// Initialize the internal handler map after the module has been
/// prepared for execution.
void bind();
bool handle(ExecutionState &state,
llvm::Function *f,
KInstruction *target,
std::vector< ref<Expr> > &arguments);
/* Convenience routines */
std::string readStringAtAddress(ExecutionState &state, ref<Expr> address);
/* Handlers */
#define HANDLER(name) void name(ExecutionState &state, \
KInstruction *target, \
std::vector< ref<Expr> > &arguments)
HANDLER(handleAbort);
HANDLER(handleAssert);
HANDLER(handleAssertFail);
HANDLER(handleAssume);
HANDLER(handleCalloc);
HANDLER(handleCheckMemoryAccess);
HANDLER(handleDefineFixedObject);
HANDLER(handleDelete);
HANDLER(handleDeleteArray);
HANDLER(handleExit);
HANDLER(handleAliasFunction);
HANDLER(handleFree);
HANDLER(handleGetErrno);
HANDLER(handleGetObjSize);
HANDLER(handleGetValue);
HANDLER(handleIsSymbolic);
HANDLER(handleMakeSymbolic);
HANDLER(handleMalloc);
HANDLER(handleMarkGlobal);
HANDLER(handleMerge);
HANDLER(handleNew);
HANDLER(handleNewArray);
HANDLER(handlePreferCex);
HANDLER(handlePrintExpr);
HANDLER(handlePrintRange);
HANDLER(handleRange);
HANDLER(handleRealloc);
HANDLER(handleReportError);
HANDLER(handleRevirtObjects);
HANDLER(handleSetForking);
HANDLER(handleSilentExit);
HANDLER(handleStackTrace);
HANDLER(handleUnderConstrained);
HANDLER(handleWarning);
HANDLER(handleWarningOnce);
#undef HANDLER
};
} // End klee namespace
#endif
|
