Initial KLEE checkin.

 - Lots more tweaks, documentation, and web page content is needed,
   but this should compile & work on OS X & Linux.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 959 insertions, 0 deletions

diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp
new file mode 100644
index 00000000..d2bc27c6
--- /dev/null
+++ b/lib/Solver/FastCexSolver.cpp
@@ -0,0 +1,959 @@
+//===-- FastCexSolver.cpp -------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "klee/Solver.h"
+
+#include "klee/Constraints.h"
+#include "klee/Expr.h"
+#include "klee/IncompleteSolver.h"
+#include "klee/util/ExprEvaluator.h"
+#include "klee/util/ExprRangeEvaluator.h"
+#include "klee/util/ExprVisitor.h"
+// FIXME: Use APInt.
+#include "klee/Internal/Support/IntEvaluation.h"
+
+#include <iostream>
+#include <sstream>
+#include <cassert>
+#include <map>
+#include <vector>
+
+using namespace klee;
+
+/***/
+
+//#define LOG
+#ifdef LOG
+std::ostream *theLog;
+#endif
+
+      // Hacker's Delight, pgs 58-63
+static uint64_t minOR(uint64_t a, uint64_t b,
+                      uint64_t c, uint64_t d) {
+  uint64_t temp, m = ((uint64_t) 1)<<63;
+  while (m) {
+    if (~a & c & m) {
+      temp = (a | m) & -m;
+      if (temp <= b) { a = temp; break; }
+    } else if (a & ~c & m) {
+      temp = (c | m) & -m;
+      if (temp <= d) { c = temp; break; }
+    }
+    m >>= 1;
+  }
+  
+  return a | c;
+}
+static uint64_t maxOR(uint64_t a, uint64_t b,
+                      uint64_t c, uint64_t d) {
+  uint64_t temp, m = ((uint64_t) 1)<<63;
+
+  while (m) {
+    if (b & d & m) {
+      temp = (b - m) | (m - 1);
+      if (temp >= a) { b = temp; break; }
+      temp = (d - m) | (m -1);
+      if (temp >= c) { d = temp; break; }
+    }
+    m >>= 1;
+  }
+
+  return b | d;
+}
+static uint64_t minAND(uint64_t a, uint64_t b,
+                       uint64_t c, uint64_t d) {
+  uint64_t temp, m = ((uint64_t) 1)<<63;
+  while (m) {
+    if (~a & ~c & m) {
+      temp = (a | m) & -m;
+      if (temp <= b) { a = temp; break; }
+      temp = (c | m) & -m;
+      if (temp <= d) { c = temp; break; }
+    }
+    m >>= 1;
+  }
+  
+  return a & c;
+}
+static uint64_t maxAND(uint64_t a, uint64_t b,
+                       uint64_t c, uint64_t d) {
+  uint64_t temp, m = ((uint64_t) 1)<<63;
+  while (m) {
+    if (b & ~d & m) {
+      temp = (b & ~m) | (m - 1);
+      if (temp >= a) { b = temp; break; }
+    } else if (~b & d & m) {
+      temp = (d & ~m) | (m - 1);
+      if (temp >= c) { d = temp; break; }
+    }
+    m >>= 1;
+  }
+  
+  return b & d;
+}
+
+///
+
+class ValueRange {
+private:
+  uint64_t m_min, m_max;
+
+public:
+  ValueRange() : m_min(1),m_max(0) {}
+  ValueRange(uint64_t value) : m_min(value), m_max(value) {}
+  ValueRange(uint64_t _min, uint64_t _max) : m_min(_min), m_max(_max) {}
+  ValueRange(const ValueRange &b) : m_min(b.m_min), m_max(b.m_max) {}
+
+  void print(std::ostream &os) const {
+    if (isFixed()) {
+      os << m_min;
+    } else {
+      os << "[" << m_min << "," << m_max << "]";
+    }
+  }
+
+  bool isEmpty() const { 
+    return m_min>m_max; 
+  }
+  bool contains(uint64_t value) const { 
+    return this->intersects(ValueRange(value)); 
+  }
+  bool intersects(const ValueRange &b) const { 
+    return !this->set_intersection(b).isEmpty(); 
+  }
+
+  bool isFullRange(unsigned bits) {
+    return m_min==0 && m_max==bits64::maxValueOfNBits(bits);
+  }
+
+  ValueRange set_intersection(const ValueRange &b) const {
+    return ValueRange(std::max(m_min,b.m_min), std::min(m_max,b.m_max));
+  }
+  ValueRange set_union(const ValueRange &b) const {
+    return ValueRange(std::min(m_min,b.m_min), std::max(m_max,b.m_max));
+  }
+  ValueRange set_difference(const ValueRange &b) const {
+    if (b.isEmpty() || b.m_min > m_max || b.m_max < m_min) { // no intersection
+      return *this;
+    } else if (b.m_min <= m_min && b.m_max >= m_max) { // empty
+      return ValueRange(1,0); 
+    } else if (b.m_min <= m_min) { // one range out
+      // cannot overflow because b.m_max < m_max
+      return ValueRange(b.m_max+1, m_max);
+    } else if (b.m_max >= m_max) {
+      // cannot overflow because b.min > m_min
+      return ValueRange(m_min, b.m_min-1);
+    } else {
+      // two ranges, take bottom
+      return ValueRange(m_min, b.m_min-1);
+    }
+  }
+  ValueRange binaryAnd(const ValueRange &b) const {
+    // XXX
+    assert(!isEmpty() && !b.isEmpty() && "XXX");
+    if (isFixed() && b.isFixed()) {
+      return ValueRange(m_min & b.m_min);
+    } else {
+      return ValueRange(minAND(m_min, m_max, b.m_min, b.m_max),
+                        maxAND(m_min, m_max, b.m_min, b.m_max));
+    }
+  }
+  ValueRange binaryAnd(uint64_t b) const { return binaryAnd(ValueRange(b)); }
+  ValueRange binaryOr(ValueRange b) const {
+    // XXX
+    assert(!isEmpty() && !b.isEmpty() && "XXX");
+    if (isFixed() && b.isFixed()) {
+      return ValueRange(m_min | b.m_min);
+    } else {
+      return ValueRange(minOR(m_min, m_max, b.m_min, b.m_max),
+                        maxOR(m_min, m_max, b.m_min, b.m_max));
+    }
+  }
+  ValueRange binaryOr(uint64_t b) const { return binaryOr(ValueRange(b)); }
+  ValueRange binaryXor(ValueRange b) const {
+    if (isFixed() && b.isFixed()) {
+      return ValueRange(m_min ^ b.m_min);
+    } else {
+      uint64_t t = m_max | b.m_max;
+      while (!bits64::isPowerOfTwo(t))
+        t = bits64::withoutRightmostBit(t);
+      return ValueRange(0, (t<<1)-1);
+    }
+  }
+
+  ValueRange binaryShiftLeft(unsigned bits) const {
+    return ValueRange(m_min<<bits, m_max<<bits);
+  }
+  ValueRange binaryShiftRight(unsigned bits) const {
+    return ValueRange(m_min>>bits, m_max>>bits);
+  }
+
+  ValueRange concat(const ValueRange &b, unsigned bits) const {
+    return binaryShiftLeft(bits).binaryOr(b);
+  }
+  ValueRange extract(uint64_t lowBit, uint64_t maxBit) const {
+    return binaryShiftRight(lowBit).binaryAnd(bits64::maxValueOfNBits(maxBit-lowBit));
+  }
+
+  ValueRange add(const ValueRange &b, unsigned width) const {
+    return ValueRange(0, bits64::maxValueOfNBits(width));
+  }
+  ValueRange sub(const ValueRange &b, unsigned width) const {
+    return ValueRange(0, bits64::maxValueOfNBits(width));
+  }
+  ValueRange mul(const ValueRange &b, unsigned width) const {
+    return ValueRange(0, bits64::maxValueOfNBits(width));
+  }
+  ValueRange udiv(const ValueRange &b, unsigned width) const {
+    return ValueRange(0, bits64::maxValueOfNBits(width));
+  }
+  ValueRange sdiv(const ValueRange &b, unsigned width) const {
+    return ValueRange(0, bits64::maxValueOfNBits(width));
+  }
+  ValueRange urem(const ValueRange &b, unsigned width) const {
+    return ValueRange(0, bits64::maxValueOfNBits(width));
+  }
+  ValueRange srem(const ValueRange &b, unsigned width) const {
+    return ValueRange(0, bits64::maxValueOfNBits(width));
+  }
+
+  // use min() to get value if true (XXX should we add a method to
+  // make code clearer?)
+  bool isFixed() const { return m_min==m_max; }
+
+  bool operator==(const ValueRange &b) const { return m_min==b.m_min && m_max==b.m_max; }
+  bool operator!=(const ValueRange &b) const { return !(*this==b); }
+
+  bool mustEqual(const uint64_t b) const { return m_min==m_max && m_min==b; }
+  bool mayEqual(const uint64_t b) const { return m_min<=b && m_max>=b; }
+  
+  bool mustEqual(const ValueRange &b) const { return isFixed() && b.isFixed() && m_min==b.m_min; }
+  bool mayEqual(const ValueRange &b) const { return this->intersects(b); }
+
+  uint64_t min() const { 
+    assert(!isEmpty() && "cannot get minimum of empty range");
+    return m_min; 
+  }
+
+  uint64_t max() const { 
+    assert(!isEmpty() && "cannot get maximum of empty range");
+    return m_max; 
+  }
+  
+  int64_t minSigned(unsigned bits) const {
+    assert((m_min>>bits)==0 && (m_max>>bits)==0 &&
+           "range is outside given number of bits");
+
+    // if max allows sign bit to be set then it can be smallest value,
+    // otherwise since the range is not empty, min cannot have a sign
+    // bit
+
+    uint64_t smallest = ((uint64_t) 1 << (bits-1));
+    if (m_max >= smallest) {
+      return ints::sext(smallest, 64, bits);
+    } else {
+      return m_min;
+    }
+  }
+
+  int64_t maxSigned(unsigned bits) const {
+    assert((m_min>>bits)==0 && (m_max>>bits)==0 &&
+           "range is outside given number of bits");
+
+    uint64_t smallest = ((uint64_t) 1 << (bits-1));
+
+    // if max and min have sign bit then max is max, otherwise if only
+    // max has sign bit then max is largest signed integer, otherwise
+    // max is max
+
+    if (m_min < smallest && m_max >= smallest) {
+      return smallest - 1;
+    } else {
+      return ints::sext(m_max, 64, bits);
+    }
+  }
+};
+
+inline std::ostream &operator<<(std::ostream &os, const ValueRange &vr) {
+  vr.print(os);
+  return os;
+}
+
+// used to find all memory object ids and the maximum size of any
+// object state that references them (for symbolic size).
+class ObjectFinder : public ExprVisitor {
+protected:
+  Action visitRead(const ReadExpr &re) {
+    addUpdates(re.updates);
+    return Action::doChildren();
+  }
+
+  // XXX nice if this information was cached somewhere, used by
+  // independence as well right?
+  void addUpdates(const UpdateList &ul) {
+    for (const UpdateNode *un=ul.head; un; un=un->next) {
+      visit(un->index);
+      visit(un->value);
+    }
+
+    addObject(*ul.root);
+  }
+
+public:
+  void addObject(const Array& array) {
+    unsigned id = array.id;
+    std::map<unsigned,unsigned>::iterator it = results.find(id);
+
+    // FIXME: Not 64-bit size clean.
+    if (it == results.end()) {
+      results[id] = (unsigned) array.size;      
+    } else {
+      it->second = std::max(it->second, (unsigned) array.size);
+    }
+  }
+
+public:
+  std::map<unsigned, unsigned> results;
+};
+
+// XXX waste of space, rather have ByteValueRange
+typedef ValueRange CexValueData;
+
+class CexObjectData {
+public:
+  unsigned size;
+  CexValueData *values;
+
+public:
+  CexObjectData(unsigned _size) : size(_size), values(new CexValueData[size]) {
+    for (unsigned i=0; i<size; i++)
+      values[i] = ValueRange(0, 255);
+  }
+};
+
+class CexRangeEvaluator : public ExprRangeEvaluator<ValueRange> {
+public:
+  std::map<unsigned, CexObjectData> &objectValues;
+  CexRangeEvaluator(std::map<unsigned, CexObjectData> &_objectValues) 
+    : objectValues(_objectValues) {}
+
+  ValueRange getInitialReadRange(const Array &os, ValueRange index) {
+    return ValueRange(0, 255);
+  }
+};
+
+class CexConstifier : public ExprEvaluator {
+protected:
+  ref<Expr> getInitialValue(const Array& array, unsigned index) {
+    std::map<unsigned, CexObjectData>::iterator it = 
+      objectValues.find(array.id);
+    assert(it != objectValues.end() && "missing object?");
+    CexObjectData &cod = it->second;
+    
+    if (index >= cod.size) {
+      return ReadExpr::create(UpdateList(&array, true, 0), 
+                              ref<Expr>(index, Expr::Int32));
+    } else {
+      CexValueData &cvd = cod.values[index];
+      assert(cvd.min() == cvd.max() && "value is not fixed");
+      return ref<Expr>(cvd.min(), Expr::Int8);
+    }
+  }
+
+public:
+  std::map<unsigned, CexObjectData> &objectValues;
+  CexConstifier(std::map<unsigned, CexObjectData> &_objectValues) 
+    : objectValues(_objectValues) {}
+};
+
+class CexData {
+public:
+  std::map<unsigned, CexObjectData> objectValues;
+
+public:
+  CexData(ObjectFinder &finder) {
+    for (std::map<unsigned,unsigned>::iterator it = finder.results.begin(),
+           ie = finder.results.end(); it != ie; ++it) {
+      objectValues.insert(std::pair<unsigned, CexObjectData>(it->first, 
+                                                             CexObjectData(it->second)));
+    }
+  }  
+  ~CexData() {
+    for (std::map<unsigned, CexObjectData>::iterator it = objectValues.begin(),
+           ie = objectValues.end(); it != ie; ++it)
+      delete[] it->second.values;
+  }
+
+  void forceExprToValue(ref<Expr> e, uint64_t value) {
+    forceExprToRange(e, CexValueData(value,value));
+  }
+
+  void forceExprToRange(ref<Expr> e, CexValueData range) {
+#ifdef LOG
+    //    *theLog << "force: " << e << " to " << range << "\n";
+#endif
+    switch (e.getKind()) {
+    case Expr::Constant: {
+      // rather a pity if the constant isn't in the range, but how can
+      // we use this?
+      break;
+    }
+
+      // Special
+
+    case Expr::NotOptimized: break;
+
+    case Expr::Read: {
+      ReadExpr *re = static_ref_cast<ReadExpr>(e);
+      const Array *array = re->updates.root;
+      CexObjectData &cod = objectValues.find(array->id)->second;
+
+      // XXX we need to respect the version here and object state chain
+
+      if (re->index.isConstant() && 
+          re->index.getConstantValue() < array->size) {
+        CexValueData &cvd = cod.values[re->index.getConstantValue()];
+        CexValueData tmp = cvd.set_intersection(range);
+        
+        if (tmp.isEmpty()) {
+          if (range.isFixed()) // ranges conflict, if new one is fixed use that
+            cvd = range;
+        } else {
+          cvd = tmp;
+        }
+      } else {
+        // XXX        fatal("XXX not implemented");
+      }
+      
+      break;
+    }
+
+    case Expr::Select: {
+      SelectExpr *se = static_ref_cast<SelectExpr>(e);
+      ValueRange cond = evalRangeForExpr(se->cond);
+      if (cond.isFixed()) {
+        if (cond.min()) {
+          forceExprToRange(se->trueExpr, range);
+        } else {
+          forceExprToRange(se->falseExpr, range);
+        }
+      } else {
+        // XXX imprecise... we have a choice here. One method is to
+        // simply force both sides into the specified range (since the
+        // condition is indetermined). This may lose in two ways, the
+        // first is that the condition chosen may limit further
+        // restrict the range in each of the children, however this is
+        // less of a problem as the range will be a superset of legal
+        // values. The other is if the condition ends up being forced
+        // by some other constraints, then we needlessly forced one
+        // side into the given range.
+        //
+        // The other method would be to force the condition to one
+        // side and force that side into the given range. This loses
+        // when we force the condition to an unsatisfiable value
+        // (either because the condition cannot be that, or the
+        // resulting range given that condition is not in the required
+        // range).
+        // 
+        // Currently we just force both into the range. A hybrid would
+        // be to evaluate the ranges for each of the children... if
+        // one of the ranges happens to already be a subset of the
+        // required range then it may be preferable to force the
+        // condition to that side.
+        forceExprToRange(se->trueExpr, range);
+        forceExprToRange(se->falseExpr, range);
+      }
+      break;
+    }
+
+      // XXX imprecise... the problem here is that extracting bits
+      // loses information about what bits are connected across the
+      // bytes. if a value can be 1 or 256 then either the top or
+      // lower byte is 0, but just extraction loses this information
+      // and will allow neither,one,or both to be 1.
+      //
+      // we can protect against this in a limited fashion by writing
+      // the extraction a byte at a time, then checking the evaluated
+      // value, isolating for that range, and continuing.
+    case Expr::Concat: {
+      ConcatExpr *ce = static_ref_cast<ConcatExpr>(e);
+      if (ce->is2ByteConcat()) {
+	forceExprToRange(ce->getKid(0), range.extract( 8, 16));
+	forceExprToRange(ce->getKid(1), range.extract( 0,  8));
+      }
+      else if (ce->is4ByteConcat()) {
+	forceExprToRange(ce->getKid(0), range.extract(24, 32));
+	forceExprToRange(ce->getKid(1), range.extract(16, 24));
+	forceExprToRange(ce->getKid(2), range.extract( 8, 16));
+	forceExprToRange(ce->getKid(3), range.extract( 0,  8));
+      }
+      else if (ce->is8ByteConcat()) {
+	forceExprToRange(ce->getKid(0), range.extract(56, 64));
+	forceExprToRange(ce->getKid(1), range.extract(48, 56));
+	forceExprToRange(ce->getKid(2), range.extract(40, 48));
+	forceExprToRange(ce->getKid(3), range.extract(32, 40));
+	forceExprToRange(ce->getKid(4), range.extract(24, 32));
+	forceExprToRange(ce->getKid(5), range.extract(16, 24));
+	forceExprToRange(ce->getKid(6), range.extract( 8, 16));
+	forceExprToRange(ce->getKid(7), range.extract( 0,  8));
+      }
+      
+      break;
+    }
+
+    case Expr::Extract: {
+      // XXX
+      break;
+    }
+
+      // Casting
+
+      // Simply intersect the output range with the range of all
+      // possible outputs and then truncate to the desired number of
+      // bits. 
+
+      // For ZExt this simplifies to just intersection with the
+      // possible input range.
+    case Expr::ZExt: {
+      CastExpr *ce = static_ref_cast<CastExpr>(e);
+      unsigned inBits = ce->src.getWidth();
+      ValueRange input = range.set_intersection(ValueRange(0, bits64::maxValueOfNBits(inBits)));
+      forceExprToRange(ce->src, input);
+      break;
+    }
+      // For SExt instead of doing the intersection we just take the output range
+      // minus the impossible values. This is nicer since it is a single interval.
+    case Expr::SExt: {
+      CastExpr *ce = static_ref_cast<CastExpr>(e);
+      unsigned inBits = ce->src.getWidth();
+      unsigned outBits = ce->width;
+      ValueRange output = range.set_difference(ValueRange(1<<(inBits-1),
+                                                          (bits64::maxValueOfNBits(outBits)-
+                                                           bits64::maxValueOfNBits(inBits-1)-1)));
+      ValueRange input = output.binaryAnd(bits64::maxValueOfNBits(inBits));
+      forceExprToRange(ce->src, input);
+      break;
+    }
+
+      // Binary
+
+    case Expr::And: {
+      BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
+      if (be->getWidth()==Expr::Bool) {
+        if (range.isFixed()) {
+          ValueRange left = evalRangeForExpr(be->left);
+          ValueRange right = evalRangeForExpr(be->right);
+
+          if (!range.min()) {
+            if (left.mustEqual(0) || right.mustEqual(0)) {
+              // all is well
+            } else {
+              // XXX heuristic, which order
+
+              forceExprToValue(be->left, 0);
+              left = evalRangeForExpr(be->left);
+
+              // see if that worked
+              if (!left.mustEqual(1))
+                forceExprToValue(be->right, 0);
+            }
+          } else {
+            if (!left.mustEqual(1)) forceExprToValue(be->left, 1);
+            if (!right.mustEqual(1)) forceExprToValue(be->right, 1);
+          }
+        }
+      } else {
+        // XXX
+      }
+      break;
+    }
+
+    case Expr::Or: {
+      BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
+      if (be->getWidth()==Expr::Bool) {
+        if (range.isFixed()) {
+          ValueRange left = evalRangeForExpr(be->left);
+          ValueRange right = evalRangeForExpr(be->right);
+
+          if (range.min()) {
+            if (left.mustEqual(1) || right.mustEqual(1)) {
+              // all is well
+            } else {
+              // XXX heuristic, which order?
+              
+              // force left to value we need
+              forceExprToValue(be->left, 1);
+              left = evalRangeForExpr(be->left);
+
+              // see if that worked
+              if (!left.mustEqual(1))
+                forceExprToValue(be->right, 1);
+            }
+          } else {
+            if (!left.mustEqual(0)) forceExprToValue(be->left, 0);
+            if (!right.mustEqual(0)) forceExprToValue(be->right, 0);
+          }
+        }
+      } else {
+        // XXX
+      }
+      break;
+    }
+
+    case Expr::Xor: break;
+
+      // Comparison
+
+    case Expr::Eq: {
+      BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
+      if (range.isFixed()) {
+        if (be->left.isConstant()) {
+          uint64_t value = be->left.getConstantValue();
+          if (range.min()) {
+            forceExprToValue(be->right, value);
+          } else {
+            if (value==0) {
+              forceExprToRange(be->right, 
+                               CexValueData(1,
+                                            ints::sext(1, 
+                                                       be->right.getWidth(),
+                                                       1)));
+            } else {
+              // XXX heuristic / lossy, could be better to pick larger range?
+              forceExprToRange(be->right, CexValueData(0, value-1));
+            }
+          }
+        } else {
+          // XXX what now
+        }
+      }
+      break;
+    }
+
+    case Expr::Ult: {
+      BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
+      
+      // XXX heuristic / lossy, what order if conflict
+
+      if (range.isFixed()) {
+        ValueRange left = evalRangeForExpr(be->left);
+        ValueRange right = evalRangeForExpr(be->right);
+
+        uint64_t maxValue = bits64::maxValueOfNBits(be->right.getWidth());
+
+        // XXX should deal with overflow (can lead to empty range)
+
+        if (left.isFixed()) {
+          if (range.min()) {
+            forceExprToRange(be->right, CexValueData(left.min()+1, maxValue));
+          } else {
+            forceExprToRange(be->right, CexValueData(0, left.min()));
+          }
+        } else if (right.isFixed()) {
+          if (range.min()) {
+            forceExprToRange(be->left, CexValueData(0, right.min()-1));
+          } else {
+            forceExprToRange(be->left, CexValueData(right.min(), maxValue));
+          }
+        } else {
+          // XXX ???
+        }
+      }
+      break;
+    }
+    case Expr::Ule: {
+      BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
+      
+      // XXX heuristic / lossy, what order if conflict
+
+      if (range.isFixed()) {
+        ValueRange left = evalRangeForExpr(be->left);
+        ValueRange right = evalRangeForExpr(be->right);
+
+        // XXX should deal with overflow (can lead to empty range)
+
+        uint64_t maxValue = bits64::maxValueOfNBits(be->right.getWidth());
+        if (left.isFixed()) {
+          if (range.min()) {
+            forceExprToRange(be->right, CexValueData(left.min(), maxValue));
+          } else {
+            forceExprToRange(be->right, CexValueData(0, left.min()-1));
+          }
+        } else if (right.isFixed()) {
+          if (range.min()) {
+            forceExprToRange(be->left, CexValueData(0, right.min()));
+          } else {
+            forceExprToRange(be->left, CexValueData(right.min()+1, maxValue));
+          }
+        } else {
+          // XXX ???
+        }
+      }
+      break;
+    }
+
+    case Expr::Ne:
+    case Expr::Ugt:
+    case Expr::Uge:
+    case Expr::Sgt:
+    case Expr::Sge:
+      assert(0 && "invalid expressions (uncanonicalized");
+
+    default:
+      break;
+    }
+  }
+
+  void fixValues() {
+    for (std::map<unsigned, CexObjectData>::iterator it = objectValues.begin(),
+           ie = objectValues.end(); it != ie; ++it) {
+      CexObjectData &cod = it->second;
+      for (unsigned i=0; i<cod.size; i++) {
+        CexValueData &cvd = cod.values[i];
+        cvd = CexValueData(cvd.min() + (cvd.max()-cvd.min())/2);
+      }
+    }
+  }
+
+  ValueRange evalRangeForExpr(ref<Expr> &e) {
+    CexRangeEvaluator ce(objectValues);
+    return ce.evaluate(e);
+  }
+
+  bool exprMustBeValue(ref<Expr> e, uint64_t value) {
+    CexConstifier cc(objectValues);
+    ref<Expr> v = cc.visit(e);
+    if (!v.isConstant()) return false;
+    // XXX reenable once all reads and vars are fixed
+    //    assert(v.isConstant() && "not all values have been fixed");
+    return v.getConstantValue()==value;
+  }
+};
+
+/* *** */
+
+
+class FastCexSolver : public IncompleteSolver {
+public:
+  FastCexSolver();
+  ~FastCexSolver();
+
+  IncompleteSolver::PartialValidity computeTruth(const Query&);  
+  bool computeValue(const Query&, ref<Expr> &result);
+  bool computeInitialValues(const Query&,
+                            const std::vector<const Array*> &objects,
+                            std::vector< std::vector<unsigned char> > &values,
+                            bool &hasSolution);
+};
+
+FastCexSolver::FastCexSolver() { }
+
+FastCexSolver::~FastCexSolver() { }
+
+IncompleteSolver::PartialValidity 
+FastCexSolver::computeTruth(const Query& query) {
+#ifdef LOG
+  std::ostringstream log;
+  theLog = &log;
+  //  log << "------ start FastCexSolver::mustBeTrue ------\n";
+  log << "-- QUERY --\n";
+  unsigned i=0;
+  for (ConstraintManager::const_iterator it = query.constraints.begin(), 
+         ie = query.constraints.end(); it != ie; ++it)
+    log << "    C" << i++ << ": " << *it << ", \n";
+  log << "    Q : " << query.expr << "\n";
+#endif
+
+  ObjectFinder of;
+  for (ConstraintManager::const_iterator it = query.constraints.begin(), 
+         ie = query.constraints.end(); it != ie; ++it)
+    of.visit(*it);
+  of.visit(query.expr);
+  CexData cd(of);
+
+  for (ConstraintManager::const_iterator it = query.constraints.begin(), 
+         ie = query.constraints.end(); it != ie; ++it)
+    cd.forceExprToValue(*it, 1);
+  cd.forceExprToValue(query.expr, 0);
+
+#ifdef LOG
+  log << " -- ranges --\n";
+  for (std::map<unsigned, CexObjectData>::iterator it = objectValues.begin(),
+         ie = objectValues.end(); it != ie; ++it) {
+    CexObjectData &cod = it->second;
+    log << "    arr" << it->first << "[" << cod.size << "] = [";
+    unsigned continueFrom=cod.size-1;
+    for (; continueFrom>0; continueFrom--)
+      if (cod.values[continueFrom-1]!=cod.values[continueFrom])
+        break;
+    for (unsigned i=0; i<cod.size; i++) {
+      log << cod.values[i];
+      if (i<cod.size-1) {
+        log << ", ";
+        if (i==continueFrom) {
+          log << "...";
+          break;
+        }
+      }
+    }
+    log << "]\n";
+  }
+#endif
+
+  // this could be done lazily of course
+  cd.fixValues();
+
+#ifdef LOG
+  log << " -- fixed values --\n";
+  for (std::map<unsigned, CexObjectData>::iterator it = objectValues.begin(),
+         ie = objectValues.end(); it != ie; ++it) {
+    CexObjectData &cod = it->second;
+    log << "    arr" << it->first << "[" << cod.size << "] = [";
+    unsigned continueFrom=cod.size-1;
+    for (; continueFrom>0; continueFrom--)
+      if (cod.values[continueFrom-1]!=cod.values[continueFrom])
+        break;
+    for (unsigned i=0; i<cod.size; i++) {
+      log << cod.values[i];
+      if (i<cod.size-1) {
+        log << ", ";
+        if (i==continueFrom) {
+          log << "...";
+          break;
+        }
+      }
+    }
+    log << "]\n";
+  }
+#endif
+
+  // check the result
+
+  bool isGood = true;
+
+  if (!cd.exprMustBeValue(query.expr, 0)) isGood = false;
+
+  for (ConstraintManager::const_iterator it = query.constraints.begin(), 
+         ie = query.constraints.end(); it != ie; ++it)
+    if (!cd.exprMustBeValue(*it, 1)) 
+      isGood = false;
+
+#ifdef LOG
+  log << " -- evaluating result --\n";
+  
+  i=0;
+  for (ConstraintManager::const_iterator it = query.constraints.begin(), 
+         ie = query.constraints.end(); it != ie; ++it) {
+    bool res = cd.exprMustBeValue(*it, 1);
+    log << "    C" << i++ << ": " << (res?"true":"false") << "\n";
+  }
+  log << "    Q : " 
+      << (cd.exprMustBeValue(query.expr, 0)?"true":"false") << "\n";
+  
+  log << "\n\n";
+#endif
+
+  return isGood ? IncompleteSolver::MayBeFalse : IncompleteSolver::None;
+}
+
+bool FastCexSolver::computeValue(const Query& query, ref<Expr> &result) {
+  ObjectFinder of;
+  for (ConstraintManager::const_iterator it = query.constraints.begin(), 
+         ie = query.constraints.end(); it != ie; ++it)
+    of.visit(*it);
+  of.visit(query.expr);
+  CexData cd(of);
+
+  for (ConstraintManager::const_iterator it = query.constraints.begin(), 
+         ie = query.constraints.end(); it != ie; ++it)
+    cd.forceExprToValue(*it, 1);
+
+  // this could be done lazily of course
+  cd.fixValues();
+
+  // check the result
+  for (ConstraintManager::const_iterator it = query.constraints.begin(), 
+         ie = query.constraints.end(); it != ie; ++it)
+    if (!cd.exprMustBeValue(*it, 1))
+      return false;
+
+  CexConstifier cc(cd.objectValues);
+  ref<Expr> value = cc.visit(query.expr);
+
+  if (value.isConstant()) {
+    result = value;
+    return true;
+  } else {
+    return false;
+  }
+}
+
+bool
+FastCexSolver::computeInitialValues(const Query& query,
+                                    const std::vector<const Array*>
+                                      &objects,
+                                    std::vector< std::vector<unsigned char> >
+                                      &values,
+                                    bool &hasSolution) {
+  ObjectFinder of;
+  for (ConstraintManager::const_iterator it = query.constraints.begin(), 
+         ie = query.constraints.end(); it != ie; ++it)
+    of.visit(*it);
+  of.visit(query.expr);
+  for (unsigned i = 0; i != objects.size(); ++i)
+    of.addObject(*objects[i]);
+  CexData cd(of);
+
+  for (ConstraintManager::const_iterator it = query.constraints.begin(), 
+         ie = query.constraints.end(); it != ie; ++it)
+    cd.forceExprToValue(*it, 1);
+  cd.forceExprToValue(query.expr, 0);
+
+  // this could be done lazily of course
+  cd.fixValues();
+
+  // check the result
+  for (ConstraintManager::const_iterator it = query.constraints.begin(), 
+         ie = query.constraints.end(); it != ie; ++it)
+    if (!cd.exprMustBeValue(*it, 1))
+      return false;
+  if (!cd.exprMustBeValue(query.expr, 0))
+    return false;
+
+  hasSolution = true;
+  CexConstifier cc(cd.objectValues);
+  for (unsigned i = 0; i != objects.size(); ++i) {
+    const Array *array = objects[i];
+    std::vector<unsigned char> data;
+    data.reserve(array->size);
+
+    for (unsigned i=0; i < array->size; i++) {
+      ref<Expr> value =
+        cc.visit(ReadExpr::create(UpdateList(array, true, 0),
+                                  ConstantExpr::create(i,
+                                                       kMachinePointerType)));
+      
+      if (value.isConstant()) {
+        data.push_back(value.getConstantValue());
+      } else {
+        // FIXME: When does this happen?
+        return false;
+      }
+    }
+
+    values.push_back(data);
+  }
+
+  return true;
+}
+
+
+Solver *klee::createFastCexSolver(Solver *s) {
+  return new Solver(new StagedSolverImpl(new FastCexSolver(), s));
+}