blob: 02e70ed4e5930b112684b25e95773e45762e3990 (
plain) (
blame)
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
|
//===-- 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 <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;
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
|
