 |
|
 |
|
| Files: |
1 |
|
Branches Taken: |
100.0% |
3 / 3 |
| Generated: |
2009-05-17 22:47 |
|
Branches Executed: |
100.0% |
3 / 3 |
| |
|
Line Coverage: |
100.0% |
23 / 23 |
| |
 |
|
 |
1 : //===- Memory.h - Abstract Execution Engine Interface --*- C++ -*------===//
2 :
3 : #ifndef KLEE_MEMORY_H
4 : #define KLEE_MEMORY_H
5 :
6 : #include "klee/Expr.h"
7 :
8 : #include <vector>
9 : #include <string>
10 :
11 : namespace llvm {
12 : class Value;
13 : }
14 :
15 : namespace klee {
16 : namespace serialize {
17 : class access;
18 : }
19 :
20 : class BitArray;
21 : class MemoryManager;
22 : class Solver;
23 :
24 : class MemoryObject {
25 : friend class STPBuilder;
26 :
27 : private:
28 : static int counter;
29 :
30 : // FIXME: I think we want to hide this in the STP layer.
31 : mutable void *stpInitialArray;
32 :
33 : public:
34 : unsigned id;
35 : uint64_t address;
36 :
37 : /// size in bytes
38 : unsigned size;
39 : std::string name;
40 :
41 : bool isLocal;
42 : bool isGlobal;
43 : bool isFixed;
44 :
45 : /// true if created by us.
46 : bool fake_object;
47 : bool isUserSpecified;
48 :
49 : /// "Location" for which this memory object was allocated. This
50 : /// should be either the allocating instruction or the global object
51 : /// it was allocated for (or whatever else makes sense).
52 : const llvm::Value *allocSite;
53 :
54 : /// A list of boolean expressions the user has requested be true of
55 : /// a counterexample. Mutable since we play a little fast and loose
56 : /// with allowing it to be added to during execution (although
57 : /// should sensibly be only at creation time).
58 : mutable std::vector< ref<Expr> > cexPreferences;
59 :
60 : // No copy constructor
61 : MemoryObject(const MemoryObject &b);
62 : MemoryObject &operator=(const MemoryObject &b);
63 :
64 : public:
65 : // XXX this is just a temp hack, should be removed
66 : explicit
67 : MemoryObject(uint64_t _address)
68 : : stpInitialArray(0),
69 : id(counter++),
70 : address(_address),
71 : isFixed(true),
72 6812762: allocSite(0) {
73 : }
74 :
75 : MemoryObject(uint64_t _address, unsigned _size,
76 : bool _isLocal, bool _isGlobal, bool _isFixed,
77 1021: const llvm::Value *_allocSite)
78 : : stpInitialArray(0),
79 : id(counter++),
80 : address(_address),
81 : size(_size),
82 : name("unnamed"),
83 : isLocal(_isLocal),
84 : isGlobal(_isGlobal),
85 : isFixed(_isFixed),
86 : fake_object(false),
87 : isUserSpecified(false),
88 2302533: allocSite(_allocSite) {
89 1021: }
90 :
91 : ~MemoryObject();
92 :
93 : /// Get an identifying string for this allocation.
94 : void getAllocInfo(std::string &result) const;
95 :
96 : void setName(std::string name) {
97 91: this->name = name;
98 : }
99 :
100 4172111: ref<Expr> getBaseExpr() const {
101 8344140: return ConstantExpr::create(address, kMachinePointerType);
102 : }
103 : ref<Expr> getSizeExpr() const {
104 338: return ConstantExpr::create(size, kMachinePointerType);
105 : }
106 3405933: ref<Expr> getOffsetExpr(ref<Expr> pointer) const {
107 3406014: return SubExpr::create(pointer, getBaseExpr());
108 : }
109 79: ref<Expr> getBoundsCheckPointer(ref<Expr> pointer) const {
110 158: return getBoundsCheckOffset(getOffsetExpr(pointer));
111 : }
112 : ref<Expr> getBoundsCheckPointer(ref<Expr> pointer, unsigned bytes) const {
113 26: return getBoundsCheckOffset(getOffsetExpr(pointer), bytes);
114 : }
115 :
116 : ref<Expr> getBoundsCheckOffset(ref<Expr> offset) const {
1: branch 0 taken
78: branch 1 taken
117 79: if (size==0) {
118 2: return EqExpr::create(offset, ref<Expr>(0, kMachinePointerType));
119 : } else {
120 156: return UltExpr::create(offset, getSizeExpr());
121 : }
122 : }
123 3405922: ref<Expr> getBoundsCheckOffset(ref<Expr> offset, unsigned bytes) const {
1: branch 1 taken
124 3405924: if (bytes<=size) {
125 : return UltExpr::create(offset,
126 6811846: ref<Expr>(size - bytes + 1, kMachinePointerType));
127 : } else {
128 1: return ref<Expr>(0, Expr::Bool);
129 : }
130 : }
131 :
132 : private:
133 : friend class serialize::access;
134 : MemoryObject() {}
135 : template<class Archive>
136 : void save(Archive &ar) const {
137 6: ar & id;
138 6: ar & size;
139 : }
140 : template<class Archive>
141 : void load(Archive &ar, unsigned version) {
142 : if (0<version) {
143 : ar & id;
144 : } else {
145 : id = counter++; // keep ids unique invariant
146 : }
147 : ar & size;
148 : address = 0;
149 : isLocal = false;
150 : fake_object = false;
151 : isFixed = true;
152 : stpInitialArray = 0;
153 : }
154 : };
155 :
156 : class ObjectState {
157 : private:
158 : friend class AddressSpace;
159 : unsigned copyOnWriteOwner; // exclusively for AddressSpace
160 :
161 : friend class ObjectHolder;
162 : unsigned refCount;
163 :
164 : uint8_t *concreteStore;
165 : // XXX cleanup name of flushMask (its backwards or something)
166 : BitArray *concreteMask;
167 :
168 : // mutable because may need flushed during read of const
169 : mutable BitArray *flushMask;
170 :
171 : ref<Expr> *knownSymbolics;
172 :
173 : public:
174 : // Use macros so DWD doesn't get all worked up about runtime overhead.
175 : #ifdef KLEE_TRACK_REFERENTS
176 : // DRE: shadow array used to store the referent metadata with each
177 : // word of memory in ObjectState. Allocated lazily. In the final
178 : // version I think we need to have a base and size stored so we can
179 : // do symbolic queries. Right now we just store the address of the
180 : // memory object. Which is of course not the right thing.
181 : ObjectHolder referents;
182 : #endif
183 :
184 : unsigned size;
185 :
186 : // mutable because we may need flush during read of const
187 : mutable UpdateList updates;
188 :
189 : bool readOnly;
190 :
191 : public:
192 : // initial contents are undefined but concrete, it is the creators
193 : // responsibility to initialize the object contents appropriate
194 : ObjectState(const MemoryObject *mo, unsigned size);
195 : ObjectState(const ObjectState &os);
196 : ~ObjectState();
197 :
198 618: void setReadOnly(bool ro) { readOnly = ro; }
199 :
200 : // make all bytes are concrete with undefined values
201 : void makeConcrete();
202 :
203 : void makeSymbolic();
204 :
205 : // make contents all concrete and zero
206 : void initializeToZero();
207 : // make contents all concrete and random
208 : void initializeToRandom();
209 :
210 : ref<Expr> read(ref<Expr> offset, Expr::Width width) const;
211 : ref<Expr> read(unsigned offset, Expr::Width width) const;
212 : ref<Expr> read1(unsigned offset) const;
213 : ref<Expr> read8(unsigned offset) const;
214 : ref<Expr> read16(unsigned offset) const;
215 : ref<Expr> read32(unsigned offset) const;
216 : ref<Expr> read64(unsigned offset) const;
217 :
218 : // return bytes written.
219 : void write(unsigned offset, ref<Expr> value);
220 : void write(ref<Expr> offset, ref<Expr> value);
221 :
222 : void write8(unsigned offset, uint8_t value);
223 : void write16(unsigned offset, uint16_t value);
224 : void write32(unsigned offset, uint32_t value);
225 : void write64(unsigned offset, uint64_t value);
226 :
227 : private:
228 : ref<Expr> read1(ref<Expr> offset) const;
229 : ref<Expr> read8(ref<Expr> offset) const;
230 : ref<Expr> read16(ref<Expr> offset) const;
231 : ref<Expr> read32(ref<Expr> offset) const;
232 : ref<Expr> read64(ref<Expr> offset) const;
233 :
234 : void write1(unsigned offset, ref<Expr> value);
235 : void write1(ref<Expr> offset, ref<Expr> value);
236 : void write8(unsigned offset, ref<Expr> value);
237 : void write8(ref<Expr> offset, ref<Expr> value);
238 : void write16(unsigned offset, ref<Expr> value);
239 : void write16(ref<Expr> offset, ref<Expr> value);
240 : void write32(unsigned offset, ref<Expr> value);
241 : void write32(ref<Expr> offset, ref<Expr> value);
242 : void write64(unsigned offset, ref<Expr> value);
243 : void write64(ref<Expr> offset, ref<Expr> value);
244 :
245 :
246 : void fastRangeCheckOffset(ref<Expr> offset, unsigned *base_r, unsigned *size_r) const;
247 : void flushRangeForRead(unsigned rangeBase, unsigned rangeSize) const;
248 : void flushRangeForWrite(unsigned rangeBase, unsigned rangeSize);
249 :
250 : bool isByteConcrete(unsigned offset) const;
251 : bool isByteFlushed(unsigned offset) const;
252 : bool isByteKnownSymbolic(unsigned offset) const;
253 :
254 : void markByteConcrete(unsigned offset);
255 : void markByteSymbolic(unsigned offset);
256 : void markByteFlushed(unsigned offset);
257 : void markByteUnflushed(unsigned offset);
258 : void setKnownSymbolic(unsigned offset, Expr *value);
259 :
260 : void print();
261 : };
262 :
263 : } // End klee namespace
264 :
265 : #endif
Generated: 2009-05-17 22:47 by zcov