klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
Solver.cpp
Go to the documentation of this file.
1 //===-- Solver.cpp --------------------------------------------------------===//
2 //
3 // The KLEE Symbolic Virtual Machine
4 //
5 // This file is distributed under the University of Illinois Open Source
6 // License. See LICENSE.TXT for details.
7 //
8 //===----------------------------------------------------------------------===//
9 
10 #include "klee/Solver.h"
11 #include "klee/SolverImpl.h"
12 
13 #include "SolverStats.h"
14 #include "STPBuilder.h"
15 #include "MetaSMTBuilder.h"
16 
17 #include "klee/Constraints.h"
18 #include "klee/Expr.h"
20 #include "klee/util/Assignment.h"
21 #include "klee/util/ExprPPrinter.h"
22 #include "klee/util/ExprUtil.h"
24 #include "klee/CommandLine.h"
25 
26 #define vc_bvBoolExtract IAMTHESPAWNOFSATAN
27 
28 #include <cassert>
29 #include <cstdio>
30 #include <map>
31 #include <vector>
32 
33 #include <errno.h>
34 #include <unistd.h>
35 #include <signal.h>
36 #include <sys/wait.h>
37 #include <sys/ipc.h>
38 #include <sys/shm.h>
39 
40 #include "llvm/Support/CommandLine.h"
41 
42 llvm::cl::opt<bool>
43 IgnoreSolverFailures("ignore-solver-failures",
44  llvm::cl::init(false),
45  llvm::cl::desc("Ignore any solver failures (default=off)"));
46 
47 
48 using namespace klee;
49 
50 
51 #ifdef SUPPORT_METASMT
52 
53 #include <metaSMT/DirectSolver_Context.hpp>
54 #include <metaSMT/backend/Z3_Backend.hpp>
55 #include <metaSMT/backend/Boolector.hpp>
56 #include <metaSMT/backend/MiniSAT.hpp>
57 #include <metaSMT/support/run_algorithm.hpp>
58 #include <metaSMT/API/Stack.hpp>
59 #include <metaSMT/API/Group.hpp>
60 
61 using namespace metaSMT;
62 using namespace metaSMT::solver;
63 
64 #endif /* SUPPORT_METASMT */
65 
66 
67 
68 /***/
69 
71 }
72 
73 bool SolverImpl::computeValidity(const Query& query, Solver::Validity &result) {
74  bool isTrue, isFalse;
75  if (!computeTruth(query, isTrue))
76  return false;
77  if (isTrue) {
78  result = Solver::True;
79  } else {
80  if (!computeTruth(query.negateExpr(), isFalse))
81  return false;
82  result = isFalse ? Solver::False : Solver::Unknown;
83  }
84  return true;
85 }
86 
88 {
89  switch (statusCode)
90  {
91  case SOLVER_RUN_STATUS_SUCCESS_SOLVABLE:
92  return "OPERATION SUCCESSFUL, QUERY IS SOLVABLE";
93  case SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE:
94  return "OPERATION SUCCESSFUL, QUERY IS UNSOLVABLE";
95  case SOLVER_RUN_STATUS_FAILURE:
96  return "OPERATION FAILED";
97  case SOLVER_RUN_STATUS_TIMEOUT:
98  return "SOLVER TIMEOUT";
99  case SOLVER_RUN_STATUS_FORK_FAILED:
100  return "FORK FAILED";
101  case SOLVER_RUN_STATUS_INTERRUPTED:
102  return "SOLVER PROCESS INTERRUPTED";
103  case SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE:
104  return "UNEXPECTED SOLVER PROCESS EXIT CODE";
105  case SOLVER_RUN_STATUS_WAITPID_FAILED:
106  return "WAITPID FAILED FOR SOLVER PROCESS";
107  default:
108  return "UNRECOGNIZED OPERATION STATUS";
109  }
110 }
111 
113  switch (v) {
114  default: return "Unknown";
115  case True: return "True";
116  case False: return "False";
117  }
118 }
119 
121  delete impl;
122 }
123 
124 char *Solver::getConstraintLog(const Query& query) {
125  return impl->getConstraintLog(query);
126 }
127 
128 void Solver::setCoreSolverTimeout(double timeout) {
129  impl->setCoreSolverTimeout(timeout);
130 }
131 
132 bool Solver::evaluate(const Query& query, Validity &result) {
133  assert(query.expr->getWidth() == Expr::Bool && "Invalid expression type!");
134 
135  // Maintain invariants implementations expect.
136  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(query.expr)) {
137  result = CE->isTrue() ? True : False;
138  return true;
139  }
140 
141  return impl->computeValidity(query, result);
142 }
143 
144 bool Solver::mustBeTrue(const Query& query, bool &result) {
145  assert(query.expr->getWidth() == Expr::Bool && "Invalid expression type!");
146 
147  // Maintain invariants implementations expect.
148  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(query.expr)) {
149  result = CE->isTrue() ? true : false;
150  return true;
151  }
152 
153  return impl->computeTruth(query, result);
154 }
155 
156 bool Solver::mustBeFalse(const Query& query, bool &result) {
157  return mustBeTrue(query.negateExpr(), result);
158 }
159 
160 bool Solver::mayBeTrue(const Query& query, bool &result) {
161  bool res;
162  if (!mustBeFalse(query, res))
163  return false;
164  result = !res;
165  return true;
166 }
167 
168 bool Solver::mayBeFalse(const Query& query, bool &result) {
169  bool res;
170  if (!mustBeTrue(query, res))
171  return false;
172  result = !res;
173  return true;
174 }
175 
176 bool Solver::getValue(const Query& query, ref<ConstantExpr> &result) {
177  // Maintain invariants implementation expect.
178  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(query.expr)) {
179  result = CE;
180  return true;
181  }
182 
183  // FIXME: Push ConstantExpr requirement down.
184  ref<Expr> tmp;
185  if (!impl->computeValue(query, tmp))
186  return false;
187 
188  result = cast<ConstantExpr>(tmp);
189  return true;
190 }
191 
192 bool
194  const std::vector<const Array*> &objects,
195  std::vector< std::vector<unsigned char> > &values) {
196  bool hasSolution;
197  bool success =
198  impl->computeInitialValues(query, objects, values, hasSolution);
199  // FIXME: Propogate this out.
200  if (!hasSolution)
201  return false;
202 
203  return success;
204 }
205 
206 std::pair< ref<Expr>, ref<Expr> > Solver::getRange(const Query& query) {
207  ref<Expr> e = query.expr;
208  Expr::Width width = e->getWidth();
209  uint64_t min, max;
210 
211  if (width==1) {
212  Solver::Validity result;
213  if (!evaluate(query, result))
214  assert(0 && "computeValidity failed");
215  switch (result) {
216  case Solver::True:
217  min = max = 1; break;
218  case Solver::False:
219  min = max = 0; break;
220  default:
221  min = 0, max = 1; break;
222  }
223  } else if (ConstantExpr *CE = dyn_cast<ConstantExpr>(e)) {
224  min = max = CE->getZExtValue();
225  } else {
226  // binary search for # of useful bits
227  uint64_t lo=0, hi=width, mid, bits=0;
228  while (lo<hi) {
229  mid = lo + (hi - lo)/2;
230  bool res;
231  bool success =
232  mustBeTrue(query.withExpr(
233  EqExpr::create(LShrExpr::create(e,
235  width)),
236  ConstantExpr::create(0, width))),
237  res);
238 
239  assert(success && "FIXME: Unhandled solver failure");
240  (void) success;
241 
242  if (res) {
243  hi = mid;
244  } else {
245  lo = mid+1;
246  }
247 
248  bits = lo;
249  }
250 
251  // could binary search for training zeros and offset
252  // min max but unlikely to be very useful
253 
254  // check common case
255  bool res = false;
256  bool success =
257  mayBeTrue(query.withExpr(EqExpr::create(e, ConstantExpr::create(0,
258  width))),
259  res);
260 
261  assert(success && "FIXME: Unhandled solver failure");
262  (void) success;
263 
264  if (res) {
265  min = 0;
266  } else {
267  // binary search for min
268  lo=0, hi=bits64::maxValueOfNBits(bits);
269  while (lo<hi) {
270  mid = lo + (hi - lo)/2;
271  bool res = false;
272  bool success =
273  mayBeTrue(query.withExpr(UleExpr::create(e,
275  width))),
276  res);
277 
278  assert(success && "FIXME: Unhandled solver failure");
279  (void) success;
280 
281  if (res) {
282  hi = mid;
283  } else {
284  lo = mid+1;
285  }
286  }
287 
288  min = lo;
289  }
290 
291  // binary search for max
292  lo=min, hi=bits64::maxValueOfNBits(bits);
293  while (lo<hi) {
294  mid = lo + (hi - lo)/2;
295  bool res;
296  bool success =
297  mustBeTrue(query.withExpr(UleExpr::create(e,
299  width))),
300  res);
301 
302  assert(success && "FIXME: Unhandled solver failure");
303  (void) success;
304 
305  if (res) {
306  hi = mid;
307  } else {
308  lo = mid+1;
309  }
310  }
311 
312  max = lo;
313  }
314 
315  return std::make_pair(ConstantExpr::create(min, width),
316  ConstantExpr::create(max, width));
317 }
318 
319 /***/
320 
321 class ValidatingSolver : public SolverImpl {
322 private:
323  Solver *solver, *oracle;
324 
325 public:
326  ValidatingSolver(Solver *_solver, Solver *_oracle)
327  : solver(_solver), oracle(_oracle) {}
328  ~ValidatingSolver() { delete solver; }
329 
330  bool computeValidity(const Query&, Solver::Validity &result);
331  bool computeTruth(const Query&, bool &isValid);
332  bool computeValue(const Query&, ref<Expr> &result);
333  bool computeInitialValues(const Query&,
334  const std::vector<const Array*> &objects,
335  std::vector< std::vector<unsigned char> > &values,
336  bool &hasSolution);
337  SolverRunStatus getOperationStatusCode();
338  char *getConstraintLog(const Query&);
339  void setCoreSolverTimeout(double timeout);
340 };
341 
343  bool &isValid) {
344  bool answer;
345 
346  if (!solver->impl->computeTruth(query, isValid))
347  return false;
348  if (!oracle->impl->computeTruth(query, answer))
349  return false;
350 
351  if (isValid != answer)
352  assert(0 && "invalid solver result (computeTruth)");
353 
354  return true;
355 }
356 
358  Solver::Validity &result) {
359  Solver::Validity answer;
360 
361  if (!solver->impl->computeValidity(query, result))
362  return false;
363  if (!oracle->impl->computeValidity(query, answer))
364  return false;
365 
366  if (result != answer)
367  assert(0 && "invalid solver result (computeValidity)");
368 
369  return true;
370 }
371 
373  ref<Expr> &result) {
374  bool answer;
375 
376  if (!solver->impl->computeValue(query, result))
377  return false;
378  // We don't want to compare, but just make sure this is a legal
379  // solution.
380  if (!oracle->impl->computeTruth(query.withExpr(NeExpr::create(query.expr,
381  result)),
382  answer))
383  return false;
384 
385  if (answer)
386  assert(0 && "invalid solver result (computeValue)");
387 
388  return true;
389 }
390 
391 bool
393  const std::vector<const Array*>
394  &objects,
395  std::vector< std::vector<unsigned char> >
396  &values,
397  bool &hasSolution) {
398  bool answer;
399 
400  if (!solver->impl->computeInitialValues(query, objects, values,
401  hasSolution))
402  return false;
403 
404  if (hasSolution) {
405  // Assert the bindings as constraints, and verify that the
406  // conjunction of the actual constraints is satisfiable.
407  std::vector< ref<Expr> > bindings;
408  for (unsigned i = 0; i != values.size(); ++i) {
409  const Array *array = objects[i];
410  assert(array);
411  for (unsigned j=0; j<array->size; j++) {
412  unsigned char value = values[i][j];
413  bindings.push_back(EqExpr::create(ReadExpr::create(UpdateList(array, 0),
414  ConstantExpr::alloc(j, array->getDomain())),
415  ConstantExpr::alloc(value, array->getRange())));
416  }
417  }
418  ConstraintManager tmp(bindings);
419  ref<Expr> constraints = Expr::createIsZero(query.expr);
421  ie = query.constraints.end(); it != ie; ++it)
422  constraints = AndExpr::create(constraints, *it);
423 
424  if (!oracle->impl->computeTruth(Query(tmp, constraints), answer))
425  return false;
426  if (!answer)
427  assert(0 && "invalid solver result (computeInitialValues)");
428  } else {
429  if (!oracle->impl->computeTruth(query, answer))
430  return false;
431  if (!answer)
432  assert(0 && "invalid solver result (computeInitialValues)");
433  }
434 
435  return true;
436 }
437 
439  return solver->impl->getOperationStatusCode();
440 }
441 
443  return solver->impl->getConstraintLog(query);
444 }
445 
447  solver->impl->setCoreSolverTimeout(timeout);
448 }
449 
451  return new Solver(new ValidatingSolver(s, oracle));
452 }
453 
454 /***/
455 
456 class DummySolverImpl : public SolverImpl {
457 public:
459 
460  bool computeValidity(const Query&, Solver::Validity &result) {
461  ++stats::queries;
462  // FIXME: We should have stats::queriesFail;
463  return false;
464  }
465  bool computeTruth(const Query&, bool &isValid) {
466  ++stats::queries;
467  // FIXME: We should have stats::queriesFail;
468  return false;
469  }
470  bool computeValue(const Query&, ref<Expr> &result) {
471  ++stats::queries;
473  return false;
474  }
476  const std::vector<const Array*> &objects,
477  std::vector< std::vector<unsigned char> > &values,
478  bool &hasSolution) {
479  ++stats::queries;
481  return false;
482  }
484  return SOLVER_RUN_STATUS_FAILURE;
485  }
486 
487 };
488 
490  return new Solver(new DummySolverImpl());
491 }
492 
493 /***/
494 
495 class STPSolverImpl : public SolverImpl {
496 private:
497  VC vc;
499  double timeout;
501  SolverRunStatus runStatusCode;
502 
503 public:
504  STPSolverImpl(bool _useForkedSTP, bool _optimizeDivides = true);
505  ~STPSolverImpl();
506 
507  char *getConstraintLog(const Query&);
508  void setCoreSolverTimeout(double _timeout) { timeout = _timeout; }
509 
510  bool computeTruth(const Query&, bool &isValid);
511  bool computeValue(const Query&, ref<Expr> &result);
512  bool computeInitialValues(const Query&,
513  const std::vector<const Array*> &objects,
514  std::vector< std::vector<unsigned char> > &values,
515  bool &hasSolution);
516  SolverRunStatus getOperationStatusCode();
517 };
518 
519 static unsigned char *shared_memory_ptr;
520 static const unsigned shared_memory_size = 1<<20;
521 static int shared_memory_id;
522 
523 static void stp_error_handler(const char* err_msg) {
524  fprintf(stderr, "error: STP Error: %s\n", err_msg);
525  abort();
526 }
527 
528 STPSolverImpl::STPSolverImpl(bool _useForkedSTP, bool _optimizeDivides)
529  : vc(vc_createValidityChecker()),
530  builder(new STPBuilder(vc, _optimizeDivides)),
531  timeout(0.0),
532  useForkedSTP(_useForkedSTP),
533  runStatusCode(SOLVER_RUN_STATUS_FAILURE)
534 {
535  assert(vc && "unable to create validity checker");
536  assert(builder && "unable to create STPBuilder");
537 
538  // In newer versions of STP, a memory management mechanism has been
539  // introduced that automatically invalidates certain C interface
540  // pointers at vc_Destroy time. This caused double-free errors
541  // due to the ExprHandle destructor also attempting to invalidate
542  // the pointers using vc_DeleteExpr. By setting EXPRDELETE to 0
543  // we restore the old behaviour.
544  vc_setInterfaceFlags(vc, EXPRDELETE, 0);
545 
546  vc_registerErrorHandler(::stp_error_handler);
547 
548  if (useForkedSTP) {
549  shared_memory_id = shmget(IPC_PRIVATE, shared_memory_size, IPC_CREAT | 0700);
550  assert(shared_memory_id>=0 && "shmget failed");
551  shared_memory_ptr = (unsigned char*) shmat(shared_memory_id, NULL, 0);
552  assert(shared_memory_ptr!=(void*)-1 && "shmat failed");
553  shmctl(shared_memory_id, IPC_RMID, NULL);
554  }
555 }
556 
558  delete builder;
559 
560  vc_Destroy(vc);
561 }
562 
563 /***/
564 
565 STPSolver::STPSolver(bool useForkedSTP, bool optimizeDivides)
566  : Solver(new STPSolverImpl(useForkedSTP, optimizeDivides))
567 {
568 }
569 
570 char *STPSolver::getConstraintLog(const Query &query) {
571  return impl->getConstraintLog(query);
572 }
573 
574 void STPSolver::setCoreSolverTimeout(double timeout) {
575  impl->setCoreSolverTimeout(timeout);
576 }
577 
578 /***/
579 
581  vc_push(vc);
582  for (std::vector< ref<Expr> >::const_iterator it = query.constraints.begin(),
583  ie = query.constraints.end(); it != ie; ++it)
584  vc_assertFormula(vc, builder->construct(*it));
585  assert(query.expr == ConstantExpr::alloc(0, Expr::Bool) &&
586  "Unexpected expression in query!");
587 
588  char *buffer;
589  unsigned long length;
590  vc_printQueryStateToBuffer(vc, builder->getFalse(),
591  &buffer, &length, false);
592  vc_pop(vc);
593 
594  return buffer;
595 }
596 
598  bool &isValid) {
599  std::vector<const Array*> objects;
600  std::vector< std::vector<unsigned char> > values;
601  bool hasSolution;
602 
603  if (!computeInitialValues(query, objects, values, hasSolution))
604  return false;
605 
606  isValid = !hasSolution;
607  return true;
608 }
609 
611  ref<Expr> &result) {
612  std::vector<const Array*> objects;
613  std::vector< std::vector<unsigned char> > values;
614  bool hasSolution;
615 
616  // Find the object used in the expression, and compute an assignment
617  // for them.
618  findSymbolicObjects(query.expr, objects);
619  if (!computeInitialValues(query.withFalse(), objects, values, hasSolution))
620  return false;
621  assert(hasSolution && "state has invalid constraint set");
622 
623  // Evaluate the expression with the computed assignment.
624  Assignment a(objects, values);
625  result = a.evaluate(query.expr);
626 
627  return true;
628 }
629 
630 static SolverImpl::SolverRunStatus runAndGetCex(::VC vc, STPBuilder *builder, ::VCExpr q,
631  const std::vector<const Array*> &objects,
632  std::vector< std::vector<unsigned char> > &values,
633  bool &hasSolution) {
634  // XXX I want to be able to timeout here, safely
635  hasSolution = !vc_query(vc, q);
636 
637  if (hasSolution) {
638  values.reserve(objects.size());
639  for (std::vector<const Array*>::const_iterator
640  it = objects.begin(), ie = objects.end(); it != ie; ++it) {
641  const Array *array = *it;
642  std::vector<unsigned char> data;
643 
644  data.reserve(array->size);
645  for (unsigned offset = 0; offset < array->size; offset++) {
646  ExprHandle counter =
647  vc_getCounterExample(vc, builder->getInitialRead(array, offset));
648  unsigned char val = getBVUnsigned(counter);
649  data.push_back(val);
650  }
651 
652  values.push_back(data);
653  }
654  }
655 
656  if (true == hasSolution) {
658  }
659  else {
661  }
662 }
663 
664 static void stpTimeoutHandler(int x) {
665  _exit(52);
666 }
667 
669  STPBuilder *builder,
670  ::VCExpr q,
671  const std::vector<const Array*> &objects,
672  std::vector< std::vector<unsigned char> >
673  &values,
674  bool &hasSolution,
675  double timeout) {
676  unsigned char *pos = shared_memory_ptr;
677  unsigned sum = 0;
678  for (std::vector<const Array*>::const_iterator
679  it = objects.begin(), ie = objects.end(); it != ie; ++it)
680  sum += (*it)->size;
681  assert(sum<shared_memory_size && "not enough shared memory for counterexample");
682 
683  fflush(stdout);
684  fflush(stderr);
685  int pid = fork();
686  if (pid==-1) {
687  fprintf(stderr, "ERROR: fork failed (for STP)");
688  if (!IgnoreSolverFailures)
689  exit(1);
691  }
692 
693  if (pid == 0) {
694  if (timeout) {
695  ::alarm(0); /* Turn off alarm so we can safely set signal handler */
696  ::signal(SIGALRM, stpTimeoutHandler);
697  ::alarm(std::max(1, (int)timeout));
698  }
699  unsigned res = vc_query(vc, q);
700  if (!res) {
701  for (std::vector<const Array*>::const_iterator
702  it = objects.begin(), ie = objects.end(); it != ie; ++it) {
703  const Array *array = *it;
704  for (unsigned offset = 0; offset < array->size; offset++) {
705  ExprHandle counter =
706  vc_getCounterExample(vc, builder->getInitialRead(array, offset));
707  *pos++ = getBVUnsigned(counter);
708  }
709  }
710  }
711  _exit(res);
712  } else {
713  int status;
714  pid_t res;
715 
716  do {
717  res = waitpid(pid, &status, 0);
718  } while (res < 0 && errno == EINTR);
719 
720  if (res < 0) {
721  fprintf(stderr, "ERROR: waitpid() for STP failed");
722  if (!IgnoreSolverFailures)
723  exit(1);
725  }
726 
727  // From timed_run.py: It appears that linux at least will on
728  // "occasion" return a status when the process was terminated by a
729  // signal, so test signal first.
730  if (WIFSIGNALED(status) || !WIFEXITED(status)) {
731  fprintf(stderr, "ERROR: STP did not return successfully. Most likely you forgot to run 'ulimit -s unlimited'\n");
732  if (!IgnoreSolverFailures) {
733  exit(1);
734  }
736  }
737 
738  int exitcode = WEXITSTATUS(status);
739  if (exitcode==0) {
740  hasSolution = true;
741  } else if (exitcode==1) {
742  hasSolution = false;
743  } else if (exitcode==52) {
744  fprintf(stderr, "error: STP timed out");
745  // mark that a timeout occurred
747  } else {
748  fprintf(stderr, "error: STP did not return a recognized code");
749  if (!IgnoreSolverFailures)
750  exit(1);
752  }
753 
754  if (hasSolution) {
755  values = std::vector< std::vector<unsigned char> >(objects.size());
756  unsigned i=0;
757  for (std::vector<const Array*>::const_iterator
758  it = objects.begin(), ie = objects.end(); it != ie; ++it) {
759  const Array *array = *it;
760  std::vector<unsigned char> &data = values[i++];
761  data.insert(data.begin(), pos, pos + array->size);
762  pos += array->size;
763  }
764  }
765 
766  if (true == hasSolution) {
768  }
769  else {
771  }
772  }
773 }
774 bool
776  const std::vector<const Array*>
777  &objects,
778  std::vector< std::vector<unsigned char> >
779  &values,
780  bool &hasSolution) {
781  runStatusCode = SOLVER_RUN_STATUS_FAILURE;
782 
784 
785  vc_push(vc);
786 
788  ie = query.constraints.end(); it != ie; ++it)
789  vc_assertFormula(vc, builder->construct(*it));
790 
791  ++stats::queries;
793 
794  ExprHandle stp_e = builder->construct(query.expr);
795 
796  if (0) {
797  char *buf;
798  unsigned long len;
799  vc_printQueryStateToBuffer(vc, stp_e, &buf, &len, false);
800  fprintf(stderr, "note: STP query: %.*s\n", (unsigned) len, buf);
801  }
802 
803  bool success;
804  if (useForkedSTP) {
805  runStatusCode = runAndGetCexForked(vc, builder, stp_e, objects, values,
806  hasSolution, timeout);
807  success = ((SOLVER_RUN_STATUS_SUCCESS_SOLVABLE == runStatusCode) ||
808  (SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE == runStatusCode));
809  } else {
810  runStatusCode = runAndGetCex(vc, builder, stp_e, objects, values, hasSolution);
811  success = true;
812  }
813 
814  if (success) {
815  if (hasSolution)
817  else
819  }
820 
821  vc_pop(vc);
822 
823  return success;
824 }
825 
827  return runStatusCode;
828 }
829 
830 #ifdef SUPPORT_METASMT
831 
832 // ------------------------------------- MetaSMTSolverImpl class declaration ------------------------------
833 
834 template<typename SolverContext>
835 class MetaSMTSolverImpl : public SolverImpl {
836 private:
837 
838  SolverContext _meta_solver;
839  MetaSMTSolver<SolverContext> *_solver;
840  MetaSMTBuilder<SolverContext> *_builder;
841  double _timeout;
842  bool _useForked;
843  SolverRunStatus _runStatusCode;
844 
845 public:
846  MetaSMTSolverImpl(MetaSMTSolver<SolverContext> *solver, bool useForked, bool optimizeDivides);
847  virtual ~MetaSMTSolverImpl();
848 
849  char *getConstraintLog(const Query&);
850  void setCoreSolverTimeout(double timeout) { _timeout = timeout; }
851 
852  bool computeTruth(const Query&, bool &isValid);
853  bool computeValue(const Query&, ref<Expr> &result);
854 
855  bool computeInitialValues(const Query &query,
856  const std::vector<const Array*> &objects,
857  std::vector< std::vector<unsigned char> > &values,
858  bool &hasSolution);
859 
861  const std::vector<const Array*> &objects,
862  std::vector< std::vector<unsigned char> > &values,
863  bool &hasSolution);
864 
866  const std::vector<const Array*> &objects,
867  std::vector< std::vector<unsigned char> > &values,
868  bool &hasSolution,
869  double timeout);
870 
871  SolverRunStatus getOperationStatusCode();
872 
873  SolverContext& get_meta_solver() { return(_meta_solver); };
874 
875 };
876 
877 
878 // ------------------------------------- MetaSMTSolver methods --------------------------------------------
879 
880 
881 template<typename SolverContext>
882 MetaSMTSolver<SolverContext>::MetaSMTSolver(bool useForked, bool optimizeDivides)
883  : Solver(new MetaSMTSolverImpl<SolverContext>(this, useForked, optimizeDivides))
884 {
885 
886 }
887 
888 template<typename SolverContext>
889 MetaSMTSolver<SolverContext>::~MetaSMTSolver()
890 {
891 
892 }
893 
894 template<typename SolverContext>
895 char *MetaSMTSolver<SolverContext>::getConstraintLog(const Query& query) {
896  return(impl->getConstraintLog(query));
897 }
898 
899 template<typename SolverContext>
900 void MetaSMTSolver<SolverContext>::setCoreSolverTimeout(double timeout) {
901  impl->setCoreSolverTimeout(timeout);
902 }
903 
904 
905 // ------------------------------------- MetaSMTSolverImpl methods ----------------------------------------
906 
907 
908 
909 template<typename SolverContext>
910 MetaSMTSolverImpl<SolverContext>::MetaSMTSolverImpl(MetaSMTSolver<SolverContext> *solver, bool useForked, bool optimizeDivides)
911  : _solver(solver),
912  _builder(new MetaSMTBuilder<SolverContext>(_meta_solver, optimizeDivides)),
913  _timeout(0.0),
914  _useForked(useForked)
915 {
916  assert(_solver && "unable to create MetaSMTSolver");
917  assert(_builder && "unable to create MetaSMTBuilder");
918 
919  if (_useForked) {
920  shared_memory_id = shmget(IPC_PRIVATE, shared_memory_size, IPC_CREAT | 0700);
921  assert(shared_memory_id >= 0 && "shmget failed");
922  shared_memory_ptr = (unsigned char*) shmat(shared_memory_id, NULL, 0);
923  assert(shared_memory_ptr != (void*) -1 && "shmat failed");
924  shmctl(shared_memory_id, IPC_RMID, NULL);
925  }
926 }
927 
928 template<typename SolverContext>
929 MetaSMTSolverImpl<SolverContext>::~MetaSMTSolverImpl() {
930 
931 }
932 
933 template<typename SolverContext>
934 char *MetaSMTSolverImpl<SolverContext>::getConstraintLog(const Query&) {
935  const char* msg = "Not supported";
936  char *buf = new char[strlen(msg) + 1];
937  strcpy(buf, msg);
938  return(buf);
939 }
940 
941 template<typename SolverContext>
942 bool MetaSMTSolverImpl<SolverContext>::computeTruth(const Query& query, bool &isValid) {
943 
944  bool success = false;
945  std::vector<const Array*> objects;
946  std::vector< std::vector<unsigned char> > values;
947  bool hasSolution;
948 
949  if (computeInitialValues(query, objects, values, hasSolution)) {
950  // query.expr is valid iff !query.expr is not satisfiable
951  isValid = !hasSolution;
952  success = true;
953  }
954 
955  return(success);
956 }
957 
958 template<typename SolverContext>
959 bool MetaSMTSolverImpl<SolverContext>::computeValue(const Query& query, ref<Expr> &result) {
960 
961  bool success = false;
962  std::vector<const Array*> objects;
963  std::vector< std::vector<unsigned char> > values;
964  bool hasSolution;
965 
966  // Find the object used in the expression, and compute an assignment for them.
967  findSymbolicObjects(query.expr, objects);
968  if (computeInitialValues(query.withFalse(), objects, values, hasSolution)) {
969  assert(hasSolution && "state has invalid constraint set");
970  // Evaluate the expression with the computed assignment.
971  Assignment a(objects, values);
972  result = a.evaluate(query.expr);
973  success = true;
974  }
975 
976  return(success);
977 }
978 
979 
980 template<typename SolverContext>
981 bool MetaSMTSolverImpl<SolverContext>::computeInitialValues(const Query &query,
982  const std::vector<const Array*> &objects,
983  std::vector< std::vector<unsigned char> > &values,
984  bool &hasSolution) {
985 
986  _runStatusCode = SOLVER_RUN_STATUS_FAILURE;
987 
989  assert(_builder);
990 
991  /*
992  * FIXME push() and pop() work for Z3 but not for Boolector.
993  * If using Z3, use push() and pop() and assert constraints.
994  * If using Boolector, assume constrainsts instead of asserting them.
995  */
996  //push(_meta_solver);
997 
998  if (!_useForked) {
999  for (ConstraintManager::const_iterator it = query.constraints.begin(), ie = query.constraints.end(); it != ie; ++it) {
1000  //assertion(_meta_solver, _builder->construct(*it));
1001  assumption(_meta_solver, _builder->construct(*it));
1002  }
1003  }
1004 
1005  ++stats::queries;
1007 
1008  bool success = true;
1009  if (_useForked) {
1010  _runStatusCode = runAndGetCexForked(query, objects, values, hasSolution, _timeout);
1011  success = ((SOLVER_RUN_STATUS_SUCCESS_SOLVABLE == _runStatusCode) || (SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE == _runStatusCode));
1012  }
1013  else {
1014  _runStatusCode = runAndGetCex(query.expr, objects, values, hasSolution);
1015  success = true;
1016  }
1017 
1018  if (success) {
1019  if (hasSolution) {
1021  }
1022  else {
1024  }
1025  }
1026 
1027  //pop(_meta_solver);
1028 
1029  return(success);
1030 }
1031 
1032 template<typename SolverContext>
1034  const std::vector<const Array*> &objects,
1035  std::vector< std::vector<unsigned char> > &values,
1036  bool &hasSolution)
1037 {
1038 
1039  // assume the negation of the query
1040  assumption(_meta_solver, _builder->construct(Expr::createIsZero(query_expr)));
1041  hasSolution = solve(_meta_solver);
1042 
1043  if (hasSolution) {
1044  values.reserve(objects.size());
1045  for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) {
1046 
1047  const Array *array = *it;
1048  assert(array);
1049  typename SolverContext::result_type array_exp = _builder->getInitialArray(array);
1050 
1051  std::vector<unsigned char> data;
1052  data.reserve(array->size);
1053 
1054  for (unsigned offset = 0; offset < array->size; offset++) {
1055  typename SolverContext::result_type elem_exp = evaluate(
1056  _meta_solver,
1057  metaSMT::logic::Array::select(array_exp, bvuint(offset, array->getDomain())));
1058  unsigned char elem_value = metaSMT::read_value(_meta_solver, elem_exp);
1059  data.push_back(elem_value);
1060  }
1061 
1062  values.push_back(data);
1063  }
1064  }
1065 
1066  if (true == hasSolution) {
1067  return(SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE);
1068  }
1069  else {
1070  return(SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE);
1071  }
1072 }
1073 
1074 static void metaSMTTimeoutHandler(int x) {
1075  _exit(52);
1076 }
1077 
1078 template<typename SolverContext>
1080  const std::vector<const Array*> &objects,
1081  std::vector< std::vector<unsigned char> > &values,
1082  bool &hasSolution,
1083  double timeout)
1084 {
1085  unsigned char *pos = shared_memory_ptr;
1086  unsigned sum = 0;
1087  for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) {
1088  sum += (*it)->size;
1089  }
1090  // sum += sizeof(uint64_t);
1091  sum += sizeof(stats::queryConstructs);
1092  assert(sum < shared_memory_size && "not enough shared memory for counterexample");
1093 
1094  fflush(stdout);
1095  fflush(stderr);
1096  int pid = fork();
1097  if (pid == -1) {
1098  fprintf(stderr, "error: fork failed (for metaSMT)");
1099  return(SolverImpl::SOLVER_RUN_STATUS_FORK_FAILED);
1100  }
1101 
1102  if (pid == 0) {
1103  if (timeout) {
1104  ::alarm(0); /* Turn off alarm so we can safely set signal handler */
1105  ::signal(SIGALRM, metaSMTTimeoutHandler);
1106  ::alarm(std::max(1, (int) timeout));
1107  }
1108 
1109  for (ConstraintManager::const_iterator it = query.constraints.begin(), ie = query.constraints.end(); it != ie; ++it) {
1110  assertion(_meta_solver, _builder->construct(*it));
1111  //assumption(_meta_solver, _builder->construct(*it));
1112  }
1113 
1114 
1115  std::vector< std::vector<typename SolverContext::result_type> > aux_arr_exprs;
1116  if (UseMetaSMT == METASMT_BACKEND_BOOLECTOR) {
1117  for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) {
1118 
1119  std::vector<typename SolverContext::result_type> aux_arr;
1120  const Array *array = *it;
1121  assert(array);
1122  typename SolverContext::result_type array_exp = _builder->getInitialArray(array);
1123 
1124  for (unsigned offset = 0; offset < array->size; offset++) {
1125  typename SolverContext::result_type elem_exp = evaluate(
1126  _meta_solver,
1127  metaSMT::logic::Array::select(array_exp, bvuint(offset, array->getDomain())));
1128  aux_arr.push_back(elem_exp);
1129  }
1130  aux_arr_exprs.push_back(aux_arr);
1131  }
1132  assert(aux_arr_exprs.size() == objects.size());
1133  }
1134 
1135 
1136  // assume the negation of the query
1137  // can be also asserted instead of assumed as we are in a child process
1138  assumption(_meta_solver, _builder->construct(Expr::createIsZero(query.expr)));
1139  unsigned res = solve(_meta_solver);
1140 
1141  if (res) {
1142 
1143  if (UseMetaSMT != METASMT_BACKEND_BOOLECTOR) {
1144 
1145  for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) {
1146 
1147  const Array *array = *it;
1148  assert(array);
1149  typename SolverContext::result_type array_exp = _builder->getInitialArray(array);
1150 
1151  for (unsigned offset = 0; offset < array->size; offset++) {
1152 
1153  typename SolverContext::result_type elem_exp = evaluate(
1154  _meta_solver,
1155  metaSMT::logic::Array::select(array_exp, bvuint(offset, array->getDomain())));
1156  unsigned char elem_value = metaSMT::read_value(_meta_solver, elem_exp);
1157  *pos++ = elem_value;
1158  }
1159  }
1160  }
1161  else {
1162  typename std::vector< std::vector<typename SolverContext::result_type> >::const_iterator eit = aux_arr_exprs.begin(), eie = aux_arr_exprs.end();
1163  for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie, eit != eie; ++it, ++eit) {
1164  const Array *array = *it;
1165  const std::vector<typename SolverContext::result_type>& arr_exp = *eit;
1166  assert(array);
1167  assert(array->size == arr_exp.size());
1168 
1169  for (unsigned offset = 0; offset < array->size; offset++) {
1170  unsigned char elem_value = metaSMT::read_value(_meta_solver, arr_exp[offset]);
1171  *pos++ = elem_value;
1172  }
1173  }
1174  }
1175  }
1176  assert((uint64_t*) pos);
1177  *((uint64_t*) pos) = stats::queryConstructs;
1178 
1179  _exit(!res);
1180  }
1181  else {
1182  int status;
1183  pid_t res;
1184 
1185  do {
1186  res = waitpid(pid, &status, 0);
1187  }
1188  while (res < 0 && errno == EINTR);
1189 
1190  if (res < 0) {
1191  fprintf(stderr, "error: waitpid() for metaSMT failed");
1192  return(SolverImpl::SOLVER_RUN_STATUS_WAITPID_FAILED);
1193  }
1194 
1195  // From timed_run.py: It appears that linux at least will on
1196  // "occasion" return a status when the process was terminated by a
1197  // signal, so test signal first.
1198  if (WIFSIGNALED(status) || !WIFEXITED(status)) {
1199  fprintf(stderr, "error: metaSMT did not return successfully (status = %d) \n", WTERMSIG(status));
1200  return(SolverImpl::SOLVER_RUN_STATUS_INTERRUPTED);
1201  }
1202 
1203  int exitcode = WEXITSTATUS(status);
1204  if (exitcode == 0) {
1205  hasSolution = true;
1206  }
1207  else if (exitcode == 1) {
1208  hasSolution = false;
1209  }
1210  else if (exitcode == 52) {
1211  fprintf(stderr, "error: metaSMT timed out");
1212  return(SolverImpl::SOLVER_RUN_STATUS_TIMEOUT);
1213  }
1214  else {
1215  fprintf(stderr, "error: metaSMT did not return a recognized code");
1216  return(SolverImpl::SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE);
1217  }
1218 
1219  if (hasSolution) {
1220  values = std::vector< std::vector<unsigned char> >(objects.size());
1221  unsigned i = 0;
1222  for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) {
1223  const Array *array = *it;
1224  assert(array);
1225  std::vector<unsigned char> &data = values[i++];
1226  data.insert(data.begin(), pos, pos + array->size);
1227  pos += array->size;
1228  }
1229  }
1230  stats::queryConstructs += (*((uint64_t*) pos) - stats::queryConstructs);
1231 
1232  if (true == hasSolution) {
1233  return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE;
1234  }
1235  else {
1236  return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE;
1237  }
1238  }
1239 }
1240 
1241 template<typename SolverContext>
1242 SolverImpl::SolverRunStatus MetaSMTSolverImpl<SolverContext>::getOperationStatusCode() {
1243  return _runStatusCode;
1244 }
1245 
1246 template class MetaSMTSolver< DirectSolver_Context < Boolector> >;
1247 template class MetaSMTSolver< DirectSolver_Context < Z3_Backend> >;
1248 template class MetaSMTSolver< DirectSolver_Context < STP_Backend> >;
1249 
1250 #endif /* SUPPORT_METASMT */
1251 
bool computeValue(const Query &, ref< Expr > &result)
Definition: Solver.cpp:470
bool computeTruth(const Query &, bool &isValid)
Definition: Solver.cpp:465
virtual ~Solver()
Definition: Solver.cpp:120
char * getConstraintLog(const Query &)
Definition: Solver.cpp:580
static const char * validity_to_str(Validity v)
validity_to_str - Return the name of given Validity enum value.
Definition: Solver.cpp:112
bool getValue(const Query &, ref< ConstantExpr > &result)
Definition: Solver.cpp:176
uint64_t maxValueOfNBits(unsigned N)
Definition: Bits.h:64
constraint_iterator end() const
Definition: Constraints.h:57
bool computeTruth(const Query &, bool &isValid)
Definition: Solver.cpp:597
bool evaluate(const Query &, Validity &result)
Definition: Solver.cpp:132
SolverImpl - Abstract base clase for solver implementations.
Definition: SolverImpl.h:22
double timeout
Definition: Solver.cpp:499
bool computeInitialValues(const Query &, const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &values, bool &hasSolution)
Definition: Solver.cpp:775
unsigned size
Definition: Expr.h:605
static ref< Expr > create(const UpdateList &updates, ref< Expr > i)
Definition: Expr.cpp:499
ref< Expr > expr
Definition: Solver.h:25
Statistic queriesValid
SolverRunStatus runStatusCode
Definition: Solver.cpp:501
ref< Expr > evaluate(const Array *mo, unsigned index) const
Definition: Assignment.h:68
Query withFalse() const
withFalse - Return a copy of the query with a false expression.
Definition: Solver.h:37
static SolverImpl::SolverRunStatus runAndGetCex(::VC vc, STPBuilder *builder,::VCExpr q, const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &values, bool &hasSolution)
Definition: Solver.cpp:630
constraints_ty::const_iterator const_iterator
Definition: Constraints.h:27
Class representing a complete list of updates into an array.
Definition: Expr.h:655
bool computeTruth(const Query &, bool &isValid)
Definition: Solver.cpp:342
bool computeValue(const Query &, ref< Expr > &result)
Definition: Solver.cpp:372
Statistic queries
STPBuilder * builder
Definition: Solver.cpp:498
bool mustBeTrue(const Query &, bool &result)
Definition: Solver.cpp:144
virtual ~SolverImpl()
Definition: Solver.cpp:70
static const unsigned shared_memory_size
Definition: Solver.cpp:520
virtual Width getWidth() const =0
bool computeInitialValues(const Query &, const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &values, bool &hasSolution)
Definition: Solver.cpp:392
virtual void setCoreSolverTimeout(double timeout)
Definition: SolverImpl.h:106
static SolverImpl::SolverRunStatus runAndGetCexForked(::VC vc, STPBuilder *builder,::VCExpr q, const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &values, bool &hasSolution, double timeout)
Definition: Solver.cpp:668
void setCoreSolverTimeout(double _timeout)
Definition: Solver.cpp:508
Query negateExpr() const
negateExpr - Return a copy of the query with the expression negated.
Definition: Solver.h:42
bool mustBeFalse(const Query &, bool &result)
Definition: Solver.cpp:156
virtual char * getConstraintLog(const Query &)
Definition: Solver.cpp:570
virtual bool computeValidity(const Query &query, Solver::Validity &result)
Definition: Solver.cpp:73
STPSolverImpl(bool _useForkedSTP, bool _optimizeDivides=true)
Definition: Solver.cpp:528
bool computeValidity(const Query &, Solver::Validity &result)
Definition: Solver.cpp:357
bool mayBeTrue(const Query &, bool &result)
Definition: Solver.cpp:160
static ref< Expr > createIsZero(ref< Expr > e)
Definition: Expr.cpp:305
const ConstraintManager & constraints
Definition: Solver.h:24
Query withExpr(ref< Expr > _expr) const
withExpr - Return a copy of the query with the given expression.
Definition: Solver.h:32
SolverRunStatus getOperationStatusCode()
getOperationStatusCode - get the status of the last solver operation
Definition: Solver.cpp:438
bool mayBeFalse(const Query &, bool &result)
Definition: Solver.cpp:168
static unsigned char * shared_memory_ptr
Definition: Solver.cpp:519
bool computeValidity(const Query &, Solver::Validity &result)
Definition: Solver.cpp:460
constraint_iterator begin() const
Definition: Constraints.h:54
SolverRunStatus getOperationStatusCode()
getOperationStatusCode - get the status of the last solver operation
Definition: Solver.cpp:483
llvm::cl::opt< bool > IgnoreSolverFailures("ignore-solver-failures", llvm::cl::init(false), llvm::cl::desc("Ignore any solver failures (default=off)"))
virtual char * getConstraintLog(const Query &query)
Definition: Solver.cpp:124
static ref< ConstantExpr > create(uint64_t v, Width w)
Definition: Expr.h:412
SolverImpl * impl
Definition: Solver.h:64
bool useForkedSTP
Definition: Solver.cpp:500
void setCoreSolverTimeout(double timeout)
Definition: Solver.cpp:446
virtual void setCoreSolverTimeout(double timeout)
Definition: Solver.cpp:574
unsigned Width
The type of an expression is simply its width, in bits.
Definition: Expr.h:94
static ref< ConstantExpr > alloc(const llvm::APInt &v)
Definition: Expr.h:398
static int shared_memory_id
Definition: Solver.cpp:521
virtual void setCoreSolverTimeout(double timeout)
Definition: Solver.cpp:128
Expr::Width getRange() const
Definition: Expr.h:645
void findSymbolicObjects(ref< Expr > e, std::vector< const Array * > &results)
Definition: ExprUtil.cpp:118
Expr::Width getDomain() const
Definition: Expr.h:644
bool getInitialValues(const Query &, const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &result)
Definition: Solver.cpp:193
Solver * createValidatingSolver(Solver *s, Solver *oracle)
Definition: Solver.cpp:450
char * getConstraintLog(const Query &)
Definition: Solver.cpp:442
ExprHandle getInitialRead(const Array *os, unsigned index)
Definition: STPBuilder.cpp:462
SolverRunStatus getOperationStatusCode()
getOperationStatusCode - get the status of the last solver operation
Definition: Solver.cpp:826
Statistic queryCounterexamples
static const Width Bool
Definition: Expr.h:97
bool computeInitialValues(const Query &, const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &values, bool &hasSolution)
Definition: Solver.cpp:475
Solver * solver
Definition: Solver.cpp:323
ValidatingSolver(Solver *_solver, Solver *_oracle)
Definition: Solver.cpp:326
static void stp_error_handler(const char *err_msg)
Definition: Solver.cpp:523
Statistic queryTime
Solver * createDummySolver()
Definition: Solver.cpp:489
virtual char * getConstraintLog(const Query &query)
Definition: SolverImpl.h:101
virtual std::pair< ref< Expr >, ref< Expr > > getRange(const Query &)
Definition: Solver.cpp:206
Statistic queriesInvalid
static void stpTimeoutHandler(int x)
Definition: Solver.cpp:664
bool computeValue(const Query &, ref< Expr > &result)
Definition: Solver.cpp:610
static const char * getOperationStatusString(SolverRunStatus statusCode)
Definition: Solver.cpp:87
Statistic queryConstructs