 |
|
 |
|
| Files: |
1 |
|
Branches Taken: |
75.5% |
173 / 229 |
| Generated: |
2009-05-17 22:47 |
|
Branches Executed: |
72.9% |
167 / 229 |
| |
|
Line Coverage: |
80.3% |
248 / 309 |
| |
 |
|
 |
1 : /* -*- mode: c++; c-basic-offset: 2; -*- */
2 :
3 : #include "Common.h"
4 :
5 : #include "klee/Memory.h"
6 :
7 : #include "klee/Expr.h"
8 : #include "klee/Machine.h"
9 : #include "klee/Solver.h"
10 : #include "klee/util/BitArray.h"
11 :
12 : #include "ObjectHolder.h"
13 :
14 : #include <llvm/Function.h>
15 : #include <llvm/Instruction.h>
16 : #include <llvm/Value.h>
17 :
18 : #include <iostream>
19 : #include <cassert>
20 : #include <sstream>
21 :
22 : using namespace llvm;
23 : using namespace klee;
24 :
25 : /***/
26 :
19508597: branch 0 taken
19508597: branch 1 taken
19508597: branch 2 taken
0: branch 3 not taken
27 19508597: ObjectHolder::ObjectHolder(const ObjectHolder &b) : os(b.os) { if (os) ++os->refCount; }
28 :
802822: branch 0 taken
802822: branch 1 taken
802822: branch 2 taken
0: branch 3 not taken
29 802822: ObjectHolder::ObjectHolder(ObjectState *_os) : os(_os) { if (os) ++os->refCount; }
30 :
20775683: branch 0 taken
103: branch 1 taken
802822: branch 2 taken
19972861: branch 3 taken
802822: branch 4 taken
19972964: branch 5 taken
802822: branch 6 taken
0: branch 7 not taken
802822: branch 10 taken
802822: branch 11 taken
802822: branch 12 taken
802822: branch 13 taken
802822: branch 14 taken
802822: branch 15 taken
802822: branch 16 taken
802822: branch 17 taken
31 20775786: ObjectHolder::~ObjectHolder() { if (os && --os->refCount==0) delete os; }
32 :
33 464264: ObjectHolder &ObjectHolder::operator=(const ObjectHolder &b) {
464264: branch 0 taken
0: branch 1 not taken
34 464264: if (b.os) ++b.os->refCount;
0: branch 0 not taken
464264: branch 1 taken
464264: branch 2 taken
464264: branch 3 taken
0: branch 4 not taken
464264: branch 5 taken
464264: branch 6 taken
464264: branch 7 taken
35 464264: if (os && --os->refCount==0) delete os;
36 464264: os = b.os;
37 464264: return *this;
38 : }
39 :
40 : /***/
41 :
42 : int MemoryObject::counter = 0;
43 :
44 : extern "C" void vc_DeleteExpr(void*);
45 :
46 4172691: MemoryObject::~MemoryObject() {
47 : // XXX gross
103: branch 0 taken
4172588: branch 1 taken
4172588: branch 2 taken
4172588: branch 3 taken
48 4172691: if (stpInitialArray)
49 103: ::vc_DeleteExpr(stpInitialArray);
50 4172691: }
51 :
52 16: void MemoryObject::getAllocInfo(std::string &result) const {
53 16: std::ostringstream info;
54 :
55 48: info << "MO" << id << "[" << size << "]";
56 :
16: branch 0 taken
0: branch 1 not taken
57 16: if (allocSite) {
58 16: info << " allocated at ";
16: branch 0 taken
0: branch 1 not taken
59 32: if (const Instruction *i = dyn_cast<Instruction>(allocSite)) {
60 32: info << i->getParent()->getParent()->getName() << "():";
61 16: info << *i;
0: branch 0 not taken
0: branch 1 not taken
62 0: } else if (const GlobalValue *gv = dyn_cast<GlobalValue>(allocSite)) {
63 0: info << "global:" << gv->getName();
64 : } else {
65 0: info << "value:" << *allocSite;
66 : }
67 : } else {
68 0: info << " (no allocation info)";
69 : }
70 :
71 32: result = info.str();
72 16: }
73 :
74 : /***/
75 :
76 766579: ObjectState::ObjectState(const MemoryObject *mo, unsigned _size)
77 : : copyOnWriteOwner(0),
78 : refCount(0),
79 : concreteStore(new uint8_t[_size]),
80 : concreteMask(0),
81 : flushMask(0),
82 : knownSymbolics(0),
83 : #ifdef KLEE_TRACK_REFERENTS
84 : referents(0),
85 : #endif
86 : size(_size),
87 : updates(mo, false, 0),
88 766579: readOnly(false) {
89 766579: }
90 :
91 36243: ObjectState::ObjectState(const ObjectState &os)
92 : : copyOnWriteOwner(0),
93 : refCount(0),
94 : concreteStore(new uint8_t[os.size]),
95 : concreteMask(os.concreteMask ? new BitArray(*os.concreteMask, os.size) : 0),
96 : flushMask(os.flushMask ? new BitArray(*os.flushMask, os.size) : 0),
97 : knownSymbolics(0),
98 : #ifdef KLEE_TRACK_REFERENTS
99 : referents(os.referents),
100 : #endif
101 : size(os.size),
102 : updates(os.updates),
1663: branch 1 taken
34580: branch 2 taken
10: branch 5 taken
36233: branch 6 taken
0: branch 11 not taken
0: branch 12 not taken
0: branch 15 not taken
0: branch 16 not taken
103 36243: readOnly(false) {
0: branch 0 not taken
36243: branch 1 taken
0: branch 3 not taken
0: branch 4 not taken
104 36243: assert(!os.readOnly && "no need to copy read only object?");
105 :
1662: branch 0 taken
34581: branch 1 taken
34581: branch 2 taken
34581: branch 3 taken
106 36243: if (os.knownSymbolics) {
94743: branch 1 taken
1662: branch 2 taken
0: branch 4 not taken
0: branch 5 not taken
107 96405: knownSymbolics = new ref<Expr>[size];
94743: branch 0 taken
1662: branch 1 taken
1662: branch 2 taken
1662: branch 3 taken
108 96405: for (unsigned i=0; i<size; i++)
109 94743: knownSymbolics[i] = os.knownSymbolics[i];
110 : }
111 :
112 36243: memcpy(concreteStore, os.concreteStore, size*sizeof(*concreteStore));
113 36243: }
114 :
115 802822: ObjectState::~ObjectState() {
5928: branch 0 taken
796894: branch 1 taken
5928: branch 2 taken
0: branch 3 not taken
5928: branch 5 taken
5928: branch 6 taken
5928: branch 7 taken
5928: branch 8 taken
116 808750: if (concreteMask) delete concreteMask;
132: branch 0 taken
802690: branch 1 taken
132: branch 2 taken
0: branch 3 not taken
132: branch 5 taken
132: branch 6 taken
132: branch 7 taken
132: branch 8 taken
117 802954: if (flushMask) delete flushMask;
5819: branch 0 taken
797003: branch 1 taken
5819: branch 2 taken
0: branch 3 not taken
229184: branch 4 taken
5819: branch 5 taken
5819: branch 8 taken
5819: branch 9 taken
5819: branch 10 taken
5819: branch 11 taken
5819: branch 12 taken
5819: branch 13 taken
118 802822: if (knownSymbolics) delete[] knownSymbolics;
802822: branch 0 taken
0: branch 1 not taken
802822: branch 3 taken
802822: branch 4 taken
119 802822: delete[] concreteStore;
120 802822: }
121 :
122 : /***/
123 :
124 755459: void ObjectState::makeConcrete() {
0: branch 0 not taken
755459: branch 1 taken
755459: branch 2 taken
755459: branch 3 taken
125 755459: if (concreteMask) delete concreteMask;
0: branch 0 not taken
755459: branch 1 taken
755459: branch 2 taken
755459: branch 3 taken
126 755459: if (flushMask) delete flushMask;
0: branch 0 not taken
755459: branch 1 taken
755459: branch 2 taken
755459: branch 3 taken
755459: branch 4 taken
755459: branch 5 taken
127 755459: if (knownSymbolics) delete[] knownSymbolics;
128 755459: concreteMask = 0;
129 755459: flushMask = 0;
130 755459: knownSymbolics = 0;
131 755459: }
132 :
133 90: void ObjectState::makeSymbolic() {
134 : assert(!updates.head &&
0: branch 0 not taken
90: branch 1 taken
135 90: "XXX makeSymbolic of objects with symbolic values is unsupported");
136 90: updates.isRooted = true;
137 :
138 : // XXX simplify this, can just delete various arrays I guess
650: branch 0 taken
90: branch 1 taken
139 740: for (unsigned i=0; i<size; i++) {
140 650: markByteSymbolic(i);
141 650: setKnownSymbolic(i, 0);
142 650: markByteFlushed(i);
143 : }
144 90: }
145 :
146 0: void ObjectState::initializeToZero() {
147 0: makeConcrete();
148 0: memset(concreteStore, 0, size);
149 0: }
150 :
151 755459: void ObjectState::initializeToRandom() {
152 755459: makeConcrete();
82648581: branch 0 taken
755459: branch 1 taken
153 83404040: for (unsigned i=0; i<size; i++) {
154 : // randomly selected by 256 sided die
155 82648581: concreteStore[i] = 0xAB;
156 : }
157 755459: }
158 :
159 : /*
160 : Cache Invariants
161 : --
162 : isByteKnownSymbolic(i) => !isByteConcrete(i)
163 : isByteConcrete(i) => !isByteKnownSymbolic(i)
164 : !isByteFlushed(i) => (isByteConcrete(i) || isByteKnownSymbolic(i))
165 : */
166 :
167 : void ObjectState::fastRangeCheckOffset(ref<Expr> offset,
168 : unsigned *base_r,
169 231: unsigned *size_r) const {
170 231: *base_r = 0;
171 231: *size_r = size;
172 231: }
173 :
174 : void ObjectState::flushRangeForRead(unsigned rangeBase,
175 162: unsigned rangeSize) const {
23: branch 0 taken
139: branch 1 taken
176 162: if (!flushMask) flushMask = new BitArray(size, true);
177 :
139798: branch 0 taken
162: branch 1 taken
178 139960: for (unsigned offset=rangeBase; offset<rangeBase+rangeSize; offset++) {
8972: branch 1 taken
130826: branch 2 taken
179 139798: if (!isByteFlushed(offset)) {
8971: branch 1 taken
1: branch 2 taken
180 8972: if (isByteConcrete(offset)) {
181 : updates.extend(ConstantExpr::create(offset, kMachinePointerType),
182 26913: ConstantExpr::create(concreteStore[offset], Expr::Int8));
183 : } else {
0: branch 1 not taken
1: branch 2 taken
184 1: assert(isByteKnownSymbolic(offset) && "invalid bit set in flushMask");
185 : updates.extend(ConstantExpr::create(offset, kMachinePointerType),
186 2: knownSymbolics[offset]);
187 : }
188 :
189 8972: flushMask->unset(offset);
190 : }
191 : }
192 162: }
193 :
194 : void ObjectState::flushRangeForWrite(unsigned rangeBase,
195 69: unsigned rangeSize) {
9: branch 0 taken
60: branch 1 taken
196 69: if (!flushMask) flushMask = new BitArray(size, true);
197 :
1206: branch 0 taken
69: branch 1 taken
198 1275: for (unsigned offset=rangeBase; offset<rangeBase+rangeSize; offset++) {
117: branch 1 taken
1089: branch 2 taken
199 1206: if (!isByteFlushed(offset)) {
117: branch 1 taken
0: branch 2 not taken
200 117: if (isByteConcrete(offset)) {
201 : updates.extend(ConstantExpr::create(offset, kMachinePointerType),
202 351: ConstantExpr::create(concreteStore[offset], Expr::Int8));
203 117: markByteSymbolic(offset);
204 : } else {
0: branch 1 not taken
0: branch 2 not taken
205 0: assert(isByteKnownSymbolic(offset) && "invalid bit set in flushMask");
206 : updates.extend(ConstantExpr::create(offset, kMachinePointerType),
207 0: knownSymbolics[offset]);
208 0: setKnownSymbolic(offset, 0);
209 : }
210 :
211 117: flushMask->unset(offset);
212 : } else {
213 : // flushed bytes that are written over still need
214 : // to be marked out
194: branch 1 taken
895: branch 2 taken
215 1089: if (isByteConcrete(offset)) {
216 194: markByteSymbolic(offset);
0: branch 1 not taken
895: branch 2 taken
217 895: } else if (isByteKnownSymbolic(offset)) {
218 0: setKnownSymbolic(offset, 0);
219 : }
220 : }
221 : }
222 69: }
223 :
224 8523119: bool ObjectState::isByteConcrete(unsigned offset) const {
32666: branch 0 taken
8490453: branch 1 taken
10335: branch 2 taken
22331: branch 3 taken
225 8555785: return !concreteMask || concreteMask->get(offset);
226 : }
227 :
228 142432: bool ObjectState::isByteFlushed(unsigned offset) const {
142432: branch 0 taken
0: branch 1 not taken
133343: branch 2 taken
9089: branch 3 taken
229 284864: return flushMask && !flushMask->get(offset);
230 : }
231 :
232 22331: bool ObjectState::isByteKnownSymbolic(unsigned offset) const {
20008: branch 0 taken
2323: branch 1 taken
20008: branch 3 taken
0: branch 4 not taken
233 22331: return knownSymbolics && knownSymbolics[offset].get();
234 : }
235 :
236 6583495: void ObjectState::markByteConcrete(unsigned offset) {
8258: branch 0 taken
6575237: branch 1 taken
237 6583495: if (concreteMask)
238 8258: concreteMask->set(offset);
239 6583495: }
240 :
241 18175: void ObjectState::markByteSymbolic(unsigned offset) {
4265: branch 0 taken
13910: branch 1 taken
242 18175: if (!concreteMask)
243 4265: concreteMask = new BitArray(size, true);
244 18175: concreteMask->unset(offset);
245 18175: }
246 :
247 6600709: void ObjectState::markByteUnflushed(unsigned offset) {
16: branch 0 taken
6600693: branch 1 taken
248 6600709: if (flushMask)
249 16: flushMask->set(offset);
250 6600709: }
251 :
252 650: void ObjectState::markByteFlushed(unsigned offset) {
90: branch 0 taken
560: branch 1 taken
253 650: if (!flushMask) {
254 90: flushMask = new BitArray(size, false);
255 : } else {
256 560: flushMask->unset(offset);
257 : }
258 650: }
259 :
260 : void ObjectState::setKnownSymbolic(unsigned offset,
261 6601359: Expr *value /* can be null */) {
21304: branch 0 taken
6580055: branch 1 taken
262 6601359: if (knownSymbolics) {
263 21304: knownSymbolics[offset] = value;
264 : } else {
4157: branch 0 taken
6575898: branch 1 taken
265 6580055: if (value) {
134441: branch 1 taken
4157: branch 2 taken
266 138598: knownSymbolics = new ref<Expr>[size];
267 4157: knownSymbolics[offset] = value;
268 : }
269 : }
270 6601359: }
271 :
272 : /***/
273 :
274 8512941: ref<Expr> ObjectState::read8(unsigned offset) const {
8491506: branch 1 taken
21435: branch 2 taken
275 8512941: if (isByteConcrete(offset)) {
276 16983012: return ConstantExpr::create(concreteStore[offset], Expr::Int8);
20007: branch 1 taken
1428: branch 2 taken
277 21435: } else if (isByteKnownSymbolic(offset)) {
278 20007: return knownSymbolics[offset];
279 : } else {
0: branch 1 not taken
1428: branch 2 taken
280 1428: assert(isByteFlushed(offset) && "unflushed byte without cache value");
281 :
282 : return ReadExpr::create(updates,
283 2856: ConstantExpr::create(offset, kMachinePointerType));
284 : }
285 : }
286 :
287 162: ref<Expr> ObjectState::read8(ref<Expr> offset) const {
0: branch 1 not taken
162: branch 2 taken
288 162: assert(!offset.isConstant() && "constant offset passed to symbolic read8");
289 : unsigned base, size;
290 162: fastRangeCheckOffset(offset, &base, &size);
291 162: flushRangeForRead(base, size);
292 :
16: branch 0 taken
146: branch 1 taken
293 162: if (size>4096) {
294 : std::string allocInfo;
295 16: updates.root->getAllocInfo(allocInfo);
296 : klee_warning_once(0, "flushing %d bytes on read, may be slow and/or crash: %s",
297 : size,
298 16: allocInfo.c_str());
299 : }
300 :
301 324: return ReadExpr::create(updates, offset);
302 : }
303 :
304 6583495: void ObjectState::write8(unsigned offset, uint8_t value) {
305 : //assert(read_only == false && "writing to read-only object!");
306 6583495: concreteStore[offset] = value;
307 6583495: setKnownSymbolic(offset, 0);
308 :
309 6583495: markByteConcrete(offset);
310 6583495: markByteUnflushed(offset);
311 6583495: }
312 :
313 17214: void ObjectState::write8(unsigned offset, ref<Expr> value) {
314 : // can happen when ExtractExpr special cases
0: branch 1 not taken
17214: branch 2 taken
315 17214: if (value.isConstant()) {
316 0: write8(offset, (uint8_t) value.getConstantValue());
317 : } else {
318 17214: setKnownSymbolic(offset, value.get());
319 :
320 17214: markByteSymbolic(offset);
321 17214: markByteUnflushed(offset);
322 : }
323 17214: }
324 :
325 69: void ObjectState::write8(ref<Expr> offset, ref<Expr> value) {
0: branch 1 not taken
69: branch 2 taken
326 69: assert(!offset.isConstant() && "constant offset passed to symbolic write8");
327 : unsigned base, size;
328 69: fastRangeCheckOffset(offset, &base, &size);
329 69: flushRangeForWrite(base, size);
330 :
0: branch 0 not taken
69: branch 1 taken
331 69: if (size>4096) {
332 : std::string allocInfo;
333 0: updates.root->getAllocInfo(allocInfo);
334 : klee_warning_once(0, "flushing %d bytes on read, may be slow and/or crash: %s",
335 : size,
336 0: allocInfo.c_str());
337 : }
338 :
339 69: updates.extend(offset, value);
340 69: }
341 :
342 : /***/
343 :
344 2137038: ref<Expr> ObjectState::read(ref<Expr> offset, Expr::Width width) const {
2136962: branch 1 taken
76: branch 2 taken
345 2137038: if (offset.isConstant()) {
346 4273924: return read((unsigned) offset.getConstantValue(), width);
347 : } else {
0: branch 0 not taken
40: branch 1 taken
11: branch 2 taken
25: branch 3 taken
0: branch 4 not taken
0: branch 5 not taken
348 76: switch (width) {
349 0: case Expr::Bool: return read1(offset);
350 80: case Expr::Int8: return read8(offset);
351 22: case Expr::Int16: return read16(offset);
352 50: case Expr::Int32: return read32(offset);
353 0: case Expr::Int64: return read64(offset);
354 0: default: assert(0 && "invalid type");
355 : }
356 : }
357 : }
358 :
359 2136962: ref<Expr> ObjectState::read(unsigned offset, Expr::Width width) const {
1: branch 0 taken
11060: branch 1 taken
1537: branch 2 taken
2124352: branch 3 taken
12: branch 4 taken
0: branch 5 not taken
360 2136962: switch (width) {
361 1: case Expr::Bool: return read1(offset);
362 11060: case Expr::Int8: return read8(offset);
363 1537: case Expr::Int16: return read16(offset);
364 2124352: case Expr::Int32: return read32(offset);
365 12: case Expr::Int64: return read64(offset);
366 0: default: assert(0 && "invalid type");
367 : }
368 : }
369 :
370 1: ref<Expr> ObjectState::read1(unsigned offset) const {
371 1: return ExtractExpr::createByteOff(read8(offset), 0, Expr::Bool);
372 : }
373 :
374 0: ref<Expr> ObjectState::read1(ref<Expr> offset) const {
375 0: return ExtractExpr::createByteOff(read8(offset), 0, Expr::Bool);
376 : }
377 :
378 1537: ref<Expr> ObjectState::read16(unsigned offset) const {
379 : if (kMachineByteOrder == machine::MSB) {
380 : return ConcatExpr::create(read8(offset+0),
381 : read8(offset+1));
382 : } else {
383 : return ConcatExpr::create(read8(offset+1),
384 1537: read8(offset+0));
385 : }
386 : }
387 :
388 11: ref<Expr> ObjectState::read16(ref<Expr> offset) const {
389 : if (kMachineByteOrder == machine::MSB) {
390 : return ConcatExpr::create
391 : (read8(AddExpr::create(offset,
392 : ConstantExpr::create(0,
393 : kMachinePointerType))),
394 : read8(AddExpr::create(offset,
395 : ConstantExpr::create(1,
396 : kMachinePointerType))));
397 : } else {
398 : return ConcatExpr::create
399 : (read8(AddExpr::create(offset,
400 : ConstantExpr::create(1,
401 : kMachinePointerType))),
402 : read8(AddExpr::create(offset,
403 : ConstantExpr::create(0,
404 33: kMachinePointerType))));
405 : }
406 : }
407 :
408 2124352: ref<Expr> ObjectState::read32(unsigned offset) const {
409 : if (kMachineByteOrder == machine::MSB) {
410 : return ConcatExpr::create4(read8(offset+0),
411 : read8(offset+1),
412 : read8(offset+2),
413 : read8(offset+3));
414 : } else {
415 : return ConcatExpr::create4(read8(offset+3),
416 : read8(offset+2),
417 : read8(offset+1),
418 2124352: read8(offset+0));
419 : }
420 : }
421 :
422 25: ref<Expr> ObjectState::read32(ref<Expr> offset) const {
423 : if (kMachineByteOrder == machine::MSB) {
424 : return ConcatExpr::create4
425 : (read8(AddExpr::create(offset,
426 : ConstantExpr::create(0,
427 : kMachinePointerType))),
428 : read8(AddExpr::create(offset,
429 : ConstantExpr::create(1,
430 : kMachinePointerType))),
431 : read8(AddExpr::create(offset,
432 : ConstantExpr::create(2,
433 : kMachinePointerType))),
434 : read8(AddExpr::create(offset,
435 : ConstantExpr::create(3,
436 : kMachinePointerType))));
437 : } else {
438 : return ConcatExpr::create4
439 : (read8(AddExpr::create(offset,
440 : ConstantExpr::create(3,
441 : kMachinePointerType))),
442 : read8(AddExpr::create(offset,
443 : ConstantExpr::create(2,
444 : kMachinePointerType))),
445 : read8(AddExpr::create(offset,
446 : ConstantExpr::create(1,
447 : kMachinePointerType))),
448 : read8(AddExpr::create(offset,
449 : ConstantExpr::create(0,
450 125: kMachinePointerType))));
451 : }
452 : }
453 :
454 12: ref<Expr> ObjectState::read64(unsigned offset) const {
455 : if (kMachineByteOrder == machine::MSB) {
456 : return ConcatExpr::create8(read8(offset+0),
457 : read8(offset+1),
458 : read8(offset+2),
459 : read8(offset+3),
460 : read8(offset+4),
461 : read8(offset+5),
462 : read8(offset+6),
463 : read8(offset+7));
464 : } else {
465 : return ConcatExpr::create8(read8(offset+7),
466 : read8(offset+6),
467 : read8(offset+5),
468 : read8(offset+4),
469 : read8(offset+3),
470 : read8(offset+2),
471 : read8(offset+1),
472 12: read8(offset+0));
473 : }
474 : }
475 :
476 0: ref<Expr> ObjectState::read64(ref<Expr> offset) const {
477 : if (kMachineByteOrder == machine::MSB) {
478 : return ConcatExpr::create8
479 : (read8(AddExpr::create(offset,
480 : ConstantExpr::create(0,
481 : kMachinePointerType))),
482 : read8(AddExpr::create(offset,
483 : ConstantExpr::create(1,
484 : kMachinePointerType))),
485 : read8(AddExpr::create(offset,
486 : ConstantExpr::create(2,
487 : kMachinePointerType))),
488 : read8(AddExpr::create(offset,
489 : ConstantExpr::create(3,
490 : kMachinePointerType))),
491 : read8(AddExpr::create(offset,
492 : ConstantExpr::create(4,
493 : kMachinePointerType))),
494 : read8(AddExpr::create(offset,
495 : ConstantExpr::create(5,
496 : kMachinePointerType))),
497 : read8(AddExpr::create(offset,
498 : ConstantExpr::create(6,
499 : kMachinePointerType))),
500 : read8(AddExpr::create(offset,
501 : ConstantExpr::create(7,
502 : kMachinePointerType))));
503 : } else {
504 : return ConcatExpr::create8
505 : (read8(AddExpr::create(offset,
506 : ConstantExpr::create(7,
507 : kMachinePointerType))),
508 : read8(AddExpr::create(offset,
509 : ConstantExpr::create(6,
510 : kMachinePointerType))),
511 : read8(AddExpr::create(offset,
512 : ConstantExpr::create(5,
513 : kMachinePointerType))),
514 : read8(AddExpr::create(offset,
515 : ConstantExpr::create(4,
516 : kMachinePointerType))),
517 : read8(AddExpr::create(offset,
518 : ConstantExpr::create(3,
519 : kMachinePointerType))),
520 : read8(AddExpr::create(offset,
521 : ConstantExpr::create(2,
522 : kMachinePointerType))),
523 : read8(AddExpr::create(offset,
524 : ConstantExpr::create(1,
525 : kMachinePointerType))),
526 : read8(AddExpr::create(offset,
527 : ConstantExpr::create(0,
528 0: kMachinePointerType))));
529 : }
530 : }
531 :
532 1268879: void ObjectState::write(ref<Expr> offset, ref<Expr> value) {
533 1268879: Expr::Width w = value.getWidth();
1268858: branch 1 taken
21: branch 2 taken
534 1268879: if (offset.isConstant()) {
535 1268858: write(offset.getConstantValue(), value);
536 : } else {
0: branch 0 not taken
5: branch 1 taken
0: branch 2 not taken
16: branch 3 taken
0: branch 4 not taken
0: branch 5 not taken
537 21: switch(w) {
538 0: case Expr::Bool: write1(offset, value); break;
539 5: case Expr::Int8: write8(offset, value); break;
540 0: case Expr::Int16: write16(offset, value); break;
541 16: case Expr::Int32: write32(offset, value); break;
542 0: case Expr::Int64: write64(offset, value); break;
543 0: default: assert(0 && "invalid number of bytes in write");
544 : }
545 : }
546 1268879: }
547 :
548 1850366: void ObjectState::write(unsigned offset, ref<Expr> value) {
549 1850366: Expr::Width w = value.getWidth();
1844657: branch 1 taken
5709: branch 2 taken
550 1850366: if (value.isConstant()) {
551 1844657: uint64_t val = value.getConstantValue();
261712: branch 0 taken
296824: branch 1 taken
1277531: branch 2 taken
8590: branch 3 taken
0: branch 4 not taken
552 1844657: switch(w) {
553 : case Expr::Bool:
554 261712: case Expr::Int8: write8(offset, val); break;
555 296824: case Expr::Int16: write16(offset, val); break;
556 1277531: case Expr::Int32: write32(offset, val); break;
557 8590: case Expr::Int64: write64(offset, val); break;
558 0: default: assert(0 && "invalid number of bytes in write");
559 : }
560 : } else {
0: branch 0 not taken
1826: branch 1 taken
74: branch 2 taken
3808: branch 3 taken
1: branch 4 taken
0: branch 5 not taken
561 5709: switch(w) {
562 0: case Expr::Bool: write1(offset, value); break;
563 1826: case Expr::Int8: write8(offset, value); break;
564 74: case Expr::Int16: write16(offset, value); break;
565 3808: case Expr::Int32: write32(offset, value); break;
566 1: case Expr::Int64: write64(offset, value); break;
567 0: default: assert(0 && "invalid number of bytes in write");
568 : }
569 : }
570 1850366: }
571 :
572 0: void ObjectState::write1(unsigned offset, ref<Expr> value) {
573 0: write8(offset, ZExtExpr::create(value, Expr::Int8));
574 0: }
575 :
576 0: void ObjectState::write1(ref<Expr> offset, ref<Expr> value) {
577 0: write8(offset, ZExtExpr::create(value, Expr::Int8));
578 0: }
579 :
580 296824: void ObjectState::write16(unsigned offset, uint16_t value) {
581 : if (kMachineByteOrder == machine::MSB) {
582 : write8(offset+0, (uint8_t) (value >> 8));
583 : write8(offset+1, (uint8_t) (value >> 0));
584 : } else {
585 296824: write8(offset+1, (uint8_t) (value >> 8));
586 296824: write8(offset+0, (uint8_t) (value >> 0));
587 : }
588 296824: }
589 :
590 74: void ObjectState::write16(unsigned offset, ref<Expr> value) {
591 : if (kMachineByteOrder == machine::MSB) {
592 : write8(offset+0, ExtractExpr::createByteOff(value, 1));
593 : write8(offset+1, ExtractExpr::createByteOff(value, 0));
594 : } else {
595 74: write8(offset+1, ExtractExpr::createByteOff(value, 1));
596 74: write8(offset+0, ExtractExpr::createByteOff(value, 0));
597 : }
598 74: }
599 :
600 :
601 0: void ObjectState::write16(ref<Expr> offset, ref<Expr> value) {
602 : if (kMachineByteOrder == machine::MSB) {
603 : write8(AddExpr::create(offset,
604 : ConstantExpr::create(0, kMachinePointerType)),
605 : ExtractExpr::createByteOff(value,1));
606 : write8(AddExpr::create(offset,
607 : ConstantExpr::create(0, kMachinePointerType)),
608 : ExtractExpr::createByteOff(value,0));
609 : } else {
610 : write8(AddExpr::create(offset,
611 : ConstantExpr::create(1, kMachinePointerType)),
612 0: ExtractExpr::createByteOff(value,1));
613 : write8(AddExpr::create(offset,
614 : ConstantExpr::create(0, kMachinePointerType)),
615 0: ExtractExpr::createByteOff(value,0));
616 : }
617 0: }
618 :
619 1277531: void ObjectState::write32(unsigned offset, uint32_t value) {
620 : if (kMachineByteOrder == machine::MSB) {
621 : write8(offset+0, (uint8_t) (value >> 24));
622 : write8(offset+1, (uint8_t) (value >> 16));
623 : write8(offset+2, (uint8_t) (value >> 8));
624 : write8(offset+3, (uint8_t) (value >> 0));
625 : } else {
626 1277531: write8(offset+3, (uint8_t) (value >> 24));
627 1277531: write8(offset+2, (uint8_t) (value >> 16));
628 1277531: write8(offset+1, (uint8_t) (value >> 8));
629 1277531: write8(offset+0, (uint8_t) (value >> 0));
630 : }
631 1277531: }
632 :
633 3808: void ObjectState::write32(unsigned offset, ref<Expr> value) {
634 : if (kMachineByteOrder == machine::MSB) {
635 : write8(offset+0, ExtractExpr::createByteOff(value, 3));
636 : write8(offset+1, ExtractExpr::createByteOff(value, 2));
637 : write8(offset+2, ExtractExpr::createByteOff(value, 1));
638 : write8(offset+3, ExtractExpr::createByteOff(value, 0));
639 : } else {
640 3808: write8(offset+3, ExtractExpr::createByteOff(value, 3));
641 3808: write8(offset+2, ExtractExpr::createByteOff(value, 2));
642 3808: write8(offset+1, ExtractExpr::createByteOff(value, 1));
643 3808: write8(offset+0, ExtractExpr::createByteOff(value, 0));
644 : }
645 3808: }
646 :
647 16: void ObjectState::write32(ref<Expr> offset, ref<Expr> value) {
648 : if (kMachineByteOrder == machine::MSB) {
649 : write8(AddExpr::create(offset,
650 : ConstantExpr::create(0, kMachinePointerType)),
651 : ExtractExpr::createByteOff(value,3));
652 : write8(AddExpr::create(offset,
653 : ConstantExpr::create(1, kMachinePointerType)),
654 : ExtractExpr::createByteOff(value,2));
655 : write8(AddExpr::create(offset,
656 : ConstantExpr::create(2, kMachinePointerType)),
657 : ExtractExpr::createByteOff(value,1));
658 : write8(AddExpr::create(offset,
659 : ConstantExpr::create(3, kMachinePointerType)),
660 : ExtractExpr::createByteOff(value,0));
661 : } else {
662 : write8(AddExpr::create(offset,
663 : ConstantExpr::create(3, kMachinePointerType)),
664 32: ExtractExpr::createByteOff(value,3));
665 : write8(AddExpr::create(offset,
666 : ConstantExpr::create(2, kMachinePointerType)),
667 32: ExtractExpr::createByteOff(value,2));
668 : write8(AddExpr::create(offset,
669 : ConstantExpr::create(1, kMachinePointerType)),
670 32: ExtractExpr::createByteOff(value,1));
671 : write8(AddExpr::create(offset,
672 : ConstantExpr::create(0, kMachinePointerType)),
673 32: ExtractExpr::createByteOff(value,0));
674 : }
675 16: }
676 :
677 8590: void ObjectState::write64(unsigned offset, uint64_t value) {
678 : if (kMachineByteOrder == machine::MSB) {
679 : write8(offset+0, (uint8_t) (value >> 56));
680 : write8(offset+1, (uint8_t) (value >> 48));
681 : write8(offset+2, (uint8_t) (value >> 40));
682 : write8(offset+3, (uint8_t) (value >> 32));
683 : write8(offset+4, (uint8_t) (value >> 24));
684 : write8(offset+5, (uint8_t) (value >> 16));
685 : write8(offset+6, (uint8_t) (value >> 8));
686 : write8(offset+7, (uint8_t) (value >> 0));
687 : } else {
688 8590: write8(offset+7, (uint8_t) (value >> 56));
689 8590: write8(offset+6, (uint8_t) (value >> 48));
690 8590: write8(offset+5, (uint8_t) (value >> 40));
691 8590: write8(offset+4, (uint8_t) (value >> 32));
692 8590: write8(offset+3, (uint8_t) (value >> 24));
693 8590: write8(offset+2, (uint8_t) (value >> 16));
694 8590: write8(offset+1, (uint8_t) (value >> 8));
695 8590: write8(offset+0, (uint8_t) (value >> 0));
696 : }
697 8590: }
698 :
699 1: void ObjectState::write64(unsigned offset, ref<Expr> value) {
700 : if (kMachineByteOrder == machine::MSB) {
701 : write8(offset+0, ExtractExpr::createByteOff(value, 7));
702 : write8(offset+1, ExtractExpr::createByteOff(value, 6));
703 : write8(offset+2, ExtractExpr::createByteOff(value, 5));
704 : write8(offset+3, ExtractExpr::createByteOff(value, 4));
705 : write8(offset+4, ExtractExpr::createByteOff(value, 3));
706 : write8(offset+5, ExtractExpr::createByteOff(value, 2));
707 : write8(offset+6, ExtractExpr::createByteOff(value, 1));
708 : write8(offset+7, ExtractExpr::createByteOff(value, 0));
709 : } else {
710 1: write8(offset+7, ExtractExpr::createByteOff(value, 7));
711 1: write8(offset+6, ExtractExpr::createByteOff(value, 6));
712 1: write8(offset+5, ExtractExpr::createByteOff(value, 5));
713 1: write8(offset+4, ExtractExpr::createByteOff(value, 4));
714 1: write8(offset+3, ExtractExpr::createByteOff(value, 3));
715 1: write8(offset+2, ExtractExpr::createByteOff(value, 2));
716 1: write8(offset+1, ExtractExpr::createByteOff(value, 1));
717 1: write8(offset+0, ExtractExpr::createByteOff(value, 0));
718 : }
719 1: }
720 :
721 0: void ObjectState::write64(ref<Expr> offset, ref<Expr> value) {
722 : if (kMachineByteOrder == machine::MSB) {
723 : write8(AddExpr::create(offset,
724 : ConstantExpr::create(0, kMachinePointerType)),
725 : ExtractExpr::createByteOff(value,7));
726 : write8(AddExpr::create(offset,
727 : ConstantExpr::create(1, kMachinePointerType)),
728 : ExtractExpr::createByteOff(value,6));
729 : write8(AddExpr::create(offset,
730 : ConstantExpr::create(2, kMachinePointerType)),
731 : ExtractExpr::createByteOff(value,5));
732 : write8(AddExpr::create(offset,
733 : ConstantExpr::create(3, kMachinePointerType)),
734 : ExtractExpr::createByteOff(value,4));
735 : write8(AddExpr::create(offset,
736 : ConstantExpr::create(4, kMachinePointerType)),
737 : ExtractExpr::createByteOff(value,3));
738 : write8(AddExpr::create(offset,
739 : ConstantExpr::create(5, kMachinePointerType)),
740 : ExtractExpr::createByteOff(value,2));
741 : write8(AddExpr::create(offset,
742 : ConstantExpr::create(6, kMachinePointerType)),
743 : ExtractExpr::createByteOff(value,1));
744 : write8(AddExpr::create(offset,
745 : ConstantExpr::create(7, kMachinePointerType)),
746 : ExtractExpr::createByteOff(value,0));
747 : } else {
748 : write8(AddExpr::create(offset,
749 : ConstantExpr::create(7, kMachinePointerType)),
750 0: ExtractExpr::createByteOff(value,7));
751 : write8(AddExpr::create(offset,
752 : ConstantExpr::create(6, kMachinePointerType)),
753 0: ExtractExpr::createByteOff(value,6));
754 : write8(AddExpr::create(offset,
755 : ConstantExpr::create(5, kMachinePointerType)),
756 0: ExtractExpr::createByteOff(value,5));
757 : write8(AddExpr::create(offset,
758 : ConstantExpr::create(4, kMachinePointerType)),
759 0: ExtractExpr::createByteOff(value,4));
760 : write8(AddExpr::create(offset,
761 : ConstantExpr::create(3, kMachinePointerType)),
762 0: ExtractExpr::createByteOff(value,3));
763 : write8(AddExpr::create(offset,
764 : ConstantExpr::create(2, kMachinePointerType)),
765 0: ExtractExpr::createByteOff(value,2));
766 : write8(AddExpr::create(offset,
767 : ConstantExpr::create(1, kMachinePointerType)),
768 0: ExtractExpr::createByteOff(value,1));
769 : write8(AddExpr::create(offset,
770 : ConstantExpr::create(0, kMachinePointerType)),
771 0: ExtractExpr::createByteOff(value,0));
772 : }
773 0: }
774 :
775 0: void ObjectState::print() {
776 : llvm::cerr << "-- ObjectState --\n";
777 0: llvm::cerr << "\tMemoryObject ID: " << updates.root->id << "\n";
778 0: llvm::cerr << "\tRoot Object: " << updates.root << "\n";
779 0: llvm::cerr << "\tIs Rooted? " << updates.isRooted << "\n";
780 0: llvm::cerr << "\tSize: " << size << "\n";
781 :
782 : llvm::cerr << "\tBytes:\n";
0: branch 1 not taken
0: branch 2 not taken
783 0: for (unsigned i=0; i<size; i++) {
784 : llvm::cerr << "\t\t["<<i<<"]"
785 : << " concrete? " << isByteConcrete(i)
786 : << " known-sym? " << isByteKnownSymbolic(i)
787 0: << " flushed? " << isByteFlushed(i) << " = ";
788 0: ref<Expr> e = read8(i);
789 0: llvm::cerr << e << "\n";
790 : }
791 :
792 : llvm::cerr << "\tUpdates:\n";
0: branch 0 not taken
0: branch 1 not taken
793 0: for (const UpdateNode *un=updates.head; un; un=un->next) {
794 0: llvm::cerr << "\t\t[" << un->index << "] = " << un->value << "\n";
795 : }
103: branch 0 taken
0: branch 1 not taken
103: branch 2 taken
0: branch 3 not taken
796 206: }
Generated: 2009-05-17 22:47 by zcov