klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
FastCexSolver.cpp
Go to the documentation of this file.
1 //===-- FastCexSolver.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 
12 #include "klee/Constraints.h"
13 #include "klee/Expr.h"
14 #include "klee/IncompleteSolver.h"
17 #include "klee/util/ExprVisitor.h"
18 // FIXME: Use APInt.
20 
21 #define DEBUG_TYPE "cex-solver"
22 #include "llvm/Support/Debug.h"
23 #include "llvm/Support/raw_ostream.h"
24 #include <sstream>
25 #include <cassert>
26 #include <map>
27 #include <vector>
28 
29 using namespace klee;
30 
31 /***/
32 
33  // Hacker's Delight, pgs 58-63
34 static uint64_t minOR(uint64_t a, uint64_t b,
35  uint64_t c, uint64_t d) {
36  uint64_t temp, m = ((uint64_t) 1)<<63;
37  while (m) {
38  if (~a & c & m) {
39  temp = (a | m) & -m;
40  if (temp <= b) { a = temp; break; }
41  } else if (a & ~c & m) {
42  temp = (c | m) & -m;
43  if (temp <= d) { c = temp; break; }
44  }
45  m >>= 1;
46  }
47 
48  return a | c;
49 }
50 static uint64_t maxOR(uint64_t a, uint64_t b,
51  uint64_t c, uint64_t d) {
52  uint64_t temp, m = ((uint64_t) 1)<<63;
53 
54  while (m) {
55  if (b & d & m) {
56  temp = (b - m) | (m - 1);
57  if (temp >= a) { b = temp; break; }
58  temp = (d - m) | (m -1);
59  if (temp >= c) { d = temp; break; }
60  }
61  m >>= 1;
62  }
63 
64  return b | d;
65 }
66 static uint64_t minAND(uint64_t a, uint64_t b,
67  uint64_t c, uint64_t d) {
68  uint64_t temp, m = ((uint64_t) 1)<<63;
69  while (m) {
70  if (~a & ~c & m) {
71  temp = (a | m) & -m;
72  if (temp <= b) { a = temp; break; }
73  temp = (c | m) & -m;
74  if (temp <= d) { c = temp; break; }
75  }
76  m >>= 1;
77  }
78 
79  return a & c;
80 }
81 static uint64_t maxAND(uint64_t a, uint64_t b,
82  uint64_t c, uint64_t d) {
83  uint64_t temp, m = ((uint64_t) 1)<<63;
84  while (m) {
85  if (b & ~d & m) {
86  temp = (b & ~m) | (m - 1);
87  if (temp >= a) { b = temp; break; }
88  } else if (~b & d & m) {
89  temp = (d & ~m) | (m - 1);
90  if (temp >= c) { d = temp; break; }
91  }
92  m >>= 1;
93  }
94 
95  return b & d;
96 }
97 
99 
100 class ValueRange {
101 private:
102  uint64_t m_min, m_max;
103 
104 public:
105  ValueRange() : m_min(1),m_max(0) {}
107  // FIXME: Support large widths.
108  m_min = m_max = ce->getLimitedValue();
109  }
110  ValueRange(uint64_t value) : m_min(value), m_max(value) {}
111  ValueRange(uint64_t _min, uint64_t _max) : m_min(_min), m_max(_max) {}
112  ValueRange(const ValueRange &b) : m_min(b.m_min), m_max(b.m_max) {}
113 
114  void print(llvm::raw_ostream &os) const {
115  if (isFixed()) {
116  os << m_min;
117  } else {
118  os << "[" << m_min << "," << m_max << "]";
119  }
120  }
121 
122  bool isEmpty() const {
123  return m_min>m_max;
124  }
125  bool contains(uint64_t value) const {
126  return this->intersects(ValueRange(value));
127  }
128  bool intersects(const ValueRange &b) const {
129  return !this->set_intersection(b).isEmpty();
130  }
131 
132  bool isFullRange(unsigned bits) {
133  return m_min==0 && m_max==bits64::maxValueOfNBits(bits);
134  }
135 
137  return ValueRange(std::max(m_min,b.m_min), std::min(m_max,b.m_max));
138  }
139  ValueRange set_union(const ValueRange &b) const {
140  return ValueRange(std::min(m_min,b.m_min), std::max(m_max,b.m_max));
141  }
143  if (b.isEmpty() || b.m_min > m_max || b.m_max < m_min) { // no intersection
144  return *this;
145  } else if (b.m_min <= m_min && b.m_max >= m_max) { // empty
146  return ValueRange(1,0);
147  } else if (b.m_min <= m_min) { // one range out
148  // cannot overflow because b.m_max < m_max
149  return ValueRange(b.m_max+1, m_max);
150  } else if (b.m_max >= m_max) {
151  // cannot overflow because b.min > m_min
152  return ValueRange(m_min, b.m_min-1);
153  } else {
154  // two ranges, take bottom
155  return ValueRange(m_min, b.m_min-1);
156  }
157  }
158  ValueRange binaryAnd(const ValueRange &b) const {
159  // XXX
160  assert(!isEmpty() && !b.isEmpty() && "XXX");
161  if (isFixed() && b.isFixed()) {
162  return ValueRange(m_min & b.m_min);
163  } else {
164  return ValueRange(minAND(m_min, m_max, b.m_min, b.m_max),
165  maxAND(m_min, m_max, b.m_min, b.m_max));
166  }
167  }
168  ValueRange binaryAnd(uint64_t b) const { return binaryAnd(ValueRange(b)); }
170  // XXX
171  assert(!isEmpty() && !b.isEmpty() && "XXX");
172  if (isFixed() && b.isFixed()) {
173  return ValueRange(m_min | b.m_min);
174  } else {
175  return ValueRange(minOR(m_min, m_max, b.m_min, b.m_max),
176  maxOR(m_min, m_max, b.m_min, b.m_max));
177  }
178  }
179  ValueRange binaryOr(uint64_t b) const { return binaryOr(ValueRange(b)); }
181  if (isFixed() && b.isFixed()) {
182  return ValueRange(m_min ^ b.m_min);
183  } else {
184  uint64_t t = m_max | b.m_max;
185  while (!bits64::isPowerOfTwo(t))
187  return ValueRange(0, (t<<1)-1);
188  }
189  }
190 
191  ValueRange binaryShiftLeft(unsigned bits) const {
192  return ValueRange(m_min<<bits, m_max<<bits);
193  }
194  ValueRange binaryShiftRight(unsigned bits) const {
195  return ValueRange(m_min>>bits, m_max>>bits);
196  }
197 
198  ValueRange concat(const ValueRange &b, unsigned bits) const {
199  return binaryShiftLeft(bits).binaryOr(b);
200  }
201  ValueRange extract(uint64_t lowBit, uint64_t maxBit) const {
202  return binaryShiftRight(lowBit).binaryAnd(bits64::maxValueOfNBits(maxBit-lowBit));
203  }
204 
205  ValueRange add(const ValueRange &b, unsigned width) const {
206  return ValueRange(0, bits64::maxValueOfNBits(width));
207  }
208  ValueRange sub(const ValueRange &b, unsigned width) const {
209  return ValueRange(0, bits64::maxValueOfNBits(width));
210  }
211  ValueRange mul(const ValueRange &b, unsigned width) const {
212  return ValueRange(0, bits64::maxValueOfNBits(width));
213  }
214  ValueRange udiv(const ValueRange &b, unsigned width) const {
215  return ValueRange(0, bits64::maxValueOfNBits(width));
216  }
217  ValueRange sdiv(const ValueRange &b, unsigned width) const {
218  return ValueRange(0, bits64::maxValueOfNBits(width));
219  }
220  ValueRange urem(const ValueRange &b, unsigned width) const {
221  return ValueRange(0, bits64::maxValueOfNBits(width));
222  }
223  ValueRange srem(const ValueRange &b, unsigned width) const {
224  return ValueRange(0, bits64::maxValueOfNBits(width));
225  }
226 
227  // use min() to get value if true (XXX should we add a method to
228  // make code clearer?)
229  bool isFixed() const { return m_min==m_max; }
230 
231  bool operator==(const ValueRange &b) const {
232  return m_min==b.m_min && m_max==b.m_max;
233  }
234  bool operator!=(const ValueRange &b) const { return !(*this==b); }
235 
236  bool mustEqual(const uint64_t b) const { return m_min==m_max && m_min==b; }
237  bool mayEqual(const uint64_t b) const { return m_min<=b && m_max>=b; }
238 
239  bool mustEqual(const ValueRange &b) const {
240  return isFixed() && b.isFixed() && m_min==b.m_min;
241  }
242  bool mayEqual(const ValueRange &b) const { return this->intersects(b); }
243 
244  uint64_t min() const {
245  assert(!isEmpty() && "cannot get minimum of empty range");
246  return m_min;
247  }
248 
249  uint64_t max() const {
250  assert(!isEmpty() && "cannot get maximum of empty range");
251  return m_max;
252  }
253 
254  int64_t minSigned(unsigned bits) const {
255  assert((m_min>>bits)==0 && (m_max>>bits)==0 &&
256  "range is outside given number of bits");
257 
258  // if max allows sign bit to be set then it can be smallest value,
259  // otherwise since the range is not empty, min cannot have a sign
260  // bit
261 
262  uint64_t smallest = ((uint64_t) 1 << (bits-1));
263  if (m_max >= smallest) {
264  return ints::sext(smallest, 64, bits);
265  } else {
266  return m_min;
267  }
268  }
269 
270  int64_t maxSigned(unsigned bits) const {
271  assert((m_min>>bits)==0 && (m_max>>bits)==0 &&
272  "range is outside given number of bits");
273 
274  uint64_t smallest = ((uint64_t) 1 << (bits-1));
275 
276  // if max and min have sign bit then max is max, otherwise if only
277  // max has sign bit then max is largest signed integer, otherwise
278  // max is max
279 
280  if (m_min < smallest && m_max >= smallest) {
281  return smallest - 1;
282  } else {
283  return ints::sext(m_max, 64, bits);
284  }
285  }
286 };
287 
288 inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os,
289  const ValueRange &vr) {
290  vr.print(os);
291  return os;
292 }
293 
294 // XXX waste of space, rather have ByteValueRange
296 
302  std::vector<CexValueData> possibleContents;
303 
308  std::vector<CexValueData> exactContents;
309 
310  CexObjectData(const CexObjectData&); // DO NOT IMPLEMENT
311  void operator=(const CexObjectData&); // DO NOT IMPLEMENT
312 
313 public:
314  CexObjectData(uint64_t size) : possibleContents(size), exactContents(size) {
315  for (uint64_t i = 0; i != size; ++i) {
316  possibleContents[i] = ValueRange(0, 255);
317  exactContents[i] = ValueRange(0, 255);
318  }
319  }
320 
321  const CexValueData getPossibleValues(size_t index) const {
322  return possibleContents[index];
323  }
324  void setPossibleValues(size_t index, CexValueData values) {
325  possibleContents[index] = values;
326  }
327  void setPossibleValue(size_t index, unsigned char value) {
328  possibleContents[index] = CexValueData(value);
329  }
330 
331  const CexValueData getExactValues(size_t index) const {
332  return exactContents[index];
333  }
334  void setExactValues(size_t index, CexValueData values) {
335  exactContents[index] = values;
336  }
337 
339  unsigned char getPossibleValue(size_t index) const {
340  const CexValueData &cvd = possibleContents[index];
341  return cvd.min() + (cvd.max() - cvd.min()) / 2;
342  }
343 };
344 
345 class CexRangeEvaluator : public ExprRangeEvaluator<ValueRange> {
346 public:
347  std::map<const Array*, CexObjectData*> &objects;
348  CexRangeEvaluator(std::map<const Array*, CexObjectData*> &_objects)
349  : objects(_objects) {}
350 
352  // Check for a concrete read of a constant array.
353  if (array.isConstantArray() &&
354  index.isFixed() &&
355  index.min() < array.size)
356  return ValueRange(array.constantValues[index.min()]->getZExtValue(8));
357 
358  return ValueRange(0, 255);
359  }
360 };
361 
363 protected:
364  ref<Expr> getInitialValue(const Array& array, unsigned index) {
365  // If the index is out of range, we cannot assign it a value, since that
366  // value cannot be part of the assignment.
367  if (index >= array.size)
368  return ReadExpr::create(UpdateList(&array, 0),
369  ConstantExpr::alloc(index, array.getDomain()));
370 
371  std::map<const Array*, CexObjectData*>::iterator it = objects.find(&array);
372  return ConstantExpr::alloc((it == objects.end() ? 127 :
373  it->second->getPossibleValue(index)),
374  array.getRange());
375  }
376 
377 public:
378  std::map<const Array*, CexObjectData*> &objects;
379  CexPossibleEvaluator(std::map<const Array*, CexObjectData*> &_objects)
380  : objects(_objects) {}
381 };
382 
384 protected:
385  ref<Expr> getInitialValue(const Array& array, unsigned index) {
386  // If the index is out of range, we cannot assign it a value, since that
387  // value cannot be part of the assignment.
388  if (index >= array.size)
389  return ReadExpr::create(UpdateList(&array, 0),
390  ConstantExpr::alloc(index, array.getDomain()));
391 
392  std::map<const Array*, CexObjectData*>::iterator it = objects.find(&array);
393  if (it == objects.end())
394  return ReadExpr::create(UpdateList(&array, 0),
395  ConstantExpr::alloc(index, array.getDomain()));
396 
397  CexValueData cvd = it->second->getExactValues(index);
398  if (!cvd.isFixed())
399  return ReadExpr::create(UpdateList(&array, 0),
400  ConstantExpr::alloc(index, array.getDomain()));
401 
402  return ConstantExpr::alloc(cvd.min(), array.getRange());
403  }
404 
405 public:
406  std::map<const Array*, CexObjectData*> &objects;
407  CexExactEvaluator(std::map<const Array*, CexObjectData*> &_objects)
408  : objects(_objects) {}
409 };
410 
411 class CexData {
412 public:
413  std::map<const Array*, CexObjectData*> objects;
414 
415  CexData(const CexData&); // DO NOT IMPLEMENT
416  void operator=(const CexData&); // DO NOT IMPLEMENT
417 
418 public:
419  CexData() {}
421  for (std::map<const Array*, CexObjectData*>::iterator it = objects.begin(),
422  ie = objects.end(); it != ie; ++it)
423  delete it->second;
424  }
425 
427  CexObjectData *&Entry = objects[A];
428 
429  if (!Entry)
430  Entry = new CexObjectData(A->size);
431 
432  return *Entry;
433  }
434 
435  void propogatePossibleValue(ref<Expr> e, uint64_t value) {
436  propogatePossibleValues(e, CexValueData(value,value));
437  }
438 
439  void propogateExactValue(ref<Expr> e, uint64_t value) {
440  propogateExactValues(e, CexValueData(value,value));
441  }
442 
444  DEBUG(llvm::errs() << "propogate: " << range << " for\n" << e << "\n";);
445 
446  switch (e->getKind()) {
447  case Expr::Constant:
448  // rather a pity if the constant isn't in the range, but how can
449  // we use this?
450  break;
451 
452  // Special
453 
454  case Expr::NotOptimized: break;
455 
456  case Expr::Read: {
457  ReadExpr *re = cast<ReadExpr>(e);
458  const Array *array = re->updates.root;
459  CexObjectData &cod = getObjectData(array);
460 
461  // FIXME: This is imprecise, we need to look through the existing writes
462  // to see if this is an initial read or not.
463  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(re->index)) {
464  uint64_t index = CE->getZExtValue();
465 
466  if (index < array->size) {
467  // If the range is fixed, just set that; even if it conflicts with the
468  // previous range it should be a better guess.
469  if (range.isFixed()) {
470  cod.setPossibleValue(index, range.min());
471  } else {
472  CexValueData cvd = cod.getPossibleValues(index);
473  CexValueData tmp = cvd.set_intersection(range);
474 
475  if (!tmp.isEmpty())
476  cod.setPossibleValues(index, tmp);
477  }
478  }
479  } else {
480  // XXX fatal("XXX not implemented");
481  }
482  break;
483  }
484 
485  case Expr::Select: {
486  SelectExpr *se = cast<SelectExpr>(e);
487  ValueRange cond = evalRangeForExpr(se->cond);
488  if (cond.isFixed()) {
489  if (cond.min()) {
490  propogatePossibleValues(se->trueExpr, range);
491  } else {
492  propogatePossibleValues(se->falseExpr, range);
493  }
494  } else {
495  // XXX imprecise... we have a choice here. One method is to
496  // simply force both sides into the specified range (since the
497  // condition is indetermined). This may lose in two ways, the
498  // first is that the condition chosen may limit further
499  // restrict the range in each of the children, however this is
500  // less of a problem as the range will be a superset of legal
501  // values. The other is if the condition ends up being forced
502  // by some other constraints, then we needlessly forced one
503  // side into the given range.
504  //
505  // The other method would be to force the condition to one
506  // side and force that side into the given range. This loses
507  // when we force the condition to an unsatisfiable value
508  // (either because the condition cannot be that, or the
509  // resulting range given that condition is not in the required
510  // range).
511  //
512  // Currently we just force both into the range. A hybrid would
513  // be to evaluate the ranges for each of the children... if
514  // one of the ranges happens to already be a subset of the
515  // required range then it may be preferable to force the
516  // condition to that side.
517  propogatePossibleValues(se->trueExpr, range);
518  propogatePossibleValues(se->falseExpr, range);
519  }
520  break;
521  }
522 
523  // XXX imprecise... the problem here is that extracting bits
524  // loses information about what bits are connected across the
525  // bytes. if a value can be 1 or 256 then either the top or
526  // lower byte is 0, but just extraction loses this information
527  // and will allow neither,one,or both to be 1.
528  //
529  // we can protect against this in a limited fashion by writing
530  // the extraction a byte at a time, then checking the evaluated
531  // value, isolating for that range, and continuing.
532  case Expr::Concat: {
533  ConcatExpr *ce = cast<ConcatExpr>(e);
534  Expr::Width LSBWidth = ce->getKid(1)->getWidth();
535  Expr::Width MSBWidth = ce->getKid(1)->getWidth();
536  propogatePossibleValues(ce->getKid(0),
537  range.extract(LSBWidth, LSBWidth + MSBWidth));
538  propogatePossibleValues(ce->getKid(1), range.extract(0, LSBWidth));
539  break;
540  }
541 
542  case Expr::Extract: {
543  // XXX
544  break;
545  }
546 
547  // Casting
548 
549  // Simply intersect the output range with the range of all possible
550  // outputs and then truncate to the desired number of bits.
551 
552  // For ZExt this simplifies to just intersection with the possible input
553  // range.
554  case Expr::ZExt: {
555  CastExpr *ce = cast<CastExpr>(e);
556  unsigned inBits = ce->src->getWidth();
557  ValueRange input =
559  propogatePossibleValues(ce->src, input);
560  break;
561  }
562  // For SExt instead of doing the intersection we just take the output
563  // range minus the impossible values. This is nicer since it is a single
564  // interval.
565  case Expr::SExt: {
566  CastExpr *ce = cast<CastExpr>(e);
567  unsigned inBits = ce->src->getWidth();
568  unsigned outBits = ce->width;
569  ValueRange output =
570  range.set_difference(ValueRange(1<<(inBits-1),
571  (bits64::maxValueOfNBits(outBits) -
572  bits64::maxValueOfNBits(inBits-1)-1)));
574  propogatePossibleValues(ce->src, input);
575  break;
576  }
577 
578  // Binary
579 
580  case Expr::Add: {
581  BinaryExpr *be = cast<BinaryExpr>(e);
582  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(be->left)) {
583  // FIXME: Don't depend on width.
584  if (CE->getWidth() <= 64) {
585  // FIXME: Why do we ever propogate empty ranges? It doesn't make
586  // sense.
587  if (range.isEmpty())
588  break;
589 
590  // C_0 + X \in [MIN, MAX) ==> X \in [MIN - C_0, MAX - C_0)
591  Expr::Width W = CE->getWidth();
592  CexValueData nrange(ConstantExpr::alloc(range.min(), W)->Sub(CE)->getZExtValue(),
593  ConstantExpr::alloc(range.max(), W)->Sub(CE)->getZExtValue());
594  if (!nrange.isEmpty())
595  propogatePossibleValues(be->right, nrange);
596  }
597  }
598  break;
599  }
600 
601  case Expr::And: {
602  BinaryExpr *be = cast<BinaryExpr>(e);
603  if (be->getWidth()==Expr::Bool) {
604  if (range.isFixed()) {
605  ValueRange left = evalRangeForExpr(be->left);
606  ValueRange right = evalRangeForExpr(be->right);
607 
608  if (!range.min()) {
609  if (left.mustEqual(0) || right.mustEqual(0)) {
610  // all is well
611  } else {
612  // XXX heuristic, which order
613 
614  propogatePossibleValue(be->left, 0);
615  left = evalRangeForExpr(be->left);
616 
617  // see if that worked
618  if (!left.mustEqual(1))
619  propogatePossibleValue(be->right, 0);
620  }
621  } else {
622  if (!left.mustEqual(1)) propogatePossibleValue(be->left, 1);
623  if (!right.mustEqual(1)) propogatePossibleValue(be->right, 1);
624  }
625  }
626  } else {
627  // XXX
628  }
629  break;
630  }
631 
632  case Expr::Or: {
633  BinaryExpr *be = cast<BinaryExpr>(e);
634  if (be->getWidth()==Expr::Bool) {
635  if (range.isFixed()) {
636  ValueRange left = evalRangeForExpr(be->left);
637  ValueRange right = evalRangeForExpr(be->right);
638 
639  if (range.min()) {
640  if (left.mustEqual(1) || right.mustEqual(1)) {
641  // all is well
642  } else {
643  // XXX heuristic, which order?
644 
645  // force left to value we need
646  propogatePossibleValue(be->left, 1);
647  left = evalRangeForExpr(be->left);
648 
649  // see if that worked
650  if (!left.mustEqual(1))
651  propogatePossibleValue(be->right, 1);
652  }
653  } else {
654  if (!left.mustEqual(0)) propogatePossibleValue(be->left, 0);
655  if (!right.mustEqual(0)) propogatePossibleValue(be->right, 0);
656  }
657  }
658  } else {
659  // XXX
660  }
661  break;
662  }
663 
664  case Expr::Xor: break;
665 
666  // Comparison
667 
668  case Expr::Eq: {
669  BinaryExpr *be = cast<BinaryExpr>(e);
670  if (range.isFixed()) {
671  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(be->left)) {
672  // FIXME: Handle large widths?
673  if (CE->getWidth() <= 64) {
674  uint64_t value = CE->getZExtValue();
675  if (range.min()) {
676  propogatePossibleValue(be->right, value);
677  } else {
678  CexValueData range;
679  if (value==0) {
680  range = CexValueData(1,
681  bits64::maxValueOfNBits(CE->getWidth()));
682  } else {
683  // FIXME: heuristic / lossy, could be better to pick larger
684  // range?
685  range = CexValueData(0, value - 1);
686  }
687  propogatePossibleValues(be->right, range);
688  }
689  } else {
690  // XXX what now
691  }
692  }
693  }
694  break;
695  }
696 
697  case Expr::Not: {
698  if (e->getWidth() == Expr::Bool && range.isFixed()) {
699  propogatePossibleValue(e->getKid(0), !range.min());
700  }
701  break;
702  }
703 
704  case Expr::Ult: {
705  BinaryExpr *be = cast<BinaryExpr>(e);
706 
707  // XXX heuristic / lossy, what order if conflict
708 
709  if (range.isFixed()) {
710  ValueRange left = evalRangeForExpr(be->left);
711  ValueRange right = evalRangeForExpr(be->right);
712 
713  uint64_t maxValue = bits64::maxValueOfNBits(be->right->getWidth());
714 
715  // XXX should deal with overflow (can lead to empty range)
716 
717  if (left.isFixed()) {
718  if (range.min()) {
719  propogatePossibleValues(be->right, CexValueData(left.min()+1,
720  maxValue));
721  } else {
722  propogatePossibleValues(be->right, CexValueData(0, left.min()));
723  }
724  } else if (right.isFixed()) {
725  if (range.min()) {
726  propogatePossibleValues(be->left, CexValueData(0, right.min()-1));
727  } else {
728  propogatePossibleValues(be->left, CexValueData(right.min(),
729  maxValue));
730  }
731  } else {
732  // XXX ???
733  }
734  }
735  break;
736  }
737  case Expr::Ule: {
738  BinaryExpr *be = cast<BinaryExpr>(e);
739 
740  // XXX heuristic / lossy, what order if conflict
741 
742  if (range.isFixed()) {
743  ValueRange left = evalRangeForExpr(be->left);
744  ValueRange right = evalRangeForExpr(be->right);
745 
746  // XXX should deal with overflow (can lead to empty range)
747 
748  uint64_t maxValue = bits64::maxValueOfNBits(be->right->getWidth());
749  if (left.isFixed()) {
750  if (range.min()) {
751  propogatePossibleValues(be->right, CexValueData(left.min(),
752  maxValue));
753  } else {
754  propogatePossibleValues(be->right, CexValueData(0, left.min()-1));
755  }
756  } else if (right.isFixed()) {
757  if (range.min()) {
758  propogatePossibleValues(be->left, CexValueData(0, right.min()));
759  } else {
760  propogatePossibleValues(be->left, CexValueData(right.min()+1,
761  maxValue));
762  }
763  } else {
764  // XXX ???
765  }
766  }
767  break;
768  }
769 
770  case Expr::Ne:
771  case Expr::Ugt:
772  case Expr::Uge:
773  case Expr::Sgt:
774  case Expr::Sge:
775  assert(0 && "invalid expressions (uncanonicalized");
776 
777  default:
778  break;
779  }
780  }
781 
783  switch (e->getKind()) {
784  case Expr::Constant: {
785  // FIXME: Assert that range contains this constant.
786  break;
787  }
788 
789  // Special
790 
791  case Expr::NotOptimized: break;
792 
793  case Expr::Read: {
794  ReadExpr *re = cast<ReadExpr>(e);
795  const Array *array = re->updates.root;
796  CexObjectData &cod = getObjectData(array);
797  CexValueData index = evalRangeForExpr(re->index);
798 
799  for (const UpdateNode *un = re->updates.head; un; un = un->next) {
800  CexValueData ui = evalRangeForExpr(un->index);
801 
802  // If these indices can't alias, continue propogation
803  if (!ui.mayEqual(index))
804  continue;
805 
806  // Otherwise if we know they alias, propogate into the write value.
807  if (ui.mustEqual(index) || re->index == un->index)
808  propogateExactValues(un->value, range);
809  return;
810  }
811 
812  // We reached the initial array write, update the exact range if possible.
813  if (index.isFixed()) {
814  if (array->isConstantArray()) {
815  // Verify the range.
816  propogateExactValues(array->constantValues[index.min()],
817  range);
818  } else {
819  CexValueData cvd = cod.getExactValues(index.min());
820  if (range.min() > cvd.min()) {
821  assert(range.min() <= cvd.max());
822  cvd = CexValueData(range.min(), cvd.max());
823  }
824  if (range.max() < cvd.max()) {
825  assert(range.max() >= cvd.min());
826  cvd = CexValueData(cvd.min(), range.max());
827  }
828  cod.setExactValues(index.min(), cvd);
829  }
830  }
831  break;
832  }
833 
834  case Expr::Select: {
835  break;
836  }
837 
838  case Expr::Concat: {
839  break;
840  }
841 
842  case Expr::Extract: {
843  break;
844  }
845 
846  // Casting
847 
848  case Expr::ZExt: {
849  break;
850  }
851 
852  case Expr::SExt: {
853  break;
854  }
855 
856  // Binary
857 
858  case Expr::And: {
859  break;
860  }
861 
862  case Expr::Or: {
863  break;
864  }
865 
866  case Expr::Xor: {
867  break;
868  }
869 
870  // Comparison
871 
872  case Expr::Eq: {
873  BinaryExpr *be = cast<BinaryExpr>(e);
874  if (range.isFixed()) {
875  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(be->left)) {
876  // FIXME: Handle large widths?
877  if (CE->getWidth() <= 64) {
878  uint64_t value = CE->getZExtValue();
879  if (range.min()) {
880  // If the equality is true, then propogate the value.
881  propogateExactValue(be->right, value);
882  } else {
883  // If the equality is false and the comparison is of booleans,
884  // then we can infer the value to propogate.
885  if (be->right->getWidth() == Expr::Bool)
886  propogateExactValue(be->right, !value);
887  }
888  }
889  }
890  }
891  break;
892  }
893 
894  // If a boolean not, and the result is known, propagate it
895  case Expr::Not: {
896  if (e->getWidth() == Expr::Bool && range.isFixed()) {
897  propogateExactValue(e->getKid(0), !range.min());
898  }
899  break;
900  }
901 
902  case Expr::Ult: {
903  break;
904  }
905 
906  case Expr::Ule: {
907  break;
908  }
909 
910  case Expr::Ne:
911  case Expr::Ugt:
912  case Expr::Uge:
913  case Expr::Sgt:
914  case Expr::Sge:
915  assert(0 && "invalid expressions (uncanonicalized");
916 
917  default:
918  break;
919  }
920  }
921 
923  CexRangeEvaluator ce(objects);
924  return ce.evaluate(e);
925  }
926 
930  return CexPossibleEvaluator(objects).visit(e);
931  }
932 
934  return CexExactEvaluator(objects).visit(e);
935  }
936 
937  void dump() {
938  llvm::errs() << "-- propogated values --\n";
939  for (std::map<const Array *, CexObjectData *>::iterator
940  it = objects.begin(),
941  ie = objects.end();
942  it != ie; ++it) {
943  const Array *A = it->first;
944  CexObjectData *COD = it->second;
945 
946  llvm::errs() << A->name << "\n";
947  llvm::errs() << "possible: [";
948  for (unsigned i = 0; i < A->size; ++i) {
949  if (i)
950  llvm::errs() << ", ";
951  llvm::errs() << COD->getPossibleValues(i);
952  }
953  llvm::errs() << "]\n";
954  llvm::errs() << "exact : [";
955  for (unsigned i = 0; i < A->size; ++i) {
956  if (i)
957  llvm::errs() << ", ";
958  llvm::errs() << COD->getExactValues(i);
959  }
960  llvm::errs() << "]\n";
961  }
962  }
963 };
964 
965 /* *** */
966 
967 
969 public:
970  FastCexSolver();
971  ~FastCexSolver();
972 
973  IncompleteSolver::PartialValidity computeTruth(const Query&);
974  bool computeValue(const Query&, ref<Expr> &result);
975  bool computeInitialValues(const Query&,
976  const std::vector<const Array*> &objects,
977  std::vector< std::vector<unsigned char> > &values,
978  bool &hasSolution);
979 };
980 
982 
984 
999 static bool propogateValues(const Query& query, CexData &cd,
1000  bool checkExpr, bool &isValid) {
1002  ie = query.constraints.end(); it != ie; ++it) {
1003  cd.propogatePossibleValue(*it, 1);
1004  cd.propogateExactValue(*it, 1);
1005  }
1006  if (checkExpr) {
1007  cd.propogatePossibleValue(query.expr, 0);
1008  cd.propogateExactValue(query.expr, 0);
1009  }
1010 
1011  DEBUG(cd.dump(););
1012 
1013  // Check the result.
1014  bool hasSatisfyingAssignment = true;
1015  if (checkExpr) {
1016  if (!cd.evaluatePossible(query.expr)->isFalse())
1017  hasSatisfyingAssignment = false;
1018 
1019  // If the query is known to be true, then we have proved validity.
1020  if (cd.evaluateExact(query.expr)->isTrue()) {
1021  isValid = true;
1022  return true;
1023  }
1024  }
1025 
1027  ie = query.constraints.end(); it != ie; ++it) {
1028  if (hasSatisfyingAssignment && !cd.evaluatePossible(*it)->isTrue())
1029  hasSatisfyingAssignment = false;
1030 
1031  // If this constraint is known to be false, then we can prove anything, so
1032  // the query is valid.
1033  if (cd.evaluateExact(*it)->isFalse()) {
1034  isValid = true;
1035  return true;
1036  }
1037  }
1038 
1039  if (hasSatisfyingAssignment) {
1040  isValid = false;
1041  return true;
1042  }
1043 
1044  return false;
1045 }
1046 
1049  CexData cd;
1050 
1051  bool isValid;
1052  bool success = propogateValues(query, cd, true, isValid);
1053 
1054  if (!success)
1055  return IncompleteSolver::None;
1056 
1058 }
1059 
1060 bool FastCexSolver::computeValue(const Query& query, ref<Expr> &result) {
1061  CexData cd;
1062 
1063  bool isValid;
1064  bool success = propogateValues(query, cd, false, isValid);
1065 
1066  // Check if propogation wasn't able to determine anything.
1067  if (!success)
1068  return false;
1069 
1070  // FIXME: We don't have a way to communicate valid constraints back.
1071  if (isValid)
1072  return false;
1073 
1074  // Propogation found a satisfying assignment, evaluate the expression.
1075  ref<Expr> value = cd.evaluatePossible(query.expr);
1076 
1077  if (isa<ConstantExpr>(value)) {
1078  // FIXME: We should be able to make sure this never fails?
1079  result = value;
1080  return true;
1081  } else {
1082  return false;
1083  }
1084 }
1085 
1086 bool
1088  const std::vector<const Array*>
1089  &objects,
1090  std::vector< std::vector<unsigned char> >
1091  &values,
1092  bool &hasSolution) {
1093  CexData cd;
1094 
1095  bool isValid;
1096  bool success = propogateValues(query, cd, true, isValid);
1097 
1098  // Check if propogation wasn't able to determine anything.
1099  if (!success)
1100  return false;
1101 
1102  hasSolution = !isValid;
1103  if (!hasSolution)
1104  return true;
1105 
1106  // Propogation found a satisfying assignment, compute the initial values.
1107  for (unsigned i = 0; i != objects.size(); ++i) {
1108  const Array *array = objects[i];
1109  assert(array);
1110  std::vector<unsigned char> data;
1111  data.reserve(array->size);
1112 
1113  for (unsigned i=0; i < array->size; i++) {
1114  ref<Expr> read =
1115  ReadExpr::create(UpdateList(array, 0),
1116  ConstantExpr::create(i, array->getDomain()));
1117  ref<Expr> value = cd.evaluatePossible(read);
1118 
1119  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(value)) {
1120  data.push_back((unsigned char) CE->getZExtValue(8));
1121  } else {
1122  // FIXME: When does this happen?
1123  return false;
1124  }
1125  }
1126 
1127  values.push_back(data);
1128  }
1129 
1130  return true;
1131 }
1132 
1133 
1135  return new Solver(new StagedSolverImpl(new FastCexSolver(), s));
1136 }
ValueRange concat(const ValueRange &b, unsigned bits) const
The validity of the query is unknown.
ValueRange(const ValueRange &b)
void setExactValues(size_t index, CexValueData values)
const CexValueData getPossibleValues(size_t index) const
uint64_t maxValueOfNBits(unsigned N)
Definition: Bits.h:64
constraint_iterator end() const
Definition: Constraints.h:57
ref< Expr > getInitialValue(const Array &array, unsigned index)
void setPossibleValues(size_t index, CexValueData values)
std::vector< CexValueData > exactContents
bool mayEqual(const uint64_t b) const
bool operator!=(const ValueRange &b) const
ref< Expr > left
Definition: Expr.h:494
static uint64_t maxOR(uint64_t a, uint64_t b, uint64_t c, uint64_t d)
ValueRange mul(const ValueRange &b, unsigned width) const
Not used in canonical form.
Definition: Expr.h:151
void propogateExactValues(ref< Expr > e, CexValueData range)
ValueRange evalRangeForExpr(const ref< Expr > &e)
static uint64_t minOR(uint64_t a, uint64_t b, uint64_t c, uint64_t d)
Solver * createFastCexSolver(Solver *s)
ValueRange CexValueData
CexPossibleEvaluator(std::map< const Array *, CexObjectData * > &_objects)
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
ref< Expr > trueExpr
Definition: Expr.h:732
llvm::raw_ostream & operator<<(llvm::raw_ostream &os, const MemoryMap &mm)
void dump()
std::map< const Array *, CexObjectData * > objects
std::vector< ref< Expr > >::iterator A
Definition: ExprUtil.cpp:123
ValueRange set_union(const ValueRange &b) const
bool contains(uint64_t value) const
int64_t maxSigned(unsigned bits) const
const std::vector< ref< ConstantExpr > > constantValues
Definition: Expr.h:610
constraints_ty::const_iterator const_iterator
Definition: Constraints.h:27
Class representing a complete list of updates into an array.
Definition: Expr.h:655
ValueRange set_intersection(const ValueRange &b) const
bool isFullRange(unsigned bits)
UpdateList updates
Definition: Expr.h:687
Not used in canonical form.
Definition: Expr.h:155
uint64_t m_min
Class representing an if-then-else expression.
Definition: Expr.h:726
ValueRange sub(const ValueRange &b, unsigned width) const
ValueRange set_difference(const ValueRange &b) const
Not used in canonical form.
Definition: Expr.h:154
uint64_t getLimitedValue(uint64_t Limit=~0ULL) const
Definition: Expr.h:368
Not used in canonical form.
Definition: Expr.h:158
The query is provably true.
static bool propogateValues(const Query &query, CexData &cd, bool checkExpr, bool &isValid)
ref< Expr > src
Definition: Expr.h:945
ValueRange binaryShiftLeft(unsigned bits) const
ValueRange(const ref< ConstantExpr > &ce)
virtual Width getWidth() const =0
CexExactEvaluator(std::map< const Array *, CexObjectData * > &_objects)
bool mustEqual(const ValueRange &b) const
IncompleteSolver::PartialValidity computeTruth(const Query &)
virtual ref< Expr > getKid(unsigned i) const =0
std::map< const Array *, CexObjectData * > & objects
void propogateExactValue(ref< Expr > e, uint64_t value)
static uint64_t minAND(uint64_t a, uint64_t b, uint64_t c, uint64_t d)
CexRangeEvaluator(std::map< const Array *, CexObjectData * > &_objects)
ValueRange srem(const ValueRange &b, unsigned width) const
bool isFalse() const
isFalse - Is this the false expression.
Definition: Expr.h:1101
const ConstraintManager & constraints
Definition: Solver.h:24
void propogatePossibleValues(ref< Expr > e, CexValueData range)
bool isFixed() const
ValueRange(uint64_t _min, uint64_t _max)
uint64_t max() const
const UpdateNode * head
pointer to the most recent update node
Definition: Expr.h:662
bool mayEqual(const ValueRange &b) const
constraint_iterator begin() const
Definition: Constraints.h:54
ValueRange binaryXor(ValueRange b) const
bool isEmpty() const
ValueRange binaryAnd(const ValueRange &b) const
bool isTrue() const
isTrue - Is this the true expression.
Definition: Expr.h:1094
const std::string name
Definition: Expr.h:603
static ref< ConstantExpr > create(uint64_t v, Width w)
Definition: Expr.h:412
bool computeInitialValues(const Query &, const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &values, bool &hasSolution)
std::map< const Array *, CexObjectData * > & objects
ValueRange urem(const ValueRange &b, unsigned width) const
uint64_t isPowerOfTwo(uint64_t x)
Definition: Bits.h:83
ref< Expr > evaluateExact(ref< Expr > e)
unsigned char getPossibleValue(size_t index) const
getPossibleValue - Return some possible value.
ValueRange getInitialReadRange(const Array &array, ValueRange index)
unsigned Width
The type of an expression is simply its width, in bits.
Definition: Expr.h:94
bool operator==(const ValueRange &b) const
ValueRange binaryShiftRight(unsigned bits) const
bool mustEqual(const uint64_t b) const
static ref< ConstantExpr > alloc(const llvm::APInt &v)
Definition: Expr.h:398
CexObjectData(uint64_t size)
Expr::Width getRange() const
Definition: Expr.h:645
static uint64_t maxAND(uint64_t a, uint64_t b, uint64_t c, uint64_t d)
void print(llvm::raw_ostream &os) const
ValueRange binaryAnd(uint64_t b) const
ref< Expr > right
Definition: Expr.h:494
ValueRange binaryOr(uint64_t b) const
const UpdateNode * next
Definition: Expr.h:577
ref< Expr > getInitialValue(const Array &array, unsigned index)
bool isConstantArray() const
Definition: Expr.h:642
ValueRange binaryOr(ValueRange b) const
Expr::Width getDomain() const
Definition: Expr.h:644
ValueRange(uint64_t value)
uint64_t m_max
const Array * root
Definition: Expr.h:659
uint64_t sext(uint64_t l, unsigned outWidth, unsigned inWidth)
Definition: IntEvaluation.h:50
ValueRange udiv(const ValueRange &b, unsigned width) const
Width width
Definition: Expr.h:946
virtual Kind getKind() const =0
ValueRange add(const ValueRange &b, unsigned width) const
Class representing a one byte read from an array.
Definition: Expr.h:681
static KTest * input
Definition: klee-replay.c:30
T evaluate(const ref< Expr > &e)
ref< Expr > index
Definition: Expr.h:688
Class representing a byte update of an array.
Definition: Expr.h:569
ref< Expr > cond
Definition: Expr.h:732
static const Width Bool
Definition: Expr.h:97
ValueRange sdiv(const ValueRange &b, unsigned width) const
Not used in canonical form.
Definition: Expr.h:159
int64_t minSigned(unsigned bits) const
ref< Expr > evaluatePossible(ref< Expr > e)
bool intersects(const ValueRange &b) const
bool computeValue(const Query &, ref< Expr > &result)
computeValue - Attempt to compute a value for the given expression.
uint64_t min() const
void propogatePossibleValue(ref< Expr > e, uint64_t value)
ValueRange extract(uint64_t lowBit, uint64_t maxBit) const
void setPossibleValue(size_t index, unsigned char value)
ref< Expr > falseExpr
Definition: Expr.h:732
uint64_t withoutRightmostBit(uint64_t x)
Definition: Bits.h:75
const CexValueData getExactValues(size_t index) const
CexObjectData & getObjectData(const Array *A)
std::vector< CexValueData > possibleContents
ref< Expr > getKid(unsigned i) const
Definition: Expr.h:807
std::map< const Array *, CexObjectData * > & objects
ref< Expr > visit(const ref< Expr > &e)
Definition: ExprVisitor.cpp:24