 |
|
 |
|
| Files: |
1 |
|
Branches Taken: |
52.0% |
106 / 204 |
| Generated: |
2009-05-17 22:47 |
|
Branches Executed: |
80.4% |
164 / 204 |
| |
|
Line Coverage: |
73.3% |
211 / 288 |
| |
 |
|
 |
1 : /* -*- mode: c++; c-basic-offset: 2; -*- */
2 :
3 : #include "Common.h"
4 :
5 : #include "SpecialFunctionHandler.h"
6 : #include "TimingSolver.h"
7 :
8 : #include "klee/ExecutionState.h"
9 : #include "klee/Memory.h"
10 :
11 : #include "klee/Internal/Module/KInstruction.h"
12 : #include "klee/Internal/Module/KModule.h"
13 :
14 : #include "Executor.h"
15 : #include "MemoryManager.h"
16 :
17 : #include "llvm/Module.h"
18 :
19 : #include <errno.h>
20 :
21 : #include "klee/Internal/FIXME/sugar.h"
22 :
23 : using namespace llvm;
24 : using namespace klee;
25 :
26 : /// \todo Almost all of the demands in this file should be replaced
27 : /// with terminateState calls.
28 :
29 : ///
30 :
31 : struct HandlerInfo {
32 : const char *name;
33 : SpecialFunctionHandler::Handler handler;
34 : bool doesNotReturn; /// Intrinsic terminates the process
35 : bool hasReturnValue; /// Intrinsic has a return value
36 : bool doNotOverride; /// Intrinsic should not be used if already defined
37 : };
38 :
39 : // FIXME: We are more or less committed to requiring an intrinsic
40 : // library these days. We can move some of this stuff there,
41 : // especially things like realloc which have complicated semantics
42 : // w.r.t. forking. Among other things this makes delayed query
43 : // dispatch easier to implement.
44 : HandlerInfo handlerInfo[] = {
45 : #define add(name, handler, ret) { name, \
46 : &SpecialFunctionHandler::handler, \
47 : false, ret, false }
48 : #define addDNR(name, handler) { name, \
49 : &SpecialFunctionHandler::handler, \
50 : true, false, false }
51 : addDNR("__assert_rtn", handleAssertFail),
52 : addDNR("__assert_fail", handleAssertFail),
53 : addDNR("_assert", handleAssert),
54 : addDNR("abort", handleAbort),
55 : addDNR("_exit", handleExit),
56 : { "exit", &SpecialFunctionHandler::handleExit, true, false, true },
57 : addDNR("klee_abort", handleAbort),
58 : addDNR("klee_silent_exit", handleSilentExit),
59 : addDNR("klee_report_error", handleReportError),
60 :
61 : add("calloc", handleCalloc, true),
62 : add("free", handleFree, false),
63 : add("klee_assume", handleAssume, false),
64 : add("klee_check_memory_access", handleCheckMemoryAccess, false),
65 : add("klee_get_value", handleGetValue, true),
66 : add("klee_define_fixed_object", handleDefineFixedObject, false),
67 : add("klee_get_obj_size", handleGetObjSize, true),
68 : add("klee_get_errno", handleGetErrno, true),
69 : add("klee_is_symbolic", handleIsSymbolic, true),
70 : add("klee_make_symbolic_name", handleMakeSymbolic, false),
71 : add("klee_mark_global", handleMarkGlobal, false),
72 : add("klee_malloc_n", handleMallocN, true),
73 : add("klee_merge", handleMerge, false),
74 : add("klee_prefer_cex", handlePreferCex, false),
75 : add("klee_print_expr", handlePrintExpr, false),
76 : add("klee_print_range", handlePrintRange, false),
77 : add("klee_revirt_objects", handleRevirtObjects, false),
78 : add("klee_set_forking", handleSetForking, false),
79 : add("klee_warning", handleWarning, false),
80 : add("klee_warning_once", handleWarningOnce, false),
81 : add("klee_under_constrained", handleUnderConstrained, false),
82 : add("klee_alias_function", handleAliasFunction, false),
83 : add("malloc", handleMalloc, true),
84 : add("realloc", handleRealloc, true),
85 :
86 : // operator delete[](void*)
87 : add("_ZdaPv", handleDeleteArray, false),
88 : // operator delete(void*)
89 : add("_ZdlPv", handleDelete, false),
90 :
91 : // operator new[](unsigned int)
92 : add("_Znaj", handleNewArray, true),
93 : // operator new(unsigned int)
94 : add("_Znwj", handleNew, true),
95 :
96 : // FIXME-64: This is wrong for 64-bit long...
97 :
98 : // operator new[](unsigned long)
99 : add("_Znam", handleNewArray, true),
100 : // operator new(unsigned long)
101 : add("_Znwm", handleNew, true),
102 :
103 : #undef addDNR
104 : #undef add
105 : };
106 :
107 103: SpecialFunctionHandler::SpecialFunctionHandler(Executor &_executor)
108 206: : executor(_executor) {}
109 :
110 :
111 103: void SpecialFunctionHandler::prepare() {
112 103: unsigned N = sizeof(handlerInfo)/sizeof(handlerInfo[0]);
113 :
4017: branch 0 taken
103: branch 1 taken
114 4120: for (unsigned i=0; i<N; ++i) {
115 4017: HandlerInfo &hi = handlerInfo[i];
116 4017: Function *f = executor.kmodule->module->getFunction(hi.name);
117 :
118 : // No need to create if the function doesn't exist, since it cannot
119 : // be called in that case.
120 :
180: branch 0 taken
3837: branch 1 taken
4: branch 2 taken
176: branch 3 taken
1: branch 5 taken
3: branch 6 taken
177: branch 7 taken
3840: branch 8 taken
121 4017: if (f && (!hi.doNotOverride || f->isDeclaration())) {
122 : // Make sure NoReturn attribute is set, for optimization and
123 : // coverage counting.
59: branch 0 taken
118: branch 1 taken
124 177: if (hi.doesNotReturn)
125 : f->addFnAttr(Attribute::NoReturn);
126 :
127 : // Change to a declaration since we handle internally (simplifies
128 : // module and allows deleting dead code).
3: branch 1 taken
174: branch 2 taken
129 177: if (!f->isDeclaration())
130 : f->deleteBody();
131 : }
132 : }
133 103: }
134 :
135 103: void SpecialFunctionHandler::bind() {
136 103: unsigned N = sizeof(handlerInfo)/sizeof(handlerInfo[0]);
137 :
4017: branch 0 taken
103: branch 1 taken
138 4120: for (unsigned i=0; i<N; ++i) {
139 4017: HandlerInfo &hi = handlerInfo[i];
140 4017: Function *f = executor.kmodule->module->getFunction(hi.name);
141 :
344: branch 0 taken
3673: branch 1 taken
3: branch 2 taken
341: branch 3 taken
1: branch 5 taken
2: branch 6 taken
342: branch 7 taken
3675: branch 8 taken
142 4017: if (f && (!hi.doNotOverride || f->isDeclaration()))
143 1026: handlers[f] = std::make_pair(hi.handler, hi.hasReturnValue);
144 : }
145 103: }
146 :
147 :
148 : bool SpecialFunctionHandler::handle(ExecutionState &state,
149 : Function *f,
150 : KInstruction *target,
151 525243: std::vector< ref<Expr> > &arguments) {
152 525243: let(it, handlers.find(f));
524955: branch 0 taken
288: branch 1 taken
153 1050486: if (it!=handlers.end()) {
154 524955: Handler h = it->second.first;
155 524955: bool hasReturnValue = it->second.second;
486: branch 0 taken
524469: branch 1 taken
0: branch 2 not taken
486: branch 3 taken
0: branch 4 not taken
524955: branch 5 taken
156 525441: if (!hasReturnValue && !target->inst->use_empty()) { // XXX check me? add test...
157 : executor.terminateStateOnExecError(state,
158 0: "expected return value from void special function");
159 : } else {
0: branch 0 not taken
524955: branch 1 taken
160 524955: (this->*h)(state, target, arguments);
161 : }
162 524955: return true;
163 : } else {
164 288: return false;
165 : }
166 : }
167 :
168 : /****/
169 :
170 : // reads a concrete string from memory
171 : std::string SpecialFunctionHandler::readStringAtAddress(ExecutionState &state,
172 118: ref<Expr> address) {
173 : ObjectPair op;
174 118: address = executor.toUnique(state, address);
0: branch 1 not taken
118: branch 2 taken
175 118: assert(address.isConstant() && "symbolic string arg to intrinsic");
0: branch 2 not taken
118: branch 3 taken
176 118: if (!state.addressSpace.resolveOne(address.getConstantValue(), op))
177 0: assert(0 && "XXX out of bounds / multiple resolution unhandled");
178 : bool res;
179 : assert(executor.solver->mustBeTrue(state,
180 : EqExpr::create(address,
181 : op.first->getBaseExpr()),
182 : res) &&
183 : res &&
118: branch 3 taken
0: branch 4 not taken
0: branch 5 not taken
118: branch 6 taken
118: branch 8 taken
0: branch 9 not taken
118: branch 11 taken
0: branch 12 not taken
184 118: "XXX interior pointer unhandled");
185 118: const MemoryObject *mo = op.first;
186 118: const ObjectState *os = op.second;
187 :
188 118: char *buf = new char[mo->size];
189 :
190 : unsigned i;
730: branch 1 taken
118: branch 2 taken
191 848: for (i = 0; i < mo->size - 1; i++) {
192 730: ref<Expr> cur = os->read8(i);
193 730: cur = executor.toUnique(state, cur);
194 : assert(cur.isConstant() &&
0: branch 1 not taken
730: branch 2 taken
195 730: "hit symbolic char while reading concrete string");
196 730: buf[i] = cur.getConstantValue();
197 : }
198 118: buf[i] = 0;
199 :
200 118: std::string result(buf);
118: branch 0 taken
0: branch 1 not taken
201 118: delete[] buf;
202 : return result;
203 : }
204 :
205 : /****/
206 :
207 : void SpecialFunctionHandler::handleAbort(ExecutionState &state,
208 : KInstruction *target,
209 1: std::vector<ref<Expr> > &arguments) {
0: branch 0 not taken
1: branch 1 taken
210 1: assert(arguments.size()==0 && "invalid number of arguments to abort");
211 :
212 : //XXX:DRE:TAINT
0: branch 0 not taken
1: branch 1 taken
213 1: if(state.underConstrained) {
214 : llvm::cerr << "TAINT: skipping abort fail\n";
215 0: executor.terminateState(state);
216 : } else {
217 5: executor.terminateStateOnError(state, "abort failure", "abort.err");
218 : }
219 1: }
220 :
221 : void SpecialFunctionHandler::handleExit(ExecutionState &state,
222 : KInstruction *target,
223 5: std::vector<ref<Expr> > &arguments) {
0: branch 0 not taken
5: branch 1 taken
224 5: assert(arguments.size()==1 && "invalid number of arguments to exit");
225 5: executor.terminateStateOnExit(state);
226 5: }
227 :
228 : void SpecialFunctionHandler::handleSilentExit(ExecutionState &state,
229 : KInstruction *target,
230 49: std::vector<ref<Expr> > &arguments) {
0: branch 0 not taken
49: branch 1 taken
231 49: assert(arguments.size()==1 && "invalid number of arguments to exit");
232 49: executor.terminateState(state);
233 49: }
234 :
235 : void SpecialFunctionHandler::handleAliasFunction(ExecutionState &state,
236 : KInstruction *target,
237 7: std::vector<ref<Expr> > &arguments) {
238 : assert(arguments.size()==2 &&
0: branch 0 not taken
7: branch 1 taken
239 7: "invalid number of arguments to klee_alias_function");
240 7: std::string old_fn = readStringAtAddress(state, arguments[0]);
241 7: std::string new_fn = readStringAtAddress(state, arguments[1]);
242 : //llvm::cerr << "Replacing " << old_fn << "() with " << new_fn << "()\n";
5: branch 0 taken
2: branch 1 taken
243 7: if (old_fn == new_fn)
244 5: state.removeFnAlias(old_fn);
245 2: else state.addFnAlias(old_fn, new_fn);
246 7: }
247 :
248 : void SpecialFunctionHandler::handleAssert(ExecutionState &state,
249 : KInstruction *target,
250 0: std::vector<ref<Expr> > &arguments) {
0: branch 0 not taken
0: branch 1 not taken
251 0: assert(arguments.size()==3 && "invalid number of arguments to _assert");
252 :
253 : //XXX:DRE:TAINT
0: branch 0 not taken
0: branch 1 not taken
254 0: if(state.underConstrained) {
255 : llvm::cerr << "TAINT: skipping assertion:"
256 0: << readStringAtAddress(state, arguments[0]) << "\n";
257 0: executor.terminateState(state);
258 : } else
259 : executor.terminateStateOnError(state,
260 : "ASSERTION FAIL: " + readStringAtAddress(state, arguments[0]),
261 0: "assert.err");
262 0: }
263 :
264 : void SpecialFunctionHandler::handleAssertFail(ExecutionState &state,
265 : KInstruction *target,
266 3: std::vector<ref<Expr> > &arguments) {
0: branch 0 not taken
3: branch 1 taken
267 3: assert(arguments.size()==4 && "invalid number of arguments to __assert_fail");
268 :
269 : //XXX:DRE:TAINT
0: branch 0 not taken
3: branch 1 taken
270 3: if(state.underConstrained) {
271 : llvm::cerr << "TAINT: skipping assertion:"
272 0: << readStringAtAddress(state, arguments[0]) << "\n";
273 0: executor.terminateState(state);
274 : } else
275 : executor.terminateStateOnError(state,
276 : "ASSERTION FAIL: " + readStringAtAddress(state, arguments[0]),
277 12: "assert.err");
278 3: }
279 :
280 : void SpecialFunctionHandler::handleReportError(ExecutionState &state,
281 : KInstruction *target,
282 3: std::vector<ref<Expr> > &arguments) {
0: branch 0 not taken
3: branch 1 taken
283 3: assert(arguments.size()==4 && "invalid number of arguments to klee_report_error");
284 :
285 : // arguments[0], arguments[1] are file, line
286 :
287 : //XXX:DRE:TAINT
0: branch 0 not taken
3: branch 1 taken
288 3: if(state.underConstrained) {
289 : llvm::cerr << "TAINT: skipping klee_report_error:"
290 : << readStringAtAddress(state, arguments[2]) << ":"
291 0: << readStringAtAddress(state, arguments[3]) << "\n";
292 0: executor.terminateState(state);
293 : } else
294 : executor.terminateStateOnError(state,
295 : readStringAtAddress(state, arguments[2]),
296 9: readStringAtAddress(state, arguments[3]));
297 3: }
298 :
299 : void SpecialFunctionHandler::handleMerge(ExecutionState &state,
300 : KInstruction *target,
301 256: std::vector<ref<Expr> > &arguments) {
302 : // nop
303 256: }
304 :
305 : void SpecialFunctionHandler::handleNew(ExecutionState &state,
306 : KInstruction *target,
307 3: std::vector<ref<Expr> > &arguments) {
308 : // XXX should type check args
0: branch 0 not taken
3: branch 1 taken
309 3: assert(arguments.size()==1 && "invalid number of arguments to new");
310 :
311 3: executor.executeAlloc(state, arguments[0], false, target);
312 3: }
313 :
314 : void SpecialFunctionHandler::handleDelete(ExecutionState &state,
315 : KInstruction *target,
316 3: std::vector<ref<Expr> > &arguments) {
317 : // XXX should type check args
0: branch 0 not taken
3: branch 1 taken
318 3: assert(arguments.size()==1 && "invalid number of arguments to delete");
319 3: executor.executeFree(state, arguments[0]);
320 3: }
321 :
322 : void SpecialFunctionHandler::handleNewArray(ExecutionState &state,
323 : KInstruction *target,
324 1: std::vector<ref<Expr> > &arguments) {
325 : // XXX should type check args
0: branch 0 not taken
1: branch 1 taken
326 1: assert(arguments.size()==1 && "invalid number of arguments to new[]");
327 1: executor.executeAlloc(state, arguments[0], false, target);
328 1: }
329 :
330 : void SpecialFunctionHandler::handleDeleteArray(ExecutionState &state,
331 : KInstruction *target,
332 1: std::vector<ref<Expr> > &arguments) {
333 : // XXX should type check args
0: branch 0 not taken
1: branch 1 taken
334 1: assert(arguments.size()==1 && "invalid number of arguments to delete[]");
335 1: executor.executeFree(state, arguments[0]);
336 1: }
337 :
338 : void SpecialFunctionHandler::handleMalloc(ExecutionState &state,
339 : KInstruction *target,
340 524454: std::vector<ref<Expr> > &arguments) {
341 : // XXX should type check args
0: branch 0 not taken
524454: branch 1 taken
342 524454: assert(arguments.size()==1 && "invalid number of arguments to malloc");
343 524454: executor.executeAlloc(state, arguments[0], false, target);
344 524454: }
345 :
346 : void SpecialFunctionHandler::handleMallocN(ExecutionState &state,
347 : KInstruction *target,
348 0: std::vector<ref<Expr> > &arguments) {
349 :
350 : // XXX should type check args
0: branch 0 not taken
0: branch 1 not taken
351 0: assert(arguments.size() == 3 && "invalid number of arguments to malloc");
352 :
353 : // mallocn(number, size, alignment)
354 0: ref<Expr> numElems = executor.toUnique(state, arguments[0]);
355 0: ref<Expr> elemSize = executor.toUnique(state, arguments[1]);
356 0: ref<Expr> elemAlignment = executor.toUnique(state, arguments[2]);
357 :
358 : assert(numElems.isConstant() &&
359 : elemSize.isConstant() &&
360 : elemAlignment.isConstant() &&
0: branch 1 not taken
0: branch 2 not taken
0: branch 4 not taken
0: branch 5 not taken
0: branch 7 not taken
0: branch 8 not taken
361 0: "symbolic arguments passed to klee_mallocn");
362 :
363 : executor.executeAllocN(state,
364 : numElems.getConstantValue(),
365 : elemSize.getConstantValue(),
366 : elemAlignment.getConstantValue(),
367 : false,
368 0: target);
369 0: }
370 :
371 : void SpecialFunctionHandler::handleAssume(ExecutionState &state,
372 : KInstruction *target,
373 26: std::vector<ref<Expr> > &arguments) {
0: branch 0 not taken
26: branch 1 taken
374 26: assert(arguments.size()==1 && "invalid number of arguments to klee_assume");
375 :
376 : ref<Expr> e = arguments[0];
377 :
26: branch 0 taken
0: branch 1 not taken
378 26: if(e.getWidth() != Expr::Bool)
379 52: e = NeExpr::create(e, ConstantExpr::create(0, e.getWidth()));
380 :
381 : bool res;
382 26: bool success = executor.solver->mustBeFalse(state, e, res);
0: branch 0 not taken
26: branch 1 taken
383 26: assert(success && "FIXME: Unhandled solver failure");
0: branch 0 not taken
26: branch 1 taken
384 26: if (res) {
385 : executor.terminateStateOnError(state,
386 : "invalid klee_assume call (provably false)",
387 0: "user.err");
388 : } else {
389 26: executor.addConstraint(state, e);
390 26: }
391 26: }
392 :
393 : void SpecialFunctionHandler::handleIsSymbolic(ExecutionState &state,
394 : KInstruction *target,
395 5: std::vector<ref<Expr> > &arguments) {
0: branch 0 not taken
5: branch 1 taken
396 5: assert(arguments.size()==1 && "invalid number of arguments to klee_is_symbolic");
397 :
398 : executor.bindLocal(target, state,
399 10: ConstantExpr::create(!arguments[0].isConstant(), Expr::Int32));
400 5: }
401 :
402 : void SpecialFunctionHandler::handlePreferCex(ExecutionState &state,
403 : KInstruction *target,
404 3: std::vector<ref<Expr> > &arguments) {
405 : assert(arguments.size()==2 &&
0: branch 0 not taken
3: branch 1 taken
406 3: "invalid number of arguments to klee_prefex_cex");
407 :
408 : ref<Expr> cond = arguments[1];
3: branch 0 taken
0: branch 1 not taken
409 3: if (cond.getWidth() != Expr::Bool)
410 3: cond = NeExpr::create(cond, ref<Expr>(0, cond.getWidth()));
411 :
412 : Executor::ExactResolutionList rl;
413 6: executor.resolveExact(state, arguments[0], rl, "prefex_cex");
414 :
415 : assert(rl.size() == 1 &&
0: branch 0 not taken
3: branch 1 taken
416 3: "prefer_cex target must resolve to precisely one object");
417 :
418 6: rl[0].first.first->cexPreferences.push_back(cond);
419 3: }
420 :
421 : void SpecialFunctionHandler::handlePrintExpr(ExecutionState &state,
422 : KInstruction *target,
423 0: std::vector<ref<Expr> > &arguments) {
424 : assert(arguments.size()==2 &&
0: branch 0 not taken
0: branch 1 not taken
425 0: "invalid number of arguments to klee_print_expr");
426 :
427 0: std::string msg_str = readStringAtAddress(state, arguments[0]);
428 0: llvm::cerr << msg_str << ":" << arguments[1] << "\n";
429 0: }
430 :
431 :
432 : void SpecialFunctionHandler::handleUnderConstrained(ExecutionState &state,
433 : KInstruction *target,
434 0: std::vector<ref<Expr> > &arguments) {
435 : // XXX should type check args
436 : assert(arguments.size()==1 &&
0: branch 0 not taken
0: branch 1 not taken
437 0: "invalid number of arguments to klee_under_constrained().");
438 : assert(arguments[0].isConstant() &&
0: branch 1 not taken
0: branch 2 not taken
439 0: "symbolic argument given to klee_under_constrained!");
440 :
441 0: unsigned v = arguments[0].getConstantValue();
442 0: llvm::cerr << "argument = " << v << " under=" << state.underConstrained << "\n";
0: branch 0 not taken
0: branch 1 not taken
443 0: if(v) {
444 : assert(state.underConstrained == false &&
0: branch 0 not taken
0: branch 1 not taken
445 0: "Bogus call to klee_under_constrained().");
446 0: state.underConstrained = v;
447 : llvm::cerr << "turning on under!\n";
448 : } else {
0: branch 0 not taken
0: branch 1 not taken
449 0: assert(state.underConstrained != 0 && "Bogus call to klee_taint_end()");
450 0: state.underConstrained = 0;
451 : llvm::cerr << "turning off under!\n";
452 : }
453 0: }
454 :
455 : void SpecialFunctionHandler::handleRevirtObjects(ExecutionState &state,
456 : KInstruction *target,
457 0: std::vector<ref<Expr> > &arguments) {
458 0: state.revirtClonedObjects();
459 0: }
460 :
461 : void SpecialFunctionHandler::handleSetForking(ExecutionState &state,
462 : KInstruction *target,
463 2: std::vector<ref<Expr> > &arguments) {
464 : assert(arguments.size()==1 &&
0: branch 0 not taken
2: branch 1 taken
465 2: "invalid number of arguments to klee_set_forking");
466 2: ref<Expr> value = executor.toUnique(state, arguments[0]);
467 :
0: branch 1 not taken
2: branch 2 taken
468 2: if (!value.isConstant()) {
469 : executor.terminateStateOnError(state,
470 : "klee_set_forking requires a constant arg",
471 0: "user.err");
472 : } else {
473 2: state.forkDisabled = !value.getConstantValue();
474 2: }
475 2: }
476 :
477 : void SpecialFunctionHandler::handleWarning(ExecutionState &state,
478 : KInstruction *target,
479 0: std::vector<ref<Expr> > &arguments) {
0: branch 0 not taken
0: branch 1 not taken
480 0: assert(arguments.size()==1 && "invalid number of arguments to klee_warning");
481 :
482 0: std::string msg_str = readStringAtAddress(state, arguments[0]);
483 : klee_warning("%s: %s", state.stack.back().kf->function->getName().c_str(),
484 0: msg_str.c_str());
485 0: }
486 :
487 : void SpecialFunctionHandler::handleWarningOnce(ExecutionState &state,
488 : KInstruction *target,
489 2: std::vector<ref<Expr> > &arguments) {
490 : assert(arguments.size()==1 &&
0: branch 0 not taken
2: branch 1 taken
491 2: "invalid number of arguments to klee_warning_once");
492 :
493 2: std::string msg_str = readStringAtAddress(state, arguments[0]);
494 : klee_warning_once(0, "%s: %s", state.stack.back().kf->function->getName().c_str(),
495 6: msg_str.c_str());
496 2: }
497 :
498 : void SpecialFunctionHandler::handlePrintRange(ExecutionState &state,
499 : KInstruction *target,
500 2: std::vector<ref<Expr> > &arguments) {
501 : assert(arguments.size()==2 &&
0: branch 0 not taken
2: branch 1 taken
502 2: "invalid number of arguments to klee_print_range");
503 :
504 2: std::string msg_str = readStringAtAddress(state, arguments[0]);
505 2: llvm::cerr << msg_str << ":" << arguments[1];
1: branch 1 taken
1: branch 2 taken
506 2: if (!arguments[1].isConstant()) {
507 : // FIXME: Pull into a unique value method?
508 : ref<Expr> value;
509 1: bool success = executor.solver->getValue(state, arguments[1], value);
0: branch 0 not taken
1: branch 1 taken
510 1: assert(success && "FIXME: Unhandled solver failure");
511 : bool res;
512 : success = executor.solver->mustBeTrue(state,
513 : EqExpr::create(arguments[1], value),
514 1: res);
0: branch 0 not taken
1: branch 1 taken
515 1: assert(success && "FIXME: Unhandled solver failure");
0: branch 0 not taken
1: branch 1 taken
516 1: if (res) {
517 0: llvm::cerr << " == " << value;
518 : } else {
519 1: llvm::cerr << " ~= " << value;
520 2: let(res, executor.solver->getRange(state, arguments[1]));
521 2: llvm::cerr << " (in [" << res.first << ", " << res.second <<"])";
522 1: }
523 : }
524 2: llvm::cerr << "\n";
525 2: }
526 :
527 : void SpecialFunctionHandler::handleGetObjSize(ExecutionState &state,
528 : KInstruction *target,
529 0: std::vector<ref<Expr> > &arguments) {
530 : // XXX should type check args
531 : assert(arguments.size()==1 &&
0: branch 0 not taken
0: branch 1 not taken
532 0: "invalid number of arguments to klee_get_obj_size");
533 : Executor::ExactResolutionList res;
534 0: executor.resolveExact(state, arguments[0], res, "klee_get_obj_size");
0: branch 0 not taken
0: branch 1 not taken
535 0: foreach(it, res.begin(), res.end()) {
536 : executor.bindLocal(target, *it->second,
537 0: ConstantExpr::create(it->first.first->size, Expr::Int32));
538 0: }
539 0: }
540 :
541 : void SpecialFunctionHandler::handleGetErrno(ExecutionState &state,
542 : KInstruction *target,
543 0: std::vector<ref<Expr> > &arguments) {
544 : // XXX should type check args
545 : assert(arguments.size()==0 &&
0: branch 0 not taken
0: branch 1 not taken
546 0: "invalid number of arguments to klee_get_obj_size");
547 : executor.bindLocal(target, state,
548 0: ConstantExpr::create(errno, Expr::Int32));
549 0: }
550 :
551 : void SpecialFunctionHandler::handleCalloc(ExecutionState &state,
552 : KInstruction *target,
553 0: std::vector<ref<Expr> > &arguments) {
554 : // XXX should type check args
555 : assert(arguments.size()==2 &&
0: branch 0 not taken
0: branch 1 not taken
556 0: "invalid number of arguments to calloc");
557 :
558 : ref<Expr> size = MulExpr::create(arguments[0],
559 0: arguments[1]);
560 0: executor.executeAlloc(state, size, false, target, true);
561 0: }
562 :
563 : void SpecialFunctionHandler::handleRealloc(ExecutionState &state,
564 : KInstruction *target,
565 3: std::vector<ref<Expr> > &arguments) {
566 : // XXX should type check args
567 : assert(arguments.size()==2 &&
0: branch 0 not taken
3: branch 1 taken
568 3: "invalid number of arguments to realloc");
569 : ref<Expr> address = arguments[0];
570 : ref<Expr> size = arguments[1];
571 :
572 : Executor::StatePair zeroSize = executor.fork(state,
573 : Expr::createIsZero(size),
574 3: true);
575 :
1: branch 0 taken
2: branch 1 taken
576 3: if (zeroSize.first) { // size == 0
577 1: executor.executeFree(*zeroSize.first, address, target);
578 : }
3: branch 0 taken
0: branch 1 not taken
579 3: if (zeroSize.second) { // size != 0
580 : Executor::StatePair zeroPointer = executor.fork(*zeroSize.second,
581 : Expr::createIsZero(address),
582 3: true);
583 :
2: branch 0 taken
1: branch 1 taken
584 3: if (zeroPointer.first) { // address == 0
585 2: executor.executeAlloc(*zeroPointer.first, size, false, target);
586 : }
2: branch 0 taken
1: branch 1 taken
587 3: if (zeroPointer.second) { // address != 0
588 : Executor::ExactResolutionList rl;
589 4: executor.resolveExact(*zeroPointer.second, address, rl, "realloc");
590 :
3: branch 0 taken
2: branch 1 taken
591 7: foreach(it, rl.begin(), rl.end()) {
592 : executor.executeAlloc(*it->second, size, false, target, false,
593 6: it->first.second);
594 2: }
595 : }
596 3: }
597 3: }
598 :
599 : void SpecialFunctionHandler::handleFree(ExecutionState &state,
600 : KInstruction *target,
601 28: std::vector<ref<Expr> > &arguments) {
602 : // XXX should type check args
603 : assert(arguments.size()==1 &&
0: branch 0 not taken
28: branch 1 taken
604 28: "invalid number of arguments to free");
605 28: executor.executeFree(state, arguments[0]);
606 28: }
607 :
608 : void SpecialFunctionHandler::handleCheckMemoryAccess(ExecutionState &state,
609 : KInstruction *target,
610 3: std::vector<ref<Expr> > &arguments) {
611 : assert(arguments.size()==2 &&
0: branch 0 not taken
3: branch 1 taken
612 3: "invalid number of arguments to klee_check_memory_access");
613 :
614 3: ref<Expr> address = executor.toUnique(state, arguments[0]);
615 3: ref<Expr> size = executor.toUnique(state, arguments[1]);
3: branch 1 taken
0: branch 2 not taken
0: branch 4 not taken
3: branch 5 taken
0: branch 6 not taken
3: branch 7 taken
616 3: if (!address.isConstant() || !size.isConstant()) {
617 : executor.terminateStateOnError(state,
618 : "check_memory_access requires constant args",
619 0: "user.err");
620 : } else {
621 : ObjectPair op;
622 :
1: branch 2 taken
2: branch 3 taken
623 3: if (!state.addressSpace.resolveOne(address.getConstantValue(), op)) {
624 : executor.terminateStateOnError(state,
625 : "check_memory_access: memory error",
626 : "ptr.err",
627 5: executor.getAddressInfo(state, address));
628 : } else {
629 : ref<Expr> chk = op.first->getBoundsCheckPointer(address,
630 6: size.getConstantValue());
0: branch 1 not taken
2: branch 2 taken
631 2: assert(chk.isConstant());
1: branch 1 taken
1: branch 2 taken
632 2: if (!chk.getConstantValue()) {
633 : executor.terminateStateOnError(state,
634 : "check_memory_access: memory error",
635 : "ptr.err",
636 5: executor.getAddressInfo(state, address));
637 2: }
638 : }
639 3: }
640 3: }
641 :
642 : void SpecialFunctionHandler::handleGetValue(ExecutionState &state,
643 : KInstruction *target,
644 3: std::vector<ref<Expr> > &arguments) {
645 : assert(arguments.size()==1 &&
0: branch 0 not taken
3: branch 1 taken
646 3: "invalid number of arguments to klee_get_value");
647 :
648 3: executor.executeGetValue(state, arguments[0], target);
649 3: }
650 :
651 : void SpecialFunctionHandler::handleDefineFixedObject(ExecutionState &state,
652 : KInstruction *target,
653 1: std::vector<ref<Expr> > &arguments) {
654 : assert(arguments.size()==2 &&
0: branch 0 not taken
1: branch 1 taken
655 1: "invalid number of arguments to klee_define_fixed_object");
656 : assert(arguments[0].isConstant() &&
0: branch 1 not taken
1: branch 2 taken
657 1: "expect constant address argument to klee_define_fixed_object");
658 : assert(arguments[1].isConstant() &&
0: branch 1 not taken
1: branch 2 taken
659 1: "expect constant size argument to klee_define_fixed_object");
660 :
661 1: uint64_t address = arguments[0].getConstantValue();
662 1: uint64_t size = arguments[1].getConstantValue();
663 2: MemoryObject *mo = executor.memory->allocateFixed(address, size, state.prevPC->inst);
664 1: executor.bindObjectInState(state, mo, false);
665 1: mo->isUserSpecified = true; // XXX hack;
666 1: }
667 :
668 : void SpecialFunctionHandler::handleMakeSymbolic(ExecutionState &state,
669 : KInstruction *target,
670 91: std::vector<ref<Expr> > &arguments) {
671 : assert(arguments.size()==3 &&
0: branch 0 not taken
91: branch 1 taken
672 91: "invalid number of arguments to klee_make_symbolic[_name]");
673 :
674 : Executor::ExactResolutionList rl;
675 182: executor.resolveExact(state, arguments[0], rl, "make_symbolic");
676 :
91: branch 2 taken
91: branch 3 taken
677 364: foreach(it, rl.begin(), rl.end()) {
678 91: MemoryObject *mo = (MemoryObject*) it->first.first;
679 91: std::string name = readStringAtAddress(state, arguments[2]);
680 182: mo->setName(name);
681 :
682 91: const ObjectState *old = it->first.second;
683 91: ExecutionState *s = it->second;
684 :
0: branch 0 not taken
91: branch 1 taken
685 91: if (old->readOnly) {
686 : executor.terminateStateOnError(*s,
687 : "cannot make readonly object symbolic",
688 0: "user.err");
689 0: return;
690 : }
691 :
692 : bool res;
693 : bool success =
694 : executor.solver->mustBeTrue(*s, EqExpr::create(arguments[1],
695 : mo->getSizeExpr()),
696 91: res);
0: branch 0 not taken
91: branch 1 taken
697 91: assert(success && "FIXME: Unhandled solver failure");
698 :
91: branch 0 taken
0: branch 1 not taken
699 91: if (res) {
700 91: executor.executeMakeSymbolic(*s, mo);
701 : } else {
702 : executor.terminateStateOnError(*s,
703 : "wrong size given to klee_make_symbolic[_name]",
704 0: "user.err");
705 : }
706 91: }
707 : }
708 :
709 : void SpecialFunctionHandler::handleMarkGlobal(ExecutionState &state,
710 : KInstruction *target,
711 0: std::vector<ref<Expr> > &arguments) {
712 : assert(arguments.size()==1 &&
0: branch 0 not taken
0: branch 1 not taken
713 0: "invalid number of arguments to klee_mark_global");
714 :
715 : Executor::ExactResolutionList rl;
716 0: executor.resolveExact(state, arguments[0], rl, "mark_global");
717 :
0: branch 0 not taken
0: branch 1 not taken
718 0: foreach(it, rl.begin(), rl.end()) {
719 0: MemoryObject *mo = (MemoryObject*) it->first.first;
0: branch 0 not taken
0: branch 1 not taken
720 0: assert(!mo->isLocal);
721 0: mo->isGlobal = true;
722 0: }
103: branch 0 taken
0: branch 1 not taken
103: branch 2 taken
0: branch 3 not taken
723 206: }
Generated: 2009-05-17 22:47 by zcov