about summary refs log tree commit diff homepage
path: root/lib/Solver
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Solver')
-rw-r--r--lib/Solver/CoreSolver.cpp4
-rw-r--r--lib/Solver/Z3Builder.cpp811
-rw-r--r--lib/Solver/Z3Builder.h196
-rw-r--r--lib/Solver/Z3Solver.cpp299
4 files changed, 1307 insertions, 3 deletions
diff --git a/lib/Solver/CoreSolver.cpp b/lib/Solver/CoreSolver.cpp
index 26842d31..94bb3a5e 100644
--- a/lib/Solver/CoreSolver.cpp
+++ b/lib/Solver/CoreSolver.cpp
@@ -88,9 +88,7 @@ Solver *createCoreSolver(CoreSolverType cst) {
     return createDummySolver();
   case Z3_SOLVER:
 #ifdef ENABLE_Z3
-    // TODO
-    llvm::report_fatal_error("Z3 support not implemented");
-    return NULL;
+    return new Z3Solver();
 #else
     llvm::errs() << "Not compiled with Z3 support\n";
     return NULL;
diff --git a/lib/Solver/Z3Builder.cpp b/lib/Solver/Z3Builder.cpp
new file mode 100644
index 00000000..f928c927
--- /dev/null
+++ b/lib/Solver/Z3Builder.cpp
@@ -0,0 +1,811 @@
+//===-- Z3Builder.cpp ------------------------------------------*- C++ -*-====//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+#include "klee/Config/config.h"
+#ifdef ENABLE_Z3
+#include "Z3Builder.h"
+
+#include "klee/Expr.h"
+#include "klee/Solver.h"
+#include "klee/util/Bits.h"
+#include "ConstantDivision.h"
+#include "klee/SolverStats.h"
+#include "llvm/Support/CommandLine.h"
+
+using namespace klee;
+
+namespace {
+llvm::cl::opt<bool> UseConstructHashZ3(
+    "use-construct-hash-z3",
+    llvm::cl::desc("Use hash-consing during Z3 query construction."),
+    llvm::cl::init(true));
+}
+
+void custom_z3_error_handler(Z3_context ctx, Z3_error_code ec) {
+  ::Z3_string errorMsg = Z3_get_error_msg(ctx, ec);
+  // FIXME: This is kind of a hack. The value comes from the enum
+  // Z3_CANCELED_MSG but this isn't currently exposed by Z3's C API
+  if (strcmp(errorMsg, "canceled") == 0) {
+    // Solver timeout is not a fatal error
+    return;
+  }
+  llvm::errs() << "Error: Incorrect use of Z3. [" << ec << "] " << errorMsg
+               << "\n";
+  abort();
+}
+
+Z3ArrayExprHash::~Z3ArrayExprHash() {}
+
+void Z3ArrayExprHash::clear() {
+  _update_node_hash.clear();
+  _array_hash.clear();
+}
+
+Z3Builder::Z3Builder(bool autoClearConstructCache)
+    : autoClearConstructCache(autoClearConstructCache) {
+  // FIXME: Should probably let the client pass in a Z3_config instead
+  Z3_config cfg = Z3_mk_config();
+  // It is very important that we ask Z3 to let us manage memory so that
+  // we are able to cache expressions and sorts.
+  ctx = Z3_mk_context_rc(cfg);
+  // Make sure we handle any errors reported by Z3.
+  Z3_set_error_handler(ctx, custom_z3_error_handler);
+  // When emitting Z3 expressions make them SMT-LIBv2 compliant
+  Z3_set_ast_print_mode(ctx, Z3_PRINT_SMTLIB2_COMPLIANT);
+  Z3_del_config(cfg);
+}
+
+Z3Builder::~Z3Builder() {
+  // Clear caches so exprs/sorts gets freed before the destroying context
+  // they aren associated with.
+  clearConstructCache();
+  _arr_hash.clear();
+  Z3_del_context(ctx);
+}
+
+Z3SortHandle Z3Builder::getBvSort(unsigned width) {
+  // FIXME: cache these
+  return Z3SortHandle(Z3_mk_bv_sort(ctx, width), ctx);
+}
+
+Z3SortHandle Z3Builder::getArraySort(Z3SortHandle domainSort,
+                                     Z3SortHandle rangeSort) {
+  // FIXME: cache these
+  return Z3SortHandle(Z3_mk_array_sort(ctx, domainSort, rangeSort), ctx);
+}
+
+Z3ASTHandle Z3Builder::buildArray(const char *name, unsigned indexWidth,
+                                  unsigned valueWidth) {
+  Z3SortHandle domainSort = getBvSort(indexWidth);
+  Z3SortHandle rangeSort = getBvSort(valueWidth);
+  Z3SortHandle t = getArraySort(domainSort, rangeSort);
+  Z3_symbol s = Z3_mk_string_symbol(ctx, const_cast<char *>(name));
+  return Z3ASTHandle(Z3_mk_const(ctx, s, t), ctx);
+}
+
+Z3ASTHandle Z3Builder::getTrue() { return Z3ASTHandle(Z3_mk_true(ctx), ctx); }
+
+Z3ASTHandle Z3Builder::getFalse() { return Z3ASTHandle(Z3_mk_false(ctx), ctx); }
+
+Z3ASTHandle Z3Builder::bvOne(unsigned width) { return bvZExtConst(width, 1); }
+
+Z3ASTHandle Z3Builder::bvZero(unsigned width) { return bvZExtConst(width, 0); }
+
+Z3ASTHandle Z3Builder::bvMinusOne(unsigned width) {
+  return bvSExtConst(width, (int64_t)-1);
+}
+
+Z3ASTHandle Z3Builder::bvConst32(unsigned width, uint32_t value) {
+  Z3SortHandle t = getBvSort(width);
+  return Z3ASTHandle(Z3_mk_unsigned_int(ctx, value, t), ctx);
+}
+
+Z3ASTHandle Z3Builder::bvConst64(unsigned width, uint64_t value) {
+  Z3SortHandle t = getBvSort(width);
+  return Z3ASTHandle(Z3_mk_unsigned_int64(ctx, value, t), ctx);
+}
+
+Z3ASTHandle Z3Builder::bvZExtConst(unsigned width, uint64_t value) {
+  if (width <= 64)
+    return bvConst64(width, value);
+
+  Z3ASTHandle expr = Z3ASTHandle(bvConst64(64, value), ctx);
+  Z3ASTHandle zero = Z3ASTHandle(bvConst64(64, 0), ctx);
+  for (width -= 64; width > 64; width -= 64)
+    expr = Z3ASTHandle(Z3_mk_concat(ctx, zero, expr), ctx);
+  return Z3ASTHandle(Z3_mk_concat(ctx, bvConst64(width, 0), expr), ctx);
+}
+
+Z3ASTHandle Z3Builder::bvSExtConst(unsigned width, uint64_t value) {
+  if (width <= 64)
+    return bvConst64(width, value);
+
+  Z3SortHandle t = getBvSort(width - 64);
+  if (value >> 63) {
+    Z3ASTHandle r = Z3ASTHandle(Z3_mk_int64(ctx, -1, t), ctx);
+    return Z3ASTHandle(Z3_mk_concat(ctx, r, bvConst64(64, value)), ctx);
+  }
+
+  Z3ASTHandle r = Z3ASTHandle(Z3_mk_int64(ctx, 0, t), ctx);
+  return Z3ASTHandle(Z3_mk_concat(ctx, r, bvConst64(64, value)), ctx);
+}
+
+Z3ASTHandle Z3Builder::bvBoolExtract(Z3ASTHandle expr, int bit) {
+  return Z3ASTHandle(Z3_mk_eq(ctx, bvExtract(expr, bit, bit), bvOne(1)), ctx);
+}
+
+Z3ASTHandle Z3Builder::bvExtract(Z3ASTHandle expr, unsigned top,
+                                 unsigned bottom) {
+  return Z3ASTHandle(Z3_mk_extract(ctx, top, bottom, expr), ctx);
+}
+
+Z3ASTHandle Z3Builder::eqExpr(Z3ASTHandle a, Z3ASTHandle b) {
+  return Z3ASTHandle(Z3_mk_eq(ctx, a, b), ctx);
+}
+
+// logical right shift
+Z3ASTHandle Z3Builder::bvRightShift(Z3ASTHandle expr, unsigned shift) {
+  unsigned width = getBVLength(expr);
+
+  if (shift == 0) {
+    return expr;
+  } else if (shift >= width) {
+    return bvZero(width); // Overshift to zero
+  } else {
+    return Z3ASTHandle(
+        Z3_mk_concat(ctx, bvZero(shift), bvExtract(expr, width - 1, shift)),
+        ctx);
+  }
+}
+
+// logical left shift
+Z3ASTHandle Z3Builder::bvLeftShift(Z3ASTHandle expr, unsigned shift) {
+  unsigned width = getBVLength(expr);
+
+  if (shift == 0) {
+    return expr;
+  } else if (shift >= width) {
+    return bvZero(width); // Overshift to zero
+  } else {
+    return Z3ASTHandle(
+        Z3_mk_concat(ctx, bvExtract(expr, width - shift - 1, 0), bvZero(shift)),
+        ctx);
+  }
+}
+
+// left shift by a variable amount on an expression of the specified width
+Z3ASTHandle Z3Builder::bvVarLeftShift(Z3ASTHandle expr, Z3ASTHandle shift) {
+  unsigned width = getBVLength(expr);
+  Z3ASTHandle res = bvZero(width);
+
+  // construct a big if-then-elif-elif-... with one case per possible shift
+  // amount
+  for (int i = width - 1; i >= 0; i--) {
+    res =
+        iteExpr(eqExpr(shift, bvConst32(width, i)), bvLeftShift(expr, i), res);
+  }
+
+  // If overshifting, shift to zero
+  Z3ASTHandle ex = bvLtExpr(shift, bvConst32(getBVLength(shift), width));
+  res = iteExpr(ex, res, bvZero(width));
+  return res;
+}
+
+// logical right shift by a variable amount on an expression of the specified
+// width
+Z3ASTHandle Z3Builder::bvVarRightShift(Z3ASTHandle expr, Z3ASTHandle shift) {
+  unsigned width = getBVLength(expr);
+  Z3ASTHandle res = bvZero(width);
+
+  // construct a big if-then-elif-elif-... with one case per possible shift
+  // amount
+  for (int i = width - 1; i >= 0; i--) {
+    res =
+        iteExpr(eqExpr(shift, bvConst32(width, i)), bvRightShift(expr, i), res);
+  }
+
+  // If overshifting, shift to zero
+  Z3ASTHandle ex = bvLtExpr(shift, bvConst32(getBVLength(shift), width));
+  res = iteExpr(ex, res, bvZero(width));
+  return res;
+}
+
+// arithmetic right shift by a variable amount on an expression of the specified
+// width
+Z3ASTHandle Z3Builder::bvVarArithRightShift(Z3ASTHandle expr,
+                                            Z3ASTHandle shift) {
+  unsigned width = getBVLength(expr);
+
+  // get the sign bit to fill with
+  Z3ASTHandle signedBool = bvBoolExtract(expr, width - 1);
+
+  // start with the result if shifting by width-1
+  Z3ASTHandle res = constructAShrByConstant(expr, width - 1, signedBool);
+
+  // construct a big if-then-elif-elif-... with one case per possible shift
+  // amount
+  // XXX more efficient to move the ite on the sign outside all exprs?
+  // XXX more efficient to sign extend, right shift, then extract lower bits?
+  for (int i = width - 2; i >= 0; i--) {
+    res = iteExpr(eqExpr(shift, bvConst32(width, i)),
+                  constructAShrByConstant(expr, i, signedBool), res);
+  }
+
+  // If overshifting, shift to zero
+  Z3ASTHandle ex = bvLtExpr(shift, bvConst32(getBVLength(shift), width));
+  res = iteExpr(ex, res, bvZero(width));
+  return res;
+}
+
+Z3ASTHandle Z3Builder::notExpr(Z3ASTHandle expr) {
+  return Z3ASTHandle(Z3_mk_not(ctx, expr), ctx);
+}
+
+Z3ASTHandle Z3Builder::bvNotExpr(Z3ASTHandle expr) {
+  return Z3ASTHandle(Z3_mk_bvnot(ctx, expr), ctx);
+}
+
+Z3ASTHandle Z3Builder::andExpr(Z3ASTHandle lhs, Z3ASTHandle rhs) {
+  ::Z3_ast args[2] = {lhs, rhs};
+  return Z3ASTHandle(Z3_mk_and(ctx, 2, args), ctx);
+}
+
+Z3ASTHandle Z3Builder::bvAndExpr(Z3ASTHandle lhs, Z3ASTHandle rhs) {
+  return Z3ASTHandle(Z3_mk_bvand(ctx, lhs, rhs), ctx);
+}
+
+Z3ASTHandle Z3Builder::orExpr(Z3ASTHandle lhs, Z3ASTHandle rhs) {
+  ::Z3_ast args[2] = {lhs, rhs};
+  return Z3ASTHandle(Z3_mk_or(ctx, 2, args), ctx);
+}
+
+Z3ASTHandle Z3Builder::bvOrExpr(Z3ASTHandle lhs, Z3ASTHandle rhs) {
+  return Z3ASTHandle(Z3_mk_bvor(ctx, lhs, rhs), ctx);
+}
+
+Z3ASTHandle Z3Builder::iffExpr(Z3ASTHandle lhs, Z3ASTHandle rhs) {
+  Z3SortHandle lhsSort = Z3SortHandle(Z3_get_sort(ctx, lhs), ctx);
+  Z3SortHandle rhsSort = Z3SortHandle(Z3_get_sort(ctx, rhs), ctx);
+  assert(Z3_get_sort_kind(ctx, lhsSort) == Z3_get_sort_kind(ctx, rhsSort) &&
+         "lhs and rhs sorts must match");
+  assert(Z3_get_sort_kind(ctx, lhsSort) == Z3_BOOL_SORT && "args must have BOOL sort");
+  return Z3ASTHandle(Z3_mk_iff(ctx, lhs, rhs), ctx);
+}
+
+Z3ASTHandle Z3Builder::bvXorExpr(Z3ASTHandle lhs, Z3ASTHandle rhs) {
+  return Z3ASTHandle(Z3_mk_bvxor(ctx, lhs, rhs), ctx);
+}
+
+Z3ASTHandle Z3Builder::bvSignExtend(Z3ASTHandle src, unsigned width) {
+  unsigned src_width =
+      Z3_get_bv_sort_size(ctx, Z3SortHandle(Z3_get_sort(ctx, src), ctx));
+  assert(src_width <= width && "attempted to extend longer data");
+
+  return Z3ASTHandle(Z3_mk_sign_ext(ctx, width - src_width, src), ctx);
+}
+
+Z3ASTHandle Z3Builder::writeExpr(Z3ASTHandle array, Z3ASTHandle index,
+                                 Z3ASTHandle value) {
+  return Z3ASTHandle(Z3_mk_store(ctx, array, index, value), ctx);
+}
+
+Z3ASTHandle Z3Builder::readExpr(Z3ASTHandle array, Z3ASTHandle index) {
+  return Z3ASTHandle(Z3_mk_select(ctx, array, index), ctx);
+}
+
+Z3ASTHandle Z3Builder::iteExpr(Z3ASTHandle condition, Z3ASTHandle whenTrue,
+                               Z3ASTHandle whenFalse) {
+  return Z3ASTHandle(Z3_mk_ite(ctx, condition, whenTrue, whenFalse), ctx);
+}
+
+unsigned Z3Builder::getBVLength(Z3ASTHandle expr) {
+  return Z3_get_bv_sort_size(ctx, Z3SortHandle(Z3_get_sort(ctx, expr), ctx));
+}
+
+Z3ASTHandle Z3Builder::bvLtExpr(Z3ASTHandle lhs, Z3ASTHandle rhs) {
+  return Z3ASTHandle(Z3_mk_bvult(ctx, lhs, rhs), ctx);
+}
+
+Z3ASTHandle Z3Builder::bvLeExpr(Z3ASTHandle lhs, Z3ASTHandle rhs) {
+  return Z3ASTHandle(Z3_mk_bvule(ctx, lhs, rhs), ctx);
+}
+
+Z3ASTHandle Z3Builder::sbvLtExpr(Z3ASTHandle lhs, Z3ASTHandle rhs) {
+  return Z3ASTHandle(Z3_mk_bvslt(ctx, lhs, rhs), ctx);
+}
+
+Z3ASTHandle Z3Builder::sbvLeExpr(Z3ASTHandle lhs, Z3ASTHandle rhs) {
+  return Z3ASTHandle(Z3_mk_bvsle(ctx, lhs, rhs), ctx);
+}
+
+Z3ASTHandle Z3Builder::constructAShrByConstant(Z3ASTHandle expr, unsigned shift,
+                                               Z3ASTHandle isSigned) {
+  unsigned width = getBVLength(expr);
+
+  if (shift == 0) {
+    return expr;
+  } else if (shift >= width) {
+    return bvZero(width); // Overshift to zero
+  } else {
+    // FIXME: Is this really the best way to interact with Z3?
+    return iteExpr(isSigned,
+                   Z3ASTHandle(Z3_mk_concat(ctx, bvMinusOne(shift),
+                                            bvExtract(expr, width - 1, shift)),
+                               ctx),
+                   bvRightShift(expr, shift));
+  }
+}
+
+Z3ASTHandle Z3Builder::getInitialArray(const Array *root) {
+
+  assert(root);
+  Z3ASTHandle array_expr;
+  bool hashed = _arr_hash.lookupArrayExpr(root, array_expr);
+
+  if (!hashed) {
+    // Unique arrays by name, so we make sure the name is unique by
+    // including the address.
+    char buf[32];
+    unsigned const addrlen =
+        sprintf(buf, "_%p", (const void *)root) + 1; // +1 for null-termination
+    unsigned const space = (root->name.length() > 32 - addrlen)
+                               ? (32 - addrlen)
+                               : root->name.length();
+    memmove(buf + space, buf, addrlen); // moving the address part to the end
+    memcpy(buf, root->name.c_str(), space); // filling out the name part
+
+    array_expr = buildArray(buf, root->getDomain(), root->getRange());
+
+    if (root->isConstantArray()) {
+      // FIXME: Flush the concrete values into Z3. Ideally we would do this
+      // using assertions, which might be faster, but we need to fix the caching
+      // to work correctly in that case.
+      for (unsigned i = 0, e = root->size; i != e; ++i) {
+        Z3ASTHandle prev = array_expr;
+        array_expr = writeExpr(
+            prev, construct(ConstantExpr::alloc(i, root->getDomain()), 0),
+            construct(root->constantValues[i], 0));
+      }
+    }
+
+    _arr_hash.hashArrayExpr(root, array_expr);
+  }
+
+  return (array_expr);
+}
+
+Z3ASTHandle Z3Builder::getInitialRead(const Array *root, unsigned index) {
+  return readExpr(getInitialArray(root), bvConst32(32, index));
+}
+
+Z3ASTHandle Z3Builder::getArrayForUpdate(const Array *root,
+                                         const UpdateNode *un) {
+  if (!un) {
+    return (getInitialArray(root));
+  } else {
+    // FIXME: This really needs to be non-recursive.
+    Z3ASTHandle un_expr;
+    bool hashed = _arr_hash.lookupUpdateNodeExpr(un, un_expr);
+
+    if (!hashed) {
+      un_expr = writeExpr(getArrayForUpdate(root, un->next),
+                          construct(un->index, 0), construct(un->value, 0));
+
+      _arr_hash.hashUpdateNodeExpr(un, un_expr);
+    }
+
+    return (un_expr);
+  }
+}
+
+/** if *width_out!=1 then result is a bitvector,
+    otherwise it is a bool */
+Z3ASTHandle Z3Builder::construct(ref<Expr> e, int *width_out) {
+  // TODO: We could potentially use Z3_simplify() here
+  // to store simpler expressions.
+  if (!UseConstructHashZ3 || isa<ConstantExpr>(e)) {
+    return constructActual(e, width_out);
+  } else {
+    ExprHashMap<std::pair<Z3ASTHandle, unsigned> >::iterator it =
+        constructed.find(e);
+    if (it != constructed.end()) {
+      if (width_out)
+        *width_out = it->second.second;
+      return it->second.first;
+    } else {
+      int width;
+      if (!width_out)
+        width_out = &width;
+      Z3ASTHandle res = constructActual(e, width_out);
+      constructed.insert(std::make_pair(e, std::make_pair(res, *width_out)));
+      return res;
+    }
+  }
+}
+
+/** if *width_out!=1 then result is a bitvector,
+    otherwise it is a bool */
+Z3ASTHandle Z3Builder::constructActual(ref<Expr> e, int *width_out) {
+  int width;
+  if (!width_out)
+    width_out = &width;
+
+  ++stats::queryConstructs;
+
+  switch (e->getKind()) {
+  case Expr::Constant: {
+    ConstantExpr *CE = cast<ConstantExpr>(e);
+    *width_out = CE->getWidth();
+
+    // Coerce to bool if necessary.
+    if (*width_out == 1)
+      return CE->isTrue() ? getTrue() : getFalse();
+
+    // Fast path.
+    if (*width_out <= 32)
+      return bvConst32(*width_out, CE->getZExtValue(32));
+    if (*width_out <= 64)
+      return bvConst64(*width_out, CE->getZExtValue());
+
+    ref<ConstantExpr> Tmp = CE;
+    Z3ASTHandle Res = bvConst64(64, Tmp->Extract(0, 64)->getZExtValue());
+    while (Tmp->getWidth() > 64) {
+      Tmp = Tmp->Extract(64, Tmp->getWidth() - 64);
+      unsigned Width = std::min(64U, Tmp->getWidth());
+      Res = Z3ASTHandle(
+          Z3_mk_concat(ctx,
+                       bvConst64(Width, Tmp->Extract(0, Width)->getZExtValue()),
+                       Res),
+          ctx);
+    }
+    return Res;
+  }
+
+  // Special
+  case Expr::NotOptimized: {
+    NotOptimizedExpr *noe = cast<NotOptimizedExpr>(e);
+    return construct(noe->src, width_out);
+  }
+
+  case Expr::Read: {
+    ReadExpr *re = cast<ReadExpr>(e);
+    assert(re && re->updates.root);
+    *width_out = re->updates.root->getRange();
+    return readExpr(getArrayForUpdate(re->updates.root, re->updates.head),
+                    construct(re->index, 0));
+  }
+
+  case Expr::Select: {
+    SelectExpr *se = cast<SelectExpr>(e);
+    Z3ASTHandle cond = construct(se->cond, 0);
+    Z3ASTHandle tExpr = construct(se->trueExpr, width_out);
+    Z3ASTHandle fExpr = construct(se->falseExpr, width_out);
+    return iteExpr(cond, tExpr, fExpr);
+  }
+
+  case Expr::Concat: {
+    ConcatExpr *ce = cast<ConcatExpr>(e);
+    unsigned numKids = ce->getNumKids();
+    Z3ASTHandle res = construct(ce->getKid(numKids - 1), 0);
+    for (int i = numKids - 2; i >= 0; i--) {
+      res =
+          Z3ASTHandle(Z3_mk_concat(ctx, construct(ce->getKid(i), 0), res), ctx);
+    }
+    *width_out = ce->getWidth();
+    return res;
+  }
+
+  case Expr::Extract: {
+    ExtractExpr *ee = cast<ExtractExpr>(e);
+    Z3ASTHandle src = construct(ee->expr, width_out);
+    *width_out = ee->getWidth();
+    if (*width_out == 1) {
+      return bvBoolExtract(src, ee->offset);
+    } else {
+      return bvExtract(src, ee->offset + *width_out - 1, ee->offset);
+    }
+  }
+
+  // Casting
+
+  case Expr::ZExt: {
+    int srcWidth;
+    CastExpr *ce = cast<CastExpr>(e);
+    Z3ASTHandle src = construct(ce->src, &srcWidth);
+    *width_out = ce->getWidth();
+    if (srcWidth == 1) {
+      return iteExpr(src, bvOne(*width_out), bvZero(*width_out));
+    } else {
+      return Z3ASTHandle(Z3_mk_concat(ctx, bvZero(*width_out - srcWidth), src),
+                         ctx);
+    }
+  }
+
+  case Expr::SExt: {
+    int srcWidth;
+    CastExpr *ce = cast<CastExpr>(e);
+    Z3ASTHandle src = construct(ce->src, &srcWidth);
+    *width_out = ce->getWidth();
+    if (srcWidth == 1) {
+      return iteExpr(src, bvMinusOne(*width_out), bvZero(*width_out));
+    } else {
+      return bvSignExtend(src, *width_out);
+    }
+  }
+
+  // Arithmetic
+  case Expr::Add: {
+    AddExpr *ae = cast<AddExpr>(e);
+    Z3ASTHandle left = construct(ae->left, width_out);
+    Z3ASTHandle right = construct(ae->right, width_out);
+    assert(*width_out != 1 && "uncanonicalized add");
+    Z3ASTHandle result = Z3ASTHandle(Z3_mk_bvadd(ctx, left, right), ctx);
+    assert(getBVLength(result) == static_cast<unsigned>(*width_out) &&
+           "width mismatch");
+    return result;
+  }
+
+  case Expr::Sub: {
+    SubExpr *se = cast<SubExpr>(e);
+    Z3ASTHandle left = construct(se->left, width_out);
+    Z3ASTHandle right = construct(se->right, width_out);
+    assert(*width_out != 1 && "uncanonicalized sub");
+    Z3ASTHandle result = Z3ASTHandle(Z3_mk_bvsub(ctx, left, right), ctx);
+    assert(getBVLength(result) == static_cast<unsigned>(*width_out) &&
+           "width mismatch");
+    return result;
+  }
+
+  case Expr::Mul: {
+    MulExpr *me = cast<MulExpr>(e);
+    Z3ASTHandle right = construct(me->right, width_out);
+    assert(*width_out != 1 && "uncanonicalized mul");
+    Z3ASTHandle left = construct(me->left, width_out);
+    Z3ASTHandle result = Z3ASTHandle(Z3_mk_bvmul(ctx, left, right), ctx);
+    assert(getBVLength(result) == static_cast<unsigned>(*width_out) &&
+           "width mismatch");
+    return result;
+  }
+
+  case Expr::UDiv: {
+    UDivExpr *de = cast<UDivExpr>(e);
+    Z3ASTHandle left = construct(de->left, width_out);
+    assert(*width_out != 1 && "uncanonicalized udiv");
+
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right)) {
+      if (CE->getWidth() <= 64) {
+        uint64_t divisor = CE->getZExtValue();
+        if (bits64::isPowerOfTwo(divisor))
+          return bvRightShift(left, bits64::indexOfSingleBit(divisor));
+      }
+    }
+
+    Z3ASTHandle right = construct(de->right, width_out);
+    Z3ASTHandle result = Z3ASTHandle(Z3_mk_bvudiv(ctx, left, right), ctx);
+    assert(getBVLength(result) == static_cast<unsigned>(*width_out) &&
+           "width mismatch");
+    return result;
+  }
+
+  case Expr::SDiv: {
+    SDivExpr *de = cast<SDivExpr>(e);
+    Z3ASTHandle left = construct(de->left, width_out);
+    assert(*width_out != 1 && "uncanonicalized sdiv");
+    Z3ASTHandle right = construct(de->right, width_out);
+    Z3ASTHandle result = Z3ASTHandle(Z3_mk_bvsdiv(ctx, left, right), ctx);
+    assert(getBVLength(result) == static_cast<unsigned>(*width_out) &&
+           "width mismatch");
+    return result;
+  }
+
+  case Expr::URem: {
+    URemExpr *de = cast<URemExpr>(e);
+    Z3ASTHandle left = construct(de->left, width_out);
+    assert(*width_out != 1 && "uncanonicalized urem");
+
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(de->right)) {
+      if (CE->getWidth() <= 64) {
+        uint64_t divisor = CE->getZExtValue();
+
+        if (bits64::isPowerOfTwo(divisor)) {
+          unsigned bits = bits64::indexOfSingleBit(divisor);
+
+          // special case for modding by 1 or else we bvExtract -1:0
+          if (bits == 0) {
+            return bvZero(*width_out);
+          } else {
+            return Z3ASTHandle(Z3_mk_concat(ctx, bvZero(*width_out - bits),
+                                            bvExtract(left, bits - 1, 0)),
+                               ctx);
+          }
+        }
+      }
+    }
+
+    Z3ASTHandle right = construct(de->right, width_out);
+    Z3ASTHandle result = Z3ASTHandle(Z3_mk_bvurem(ctx, left, right), ctx);
+    assert(getBVLength(result) == static_cast<unsigned>(*width_out) &&
+           "width mismatch");
+    return result;
+  }
+
+  case Expr::SRem: {
+    SRemExpr *de = cast<SRemExpr>(e);
+    Z3ASTHandle left = construct(de->left, width_out);
+    Z3ASTHandle right = construct(de->right, width_out);
+    assert(*width_out != 1 && "uncanonicalized srem");
+    // LLVM's srem instruction says that the sign follows the dividend
+    // (``left``).
+    // Z3's C API says ``Z3_mk_bvsrem()`` does this so these seem to match.
+    Z3ASTHandle result = Z3ASTHandle(Z3_mk_bvsrem(ctx, left, right), ctx);
+    assert(getBVLength(result) == static_cast<unsigned>(*width_out) &&
+           "width mismatch");
+    return result;
+  }
+
+  // Bitwise
+  case Expr::Not: {
+    NotExpr *ne = cast<NotExpr>(e);
+    Z3ASTHandle expr = construct(ne->expr, width_out);
+    if (*width_out == 1) {
+      return notExpr(expr);
+    } else {
+      return bvNotExpr(expr);
+    }
+  }
+
+  case Expr::And: {
+    AndExpr *ae = cast<AndExpr>(e);
+    Z3ASTHandle left = construct(ae->left, width_out);
+    Z3ASTHandle right = construct(ae->right, width_out);
+    if (*width_out == 1) {
+      return andExpr(left, right);
+    } else {
+      return bvAndExpr(left, right);
+    }
+  }
+
+  case Expr::Or: {
+    OrExpr *oe = cast<OrExpr>(e);
+    Z3ASTHandle left = construct(oe->left, width_out);
+    Z3ASTHandle right = construct(oe->right, width_out);
+    if (*width_out == 1) {
+      return orExpr(left, right);
+    } else {
+      return bvOrExpr(left, right);
+    }
+  }
+
+  case Expr::Xor: {
+    XorExpr *xe = cast<XorExpr>(e);
+    Z3ASTHandle left = construct(xe->left, width_out);
+    Z3ASTHandle right = construct(xe->right, width_out);
+
+    if (*width_out == 1) {
+      // XXX check for most efficient?
+      return iteExpr(left, Z3ASTHandle(notExpr(right)), right);
+    } else {
+      return bvXorExpr(left, right);
+    }
+  }
+
+  case Expr::Shl: {
+    ShlExpr *se = cast<ShlExpr>(e);
+    Z3ASTHandle left = construct(se->left, width_out);
+    assert(*width_out != 1 && "uncanonicalized shl");
+
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(se->right)) {
+      return bvLeftShift(left, (unsigned)CE->getLimitedValue());
+    } else {
+      int shiftWidth;
+      Z3ASTHandle amount = construct(se->right, &shiftWidth);
+      return bvVarLeftShift(left, amount);
+    }
+  }
+
+  case Expr::LShr: {
+    LShrExpr *lse = cast<LShrExpr>(e);
+    Z3ASTHandle left = construct(lse->left, width_out);
+    assert(*width_out != 1 && "uncanonicalized lshr");
+
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(lse->right)) {
+      return bvRightShift(left, (unsigned)CE->getLimitedValue());
+    } else {
+      int shiftWidth;
+      Z3ASTHandle amount = construct(lse->right, &shiftWidth);
+      return bvVarRightShift(left, amount);
+    }
+  }
+
+  case Expr::AShr: {
+    AShrExpr *ase = cast<AShrExpr>(e);
+    Z3ASTHandle left = construct(ase->left, width_out);
+    assert(*width_out != 1 && "uncanonicalized ashr");
+
+    if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ase->right)) {
+      unsigned shift = (unsigned)CE->getLimitedValue();
+      Z3ASTHandle signedBool = bvBoolExtract(left, *width_out - 1);
+      return constructAShrByConstant(left, shift, signedBool);
+    } else {
+      int shiftWidth;
+      Z3ASTHandle amount = construct(ase->right, &shiftWidth);
+      return bvVarArithRightShift(left, amount);
+    }
+  }
+
+  // Comparison
+
+  case Expr::Eq: {
+    EqExpr *ee = cast<EqExpr>(e);
+    Z3ASTHandle left = construct(ee->left, width_out);
+    Z3ASTHandle right = construct(ee->right, width_out);
+    if (*width_out == 1) {
+      if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ee->left)) {
+        if (CE->isTrue())
+          return right;
+        return notExpr(right);
+      } else {
+        return iffExpr(left, right);
+      }
+    } else {
+      *width_out = 1;
+      return eqExpr(left, right);
+    }
+  }
+
+  case Expr::Ult: {
+    UltExpr *ue = cast<UltExpr>(e);
+    Z3ASTHandle left = construct(ue->left, width_out);
+    Z3ASTHandle right = construct(ue->right, width_out);
+    assert(*width_out != 1 && "uncanonicalized ult");
+    *width_out = 1;
+    return bvLtExpr(left, right);
+  }
+
+  case Expr::Ule: {
+    UleExpr *ue = cast<UleExpr>(e);
+    Z3ASTHandle left = construct(ue->left, width_out);
+    Z3ASTHandle right = construct(ue->right, width_out);
+    assert(*width_out != 1 && "uncanonicalized ule");
+    *width_out = 1;
+    return bvLeExpr(left, right);
+  }
+
+  case Expr::Slt: {
+    SltExpr *se = cast<SltExpr>(e);
+    Z3ASTHandle left = construct(se->left, width_out);
+    Z3ASTHandle right = construct(se->right, width_out);
+    assert(*width_out != 1 && "uncanonicalized slt");
+    *width_out = 1;
+    return sbvLtExpr(left, right);
+  }
+
+  case Expr::Sle: {
+    SleExpr *se = cast<SleExpr>(e);
+    Z3ASTHandle left = construct(se->left, width_out);
+    Z3ASTHandle right = construct(se->right, width_out);
+    assert(*width_out != 1 && "uncanonicalized sle");
+    *width_out = 1;
+    return sbvLeExpr(left, right);
+  }
+
+// unused due to canonicalization
+#if 0
+  case Expr::Ne:
+  case Expr::Ugt:
+  case Expr::Uge:
+  case Expr::Sgt:
+  case Expr::Sge:
+#endif
+
+  default:
+    assert(0 && "unhandled Expr type");
+    return getTrue();
+  }
+}
+#endif // ENABLE_Z3
diff --git a/lib/Solver/Z3Builder.h b/lib/Solver/Z3Builder.h
new file mode 100644
index 00000000..f3b2732b
--- /dev/null
+++ b/lib/Solver/Z3Builder.h
@@ -0,0 +1,196 @@
+//===-- Z3Builder.h --------------------------------------------*- C++ -*-====//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef __UTIL_Z3BUILDER_H__
+#define __UTIL_Z3BUILDER_H__
+
+#include "klee/util/ExprHashMap.h"
+#include "klee/util/ArrayExprHash.h"
+#include "klee/Config/config.h"
+#include <z3.h>
+
+namespace klee {
+
+template <typename T> class Z3NodeHandle {
+  // Internally these Z3 types are pointers
+  // so storing these should be cheap.
+  // It would be nice if we could infer the Z3_context from the node
+  // but I can't see a way to do this from Z3's API.
+protected:
+  T node;
+  ::Z3_context context;
+
+private:
+  // To be specialised
+  inline ::Z3_ast as_ast();
+
+public:
+  Z3NodeHandle() : node(NULL), context(NULL) {}
+  Z3NodeHandle(const T _node, const ::Z3_context _context)
+      : node(_node), context(_context) {
+    if (node && context) {
+      ::Z3_inc_ref(context, as_ast());
+    }
+  };
+  ~Z3NodeHandle() {
+    if (node && context) {
+      ::Z3_dec_ref(context, as_ast());
+    }
+  }
+  Z3NodeHandle(const Z3NodeHandle &b) : node(b.node), context(b.context) {
+    if (node && context) {
+      ::Z3_inc_ref(context, as_ast());
+    }
+  }
+  Z3NodeHandle &operator=(const Z3NodeHandle &b) {
+    if (node == NULL && context == NULL) {
+      // Special case for when this object was constructed
+      // using the default constructor. Try to inherit a non null
+      // context.
+      context = b.context;
+    }
+    assert(context == b.context && "Mismatched Z3 contexts!");
+    // node != nullptr ==> context != NULL
+    assert((node == NULL || context) &&
+           "Can't have non nullptr node with nullptr context");
+
+    if (node && context) {
+      ::Z3_dec_ref(context, as_ast());
+    }
+    node = b.node;
+    if (node && context) {
+      ::Z3_inc_ref(context, as_ast());
+    }
+    return *this;
+  }
+  // To be specialised
+  void dump();
+
+  operator T() { return node; }
+};
+
+// Specialise for Z3_sort
+template <> inline ::Z3_ast Z3NodeHandle<Z3_sort>::as_ast() {
+  // In Z3 internally this call is just a cast. We could just do that
+  // instead to simplify our implementation but this seems cleaner.
+  return ::Z3_sort_to_ast(context, node);
+}
+template <> inline void Z3NodeHandle<Z3_sort>::dump() {
+  llvm::errs() << "Z3SortHandle:\n" << ::Z3_sort_to_string(context, node)
+               << "\n";
+}
+typedef Z3NodeHandle<Z3_sort> Z3SortHandle;
+
+// Specialise for Z3_ast
+template <> inline ::Z3_ast Z3NodeHandle<Z3_ast>::as_ast() { return node; }
+template <> inline void Z3NodeHandle<Z3_ast>::dump() {
+  llvm::errs() << "Z3ASTHandle:\n" << ::Z3_ast_to_string(context, as_ast())
+               << "\n";
+}
+typedef Z3NodeHandle<Z3_ast> Z3ASTHandle;
+
+class Z3ArrayExprHash : public ArrayExprHash<Z3ASTHandle> {
+
+  friend class Z3Builder;
+
+public:
+  Z3ArrayExprHash(){};
+  virtual ~Z3ArrayExprHash();
+  void clear();
+};
+
+class Z3Builder {
+  ExprHashMap<std::pair<Z3ASTHandle, unsigned> > constructed;
+  Z3ArrayExprHash _arr_hash;
+
+private:
+  Z3ASTHandle bvOne(unsigned width);
+  Z3ASTHandle bvZero(unsigned width);
+  Z3ASTHandle bvMinusOne(unsigned width);
+  Z3ASTHandle bvConst32(unsigned width, uint32_t value);
+  Z3ASTHandle bvConst64(unsigned width, uint64_t value);
+  Z3ASTHandle bvZExtConst(unsigned width, uint64_t value);
+  Z3ASTHandle bvSExtConst(unsigned width, uint64_t value);
+  Z3ASTHandle bvBoolExtract(Z3ASTHandle expr, int bit);
+  Z3ASTHandle bvExtract(Z3ASTHandle expr, unsigned top, unsigned bottom);
+  Z3ASTHandle eqExpr(Z3ASTHandle a, Z3ASTHandle b);
+
+  // logical left and right shift (not arithmetic)
+  Z3ASTHandle bvLeftShift(Z3ASTHandle expr, unsigned shift);
+  Z3ASTHandle bvRightShift(Z3ASTHandle expr, unsigned shift);
+  Z3ASTHandle bvVarLeftShift(Z3ASTHandle expr, Z3ASTHandle shift);
+  Z3ASTHandle bvVarRightShift(Z3ASTHandle expr, Z3ASTHandle shift);
+  Z3ASTHandle bvVarArithRightShift(Z3ASTHandle expr, Z3ASTHandle shift);
+
+  Z3ASTHandle notExpr(Z3ASTHandle expr);
+  Z3ASTHandle bvNotExpr(Z3ASTHandle expr);
+  Z3ASTHandle andExpr(Z3ASTHandle lhs, Z3ASTHandle rhs);
+  Z3ASTHandle bvAndExpr(Z3ASTHandle lhs, Z3ASTHandle rhs);
+  Z3ASTHandle orExpr(Z3ASTHandle lhs, Z3ASTHandle rhs);
+  Z3ASTHandle bvOrExpr(Z3ASTHandle lhs, Z3ASTHandle rhs);
+  Z3ASTHandle iffExpr(Z3ASTHandle lhs, Z3ASTHandle rhs);
+  Z3ASTHandle bvXorExpr(Z3ASTHandle lhs, Z3ASTHandle rhs);
+  Z3ASTHandle bvSignExtend(Z3ASTHandle src, unsigned width);
+
+  // Array operations
+  Z3ASTHandle writeExpr(Z3ASTHandle array, Z3ASTHandle index,
+                        Z3ASTHandle value);
+  Z3ASTHandle readExpr(Z3ASTHandle array, Z3ASTHandle index);
+
+  // ITE-expression constructor
+  Z3ASTHandle iteExpr(Z3ASTHandle condition, Z3ASTHandle whenTrue,
+                      Z3ASTHandle whenFalse);
+
+  // Bitvector length
+  unsigned getBVLength(Z3ASTHandle expr);
+
+  // Bitvector comparison
+  Z3ASTHandle bvLtExpr(Z3ASTHandle lhs, Z3ASTHandle rhs);
+  Z3ASTHandle bvLeExpr(Z3ASTHandle lhs, Z3ASTHandle rhs);
+  Z3ASTHandle sbvLtExpr(Z3ASTHandle lhs, Z3ASTHandle rhs);
+  Z3ASTHandle sbvLeExpr(Z3ASTHandle lhs, Z3ASTHandle rhs);
+
+  Z3ASTHandle constructAShrByConstant(Z3ASTHandle expr, unsigned shift,
+                                      Z3ASTHandle isSigned);
+
+  Z3ASTHandle getInitialArray(const Array *os);
+  Z3ASTHandle getArrayForUpdate(const Array *root, const UpdateNode *un);
+
+  Z3ASTHandle constructActual(ref<Expr> e, int *width_out);
+  Z3ASTHandle construct(ref<Expr> e, int *width_out);
+
+  Z3ASTHandle buildArray(const char *name, unsigned indexWidth,
+                         unsigned valueWidth);
+
+  Z3SortHandle getBvSort(unsigned width);
+  Z3SortHandle getArraySort(Z3SortHandle domainSort, Z3SortHandle rangeSort);
+  bool autoClearConstructCache;
+
+public:
+  Z3_context ctx;
+
+  Z3Builder(bool autoClearConstructCache = true);
+  ~Z3Builder();
+
+  Z3ASTHandle getTrue();
+  Z3ASTHandle getFalse();
+  Z3ASTHandle getInitialRead(const Array *os, unsigned index);
+
+  Z3ASTHandle construct(ref<Expr> e) {
+    Z3ASTHandle res = construct(e, 0);
+    if (autoClearConstructCache)
+      clearConstructCache();
+    return res;
+  }
+
+  void clearConstructCache() { constructed.clear(); }
+};
+}
+
+#endif
diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp
new file mode 100644
index 00000000..994386ab
--- /dev/null
+++ b/lib/Solver/Z3Solver.cpp
@@ -0,0 +1,299 @@
+//===-- Z3Solver.cpp -------------------------------------------*- C++ -*-====//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+#include "klee/Config/config.h"
+#ifdef ENABLE_Z3
+#include "Z3Builder.h"
+#include "klee/Constraints.h"
+#include "klee/Solver.h"
+#include "klee/SolverImpl.h"
+#include "klee/util/Assignment.h"
+#include "klee/util/ExprUtil.h"
+
+namespace klee {
+
+class Z3SolverImpl : public SolverImpl {
+private:
+  Z3Builder *builder;
+  double timeout;
+  SolverRunStatus runStatusCode;
+  ::Z3_params solverParameters;
+  // Parameter symbols
+  ::Z3_symbol timeoutParamStrSymbol;
+
+  bool internalRunSolver(const Query &,
+                         const std::vector<const Array *> *objects,
+                         std::vector<std::vector<unsigned char> > *values,
+                         bool &hasSolution);
+
+public:
+  Z3SolverImpl();
+  ~Z3SolverImpl();
+
+  char *getConstraintLog(const Query &);
+  void setCoreSolverTimeout(double _timeout) {
+    assert(_timeout >= 0.0 && "timeout must be >= 0");
+    timeout = _timeout;
+
+    unsigned int timeoutInMilliSeconds = (unsigned int)((timeout * 1000) + 0.5);
+    if (timeoutInMilliSeconds == 0)
+      timeoutInMilliSeconds = UINT_MAX;
+    Z3_params_set_uint(builder->ctx, solverParameters, timeoutParamStrSymbol,
+                       timeoutInMilliSeconds);
+  }
+
+  bool computeTruth(const Query &, bool &isValid);
+  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);
+  SolverRunStatus
+  handleSolverResponse(::Z3_solver theSolver, ::Z3_lbool satisfiable,
+                       const std::vector<const Array *> *objects,
+                       std::vector<std::vector<unsigned char> > *values,
+                       bool &hasSolution);
+  SolverRunStatus getOperationStatusCode();
+};
+
+Z3SolverImpl::Z3SolverImpl()
+    : builder(new Z3Builder(/*autoClearConstructCache=*/false)), timeout(0.0),
+      runStatusCode(SOLVER_RUN_STATUS_FAILURE) {
+  assert(builder && "unable to create Z3Builder");
+  solverParameters = Z3_mk_params(builder->ctx);
+  Z3_params_inc_ref(builder->ctx, solverParameters);
+  timeoutParamStrSymbol = Z3_mk_string_symbol(builder->ctx, "timeout");
+  setCoreSolverTimeout(timeout);
+}
+
+Z3SolverImpl::~Z3SolverImpl() {
+  Z3_params_dec_ref(builder->ctx, solverParameters);
+  delete builder;
+}
+
+Z3Solver::Z3Solver() : Solver(new Z3SolverImpl()) {}
+
+char *Z3Solver::getConstraintLog(const Query &query) {
+  return impl->getConstraintLog(query);
+}
+
+void Z3Solver::setCoreSolverTimeout(double timeout) {
+  impl->setCoreSolverTimeout(timeout);
+}
+
+char *Z3SolverImpl::getConstraintLog(const Query &query) {
+  std::vector<Z3ASTHandle> assumptions;
+  for (std::vector<ref<Expr> >::const_iterator it = query.constraints.begin(),
+                                               ie = query.constraints.end();
+       it != ie; ++it) {
+    assumptions.push_back(builder->construct(*it));
+  }
+  ::Z3_ast *assumptionsArray = NULL;
+  int numAssumptions = query.constraints.size();
+  if (numAssumptions) {
+    assumptionsArray = (::Z3_ast *)malloc(sizeof(::Z3_ast) * numAssumptions);
+    for (int index = 0; index < numAssumptions; ++index) {
+      assumptionsArray[index] = (::Z3_ast)assumptions[index];
+    }
+  }
+
+  // KLEE Queries are validity queries i.e.
+  // ∀ X Constraints(X) → query(X)
+  // but Z3 works in terms of satisfiability so instead we ask the
+  // the negation of the equivalent i.e.
+  // ∃ X Constraints(X) ∧ ¬ query(X)
+  Z3ASTHandle formula = Z3ASTHandle(
+      Z3_mk_not(builder->ctx, builder->construct(query.expr)), builder->ctx);
+
+  ::Z3_string result = Z3_benchmark_to_smtlib_string(
+      builder->ctx,
+      /*name=*/"Emited by klee::Z3SolverImpl::getConstraintLog()",
+      /*logic=*/"",
+      /*status=*/"unknown",
+      /*attributes=*/"",
+      /*num_assumptions=*/numAssumptions,
+      /*assumptions=*/assumptionsArray,
+      /*formula=*/formula);
+
+  if (numAssumptions)
+    free(assumptionsArray);
+  // Client is responsible for freeing the returned C-string
+  return strdup(result);
+}
+
+bool Z3SolverImpl::computeTruth(const Query &query, bool &isValid) {
+  bool hasSolution;
+  bool status =
+      internalRunSolver(query, /*objects=*/NULL, /*values=*/NULL, hasSolution);
+  isValid = !hasSolution;
+  return status;
+}
+
+bool Z3SolverImpl::computeValue(const Query &query, ref<Expr> &result) {
+  std::vector<const Array *> objects;
+  std::vector<std::vector<unsigned char> > values;
+  bool hasSolution;
+
+  // Find the object used in the expression, and compute an assignment
+  // for them.
+  findSymbolicObjects(query.expr, objects);
+  if (!computeInitialValues(query.withFalse(), objects, values, hasSolution))
+    return false;
+  assert(hasSolution && "state has invalid constraint set");
+
+  // Evaluate the expression with the computed assignment.
+  Assignment a(objects, values);
+  result = a.evaluate(query.expr);
+
+  return true;
+}
+
+bool Z3SolverImpl::computeInitialValues(
+    const Query &query, const std::vector<const Array *> &objects,
+    std::vector<std::vector<unsigned char> > &values, bool &hasSolution) {
+  return internalRunSolver(query, &objects, &values, hasSolution);
+}
+
+bool Z3SolverImpl::internalRunSolver(
+    const Query &query, const std::vector<const Array *> *objects,
+    std::vector<std::vector<unsigned char> > *values, bool &hasSolution) {
+  TimerStatIncrementer t(stats::queryTime);
+  // TODO: Does making a new solver for each query have a performance
+  // impact vs making one global solver and using push and pop?
+  // TODO: is the "simple_solver" the right solver to use for
+  // best performance?
+  Z3_solver theSolver = Z3_mk_simple_solver(builder->ctx);
+  Z3_solver_inc_ref(builder->ctx, theSolver);
+  Z3_solver_set_params(builder->ctx, theSolver, solverParameters);
+
+  runStatusCode = SOLVER_RUN_STATUS_FAILURE;
+
+  for (ConstraintManager::const_iterator it = query.constraints.begin(),
+                                         ie = query.constraints.end();
+       it != ie; ++it) {
+    Z3_solver_assert(builder->ctx, theSolver, builder->construct(*it));
+  }
+  ++stats::queries;
+  if (objects)
+    ++stats::queryCounterexamples;
+
+  Z3ASTHandle z3QueryExpr =
+      Z3ASTHandle(builder->construct(query.expr), builder->ctx);
+
+  // KLEE Queries are validity queries i.e.
+  // ∀ X Constraints(X) → query(X)
+  // but Z3 works in terms of satisfiability so instead we ask the
+  // negation of the equivalent i.e.
+  // ∃ X Constraints(X) ∧ ¬ query(X)
+  Z3_solver_assert(
+      builder->ctx, theSolver,
+      Z3ASTHandle(Z3_mk_not(builder->ctx, z3QueryExpr), builder->ctx));
+
+  ::Z3_lbool satisfiable = Z3_solver_check(builder->ctx, theSolver);
+  runStatusCode = handleSolverResponse(theSolver, satisfiable, objects, values,
+                                       hasSolution);
+
+  Z3_solver_dec_ref(builder->ctx, theSolver);
+  // Clear the builder's cache to prevent memory usage exploding.
+  // By using ``autoClearConstructCache=false`` and clearning now
+  // we allow Z3_ast expressions to be shared from an entire
+  // ``Query`` rather than only sharing within a single call to
+  // ``builder->construct()``.
+  builder->clearConstructCache();
+
+  if (runStatusCode == SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE ||
+      runStatusCode == SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE) {
+    if (hasSolution) {
+      ++stats::queriesInvalid;
+    } else {
+      ++stats::queriesValid;
+    }
+    return true; // success
+  }
+  return false; // failed
+}
+
+SolverImpl::SolverRunStatus Z3SolverImpl::handleSolverResponse(
+    ::Z3_solver theSolver, ::Z3_lbool satisfiable,
+    const std::vector<const Array *> *objects,
+    std::vector<std::vector<unsigned char> > *values, bool &hasSolution) {
+  switch (satisfiable) {
+  case Z3_L_TRUE: {
+    hasSolution = true;
+    if (!objects) {
+      // No assignment is needed
+      assert(values == NULL);
+      return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE;
+    }
+    assert(values && "values cannot be nullptr");
+    ::Z3_model theModel = Z3_solver_get_model(builder->ctx, theSolver);
+    assert(theModel && "Failed to retrieve model");
+    Z3_model_inc_ref(builder->ctx, theModel);
+    values->reserve(objects->size());
+    for (std::vector<const Array *>::const_iterator it = objects->begin(),
+                                                    ie = objects->end();
+         it != ie; ++it) {
+      const Array *array = *it;
+      std::vector<unsigned char> data;
+
+      data.reserve(array->size);
+      for (unsigned offset = 0; offset < array->size; offset++) {
+        // We can't use Z3ASTHandle here so have to do ref counting manually
+        ::Z3_ast arrayElementExpr;
+        Z3ASTHandle initial_read = builder->getInitialRead(array, offset);
+
+        bool successfulEval =
+            Z3_model_eval(builder->ctx, theModel, initial_read,
+                          /*model_completion=*/Z3_TRUE, &arrayElementExpr);
+        assert(successfulEval && "Failed to evaluate model");
+        Z3_inc_ref(builder->ctx, arrayElementExpr);
+        assert(Z3_get_ast_kind(builder->ctx, arrayElementExpr) ==
+                   Z3_NUMERAL_AST &&
+               "Evaluated expression has wrong sort");
+
+        int arrayElementValue = 0;
+        bool successGet = Z3_get_numeral_int(builder->ctx, arrayElementExpr,
+                                             &arrayElementValue);
+        assert(successGet && "failed to get value back");
+        assert(arrayElementValue >= 0 && arrayElementValue <= 255 &&
+               "Integer from model is out of range");
+        data.push_back(arrayElementValue);
+        Z3_dec_ref(builder->ctx, arrayElementExpr);
+      }
+      values->push_back(data);
+    }
+
+    Z3_model_dec_ref(builder->ctx, theModel);
+    return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE;
+  }
+  case Z3_L_FALSE:
+    hasSolution = false;
+    return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE;
+  case Z3_L_UNDEF: {
+    ::Z3_string reason =
+        ::Z3_solver_get_reason_unknown(builder->ctx, theSolver);
+    if (strcmp(reason, "timeout") == 0 || strcmp(reason, "canceled") == 0) {
+      return SolverImpl::SOLVER_RUN_STATUS_TIMEOUT;
+    }
+    if (strcmp(reason, "unknown") == 0) {
+      return SolverImpl::SOLVER_RUN_STATUS_FAILURE;
+    }
+    llvm::errs() << "Unexpected solver failure. Reason is \"" << reason
+                 << "\"\n";
+    abort();
+  }
+  default:
+    llvm_unreachable("unhandled Z3 result");
+  }
+}
+
+SolverImpl::SolverRunStatus Z3SolverImpl::getOperationStatusCode() {
+  return runStatusCode;
+}
+}
+#endif // ENABLE_Z3
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-22 03:21:16 +0000