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
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
|
//===-- Memory.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_MEMORY_H
#define KLEE_MEMORY_H
#include "klee/Expr.h"
#include "llvm/ADT/StringExtras.h"
#include <vector>
#include <string>
namespace llvm {
class Value;
}
namespace klee {
class BitArray;
class MemoryManager;
class Solver;
class MemoryObject {
friend class STPBuilder;
private:
static int counter;
public:
unsigned id;
uint64_t address;
/// size in bytes
unsigned size;
std::string name;
bool isLocal;
bool isGlobal;
bool isFixed;
/// true if created by us.
bool fake_object;
bool isUserSpecified;
/// "Location" for which this memory object was allocated. This
/// should be either the allocating instruction or the global object
/// it was allocated for (or whatever else makes sense).
const llvm::Value *allocSite;
/// A list of boolean expressions the user has requested be true of
/// a counterexample. Mutable since we play a little fast and loose
/// with allowing it to be added to during execution (although
/// should sensibly be only at creation time).
mutable std::vector< ref<Expr> > cexPreferences;
// DO NOT IMPLEMENT
MemoryObject(const MemoryObject &b);
MemoryObject &operator=(const MemoryObject &b);
public:
// XXX this is just a temp hack, should be removed
explicit
MemoryObject(uint64_t _address)
: id(counter++),
address(_address),
size(0),
isFixed(true),
allocSite(0) {
}
MemoryObject(uint64_t _address, unsigned _size,
bool _isLocal, bool _isGlobal, bool _isFixed,
const llvm::Value *_allocSite)
: id(counter++),
address(_address),
size(_size),
name("unnamed"),
isLocal(_isLocal),
isGlobal(_isGlobal),
isFixed(_isFixed),
fake_object(false),
isUserSpecified(false),
allocSite(_allocSite) {
}
~MemoryObject();
/// Get an identifying string for this allocation.
void getAllocInfo(std::string &result) const;
void setName(std::string name) {
this->name = name;
}
ref<ConstantExpr> getBaseExpr() const {
return ConstantExpr::create(address, kMachinePointerType);
}
ref<ConstantExpr> getSizeExpr() const {
return ConstantExpr::create(size, kMachinePointerType);
}
ref<Expr> getOffsetExpr(ref<Expr> pointer) const {
return SubExpr::create(pointer, getBaseExpr());
}
ref<Expr> getBoundsCheckPointer(ref<Expr> pointer) const {
return getBoundsCheckOffset(getOffsetExpr(pointer));
}
ref<Expr> getBoundsCheckPointer(ref<Expr> pointer, unsigned bytes) const {
return getBoundsCheckOffset(getOffsetExpr(pointer), bytes);
}
ref<Expr> getBoundsCheckOffset(ref<Expr> offset) const {
if (size==0) {
return EqExpr::create(offset, ConstantExpr::alloc(0, kMachinePointerType));
} else {
return UltExpr::create(offset, getSizeExpr());
}
}
ref<Expr> getBoundsCheckOffset(ref<Expr> offset, unsigned bytes) const {
if (bytes<=size) {
return UltExpr::create(offset,
ConstantExpr::alloc(size - bytes + 1, kMachinePointerType));
} else {
return ConstantExpr::alloc(0, Expr::Bool);
}
}
};
class ObjectState {
private:
friend class AddressSpace;
unsigned copyOnWriteOwner; // exclusively for AddressSpace
friend class ObjectHolder;
unsigned refCount;
const MemoryObject *object;
uint8_t *concreteStore;
// XXX cleanup name of flushMask (its backwards or something)
BitArray *concreteMask;
// mutable because may need flushed during read of const
mutable BitArray *flushMask;
ref<Expr> *knownSymbolics;
// mutable because we may need flush during read of const
mutable UpdateList updates;
public:
unsigned size;
bool readOnly;
public:
/// Create a new object state for the given memory object with concrete
/// contents. The initial contents are undefined, it is the callers
/// responsibility to initialize the object contents appropriately.
ObjectState(const MemoryObject *mo);
/// Create a new object state for the given memory object with symbolic
/// contents.
ObjectState(const MemoryObject *mo, const Array *array);
ObjectState(const ObjectState &os);
~ObjectState();
const MemoryObject *getObject() const { return object; }
void setReadOnly(bool ro) { readOnly = ro; }
// make contents all concrete and zero
void initializeToZero();
// make contents all concrete and random
void initializeToRandom();
ref<Expr> read(ref<Expr> offset, Expr::Width width) const;
ref<Expr> read(unsigned offset, Expr::Width width) const;
ref<Expr> read8(unsigned offset) const;
// return bytes written.
void write(unsigned offset, ref<Expr> value);
void write(ref<Expr> offset, ref<Expr> value);
void write8(unsigned offset, uint8_t value);
void write16(unsigned offset, uint16_t value);
void write32(unsigned offset, uint32_t value);
void write64(unsigned offset, uint64_t value);
private:
const UpdateList &getUpdates() const;
void makeConcrete();
void makeSymbolic();
ref<Expr> read8(ref<Expr> offset) const;
void write8(unsigned offset, ref<Expr> value);
void write8(ref<Expr> offset, ref<Expr> value);
void fastRangeCheckOffset(ref<Expr> offset, unsigned *base_r,
unsigned *size_r) const;
void flushRangeForRead(unsigned rangeBase, unsigned rangeSize) const;
void flushRangeForWrite(unsigned rangeBase, unsigned rangeSize);
bool isByteConcrete(unsigned offset) const;
bool isByteFlushed(unsigned offset) const;
bool isByteKnownSymbolic(unsigned offset) const;
void markByteConcrete(unsigned offset);
void markByteSymbolic(unsigned offset);
void markByteFlushed(unsigned offset);
void markByteUnflushed(unsigned offset);
void setKnownSymbolic(unsigned offset, Expr *value);
void print();
};
} // End klee namespace
#endif
|
