 |
|
 |
|
| Files: |
1 |
|
Branches Taken: |
16.2% |
33 / 204 |
| Generated: |
2009-05-17 22:47 |
|
Branches Executed: |
24.5% |
50 / 204 |
| |
|
Line Coverage: |
21.7% |
59 / 272 |
| |
 |
|
 |
1 : /* -*- mode: c++; c-basic-offset: 2; -*- */
2 :
3 : #include "klee/Solver.h"
4 : #include "klee/SolverImpl.h"
5 :
6 : #include "SolverStats.h"
7 : #include "STPBuilder.h"
8 :
9 : #include "klee/Constraints.h"
10 : #include "klee/Expr.h"
11 : // FIXME: This shouldn't be here.
12 : #include "klee/Memory.h"
13 : #include "klee/TimerStatIncrementer.h"
14 : #include "klee/util/Assignment.h"
15 : #include "klee/util/ExprPPrinter.h"
16 : #include "klee/util/ExprUtil.h"
17 : #include "klee/Internal/Support/Timer.h"
18 :
19 : #define vc_bvBoolExtract IAMTHESPAWNOFSATAN
20 :
21 : #include <cassert>
22 : #include <map>
23 : #include <vector>
24 :
25 : #include <sys/wait.h>
26 : #include <sys/ipc.h>
27 : #include <sys/shm.h>
28 :
29 : #include "klee/Internal/FIXME/sugar.h"
30 :
31 : using namespace klee;
32 :
33 : /***/
34 :
35 0: const char *Solver::validity_to_str(Validity v) {
0: branch 0 not taken
0: branch 1 not taken
0: branch 2 not taken
36 0: switch (v) {
37 0: default: return "Unknown";
38 0: case True: return "True";
39 0: case False: return "False";
40 : }
41 : }
42 :
43 4: Solver::~Solver() {
4: branch 0 taken
4: branch 1 taken
4: branch 3 taken
0: branch 4 not taken
44 4: delete impl;
45 4: }
46 :
47 4: SolverImpl::~SolverImpl() {
4: branch 0 taken
4: branch 1 taken
0: branch 3 not taken
0: branch 4 not taken
0: branch 6 not taken
4: branch 7 taken
48 4: }
49 :
50 0: bool Solver::evaluate(const Query& query, Validity &result) {
0: branch 0 not taken
0: branch 1 not taken
51 0: assert(query.expr.getWidth() == Expr::Bool && "Invalid expression type!");
52 :
53 : // Maintain invariants implementation expect.
0: branch 1 not taken
0: branch 2 not taken
54 0: if (query.expr.isConstant()) {
0: branch 0 not taken
0: branch 1 not taken
55 0: result = query.expr.getConstantValue() ? True : False;
56 0: return true;
57 : }
58 :
59 0: return impl->computeValidity(query, result);
60 : }
61 :
62 0: bool SolverImpl::computeValidity(const Query& query, Solver::Validity &result) {
63 : bool isTrue, isFalse;
0: branch 1 not taken
0: branch 2 not taken
64 0: if (!computeTruth(query, isTrue))
65 0: return false;
0: branch 0 not taken
0: branch 1 not taken
66 0: if (isTrue) {
67 0: result = Solver::True;
68 : } else {
0: branch 2 not taken
0: branch 3 not taken
69 0: if (!computeTruth(query.negateExpr(), isFalse))
70 0: return false;
0: branch 0 not taken
0: branch 1 not taken
71 0: result = isFalse ? Solver::False : Solver::Unknown;
72 : }
73 0: return true;
74 : }
75 :
76 1017: bool Solver::mustBeTrue(const Query& query, bool &result) {
0: branch 0 not taken
1017: branch 1 taken
77 2034: assert(query.expr.getWidth() == Expr::Bool && "Invalid expression type!");
78 :
79 : // Maintain invariants implementation expect.
0: branch 1 not taken
1017: branch 2 taken
80 1017: if (query.expr.isConstant()) {
81 0: result = query.expr.getConstantValue() ? true : false;
82 0: return true;
83 : }
84 :
85 1017: return impl->computeTruth(query, result);
86 : }
87 :
88 0: bool Solver::mustBeFalse(const Query& query, bool &result) {
89 0: return mustBeTrue(query.negateExpr(), result);
90 : }
91 :
92 0: bool Solver::mayBeTrue(const Query& query, bool &result) {
93 : bool res;
0: branch 1 not taken
0: branch 2 not taken
94 0: if (!mustBeFalse(query, res))
95 0: return false;
96 0: result = !res;
97 0: return true;
98 : }
99 :
100 0: bool Solver::mayBeFalse(const Query& query, bool &result) {
101 : bool res;
0: branch 1 not taken
0: branch 2 not taken
102 0: if (!mustBeTrue(query, res))
103 0: return false;
104 0: result = !res;
105 0: return true;
106 : }
107 :
108 0: bool Solver::getValue(const Query& query, ref<Expr> &result) {
109 : // Maintain invariants implementation expect.
0: branch 1 not taken
0: branch 2 not taken
110 0: if (query.expr.isConstant()) {
111 0: result = query.expr;
112 0: return true;
113 : }
114 :
115 0: return impl->computeValue(query, result);
116 : }
117 :
118 : bool
119 : Solver::getInitialValues(const Query& query,
120 : const std::vector<const MemoryObject*> &objects,
121 0: std::vector< std::vector<unsigned char> > &values) {
122 : bool hasSolution;
123 : bool success =
124 0: impl->computeInitialValues(query, objects, values, hasSolution);
125 : // FIXME: Propogate this out.
0: branch 0 not taken
0: branch 1 not taken
126 0: if (!hasSolution)
127 0: return false;
128 :
129 0: return success;
130 : }
131 :
132 0: std::pair< ref<Expr>, ref<Expr> > Solver::getRange(const Query& query) {
133 0: ref<Expr> e = query.expr;
134 0: Expr::Width width = e.getWidth();
135 : uint64_t min, max;
136 :
0: branch 0 not taken
0: branch 1 not taken
137 0: if (width==1) {
138 : Solver::Validity result;
0: branch 1 not taken
0: branch 2 not taken
139 0: if (!evaluate(query, result))
140 0: assert(0 && "computeValidity failed");
0: branch 0 not taken
0: branch 1 not taken
0: branch 2 not taken
141 0: switch (result) {
142 : case Solver::True:
143 0: min = max = 1; break;
144 : case Solver::False:
145 0: min = max = 0; break;
146 : default:
147 0: min = 0, max = 1; break;
148 : }
0: branch 1 not taken
0: branch 2 not taken
149 0: } else if (e.isConstant()) {
150 0: min = max = e.getConstantValue();
151 : } else {
152 : // binary search for # of useful bits
153 0: uint64_t lo=0, hi=width, mid, bits=0;
0: branch 0 not taken
0: branch 1 not taken
154 0: while (lo<hi) {
155 0: mid = (lo+hi)/2;
156 : bool res;
157 : bool success =
158 : mustBeTrue(query.withExpr(
159 : EqExpr::create(LShrExpr::create(e,
160 : ConstantExpr::create(mid,
161 : width)),
162 : ConstantExpr::create(0, width))),
163 0: res);
0: branch 0 not taken
0: branch 1 not taken
164 0: assert(success && "FIXME: Unhandled solver failure");
0: branch 0 not taken
0: branch 1 not taken
165 0: if (res) {
166 0: hi = mid;
167 : } else {
168 0: lo = mid+1;
169 : }
170 :
171 0: bits = lo;
172 : }
173 :
174 : // could binary search for training zeros and offset
175 : // min max but unlikely to be very useful
176 :
177 : // check common case
178 : bool res;
179 : bool success =
180 : mayBeTrue(query.withExpr(EqExpr::create(e, ConstantExpr::create(0,
181 : width))),
182 0: res);
0: branch 0 not taken
0: branch 1 not taken
183 0: assert(success && "FIXME: Unhandled solver failure");
0: branch 0 not taken
0: branch 1 not taken
184 0: if (res) {
185 0: min = 0;
186 : } else {
187 : // binary search for min
188 0: lo=0, hi=bits64::maxValueOfNBits(bits);
0: branch 0 not taken
0: branch 1 not taken
189 0: while (lo<hi) {
190 0: mid = (lo+hi)/2;
191 : bool res;
192 : bool success =
193 : mayBeTrue(query.withExpr(UleExpr::create(e,
194 : ConstantExpr::create(mid,
195 : width))),
196 0: res);
0: branch 0 not taken
0: branch 1 not taken
197 0: assert(success && "FIXME: Unhandled solver failure");
0: branch 0 not taken
0: branch 1 not taken
198 0: if (res) {
199 0: hi = mid;
200 : } else {
201 0: lo = mid+1;
202 : }
203 : }
204 :
205 0: min = lo;
206 : }
207 :
208 : // binary search for max
209 0: lo=min, hi=bits64::maxValueOfNBits(bits);
0: branch 0 not taken
0: branch 1 not taken
210 0: while (lo<hi) {
211 0: mid = (lo+hi)/2;
212 : bool res;
213 : bool success =
214 : mustBeTrue(query.withExpr(UleExpr::create(e,
215 : ConstantExpr::create(mid,
216 : width))),
217 0: res);
0: branch 0 not taken
0: branch 1 not taken
218 0: assert(success && "FIXME: Unhandled solver failure");
0: branch 0 not taken
0: branch 1 not taken
219 0: if (res) {
220 0: hi = mid;
221 : } else {
222 0: lo = mid+1;
223 : }
224 : }
225 :
226 0: max = lo;
227 : }
228 :
229 : return std::make_pair(ConstantExpr::create(min, width),
230 0: ConstantExpr::create(max, width));
231 : }
232 :
233 : /***/
234 :
235 : class ValidatingSolver : public SolverImpl {
236 : private:
237 : Solver *solver, *oracle;
238 :
239 : public:
240 : ValidatingSolver(Solver *_solver, Solver *_oracle)
241 0: : solver(_solver), oracle(_oracle) {}
0: branch 0 not taken
0: branch 1 not taken
0: branch 5 not taken
0: branch 6 not taken
0: branch 8 not taken
0: branch 9 not taken
0: branch 13 not taken
0: branch 14 not taken
242 0: ~ValidatingSolver() { delete solver; }
243 :
244 : bool computeValidity(const Query&, Solver::Validity &result);
245 : bool computeTruth(const Query&, bool &isValid);
246 : bool computeValue(const Query&, ref<Expr> &result);
247 : bool computeInitialValues(const Query&,
248 : const std::vector<const MemoryObject*> &objects,
249 : std::vector< std::vector<unsigned char> > &values,
250 : bool &hasSolution);
251 : };
252 :
253 : bool ValidatingSolver::computeTruth(const Query& query,
254 0: bool &isValid) {
255 : bool answer;
256 :
0: branch 1 not taken
0: branch 2 not taken
257 0: if (!solver->impl->computeTruth(query, isValid))
258 0: return false;
0: branch 1 not taken
0: branch 2 not taken
259 0: if (!oracle->impl->computeTruth(query, answer))
260 0: return false;
261 :
0: branch 0 not taken
0: branch 1 not taken
262 0: if (isValid != answer)
263 0: assert(0 && "invalid solver result (computeTruth)");
264 :
265 0: return true;
266 : }
267 :
268 : bool ValidatingSolver::computeValidity(const Query& query,
269 0: Solver::Validity &result) {
270 : Solver::Validity answer;
271 :
0: branch 1 not taken
0: branch 2 not taken
272 0: if (!solver->impl->computeValidity(query, result))
273 0: return false;
0: branch 1 not taken
0: branch 2 not taken
274 0: if (!oracle->impl->computeValidity(query, answer))
275 0: return false;
276 :
0: branch 0 not taken
0: branch 1 not taken
277 0: if (result != answer)
278 0: assert(0 && "invalid solver result (computeValidity)");
279 :
280 0: return true;
281 : }
282 :
283 : bool ValidatingSolver::computeValue(const Query& query,
284 0: ref<Expr> &result) {
285 : bool answer;
286 :
0: branch 1 not taken
0: branch 2 not taken
287 0: if (!solver->impl->computeValue(query, result))
288 0: return false;
289 : // We don't want to compare, but just make sure this is a legal
290 : // solution.
0: branch 4 not taken
0: branch 5 not taken
291 0: if (!oracle->impl->computeTruth(query.withExpr(NeExpr::create(query.expr,
292 : result)),
293 : answer))
294 0: return false;
295 :
0: branch 0 not taken
0: branch 1 not taken
296 0: if (answer)
297 0: assert(0 && "invalid solver result (computeValue)");
298 :
299 0: return true;
300 : }
301 :
302 : bool
303 : ValidatingSolver::computeInitialValues(const Query& query,
304 : const std::vector<const MemoryObject*>
305 : &objects,
306 : std::vector< std::vector<unsigned char> >
307 : &values,
308 0: bool &hasSolution) {
309 : bool answer;
310 :
0: branch 1 not taken
0: branch 2 not taken
311 0: if (!solver->impl->computeInitialValues(query, objects, values,
312 : hasSolution))
313 0: return false;
314 :
0: branch 0 not taken
0: branch 1 not taken
315 0: if (hasSolution) {
316 : // Assert the bindings as constraints, and verify that the
317 : // conjunction of the actual constraints is satisfiable.
318 : std::vector< ref<Expr> > bindings;
319 0: unsigned i=0;
0: branch 0 not taken
0: branch 1 not taken
320 0: foreach(it, values.begin(), values.end()) {
321 0: const MemoryObject *mo = objects[i++];
0: branch 0 not taken
0: branch 1 not taken
322 0: for (unsigned j=0; j<mo->size; j++) {
323 0: unsigned char value = (*it)[j];
324 : bindings.push_back(EqExpr::create(ReadExpr::create(UpdateList(mo, true, 0),
325 : ref<Expr>(j, Expr::Int32)),
326 0: ref<Expr>(value, Expr::Int8)));
327 : }
328 : }
329 : ConstraintManager tmp(bindings);
330 0: ref<Expr> constraints = Expr::createNot(query.expr);
0: branch 0 not taken
0: branch 1 not taken
331 0: foreach(it, query.constraints.begin(), query.constraints.end())
332 0: constraints = AndExpr::create(constraints, *it);
333 :
0: branch 2 not taken
0: branch 3 not taken
334 0: if (!oracle->impl->computeTruth(Query(tmp, constraints), answer))
335 0: return false;
0: branch 0 not taken
0: branch 1 not taken
336 0: if (!answer)
337 0: assert(0 && "invalid solver result (computeInitialValues)");
338 : } else {
0: branch 1 not taken
0: branch 2 not taken
339 0: if (!oracle->impl->computeTruth(query, answer))
340 0: return false;
0: branch 0 not taken
0: branch 1 not taken
341 0: if (!answer)
342 0: assert(0 && "invalid solver result (computeInitialValues)");
343 : }
344 :
345 0: return true;
346 : }
347 :
348 0: Solver *klee::createValidatingSolver(Solver *s, Solver *oracle) {
349 0: return new Solver(new ValidatingSolver(s, oracle));
350 : }
351 :
352 : /***/
353 :
354 : class STPSolverImpl : public SolverImpl {
355 : private:
356 : /// The solver we are part of, for access to public information.
357 : STPSolver *solver;
358 : VC vc;
359 : STPBuilder *builder;
360 : double timeout;
361 : bool useForkedSTP;
362 :
363 : public:
364 : STPSolverImpl(STPSolver *_solver, bool _useForkedSTP);
365 : ~STPSolverImpl();
366 :
367 : char *getConstraintLog(const Query&);
368 0: void setTimeout(double _timeout) { timeout = _timeout; }
369 :
370 : bool computeTruth(const Query&, bool &isValid);
371 : bool computeValue(const Query&, ref<Expr> &result);
372 : bool computeInitialValues(const Query&,
373 : const std::vector<const MemoryObject*> &objects,
374 : std::vector< std::vector<unsigned char> > &values,
375 : bool &hasSolution);
376 : };
377 :
378 : static unsigned char *shared_memory_ptr;
379 : static const unsigned shared_memory_size = 1<<20;
380 : static int shared_memory_id;
381 :
382 0: static void stp_error_handler(const char* err_msg) {
383 0: fprintf(stderr, "error: STP Error: %s\n", err_msg);
384 0: abort();
385 : }
386 :
387 1: STPSolverImpl::STPSolverImpl(STPSolver *_solver, bool _useForkedSTP)
388 : : solver(_solver),
389 : vc(vc_createValidityChecker()),
390 : builder(new STPBuilder(vc)),
391 : timeout(0.0),
392 2: useForkedSTP(_useForkedSTP)
393 : {
0: branch 0 not taken
1: branch 1 taken
0: branch 3 not taken
0: branch 4 not taken
394 1: assert(vc && "unable to create validity checker");
0: branch 0 not taken
1: branch 1 taken
0: branch 3 not taken
0: branch 4 not taken
395 1: assert(builder && "unable to create STPBuilder");
396 :
397 1: vc_registerErrorHandler(::stp_error_handler);
398 :
1: branch 0 taken
0: branch 1 not taken
0: branch 2 not taken
0: branch 3 not taken
399 1: if (useForkedSTP) {
400 1: shared_memory_id = shmget(IPC_PRIVATE, shared_memory_size, IPC_CREAT | 0700);
0: branch 0 not taken
1: branch 1 taken
0: branch 3 not taken
0: branch 4 not taken
401 1: assert(shared_memory_id>=0 && "shmget failed");
402 1: shared_memory_ptr = (unsigned char*) shmat(shared_memory_id, NULL, 0);
0: branch 0 not taken
1: branch 1 taken
0: branch 3 not taken
0: branch 4 not taken
403 1: assert(shared_memory_ptr!=(void*)-1 && "shmat failed");
404 1: shmctl(shared_memory_id, IPC_RMID, NULL);
405 : }
406 1: }
407 :
408 1: STPSolverImpl::~STPSolverImpl() {
1: branch 0 taken
0: branch 1 not taken
1: branch 4 taken
1: branch 5 taken
0: branch 8 not taken
0: branch 9 not taken
409 1: delete builder;
410 :
411 1: vc_Destroy(vc);
1: branch 1 taken
0: branch 2 not taken
0: branch 5 not taken
0: branch 6 not taken
0: branch 9 not taken
0: branch 10 not taken
412 1: }
413 :
414 : /***/
415 :
416 1: STPSolver::STPSolver(bool useForkedSTP)
417 2: : Solver(new STPSolverImpl(this, useForkedSTP))
418 : {
419 1: }
420 :
421 0: char *STPSolver::getConstraintLog(const Query &query) {
422 0: return static_cast<STPSolverImpl*>(impl)->getConstraintLog(query);
423 : }
424 :
425 0: void STPSolver::setTimeout(double timeout) {
426 0: static_cast<STPSolverImpl*>(impl)->setTimeout(timeout);
427 0: }
428 :
429 : /***/
430 :
431 0: char *STPSolverImpl::getConstraintLog(const Query &query) {
432 0: vc_push(vc);
0: branch 0 not taken
0: branch 1 not taken
433 0: foreach (ei, query.constraints.begin(), query.constraints.end())
434 0: vc_assertFormula(vc, builder->construct(*ei));
435 : assert(query.expr == ref<Expr>(0, Expr::Bool) &&
0: branch 0 not taken
0: branch 1 not taken
0: branch 3 not taken
0: branch 4 not taken
436 0: "Unexpected expression in query!");
437 :
438 : char *buffer;
439 : unsigned long length;
440 : vc_printQueryStateToBuffer(vc, builder->getFalse(),
441 0: &buffer, &length, false);
442 0: vc_pop(vc);
443 :
444 0: return buffer;
445 : }
446 :
447 : bool STPSolverImpl::computeTruth(const Query& query,
448 0: bool &isValid) {
449 : std::vector<const MemoryObject*> objects;
450 : std::vector< std::vector<unsigned char> > values;
451 : bool hasSolution;
452 :
0: branch 1 not taken
0: branch 2 not taken
453 0: if (!computeInitialValues(query, objects, values, hasSolution))
454 0: return false;
455 :
456 0: isValid = !hasSolution;
457 0: return true;
458 : }
459 :
460 : bool STPSolverImpl::computeValue(const Query& query,
461 0: ref<Expr> &result) {
462 : std::vector<const MemoryObject *> objects;
463 : std::vector< std::vector<unsigned char> > values;
464 : bool hasSolution;
465 :
466 : // Find the object used in the expression, and compute an assignment
467 : // for them.
468 0: findSymbolicObjects(query.expr, objects);
0: branch 1 not taken
0: branch 2 not taken
469 0: if (!computeInitialValues(query.withFalse(), objects, values, hasSolution))
470 0: return false;
0: branch 0 not taken
0: branch 1 not taken
471 0: assert(hasSolution && "state has invalid constraint set");
472 :
473 : // Evaluate the expression with the computed assignment.
474 : Assignment a(objects, values);
475 0: result = a.evaluate(query.expr);
476 :
477 0: return true;
478 : }
479 :
480 : static void runAndGetCex(::VC vc, STPBuilder *builder, ::VCExpr q,
481 : const std::vector<const MemoryObject*> &objects,
482 : std::vector< std::vector<unsigned char> > &values,
483 0: bool &hasSolution) {
484 : // XXX I want to be able to timeout here, safely
485 0: hasSolution = !vc_query(vc, q);
486 :
0: branch 0 not taken
0: branch 1 not taken
487 0: if (hasSolution) {
488 0: values.reserve(objects.size());
0: branch 1 not taken
0: branch 2 not taken
489 0: foreach(oi, objects.begin(), objects.end()) {
490 0: const MemoryObject *obj = *oi;
491 : std::vector<unsigned char> data;
492 :
493 0: data.reserve(obj->size);
0: branch 1 not taken
0: branch 2 not taken
494 0: for (unsigned offset = 0; offset<obj->size; offset++) {
495 : ExprHandle counter = vc_getCounterExample(vc,
496 : builder->getInitialRead(obj,
497 0: offset));
498 0: unsigned char val = getBVUnsigned(counter);
499 : data.push_back(val);
500 : }
501 :
502 : values.push_back(data);
503 : }
504 : }
505 0: }
506 :
507 0: static void stpTimeoutHandler(int x) {
508 0: _exit(52);
509 : }
510 :
511 : static bool runAndGetCexForked(::VC vc,
512 : STPBuilder *builder,
513 : ::VCExpr q,
514 : const std::vector<const MemoryObject*> &objects,
515 : std::vector< std::vector<unsigned char> > &values,
516 : bool &hasSolution,
517 1017: double timeout) {
518 1017: unsigned char *pos = shared_memory_ptr;
519 1017: unsigned sum = 0;
1959: branch 0 taken
1017: branch 1 taken
520 2976: foreach(it, objects.begin(), objects.end())
521 1959: sum += (*it)->size;
0: branch 0 not taken
1017: branch 1 taken
522 1017: assert(sum<shared_memory_size && "not enough shared memory for counterexample");
523 :
524 1017: fflush(stdout);
525 1017: fflush(stderr);
526 1017: int pid = fork();
0: branch 0 not taken
1017: branch 1 taken
527 1017: if (pid==-1) {
528 0: fprintf(stderr, "error: fork failed (for STP)");
529 0: return false;
530 : }
531 :
0: branch 0 not taken
1017: branch 1 taken
532 1017: if (pid == 0) {
0: branch 0 not taken
0: branch 1 not taken
533 0: if (timeout) {
534 0: ::alarm(0); /* Turn off alarm so we can safely set signal handler */
535 0: ::signal(SIGALRM, stpTimeoutHandler);
536 0: ::alarm(std::max(1, (int)timeout));
537 : }
538 0: unsigned res = vc_query(vc, q);
0: branch 0 not taken
0: branch 1 not taken
539 0: if (!res) {
0: branch 0 not taken
0: branch 1 not taken
540 0: foreach(oi, objects.begin(), objects.end()) {
541 0: const MemoryObject *mo = *oi;
0: branch 1 not taken
0: branch 2 not taken
542 0: for (unsigned offset = 0; offset<mo->size; offset++) {
543 : ExprHandle counter = vc_getCounterExample(vc,
544 : builder->getInitialRead(mo,
545 0: offset));
546 0: *pos++ = getBVUnsigned(counter);
547 : }
548 : }
549 : }
550 0: _exit(res);
551 : } else {
552 : int status;
553 1017: int res = waitpid(pid, &status, 0);
554 :
0: branch 0 not taken
1017: branch 1 taken
555 1017: if (res<0) {
556 0: fprintf(stderr, "error: waitpid() for STP failed");
557 0: return false;
558 : }
559 :
560 : // From timed_run.py: It appears that linux at least will on
561 : // "occasion" return a status when the process was terminated by a
562 : // signal, so test signal first.
1017: branch 0 taken
0: branch 1 not taken
0: branch 2 not taken
1017: branch 3 taken
563 1017: if (WIFSIGNALED(status) || !WIFEXITED(status)) {
564 0: fprintf(stderr, "error: STP did not return successfully");
565 0: return false;
566 : }
567 :
568 1017: int exitcode = WEXITSTATUS(status);
0: branch 0 not taken
1017: branch 1 taken
569 1017: if (exitcode==0) {
570 0: hasSolution = true;
1017: branch 0 taken
0: branch 1 not taken
571 1017: } else if (exitcode==1) {
572 1017: hasSolution = false;
0: branch 0 not taken
0: branch 1 not taken
573 0: } else if (exitcode==52) {
574 0: fprintf(stderr, "error: STP timed out");
575 0: return false;
576 : } else {
577 0: fprintf(stderr, "error: STP did not return a recognized code");
578 0: return false;
579 : }
580 :
0: branch 0 not taken
1017: branch 1 taken
581 1017: if (hasSolution) {
582 0: values = std::vector< std::vector<unsigned char> >(objects.size());
583 0: unsigned i=0;
0: branch 0 not taken
0: branch 1 not taken
584 0: foreach(oi, objects.begin(), objects.end()) {
585 0: const MemoryObject *mo = *oi;
586 0: std::vector<unsigned char> &data = values[i++];
587 0: data.insert(data.begin(), pos, pos+mo->size);
588 0: pos += mo->size;
589 : }
590 : }
591 :
592 1017: return true;
593 : }
594 : }
595 :
596 : bool
597 : STPSolverImpl::computeInitialValues(const Query &query,
598 : const std::vector<const MemoryObject*>
599 : &objects,
600 : std::vector< std::vector<unsigned char> >
601 : &values,
602 1017: bool &hasSolution) {
603 : TimerStatIncrementer t(stats::queryTime);
604 :
605 1017: vc_push(vc);
606 :
1017: branch 0 taken
1017: branch 1 taken
607 4068: foreach(ei, query.constraints.begin(), query.constraints.end())
608 2034: vc_assertFormula(vc, builder->construct(*ei));
609 :
610 : ++stats::queries;
611 : ++stats::queryCounterexamples;
612 :
613 2034: ExprHandle stp_e = builder->construct(query.expr);
614 :
615 : bool success;
1017: branch 0 taken
0: branch 1 not taken
616 1017: if (useForkedSTP) {
617 : success = runAndGetCexForked(vc, builder, stp_e, objects, values,
618 2034: hasSolution, timeout);
619 : } else {
620 0: runAndGetCex(vc, builder, stp_e, objects, values, hasSolution);
621 0: success = true;
622 : }
623 :
1017: branch 0 taken
0: branch 1 not taken
624 1017: if (success) {
0: branch 0 not taken
1017: branch 1 taken
625 1017: if (hasSolution)
626 : ++stats::queriesInvalid;
627 : else
628 : ++stats::queriesValid;
629 : }
630 :
631 1017: vc_pop(vc);
632 :
633 1017: return success;
634 : }
Generated: 2009-05-17 22:47 by zcov