 |
|
 |
|
| Files: |
1 |
|
Branches Taken: |
62.1% |
72 / 116 |
| Generated: |
2009-05-17 22:47 |
|
Branches Executed: |
79.3% |
92 / 116 |
| |
|
Line Coverage: |
72.5% |
116 / 160 |
| |
 |
|
 |
1 : /* -*- mode: c++; c-basic-offset: 2; -*- */
2 :
3 : #include "AddressSpace.h"
4 : #include "CoreStats.h"
5 : #include "TimingSolver.h"
6 :
7 : #include "klee/Expr.h"
8 : #include "klee/Memory.h"
9 : #include "klee/TimerStatIncrementer.h"
10 :
11 : #include "klee/Internal/FIXME/sugar.h"
12 :
13 : using namespace klee;
14 :
15 : ///
16 :
17 766579: void AddressSpace::bindObject(const MemoryObject *mo, ObjectState *os) {
0: branch 0 not taken
766579: branch 1 taken
18 766579: assert(os->copyOnWriteOwner==0 && "object already has owner");
19 766579: os->copyOnWriteOwner = cowKey;
20 2299737: objects = objects.replace(std::make_pair(mo, os));
21 766579: }
22 :
23 601316: void AddressSpace::unbindObject(const MemoryObject *mo) {
24 1202632: objects = objects.remove(mo);
25 601316: }
26 :
27 8333: const ObjectState *AddressSpace::findObject(const MemoryObject *mo) const {
28 16666: const MemoryMap::value_type *res = objects.lookup(mo);
29 :
8333: branch 0 taken
0: branch 1 not taken
30 16666: return res ? res->second : 0;
31 : }
32 :
33 : ObjectState *AddressSpace::getWriteable(const MemoryObject *mo,
34 1277148: const ObjectState *os) {
0: branch 0 not taken
1277148: branch 1 taken
35 1277148: assert(!os->readOnly);
36 :
1240905: branch 0 taken
36243: branch 1 taken
37 1277148: if (cowKey==os->copyOnWriteOwner) {
38 1240905: return const_cast<ObjectState*>(os);
39 : } else {
40 36243: ObjectState *n = new ObjectState(*os);
41 36243: n->copyOnWriteOwner = cowKey;
42 108729: objects = objects.replace(std::make_pair(mo, n));
43 36243: return n;
44 : }
45 : }
46 :
47 : ///
48 :
49 3406082: bool AddressSpace::resolveOne(uint64_t addr64, ObjectPair &result) {
50 3406082: unsigned address = (unsigned) addr64;
51 3406082: MemoryObject hack(address);
52 3406082: let(res, objects.lookup_previous(&hack));
53 :
3406079: branch 0 taken
3: branch 1 taken
54 3406082: if (res) {
55 3406079: const MemoryObject *mo = res->first;
1: branch 0 taken
3406078: branch 1 taken
0: branch 2 not taken
1: branch 3 taken
3406061: branch 4 taken
17: branch 5 taken
56 3406079: if ((mo->size==0 && address==mo->address) ||
57 : (address - mo->address < mo->size)) {
58 3406062: result = *res;
59 3406062: return true;
60 : }
61 : }
62 :
63 20: return false;
64 : }
65 :
66 : bool AddressSpace::resolveOne(ExecutionState &state,
67 : TimingSolver *solver,
68 : ref<Expr> address,
69 : ObjectPair &result,
70 3405920: bool &success) {
3405829: branch 0 taken
91: branch 1 taken
71 3405920: if (address.isConstant()) {
72 3405829: success = resolveOne(address.getConstantValue(), result);
73 3405829: return true;
74 : } else {
75 : TimerStatIncrementer timer(stats::resolveTime);
76 :
77 : // try cheap search, will succeed for any inbounds pointer
78 :
79 : ref<Expr> cex(0);
0: branch 2 not taken
91: branch 3 taken
80 91: if (!solver->getValue(state, address, cex))
81 0: return false;
82 91: unsigned example = (unsigned) cex.getConstantValue();
83 91: MemoryObject hack(example);
84 91: let (res, objects.lookup_previous(&hack));
85 :
91: branch 0 taken
0: branch 1 not taken
86 91: if (res) {
87 91: const MemoryObject *mo = res->first;
91: branch 0 taken
0: branch 1 not taken
88 91: if (example - mo->address < mo->size) {
89 91: result = *res;
90 91: success = true;
91 91: return true;
92 : }
93 : }
94 :
95 : // didn't work, now we have to search
96 :
97 0: let(oi, objects.upper_bound(&hack));
98 0: let(begin, objects.begin());
99 0: let(end, objects.end());
100 :
101 0: let(start, oi);
0: branch 0 not taken
0: branch 1 not taken
102 0: while (oi!=begin) {
103 0: --oi;
104 0: const MemoryObject *mo = oi->first;
105 :
106 : bool mayBeTrue;
0: branch 4 not taken
0: branch 5 not taken
107 0: if (!solver->mayBeTrue(state,
108 : mo->getBoundsCheckPointer(address), mayBeTrue))
109 0: return false;
0: branch 0 not taken
0: branch 1 not taken
110 0: if (mayBeTrue) {
111 0: result = *oi;
112 0: success = true;
113 0: return true;
114 : } else {
115 : bool mustBeTrue;
0: branch 5 not taken
0: branch 6 not taken
116 0: if (!solver->mustBeTrue(state,
117 : UgeExpr::create(address, mo->getBaseExpr()),
118 : mustBeTrue))
119 0: return false;
0: branch 0 not taken
0: branch 1 not taken
120 0: if (mustBeTrue)
121 0: break;
122 : }
123 : }
124 :
125 : // search forwards
0: branch 2 not taken
0: branch 3 not taken
126 0: for (oi=start; oi!=end; ++oi) {
127 0: const MemoryObject *mo = oi->first;
128 :
129 : bool mustBeTrue;
0: branch 5 not taken
0: branch 6 not taken
130 0: if (!solver->mustBeTrue(state,
131 : UltExpr::create(address, mo->getBaseExpr()),
132 : mustBeTrue))
133 0: return false;
0: branch 0 not taken
0: branch 1 not taken
134 0: if (mustBeTrue) {
135 0: break;
136 : } else {
137 : bool mayBeTrue;
138 :
0: branch 4 not taken
0: branch 5 not taken
139 0: if (!solver->mayBeTrue(state,
140 : mo->getBoundsCheckPointer(address),
141 : mayBeTrue))
142 0: return false;
0: branch 0 not taken
0: branch 1 not taken
143 0: if (mayBeTrue) {
144 0: result = *oi;
145 0: success = true;
146 0: return true;
147 : }
148 : }
149 : }
150 :
151 0: success = false;
152 0: return true;
153 : }
154 : }
155 :
156 : bool AddressSpace::resolve(ExecutionState &state,
157 : TimingSolver *solver,
158 : ref<Expr> p,
159 : ResolutionList &rl,
160 : unsigned maxResolutions,
161 141: double timeout) {
132: branch 0 taken
9: branch 1 taken
162 141: if (p.isConstant()) {
163 : ObjectPair res;
122: branch 1 taken
10: branch 2 taken
164 132: if (resolveOne(p.getConstantValue(), res))
165 122: rl.push_back(res);
166 132: return false;
167 : } else {
168 : TimerStatIncrementer timer(stats::resolveTime);
169 9: uint64_t timeout_us = (uint64_t) (timeout*1000000.);
170 :
171 : // XXX in general this isn't exactly what we want... for
172 : // a multiple resolution case (or for example, a \in {b,c,0})
173 : // we want to find the first object, find a cex assuming
174 : // not the first, find a cex assuming not the second...
175 : // etc.
176 :
177 : // XXX how do we smartly amortize the cost of checking to
178 : // see if we need to keep searching up/down, in bad cases?
179 : // maybe we don't care?
180 :
181 : // XXX we really just need a smart place to start (although
182 : // if its a known solution then the code below is guaranteed
183 : // to hit the fast path with exactly 2 queries). we could also
184 : // just get this by inspection of the expr.
185 :
186 : ref<Expr> cex(0);
0: branch 2 not taken
9: branch 3 taken
187 9: if (!solver->getValue(state, p, cex))
188 2: return true;
189 9: unsigned example = (unsigned) cex.getConstantValue();
190 9: MemoryObject hack(example);
191 :
192 9: let(oi, objects.upper_bound(&hack));
193 9: let(begin, objects.begin());
194 9: let(end, objects.end());
195 :
196 9: let(start, oi);
197 :
198 : // XXX in the common case we can save one query if we ask
199 : // mustBeTrue before mayBeTrue for the first result. easy
200 : // to add I just want to have a nice symbolic test case first.
201 :
202 : // search backwards, start with one minus because this
203 : // is the object that p *should* be within, which means we
204 : // get write off the end with 4 queries (XXX can be better,
205 : // no?)
36: branch 3 taken
1: branch 4 taken
206 74: while (oi!=begin) {
207 36: --oi;
208 36: const MemoryObject *mo = oi->first;
0: branch 0 not taken
36: branch 1 taken
36: branch 2 taken
36: branch 3 taken
0: branch 4 not taken
36: branch 5 taken
209 36: if (timeout_us && timeout_us < timer.check())
210 0: return true;
211 :
212 : // XXX I think there is some query wasteage here?
213 36: ref<Expr> inBounds = mo->getBoundsCheckPointer(p);
214 : bool mayBeTrue;
0: branch 2 not taken
36: branch 3 taken
215 36: if (!solver->mayBeTrue(state, inBounds, mayBeTrue))
216 0: return true;
14: branch 0 taken
22: branch 1 taken
217 36: if (mayBeTrue) {
218 14: rl.push_back(*oi);
219 :
220 : // fast path check
221 14: unsigned size = rl.size();
8: branch 0 taken
6: branch 1 taken
222 14: if (size==1) {
223 : bool mustBeTrue;
0: branch 2 not taken
8: branch 3 taken
224 8: if (!solver->mustBeTrue(state, inBounds, mustBeTrue))
225 0: return true;
2: branch 0 taken
6: branch 1 taken
226 8: if (mustBeTrue)
227 2: return false;
0: branch 0 not taken
6: branch 1 taken
228 6: } else if (size==maxResolutions) {
229 0: return true;
230 : }
231 : }
232 :
233 : bool mustBeTrue;
0: branch 5 not taken
34: branch 6 taken
234 34: if (!solver->mustBeTrue(state,
235 : UgeExpr::create(p, mo->getBaseExpr()),
236 : mustBeTrue))
237 0: return true;
28: branch 0 taken
6: branch 1 taken
238 34: if (mustBeTrue)
239 6: break;
240 : }
241 : // search forwards
48: branch 4 taken
2: branch 5 taken
242 100: for (oi=start; oi!=end; ++oi) {
243 48: const MemoryObject *mo = oi->first;
0: branch 0 not taken
48: branch 1 taken
48: branch 2 taken
48: branch 3 taken
0: branch 4 not taken
48: branch 5 taken
244 48: if (timeout_us && timeout_us < timer.check())
245 0: return true;
246 :
247 : bool mustBeTrue;
0: branch 5 not taken
48: branch 6 taken
248 48: if (!solver->mustBeTrue(state,
249 : UltExpr::create(p, mo->getBaseExpr()),
250 : mustBeTrue))
251 0: return true;
5: branch 0 taken
43: branch 1 taken
252 48: if (mustBeTrue)
253 5: break;
254 :
255 : // XXX I think there is some query wasteage here?
256 43: ref<Expr> inBounds = mo->getBoundsCheckPointer(p);
257 : bool mayBeTrue;
0: branch 2 not taken
43: branch 3 taken
258 43: if (!solver->mayBeTrue(state, inBounds, mayBeTrue))
259 0: return true;
5: branch 0 taken
38: branch 1 taken
260 43: if (mayBeTrue) {
261 5: rl.push_back(*oi);
262 :
263 : // fast path check
264 5: unsigned size = rl.size();
1: branch 0 taken
4: branch 1 taken
265 5: if (size==1) {
266 : bool mustBeTrue;
0: branch 2 not taken
1: branch 3 taken
267 1: if (!solver->mustBeTrue(state, inBounds, mustBeTrue))
268 0: return true;
0: branch 0 not taken
1: branch 1 taken
269 1: if (mustBeTrue)
270 0: return false;
0: branch 0 not taken
4: branch 1 taken
271 4: } else if (size==maxResolutions) {
272 0: return true;
273 : }
274 : }
275 9: }
276 : }
277 :
278 7: return false;
279 : }
280 :
281 : // These two are pretty big hack so we can sort of pass memory back
282 : // and forth to externals. They work by abusing the concrete cache
283 : // store inside of the object states, which allows them to
284 : // transparently avoid screwing up symbolics (if the byte is symbolic
285 : // then its concrete cache byte isn't being used) but is just a hack.
286 :
287 288: void AddressSpace::copyOutConcretes() {
45995: branch 1 taken
288: branch 2 taken
288 92854: foreach(oi, objects.begin(), objects.end()) {
289 45995: const MemoryObject *mo = oi->first;
290 :
45994: branch 0 taken
1: branch 1 taken
291 45995: if (!mo->isUserSpecified) {
292 91988: ObjectState *os = oi->second;
293 45994: uint8_t *address = (uint8_t*) (unsigned long) mo->address;
294 :
44266: branch 0 taken
1728: branch 1 taken
295 45994: if (!os->readOnly)
296 44266: memcpy(address, os->concreteStore, mo->size);
297 : }
298 288: }
299 288: }
300 :
301 287: bool AddressSpace::copyInConcretes() {
45971: branch 1 taken
287: branch 2 taken
302 92803: foreach(oi, objects.begin(), objects.end()) {
303 45971: const MemoryObject *mo = oi->first;
304 :
45970: branch 0 taken
1: branch 1 taken
305 45971: if (!mo->isUserSpecified) {
306 91940: const ObjectState *os = oi->second;
307 45970: uint8_t *address = (uint8_t*) (unsigned long) mo->address;
308 :
6: branch 1 taken
45964: branch 2 taken
309 45970: if (memcmp(address, os->concreteStore, mo->size)!=0) {
0: branch 0 not taken
6: branch 1 taken
310 6: if (os->readOnly) {
311 0: return false;
312 : } else {
313 6: ObjectState *wos = getWriteable(mo, os);
314 6: memcpy(wos->concreteStore, address, mo->size);
315 : }
316 : }
317 : }
318 287: }
319 :
320 287: return true;
321 : }
322 :
323 : /***/
324 :
325 81715229: bool MemoryObjectLT::operator()(const MemoryObject *a, const MemoryObject *b) const {
326 81715229: return a->address < b->address;
103: branch 0 taken
0: branch 1 not taken
103: branch 2 taken
0: branch 3 not taken
327 206: }
328 :
Generated: 2009-05-17 22:47 by zcov